%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM077-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 : n007.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:42 PM UTC 2026
% Result : Unsatisfiable 74.65s 11.33s
% Output : Refutation 76.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 68
% Syntax : Number of formulae : 297 ( 64 unt; 43 def)
% Number of atoms : 709 ( 110 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 787 ( 375 ~; 373 |; 0 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 40 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 9 con; 0-3 aty)
% Number of variables : 163 ( 0 sgn 163 !; 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(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(f9,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
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(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(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
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(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(f133,axiom,
! [X2,X0,X1] : segment(X0,X1,X2) = domain_of(restrict(X0,X1,singleton(X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',segment) ).
fof(f135,axiom,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| X2 = null_class
| member(least(X0,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_ordering2) ).
fof(f136,plain,
! [X2,X0,X1] :
( member(least(X0,X2),X2)
| ~ subclass(X2,X1)
| null_class = X2
| ~ well_ordering(X0,X1) ),
inference(reorient_equations,[],[f135]) ).
fof(f140,axiom,
! [X2,X3,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| ~ member(X3,X2)
| ~ member(ordered_pair(X3,least(X0,X2)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_ordering5) ).
fof(f176,negated_conjecture,
well_ordering(xr,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_well_ordering_property7_1) ).
fof(f177,negated_conjecture,
member(u,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_well_ordering_property7_2) ).
fof(f178,negated_conjecture,
segment(xr,y,u) = y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_well_ordering_property7_3) ).
fof(f179,plain,
y = segment(xr,y,u),
inference(reorient_equations,[],[f178]) ).
fof(f180,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,X0,X1] : segment(X0,X1,X2) = domain_of(intersection(X0,cross_product(X1,unordered_pair(X2,X2)))),
inference(definition_unfolding,[],[f133,f28,f12]) ).
fof(f197,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,f180]) ).
fof(f198,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f180]) ).
fof(f200,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f180]) ).
fof(f204,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(f255,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(least(X0,X2),least(X0,X2)))),X0)
| ~ subclass(X2,X1)
| ~ member(X3,X2)
| ~ well_ordering(X0,X1) ),
inference(definition_unfolding,[],[f140,f180]) ).
fof(f270,plain,
y = domain_of(intersection(xr,cross_product(y,unordered_pair(u,u)))),
inference(definition_unfolding,[],[f179,f194]) ).
fof(f277,definition,
sF0 = unordered_pair(u,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f278,plain,
unordered_pair(u,u) = sF0,
inference(reorient_equations,[],[f277]) ).
fof(f279,definition,
sF1 = cross_product(y,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f280,plain,
cross_product(y,sF0) = sF1,
inference(reorient_equations,[],[f279]) ).
fof(f281,definition,
sF2 = intersection(xr,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f282,plain,
intersection(xr,sF1) = sF2,
inference(reorient_equations,[],[f281]) ).
fof(f283,definition,
sF3 = domain_of(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f284,plain,
domain_of(sF2) = sF3,
inference(reorient_equations,[],[f283]) ).
fof(f285,plain,
y = sF3,
inference(definition_folding,[],[f270,f284,f282,f280,f278]) ).
fof(f286,plain,
y = domain_of(sF2),
inference(forward_demodulation,[],[f284,f285]) ).
fof(f288,definition,
( spl4_1
<=> member(u,y) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f290,plain,
( member(u,y)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,plain,
spl4_1,
inference(avatar_split_clause,[],[f177,f288]) ).
fof(f293,definition,
( spl4_2
<=> well_ordering(xr,y) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f295,plain,
( well_ordering(xr,y)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f296,plain,
spl4_2,
inference(avatar_split_clause,[],[f176,f293]) ).
fof(f298,definition,
( spl4_3
<=> cross_product(y,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f300,plain,
( cross_product(y,sF0) = sF1
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,plain,
spl4_3,
inference(avatar_split_clause,[],[f280,f298]) ).
fof(f303,definition,
( spl4_4
<=> intersection(xr,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f305,plain,
( intersection(xr,sF1) = sF2
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f306,plain,
spl4_4,
inference(avatar_split_clause,[],[f282,f303]) ).
fof(f308,definition,
( spl4_5
<=> unordered_pair(u,u) = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f310,plain,
( unordered_pair(u,u) = sF0
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f311,plain,
spl4_5,
inference(avatar_split_clause,[],[f278,f308]) ).
fof(f312,plain,
( ! [X0] :
( ~ member(X0,sF2)
| member(X0,sF1) )
| ~ spl4_4 ),
inference(superposition,[],[f22,f305]) ).
fof(f313,plain,
( ! [X0] :
( ~ member(X0,sF2)
| member(X0,xr) )
| ~ spl4_4 ),
inference(superposition,[],[f21,f305]) ).
fof(f315,definition,
( spl4_6
<=> y = domain_of(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f317,plain,
( y = domain_of(sF2)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
spl4_6,
inference(avatar_split_clause,[],[f286,f315]) ).
fof(f320,definition,
( spl4_7
<=> ! [X0] :
( ~ member(X0,sF2)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f321,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,sF2) )
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( spl4_7
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f312,f303,f320]) ).
fof(f324,definition,
( spl4_8
<=> ! [X0] :
( ~ member(X0,sF2)
| member(X0,xr) ) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f325,plain,
( ! [X0] :
( member(X0,xr)
| ~ member(X0,sF2) )
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f326,plain,
( spl4_8
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f313,f303,f324]) ).
fof(f344,plain,
! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ subclass(X1,universal_class)
| member(X0,unordered_pair(X0,X2)) ),
inference(resolution,[],[f1,f9]) ).
fof(f347,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X0,X2))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[],[f344,f4]) ).
fof(f359,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,sF0) )
| ~ spl4_3 ),
inference(superposition,[],[f198,f300]) ).
fof(f361,definition,
( spl4_12
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f362,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,sF0) )
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f363,plain,
( spl4_12
| ~ spl4_3 ),
inference(avatar_split_clause,[],[f359,f298,f361]) ).
fof(f368,plain,
( ! [X0] :
( member(u,sF0)
| ~ member(u,X0) )
| ~ spl4_5 ),
inference(superposition,[],[f347,f310]) ).
fof(f369,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) )
| ~ spl4_5 ),
inference(superposition,[],[f204,f310]) ).
fof(f387,definition,
( spl4_13
<=> ! [X0] : ~ member(u,X0) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f388,plain,
( ! [X0] : ~ member(u,X0)
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f390,definition,
( spl4_14
<=> member(u,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f392,plain,
( member(u,sF0)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f393,plain,
( spl4_13
| spl4_14
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f368,f308,f390,f387]) ).
fof(f397,plain,
( $false
| ~ spl4_1
| ~ spl4_13 ),
inference(unit_resulting_resolution,[],[f23,f290,f290,f388]) ).
fof(f410,plain,
( ~ spl4_1
| ~ spl4_13 ),
inference(avatar_contradiction_clause,[],[f397]) ).
fof(f414,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0
| u = X0 )
| ~ spl4_5 ),
inference(superposition,[],[f8,f310]) ).
fof(f415,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0 )
| ~ spl4_5 ),
inference(duplicate_literal_removal,[],[f414]) ).
fof(f417,definition,
( spl4_15
<=> ! [X0] :
( ~ member(X0,sF0)
| u = X0 ) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f418,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0 )
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( spl4_15
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f415,f308,f417]) ).
fof(f422,plain,
( ! [X0] :
( u = not_subclass_element(sF0,X0)
| subclass(sF0,X0) )
| ~ spl4_15 ),
inference(resolution,[],[f418,f2]) ).
fof(f457,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f469,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f470,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f526,definition,
( spl4_20
<=> ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl4_20])],[avatar_definition]) ).
fof(f527,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) )
| ~ spl4_20 ),
inference(avatar_component_clause,[],[f526]) ).
fof(f528,plain,
( spl4_20
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f369,f308,f526]) ).
fof(f559,plain,
! [X2,X0,X1] :
( intersection(X0,cross_product(X1,X2)) = null_class
| regular(intersection(X0,cross_product(X1,X2))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),first(regular(intersection(X0,cross_product(X1,X2))))),unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),unordered_pair(second(regular(intersection(X0,cross_product(X1,X2)))),second(regular(intersection(X0,cross_product(X1,X2))))))) ),
inference(resolution,[],[f469,f200]) ).
fof(f569,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(superposition,[],[f204,f559]) ).
fof(f577,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(trivial_inequality_removal,[],[f569]) ).
fof(f586,plain,
( ! [X0] :
( ~ member(X0,y)
| regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl4_6 ),
inference(superposition,[],[f577,f317]) ).
fof(f592,definition,
( spl4_24
<=> ! [X0] :
( ~ member(X0,y)
| regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
fof(f593,plain,
( ! [X0] :
( ~ member(X0,y)
| regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF2,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( spl4_24
| ~ spl4_6 ),
inference(avatar_split_clause,[],[f586,f315,f592]) ).
fof(f600,plain,
( regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class)))),first(regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class)))),second(regular(intersection(sF2,cross_product(unordered_pair(u,u),universal_class)))))))
| ~ spl4_1
| ~ spl4_24 ),
inference(resolution,[],[f593,f290]) ).
fof(f601,plain,
( regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),first(regular(intersection(sF2,cross_product(sF0,universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),second(regular(intersection(sF2,cross_product(sF0,universal_class)))))))
| ~ spl4_1
| ~ spl4_5
| ~ spl4_24 ),
inference(forward_demodulation,[],[f600,f310]) ).
fof(f603,definition,
( spl4_25
<=> regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),first(regular(intersection(sF2,cross_product(sF0,universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),second(regular(intersection(sF2,cross_product(sF0,universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
fof(f605,plain,
( regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),first(regular(intersection(sF2,cross_product(sF0,universal_class))))),unordered_pair(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),unordered_pair(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),second(regular(intersection(sF2,cross_product(sF0,universal_class)))))))
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f606,plain,
( spl4_25
| ~ spl4_1
| ~ spl4_5
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f601,f592,f308,f288,f603]) ).
fof(f614,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF1)
| member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_12
| ~ spl4_25 ),
inference(superposition,[],[f362,f605]) ).
fof(f617,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),X0) )
| ~ spl4_25 ),
inference(superposition,[],[f197,f605]) ).
fof(f626,definition,
( spl4_26
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f627,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),X0) )
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f628,plain,
( spl4_26
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f617,f603,f626]) ).
fof(f629,plain,
( member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| null_class = intersection(sF2,cross_product(sF0,universal_class))
| ~ spl4_26 ),
inference(resolution,[],[f627,f469]) ).
fof(f642,definition,
( spl4_28
<=> member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f644,plain,
( member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl4_29
<=> member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF1) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f648,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF1)
| spl4_29 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f649,plain,
( spl4_28
| ~ spl4_29
| ~ spl4_12
| ~ spl4_25 ),
inference(avatar_split_clause,[],[f614,f603,f361,f646,f642]) ).
fof(f650,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| ~ spl4_7
| spl4_29 ),
inference(resolution,[],[f648,f321]) ).
fof(f654,definition,
( spl4_30
<=> member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f655,plain,
( member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f656,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| spl4_30 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f657,plain,
( ~ spl4_30
| ~ spl4_7
| spl4_29 ),
inference(avatar_split_clause,[],[f650,f646,f320,f654]) ).
fof(f658,plain,
( null_class = intersection(sF2,cross_product(sF0,universal_class))
| spl4_30 ),
inference(resolution,[],[f656,f470]) ).
fof(f695,plain,
( u = second(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_15
| ~ spl4_28 ),
inference(resolution,[],[f644,f418]) ).
fof(f700,definition,
( spl4_36
<=> u = second(regular(intersection(sF2,cross_product(sF0,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl4_36])],[avatar_definition]) ).
fof(f702,plain,
( u = second(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_36 ),
inference(avatar_component_clause,[],[f700]) ).
fof(f703,plain,
( spl4_36
| ~ spl4_15
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f695,f642,f417,f700]) ).
fof(f859,plain,
( ! [X0,X1] :
( ~ subclass(sF0,X0)
| null_class = sF0
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) )
| ~ spl4_15 ),
inference(resolution,[],[f136,f418]) ).
fof(f904,definition,
( spl4_46
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f905,plain,
( null_class != sF0
| spl4_46 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f906,plain,
( null_class = sF0
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f904]) ).
fof(f913,plain,
( member(u,null_class)
| ~ spl4_14
| ~ spl4_46 ),
inference(superposition,[],[f392,f906]) ).
fof(f1124,definition,
( spl4_57
<=> null_class = intersection(sF2,cross_product(sF0,universal_class)) ),
introduced(definition,[new_symbols(definition,[spl4_57])],[avatar_definition]) ).
fof(f1125,plain,
( null_class != intersection(sF2,cross_product(sF0,universal_class))
| spl4_57 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1126,plain,
( null_class = intersection(sF2,cross_product(sF0,universal_class))
| ~ spl4_57 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1128,definition,
( spl4_58
<=> member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0) ),
introduced(definition,[new_symbols(definition,[spl4_58])],[avatar_definition]) ).
fof(f1130,plain,
( member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_58 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1131,plain,
( spl4_57
| spl4_58
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f629,f626,f1128,f1124]) ).
fof(f1142,definition,
( spl4_60
<=> member(u,null_class) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1144,plain,
( member(u,null_class)
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1145,plain,
( spl4_60
| ~ spl4_14
| ~ spl4_46 ),
inference(avatar_split_clause,[],[f913,f904,f390,f1142]) ).
fof(f1146,plain,
( ! [X0] :
( member(u,X0)
| null_class = X0 )
| ~ spl4_60 ),
inference(resolution,[],[f1144,f457]) ).
fof(f1148,definition,
( spl4_61
<=> ! [X0] :
( member(u,X0)
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl4_61])],[avatar_definition]) ).
fof(f1149,plain,
( ! [X0] :
( member(u,X0)
| null_class = X0 )
| ~ spl4_61 ),
inference(avatar_component_clause,[],[f1148]) ).
fof(f1150,plain,
( spl4_61
| ~ spl4_60 ),
inference(avatar_split_clause,[],[f1146,f1142,f1148]) ).
fof(f1156,plain,
( ! [X0] :
( complement(X0) = null_class
| ~ member(u,X0) )
| ~ spl4_61 ),
inference(resolution,[],[f1149,f24]) ).
fof(f1167,definition,
( spl4_62
<=> ! [X0] :
( complement(X0) = null_class
| ~ member(u,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_62])],[avatar_definition]) ).
fof(f1168,plain,
( ! [X0] :
( ~ member(u,X0)
| complement(X0) = null_class )
| ~ spl4_62 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1169,plain,
( spl4_62
| ~ spl4_61 ),
inference(avatar_split_clause,[],[f1156,f1148,f1167]) ).
fof(f1172,plain,
( null_class = complement(y)
| ~ spl4_1
| ~ spl4_62 ),
inference(resolution,[],[f1168,f290]) ).
fof(f1188,definition,
( spl4_63
<=> null_class = complement(y) ),
introduced(definition,[new_symbols(definition,[spl4_63])],[avatar_definition]) ).
fof(f1190,plain,
( null_class = complement(y)
| ~ spl4_63 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1191,plain,
( spl4_63
| ~ spl4_1
| ~ spl4_62 ),
inference(avatar_split_clause,[],[f1172,f1167,f288,f1188]) ).
fof(f1192,plain,
( ! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,y) )
| ~ spl4_63 ),
inference(superposition,[],[f24,f1190]) ).
fof(f1194,definition,
( spl4_64
<=> ! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl4_64])],[avatar_definition]) ).
fof(f1195,plain,
( ! [X0] :
( ~ member(X0,y)
| ~ member(X0,null_class) )
| ~ spl4_64 ),
inference(avatar_component_clause,[],[f1194]) ).
fof(f1196,plain,
( spl4_64
| ~ spl4_63 ),
inference(avatar_split_clause,[],[f1192,f1188,f1194]) ).
fof(f1207,plain,
( ~ member(u,null_class)
| ~ spl4_1
| ~ spl4_64 ),
inference(resolution,[],[f1195,f290]) ).
fof(f1212,plain,
( $false
| ~ spl4_1
| ~ spl4_60
| ~ spl4_64 ),
inference(forward_subsumption_resolution,[],[f1207,f1144]) ).
fof(f1213,plain,
( ~ spl4_1
| ~ spl4_60
| ~ spl4_64 ),
inference(avatar_contradiction_clause,[],[f1212]) ).
fof(f1226,plain,
( ! [X0,X1] :
( ~ subclass(sF0,X0)
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) )
| ~ spl4_15
| spl4_46 ),
inference(forward_subsumption_resolution,[],[f859,f905]) ).
fof(f1899,definition,
( spl4_77
<=> ! [X0,X1] :
( ~ subclass(sF0,X0)
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_77])],[avatar_definition]) ).
fof(f1900,plain,
( ! [X0,X1] :
( ~ subclass(sF0,X0)
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) )
| ~ spl4_77 ),
inference(avatar_component_clause,[],[f1899]) ).
fof(f1901,plain,
( spl4_77
| ~ spl4_15
| spl4_46 ),
inference(avatar_split_clause,[],[f1226,f904,f417,f1899]) ).
fof(f1959,plain,
( null_class != null_class
| ~ member(u,domain_of(sF2))
| ~ spl4_20
| ~ spl4_57 ),
inference(superposition,[],[f527,f1126]) ).
fof(f1965,plain,
( ~ member(u,domain_of(sF2))
| ~ spl4_20
| ~ spl4_57 ),
inference(trivial_inequality_removal,[],[f1959]) ).
fof(f1967,plain,
( ~ member(u,y)
| ~ spl4_6
| ~ spl4_20
| ~ spl4_57 ),
inference(forward_demodulation,[],[f1965,f317]) ).
fof(f1971,plain,
( $false
| ~ spl4_1
| ~ spl4_6
| ~ spl4_20
| ~ spl4_57 ),
inference(forward_subsumption_resolution,[],[f1967,f290]) ).
fof(f1972,plain,
( ~ spl4_1
| ~ spl4_6
| ~ spl4_20
| ~ spl4_57 ),
inference(avatar_contradiction_clause,[],[f1971]) ).
fof(f1988,plain,
( u = first(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_15
| ~ spl4_58 ),
inference(resolution,[],[f1130,f418]) ).
fof(f2002,definition,
( spl4_84
<=> u = first(regular(intersection(sF2,cross_product(sF0,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl4_84])],[avatar_definition]) ).
fof(f2004,plain,
( u = first(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_84 ),
inference(avatar_component_clause,[],[f2002]) ).
fof(f2005,plain,
( spl4_84
| ~ spl4_15
| ~ spl4_58 ),
inference(avatar_split_clause,[],[f1988,f1128,f417,f2002]) ).
fof(f2007,plain,
( regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),second(regular(intersection(sF2,cross_product(sF0,universal_class)))))))
| ~ spl4_25
| ~ spl4_84 ),
inference(superposition,[],[f605,f2004]) ).
fof(f2012,plain,
( regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(u,u)))
| ~ spl4_25
| ~ spl4_36
| ~ spl4_84 ),
inference(forward_demodulation,[],[f2007,f702]) ).
fof(f2013,plain,
( unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class)))
| ~ spl4_5
| ~ spl4_25
| ~ spl4_36
| ~ spl4_84 ),
inference(forward_demodulation,[],[f2012,f310]) ).
fof(f2097,definition,
( spl4_89
<=> unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class))) ),
introduced(definition,[new_symbols(definition,[spl4_89])],[avatar_definition]) ).
fof(f2099,plain,
( unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class)))
| ~ spl4_89 ),
inference(avatar_component_clause,[],[f2097]) ).
fof(f2100,plain,
( spl4_89
| ~ spl4_5
| ~ spl4_25
| ~ spl4_36
| ~ spl4_84 ),
inference(avatar_split_clause,[],[f2013,f2002,f700,f603,f308,f2097]) ).
fof(f2433,definition,
( spl4_96
<=> ! [X0] :
( u = not_subclass_element(sF0,X0)
| subclass(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_96])],[avatar_definition]) ).
fof(f2434,plain,
( ! [X0] :
( subclass(sF0,X0)
| u = not_subclass_element(sF0,X0) )
| ~ spl4_96 ),
inference(avatar_component_clause,[],[f2433]) ).
fof(f2435,plain,
( spl4_96
| ~ spl4_15 ),
inference(avatar_split_clause,[],[f422,f417,f2433]) ).
fof(f2539,plain,
( $false
| spl4_30
| spl4_57 ),
inference(forward_subsumption_resolution,[],[f658,f1125]) ).
fof(f2540,plain,
( spl4_30
| spl4_57 ),
inference(avatar_contradiction_clause,[],[f2539]) ).
fof(f3065,definition,
( spl4_114
<=> ! [X0] :
( ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_114])],[avatar_definition]) ).
fof(f3066,plain,
( ! [X0] :
( ~ well_ordering(xr,X0)
| ~ subclass(sF0,X0) )
| ~ spl4_114 ),
inference(avatar_component_clause,[],[f3065]) ).
fof(f3068,plain,
( ~ subclass(sF0,y)
| ~ spl4_2
| ~ spl4_114 ),
inference(resolution,[],[f3066,f295]) ).
fof(f3074,definition,
( spl4_116
<=> subclass(sF0,y) ),
introduced(definition,[new_symbols(definition,[spl4_116])],[avatar_definition]) ).
fof(f3075,plain,
( subclass(sF0,y)
| ~ spl4_116 ),
inference(avatar_component_clause,[],[f3074]) ).
fof(f3076,plain,
( ~ subclass(sF0,y)
| spl4_116 ),
inference(avatar_component_clause,[],[f3074]) ).
fof(f3077,plain,
( ~ spl4_116
| ~ spl4_2
| ~ spl4_114 ),
inference(avatar_split_clause,[],[f3068,f3065,f293,f3074]) ).
fof(f3078,plain,
( u = not_subclass_element(sF0,y)
| ~ spl4_96
| spl4_116 ),
inference(resolution,[],[f3076,f2434]) ).
fof(f3080,definition,
( spl4_117
<=> u = not_subclass_element(sF0,y) ),
introduced(definition,[new_symbols(definition,[spl4_117])],[avatar_definition]) ).
fof(f3082,plain,
( u = not_subclass_element(sF0,y)
| ~ spl4_117 ),
inference(avatar_component_clause,[],[f3080]) ).
fof(f3083,plain,
( spl4_117
| ~ spl4_96
| spl4_116 ),
inference(avatar_split_clause,[],[f3078,f3074,f2433,f3080]) ).
fof(f3085,plain,
( ~ member(u,y)
| subclass(sF0,y)
| ~ spl4_117 ),
inference(superposition,[],[f3,f3082]) ).
fof(f3087,plain,
( subclass(sF0,y)
| ~ spl4_1
| ~ spl4_117 ),
inference(forward_subsumption_resolution,[],[f3085,f290]) ).
fof(f3089,plain,
( $false
| ~ spl4_1
| spl4_116
| ~ spl4_117 ),
inference(forward_subsumption_resolution,[],[f3087,f3076]) ).
fof(f3090,plain,
( ~ spl4_1
| spl4_116
| ~ spl4_117 ),
inference(avatar_contradiction_clause,[],[f3089]) ).
fof(f3210,plain,
( member(unordered_pair(sF0,unordered_pair(u,sF0)),sF2)
| ~ spl4_30
| ~ spl4_89 ),
inference(superposition,[],[f655,f2099]) ).
fof(f3257,plain,
( ! [X0] :
( ~ well_ordering(X0,y)
| u = least(X0,sF0) )
| ~ spl4_77
| ~ spl4_116 ),
inference(resolution,[],[f3075,f1900]) ).
fof(f3260,definition,
( spl4_119
<=> ! [X0] :
( ~ well_ordering(X0,y)
| u = least(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_119])],[avatar_definition]) ).
fof(f3261,plain,
( ! [X0] :
( ~ well_ordering(X0,y)
| u = least(X0,sF0) )
| ~ spl4_119 ),
inference(avatar_component_clause,[],[f3260]) ).
fof(f3262,plain,
( spl4_119
| ~ spl4_77
| ~ spl4_116 ),
inference(avatar_split_clause,[],[f3257,f3074,f1899,f3260]) ).
fof(f3315,plain,
( u = least(xr,sF0)
| ~ spl4_2
| ~ spl4_119 ),
inference(resolution,[],[f3261,f295]) ).
fof(f3383,definition,
( spl4_120
<=> u = least(xr,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_120])],[avatar_definition]) ).
fof(f3385,plain,
( u = least(xr,sF0)
| ~ spl4_120 ),
inference(avatar_component_clause,[],[f3383]) ).
fof(f3386,plain,
( spl4_120
| ~ spl4_2
| ~ spl4_119 ),
inference(avatar_split_clause,[],[f3315,f3260,f293,f3383]) ).
fof(f3388,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(u,u))),xr)
| ~ subclass(sF0,X1)
| ~ member(X0,sF0)
| ~ well_ordering(xr,X1) )
| ~ spl4_120 ),
inference(superposition,[],[f255,f3385]) ).
fof(f3391,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),xr)
| ~ subclass(sF0,X1)
| ~ member(X0,sF0)
| ~ well_ordering(xr,X1) )
| ~ spl4_5
| ~ spl4_120 ),
inference(forward_demodulation,[],[f3388,f310]) ).
fof(f3394,definition,
( spl4_121
<=> ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),xr)
| ~ member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_121])],[avatar_definition]) ).
fof(f3395,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),xr)
| ~ member(X0,sF0) )
| ~ spl4_121 ),
inference(avatar_component_clause,[],[f3394]) ).
fof(f3396,plain,
( spl4_114
| spl4_121
| ~ spl4_5
| ~ spl4_120 ),
inference(avatar_split_clause,[],[f3391,f3383,f308,f3394,f3065]) ).
fof(f3400,plain,
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),xr)
| ~ member(u,sF0)
| ~ spl4_5
| ~ spl4_121 ),
inference(superposition,[],[f3395,f310]) ).
fof(f3404,plain,
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),xr)
| ~ spl4_5
| ~ spl4_14
| ~ spl4_121 ),
inference(forward_subsumption_resolution,[],[f3400,f392]) ).
fof(f3476,definition,
( spl4_124
<=> member(unordered_pair(sF0,unordered_pair(u,sF0)),xr) ),
introduced(definition,[new_symbols(definition,[spl4_124])],[avatar_definition]) ).
fof(f3478,plain,
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),xr)
| spl4_124 ),
inference(avatar_component_clause,[],[f3476]) ).
fof(f3479,plain,
( ~ spl4_124
| ~ spl4_5
| ~ spl4_14
| ~ spl4_121 ),
inference(avatar_split_clause,[],[f3404,f3394,f390,f308,f3476]) ).
fof(f3727,plain,
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),sF2)
| ~ spl4_8
| spl4_124 ),
inference(resolution,[],[f3478,f325]) ).
fof(f3731,plain,
( $false
| ~ spl4_8
| ~ spl4_30
| ~ spl4_89
| spl4_124 ),
inference(forward_subsumption_resolution,[],[f3727,f3210]) ).
fof(f3732,plain,
( ~ spl4_8
| ~ spl4_30
| ~ spl4_89
| spl4_124 ),
inference(avatar_contradiction_clause,[],[f3731]) ).
cnf(s142,plain,
spl4_1,
inference(sat_conversion,[],[f291]) ).
cnf(s144,plain,
spl4_2,
inference(sat_conversion,[],[f296]) ).
cnf(s146,plain,
spl4_3,
inference(sat_conversion,[],[f301]) ).
cnf(s148,plain,
spl4_4,
inference(sat_conversion,[],[f306]) ).
cnf(s150,plain,
spl4_5,
inference(sat_conversion,[],[f311]) ).
cnf(s154,plain,
spl4_6,
inference(sat_conversion,[],[f318]) ).
cnf(s156,plain,
( ~ spl4_4
| spl4_7 ),
inference(sat_conversion,[],[f322]) ).
cnf(s158,plain,
( ~ spl4_4
| spl4_8 ),
inference(sat_conversion,[],[f326]) ).
cnf(s182,plain,
( ~ spl4_3
| spl4_12 ),
inference(sat_conversion,[],[f363]) ).
cnf(s203,plain,
( ~ spl4_5
| spl4_13
| spl4_14 ),
inference(sat_conversion,[],[f393]) ).
cnf(s209,plain,
( ~ spl4_1
| ~ spl4_13 ),
inference(sat_conversion,[],[f410]) ).
cnf(s215,plain,
( ~ spl4_5
| spl4_15 ),
inference(sat_conversion,[],[f419]) ).
cnf(s283,plain,
( ~ spl4_5
| spl4_20 ),
inference(sat_conversion,[],[f528]) ).
cnf(s329,plain,
( ~ spl4_6
| spl4_24 ),
inference(sat_conversion,[],[f594]) ).
cnf(s337,plain,
( ~ spl4_1
| ~ spl4_5
| ~ spl4_24
| spl4_25 ),
inference(sat_conversion,[],[f606]) ).
cnf(s351,plain,
( ~ spl4_25
| spl4_26 ),
inference(sat_conversion,[],[f628]) ).
cnf(s359,plain,
( ~ spl4_12
| ~ spl4_25
| spl4_28
| ~ spl4_29 ),
inference(sat_conversion,[],[f649]) ).
cnf(s363,plain,
( ~ spl4_7
| spl4_29
| ~ spl4_30 ),
inference(sat_conversion,[],[f657]) ).
cnf(s386,plain,
( ~ spl4_15
| ~ spl4_28
| spl4_36 ),
inference(sat_conversion,[],[f703]) ).
cnf(s540,plain,
( ~ spl4_26
| spl4_57
| spl4_58 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s544,plain,
( ~ spl4_14
| ~ spl4_46
| spl4_60 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s547,plain,
( ~ spl4_60
| spl4_61 ),
inference(sat_conversion,[],[f1150]) ).
cnf(s556,plain,
( ~ spl4_61
| spl4_62 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s569,plain,
( ~ spl4_1
| ~ spl4_62
| spl4_63 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s572,plain,
( ~ spl4_63
| spl4_64 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s575,plain,
( ~ spl4_1
| ~ spl4_60
| ~ spl4_64 ),
inference(sat_conversion,[],[f1213]) ).
cnf(s957,plain,
( ~ spl4_15
| spl4_46
| spl4_77 ),
inference(sat_conversion,[],[f1901]) ).
cnf(s983,plain,
( ~ spl4_1
| ~ spl4_6
| ~ spl4_20
| ~ spl4_57 ),
inference(sat_conversion,[],[f1972]) ).
cnf(s1020,plain,
( ~ spl4_15
| ~ spl4_58
| spl4_84 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s1048,plain,
( ~ spl4_5
| ~ spl4_25
| ~ spl4_36
| ~ spl4_84
| spl4_89 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s1093,plain,
( ~ spl4_15
| spl4_96 ),
inference(sat_conversion,[],[f2435]) ).
cnf(s1144,plain,
( spl4_30
| spl4_57 ),
inference(sat_conversion,[],[f2540]) ).
cnf(s1355,plain,
( ~ spl4_2
| ~ spl4_114
| ~ spl4_116 ),
inference(sat_conversion,[],[f3077]) ).
cnf(s1358,plain,
( ~ spl4_96
| spl4_116
| spl4_117 ),
inference(sat_conversion,[],[f3083]) ).
cnf(s1360,plain,
( ~ spl4_1
| spl4_116
| ~ spl4_117 ),
inference(sat_conversion,[],[f3090]) ).
cnf(s1417,plain,
( ~ spl4_77
| ~ spl4_116
| spl4_119 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s1469,plain,
( ~ spl4_2
| ~ spl4_119
| spl4_120 ),
inference(sat_conversion,[],[f3386]) ).
cnf(s1473,plain,
( ~ spl4_5
| spl4_114
| ~ spl4_120
| spl4_121 ),
inference(sat_conversion,[],[f3396]) ).
cnf(s1497,plain,
( ~ spl4_5
| ~ spl4_14
| ~ spl4_121
| ~ spl4_124 ),
inference(sat_conversion,[],[f3479]) ).
cnf(s1627,plain,
( ~ spl4_8
| ~ spl4_30
| ~ spl4_89
| spl4_124 ),
inference(sat_conversion,[],[f3732]) ).
cnf(s1628,plain,
spl4_24,
inference(rat,[],[s329,s154]) ).
cnf(s1633,plain,
spl4_20,
inference(rat,[],[s283,s150]) ).
cnf(s1634,plain,
spl4_15,
inference(rat,[],[s215,s150]) ).
cnf(s1636,plain,
spl4_96,
inference(rat,[],[s1093,s1634]) ).
cnf(s1640,plain,
spl4_8,
inference(rat,[],[s158,s148]) ).
cnf(s1641,plain,
spl4_7,
inference(rat,[],[s156,s148]) ).
cnf(s1646,plain,
spl4_12,
inference(rat,[],[s182,s146]) ).
cnf(s1651,plain,
~ spl4_57,
inference(rat,[],[s983,s1633,s154,s142]) ).
cnf(s1653,plain,
spl4_25,
inference(rat,[],[s337,s150,s1628,s142]) ).
cnf(s1655,plain,
~ spl4_13,
inference(rat,[],[s209,s142]) ).
cnf(s1656,plain,
spl4_30,
inference(rat,[],[s1144,s1651]) ).
cnf(s1659,plain,
spl4_26,
inference(rat,[],[s351,s1653]) ).
cnf(s1660,plain,
spl4_14,
inference(rat,[],[s203,s150,s1655]) ).
cnf(s1661,plain,
spl4_29,
inference(rat,[],[s363,s1641,s1656]) ).
cnf(s1665,plain,
spl4_58,
inference(rat,[],[s540,s1651,s1659]) ).
cnf(s1669,plain,
spl4_28,
inference(rat,[],[s359,s1653,s1646,s1661]) ).
cnf(s1670,plain,
spl4_84,
inference(rat,[],[s1020,s1634,s1665]) ).
cnf(s1672,plain,
spl4_36,
inference(rat,[],[s386,s1634,s1669]) ).
cnf(s1679,plain,
spl4_89,
inference(rat,[],[s1048,s1670,s1653,s150,s1672]) ).
cnf(s1683,plain,
spl4_124,
inference(rat,[],[s1627,s1656,s1640,s1679]) ).
cnf(s1684,plain,
~ spl4_121,
inference(rat,[],[s1497,s1660,s150,s1683]) ).
cnf(s1685,plain,
~ spl4_60,
inference(rat,[],[s569,s556,s572,s547,s575,s142]) ).
cnf(s1686,plain,
~ spl4_46,
inference(rat,[],[s544,s1660,s1685]) ).
cnf(s1688,plain,
spl4_77,
inference(rat,[],[s957,s1634,s1686]) ).
cnf(s1699,plain,
spl4_116,
inference(rat,[],[s1358,s1360,s1636,s142]) ).
cnf(s1700,plain,
spl4_119,
inference(rat,[],[s1417,s1688,s1699]) ).
cnf(s1701,plain,
~ spl4_114,
inference(rat,[],[s1355,s144,s1699]) ).
cnf(s1702,plain,
spl4_120,
inference(rat,[],[s1469,s144,s1700]) ).
cnf(s1703,plain,
$false,
inference(rat,[],[s1473,s1684,s150,s1702,s1701]) ).
fof(f3733,plain,
$false,
inference(avatar_sat_refutation,[],[s1703]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM077-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n007.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 18:47:25 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.44 Running first-order theorem proving
% 0.14/0.44 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
% 10.60/2.19 % (1711493)Input is clausal, will run a generic CNF schedule.
% 10.60/2.19 % (1711499)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3293670407:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.60/2.19 % (1711500)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3782024360:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.60/2.19 % (1711502)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2469909710:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.60/2.19 % (1711498)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=3868421392:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.60/2.19 % (1711504)dis-21_1_sil=8000:lcm=predicate:random_seed=3447273379: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)
% 10.60/2.19 % (1711503)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=511679326:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.60/2.19 % (1711501)lrs+10_1_sil=8000:sp=occurrence:random_seed=3561451319:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.60/2.19 % (1711504)Instruction limit reached!
% 10.60/2.19 % (1711504)------------------------------
% 10.60/2.19 % (1711504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.19 % (1711504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.19 % (1711504)CaDiCaL version: 2.1.3
% 10.60/2.19 % (1711504)Termination reason: Instruction limit
% 10.60/2.19 % (1711504)Termination phase: Saturation
% 10.60/2.19 % (1711504)Time elapsed: 0.064 s
% 10.60/2.19 % (1711504)Peak memory usage: 89 MB
% 10.60/2.19 % (1711504)Instructions burned: 117 (million)
% 10.60/2.19 % (1711501)Instruction limit reached!
% 10.60/2.19 % (1711501)------------------------------
% 10.60/2.19 % (1711501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.19 % (1711501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.19 % (1711501)CaDiCaL version: 2.1.3
% 10.60/2.19 % (1711501)Termination reason: Instruction limit
% 10.60/2.19 % (1711501)Termination phase: Saturation
% 10.60/2.19 % (1711501)Time elapsed: 0.065 s
% 10.60/2.19 % (1711501)Peak memory usage: 89 MB
% 10.60/2.19 % (1711501)Instructions burned: 108 (million)
% 10.60/2.19 % (1711502)Instruction limit reached!
% 10.60/2.19 % (1711502)------------------------------
% 10.60/2.19 % (1711502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.19 % (1711502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.19 % (1711502)CaDiCaL version: 2.1.3
% 10.60/2.19 % (1711502)Termination reason: Instruction limit
% 10.60/2.19 % (1711502)Termination phase: Saturation
% 10.60/2.19 % (1711502)Time elapsed: 0.070 s
% 10.60/2.19 % (1711502)Peak memory usage: 88 MB
% 10.60/2.19 % (1711502)Instructions burned: 114 (million)
% 10.60/2.19 % (1711503)Instruction limit reached!
% 10.60/2.19 % (1711503)------------------------------
% 10.60/2.19 % (1711503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.60/2.19 % (1711503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.60/2.19 % (1711503)CaDiCaL version: 2.1.3
% 10.60/2.19 % (1711503)Termination reason: Instruction limit
% 10.60/2.19 % (1711503)Termination phase: Saturation
% 10.60/2.19 % (1711503)Time elapsed: 0.129 s
% 10.60/2.19 % (1711503)Peak memory usage: 90 MB
% 10.60/2.19 % (1711503)Instructions burned: 180 (million)
% 10.60/2.19 % (1711514)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3457504894:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.60/2.19 % (1711513)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3884239474: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)
% 10.60/2.19 % (1711512)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=1541458714:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.60/2.19 % (1711512)Refutation not found, incomplete strategy
% 10.60/2.19 % (1711512)------------------------------
% 10.60/2.19 % (1711512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711512)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711512)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.50 % (1711512)Time elapsed: 0.004 s
% 19.40/3.50 % (1711512)Peak memory usage: 88 MB
% 19.40/3.50 % (1711512)Instructions burned: 3 (million)
% 19.40/3.50 % (1711514)Refutation not found, incomplete strategy
% 19.40/3.50 % (1711514)------------------------------
% 19.40/3.50 % (1711514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711514)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711514)Termination reason: Refutation not found, incomplete strategy
% 19.40/3.50 % (1711514)Time elapsed: 0.005 s
% 19.40/3.50 % (1711514)Peak memory usage: 88 MB
% 19.40/3.50 % (1711514)Instructions burned: 6 (million)
% 19.40/3.50 % (1711515)lrs+10_64_to=lpo:sil=8000:random_seed=3065058984:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 19.40/3.50 % (1711513)Instruction limit reached!
% 19.40/3.50 % (1711513)------------------------------
% 19.40/3.50 % (1711513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711513)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711513)Termination reason: Instruction limit
% 19.40/3.50 % (1711513)Termination phase: Saturation
% 19.40/3.50 % (1711513)Time elapsed: 0.093 s
% 19.40/3.50 % (1711513)Peak memory usage: 90 MB
% 19.40/3.50 % (1711513)Instructions burned: 189 (million)
% 19.40/3.50 % (1711515)Instruction limit reached!
% 19.40/3.50 % (1711515)------------------------------
% 19.40/3.50 % (1711515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711515)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711515)Termination reason: Instruction limit
% 19.40/3.50 % (1711515)Termination phase: Saturation
% 19.40/3.50 % (1711515)Time elapsed: 0.043 s
% 19.40/3.50 % (1711515)Peak memory usage: 89 MB
% 19.40/3.50 % (1711515)Instructions burned: 126 (million)
% 19.40/3.50 % (1711521)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1008358661:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.40/3.50 % (1711514)------------------------------
% 19.40/3.50 % (1711514)------------------------------
% 19.40/3.50 % (1711512)------------------------------
% 19.40/3.50 % (1711512)------------------------------
% 19.40/3.50 % (1711520)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3688569718:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.40/3.50 % (1711521)Instruction limit reached!
% 19.40/3.50 % (1711521)------------------------------
% 19.40/3.50 % (1711521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711521)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711521)Termination reason: Instruction limit
% 19.40/3.50 % (1711521)Termination phase: Saturation
% 19.40/3.50 % (1711521)Time elapsed: 0.060 s
% 19.40/3.50 % (1711521)Peak memory usage: 91 MB
% 19.40/3.50 % (1711521)Instructions burned: 157 (million)
% 19.40/3.50 % (1711520)Instruction limit reached!
% 19.40/3.50 % (1711520)------------------------------
% 19.40/3.50 % (1711520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.40/3.50 % (1711520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.40/3.50 % (1711520)CaDiCaL version: 2.1.3
% 19.40/3.50 % (1711520)Termination reason: Instruction limit
% 19.40/3.50 % (1711520)Termination phase: Saturation
% 19.40/3.50 % (1711520)Time elapsed: 0.112 s
% 19.40/3.50 % (1711520)Peak memory usage: 90 MB
% 19.40/3.50 % (1711520)Instructions burned: 194 (million)
% 19.40/3.50 % (1711526)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=614037755:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 19.40/3.50 % (1711524)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=974155659:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 19.40/3.50 % (1711525)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=4149510042:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 31.26/5.07 % (1711526)Instruction limit reached!
% 31.26/5.07 % (1711526)------------------------------
% 31.26/5.07 % (1711526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711526)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711526)Termination reason: Instruction limit
% 31.26/5.07 % (1711526)Termination phase: Saturation
% 31.26/5.07 % (1711526)Time elapsed: 0.040 s
% 31.26/5.07 % (1711526)Peak memory usage: 89 MB
% 31.26/5.07 % (1711526)Instructions burned: 108 (million)
% 31.26/5.07 % (1711525)Instruction limit reached!
% 31.26/5.07 % (1711525)------------------------------
% 31.26/5.07 % (1711525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711525)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711525)Termination reason: Instruction limit
% 31.26/5.07 % (1711525)Termination phase: Saturation
% 31.26/5.07 % (1711525)Time elapsed: 0.064 s
% 31.26/5.07 % (1711525)Peak memory usage: 89 MB
% 31.26/5.07 % (1711525)Instructions burned: 107 (million)
% 31.26/5.07 % (1711527)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4004421027:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 31.26/5.07 % (1711531)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2613778724:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 31.26/5.07 % (1711532)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2932326585:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 31.26/5.07 % (1711527)Instruction limit reached!
% 31.26/5.07 % (1711527)------------------------------
% 31.26/5.07 % (1711527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711527)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711527)Termination reason: Instruction limit
% 31.26/5.07 % (1711527)Termination phase: Saturation
% 31.26/5.07 % (1711527)Time elapsed: 0.165 s
% 31.26/5.07 % (1711527)Peak memory usage: 90 MB
% 31.26/5.07 % (1711527)Instructions burned: 242 (million)
% 31.26/5.07 % (1711532)Instruction limit reached!
% 31.26/5.07 % (1711532)------------------------------
% 31.26/5.07 % (1711532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711532)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711532)Termination reason: Instruction limit
% 31.26/5.07 % (1711532)Termination phase: Saturation
% 31.26/5.07 % (1711532)Time elapsed: 0.092 s
% 31.26/5.07 % (1711532)Peak memory usage: 89 MB
% 31.26/5.07 % (1711532)Instructions burned: 134 (million)
% 31.26/5.07 % (1711536)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3249290189:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 31.26/5.07 % (1711537)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1391974202:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 31.26/5.07 % (1711537)Instruction limit reached!
% 31.26/5.07 % (1711537)------------------------------
% 31.26/5.07 % (1711537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711537)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711537)Termination reason: Instruction limit
% 31.26/5.07 % (1711537)Termination phase: Saturation
% 31.26/5.07 % (1711537)Time elapsed: 0.105 s
% 31.26/5.07 % (1711537)Peak memory usage: 89 MB
% 31.26/5.07 % (1711537)Instructions burned: 191 (million)
% 31.26/5.07 % (1711540)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3164984883:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 31.26/5.07 % (1711536)Instruction limit reached!
% 31.26/5.07 % (1711536)------------------------------
% 31.26/5.07 % (1711536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.26/5.07 % (1711536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.26/5.07 % (1711536)CaDiCaL version: 2.1.3
% 31.26/5.07 % (1711536)Termination reason: Instruction limit
% 31.26/5.07 % (1711536)Termination phase: Saturation
% 31.26/5.07 % (1711536)Time elapsed: 0.305 s
% 50.14/7.88 % (1711536)Peak memory usage: 95 MB
% 50.14/7.88 % (1711536)Instructions burned: 500 (million)
% 50.14/7.88 % (1711542)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3002839020:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 50.14/7.88 % (1711540)Instruction limit reached!
% 50.14/7.88 % (1711540)------------------------------
% 50.14/7.88 % (1711540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.14/7.88 % (1711540)CaDiCaL version: 2.1.3
% 50.14/7.88 % (1711540)Termination reason: Instruction limit
% 50.14/7.88 % (1711540)Termination phase: Saturation
% 50.14/7.88 % (1711540)Time elapsed: 0.168 s
% 50.14/7.88 % (1711540)Peak memory usage: 92 MB
% 50.14/7.88 % (1711540)Instructions burned: 264 (million)
% 50.14/7.88 % (1711542)Instruction limit reached!
% 50.14/7.88 % (1711542)------------------------------
% 50.14/7.88 % (1711542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.14/7.88 % (1711542)CaDiCaL version: 2.1.3
% 50.14/7.88 % (1711542)Termination reason: Instruction limit
% 50.14/7.88 % (1711542)Termination phase: Saturation
% 50.14/7.88 % (1711542)Time elapsed: 0.102 s
% 50.14/7.88 % (1711542)Peak memory usage: 89 MB
% 50.14/7.88 % (1711542)Instructions burned: 157 (million)
% 50.14/7.88 % (1711544)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=251402529:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 50.14/7.88 % (1711545)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2991791099:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 50.14/7.88 % (1711545)Instruction limit reached!
% 50.14/7.88 % (1711545)------------------------------
% 50.14/7.88 % (1711545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.14/7.88 % (1711545)CaDiCaL version: 2.1.3
% 50.14/7.88 % (1711545)Termination reason: Instruction limit
% 50.14/7.88 % (1711545)Termination phase: Saturation
% 50.14/7.88 % (1711545)Time elapsed: 0.263 s
% 50.14/7.88 % (1711545)Peak memory usage: 89 MB
% 50.14/7.88 % (1711545)Instructions burned: 537 (million)
% 50.14/7.88 % (1711548)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=287060030:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 50.14/7.88 % (1711548)Instruction limit reached!
% 50.14/7.88 % (1711548)------------------------------
% 50.14/7.88 % (1711548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.14/7.88 % (1711548)CaDiCaL version: 2.1.3
% 50.14/7.88 % (1711548)Termination reason: Instruction limit
% 50.14/7.88 % (1711548)Termination phase: Saturation
% 50.14/7.88 % (1711548)Time elapsed: 0.092 s
% 50.14/7.88 % (1711548)Peak memory usage: 90 MB
% 50.14/7.88 % (1711548)Instructions burned: 182 (million)
% 50.14/7.88 % (1711550)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=164592333:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 50.14/7.88 % (1711531)Instruction limit reached!
% 50.14/7.88 % (1711531)------------------------------
% 50.14/7.88 % (1711531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.14/7.88 % (1711531)CaDiCaL version: 2.1.3
% 50.14/7.88 % (1711531)Termination reason: Instruction limit
% 50.14/7.88 % (1711531)Termination phase: Saturation
% 50.14/7.88 % (1711531)Time elapsed: 1.741 s
% 50.14/7.88 % (1711531)Peak memory usage: 157 MB
% 50.14/7.88 % (1711531)Instructions burned: 5209 (million)
% 50.14/7.88 % (1711552)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=1472141421:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 50.14/7.88 % (1711524)Instruction limit reached!
% 50.14/7.88 % (1711524)------------------------------
% 50.14/7.88 % (1711524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.14/7.88 % (1711524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711524)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711524)Termination reason: Instruction limit
% 69.29/10.50 % (1711524)Termination phase: Saturation
% 69.29/10.50 % (1711524)Time elapsed: 2.076 s
% 69.29/10.50 % (1711524)Peak memory usage: 145 MB
% 69.29/10.50 % (1711524)Instructions burned: 3394 (million)
% 69.29/10.50 % (1711552)Instruction limit reached!
% 69.29/10.50 % (1711552)------------------------------
% 69.29/10.50 % (1711552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.29/10.50 % (1711552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711552)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711552)Termination reason: Instruction limit
% 69.29/10.50 % (1711552)Termination phase: Saturation
% 69.29/10.50 % (1711552)Time elapsed: 0.101 s
% 69.29/10.50 % (1711552)Peak memory usage: 90 MB
% 69.29/10.50 % (1711552)Instructions burned: 417 (million)
% 69.29/10.50 % (1711554)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=751866222:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 69.29/10.50 % (1711555)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=210951713:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 69.29/10.50 % (1711555)Refutation not found, incomplete strategy
% 69.29/10.50 % (1711555)------------------------------
% 69.29/10.50 % (1711555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.29/10.50 % (1711555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711555)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711555)Termination reason: Refutation not found, incomplete strategy
% 69.29/10.50 % (1711555)Time elapsed: 0.001 s
% 69.29/10.50 % (1711555)Peak memory usage: 88 MB
% 69.29/10.50 % (1711555)Instructions burned: 1 (million)
% 69.29/10.50 % (1711555)------------------------------
% 69.29/10.50 % (1711555)------------------------------
% 69.29/10.50 % (1711558)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2241942342:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 69.29/10.50 % (1711558)Instruction limit reached!
% 69.29/10.50 % (1711558)------------------------------
% 69.29/10.50 % (1711558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.29/10.50 % (1711558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711558)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711558)Termination reason: Instruction limit
% 69.29/10.50 % (1711558)Termination phase: Saturation
% 69.29/10.50 % (1711558)Time elapsed: 0.388 s
% 69.29/10.50 % (1711558)Peak memory usage: 98 MB
% 69.29/10.50 % (1711558)Instructions burned: 720 (million)
% 69.29/10.50 % (1711544)Instruction limit reached!
% 69.29/10.50 % (1711544)------------------------------
% 69.29/10.50 % (1711544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.29/10.50 % (1711544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711544)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711544)Termination reason: Instruction limit
% 69.29/10.50 % (1711544)Termination phase: Saturation
% 69.29/10.50 % (1711544)Time elapsed: 1.910 s
% 69.29/10.50 % (1711544)Peak memory usage: 148 MB
% 69.29/10.50 % (1711544)Instructions burned: 3258 (million)
% 69.29/10.50 % (1711560)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3669281854:i=598:bs=on:bd=preordered:av=off:ss=axioms_2962 on theBenchmark for (2962ds/598Mi)
% 69.29/10.50 % (1711561)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=882026028:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi)
% 69.29/10.50 % (1711560)Instruction limit reached!
% 69.29/10.50 % (1711560)------------------------------
% 69.29/10.50 % (1711560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.29/10.50 % (1711560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.29/10.50 % (1711560)CaDiCaL version: 2.1.3
% 69.29/10.50 % (1711560)Termination reason: Instruction limit
% 69.29/10.50 % (1711560)Termination phase: Saturation
% 69.29/10.50 % (1711560)Time elapsed: 0.333 s
% 69.29/10.50 % (1711560)Peak memory usage: 93 MB
% 69.29/10.50 % (1711560)Instructions burned: 599 (million)
% 69.29/10.50 % (1711564)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=3382026384:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2957 on theBenchmark for (2957ds/1997Mi)
% 74.65/11.33 % (1711564)Instruction limit reached!
% 74.65/11.33 % (1711564)------------------------------
% 74.65/11.33 % (1711564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711564)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711564)Termination reason: Instruction limit
% 74.65/11.33 % (1711564)Termination phase: Saturation
% 74.65/11.33 % (1711564)Time elapsed: 1.319 s
% 74.65/11.33 % (1711564)Peak memory usage: 138 MB
% 74.65/11.33 % (1711564)Instructions burned: 1997 (million)
% 74.65/11.33 % (1711561)Instruction limit reached!
% 74.65/11.33 % (1711561)------------------------------
% 74.65/11.33 % (1711561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711561)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711561)Termination reason: Instruction limit
% 74.65/11.33 % (1711561)Termination phase: Saturation
% 74.65/11.33 % (1711561)Time elapsed: 1.835 s
% 74.65/11.33 % (1711561)Peak memory usage: 145 MB
% 74.65/11.33 % (1711561)Instructions burned: 2989 (million)
% 74.65/11.33 % (1711566)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=2347535475:i=2088:bd=preordered:av=off_2942 on theBenchmark for (2942ds/2088Mi)
% 74.65/11.33 % (1711567)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1437828375:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 74.65/11.33 % (1711550)Instruction limit reached!
% 74.65/11.33 % (1711550)------------------------------
% 74.65/11.33 % (1711550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711550)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711550)Termination reason: Instruction limit
% 74.65/11.33 % (1711550)Termination phase: Saturation
% 74.65/11.33 % (1711550)Time elapsed: 3.956 s
% 74.65/11.33 % (1711550)Peak memory usage: 167 MB
% 74.65/11.33 % (1711550)Instructions burned: 10308 (million)
% 74.65/11.33 % (1711567)Instruction limit reached!
% 74.65/11.33 % (1711567)------------------------------
% 74.65/11.33 % (1711567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711567)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711567)Termination reason: Instruction limit
% 74.65/11.33 % (1711567)Termination phase: Saturation
% 74.65/11.33 % (1711567)Time elapsed: 0.677 s
% 74.65/11.33 % (1711567)Peak memory usage: 102 MB
% 74.65/11.33 % (1711567)Instructions burned: 1099 (million)
% 74.65/11.33 % (1711570)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=365723194:i=433:bd=preordered_2933 on theBenchmark for (2933ds/433Mi)
% 74.65/11.33 % (1711571)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1296459155:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2933 on theBenchmark for (2933ds/2942Mi)
% 74.65/11.33 % (1711570)Instruction limit reached!
% 74.65/11.33 % (1711570)------------------------------
% 74.65/11.33 % (1711570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711570)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711570)Termination reason: Instruction limit
% 74.65/11.33 % (1711570)Termination phase: Saturation
% 74.65/11.33 % (1711570)Time elapsed: 0.133 s
% 74.65/11.33 % (1711570)Peak memory usage: 91 MB
% 74.65/11.33 % (1711570)Instructions burned: 436 (million)
% 74.65/11.33 % (1711574)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1771313109:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2931 on theBenchmark for (2931ds/6922Mi)
% 74.65/11.33 % (1711566)Instruction limit reached!
% 74.65/11.33 % (1711566)------------------------------
% 74.65/11.33 % (1711566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711566)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711566)Termination reason: Instruction limit
% 74.65/11.33 % (1711566)Termination phase: Saturation
% 74.65/11.33 % (1711566)Time elapsed: 1.327 s
% 74.65/11.33 % (1711566)Peak memory usage: 137 MB
% 74.65/11.33 % (1711566)Instructions burned: 2089 (million)
% 74.65/11.33 % (1711576)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=1823693766:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2927 on theBenchmark for (2927ds/596Mi)
% 74.65/11.33 % (1711554)Instruction limit reached!
% 74.65/11.33 % (1711554)------------------------------
% 74.65/11.33 % (1711554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711554)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711554)Termination reason: Instruction limit
% 74.65/11.33 % (1711554)Termination phase: Saturation
% 74.65/11.33 % (1711554)Time elapsed: 4.559 s
% 74.65/11.33 % (1711554)Peak memory usage: 189 MB
% 74.65/11.33 % (1711554)Instructions burned: 8480 (million)
% 74.65/11.33 % (1711576)Instruction limit reached!
% 74.65/11.33 % (1711576)------------------------------
% 74.65/11.33 % (1711576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711576)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711576)Termination reason: Instruction limit
% 74.65/11.33 % (1711576)Termination phase: Saturation
% 74.65/11.33 % (1711576)Time elapsed: 0.320 s
% 74.65/11.33 % (1711576)Peak memory usage: 99 MB
% 74.65/11.33 % (1711576)Instructions burned: 597 (million)
% 74.65/11.33 % (1711578)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=3996342512:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2924 on theBenchmark for (2924ds/4123Mi)
% 74.65/11.33 % (1711579)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1698911616:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2922 on theBenchmark for (2922ds/16411Mi)
% 74.65/11.33 % (1711571)Instruction limit reached!
% 74.65/11.33 % (1711571)------------------------------
% 74.65/11.33 % (1711571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711571)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711571)Termination reason: Instruction limit
% 74.65/11.33 % (1711571)Termination phase: Saturation
% 74.65/11.33 % (1711571)Time elapsed: 1.374 s
% 74.65/11.33 % (1711571)Peak memory usage: 143 MB
% 74.65/11.33 % (1711571)Instructions burned: 2946 (million)
% 74.65/11.33 % (1711582)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1456553658:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2917 on theBenchmark for (2917ds/1670Mi)
% 74.65/11.33 % (1711582)Instruction limit reached!
% 74.65/11.33 % (1711582)------------------------------
% 74.65/11.33 % (1711582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711582)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711582)Termination reason: Instruction limit
% 74.65/11.33 % (1711582)Termination phase: Saturation
% 74.65/11.33 % (1711582)Time elapsed: 0.575 s
% 74.65/11.33 % (1711582)Peak memory usage: 137 MB
% 74.65/11.33 % (1711582)Instructions burned: 1671 (million)
% 74.65/11.33 % (1711584)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=221962109:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2910 on theBenchmark for (2910ds/1722Mi)
% 74.65/11.33 % (1711584)Instruction limit reached!
% 74.65/11.33 % (1711584)------------------------------
% 74.65/11.33 % (1711584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711584)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711584)Termination reason: Instruction limit
% 74.65/11.33 % (1711584)Termination phase: Saturation
% 74.65/11.33 % (1711584)Time elapsed: 0.679 s
% 74.65/11.33 % (1711584)Peak memory usage: 135 MB
% 74.65/11.33 % (1711584)Instructions burned: 1722 (million)
% 74.65/11.33 % (1711586)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=2420442259:cts=off:cond=on:i=9530:bs=on:fsd=on_2902 on theBenchmark for (2902ds/9530Mi)
% 74.65/11.33 % (1711578)Instruction limit reached!
% 74.65/11.33 % (1711578)------------------------------
% 74.65/11.33 % (1711578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711578)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711578)Termination reason: Instruction limit
% 74.65/11.33 % (1711578)Termination phase: Saturation
% 74.65/11.33 % (1711578)Time elapsed: 2.420 s
% 74.65/11.33 % (1711578)Peak memory usage: 157 MB
% 74.65/11.33 % (1711578)Instructions burned: 4124 (million)
% 74.65/11.33 % (1711588)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=72569797:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi)
% 74.65/11.33 % (1711574)Instruction limit reached!
% 74.65/11.33 % (1711574)------------------------------
% 74.65/11.33 % (1711574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.65/11.33 % (1711574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.65/11.33 % (1711574)CaDiCaL version: 2.1.3
% 74.65/11.33 % (1711574)Termination reason: Instruction limit
% 74.65/11.33 % (1711574)Termination phase: Saturation
% 74.65/11.33 % (1711574)Time elapsed: 3.486 s
% 74.65/11.33 % (1711574)Peak memory usage: 183 MB
% 74.65/11.33 % (1711574)Instructions burned: 6923 (million)
% 74.65/11.33 % (1711586)First to succeed.
% 74.65/11.33 % (1711586)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1711493"
% 74.65/11.33 % (1711586)Refutation found. Thanks to Tanya!
% 74.65/11.33 % SZS status Unsatisfiable for theBenchmark
% 74.65/11.33 % SZS output start Proof for theBenchmark
% See solution above
% 76.06/11.53 % (1711586)------------------------------
% 76.06/11.53 % (1711586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.06/11.53 % (1711586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.06/11.53 % (1711586)CaDiCaL version: 2.1.3
% 76.06/11.53 % (1711586)Termination reason: Refutation
% 76.06/11.53 % (1711586)Time elapsed: 0.647 s
% 76.06/11.53 % (1711586)Peak memory usage: 136 MB
% 76.06/11.53 % (1711586)Instructions burned: 1711 (million)
% 76.06/11.53 % (1711586)------------------------------
% 76.06/11.53 % (1711586)------------------------------
% 76.06/11.53 % (1711493)Success in time 10.696 s
% 76.06/11.53 % Vampire exiting
%------------------------------------------------------------------------------