%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM033-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:11:37 PM UTC 2026
% Result : Unsatisfiable 125.33s 33.10s
% Output : Refutation 228.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 44
% Syntax : Number of formulae : 173 ( 53 unt; 16 def)
% Number of atoms : 421 ( 51 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 480 ( 232 ~; 241 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 11 con; 0-3 aty)
% Number of variables : 230 ( 0 sgn 230 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f11,axiom,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pairs_in_universal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f38,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(ordered_pair(X0,X1),X2),X3)
| ~ member(ordered_pair(ordered_pair(X1,X0),X2),cross_product(cross_product(universal_class,universal_class),universal_class))
| member(ordered_pair(ordered_pair(X1,X0),X2),flip(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip3) ).
fof(f39,axiom,
! [X0] : domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,axiom,
! [X0] : union(X0,inverse(X0)) = symmetrization_of(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetrization) ).
fof(f176,negated_conjecture,
subclass(x,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_symmetrization_property6_1) ).
fof(f177,negated_conjecture,
symmetrization_of(x) = x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_symmetrization_property6_2) ).
fof(f178,plain,
x = symmetrization_of(x),
inference(reorient_equations,[],[f177]) ).
fof(f179,negated_conjecture,
inverse(x) != x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_symmetrization_property6_3) ).
fof(f180,plain,
x != inverse(x),
inference(reorient_equations,[],[f179]) ).
fof(f181,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f194,plain,
! [X0] : symmetrization_of(X0) = complement(intersection(complement(X0),complement(domain_of(flip(cross_product(X0,universal_class)))))),
inference(definition_unfolding,[],[f122,f26,f39]) ).
fof(f198,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f181]) ).
fof(f199,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f181]) ).
fof(f200,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f181]) ).
fof(f201,plain,
! [X2,X0,X1] :
( unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0
| ~ member(X0,cross_product(X1,X2)) ),
inference(definition_unfolding,[],[f17,f181]) ).
fof(f206,plain,
! [X0,X1] :
( null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f210,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3)) ),
inference(definition_unfolding,[],[f38,f181,f181,f181,f181,f181,f181]) ).
fof(f271,plain,
x = complement(intersection(complement(x),complement(domain_of(flip(cross_product(x,universal_class)))))),
inference(definition_unfolding,[],[f178,f194]) ).
fof(f272,plain,
x != domain_of(flip(cross_product(x,universal_class))),
inference(definition_unfolding,[],[f180,f39]) ).
fof(f281,definition,
~ sP4(x),
introduced(definition,[new_symbols(definition,[sP4])],[inequality_splitting_name_introduction]) ).
fof(f282,plain,
sP4(domain_of(flip(cross_product(x,universal_class)))),
inference(inequality_splitting,[],[f272,f281]) ).
fof(f289,definition,
sF5 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f290,plain,
cross_product(universal_class,universal_class) = sF5,
inference(reorient_equations,[],[f289]) ).
fof(f291,plain,
subclass(x,sF5),
inference(definition_folding,[],[f176,f290]) ).
fof(f292,definition,
sF6 = complement(x),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f293,plain,
complement(x) = sF6,
inference(reorient_equations,[],[f292]) ).
fof(f294,definition,
sF7 = cross_product(x,universal_class),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f295,plain,
cross_product(x,universal_class) = sF7,
inference(reorient_equations,[],[f294]) ).
fof(f296,definition,
sF8 = flip(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f297,plain,
flip(sF7) = sF8,
inference(reorient_equations,[],[f296]) ).
fof(f298,definition,
sF9 = domain_of(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f299,plain,
domain_of(sF8) = sF9,
inference(reorient_equations,[],[f298]) ).
fof(f300,definition,
sF10 = complement(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f301,plain,
complement(sF9) = sF10,
inference(reorient_equations,[],[f300]) ).
fof(f302,definition,
sF11 = intersection(sF6,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f303,plain,
intersection(sF6,sF10) = sF11,
inference(reorient_equations,[],[f302]) ).
fof(f304,definition,
sF12 = complement(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f305,plain,
complement(sF11) = sF12,
inference(reorient_equations,[],[f304]) ).
fof(f306,plain,
x = sF12,
inference(definition_folding,[],[f271,f305,f303,f301,f299,f297,f295,f293]) ).
fof(f307,plain,
sP4(sF9),
inference(definition_folding,[],[f282,f299,f297,f295]) ).
fof(f308,plain,
subclass(x,cross_product(universal_class,universal_class)),
inference(backward_demodulation,[],[f291,f290]) ).
fof(f309,plain,
flip(cross_product(x,universal_class)) = sF8,
inference(forward_demodulation,[],[f297,f295]) ).
fof(f310,plain,
x = complement(sF11),
inference(forward_demodulation,[],[f305,f306]) ).
fof(f316,plain,
! [X0] :
( ~ member(X0,sF10)
| ~ member(X0,sF9) ),
inference(superposition,[],[f24,f301]) ).
fof(f320,plain,
! [X0] :
( member(X0,sF11)
| ~ member(X0,universal_class)
| member(X0,x) ),
inference(superposition,[],[f25,f310]) ).
fof(f328,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f347,plain,
! [X0] :
( member(X0,sF10)
| ~ member(X0,sF11) ),
inference(superposition,[],[f22,f303]) ).
fof(f352,plain,
! [X0] :
( ~ member(X0,sF11)
| ~ member(X0,sF9) ),
inference(resolution,[],[f347,f316]) ).
fof(f355,plain,
! [X0] :
( member(X0,x)
| ~ member(X0,universal_class)
| ~ member(X0,sF9) ),
inference(resolution,[],[f352,f320]) ).
fof(f358,plain,
! [X0] :
( ~ member(not_subclass_element(X0,x),sF9)
| ~ member(not_subclass_element(X0,x),universal_class)
| subclass(X0,x) ),
inference(resolution,[],[f355,f3]) ).
fof(f360,plain,
( ~ member(not_subclass_element(sF9,x),universal_class)
| subclass(sF9,x)
| subclass(sF9,x) ),
inference(resolution,[],[f358,f2]) ).
fof(f362,plain,
( ~ member(not_subclass_element(sF9,x),universal_class)
| subclass(sF9,x) ),
inference(duplicate_literal_removal,[],[f360]) ).
fof(f364,definition,
( spl13_1
<=> subclass(sF9,x) ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
fof(f365,plain,
( ~ subclass(sF9,x)
| spl13_1 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl13_2
<=> member(not_subclass_element(sF9,x),universal_class) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
fof(f370,plain,
( ~ member(not_subclass_element(sF9,x),universal_class)
| spl13_2 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,plain,
( spl13_1
| ~ spl13_2 ),
inference(avatar_split_clause,[],[f362,f368,f364]) ).
fof(f401,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(second(X0),X2)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f199,f201]) ).
fof(f403,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(first(X0),X1)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f198,f201]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),X1) ),
inference(factoring,[],[f403]) ).
fof(f407,plain,
! [X2,X3,X0,X1] :
( ~ subclass(X2,cross_product(X1,X3))
| ~ member(X0,X2)
| member(first(X0),X1) ),
inference(resolution,[],[f406,f1]) ).
fof(f411,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(second(X0),X2) ),
inference(factoring,[],[f401]) ).
fof(f412,plain,
! [X2,X3,X0,X1] :
( ~ subclass(X2,cross_product(X3,X1))
| ~ member(X0,X2)
| member(second(X0),X1) ),
inference(resolution,[],[f411,f1]) ).
fof(f414,plain,
! [X0] :
( member(first(X0),universal_class)
| ~ member(X0,x) ),
inference(resolution,[],[f407,f308]) ).
fof(f430,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(unordered_pair(X2,X2),universal_class))
| member(X0,null_class)
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1)) ),
inference(superposition,[],[f23,f206]) ).
fof(f445,plain,
! [X0] :
( member(second(X0),universal_class)
| ~ member(X0,x) ),
inference(resolution,[],[f412,f308]) ).
fof(f476,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f328,f3]) ).
fof(f495,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f476]) ).
fof(f791,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),cross_product(universal_class,universal_class)) ),
inference(resolution,[],[f210,f200]) ).
fof(f1126,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),sF8)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(x,universal_class))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class)) ),
inference(superposition,[],[f791,f309]) ).
fof(f1128,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(x,universal_class))
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),sF8)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class)) ),
inference(forward_subsumption_resolution,[],[f1126,f199]) ).
fof(f1497,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f495,f70]) ).
fof(f1502,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f1497,f7]) ).
fof(f1503,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f1502]) ).
fof(f1505,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f1503,f495]) ).
fof(f1523,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,null_class) ),
inference(superposition,[],[f22,f1505]) ).
fof(f1548,plain,
! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,sF9) ),
inference(resolution,[],[f1523,f352]) ).
fof(f1559,plain,
! [X0] : ~ member(X0,null_class),
inference(forward_subsumption_resolution,[],[f1548,f1523]) ).
fof(f1615,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(resolution,[],[f430,f200]) ).
fof(f1626,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(forward_subsumption_resolution,[],[f1615,f1559]) ).
fof(f2117,definition,
( spl13_46
<=> ! [X1] : ~ member(X1,universal_class) ),
introduced(definition,[new_symbols(definition,[spl13_46])],[avatar_definition]) ).
fof(f2118,plain,
( ! [X1] : ~ member(X1,universal_class)
| ~ spl13_46 ),
inference(avatar_component_clause,[],[f2117]) ).
fof(f2743,definition,
( spl13_75
<=> subclass(x,sF9) ),
introduced(definition,[new_symbols(definition,[spl13_75])],[avatar_definition]) ).
fof(f2744,plain,
( ~ subclass(x,sF9)
| spl13_75 ),
inference(avatar_component_clause,[],[f2743]) ).
fof(f2745,plain,
( subclass(x,sF9)
| ~ spl13_75 ),
inference(avatar_component_clause,[],[f2743]) ).
fof(f2747,definition,
( spl13_76
<=> member(not_subclass_element(x,sF9),universal_class) ),
introduced(definition,[new_symbols(definition,[spl13_76])],[avatar_definition]) ).
fof(f2748,plain,
( member(not_subclass_element(x,sF9),universal_class)
| ~ spl13_76 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2749,plain,
( ~ member(not_subclass_element(x,sF9),universal_class)
| spl13_76 ),
inference(avatar_component_clause,[],[f2747]) ).
fof(f2774,plain,
( ! [X0] :
( ~ member(not_subclass_element(x,sF9),X0)
| ~ subclass(X0,universal_class) )
| spl13_76 ),
inference(resolution,[],[f2749,f1]) ).
fof(f2775,plain,
( ! [X0] : ~ member(not_subclass_element(x,sF9),X0)
| spl13_76 ),
inference(forward_subsumption_resolution,[],[f2774,f4]) ).
fof(f2776,plain,
( subclass(x,sF9)
| spl13_76 ),
inference(resolution,[],[f2775,f2]) ).
fof(f2797,plain,
( spl13_75
| spl13_76 ),
inference(avatar_split_clause,[],[f2776,f2747,f2743]) ).
fof(f2798,plain,
( ~ subclass(sF9,x)
| x = sF9
| ~ spl13_75 ),
inference(resolution,[],[f2745,f7]) ).
fof(f2800,definition,
( spl13_77
<=> x = sF9 ),
introduced(definition,[new_symbols(definition,[spl13_77])],[avatar_definition]) ).
fof(f2802,plain,
( x = sF9
| ~ spl13_77 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2803,plain,
( spl13_77
| ~ spl13_1
| ~ spl13_75 ),
inference(avatar_split_clause,[],[f2798,f2743,f364,f2800]) ).
fof(f3046,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF9,x),X0)
| ~ subclass(X0,universal_class) )
| spl13_2 ),
inference(resolution,[],[f370,f1]) ).
fof(f3047,plain,
( ! [X0] : ~ member(not_subclass_element(sF9,x),X0)
| spl13_2 ),
inference(forward_subsumption_resolution,[],[f3046,f4]) ).
fof(f3048,plain,
( subclass(sF9,x)
| spl13_2 ),
inference(resolution,[],[f3047,f2]) ).
fof(f3069,plain,
( $false
| spl13_1
| spl13_2 ),
inference(forward_subsumption_resolution,[],[f3048,f365]) ).
fof(f3070,plain,
( spl13_1
| spl13_2 ),
inference(avatar_contradiction_clause,[],[f3069]) ).
fof(f3182,plain,
( sP4(x)
| ~ spl13_77 ),
inference(backward_demodulation,[],[f307,f2802]) ).
fof(f3299,plain,
( $false
| ~ spl13_77 ),
inference(forward_subsumption_resolution,[],[f3182,f281]) ).
fof(f3300,plain,
~ spl13_77,
inference(avatar_contradiction_clause,[],[f3299]) ).
fof(f3832,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),sF8)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ),
inference(resolution,[],[f1128,f200]) ).
fof(f3844,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X3,universal_class)
| member(X3,domain_of(sF8))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X3,X3)) ),
inference(resolution,[],[f3832,f1626]) ).
fof(f3848,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X3,universal_class)
| member(X3,domain_of(sF8))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X3,X3)) ),
inference(duplicate_literal_removal,[],[f3844]) ).
fof(f3855,plain,
! [X2,X3,X0,X1] :
( member(X3,sF9)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X3,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X3,X3)) ),
inference(forward_demodulation,[],[f3848,f299]) ).
fof(f3869,definition,
( spl13_93
<=> ! [X0,X1,X3] :
( member(X3,sF9)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X3,X3))
| ~ member(X3,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ) ),
introduced(definition,[new_symbols(definition,[spl13_93])],[avatar_definition]) ).
fof(f3870,plain,
( ! [X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X3,X3))
| ~ member(X3,universal_class)
| member(X3,sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) )
| ~ spl13_93 ),
inference(avatar_component_clause,[],[f3869]) ).
fof(f3871,plain,
( spl13_46
| spl13_93 ),
inference(avatar_split_clause,[],[f3855,f3869,f2117]) ).
fof(f3883,plain,
( $false
| ~ spl13_46
| ~ spl13_76 ),
inference(resolution,[],[f2118,f2748]) ).
fof(f3899,plain,
( ~ spl13_46
| ~ spl13_76 ),
inference(avatar_contradiction_clause,[],[f3883]) ).
fof(f4467,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))
| ~ member(X2,universal_class)
| member(X2,sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) )
| ~ spl13_93 ),
inference(resolution,[],[f3870,f200]) ).
fof(f4483,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class) )
| ~ spl13_93 ),
inference(resolution,[],[f4467,f9]) ).
fof(f4486,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) )
| ~ spl13_93 ),
inference(duplicate_literal_removal,[],[f4483]) ).
fof(f4487,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) )
| ~ spl13_93 ),
inference(forward_subsumption_resolution,[],[f4486,f11]) ).
fof(f4508,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),x)
| member(X0,sF9)
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2)) )
| ~ spl13_93 ),
inference(superposition,[],[f4487,f201]) ).
fof(f4557,plain,
( ! [X2,X0,X1] :
( member(X0,sF9)
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2))
| ~ member(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),universal_class)
| ~ member(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),sF9) )
| ~ spl13_93 ),
inference(resolution,[],[f4508,f355]) ).
fof(f4559,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),sF9)
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9) )
| ~ spl13_93 ),
inference(forward_subsumption_resolution,[],[f4557,f11]) ).
fof(f5644,plain,
( ! [X2,X0,X1] :
( ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))),x)
| ~ member(first(X0),universal_class)
| ~ member(second(X0),universal_class) )
| ~ spl13_93 ),
inference(resolution,[],[f4559,f4487]) ).
fof(f5648,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))),x)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(second(X0),universal_class) )
| ~ spl13_93 ),
inference(duplicate_literal_removal,[],[f5644]) ).
fof(f5655,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ member(X0,x)
| ~ member(first(X0),universal_class)
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(second(X0),universal_class)
| ~ member(X0,cross_product(X3,X4)) )
| ~ spl13_93 ),
inference(superposition,[],[f5648,f201]) ).
fof(f5656,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ member(X0,x)
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(second(X0),universal_class)
| ~ member(X0,cross_product(X3,X4)) )
| ~ spl13_93 ),
inference(forward_subsumption_resolution,[],[f5655,f414]) ).
fof(f5659,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(X0,x) )
| ~ spl13_93 ),
inference(forward_subsumption_resolution,[],[f5656,f445]) ).
fof(f5674,plain,
( ! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(X0,sF9)
| ~ member(X0,x) )
| ~ spl13_93 ),
inference(factoring,[],[f5659]) ).
fof(f5678,plain,
( ! [X2,X3,X0,X1] :
( ~ subclass(X1,cross_product(X2,X3))
| ~ member(X0,x)
| ~ member(X0,X1)
| member(X0,sF9) )
| ~ spl13_93 ),
inference(resolution,[],[f5674,f1]) ).
fof(f5694,plain,
( ! [X0] :
( ~ member(X0,x)
| ~ member(X0,x)
| member(X0,sF9) )
| ~ spl13_93 ),
inference(resolution,[],[f5678,f308]) ).
fof(f5696,plain,
( ! [X0] :
( member(X0,sF9)
| ~ member(X0,x) )
| ~ spl13_93 ),
inference(duplicate_literal_removal,[],[f5694]) ).
fof(f5698,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF9),x)
| subclass(X0,sF9) )
| ~ spl13_93 ),
inference(resolution,[],[f5696,f3]) ).
fof(f5751,plain,
( subclass(x,sF9)
| subclass(x,sF9)
| ~ spl13_93 ),
inference(resolution,[],[f5698,f2]) ).
fof(f5759,plain,
( subclass(x,sF9)
| ~ spl13_93 ),
inference(duplicate_literal_removal,[],[f5751]) ).
fof(f5760,plain,
( $false
| spl13_75
| ~ spl13_93 ),
inference(forward_subsumption_resolution,[],[f5759,f2744]) ).
fof(f5761,plain,
( spl13_75
| ~ spl13_93 ),
inference(avatar_contradiction_clause,[],[f5760]) ).
cnf(s1,plain,
( spl13_1
| ~ spl13_2 ),
inference(sat_conversion,[],[f371]) ).
cnf(s52,plain,
( spl13_75
| spl13_76 ),
inference(sat_conversion,[],[f2797]) ).
cnf(s53,plain,
( ~ spl13_1
| ~ spl13_75
| spl13_77 ),
inference(sat_conversion,[],[f2803]) ).
cnf(s56,plain,
( spl13_1
| spl13_2 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s61,plain,
~ spl13_77,
inference(sat_conversion,[],[f3300]) ).
cnf(s67,plain,
( spl13_46
| spl13_93 ),
inference(sat_conversion,[],[f3871]) ).
cnf(s69,plain,
( ~ spl13_46
| ~ spl13_76 ),
inference(sat_conversion,[],[f3899]) ).
cnf(s105,plain,
( spl13_75
| ~ spl13_93 ),
inference(sat_conversion,[],[f5761]) ).
cnf(s107,plain,
( ~ spl13_1
| ~ spl13_75 ),
inference(rat,[],[s53,s61]) ).
cnf(s108,plain,
spl13_1,
inference(rat,[],[s1,s56]) ).
cnf(s109,plain,
~ spl13_75,
inference(rat,[],[s107,s108]) ).
cnf(s110,plain,
~ spl13_93,
inference(rat,[],[s105,s109]) ).
cnf(s111,plain,
spl13_76,
inference(rat,[],[s52,s109]) ).
cnf(s113,plain,
spl13_46,
inference(rat,[],[s67,s110]) ).
cnf(s114,plain,
$false,
inference(rat,[],[s69,s111,s113]) ).
fof(f5764,plain,
$false,
inference(avatar_sat_refutation,[],[s114]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM033-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 18:47:16 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 12.54/2.64 % (3887158)Input is clausal, will run a generic CNF schedule.
% 12.54/2.64 % (3887163)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=2998054561:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.54/2.64 % (3887168)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1419281342:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.54/2.64 % (3887164)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2554264580:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.54/2.64 % (3887165)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3315873765:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.54/2.64 % (3887167)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1108168066:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.54/2.64 % (3887166)lrs+10_1_sil=8000:sp=occurrence:random_seed=2101566970:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.54/2.64 % (3887169)dis-21_1_sil=8000:lcm=predicate:random_seed=1604593310: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)
% 12.54/2.64 % (3887166)Instruction limit reached!
% 12.54/2.64 % (3887166)------------------------------
% 12.54/2.64 % (3887166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.64 % (3887166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.64 % (3887166)CaDiCaL version: 2.1.3
% 12.54/2.64 % (3887166)Termination reason: Instruction limit
% 12.54/2.64 % (3887166)Termination phase: Saturation
% 12.54/2.64 % (3887166)Time elapsed: 0.070 s
% 12.54/2.64 % (3887166)Peak memory usage: 89 MB
% 12.54/2.64 % (3887166)Instructions burned: 108 (million)
% 12.54/2.64 % (3887167)Instruction limit reached!
% 12.54/2.64 % (3887167)------------------------------
% 12.54/2.64 % (3887167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.64 % (3887167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.64 % (3887167)CaDiCaL version: 2.1.3
% 12.54/2.64 % (3887167)Termination reason: Instruction limit
% 12.54/2.64 % (3887167)Termination phase: Saturation
% 12.54/2.64 % (3887167)Time elapsed: 0.070 s
% 12.54/2.64 % (3887167)Peak memory usage: 89 MB
% 12.54/2.64 % (3887167)Instructions burned: 114 (million)
% 12.54/2.64 % (3887169)Instruction limit reached!
% 12.54/2.64 % (3887169)------------------------------
% 12.54/2.64 % (3887169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.64 % (3887169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.64 % (3887169)CaDiCaL version: 2.1.3
% 12.54/2.64 % (3887169)Termination reason: Instruction limit
% 12.54/2.64 % (3887169)Termination phase: Saturation
% 12.54/2.64 % (3887169)Time elapsed: 0.072 s
% 12.54/2.64 % (3887169)Peak memory usage: 89 MB
% 12.54/2.64 % (3887169)Instructions burned: 118 (million)
% 12.54/2.64 % (3887168)Instruction limit reached!
% 12.54/2.64 % (3887168)------------------------------
% 12.54/2.64 % (3887168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.64 % (3887168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.64 % (3887168)CaDiCaL version: 2.1.3
% 12.54/2.64 % (3887168)Termination reason: Instruction limit
% 12.54/2.64 % (3887168)Termination phase: Saturation
% 12.54/2.64 % (3887168)Time elapsed: 0.139 s
% 12.54/2.64 % (3887168)Peak memory usage: 90 MB
% 12.54/2.64 % (3887168)Instructions burned: 180 (million)
% 12.54/2.64 % (3887177)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=3569108479:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.54/2.64 % (3887178)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3085915533:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 12.54/2.64 % (3887177)Refutation not found, incomplete strategy
% 12.54/2.64 % (3887177)------------------------------
% 12.54/2.64 % (3887177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.64 % (3887177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.64 % (3887177)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887177)Termination reason: Refutation not found, incomplete strategy
% 21.38/4.02 % (3887177)Time elapsed: 0.003 s
% 21.38/4.02 % (3887177)Peak memory usage: 88 MB
% 21.38/4.02 % (3887177)Instructions burned: 2 (million)
% 21.38/4.02 % (3887179)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3765273819:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 21.38/4.02 % (3887180)lrs+10_64_to=lpo:sil=8000:random_seed=3248521817:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.38/4.02 % (3887178)Instruction limit reached!
% 21.38/4.02 % (3887178)------------------------------
% 21.38/4.02 % (3887178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/4.02 % (3887178)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887178)Termination reason: Instruction limit
% 21.38/4.02 % (3887178)Termination phase: Saturation
% 21.38/4.02 % (3887178)Time elapsed: 0.108 s
% 21.38/4.02 % (3887178)Peak memory usage: 90 MB
% 21.38/4.02 % (3887178)Instructions burned: 190 (million)
% 21.38/4.02 % (3887180)Instruction limit reached!
% 21.38/4.02 % (3887180)------------------------------
% 21.38/4.02 % (3887180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/4.02 % (3887180)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887180)Termination reason: Instruction limit
% 21.38/4.02 % (3887180)Termination phase: Saturation
% 21.38/4.02 % (3887180)Time elapsed: 0.082 s
% 21.38/4.02 % (3887180)Peak memory usage: 89 MB
% 21.38/4.02 % (3887180)Instructions burned: 126 (million)
% 21.38/4.02 % (3887179)Instruction limit reached!
% 21.38/4.02 % (3887179)------------------------------
% 21.38/4.02 % (3887179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/4.02 % (3887179)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887179)Termination reason: Instruction limit
% 21.38/4.02 % (3887179)Termination phase: Saturation
% 21.38/4.02 % (3887179)Time elapsed: 0.142 s
% 21.38/4.02 % (3887179)Peak memory usage: 90 MB
% 21.38/4.02 % (3887179)Instructions burned: 220 (million)
% 21.38/4.02 % (3887177)------------------------------
% 21.38/4.02 % (3887177)------------------------------
% 21.38/4.02 % (3887185)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=611873116:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.38/4.02 % (3887186)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1837512818:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 21.38/4.02 % (3887187)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3566423877:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 21.38/4.02 % (3887185)Instruction limit reached!
% 21.38/4.02 % (3887185)------------------------------
% 21.38/4.02 % (3887185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/4.02 % (3887185)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887185)Termination reason: Instruction limit
% 21.38/4.02 % (3887185)Termination phase: Saturation
% 21.38/4.02 % (3887185)Time elapsed: 0.115 s
% 21.38/4.02 % (3887185)Peak memory usage: 89 MB
% 21.38/4.02 % (3887185)Instructions burned: 195 (million)
% 21.38/4.02 % (3887188)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=542341441:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 21.38/4.02 % (3887186)Instruction limit reached!
% 21.38/4.02 % (3887186)------------------------------
% 21.38/4.02 % (3887186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.38/4.02 % (3887186)CaDiCaL version: 2.1.3
% 21.38/4.02 % (3887186)Termination reason: Instruction limit
% 21.38/4.02 % (3887186)Termination phase: Saturation
% 21.38/4.02 % (3887186)Time elapsed: 0.111 s
% 21.38/4.02 % (3887186)Peak memory usage: 91 MB
% 21.38/4.02 % (3887186)Instructions burned: 158 (million)
% 21.38/4.02 % (3887188)Instruction limit reached!
% 21.38/4.02 % (3887188)------------------------------
% 21.38/4.02 % (3887188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.38/4.02 % (3887188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887188)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887188)Termination reason: Instruction limit
% 35.42/5.93 % (3887188)Termination phase: Saturation
% 35.42/5.93 % (3887188)Time elapsed: 0.065 s
% 35.42/5.93 % (3887188)Peak memory usage: 90 MB
% 35.42/5.93 % (3887188)Instructions burned: 106 (million)
% 35.42/5.93 % (3887192)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=545031176:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 35.42/5.93 % (3887194)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4249595589:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 35.42/5.93 % (3887192)Instruction limit reached!
% 35.42/5.93 % (3887192)------------------------------
% 35.42/5.93 % (3887192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/5.93 % (3887192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887192)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887192)Termination reason: Instruction limit
% 35.42/5.93 % (3887192)Termination phase: Saturation
% 35.42/5.93 % (3887192)Time elapsed: 0.073 s
% 35.42/5.93 % (3887192)Peak memory usage: 89 MB
% 35.42/5.93 % (3887192)Instructions burned: 108 (million)
% 35.42/5.93 % (3887195)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3766647358:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 35.42/5.93 % (3887194)Instruction limit reached!
% 35.42/5.93 % (3887194)------------------------------
% 35.42/5.93 % (3887194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/5.93 % (3887194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887194)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887194)Termination reason: Instruction limit
% 35.42/5.93 % (3887194)Termination phase: Saturation
% 35.42/5.93 % (3887194)Time elapsed: 0.166 s
% 35.42/5.93 % (3887194)Peak memory usage: 90 MB
% 35.42/5.93 % (3887194)Instructions burned: 243 (million)
% 35.42/5.93 % (3887198)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=192486443:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 35.42/5.93 % (3887198)Refutation not found, incomplete strategy
% 35.42/5.93 % (3887198)------------------------------
% 35.42/5.93 % (3887198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/5.93 % (3887198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887198)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887198)Termination reason: Refutation not found, incomplete strategy
% 35.42/5.93 % (3887198)Time elapsed: 0.002 s
% 35.42/5.93 % (3887198)Peak memory usage: 88 MB
% 35.42/5.93 % (3887198)Instructions burned: 2 (million)
% 35.42/5.93 % (3887200)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3233816473:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 35.42/5.93 % (3887198)------------------------------
% 35.42/5.93 % (3887198)------------------------------
% 35.42/5.93 % (3887203)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1797825636:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 35.42/5.93 % (3887200)Instruction limit reached!
% 35.42/5.93 % (3887200)------------------------------
% 35.42/5.93 % (3887200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/5.93 % (3887200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887200)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887200)Termination reason: Instruction limit
% 35.42/5.93 % (3887200)Termination phase: Saturation
% 35.42/5.93 % (3887200)Time elapsed: 0.313 s
% 35.42/5.93 % (3887200)Peak memory usage: 94 MB
% 35.42/5.93 % (3887200)Instructions burned: 499 (million)
% 35.42/5.93 % (3887203)Instruction limit reached!
% 35.42/5.93 % (3887203)------------------------------
% 35.42/5.93 % (3887203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/5.93 % (3887203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/5.93 % (3887203)CaDiCaL version: 2.1.3
% 35.42/5.93 % (3887203)Termination reason: Instruction limit
% 35.42/5.93 % (3887203)Termination phase: Saturation
% 35.42/5.93 % (3887203)Time elapsed: 0.107 s
% 35.42/5.93 % (3887203)Peak memory usage: 89 MB
% 35.42/5.93 % (3887203)Instructions burned: 191 (million)
% 35.42/5.93 % (3887205)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4251265083:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 55.65/8.89 % (3887206)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1498207511:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 55.65/8.89 % (3887205)Instruction limit reached!
% 55.65/8.89 % (3887205)------------------------------
% 55.65/8.89 % (3887205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.65/8.89 % (3887205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.65/8.89 % (3887205)CaDiCaL version: 2.1.3
% 55.65/8.89 % (3887205)Termination reason: Instruction limit
% 55.65/8.89 % (3887205)Termination phase: Saturation
% 55.65/8.89 % (3887205)Time elapsed: 0.172 s
% 55.65/8.89 % (3887205)Peak memory usage: 91 MB
% 55.65/8.89 % (3887205)Instructions burned: 265 (million)
% 55.65/8.89 % (3887206)Instruction limit reached!
% 55.65/8.89 % (3887206)------------------------------
% 55.65/8.89 % (3887206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.65/8.89 % (3887206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.65/8.89 % (3887206)CaDiCaL version: 2.1.3
% 55.65/8.89 % (3887206)Termination reason: Instruction limit
% 55.65/8.89 % (3887206)Termination phase: Saturation
% 55.65/8.89 % (3887206)Time elapsed: 0.092 s
% 55.65/8.89 % (3887206)Peak memory usage: 89 MB
% 55.65/8.89 % (3887206)Instructions burned: 156 (million)
% 55.65/8.89 % (3887209)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=2172996774:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 55.65/8.89 % (3887210)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=184586027:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 55.65/8.89 % (3887210)Refutation not found, incomplete strategy
% 55.65/8.89 % (3887210)------------------------------
% 55.65/8.89 % (3887210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.65/8.89 % (3887210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.65/8.89 % (3887210)CaDiCaL version: 2.1.3
% 55.65/8.89 % (3887210)Termination reason: Refutation not found, incomplete strategy
% 55.65/8.89 % (3887210)Time elapsed: 0.118 s
% 55.65/8.89 % (3887210)Peak memory usage: 89 MB
% 55.65/8.89 % (3887210)Instructions burned: 243 (million)
% 55.65/8.89 % (3887210)------------------------------
% 55.65/8.89 % (3887210)------------------------------
% 55.65/8.89 % (3887213)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1786245753:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 55.65/8.89 % (3887213)Instruction limit reached!
% 55.65/8.89 % (3887213)------------------------------
% 55.65/8.89 % (3887213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.65/8.89 % (3887213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.65/8.89 % (3887213)CaDiCaL version: 2.1.3
% 55.65/8.89 % (3887213)Termination reason: Instruction limit
% 55.65/8.89 % (3887213)Termination phase: Saturation
% 55.65/8.89 % (3887213)Time elapsed: 0.111 s
% 55.65/8.89 % (3887213)Peak memory usage: 90 MB
% 55.65/8.89 % (3887213)Instructions burned: 181 (million)
% 55.65/8.89 % (3887187)Instruction limit reached!
% 55.65/8.89 % (3887187)------------------------------
% 55.65/8.89 % (3887187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.65/8.89 % (3887187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.65/8.89 % (3887187)CaDiCaL version: 2.1.3
% 55.65/8.89 % (3887187)Termination reason: Instruction limit
% 55.65/8.89 % (3887187)Termination phase: Saturation
% 55.65/8.89 % (3887187)Time elapsed: 2.070 s
% 55.65/8.89 % (3887187)Peak memory usage: 145 MB
% 55.65/8.89 % (3887187)Instructions burned: 3394 (million)
% 55.65/8.89 % (3887216)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=2859894310:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 55.65/8.89 % (3887217)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=1209544230:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 55.65/8.89 % (3887217)Instruction limit reached!
% 55.65/8.89 % (3887217)------------------------------
% 55.65/8.89 % (3887217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887217)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887217)Termination reason: Instruction limit
% 81.31/12.36 % (3887217)Termination phase: Saturation
% 81.31/12.36 % (3887217)Time elapsed: 0.190 s
% 81.31/12.36 % (3887217)Peak memory usage: 90 MB
% 81.31/12.36 % (3887217)Instructions burned: 414 (million)
% 81.31/12.36 % (3887220)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=3639071875:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 81.31/12.36 % (3887209)Instruction limit reached!
% 81.31/12.36 % (3887209)------------------------------
% 81.31/12.36 % (3887209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887209)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887209)Termination reason: Instruction limit
% 81.31/12.36 % (3887209)Termination phase: Saturation
% 81.31/12.36 % (3887209)Time elapsed: 1.992 s
% 81.31/12.36 % (3887209)Peak memory usage: 146 MB
% 81.31/12.36 % (3887209)Instructions burned: 3256 (million)
% 81.31/12.36 % (3887195)Instruction limit reached!
% 81.31/12.36 % (3887195)------------------------------
% 81.31/12.36 % (3887195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887195)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887195)Termination reason: Instruction limit
% 81.31/12.36 % (3887195)Termination phase: Saturation
% 81.31/12.36 % (3887195)Time elapsed: 3.186 s
% 81.31/12.36 % (3887195)Peak memory usage: 151 MB
% 81.31/12.36 % (3887195)Instructions burned: 5209 (million)
% 81.31/12.36 % (3887222)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=2677383768:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi)
% 81.31/12.36 % (3887222)Refutation not found, incomplete strategy
% 81.31/12.36 % (3887222)------------------------------
% 81.31/12.36 % (3887222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887222)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887222)Termination reason: Refutation not found, incomplete strategy
% 81.31/12.36 % (3887222)Time elapsed: 0.003 s
% 81.31/12.36 % (3887222)Peak memory usage: 88 MB
% 81.31/12.36 % (3887222)Instructions burned: 2 (million)
% 81.31/12.36 % (3887223)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3857040692:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 81.31/12.36 % (3887222)------------------------------
% 81.31/12.36 % (3887222)------------------------------
% 81.31/12.36 % (3887226)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3728307256:i=598:bs=on:bd=preordered:av=off:ss=axioms_2954 on theBenchmark for (2954ds/598Mi)
% 81.31/12.36 % (3887223)Instruction limit reached!
% 81.31/12.36 % (3887223)------------------------------
% 81.31/12.36 % (3887223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887223)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887223)Termination reason: Instruction limit
% 81.31/12.36 % (3887223)Termination phase: Saturation
% 81.31/12.36 % (3887223)Time elapsed: 0.482 s
% 81.31/12.36 % (3887223)Peak memory usage: 96 MB
% 81.31/12.36 % (3887223)Instructions burned: 721 (million)
% 81.31/12.36 % (3887226)Instruction limit reached!
% 81.31/12.36 % (3887226)------------------------------
% 81.31/12.36 % (3887226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.31/12.36 % (3887226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.31/12.36 % (3887226)CaDiCaL version: 2.1.3
% 81.31/12.36 % (3887226)Termination reason: Instruction limit
% 81.31/12.36 % (3887226)Termination phase: Saturation
% 81.31/12.36 % (3887226)Time elapsed: 0.326 s
% 81.31/12.36 % (3887226)Peak memory usage: 90 MB
% 81.31/12.36 % (3887226)Instructions burned: 599 (million)
% 81.31/12.36 % (3887228)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1751989661:i=2989:sd=3:ss=axioms:sgt=60_2950 on theBenchmark for (2950ds/2989Mi)
% 119.00/17.69 % (3887229)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=1052698371:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2949 on theBenchmark for (2949ds/1997Mi)
% 119.00/17.69 % (3887229)Instruction limit reached!
% 119.00/17.69 % (3887229)------------------------------
% 119.00/17.69 % (3887229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.00/17.69 % (3887229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.00/17.69 % (3887229)CaDiCaL version: 2.1.3
% 119.00/17.69 % (3887229)Termination reason: Instruction limit
% 119.00/17.69 % (3887229)Termination phase: Saturation
% 119.00/17.69 % (3887229)Time elapsed: 1.341 s
% 119.00/17.69 % (3887229)Peak memory usage: 137 MB
% 119.00/17.69 % (3887229)Instructions burned: 1997 (million)
% 119.00/17.69 % (3887232)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=4207198722:i=2088:bd=preordered:av=off_2934 on theBenchmark for (2934ds/2088Mi)
% 119.00/17.69 % (3887220)Instruction limit reached!
% 119.00/17.69 % (3887220)------------------------------
% 119.00/17.69 % (3887220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.00/17.69 % (3887220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.00/17.69 % (3887220)CaDiCaL version: 2.1.3
% 119.00/17.69 % (3887220)Termination reason: Instruction limit
% 119.00/17.69 % (3887220)Termination phase: Saturation
% 119.00/17.69 % (3887220)Time elapsed: 3.481 s
% 119.00/17.69 % (3887220)Peak memory usage: 166 MB
% 119.00/17.69 % (3887220)Instructions burned: 8479 (million)
% 119.00/17.69 % (3887228)Instruction limit reached!
% 119.00/17.69 % (3887228)------------------------------
% 119.00/17.69 % (3887228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.00/17.69 % (3887228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.00/17.69 % (3887228)CaDiCaL version: 2.1.3
% 119.00/17.69 % (3887228)Termination reason: Instruction limit
% 119.00/17.69 % (3887228)Termination phase: Saturation
% 119.00/17.69 % (3887228)Time elapsed: 1.770 s
% 119.00/17.69 % (3887228)Peak memory usage: 140 MB
% 119.00/17.69 % (3887228)Instructions burned: 2989 (million)
% 119.00/17.69 % (3887234)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2238441748:i=1098:nicw=on_2931 on theBenchmark for (2931ds/1098Mi)
% 119.00/17.69 % (3887235)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3840137920:i=433:bd=preordered_2931 on theBenchmark for (2931ds/433Mi)
% 119.00/17.69 % (3887235)Instruction limit reached!
% 119.00/17.69 % (3887235)------------------------------
% 119.00/17.69 % (3887235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.00/17.69 % (3887235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.00/17.69 % (3887235)CaDiCaL version: 2.1.3
% 119.00/17.69 % (3887235)Termination reason: Instruction limit
% 119.00/17.69 % (3887235)Termination phase: Saturation
% 119.00/17.69 % (3887235)Time elapsed: 0.232 s
% 119.00/17.69 % (3887235)Peak memory usage: 91 MB
% 119.00/17.69 % (3887235)Instructions burned: 434 (million)
% 119.00/17.69 % (3887238)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=393817539:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2927 on theBenchmark for (2927ds/2942Mi)
% 119.00/17.69 % (3887234)Instruction limit reached!
% 119.00/17.69 % (3887234)------------------------------
% 119.00/17.69 % (3887234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.00/17.69 % (3887234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.00/17.69 % (3887234)CaDiCaL version: 2.1.3
% 119.00/17.69 % (3887234)Termination reason: Instruction limit
% 119.00/17.69 % (3887234)Termination phase: Saturation
% 119.00/17.69 % (3887234)Time elapsed: 0.677 s
% 119.00/17.69 % (3887234)Peak memory usage: 101 MB
% 119.00/17.69 % (3887234)Instructions burned: 1099 (million)
% 119.00/17.69 % (3887240)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3540154464:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2923 on theBenchmark for (2923ds/6922Mi)
% 119.00/17.69 % (3887232)Instruction limit reached!
% 119.00/17.69 % (3887232)------------------------------
% 119.00/17.69 % (3887232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887232)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887232)Termination reason: Instruction limit
% 132.74/19.79 % (3887232)Termination phase: Saturation
% 132.74/19.79 % (3887232)Time elapsed: 1.308 s
% 132.74/19.79 % (3887232)Peak memory usage: 138 MB
% 132.74/19.79 % (3887232)Instructions burned: 2088 (million)
% 132.74/19.79 % (3887242)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=3868633549:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2919 on theBenchmark for (2919ds/596Mi)
% 132.74/19.79 % (3887242)Instruction limit reached!
% 132.74/19.79 % (3887242)------------------------------
% 132.74/19.79 % (3887242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887242)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887242)Termination reason: Instruction limit
% 132.74/19.79 % (3887242)Termination phase: Saturation
% 132.74/19.79 % (3887242)Time elapsed: 0.325 s
% 132.74/19.79 % (3887242)Peak memory usage: 99 MB
% 132.74/19.79 % (3887242)Instructions burned: 596 (million)
% 132.74/19.79 % (3887244)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=52297741:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2914 on theBenchmark for (2914ds/4123Mi)
% 132.74/19.79 % (3887216)Instruction limit reached!
% 132.74/19.79 % (3887216)------------------------------
% 132.74/19.79 % (3887216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887216)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887216)Termination reason: Instruction limit
% 132.74/19.79 % (3887216)Termination phase: Saturation
% 132.74/19.79 % (3887216)Time elapsed: 6.025 s
% 132.74/19.79 % (3887216)Peak memory usage: 159 MB
% 132.74/19.79 % (3887216)Instructions burned: 10309 (million)
% 132.74/19.79 % (3887246)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2355359668:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2910 on theBenchmark for (2910ds/16411Mi)
% 132.74/19.79 % (3887238)Instruction limit reached!
% 132.74/19.79 % (3887238)------------------------------
% 132.74/19.79 % (3887238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887238)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887238)Termination reason: Instruction limit
% 132.74/19.79 % (3887238)Termination phase: Saturation
% 132.74/19.79 % (3887238)Time elapsed: 1.982 s
% 132.74/19.79 % (3887238)Peak memory usage: 144 MB
% 132.74/19.79 % (3887238)Instructions burned: 2943 (million)
% 132.74/19.79 % (3887248)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=640297121:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2905 on theBenchmark for (2905ds/1670Mi)
% 132.74/19.79 % (3887248)Instruction limit reached!
% 132.74/19.79 % (3887248)------------------------------
% 132.74/19.79 % (3887248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887248)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887248)Termination reason: Instruction limit
% 132.74/19.79 % (3887248)Termination phase: Saturation
% 132.74/19.79 % (3887248)Time elapsed: 1.065 s
% 132.74/19.79 % (3887248)Peak memory usage: 136 MB
% 132.74/19.79 % (3887248)Instructions burned: 1670 (million)
% 132.74/19.79 % (3887250)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=295044906:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2893 on theBenchmark for (2893ds/1722Mi)
% 132.74/19.79 % (3887244)Instruction limit reached!
% 132.74/19.79 % (3887244)------------------------------
% 132.74/19.79 % (3887244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.74/19.79 % (3887244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.74/19.79 % (3887244)CaDiCaL version: 2.1.3
% 132.74/19.79 % (3887244)Termination reason: Instruction limit
% 132.74/19.79 % (3887244)Termination phase: Saturation
% 132.74/19.79 % (3887244)Time elapsed: 2.643 s
% 132.74/19.79 % (3887244)Peak memory usage: 155 MB
% 132.74/19.79 % (3887244)Instructions burned: 4125 (million)
% 132.74/19.79 % (3887252)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=3853722868:cts=off:cond=on:i=9530:bs=on:fsd=on_2886 on theBenchmark for (2886ds/9530Mi)
% 148.45/21.87 % (3887240)Instruction limit reached!
% 148.45/21.87 % (3887240)------------------------------
% 148.45/21.87 % (3887240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/21.87 % (3887240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/21.87 % (3887240)CaDiCaL version: 2.1.3
% 148.45/21.87 % (3887240)Termination reason: Instruction limit
% 148.45/21.87 % (3887240)Termination phase: Saturation
% 148.45/21.87 % (3887240)Time elapsed: 3.748 s
% 148.45/21.87 % (3887240)Peak memory usage: 187 MB
% 148.45/21.87 % (3887240)Instructions burned: 6922 (million)
% 148.45/21.87 % (3887254)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2215943706:st=2:i=4495:sd=10:ss=included_2883 on theBenchmark for (2883ds/4495Mi)
% 148.45/21.87 % (3887250)Instruction limit reached!
% 148.45/21.87 % (3887250)------------------------------
% 148.45/21.87 % (3887250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/21.87 % (3887250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/21.87 % (3887250)CaDiCaL version: 2.1.3
% 148.45/21.87 % (3887250)Termination reason: Instruction limit
% 148.45/21.87 % (3887250)Termination phase: Saturation
% 148.45/21.87 % (3887250)Time elapsed: 1.196 s
% 148.45/21.87 % (3887250)Peak memory usage: 135 MB
% 148.45/21.87 % (3887250)Instructions burned: 1723 (million)
% 148.45/21.87 % (3887256)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=400507896:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2879 on theBenchmark for (2879ds/4920Mi)
% 148.45/21.87 % (3887254)Instruction limit reached!
% 148.45/21.87 % (3887254)------------------------------
% 148.45/21.87 % (3887254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/21.87 % (3887254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/21.87 % (3887254)CaDiCaL version: 2.1.3
% 148.45/21.87 % (3887254)Termination reason: Instruction limit
% 148.45/21.87 % (3887254)Termination phase: Saturation
% 148.45/21.87 % (3887254)Time elapsed: 2.749 s
% 148.45/21.87 % (3887254)Peak memory usage: 148 MB
% 148.45/21.87 % (3887254)Instructions burned: 4496 (million)
% 148.45/21.87 % (3887258)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=3058921123:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2854 on theBenchmark for (2854ds/2083Mi)
% 148.45/21.87 % (3887256)Instruction limit reached!
% 148.45/21.87 % (3887256)------------------------------
% 148.45/21.87 % (3887256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/21.87 % (3887256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/21.87 % (3887256)CaDiCaL version: 2.1.3
% 148.45/21.87 % (3887256)Termination reason: Instruction limit
% 148.45/21.87 % (3887256)Termination phase: Saturation
% 148.45/21.87 % (3887256)Time elapsed: 3.107 s
% 148.45/21.87 % (3887256)Peak memory usage: 147 MB
% 148.45/21.87 % (3887256)Instructions burned: 4921 (million)
% 148.45/21.87 % (3887260)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=4073007147:i=4629:av=off:gsp=on_2846 on theBenchmark for (2846ds/4629Mi)
% 148.45/21.87 % (3887258)Instruction limit reached!
% 148.45/21.87 % (3887258)------------------------------
% 148.45/21.87 % (3887258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.45/21.87 % (3887258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.45/21.87 % (3887258)CaDiCaL version: 2.1.3
% 148.45/21.87 % (3887258)Termination reason: Instruction limit
% 148.45/21.87 % (3887258)Termination phase: Saturation
% 148.45/21.87 % (3887258)Time elapsed: 1.265 s
% 148.45/21.87 % (3887258)Peak memory usage: 134 MB
% 148.45/21.87 % (3887258)Instructions burned: 2084 (million)
% 148.45/21.87 % (3887262)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2356179888:i=1258:av=off_2840 on theBenchmark for (2840ds/1258Mi)
% 148.45/21.87 % (3887262)Instruction limit reached!
% 148.45/21.87 % (3887262)------------------------------
% 148.45/21.87 % (3887262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887262)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887262)Termination reason: Instruction limit
% 183.52/26.76 % (3887262)Termination phase: Saturation
% 183.52/26.76 % (3887262)Time elapsed: 0.686 s
% 183.52/26.76 % (3887262)Peak memory usage: 96 MB
% 183.52/26.76 % (3887262)Instructions burned: 1260 (million)
% 183.52/26.76 % (3887264)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2605559596:i=7343:av=off:ss=included_2831 on theBenchmark for (2831ds/7343Mi)
% 183.52/26.76 % (3887264)Refutation not found, incomplete strategy
% 183.52/26.76 % (3887264)------------------------------
% 183.52/26.76 % (3887264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887264)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887264)Termination reason: Refutation not found, incomplete strategy
% 183.52/26.76 % (3887264)Time elapsed: 0.615 s
% 183.52/26.76 % (3887264)Peak memory usage: 128 MB
% 183.52/26.76 % (3887264)Instructions burned: 922 (million)
% 183.52/26.76 % (3887252)Instruction limit reached!
% 183.52/26.76 % (3887252)------------------------------
% 183.52/26.76 % (3887252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887252)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887252)Termination reason: Instruction limit
% 183.52/26.76 % (3887252)Termination phase: Saturation
% 183.52/26.76 % (3887252)Time elapsed: 6.251 s
% 183.52/26.76 % (3887252)Peak memory usage: 170 MB
% 183.52/26.76 % (3887252)Instructions burned: 9532 (million)
% 183.52/26.76 % (3887264)------------------------------
% 183.52/26.76 % (3887264)------------------------------
% 183.52/26.76 % (3887266)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4076100419:i=1325:sd=2:ss=axioms:sgt=16_2822 on theBenchmark for (2822ds/1325Mi)
% 183.52/26.76 % (3887266)Refutation not found, incomplete strategy
% 183.52/26.76 % (3887266)------------------------------
% 183.52/26.76 % (3887266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887266)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887266)Termination reason: Refutation not found, incomplete strategy
% 183.52/26.76 % (3887266)Time elapsed: 0.003 s
% 183.52/26.76 % (3887266)Peak memory usage: 88 MB
% 183.52/26.76 % (3887266)Instructions burned: 3 (million)
% 183.52/26.76 % (3887267)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=2161349960:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2821 on theBenchmark for (2821ds/2646Mi)
% 183.52/26.76 % (3887266)------------------------------
% 183.52/26.76 % (3887266)------------------------------
% 183.52/26.76 % (3887260)Instruction limit reached!
% 183.52/26.76 % (3887260)------------------------------
% 183.52/26.76 % (3887260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887260)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887260)Termination reason: Instruction limit
% 183.52/26.76 % (3887260)Termination phase: Saturation
% 183.52/26.76 % (3887260)Time elapsed: 2.843 s
% 183.52/26.76 % (3887260)Peak memory usage: 153 MB
% 183.52/26.76 % (3887260)Instructions burned: 4630 (million)
% 183.52/26.76 % (3887270)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=348786624:i=1489:sd=2:ep=R:ss=axioms_2818 on theBenchmark for (2818ds/1489Mi)
% 183.52/26.76 % (3887271)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=4132454251:i=1503_2816 on theBenchmark for (2816ds/1503Mi)
% 183.52/26.76 % (3887270)Refutation not found, incomplete strategy
% 183.52/26.76 % (3887270)------------------------------
% 183.52/26.76 % (3887270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.52/26.76 % (3887270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.52/26.76 % (3887270)CaDiCaL version: 2.1.3
% 183.52/26.76 % (3887270)Termination reason: Refutation not found, incomplete strategy
% 183.52/26.76 % (3887270)Time elapsed: 0.591 s
% 183.52/26.76 % (3887270)Peak memory usage: 128 MB
% 183.52/26.76 % (3887270)Instructions burned: 893 (million)
% 215.42/31.29 % (3887270)------------------------------
% 215.42/31.29 % (3887270)------------------------------
% 215.42/31.29 % (3887274)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2781414794:i=13942:kws=frequency_2808 on theBenchmark for (2808ds/13942Mi)
% 215.42/31.29 % (3887271)Instruction limit reached!
% 215.42/31.29 % (3887271)------------------------------
% 215.42/31.29 % (3887271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.42/31.29 % (3887271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.42/31.29 % (3887271)CaDiCaL version: 2.1.3
% 215.42/31.29 % (3887271)Termination reason: Instruction limit
% 215.42/31.29 % (3887271)Termination phase: Saturation
% 215.42/31.29 % (3887271)Time elapsed: 0.999 s
% 215.42/31.29 % (3887271)Peak memory usage: 134 MB
% 215.42/31.29 % (3887271)Instructions burned: 1505 (million)
% 215.42/31.29 % (3887246)Instruction limit reached!
% 215.42/31.29 % (3887246)------------------------------
% 215.42/31.29 % (3887246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.42/31.29 % (3887246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.42/31.29 % (3887246)CaDiCaL version: 2.1.3
% 215.42/31.29 % (3887246)Termination reason: Instruction limit
% 215.42/31.29 % (3887246)Termination phase: Saturation
% 215.42/31.29 % (3887246)Time elapsed: 10.539 s
% 215.42/31.29 % (3887246)Peak memory usage: 203 MB
% 215.42/31.29 % (3887246)Instructions burned: 16412 (million)
% 215.42/31.29 % (3887276)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=74212588:i=3604:fsr=off:er=filter_2804 on theBenchmark for (2804ds/3604Mi)
% 215.42/31.29 % (3887267)Instruction limit reached!
% 215.42/31.29 % (3887267)------------------------------
% 215.42/31.29 % (3887267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.42/31.29 % (3887267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.42/31.29 % (3887267)CaDiCaL version: 2.1.3
% 215.42/31.29 % (3887267)Termination reason: Instruction limit
% 215.42/31.29 % (3887267)Termination phase: Saturation
% 215.42/31.29 % (3887267)Time elapsed: 1.764 s
% 215.42/31.29 % (3887267)Peak memory usage: 144 MB
% 215.42/31.29 % (3887267)Instructions burned: 2646 (million)
% 215.42/31.29 % (3887278)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1362388467:i=1876:sd=1:ss=included:sgt=32_2803 on theBenchmark for (2803ds/1876Mi)
% 215.42/31.29 % (3887279)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3066712413:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2801 on theBenchmark for (2801ds/1932Mi)
% 215.42/31.29 % (3887278)Refutation not found, incomplete strategy
% 215.42/31.29 % (3887278)------------------------------
% 215.42/31.29 % (3887278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.42/31.29 % (3887278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.42/31.29 % (3887278)CaDiCaL version: 2.1.3
% 215.42/31.29 % (3887278)Termination reason: Refutation not found, incomplete strategy
% 215.42/31.29 % (3887278)Time elapsed: 0.608 s
% 215.42/31.29 % (3887278)Peak memory usage: 128 MB
% 215.42/31.29 % (3887278)Instructions burned: 913 (million)
% 215.42/31.29 % (3887279)Refutation not found, incomplete strategy
% 215.42/31.29 % (3887279)------------------------------
% 215.42/31.29 % (3887279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.42/31.29 % (3887279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.42/31.29 % (3887279)CaDiCaL version: 2.1.3
% 215.42/31.29 % (3887279)Termination reason: Refutation not found, incomplete strategy
% 215.42/31.29 % (3887279)Time elapsed: 0.582 s
% 215.42/31.29 % (3887279)Peak memory usage: 128 MB
% 215.42/31.29 % (3887279)Instructions burned: 873 (million)
% 215.42/31.29 % (3887278)------------------------------
% 215.42/31.29 % (3887278)------------------------------
% 215.42/31.29 % (3887279)------------------------------
% 215.42/31.29 % (3887279)------------------------------
% 215.42/31.29 % (3887282)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=3272501502:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2792 on theBenchmark for (2792ds/1980Mi)
% 215.42/31.29 % (3887283)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=1768766268:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2791 on theBenchmark for (2791ds/3902Mi)
% 125.33/33.10 % (3887276)Instruction limit reached!
% 125.33/33.10 % (3887276)------------------------------
% 125.33/33.10 % (3887276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887276)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887276)Termination reason: Instruction limit
% 125.33/33.10 % (3887276)Termination phase: Saturation
% 125.33/33.10 % (3887276)Time elapsed: 2.184 s
% 125.33/33.10 % (3887276)Peak memory usage: 141 MB
% 125.33/33.10 % (3887276)Instructions burned: 3604 (million)
% 125.33/33.10 % (3887286)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2454701596:avsq=on:i=3916:aac=none:amm=off_2781 on theBenchmark for (2781ds/3916Mi)
% 125.33/33.10 % (3887282)Instruction limit reached!
% 125.33/33.10 % (3887282)------------------------------
% 125.33/33.10 % (3887282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887282)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887282)Termination reason: Instruction limit
% 125.33/33.10 % (3887282)Termination phase: Saturation
% 125.33/33.10 % (3887282)Time elapsed: 1.285 s
% 125.33/33.10 % (3887282)Peak memory usage: 137 MB
% 125.33/33.10 % (3887282)Instructions burned: 1980 (million)
% 125.33/33.10 % (3887288)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3736444125:cond=on:i=3940:av=off:er=known_2778 on theBenchmark for (2778ds/3940Mi)
% 125.33/33.10 % (3887283)Instruction limit reached!
% 125.33/33.10 % (3887283)------------------------------
% 125.33/33.10 % (3887283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887283)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887283)Termination reason: Instruction limit
% 125.33/33.10 % (3887283)Termination phase: Saturation
% 125.33/33.10 % (3887283)Time elapsed: 2.627 s
% 125.33/33.10 % (3887283)Peak memory usage: 151 MB
% 125.33/33.10 % (3887283)Instructions burned: 3902 (million)
% 125.33/33.10 % (3887290)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=313860284:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2763 on theBenchmark for (2763ds/3980Mi)
% 125.33/33.10 % (3887286)Instruction limit reached!
% 125.33/33.10 % (3887286)------------------------------
% 125.33/33.10 % (3887286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887286)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887286)Termination reason: Instruction limit
% 125.33/33.10 % (3887286)Termination phase: Saturation
% 125.33/33.10 % (3887286)Time elapsed: 2.300 s
% 125.33/33.10 % (3887286)Peak memory usage: 105 MB
% 125.33/33.10 % (3887286)Instructions burned: 3917 (million)
% 125.33/33.10 % (3887292)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2759217671:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2756 on theBenchmark for (2756ds/2087Mi)
% 125.33/33.10 % (3887288)Instruction limit reached!
% 125.33/33.10 % (3887288)------------------------------
% 125.33/33.10 % (3887288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887288)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887288)Termination reason: Instruction limit
% 125.33/33.10 % (3887288)Termination phase: Saturation
% 125.33/33.10 % (3887288)Time elapsed: 2.435 s
% 125.33/33.10 % (3887288)Peak memory usage: 146 MB
% 125.33/33.10 % (3887288)Instructions burned: 3940 (million)
% 125.33/33.10 % (3887294)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=700471380:cts=off:cond=on:i=4272:bs=on:fsd=on_2752 on theBenchmark for (2752ds/4272Mi)
% 125.33/33.10 % (3887292)Instruction limit reached!
% 125.33/33.10 % (3887292)------------------------------
% 125.33/33.10 % (3887292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887292)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887292)Termination reason: Instruction limit
% 125.33/33.10 % (3887292)Termination phase: Saturation
% 125.33/33.10 % (3887292)Time elapsed: 1.407 s
% 125.33/33.10 % (3887292)Peak memory usage: 139 MB
% 125.33/33.10 % (3887292)Instructions burned: 2087 (million)
% 125.33/33.10 % (3887296)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3686556800:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2740 on theBenchmark for (2740ds/2197Mi)
% 125.33/33.10 % (3887290)Instruction limit reached!
% 125.33/33.10 % (3887290)------------------------------
% 125.33/33.10 % (3887290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887290)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887290)Termination reason: Instruction limit
% 125.33/33.10 % (3887290)Termination phase: Saturation
% 125.33/33.10 % (3887290)Time elapsed: 2.530 s
% 125.33/33.10 % (3887290)Peak memory usage: 155 MB
% 125.33/33.10 % (3887290)Instructions burned: 3981 (million)
% 125.33/33.10 % (3887298)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2498299622:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2736 on theBenchmark for (2736ds/6508Mi)
% 125.33/33.10 % (3887296)Instruction limit reached!
% 125.33/33.10 % (3887296)------------------------------
% 125.33/33.10 % (3887296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887296)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887296)Termination reason: Instruction limit
% 125.33/33.10 % (3887296)Termination phase: Saturation
% 125.33/33.10 % (3887296)Time elapsed: 1.355 s
% 125.33/33.10 % (3887296)Peak memory usage: 140 MB
% 125.33/33.10 % (3887296)Instructions burned: 2198 (million)
% 125.33/33.10 % (3887300)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3796834569:i=2330:fgj=on:av=off:fsr=off_2725 on theBenchmark for (2725ds/2330Mi)
% 125.33/33.10 % (3887294)Instruction limit reached!
% 125.33/33.10 % (3887294)------------------------------
% 125.33/33.10 % (3887294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887294)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887294)Termination reason: Instruction limit
% 125.33/33.10 % (3887294)Termination phase: Saturation
% 125.33/33.10 % (3887294)Time elapsed: 2.940 s
% 125.33/33.10 % (3887294)Peak memory usage: 150 MB
% 125.33/33.10 % (3887294)Instructions burned: 4273 (million)
% 125.33/33.10 % (3887302)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2956195202:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2721 on theBenchmark for (2721ds/7592Mi)
% 125.33/33.10 % (3887274)Instruction limit reached!
% 125.33/33.10 % (3887274)------------------------------
% 125.33/33.10 % (3887274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887274)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887274)Termination reason: Instruction limit
% 125.33/33.10 % (3887274)Termination phase: Saturation
% 125.33/33.10 % (3887274)Time elapsed: 9.179 s
% 125.33/33.10 % (3887274)Peak memory usage: 223 MB
% 125.33/33.10 % (3887274)Instructions burned: 13943 (million)
% 125.33/33.10 % (3887304)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=3444472448:i=2693:kws=precedence:ins=1:av=off_2714 on theBenchmark for (2714ds/2693Mi)
% 125.33/33.10 % (3887300)Instruction limit reached!
% 125.33/33.10 % (3887300)------------------------------
% 125.33/33.10 % (3887300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887300)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887300)Termination reason: Instruction limit
% 125.33/33.10 % (3887300)Termination phase: Saturation
% 125.33/33.10 % (3887300)Time elapsed: 1.290 s
% 125.33/33.10 % (3887300)Peak memory usage: 134 MB
% 125.33/33.10 % (3887300)Instructions burned: 2332 (million)
% 125.33/33.10 % (3887306)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=531272930:i=28651:sd=4:ss=included:sgt=64_2710 on theBenchmark for (2710ds/28651Mi)
% 125.33/33.10 % (3887298)Instruction limit reached!
% 125.33/33.10 % (3887298)------------------------------
% 125.33/33.10 % (3887298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887298)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887298)Termination reason: Instruction limit
% 125.33/33.10 % (3887298)Termination phase: Saturation
% 125.33/33.10 % (3887298)Time elapsed: 3.896 s
% 125.33/33.10 % (3887298)Peak memory usage: 135 MB
% 125.33/33.10 % (3887298)Instructions burned: 6509 (million)
% 125.33/33.10 % (3887304)Instruction limit reached!
% 125.33/33.10 % (3887304)------------------------------
% 125.33/33.10 % (3887304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887304)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887304)Termination reason: Instruction limit
% 125.33/33.10 % (3887304)Termination phase: Saturation
% 125.33/33.10 % (3887304)Time elapsed: 1.760 s
% 125.33/33.10 % (3887304)Peak memory usage: 144 MB
% 125.33/33.10 % (3887304)Instructions burned: 2694 (million)
% 125.33/33.10 % (3887308)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=873739430:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2695 on theBenchmark for (2695ds/2700Mi)
% 125.33/33.10 % (3887309)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3471077206:i=3196:nm=4_2695 on theBenchmark for (2695ds/3196Mi)
% 125.33/33.10 % (3887302)Instruction limit reached!
% 125.33/33.10 % (3887302)------------------------------
% 125.33/33.10 % (3887302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.33/33.10 % (3887302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.33/33.10 % (3887302)CaDiCaL version: 2.1.3
% 125.33/33.10 % (3887302)Termination reason: Instruction limit
% 125.33/33.10 % (3887302)Termination phase: Saturation
% 125.33/33.10 % (3887302)Time elapsed: 3.619 s
% 125.33/33.10 % (3887302)Peak memory usage: 133 MB
% 125.33/33.10 % (3887302)Instructions burned: 7593 (million)
% 125.33/33.10 % (3887312)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3904806273:cts=off:i=3254:av=off_2683 on theBenchmark for (2683ds/3254Mi)
% 125.33/33.10 % (3887308)First to succeed.
% 125.33/33.10 % (3887308)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3887158"
% 125.33/33.10 % (3887308)Refutation found. Thanks to Tanya!
% 125.33/33.10 % SZS status Unsatisfiable for theBenchmark
% 125.33/33.10 % SZS output start Proof for theBenchmark
% See solution above
% 228.80/33.29 % (3887308)------------------------------
% 228.80/33.29 % (3887308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 228.80/33.29 % (3887308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 228.80/33.29 % (3887308)CaDiCaL version: 2.1.3
% 228.80/33.29 % (3887308)Termination reason: Refutation
% 228.80/33.29 % (3887308)Time elapsed: 1.323 s
% 228.80/33.29 % (3887308)Peak memory usage: 137 MB
% 228.80/33.29 % (3887308)Instructions burned: 2009 (million)
% 228.80/33.29 % (3887308)------------------------------
% 228.80/33.29 % (3887308)------------------------------
% 228.80/33.29 % (3887158)Success in time 32.239 s
% 228.80/33.29 % Vampire exiting
%------------------------------------------------------------------------------