%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET100-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:07 PM UTC 2026
% Result : Unsatisfiable 8.67s 2.10s
% Output : Refutation 9.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 57
% Syntax : Number of formulae : 339 ( 33 unt; 29 def)
% Number of atoms : 876 ( 121 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 873 ( 336 ~; 515 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 11 con; 0-2 aty)
% Number of variables : 122 ( 0 sgn 122 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
fof(f105,axiom,
! [X0] : subclass(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_is_reflexive) ).
fof(f107,axiom,
! [X0,X1] :
( member(not_subclass_element(X1,X0),X1)
| member(not_subclass_element(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equality1) ).
fof(f109,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| X1 = X0
| member(not_subclass_element(X1,X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equality3) ).
fof(f110,plain,
! [X0,X1] :
( member(not_subclass_element(X1,X0),X1)
| X0 = X1
| ~ member(not_subclass_element(X0,X1),X1) ),
inference(reorient_equations,[],[f109]) ).
fof(f111,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X1,X0),X0)
| ~ member(not_subclass_element(X0,X1),X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equality4) ).
fof(f113,axiom,
! [X0] : ~ member(X0,null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_of_null_class) ).
fof(f115,axiom,
! [X0] :
( ~ subclass(X0,null_class)
| X0 = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',corollary_of_null_class_is_subclass) ).
fof(f116,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(reorient_equations,[],[f115]) ).
fof(f117,axiom,
! [X0] :
( X0 = null_class
| member(not_subclass_element(X0,null_class),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',null_class_is_unique) ).
fof(f118,plain,
! [X0] :
( member(not_subclass_element(X0,null_class),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f117]) ).
fof(f123,axiom,
! [X0,X1] :
( member(X0,universal_class)
| unordered_pair(X1,X0) = singleton(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_equals_singleton1) ).
fof(f124,axiom,
! [X0,X1] :
( member(X0,universal_class)
| unordered_pair(X0,X1) = singleton(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_equals_singleton2) ).
fof(f131,axiom,
! [X2,X0,X1] :
( subclass(unordered_pair(X0,X2),X1)
| ~ member(X2,X1)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_is_subset) ).
fof(f137,axiom,
! [X0,X1] :
( ~ member(X0,singleton(X1))
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',only_member_in_singleton) ).
fof(f138,axiom,
! [X0] :
( member(X0,universal_class)
| singleton(X0) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_is_null_class) ).
fof(f162,negated_conjecture,
unordered_pair(x,y) != union(singleton(x),singleton(y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_unordered_pairs_and_singletons_1) ).
fof(f217,plain,
! [X0,X1] :
( unordered_pair(X1,X0) = unordered_pair(X1,X1)
| member(X0,universal_class) ),
inference(definition_unfolding,[],[f123,f12]) ).
fof(f218,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = unordered_pair(X1,X1)
| member(X0,universal_class) ),
inference(definition_unfolding,[],[f124,f12]) ).
fof(f227,plain,
! [X0,X1] :
( ~ member(X0,unordered_pair(X1,X1))
| X0 = X1 ),
inference(definition_unfolding,[],[f137,f12]) ).
fof(f228,plain,
! [X0] :
( unordered_pair(X0,X0) = null_class
| member(X0,universal_class) ),
inference(definition_unfolding,[],[f138,f12]) ).
fof(f244,plain,
unordered_pair(x,y) != complement(intersection(complement(unordered_pair(x,x)),complement(unordered_pair(y,y)))),
inference(definition_unfolding,[],[f162,f26,f12,f12]) ).
fof(f248,definition,
sF0 = unordered_pair(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f249,plain,
unordered_pair(x,y) = sF0,
inference(reorient_equations,[],[f248]) ).
fof(f250,definition,
sF1 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f251,plain,
unordered_pair(x,x) = sF1,
inference(reorient_equations,[],[f250]) ).
fof(f252,definition,
sF2 = complement(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f253,plain,
complement(sF1) = sF2,
inference(reorient_equations,[],[f252]) ).
fof(f254,definition,
sF3 = unordered_pair(y,y),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f255,plain,
unordered_pair(y,y) = sF3,
inference(reorient_equations,[],[f254]) ).
fof(f256,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f257,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f256]) ).
fof(f258,definition,
sF5 = intersection(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f259,plain,
intersection(sF2,sF4) = sF5,
inference(reorient_equations,[],[f258]) ).
fof(f260,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f261,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f260]) ).
fof(f262,plain,
sF0 != sF6,
inference(definition_folding,[],[f244,f261,f259,f257,f255,f253,f251,f249]) ).
fof(f263,plain,
( member(x,sF0)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f249]) ).
fof(f264,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f251]) ).
fof(f265,plain,
( member(y,sF3)
| ~ member(y,universal_class) ),
inference(superposition,[],[f9,f255]) ).
fof(f267,definition,
( spl7_1
<=> member(y,universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition]) ).
fof(f268,plain,
( member(y,universal_class)
| ~ spl7_1 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f269,plain,
( ~ member(y,universal_class)
| spl7_1 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl7_2
<=> member(y,sF3) ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f273,plain,
( member(y,sF3)
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( ~ spl7_1
| spl7_2 ),
inference(avatar_split_clause,[],[f265,f271,f267]) ).
fof(f276,definition,
( spl7_3
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f278,plain,
( ~ member(x,universal_class)
| spl7_3 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f280,definition,
( spl7_4
<=> member(x,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
fof(f282,plain,
( member(x,sF1)
| ~ spl7_4 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,plain,
( ~ spl7_3
| spl7_4 ),
inference(avatar_split_clause,[],[f264,f280,f276]) ).
fof(f285,definition,
( spl7_5
<=> member(x,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition]) ).
fof(f287,plain,
( member(x,sF0)
| ~ spl7_5 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,plain,
( ~ spl7_3
| spl7_5 ),
inference(avatar_split_clause,[],[f263,f285,f276]) ).
fof(f290,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0 ),
inference(superposition,[],[f227,f251]) ).
fof(f291,plain,
! [X0] :
( ~ member(X0,sF3)
| y = X0 ),
inference(superposition,[],[f227,f255]) ).
fof(f293,plain,
( member(y,sF0)
| ~ member(y,universal_class) ),
inference(superposition,[],[f10,f249]) ).
fof(f299,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,sF5) ),
inference(superposition,[],[f24,f261]) ).
fof(f300,plain,
! [X0] :
( ~ member(X0,sF2)
| ~ member(X0,sF1) ),
inference(superposition,[],[f24,f253]) ).
fof(f301,plain,
! [X0] :
( ~ member(X0,sF4)
| ~ member(X0,sF3) ),
inference(superposition,[],[f24,f257]) ).
fof(f305,plain,
! [X0] :
( ~ member(X0,sF0)
| x = X0
| y = X0 ),
inference(superposition,[],[f8,f249]) ).
fof(f312,plain,
! [X0] :
( member(X0,sF6)
| ~ member(X0,universal_class)
| member(X0,sF5) ),
inference(superposition,[],[f25,f261]) ).
fof(f313,plain,
! [X0] :
( member(X0,sF2)
| ~ member(X0,universal_class)
| member(X0,sF1) ),
inference(superposition,[],[f25,f253]) ).
fof(f314,plain,
! [X0] :
( member(X0,sF4)
| ~ member(X0,universal_class)
| member(X0,sF3) ),
inference(superposition,[],[f25,f257]) ).
fof(f316,plain,
! [X0] :
( member(X0,sF2)
| ~ member(X0,sF5) ),
inference(superposition,[],[f21,f259]) ).
fof(f317,plain,
! [X0] :
( member(X0,sF4)
| ~ member(X0,sF5) ),
inference(superposition,[],[f22,f259]) ).
fof(f325,plain,
! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF3) ),
inference(resolution,[],[f301,f317]) ).
fof(f326,plain,
! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF1) ),
inference(resolution,[],[f316,f300]) ).
fof(f334,plain,
( null_class = sF1
| member(x,universal_class) ),
inference(superposition,[],[f251,f228]) ).
fof(f335,plain,
( null_class = sF3
| member(y,universal_class) ),
inference(superposition,[],[f255,f228]) ).
fof(f342,plain,
( null_class = sF3
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f335,f269]) ).
fof(f343,plain,
( null_class = sF1
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f334,f278]) ).
fof(f347,plain,
( sF4 = complement(null_class)
| spl7_1 ),
inference(backward_demodulation,[],[f257,f342]) ).
fof(f353,plain,
( null_class = unordered_pair(x,x)
| spl7_3 ),
inference(backward_demodulation,[],[f251,f343]) ).
fof(f354,plain,
( sF2 = complement(null_class)
| spl7_3 ),
inference(backward_demodulation,[],[f253,f343]) ).
fof(f357,plain,
( ! [X0] :
( member(X0,null_class)
| member(X0,sF2)
| ~ member(X0,universal_class) )
| spl7_3 ),
inference(backward_demodulation,[],[f313,f343]) ).
fof(f361,plain,
( ! [X0] :
( member(X0,sF2)
| ~ member(X0,universal_class) )
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f357,f113]) ).
fof(f362,plain,
( sF2 = sF4
| spl7_1
| spl7_3 ),
inference(backward_demodulation,[],[f347,f354]) ).
fof(f366,plain,
( sF5 = intersection(sF2,sF2)
| spl7_1
| spl7_3 ),
inference(backward_demodulation,[],[f259,f362]) ).
fof(f406,definition,
( spl7_7
<=> null_class = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition]) ).
fof(f407,plain,
( null_class != sF6
| spl7_7 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f419,definition,
( spl7_10
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl7_10])],[avatar_definition]) ).
fof(f421,plain,
( null_class = sF0
| ~ spl7_10 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f435,plain,
( ! [X0] :
( member(X0,sF5)
| ~ member(X0,sF2)
| ~ member(X0,sF2) )
| spl7_1
| spl7_3 ),
inference(superposition,[],[f23,f366]) ).
fof(f438,plain,
( ! [X0] :
( member(X0,sF5)
| ~ member(X0,sF2) )
| spl7_1
| spl7_3 ),
inference(duplicate_literal_removal,[],[f435]) ).
fof(f452,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF0),sF0)
| sF0 = X0
| x = not_subclass_element(sF0,X0)
| y = not_subclass_element(sF0,X0) ),
inference(resolution,[],[f110,f305]) ).
fof(f453,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF5)
| ~ member(not_subclass_element(X0,sF6),sF6)
| sF6 = X0 ),
inference(resolution,[],[f110,f299]) ).
fof(f502,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF5)
| subclass(sF6,X0) ),
inference(resolution,[],[f2,f299]) ).
fof(f503,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF2)
| subclass(sF6,X0) )
| spl7_1
| spl7_3 ),
inference(resolution,[],[f502,f438]) ).
fof(f508,plain,
! [X2,X0,X1] :
( ~ subclass(X1,unordered_pair(X2,X0))
| ~ member(X2,X1)
| ~ member(X0,X1)
| unordered_pair(X2,X0) = X1 ),
inference(resolution,[],[f131,f7]) ).
fof(f596,plain,
( unordered_pair(x,x) = sF0
| member(y,universal_class) ),
inference(superposition,[],[f249,f217]) ).
fof(f631,plain,
( unordered_pair(x,x) = sF0
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f596,f269]) ).
fof(f633,plain,
( null_class = sF0
| spl7_1
| spl7_3 ),
inference(forward_demodulation,[],[f631,f353]) ).
fof(f635,plain,
( spl7_10
| spl7_1
| spl7_3 ),
inference(avatar_split_clause,[],[f633,f276,f267,f419]) ).
fof(f637,plain,
( null_class != sF6
| ~ spl7_10 ),
inference(backward_demodulation,[],[f262,f421]) ).
fof(f650,plain,
( ~ spl7_7
| ~ spl7_10 ),
inference(avatar_split_clause,[],[f637,f419,f406]) ).
fof(f695,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF6,X0),universal_class)
| subclass(sF6,X0) )
| spl7_1
| spl7_3 ),
inference(resolution,[],[f503,f361]) ).
fof(f786,plain,
( ! [X0,X1] :
( subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),X1)
| ~ subclass(X1,universal_class) )
| spl7_1
| spl7_3 ),
inference(resolution,[],[f695,f1]) ).
fof(f787,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF6,X0),X1)
| subclass(sF6,X0) )
| spl7_1
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f786,f4]) ).
fof(f791,plain,
( subclass(sF6,null_class)
| null_class = sF6
| spl7_1
| spl7_3 ),
inference(resolution,[],[f787,f118]) ).
fof(f806,plain,
( null_class = sF6
| spl7_1
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f791,f116]) ).
fof(f807,plain,
( $false
| spl7_1
| spl7_3
| spl7_7 ),
inference(forward_subsumption_resolution,[],[f806,f407]) ).
fof(f808,plain,
( spl7_1
| spl7_3
| spl7_7 ),
inference(avatar_contradiction_clause,[],[f807]) ).
fof(f814,plain,
( member(y,sF0)
| ~ spl7_1 ),
inference(forward_subsumption_resolution,[],[f293,f268]) ).
fof(f879,plain,
! [X0] :
( ~ subclass(X0,sF3)
| ~ member(y,X0)
| ~ member(y,X0)
| sF3 = X0 ),
inference(superposition,[],[f508,f255]) ).
fof(f885,plain,
! [X0] :
( sF3 = unordered_pair(X0,y)
| member(X0,universal_class) ),
inference(superposition,[],[f218,f255]) ).
fof(f897,plain,
! [X0] :
( ~ subclass(X0,sF3)
| ~ member(y,X0)
| sF3 = X0 ),
inference(duplicate_literal_removal,[],[f879]) ).
fof(f936,plain,
! [X0] :
( member(X0,sF5)
| ~ member(X0,sF4)
| ~ member(X0,sF2) ),
inference(superposition,[],[f23,f259]) ).
fof(f976,plain,
! [X0] :
( y = not_subclass_element(sF3,X0)
| subclass(sF3,X0) ),
inference(resolution,[],[f291,f2]) ).
fof(f1064,plain,
( sF0 = sF3
| member(x,universal_class) ),
inference(superposition,[],[f249,f885]) ).
fof(f1069,plain,
( sF0 = sF3
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1064,f278]) ).
fof(f1077,plain,
( ! [X0] :
( member(X0,sF4)
| member(X0,sF0)
| ~ member(X0,universal_class) )
| spl7_3 ),
inference(backward_demodulation,[],[f314,f1069]) ).
fof(f1078,plain,
( ! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF0) )
| spl7_3 ),
inference(backward_demodulation,[],[f325,f1069]) ).
fof(f1086,plain,
( ! [X0] :
( ~ subclass(X0,sF0)
| ~ member(y,X0)
| sF3 = X0 )
| spl7_3 ),
inference(backward_demodulation,[],[f897,f1069]) ).
fof(f1106,plain,
( ! [X0] :
( subclass(sF0,X0)
| y = not_subclass_element(sF3,X0) )
| spl7_3 ),
inference(backward_demodulation,[],[f976,f1069]) ).
fof(f1113,plain,
( ! [X0] :
( y = not_subclass_element(sF0,X0)
| subclass(sF0,X0) )
| spl7_3 ),
inference(forward_demodulation,[],[f1106,f1069]) ).
fof(f1115,plain,
( ! [X0] :
( ~ member(y,X0)
| ~ subclass(X0,sF0)
| sF0 = X0 )
| spl7_3 ),
inference(forward_demodulation,[],[f1086,f1069]) ).
fof(f1280,definition,
( spl7_27
<=> member(y,sF5) ),
introduced(definition,[new_symbols(definition,[spl7_27])],[avatar_definition]) ).
fof(f1281,plain,
( member(y,sF5)
| ~ spl7_27 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1282,plain,
( ~ member(y,sF5)
| spl7_27 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1379,plain,
( ~ member(y,universal_class)
| member(y,sF5)
| ~ subclass(sF6,sF0)
| sF0 = sF6
| spl7_3 ),
inference(resolution,[],[f312,f1115]) ).
fof(f1380,plain,
( member(y,sF5)
| ~ subclass(sF6,sF0)
| sF0 = sF6
| ~ spl7_1
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1379,f268]) ).
fof(f1382,plain,
( ~ subclass(sF6,sF0)
| sF0 = sF6
| ~ spl7_1
| spl7_3
| spl7_27 ),
inference(forward_subsumption_resolution,[],[f1380,f1282]) ).
fof(f1384,plain,
( ~ subclass(sF6,sF0)
| ~ spl7_1
| spl7_3
| spl7_27 ),
inference(forward_subsumption_resolution,[],[f1382,f262]) ).
fof(f1385,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF4)
| sF6 = X0
| ~ member(not_subclass_element(X0,sF6),sF6)
| ~ member(not_subclass_element(sF6,X0),sF2) ),
inference(resolution,[],[f453,f936]) ).
fof(f1387,plain,
( ! [X0] :
( sF6 = X0
| ~ member(not_subclass_element(X0,sF6),sF6)
| ~ member(not_subclass_element(sF6,X0),sF2)
| member(not_subclass_element(sF6,X0),sF0)
| ~ member(not_subclass_element(sF6,X0),universal_class) )
| spl7_3 ),
inference(resolution,[],[f1385,f1077]) ).
fof(f1391,plain,
( ! [X0] :
( member(not_subclass_element(sF6,X0),sF0)
| ~ member(not_subclass_element(X0,sF6),sF6)
| sF6 = X0
| ~ member(not_subclass_element(sF6,X0),universal_class) )
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1387,f361]) ).
fof(f1396,plain,
( ~ member(not_subclass_element(sF0,sF6),sF6)
| sF0 = sF6
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| ~ member(not_subclass_element(sF0,sF6),sF6)
| sF0 = sF6
| spl7_3 ),
inference(resolution,[],[f1391,f111]) ).
fof(f1399,plain,
( ~ member(not_subclass_element(sF0,sF6),sF6)
| sF0 = sF6
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| spl7_3 ),
inference(duplicate_literal_removal,[],[f1396]) ).
fof(f1402,plain,
( ~ member(not_subclass_element(sF0,sF6),sF6)
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1399,f262]) ).
fof(f1407,definition,
( spl7_32
<=> member(not_subclass_element(sF6,sF0),universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_32])],[avatar_definition]) ).
fof(f1408,plain,
( member(not_subclass_element(sF6,sF0),universal_class)
| ~ spl7_32 ),
inference(avatar_component_clause,[],[f1407]) ).
fof(f1409,plain,
( ~ member(not_subclass_element(sF6,sF0),universal_class)
| spl7_32 ),
inference(avatar_component_clause,[],[f1407]) ).
fof(f1411,definition,
( spl7_33
<=> member(not_subclass_element(sF0,sF6),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_33])],[avatar_definition]) ).
fof(f1412,plain,
( member(not_subclass_element(sF0,sF6),sF6)
| ~ spl7_33 ),
inference(avatar_component_clause,[],[f1411]) ).
fof(f1413,plain,
( ~ member(not_subclass_element(sF0,sF6),sF6)
| spl7_33 ),
inference(avatar_component_clause,[],[f1411]) ).
fof(f1414,plain,
( ~ spl7_32
| ~ spl7_33
| spl7_3 ),
inference(avatar_split_clause,[],[f1402,f276,f1411,f1407]) ).
fof(f1417,definition,
( spl7_34
<=> y = not_subclass_element(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_34])],[avatar_definition]) ).
fof(f1418,plain,
( y != not_subclass_element(sF0,sF6)
| spl7_34 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1419,plain,
( y = not_subclass_element(sF0,sF6)
| ~ spl7_34 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1422,definition,
( spl7_35
<=> x = not_subclass_element(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_35])],[avatar_definition]) ).
fof(f1423,plain,
( x != not_subclass_element(sF0,sF6)
| spl7_35 ),
inference(avatar_component_clause,[],[f1422]) ).
fof(f1424,plain,
( x = not_subclass_element(sF0,sF6)
| ~ spl7_35 ),
inference(avatar_component_clause,[],[f1422]) ).
fof(f1427,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF6,sF0),X0)
| ~ subclass(X0,universal_class) )
| spl7_32 ),
inference(resolution,[],[f1409,f1]) ).
fof(f1428,plain,
( ! [X0] : ~ member(not_subclass_element(sF6,sF0),X0)
| spl7_32 ),
inference(forward_subsumption_resolution,[],[f1427,f4]) ).
fof(f1429,plain,
( subclass(sF6,sF0)
| spl7_32 ),
inference(resolution,[],[f1428,f2]) ).
fof(f1430,plain,
( sF0 = sF6
| ~ member(not_subclass_element(sF0,sF6),sF6)
| spl7_32 ),
inference(resolution,[],[f1428,f110]) ).
fof(f1446,plain,
( ~ member(not_subclass_element(sF0,sF6),sF6)
| spl7_32 ),
inference(forward_subsumption_resolution,[],[f1430,f262]) ).
fof(f1447,plain,
( $false
| ~ spl7_1
| spl7_3
| spl7_27
| spl7_32 ),
inference(forward_subsumption_resolution,[],[f1429,f1384]) ).
fof(f1448,plain,
( ~ spl7_1
| spl7_3
| spl7_27
| spl7_32 ),
inference(avatar_contradiction_clause,[],[f1447]) ).
fof(f1449,plain,
( ~ spl7_33
| spl7_32 ),
inference(avatar_split_clause,[],[f1446,f1407,f1411]) ).
fof(f1450,plain,
( ~ member(not_subclass_element(sF0,sF6),universal_class)
| member(not_subclass_element(sF0,sF6),sF5)
| spl7_33 ),
inference(resolution,[],[f1413,f312]) ).
fof(f1454,definition,
( spl7_36
<=> member(not_subclass_element(sF0,sF6),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_36])],[avatar_definition]) ).
fof(f1455,plain,
( ~ member(not_subclass_element(sF0,sF6),sF5)
| spl7_36 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1456,plain,
( member(not_subclass_element(sF0,sF6),sF5)
| ~ spl7_36 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1458,definition,
( spl7_37
<=> member(not_subclass_element(sF0,sF6),universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_37])],[avatar_definition]) ).
fof(f1459,plain,
( member(not_subclass_element(sF0,sF6),universal_class)
| ~ spl7_37 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1460,plain,
( ~ member(not_subclass_element(sF0,sF6),universal_class)
| spl7_37 ),
inference(avatar_component_clause,[],[f1458]) ).
fof(f1461,plain,
( spl7_36
| ~ spl7_37
| spl7_33 ),
inference(avatar_split_clause,[],[f1450,f1411,f1458,f1454]) ).
fof(f1506,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF6),X0)
| ~ subclass(X0,universal_class) )
| spl7_37 ),
inference(resolution,[],[f1460,f1]) ).
fof(f1508,plain,
( ! [X0] : ~ member(not_subclass_element(sF0,sF6),X0)
| spl7_37 ),
inference(forward_subsumption_resolution,[],[f1506,f4]) ).
fof(f1509,plain,
( subclass(sF0,sF6)
| spl7_37 ),
inference(resolution,[],[f1508,f2]) ).
fof(f1510,plain,
( sF0 = sF6
| ~ member(not_subclass_element(sF6,sF0),sF0)
| spl7_37 ),
inference(resolution,[],[f1508,f110]) ).
fof(f1511,plain,
( member(not_subclass_element(sF6,sF0),sF6)
| sF0 = sF6
| spl7_37 ),
inference(resolution,[],[f1508,f107]) ).
fof(f1529,plain,
( ~ member(y,sF5)
| subclass(sF0,sF6)
| spl7_3
| spl7_36 ),
inference(superposition,[],[f1455,f1113]) ).
fof(f1566,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF4)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),sF2) ),
inference(resolution,[],[f502,f936]) ).
fof(f1568,plain,
( ! [X0] :
( subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),sF2)
| member(not_subclass_element(sF6,X0),sF0)
| ~ member(not_subclass_element(sF6,X0),universal_class) )
| spl7_3 ),
inference(resolution,[],[f1566,f1077]) ).
fof(f1572,plain,
( ! [X0] :
( member(not_subclass_element(sF6,X0),sF0)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class) )
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1568,f361]) ).
fof(f1577,plain,
( subclass(sF6,sF0)
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| subclass(sF6,sF0)
| spl7_3 ),
inference(resolution,[],[f1572,f3]) ).
fof(f1581,plain,
( subclass(sF6,sF0)
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| spl7_3 ),
inference(duplicate_literal_removal,[],[f1577]) ).
fof(f1605,definition,
( spl7_45
<=> subclass(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_45])],[avatar_definition]) ).
fof(f1606,plain,
( ~ subclass(sF0,sF6)
| spl7_45 ),
inference(avatar_component_clause,[],[f1605]) ).
fof(f1607,plain,
( subclass(sF0,sF6)
| ~ spl7_45 ),
inference(avatar_component_clause,[],[f1605]) ).
fof(f1612,plain,
( member(not_subclass_element(sF6,sF0),sF6)
| spl7_37 ),
inference(forward_subsumption_resolution,[],[f1511,f262]) ).
fof(f1613,plain,
( ~ member(not_subclass_element(sF6,sF0),sF0)
| spl7_37 ),
inference(forward_subsumption_resolution,[],[f1510,f262]) ).
fof(f1614,plain,
( spl7_45
| spl7_37 ),
inference(avatar_split_clause,[],[f1509,f1458,f1605]) ).
fof(f1615,plain,
( subclass(sF0,sF6)
| spl7_3
| ~ spl7_27
| spl7_36 ),
inference(forward_subsumption_resolution,[],[f1529,f1281]) ).
fof(f1620,definition,
( spl7_47
<=> member(not_subclass_element(sF6,sF0),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_47])],[avatar_definition]) ).
fof(f1622,plain,
( member(not_subclass_element(sF6,sF0),sF6)
| ~ spl7_47 ),
inference(avatar_component_clause,[],[f1620]) ).
fof(f1625,definition,
( spl7_48
<=> member(not_subclass_element(sF6,sF0),sF0) ),
introduced(definition,[new_symbols(definition,[spl7_48])],[avatar_definition]) ).
fof(f1626,plain,
( member(not_subclass_element(sF6,sF0),sF0)
| ~ spl7_48 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1627,plain,
( ~ member(not_subclass_element(sF6,sF0),sF0)
| spl7_48 ),
inference(avatar_component_clause,[],[f1625]) ).
fof(f1630,plain,
( spl7_47
| spl7_37 ),
inference(avatar_split_clause,[],[f1612,f1458,f1620]) ).
fof(f1631,plain,
( ~ spl7_48
| spl7_37 ),
inference(avatar_split_clause,[],[f1613,f1458,f1625]) ).
fof(f1632,plain,
( spl7_45
| spl7_3
| ~ spl7_27
| spl7_36 ),
inference(avatar_split_clause,[],[f1615,f1454,f1280,f276,f1605]) ).
fof(f1639,plain,
( ~ member(not_subclass_element(sF0,sF6),sF0)
| spl7_3
| ~ spl7_36 ),
inference(resolution,[],[f1456,f1078]) ).
fof(f1644,plain,
( subclass(sF0,sF6)
| spl7_3
| ~ spl7_36 ),
inference(resolution,[],[f1639,f2]) ).
fof(f1648,plain,
( ~ member(y,sF0)
| subclass(sF0,sF6)
| spl7_3
| ~ spl7_36 ),
inference(superposition,[],[f1639,f1113]) ).
fof(f1649,plain,
( subclass(sF0,sF6)
| ~ spl7_1
| spl7_3
| ~ spl7_36 ),
inference(forward_subsumption_resolution,[],[f1648,f814]) ).
fof(f1652,plain,
( $false
| spl7_3
| ~ spl7_36
| spl7_45 ),
inference(forward_subsumption_resolution,[],[f1644,f1606]) ).
fof(f1653,plain,
( spl7_3
| ~ spl7_36
| spl7_45 ),
inference(avatar_contradiction_clause,[],[f1652]) ).
fof(f1654,plain,
( $false
| ~ spl7_1
| spl7_3
| ~ spl7_36
| spl7_45 ),
inference(forward_subsumption_resolution,[],[f1649,f1606]) ).
fof(f1655,plain,
( ~ spl7_1
| spl7_3
| ~ spl7_36
| spl7_45 ),
inference(avatar_contradiction_clause,[],[f1654]) ).
fof(f1659,definition,
( spl7_49
<=> subclass(sF6,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_49])],[avatar_definition]) ).
fof(f1660,plain,
( ~ subclass(sF6,sF0)
| spl7_49 ),
inference(avatar_component_clause,[],[f1659]) ).
fof(f1662,plain,
( ~ spl7_32
| spl7_49
| spl7_3 ),
inference(avatar_split_clause,[],[f1581,f276,f1659,f1407]) ).
fof(f1667,plain,
( ~ subclass(sF6,sF0)
| sF0 = sF6
| ~ spl7_45 ),
inference(resolution,[],[f1607,f7]) ).
fof(f1668,plain,
( ~ subclass(sF6,sF0)
| ~ spl7_45 ),
inference(forward_subsumption_resolution,[],[f1667,f262]) ).
fof(f1669,plain,
( ~ spl7_49
| ~ spl7_45 ),
inference(avatar_split_clause,[],[f1668,f1605,f1659]) ).
fof(f1670,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF6,sF0),X0)
| ~ subclass(X0,universal_class) )
| spl7_32 ),
inference(resolution,[],[f1409,f1]) ).
fof(f1671,plain,
( ! [X0] : ~ member(not_subclass_element(sF6,sF0),X0)
| spl7_32 ),
inference(forward_subsumption_resolution,[],[f1670,f4]) ).
fof(f1672,plain,
( subclass(sF6,sF0)
| spl7_32 ),
inference(resolution,[],[f1671,f2]) ).
fof(f1690,plain,
( $false
| spl7_32
| spl7_49 ),
inference(forward_subsumption_resolution,[],[f1672,f1660]) ).
fof(f1691,plain,
( spl7_32
| spl7_49 ),
inference(avatar_contradiction_clause,[],[f1690]) ).
fof(f1802,plain,
( subclass(sF0,sF6)
| ~ spl7_33 ),
inference(resolution,[],[f1412,f3]) ).
fof(f1806,plain,
( $false
| ~ spl7_33
| spl7_45 ),
inference(forward_subsumption_resolution,[],[f1802,f1606]) ).
fof(f1807,plain,
( ~ spl7_33
| spl7_45 ),
inference(avatar_contradiction_clause,[],[f1806]) ).
fof(f1808,plain,
( ~ member(not_subclass_element(sF0,sF6),sF1)
| ~ spl7_36 ),
inference(resolution,[],[f1456,f326]) ).
fof(f1809,plain,
( ~ member(not_subclass_element(sF0,sF6),sF3)
| ~ spl7_36 ),
inference(resolution,[],[f1456,f325]) ).
fof(f1843,plain,
! [X0] :
( member(not_subclass_element(sF6,X0),sF3)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),sF2) ),
inference(resolution,[],[f314,f1566]) ).
fof(f1863,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF2)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0) ),
inference(resolution,[],[f1843,f291]) ).
fof(f1887,plain,
! [X0] :
( subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| member(not_subclass_element(sF6,X0),sF1) ),
inference(resolution,[],[f1863,f313]) ).
fof(f1890,plain,
! [X0] :
( member(not_subclass_element(sF6,X0),sF1)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0) ),
inference(duplicate_literal_removal,[],[f1887]) ).
fof(f1914,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF6,sF0),X0)
| ~ subclass(X0,sF0) )
| spl7_48 ),
inference(resolution,[],[f1627,f1]) ).
fof(f1921,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(resolution,[],[f1890,f290]) ).
fof(f1951,plain,
( ~ subclass(sF6,sF0)
| member(not_subclass_element(sF0,sF6),sF0)
| sF0 = sF6
| spl7_48 ),
inference(resolution,[],[f1914,f107]) ).
fof(f1953,plain,
( ~ subclass(sF1,sF0)
| ~ member(not_subclass_element(sF6,sF0),universal_class)
| y = not_subclass_element(sF6,sF0)
| subclass(sF6,sF0)
| spl7_48 ),
inference(resolution,[],[f1914,f1890]) ).
fof(f1956,plain,
( ~ subclass(sF6,sF0)
| ~ spl7_47
| spl7_48 ),
inference(resolution,[],[f1914,f1622]) ).
fof(f1974,plain,
( ~ spl7_49
| ~ spl7_47
| spl7_48 ),
inference(avatar_split_clause,[],[f1956,f1625,f1620,f1659]) ).
fof(f1975,plain,
( ~ subclass(sF1,sF0)
| y = not_subclass_element(sF6,sF0)
| subclass(sF6,sF0)
| ~ spl7_32
| spl7_48 ),
inference(forward_subsumption_resolution,[],[f1953,f1408]) ).
fof(f1976,plain,
( ~ subclass(sF6,sF0)
| member(not_subclass_element(sF0,sF6),sF0)
| spl7_48 ),
inference(forward_subsumption_resolution,[],[f1951,f262]) ).
fof(f1979,definition,
( spl7_67
<=> y = not_subclass_element(sF6,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_67])],[avatar_definition]) ).
fof(f1981,plain,
( y = not_subclass_element(sF6,sF0)
| ~ spl7_67 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1983,definition,
( spl7_68
<=> subclass(sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_68])],[avatar_definition]) ).
fof(f1985,plain,
( ~ subclass(sF1,sF0)
| spl7_68 ),
inference(avatar_component_clause,[],[f1983]) ).
fof(f1986,plain,
( spl7_49
| spl7_67
| ~ spl7_68
| ~ spl7_32
| spl7_48 ),
inference(avatar_split_clause,[],[f1975,f1625,f1407,f1983,f1979,f1659]) ).
fof(f1988,definition,
( spl7_69
<=> member(not_subclass_element(sF0,sF6),sF0) ),
introduced(definition,[new_symbols(definition,[spl7_69])],[avatar_definition]) ).
fof(f1989,plain,
( ~ member(not_subclass_element(sF0,sF6),sF0)
| spl7_69 ),
inference(avatar_component_clause,[],[f1988]) ).
fof(f1990,plain,
( member(not_subclass_element(sF0,sF6),sF0)
| ~ spl7_69 ),
inference(avatar_component_clause,[],[f1988]) ).
fof(f1991,plain,
( spl7_69
| ~ spl7_49
| spl7_48 ),
inference(avatar_split_clause,[],[f1976,f1625,f1659,f1988]) ).
fof(f1999,plain,
( x = not_subclass_element(sF0,sF6)
| y = not_subclass_element(sF0,sF6)
| ~ spl7_69 ),
inference(resolution,[],[f1990,f305]) ).
fof(f2000,plain,
( spl7_34
| spl7_35
| ~ spl7_69 ),
inference(avatar_split_clause,[],[f1999,f1988,f1422,f1417]) ).
fof(f2005,plain,
( ~ member(x,sF1)
| ~ spl7_35
| ~ spl7_36 ),
inference(backward_demodulation,[],[f1808,f1424]) ).
fof(f2015,plain,
( $false
| ~ spl7_4
| ~ spl7_35
| ~ spl7_36 ),
inference(forward_subsumption_resolution,[],[f2005,f282]) ).
fof(f2016,plain,
( ~ spl7_4
| ~ spl7_35
| ~ spl7_36 ),
inference(avatar_contradiction_clause,[],[f2015]) ).
fof(f2023,plain,
( ~ member(y,sF3)
| ~ spl7_34
| ~ spl7_36 ),
inference(forward_demodulation,[],[f1809,f1419]) ).
fof(f2032,plain,
( $false
| ~ spl7_2
| ~ spl7_34
| ~ spl7_36 ),
inference(forward_subsumption_resolution,[],[f2023,f273]) ).
fof(f2033,plain,
( ~ spl7_2
| ~ spl7_34
| ~ spl7_36 ),
inference(avatar_contradiction_clause,[],[f2032]) ).
fof(f2035,plain,
( sF0 = sF6
| x = not_subclass_element(sF0,sF6)
| y = not_subclass_element(sF0,sF6)
| ~ spl7_48 ),
inference(resolution,[],[f1626,f452]) ).
fof(f2036,plain,
( subclass(sF6,sF0)
| ~ spl7_48 ),
inference(resolution,[],[f1626,f3]) ).
fof(f2040,definition,
( spl7_71
<=> x = not_subclass_element(sF6,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_71])],[avatar_definition]) ).
fof(f2042,plain,
( x = not_subclass_element(sF6,sF0)
| ~ spl7_71 ),
inference(avatar_component_clause,[],[f2040]) ).
fof(f2044,plain,
( spl7_49
| ~ spl7_48 ),
inference(avatar_split_clause,[],[f2036,f1625,f1659]) ).
fof(f2045,plain,
( x = not_subclass_element(sF0,sF6)
| y = not_subclass_element(sF0,sF6)
| ~ spl7_48 ),
inference(forward_subsumption_resolution,[],[f2035,f262]) ).
fof(f2046,plain,
( y = not_subclass_element(sF0,sF6)
| spl7_35
| ~ spl7_48 ),
inference(forward_subsumption_resolution,[],[f2045,f1423]) ).
fof(f2047,plain,
( $false
| spl7_34
| spl7_35
| ~ spl7_48 ),
inference(forward_subsumption_resolution,[],[f2046,f1418]) ).
fof(f2048,plain,
( spl7_34
| spl7_35
| ~ spl7_48 ),
inference(avatar_contradiction_clause,[],[f2047]) ).
fof(f2052,plain,
( member(y,universal_class)
| ~ spl7_34
| ~ spl7_37 ),
inference(backward_demodulation,[],[f1459,f1419]) ).
fof(f2065,plain,
( unordered_pair(x,x) = sF0
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f596,f269]) ).
fof(f2084,plain,
( $false
| spl7_1
| ~ spl7_34
| ~ spl7_37 ),
inference(forward_subsumption_resolution,[],[f2052,f269]) ).
fof(f2085,plain,
( spl7_1
| ~ spl7_34
| ~ spl7_37 ),
inference(avatar_contradiction_clause,[],[f2084]) ).
fof(f2090,plain,
( sF0 = sF1
| spl7_1 ),
inference(backward_demodulation,[],[f251,f2065]) ).
fof(f2146,plain,
( ~ subclass(sF0,sF0)
| spl7_1
| spl7_68 ),
inference(backward_demodulation,[],[f1985,f2090]) ).
fof(f2150,plain,
( $false
| spl7_1
| spl7_68 ),
inference(forward_subsumption_resolution,[],[f2146,f105]) ).
fof(f2151,plain,
( spl7_1
| spl7_68 ),
inference(avatar_contradiction_clause,[],[f2150]) ).
fof(f2163,plain,
( member(y,sF0)
| ~ spl7_1 ),
inference(forward_subsumption_resolution,[],[f293,f268]) ).
fof(f2301,plain,
( subclass(sF0,sF6)
| spl7_69 ),
inference(resolution,[],[f1989,f2]) ).
fof(f2305,plain,
( $false
| spl7_45
| spl7_69 ),
inference(forward_subsumption_resolution,[],[f2301,f1606]) ).
fof(f2306,plain,
( spl7_45
| spl7_69 ),
inference(avatar_contradiction_clause,[],[f2305]) ).
fof(f2761,plain,
( y = not_subclass_element(sF6,sF0)
| subclass(sF6,sF0)
| x = not_subclass_element(sF6,sF0)
| ~ spl7_32 ),
inference(resolution,[],[f1921,f1408]) ).
fof(f2764,plain,
( y = not_subclass_element(sF6,sF0)
| x = not_subclass_element(sF6,sF0)
| ~ spl7_32
| spl7_49 ),
inference(forward_subsumption_resolution,[],[f2761,f1660]) ).
fof(f2765,plain,
( spl7_71
| spl7_67
| ~ spl7_32
| spl7_49 ),
inference(avatar_split_clause,[],[f2764,f1659,f1407,f1979,f2040]) ).
fof(f2769,plain,
( ~ member(x,sF0)
| spl7_48
| ~ spl7_71 ),
inference(backward_demodulation,[],[f1627,f2042]) ).
fof(f2779,plain,
( $false
| ~ spl7_5
| spl7_48
| ~ spl7_71 ),
inference(forward_subsumption_resolution,[],[f2769,f287]) ).
fof(f2780,plain,
( ~ spl7_5
| spl7_48
| ~ spl7_71 ),
inference(avatar_contradiction_clause,[],[f2779]) ).
fof(f2782,plain,
( member(y,universal_class)
| ~ spl7_32
| ~ spl7_67 ),
inference(forward_demodulation,[],[f1408,f1981]) ).
fof(f2785,plain,
( ~ member(y,sF0)
| spl7_48
| ~ spl7_67 ),
inference(forward_demodulation,[],[f1627,f1981]) ).
fof(f2794,plain,
( $false
| ~ spl7_1
| spl7_48
| ~ spl7_67 ),
inference(forward_subsumption_resolution,[],[f2785,f2163]) ).
fof(f2795,plain,
( ~ spl7_1
| spl7_48
| ~ spl7_67 ),
inference(avatar_contradiction_clause,[],[f2794]) ).
fof(f2886,plain,
( $false
| spl7_1
| ~ spl7_32
| ~ spl7_67 ),
inference(forward_subsumption_resolution,[],[f2782,f269]) ).
fof(f2887,plain,
( spl7_1
| ~ spl7_32
| ~ spl7_67 ),
inference(avatar_contradiction_clause,[],[f2886]) ).
cnf(s1,plain,
( ~ spl7_1
| spl7_2 ),
inference(sat_conversion,[],[f274]) ).
cnf(s2,plain,
( ~ spl7_3
| spl7_4 ),
inference(sat_conversion,[],[f283]) ).
cnf(s3,plain,
( ~ spl7_3
| spl7_5 ),
inference(sat_conversion,[],[f288]) ).
cnf(s6,plain,
( spl7_1
| spl7_3
| spl7_10 ),
inference(sat_conversion,[],[f635]) ).
cnf(s8,plain,
( ~ spl7_7
| ~ spl7_10 ),
inference(sat_conversion,[],[f650]) ).
cnf(s9,plain,
( spl7_1
| spl7_3
| spl7_7 ),
inference(sat_conversion,[],[f808]) ).
cnf(s37,plain,
( spl7_3
| ~ spl7_32
| ~ spl7_33 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s41,plain,
( ~ spl7_1
| spl7_3
| spl7_27
| spl7_32 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s42,plain,
( spl7_32
| ~ spl7_33 ),
inference(sat_conversion,[],[f1449]) ).
cnf(s43,plain,
( spl7_33
| spl7_36
| ~ spl7_37 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s55,plain,
( spl7_37
| spl7_45 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s59,plain,
( spl7_37
| spl7_47 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s60,plain,
( spl7_37
| ~ spl7_48 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s61,plain,
( spl7_3
| ~ spl7_27
| spl7_36
| spl7_45 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s63,plain,
( spl7_3
| ~ spl7_36
| spl7_45 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s64,plain,
( ~ spl7_1
| spl7_3
| ~ spl7_36
| spl7_45 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s67,plain,
( spl7_3
| ~ spl7_32
| spl7_49 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s70,plain,
( ~ spl7_45
| ~ spl7_49 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s71,plain,
( spl7_32
| spl7_49 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s81,plain,
( ~ spl7_33
| spl7_45 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s88,plain,
( ~ spl7_47
| spl7_48
| ~ spl7_49 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s89,plain,
( ~ spl7_32
| spl7_48
| spl7_49
| spl7_67
| ~ spl7_68 ),
inference(sat_conversion,[],[f1986]) ).
cnf(s90,plain,
( spl7_48
| ~ spl7_49
| spl7_69 ),
inference(sat_conversion,[],[f1991]) ).
cnf(s93,plain,
( spl7_34
| spl7_35
| ~ spl7_69 ),
inference(sat_conversion,[],[f2000]) ).
cnf(s94,plain,
( ~ spl7_4
| ~ spl7_35
| ~ spl7_36 ),
inference(sat_conversion,[],[f2016]) ).
cnf(s96,plain,
( ~ spl7_2
| ~ spl7_34
| ~ spl7_36 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s98,plain,
( ~ spl7_48
| spl7_49 ),
inference(sat_conversion,[],[f2044]) ).
cnf(s99,plain,
( spl7_34
| spl7_35
| ~ spl7_48 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s100,plain,
( spl7_1
| ~ spl7_34
| ~ spl7_37 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s112,plain,
( spl7_1
| spl7_68 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s120,plain,
( spl7_45
| spl7_69 ),
inference(sat_conversion,[],[f2306]) ).
cnf(s140,plain,
( ~ spl7_32
| spl7_49
| spl7_67
| spl7_71 ),
inference(sat_conversion,[],[f2765]) ).
cnf(s141,plain,
( ~ spl7_5
| spl7_48
| ~ spl7_71 ),
inference(sat_conversion,[],[f2780]) ).
cnf(s142,plain,
( ~ spl7_1
| spl7_48
| ~ spl7_67 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s144,plain,
( spl7_1
| ~ spl7_32
| ~ spl7_67 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s152,plain,
( spl7_3
| spl7_1 ),
inference(rat,[],[s8,s6,s9]) ).
cnf(s153,plain,
( spl7_32
| spl7_1 ),
inference(rat,[],[s94,s93,s43,s100,s55,s120,s70,s42,s71,s2,s152]) ).
cnf(s154,plain,
( spl7_37
| spl7_1 ),
inference(rat,[],[s88,s89,s59,s60,s112,s144,s153]) ).
cnf(s155,plain,
( spl7_35
| spl7_1 ),
inference(rat,[],[s90,s89,s93,s99,s112,s144,s153,s100,s154]) ).
cnf(s156,plain,
spl7_1,
inference(rat,[],[s89,s98,s70,s81,s43,s94,s155,s154,s144,s153,s2,s152,s112]) ).
cnf(s158,plain,
spl7_2,
inference(rat,[],[s1,s156]) ).
cnf(s160,plain,
( spl7_34
| spl7_35
| ~ spl7_32 ),
inference(rat,[],[s141,s3,s140,s67,s90,s142,s93,s99,s156]) ).
cnf(s161,plain,
( spl7_37
| ~ spl7_32 ),
inference(rat,[],[s141,s3,s140,s67,s88,s142,s59,s60,s156]) ).
cnf(s162,plain,
( ~ spl7_36
| ~ spl7_32
| ~ spl7_4 ),
inference(rat,[],[s160,s94,s96,s158]) ).
cnf(s163,plain,
( ~ spl7_32
| ~ spl7_4 ),
inference(rat,[],[s140,s142,s141,s98,s3,s70,s37,s81,s43,s162,s161,s156]) ).
cnf(s164,plain,
~ spl7_4,
inference(rat,[],[s93,s94,s96,s43,s55,s120,s70,s42,s71,s163,s158]) ).
cnf(s165,plain,
~ spl7_3,
inference(rat,[],[s2,s164]) ).
cnf(s171,plain,
~ spl7_32,
inference(rat,[],[s63,s70,s43,s37,s67,s161,s165]) ).
cnf(s172,plain,
spl7_49,
inference(rat,[],[s71,s171]) ).
cnf(s174,plain,
spl7_27,
inference(rat,[],[s41,s165,s156,s171]) ).
cnf(s175,plain,
~ spl7_45,
inference(rat,[],[s70,s172]) ).
cnf(s176,plain,
spl7_36,
inference(rat,[],[s61,s175,s165,s174]) ).
cnf(s179,plain,
$false,
inference(rat,[],[s64,s165,s156,s175,s176]) ).
fof(f2998,plain,
$false,
inference(avatar_sat_refutation,[],[s179]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET100-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n013.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.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 00:41:22 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
% 8.67/2.10 % (706020)Input is clausal, will run a generic CNF schedule.
% 8.67/2.10 % (706026)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1560990846:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.67/2.10 % (706031)dis-21_1_sil=8000:lcm=predicate:random_seed=4034730163: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)
% 8.67/2.10 % (706030)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2352805224:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.67/2.10 % (706025)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=100813576:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.67/2.10 % (706027)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=278324418:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.67/2.10 % (706029)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2730974748:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.67/2.10 % (706028)lrs+10_1_sil=8000:sp=occurrence:random_seed=3973955666:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.67/2.10 % (706029)Instruction limit reached!
% 8.67/2.10 % (706029)------------------------------
% 8.67/2.10 % (706029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706029)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706029)Termination reason: Instruction limit
% 8.67/2.10 % (706029)Termination phase: Saturation
% 8.67/2.10 % (706029)Time elapsed: 0.051 s
% 8.67/2.10 % (706029)Peak memory usage: 88 MB
% 8.67/2.10 % (706029)Instructions burned: 114 (million)
% 8.67/2.10 % (706031)Instruction limit reached!
% 8.67/2.10 % (706031)------------------------------
% 8.67/2.10 % (706031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706031)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706028)Instruction limit reached!
% 8.67/2.10 % (706028)------------------------------
% 8.67/2.10 % (706028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706031)Termination reason: Instruction limit
% 8.67/2.10 % (706031)Termination phase: Saturation
% 8.67/2.10 % (706031)Time elapsed: 0.073 s
% 8.67/2.10 % (706031)Peak memory usage: 89 MB
% 8.67/2.10 % (706028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706031)Instructions burned: 118 (million)
% 8.67/2.10 % (706028)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706028)Termination reason: Instruction limit
% 8.67/2.10 % (706028)Termination phase: Saturation
% 8.67/2.10 % (706028)Time elapsed: 0.073 s
% 8.67/2.10 % (706028)Peak memory usage: 89 MB
% 8.67/2.10 % (706028)Instructions burned: 109 (million)
% 8.67/2.10 % (706030)Instruction limit reached!
% 8.67/2.10 % (706030)------------------------------
% 8.67/2.10 % (706030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706030)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706030)Termination reason: Instruction limit
% 8.67/2.10 % (706030)Termination phase: Saturation
% 8.67/2.10 % (706030)Time elapsed: 0.121 s
% 8.67/2.10 % (706030)Peak memory usage: 90 MB
% 8.67/2.10 % (706030)Instructions burned: 182 (million)
% 8.67/2.10 % (706039)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=4262265017:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.67/2.10 % (706039)Refutation not found, incomplete strategy
% 8.67/2.10 % (706039)------------------------------
% 8.67/2.10 % (706039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706039)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706039)Termination reason: Refutation not found, incomplete strategy
% 8.67/2.10 % (706039)Time elapsed: 0.003 s
% 8.67/2.10 % (706039)Peak memory usage: 88 MB
% 8.67/2.10 % (706039)Instructions burned: 4 (million)
% 8.67/2.10 % (706041)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=896743910:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.67/2.10 % (706040)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2181912711: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)
% 8.67/2.10 % (706042)lrs+10_64_to=lpo:sil=8000:random_seed=652954272:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 8.67/2.10 % (706040)Instruction limit reached!
% 8.67/2.10 % (706040)------------------------------
% 8.67/2.10 % (706040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706040)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706040)Termination reason: Instruction limit
% 8.67/2.10 % (706040)Termination phase: Saturation
% 8.67/2.10 % (706040)Time elapsed: 0.102 s
% 8.67/2.10 % (706040)Peak memory usage: 90 MB
% 8.67/2.10 % (706040)Instructions burned: 191 (million)
% 8.67/2.10 % (706042)Instruction limit reached!
% 8.67/2.10 % (706042)------------------------------
% 8.67/2.10 % (706042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706042)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706042)Termination reason: Instruction limit
% 8.67/2.10 % (706042)Termination phase: Saturation
% 8.67/2.10 % (706042)Time elapsed: 0.079 s
% 8.67/2.10 % (706042)Peak memory usage: 89 MB
% 8.67/2.10 % (706042)Instructions burned: 126 (million)
% 8.67/2.10 % (706041)Instruction limit reached!
% 8.67/2.10 % (706041)------------------------------
% 8.67/2.10 % (706041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706041)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706041)Termination reason: Instruction limit
% 8.67/2.10 % (706041)Termination phase: Saturation
% 8.67/2.10 % (706041)Time elapsed: 0.140 s
% 8.67/2.10 % (706041)Peak memory usage: 90 MB
% 8.67/2.10 % (706041)Instructions burned: 220 (million)
% 8.67/2.10 % (706039)------------------------------
% 8.67/2.10 % (706039)------------------------------
% 8.67/2.10 % (706047)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3932370330:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 8.67/2.10 % (706048)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1537893884:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.67/2.10 % (706049)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2296677976:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 8.67/2.10 % (706048)Instruction limit reached!
% 8.67/2.10 % (706048)------------------------------
% 8.67/2.10 % (706048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706048)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706048)Termination reason: Instruction limit
% 8.67/2.10 % (706048)Termination phase: Saturation
% 8.67/2.10 % (706048)Time elapsed: 0.093 s
% 8.67/2.10 % (706048)Peak memory usage: 90 MB
% 8.67/2.10 % (706048)Instructions burned: 158 (million)
% 8.67/2.10 % (706050)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=869782714:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 8.67/2.10 % (706047)Instruction limit reached!
% 8.67/2.10 % (706047)------------------------------
% 8.67/2.10 % (706047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706047)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706047)Termination reason: Instruction limit
% 8.67/2.10 % (706047)Termination phase: Saturation
% 8.67/2.10 % (706047)Time elapsed: 0.130 s
% 8.67/2.10 % (706047)Peak memory usage: 90 MB
% 8.67/2.10 % (706047)Instructions burned: 194 (million)
% 8.67/2.10 % (706050)Instruction limit reached!
% 8.67/2.10 % (706050)------------------------------
% 8.67/2.10 % (706050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706050)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706050)Termination reason: Instruction limit
% 8.67/2.10 % (706050)Termination phase: Saturation
% 8.67/2.10 % (706050)Time elapsed: 0.066 s
% 8.67/2.10 % (706050)Peak memory usage: 89 MB
% 8.67/2.10 % (706050)Instructions burned: 106 (million)
% 8.67/2.10 % (706055)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3877275272:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 8.67/2.10 % (706056)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=563045923:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 8.67/2.10 % (706055)Refutation not found, incomplete strategy
% 8.67/2.10 % (706055)------------------------------
% 8.67/2.10 % (706055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706055)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706055)Termination reason: Refutation not found, incomplete strategy
% 8.67/2.10 % (706055)Time elapsed: 0.005 s
% 8.67/2.10 % (706055)Peak memory usage: 88 MB
% 8.67/2.10 % (706055)Instructions burned: 9 (million)
% 8.67/2.10 % (706057)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3597117543:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 8.67/2.10 % (706027)First to succeed.
% 8.67/2.10 % (706027)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-706020"
% 8.67/2.10 % (706056)Instruction limit reached!
% 8.67/2.10 % (706056)------------------------------
% 8.67/2.10 % (706056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.67/2.10 % (706056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.67/2.10 % (706056)CaDiCaL version: 2.1.3
% 8.67/2.10 % (706056)Termination reason: Instruction limit
% 8.67/2.10 % (706056)Termination phase: Saturation
% 8.67/2.10 % (706056)Time elapsed: 0.167 s
% 8.67/2.10 % (706056)Peak memory usage: 89 MB
% 8.67/2.10 % (706056)Instructions burned: 242 (million)
% 8.67/2.10 % (706055)------------------------------
% 8.67/2.10 % (706055)------------------------------
% 8.67/2.10 % (706061)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3194090581:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 8.67/2.10 % (706027)Refutation found. Thanks to Tanya!
% 8.67/2.10 % SZS status Unsatisfiable for theBenchmark
% 8.67/2.10 % SZS output start Proof for theBenchmark
% See solution above
% 9.30/2.29 % (706027)------------------------------
% 9.30/2.29 % (706027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.30/2.29 % (706027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.30/2.29 % (706027)CaDiCaL version: 2.1.3
% 9.30/2.29 % (706027)Termination reason: Refutation
% 9.30/2.29 % (706027)Time elapsed: 0.829 s
% 9.30/2.29 % (706027)Peak memory usage: 132 MB
% 9.30/2.29 % (706027)Instructions burned: 1241 (million)
% 9.30/2.29 % (706027)------------------------------
% 9.30/2.29 % (706027)------------------------------
% 9.30/2.29 % (706020)Success in time 1.243 s
% 9.30/2.29 % Vampire exiting
%------------------------------------------------------------------------------