%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM146-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:11:49 PM UTC 2026
% Result : Unsatisfiable 84.50s 12.88s
% Output : Refutation 85.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 115
% Syntax : Number of formulae : 548 ( 126 unt; 86 def)
% Number of atoms : 1327 ( 166 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1410 ( 631 ~; 704 |; 0 &)
% ( 75 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 79 ( 77 usr; 76 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 15 con; 0-3 aty)
% Number of variables : 244 ( 0 sgn 244 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f19,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),element_relation)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation2) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,complement(X1))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f44,axiom,
! [X0] : union(X0,singleton(X0)) = successor(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor) ).
fof(f54,axiom,
! [X0] : domain_of(restrict(element_relation,universal_class,X0)) = sum_class(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class_definition) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f176,negated_conjecture,
subclass(sum_class(x),x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_successor_or_transitive_set_is_set_1) ).
fof(f177,negated_conjecture,
~ subclass(sum_class(successor(x)),successor(x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_successor_or_transitive_set_is_set_2) ).
fof(f178,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f183,plain,
! [X0] : successor(X0) = complement(intersection(complement(X0),complement(unordered_pair(X0,X0)))),
inference(definition_unfolding,[],[f44,f26,f12]) ).
fof(f184,plain,
! [X0] : sum_class(X0) = domain_of(intersection(element_relation,cross_product(universal_class,X0))),
inference(definition_unfolding,[],[f54,f28]) ).
fof(f195,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f178]) ).
fof(f196,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f178]) ).
fof(f197,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f178]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f178]) ).
fof(f199,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| member(X0,X1) ),
inference(definition_unfolding,[],[f19,f178]) ).
fof(f202,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f203,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f268,plain,
subclass(domain_of(intersection(element_relation,cross_product(universal_class,x))),x),
inference(definition_unfolding,[],[f176,f184]) ).
fof(f269,plain,
~ subclass(domain_of(intersection(element_relation,cross_product(universal_class,complement(intersection(complement(x),complement(unordered_pair(x,x))))))),complement(intersection(complement(x),complement(unordered_pair(x,x))))),
inference(definition_unfolding,[],[f177,f184,f183,f183]) ).
fof(f276,definition,
sF0 = cross_product(universal_class,x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f277,plain,
cross_product(universal_class,x) = sF0,
inference(reorient_equations,[],[f276]) ).
fof(f278,definition,
sF1 = intersection(element_relation,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f279,plain,
intersection(element_relation,sF0) = sF1,
inference(reorient_equations,[],[f278]) ).
fof(f280,definition,
sF2 = domain_of(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f281,plain,
domain_of(sF1) = sF2,
inference(reorient_equations,[],[f280]) ).
fof(f282,plain,
subclass(sF2,x),
inference(definition_folding,[],[f268,f281,f279,f277]) ).
fof(f283,definition,
sF3 = complement(x),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f284,plain,
complement(x) = sF3,
inference(reorient_equations,[],[f283]) ).
fof(f285,definition,
sF4 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f286,plain,
unordered_pair(x,x) = sF4,
inference(reorient_equations,[],[f285]) ).
fof(f287,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f288,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f287]) ).
fof(f289,definition,
sF6 = intersection(sF3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f290,plain,
intersection(sF3,sF5) = sF6,
inference(reorient_equations,[],[f289]) ).
fof(f291,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f292,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f291]) ).
fof(f293,definition,
sF8 = cross_product(universal_class,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f294,plain,
cross_product(universal_class,sF7) = sF8,
inference(reorient_equations,[],[f293]) ).
fof(f295,definition,
sF9 = intersection(element_relation,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f296,plain,
intersection(element_relation,sF8) = sF9,
inference(reorient_equations,[],[f295]) ).
fof(f297,definition,
sF10 = domain_of(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f298,plain,
domain_of(sF9) = sF10,
inference(reorient_equations,[],[f297]) ).
fof(f299,plain,
~ subclass(sF10,sF7),
inference(definition_folding,[],[f269,f292,f290,f288,f286,f284,f298,f296,f294,f292,f290,f288,f286,f284]) ).
fof(f303,plain,
! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ subclass(X1,universal_class)
| member(X0,complement(X2))
| member(X0,X2) ),
inference(resolution,[],[f1,f25]) ).
fof(f304,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| ~ subclass(X2,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f1,f3]) ).
fof(f305,plain,
! [X2,X0,X1] :
( member(X0,complement(X2))
| ~ member(X0,X1)
| member(X0,X2) ),
inference(forward_subsumption_resolution,[],[f303,f4]) ).
fof(f315,definition,
( spl11_1
<=> intersection(sF3,sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f317,plain,
( intersection(sF3,sF5) = sF6
| ~ spl11_1 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
spl11_1,
inference(avatar_split_clause,[],[f290,f315]) ).
fof(f320,plain,
( ! [X0] :
( ~ member(X0,sF6)
| member(X0,sF3) )
| ~ spl11_1 ),
inference(superposition,[],[f21,f317]) ).
fof(f322,definition,
( spl11_2
<=> unordered_pair(x,x) = sF4 ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f324,plain,
( unordered_pair(x,x) = sF4
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f325,plain,
spl11_2,
inference(avatar_split_clause,[],[f286,f322]) ).
fof(f327,definition,
( spl11_3
<=> subclass(sF2,x) ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
fof(f329,plain,
( subclass(sF2,x)
| ~ spl11_3 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f330,plain,
spl11_3,
inference(avatar_split_clause,[],[f282,f327]) ).
fof(f334,plain,
( ! [X0] :
( member(X0,sF6)
| ~ member(X0,sF5)
| ~ member(X0,sF3) )
| ~ spl11_1 ),
inference(superposition,[],[f23,f317]) ).
fof(f336,definition,
( spl11_4
<=> ! [X0] :
( member(X0,sF6)
| ~ member(X0,sF5)
| ~ member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl11_4])],[avatar_definition]) ).
fof(f337,plain,
( ! [X0] :
( member(X0,sF6)
| ~ member(X0,sF5)
| ~ member(X0,sF3) )
| ~ spl11_4 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( spl11_4
| ~ spl11_1 ),
inference(avatar_split_clause,[],[f334,f315,f336]) ).
fof(f340,definition,
( spl11_5
<=> cross_product(universal_class,x) = sF0 ),
introduced(definition,[new_symbols(definition,[spl11_5])],[avatar_definition]) ).
fof(f342,plain,
( cross_product(universal_class,x) = sF0
| ~ spl11_5 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,plain,
spl11_5,
inference(avatar_split_clause,[],[f277,f340]) ).
fof(f345,definition,
( spl11_6
<=> cross_product(universal_class,sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl11_6])],[avatar_definition]) ).
fof(f347,plain,
( cross_product(universal_class,sF7) = sF8
| ~ spl11_6 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f348,plain,
spl11_6,
inference(avatar_split_clause,[],[f294,f345]) ).
fof(f350,definition,
( spl11_7
<=> intersection(element_relation,sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl11_7])],[avatar_definition]) ).
fof(f352,plain,
( intersection(element_relation,sF8) = sF9
| ~ spl11_7 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
spl11_7,
inference(avatar_split_clause,[],[f296,f350]) ).
fof(f355,definition,
( spl11_8
<=> intersection(element_relation,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl11_8])],[avatar_definition]) ).
fof(f357,plain,
( intersection(element_relation,sF0) = sF1
| ~ spl11_8 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,plain,
spl11_8,
inference(avatar_split_clause,[],[f279,f355]) ).
fof(f363,definition,
( spl11_9
<=> domain_of(sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl11_9])],[avatar_definition]) ).
fof(f365,plain,
( domain_of(sF9) = sF10
| ~ spl11_9 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f366,plain,
spl11_9,
inference(avatar_split_clause,[],[f298,f363]) ).
fof(f370,definition,
( spl11_10
<=> domain_of(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl11_10])],[avatar_definition]) ).
fof(f372,plain,
( domain_of(sF1) = sF2
| ~ spl11_10 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
spl11_10,
inference(avatar_split_clause,[],[f281,f370]) ).
fof(f379,definition,
( spl11_11
<=> complement(x) = sF3 ),
introduced(definition,[new_symbols(definition,[spl11_11])],[avatar_definition]) ).
fof(f381,plain,
( complement(x) = sF3
| ~ spl11_11 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f382,plain,
spl11_11,
inference(avatar_split_clause,[],[f284,f379]) ).
fof(f383,plain,
( ! [X0,X1] :
( member(X0,sF3)
| ~ member(X0,X1)
| member(X0,x) )
| ~ spl11_11 ),
inference(superposition,[],[f305,f381]) ).
fof(f384,plain,
( ! [X0] :
( ~ member(X0,sF3)
| ~ member(X0,x) )
| ~ spl11_11 ),
inference(superposition,[],[f24,f381]) ).
fof(f386,definition,
( spl11_12
<=> ! [X0] :
( ~ member(X0,sF6)
| member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl11_12])],[avatar_definition]) ).
fof(f387,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF6) )
| ~ spl11_12 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f388,plain,
( spl11_12
| ~ spl11_1 ),
inference(avatar_split_clause,[],[f320,f315,f386]) ).
fof(f390,definition,
( spl11_13
<=> ! [X0] :
( ~ member(X0,sF3)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl11_13])],[avatar_definition]) ).
fof(f391,plain,
( ! [X0] :
( ~ member(X0,sF3)
| ~ member(X0,x) )
| ~ spl11_13 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f392,plain,
( spl11_13
| ~ spl11_11 ),
inference(avatar_split_clause,[],[f384,f379,f390]) ).
fof(f394,plain,
( ! [X0] :
( ~ member(X0,sF9)
| member(X0,sF8) )
| ~ spl11_7 ),
inference(superposition,[],[f22,f352]) ).
fof(f395,plain,
( ! [X0] :
( ~ member(X0,sF9)
| member(X0,element_relation) )
| ~ spl11_7 ),
inference(superposition,[],[f21,f352]) ).
fof(f402,definition,
( spl11_15
<=> ! [X0] :
( ~ member(X0,sF9)
| member(X0,sF8) ) ),
introduced(definition,[new_symbols(definition,[spl11_15])],[avatar_definition]) ).
fof(f403,plain,
( ! [X0] :
( member(X0,sF8)
| ~ member(X0,sF9) )
| ~ spl11_15 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( spl11_15
| ~ spl11_7 ),
inference(avatar_split_clause,[],[f394,f350,f402]) ).
fof(f410,definition,
( spl11_17
<=> ! [X0,X1] :
( member(X0,sF3)
| ~ member(X0,X1)
| member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl11_17])],[avatar_definition]) ).
fof(f411,plain,
( ! [X0,X1] :
( member(X0,sF3)
| ~ member(X0,X1)
| member(X0,x) )
| ~ spl11_17 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f412,plain,
( spl11_17
| ~ spl11_11 ),
inference(avatar_split_clause,[],[f383,f379,f410]) ).
fof(f413,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,sF0)
| ~ member(X0,element_relation) )
| ~ spl11_8 ),
inference(superposition,[],[f23,f357]) ).
fof(f417,definition,
( spl11_18
<=> ! [X0] :
( member(X0,sF1)
| ~ member(X0,sF0)
| ~ member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl11_18])],[avatar_definition]) ).
fof(f418,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,sF0)
| ~ member(X0,element_relation) )
| ~ spl11_18 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( spl11_18
| ~ spl11_8 ),
inference(avatar_split_clause,[],[f413,f355,f417]) ).
fof(f431,definition,
( spl11_20
<=> complement(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl11_20])],[avatar_definition]) ).
fof(f433,plain,
( complement(sF6) = sF7
| ~ spl11_20 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f434,plain,
spl11_20,
inference(avatar_split_clause,[],[f292,f431]) ).
fof(f435,plain,
( ! [X0,X1] :
( member(X0,sF7)
| ~ member(X0,X1)
| member(X0,sF6) )
| ~ spl11_20 ),
inference(superposition,[],[f305,f433]) ).
fof(f436,plain,
( ! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sF6) )
| ~ spl11_20 ),
inference(superposition,[],[f24,f433]) ).
fof(f438,definition,
( spl11_21
<=> ! [X0,X1] :
( member(X0,sF7)
| ~ member(X0,X1)
| member(X0,sF6) ) ),
introduced(definition,[new_symbols(definition,[spl11_21])],[avatar_definition]) ).
fof(f439,plain,
( ! [X0,X1] :
( member(X0,sF7)
| ~ member(X0,X1)
| member(X0,sF6) )
| ~ spl11_21 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f440,plain,
( spl11_21
| ~ spl11_20 ),
inference(avatar_split_clause,[],[f435,f431,f438]) ).
fof(f441,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF7),X1)
| member(not_subclass_element(X0,sF7),sF6)
| subclass(X0,sF7) )
| ~ spl11_21 ),
inference(resolution,[],[f439,f3]) ).
fof(f443,definition,
( spl11_22
<=> ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF7),X1)
| member(not_subclass_element(X0,sF7),sF6)
| subclass(X0,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl11_22])],[avatar_definition]) ).
fof(f444,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,sF7),sF6)
| ~ member(not_subclass_element(X0,sF7),X1)
| subclass(X0,sF7) )
| ~ spl11_22 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( spl11_22
| ~ spl11_21 ),
inference(avatar_split_clause,[],[f441,f438,f443]) ).
fof(f447,definition,
( spl11_23
<=> ! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sF6) ) ),
introduced(definition,[new_symbols(definition,[spl11_23])],[avatar_definition]) ).
fof(f448,plain,
( ! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sF6) )
| ~ spl11_23 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( spl11_23
| ~ spl11_20 ),
inference(avatar_split_clause,[],[f436,f431,f447]) ).
fof(f459,definition,
( spl11_24
<=> subclass(sF10,sF7) ),
introduced(definition,[new_symbols(definition,[spl11_24])],[avatar_definition]) ).
fof(f461,plain,
( ~ subclass(sF10,sF7)
| spl11_24 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f462,plain,
~ spl11_24,
inference(avatar_split_clause,[],[f299,f459]) ).
fof(f480,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| member(X1,sF7) )
| ~ spl11_6 ),
inference(superposition,[],[f196,f347]) ).
fof(f483,definition,
( spl11_27
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| member(X1,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl11_27])],[avatar_definition]) ).
fof(f484,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| member(X1,sF7) )
| ~ spl11_27 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( spl11_27
| ~ spl11_6 ),
inference(avatar_split_clause,[],[f480,f345,f483]) ).
fof(f491,definition,
( spl11_28
<=> complement(sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl11_28])],[avatar_definition]) ).
fof(f493,plain,
( complement(sF4) = sF5
| ~ spl11_28 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f494,plain,
spl11_28,
inference(avatar_split_clause,[],[f288,f491]) ).
fof(f495,plain,
( ! [X0,X1] :
( member(X0,sF5)
| ~ member(X0,X1)
| member(X0,sF4) )
| ~ spl11_28 ),
inference(superposition,[],[f305,f493]) ).
fof(f498,definition,
( spl11_29
<=> ! [X0,X1] :
( member(X0,sF5)
| ~ member(X0,X1)
| member(X0,sF4) ) ),
introduced(definition,[new_symbols(definition,[spl11_29])],[avatar_definition]) ).
fof(f499,plain,
( ! [X0,X1] :
( member(X0,sF5)
| ~ member(X0,X1)
| member(X0,sF4) )
| ~ spl11_29 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( spl11_29
| ~ spl11_28 ),
inference(avatar_split_clause,[],[f495,f491,f498]) ).
fof(f520,plain,
( ! [X0] :
( ~ member(X0,x)
| ~ member(X0,sF6) )
| ~ spl11_12
| ~ spl11_13 ),
inference(resolution,[],[f391,f387]) ).
fof(f526,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,domain_of(X0))
| ~ member(X1,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f203,f1]) ).
fof(f527,plain,
! [X2,X0,X1] :
( member(X1,domain_of(X0))
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,X2) ),
inference(forward_subsumption_resolution,[],[f526,f4]) ).
fof(f537,definition,
( spl11_33
<=> ! [X0] :
( ~ member(X0,sF9)
| member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl11_33])],[avatar_definition]) ).
fof(f538,plain,
( ! [X0] :
( member(X0,element_relation)
| ~ member(X0,sF9) )
| ~ spl11_33 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f539,plain,
( spl11_33
| ~ spl11_7 ),
inference(avatar_split_clause,[],[f395,f350,f537]) ).
fof(f547,plain,
( ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl11_10 ),
inference(superposition,[],[f527,f372]) ).
fof(f562,definition,
( spl11_37
<=> ! [X0] :
( ~ member(X0,x)
| ~ member(X0,sF6) ) ),
introduced(definition,[new_symbols(definition,[spl11_37])],[avatar_definition]) ).
fof(f563,plain,
( ! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,x) )
| ~ spl11_37 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f564,plain,
( spl11_37
| ~ spl11_12
| ~ spl11_13 ),
inference(avatar_split_clause,[],[f520,f390,f386,f562]) ).
fof(f565,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF7),x)
| ~ member(not_subclass_element(X0,sF7),X1)
| subclass(X0,sF7) )
| ~ spl11_22
| ~ spl11_37 ),
inference(resolution,[],[f563,f444]) ).
fof(f569,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF7),x)
| subclass(X0,sF7) )
| ~ spl11_22
| ~ spl11_37 ),
inference(condensation,[],[f565]) ).
fof(f571,definition,
( spl11_38
<=> ! [X0] :
( ~ member(not_subclass_element(X0,sF7),x)
| subclass(X0,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl11_38])],[avatar_definition]) ).
fof(f572,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF7),x)
| subclass(X0,sF7) )
| ~ spl11_38 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f573,plain,
( spl11_38
| ~ spl11_22
| ~ spl11_37 ),
inference(avatar_split_clause,[],[f569,f562,f443,f571]) ).
fof(f574,plain,
( subclass(x,sF7)
| subclass(x,sF7)
| ~ spl11_38 ),
inference(resolution,[],[f572,f2]) ).
fof(f575,plain,
( ! [X0,X1] :
( subclass(X0,sF7)
| ~ member(not_subclass_element(X0,sF7),X1)
| ~ subclass(X1,x) )
| ~ spl11_38 ),
inference(resolution,[],[f572,f1]) ).
fof(f576,plain,
( subclass(x,sF7)
| ~ spl11_38 ),
inference(duplicate_literal_removal,[],[f574]) ).
fof(f583,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,x)
| ~ member(X0,universal_class) )
| ~ spl11_5 ),
inference(superposition,[],[f197,f342]) ).
fof(f592,definition,
( spl11_40
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,x)
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl11_40])],[avatar_definition]) ).
fof(f593,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,x)
| ~ member(X0,universal_class) )
| ~ spl11_40 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( spl11_40
| ~ spl11_5 ),
inference(avatar_split_clause,[],[f583,f340,f592]) ).
fof(f621,definition,
( spl11_44
<=> ! [X0,X1] :
( subclass(X0,sF7)
| ~ member(not_subclass_element(X0,sF7),X1)
| ~ subclass(X1,x) ) ),
introduced(definition,[new_symbols(definition,[spl11_44])],[avatar_definition]) ).
fof(f622,plain,
( ! [X0,X1] :
( subclass(X0,sF7)
| ~ member(not_subclass_element(X0,sF7),X1)
| ~ subclass(X1,x) )
| ~ spl11_44 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( spl11_44
| ~ spl11_38 ),
inference(avatar_split_clause,[],[f575,f571,f621]) ).
fof(f624,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF10,sF7),X0)
| ~ subclass(X0,x) )
| spl11_24
| ~ spl11_44 ),
inference(resolution,[],[f622,f461]) ).
fof(f626,definition,
( spl11_45
<=> ! [X0] :
( ~ member(not_subclass_element(sF10,sF7),X0)
| ~ subclass(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl11_45])],[avatar_definition]) ).
fof(f627,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF10,sF7),X0)
| ~ subclass(X0,x) )
| ~ spl11_45 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f628,plain,
( spl11_45
| spl11_24
| ~ spl11_44 ),
inference(avatar_split_clause,[],[f624,f621,f459,f626]) ).
fof(f706,plain,
( ! [X0] :
( ~ member(X0,sF4)
| x = X0
| x = X0 )
| ~ spl11_2 ),
inference(superposition,[],[f8,f324]) ).
fof(f707,plain,
( ! [X0] :
( ~ member(X0,sF4)
| x = X0 )
| ~ spl11_2 ),
inference(duplicate_literal_removal,[],[f706]) ).
fof(f709,definition,
( spl11_50
<=> ! [X0] :
( ~ member(X0,sF4)
| x = X0 ) ),
introduced(definition,[new_symbols(definition,[spl11_50])],[avatar_definition]) ).
fof(f710,plain,
( ! [X0] :
( ~ member(X0,sF4)
| x = X0 )
| ~ spl11_50 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( spl11_50
| ~ spl11_2 ),
inference(avatar_split_clause,[],[f707,f322,f709]) ).
fof(f736,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f781,definition,
( spl11_58
<=> ! [X0] : ~ member(not_subclass_element(sF10,sF7),X0) ),
introduced(definition,[new_symbols(definition,[spl11_58])],[avatar_definition]) ).
fof(f782,plain,
( ! [X0] : ~ member(not_subclass_element(sF10,sF7),X0)
| ~ spl11_58 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f829,plain,
( subclass(sF10,sF7)
| ~ spl11_58 ),
inference(resolution,[],[f782,f2]) ).
fof(f851,plain,
( $false
| spl11_24
| ~ spl11_58 ),
inference(forward_subsumption_resolution,[],[f829,f461]) ).
fof(f852,plain,
( spl11_24
| ~ spl11_58 ),
inference(avatar_contradiction_clause,[],[f851]) ).
fof(f900,plain,
! [X0,X1] :
( unordered_pair(X0,X1) = null_class
| regular(unordered_pair(X0,X1)) = X0
| regular(unordered_pair(X0,X1)) = X1 ),
inference(resolution,[],[f68,f8]) ).
fof(f902,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f903,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f1009,plain,
! [X2,X0,X1] :
( intersection(X0,cross_product(X1,X2)) = null_class
| regular(intersection(X0,cross_product(X1,X2))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),first(regular(intersection(X0,cross_product(X1,X2))))),unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),unordered_pair(second(regular(intersection(X0,cross_product(X1,X2)))),second(regular(intersection(X0,cross_product(X1,X2))))))) ),
inference(resolution,[],[f902,f198]) ).
fof(f1026,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(superposition,[],[f202,f1009]) ).
fof(f1034,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(trivial_inequality_removal,[],[f1026]) ).
fof(f1044,plain,
( ! [X0] :
( ~ member(X0,sF10)
| regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl11_9 ),
inference(superposition,[],[f1034,f365]) ).
fof(f1050,definition,
( spl11_66
<=> ! [X0] :
( ~ member(X0,sF10)
| regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl11_66])],[avatar_definition]) ).
fof(f1051,plain,
( ! [X0] :
( ~ member(X0,sF10)
| regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl11_66 ),
inference(avatar_component_clause,[],[f1050]) ).
fof(f1052,plain,
( spl11_66
| ~ spl11_9 ),
inference(avatar_split_clause,[],[f1044,f363,f1050]) ).
fof(f1055,plain,
( ! [X0] :
( regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))))))
| subclass(sF10,X0) )
| ~ spl11_66 ),
inference(resolution,[],[f1051,f2]) ).
fof(f1060,definition,
( spl11_67
<=> ! [X0] :
( regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))))))
| subclass(sF10,X0) ) ),
introduced(definition,[new_symbols(definition,[spl11_67])],[avatar_definition]) ).
fof(f1061,plain,
( ! [X0] :
( subclass(sF10,X0)
| regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,X0),not_subclass_element(sF10,X0)),universal_class))))))) )
| ~ spl11_67 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1062,plain,
( spl11_67
| ~ spl11_66 ),
inference(avatar_split_clause,[],[f1055,f1050,f1060]) ).
fof(f1063,plain,
( regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))))))
| spl11_24
| ~ spl11_67 ),
inference(resolution,[],[f1061,f461]) ).
fof(f1066,definition,
( spl11_68
<=> regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl11_68])],[avatar_definition]) ).
fof(f1068,plain,
( regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))),unordered_pair(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))))))
| ~ spl11_68 ),
inference(avatar_component_clause,[],[f1066]) ).
fof(f1069,plain,
( spl11_68
| spl11_24
| ~ spl11_67 ),
inference(avatar_split_clause,[],[f1063,f1060,f459,f1066]) ).
fof(f1076,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0) )
| ~ spl11_68 ),
inference(superposition,[],[f195,f1068]) ).
fof(f1077,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X1) )
| ~ spl11_68 ),
inference(superposition,[],[f196,f1068]) ).
fof(f1079,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation)
| member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))))
| ~ spl11_68 ),
inference(superposition,[],[f199,f1068]) ).
fof(f1080,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF8)
| member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF7)
| ~ spl11_27
| ~ spl11_68 ),
inference(superposition,[],[f484,f1068]) ).
fof(f1084,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF0)
| ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),x)
| ~ member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| ~ spl11_40
| ~ spl11_68 ),
inference(superposition,[],[f593,f1068]) ).
fof(f1096,definition,
( spl11_69
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),x) ),
introduced(definition,[new_symbols(definition,[spl11_69])],[avatar_definition]) ).
fof(f1097,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),x)
| spl11_69 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1100,definition,
( spl11_70
<=> member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF0) ),
introduced(definition,[new_symbols(definition,[spl11_70])],[avatar_definition]) ).
fof(f1101,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF0)
| ~ spl11_70 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1105,definition,
( spl11_71
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF7) ),
introduced(definition,[new_symbols(definition,[spl11_71])],[avatar_definition]) ).
fof(f1107,plain,
( member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF7)
| ~ spl11_71 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1109,definition,
( spl11_72
<=> member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF8) ),
introduced(definition,[new_symbols(definition,[spl11_72])],[avatar_definition]) ).
fof(f1110,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF8)
| ~ spl11_72 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1111,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF8)
| spl11_72 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1112,plain,
( spl11_71
| ~ spl11_72
| ~ spl11_27
| ~ spl11_68 ),
inference(avatar_split_clause,[],[f1080,f1066,f483,f1109,f1105]) ).
fof(f1114,definition,
( spl11_73
<=> member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl11_73])],[avatar_definition]) ).
fof(f1115,plain,
( ~ member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| spl11_73 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1119,definition,
( spl11_74
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl11_74])],[avatar_definition]) ).
fof(f1120,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0) )
| ~ spl11_74 ),
inference(avatar_component_clause,[],[f1119]) ).
fof(f1121,plain,
( spl11_74
| ~ spl11_68 ),
inference(avatar_split_clause,[],[f1076,f1066,f1119]) ).
fof(f1122,plain,
( ~ spl11_73
| ~ spl11_69
| spl11_70
| ~ spl11_40
| ~ spl11_68 ),
inference(avatar_split_clause,[],[f1084,f1066,f592,f1100,f1096,f1114]) ).
fof(f1127,plain,
( member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ spl11_74 ),
inference(resolution,[],[f1120,f902]) ).
fof(f1131,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF8)
| member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| ~ spl11_6
| ~ spl11_74 ),
inference(superposition,[],[f1120,f347]) ).
fof(f1135,definition,
( spl11_75
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X1) ) ),
introduced(definition,[new_symbols(definition,[spl11_75])],[avatar_definition]) ).
fof(f1136,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X1) )
| ~ spl11_75 ),
inference(avatar_component_clause,[],[f1135]) ).
fof(f1137,plain,
( spl11_75
| ~ spl11_68 ),
inference(avatar_split_clause,[],[f1077,f1066,f1135]) ).
fof(f1138,plain,
( member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ spl11_75 ),
inference(resolution,[],[f1136,f902]) ).
fof(f1148,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF6)
| ~ spl11_23
| ~ spl11_71 ),
inference(resolution,[],[f1107,f448]) ).
fof(f1158,definition,
( spl11_76
<=> member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))) ),
introduced(definition,[new_symbols(definition,[spl11_76])],[avatar_definition]) ).
fof(f1160,plain,
( member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))))
| ~ spl11_76 ),
inference(avatar_component_clause,[],[f1158]) ).
fof(f1162,definition,
( spl11_77
<=> member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation) ),
introduced(definition,[new_symbols(definition,[spl11_77])],[avatar_definition]) ).
fof(f1163,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation)
| ~ spl11_77 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1164,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation)
| spl11_77 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1165,plain,
( spl11_76
| ~ spl11_77
| ~ spl11_68 ),
inference(avatar_split_clause,[],[f1079,f1066,f1162,f1158]) ).
fof(f1173,definition,
( spl11_78
<=> not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))) ),
introduced(definition,[new_symbols(definition,[spl11_78])],[avatar_definition]) ).
fof(f1174,plain,
( not_subclass_element(sF10,sF7) != regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| spl11_78 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1175,plain,
( not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| ~ spl11_78 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1183,plain,
( null_class = intersection(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),not_subclass_element(sF10,sF7))
| null_class = unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))
| ~ spl11_78 ),
inference(superposition,[],[f70,f1175]) ).
fof(f1198,definition,
( spl11_81
<=> null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl11_81])],[avatar_definition]) ).
fof(f1199,plain,
( null_class != intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| spl11_81 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1200,plain,
( null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ spl11_81 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1202,definition,
( spl11_82
<=> member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))) ),
introduced(definition,[new_symbols(definition,[spl11_82])],[avatar_definition]) ).
fof(f1204,plain,
( member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| ~ spl11_82 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1205,plain,
( spl11_81
| spl11_82
| ~ spl11_74 ),
inference(avatar_split_clause,[],[f1127,f1119,f1202,f1198]) ).
fof(f1217,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF10,sF7),domain_of(sF9))
| ~ spl11_81 ),
inference(superposition,[],[f202,f1200]) ).
fof(f1223,plain,
( ~ member(not_subclass_element(sF10,sF7),domain_of(sF9))
| ~ spl11_81 ),
inference(trivial_inequality_removal,[],[f1217]) ).
fof(f1225,plain,
( ~ member(not_subclass_element(sF10,sF7),sF10)
| ~ spl11_9
| ~ spl11_81 ),
inference(forward_demodulation,[],[f1223,f365]) ).
fof(f1227,definition,
( spl11_83
<=> member(not_subclass_element(sF10,sF7),sF10) ),
introduced(definition,[new_symbols(definition,[spl11_83])],[avatar_definition]) ).
fof(f1229,plain,
( ~ member(not_subclass_element(sF10,sF7),sF10)
| spl11_83 ),
inference(avatar_component_clause,[],[f1227]) ).
fof(f1230,plain,
( ~ spl11_83
| ~ spl11_9
| ~ spl11_81 ),
inference(avatar_split_clause,[],[f1225,f1198,f363,f1227]) ).
fof(f1232,plain,
( subclass(sF10,sF7)
| spl11_83 ),
inference(resolution,[],[f1229,f2]) ).
fof(f1236,plain,
( $false
| spl11_24
| spl11_83 ),
inference(forward_subsumption_resolution,[],[f1232,f461]) ).
fof(f1237,plain,
( spl11_24
| spl11_83 ),
inference(avatar_contradiction_clause,[],[f1236]) ).
fof(f1238,plain,
( member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| ~ spl11_75
| spl11_81 ),
inference(forward_subsumption_resolution,[],[f1138,f1199]) ).
fof(f1239,plain,
( not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| ~ spl11_82 ),
inference(resolution,[],[f1204,f8]) ).
fof(f1243,plain,
( not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| ~ spl11_82 ),
inference(duplicate_literal_removal,[],[f1239]) ).
fof(f1248,definition,
( spl11_84
<=> not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl11_84])],[avatar_definition]) ).
fof(f1250,plain,
( not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| ~ spl11_84 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1251,plain,
( spl11_84
| ~ spl11_82 ),
inference(avatar_split_clause,[],[f1243,f1202,f1248]) ).
fof(f1260,definition,
( spl11_85
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF6) ),
introduced(definition,[new_symbols(definition,[spl11_85])],[avatar_definition]) ).
fof(f1262,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF6)
| spl11_85 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1263,plain,
( ~ spl11_85
| ~ spl11_23
| ~ spl11_71 ),
inference(avatar_split_clause,[],[f1148,f1105,f447,f1260]) ).
fof(f1264,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF5)
| ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF3)
| ~ spl11_4
| spl11_85 ),
inference(resolution,[],[f1262,f337]) ).
fof(f1270,definition,
( spl11_86
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl11_86])],[avatar_definition]) ).
fof(f1272,plain,
( member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| ~ spl11_86 ),
inference(avatar_component_clause,[],[f1270]) ).
fof(f1273,plain,
( spl11_86
| ~ spl11_75
| spl11_81 ),
inference(avatar_split_clause,[],[f1238,f1198,f1135,f1270]) ).
fof(f1282,definition,
( spl11_87
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF3) ),
introduced(definition,[new_symbols(definition,[spl11_87])],[avatar_definition]) ).
fof(f1284,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF3)
| spl11_87 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1286,definition,
( spl11_88
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF5) ),
introduced(definition,[new_symbols(definition,[spl11_88])],[avatar_definition]) ).
fof(f1288,plain,
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF5)
| spl11_88 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1289,plain,
( ~ spl11_87
| ~ spl11_88
| ~ spl11_4
| spl11_85 ),
inference(avatar_split_clause,[],[f1264,f1260,f336,f1286,f1282]) ).
fof(f1290,plain,
( ! [X0] :
( ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0)
| member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF4) )
| ~ spl11_29
| spl11_88 ),
inference(resolution,[],[f1288,f499]) ).
fof(f1379,definition,
( spl11_97
<=> member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF4) ),
introduced(definition,[new_symbols(definition,[spl11_97])],[avatar_definition]) ).
fof(f1381,plain,
( member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),sF4)
| ~ spl11_97 ),
inference(avatar_component_clause,[],[f1379]) ).
fof(f1383,definition,
( spl11_98
<=> ! [X0] : ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0) ),
introduced(definition,[new_symbols(definition,[spl11_98])],[avatar_definition]) ).
fof(f1384,plain,
( ! [X0] : ~ member(second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),X0)
| ~ spl11_98 ),
inference(avatar_component_clause,[],[f1383]) ).
fof(f1385,plain,
( spl11_97
| spl11_98
| ~ spl11_29
| spl11_88 ),
inference(avatar_split_clause,[],[f1290,f1286,f498,f1383,f1379]) ).
fof(f1386,plain,
( x = second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| ~ spl11_50
| ~ spl11_97 ),
inference(resolution,[],[f1381,f710]) ).
fof(f1391,definition,
( spl11_99
<=> x = second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl11_99])],[avatar_definition]) ).
fof(f1393,plain,
( x = second(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))))
| ~ spl11_99 ),
inference(avatar_component_clause,[],[f1391]) ).
fof(f1394,plain,
( spl11_99
| ~ spl11_50
| ~ spl11_97 ),
inference(avatar_split_clause,[],[f1386,f1379,f709,f1391]) ).
fof(f1400,plain,
( member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),x)
| ~ spl11_76
| ~ spl11_99 ),
inference(superposition,[],[f1160,f1393]) ).
fof(f1408,plain,
( member(not_subclass_element(sF10,sF7),x)
| ~ spl11_76
| ~ spl11_84
| ~ spl11_99 ),
inference(forward_demodulation,[],[f1400,f1250]) ).
fof(f1412,definition,
( spl11_100
<=> member(not_subclass_element(sF10,sF7),x) ),
introduced(definition,[new_symbols(definition,[spl11_100])],[avatar_definition]) ).
fof(f1413,plain,
( ~ member(not_subclass_element(sF10,sF7),x)
| spl11_100 ),
inference(avatar_component_clause,[],[f1412]) ).
fof(f1414,plain,
( member(not_subclass_element(sF10,sF7),x)
| ~ spl11_100 ),
inference(avatar_component_clause,[],[f1412]) ).
fof(f1415,plain,
( spl11_100
| ~ spl11_76
| ~ spl11_84
| ~ spl11_99 ),
inference(avatar_split_clause,[],[f1408,f1391,f1248,f1158,f1412]) ).
fof(f1419,plain,
( ~ subclass(x,sF7)
| subclass(sF10,sF7)
| ~ spl11_100 ),
inference(resolution,[],[f1414,f304]) ).
fof(f1421,plain,
( subclass(sF10,sF7)
| ~ spl11_38
| ~ spl11_100 ),
inference(forward_subsumption_resolution,[],[f1419,f576]) ).
fof(f1426,plain,
( $false
| spl11_24
| ~ spl11_38
| ~ spl11_100 ),
inference(forward_subsumption_resolution,[],[f1421,f461]) ).
fof(f1427,plain,
( spl11_24
| ~ spl11_38
| ~ spl11_100 ),
inference(avatar_contradiction_clause,[],[f1426]) ).
fof(f1447,plain,
( $false
| ~ spl11_21
| ~ spl11_86
| ~ spl11_98 ),
inference(unit_resulting_resolution,[],[f439,f1272,f1384,f1384]) ).
fof(f1494,plain,
( ~ spl11_21
| ~ spl11_86
| ~ spl11_98 ),
inference(avatar_contradiction_clause,[],[f1447]) ).
fof(f1516,definition,
( spl11_101
<=> null_class = unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)) ),
introduced(definition,[new_symbols(definition,[spl11_101])],[avatar_definition]) ).
fof(f1517,plain,
( null_class != unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))
| spl11_101 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1518,plain,
( null_class = unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))
| ~ spl11_101 ),
inference(avatar_component_clause,[],[f1516]) ).
fof(f1520,definition,
( spl11_102
<=> null_class = intersection(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),not_subclass_element(sF10,sF7)) ),
introduced(definition,[new_symbols(definition,[spl11_102])],[avatar_definition]) ).
fof(f1522,plain,
( null_class = intersection(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),not_subclass_element(sF10,sF7))
| ~ spl11_102 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1523,plain,
( spl11_101
| spl11_102
| ~ spl11_78 ),
inference(avatar_split_clause,[],[f1183,f1173,f1520,f1516]) ).
fof(f1535,plain,
( member(first(regular(intersection(sF9,cross_product(null_class,universal_class)))),null_class)
| ~ spl11_82
| ~ spl11_101 ),
inference(superposition,[],[f1204,f1518]) ).
fof(f1536,plain,
( not_subclass_element(sF10,sF7) = first(regular(intersection(sF9,cross_product(null_class,universal_class))))
| ~ spl11_84
| ~ spl11_101 ),
inference(superposition,[],[f1250,f1518]) ).
fof(f1573,plain,
( member(not_subclass_element(sF10,sF7),null_class)
| ~ spl11_82
| ~ spl11_84
| ~ spl11_101 ),
inference(forward_demodulation,[],[f1535,f1536]) ).
fof(f1596,definition,
( spl11_105
<=> ! [X0] :
( ~ member(X0,null_class)
| not_subclass_element(sF10,sF7) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl11_105])],[avatar_definition]) ).
fof(f1597,plain,
( ! [X0] :
( ~ member(X0,null_class)
| not_subclass_element(sF10,sF7) = X0 )
| ~ spl11_105 ),
inference(avatar_component_clause,[],[f1596]) ).
fof(f1629,definition,
( spl11_108
<=> member(not_subclass_element(sF10,sF7),null_class) ),
introduced(definition,[new_symbols(definition,[spl11_108])],[avatar_definition]) ).
fof(f1630,plain,
( ~ member(not_subclass_element(sF10,sF7),null_class)
| spl11_108 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1631,plain,
( member(not_subclass_element(sF10,sF7),null_class)
| ~ spl11_108 ),
inference(avatar_component_clause,[],[f1629]) ).
fof(f1632,plain,
( spl11_108
| ~ spl11_82
| ~ spl11_84
| ~ spl11_101 ),
inference(avatar_split_clause,[],[f1573,f1516,f1248,f1202,f1629]) ).
fof(f1672,definition,
( spl11_111
<=> ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl11_111])],[avatar_definition]) ).
fof(f1673,plain,
( ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl11_111 ),
inference(avatar_component_clause,[],[f1672]) ).
fof(f1674,plain,
( spl11_111
| ~ spl11_10 ),
inference(avatar_split_clause,[],[f547,f370,f1672]) ).
fof(f2044,definition,
( spl11_138
<=> member(not_subclass_element(sF10,sF7),sF0) ),
introduced(definition,[new_symbols(definition,[spl11_138])],[avatar_definition]) ).
fof(f2557,plain,
( ! [X0] :
( member(not_subclass_element(sF10,sF7),X0)
| null_class = X0 )
| ~ spl11_108 ),
inference(resolution,[],[f736,f1631]) ).
fof(f2564,definition,
( spl11_173
<=> ! [X0] :
( member(not_subclass_element(sF10,sF7),X0)
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl11_173])],[avatar_definition]) ).
fof(f2565,plain,
( ! [X0] :
( member(not_subclass_element(sF10,sF7),X0)
| null_class = X0 )
| ~ spl11_173 ),
inference(avatar_component_clause,[],[f2564]) ).
fof(f2566,plain,
( spl11_173
| ~ spl11_108 ),
inference(avatar_split_clause,[],[f2557,f1629,f2564]) ).
fof(f2568,plain,
( null_class = sF7
| subclass(sF10,sF7)
| ~ spl11_173 ),
inference(resolution,[],[f2565,f3]) ).
fof(f2570,plain,
( null_class = x
| spl11_100
| ~ spl11_173 ),
inference(resolution,[],[f2565,f1413]) ).
fof(f2599,plain,
( null_class = sF7
| spl11_24
| ~ spl11_173 ),
inference(forward_subsumption_resolution,[],[f2568,f461]) ).
fof(f2605,definition,
( spl11_174
<=> null_class = sF7 ),
introduced(definition,[new_symbols(definition,[spl11_174])],[avatar_definition]) ).
fof(f2607,plain,
( null_class = sF7
| ~ spl11_174 ),
inference(avatar_component_clause,[],[f2605]) ).
fof(f2608,plain,
( spl11_174
| spl11_24
| ~ spl11_173 ),
inference(avatar_split_clause,[],[f2599,f2564,f459,f2605]) ).
fof(f2651,plain,
( ~ member(not_subclass_element(sF10,null_class),x)
| spl11_100
| ~ spl11_174 ),
inference(superposition,[],[f1413,f2607]) ).
fof(f2656,plain,
( member(not_subclass_element(sF10,null_class),null_class)
| ~ spl11_108
| ~ spl11_174 ),
inference(superposition,[],[f1631,f2607]) ).
fof(f2686,plain,
( ~ member(not_subclass_element(sF10,null_class),null_class)
| spl11_100
| ~ spl11_173
| ~ spl11_174 ),
inference(forward_demodulation,[],[f2651,f2570]) ).
fof(f2720,plain,
( $false
| spl11_100
| ~ spl11_108
| ~ spl11_173
| ~ spl11_174 ),
inference(forward_subsumption_resolution,[],[f2686,f2656]) ).
fof(f2721,plain,
( spl11_100
| ~ spl11_108
| ~ spl11_173
| ~ spl11_174 ),
inference(avatar_contradiction_clause,[],[f2720]) ).
fof(f2736,plain,
( ~ member(not_subclass_element(sF10,sF7),universal_class)
| spl11_73
| ~ spl11_84 ),
inference(forward_demodulation,[],[f1115,f1250]) ).
fof(f2853,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF9)
| ~ spl11_15
| spl11_72 ),
inference(resolution,[],[f1111,f403]) ).
fof(f2866,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF9)
| ~ spl11_33
| spl11_77 ),
inference(resolution,[],[f1164,f538]) ).
fof(f3096,plain,
( null_class != null_class
| not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| spl11_101 ),
inference(superposition,[],[f1517,f900]) ).
fof(f3097,plain,
( null_class != null_class
| not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| spl11_101 ),
inference(duplicate_literal_removal,[],[f3096]) ).
fof(f3098,plain,
( not_subclass_element(sF10,sF7) = regular(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| spl11_101 ),
inference(trivial_inequality_removal,[],[f3097]) ).
fof(f3100,plain,
( $false
| spl11_78
| spl11_101 ),
inference(forward_subsumption_resolution,[],[f3098,f1174]) ).
fof(f3101,plain,
( spl11_78
| spl11_101 ),
inference(avatar_contradiction_clause,[],[f3100]) ).
fof(f3121,definition,
( spl11_178
<=> member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1) ),
introduced(definition,[new_symbols(definition,[spl11_178])],[avatar_definition]) ).
fof(f3122,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| ~ spl11_178 ),
inference(avatar_component_clause,[],[f3121]) ).
fof(f3123,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| spl11_178 ),
inference(avatar_component_clause,[],[f3121]) ).
fof(f3126,definition,
( spl11_179
<=> member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF9) ),
introduced(definition,[new_symbols(definition,[spl11_179])],[avatar_definition]) ).
fof(f3127,plain,
( member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF9)
| ~ spl11_179 ),
inference(avatar_component_clause,[],[f3126]) ).
fof(f3128,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF9)
| spl11_179 ),
inference(avatar_component_clause,[],[f3126]) ).
fof(f3129,plain,
( ~ spl11_179
| ~ spl11_15
| spl11_72 ),
inference(avatar_split_clause,[],[f2853,f1109,f402,f3126]) ).
fof(f3130,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF0)
| ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation)
| ~ spl11_18
| spl11_178 ),
inference(resolution,[],[f3123,f418]) ).
fof(f3138,plain,
( null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| spl11_179 ),
inference(resolution,[],[f3128,f903]) ).
fof(f3147,plain,
( $false
| spl11_81
| spl11_179 ),
inference(forward_subsumption_resolution,[],[f3138,f1199]) ).
fof(f3148,plain,
( spl11_81
| spl11_179 ),
inference(avatar_contradiction_clause,[],[f3147]) ).
fof(f3150,plain,
( member(first(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))),universal_class)
| ~ spl11_6
| ~ spl11_72
| ~ spl11_74 ),
inference(forward_subsumption_resolution,[],[f1131,f1110]) ).
fof(f3153,plain,
( $false
| ~ spl11_33
| spl11_77
| ~ spl11_179 ),
inference(forward_subsumption_resolution,[],[f2866,f3127]) ).
fof(f3154,plain,
( ~ spl11_33
| spl11_77
| ~ spl11_179 ),
inference(avatar_contradiction_clause,[],[f3153]) ).
fof(f3156,plain,
( member(not_subclass_element(sF10,sF7),universal_class)
| ~ spl11_6
| ~ spl11_72
| ~ spl11_74
| ~ spl11_84 ),
inference(forward_demodulation,[],[f3150,f1250]) ).
fof(f3163,plain,
( $false
| ~ spl11_6
| ~ spl11_72
| spl11_73
| ~ spl11_74
| ~ spl11_84 ),
inference(forward_subsumption_resolution,[],[f3156,f2736]) ).
fof(f3164,plain,
( ~ spl11_6
| ~ spl11_72
| spl11_73
| ~ spl11_74
| ~ spl11_84 ),
inference(avatar_contradiction_clause,[],[f3163]) ).
fof(f3195,plain,
( $false
| ~ spl11_17
| spl11_69
| ~ spl11_86
| spl11_87 ),
inference(unit_resulting_resolution,[],[f411,f1272,f1284,f1097]) ).
fof(f3201,plain,
( ~ spl11_17
| spl11_69
| ~ spl11_86
| spl11_87 ),
inference(avatar_contradiction_clause,[],[f3195]) ).
fof(f3204,plain,
( ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation)
| ~ spl11_18
| ~ spl11_70
| spl11_178 ),
inference(forward_subsumption_resolution,[],[f3130,f1101]) ).
fof(f3206,plain,
( $false
| ~ spl11_18
| ~ spl11_70
| ~ spl11_77
| spl11_178 ),
inference(forward_subsumption_resolution,[],[f3204,f1163]) ).
fof(f3207,plain,
( ~ spl11_18
| ~ spl11_70
| ~ spl11_77
| spl11_178 ),
inference(avatar_contradiction_clause,[],[f3206]) ).
fof(f3271,plain,
( ! [X0] :
( ~ member(X0,null_class)
| member(X0,unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))) )
| ~ spl11_102 ),
inference(superposition,[],[f21,f1522]) ).
fof(f3737,definition,
( spl11_184
<=> ! [X0] :
( ~ member(X0,null_class)
| member(X0,unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7))) ) ),
introduced(definition,[new_symbols(definition,[spl11_184])],[avatar_definition]) ).
fof(f3738,plain,
( ! [X0] :
( member(X0,unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)))
| ~ member(X0,null_class) )
| ~ spl11_184 ),
inference(avatar_component_clause,[],[f3737]) ).
fof(f3739,plain,
( spl11_184
| ~ spl11_102 ),
inference(avatar_split_clause,[],[f3271,f1520,f3737]) ).
fof(f3852,plain,
( ! [X0] :
( ~ member(X0,null_class)
| not_subclass_element(sF10,sF7) = X0
| not_subclass_element(sF10,sF7) = X0 )
| ~ spl11_184 ),
inference(resolution,[],[f3738,f8]) ).
fof(f3859,plain,
( ! [X0] :
( ~ member(X0,null_class)
| not_subclass_element(sF10,sF7) = X0 )
| ~ spl11_184 ),
inference(duplicate_literal_removal,[],[f3852]) ).
fof(f3860,plain,
( spl11_105
| ~ spl11_184 ),
inference(avatar_split_clause,[],[f3859,f3737,f1596]) ).
fof(f5076,plain,
( ! [X0] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ member(not_subclass_element(sF10,sF7),X0)
| ~ subclass(sF2,x) )
| ~ spl11_45
| ~ spl11_111 ),
inference(resolution,[],[f1673,f627]) ).
fof(f5085,plain,
( ! [X0] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ member(not_subclass_element(sF10,sF7),X0) )
| ~ spl11_3
| ~ spl11_45
| ~ spl11_111 ),
inference(forward_subsumption_resolution,[],[f5076,f329]) ).
fof(f5089,definition,
( spl11_260
<=> null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl11_260])],[avatar_definition]) ).
fof(f5091,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ spl11_260 ),
inference(avatar_component_clause,[],[f5089]) ).
fof(f5092,plain,
( spl11_58
| spl11_260
| ~ spl11_3
| ~ spl11_45
| ~ spl11_111 ),
inference(avatar_split_clause,[],[f5085,f1672,f626,f327,f5089,f781]) ).
fof(f5098,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ member(X0,sF1) )
| ~ spl11_260 ),
inference(superposition,[],[f23,f5091]) ).
fof(f5113,definition,
( spl11_262
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl11_262])],[avatar_definition]) ).
fof(f5114,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| member(X0,null_class)
| ~ member(X0,sF1) )
| ~ spl11_262 ),
inference(avatar_component_clause,[],[f5113]) ).
fof(f5115,plain,
( spl11_262
| ~ spl11_260 ),
inference(avatar_split_clause,[],[f5098,f5089,f5113]) ).
fof(f5124,plain,
( ! [X0] :
( member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),null_class)
| ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)) )
| ~ spl11_262 ),
inference(resolution,[],[f5114,f902]) ).
fof(f5440,definition,
( spl11_277
<=> member(not_subclass_element(sF10,sF7),element_relation) ),
introduced(definition,[new_symbols(definition,[spl11_277])],[avatar_definition]) ).
fof(f5447,definition,
( spl11_278
<=> member(not_subclass_element(sF10,sF7),sF1) ),
introduced(definition,[new_symbols(definition,[spl11_278])],[avatar_definition]) ).
fof(f5448,plain,
( member(not_subclass_element(sF10,sF7),sF1)
| ~ spl11_278 ),
inference(avatar_component_clause,[],[f5447]) ).
fof(f5449,plain,
( ~ member(not_subclass_element(sF10,sF7),sF1)
| spl11_278 ),
inference(avatar_component_clause,[],[f5447]) ).
fof(f5451,plain,
( ~ member(not_subclass_element(sF10,sF7),sF0)
| ~ member(not_subclass_element(sF10,sF7),element_relation)
| ~ spl11_18
| spl11_278 ),
inference(resolution,[],[f5449,f418]) ).
fof(f5453,plain,
( ~ spl11_277
| ~ spl11_138
| ~ spl11_18
| spl11_278 ),
inference(avatar_split_clause,[],[f5451,f5447,f417,f2044,f5440]) ).
fof(f5528,definition,
( spl11_283
<=> ! [X0] :
( member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),null_class)
| ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)) ) ),
introduced(definition,[new_symbols(definition,[spl11_283])],[avatar_definition]) ).
fof(f5529,plain,
( ! [X0] :
( member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),null_class)
| ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)) )
| ~ spl11_283 ),
inference(avatar_component_clause,[],[f5528]) ).
fof(f5530,plain,
( spl11_283
| ~ spl11_262 ),
inference(avatar_split_clause,[],[f5124,f5113,f5528]) ).
fof(f5533,plain,
( ! [X0] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| not_subclass_element(sF10,sF7) = regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) )
| ~ spl11_105
| ~ spl11_283 ),
inference(resolution,[],[f5529,f1597]) ).
fof(f5594,definition,
( spl11_289
<=> ! [X0] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| not_subclass_element(sF10,sF7) = regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) ) ),
introduced(definition,[new_symbols(definition,[spl11_289])],[avatar_definition]) ).
fof(f5595,plain,
( ! [X0] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF1)
| null_class = intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| not_subclass_element(sF10,sF7) = regular(intersection(X0,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) )
| ~ spl11_289 ),
inference(avatar_component_clause,[],[f5594]) ).
fof(f5596,plain,
( spl11_289
| ~ spl11_105
| ~ spl11_283 ),
inference(avatar_split_clause,[],[f5533,f5528,f1596,f5594]) ).
fof(f5597,plain,
( null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| not_subclass_element(sF10,sF7) = regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))
| ~ spl11_178
| ~ spl11_289 ),
inference(resolution,[],[f5595,f3122]) ).
fof(f5612,plain,
( not_subclass_element(sF10,sF7) = regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))
| spl11_81
| ~ spl11_178
| ~ spl11_289 ),
inference(forward_subsumption_resolution,[],[f5597,f1199]) ).
fof(f5615,definition,
( spl11_290
<=> not_subclass_element(sF10,sF7) = regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))) ),
introduced(definition,[new_symbols(definition,[spl11_290])],[avatar_definition]) ).
fof(f5617,plain,
( not_subclass_element(sF10,sF7) = regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))
| ~ spl11_290 ),
inference(avatar_component_clause,[],[f5615]) ).
fof(f5618,plain,
( spl11_290
| spl11_81
| ~ spl11_178
| ~ spl11_289 ),
inference(avatar_split_clause,[],[f5612,f5594,f3121,f1198,f5615]) ).
fof(f5626,plain,
( not_subclass_element(sF10,sF7) != regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))
| member(not_subclass_element(sF10,sF7),element_relation)
| ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),element_relation) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f5819,plain,
( member(not_subclass_element(sF10,sF7),null_class)
| ~ member(not_subclass_element(sF10,sF7),sF1)
| null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| ~ spl11_283
| ~ spl11_290 ),
inference(superposition,[],[f5529,f5617]) ).
fof(f5828,plain,
( ~ member(not_subclass_element(sF10,sF7),sF1)
| null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| spl11_108
| ~ spl11_283
| ~ spl11_290 ),
inference(forward_subsumption_resolution,[],[f5819,f1630]) ).
fof(f5831,plain,
( null_class = intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))
| spl11_108
| ~ spl11_278
| ~ spl11_283
| ~ spl11_290 ),
inference(forward_subsumption_resolution,[],[f5828,f5448]) ).
fof(f5832,plain,
( $false
| spl11_81
| spl11_108
| ~ spl11_278
| ~ spl11_283
| ~ spl11_290 ),
inference(forward_subsumption_resolution,[],[f5831,f1199]) ).
fof(f5833,plain,
( spl11_81
| spl11_108
| ~ spl11_278
| ~ spl11_283
| ~ spl11_290 ),
inference(avatar_contradiction_clause,[],[f5832]) ).
fof(f5835,plain,
( not_subclass_element(sF10,sF7) != regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class)))
| member(not_subclass_element(sF10,sF7),sF0)
| ~ member(regular(intersection(sF9,cross_product(unordered_pair(not_subclass_element(sF10,sF7),not_subclass_element(sF10,sF7)),universal_class))),sF0) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s158,plain,
spl11_1,
inference(sat_conversion,[],[f318]) ).
cnf(s162,plain,
spl11_2,
inference(sat_conversion,[],[f325]) ).
cnf(s164,plain,
spl11_3,
inference(sat_conversion,[],[f330]) ).
cnf(s168,plain,
( ~ spl11_1
| spl11_4 ),
inference(sat_conversion,[],[f338]) ).
cnf(s170,plain,
spl11_5,
inference(sat_conversion,[],[f343]) ).
cnf(s172,plain,
spl11_6,
inference(sat_conversion,[],[f348]) ).
cnf(s174,plain,
spl11_7,
inference(sat_conversion,[],[f353]) ).
cnf(s176,plain,
spl11_8,
inference(sat_conversion,[],[f358]) ).
cnf(s181,plain,
spl11_9,
inference(sat_conversion,[],[f366]) ).
cnf(s185,plain,
spl11_10,
inference(sat_conversion,[],[f373]) ).
cnf(s190,plain,
spl11_11,
inference(sat_conversion,[],[f382]) ).
cnf(s194,plain,
( ~ spl11_1
| spl11_12 ),
inference(sat_conversion,[],[f388]) ).
cnf(s196,plain,
( ~ spl11_11
| spl11_13 ),
inference(sat_conversion,[],[f392]) ).
cnf(s204,plain,
( ~ spl11_7
| spl11_15 ),
inference(sat_conversion,[],[f404]) ).
cnf(s208,plain,
( ~ spl11_11
| spl11_17 ),
inference(sat_conversion,[],[f412]) ).
cnf(s213,plain,
( ~ spl11_8
| spl11_18 ),
inference(sat_conversion,[],[f419]) ).
cnf(s223,plain,
spl11_20,
inference(sat_conversion,[],[f434]) ).
cnf(s227,plain,
( ~ spl11_20
| spl11_21 ),
inference(sat_conversion,[],[f440]) ).
cnf(s230,plain,
( ~ spl11_21
| spl11_22 ),
inference(sat_conversion,[],[f445]) ).
cnf(s232,plain,
( ~ spl11_20
| spl11_23 ),
inference(sat_conversion,[],[f449]) ).
cnf(s241,plain,
~ spl11_24,
inference(sat_conversion,[],[f462]) ).
cnf(s255,plain,
( ~ spl11_6
| spl11_27 ),
inference(sat_conversion,[],[f485]) ).
cnf(s261,plain,
spl11_28,
inference(sat_conversion,[],[f494]) ).
cnf(s265,plain,
( ~ spl11_28
| spl11_29 ),
inference(sat_conversion,[],[f500]) ).
cnf(s290,plain,
( ~ spl11_7
| spl11_33 ),
inference(sat_conversion,[],[f539]) ).
cnf(s306,plain,
( ~ spl11_12
| ~ spl11_13
| spl11_37 ),
inference(sat_conversion,[],[f564]) ).
cnf(s311,plain,
( ~ spl11_22
| ~ spl11_37
| spl11_38 ),
inference(sat_conversion,[],[f573]) ).
cnf(s324,plain,
( ~ spl11_5
| spl11_40 ),
inference(sat_conversion,[],[f594]) ).
cnf(s339,plain,
( ~ spl11_38
| spl11_44 ),
inference(sat_conversion,[],[f623]) ).
cnf(s342,plain,
( spl11_24
| ~ spl11_44
| spl11_45 ),
inference(sat_conversion,[],[f628]) ).
cnf(s404,plain,
( ~ spl11_2
| spl11_50 ),
inference(sat_conversion,[],[f711]) ).
cnf(s476,plain,
( spl11_24
| ~ spl11_58 ),
inference(sat_conversion,[],[f852]) ).
cnf(s633,plain,
( ~ spl11_9
| spl11_66 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s640,plain,
( ~ spl11_66
| spl11_67 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s644,plain,
( spl11_24
| ~ spl11_67
| spl11_68 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s666,plain,
( ~ spl11_27
| ~ spl11_68
| spl11_71
| ~ spl11_72 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s670,plain,
( ~ spl11_68
| spl11_74 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s672,plain,
( ~ spl11_40
| ~ spl11_68
| ~ spl11_69
| spl11_70
| ~ spl11_73 ),
inference(sat_conversion,[],[f1122]) ).
cnf(s678,plain,
( ~ spl11_68
| spl11_75 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s689,plain,
( ~ spl11_68
| spl11_76
| ~ spl11_77 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s699,plain,
( ~ spl11_74
| spl11_81
| spl11_82 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s717,plain,
( ~ spl11_9
| ~ spl11_81
| ~ spl11_83 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s721,plain,
( spl11_24
| spl11_83 ),
inference(sat_conversion,[],[f1237]) ).
cnf(s727,plain,
( ~ spl11_82
| spl11_84 ),
inference(sat_conversion,[],[f1251]) ).
cnf(s733,plain,
( ~ spl11_23
| ~ spl11_71
| ~ spl11_85 ),
inference(sat_conversion,[],[f1263]) ).
cnf(s737,plain,
( ~ spl11_75
| spl11_81
| spl11_86 ),
inference(sat_conversion,[],[f1273]) ).
cnf(s739,plain,
( ~ spl11_4
| spl11_85
| ~ spl11_87
| ~ spl11_88 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s772,plain,
( ~ spl11_29
| spl11_88
| spl11_97
| spl11_98 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s775,plain,
( ~ spl11_50
| ~ spl11_97
| spl11_99 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s784,plain,
( ~ spl11_76
| ~ spl11_84
| ~ spl11_99
| spl11_100 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s789,plain,
( spl11_24
| ~ spl11_38
| ~ spl11_100 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s820,plain,
( ~ spl11_21
| ~ spl11_86
| ~ spl11_98 ),
inference(sat_conversion,[],[f1494]) ).
cnf(s830,plain,
( ~ spl11_78
| spl11_101
| spl11_102 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s902,plain,
( ~ spl11_82
| ~ spl11_84
| ~ spl11_101
| spl11_108 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s917,plain,
( ~ spl11_10
| spl11_111 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s1250,plain,
( ~ spl11_108
| spl11_173 ),
inference(sat_conversion,[],[f2566]) ).
cnf(s1267,plain,
( spl11_24
| ~ spl11_173
| spl11_174 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s1301,plain,
( spl11_100
| ~ spl11_108
| ~ spl11_173
| ~ spl11_174 ),
inference(sat_conversion,[],[f2721]) ).
cnf(s1525,plain,
( spl11_78
| spl11_101 ),
inference(sat_conversion,[],[f3101]) ).
cnf(s1578,plain,
( ~ spl11_15
| spl11_72
| ~ spl11_179 ),
inference(sat_conversion,[],[f3129]) ).
cnf(s1584,plain,
( spl11_81
| spl11_179 ),
inference(sat_conversion,[],[f3148]) ).
cnf(s1589,plain,
( ~ spl11_33
| spl11_77
| ~ spl11_179 ),
inference(sat_conversion,[],[f3154]) ).
cnf(s1593,plain,
( ~ spl11_6
| ~ spl11_72
| spl11_73
| ~ spl11_74
| ~ spl11_84 ),
inference(sat_conversion,[],[f3164]) ).
cnf(s1608,plain,
( ~ spl11_17
| spl11_69
| ~ spl11_86
| spl11_87 ),
inference(sat_conversion,[],[f3201]) ).
cnf(s1613,plain,
( ~ spl11_18
| ~ spl11_70
| ~ spl11_77
| spl11_178 ),
inference(sat_conversion,[],[f3207]) ).
cnf(s1884,plain,
( ~ spl11_102
| spl11_184 ),
inference(sat_conversion,[],[f3739]) ).
cnf(s1972,plain,
( spl11_105
| ~ spl11_184 ),
inference(sat_conversion,[],[f3860]) ).
cnf(s2565,plain,
( ~ spl11_3
| ~ spl11_45
| spl11_58
| ~ spl11_111
| spl11_260 ),
inference(sat_conversion,[],[f5092]) ).
cnf(s2574,plain,
( ~ spl11_260
| spl11_262 ),
inference(sat_conversion,[],[f5115]) ).
cnf(s2730,plain,
( ~ spl11_18
| ~ spl11_138
| ~ spl11_277
| spl11_278 ),
inference(sat_conversion,[],[f5453]) ).
cnf(s2754,plain,
( ~ spl11_262
| spl11_283 ),
inference(sat_conversion,[],[f5530]) ).
cnf(s2776,plain,
( ~ spl11_105
| ~ spl11_283
| spl11_289 ),
inference(sat_conversion,[],[f5596]) ).
cnf(s2785,plain,
( spl11_81
| ~ spl11_178
| ~ spl11_289
| spl11_290 ),
inference(sat_conversion,[],[f5618]) ).
cnf(s2793,plain,
( ~ spl11_77
| spl11_277
| ~ spl11_290 ),
inference(sat_conversion,[],[f5626]) ).
cnf(s2945,plain,
( spl11_81
| spl11_108
| ~ spl11_278
| ~ spl11_283
| ~ spl11_290 ),
inference(sat_conversion,[],[f5833]) ).
cnf(s2947,plain,
( ~ spl11_70
| spl11_138
| ~ spl11_290 ),
inference(sat_conversion,[],[f5835]) ).
cnf(s2949,plain,
spl11_29,
inference(rat,[],[s265,s261]) ).
cnf(s2950,plain,
spl11_83,
inference(rat,[],[s721,s241]) ).
cnf(s2951,plain,
~ spl11_58,
inference(rat,[],[s476,s241]) ).
cnf(s2953,plain,
spl11_23,
inference(rat,[],[s232,s223]) ).
cnf(s2954,plain,
spl11_21,
inference(rat,[],[s227,s223]) ).
cnf(s2956,plain,
spl11_22,
inference(rat,[],[s230,s2954]) ).
cnf(s2958,plain,
spl11_17,
inference(rat,[],[s208,s190]) ).
cnf(s2959,plain,
spl11_13,
inference(rat,[],[s196,s190]) ).
cnf(s2960,plain,
spl11_111,
inference(rat,[],[s917,s185]) ).
cnf(s2962,plain,
~ spl11_81,
inference(rat,[],[s717,s2950,s181]) ).
cnf(s2963,plain,
spl11_66,
inference(rat,[],[s633,s181]) ).
cnf(s2965,plain,
spl11_179,
inference(rat,[],[s1584,s2962]) ).
cnf(s2966,plain,
spl11_67,
inference(rat,[],[s640,s2963]) ).
cnf(s2968,plain,
spl11_68,
inference(rat,[],[s644,s241,s2966]) ).
cnf(s2970,plain,
spl11_75,
inference(rat,[],[s678,s2968]) ).
cnf(s2971,plain,
spl11_74,
inference(rat,[],[s670,s2968]) ).
cnf(s2973,plain,
spl11_86,
inference(rat,[],[s737,s2962,s2970]) ).
cnf(s2975,plain,
spl11_82,
inference(rat,[],[s699,s2962,s2971]) ).
cnf(s2976,plain,
~ spl11_98,
inference(rat,[],[s820,s2954,s2973]) ).
cnf(s2977,plain,
spl11_84,
inference(rat,[],[s727,s2975]) ).
cnf(s2985,plain,
spl11_18,
inference(rat,[],[s213,s176]) ).
cnf(s2986,plain,
spl11_33,
inference(rat,[],[s290,s174]) ).
cnf(s2987,plain,
spl11_15,
inference(rat,[],[s204,s174]) ).
cnf(s2989,plain,
spl11_77,
inference(rat,[],[s1589,s2965,s2986]) ).
cnf(s2990,plain,
spl11_72,
inference(rat,[],[s1578,s2965,s2987]) ).
cnf(s2991,plain,
spl11_76,
inference(rat,[],[s689,s2968,s2989]) ).
cnf(s2992,plain,
spl11_73,
inference(rat,[],[s1593,s2977,s2971,s2990,s172]) ).
cnf(s2997,plain,
spl11_27,
inference(rat,[],[s255,s172]) ).
cnf(s2999,plain,
spl11_71,
inference(rat,[],[s666,s2990,s2968,s2997]) ).
cnf(s3002,plain,
~ spl11_85,
inference(rat,[],[s733,s2953,s2999]) ).
cnf(s3008,plain,
spl11_40,
inference(rat,[],[s324,s170]) ).
cnf(s3015,plain,
spl11_50,
inference(rat,[],[s404,s162]) ).
cnf(s3021,plain,
spl11_12,
inference(rat,[],[s194,s158]) ).
cnf(s3022,plain,
spl11_4,
inference(rat,[],[s168,s158]) ).
cnf(s3024,plain,
spl11_37,
inference(rat,[],[s306,s2959,s3021]) ).
cnf(s3027,plain,
spl11_38,
inference(rat,[],[s311,s2956,s3024]) ).
cnf(s3031,plain,
~ spl11_100,
inference(rat,[],[s789,s241,s3027]) ).
cnf(s3032,plain,
spl11_44,
inference(rat,[],[s339,s3027]) ).
cnf(s3035,plain,
~ spl11_99,
inference(rat,[],[s784,s2991,s2977,s3031]) ).
cnf(s3036,plain,
spl11_45,
inference(rat,[],[s342,s241,s3032]) ).
cnf(s3040,plain,
~ spl11_97,
inference(rat,[],[s775,s3015,s3035]) ).
cnf(s3041,plain,
spl11_260,
inference(rat,[],[s2565,s164,s2960,s2951,s3036]) ).
cnf(s3048,plain,
spl11_88,
inference(rat,[],[s772,s2976,s2949,s3040]) ).
cnf(s3049,plain,
spl11_262,
inference(rat,[],[s2574,s3041]) ).
cnf(s3054,plain,
~ spl11_87,
inference(rat,[],[s739,s3022,s3002,s3048]) ).
cnf(s3055,plain,
spl11_283,
inference(rat,[],[s2754,s3049]) ).
cnf(s3063,plain,
spl11_69,
inference(rat,[],[s1608,s2973,s2958,s3054]) ).
cnf(s3069,plain,
spl11_70,
inference(rat,[],[s672,s2992,s3008,s2968,s3063]) ).
cnf(s3075,plain,
spl11_178,
inference(rat,[],[s1613,s2989,s2985,s3069]) ).
cnf(s3085,plain,
~ spl11_108,
inference(rat,[],[s1301,s1267,s1250,s3031,s241]) ).
cnf(s3086,plain,
~ spl11_101,
inference(rat,[],[s902,s2977,s2975,s3085]) ).
cnf(s3087,plain,
spl11_78,
inference(rat,[],[s1525,s3086]) ).
cnf(s3088,plain,
spl11_102,
inference(rat,[],[s830,s3087,s3086]) ).
cnf(s3089,plain,
spl11_184,
inference(rat,[],[s1884,s3088]) ).
cnf(s3093,plain,
spl11_105,
inference(rat,[],[s1972,s3089]) ).
cnf(s3097,plain,
spl11_289,
inference(rat,[],[s2776,s3055,s3093]) ).
cnf(s3101,plain,
spl11_290,
inference(rat,[],[s2785,s3075,s2962,s3097]) ).
cnf(s3103,plain,
spl11_277,
inference(rat,[],[s2793,s2989,s3101]) ).
cnf(s3106,plain,
spl11_138,
inference(rat,[],[s2947,s3069,s3101]) ).
cnf(s3107,plain,
~ spl11_278,
inference(rat,[],[s2945,s3085,s3055,s2962,s3101]) ).
cnf(s3110,plain,
$false,
inference(rat,[],[s2730,s3106,s2985,s3103,s3107]) ).
fof(f5836,plain,
$false,
inference(avatar_sat_refutation,[],[s3110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM146-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 19:00:40 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.87/2.25 % (1534195)Input is clausal, will run a generic CNF schedule.
% 9.87/2.25 % (1534204)lrs+10_1_sil=8000:sp=occurrence:random_seed=484479334:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.87/2.25 % (1534207)dis-21_1_sil=8000:lcm=predicate:random_seed=2091835580: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)
% 9.87/2.25 % (1534206)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1305343882:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.87/2.25 % (1534201)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=3071517504:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.87/2.25 % (1534202)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=902675924:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.87/2.25 % (1534203)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2464088664:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.87/2.25 % (1534205)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3411525787:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.87/2.25 % (1534204)Instruction limit reached!
% 9.87/2.25 % (1534204)------------------------------
% 9.87/2.25 % (1534204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.25 % (1534204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.25 % (1534204)CaDiCaL version: 2.1.3
% 9.87/2.25 % (1534204)Termination reason: Instruction limit
% 9.87/2.25 % (1534204)Termination phase: Saturation
% 9.87/2.25 % (1534204)Time elapsed: 0.041 s
% 9.87/2.25 % (1534204)Peak memory usage: 90 MB
% 9.87/2.25 % (1534204)Instructions burned: 109 (million)
% 9.87/2.25 % (1534207)Instruction limit reached!
% 9.87/2.25 % (1534207)------------------------------
% 9.87/2.25 % (1534207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.25 % (1534207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.25 % (1534207)CaDiCaL version: 2.1.3
% 9.87/2.25 % (1534207)Termination reason: Instruction limit
% 9.87/2.25 % (1534207)Termination phase: Saturation
% 9.87/2.25 % (1534207)Time elapsed: 0.056 s
% 9.87/2.25 % (1534207)Peak memory usage: 89 MB
% 9.87/2.25 % (1534207)Instructions burned: 118 (million)
% 9.87/2.25 % (1534205)Instruction limit reached!
% 9.87/2.25 % (1534205)------------------------------
% 9.87/2.25 % (1534205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.25 % (1534205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.25 % (1534205)CaDiCaL version: 2.1.3
% 9.87/2.25 % (1534205)Termination reason: Instruction limit
% 9.87/2.25 % (1534205)Termination phase: Saturation
% 9.87/2.25 % (1534205)Time elapsed: 0.072 s
% 9.87/2.25 % (1534205)Peak memory usage: 89 MB
% 9.87/2.25 % (1534205)Instructions burned: 115 (million)
% 9.87/2.25 % (1534206)Instruction limit reached!
% 9.87/2.25 % (1534206)------------------------------
% 9.87/2.25 % (1534206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.25 % (1534206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.25 % (1534206)CaDiCaL version: 2.1.3
% 9.87/2.25 % (1534206)Termination reason: Instruction limit
% 9.87/2.25 % (1534206)Termination phase: Saturation
% 9.87/2.25 % (1534206)Time elapsed: 0.078 s
% 9.87/2.25 % (1534206)Peak memory usage: 90 MB
% 9.87/2.25 % (1534206)Instructions burned: 182 (million)
% 9.87/2.25 % (1534215)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=808006460:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.87/2.25 % (1534215)Refutation not found, incomplete strategy
% 9.87/2.25 % (1534215)------------------------------
% 9.87/2.25 % (1534215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.87/2.25 % (1534215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.87/2.25 % (1534215)CaDiCaL version: 2.1.3
% 9.87/2.25 % (1534215)Termination reason: Refutation not found, incomplete strategy
% 9.87/2.25 % (1534215)Time elapsed: 0.004 s
% 9.87/2.25 % (1534215)Peak memory usage: 88 MB
% 9.87/2.25 % (1534215)Instructions burned: 4 (million)
% 9.87/2.25 % (1534218)lrs+10_64_to=lpo:sil=8000:random_seed=1198051802:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 17.09/3.24 % (1534216)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2361640892: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)
% 17.09/3.24 % (1534216)Refutation not found, incomplete strategy
% 17.09/3.24 % (1534216)------------------------------
% 17.09/3.24 % (1534216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.24 % (1534216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.24 % (1534216)CaDiCaL version: 2.1.3
% 17.09/3.24 % (1534216)Termination reason: Refutation not found, incomplete strategy
% 17.09/3.24 % (1534216)Time elapsed: 0.012 s
% 17.09/3.24 % (1534216)Peak memory usage: 89 MB
% 17.09/3.24 % (1534216)Instructions burned: 21 (million)
% 17.09/3.24 % (1534217)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2259325602:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 17.09/3.24 % (1534218)Instruction limit reached!
% 17.09/3.24 % (1534218)------------------------------
% 17.09/3.24 % (1534218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.24 % (1534218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.24 % (1534218)CaDiCaL version: 2.1.3
% 17.09/3.24 % (1534218)Termination reason: Instruction limit
% 17.09/3.24 % (1534218)Termination phase: Saturation
% 17.09/3.24 % (1534218)Time elapsed: 0.043 s
% 17.09/3.24 % (1534218)Peak memory usage: 90 MB
% 17.09/3.24 % (1534218)Instructions burned: 128 (million)
% 17.09/3.24 % (1534223)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2011300058:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 17.09/3.24 % (1534217)Instruction limit reached!
% 17.09/3.24 % (1534217)------------------------------
% 17.09/3.24 % (1534217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.24 % (1534217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.24 % (1534217)CaDiCaL version: 2.1.3
% 17.09/3.24 % (1534217)Termination reason: Instruction limit
% 17.09/3.24 % (1534217)Termination phase: Saturation
% 17.09/3.24 % (1534217)Time elapsed: 0.133 s
% 17.09/3.24 % (1534217)Peak memory usage: 89 MB
% 17.09/3.24 % (1534217)Instructions burned: 220 (million)
% 17.09/3.24 % (1534223)Instruction limit reached!
% 17.09/3.24 % (1534223)------------------------------
% 17.09/3.24 % (1534223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.24 % (1534223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.24 % (1534223)CaDiCaL version: 2.1.3
% 17.09/3.24 % (1534223)Termination reason: Instruction limit
% 17.09/3.24 % (1534223)Termination phase: Saturation
% 17.09/3.24 % (1534223)Time elapsed: 0.055 s
% 17.09/3.24 % (1534223)Peak memory usage: 90 MB
% 17.09/3.24 % (1534223)Instructions burned: 197 (million)
% 17.09/3.24 % (1534215)------------------------------
% 17.09/3.24 % (1534215)------------------------------
% 17.09/3.24 % (1534216)------------------------------
% 17.09/3.24 % (1534216)------------------------------
% 17.09/3.24 % (1534226)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3416957393:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 17.09/3.24 % (1534225)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=326522590:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 17.09/3.24 % (1534227)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=3816328573:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 17.09/3.24 % (1534225)Instruction limit reached!
% 17.09/3.24 % (1534225)------------------------------
% 17.09/3.24 % (1534225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.24 % (1534225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.24 % (1534225)CaDiCaL version: 2.1.3
% 17.09/3.24 % (1534225)Termination reason: Instruction limit
% 17.09/3.24 % (1534225)Termination phase: Saturation
% 17.09/3.24 % (1534225)Time elapsed: 0.110 s
% 17.09/3.24 % (1534225)Peak memory usage: 91 MB
% 17.09/3.24 % (1534225)Instructions burned: 157 (million)
% 17.09/3.24 % (1534227)Instruction limit reached!
% 17.09/3.24 % (1534227)------------------------------
% 17.09/3.24 % (1534227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534227)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534227)Termination reason: Instruction limit
% 28.97/4.96 % (1534227)Termination phase: Saturation
% 28.97/4.96 % (1534227)Time elapsed: 0.066 s
% 28.97/4.96 % (1534227)Peak memory usage: 89 MB
% 28.97/4.96 % (1534227)Instructions burned: 107 (million)
% 28.97/4.96 % (1534229)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3673251338:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 28.97/4.96 % (1534229)Instruction limit reached!
% 28.97/4.96 % (1534229)------------------------------
% 28.97/4.96 % (1534229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534229)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534229)Termination reason: Instruction limit
% 28.97/4.96 % (1534229)Termination phase: Saturation
% 28.97/4.96 % (1534229)Time elapsed: 0.074 s
% 28.97/4.96 % (1534229)Peak memory usage: 89 MB
% 28.97/4.96 % (1534229)Instructions burned: 108 (million)
% 28.97/4.96 % (1534233)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2211532166:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 28.97/4.96 % (1534232)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3253123039:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 28.97/4.96 % (1534235)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=313769830:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 28.97/4.96 % (1534235)Refutation not found, incomplete strategy
% 28.97/4.96 % (1534235)------------------------------
% 28.97/4.96 % (1534235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534235)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534235)Termination reason: Refutation not found, incomplete strategy
% 28.97/4.96 % (1534235)Time elapsed: 0.006 s
% 28.97/4.96 % (1534235)Peak memory usage: 88 MB
% 28.97/4.96 % (1534235)Instructions burned: 8 (million)
% 28.97/4.96 % (1534232)Instruction limit reached!
% 28.97/4.96 % (1534232)------------------------------
% 28.97/4.96 % (1534232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534232)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534232)Termination reason: Instruction limit
% 28.97/4.96 % (1534232)Termination phase: Saturation
% 28.97/4.96 % (1534232)Time elapsed: 0.140 s
% 28.97/4.96 % (1534232)Peak memory usage: 91 MB
% 28.97/4.96 % (1534232)Instructions burned: 244 (million)
% 28.97/4.96 % (1534239)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=639524508:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 28.97/4.96 % (1534235)------------------------------
% 28.97/4.96 % (1534235)------------------------------
% 28.97/4.96 % (1534241)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1908413906:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 28.97/4.96 % (1534239)Instruction limit reached!
% 28.97/4.96 % (1534239)------------------------------
% 28.97/4.96 % (1534239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534239)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534239)Termination reason: Instruction limit
% 28.97/4.96 % (1534239)Termination phase: Saturation
% 28.97/4.96 % (1534239)Time elapsed: 0.307 s
% 28.97/4.96 % (1534239)Peak memory usage: 93 MB
% 28.97/4.96 % (1534239)Instructions burned: 499 (million)
% 28.97/4.96 % (1534241)Instruction limit reached!
% 28.97/4.96 % (1534241)------------------------------
% 28.97/4.96 % (1534241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.97/4.96 % (1534241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.97/4.96 % (1534241)CaDiCaL version: 2.1.3
% 28.97/4.96 % (1534241)Termination reason: Instruction limit
% 28.97/4.96 % (1534241)Termination phase: Saturation
% 28.97/4.96 % (1534241)Time elapsed: 0.104 s
% 28.97/4.96 % (1534241)Peak memory usage: 89 MB
% 28.97/4.96 % (1534241)Instructions burned: 192 (million)
% 48.32/7.81 % (1534243)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=649065593:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 48.32/7.81 % (1534244)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2707033350:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 48.32/7.81 % (1534244)Instruction limit reached!
% 48.32/7.81 % (1534244)------------------------------
% 48.32/7.81 % (1534244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.32/7.81 % (1534244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.32/7.81 % (1534244)CaDiCaL version: 2.1.3
% 48.32/7.81 % (1534244)Termination reason: Instruction limit
% 48.32/7.81 % (1534244)Termination phase: Saturation
% 48.32/7.81 % (1534244)Time elapsed: 0.107 s
% 48.32/7.81 % (1534244)Peak memory usage: 89 MB
% 48.32/7.81 % (1534244)Instructions burned: 157 (million)
% 48.32/7.81 % (1534243)Instruction limit reached!
% 48.32/7.81 % (1534243)------------------------------
% 48.32/7.81 % (1534243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.32/7.81 % (1534243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.32/7.81 % (1534243)CaDiCaL version: 2.1.3
% 48.32/7.81 % (1534243)Termination reason: Instruction limit
% 48.32/7.81 % (1534243)Termination phase: Saturation
% 48.32/7.81 % (1534243)Time elapsed: 0.173 s
% 48.32/7.81 % (1534243)Peak memory usage: 91 MB
% 48.32/7.81 % (1534243)Instructions burned: 265 (million)
% 48.32/7.81 % (1534226)Instruction limit reached!
% 48.32/7.81 % (1534226)------------------------------
% 48.32/7.81 % (1534226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.32/7.81 % (1534226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.32/7.81 % (1534226)CaDiCaL version: 2.1.3
% 48.32/7.81 % (1534226)Termination reason: Instruction limit
% 48.32/7.81 % (1534226)Termination phase: Saturation
% 48.32/7.81 % (1534226)Time elapsed: 1.148 s
% 48.32/7.81 % (1534226)Peak memory usage: 148 MB
% 48.32/7.81 % (1534226)Instructions burned: 3398 (million)
% 48.32/7.81 % (1534247)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=903815595:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 48.32/7.81 % (1534248)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3146076751:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 48.32/7.81 % (1534249)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2774430306:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 48.32/7.81 % (1534249)Instruction limit reached!
% 48.32/7.81 % (1534249)------------------------------
% 48.32/7.81 % (1534249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.32/7.81 % (1534249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.32/7.81 % (1534249)CaDiCaL version: 2.1.3
% 48.32/7.81 % (1534249)Termination reason: Instruction limit
% 48.32/7.81 % (1534249)Termination phase: Saturation
% 48.32/7.81 % (1534249)Time elapsed: 0.057 s
% 48.32/7.81 % (1534249)Peak memory usage: 90 MB
% 48.32/7.81 % (1534249)Instructions burned: 184 (million)
% 48.32/7.81 % (1534253)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1256378198:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 48.32/7.81 % (1534248)Instruction limit reached!
% 48.32/7.81 % (1534248)------------------------------
% 48.32/7.81 % (1534248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.32/7.81 % (1534248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.32/7.81 % (1534248)CaDiCaL version: 2.1.3
% 48.32/7.81 % (1534248)Termination reason: Instruction limit
% 48.32/7.81 % (1534248)Termination phase: Saturation
% 48.32/7.81 % (1534248)Time elapsed: 0.253 s
% 48.32/7.81 % (1534248)Peak memory usage: 89 MB
% 48.32/7.81 % (1534248)Instructions burned: 537 (million)
% 48.32/7.81 % (1534255)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=683623321:i=412:gtgl=4:gtg=exists_all_2979 on theBenchmark for (2979ds/412Mi)
% 48.32/7.81 % (1534255)Instruction limit reached!
% 48.32/7.81 % (1534255)------------------------------
% 48.32/7.81 % (1534255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534255)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534255)Termination reason: Instruction limit
% 70.69/10.93 % (1534255)Termination phase: Saturation
% 70.69/10.93 % (1534255)Time elapsed: 0.188 s
% 70.69/10.93 % (1534255)Peak memory usage: 90 MB
% 70.69/10.93 % (1534255)Instructions burned: 412 (million)
% 70.69/10.93 % (1534257)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3747910160:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 70.69/10.93 % (1534247)Instruction limit reached!
% 70.69/10.93 % (1534247)------------------------------
% 70.69/10.93 % (1534247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534247)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534247)Termination reason: Instruction limit
% 70.69/10.93 % (1534247)Termination phase: Saturation
% 70.69/10.93 % (1534247)Time elapsed: 1.283 s
% 70.69/10.93 % (1534247)Peak memory usage: 147 MB
% 70.69/10.93 % (1534247)Instructions burned: 3259 (million)
% 70.69/10.93 % (1534259)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=4147399737:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 70.69/10.93 % (1534259)Instruction limit reached!
% 70.69/10.93 % (1534259)------------------------------
% 70.69/10.93 % (1534259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534259)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534259)Termination reason: Instruction limit
% 70.69/10.93 % (1534259)Termination phase: Saturation
% 70.69/10.93 % (1534259)Time elapsed: 0.057 s
% 70.69/10.93 % (1534259)Peak memory usage: 88 MB
% 70.69/10.93 % (1534259)Instructions burned: 309 (million)
% 70.69/10.93 % (1534261)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3080394010:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 70.69/10.93 % (1534261)Instruction limit reached!
% 70.69/10.93 % (1534261)------------------------------
% 70.69/10.93 % (1534261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534261)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534261)Termination reason: Instruction limit
% 70.69/10.93 % (1534261)Termination phase: Saturation
% 70.69/10.93 % (1534261)Time elapsed: 0.259 s
% 70.69/10.93 % (1534261)Peak memory usage: 97 MB
% 70.69/10.93 % (1534261)Instructions burned: 721 (million)
% 70.69/10.93 % (1534263)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2211380315:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 70.69/10.93 % (1534263)Refutation not found, incomplete strategy
% 70.69/10.93 % (1534263)------------------------------
% 70.69/10.93 % (1534263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534263)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534263)Termination reason: Refutation not found, incomplete strategy
% 70.69/10.93 % (1534263)Time elapsed: 0.022 s
% 70.69/10.93 % (1534263)Peak memory usage: 88 MB
% 70.69/10.93 % (1534263)Instructions burned: 33 (million)
% 70.69/10.93 % (1534263)------------------------------
% 70.69/10.93 % (1534263)------------------------------
% 70.69/10.93 % (1534265)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1469316031:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 70.69/10.93 % (1534233)Instruction limit reached!
% 70.69/10.93 % (1534233)------------------------------
% 70.69/10.93 % (1534233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.69/10.93 % (1534233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.69/10.93 % (1534233)CaDiCaL version: 2.1.3
% 70.69/10.93 % (1534233)Termination reason: Instruction limit
% 70.69/10.93 % (1534233)Termination phase: Saturation
% 70.69/10.93 % (1534233)Time elapsed: 3.289 s
% 70.69/10.93 % (1534233)Peak memory usage: 161 MB
% 70.69/10.93 % (1534233)Instructions burned: 5209 (million)
% 84.50/12.88 % (1534267)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3014106005:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2958 on theBenchmark for (2958ds/1997Mi)
% 84.50/12.88 % (1534265)Instruction limit reached!
% 84.50/12.88 % (1534265)------------------------------
% 84.50/12.88 % (1534265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534265)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534265)Termination reason: Instruction limit
% 84.50/12.88 % (1534265)Termination phase: Saturation
% 84.50/12.88 % (1534265)Time elapsed: 1.375 s
% 84.50/12.88 % (1534265)Peak memory usage: 145 MB
% 84.50/12.88 % (1534265)Instructions burned: 2991 (million)
% 84.50/12.88 % (1534269)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2245033002:i=2088:bd=preordered:av=off_2946 on theBenchmark for (2946ds/2088Mi)
% 84.50/12.88 % (1534267)Instruction limit reached!
% 84.50/12.88 % (1534267)------------------------------
% 84.50/12.88 % (1534267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534267)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534267)Termination reason: Instruction limit
% 84.50/12.88 % (1534267)Termination phase: Saturation
% 84.50/12.88 % (1534267)Time elapsed: 1.441 s
% 84.50/12.88 % (1534267)Peak memory usage: 137 MB
% 84.50/12.88 % (1534267)Instructions burned: 1998 (million)
% 84.50/12.88 % (1534271)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=245370266:i=1098:nicw=on_2942 on theBenchmark for (2942ds/1098Mi)
% 84.50/12.88 % (1534271)Instruction limit reached!
% 84.50/12.88 % (1534271)------------------------------
% 84.50/12.88 % (1534271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534271)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534271)Termination reason: Instruction limit
% 84.50/12.88 % (1534271)Termination phase: Saturation
% 84.50/12.88 % (1534271)Time elapsed: 0.386 s
% 84.50/12.88 % (1534271)Peak memory usage: 101 MB
% 84.50/12.88 % (1534271)Instructions burned: 1101 (million)
% 84.50/12.88 % (1534273)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3696112099:i=433:bd=preordered_2937 on theBenchmark for (2937ds/433Mi)
% 84.50/12.88 % (1534273)Instruction limit reached!
% 84.50/12.88 % (1534273)------------------------------
% 84.50/12.88 % (1534273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534273)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534273)Termination reason: Instruction limit
% 84.50/12.88 % (1534273)Termination phase: Saturation
% 84.50/12.88 % (1534273)Time elapsed: 0.135 s
% 84.50/12.88 % (1534273)Peak memory usage: 93 MB
% 84.50/12.88 % (1534273)Instructions burned: 434 (million)
% 84.50/12.88 % (1534275)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2999276260:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2935 on theBenchmark for (2935ds/2942Mi)
% 84.50/12.88 % (1534269)Instruction limit reached!
% 84.50/12.88 % (1534269)------------------------------
% 84.50/12.88 % (1534269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534269)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534269)Termination reason: Instruction limit
% 84.50/12.88 % (1534269)Termination phase: Saturation
% 84.50/12.88 % (1534269)Time elapsed: 1.094 s
% 84.50/12.88 % (1534269)Peak memory usage: 138 MB
% 84.50/12.88 % (1534269)Instructions burned: 2089 (million)
% 84.50/12.88 % (1534277)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3289724012:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi)
% 84.50/12.88 % (1534257)Instruction limit reached!
% 84.50/12.88 % (1534257)------------------------------
% 84.50/12.88 % (1534257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534257)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534257)Termination reason: Instruction limit
% 84.50/12.88 % (1534257)Termination phase: Saturation
% 84.50/12.88 % (1534257)Time elapsed: 4.430 s
% 84.50/12.88 % (1534257)Peak memory usage: 175 MB
% 84.50/12.88 % (1534257)Instructions burned: 8481 (million)
% 84.50/12.88 % (1534279)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3643328083:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2930 on theBenchmark for (2930ds/596Mi)
% 84.50/12.88 % (1534279)Instruction limit reached!
% 84.50/12.88 % (1534279)------------------------------
% 84.50/12.88 % (1534279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534279)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534279)Termination reason: Instruction limit
% 84.50/12.88 % (1534279)Termination phase: Saturation
% 84.50/12.88 % (1534279)Time elapsed: 0.325 s
% 84.50/12.88 % (1534279)Peak memory usage: 99 MB
% 84.50/12.88 % (1534279)Instructions burned: 596 (million)
% 84.50/12.88 % (1534281)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2894807092:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/4123Mi)
% 84.50/12.88 % (1534275)Instruction limit reached!
% 84.50/12.88 % (1534275)------------------------------
% 84.50/12.88 % (1534275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534275)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534275)Termination reason: Instruction limit
% 84.50/12.88 % (1534275)Termination phase: Saturation
% 84.50/12.88 % (1534275)Time elapsed: 1.049 s
% 84.50/12.88 % (1534275)Peak memory usage: 146 MB
% 84.50/12.88 % (1534275)Instructions burned: 2944 (million)
% 84.50/12.88 % (1534283)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2776842798:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 84.50/12.88 % (1534253)Instruction limit reached!
% 84.50/12.88 % (1534253)------------------------------
% 84.50/12.88 % (1534253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534253)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534253)Termination reason: Instruction limit
% 84.50/12.88 % (1534253)Termination phase: Saturation
% 84.50/12.88 % (1534253)Time elapsed: 6.596 s
% 84.50/12.88 % (1534253)Peak memory usage: 180 MB
% 84.50/12.88 % (1534253)Instructions burned: 10307 (million)
% 84.50/12.88 % (1534285)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1352049217:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2914 on theBenchmark for (2914ds/1670Mi)
% 84.50/12.88 % (1534285)Instruction limit reached!
% 84.50/12.88 % (1534285)------------------------------
% 84.50/12.88 % (1534285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534285)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534285)Termination reason: Instruction limit
% 84.50/12.88 % (1534285)Termination phase: Saturation
% 84.50/12.88 % (1534285)Time elapsed: 1.049 s
% 84.50/12.88 % (1534285)Peak memory usage: 137 MB
% 84.50/12.88 % (1534285)Instructions burned: 1670 (million)
% 84.50/12.88 % (1534287)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3220997555:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2902 on theBenchmark for (2902ds/1722Mi)
% 84.50/12.88 % (1534281)Instruction limit reached!
% 84.50/12.88 % (1534281)------------------------------
% 84.50/12.88 % (1534281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534281)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534281)Termination reason: Instruction limit
% 84.50/12.88 % (1534281)Termination phase: Saturation
% 84.50/12.88 % (1534281)Time elapsed: 2.374 s
% 84.50/12.88 % (1534281)Peak memory usage: 161 MB
% 84.50/12.88 % (1534281)Instructions burned: 4124 (million)
% 84.50/12.88 % (1534289)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3091579175:cts=off:cond=on:i=9530:bs=on:fsd=on_2900 on theBenchmark for (2900ds/9530Mi)
% 84.50/12.88 % (1534277)Instruction limit reached!
% 84.50/12.88 % (1534277)------------------------------
% 84.50/12.88 % (1534277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534277)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534277)Termination reason: Instruction limit
% 84.50/12.88 % (1534277)Termination phase: Saturation
% 84.50/12.88 % (1534277)Time elapsed: 3.636 s
% 84.50/12.88 % (1534277)Peak memory usage: 179 MB
% 84.50/12.88 % (1534277)Instructions burned: 6923 (million)
% 84.50/12.88 % (1534291)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2382807198:st=2:i=4495:sd=10:ss=included_2895 on theBenchmark for (2895ds/4495Mi)
% 84.50/12.88 % (1534287)Instruction limit reached!
% 84.50/12.88 % (1534287)------------------------------
% 84.50/12.88 % (1534287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.50/12.88 % (1534287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.50/12.88 % (1534287)CaDiCaL version: 2.1.3
% 84.50/12.88 % (1534287)Termination reason: Instruction limit
% 84.50/12.88 % (1534287)Termination phase: Saturation
% 84.50/12.88 % (1534287)Time elapsed: 1.186 s
% 84.50/12.88 % (1534287)Peak memory usage: 134 MB
% 84.50/12.88 % (1534287)Instructions burned: 1723 (million)
% 84.50/12.88 % (1534293)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3725204383:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2888 on theBenchmark for (2888ds/4920Mi)
% 84.50/12.88 % (1534289)First to succeed.
% 84.50/12.88 % (1534289)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1534195"
% 84.50/12.88 % (1534289)Refutation found. Thanks to Tanya!
% 84.50/12.88 % SZS status Unsatisfiable for theBenchmark
% 84.50/12.88 % SZS output start Proof for theBenchmark
% See solution above
% 85.18/13.08 % (1534289)------------------------------
% 85.18/13.08 % (1534289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.18/13.08 % (1534289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.18/13.08 % (1534289)CaDiCaL version: 2.1.3
% 85.18/13.08 % (1534289)Termination reason: Refutation
% 85.18/13.08 % (1534289)Time elapsed: 1.658 s
% 85.18/13.08 % (1534289)Peak memory usage: 141 MB
% 85.18/13.08 % (1534289)Instructions burned: 2384 (million)
% 85.18/13.08 % (1534289)------------------------------
% 85.18/13.08 % (1534289)------------------------------
% 85.18/13.08 % (1534195)Success in time 12.054 s
% 85.18/13.08 % Vampire exiting
%------------------------------------------------------------------------------