%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM076-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 69.78s 20.86s
% Output : Refutation 142.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 69
% Syntax : Number of formulae : 312 ( 66 unt; 45 def)
% Number of atoms : 764 ( 115 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 858 ( 406 ~; 411 |; 0 &)
% ( 41 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 46 ( 44 usr; 42 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 9 con; 0-3 aty)
% Number of variables : 175 ( 0 sgn 175 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f133,axiom,
! [X2,X0,X1] : segment(X0,X1,X2) = domain_of(restrict(X0,X1,singleton(X2))),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',well_ordering5) ).
fof(f176,negated_conjecture,
well_ordering(xr,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property7_1) ).
fof(f177,negated_conjecture,
member(u,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property7_2) ).
fof(f178,negated_conjecture,
member(u,segment(xr,y,u)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_property7_3) ).
fof(f179,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(f193,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(f196,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,f179]) ).
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(X1,X3) ),
inference(definition_unfolding,[],[f15,f179]) ).
fof(f199,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,f179]) ).
fof(f203,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(f254,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,f179]) ).
fof(f269,plain,
member(u,domain_of(intersection(xr,cross_product(y,unordered_pair(u,u))))),
inference(definition_unfolding,[],[f178,f193]) ).
fof(f276,definition,
sF0 = unordered_pair(u,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f277,plain,
unordered_pair(u,u) = sF0,
inference(reorient_equations,[],[f276]) ).
fof(f278,definition,
sF1 = cross_product(y,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f279,plain,
cross_product(y,sF0) = sF1,
inference(reorient_equations,[],[f278]) ).
fof(f280,definition,
sF2 = intersection(xr,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f281,plain,
intersection(xr,sF1) = sF2,
inference(reorient_equations,[],[f280]) ).
fof(f282,definition,
sF3 = domain_of(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f283,plain,
domain_of(sF2) = sF3,
inference(reorient_equations,[],[f282]) ).
fof(f284,plain,
member(u,sF3),
inference(definition_folding,[],[f269,f283,f281,f279,f277]) ).
fof(f286,definition,
( spl4_1
<=> well_ordering(xr,y) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f288,plain,
( well_ordering(xr,y)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f289,plain,
spl4_1,
inference(avatar_split_clause,[],[f176,f286]) ).
fof(f291,definition,
( spl4_2
<=> member(u,y) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f293,plain,
( member(u,y)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f294,plain,
spl4_2,
inference(avatar_split_clause,[],[f177,f291]) ).
fof(f296,definition,
( spl4_3
<=> cross_product(y,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f298,plain,
( cross_product(y,sF0) = sF1
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f299,plain,
spl4_3,
inference(avatar_split_clause,[],[f279,f296]) ).
fof(f301,definition,
( spl4_4
<=> unordered_pair(u,u) = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f303,plain,
( unordered_pair(u,u) = sF0
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
spl4_4,
inference(avatar_split_clause,[],[f277,f301]) ).
fof(f306,definition,
( spl4_5
<=> intersection(xr,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f308,plain,
( intersection(xr,sF1) = sF2
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
spl4_5,
inference(avatar_split_clause,[],[f281,f306]) ).
fof(f311,definition,
( spl4_6
<=> member(u,sF3) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f313,plain,
( member(u,sF3)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,plain,
spl4_6,
inference(avatar_split_clause,[],[f284,f311]) ).
fof(f315,plain,
( ! [X0] :
( ~ member(X0,sF2)
| member(X0,xr) )
| ~ spl4_5 ),
inference(superposition,[],[f21,f308]) ).
fof(f316,plain,
( ! [X0] :
( ~ member(X0,sF2)
| member(X0,sF1) )
| ~ spl4_5 ),
inference(superposition,[],[f22,f308]) ).
fof(f318,definition,
( spl4_7
<=> ! [X0] :
( ~ member(X0,sF2)
| member(X0,xr) ) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f319,plain,
( ! [X0] :
( member(X0,xr)
| ~ member(X0,sF2) )
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f320,plain,
( spl4_7
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f315,f306,f318]) ).
fof(f322,definition,
( spl4_8
<=> ! [X0] :
( ~ member(X0,sF2)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f323,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,sF2) )
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( spl4_8
| ~ spl4_5 ),
inference(avatar_split_clause,[],[f316,f306,f322]) ).
fof(f326,definition,
( spl4_9
<=> domain_of(sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f328,plain,
( domain_of(sF2) = sF3
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f329,plain,
spl4_9,
inference(avatar_split_clause,[],[f283,f326]) ).
fof(f345,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f9,f1]) ).
fof(f346,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,X2) ),
inference(forward_subsumption_resolution,[],[f345,f4]) ).
fof(f350,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,[],[f197,f298]) ).
fof(f352,definition,
( spl4_11
<=> ! [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_11])],[avatar_definition]) ).
fof(f353,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,sF0) )
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( spl4_11
| ~ spl4_3 ),
inference(avatar_split_clause,[],[f350,f296,f352]) ).
fof(f355,plain,
( ! [X0,X1] :
( member(X0,sF0)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2) )
| ~ spl4_8
| ~ spl4_11 ),
inference(resolution,[],[f353,f323]) ).
fof(f366,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) )
| ~ spl4_4 ),
inference(superposition,[],[f203,f303]) ).
fof(f370,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0
| u = X0 )
| ~ spl4_4 ),
inference(superposition,[],[f8,f303]) ).
fof(f371,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0 )
| ~ spl4_4 ),
inference(duplicate_literal_removal,[],[f370]) ).
fof(f373,definition,
( spl4_13
<=> ! [X0] :
( ~ member(X0,sF0)
| u = X0 ) ),
introduced(definition,[new_symbols(definition,[spl4_13])],[avatar_definition]) ).
fof(f374,plain,
( ! [X0] :
( ~ member(X0,sF0)
| u = X0 )
| ~ spl4_13 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f375,plain,
( spl4_13
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f371,f301,f373]) ).
fof(f384,plain,
( ! [X0] :
( subclass(sF0,X0)
| u = not_subclass_element(sF0,X0) )
| ~ spl4_13 ),
inference(resolution,[],[f2,f374]) ).
fof(f410,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f419,definition,
( spl4_15
<=> ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl4_15])],[avatar_definition]) ).
fof(f420,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF0,universal_class))
| ~ member(u,domain_of(X0)) )
| ~ spl4_15 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f421,plain,
( spl4_15
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f366,f301,f419]) ).
fof(f430,plain,
( ! [X0] :
( member(u,sF0)
| ~ member(u,X0) )
| ~ spl4_4 ),
inference(superposition,[],[f346,f303]) ).
fof(f432,definition,
( spl4_17
<=> ! [X0] : ~ member(u,X0) ),
introduced(definition,[new_symbols(definition,[spl4_17])],[avatar_definition]) ).
fof(f433,plain,
( ! [X0] : ~ member(u,X0)
| ~ spl4_17 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,definition,
( spl4_18
<=> member(u,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_18])],[avatar_definition]) ).
fof(f437,plain,
( member(u,sF0)
| ~ spl4_18 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f438,plain,
( spl4_17
| spl4_18
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f430,f301,f435,f432]) ).
fof(f441,plain,
( $false
| ~ spl4_6
| ~ spl4_17 ),
inference(unit_resulting_resolution,[],[f1,f4,f313,f433]) ).
fof(f459,plain,
( ~ spl4_6
| ~ spl4_17 ),
inference(avatar_contradiction_clause,[],[f441]) ).
fof(f467,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f468,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f539,definition,
( spl4_21
<=> ! [X0] :
( subclass(sF0,X0)
| u = not_subclass_element(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_21])],[avatar_definition]) ).
fof(f540,plain,
( ! [X0] :
( subclass(sF0,X0)
| u = not_subclass_element(sF0,X0) )
| ~ spl4_21 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f541,plain,
( spl4_21
| ~ spl4_13 ),
inference(avatar_split_clause,[],[f384,f373,f539]) ).
fof(f548,definition,
( spl4_23
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f549,plain,
( null_class != sF0
| spl4_23 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( null_class = sF0
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f576,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,[],[f467,f199]) ).
fof(f586,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,[],[f203,f576]) ).
fof(f594,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,[],[f586]) ).
fof(f603,plain,
( ! [X0] :
( ~ member(X0,sF3)
| 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_9 ),
inference(superposition,[],[f594,f328]) ).
fof(f609,definition,
( spl4_26
<=> ! [X0] :
( ~ member(X0,sF3)
| 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_26])],[avatar_definition]) ).
fof(f610,plain,
( ! [X0] :
( ~ member(X0,sF3)
| 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_26 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( spl4_26
| ~ spl4_9 ),
inference(avatar_split_clause,[],[f603,f326,f609]) ).
fof(f617,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_6
| ~ spl4_26 ),
inference(resolution,[],[f610,f313]) ).
fof(f618,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_4
| ~ spl4_6
| ~ spl4_26 ),
inference(forward_demodulation,[],[f617,f303]) ).
fof(f620,definition,
( spl4_27
<=> 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_27])],[avatar_definition]) ).
fof(f622,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_27 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( spl4_27
| ~ spl4_4
| ~ spl4_6
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f618,f609,f311,f301,f620]) ).
fof(f634,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_27 ),
inference(superposition,[],[f196,f622]) ).
fof(f644,definition,
( spl4_28
<=> ! [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_28])],[avatar_definition]) ).
fof(f645,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_28 ),
inference(avatar_component_clause,[],[f644]) ).
fof(f646,plain,
( spl4_28
| ~ spl4_27 ),
inference(avatar_split_clause,[],[f634,f620,f644]) ).
fof(f647,plain,
( member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| null_class = intersection(sF2,cross_product(sF0,universal_class))
| ~ spl4_28 ),
inference(resolution,[],[f645,f467]) ).
fof(f670,definition,
( spl4_32
<=> member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0) ),
introduced(definition,[new_symbols(definition,[spl4_32])],[avatar_definition]) ).
fof(f671,plain,
( ~ member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| spl4_32 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f672,plain,
( member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_32 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f674,plain,
( u = second(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_13
| ~ spl4_32 ),
inference(resolution,[],[f672,f374]) ).
fof(f677,definition,
( spl4_33
<=> u = second(regular(intersection(sF2,cross_product(sF0,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f679,plain,
( u = second(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f680,plain,
( spl4_33
| ~ spl4_13
| ~ spl4_32 ),
inference(avatar_split_clause,[],[f674,f670,f373,f677]) ).
fof(f793,plain,
( ! [X0,X1] :
( ~ subclass(sF0,X0)
| null_class = sF0
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) )
| ~ spl4_13 ),
inference(resolution,[],[f136,f374]) ).
fof(f901,definition,
( spl4_46
<=> ! [X0,X1] :
( member(X0,sF0)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2) ) ),
introduced(definition,[new_symbols(definition,[spl4_46])],[avatar_definition]) ).
fof(f902,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2)
| member(X0,sF0) )
| ~ spl4_46 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f903,plain,
( spl4_46
| ~ spl4_8
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f355,f352,f322,f901]) ).
fof(f911,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| member(second(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_27
| ~ spl4_46 ),
inference(superposition,[],[f902,f622]) ).
fof(f997,definition,
( spl4_49
<=> null_class = intersection(sF2,cross_product(sF0,universal_class)) ),
introduced(definition,[new_symbols(definition,[spl4_49])],[avatar_definition]) ).
fof(f998,plain,
( null_class != intersection(sF2,cross_product(sF0,universal_class))
| spl4_49 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f999,plain,
( null_class = intersection(sF2,cross_product(sF0,universal_class))
| ~ spl4_49 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f1001,definition,
( spl4_50
<=> member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0) ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f1003,plain,
( member(first(regular(intersection(sF2,cross_product(sF0,universal_class)))),sF0)
| ~ spl4_50 ),
inference(avatar_component_clause,[],[f1001]) ).
fof(f1004,plain,
( spl4_49
| spl4_50
| ~ spl4_28 ),
inference(avatar_split_clause,[],[f647,f644,f1001,f997]) ).
fof(f1015,plain,
( null_class != null_class
| ~ member(u,domain_of(sF2))
| ~ spl4_15
| ~ spl4_49 ),
inference(superposition,[],[f420,f999]) ).
fof(f1022,plain,
( ~ member(u,domain_of(sF2))
| ~ spl4_15
| ~ spl4_49 ),
inference(trivial_inequality_removal,[],[f1015]) ).
fof(f1023,plain,
( ~ member(u,sF3)
| ~ spl4_9
| ~ spl4_15
| ~ spl4_49 ),
inference(forward_demodulation,[],[f1022,f328]) ).
fof(f1027,plain,
( $false
| ~ spl4_6
| ~ spl4_9
| ~ spl4_15
| ~ spl4_49 ),
inference(forward_subsumption_resolution,[],[f1023,f313]) ).
fof(f1028,plain,
( ~ spl4_6
| ~ spl4_9
| ~ spl4_15
| ~ spl4_49 ),
inference(avatar_contradiction_clause,[],[f1027]) ).
fof(f1032,plain,
( u = first(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_13
| ~ spl4_50 ),
inference(resolution,[],[f1003,f374]) ).
fof(f1037,definition,
( spl4_51
<=> u = first(regular(intersection(sF2,cross_product(sF0,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl4_51])],[avatar_definition]) ).
fof(f1039,plain,
( u = first(regular(intersection(sF2,cross_product(sF0,universal_class))))
| ~ spl4_51 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1040,plain,
( spl4_51
| ~ spl4_13
| ~ spl4_50 ),
inference(avatar_split_clause,[],[f1032,f1001,f373,f1037]) ).
fof(f1046,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_27
| ~ spl4_51 ),
inference(superposition,[],[f622,f1039]) ).
fof(f1047,plain,
( regular(intersection(sF2,cross_product(sF0,universal_class))) = unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(u,u)))
| ~ spl4_27
| ~ spl4_33
| ~ spl4_51 ),
inference(forward_demodulation,[],[f1046,f679]) ).
fof(f1050,plain,
( unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class)))
| ~ spl4_4
| ~ spl4_27
| ~ spl4_33
| ~ spl4_51 ),
inference(forward_demodulation,[],[f1047,f303]) ).
fof(f1057,definition,
( spl4_53
<=> unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class))) ),
introduced(definition,[new_symbols(definition,[spl4_53])],[avatar_definition]) ).
fof(f1059,plain,
( unordered_pair(sF0,unordered_pair(u,sF0)) = regular(intersection(sF2,cross_product(sF0,universal_class)))
| ~ spl4_53 ),
inference(avatar_component_clause,[],[f1057]) ).
fof(f1075,plain,
( member(unordered_pair(sF0,unordered_pair(u,sF0)),sF2)
| null_class = intersection(sF2,cross_product(sF0,universal_class))
| ~ spl4_53 ),
inference(superposition,[],[f468,f1059]) ).
fof(f1080,plain,
( member(unordered_pair(sF0,unordered_pair(u,sF0)),sF2)
| spl4_49
| ~ spl4_53 ),
inference(forward_subsumption_resolution,[],[f1075,f998]) ).
fof(f1259,plain,
( member(u,null_class)
| ~ spl4_18
| ~ spl4_23 ),
inference(superposition,[],[f437,f550]) ).
fof(f1538,definition,
( spl4_73
<=> ! [X2,X0] :
( ~ subclass(sF0,X0)
| u = least(X2,sF0)
| ~ well_ordering(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_73])],[avatar_definition]) ).
fof(f1539,plain,
( ! [X2,X0] :
( ~ subclass(sF0,X0)
| u = least(X2,sF0)
| ~ well_ordering(X2,X0) )
| ~ spl4_73 ),
inference(avatar_component_clause,[],[f1538]) ).
fof(f1856,definition,
( spl4_98
<=> member(u,null_class) ),
introduced(definition,[new_symbols(definition,[spl4_98])],[avatar_definition]) ).
fof(f1858,plain,
( member(u,null_class)
| ~ spl4_98 ),
inference(avatar_component_clause,[],[f1856]) ).
fof(f1859,plain,
( spl4_98
| ~ spl4_18
| ~ spl4_23 ),
inference(avatar_split_clause,[],[f1259,f548,f435,f1856]) ).
fof(f2129,plain,
( ! [X0] :
( member(u,X0)
| null_class = X0 )
| ~ spl4_98 ),
inference(resolution,[],[f410,f1858]) ).
fof(f2171,definition,
( spl4_104
<=> ! [X0] :
( member(u,X0)
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl4_104])],[avatar_definition]) ).
fof(f2172,plain,
( ! [X0] :
( member(u,X0)
| null_class = X0 )
| ~ spl4_104 ),
inference(avatar_component_clause,[],[f2171]) ).
fof(f2173,plain,
( spl4_104
| ~ spl4_98 ),
inference(avatar_split_clause,[],[f2129,f1856,f2171]) ).
fof(f2180,plain,
( ! [X0] :
( complement(X0) = null_class
| ~ member(u,X0) )
| ~ spl4_104 ),
inference(resolution,[],[f2172,f24]) ).
fof(f2192,definition,
( spl4_105
<=> ! [X0] :
( complement(X0) = null_class
| ~ member(u,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_105])],[avatar_definition]) ).
fof(f2193,plain,
( ! [X0] :
( ~ member(u,X0)
| complement(X0) = null_class )
| ~ spl4_105 ),
inference(avatar_component_clause,[],[f2192]) ).
fof(f2194,plain,
( spl4_105
| ~ spl4_104 ),
inference(avatar_split_clause,[],[f2180,f2171,f2192]) ).
fof(f2198,plain,
( null_class = complement(y)
| ~ spl4_2
| ~ spl4_105 ),
inference(resolution,[],[f2193,f293]) ).
fof(f2217,definition,
( spl4_106
<=> null_class = complement(y) ),
introduced(definition,[new_symbols(definition,[spl4_106])],[avatar_definition]) ).
fof(f2219,plain,
( null_class = complement(y)
| ~ spl4_106 ),
inference(avatar_component_clause,[],[f2217]) ).
fof(f2220,plain,
( spl4_106
| ~ spl4_2
| ~ spl4_105 ),
inference(avatar_split_clause,[],[f2198,f2192,f291,f2217]) ).
fof(f2226,plain,
( ! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,y) )
| ~ spl4_106 ),
inference(superposition,[],[f24,f2219]) ).
fof(f2228,definition,
( spl4_108
<=> ! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl4_108])],[avatar_definition]) ).
fof(f2229,plain,
( ! [X0] :
( ~ member(X0,y)
| ~ member(X0,null_class) )
| ~ spl4_108 ),
inference(avatar_component_clause,[],[f2228]) ).
fof(f2230,plain,
( spl4_108
| ~ spl4_106 ),
inference(avatar_split_clause,[],[f2226,f2217,f2228]) ).
fof(f2245,plain,
( ~ member(u,null_class)
| ~ spl4_2
| ~ spl4_108 ),
inference(resolution,[],[f2229,f293]) ).
fof(f2249,plain,
( $false
| ~ spl4_2
| ~ spl4_98
| ~ spl4_108 ),
inference(forward_subsumption_resolution,[],[f2245,f1858]) ).
fof(f2250,plain,
( ~ spl4_2
| ~ spl4_98
| ~ spl4_108 ),
inference(avatar_contradiction_clause,[],[f2249]) ).
fof(f2264,plain,
( ! [X0,X1] :
( ~ subclass(sF0,X0)
| ~ well_ordering(X1,X0)
| u = least(X1,sF0) )
| ~ spl4_13
| spl4_23 ),
inference(forward_subsumption_resolution,[],[f793,f549]) ).
fof(f2272,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| ~ spl4_27
| spl4_32
| ~ spl4_46 ),
inference(forward_subsumption_resolution,[],[f911,f671]) ).
fof(f2282,definition,
( spl4_109
<=> member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl4_109])],[avatar_definition]) ).
fof(f2284,plain,
( ~ member(regular(intersection(sF2,cross_product(sF0,universal_class))),sF2)
| spl4_109 ),
inference(avatar_component_clause,[],[f2282]) ).
fof(f2285,plain,
( ~ spl4_109
| ~ spl4_27
| spl4_32
| ~ spl4_46 ),
inference(avatar_split_clause,[],[f2272,f901,f670,f620,f2282]) ).
fof(f2292,plain,
( null_class = intersection(sF2,cross_product(sF0,universal_class))
| spl4_109 ),
inference(resolution,[],[f2284,f468]) ).
fof(f2299,plain,
( $false
| spl4_49
| spl4_109 ),
inference(forward_subsumption_resolution,[],[f2292,f998]) ).
fof(f2300,plain,
( spl4_49
| spl4_109 ),
inference(avatar_contradiction_clause,[],[f2299]) ).
fof(f2533,plain,
( spl4_53
| ~ spl4_4
| ~ spl4_27
| ~ spl4_33
| ~ spl4_51 ),
inference(avatar_split_clause,[],[f1050,f1037,f677,f620,f301,f1057]) ).
fof(f2753,definition,
( spl4_120
<=> ! [X0] :
( ~ member(X0,sF0)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),sF2) ) ),
introduced(definition,[new_symbols(definition,[spl4_120])],[avatar_definition]) ).
fof(f2754,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),sF2)
| ~ member(X0,sF0) )
| ~ spl4_120 ),
inference(avatar_component_clause,[],[f2753]) ).
fof(f2763,plain,
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),sF2)
| ~ member(u,sF0)
| ~ spl4_4
| ~ spl4_120 ),
inference(superposition,[],[f2754,f303]) ).
fof(f2768,plain,
( ~ member(u,sF0)
| ~ spl4_4
| spl4_49
| ~ spl4_53
| ~ spl4_120 ),
inference(forward_subsumption_resolution,[],[f2763,f1080]) ).
fof(f2769,plain,
( $false
| ~ spl4_4
| ~ spl4_18
| spl4_49
| ~ spl4_53
| ~ spl4_120 ),
inference(forward_subsumption_resolution,[],[f2768,f437]) ).
fof(f2770,plain,
( ~ spl4_4
| ~ spl4_18
| spl4_49
| ~ spl4_53
| ~ spl4_120 ),
inference(avatar_contradiction_clause,[],[f2769]) ).
fof(f2780,plain,
( spl4_73
| ~ spl4_13
| spl4_23 ),
inference(avatar_split_clause,[],[f2264,f548,f373,f1538]) ).
fof(f2799,plain,
( ! [X0,X1] :
( u = least(X0,sF0)
| ~ well_ordering(X0,X1)
| u = not_subclass_element(sF0,X1) )
| ~ spl4_21
| ~ spl4_73 ),
inference(resolution,[],[f1539,f540]) ).
fof(f2935,definition,
( spl4_125
<=> ! [X0,X1] :
( u = least(X0,sF0)
| ~ well_ordering(X0,X1)
| u = not_subclass_element(sF0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_125])],[avatar_definition]) ).
fof(f2936,plain,
( ! [X0,X1] :
( ~ well_ordering(X0,X1)
| u = least(X0,sF0)
| u = not_subclass_element(sF0,X1) )
| ~ spl4_125 ),
inference(avatar_component_clause,[],[f2935]) ).
fof(f2937,plain,
( spl4_125
| ~ spl4_21
| ~ spl4_73 ),
inference(avatar_split_clause,[],[f2799,f1538,f539,f2935]) ).
fof(f2938,plain,
( u = least(xr,sF0)
| u = not_subclass_element(sF0,y)
| ~ spl4_1
| ~ spl4_125 ),
inference(resolution,[],[f2936,f288]) ).
fof(f2940,definition,
( spl4_126
<=> u = not_subclass_element(sF0,y) ),
introduced(definition,[new_symbols(definition,[spl4_126])],[avatar_definition]) ).
fof(f2941,plain,
( u != not_subclass_element(sF0,y)
| spl4_126 ),
inference(avatar_component_clause,[],[f2940]) ).
fof(f2942,plain,
( u = not_subclass_element(sF0,y)
| ~ spl4_126 ),
inference(avatar_component_clause,[],[f2940]) ).
fof(f2944,definition,
( spl4_127
<=> u = least(xr,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_127])],[avatar_definition]) ).
fof(f2946,plain,
( u = least(xr,sF0)
| ~ spl4_127 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2947,plain,
( spl4_126
| spl4_127
| ~ spl4_1
| ~ spl4_125 ),
inference(avatar_split_clause,[],[f2938,f2935,f286,f2944,f2940]) ).
fof(f2949,plain,
( ~ member(u,y)
| subclass(sF0,y)
| ~ spl4_126 ),
inference(superposition,[],[f3,f2942]) ).
fof(f2951,plain,
( subclass(sF0,y)
| ~ spl4_2
| ~ spl4_126 ),
inference(forward_subsumption_resolution,[],[f2949,f293]) ).
fof(f2953,definition,
( spl4_128
<=> subclass(sF0,y) ),
introduced(definition,[new_symbols(definition,[spl4_128])],[avatar_definition]) ).
fof(f2954,plain,
( ~ subclass(sF0,y)
| spl4_128 ),
inference(avatar_component_clause,[],[f2953]) ).
fof(f2955,plain,
( subclass(sF0,y)
| ~ spl4_128 ),
inference(avatar_component_clause,[],[f2953]) ).
fof(f2956,plain,
( spl4_128
| ~ spl4_2
| ~ spl4_126 ),
inference(avatar_split_clause,[],[f2951,f2940,f291,f2953]) ).
fof(f2957,plain,
( ! [X0] :
( u = least(X0,sF0)
| ~ well_ordering(X0,y) )
| ~ spl4_73
| ~ spl4_128 ),
inference(resolution,[],[f2955,f1539]) ).
fof(f2960,definition,
( spl4_129
<=> ! [X0] :
( u = least(X0,sF0)
| ~ well_ordering(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl4_129])],[avatar_definition]) ).
fof(f2961,plain,
( ! [X0] :
( ~ well_ordering(X0,y)
| u = least(X0,sF0) )
| ~ spl4_129 ),
inference(avatar_component_clause,[],[f2960]) ).
fof(f2962,plain,
( spl4_129
| ~ spl4_73
| ~ spl4_128 ),
inference(avatar_split_clause,[],[f2957,f2953,f1538,f2960]) ).
fof(f2963,plain,
( u = least(xr,sF0)
| ~ spl4_1
| ~ spl4_129 ),
inference(resolution,[],[f2961,f288]) ).
fof(f2964,plain,
( spl4_127
| ~ spl4_1
| ~ spl4_129 ),
inference(avatar_split_clause,[],[f2963,f2960,f286,f2944]) ).
fof(f2968,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_127 ),
inference(superposition,[],[f254,f2946]) ).
fof(f2969,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_4
| ~ spl4_127 ),
inference(forward_demodulation,[],[f2968,f303]) ).
fof(f2972,definition,
( spl4_130
<=> ! [X1] :
( ~ subclass(sF0,X1)
| ~ well_ordering(xr,X1) ) ),
introduced(definition,[new_symbols(definition,[spl4_130])],[avatar_definition]) ).
fof(f2973,plain,
( ! [X1] :
( ~ well_ordering(xr,X1)
| ~ subclass(sF0,X1) )
| ~ spl4_130 ),
inference(avatar_component_clause,[],[f2972]) ).
fof(f2975,definition,
( spl4_131
<=> ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),xr)
| ~ member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_131])],[avatar_definition]) ).
fof(f2976,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),xr)
| ~ member(X0,sF0) )
| ~ spl4_131 ),
inference(avatar_component_clause,[],[f2975]) ).
fof(f2977,plain,
( spl4_130
| spl4_131
| ~ spl4_4
| ~ spl4_127 ),
inference(avatar_split_clause,[],[f2969,f2944,f301,f2975,f2972]) ).
fof(f2979,plain,
( ~ subclass(sF0,y)
| ~ spl4_1
| ~ spl4_130 ),
inference(resolution,[],[f2973,f288]) ).
fof(f2981,plain,
( $false
| ~ spl4_1
| ~ spl4_128
| ~ spl4_130 ),
inference(forward_subsumption_resolution,[],[f2979,f2955]) ).
fof(f2982,plain,
( ~ spl4_1
| ~ spl4_128
| ~ spl4_130 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f2984,plain,
( u = not_subclass_element(sF0,y)
| ~ spl4_21
| spl4_128 ),
inference(resolution,[],[f2954,f540]) ).
fof(f2986,plain,
( $false
| ~ spl4_21
| spl4_126
| spl4_128 ),
inference(forward_subsumption_resolution,[],[f2984,f2941]) ).
fof(f2987,plain,
( ~ spl4_21
| spl4_126
| spl4_128 ),
inference(avatar_contradiction_clause,[],[f2986]) ).
fof(f2996,plain,
( ! [X0] :
( ~ member(X0,sF0)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF0)),sF2) )
| ~ spl4_7
| ~ spl4_131 ),
inference(resolution,[],[f2976,f319]) ).
fof(f3385,plain,
( spl4_120
| ~ spl4_7
| ~ spl4_131 ),
inference(avatar_split_clause,[],[f2996,f2975,f318,f2753]) ).
cnf(s142,plain,
spl4_1,
inference(sat_conversion,[],[f289]) ).
cnf(s144,plain,
spl4_2,
inference(sat_conversion,[],[f294]) ).
cnf(s146,plain,
spl4_3,
inference(sat_conversion,[],[f299]) ).
cnf(s148,plain,
spl4_4,
inference(sat_conversion,[],[f304]) ).
cnf(s150,plain,
spl4_5,
inference(sat_conversion,[],[f309]) ).
cnf(s152,plain,
spl4_6,
inference(sat_conversion,[],[f314]) ).
cnf(s156,plain,
( ~ spl4_5
| spl4_7 ),
inference(sat_conversion,[],[f320]) ).
cnf(s158,plain,
( ~ spl4_5
| spl4_8 ),
inference(sat_conversion,[],[f324]) ).
cnf(s160,plain,
spl4_9,
inference(sat_conversion,[],[f329]) ).
cnf(s179,plain,
( ~ spl4_3
| spl4_11 ),
inference(sat_conversion,[],[f354]) ).
cnf(s193,plain,
( ~ spl4_4
| spl4_13 ),
inference(sat_conversion,[],[f375]) ).
cnf(s226,plain,
( ~ spl4_4
| spl4_15 ),
inference(sat_conversion,[],[f421]) ).
cnf(s233,plain,
( ~ spl4_4
| spl4_17
| spl4_18 ),
inference(sat_conversion,[],[f438]) ).
cnf(s239,plain,
( ~ spl4_6
| ~ spl4_17 ),
inference(sat_conversion,[],[f459]) ).
cnf(s293,plain,
( ~ spl4_13
| spl4_21 ),
inference(sat_conversion,[],[f541]) ).
cnf(s337,plain,
( ~ spl4_9
| spl4_26 ),
inference(sat_conversion,[],[f611]) ).
cnf(s345,plain,
( ~ spl4_4
| ~ spl4_6
| ~ spl4_26
| spl4_27 ),
inference(sat_conversion,[],[f623]) ).
cnf(s360,plain,
( ~ spl4_27
| spl4_28 ),
inference(sat_conversion,[],[f646]) ).
cnf(s373,plain,
( ~ spl4_13
| ~ spl4_32
| spl4_33 ),
inference(sat_conversion,[],[f680]) ).
cnf(s476,plain,
( ~ spl4_8
| ~ spl4_11
| spl4_46 ),
inference(sat_conversion,[],[f903]) ).
cnf(s532,plain,
( ~ spl4_28
| spl4_49
| spl4_50 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s547,plain,
( ~ spl4_6
| ~ spl4_9
| ~ spl4_15
| ~ spl4_49 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s554,plain,
( ~ spl4_13
| ~ spl4_50
| spl4_51 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s890,plain,
( ~ spl4_18
| ~ spl4_23
| spl4_98 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s1060,plain,
( ~ spl4_98
| spl4_104 ),
inference(sat_conversion,[],[f2173]) ).
cnf(s1070,plain,
( ~ spl4_104
| spl4_105 ),
inference(sat_conversion,[],[f2194]) ).
cnf(s1085,plain,
( ~ spl4_2
| ~ spl4_105
| spl4_106 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s1090,plain,
( ~ spl4_106
| spl4_108 ),
inference(sat_conversion,[],[f2230]) ).
cnf(s1093,plain,
( ~ spl4_2
| ~ spl4_98
| ~ spl4_108 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s1164,plain,
( ~ spl4_27
| spl4_32
| ~ spl4_46
| ~ spl4_109 ),
inference(sat_conversion,[],[f2285]) ).
cnf(s1170,plain,
( spl4_49
| spl4_109 ),
inference(sat_conversion,[],[f2300]) ).
cnf(s1338,plain,
( ~ spl4_4
| ~ spl4_27
| ~ spl4_33
| ~ spl4_51
| spl4_53 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s1425,plain,
( ~ spl4_4
| ~ spl4_18
| spl4_49
| ~ spl4_53
| ~ spl4_120 ),
inference(sat_conversion,[],[f2770]) ).
cnf(s1435,plain,
( ~ spl4_13
| spl4_23
| spl4_73 ),
inference(sat_conversion,[],[f2780]) ).
cnf(s1585,plain,
( ~ spl4_21
| ~ spl4_73
| spl4_125 ),
inference(sat_conversion,[],[f2937]) ).
cnf(s1588,plain,
( ~ spl4_1
| ~ spl4_125
| spl4_126
| spl4_127 ),
inference(sat_conversion,[],[f2947]) ).
cnf(s1592,plain,
( ~ spl4_2
| ~ spl4_126
| spl4_128 ),
inference(sat_conversion,[],[f2956]) ).
cnf(s1596,plain,
( ~ spl4_73
| ~ spl4_128
| spl4_129 ),
inference(sat_conversion,[],[f2962]) ).
cnf(s1599,plain,
( ~ spl4_1
| spl4_127
| ~ spl4_129 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s1603,plain,
( ~ spl4_4
| ~ spl4_127
| spl4_130
| spl4_131 ),
inference(sat_conversion,[],[f2977]) ).
cnf(s1606,plain,
( ~ spl4_1
| ~ spl4_128
| ~ spl4_130 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s1610,plain,
( ~ spl4_21
| spl4_126
| spl4_128 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s1883,plain,
( ~ spl4_7
| spl4_120
| ~ spl4_131 ),
inference(sat_conversion,[],[f3385]) ).
cnf(s1885,plain,
spl4_26,
inference(rat,[],[s337,s160]) ).
cnf(s1886,plain,
~ spl4_17,
inference(rat,[],[s239,s152]) ).
cnf(s1888,plain,
spl4_8,
inference(rat,[],[s158,s150]) ).
cnf(s1889,plain,
spl4_7,
inference(rat,[],[s156,s150]) ).
cnf(s1899,plain,
spl4_27,
inference(rat,[],[s345,s152,s1885,s148]) ).
cnf(s1900,plain,
spl4_18,
inference(rat,[],[s233,s1886,s148]) ).
cnf(s1901,plain,
spl4_15,
inference(rat,[],[s226,s148]) ).
cnf(s1902,plain,
spl4_13,
inference(rat,[],[s193,s148]) ).
cnf(s1906,plain,
spl4_28,
inference(rat,[],[s360,s1899]) ).
cnf(s1908,plain,
~ spl4_49,
inference(rat,[],[s547,s152,s160,s1901]) ).
cnf(s1911,plain,
spl4_21,
inference(rat,[],[s293,s1902]) ).
cnf(s1915,plain,
spl4_109,
inference(rat,[],[s1170,s1908]) ).
cnf(s1916,plain,
spl4_50,
inference(rat,[],[s532,s1906,s1908]) ).
cnf(s1917,plain,
spl4_51,
inference(rat,[],[s554,s1902,s1916]) ).
cnf(s1923,plain,
spl4_11,
inference(rat,[],[s179,s146]) ).
cnf(s1929,plain,
spl4_46,
inference(rat,[],[s476,s1888,s1923]) ).
cnf(s1933,plain,
spl4_32,
inference(rat,[],[s1164,s1915,s1899,s1929]) ).
cnf(s1934,plain,
spl4_33,
inference(rat,[],[s373,s1902,s1933]) ).
cnf(s1937,plain,
spl4_53,
inference(rat,[],[s1338,s1917,s1899,s148,s1934]) ).
cnf(s1942,plain,
~ spl4_120,
inference(rat,[],[s1425,s1908,s1900,s148,s1937]) ).
cnf(s1944,plain,
~ spl4_131,
inference(rat,[],[s1883,s1889,s1942]) ).
cnf(s1954,plain,
~ spl4_98,
inference(rat,[],[s1085,s1070,s1090,s1060,s1093,s144]) ).
cnf(s1955,plain,
~ spl4_23,
inference(rat,[],[s890,s1900,s1954]) ).
cnf(s1957,plain,
spl4_73,
inference(rat,[],[s1435,s1902,s1955]) ).
cnf(s1960,plain,
spl4_125,
inference(rat,[],[s1585,s1911,s1957]) ).
cnf(s1966,plain,
spl4_126,
inference(rat,[],[s1603,s1606,s1588,s1610,s148,s1944,s142,s1960,s1911]) ).
cnf(s1967,plain,
spl4_128,
inference(rat,[],[s1592,s144,s1966]) ).
cnf(s1968,plain,
~ spl4_130,
inference(rat,[],[s1606,s142,s1967]) ).
cnf(s1969,plain,
spl4_129,
inference(rat,[],[s1596,s1957,s1967]) ).
cnf(s1970,plain,
~ spl4_127,
inference(rat,[],[s1603,s1944,s148,s1968]) ).
cnf(s1971,plain,
$false,
inference(rat,[],[s1599,s142,s1969,s1970]) ).
fof(f3386,plain,
$false,
inference(avatar_sat_refutation,[],[s1971]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM076-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n002.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 18:52:22 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.44 Running first-order theorem proving
% 0.13/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.70/3.26 % (3813435)Input is clausal, will run a generic CNF schedule.
% 16.70/3.26 % (3813546)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2249149400:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.70/3.26 % (3813542)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=69834228:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.70/3.26 % (3813541)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=2826394750:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.70/3.26 % (3813543)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4223182264:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.70/3.26 % (3813547)dis-21_1_sil=8000:lcm=predicate:random_seed=3893156345: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)
% 16.70/3.26 % (3813545)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2464289666:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.70/3.26 % (3813544)lrs+10_1_sil=8000:sp=occurrence:random_seed=1208397851:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.70/3.26 % (3813546)Instruction limit reached!
% 16.70/3.26 % (3813546)------------------------------
% 16.70/3.26 % (3813546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.70/3.26 % (3813546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.70/3.26 % (3813546)CaDiCaL version: 2.1.3
% 16.70/3.26 % (3813546)Termination reason: Instruction limit
% 16.70/3.26 % (3813546)Termination phase: Saturation
% 16.70/3.26 % (3813546)Time elapsed: 0.078 s
% 16.70/3.26 % (3813546)Peak memory usage: 90 MB
% 16.70/3.26 % (3813546)Instructions burned: 180 (million)
% 16.70/3.26 % (3813547)Instruction limit reached!
% 16.70/3.26 % (3813547)------------------------------
% 16.70/3.26 % (3813547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.70/3.26 % (3813547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.70/3.26 % (3813547)CaDiCaL version: 2.1.3
% 16.70/3.26 % (3813547)Termination reason: Instruction limit
% 16.70/3.26 % (3813547)Termination phase: Saturation
% 16.70/3.26 % (3813547)Time elapsed: 0.066 s
% 16.70/3.26 % (3813547)Peak memory usage: 89 MB
% 16.70/3.26 % (3813547)Instructions burned: 118 (million)
% 16.70/3.26 % (3813545)Instruction limit reached!
% 16.70/3.26 % (3813545)------------------------------
% 16.70/3.26 % (3813545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.70/3.26 % (3813545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.70/3.26 % (3813545)CaDiCaL version: 2.1.3
% 16.70/3.26 % (3813545)Termination reason: Instruction limit
% 16.70/3.26 % (3813545)Termination phase: Saturation
% 16.70/3.26 % (3813545)Time elapsed: 0.072 s
% 16.70/3.26 % (3813545)Peak memory usage: 89 MB
% 16.70/3.26 % (3813545)Instructions burned: 114 (million)
% 16.70/3.26 % (3813544)Instruction limit reached!
% 16.70/3.26 % (3813544)------------------------------
% 16.70/3.26 % (3813544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.70/3.26 % (3813544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.70/3.26 % (3813544)CaDiCaL version: 2.1.3
% 16.70/3.26 % (3813544)Termination reason: Instruction limit
% 16.70/3.26 % (3813544)Termination phase: Saturation
% 16.70/3.26 % (3813544)Time elapsed: 0.082 s
% 16.70/3.26 % (3813544)Peak memory usage: 89 MB
% 16.70/3.26 % (3813544)Instructions burned: 107 (million)
% 16.70/3.26 % (3813577)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1488875208:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.70/3.26 % (3813577)Refutation not found, incomplete strategy
% 16.70/3.26 % (3813577)------------------------------
% 16.70/3.26 % (3813577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.70/3.26 % (3813577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.70/3.26 % (3813577)CaDiCaL version: 2.1.3
% 16.70/3.26 % (3813577)Termination reason: Refutation not found, incomplete strategy
% 16.70/3.26 % (3813577)Time elapsed: 0.004 s
% 16.70/3.26 % (3813577)Peak memory usage: 88 MB
% 16.70/3.26 % (3813577)Instructions burned: 4 (million)
% 16.70/3.26 % (3813561)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=2297118779:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 30.91/5.26 % (3813561)Refutation not found, incomplete strategy
% 30.91/5.26 % (3813561)------------------------------
% 30.91/5.26 % (3813561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.26 % (3813561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.26 % (3813561)CaDiCaL version: 2.1.3
% 30.91/5.26 % (3813561)Termination reason: Refutation not found, incomplete strategy
% 30.91/5.26 % (3813561)Time elapsed: 0.006 s
% 30.91/5.26 % (3813561)Peak memory usage: 88 MB
% 30.91/5.26 % (3813561)Instructions burned: 3 (million)
% 30.91/5.26 % (3813576)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=63481246: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)
% 30.91/5.26 % (3813584)lrs+10_64_to=lpo:sil=8000:random_seed=2760073788:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 30.91/5.26 % (3813576)Instruction limit reached!
% 30.91/5.26 % (3813576)------------------------------
% 30.91/5.26 % (3813576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.26 % (3813576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.26 % (3813576)CaDiCaL version: 2.1.3
% 30.91/5.26 % (3813576)Termination reason: Instruction limit
% 30.91/5.26 % (3813576)Termination phase: Saturation
% 30.91/5.26 % (3813576)Time elapsed: 0.178 s
% 30.91/5.26 % (3813576)Peak memory usage: 90 MB
% 30.91/5.26 % (3813576)Instructions burned: 190 (million)
% 30.91/5.26 % (3813577)------------------------------
% 30.91/5.26 % (3813577)------------------------------
% 30.91/5.26 % (3813584)Instruction limit reached!
% 30.91/5.26 % (3813584)------------------------------
% 30.91/5.26 % (3813584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.26 % (3813584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.26 % (3813584)CaDiCaL version: 2.1.3
% 30.91/5.26 % (3813584)Termination reason: Instruction limit
% 30.91/5.26 % (3813584)Termination phase: Saturation
% 30.91/5.26 % (3813584)Time elapsed: 0.139 s
% 30.91/5.26 % (3813584)Peak memory usage: 89 MB
% 30.91/5.26 % (3813584)Instructions burned: 126 (million)
% 30.91/5.26 % (3813561)------------------------------
% 30.91/5.26 % (3813561)------------------------------
% 30.91/5.26 % (3813603)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3591958629:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 30.91/5.26 % (3813602)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2280841089:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 30.91/5.26 % (3813603)Instruction limit reached!
% 30.91/5.26 % (3813603)------------------------------
% 30.91/5.26 % (3813603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.26 % (3813603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.26 % (3813603)CaDiCaL version: 2.1.3
% 30.91/5.26 % (3813603)Termination reason: Instruction limit
% 30.91/5.26 % (3813603)Termination phase: Saturation
% 30.91/5.26 % (3813603)Time elapsed: 0.095 s
% 30.91/5.26 % (3813603)Peak memory usage: 91 MB
% 30.91/5.26 % (3813603)Instructions burned: 157 (million)
% 30.91/5.26 % (3813604)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4232156426:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 30.91/5.26 % (3813602)Instruction limit reached!
% 30.91/5.26 % (3813602)------------------------------
% 30.91/5.26 % (3813602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.26 % (3813602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.26 % (3813602)CaDiCaL version: 2.1.3
% 30.91/5.26 % (3813602)Termination reason: Instruction limit
% 30.91/5.26 % (3813602)Termination phase: Saturation
% 30.91/5.26 % (3813602)Time elapsed: 0.186 s
% 30.91/5.26 % (3813602)Peak memory usage: 90 MB
% 30.91/5.26 % (3813602)Instructions burned: 194 (million)
% 30.91/5.26 % (3813605)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=274857426:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 30.91/5.26 % (3813610)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3421046595:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 45.59/7.30 % (3813605)Instruction limit reached!
% 45.59/7.30 % (3813605)------------------------------
% 45.59/7.30 % (3813605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813605)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813605)Termination reason: Instruction limit
% 45.59/7.30 % (3813605)Termination phase: Saturation
% 45.59/7.30 % (3813605)Time elapsed: 0.116 s
% 45.59/7.30 % (3813605)Peak memory usage: 89 MB
% 45.59/7.30 % (3813605)Instructions burned: 106 (million)
% 45.59/7.30 % (3813610)Instruction limit reached!
% 45.59/7.30 % (3813610)------------------------------
% 45.59/7.30 % (3813610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813610)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813610)Termination reason: Instruction limit
% 45.59/7.30 % (3813610)Termination phase: Saturation
% 45.59/7.30 % (3813610)Time elapsed: 0.073 s
% 45.59/7.30 % (3813610)Peak memory usage: 89 MB
% 45.59/7.30 % (3813610)Instructions burned: 109 (million)
% 45.59/7.30 % (3813612)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1803341662:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 45.59/7.30 % (3813619)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3370115659:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 45.59/7.30 % (3813620)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2072519319:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 45.59/7.30 % (3813612)Instruction limit reached!
% 45.59/7.30 % (3813612)------------------------------
% 45.59/7.30 % (3813612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813612)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813612)Termination reason: Instruction limit
% 45.59/7.30 % (3813612)Termination phase: Saturation
% 45.59/7.30 % (3813612)Time elapsed: 0.262 s
% 45.59/7.30 % (3813612)Peak memory usage: 90 MB
% 45.59/7.30 % (3813612)Instructions burned: 242 (million)
% 45.59/7.30 % (3813620)Instruction limit reached!
% 45.59/7.30 % (3813620)------------------------------
% 45.59/7.30 % (3813620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813620)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813620)Termination reason: Instruction limit
% 45.59/7.30 % (3813620)Termination phase: Saturation
% 45.59/7.30 % (3813620)Time elapsed: 0.153 s
% 45.59/7.30 % (3813620)Peak memory usage: 90 MB
% 45.59/7.30 % (3813620)Instructions burned: 135 (million)
% 45.59/7.30 % (3813626)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2865908803:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 45.59/7.30 % (3813627)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2272052624:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 45.59/7.30 % (3813627)Instruction limit reached!
% 45.59/7.30 % (3813627)------------------------------
% 45.59/7.30 % (3813627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813627)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813627)Termination reason: Instruction limit
% 45.59/7.30 % (3813627)Termination phase: Saturation
% 45.59/7.30 % (3813627)Time elapsed: 0.179 s
% 45.59/7.30 % (3813627)Peak memory usage: 89 MB
% 45.59/7.30 % (3813627)Instructions burned: 191 (million)
% 45.59/7.30 % (3813637)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1229833203:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 45.59/7.30 % (3813626)Instruction limit reached!
% 45.59/7.30 % (3813626)------------------------------
% 45.59/7.30 % (3813626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.59/7.30 % (3813626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.59/7.30 % (3813626)CaDiCaL version: 2.1.3
% 45.59/7.30 % (3813626)Termination reason: Instruction limit
% 45.59/7.30 % (3813626)Termination phase: Saturation
% 45.59/7.30 % (3813626)Time elapsed: 0.510 s
% 83.42/12.68 % (3813626)Peak memory usage: 95 MB
% 83.42/12.68 % (3813626)Instructions burned: 499 (million)
% 83.42/12.68 % (3813637)Instruction limit reached!
% 83.42/12.68 % (3813637)------------------------------
% 83.42/12.68 % (3813637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.42/12.68 % (3813637)CaDiCaL version: 2.1.3
% 83.42/12.68 % (3813637)Termination reason: Instruction limit
% 83.42/12.68 % (3813637)Termination phase: Saturation
% 83.42/12.68 % (3813637)Time elapsed: 0.261 s
% 83.42/12.68 % (3813637)Peak memory usage: 92 MB
% 83.42/12.68 % (3813637)Instructions burned: 264 (million)
% 83.42/12.68 % (3813640)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3480587649:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 83.42/12.68 % (3813640)Instruction limit reached!
% 83.42/12.68 % (3813640)------------------------------
% 83.42/12.68 % (3813640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.42/12.68 % (3813640)CaDiCaL version: 2.1.3
% 83.42/12.68 % (3813640)Termination reason: Instruction limit
% 83.42/12.68 % (3813640)Termination phase: Saturation
% 83.42/12.68 % (3813640)Time elapsed: 0.186 s
% 83.42/12.68 % (3813640)Peak memory usage: 90 MB
% 83.42/12.68 % (3813640)Instructions burned: 157 (million)
% 83.42/12.68 % (3813641)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=3832845647:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 83.42/12.68 % (3813645)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1263389032:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 83.42/12.68 % (3813645)Instruction limit reached!
% 83.42/12.68 % (3813645)------------------------------
% 83.42/12.68 % (3813645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.42/12.68 % (3813645)CaDiCaL version: 2.1.3
% 83.42/12.68 % (3813645)Termination reason: Instruction limit
% 83.42/12.68 % (3813645)Termination phase: Saturation
% 83.42/12.68 % (3813645)Time elapsed: 0.438 s
% 83.42/12.68 % (3813645)Peak memory usage: 89 MB
% 83.42/12.68 % (3813645)Instructions burned: 537 (million)
% 83.42/12.68 % (3813648)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1937004151:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 83.42/12.68 % (3813648)Instruction limit reached!
% 83.42/12.68 % (3813648)------------------------------
% 83.42/12.68 % (3813648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.42/12.68 % (3813648)CaDiCaL version: 2.1.3
% 83.42/12.68 % (3813648)Termination reason: Instruction limit
% 83.42/12.68 % (3813648)Termination phase: Saturation
% 83.42/12.68 % (3813648)Time elapsed: 0.168 s
% 83.42/12.68 % (3813648)Peak memory usage: 90 MB
% 83.42/12.68 % (3813648)Instructions burned: 181 (million)
% 83.42/12.68 % (3813604)Instruction limit reached!
% 83.42/12.68 % (3813604)------------------------------
% 83.42/12.68 % (3813604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.42/12.68 % (3813604)CaDiCaL version: 2.1.3
% 83.42/12.68 % (3813604)Termination reason: Instruction limit
% 83.42/12.68 % (3813604)Termination phase: Saturation
% 83.42/12.68 % (3813604)Time elapsed: 3.118 s
% 83.42/12.68 % (3813604)Peak memory usage: 146 MB
% 83.42/12.68 % (3813604)Instructions burned: 3395 (million)
% 83.42/12.68 % (3813652)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=995442129:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi)
% 83.42/12.68 % (3813653)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=3165205849:i=412:gtgl=4:gtg=exists_all_2958 on theBenchmark for (2958ds/412Mi)
% 83.42/12.68 % (3813619)Instruction limit reached!
% 83.42/12.68 % (3813619)------------------------------
% 83.42/12.68 % (3813619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.42/12.68 % (3813619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813619)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813619)Termination reason: Instruction limit
% 123.63/18.34 % (3813619)Termination phase: Saturation
% 123.63/18.34 % (3813619)Time elapsed: 2.907 s
% 123.63/18.34 % (3813619)Peak memory usage: 157 MB
% 123.63/18.34 % (3813619)Instructions burned: 5208 (million)
% 123.63/18.34 % (3813653)Instruction limit reached!
% 123.63/18.34 % (3813653)------------------------------
% 123.63/18.34 % (3813653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.63/18.34 % (3813653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813653)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813653)Termination reason: Instruction limit
% 123.63/18.34 % (3813653)Termination phase: Saturation
% 123.63/18.34 % (3813653)Time elapsed: 0.174 s
% 123.63/18.34 % (3813653)Peak memory usage: 90 MB
% 123.63/18.34 % (3813653)Instructions burned: 413 (million)
% 123.63/18.34 % (3813658)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=634315288:s2pl=no:i=8478:s2at=4:nm=6_2956 on theBenchmark for (2956ds/8478Mi)
% 123.63/18.34 % (3813659)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=3377393878:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2954 on theBenchmark for (2954ds/303Mi)
% 123.63/18.34 % (3813659)Refutation not found, incomplete strategy
% 123.63/18.34 % (3813659)------------------------------
% 123.63/18.34 % (3813659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.63/18.34 % (3813659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813659)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813659)Termination reason: Refutation not found, incomplete strategy
% 123.63/18.34 % (3813659)Time elapsed: 0.002 s
% 123.63/18.34 % (3813659)Peak memory usage: 88 MB
% 123.63/18.34 % (3813659)Instructions burned: 1 (million)
% 123.63/18.34 % (3813659)------------------------------
% 123.63/18.34 % (3813659)------------------------------
% 123.63/18.34 % (3813662)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3719864961:st=4:i=720:sd=3:fsr=off:ss=axioms_2949 on theBenchmark for (2949ds/720Mi)
% 123.63/18.34 % (3813662)Instruction limit reached!
% 123.63/18.34 % (3813662)------------------------------
% 123.63/18.34 % (3813662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.63/18.34 % (3813662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813662)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813662)Termination reason: Instruction limit
% 123.63/18.34 % (3813662)Termination phase: Saturation
% 123.63/18.34 % (3813662)Time elapsed: 0.372 s
% 123.63/18.34 % (3813662)Peak memory usage: 98 MB
% 123.63/18.34 % (3813662)Instructions burned: 721 (million)
% 123.63/18.34 % (3813664)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=404926415:i=598:bs=on:bd=preordered:av=off:ss=axioms_2943 on theBenchmark for (2943ds/598Mi)
% 123.63/18.34 % (3813641)Instruction limit reached!
% 123.63/18.34 % (3813641)------------------------------
% 123.63/18.34 % (3813641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.63/18.34 % (3813641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813641)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813641)Termination reason: Instruction limit
% 123.63/18.34 % (3813641)Termination phase: Saturation
% 123.63/18.34 % (3813641)Time elapsed: 3.163 s
% 123.63/18.34 % (3813641)Peak memory usage: 150 MB
% 123.63/18.34 % (3813641)Instructions burned: 3257 (million)
% 123.63/18.34 % (3813664)Instruction limit reached!
% 123.63/18.34 % (3813664)------------------------------
% 123.63/18.34 % (3813664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.63/18.34 % (3813664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.63/18.34 % (3813664)CaDiCaL version: 2.1.3
% 123.63/18.34 % (3813664)Termination reason: Instruction limit
% 123.63/18.34 % (3813664)Termination phase: Saturation
% 123.63/18.34 % (3813664)Time elapsed: 0.303 s
% 123.63/18.34 % (3813664)Peak memory usage: 94 MB
% 123.63/18.34 % (3813664)Instructions burned: 599 (million)
% 123.63/18.34 % (3813666)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1003464973:i=2989:sd=3:ss=axioms:sgt=60_2939 on theBenchmark for (2939ds/2989Mi)
% 123.63/18.34 % (3813669)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=1223981607:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2938 on theBenchmark for (2938ds/1997Mi)
% 69.78/20.86 % (3813669)Instruction limit reached!
% 69.78/20.86 % (3813669)------------------------------
% 69.78/20.86 % (3813669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813669)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813669)Termination reason: Instruction limit
% 69.78/20.86 % (3813669)Termination phase: Saturation
% 69.78/20.86 % (3813669)Time elapsed: 1.205 s
% 69.78/20.86 % (3813669)Peak memory usage: 138 MB
% 69.78/20.86 % (3813669)Instructions burned: 1998 (million)
% 69.78/20.86 % (3813676)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=1285531858:i=2088:bd=preordered:av=off_2923 on theBenchmark for (2923ds/2088Mi)
% 69.78/20.86 % (3813676)Instruction limit reached!
% 69.78/20.86 % (3813676)------------------------------
% 69.78/20.86 % (3813676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813676)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813676)Termination reason: Instruction limit
% 69.78/20.86 % (3813676)Termination phase: Saturation
% 69.78/20.86 % (3813676)Time elapsed: 1.199 s
% 69.78/20.86 % (3813676)Peak memory usage: 137 MB
% 69.78/20.86 % (3813676)Instructions burned: 2088 (million)
% 69.78/20.86 % (3813666)Instruction limit reached!
% 69.78/20.86 % (3813666)------------------------------
% 69.78/20.86 % (3813666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813666)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813666)Termination reason: Instruction limit
% 69.78/20.86 % (3813666)Termination phase: Saturation
% 69.78/20.86 % (3813666)Time elapsed: 2.913 s
% 69.78/20.86 % (3813666)Peak memory usage: 143 MB
% 69.78/20.86 % (3813666)Instructions burned: 2989 (million)
% 69.78/20.86 % (3813680)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3605786157:i=1098:nicw=on_2909 on theBenchmark for (2909ds/1098Mi)
% 69.78/20.86 % (3813681)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=528456408:i=433:bd=preordered_2906 on theBenchmark for (2906ds/433Mi)
% 69.78/20.86 % (3813680)Instruction limit reached!
% 69.78/20.86 % (3813680)------------------------------
% 69.78/20.86 % (3813680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813680)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813680)Termination reason: Instruction limit
% 69.78/20.86 % (3813680)Termination phase: Saturation
% 69.78/20.86 % (3813680)Time elapsed: 0.581 s
% 69.78/20.86 % (3813680)Peak memory usage: 103 MB
% 69.78/20.86 % (3813680)Instructions burned: 1100 (million)
% 69.78/20.86 % (3813681)Instruction limit reached!
% 69.78/20.86 % (3813681)------------------------------
% 69.78/20.86 % (3813681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813681)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813681)Termination reason: Instruction limit
% 69.78/20.86 % (3813681)Termination phase: Saturation
% 69.78/20.86 % (3813681)Time elapsed: 0.443 s
% 69.78/20.86 % (3813681)Peak memory usage: 92 MB
% 69.78/20.86 % (3813681)Instructions burned: 434 (million)
% 69.78/20.86 % (3813684)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2242509466:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2900 on theBenchmark for (2900ds/2942Mi)
% 69.78/20.86 % (3813685)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=877688739:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2899 on theBenchmark for (2899ds/6922Mi)
% 69.78/20.86 % (3813684)Instruction limit reached!
% 69.78/20.86 % (3813684)------------------------------
% 69.78/20.86 % (3813684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813684)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813684)Termination reason: Instruction limit
% 69.78/20.86 % (3813684)Termination phase: Saturation
% 69.78/20.86 % (3813684)Time elapsed: 1.667 s
% 69.78/20.86 % (3813684)Peak memory usage: 141 MB
% 69.78/20.86 % (3813684)Instructions burned: 2943 (million)
% 69.78/20.86 % (3813658)Instruction limit reached!
% 69.78/20.86 % (3813658)------------------------------
% 69.78/20.86 % (3813658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813658)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813658)Termination reason: Instruction limit
% 69.78/20.86 % (3813658)Termination phase: Saturation
% 69.78/20.86 % (3813658)Time elapsed: 7.336 s
% 69.78/20.86 % (3813658)Peak memory usage: 186 MB
% 69.78/20.86 % (3813658)Instructions burned: 8478 (million)
% 69.78/20.86 % (3813688)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=3660743470:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2881 on theBenchmark for (2881ds/596Mi)
% 69.78/20.86 % (3813691)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=2923383465:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2880 on theBenchmark for (2880ds/4123Mi)
% 69.78/20.86 % (3813688)Instruction limit reached!
% 69.78/20.86 % (3813688)------------------------------
% 69.78/20.86 % (3813688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813688)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813688)Termination reason: Instruction limit
% 69.78/20.86 % (3813688)Termination phase: Saturation
% 69.78/20.86 % (3813688)Time elapsed: 0.278 s
% 69.78/20.86 % (3813688)Peak memory usage: 99 MB
% 69.78/20.86 % (3813688)Instructions burned: 597 (million)
% 69.78/20.86 % (3813695)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2645651466:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2876 on theBenchmark for (2876ds/16411Mi)
% 69.78/20.86 % (3813652)Instruction limit reached!
% 69.78/20.86 % (3813652)------------------------------
% 69.78/20.86 % (3813652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813652)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813652)Termination reason: Instruction limit
% 69.78/20.86 % (3813652)Termination phase: Saturation
% 69.78/20.86 % (3813652)Time elapsed: 11.284 s
% 69.78/20.86 % (3813652)Peak memory usage: 174 MB
% 69.78/20.86 % (3813652)Instructions burned: 10308 (million)
% 69.78/20.86 % (3813702)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1723084726:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2843 on theBenchmark for (2843ds/1670Mi)
% 69.78/20.86 % (3813691)Instruction limit reached!
% 69.78/20.86 % (3813691)------------------------------
% 69.78/20.86 % (3813691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813691)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813691)Termination reason: Instruction limit
% 69.78/20.86 % (3813691)Termination phase: Saturation
% 69.78/20.86 % (3813691)Time elapsed: 4.195 s
% 69.78/20.86 % (3813691)Peak memory usage: 155 MB
% 69.78/20.86 % (3813691)Instructions burned: 4123 (million)
% 69.78/20.86 % (3813704)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=2492824651:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2835 on theBenchmark for (2835ds/1722Mi)
% 69.78/20.86 % (3813685)Instruction limit reached!
% 69.78/20.86 % (3813685)------------------------------
% 69.78/20.86 % (3813685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813685)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813685)Termination reason: Instruction limit
% 69.78/20.86 % (3813685)Termination phase: Saturation
% 69.78/20.86 % (3813685)Time elapsed: 6.876 s
% 69.78/20.86 % (3813685)Peak memory usage: 183 MB
% 69.78/20.86 % (3813685)Instructions burned: 6922 (million)
% 69.78/20.86 % (3813706)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=2754071603:cts=off:cond=on:i=9530:bs=on:fsd=on_2828 on theBenchmark for (2828ds/9530Mi)
% 69.78/20.86 % (3813702)Instruction limit reached!
% 69.78/20.86 % (3813702)------------------------------
% 69.78/20.86 % (3813702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813702)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813702)Termination reason: Instruction limit
% 69.78/20.86 % (3813702)Termination phase: Saturation
% 69.78/20.86 % (3813702)Time elapsed: 1.716 s
% 69.78/20.86 % (3813702)Peak memory usage: 137 MB
% 69.78/20.86 % (3813702)Instructions burned: 1670 (million)
% 69.78/20.86 % (3813710)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2678999513:st=2:i=4495:sd=10:ss=included_2824 on theBenchmark for (2824ds/4495Mi)
% 69.78/20.86 % (3813704)Instruction limit reached!
% 69.78/20.86 % (3813704)------------------------------
% 69.78/20.86 % (3813704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.78/20.86 % (3813704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.78/20.86 % (3813704)CaDiCaL version: 2.1.3
% 69.78/20.86 % (3813704)Termination reason: Instruction limit
% 69.78/20.86 % (3813704)Termination phase: Saturation
% 69.78/20.86 % (3813704)Time elapsed: 1.868 s
% 69.78/20.86 % (3813704)Peak memory usage: 135 MB
% 69.78/20.86 % (3813704)Instructions burned: 1722 (million)
% 69.78/20.86 % (3813712)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=1403747651:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2813 on theBenchmark for (2813ds/4920Mi)
% 69.78/20.86 % (3813706)First to succeed.
% 69.78/20.86 % (3813706)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3813435"
% 69.78/20.86 % (3813706)Refutation found. Thanks to Tanya!
% 69.78/20.86 % SZS status Unsatisfiable for theBenchmark
% 69.78/20.86 % SZS output start Proof for theBenchmark
% See solution above
% 142.11/21.11 % (3813706)------------------------------
% 142.11/21.11 % (3813706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.11/21.11 % (3813706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.11/21.11 % (3813706)CaDiCaL version: 2.1.3
% 142.11/21.11 % (3813706)Termination reason: Refutation
% 142.11/21.11 % (3813706)Time elapsed: 2.041 s
% 142.11/21.11 % (3813706)Peak memory usage: 136 MB
% 142.11/21.11 % (3813706)Instructions burned: 1822 (million)
% 142.11/21.11 % (3813706)------------------------------
% 142.11/21.11 % (3813706)------------------------------
% 142.11/21.11 % (3813435)Success in time 19.978 s
% 142.11/21.11 % Vampire exiting
%------------------------------------------------------------------------------