%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM219-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:55 PM UTC 2026
% Result : Unsatisfiable 83.60s 22.34s
% Output : Refutation 152.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 41
% Syntax : Number of formulae : 163 ( 28 unt; 15 def)
% Number of atoms : 353 ( 43 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 344 ( 154 ~; 175 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 16 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-3 aty)
% Number of variables : 144 ( 0 sgn 144 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',domain1) ).
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/sandbox2/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(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f156,axiom,
! [X0] : subclass(rest_of(X0),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rest_of1) ).
fof(f157,axiom,
! [X2,X0,X1] :
( ~ member(ordered_pair(X0,X1),rest_of(X2))
| member(X0,domain_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rest_of2) ).
fof(f159,axiom,
! [X2,X0,X1] :
( ~ member(X0,domain_of(X1))
| restrict(X1,X0,universal_class) != X2
| member(ordered_pair(X0,X2),rest_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rest_of4) ).
fof(f176,negated_conjecture,
domain_of(rest_of(u)) != domain_of(u),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_domain_of_rest_of_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(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(f196,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,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(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(f202,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(f260,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),rest_of(X2))
| member(X0,domain_of(X2)) ),
inference(definition_unfolding,[],[f157,f177]) ).
fof(f262,plain,
! [X2,X0,X1] :
( ~ member(X0,domain_of(X1))
| intersection(X1,cross_product(X0,universal_class)) != X2
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),rest_of(X1)) ),
inference(definition_unfolding,[],[f159,f28,f177]) ).
fof(f268,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f271,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(intersection(X1,cross_product(X0,universal_class)),intersection(X1,cross_product(X0,universal_class))))),rest_of(X1))
| ~ member(X0,domain_of(X1)) ),
inference(equality_resolution,[],[f262]) ).
fof(f274,definition,
( spl0_1
<=> domain_of(rest_of(u)) = domain_of(u) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f276,plain,
( domain_of(rest_of(u)) != domain_of(u)
| spl0_1 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f277,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f176,f274]) ).
fof(f280,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| ~ subclass(X2,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f1,f3]) ).
fof(f283,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f22,f2]) ).
fof(f285,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f21,f2]) ).
fof(f297,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f285,f3]) ).
fof(f301,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f297]) ).
fof(f302,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f283,f3]) ).
fof(f306,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f302]) ).
fof(f312,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f317,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,f202]) ).
fof(f319,plain,
! [X2,X3,X0,X1] :
( member(first(X0),domain_of(X1))
| ~ member(X0,rest_of(X1))
| ~ member(X0,cross_product(X2,X3)) ),
inference(superposition,[],[f260,f197]) ).
fof(f360,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,[],[f317,f196]) ).
fof(f367,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(first(X0),X1)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f194,f197]) ).
fof(f438,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f301,f70]) ).
fof(f501,definition,
( spl0_8
<=> subclass(domain_of(u),domain_of(rest_of(u))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f502,plain,
( subclass(domain_of(u),domain_of(rest_of(u)))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f503,plain,
( ~ subclass(domain_of(u),domain_of(rest_of(u)))
| spl0_8 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f505,definition,
( spl0_9
<=> subclass(domain_of(rest_of(u)),domain_of(u)) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f507,plain,
( ~ subclass(domain_of(rest_of(u)),domain_of(u))
| spl0_9 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f513,plain,
( member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),domain_of(u))
| spl0_8 ),
inference(unit_resulting_resolution,[],[f2,f503]) ).
fof(f515,definition,
( spl0_10
<=> member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),domain_of(u)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f517,plain,
( member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),domain_of(u))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f518,plain,
( spl0_10
| spl0_8 ),
inference(avatar_split_clause,[],[f513,f501,f515]) ).
fof(f523,plain,
( member(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),domain_of(rest_of(u)))
| spl0_9 ),
inference(unit_resulting_resolution,[],[f2,f507]) ).
fof(f525,definition,
( spl0_11
<=> member(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),domain_of(rest_of(u))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f527,plain,
( member(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),domain_of(rest_of(u)))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f528,plain,
( spl0_11
| spl0_9 ),
inference(avatar_split_clause,[],[f523,f505,f525]) ).
fof(f531,plain,
( member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f1,f4,f517]) ).
fof(f582,definition,
( spl0_14
<=> member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f584,plain,
( member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f582]) ).
fof(f585,plain,
( spl0_14
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f531,f515,f582]) ).
fof(f586,plain,
( null_class != intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))
| ~ spl0_11 ),
inference(unit_resulting_resolution,[],[f201,f527]) ).
fof(f621,plain,
( ~ subclass(domain_of(rest_of(u)),domain_of(u))
| spl0_1
| ~ spl0_8 ),
inference(unit_resulting_resolution,[],[f7,f276,f502]) ).
fof(f660,definition,
( spl0_17
<=> null_class = intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f662,plain,
( null_class != intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))
| spl0_17 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( ~ spl0_17
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f586,f525,f660]) ).
fof(f667,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))
| spl0_17 ),
inference(unit_resulting_resolution,[],[f68,f662]) ).
fof(f955,definition,
( spl0_26
<=> member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f957,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f958,plain,
( spl0_26
| spl0_17 ),
inference(avatar_split_clause,[],[f667,f660,f955]) ).
fof(f967,plain,
( member(unordered_pair(unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),not_subclass_element(domain_of(u),domain_of(rest_of(u)))),unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),unordered_pair(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class))))),rest_of(u))
| ~ spl0_10 ),
inference(unit_resulting_resolution,[],[f271,f517]) ).
fof(f1109,plain,
( ! [X0] : member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),unordered_pair(X0,not_subclass_element(domain_of(u),domain_of(rest_of(u)))))
| ~ spl0_14 ),
inference(unit_resulting_resolution,[],[f10,f584]) ).
fof(f1129,definition,
( spl0_28
<=> member(unordered_pair(unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),not_subclass_element(domain_of(u),domain_of(rest_of(u)))),unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),unordered_pair(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class))))),rest_of(u)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1131,plain,
( member(unordered_pair(unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),not_subclass_element(domain_of(u),domain_of(rest_of(u)))),unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),unordered_pair(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class))))),rest_of(u))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1129]) ).
fof(f1132,plain,
( spl0_28
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f967,f515,f1129]) ).
fof(f1592,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))
| spl0_17 ),
inference(unit_resulting_resolution,[],[f312,f662]) ).
fof(f1638,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),rest_of(u))
| ~ spl0_26 ),
inference(resolution,[],[f957,f21]) ).
fof(f2166,definition,
( spl0_43
<=> member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),rest_of(u)) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f2168,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),rest_of(u))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f2166]) ).
fof(f2169,plain,
( spl0_43
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1638,f955,f2166]) ).
fof(f2437,definition,
( spl0_45
<=> null_class = domain_of(null_class) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f2438,plain,
( null_class != domain_of(null_class)
| spl0_45 ),
inference(avatar_component_clause,[],[f2437]) ).
fof(f2439,plain,
( null_class = domain_of(null_class)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f2437]) ).
fof(f2626,definition,
( spl0_49
<=> member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f2628,plain,
( member(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f2626]) ).
fof(f2629,plain,
( spl0_49
| spl0_17 ),
inference(avatar_split_clause,[],[f1592,f660,f2626]) ).
fof(f2635,plain,
( member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),domain_of(u))
| ~ spl0_43
| ~ spl0_49 ),
inference(unit_resulting_resolution,[],[f319,f2168,f2628]) ).
fof(f2642,plain,
( member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))))
| ~ spl0_49 ),
inference(unit_resulting_resolution,[],[f367,f2628,f2628]) ).
fof(f2799,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f438,f7]) ).
fof(f2802,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f2799]) ).
fof(f2804,definition,
( spl0_51
<=> member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),domain_of(u)) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f2806,plain,
( member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),domain_of(u))
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f2804]) ).
fof(f2807,plain,
( spl0_51
| ~ spl0_43
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f2635,f2626,f2166,f2804]) ).
fof(f3767,definition,
( spl0_56
<=> member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u)))) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f3769,plain,
( member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))))
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f3767]) ).
fof(f3770,plain,
( spl0_56
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f2642,f2626,f3767]) ).
fof(f3817,plain,
( member(first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class)))),intersection(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),domain_of(u)))
| ~ spl0_51
| ~ spl0_56 ),
inference(unit_resulting_resolution,[],[f23,f2806,f3769]) ).
fof(f3876,plain,
( not_subclass_element(domain_of(rest_of(u)),domain_of(u)) = first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))))
| not_subclass_element(domain_of(rest_of(u)),domain_of(u)) = first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))))
| ~ spl0_56 ),
inference(resolution,[],[f3769,f8]) ).
fof(f3882,plain,
( not_subclass_element(domain_of(rest_of(u)),domain_of(u)) = first(regular(intersection(rest_of(u),cross_product(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),universal_class))))
| ~ spl0_56 ),
inference(duplicate_literal_removal,[],[f3876]) ).
fof(f3888,plain,
( member(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),intersection(unordered_pair(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),not_subclass_element(domain_of(rest_of(u)),domain_of(u))),domain_of(u)))
| ~ spl0_51
| ~ spl0_56 ),
inference(forward_demodulation,[],[f3817,f3882]) ).
fof(f5352,plain,
( ~ spl0_9
| spl0_1
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f621,f501,f274,f505]) ).
fof(f5358,plain,
( ! [X0] : ~ member(not_subclass_element(domain_of(rest_of(u)),domain_of(u)),intersection(X0,domain_of(u)))
| spl0_9 ),
inference(unit_resulting_resolution,[],[f280,f306,f507]) ).
fof(f5372,plain,
( $false
| spl0_9
| ~ spl0_51
| ~ spl0_56 ),
inference(backward_subsumption_resolution,[],[f3888,f5358]) ).
fof(f5373,plain,
( spl0_9
| ~ spl0_51
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[],[f5372]) ).
fof(f5485,plain,
( member(unordered_pair(unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),not_subclass_element(domain_of(u),domain_of(rest_of(u)))),unordered_pair(not_subclass_element(domain_of(u),domain_of(rest_of(u))),unordered_pair(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class))))),cross_product(universal_class,universal_class))
| ~ spl0_28 ),
inference(unit_resulting_resolution,[],[f1,f156,f1131]) ).
fof(f5641,plain,
( ~ member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),domain_of(rest_of(u)))
| spl0_8 ),
inference(unit_resulting_resolution,[],[f280,f268,f503]) ).
fof(f5830,definition,
( spl0_85
<=> member(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),universal_class) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f5831,plain,
( member(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),universal_class)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f5830]) ).
fof(f5832,plain,
( ~ member(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),universal_class)
| spl0_85 ),
inference(avatar_component_clause,[],[f5830]) ).
fof(f5844,plain,
( ! [X0,X1] : ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class)),intersection(u,cross_product(not_subclass_element(domain_of(u),domain_of(rest_of(u))),universal_class))))),cross_product(X1,universal_class))
| spl0_85 ),
inference(unit_resulting_resolution,[],[f195,f5832]) ).
fof(f5849,plain,
( $false
| ~ spl0_28
| spl0_85 ),
inference(backward_subsumption_resolution,[],[f5485,f5844]) ).
fof(f5850,plain,
( ~ spl0_28
| spl0_85 ),
inference(avatar_contradiction_clause,[],[f5849]) ).
fof(f6748,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f2802,f301]) ).
fof(f6774,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f201,f6748]) ).
fof(f6782,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f6774]) ).
fof(f6784,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl0_45 ),
inference(forward_demodulation,[],[f6782,f2439]) ).
fof(f6814,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)) )
| ~ spl0_45 ),
inference(backward_subsumption_resolution,[],[f360,f6784]) ).
fof(f6827,plain,
( member(not_subclass_element(domain_of(u),domain_of(rest_of(u))),domain_of(rest_of(u)))
| ~ spl0_14
| ~ spl0_28
| ~ spl0_45
| ~ spl0_85 ),
inference(unit_resulting_resolution,[],[f6814,f584,f1109,f5831,f1131]) ).
fof(f6850,plain,
( $false
| spl0_8
| ~ spl0_14
| ~ spl0_28
| ~ spl0_45
| ~ spl0_85 ),
inference(backward_subsumption_resolution,[],[f5641,f6827]) ).
fof(f6851,plain,
( spl0_8
| ~ spl0_14
| ~ spl0_28
| ~ spl0_45
| ~ spl0_85 ),
inference(avatar_contradiction_clause,[],[f6850]) ).
fof(f6977,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f6782,f68]) ).
fof(f6983,plain,
( $false
| spl0_45 ),
inference(backward_subsumption_resolution,[],[f2438,f6977]) ).
fof(f6984,plain,
spl0_45,
inference(avatar_contradiction_clause,[],[f6983]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f277]) ).
cnf(s7,plain,
( spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f518]) ).
cnf(s8,plain,
( spl0_9
| spl0_11 ),
inference(sat_conversion,[],[f528]) ).
cnf(s11,plain,
( ~ spl0_10
| spl0_14 ),
inference(sat_conversion,[],[f585]) ).
cnf(s15,plain,
( ~ spl0_11
| ~ spl0_17 ),
inference(sat_conversion,[],[f663]) ).
cnf(s26,plain,
( spl0_17
| spl0_26 ),
inference(sat_conversion,[],[f958]) ).
cnf(s33,plain,
( ~ spl0_10
| spl0_28 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s56,plain,
( ~ spl0_26
| spl0_43 ),
inference(sat_conversion,[],[f2169]) ).
cnf(s62,plain,
( spl0_17
| spl0_49 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s64,plain,
( ~ spl0_43
| ~ spl0_49
| spl0_51 ),
inference(sat_conversion,[],[f2807]) ).
cnf(s73,plain,
( ~ spl0_49
| spl0_56 ),
inference(sat_conversion,[],[f3770]) ).
cnf(s99,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f5352]) ).
cnf(s102,plain,
( spl0_9
| ~ spl0_51
| ~ spl0_56 ),
inference(sat_conversion,[],[f5373]) ).
cnf(s105,plain,
( ~ spl0_28
| spl0_85 ),
inference(sat_conversion,[],[f5850]) ).
cnf(s131,plain,
( spl0_8
| ~ spl0_14
| ~ spl0_28
| ~ spl0_45
| ~ spl0_85 ),
inference(sat_conversion,[],[f6851]) ).
cnf(s132,plain,
spl0_45,
inference(sat_conversion,[],[f6984]) ).
cnf(s133,plain,
( spl0_8
| ~ spl0_14
| ~ spl0_28
| ~ spl0_85 ),
inference(rat,[],[s131,s132]) ).
cnf(s136,plain,
spl0_8,
inference(rat,[],[s133,s105,s11,s33,s7]) ).
cnf(s137,plain,
~ spl0_9,
inference(rat,[],[s99,s1,s136]) ).
cnf(s138,plain,
spl0_11,
inference(rat,[],[s8,s137]) ).
cnf(s141,plain,
~ spl0_17,
inference(rat,[],[s15,s138]) ).
cnf(s147,plain,
spl0_49,
inference(rat,[],[s62,s141]) ).
cnf(s149,plain,
spl0_26,
inference(rat,[],[s26,s141]) ).
cnf(s155,plain,
spl0_56,
inference(rat,[],[s73,s147]) ).
cnf(s156,plain,
spl0_43,
inference(rat,[],[s56,s149]) ).
cnf(s159,plain,
~ spl0_51,
inference(rat,[],[s102,s137,s155]) ).
cnf(s160,plain,
$false,
inference(rat,[],[s64,s147,s159,s156]) ).
fof(f7103,plain,
$false,
inference(avatar_sat_refutation,[],[s160]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM219-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 19:17:47 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.49/2.66 % (2938858)Input is clausal, will run a generic CNF schedule.
% 12.49/2.66 % (2938863)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=2181184952:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.49/2.66 % (2938869)dis-21_1_sil=8000:lcm=predicate:random_seed=3212533591: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.49/2.66 % (2938867)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=941619775:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.49/2.66 % (2938865)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4062569107:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.49/2.66 % (2938866)lrs+10_1_sil=8000:sp=occurrence:random_seed=813869460:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.49/2.66 % (2938864)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3829957179:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.49/2.66 % (2938868)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1707972462:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.49/2.66 % (2938866)Instruction limit reached!
% 12.49/2.66 % (2938866)------------------------------
% 12.49/2.66 % (2938866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (2938866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (2938866)CaDiCaL version: 2.1.3
% 12.49/2.66 % (2938866)Termination reason: Instruction limit
% 12.49/2.66 % (2938866)Termination phase: Saturation
% 12.49/2.66 % (2938866)Time elapsed: 0.056 s
% 12.49/2.66 % (2938866)Peak memory usage: 89 MB
% 12.49/2.66 % (2938866)Instructions burned: 108 (million)
% 12.49/2.66 % (2938867)Instruction limit reached!
% 12.49/2.66 % (2938867)------------------------------
% 12.49/2.66 % (2938867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (2938867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (2938867)CaDiCaL version: 2.1.3
% 12.49/2.66 % (2938867)Termination reason: Instruction limit
% 12.49/2.66 % (2938867)Termination phase: Saturation
% 12.49/2.66 % (2938867)Time elapsed: 0.071 s
% 12.49/2.66 % (2938867)Peak memory usage: 89 MB
% 12.49/2.66 % (2938867)Instructions burned: 115 (million)
% 12.49/2.66 % (2938869)Instruction limit reached!
% 12.49/2.66 % (2938869)------------------------------
% 12.49/2.66 % (2938869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (2938869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (2938869)CaDiCaL version: 2.1.3
% 12.49/2.66 % (2938869)Termination reason: Instruction limit
% 12.49/2.66 % (2938869)Termination phase: Saturation
% 12.49/2.66 % (2938869)Time elapsed: 0.074 s
% 12.49/2.66 % (2938869)Peak memory usage: 89 MB
% 12.49/2.66 % (2938869)Instructions burned: 118 (million)
% 12.49/2.66 % (2938868)Instruction limit reached!
% 12.49/2.66 % (2938868)------------------------------
% 12.49/2.66 % (2938868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (2938868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (2938868)CaDiCaL version: 2.1.3
% 12.49/2.66 % (2938868)Termination reason: Instruction limit
% 12.49/2.66 % (2938868)Termination phase: Saturation
% 12.49/2.66 % (2938868)Time elapsed: 0.136 s
% 12.49/2.66 % (2938868)Peak memory usage: 91 MB
% 12.49/2.66 % (2938868)Instructions burned: 181 (million)
% 12.49/2.66 % (2938877)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=4215555848:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.49/2.66 % (2938877)Refutation not found, incomplete strategy
% 12.49/2.66 % (2938877)------------------------------
% 12.49/2.66 % (2938877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (2938877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (2938877)CaDiCaL version: 2.1.3
% 12.49/2.66 % (2938877)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.66 % (2938877)Time elapsed: 0.002 s
% 12.49/2.66 % (2938877)Peak memory usage: 88 MB
% 12.49/2.66 % (2938877)Instructions burned: 1 (million)
% 12.49/2.66 % (2938879)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1850784385:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 22.92/4.05 % (2938878)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3115966665: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)
% 22.92/4.05 % (2938880)lrs+10_64_to=lpo:sil=8000:random_seed=1905898554:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 22.92/4.05 % (2938878)Instruction limit reached!
% 22.92/4.05 % (2938878)------------------------------
% 22.92/4.05 % (2938878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.05 % (2938878)CaDiCaL version: 2.1.3
% 22.92/4.05 % (2938878)Termination reason: Instruction limit
% 22.92/4.05 % (2938878)Termination phase: Saturation
% 22.92/4.05 % (2938878)Time elapsed: 0.108 s
% 22.92/4.05 % (2938878)Peak memory usage: 90 MB
% 22.92/4.05 % (2938878)Instructions burned: 189 (million)
% 22.92/4.05 % (2938879)Instruction limit reached!
% 22.92/4.05 % (2938879)------------------------------
% 22.92/4.05 % (2938879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.05 % (2938879)CaDiCaL version: 2.1.3
% 22.92/4.05 % (2938879)Termination reason: Instruction limit
% 22.92/4.05 % (2938879)Termination phase: Saturation
% 22.92/4.05 % (2938879)Time elapsed: 0.131 s
% 22.92/4.05 % (2938879)Peak memory usage: 89 MB
% 22.92/4.05 % (2938879)Instructions burned: 221 (million)
% 22.92/4.05 % (2938880)Instruction limit reached!
% 22.92/4.05 % (2938880)------------------------------
% 22.92/4.05 % (2938880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.05 % (2938880)CaDiCaL version: 2.1.3
% 22.92/4.05 % (2938880)Termination reason: Instruction limit
% 22.92/4.05 % (2938880)Termination phase: Saturation
% 22.92/4.05 % (2938880)Time elapsed: 0.082 s
% 22.92/4.05 % (2938880)Peak memory usage: 89 MB
% 22.92/4.05 % (2938880)Instructions burned: 126 (million)
% 22.92/4.05 % (2938877)------------------------------
% 22.92/4.05 % (2938877)------------------------------
% 22.92/4.05 % (2938885)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=300449769:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 22.92/4.05 % (2938886)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1060418135:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 22.92/4.05 % (2938887)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1171604530:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 22.92/4.05 % (2938885)Instruction limit reached!
% 22.92/4.05 % (2938885)------------------------------
% 22.92/4.05 % (2938885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.05 % (2938885)CaDiCaL version: 2.1.3
% 22.92/4.05 % (2938885)Termination reason: Instruction limit
% 22.92/4.05 % (2938885)Termination phase: Saturation
% 22.92/4.05 % (2938885)Time elapsed: 0.120 s
% 22.92/4.05 % (2938885)Peak memory usage: 90 MB
% 22.92/4.05 % (2938885)Instructions burned: 195 (million)
% 22.92/4.05 % (2938888)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=4059812558:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 22.92/4.05 % (2938886)Instruction limit reached!
% 22.92/4.05 % (2938886)------------------------------
% 22.92/4.05 % (2938886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.92/4.05 % (2938886)CaDiCaL version: 2.1.3
% 22.92/4.05 % (2938886)Termination reason: Instruction limit
% 22.92/4.05 % (2938886)Termination phase: Saturation
% 22.92/4.05 % (2938886)Time elapsed: 0.111 s
% 22.92/4.05 % (2938886)Peak memory usage: 91 MB
% 22.92/4.05 % (2938886)Instructions burned: 158 (million)
% 22.92/4.05 % (2938888)Instruction limit reached!
% 22.92/4.05 % (2938888)------------------------------
% 22.92/4.05 % (2938888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.92/4.05 % (2938888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938888)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938888)Termination reason: Instruction limit
% 35.98/5.94 % (2938888)Termination phase: Saturation
% 35.98/5.94 % (2938888)Time elapsed: 0.063 s
% 35.98/5.94 % (2938888)Peak memory usage: 90 MB
% 35.98/5.94 % (2938888)Instructions burned: 106 (million)
% 35.98/5.94 % (2938892)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=93843535:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 35.98/5.94 % (2938892)Refutation not found, incomplete strategy
% 35.98/5.94 % (2938892)------------------------------
% 35.98/5.94 % (2938892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.98/5.94 % (2938892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938892)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938892)Termination reason: Refutation not found, incomplete strategy
% 35.98/5.94 % (2938892)Time elapsed: 0.007 s
% 35.98/5.94 % (2938892)Peak memory usage: 88 MB
% 35.98/5.94 % (2938892)Instructions burned: 11 (million)
% 35.98/5.94 % (2938894)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1117697004:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 35.98/5.94 % (2938895)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3753569802:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 35.98/5.94 % (2938894)Instruction limit reached!
% 35.98/5.94 % (2938894)------------------------------
% 35.98/5.94 % (2938894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.98/5.94 % (2938894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938894)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938894)Termination reason: Instruction limit
% 35.98/5.94 % (2938894)Termination phase: Saturation
% 35.98/5.94 % (2938894)Time elapsed: 0.165 s
% 35.98/5.94 % (2938894)Peak memory usage: 90 MB
% 35.98/5.94 % (2938894)Instructions burned: 242 (million)
% 35.98/5.94 % (2938892)------------------------------
% 35.98/5.94 % (2938892)------------------------------
% 35.98/5.94 % (2938899)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=899506134:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 35.98/5.94 % (2938899)Refutation not found, incomplete strategy
% 35.98/5.94 % (2938899)------------------------------
% 35.98/5.94 % (2938899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.98/5.94 % (2938899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938899)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938899)Termination reason: Refutation not found, incomplete strategy
% 35.98/5.94 % (2938899)Time elapsed: 0.003 s
% 35.98/5.94 % (2938899)Peak memory usage: 88 MB
% 35.98/5.94 % (2938899)Instructions burned: 3 (million)
% 35.98/5.94 % (2938900)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2034480870:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 35.98/5.94 % (2938899)------------------------------
% 35.98/5.94 % (2938899)------------------------------
% 35.98/5.94 % (2938900)Instruction limit reached!
% 35.98/5.94 % (2938900)------------------------------
% 35.98/5.94 % (2938900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.98/5.94 % (2938900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938900)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938900)Termination reason: Instruction limit
% 35.98/5.94 % (2938900)Termination phase: Saturation
% 35.98/5.94 % (2938900)Time elapsed: 0.302 s
% 35.98/5.94 % (2938900)Peak memory usage: 93 MB
% 35.98/5.94 % (2938900)Instructions burned: 500 (million)
% 35.98/5.94 % (2938903)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3331025930:i=191:fgj=on:bd=all_2984 on theBenchmark for (2984ds/191Mi)
% 35.98/5.94 % (2938903)Instruction limit reached!
% 35.98/5.94 % (2938903)------------------------------
% 35.98/5.94 % (2938903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.98/5.94 % (2938903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.98/5.94 % (2938903)CaDiCaL version: 2.1.3
% 35.98/5.94 % (2938903)Termination reason: Instruction limit
% 35.98/5.94 % (2938903)Termination phase: Saturation
% 35.98/5.94 % (2938903)Time elapsed: 0.106 s
% 35.98/5.94 % (2938903)Peak memory usage: 89 MB
% 35.98/5.94 % (2938903)Instructions burned: 192 (million)
% 59.39/9.26 % (2938904)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1330646094:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 59.39/9.26 % (2938906)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=311753313:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi)
% 59.39/9.26 % (2938904)Instruction limit reached!
% 59.39/9.26 % (2938904)------------------------------
% 59.39/9.26 % (2938904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.39/9.26 % (2938904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.39/9.26 % (2938904)CaDiCaL version: 2.1.3
% 59.39/9.26 % (2938904)Termination reason: Instruction limit
% 59.39/9.26 % (2938904)Termination phase: Saturation
% 59.39/9.26 % (2938904)Time elapsed: 0.173 s
% 59.39/9.26 % (2938904)Peak memory usage: 92 MB
% 59.39/9.26 % (2938904)Instructions burned: 264 (million)
% 59.39/9.26 % (2938906)Instruction limit reached!
% 59.39/9.26 % (2938906)------------------------------
% 59.39/9.26 % (2938906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.39/9.26 % (2938906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.39/9.26 % (2938906)CaDiCaL version: 2.1.3
% 59.39/9.26 % (2938906)Termination reason: Instruction limit
% 59.39/9.26 % (2938906)Termination phase: Saturation
% 59.39/9.26 % (2938906)Time elapsed: 0.109 s
% 59.39/9.26 % (2938906)Peak memory usage: 90 MB
% 59.39/9.26 % (2938906)Instructions burned: 157 (million)
% 59.39/9.26 % (2938909)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=423500050:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi)
% 59.39/9.26 % (2938910)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=387075634:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 59.39/9.26 % (2938910)Instruction limit reached!
% 59.39/9.26 % (2938910)------------------------------
% 59.39/9.26 % (2938910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.39/9.26 % (2938910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.39/9.26 % (2938910)CaDiCaL version: 2.1.3
% 59.39/9.26 % (2938910)Termination reason: Instruction limit
% 59.39/9.26 % (2938910)Termination phase: Saturation
% 59.39/9.26 % (2938910)Time elapsed: 0.268 s
% 59.39/9.26 % (2938910)Peak memory usage: 89 MB
% 59.39/9.26 % (2938910)Instructions burned: 537 (million)
% 59.39/9.26 % (2938913)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2744230994:i=180:bd=preordered:av=off_2974 on theBenchmark for (2974ds/180Mi)
% 59.39/9.26 % (2938913)Instruction limit reached!
% 59.39/9.26 % (2938913)------------------------------
% 59.39/9.26 % (2938913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.39/9.26 % (2938913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.39/9.26 % (2938913)CaDiCaL version: 2.1.3
% 59.39/9.26 % (2938913)Termination reason: Instruction limit
% 59.39/9.26 % (2938913)Termination phase: Saturation
% 59.39/9.26 % (2938913)Time elapsed: 0.107 s
% 59.39/9.26 % (2938913)Peak memory usage: 90 MB
% 59.39/9.26 % (2938913)Instructions burned: 180 (million)
% 59.39/9.26 % (2938887)Instruction limit reached!
% 59.39/9.26 % (2938887)------------------------------
% 59.39/9.26 % (2938887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.39/9.26 % (2938887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.39/9.26 % (2938887)CaDiCaL version: 2.1.3
% 59.39/9.26 % (2938887)Termination reason: Instruction limit
% 59.39/9.26 % (2938887)Termination phase: Saturation
% 59.39/9.26 % (2938887)Time elapsed: 2.120 s
% 59.39/9.26 % (2938887)Peak memory usage: 147 MB
% 59.39/9.26 % (2938887)Instructions burned: 3395 (million)
% 59.39/9.26 % (2938915)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=4154623697:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 59.39/9.26 % (2938916)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=1533493340:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 59.39/9.26 % (2938916)Instruction limit reached!
% 59.39/9.26 % (2938916)------------------------------
% 59.39/9.26 % (2938916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938916)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938916)Termination reason: Instruction limit
% 82.53/12.55 % (2938916)Termination phase: Saturation
% 82.53/12.55 % (2938916)Time elapsed: 0.186 s
% 82.53/12.55 % (2938916)Peak memory usage: 90 MB
% 82.53/12.55 % (2938916)Instructions burned: 412 (million)
% 82.53/12.55 % (2938919)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=1196522562:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 82.53/12.55 % (2938909)Instruction limit reached!
% 82.53/12.55 % (2938909)------------------------------
% 82.53/12.55 % (2938909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938909)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938909)Termination reason: Instruction limit
% 82.53/12.55 % (2938909)Termination phase: Saturation
% 82.53/12.55 % (2938909)Time elapsed: 1.854 s
% 82.53/12.55 % (2938909)Peak memory usage: 148 MB
% 82.53/12.55 % (2938909)Instructions burned: 3257 (million)
% 82.53/12.55 % (2938921)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=1526217734:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2959 on theBenchmark for (2959ds/303Mi)
% 82.53/12.55 % (2938921)Refutation not found, incomplete strategy
% 82.53/12.55 % (2938921)------------------------------
% 82.53/12.55 % (2938921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938921)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938921)Termination reason: Refutation not found, incomplete strategy
% 82.53/12.55 % (2938921)Time elapsed: 0.002 s
% 82.53/12.55 % (2938921)Peak memory usage: 88 MB
% 82.53/12.55 % (2938921)Instructions burned: 1 (million)
% 82.53/12.55 % (2938895)Instruction limit reached!
% 82.53/12.55 % (2938895)------------------------------
% 82.53/12.55 % (2938895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938895)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938895)Termination reason: Instruction limit
% 82.53/12.55 % (2938895)Termination phase: Saturation
% 82.53/12.55 % (2938895)Time elapsed: 3.259 s
% 82.53/12.55 % (2938895)Peak memory usage: 156 MB
% 82.53/12.55 % (2938895)Instructions burned: 5209 (million)
% 82.53/12.55 % (2938921)------------------------------
% 82.53/12.55 % (2938921)------------------------------
% 82.53/12.55 % (2938923)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2289505161:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 82.53/12.55 % (2938925)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3636710264:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi)
% 82.53/12.55 % (2938923)Instruction limit reached!
% 82.53/12.55 % (2938923)------------------------------
% 82.53/12.55 % (2938923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938923)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938923)Termination reason: Instruction limit
% 82.53/12.55 % (2938923)Termination phase: Saturation
% 82.53/12.55 % (2938923)Time elapsed: 0.468 s
% 82.53/12.55 % (2938923)Peak memory usage: 96 MB
% 82.53/12.55 % (2938923)Instructions burned: 721 (million)
% 82.53/12.55 % (2938925)Instruction limit reached!
% 82.53/12.55 % (2938925)------------------------------
% 82.53/12.55 % (2938925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.53/12.55 % (2938925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.53/12.55 % (2938925)CaDiCaL version: 2.1.3
% 82.53/12.55 % (2938925)Termination reason: Instruction limit
% 82.53/12.55 % (2938925)Termination phase: Saturation
% 82.53/12.55 % (2938925)Time elapsed: 0.344 s
% 82.53/12.55 % (2938925)Peak memory usage: 91 MB
% 82.53/12.55 % (2938925)Instructions burned: 599 (million)
% 82.53/12.55 % (2938927)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3266416466:i=2989:sd=3:ss=axioms:sgt=60_2950 on theBenchmark for (2950ds/2989Mi)
% 116.25/17.27 % (2938928)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=255198230:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi)
% 116.25/17.27 % (2938928)Instruction limit reached!
% 116.25/17.27 % (2938928)------------------------------
% 116.25/17.27 % (2938928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.25/17.27 % (2938928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.25/17.27 % (2938928)CaDiCaL version: 2.1.3
% 116.25/17.27 % (2938928)Termination reason: Instruction limit
% 116.25/17.27 % (2938928)Termination phase: Saturation
% 116.25/17.27 % (2938928)Time elapsed: 1.298 s
% 116.25/17.27 % (2938928)Peak memory usage: 138 MB
% 116.25/17.27 % (2938928)Instructions burned: 1998 (million)
% 116.25/17.27 % (2938931)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=2123140362:i=2088:bd=preordered:av=off_2935 on theBenchmark for (2935ds/2088Mi)
% 116.25/17.27 % (2938927)Instruction limit reached!
% 116.25/17.27 % (2938927)------------------------------
% 116.25/17.27 % (2938927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.25/17.27 % (2938927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.25/17.27 % (2938927)CaDiCaL version: 2.1.3
% 116.25/17.27 % (2938927)Termination reason: Instruction limit
% 116.25/17.27 % (2938927)Termination phase: Saturation
% 116.25/17.27 % (2938927)Time elapsed: 1.845 s
% 116.25/17.27 % (2938927)Peak memory usage: 142 MB
% 116.25/17.27 % (2938927)Instructions burned: 2989 (million)
% 116.25/17.27 % (2938933)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=191342373:i=1098:nicw=on_2930 on theBenchmark for (2930ds/1098Mi)
% 116.25/17.27 % (2938933)Instruction limit reached!
% 116.25/17.27 % (2938933)------------------------------
% 116.25/17.27 % (2938933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.25/17.27 % (2938933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.25/17.27 % (2938933)CaDiCaL version: 2.1.3
% 116.25/17.27 % (2938933)Termination reason: Instruction limit
% 116.25/17.27 % (2938933)Termination phase: Saturation
% 116.25/17.27 % (2938933)Time elapsed: 0.669 s
% 116.25/17.27 % (2938933)Peak memory usage: 102 MB
% 116.25/17.27 % (2938933)Instructions burned: 1098 (million)
% 116.25/17.27 % (2938931)Instruction limit reached!
% 116.25/17.27 % (2938931)------------------------------
% 116.25/17.27 % (2938931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.25/17.27 % (2938931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.25/17.27 % (2938931)CaDiCaL version: 2.1.3
% 116.25/17.27 % (2938931)Termination reason: Instruction limit
% 116.25/17.27 % (2938931)Termination phase: Saturation
% 116.25/17.27 % (2938931)Time elapsed: 1.325 s
% 116.25/17.27 % (2938931)Peak memory usage: 138 MB
% 116.25/17.27 % (2938931)Instructions burned: 2089 (million)
% 116.25/17.27 % (2938935)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3314189034:i=433:bd=preordered_2922 on theBenchmark for (2922ds/433Mi)
% 116.25/17.27 % (2938935)Refutation not found, incomplete strategy
% 116.25/17.27 % (2938935)------------------------------
% 116.25/17.27 % (2938935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.25/17.27 % (2938935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.25/17.27 % (2938935)CaDiCaL version: 2.1.3
% 116.25/17.27 % (2938935)Termination reason: Refutation not found, incomplete strategy
% 116.25/17.27 % (2938935)Time elapsed: 0.013 s
% 116.25/17.27 % (2938935)Peak memory usage: 89 MB
% 116.25/17.27 % (2938935)Instructions burned: 20 (million)
% 116.25/17.27 % (2938936)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3429907512:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2920 on theBenchmark for (2920ds/2942Mi)
% 116.25/17.27 % (2938935)------------------------------
% 116.25/17.27 % (2938935)------------------------------
% 116.25/17.27 % (2938939)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2049665538:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2917 on theBenchmark for (2917ds/6922Mi)
% 116.25/17.27 % (2938919)Instruction limit reached!
% 116.25/17.27 % (2938919)------------------------------
% 116.25/17.27 % (2938919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938919)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938919)Termination reason: Instruction limit
% 131.18/19.33 % (2938919)Termination phase: Saturation
% 131.18/19.33 % (2938919)Time elapsed: 5.048 s
% 131.18/19.33 % (2938919)Peak memory usage: 165 MB
% 131.18/19.33 % (2938919)Instructions burned: 8479 (million)
% 131.18/19.33 % (2938941)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=1988389988:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2915 on theBenchmark for (2915ds/596Mi)
% 131.18/19.33 % (2938941)Instruction limit reached!
% 131.18/19.33 % (2938941)------------------------------
% 131.18/19.33 % (2938941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938941)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938941)Termination reason: Instruction limit
% 131.18/19.33 % (2938941)Termination phase: Saturation
% 131.18/19.33 % (2938941)Time elapsed: 0.327 s
% 131.18/19.33 % (2938941)Peak memory usage: 99 MB
% 131.18/19.33 % (2938941)Instructions burned: 597 (million)
% 131.18/19.33 % (2938943)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=2695148119:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2910 on theBenchmark for (2910ds/4123Mi)
% 131.18/19.33 % (2938915)Instruction limit reached!
% 131.18/19.33 % (2938915)------------------------------
% 131.18/19.33 % (2938915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938915)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938915)Termination reason: Instruction limit
% 131.18/19.33 % (2938915)Termination phase: Saturation
% 131.18/19.33 % (2938915)Time elapsed: 6.524 s
% 131.18/19.33 % (2938915)Peak memory usage: 173 MB
% 131.18/19.33 % (2938915)Instructions burned: 10309 (million)
% 131.18/19.33 % (2938945)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3071572061:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2905 on theBenchmark for (2905ds/16411Mi)
% 131.18/19.33 % (2938936)Instruction limit reached!
% 131.18/19.33 % (2938936)------------------------------
% 131.18/19.33 % (2938936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938936)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938936)Termination reason: Instruction limit
% 131.18/19.33 % (2938936)Termination phase: Saturation
% 131.18/19.33 % (2938936)Time elapsed: 1.931 s
% 131.18/19.33 % (2938936)Peak memory usage: 145 MB
% 131.18/19.33 % (2938936)Instructions burned: 2942 (million)
% 131.18/19.33 % (2938947)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1559680075:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2899 on theBenchmark for (2899ds/1670Mi)
% 131.18/19.33 % (2938947)Instruction limit reached!
% 131.18/19.33 % (2938947)------------------------------
% 131.18/19.33 % (2938947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938947)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938947)Termination reason: Instruction limit
% 131.18/19.33 % (2938947)Termination phase: Saturation
% 131.18/19.33 % (2938947)Time elapsed: 1.038 s
% 131.18/19.33 % (2938947)Peak memory usage: 136 MB
% 131.18/19.33 % (2938947)Instructions burned: 1671 (million)
% 131.18/19.33 % (2938949)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=3872652286:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2887 on theBenchmark for (2887ds/1722Mi)
% 131.18/19.33 % (2938943)Instruction limit reached!
% 131.18/19.33 % (2938943)------------------------------
% 131.18/19.33 % (2938943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.18/19.33 % (2938943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.18/19.33 % (2938943)CaDiCaL version: 2.1.3
% 131.18/19.33 % (2938943)Termination reason: Instruction limit
% 131.18/19.33 % (2938943)Termination phase: Saturation
% 131.18/19.33 % (2938943)Time elapsed: 2.598 s
% 131.18/19.33 % (2938943)Peak memory usage: 157 MB
% 145.92/21.47 % (2938943)Instructions burned: 4124 (million)
% 145.92/21.47 % (2938951)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=1387369515:cts=off:cond=on:i=9530:bs=on:fsd=on_2882 on theBenchmark for (2882ds/9530Mi)
% 145.92/21.47 % (2938949)Refutation not found, incomplete strategy
% 145.92/21.47 % (2938949)------------------------------
% 145.92/21.47 % (2938949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.92/21.47 % (2938949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.92/21.47 % (2938949)CaDiCaL version: 2.1.3
% 145.92/21.47 % (2938949)Termination reason: Refutation not found, incomplete strategy
% 145.92/21.47 % (2938949)Time elapsed: 0.607 s
% 145.92/21.47 % (2938949)Peak memory usage: 129 MB
% 145.92/21.47 % (2938949)Instructions burned: 916 (million)
% 145.92/21.47 % (2938939)Instruction limit reached!
% 145.92/21.47 % (2938939)------------------------------
% 145.92/21.47 % (2938939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.92/21.47 % (2938939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.92/21.47 % (2938939)CaDiCaL version: 2.1.3
% 145.92/21.47 % (2938939)Termination reason: Instruction limit
% 145.92/21.47 % (2938939)Termination phase: Saturation
% 145.92/21.47 % (2938939)Time elapsed: 3.788 s
% 145.92/21.47 % (2938939)Peak memory usage: 164 MB
% 145.92/21.47 % (2938939)Instructions burned: 6924 (million)
% 145.92/21.47 % (2938949)------------------------------
% 145.92/21.47 % (2938949)------------------------------
% 145.92/21.47 % (2938953)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1568596957:st=2:i=4495:sd=10:ss=included_2878 on theBenchmark for (2878ds/4495Mi)
% 145.92/21.47 % (2938954)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=3692205135:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2877 on theBenchmark for (2877ds/4920Mi)
% 145.92/21.47 % (2938953)Instruction limit reached!
% 145.92/21.47 % (2938953)------------------------------
% 145.92/21.47 % (2938953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.92/21.47 % (2938953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.92/21.47 % (2938953)CaDiCaL version: 2.1.3
% 145.92/21.47 % (2938953)Termination reason: Instruction limit
% 145.92/21.47 % (2938953)Termination phase: Saturation
% 145.92/21.47 % (2938953)Time elapsed: 2.586 s
% 145.92/21.47 % (2938953)Peak memory usage: 161 MB
% 145.92/21.47 % (2938953)Instructions burned: 4496 (million)
% 145.92/21.47 % (2938957)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=1586960403:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2850 on theBenchmark for (2850ds/2083Mi)
% 145.92/21.47 % (2938954)Instruction limit reached!
% 145.92/21.47 % (2938954)------------------------------
% 145.92/21.47 % (2938954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.92/21.47 % (2938954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.92/21.47 % (2938954)CaDiCaL version: 2.1.3
% 145.92/21.47 % (2938954)Termination reason: Instruction limit
% 145.92/21.47 % (2938954)Termination phase: Saturation
% 145.92/21.47 % (2938954)Time elapsed: 3.080 s
% 145.92/21.47 % (2938954)Peak memory usage: 151 MB
% 145.92/21.47 % (2938954)Instructions burned: 4921 (million)
% 145.92/21.47 % (2938959)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=392334351:i=4629:av=off:gsp=on_2844 on theBenchmark for (2844ds/4629Mi)
% 145.92/21.47 % (2938959)Refutation not found, incomplete strategy
% 145.92/21.47 % (2938959)------------------------------
% 145.92/21.47 % (2938959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.92/21.47 % (2938959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.92/21.47 % (2938959)CaDiCaL version: 2.1.3
% 145.92/21.47 % (2938959)Termination reason: Refutation not found, incomplete strategy
% 145.92/21.47 % (2938959)Time elapsed: 0.589 s
% 145.92/21.47 % (2938959)Peak memory usage: 129 MB
% 145.92/21.47 % (2938959)Instructions burned: 893 (million)
% 145.92/21.47 % (2938957)Instruction limit reached!
% 145.92/21.47 % (2938957)------------------------------
% 145.92/21.47 % (2938957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938957)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938957)Termination reason: Instruction limit
% 83.60/22.34 % (2938957)Termination phase: Saturation
% 83.60/22.34 % (2938957)Time elapsed: 1.300 s
% 83.60/22.34 % (2938957)Peak memory usage: 137 MB
% 83.60/22.34 % (2938957)Instructions burned: 2083 (million)
% 83.60/22.34 % (2938959)------------------------------
% 83.60/22.34 % (2938959)------------------------------
% 83.60/22.34 % (2938961)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2050977270:i=1258:av=off_2835 on theBenchmark for (2835ds/1258Mi)
% 83.60/22.34 % (2938962)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3989047260:i=7343:av=off:ss=included_2834 on theBenchmark for (2834ds/7343Mi)
% 83.60/22.34 % (2938961)Instruction limit reached!
% 83.60/22.34 % (2938961)------------------------------
% 83.60/22.34 % (2938961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938961)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938961)Termination reason: Instruction limit
% 83.60/22.34 % (2938961)Termination phase: Saturation
% 83.60/22.34 % (2938961)Time elapsed: 0.722 s
% 83.60/22.34 % (2938961)Peak memory usage: 95 MB
% 83.60/22.34 % (2938961)Instructions burned: 1259 (million)
% 83.60/22.34 % (2938962)Refutation not found, incomplete strategy
% 83.60/22.34 % (2938962)------------------------------
% 83.60/22.34 % (2938962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938962)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938962)Termination reason: Refutation not found, incomplete strategy
% 83.60/22.34 % (2938962)Time elapsed: 0.602 s
% 83.60/22.34 % (2938962)Peak memory usage: 128 MB
% 83.60/22.34 % (2938962)Instructions burned: 908 (million)
% 83.60/22.34 % (2938965)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2601755153:i=1325:sd=2:ss=axioms:sgt=16_2826 on theBenchmark for (2826ds/1325Mi)
% 83.60/22.34 % (2938965)Refutation not found, incomplete strategy
% 83.60/22.34 % (2938965)------------------------------
% 83.60/22.34 % (2938965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938965)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938965)Termination reason: Refutation not found, incomplete strategy
% 83.60/22.34 % (2938965)Time elapsed: 0.002 s
% 83.60/22.34 % (2938965)Peak memory usage: 88 MB
% 83.60/22.34 % (2938965)Instructions burned: 1 (million)
% 83.60/22.34 % (2938962)------------------------------
% 83.60/22.34 % (2938962)------------------------------
% 83.60/22.34 % (2938965)------------------------------
% 83.60/22.34 % (2938965)------------------------------
% 83.60/22.34 % (2938967)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=465587704:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2824 on theBenchmark for (2824ds/2646Mi)
% 83.60/22.34 % (2938968)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1702349238:i=1489:sd=2:ep=R:ss=axioms_2822 on theBenchmark for (2822ds/1489Mi)
% 83.60/22.34 % (2938951)Instruction limit reached!
% 83.60/22.34 % (2938951)------------------------------
% 83.60/22.34 % (2938951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938951)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938951)Termination reason: Instruction limit
% 83.60/22.34 % (2938951)Termination phase: Saturation
% 83.60/22.34 % (2938951)Time elapsed: 6.189 s
% 83.60/22.34 % (2938951)Peak memory usage: 166 MB
% 83.60/22.34 % (2938951)Instructions burned: 9532 (million)
% 83.60/22.34 % (2938971)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=1341154360:i=1503_2819 on theBenchmark for (2819ds/1503Mi)
% 83.60/22.34 % (2938968)Refutation not found, incomplete strategy
% 83.60/22.34 % (2938968)------------------------------
% 83.60/22.34 % (2938968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938968)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938968)Termination reason: Refutation not found, incomplete strategy
% 83.60/22.34 % (2938968)Time elapsed: 0.596 s
% 83.60/22.34 % (2938968)Peak memory usage: 128 MB
% 83.60/22.34 % (2938968)Instructions burned: 896 (million)
% 83.60/22.34 % (2938968)------------------------------
% 83.60/22.34 % (2938968)------------------------------
% 83.60/22.34 % (2938974)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3591725108:i=13942:kws=frequency_2812 on theBenchmark for (2812ds/13942Mi)
% 83.60/22.34 % (2938971)Instruction limit reached!
% 83.60/22.34 % (2938971)------------------------------
% 83.60/22.34 % (2938971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938971)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938971)Termination reason: Instruction limit
% 83.60/22.34 % (2938971)Termination phase: Saturation
% 83.60/22.34 % (2938971)Time elapsed: 1.001 s
% 83.60/22.34 % (2938971)Peak memory usage: 134 MB
% 83.60/22.34 % (2938971)Instructions burned: 1504 (million)
% 83.60/22.34 % (2938967)Instruction limit reached!
% 83.60/22.34 % (2938967)------------------------------
% 83.60/22.34 % (2938967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938967)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938967)Termination reason: Instruction limit
% 83.60/22.34 % (2938967)Termination phase: Saturation
% 83.60/22.34 % (2938967)Time elapsed: 1.710 s
% 83.60/22.34 % (2938967)Peak memory usage: 144 MB
% 83.60/22.34 % (2938967)Instructions burned: 2647 (million)
% 83.60/22.34 % (2938976)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=4214095176:i=3604:fsr=off:er=filter_2807 on theBenchmark for (2807ds/3604Mi)
% 83.60/22.34 % (2938978)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3948050732:i=1876:sd=1:ss=included:sgt=32_2805 on theBenchmark for (2805ds/1876Mi)
% 83.60/22.34 % (2938945)Instruction limit reached!
% 83.60/22.34 % (2938945)------------------------------
% 83.60/22.34 % (2938945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938945)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938945)Termination reason: Instruction limit
% 83.60/22.34 % (2938945)Termination phase: Saturation
% 83.60/22.34 % (2938945)Time elapsed: 10.011 s
% 83.60/22.34 % (2938945)Peak memory usage: 223 MB
% 83.60/22.34 % (2938945)Instructions burned: 16414 (million)
% 83.60/22.34 % (2938980)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1052024853:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2803 on theBenchmark for (2803ds/1932Mi)
% 83.60/22.34 % (2938978)Refutation not found, incomplete strategy
% 83.60/22.34 % (2938978)------------------------------
% 83.60/22.34 % (2938978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938978)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938978)Termination reason: Refutation not found, incomplete strategy
% 83.60/22.34 % (2938978)Time elapsed: 0.571 s
% 83.60/22.34 % (2938978)Peak memory usage: 128 MB
% 83.60/22.34 % (2938978)Instructions burned: 863 (million)
% 83.60/22.34 % (2938980)Refutation not found, incomplete strategy
% 83.60/22.34 % (2938980)------------------------------
% 83.60/22.34 % (2938980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.60/22.34 % (2938980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.60/22.34 % (2938980)CaDiCaL version: 2.1.3
% 83.60/22.34 % (2938980)Termination reason: Refutation not found, incomplete strategy
% 83.60/22.34 % (2938980)Time elapsed: 0.573 s
% 83.60/22.34 % (2938980)Peak memory usage: 128 MB
% 83.60/22.34 % (2938980)Instructions burned: 862 (million)
% 83.60/22.34 % (2938978)------------------------------
% 83.60/22.34 % (2938978)------------------------------
% 83.60/22.34 % (2938982)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=863522061:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2795 on theBenchmark for (2795ds/1980Mi)
% 83.60/22.34 % (2938980)------------------------------
% 83.60/22.34 % (2938980)------------------------------
% 83.60/22.34 % (2938984)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=3907607796:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2793 on theBenchmark for (2793ds/3902Mi)
% 83.60/22.34 % (2938976)First to succeed.
% 83.60/22.34 % (2938976)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2938858"
% 83.60/22.34 % (2938976)Refutation found. Thanks to Tanya!
% 83.60/22.34 % SZS status Unsatisfiable for theBenchmark
% 83.60/22.34 % SZS output start Proof for theBenchmark
% See solution above
% 152.70/22.54 % (2938976)------------------------------
% 152.70/22.54 % (2938976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.70/22.54 % (2938976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.70/22.54 % (2938976)CaDiCaL version: 2.1.3
% 152.70/22.54 % (2938976)Termination reason: Refutation
% 152.70/22.54 % (2938976)Time elapsed: 1.705 s
% 152.70/22.54 % (2938976)Peak memory usage: 145 MB
% 152.70/22.54 % (2938976)Instructions burned: 2715 (million)
% 152.70/22.54 % (2938976)------------------------------
% 152.70/22.54 % (2938976)------------------------------
% 152.70/22.54 % (2938858)Success in time 21.484 s
% 152.70/22.54 % Vampire exiting
%------------------------------------------------------------------------------