%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM247-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 : n013.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:58 PM UTC 2026
% Result : Unsatisfiable 16.48s 6.42s
% Output : Refutation 39.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 24
% Syntax : Number of formulae : 77 ( 32 unt; 5 def)
% Number of atoms : 130 ( 37 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 104 ( 51 ~; 53 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-3 aty)
% Number of variables : 107 ( 107 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),X0) ),
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(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
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(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(f19,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),element_relation)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation2) ).
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(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f54,axiom,
! [X0] : domain_of(restrict(element_relation,universal_class,X0)) = sum_class(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class_definition) ).
fof(f58,axiom,
! [X0,X1] : subclass(compose(X0,X1),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose1) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f166,axiom,
! [X0,X1] :
( compose(X1,rest_of(X0)) = X0
| ~ member(X0,recursion_equation_functions(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',recursion_equation_functions4) ).
fof(f176,negated_conjecture,
~ subclass(sum_class(recursion_equation_functions(z)),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_transfinite_recursion_property3_1) ).
fof(f177,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(f183,plain,
! [X0] : sum_class(X0) = domain_of(intersection(element_relation,cross_product(universal_class,X0))),
inference(definition_unfolding,[],[f54,f28]) ).
fof(f194,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,f177]) ).
fof(f195,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,f177]) ).
fof(f197,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,f177]) ).
fof(f198,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| member(X0,X1) ),
inference(definition_unfolding,[],[f19,f177]) ).
fof(f201,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f267,plain,
~ subclass(domain_of(intersection(element_relation,cross_product(universal_class,recursion_equation_functions(z)))),cross_product(universal_class,universal_class)),
inference(definition_unfolding,[],[f176,f183]) ).
fof(f292,definition,
sF8 = recursion_equation_functions(z),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f293,plain,
recursion_equation_functions(z) = sF8,
inference(reorient_equations,[],[f292]) ).
fof(f294,definition,
sF9 = cross_product(universal_class,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f295,plain,
cross_product(universal_class,sF8) = sF9,
inference(reorient_equations,[],[f294]) ).
fof(f296,definition,
sF10 = intersection(element_relation,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f297,plain,
intersection(element_relation,sF9) = sF10,
inference(reorient_equations,[],[f296]) ).
fof(f298,definition,
sF11 = domain_of(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f299,plain,
domain_of(sF10) = sF11,
inference(reorient_equations,[],[f298]) ).
fof(f300,definition,
sF12 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f301,plain,
cross_product(universal_class,universal_class) = sF12,
inference(reorient_equations,[],[f300]) ).
fof(f302,plain,
~ subclass(sF11,sF12),
inference(definition_folding,[],[f267,f301,f299,f297,f295,f293]) ).
fof(f305,plain,
member(not_subclass_element(sF11,sF12),sF11),
inference(resolution,[],[f302,f2]) ).
fof(f319,plain,
! [X0] :
( ~ member(X0,sF10)
| member(X0,sF9) ),
inference(superposition,[],[f22,f297]) ).
fof(f320,plain,
! [X0] :
( ~ member(X0,sF10)
| member(X0,element_relation) ),
inference(superposition,[],[f21,f297]) ).
fof(f326,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X1,X2))
| member(second(X0),X2)
| ~ member(X0,cross_product(X3,X4)) ),
inference(superposition,[],[f195,f197]) ).
fof(f330,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),X1)
| ~ member(X0,cross_product(X3,X4)) ),
inference(superposition,[],[f194,f197]) ).
fof(f336,plain,
! [X2,X0,X1] :
( ~ member(X0,sF9)
| member(second(X0),sF8)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f326,f295]) ).
fof(f384,plain,
! [X0,X1] :
( intersection(X0,X1) = null_class
| member(regular(intersection(X0,X1)),X1) ),
inference(resolution,[],[f68,f22]) ).
fof(f385,plain,
! [X0,X1] :
( intersection(X0,X1) = null_class
| member(regular(intersection(X0,X1)),X0) ),
inference(resolution,[],[f68,f21]) ).
fof(f408,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X0) ),
inference(superposition,[],[f201,f385]) ).
fof(f412,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X0) ),
inference(trivial_inequality_removal,[],[f408]) ).
fof(f417,plain,
! [X0] :
( ~ member(X0,sF11)
| member(regular(intersection(sF10,cross_product(unordered_pair(X0,X0),universal_class))),sF10) ),
inference(superposition,[],[f412,f299]) ).
fof(f427,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),cross_product(unordered_pair(X1,X1),universal_class)) ),
inference(superposition,[],[f201,f384]) ).
fof(f431,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),cross_product(unordered_pair(X1,X1),universal_class)) ),
inference(trivial_inequality_removal,[],[f427]) ).
fof(f436,plain,
! [X0] :
( ~ member(X0,sF11)
| member(regular(intersection(sF10,cross_product(unordered_pair(X0,X0),universal_class))),cross_product(unordered_pair(X0,X0),universal_class)) ),
inference(superposition,[],[f431,f299]) ).
fof(f437,plain,
member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)),
inference(resolution,[],[f436,f305]) ).
fof(f441,plain,
! [X0,X1] :
( member(first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)))
| ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(X0,X1)) ),
inference(resolution,[],[f437,f330]) ).
fof(f459,plain,
member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),sF10),
inference(resolution,[],[f417,f305]) ).
fof(f462,plain,
member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),element_relation),
inference(resolution,[],[f459,f320]) ).
fof(f463,plain,
member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),sF9),
inference(resolution,[],[f459,f319]) ).
fof(f472,plain,
! [X0,X1] :
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),sF8) ),
inference(resolution,[],[f463,f336]) ).
fof(f528,plain,
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),sF9)
| member(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),sF8) ),
inference(superposition,[],[f472,f295]) ).
fof(f529,plain,
member(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),sF8),
inference(forward_subsumption_resolution,[],[f528,f463]) ).
fof(f620,plain,
! [X0,X1] : subclass(compose(X0,X1),sF12),
inference(forward_demodulation,[],[f58,f301]) ).
fof(f622,plain,
! [X0,X1] :
( subclass(X0,sF12)
| ~ member(X0,recursion_equation_functions(X1)) ),
inference(superposition,[],[f620,f166]) ).
fof(f764,plain,
! [X0,X1] :
( not_subclass_element(sF11,sF12) = first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))
| not_subclass_element(sF11,sF12) = first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))
| ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(X0,X1)) ),
inference(resolution,[],[f8,f441]) ).
fof(f767,plain,
! [X0,X1] :
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(X0,X1))
| not_subclass_element(sF11,sF12) = first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))) ),
inference(duplicate_literal_removal,[],[f764]) ).
fof(f826,plain,
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),sF9)
| not_subclass_element(sF11,sF12) = first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))) ),
inference(superposition,[],[f767,f295]) ).
fof(f827,plain,
not_subclass_element(sF11,sF12) = first(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),
inference(forward_subsumption_resolution,[],[f826,f463]) ).
fof(f835,plain,
! [X0,X1] :
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),cross_product(X0,X1))
| regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),unordered_pair(not_subclass_element(sF11,sF12),unordered_pair(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))))) ),
inference(superposition,[],[f197,f827]) ).
fof(f843,plain,
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),sF9)
| regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),unordered_pair(not_subclass_element(sF11,sF12),unordered_pair(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))))) ),
inference(superposition,[],[f835,f295]) ).
fof(f844,plain,
regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),unordered_pair(not_subclass_element(sF11,sF12),unordered_pair(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))))),
inference(forward_subsumption_resolution,[],[f843,f463]) ).
fof(f852,plain,
( ~ member(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))),element_relation)
| member(not_subclass_element(sF11,sF12),second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))) ),
inference(superposition,[],[f198,f844]) ).
fof(f860,plain,
member(not_subclass_element(sF11,sF12),second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class))))),
inference(forward_subsumption_resolution,[],[f852,f462]) ).
fof(f882,plain,
! [X0] :
( ~ subclass(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),X0)
| member(not_subclass_element(sF11,sF12),X0) ),
inference(resolution,[],[f860,f1]) ).
fof(f937,plain,
! [X0] :
( ~ member(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),recursion_equation_functions(X0))
| member(not_subclass_element(sF11,sF12),sF12) ),
inference(resolution,[],[f882,f622]) ).
fof(f945,plain,
( ~ member(second(regular(intersection(sF10,cross_product(unordered_pair(not_subclass_element(sF11,sF12),not_subclass_element(sF11,sF12)),universal_class)))),sF8)
| member(not_subclass_element(sF11,sF12),sF12) ),
inference(superposition,[],[f937,f293]) ).
fof(f946,plain,
member(not_subclass_element(sF11,sF12),sF12),
inference(forward_subsumption_resolution,[],[f945,f529]) ).
fof(f948,plain,
$false,
inference(unit_resulting_resolution,[],[f3,f302,f946]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM247-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 19:18:11 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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.51/2.62 % (498976)Input is clausal, will run a generic CNF schedule.
% 12.51/2.62 % (498985)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2488168123:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.51/2.62 % (498985)Instruction limit reached!
% 12.51/2.62 % (498985)------------------------------
% 12.51/2.62 % (498985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.62 % (498985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.62 % (498985)CaDiCaL version: 2.1.3
% 12.51/2.62 % (498985)Termination reason: Instruction limit
% 12.51/2.62 % (498985)Termination phase: Saturation
% 12.51/2.62 % (498985)Time elapsed: 0.040 s
% 12.51/2.62 % (498985)Peak memory usage: 89 MB
% 12.51/2.62 % (498985)Instructions burned: 115 (million)
% 12.51/2.62 % (498981)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=88559757:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.51/2.62 % (498982)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4249200098:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.51/2.62 % (498984)lrs+10_1_sil=8000:sp=occurrence:random_seed=1016213749:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.51/2.62 % (498987)dis-21_1_sil=8000:lcm=predicate:random_seed=1292392268: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.51/2.62 % (498983)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2171245063:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.51/2.62 % (498986)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3850738430:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.51/2.62 % (498984)Refutation not found, incomplete strategy
% 12.51/2.62 % (498984)------------------------------
% 12.51/2.62 % (498984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.62 % (498984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.62 % (498984)CaDiCaL version: 2.1.3
% 12.51/2.62 % (498984)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.62 % (498984)Time elapsed: 0.025 s
% 12.51/2.62 % (498984)Peak memory usage: 89 MB
% 12.51/2.62 % (498984)Instructions burned: 32 (million)
% 12.51/2.62 % (498987)Instruction limit reached!
% 12.51/2.62 % (498987)------------------------------
% 12.51/2.62 % (498987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.62 % (498987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.62 % (498987)CaDiCaL version: 2.1.3
% 12.51/2.62 % (498987)Termination reason: Instruction limit
% 12.51/2.62 % (498987)Termination phase: Saturation
% 12.51/2.62 % (498987)Time elapsed: 0.066 s
% 12.51/2.62 % (498987)Peak memory usage: 88 MB
% 12.51/2.62 % (498987)Instructions burned: 119 (million)
% 12.51/2.62 % (498994)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=3234743151:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 12.51/2.62 % (498994)Refutation not found, incomplete strategy
% 12.51/2.62 % (498994)------------------------------
% 12.51/2.62 % (498994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.62 % (498994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.62 % (498994)CaDiCaL version: 2.1.3
% 12.51/2.62 % (498994)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.62 % (498994)Time elapsed: 0.002 s
% 12.51/2.62 % (498994)Peak memory usage: 88 MB
% 12.51/2.62 % (498994)Instructions burned: 4 (million)
% 12.51/2.62 % (498986)Instruction limit reached!
% 12.51/2.62 % (498986)------------------------------
% 12.51/2.62 % (498986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.62 % (498986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.62 % (498986)CaDiCaL version: 2.1.3
% 12.51/2.62 % (498986)Termination reason: Instruction limit
% 12.51/2.62 % (498986)Termination phase: Saturation
% 12.51/2.62 % (498986)Time elapsed: 0.137 s
% 12.51/2.62 % (498986)Peak memory usage: 90 MB
% 12.51/2.62 % (498986)Instructions burned: 180 (million)
% 12.51/2.62 % (498996)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2582027320: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)
% 17.74/3.49 % (498984)------------------------------
% 17.74/3.49 % (498984)------------------------------
% 17.74/3.49 % (498994)------------------------------
% 17.74/3.49 % (498994)------------------------------
% 17.74/3.49 % (498998)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2236863183:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 17.74/3.49 % (498998)Refutation not found, incomplete strategy
% 17.74/3.49 % (498998)------------------------------
% 17.74/3.49 % (498998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.74/3.49 % (498998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.74/3.49 % (498998)CaDiCaL version: 2.1.3
% 17.74/3.49 % (498998)Termination reason: Refutation not found, incomplete strategy
% 17.74/3.49 % (498998)Time elapsed: 0.004 s
% 17.74/3.49 % (498998)Peak memory usage: 88 MB
% 17.74/3.49 % (498998)Instructions burned: 4 (million)
% 17.74/3.49 % (498996)Instruction limit reached!
% 17.74/3.49 % (498996)------------------------------
% 17.74/3.49 % (498996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.74/3.49 % (498996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.74/3.49 % (498996)CaDiCaL version: 2.1.3
% 17.74/3.49 % (498996)Termination reason: Instruction limit
% 17.74/3.49 % (498996)Termination phase: Saturation
% 17.74/3.49 % (498996)Time elapsed: 0.123 s
% 17.74/3.49 % (498996)Peak memory usage: 91 MB
% 17.74/3.49 % (498996)Instructions burned: 190 (million)
% 17.74/3.49 % (499001)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=130732147:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 17.74/3.49 % (499000)lrs+10_64_to=lpo:sil=8000:random_seed=2230339849:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 17.74/3.49 % (499001)Instruction limit reached!
% 17.74/3.49 % (499001)------------------------------
% 17.74/3.49 % (499001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.74/3.49 % (499001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.74/3.49 % (499001)CaDiCaL version: 2.1.3
% 17.74/3.49 % (499001)Termination reason: Instruction limit
% 17.74/3.49 % (499001)Termination phase: Saturation
% 17.74/3.49 % (499001)Time elapsed: 0.071 s
% 17.74/3.49 % (499001)Peak memory usage: 90 MB
% 17.74/3.49 % (499001)Instructions burned: 197 (million)
% 17.74/3.49 % (499000)Instruction limit reached!
% 17.74/3.49 % (499000)------------------------------
% 17.74/3.49 % (499000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.74/3.49 % (499000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.74/3.49 % (499000)CaDiCaL version: 2.1.3
% 17.74/3.49 % (499000)Termination reason: Instruction limit
% 17.74/3.49 % (499000)Termination phase: Saturation
% 17.74/3.49 % (499000)Time elapsed: 0.081 s
% 17.74/3.49 % (499000)Peak memory usage: 89 MB
% 17.74/3.49 % (499000)Instructions burned: 127 (million)
% 17.74/3.49 % (499003)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3801853525:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 17.74/3.49 % (498998)------------------------------
% 17.74/3.49 % (498998)------------------------------
% 17.74/3.49 % (499006)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=145771860:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 17.74/3.49 % (499003)Instruction limit reached!
% 17.74/3.49 % (499003)------------------------------
% 17.74/3.49 % (499003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.74/3.49 % (499003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.74/3.49 % (499003)CaDiCaL version: 2.1.3
% 17.74/3.49 % (499003)Termination reason: Instruction limit
% 17.74/3.49 % (499003)Termination phase: Saturation
% 17.74/3.49 % (499003)Time elapsed: 0.114 s
% 17.74/3.49 % (499003)Peak memory usage: 91 MB
% 17.74/3.49 % (499003)Instructions burned: 157 (million)
% 17.74/3.49 % (499007)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=2831861409:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 17.74/3.49 % (499009)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3079052368:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 17.74/3.49 % (499007)Instruction limit reached!
% 31.62/5.37 % (499007)------------------------------
% 31.62/5.37 % (499007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499007)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499007)Termination reason: Instruction limit
% 31.62/5.37 % (499007)Termination phase: Saturation
% 31.62/5.37 % (499007)Time elapsed: 0.067 s
% 31.62/5.37 % (499007)Peak memory usage: 89 MB
% 31.62/5.37 % (499007)Instructions burned: 106 (million)
% 31.62/5.37 % (499011)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2226888872:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 31.62/5.37 % (499009)Instruction limit reached!
% 31.62/5.37 % (499009)------------------------------
% 31.62/5.37 % (499009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499009)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499009)Termination reason: Instruction limit
% 31.62/5.37 % (499009)Termination phase: Saturation
% 31.62/5.37 % (499009)Time elapsed: 0.074 s
% 31.62/5.37 % (499009)Peak memory usage: 90 MB
% 31.62/5.37 % (499009)Instructions burned: 107 (million)
% 31.62/5.37 % (499014)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3657337089:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 31.62/5.37 % (499011)Instruction limit reached!
% 31.62/5.37 % (499011)------------------------------
% 31.62/5.37 % (499011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499011)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499011)Termination reason: Instruction limit
% 31.62/5.37 % (499011)Termination phase: Saturation
% 31.62/5.37 % (499011)Time elapsed: 0.152 s
% 31.62/5.37 % (499011)Peak memory usage: 91 MB
% 31.62/5.37 % (499011)Instructions burned: 243 (million)
% 31.62/5.37 % (499016)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3244220711:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 31.62/5.37 % (499016)Refutation not found, incomplete strategy
% 31.62/5.37 % (499016)------------------------------
% 31.62/5.37 % (499016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499016)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499016)Termination reason: Refutation not found, incomplete strategy
% 31.62/5.37 % (499016)Time elapsed: 0.009 s
% 31.62/5.37 % (499016)Peak memory usage: 88 MB
% 31.62/5.37 % (499016)Instructions burned: 13 (million)
% 31.62/5.37 % (499018)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4152232700:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 31.62/5.37 % (499016)------------------------------
% 31.62/5.37 % (499016)------------------------------
% 31.62/5.37 % (499021)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=668517564:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 31.62/5.37 % (499018)Instruction limit reached!
% 31.62/5.37 % (499018)------------------------------
% 31.62/5.37 % (499018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499018)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499018)Termination reason: Instruction limit
% 31.62/5.37 % (499018)Termination phase: Saturation
% 31.62/5.37 % (499018)Time elapsed: 0.308 s
% 31.62/5.37 % (499018)Peak memory usage: 94 MB
% 31.62/5.37 % (499018)Instructions burned: 499 (million)
% 31.62/5.37 % (499021)Instruction limit reached!
% 31.62/5.37 % (499021)------------------------------
% 31.62/5.37 % (499021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.62/5.37 % (499021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.62/5.37 % (499021)CaDiCaL version: 2.1.3
% 31.62/5.37 % (499021)Termination reason: Instruction limit
% 31.62/5.37 % (499021)Termination phase: Saturation
% 31.62/5.37 % (499021)Time elapsed: 0.109 s
% 31.62/5.37 % (499021)Peak memory usage: 89 MB
% 31.62/5.37 % (499021)Instructions burned: 191 (million)
% 31.62/5.37 % (499023)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1833624221:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 16.48/6.42 % (499024)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2624146950:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 16.48/6.42 % (499024)Instruction limit reached!
% 16.48/6.42 % (499024)------------------------------
% 16.48/6.42 % (499024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499024)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499024)Termination reason: Instruction limit
% 16.48/6.42 % (499024)Termination phase: Saturation
% 16.48/6.42 % (499024)Time elapsed: 0.090 s
% 16.48/6.42 % (499024)Peak memory usage: 90 MB
% 16.48/6.42 % (499024)Instructions burned: 157 (million)
% 16.48/6.42 % (499023)Instruction limit reached!
% 16.48/6.42 % (499023)------------------------------
% 16.48/6.42 % (499023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499023)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499023)Termination reason: Instruction limit
% 16.48/6.42 % (499023)Termination phase: Saturation
% 16.48/6.42 % (499023)Time elapsed: 0.173 s
% 16.48/6.42 % (499023)Peak memory usage: 92 MB
% 16.48/6.42 % (499023)Instructions burned: 265 (million)
% 16.48/6.42 % (499006)Instruction limit reached!
% 16.48/6.42 % (499006)------------------------------
% 16.48/6.42 % (499006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499006)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499006)Termination reason: Instruction limit
% 16.48/6.42 % (499006)Termination phase: Saturation
% 16.48/6.42 % (499006)Time elapsed: 1.173 s
% 16.48/6.42 % (499006)Peak memory usage: 147 MB
% 16.48/6.42 % (499006)Instructions burned: 3394 (million)
% 16.48/6.42 % (499027)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=1493492235:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 16.48/6.42 % (499028)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=728316929:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 16.48/6.42 % (499029)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3228207306:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 16.48/6.42 % (499029)Instruction limit reached!
% 16.48/6.42 % (499029)------------------------------
% 16.48/6.42 % (499029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499029)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499029)Termination reason: Instruction limit
% 16.48/6.42 % (499029)Termination phase: Saturation
% 16.48/6.42 % (499029)Time elapsed: 0.052 s
% 16.48/6.42 % (499029)Peak memory usage: 89 MB
% 16.48/6.42 % (499029)Instructions burned: 184 (million)
% 16.48/6.42 % (499033)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=368039914:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 16.48/6.42 % (499028)Instruction limit reached!
% 16.48/6.42 % (499028)------------------------------
% 16.48/6.42 % (499028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499028)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499028)Termination reason: Instruction limit
% 16.48/6.42 % (499028)Termination phase: Saturation
% 16.48/6.42 % (499028)Time elapsed: 0.204 s
% 16.48/6.42 % (499028)Peak memory usage: 88 MB
% 16.48/6.42 % (499028)Instructions burned: 539 (million)
% 16.48/6.42 % (499035)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=1393503922:i=412:gtgl=4:gtg=exists_all_2977 on theBenchmark for (2977ds/412Mi)
% 16.48/6.42 % (499035)Instruction limit reached!
% 16.48/6.42 % (499035)------------------------------
% 16.48/6.42 % (499035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499035)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499035)Termination reason: Instruction limit
% 16.48/6.42 % (499035)Termination phase: Saturation
% 16.48/6.42 % (499035)Time elapsed: 0.187 s
% 16.48/6.42 % (499035)Peak memory usage: 90 MB
% 16.48/6.42 % (499035)Instructions burned: 413 (million)
% 16.48/6.42 % (499037)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=3047504032:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 16.48/6.42 % (499027)Instruction limit reached!
% 16.48/6.42 % (499027)------------------------------
% 16.48/6.42 % (499027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499027)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499027)Termination reason: Instruction limit
% 16.48/6.42 % (499027)Termination phase: Saturation
% 16.48/6.42 % (499027)Time elapsed: 1.232 s
% 16.48/6.42 % (499027)Peak memory usage: 149 MB
% 16.48/6.42 % (499027)Instructions burned: 3261 (million)
% 16.48/6.42 % (499039)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=2721515207:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2966 on theBenchmark for (2966ds/303Mi)
% 16.48/6.42 % (499039)Refutation not found, incomplete strategy
% 16.48/6.42 % (499039)------------------------------
% 16.48/6.42 % (499039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499039)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499039)Termination reason: Refutation not found, incomplete strategy
% 16.48/6.42 % (499039)Time elapsed: 0.001 s
% 16.48/6.42 % (499039)Peak memory usage: 88 MB
% 16.48/6.42 % (499039)Instructions burned: 2 (million)
% 16.48/6.42 % (499039)------------------------------
% 16.48/6.42 % (499039)------------------------------
% 16.48/6.42 % (499041)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=896803940:st=4:i=720:sd=3:fsr=off:ss=axioms_2964 on theBenchmark for (2964ds/720Mi)
% 16.48/6.42 % (499041)Instruction limit reached!
% 16.48/6.42 % (499041)------------------------------
% 16.48/6.42 % (499041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499041)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499041)Termination reason: Instruction limit
% 16.48/6.42 % (499041)Termination phase: Saturation
% 16.48/6.42 % (499041)Time elapsed: 0.221 s
% 16.48/6.42 % (499041)Peak memory usage: 96 MB
% 16.48/6.42 % (499041)Instructions burned: 723 (million)
% 16.48/6.42 % (499043)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2172842803:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 16.48/6.42 % (499043)Instruction limit reached!
% 16.48/6.42 % (499043)------------------------------
% 16.48/6.42 % (499043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499043)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499043)Termination reason: Instruction limit
% 16.48/6.42 % (499043)Termination phase: Saturation
% 16.48/6.42 % (499043)Time elapsed: 0.209 s
% 16.48/6.42 % (499043)Peak memory usage: 93 MB
% 16.48/6.42 % (499043)Instructions burned: 598 (million)
% 16.48/6.42 % (499014)Instruction limit reached!
% 16.48/6.42 % (499014)------------------------------
% 16.48/6.42 % (499014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499014)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499014)Termination reason: Instruction limit
% 16.48/6.42 % (499014)Termination phase: Saturation
% 16.48/6.42 % (499014)Time elapsed: 3.267 s
% 16.48/6.42 % (499014)Peak memory usage: 158 MB
% 16.48/6.42 % (499014)Instructions burned: 5208 (million)
% 16.48/6.42 % (499045)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2244594145:i=2989:sd=3:ss=axioms:sgt=60_2957 on theBenchmark for (2957ds/2989Mi)
% 16.48/6.42 % (499046)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=268441718:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi)
% 16.48/6.42 % (499046)First to succeed.
% 16.48/6.42 % (499046)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-498976"
% 16.48/6.42 % (499045)Instruction limit reached!
% 16.48/6.42 % (499045)------------------------------
% 16.48/6.42 % (499045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.48/6.42 % (499045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.48/6.42 % (499045)CaDiCaL version: 2.1.3
% 16.48/6.42 % (499045)Termination reason: Instruction limit
% 16.48/6.42 % (499045)Termination phase: Saturation
% 16.48/6.42 % (499045)Time elapsed: 1.003 s
% 16.48/6.42 % (499045)Peak memory usage: 145 MB
% 16.48/6.42 % (499045)Instructions burned: 2991 (million)
% 16.48/6.42 % (499046)Refutation found. Thanks to Tanya!
% 16.48/6.42 % SZS status Unsatisfiable for theBenchmark
% 16.48/6.42 % SZS output start Proof for theBenchmark
% See solution above
% 39.87/6.52 % (499046)------------------------------
% 39.87/6.52 % (499046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.87/6.52 % (499046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.87/6.52 % (499046)CaDiCaL version: 2.1.3
% 39.87/6.52 % (499046)Termination reason: Refutation
% 39.87/6.52 % (499046)Time elapsed: 0.776 s
% 39.87/6.52 % (499046)Peak memory usage: 132 MB
% 39.87/6.52 % (499046)Instructions burned: 1200 (million)
% 39.87/6.52 % (499046)------------------------------
% 39.87/6.52 % (499046)------------------------------
% 39.87/6.52 % (498976)Success in time 5.566 s
% 39.87/6.52 % Vampire exiting
%------------------------------------------------------------------------------