%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET099+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:40:06 PM UTC 2026
% Result : Theorem 12.38s 2.66s
% Output : Refutation 13.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of formulae : 157 ( 19 unt; 4 def)
% Number of atoms : 442 ( 121 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 462 ( 177 ~; 225 |; 44 &)
% ( 10 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 212 ( 0 sgn 203 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subclass(X0,X1)
<=> ! [X2] :
( member(X2,X0)
=> member(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_defn) ).
fof(f2,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f3,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subclass(X0,X1)
& subclass(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality) ).
fof(f4,axiom,
! [X0,X1,X2] :
( member(X0,unordered_pair(X1,X2))
<=> ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_defn) ).
fof(f6,axiom,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set_defn) ).
fof(f13,axiom,
! [X0,X1,X2] :
( member(X2,intersection(X0,X1))
<=> ( member(X2,X0)
& member(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection) ).
fof(f14,axiom,
! [X0,X1] :
( member(X1,complement(X0))
<=> ( member(X1,universal_class)
& ~ member(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement) ).
fof(f16,axiom,
! [X0] : ~ member(X0,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',null_class_defn) ).
fof(f41,axiom,
! [X0] :
( X0 != null_class
=> ? [X1] :
( member(X1,universal_class)
& member(X1,X0)
& disjoint(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity) ).
fof(f44,conjecture,
! [X0] :
( ! [X1,X2] :
( ( member(X1,X0)
& member(X2,intersection(complement(singleton(X1)),X0)) )
=> X1 = X2 )
=> ( X0 = null_class
| ? [X3] : singleton(X3) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_2_to_number_of_elements_in_class) ).
fof(f45,negated_conjecture,
~ ! [X0] :
( ! [X1,X2] :
( ( member(X1,X0)
& member(X2,intersection(complement(singleton(X1)),X0)) )
=> X1 = X2 )
=> ( X0 = null_class
| ? [X3] : singleton(X3) = X0 ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f47,plain,
! [X0,X1] :
( subclass(X0,X1)
<=> ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f57,plain,
! [X0] :
( ? [X1] :
( member(X1,universal_class)
& member(X1,X0)
& disjoint(X1,X0) )
| null_class = X0 ),
inference(ennf_transformation,[],[f41]) ).
fof(f60,plain,
? [X0] :
( null_class != X0
& ! [X3] : singleton(X3) != X0
& ! [X1,X2] :
( X1 = X2
| ~ member(X1,X0)
| ~ member(X2,intersection(complement(singleton(X1)),X0)) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f61,plain,
? [X0] :
( null_class != X0
& ! [X3] : singleton(X3) != X0
& ! [X1,X2] :
( X1 = X2
| ~ member(X1,X0)
| ~ member(X2,intersection(complement(singleton(X1)),X0)) ) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) )
| ~ subclass(X0,X1) ) ),
inference(nnf_transformation,[],[f47]) ).
fof(f63,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subclass(X0,X1) ) ),
inference(rectify,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( ( subclass(X0,X1)
| ( ~ member(sK0(X0,X1),X1)
& member(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subclass(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subclass(X0,X1)
| ~ subclass(X1,X0) )
& ( ( subclass(X0,X1)
& subclass(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f66,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subclass(X0,X1)
| ~ subclass(X1,X0) )
& ( ( subclass(X0,X1)
& subclass(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f65]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| ( X0 != X1
& X0 != X2 ) )
& ( ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) )
| ~ member(X0,unordered_pair(X1,X2)) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f68,plain,
! [X0,X1,X2] :
( ( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| ( X0 != X1
& X0 != X2 ) )
& ( ( member(X0,universal_class)
& ( X0 = X1
| X0 = X2 ) )
| ~ member(X0,unordered_pair(X1,X2)) ) ),
inference(flattening,[],[f67]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ( member(X2,intersection(X0,X1))
| ~ member(X2,X0)
| ~ member(X2,X1) )
& ( ( member(X2,X0)
& member(X2,X1) )
| ~ member(X2,intersection(X0,X1)) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ( member(X2,intersection(X0,X1))
| ~ member(X2,X0)
| ~ member(X2,X1) )
& ( ( member(X2,X0)
& member(X2,X1) )
| ~ member(X2,intersection(X0,X1)) ) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( ( member(X1,complement(X0))
| ~ member(X1,universal_class)
| member(X1,X0) )
& ( ( member(X1,universal_class)
& ~ member(X1,X0) )
| ~ member(X1,complement(X0)) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f76,plain,
! [X0,X1] :
( ( member(X1,complement(X0))
| ~ member(X1,universal_class)
| member(X1,X0) )
& ( ( member(X1,universal_class)
& ~ member(X1,X0) )
| ~ member(X1,complement(X0)) ) ),
inference(flattening,[],[f75]) ).
fof(f102,plain,
! [X0] :
( ( member(sK4(X0),universal_class)
& member(sK4(X0),X0)
& disjoint(sK4(X0),X0) )
| null_class = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f57]) ).
fof(f104,plain,
? [X0] :
( null_class != X0
& ! [X1] : singleton(X1) != X0
& ! [X2,X3] :
( X2 = X3
| ~ member(X2,X0)
| ~ member(X3,intersection(complement(singleton(X2)),X0)) ) ),
inference(rectify,[],[f61]) ).
fof(f105,plain,
( null_class != sK6
& ! [X1] : singleton(X1) != sK6
& ! [X2,X3] :
( X2 = X3
| ~ member(X2,sK6)
| ~ member(X3,intersection(complement(singleton(X2)),sK6)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X0,sK6)],[f104]) ).
fof(f106,plain,
! [X3,X0,X1] :
( ~ member(X3,X0)
| member(X3,X1)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f107,plain,
! [X0,X1] :
( member(sK0(X0,X1),X0)
| subclass(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f108,plain,
! [X0,X1] :
( ~ member(sK0(X0,X1),X1)
| subclass(X0,X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f109,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[],[f2]) ).
fof(f112,plain,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f66]) ).
fof(f113,plain,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[],[f68]) ).
fof(f115,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X1,X2))
| ~ member(X0,universal_class)
| X0 != X2 ),
inference(cnf_transformation,[],[f68]) ).
fof(f118,plain,
! [X0] : singleton(X0) = unordered_pair(X0,X0),
inference(cnf_transformation,[],[f6]) ).
fof(f130,plain,
! [X2,X0,X1] :
( ~ member(X2,intersection(X0,X1))
| member(X2,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ member(X2,intersection(X0,X1))
| member(X2,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f132,plain,
! [X2,X0,X1] :
( member(X2,intersection(X0,X1))
| ~ member(X2,X0)
| ~ member(X2,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f133,plain,
! [X0,X1] :
( ~ member(X1,complement(X0))
| ~ member(X1,X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f134,plain,
! [X0,X1] :
( ~ member(X1,complement(X0))
| member(X1,universal_class) ),
inference(cnf_transformation,[],[f76]) ).
fof(f135,plain,
! [X0,X1] :
( member(X1,complement(X0))
| ~ member(X1,universal_class)
| member(X1,X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f137,plain,
! [X0] : ~ member(X0,null_class),
inference(cnf_transformation,[],[f16]) ).
fof(f188,plain,
! [X0] :
( member(sK4(X0),X0)
| null_class = X0 ),
inference(cnf_transformation,[],[f102]) ).
fof(f189,plain,
! [X0] :
( member(sK4(X0),universal_class)
| null_class = X0 ),
inference(cnf_transformation,[],[f102]) ).
fof(f193,plain,
! [X2,X3] :
( X2 = X3
| ~ member(X2,sK6)
| ~ member(X3,intersection(complement(singleton(X2)),sK6)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f194,plain,
! [X1] : singleton(X1) != sK6,
inference(cnf_transformation,[],[f105]) ).
fof(f195,plain,
null_class != sK6,
inference(cnf_transformation,[],[f105]) ).
fof(f233,plain,
! [X1] : sK6 != unordered_pair(X1,X1),
inference(definition_unfolding,[],[f194,f118]) ).
fof(f234,plain,
! [X2,X3] :
( ~ member(X3,intersection(complement(unordered_pair(X2,X2)),sK6))
| ~ member(X2,sK6)
| X2 = X3 ),
inference(definition_unfolding,[],[f193,f118]) ).
fof(f238,plain,
! [X2,X1] :
( member(X2,unordered_pair(X1,X2))
| ~ member(X2,universal_class) ),
inference(equality_resolution,[],[f115]) ).
fof(f241,plain,
! [X0] :
( ~ member(X0,sK6)
| sK4(intersection(complement(unordered_pair(X0,X0)),sK6)) = X0
| null_class = intersection(complement(unordered_pair(X0,X0)),sK6) ),
inference(resolution,[],[f234,f188]) ).
fof(f244,plain,
! [X0,X1] :
( ~ member(sK0(X0,complement(X1)),universal_class)
| subclass(X0,complement(X1))
| member(sK0(X0,complement(X1)),X1) ),
inference(resolution,[],[f108,f135]) ).
fof(f249,plain,
! [X0,X1] :
( member(sK4(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f130,f188]) ).
fof(f256,plain,
! [X0,X1] :
( member(sK4(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f131,f188]) ).
fof(f257,plain,
! [X2,X0,X1] :
( member(sK0(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f131,f107]) ).
fof(f259,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f257,f108]) ).
fof(f264,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f259]) ).
fof(f265,plain,
! [X0,X1] :
( ~ member(X0,complement(unordered_pair(X1,X1)))
| ~ member(X0,sK6)
| ~ member(X1,sK6)
| X0 = X1 ),
inference(resolution,[],[f132,f234]) ).
fof(f268,plain,
! [X2,X0,X1] :
( ~ member(sK0(X0,intersection(X1,X2)),X2)
| ~ member(sK0(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f132,f108]) ).
fof(f278,plain,
! [X0,X1] :
( member(X0,unordered_pair(X1,X1))
| ~ member(X1,sK6)
| X0 = X1
| ~ member(X0,universal_class)
| ~ member(X0,sK6) ),
inference(resolution,[],[f265,f135]) ).
fof(f288,plain,
! [X0,X1] :
( ~ subclass(X0,intersection(X0,X1))
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f264,f112]) ).
fof(f296,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X1,sK6)
| X0 = X1
| ~ member(X0,universal_class)
| ~ member(X0,sK6) ),
inference(resolution,[],[f113,f278]) ).
fof(f297,plain,
! [X2,X0,X1] :
( subclass(unordered_pair(X0,X1),X2)
| sK0(unordered_pair(X0,X1),X2) = X0
| sK0(unordered_pair(X0,X1),X2) = X1 ),
inference(resolution,[],[f113,f107]) ).
fof(f300,plain,
! [X0,X1] :
( ~ member(X1,sK6)
| X0 = X1
| ~ member(X0,universal_class)
| ~ member(X0,sK6) ),
inference(duplicate_literal_removal,[],[f296]) ).
fof(f301,plain,
! [X0] :
( sK4(sK6) = X0
| ~ member(X0,universal_class)
| ~ member(X0,sK6)
| null_class = sK6 ),
inference(resolution,[],[f300,f188]) ).
fof(f302,plain,
! [X0,X1] :
( ~ member(X0,sK6)
| ~ member(X0,universal_class)
| sK0(sK6,X1) = X0
| subclass(sK6,X1) ),
inference(resolution,[],[f300,f107]) ).
fof(f305,plain,
! [X0] :
( ~ member(X0,sK6)
| ~ member(X0,universal_class)
| sK4(sK6) = X0 ),
inference(forward_subsumption_resolution,[],[f301,f195]) ).
fof(f306,plain,
! [X0] :
( ~ member(sK4(sK6),universal_class)
| sK4(sK6) = sK0(sK6,X0)
| subclass(sK6,X0)
| null_class = sK6 ),
inference(resolution,[],[f302,f188]) ).
fof(f310,plain,
! [X0] :
( sK4(sK6) = sK0(sK6,X0)
| subclass(sK6,X0)
| null_class = sK6 ),
inference(forward_subsumption_resolution,[],[f306,f189]) ).
fof(f311,plain,
! [X0] :
( subclass(sK6,X0)
| sK4(sK6) = sK0(sK6,X0) ),
inference(forward_subsumption_resolution,[],[f310,f195]) ).
fof(f326,plain,
! [X2,X0,X1] :
( member(sK0(X0,X1),X2)
| ~ subclass(X0,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f106,f107]) ).
fof(f354,definition,
( spl7_2
<=> member(sK4(sK6),sK6) ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f355,plain,
( ~ member(sK4(sK6),sK6)
| spl7_2 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( member(sK4(sK6),sK6)
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f371,plain,
! [X2,X0,X1] :
( ~ subclass(X0,X1)
| subclass(X0,intersection(X2,X1))
| ~ member(sK0(X0,intersection(X2,X1)),X2)
| subclass(X0,intersection(X2,X1)) ),
inference(resolution,[],[f326,f268]) ).
fof(f372,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,complement(X1))
| subclass(X0,complement(X1))
| member(sK0(X0,complement(X1)),X1) ),
inference(resolution,[],[f326,f244]) ).
fof(f388,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,complement(X1))
| member(sK0(X0,complement(X1)),X1) ),
inference(duplicate_literal_removal,[],[f372]) ).
fof(f389,plain,
! [X2,X0,X1] :
( ~ member(sK0(X0,intersection(X2,X1)),X2)
| subclass(X0,intersection(X2,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f371]) ).
fof(f392,plain,
! [X0,X1] :
( member(sK0(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(forward_subsumption_resolution,[],[f388,f109]) ).
fof(f414,plain,
( sK4(sK6) = sK4(intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6))
| null_class = intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6)
| null_class = sK6 ),
inference(resolution,[],[f241,f188]) ).
fof(f423,definition,
( spl7_3
<=> null_class = intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f424,plain,
( null_class != intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6)
| spl7_3 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f425,plain,
( null_class = intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6)
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f427,definition,
( spl7_4
<=> sK4(sK6) = sK4(intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6)) ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
fof(f429,plain,
( sK4(sK6) = sK4(intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6))
| ~ spl7_4 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f431,plain,
( sK4(sK6) = sK4(intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6))
| null_class = intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6) ),
inference(forward_subsumption_resolution,[],[f414,f195]) ).
fof(f432,plain,
( spl7_3
| spl7_4 ),
inference(avatar_split_clause,[],[f431,f427,f423]) ).
fof(f449,definition,
( spl7_5
<=> member(sK4(sK6),universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition]) ).
fof(f450,plain,
( ~ member(sK4(sK6),universal_class)
| spl7_5 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f451,plain,
( member(sK4(sK6),universal_class)
| ~ spl7_5 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f475,plain,
! [X0,X1] :
( ~ member(sK4(intersection(complement(X0),X1)),X0)
| null_class = intersection(complement(X0),X1) ),
inference(resolution,[],[f256,f133]) ).
fof(f479,plain,
! [X0] :
( null_class = intersection(sK6,X0)
| ~ member(sK4(intersection(sK6,X0)),universal_class)
| sK4(sK6) = sK4(intersection(sK6,X0)) ),
inference(resolution,[],[f256,f305]) ).
fof(f483,plain,
! [X0] :
( sK4(sK6) = sK4(intersection(sK6,X0))
| null_class = intersection(sK6,X0) ),
inference(forward_subsumption_resolution,[],[f479,f189]) ).
fof(f490,plain,
! [X0,X1] :
( ~ member(sK4(intersection(X0,complement(X1))),X1)
| null_class = intersection(X0,complement(X1)) ),
inference(resolution,[],[f249,f133]) ).
fof(f517,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f389,f107]) ).
fof(f528,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f517]) ).
fof(f599,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f528,f288]) ).
fof(f622,plain,
! [X0] :
( member(sK4(sK6),X0)
| null_class = intersection(sK6,X0)
| null_class = intersection(sK6,X0) ),
inference(superposition,[],[f249,f483]) ).
fof(f623,plain,
! [X0] :
( member(sK4(sK6),sK6)
| null_class = intersection(sK6,X0)
| null_class = intersection(sK6,X0) ),
inference(superposition,[],[f256,f483]) ).
fof(f624,plain,
! [X0] :
( ~ member(sK4(sK6),X0)
| null_class = intersection(sK6,complement(X0))
| null_class = intersection(sK6,complement(X0)) ),
inference(superposition,[],[f490,f483]) ).
fof(f633,plain,
! [X0] :
( ~ member(sK4(sK6),X0)
| null_class = intersection(sK6,complement(X0)) ),
inference(duplicate_literal_removal,[],[f624]) ).
fof(f634,plain,
! [X0] :
( member(sK4(sK6),sK6)
| null_class = intersection(sK6,X0) ),
inference(duplicate_literal_removal,[],[f623]) ).
fof(f635,plain,
! [X0] :
( member(sK4(sK6),X0)
| null_class = intersection(sK6,X0) ),
inference(duplicate_literal_removal,[],[f622]) ).
fof(f641,plain,
! [X0] :
( null_class = intersection(sK6,complement(X0))
| member(sK4(sK6),universal_class) ),
inference(resolution,[],[f635,f134]) ).
fof(f659,plain,
! [X0] :
( null_class = intersection(sK6,complement(unordered_pair(X0,sK4(sK6))))
| ~ member(sK4(sK6),universal_class) ),
inference(resolution,[],[f633,f238]) ).
fof(f660,plain,
( ! [X0] : null_class = intersection(sK6,complement(unordered_pair(X0,sK4(sK6))))
| ~ spl7_5 ),
inference(forward_subsumption_resolution,[],[f659,f451]) ).
fof(f667,plain,
! [X0] : intersection(X0,universal_class) = X0,
inference(resolution,[],[f599,f109]) ).
fof(f675,plain,
! [X0] :
( sK4(sK6) = sK0(sK6,X0)
| sK6 = intersection(sK6,X0) ),
inference(resolution,[],[f599,f311]) ).
fof(f679,plain,
! [X0,X1] :
( ~ member(X1,X0)
| member(X1,universal_class) ),
inference(superposition,[],[f130,f667]) ).
fof(f694,plain,
! [X0] :
( member(sK4(sK6),sK6)
| subclass(sK6,X0)
| sK6 = intersection(sK6,X0) ),
inference(superposition,[],[f107,f675]) ).
fof(f699,plain,
! [X0] :
( member(sK4(sK6),X0)
| subclass(sK6,complement(X0))
| sK6 = intersection(sK6,complement(X0)) ),
inference(superposition,[],[f392,f675]) ).
fof(f702,plain,
! [X0] :
( member(sK4(sK6),X0)
| sK6 = intersection(sK6,complement(X0)) ),
inference(forward_subsumption_resolution,[],[f699,f599]) ).
fof(f745,plain,
! [X0] :
( sK6 = intersection(sK6,complement(complement(X0)))
| member(sK4(sK6),universal_class) ),
inference(resolution,[],[f702,f134]) ).
fof(f1113,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,complement(unordered_pair(sK4(sK6),sK4(sK6))))
| ~ member(X0,sK6) )
| ~ spl7_3 ),
inference(superposition,[],[f132,f425]) ).
fof(f1132,plain,
( ! [X0] :
( ~ member(X0,complement(unordered_pair(sK4(sK6),sK4(sK6))))
| ~ member(X0,sK6) )
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f1113,f137]) ).
fof(f1142,plain,
( ! [X0] :
( ~ member(X0,sK6)
| ~ member(X0,universal_class)
| member(X0,unordered_pair(sK4(sK6),sK4(sK6))) )
| ~ spl7_3 ),
inference(resolution,[],[f1132,f135]) ).
fof(f1149,plain,
( ! [X0] :
( member(X0,unordered_pair(sK4(sK6),sK4(sK6)))
| ~ member(X0,sK6) )
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f1142,f679]) ).
fof(f1180,plain,
( ! [X0] :
( ~ member(sK0(X0,unordered_pair(sK4(sK6),sK4(sK6))),sK6)
| subclass(X0,unordered_pair(sK4(sK6),sK4(sK6))) )
| ~ spl7_3 ),
inference(resolution,[],[f1149,f108]) ).
fof(f1190,plain,
( subclass(sK6,unordered_pair(sK4(sK6),sK4(sK6)))
| subclass(sK6,unordered_pair(sK4(sK6),sK4(sK6)))
| ~ spl7_3 ),
inference(resolution,[],[f1180,f107]) ).
fof(f1200,plain,
( subclass(sK6,unordered_pair(sK4(sK6),sK4(sK6)))
| ~ spl7_3 ),
inference(duplicate_literal_removal,[],[f1190]) ).
fof(f1203,plain,
( ~ subclass(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| sK6 = unordered_pair(sK4(sK6),sK4(sK6))
| ~ spl7_3 ),
inference(resolution,[],[f1200,f112]) ).
fof(f1204,plain,
( ~ subclass(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f1203,f233]) ).
fof(f1205,plain,
( sK4(sK6) = sK0(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| sK4(sK6) = sK0(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| ~ spl7_3 ),
inference(resolution,[],[f1204,f297]) ).
fof(f1206,plain,
( sK4(sK6) = sK0(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| ~ spl7_3 ),
inference(duplicate_literal_removal,[],[f1205]) ).
fof(f1209,plain,
( ~ member(sK4(sK6),sK6)
| subclass(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| ~ spl7_3 ),
inference(superposition,[],[f108,f1206]) ).
fof(f1210,plain,
( subclass(unordered_pair(sK4(sK6),sK4(sK6)),sK6)
| ~ spl7_2
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f1209,f356]) ).
fof(f1213,plain,
( $false
| ~ spl7_2
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f1210,f1204]) ).
fof(f1214,plain,
( ~ spl7_2
| ~ spl7_3 ),
inference(avatar_contradiction_clause,[],[f1213]) ).
fof(f1215,plain,
( ! [X0] : null_class = intersection(sK6,X0)
| spl7_2 ),
inference(forward_subsumption_resolution,[],[f634,f355]) ).
fof(f1216,plain,
! [X0] :
( member(sK4(sK6),sK6)
| sK6 = intersection(sK6,X0) ),
inference(forward_subsumption_resolution,[],[f694,f599]) ).
fof(f1223,plain,
( ! [X0] : sK6 = intersection(sK6,X0)
| spl7_2 ),
inference(forward_subsumption_resolution,[],[f1216,f355]) ).
fof(f1228,plain,
( null_class = sK6
| spl7_2 ),
inference(forward_demodulation,[],[f1223,f1215]) ).
fof(f1229,plain,
( $false
| spl7_2 ),
inference(forward_subsumption_resolution,[],[f1228,f195]) ).
fof(f1230,plain,
spl7_2,
inference(avatar_contradiction_clause,[],[f1229]) ).
fof(f3693,plain,
( ~ member(sK4(sK6),unordered_pair(sK4(sK6),sK4(sK6)))
| null_class = intersection(complement(unordered_pair(sK4(sK6),sK4(sK6))),sK6)
| ~ spl7_4 ),
inference(superposition,[],[f475,f429]) ).
fof(f3705,plain,
( ~ member(sK4(sK6),unordered_pair(sK4(sK6),sK4(sK6)))
| spl7_3
| ~ spl7_4 ),
inference(forward_subsumption_resolution,[],[f3693,f424]) ).
fof(f3707,plain,
( sK6 = intersection(sK6,complement(unordered_pair(sK4(sK6),sK4(sK6))))
| spl7_3
| ~ spl7_4 ),
inference(resolution,[],[f3705,f702]) ).
fof(f3722,plain,
( null_class = sK6
| spl7_3
| ~ spl7_4
| ~ spl7_5 ),
inference(forward_demodulation,[],[f3707,f660]) ).
fof(f3725,plain,
( $false
| spl7_3
| ~ spl7_4
| ~ spl7_5 ),
inference(forward_subsumption_resolution,[],[f3722,f195]) ).
fof(f3726,plain,
( spl7_3
| ~ spl7_4
| ~ spl7_5 ),
inference(avatar_contradiction_clause,[],[f3725]) ).
fof(f3728,plain,
( ! [X0] : null_class = intersection(sK6,complement(X0))
| spl7_5 ),
inference(forward_subsumption_resolution,[],[f641,f450]) ).
fof(f3729,plain,
( ! [X0] : sK6 = intersection(sK6,complement(complement(X0)))
| spl7_5 ),
inference(forward_subsumption_resolution,[],[f745,f450]) ).
fof(f3746,plain,
( null_class = sK6
| spl7_5 ),
inference(forward_demodulation,[],[f3729,f3728]) ).
fof(f3754,plain,
( $false
| spl7_5 ),
inference(forward_subsumption_resolution,[],[f3746,f195]) ).
fof(f3755,plain,
spl7_5,
inference(avatar_contradiction_clause,[],[f3754]) ).
cnf(s3,plain,
( spl7_3
| spl7_4 ),
inference(sat_conversion,[],[f432]) ).
cnf(s20,plain,
( ~ spl7_2
| ~ spl7_3 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s24,plain,
spl7_2,
inference(sat_conversion,[],[f1230]) ).
cnf(s167,plain,
( spl7_3
| ~ spl7_4
| ~ spl7_5 ),
inference(sat_conversion,[],[f3726]) ).
cnf(s176,plain,
spl7_5,
inference(sat_conversion,[],[f3755]) ).
cnf(s177,plain,
( spl7_3
| ~ spl7_4 ),
inference(rat,[],[s167,s176]) ).
cnf(s214,plain,
~ spl7_3,
inference(rat,[],[s20,s24]) ).
cnf(s215,plain,
~ spl7_4,
inference(rat,[],[s177,s214]) ).
cnf(s231,plain,
$false,
inference(rat,[],[s3,s215,s214]) ).
fof(f3756,plain,
$false,
inference(avatar_sat_refutation,[],[s231]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET099+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 00:41:02 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.62/2.39 % (329473)Detected formulas, will run a generic FOF schedule.
% 10.62/2.39 % (329484)dis-21_1_sil=8000:lcm=predicate:random_seed=1178032529:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.62/2.39 % (329482)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1296347544:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.62/2.39 % (329481)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1783849736:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.62/2.39 % (329480)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3947673228:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.62/2.39 % (329478)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=3191735411:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.62/2.39 % (329479)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4054659079:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.62/2.39 % (329483)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1228486634:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.62/2.39 % (329481)Refutation not found, incomplete strategy
% 10.62/2.39 % (329481)------------------------------
% 10.62/2.39 % (329481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.39 % (329481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.39 % (329481)CaDiCaL version: 2.1.3
% 10.62/2.39 % (329481)Termination reason: Refutation not found, incomplete strategy
% 10.62/2.39 % (329481)Time elapsed: 0.001 s
% 10.62/2.39 % (329481)Peak memory usage: 88 MB
% 10.62/2.39 % (329481)Instructions burned: 1 (million)
% 10.62/2.39 % (329484)Instruction limit reached!
% 10.62/2.39 % (329484)------------------------------
% 10.62/2.39 % (329484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.39 % (329484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.39 % (329484)CaDiCaL version: 2.1.3
% 10.62/2.39 % (329484)Termination reason: Instruction limit
% 10.62/2.39 % (329484)Termination phase: Saturation
% 10.62/2.39 % (329484)Time elapsed: 0.042 s
% 10.62/2.39 % (329484)Peak memory usage: 89 MB
% 10.62/2.39 % (329484)Instructions burned: 131 (million)
% 10.62/2.39 % (329482)Instruction limit reached!
% 10.62/2.39 % (329482)------------------------------
% 10.62/2.39 % (329482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.39 % (329482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.39 % (329482)CaDiCaL version: 2.1.3
% 10.62/2.39 % (329482)Termination reason: Instruction limit
% 10.62/2.39 % (329482)Termination phase: Saturation
% 10.62/2.39 % (329482)Time elapsed: 0.076 s
% 10.62/2.39 % (329482)Peak memory usage: 88 MB
% 10.62/2.39 % (329482)Instructions burned: 121 (million)
% 10.62/2.39 % (329492)lrs+10_1_sil=8000:sp=occurrence:random_seed=1245634313:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.62/2.39 % (329483)Instruction limit reached!
% 10.62/2.39 % (329483)------------------------------
% 10.62/2.39 % (329483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.39 % (329483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.39 % (329483)CaDiCaL version: 2.1.3
% 10.62/2.39 % (329483)Termination reason: Instruction limit
% 10.62/2.39 % (329483)Termination phase: Saturation
% 10.62/2.39 % (329483)Time elapsed: 0.106 s
% 10.62/2.39 % (329483)Peak memory usage: 90 MB
% 10.62/2.39 % (329483)Instructions burned: 139 (million)
% 10.62/2.39 % (329492)Instruction limit reached!
% 10.62/2.39 % (329492)------------------------------
% 10.62/2.39 % (329492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.62/2.39 % (329492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.62/2.39 % (329492)CaDiCaL version: 2.1.3
% 10.62/2.39 % (329492)Termination reason: Instruction limit
% 10.62/2.39 % (329492)Termination phase: Saturation
% 10.62/2.39 % (329492)Time elapsed: 0.100 s
% 10.62/2.39 % (329492)Peak memory usage: 92 MB
% 10.62/2.39 % (329492)Instructions burned: 289 (million)
% 10.62/2.39 % (329493)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1955102807:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.38/2.66 % (329495)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3324286464:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.38/2.66 % (329481)------------------------------
% 12.38/2.66 % (329481)------------------------------
% 12.38/2.66 % (329493)Instruction limit reached!
% 12.38/2.66 % (329493)------------------------------
% 12.38/2.66 % (329493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329493)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329493)Termination reason: Instruction limit
% 12.38/2.66 % (329493)Termination phase: Saturation
% 12.38/2.66 % (329493)Time elapsed: 0.078 s
% 12.38/2.66 % (329493)Peak memory usage: 90 MB
% 12.38/2.66 % (329493)Instructions burned: 157 (million)
% 12.38/2.66 % (329496)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3710794542:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 12.38/2.66 % (329496)Instruction limit reached!
% 12.38/2.66 % (329496)------------------------------
% 12.38/2.66 % (329496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329496)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329496)Termination reason: Instruction limit
% 12.38/2.66 % (329496)Termination phase: Saturation
% 12.38/2.66 % (329496)Time elapsed: 0.080 s
% 12.38/2.66 % (329496)Peak memory usage: 92 MB
% 12.38/2.66 % (329496)Instructions burned: 251 (million)
% 12.38/2.66 % (329499)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2327505572:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 12.38/2.66 % (329501)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2807653831:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 12.38/2.66 % (329495)Instruction limit reached!
% 12.38/2.66 % (329495)------------------------------
% 12.38/2.66 % (329495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329495)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329495)Termination reason: Instruction limit
% 12.38/2.66 % (329495)Termination phase: Saturation
% 12.38/2.66 % (329495)Time elapsed: 0.220 s
% 12.38/2.66 % (329495)Peak memory usage: 92 MB
% 12.38/2.66 % (329502)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1982172607:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 12.38/2.66 % (329495)Instructions burned: 326 (million)
% 12.38/2.66 % (329502)Instruction limit reached!
% 12.38/2.66 % (329502)------------------------------
% 12.38/2.66 % (329502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329502)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329502)Termination reason: Instruction limit
% 12.38/2.66 % (329502)Termination phase: Saturation
% 12.38/2.66 % (329502)Time elapsed: 0.042 s
% 12.38/2.66 % (329502)Peak memory usage: 89 MB
% 12.38/2.66 % (329502)Instructions burned: 116 (million)
% 12.38/2.66 % (329499)Instruction limit reached!
% 12.38/2.66 % (329499)------------------------------
% 12.38/2.66 % (329499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329499)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329499)Termination reason: Instruction limit
% 12.38/2.66 % (329499)Termination phase: Saturation
% 12.38/2.66 % (329499)Time elapsed: 0.183 s
% 12.38/2.66 % (329499)Peak memory usage: 89 MB
% 12.38/2.66 % (329499)Instructions burned: 295 (million)
% 12.38/2.66 % (329506)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2793184316:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 12.38/2.66 % (329507)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2980119514:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 12.38/2.66 % (329507)Instruction limit reached!
% 12.38/2.66 % (329507)------------------------------
% 12.38/2.66 % (329507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329507)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329507)Termination reason: Instruction limit
% 12.38/2.66 % (329507)Termination phase: Saturation
% 12.38/2.66 % (329507)Time elapsed: 0.037 s
% 12.38/2.66 % (329507)Peak memory usage: 89 MB
% 12.38/2.66 % (329507)Instructions burned: 116 (million)
% 12.38/2.66 % (329506)Instruction limit reached!
% 12.38/2.66 % (329506)------------------------------
% 12.38/2.66 % (329506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329506)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329506)Termination reason: Instruction limit
% 12.38/2.66 % (329506)Termination phase: Saturation
% 12.38/2.66 % (329506)Time elapsed: 0.070 s
% 12.38/2.66 % (329506)Peak memory usage: 89 MB
% 12.38/2.66 % (329506)Instructions burned: 128 (million)
% 12.38/2.66 % (329511)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3777215902:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 12.38/2.66 % (329511)Refutation not found, incomplete strategy
% 12.38/2.66 % (329511)------------------------------
% 12.38/2.66 % (329511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329511)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329511)Termination reason: Refutation not found, incomplete strategy
% 12.38/2.66 % (329511)Time elapsed: 0.001 s
% 12.38/2.66 % (329511)Peak memory usage: 88 MB
% 12.38/2.66 % (329511)Instructions burned: 1 (million)
% 12.38/2.66 % (329509)lrs+10_1_sil=8000:sp=occurrence:random_seed=428398945:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 12.38/2.66 % (329512)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2326617211:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 12.38/2.66 % (329511)------------------------------
% 12.38/2.66 % (329511)------------------------------
% 12.38/2.66 % (329516)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2805860556:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 12.38/2.66 % (329516)Instruction limit reached!
% 12.38/2.66 % (329516)------------------------------
% 12.38/2.66 % (329516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329516)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329516)Termination reason: Instruction limit
% 12.38/2.66 % (329516)Termination phase: Saturation
% 12.38/2.66 % (329516)Time elapsed: 0.041 s
% 12.38/2.66 % (329516)Peak memory usage: 90 MB
% 12.38/2.66 % (329516)Instructions burned: 136 (million)
% 12.38/2.66 % (329518)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=476248958:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 12.38/2.66 % (329509)Instruction limit reached!
% 12.38/2.66 % (329509)------------------------------
% 12.38/2.66 % (329509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329509)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329509)Termination reason: Instruction limit
% 12.38/2.66 % (329509)Termination phase: Saturation
% 12.38/2.66 % (329509)Time elapsed: 0.552 s
% 12.38/2.66 % (329509)Peak memory usage: 98 MB
% 12.38/2.66 % (329509)Instructions burned: 908 (million)
% 12.38/2.66 % (329518)Instruction limit reached!
% 12.38/2.66 % (329518)------------------------------
% 12.38/2.66 % (329518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329518)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329518)Termination reason: Instruction limit
% 12.38/2.66 % (329518)Termination phase: Saturation
% 12.38/2.66 % (329518)Time elapsed: 0.190 s
% 12.38/2.66 % (329518)Peak memory usage: 93 MB
% 12.38/2.66 % (329518)Instructions burned: 595 (million)
% 12.38/2.66 % (329521)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=120986363:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 12.38/2.66 % (329521)Instruction limit reached!
% 12.38/2.66 % (329521)------------------------------
% 12.38/2.66 % (329521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329521)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329521)Termination reason: Instruction limit
% 12.38/2.66 % (329521)Termination phase: Saturation
% 12.38/2.66 % (329521)Time elapsed: 0.041 s
% 12.38/2.66 % (329521)Peak memory usage: 91 MB
% 12.38/2.66 % (329521)Instructions burned: 127 (million)
% 12.38/2.66 % (329501)First to succeed.
% 12.38/2.66 % (329520)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2907509872:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 12.38/2.66 % (329501)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-329473"
% 12.38/2.66 % (329523)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2694587046:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 12.38/2.66 % (329523)Instruction limit reached!
% 12.38/2.66 % (329523)------------------------------
% 12.38/2.66 % (329523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329523)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329523)Termination reason: Instruction limit
% 12.38/2.66 % (329523)Termination phase: Saturation
% 12.38/2.66 % (329523)Time elapsed: 0.046 s
% 12.38/2.66 % (329523)Peak memory usage: 90 MB
% 12.38/2.66 % (329523)Instructions burned: 134 (million)
% 12.38/2.66 % (329526)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4124325248:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 12.38/2.66 % (329526)Refutation not found, incomplete strategy
% 12.38/2.66 % (329526)------------------------------
% 12.38/2.66 % (329526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.38/2.66 % (329526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.38/2.66 % (329526)CaDiCaL version: 2.1.3
% 12.38/2.66 % (329526)Termination reason: Refutation not found, incomplete strategy
% 12.38/2.66 % (329526)Time elapsed: 0.001 s
% 12.38/2.66 % (329526)Peak memory usage: 88 MB
% 12.38/2.66 % (329526)Instructions burned: 2 (million)
% 12.38/2.66 % (329501)Refutation found. Thanks to Tanya!
% 12.38/2.66 % SZS status Theorem for theBenchmark
% 12.38/2.66 % SZS output start Proof for theBenchmark
% See solution above
% 13.39/2.86 % (329501)------------------------------
% 13.39/2.86 % (329501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.39/2.86 % (329501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.39/2.86 % (329501)CaDiCaL version: 2.1.3
% 13.39/2.86 % (329501)Termination reason: Refutation
% 13.39/2.86 % (329501)Time elapsed: 0.999 s
% 13.39/2.86 % (329501)Peak memory usage: 134 MB
% 13.39/2.86 % (329501)Instructions burned: 1491 (million)
% 13.39/2.86 % (329501)------------------------------
% 13.39/2.86 % (329501)------------------------------
% 13.39/2.86 % (329473)Success in time 1.811 s
% 13.39/2.86 % Vampire exiting
%------------------------------------------------------------------------------