%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET251-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:37 PM UTC 2026
% Result : Unsatisfiable 82.50s 12.85s
% Output : Refutation 85.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 121
% Syntax : Number of formulae : 580 ( 86 unt; 91 def)
% Number of atoms : 1530 ( 156 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1775 ( 825 ~; 864 |; 0 &)
% ( 86 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 90 ( 88 usr; 87 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-3 aty)
% Number of variables : 333 ( 0 sgn 333 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f10,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f19,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),element_relation)
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation2) ).
fof(f20,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation3) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/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(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,negated_conjecture,
member(y,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_restriction_of_element_relation_1) ).
fof(f123,negated_conjecture,
domain_of(restrict(element_relation,x,singleton(y))) != intersection(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_restriction_of_element_relation_2) ).
fof(f128,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(f137,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,f128]) ).
fof(f138,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,f128]) ).
fof(f139,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,f128]) ).
fof(f140,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,f128]) ).
fof(f141,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,f128]) ).
fof(f142,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation) ),
inference(definition_unfolding,[],[f20,f128,f128]) ).
fof(f144,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(f145,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(f186,plain,
intersection(x,y) != domain_of(intersection(element_relation,cross_product(x,unordered_pair(y,y)))),
inference(definition_unfolding,[],[f123,f28,f12]) ).
fof(f188,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f191,definition,
sF0 = intersection(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f192,plain,
intersection(x,y) = sF0,
inference(reorient_equations,[],[f191]) ).
fof(f193,definition,
sF1 = unordered_pair(y,y),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f194,plain,
unordered_pair(y,y) = sF1,
inference(reorient_equations,[],[f193]) ).
fof(f195,definition,
sF2 = cross_product(x,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f196,plain,
cross_product(x,sF1) = sF2,
inference(reorient_equations,[],[f195]) ).
fof(f197,definition,
sF3 = intersection(element_relation,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f198,plain,
intersection(element_relation,sF2) = sF3,
inference(reorient_equations,[],[f197]) ).
fof(f199,definition,
sF4 = domain_of(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f200,plain,
domain_of(sF3) = sF4,
inference(reorient_equations,[],[f199]) ).
fof(f201,plain,
sF0 != sF4,
inference(definition_folding,[],[f186,f200,f198,f196,f194,f192]) ).
fof(f203,definition,
( spl5_1
<=> intersection(x,y) = sF0 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f205,plain,
( intersection(x,y) = sF0
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
spl5_1,
inference(avatar_split_clause,[],[f192,f203]) ).
fof(f208,definition,
( spl5_2
<=> cross_product(x,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f210,plain,
( cross_product(x,sF1) = sF2
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
spl5_2,
inference(avatar_split_clause,[],[f196,f208]) ).
fof(f215,definition,
( spl5_3
<=> unordered_pair(y,y) = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
fof(f217,plain,
( unordered_pair(y,y) = sF1
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,plain,
spl5_3,
inference(avatar_split_clause,[],[f194,f215]) ).
fof(f220,definition,
( spl5_4
<=> member(y,universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
fof(f222,plain,
( member(y,universal_class)
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
spl5_4,
inference(avatar_split_clause,[],[f122,f220]) ).
fof(f235,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,y)
| ~ member(X0,x) )
| ~ spl5_1 ),
inference(superposition,[],[f23,f205]) ).
fof(f237,definition,
( spl5_7
<=> ! [X0] :
( member(X0,sF0)
| ~ member(X0,y)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition]) ).
fof(f238,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,y)
| ~ member(X0,x) )
| ~ spl5_7 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f239,plain,
( spl5_7
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f235,f203,f237]) ).
fof(f241,plain,
( ! [X0] : member(y,unordered_pair(y,X0))
| ~ spl5_4 ),
inference(resolution,[],[f222,f9]) ).
fof(f243,definition,
( spl5_8
<=> ! [X0] : member(y,unordered_pair(y,X0)) ),
introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition]) ).
fof(f244,plain,
( ! [X0] : member(y,unordered_pair(y,X0))
| ~ spl5_8 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f245,plain,
( spl5_8
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f241,f220,f243]) ).
fof(f246,plain,
( member(y,sF1)
| ~ spl5_3
| ~ spl5_8 ),
inference(superposition,[],[f244,f217]) ).
fof(f248,definition,
( spl5_9
<=> domain_of(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition]) ).
fof(f250,plain,
( domain_of(sF3) = sF4
| ~ spl5_9 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
spl5_9,
inference(avatar_split_clause,[],[f200,f248]) ).
fof(f253,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF1,universal_class))
| ~ member(y,domain_of(X0)) )
| ~ spl5_3 ),
inference(superposition,[],[f144,f217]) ).
fof(f255,plain,
( ! [X0] :
( ~ member(X0,sF1)
| y = X0
| y = X0 )
| ~ spl5_3 ),
inference(superposition,[],[f8,f217]) ).
fof(f256,plain,
( ! [X0] :
( ~ member(X0,sF1)
| y = X0 )
| ~ spl5_3 ),
inference(duplicate_literal_removal,[],[f255]) ).
fof(f258,definition,
( spl5_10
<=> intersection(element_relation,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition]) ).
fof(f260,plain,
( intersection(element_relation,sF2) = sF3
| ~ spl5_10 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f261,plain,
spl5_10,
inference(avatar_split_clause,[],[f198,f258]) ).
fof(f262,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) )
| ~ spl5_10 ),
inference(superposition,[],[f23,f260]) ).
fof(f263,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) )
| ~ spl5_10 ),
inference(superposition,[],[f22,f260]) ).
fof(f264,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,element_relation) )
| ~ spl5_10 ),
inference(superposition,[],[f21,f260]) ).
fof(f266,definition,
( spl5_11
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition]) ).
fof(f267,plain,
( ! [X0] :
( member(X0,sF2)
| ~ member(X0,sF3) )
| ~ spl5_11 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f268,plain,
( spl5_11
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f263,f258,f266]) ).
fof(f270,definition,
( spl5_12
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition]) ).
fof(f271,plain,
( ! [X0] :
( member(X0,element_relation)
| ~ member(X0,sF3) )
| ~ spl5_12 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( spl5_12
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f264,f258,f270]) ).
fof(f274,definition,
( spl5_13
<=> sF0 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition]) ).
fof(f276,plain,
( sF0 != sF4
| spl5_13 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f277,plain,
~ spl5_13,
inference(avatar_split_clause,[],[f201,f274]) ).
fof(f280,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,x) )
| ~ spl5_2 ),
inference(superposition,[],[f137,f210]) ).
fof(f282,definition,
( spl5_14
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_14])],[avatar_definition]) ).
fof(f283,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,x) )
| ~ spl5_14 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( spl5_14
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f280,f208,f282]) ).
fof(f289,definition,
( spl5_15
<=> ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl5_15])],[avatar_definition]) ).
fof(f290,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) )
| ~ spl5_15 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f291,plain,
( spl5_15
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f262,f258,f289]) ).
fof(f294,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,sF1) )
| ~ spl5_2 ),
inference(superposition,[],[f138,f210]) ).
fof(f296,definition,
( spl5_16
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition]) ).
fof(f297,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,sF1) )
| ~ spl5_16 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f298,plain,
( spl5_16
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f294,f208,f296]) ).
fof(f303,definition,
( spl5_17
<=> ! [X0] :
( ~ member(X0,sF1)
| y = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition]) ).
fof(f304,plain,
( ! [X0] :
( ~ member(X0,sF1)
| y = X0 )
| ~ spl5_17 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f305,plain,
( spl5_17
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f256,f215,f303]) ).
fof(f307,definition,
( spl5_18
<=> member(y,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
fof(f309,plain,
( member(y,sF1)
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( spl5_18
| ~ spl5_3
| ~ spl5_8 ),
inference(avatar_split_clause,[],[f246,f243,f215,f307]) ).
fof(f316,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X1) ),
inference(resolution,[],[f2,f22]) ).
fof(f317,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X0) ),
inference(resolution,[],[f2,f21]) ).
fof(f324,plain,
( ! [X0] :
( subclass(X0,sF0)
| ~ member(not_subclass_element(X0,sF0),y)
| ~ member(not_subclass_element(X0,sF0),x) )
| ~ spl5_7 ),
inference(resolution,[],[f3,f238]) ).
fof(f329,definition,
( spl5_19
<=> ! [X0] :
( subclass(X0,sF0)
| ~ member(not_subclass_element(X0,sF0),y)
| ~ member(not_subclass_element(X0,sF0),x) ) ),
introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition]) ).
fof(f330,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF0),x)
| ~ member(not_subclass_element(X0,sF0),y)
| subclass(X0,sF0) )
| ~ spl5_19 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( spl5_19
| ~ spl5_7 ),
inference(avatar_split_clause,[],[f324,f237,f329]) ).
fof(f336,plain,
! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ subclass(X1,universal_class)
| member(X0,unordered_pair(X2,X0)) ),
inference(resolution,[],[f1,f10]) ).
fof(f351,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X2,X0))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[],[f336,f4]) ).
fof(f355,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,[],[f145,f1]) ).
fof(f356,plain,
( ! [X0] :
( null_class = intersection(X0,cross_product(unordered_pair(y,y),universal_class))
| member(y,domain_of(X0)) )
| ~ spl5_4 ),
inference(resolution,[],[f145,f222]) ).
fof(f358,plain,
( ! [X0] :
( null_class = intersection(X0,cross_product(sF1,universal_class))
| member(y,domain_of(X0)) )
| ~ spl5_3
| ~ spl5_4 ),
inference(forward_demodulation,[],[f356,f217]) ).
fof(f359,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,[],[f355,f4]) ).
fof(f361,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_9 ),
inference(superposition,[],[f359,f250]) ).
fof(f363,definition,
( spl5_20
<=> ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition]) ).
fof(f364,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_20 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( spl5_20
| ~ spl5_9 ),
inference(avatar_split_clause,[],[f361,f248,f363]) ).
fof(f367,plain,
( ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),x) )
| ~ spl5_1 ),
inference(superposition,[],[f317,f205]) ).
fof(f376,definition,
( spl5_22
<=> ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),x) ) ),
introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition]) ).
fof(f377,plain,
( ! [X0] :
( member(not_subclass_element(sF0,X0),x)
| subclass(sF0,X0) )
| ~ spl5_22 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f378,plain,
( spl5_22
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f367,f203,f376]) ).
fof(f388,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,x) )
| ~ spl5_2 ),
inference(superposition,[],[f139,f210]) ).
fof(f390,definition,
( spl5_23
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_23])],[avatar_definition]) ).
fof(f391,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,x) )
| ~ spl5_23 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f392,plain,
( spl5_23
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f388,f208,f390]) ).
fof(f399,plain,
( ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),y) )
| ~ spl5_1 ),
inference(superposition,[],[f316,f205]) ).
fof(f403,plain,
( ! [X0,X1] :
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(X0,sF4),not_subclass_element(X0,sF4)),universal_class))
| ~ member(not_subclass_element(X0,sF4),X1)
| subclass(X0,sF4) )
| ~ spl5_20 ),
inference(resolution,[],[f364,f3]) ).
fof(f405,definition,
( spl5_24
<=> ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),y) ) ),
introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition]) ).
fof(f406,plain,
( ! [X0] :
( member(not_subclass_element(sF0,X0),y)
| subclass(sF0,X0) )
| ~ spl5_24 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f407,plain,
( spl5_24
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f399,f203,f405]) ).
fof(f419,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f427,definition,
( spl5_27
<=> ! [X0] :
( null_class != intersection(X0,cross_product(sF1,universal_class))
| ~ member(y,domain_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl5_27])],[avatar_definition]) ).
fof(f428,plain,
( ! [X0] :
( null_class != intersection(X0,cross_product(sF1,universal_class))
| ~ member(y,domain_of(X0)) )
| ~ spl5_27 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f429,plain,
( spl5_27
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f253,f215,f427]) ).
fof(f431,definition,
( spl5_28
<=> ! [X0] :
( null_class = intersection(X0,cross_product(sF1,universal_class))
| member(y,domain_of(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl5_28])],[avatar_definition]) ).
fof(f432,plain,
( ! [X0] :
( member(y,domain_of(X0))
| null_class = intersection(X0,cross_product(sF1,universal_class)) )
| ~ spl5_28 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( spl5_28
| ~ spl5_3
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f358,f220,f215,f431]) ).
fof(f434,plain,
( member(y,sF4)
| null_class = intersection(sF3,cross_product(sF1,universal_class))
| ~ spl5_9
| ~ spl5_28 ),
inference(superposition,[],[f432,f250]) ).
fof(f437,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f438,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f441,plain,
( null_class = sF1
| y = regular(sF1)
| ~ spl5_17 ),
inference(resolution,[],[f68,f304]) ).
fof(f443,definition,
( spl5_29
<=> ! [X0,X1] :
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(X0,sF4),not_subclass_element(X0,sF4)),universal_class))
| ~ member(not_subclass_element(X0,sF4),X1)
| subclass(X0,sF4) ) ),
introduced(definition,[new_symbols(definition,[spl5_29])],[avatar_definition]) ).
fof(f444,plain,
( ! [X0,X1] :
( subclass(X0,sF4)
| ~ member(not_subclass_element(X0,sF4),X1)
| null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(X0,sF4),not_subclass_element(X0,sF4)),universal_class)) )
| ~ spl5_29 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( spl5_29
| ~ spl5_20 ),
inference(avatar_split_clause,[],[f403,f363,f443]) ).
fof(f448,definition,
( spl5_30
<=> null_class = intersection(sF3,cross_product(sF1,universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_30])],[avatar_definition]) ).
fof(f449,plain,
( null_class != intersection(sF3,cross_product(sF1,universal_class))
| spl5_30 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f450,plain,
( null_class = intersection(sF3,cross_product(sF1,universal_class))
| ~ spl5_30 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f452,definition,
( spl5_31
<=> member(y,sF4) ),
introduced(definition,[new_symbols(definition,[spl5_31])],[avatar_definition]) ).
fof(f454,plain,
( member(y,sF4)
| ~ spl5_31 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( spl5_30
| spl5_31
| ~ spl5_9
| ~ spl5_28 ),
inference(avatar_split_clause,[],[f434,f431,f248,f452,f448]) ).
fof(f459,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(sF1,universal_class))
| ~ member(X0,sF3) )
| ~ spl5_30 ),
inference(superposition,[],[f23,f450]) ).
fof(f460,plain,
( ! [X0] :
( ~ member(X0,null_class)
| member(X0,cross_product(sF1,universal_class)) )
| ~ spl5_30 ),
inference(superposition,[],[f22,f450]) ).
fof(f461,plain,
( ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF3) )
| ~ spl5_30 ),
inference(superposition,[],[f21,f450]) ).
fof(f465,definition,
( spl5_32
<=> ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_32])],[avatar_definition]) ).
fof(f466,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,null_class) )
| ~ spl5_32 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( spl5_32
| ~ spl5_30 ),
inference(avatar_split_clause,[],[f461,f448,f465]) ).
fof(f470,definition,
( spl5_33
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(sF1,universal_class))
| ~ member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_33])],[avatar_definition]) ).
fof(f471,plain,
( ! [X0] :
( ~ member(X0,cross_product(sF1,universal_class))
| member(X0,null_class)
| ~ member(X0,sF3) )
| ~ spl5_33 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( spl5_33
| ~ spl5_30 ),
inference(avatar_split_clause,[],[f459,f448,f470]) ).
fof(f475,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_33 ),
inference(resolution,[],[f471,f139]) ).
fof(f478,definition,
( spl5_34
<=> ! [X0] :
( ~ member(X0,null_class)
| member(X0,cross_product(sF1,universal_class)) ) ),
introduced(definition,[new_symbols(definition,[spl5_34])],[avatar_definition]) ).
fof(f479,plain,
( ! [X0] :
( member(X0,cross_product(sF1,universal_class))
| ~ member(X0,null_class) )
| ~ spl5_34 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( spl5_34
| ~ spl5_30 ),
inference(avatar_split_clause,[],[f460,f448,f478]) ).
fof(f483,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X1,universal_class) )
| ~ spl5_34 ),
inference(resolution,[],[f479,f138]) ).
fof(f484,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) )
| ~ spl5_34 ),
inference(resolution,[],[f479,f137]) ).
fof(f553,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,[],[f437,f140]) ).
fof(f563,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,[],[f144,f553]) ).
fof(f564,plain,
( ! [X0] :
( null_class != null_class
| ~ member(y,domain_of(X0))
| regular(intersection(X0,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),first(regular(intersection(X0,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(sF1,universal_class)))),second(regular(intersection(X0,cross_product(sF1,universal_class))))))) )
| ~ spl5_27 ),
inference(superposition,[],[f428,f553]) ).
fof(f570,plain,
( ! [X0] :
( ~ member(y,domain_of(X0))
| regular(intersection(X0,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),first(regular(intersection(X0,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(sF1,universal_class)))),second(regular(intersection(X0,cross_product(sF1,universal_class))))))) )
| ~ spl5_27 ),
inference(trivial_inequality_removal,[],[f564]) ).
fof(f571,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,[],[f563]) ).
fof(f581,plain,
( ! [X0] :
( ~ member(X0,sF4)
| regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl5_9 ),
inference(superposition,[],[f571,f250]) ).
fof(f584,definition,
( spl5_36
<=> ! [X0] :
( ~ member(y,domain_of(X0))
| regular(intersection(X0,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),first(regular(intersection(X0,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(sF1,universal_class)))),second(regular(intersection(X0,cross_product(sF1,universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl5_36])],[avatar_definition]) ).
fof(f585,plain,
( ! [X0] :
( ~ member(y,domain_of(X0))
| regular(intersection(X0,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),first(regular(intersection(X0,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(sF1,universal_class)))),second(regular(intersection(X0,cross_product(sF1,universal_class))))))) )
| ~ spl5_36 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( spl5_36
| ~ spl5_27 ),
inference(avatar_split_clause,[],[f570,f427,f584]) ).
fof(f588,definition,
( spl5_37
<=> ! [X0] :
( ~ member(X0,sF4)
| regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl5_37])],[avatar_definition]) ).
fof(f589,plain,
( ! [X0] :
( ~ member(X0,sF4)
| regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl5_37 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f590,plain,
( spl5_37
| ~ spl5_9 ),
inference(avatar_split_clause,[],[f581,f248,f588]) ).
fof(f593,plain,
( ! [X0] :
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))))))
| subclass(sF4,X0) )
| ~ spl5_37 ),
inference(resolution,[],[f589,f2]) ).
fof(f598,definition,
( spl5_38
<=> ! [X0] :
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))))))
| subclass(sF4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_38])],[avatar_definition]) ).
fof(f599,plain,
( ! [X0] :
( subclass(sF4,X0)
| regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,X0),not_subclass_element(sF4,X0)),universal_class))))))) )
| ~ spl5_38 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( spl5_38
| ~ spl5_37 ),
inference(avatar_split_clause,[],[f593,f588,f598]) ).
fof(f605,plain,
( ~ member(y,sF4)
| regular(intersection(sF3,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),first(regular(intersection(sF3,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class)))))))
| ~ spl5_9
| ~ spl5_36 ),
inference(superposition,[],[f585,f250]) ).
fof(f694,definition,
( spl5_42
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_42])],[avatar_definition]) ).
fof(f695,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_42 ),
inference(avatar_component_clause,[],[f694]) ).
fof(f696,plain,
( spl5_42
| ~ spl5_33 ),
inference(avatar_split_clause,[],[f475,f470,f694]) ).
fof(f709,definition,
( spl5_43
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_43])],[avatar_definition]) ).
fof(f710,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) )
| ~ spl5_43 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( spl5_43
| ~ spl5_34 ),
inference(avatar_split_clause,[],[f484,f478,f709]) ).
fof(f722,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| ~ member(X0,X1)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(resolution,[],[f142,f139]) ).
fof(f806,definition,
( spl5_48
<=> y = regular(sF1) ),
introduced(definition,[new_symbols(definition,[spl5_48])],[avatar_definition]) ).
fof(f808,plain,
( y = regular(sF1)
| ~ spl5_48 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f810,definition,
( spl5_49
<=> null_class = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_49])],[avatar_definition]) ).
fof(f812,plain,
( null_class = sF1
| ~ spl5_49 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f813,plain,
( spl5_48
| spl5_49
| ~ spl5_17 ),
inference(avatar_split_clause,[],[f441,f303,f810,f806]) ).
fof(f815,plain,
( null_class = intersection(sF1,y)
| null_class = sF1
| ~ spl5_48 ),
inference(superposition,[],[f70,f808]) ).
fof(f904,plain,
( ! [X0,X1] :
( member(X0,X1)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3) )
| ~ spl5_12 ),
inference(resolution,[],[f141,f271]) ).
fof(f915,definition,
( spl5_57
<=> ! [X0,X1] :
( member(X0,X1)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_57])],[avatar_definition]) ).
fof(f916,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| member(X0,X1) )
| ~ spl5_57 ),
inference(avatar_component_clause,[],[f915]) ).
fof(f917,plain,
( spl5_57
| ~ spl5_12 ),
inference(avatar_split_clause,[],[f904,f270,f915]) ).
fof(f1055,definition,
( spl5_71
<=> member(y,y) ),
introduced(definition,[new_symbols(definition,[spl5_71])],[avatar_definition]) ).
fof(f1056,plain,
( member(y,y)
| ~ spl5_71 ),
inference(avatar_component_clause,[],[f1055]) ).
fof(f1431,definition,
( spl5_93
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl5_93])],[avatar_definition]) ).
fof(f1432,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X1,universal_class) )
| ~ spl5_93 ),
inference(avatar_component_clause,[],[f1431]) ).
fof(f1433,plain,
( spl5_93
| ~ spl5_34 ),
inference(avatar_split_clause,[],[f483,f478,f1431]) ).
fof(f1510,definition,
( spl5_98
<=> null_class = intersection(sF1,y) ),
introduced(definition,[new_symbols(definition,[spl5_98])],[avatar_definition]) ).
fof(f1512,plain,
( null_class = intersection(sF1,y)
| ~ spl5_98 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1513,plain,
( spl5_49
| spl5_98
| ~ spl5_48 ),
inference(avatar_split_clause,[],[f815,f806,f1510,f810]) ).
fof(f1516,plain,
( member(y,null_class)
| ~ spl5_18
| ~ spl5_49 ),
inference(superposition,[],[f309,f812]) ).
fof(f1546,definition,
( spl5_99
<=> member(y,null_class) ),
introduced(definition,[new_symbols(definition,[spl5_99])],[avatar_definition]) ).
fof(f1547,plain,
( ~ member(y,null_class)
| spl5_99 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1548,plain,
( member(y,null_class)
| ~ spl5_99 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1549,plain,
( spl5_99
| ~ spl5_18
| ~ spl5_49 ),
inference(avatar_split_clause,[],[f1516,f810,f307,f1546]) ).
fof(f1553,plain,
( ! [X0] :
( member(y,X0)
| null_class = X0 )
| ~ spl5_99 ),
inference(resolution,[],[f1548,f419]) ).
fof(f1565,plain,
( regular(intersection(sF3,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),first(regular(intersection(sF3,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class)))))))
| ~ spl5_9
| ~ spl5_31
| ~ spl5_36 ),
inference(forward_subsumption_resolution,[],[f605,f454]) ).
fof(f1585,definition,
( spl5_100
<=> ! [X0] :
( member(y,X0)
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_100])],[avatar_definition]) ).
fof(f1586,plain,
( ! [X0] :
( member(y,X0)
| null_class = X0 )
| ~ spl5_100 ),
inference(avatar_component_clause,[],[f1585]) ).
fof(f1587,plain,
( spl5_100
| ~ spl5_99 ),
inference(avatar_split_clause,[],[f1553,f1546,f1585]) ).
fof(f1593,plain,
( ! [X0] :
( complement(X0) = null_class
| ~ member(y,X0) )
| ~ spl5_100 ),
inference(resolution,[],[f1586,f24]) ).
fof(f1611,definition,
( spl5_102
<=> ! [X0] :
( complement(X0) = null_class
| ~ member(y,X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_102])],[avatar_definition]) ).
fof(f1612,plain,
( ! [X0] :
( ~ member(y,X0)
| complement(X0) = null_class )
| ~ spl5_102 ),
inference(avatar_component_clause,[],[f1611]) ).
fof(f1613,plain,
( spl5_102
| ~ spl5_100 ),
inference(avatar_split_clause,[],[f1593,f1585,f1611]) ).
fof(f1614,plain,
( ! [X0] :
( complement(X0) = null_class
| null_class = X0 )
| ~ spl5_100
| ~ spl5_102 ),
inference(resolution,[],[f1612,f1586]) ).
fof(f1831,definition,
( spl5_117
<=> regular(intersection(sF3,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),first(regular(intersection(sF3,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl5_117])],[avatar_definition]) ).
fof(f1833,plain,
( regular(intersection(sF3,cross_product(sF1,universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),first(regular(intersection(sF3,cross_product(sF1,universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class)))))))
| ~ spl5_117 ),
inference(avatar_component_clause,[],[f1831]) ).
fof(f1834,plain,
( spl5_117
| ~ spl5_9
| ~ spl5_31
| ~ spl5_36 ),
inference(avatar_split_clause,[],[f1565,f584,f452,f248,f1831]) ).
fof(f2069,plain,
( ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF1) )
| ~ spl5_98 ),
inference(superposition,[],[f21,f1512]) ).
fof(f2079,definition,
( spl5_121
<=> ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_121])],[avatar_definition]) ).
fof(f2080,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,null_class) )
| ~ spl5_121 ),
inference(avatar_component_clause,[],[f2079]) ).
fof(f2081,plain,
( spl5_121
| ~ spl5_98 ),
inference(avatar_split_clause,[],[f2069,f1510,f2079]) ).
fof(f2231,plain,
( ! [X0] :
( ~ member(X0,null_class)
| y = X0 )
| ~ spl5_17
| ~ spl5_121 ),
inference(resolution,[],[f2080,f304]) ).
fof(f2273,definition,
( spl5_126
<=> ! [X0] :
( ~ member(X0,null_class)
| y = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_126])],[avatar_definition]) ).
fof(f2274,plain,
( ! [X0] :
( ~ member(X0,null_class)
| y = X0 )
| ~ spl5_126 ),
inference(avatar_component_clause,[],[f2273]) ).
fof(f2275,plain,
( spl5_126
| ~ spl5_17
| ~ spl5_121 ),
inference(avatar_split_clause,[],[f2231,f2079,f303,f2273]) ).
fof(f2396,plain,
( ! [X0,X1] :
( y = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_42
| ~ spl5_126 ),
inference(resolution,[],[f2274,f695]) ).
fof(f2631,definition,
( spl5_142
<=> ! [X0] :
( complement(X0) = null_class
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_142])],[avatar_definition]) ).
fof(f2632,plain,
( ! [X0] :
( complement(X0) = null_class
| null_class = X0 )
| ~ spl5_142 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2633,plain,
( spl5_142
| ~ spl5_100
| ~ spl5_102 ),
inference(avatar_split_clause,[],[f1614,f1611,f1585,f2631]) ).
fof(f2635,plain,
( ! [X0,X1] :
( ~ member(X0,null_class)
| ~ member(X0,X1)
| null_class = X1 )
| ~ spl5_142 ),
inference(superposition,[],[f24,f2632]) ).
fof(f2636,plain,
( ! [X0,X1] :
( ~ member(X0,null_class)
| null_class = X1 )
| ~ spl5_142 ),
inference(forward_subsumption_resolution,[],[f2635,f419]) ).
fof(f2638,definition,
( spl5_143
<=> ! [X1] : null_class = X1 ),
introduced(definition,[new_symbols(definition,[spl5_143])],[avatar_definition]) ).
fof(f2639,plain,
( ! [X1] : null_class = X1
| ~ spl5_143 ),
inference(avatar_component_clause,[],[f2638]) ).
fof(f2641,definition,
( spl5_144
<=> ! [X0] : ~ member(X0,null_class) ),
introduced(definition,[new_symbols(definition,[spl5_144])],[avatar_definition]) ).
fof(f2642,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl5_144 ),
inference(avatar_component_clause,[],[f2641]) ).
fof(f2643,plain,
( spl5_143
| spl5_144
| ~ spl5_142 ),
inference(avatar_split_clause,[],[f2636,f2631,f2641,f2638]) ).
fof(f2644,plain,
( ! [X0,X1] : X0 = X1
| ~ spl5_143 ),
inference(superposition,[],[f2639,f2639]) ).
fof(f3020,plain,
( null_class != sF0
| spl5_13
| ~ spl5_143 ),
inference(superposition,[],[f276,f2639]) ).
fof(f3466,plain,
( $false
| spl5_13
| ~ spl5_143 ),
inference(forward_subsumption_resolution,[],[f3020,f2644]) ).
fof(f3467,plain,
( spl5_13
| ~ spl5_143 ),
inference(avatar_contradiction_clause,[],[f3466]) ).
fof(f3937,plain,
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF2)
| member(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1)
| ~ spl5_16
| ~ spl5_117 ),
inference(superposition,[],[f297,f1833]) ).
fof(f3942,definition,
( spl5_145
<=> member(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1) ),
introduced(definition,[new_symbols(definition,[spl5_145])],[avatar_definition]) ).
fof(f3944,plain,
( member(second(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1)
| ~ spl5_145 ),
inference(avatar_component_clause,[],[f3942]) ).
fof(f3946,definition,
( spl5_146
<=> member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl5_146])],[avatar_definition]) ).
fof(f3948,plain,
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF2)
| spl5_146 ),
inference(avatar_component_clause,[],[f3946]) ).
fof(f3949,plain,
( spl5_145
| ~ spl5_146
| ~ spl5_16
| ~ spl5_117 ),
inference(avatar_split_clause,[],[f3937,f1831,f296,f3946,f3942]) ).
fof(f3959,plain,
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF3)
| ~ spl5_11
| spl5_146 ),
inference(resolution,[],[f267,f3948]) ).
fof(f3961,definition,
( spl5_147
<=> member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF3) ),
introduced(definition,[new_symbols(definition,[spl5_147])],[avatar_definition]) ).
fof(f3962,plain,
( member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF3)
| ~ spl5_147 ),
inference(avatar_component_clause,[],[f3961]) ).
fof(f3963,plain,
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF3)
| spl5_147 ),
inference(avatar_component_clause,[],[f3961]) ).
fof(f3964,plain,
( ~ spl5_147
| ~ spl5_11
| spl5_146 ),
inference(avatar_split_clause,[],[f3959,f3946,f266,f3961]) ).
fof(f3988,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),X0) )
| ~ spl5_117 ),
inference(superposition,[],[f137,f1833]) ).
fof(f3991,definition,
( spl5_148
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_148])],[avatar_definition]) ).
fof(f3992,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),X0) )
| ~ spl5_148 ),
inference(avatar_component_clause,[],[f3991]) ).
fof(f3993,plain,
( spl5_148
| ~ spl5_117 ),
inference(avatar_split_clause,[],[f3988,f1831,f3991]) ).
fof(f4191,plain,
( ~ member(regular(intersection(sF3,cross_product(sF1,universal_class))),sF3)
| member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class)))))
| ~ spl5_57
| ~ spl5_117 ),
inference(superposition,[],[f916,f1833]) ).
fof(f4192,plain,
( null_class = intersection(sF3,cross_product(sF1,universal_class))
| spl5_147 ),
inference(resolution,[],[f438,f3963]) ).
fof(f4210,plain,
( $false
| spl5_30
| spl5_147 ),
inference(forward_subsumption_resolution,[],[f4192,f449]) ).
fof(f4211,plain,
( spl5_30
| spl5_147 ),
inference(avatar_contradiction_clause,[],[f4210]) ).
fof(f4213,plain,
( member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class)))))
| ~ spl5_57
| ~ spl5_117
| ~ spl5_147 ),
inference(forward_subsumption_resolution,[],[f4191,f3962]) ).
fof(f4218,plain,
( y = second(regular(intersection(sF3,cross_product(sF1,universal_class))))
| ~ spl5_17
| ~ spl5_145 ),
inference(resolution,[],[f3944,f304]) ).
fof(f4222,definition,
( spl5_152
<=> y = second(regular(intersection(sF3,cross_product(sF1,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl5_152])],[avatar_definition]) ).
fof(f4225,plain,
( spl5_152
| ~ spl5_17
| ~ spl5_145 ),
inference(avatar_split_clause,[],[f4218,f3942,f303,f4222]) ).
fof(f4248,definition,
( spl5_154
<=> member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class))))) ),
introduced(definition,[new_symbols(definition,[spl5_154])],[avatar_definition]) ).
fof(f4251,plain,
( spl5_154
| ~ spl5_57
| ~ spl5_117
| ~ spl5_147 ),
inference(avatar_split_clause,[],[f4213,f3961,f1831,f915,f4248]) ).
fof(f4392,plain,
( null_class = intersection(sF3,cross_product(sF1,universal_class))
| member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1)
| ~ spl5_148 ),
inference(resolution,[],[f437,f3992]) ).
fof(f4409,plain,
( member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1)
| spl5_30
| ~ spl5_148 ),
inference(forward_subsumption_resolution,[],[f4392,f449]) ).
fof(f4413,definition,
( spl5_156
<=> member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1) ),
introduced(definition,[new_symbols(definition,[spl5_156])],[avatar_definition]) ).
fof(f4415,plain,
( member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),sF1)
| ~ spl5_156 ),
inference(avatar_component_clause,[],[f4413]) ).
fof(f4416,plain,
( spl5_156
| spl5_30
| ~ spl5_148 ),
inference(avatar_split_clause,[],[f4409,f3991,f448,f4413]) ).
fof(f4417,plain,
( y = first(regular(intersection(sF3,cross_product(sF1,universal_class))))
| ~ spl5_17
| ~ spl5_156 ),
inference(resolution,[],[f4415,f304]) ).
fof(f4420,definition,
( spl5_157
<=> y = first(regular(intersection(sF3,cross_product(sF1,universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl5_157])],[avatar_definition]) ).
fof(f4423,plain,
( spl5_157
| ~ spl5_17
| ~ spl5_156 ),
inference(avatar_split_clause,[],[f4417,f4413,f303,f4420]) ).
fof(f4424,plain,
( y != first(regular(intersection(sF3,cross_product(sF1,universal_class))))
| y != second(regular(intersection(sF3,cross_product(sF1,universal_class))))
| member(y,y)
| ~ member(first(regular(intersection(sF3,cross_product(sF1,universal_class)))),second(regular(intersection(sF3,cross_product(sF1,universal_class))))) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f4445,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,y)
| ~ member(X0,sF1) )
| ~ spl5_98 ),
inference(superposition,[],[f23,f1512]) ).
fof(f4525,definition,
( spl5_160
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,y)
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_160])],[avatar_definition]) ).
fof(f4526,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,y)
| ~ member(X0,sF1) )
| ~ spl5_160 ),
inference(avatar_component_clause,[],[f4525]) ).
fof(f4527,plain,
( spl5_160
| ~ spl5_98 ),
inference(avatar_split_clause,[],[f4445,f1510,f4525]) ).
fof(f4534,plain,
( ~ member(y,y)
| ~ member(y,sF1)
| spl5_99
| ~ spl5_160 ),
inference(resolution,[],[f4526,f1547]) ).
fof(f4536,plain,
( ~ member(y,sF1)
| ~ spl5_71
| spl5_99
| ~ spl5_160 ),
inference(forward_subsumption_resolution,[],[f4534,f1056]) ).
fof(f4539,plain,
( $false
| ~ spl5_18
| ~ spl5_71
| spl5_99
| ~ spl5_160 ),
inference(forward_subsumption_resolution,[],[f4536,f309]) ).
fof(f4540,plain,
( ~ spl5_18
| ~ spl5_71
| spl5_99
| ~ spl5_160 ),
inference(avatar_contradiction_clause,[],[f4539]) ).
fof(f4569,plain,
( $false
| ~ spl5_99
| ~ spl5_144 ),
inference(unit_resulting_resolution,[],[f1,f1548,f188,f2642]) ).
fof(f4582,plain,
( ~ spl5_99
| ~ spl5_144 ),
inference(avatar_contradiction_clause,[],[f4569]) ).
fof(f5169,definition,
( spl5_174
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X0,sF1)
| ~ member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl5_174])],[avatar_definition]) ).
fof(f5170,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X0,sF1)
| ~ member(X1,universal_class) )
| ~ spl5_174 ),
inference(avatar_component_clause,[],[f5169]) ).
fof(f5172,plain,
( ! [X0,X1] :
( ~ member(X0,sF1)
| ~ member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class) )
| ~ spl5_32
| ~ spl5_174 ),
inference(resolution,[],[f5170,f466]) ).
fof(f5185,plain,
( ! [X0,X1] :
( ~ member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class) )
| ~ spl5_32
| ~ spl5_43
| ~ spl5_174 ),
inference(forward_subsumption_resolution,[],[f5172,f710]) ).
fof(f5186,plain,
( ! [X0,X1] : ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ spl5_32
| ~ spl5_43
| ~ spl5_93
| ~ spl5_174 ),
inference(forward_subsumption_resolution,[],[f5185,f1432]) ).
fof(f5201,definition,
( spl5_176
<=> ! [X0,X1] : ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class) ),
introduced(definition,[new_symbols(definition,[spl5_176])],[avatar_definition]) ).
fof(f5202,plain,
( ! [X0,X1] : ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ spl5_176 ),
inference(avatar_component_clause,[],[f5201]) ).
fof(f5203,plain,
( spl5_176
| ~ spl5_32
| ~ spl5_43
| ~ spl5_93
| ~ spl5_174 ),
inference(avatar_split_clause,[],[f5186,f5169,f1431,f709,f465,f5201]) ).
fof(f7239,definition,
( spl5_287
<=> null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_287])],[avatar_definition]) ).
fof(f7240,plain,
( null_class != intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| spl5_287 ),
inference(avatar_component_clause,[],[f7239]) ).
fof(f7241,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ spl5_287 ),
inference(avatar_component_clause,[],[f7239]) ).
fof(f7248,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_287 ),
inference(superposition,[],[f23,f7241]) ).
fof(f7299,definition,
( spl5_290
<=> member(not_subclass_element(sF0,sF4),x) ),
introduced(definition,[new_symbols(definition,[spl5_290])],[avatar_definition]) ).
fof(f7300,plain,
( member(not_subclass_element(sF0,sF4),x)
| ~ spl5_290 ),
inference(avatar_component_clause,[],[f7299]) ).
fof(f7301,plain,
( ~ member(not_subclass_element(sF0,sF4),x)
| spl5_290 ),
inference(avatar_component_clause,[],[f7299]) ).
fof(f7307,definition,
( spl5_292
<=> subclass(sF0,sF4) ),
introduced(definition,[new_symbols(definition,[spl5_292])],[avatar_definition]) ).
fof(f7308,plain,
( subclass(sF0,sF4)
| ~ spl5_292 ),
inference(avatar_component_clause,[],[f7307]) ).
fof(f7309,plain,
( ~ subclass(sF0,sF4)
| spl5_292 ),
inference(avatar_component_clause,[],[f7307]) ).
fof(f7311,plain,
( subclass(sF0,sF4)
| ~ spl5_22
| spl5_290 ),
inference(resolution,[],[f7301,f377]) ).
fof(f7315,plain,
( spl5_292
| ~ spl5_22
| spl5_290 ),
inference(avatar_split_clause,[],[f7311,f7299,f376,f7307]) ).
fof(f7318,plain,
( ~ subclass(sF4,sF0)
| sF0 = sF4
| ~ spl5_292 ),
inference(resolution,[],[f7308,f7]) ).
fof(f7319,plain,
( ~ subclass(sF4,sF0)
| spl5_13
| ~ spl5_292 ),
inference(forward_subsumption_resolution,[],[f7318,f276]) ).
fof(f7329,definition,
( spl5_294
<=> subclass(sF4,sF0) ),
introduced(definition,[new_symbols(definition,[spl5_294])],[avatar_definition]) ).
fof(f7331,plain,
( ~ subclass(sF4,sF0)
| spl5_294 ),
inference(avatar_component_clause,[],[f7329]) ).
fof(f7332,plain,
( ~ spl5_294
| spl5_13
| ~ spl5_292 ),
inference(avatar_split_clause,[],[f7319,f7307,f274,f7329]) ).
fof(f7333,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))))))
| ~ spl5_38
| spl5_294 ),
inference(resolution,[],[f7331,f599]) ).
fof(f7335,definition,
( spl5_295
<=> regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl5_295])],[avatar_definition]) ).
fof(f7337,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))))))
| ~ spl5_295 ),
inference(avatar_component_clause,[],[f7335]) ).
fof(f7338,plain,
( spl5_295
| ~ spl5_38
| spl5_294 ),
inference(avatar_split_clause,[],[f7333,f7329,f598,f7335]) ).
fof(f7346,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),X0) )
| ~ spl5_295 ),
inference(superposition,[],[f137,f7337]) ).
fof(f7351,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF2)
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),x)
| ~ spl5_14
| ~ spl5_295 ),
inference(superposition,[],[f283,f7337]) ).
fof(f7352,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF2)
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_16
| ~ spl5_295 ),
inference(superposition,[],[f297,f7337]) ).
fof(f7357,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))))
| ~ spl5_57
| ~ spl5_295 ),
inference(superposition,[],[f916,f7337]) ).
fof(f7397,definition,
( spl5_297
<=> member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),x) ),
introduced(definition,[new_symbols(definition,[spl5_297])],[avatar_definition]) ).
fof(f7399,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),x)
| ~ spl5_297 ),
inference(avatar_component_clause,[],[f7397]) ).
fof(f7401,definition,
( spl5_298
<=> member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl5_298])],[avatar_definition]) ).
fof(f7402,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF2)
| ~ spl5_298 ),
inference(avatar_component_clause,[],[f7401]) ).
fof(f7403,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF2)
| spl5_298 ),
inference(avatar_component_clause,[],[f7401]) ).
fof(f7404,plain,
( spl5_297
| ~ spl5_298
| ~ spl5_14
| ~ spl5_295 ),
inference(avatar_split_clause,[],[f7351,f7335,f282,f7401,f7397]) ).
fof(f7405,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| ~ spl5_11
| spl5_298 ),
inference(resolution,[],[f7403,f267]) ).
fof(f7413,definition,
( spl5_299
<=> member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3) ),
introduced(definition,[new_symbols(definition,[spl5_299])],[avatar_definition]) ).
fof(f7414,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| ~ spl5_299 ),
inference(avatar_component_clause,[],[f7413]) ).
fof(f7415,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| spl5_299 ),
inference(avatar_component_clause,[],[f7413]) ).
fof(f7416,plain,
( ~ spl5_299
| ~ spl5_11
| spl5_298 ),
inference(avatar_split_clause,[],[f7405,f7401,f266,f7413]) ).
fof(f7417,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| spl5_299 ),
inference(resolution,[],[f7415,f438]) ).
fof(f7427,definition,
( spl5_300
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_300])],[avatar_definition]) ).
fof(f7428,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),X0) )
| ~ spl5_300 ),
inference(avatar_component_clause,[],[f7427]) ).
fof(f7429,plain,
( spl5_300
| ~ spl5_295 ),
inference(avatar_split_clause,[],[f7346,f7335,f7427]) ).
fof(f7433,definition,
( spl5_301
<=> null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_301])],[avatar_definition]) ).
fof(f7434,plain,
( null_class != intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| spl5_301 ),
inference(avatar_component_clause,[],[f7433]) ).
fof(f7435,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| ~ spl5_301 ),
inference(avatar_component_clause,[],[f7433]) ).
fof(f7436,plain,
( spl5_301
| spl5_299 ),
inference(avatar_split_clause,[],[f7417,f7413,f7433]) ).
fof(f7439,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_16
| ~ spl5_295
| ~ spl5_298 ),
inference(forward_subsumption_resolution,[],[f7352,f7402]) ).
fof(f7441,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))))
| ~ spl5_57
| ~ spl5_295
| ~ spl5_299 ),
inference(forward_subsumption_resolution,[],[f7357,f7414]) ).
fof(f7455,definition,
( spl5_302
<=> member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1) ),
introduced(definition,[new_symbols(definition,[spl5_302])],[avatar_definition]) ).
fof(f7457,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_302 ),
inference(avatar_component_clause,[],[f7455]) ).
fof(f7458,plain,
( spl5_302
| ~ spl5_16
| ~ spl5_295
| ~ spl5_298 ),
inference(avatar_split_clause,[],[f7439,f7401,f7335,f296,f7455]) ).
fof(f7459,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)))
| null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| ~ spl5_300 ),
inference(resolution,[],[f7428,f437]) ).
fof(f7468,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)))
| ~ spl5_300
| spl5_301 ),
inference(forward_subsumption_resolution,[],[f7459,f7434]) ).
fof(f7475,plain,
( y = second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_17
| ~ spl5_302 ),
inference(resolution,[],[f7457,f304]) ).
fof(f7488,definition,
( spl5_303
<=> y = second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl5_303])],[avatar_definition]) ).
fof(f7491,plain,
( spl5_303
| ~ spl5_17
| ~ spl5_302 ),
inference(avatar_split_clause,[],[f7475,f7455,f303,f7488]) ).
fof(f7493,definition,
( spl5_304
<=> member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0))) ),
introduced(definition,[new_symbols(definition,[spl5_304])],[avatar_definition]) ).
fof(f7495,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)))
| ~ spl5_304 ),
inference(avatar_component_clause,[],[f7493]) ).
fof(f7496,plain,
( spl5_304
| ~ spl5_300
| spl5_301 ),
inference(avatar_split_clause,[],[f7468,f7433,f7427,f7493]) ).
fof(f7505,plain,
( not_subclass_element(sF4,sF0) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| not_subclass_element(sF4,sF0) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_304 ),
inference(resolution,[],[f7495,f8]) ).
fof(f7510,plain,
( not_subclass_element(sF4,sF0) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_304 ),
inference(duplicate_literal_removal,[],[f7505]) ).
fof(f7513,definition,
( spl5_305
<=> not_subclass_element(sF4,sF0) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl5_305])],[avatar_definition]) ).
fof(f7515,plain,
( not_subclass_element(sF4,sF0) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_305 ),
inference(avatar_component_clause,[],[f7513]) ).
fof(f7516,plain,
( spl5_305
| ~ spl5_304 ),
inference(avatar_split_clause,[],[f7510,f7493,f7513]) ).
fof(f7521,plain,
( member(not_subclass_element(sF4,sF0),x)
| ~ spl5_297
| ~ spl5_305 ),
inference(superposition,[],[f7399,f7515]) ).
fof(f7534,definition,
( spl5_307
<=> member(not_subclass_element(sF4,sF0),x) ),
introduced(definition,[new_symbols(definition,[spl5_307])],[avatar_definition]) ).
fof(f7536,plain,
( member(not_subclass_element(sF4,sF0),x)
| ~ spl5_307 ),
inference(avatar_component_clause,[],[f7534]) ).
fof(f7537,plain,
( spl5_307
| ~ spl5_297
| ~ spl5_305 ),
inference(avatar_split_clause,[],[f7521,f7513,f7397,f7534]) ).
fof(f7538,plain,
( ~ member(not_subclass_element(sF4,sF0),y)
| subclass(sF4,sF0)
| ~ spl5_19
| ~ spl5_307 ),
inference(resolution,[],[f7536,f330]) ).
fof(f7540,plain,
( ~ member(not_subclass_element(sF4,sF0),y)
| ~ spl5_19
| spl5_294
| ~ spl5_307 ),
inference(forward_subsumption_resolution,[],[f7538,f7331]) ).
fof(f7542,definition,
( spl5_308
<=> member(not_subclass_element(sF4,sF0),y) ),
introduced(definition,[new_symbols(definition,[spl5_308])],[avatar_definition]) ).
fof(f7545,plain,
( ~ spl5_308
| ~ spl5_19
| spl5_294
| ~ spl5_307 ),
inference(avatar_split_clause,[],[f7540,f7534,f7329,f329,f7542]) ).
fof(f7603,definition,
( spl5_314
<=> member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))) ),
introduced(definition,[new_symbols(definition,[spl5_314])],[avatar_definition]) ).
fof(f7606,plain,
( spl5_314
| ~ spl5_57
| ~ spl5_295
| ~ spl5_299 ),
inference(avatar_split_clause,[],[f7441,f7413,f7335,f915,f7603]) ).
fof(f7607,plain,
( not_subclass_element(sF4,sF0) != first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| y != second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))))
| member(not_subclass_element(sF4,sF0),y) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f7659,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF4,sF0),domain_of(sF3))
| ~ spl5_301 ),
inference(superposition,[],[f144,f7435]) ).
fof(f7671,plain,
( ~ member(not_subclass_element(sF4,sF0),domain_of(sF3))
| ~ spl5_301 ),
inference(trivial_inequality_removal,[],[f7659]) ).
fof(f7674,plain,
( ~ member(not_subclass_element(sF4,sF0),sF4)
| ~ spl5_9
| ~ spl5_301 ),
inference(forward_demodulation,[],[f7671,f250]) ).
fof(f7677,definition,
( spl5_315
<=> member(not_subclass_element(sF4,sF0),sF4) ),
introduced(definition,[new_symbols(definition,[spl5_315])],[avatar_definition]) ).
fof(f7679,plain,
( ~ member(not_subclass_element(sF4,sF0),sF4)
| spl5_315 ),
inference(avatar_component_clause,[],[f7677]) ).
fof(f7680,plain,
( ~ spl5_315
| ~ spl5_9
| ~ spl5_301 ),
inference(avatar_split_clause,[],[f7674,f7433,f248,f7677]) ).
fof(f7681,plain,
( subclass(sF4,sF0)
| spl5_315 ),
inference(resolution,[],[f7679,f2]) ).
fof(f7721,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),X0)
| null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class)) )
| ~ spl5_29
| spl5_292 ),
inference(resolution,[],[f7309,f444]) ).
fof(f8244,definition,
( spl5_345
<=> ! [X1] : ~ member(not_subclass_element(sF0,sF4),X1) ),
introduced(definition,[new_symbols(definition,[spl5_345])],[avatar_definition]) ).
fof(f8245,plain,
( ! [X1] : ~ member(not_subclass_element(sF0,sF4),X1)
| ~ spl5_345 ),
inference(avatar_component_clause,[],[f8244]) ).
fof(f8438,definition,
( spl5_355
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_355])],[avatar_definition]) ).
fof(f8439,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| member(X0,null_class)
| ~ member(X0,sF3) )
| ~ spl5_355 ),
inference(avatar_component_clause,[],[f8438]) ).
fof(f8440,plain,
( spl5_355
| ~ spl5_287 ),
inference(avatar_split_clause,[],[f7248,f7239,f8438]) ).
fof(f8443,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4))) )
| ~ spl5_355 ),
inference(resolution,[],[f8439,f139]) ).
fof(f8459,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4))) )
| ~ spl5_176
| ~ spl5_355 ),
inference(forward_subsumption_resolution,[],[f8443,f5202]) ).
fof(f8462,definition,
( spl5_356
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4))) ) ),
introduced(definition,[new_symbols(definition,[spl5_356])],[avatar_definition]) ).
fof(f8463,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4))) )
| ~ spl5_356 ),
inference(avatar_component_clause,[],[f8462]) ).
fof(f8464,plain,
( spl5_356
| ~ spl5_176
| ~ spl5_355 ),
inference(avatar_split_clause,[],[f8459,f8438,f5201,f8462]) ).
fof(f8466,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),element_relation) )
| ~ spl5_15
| ~ spl5_356 ),
inference(resolution,[],[f8463,f290]) ).
fof(f8481,definition,
( spl5_357
<=> ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl5_357])],[avatar_definition]) ).
fof(f8482,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF2)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),element_relation) )
| ~ spl5_357 ),
inference(avatar_component_clause,[],[f8481]) ).
fof(f8483,plain,
( spl5_357
| ~ spl5_15
| ~ spl5_356 ),
inference(avatar_split_clause,[],[f8466,f8462,f289,f8481]) ).
fof(f8484,plain,
( ! [X0,X1] :
( ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| ~ member(X1,sF1)
| ~ member(X0,x) )
| ~ spl5_23
| ~ spl5_357 ),
inference(resolution,[],[f8482,f391]) ).
fof(f8513,definition,
( spl5_359
<=> ! [X0,X1] :
( ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| ~ member(X1,sF1)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_359])],[avatar_definition]) ).
fof(f8514,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X1,sF1)
| ~ member(X0,x) )
| ~ spl5_359 ),
inference(avatar_component_clause,[],[f8513]) ).
fof(f8515,plain,
( spl5_359
| ~ spl5_23
| ~ spl5_357 ),
inference(avatar_split_clause,[],[f8484,f8481,f390,f8513]) ).
fof(f8516,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X0,sF1)
| ~ member(X1,x)
| ~ member(X1,X0)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class) )
| ~ spl5_359 ),
inference(resolution,[],[f8514,f722]) ).
fof(f8528,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X0,sF1)
| ~ member(X1,x)
| ~ member(X1,X0)
| ~ member(X1,universal_class) )
| ~ spl5_359 ),
inference(duplicate_literal_removal,[],[f8516]) ).
fof(f8537,definition,
( spl5_360
<=> ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X0,sF1)
| ~ member(X1,x)
| ~ member(X1,X0)
| ~ member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl5_360])],[avatar_definition]) ).
fof(f8538,plain,
( ! [X0,X1] :
( ~ member(X1,unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)))
| ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(X1,x)
| ~ member(X1,X0)
| ~ member(X1,universal_class) )
| ~ spl5_360 ),
inference(avatar_component_clause,[],[f8537]) ).
fof(f8539,plain,
( spl5_360
| ~ spl5_359 ),
inference(avatar_split_clause,[],[f8528,f8513,f8537]) ).
fof(f8541,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(not_subclass_element(sF0,sF4),x)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(not_subclass_element(sF0,sF4),universal_class)
| ~ member(not_subclass_element(sF0,sF4),X1) )
| ~ spl5_360 ),
inference(resolution,[],[f8538,f351]) ).
fof(f8555,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),x)
| ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(not_subclass_element(sF0,sF4),universal_class) )
| ~ spl5_360 ),
inference(condensation,[],[f8541]) ).
fof(f8559,plain,
( ! [X0] :
( ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(not_subclass_element(sF0,sF4),universal_class) )
| ~ spl5_290
| ~ spl5_360 ),
inference(forward_subsumption_resolution,[],[f8555,f7300]) ).
fof(f8563,definition,
( spl5_361
<=> member(not_subclass_element(sF0,sF4),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_361])],[avatar_definition]) ).
fof(f8565,plain,
( ~ member(not_subclass_element(sF0,sF4),universal_class)
| spl5_361 ),
inference(avatar_component_clause,[],[f8563]) ).
fof(f8567,definition,
( spl5_362
<=> ! [X0] :
( ~ member(X0,universal_class)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_362])],[avatar_definition]) ).
fof(f8568,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(X0,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_362 ),
inference(avatar_component_clause,[],[f8567]) ).
fof(f8569,plain,
( ~ spl5_361
| spl5_362
| ~ spl5_290
| ~ spl5_360 ),
inference(avatar_split_clause,[],[f8559,f8537,f7299,f8567,f8563]) ).
fof(f8573,plain,
( ~ member(y,universal_class)
| ~ member(y,sF1)
| subclass(sF0,sF4)
| ~ spl5_24
| ~ spl5_362 ),
inference(resolution,[],[f8568,f406]) ).
fof(f8613,plain,
( ~ member(y,sF1)
| subclass(sF0,sF4)
| ~ spl5_4
| ~ spl5_24
| ~ spl5_362 ),
inference(forward_subsumption_resolution,[],[f8573,f222]) ).
fof(f8628,plain,
( subclass(sF0,sF4)
| ~ spl5_4
| ~ spl5_18
| ~ spl5_24
| ~ spl5_362 ),
inference(forward_subsumption_resolution,[],[f8613,f309]) ).
fof(f8634,plain,
( $false
| ~ spl5_4
| ~ spl5_18
| ~ spl5_24
| spl5_292
| ~ spl5_362 ),
inference(forward_subsumption_resolution,[],[f8628,f7309]) ).
fof(f8635,plain,
( ~ spl5_4
| ~ spl5_18
| ~ spl5_24
| spl5_292
| ~ spl5_362 ),
inference(avatar_contradiction_clause,[],[f8634]) ).
fof(f8638,plain,
( $false
| ~ spl5_290
| spl5_361 ),
inference(unit_resulting_resolution,[],[f1,f4,f7300,f8565]) ).
fof(f8641,plain,
( ~ spl5_290
| spl5_361 ),
inference(avatar_contradiction_clause,[],[f8638]) ).
fof(f8653,plain,
( ! [X0] : ~ member(not_subclass_element(sF0,sF4),X0)
| ~ spl5_29
| spl5_287
| spl5_292 ),
inference(forward_subsumption_resolution,[],[f7721,f7240]) ).
fof(f8655,plain,
( spl5_345
| ~ spl5_29
| spl5_287
| spl5_292 ),
inference(avatar_split_clause,[],[f8653,f7307,f7239,f443,f8244]) ).
fof(f8706,plain,
( subclass(sF0,sF4)
| ~ spl5_345 ),
inference(resolution,[],[f8245,f2]) ).
fof(f8748,plain,
( $false
| spl5_292
| ~ spl5_345 ),
inference(forward_subsumption_resolution,[],[f8706,f7309]) ).
fof(f8749,plain,
( spl5_292
| ~ spl5_345 ),
inference(avatar_contradiction_clause,[],[f8748]) ).
fof(f8772,plain,
( ! [X0,X1] :
( member(y,null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_42
| ~ spl5_126 ),
inference(forward_subsumption_demodulation,[],[f695,f2396]) ).
fof(f8778,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_42
| spl5_99
| ~ spl5_126 ),
inference(forward_subsumption_resolution,[],[f8772,f1547]) ).
fof(f9108,plain,
( spl5_174
| ~ spl5_42
| spl5_99
| ~ spl5_126 ),
inference(avatar_split_clause,[],[f8778,f2273,f1546,f694,f5169]) ).
fof(f9191,plain,
( $false
| spl5_13
| ~ spl5_292
| spl5_315 ),
inference(forward_subsumption_resolution,[],[f7681,f7319]) ).
fof(f9192,plain,
( spl5_13
| ~ spl5_292
| spl5_315 ),
inference(avatar_contradiction_clause,[],[f9191]) ).
cnf(s100,plain,
spl5_1,
inference(sat_conversion,[],[f206]) ).
cnf(s102,plain,
spl5_2,
inference(sat_conversion,[],[f211]) ).
cnf(s106,plain,
spl5_3,
inference(sat_conversion,[],[f218]) ).
cnf(s108,plain,
spl5_4,
inference(sat_conversion,[],[f223]) ).
cnf(s115,plain,
( ~ spl5_1
| spl5_7 ),
inference(sat_conversion,[],[f239]) ).
cnf(s119,plain,
( ~ spl5_4
| spl5_8 ),
inference(sat_conversion,[],[f245]) ).
cnf(s122,plain,
spl5_9,
inference(sat_conversion,[],[f251]) ).
cnf(s127,plain,
spl5_10,
inference(sat_conversion,[],[f261]) ).
cnf(s132,plain,
( ~ spl5_10
| spl5_11 ),
inference(sat_conversion,[],[f268]) ).
cnf(s134,plain,
( ~ spl5_10
| spl5_12 ),
inference(sat_conversion,[],[f272]) ).
cnf(s136,plain,
~ spl5_13,
inference(sat_conversion,[],[f277]) ).
cnf(s141,plain,
( ~ spl5_2
| spl5_14 ),
inference(sat_conversion,[],[f284]) ).
cnf(s146,plain,
( ~ spl5_10
| spl5_15 ),
inference(sat_conversion,[],[f291]) ).
cnf(s151,plain,
( ~ spl5_2
| spl5_16 ),
inference(sat_conversion,[],[f298]) ).
cnf(s155,plain,
( ~ spl5_3
| spl5_17 ),
inference(sat_conversion,[],[f305]) ).
cnf(s157,plain,
( ~ spl5_3
| ~ spl5_8
| spl5_18 ),
inference(sat_conversion,[],[f310]) ).
cnf(s173,plain,
( ~ spl5_7
| spl5_19 ),
inference(sat_conversion,[],[f331]) ).
cnf(s197,plain,
( ~ spl5_9
| spl5_20 ),
inference(sat_conversion,[],[f365]) ).
cnf(s204,plain,
( ~ spl5_1
| spl5_22 ),
inference(sat_conversion,[],[f378]) ).
cnf(s211,plain,
( ~ spl5_2
| spl5_23 ),
inference(sat_conversion,[],[f392]) ).
cnf(s219,plain,
( ~ spl5_1
| spl5_24 ),
inference(sat_conversion,[],[f407]) ).
cnf(s233,plain,
( ~ spl5_3
| spl5_27 ),
inference(sat_conversion,[],[f429]) ).
cnf(s235,plain,
( ~ spl5_3
| ~ spl5_4
| spl5_28 ),
inference(sat_conversion,[],[f433]) ).
cnf(s244,plain,
( ~ spl5_20
| spl5_29 ),
inference(sat_conversion,[],[f445]) ).
cnf(s247,plain,
( ~ spl5_9
| ~ spl5_28
| spl5_30
| spl5_31 ),
inference(sat_conversion,[],[f455]) ).
cnf(s255,plain,
( ~ spl5_30
| spl5_32 ),
inference(sat_conversion,[],[f467]) ).
cnf(s258,plain,
( ~ spl5_30
| spl5_33 ),
inference(sat_conversion,[],[f472]) ).
cnf(s264,plain,
( ~ spl5_30
| spl5_34 ),
inference(sat_conversion,[],[f480]) ).
cnf(s339,plain,
( ~ spl5_27
| spl5_36 ),
inference(sat_conversion,[],[f586]) ).
cnf(s341,plain,
( ~ spl5_9
| spl5_37 ),
inference(sat_conversion,[],[f590]) ).
cnf(s348,plain,
( ~ spl5_37
| spl5_38 ),
inference(sat_conversion,[],[f600]) ).
cnf(s385,plain,
( ~ spl5_33
| spl5_42 ),
inference(sat_conversion,[],[f696]) ).
cnf(s394,plain,
( ~ spl5_34
| spl5_43 ),
inference(sat_conversion,[],[f711]) ).
cnf(s457,plain,
( ~ spl5_17
| spl5_48
| spl5_49 ),
inference(sat_conversion,[],[f813]) ).
cnf(s511,plain,
( ~ spl5_12
| spl5_57 ),
inference(sat_conversion,[],[f917]) ).
cnf(s769,plain,
( ~ spl5_34
| spl5_93 ),
inference(sat_conversion,[],[f1433]) ).
cnf(s810,plain,
( ~ spl5_48
| spl5_49
| spl5_98 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s838,plain,
( ~ spl5_18
| ~ spl5_49
| spl5_99 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s880,plain,
( ~ spl5_99
| spl5_100 ),
inference(sat_conversion,[],[f1587]) ).
cnf(s891,plain,
( ~ spl5_100
| spl5_102 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s1034,plain,
( ~ spl5_9
| ~ spl5_31
| ~ spl5_36
| spl5_117 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s1186,plain,
( ~ spl5_98
| spl5_121 ),
inference(sat_conversion,[],[f2081]) ).
cnf(s1347,plain,
( ~ spl5_17
| ~ spl5_121
| spl5_126 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s1505,plain,
( ~ spl5_100
| ~ spl5_102
| spl5_142 ),
inference(sat_conversion,[],[f2633]) ).
cnf(s1508,plain,
( ~ spl5_142
| spl5_143
| spl5_144 ),
inference(sat_conversion,[],[f2643]) ).
cnf(s1591,plain,
( spl5_13
| ~ spl5_143 ),
inference(sat_conversion,[],[f3467]) ).
cnf(s2481,plain,
( ~ spl5_16
| ~ spl5_117
| spl5_145
| ~ spl5_146 ),
inference(sat_conversion,[],[f3949]) ).
cnf(s2496,plain,
( ~ spl5_11
| spl5_146
| ~ spl5_147 ),
inference(sat_conversion,[],[f3964]) ).
cnf(s2501,plain,
( ~ spl5_117
| spl5_148 ),
inference(sat_conversion,[],[f3993]) ).
cnf(s2534,plain,
( spl5_30
| spl5_147 ),
inference(sat_conversion,[],[f4211]) ).
cnf(s2541,plain,
( ~ spl5_17
| ~ spl5_145
| spl5_152 ),
inference(sat_conversion,[],[f4225]) ).
cnf(s2551,plain,
( ~ spl5_57
| ~ spl5_117
| ~ spl5_147
| spl5_154 ),
inference(sat_conversion,[],[f4251]) ).
cnf(s2563,plain,
( spl5_30
| ~ spl5_148
| spl5_156 ),
inference(sat_conversion,[],[f4416]) ).
cnf(s2566,plain,
( ~ spl5_17
| ~ spl5_156
| spl5_157 ),
inference(sat_conversion,[],[f4423]) ).
cnf(s2567,plain,
( spl5_71
| ~ spl5_152
| ~ spl5_154
| ~ spl5_157 ),
inference(sat_conversion,[],[f4424]) ).
cnf(s2595,plain,
( ~ spl5_98
| spl5_160 ),
inference(sat_conversion,[],[f4527]) ).
cnf(s2600,plain,
( ~ spl5_18
| ~ spl5_71
| spl5_99
| ~ spl5_160 ),
inference(sat_conversion,[],[f4540]) ).
cnf(s2673,plain,
( ~ spl5_99
| ~ spl5_144 ),
inference(sat_conversion,[],[f4582]) ).
cnf(s2988,plain,
( ~ spl5_32
| ~ spl5_43
| ~ spl5_93
| ~ spl5_174
| spl5_176 ),
inference(sat_conversion,[],[f5203]) ).
cnf(s3845,plain,
( ~ spl5_22
| spl5_290
| spl5_292 ),
inference(sat_conversion,[],[f7315]) ).
cnf(s3852,plain,
( spl5_13
| ~ spl5_292
| ~ spl5_294 ),
inference(sat_conversion,[],[f7332]) ).
cnf(s3855,plain,
( ~ spl5_38
| spl5_294
| spl5_295 ),
inference(sat_conversion,[],[f7338]) ).
cnf(s3890,plain,
( ~ spl5_14
| ~ spl5_295
| spl5_297
| ~ spl5_298 ),
inference(sat_conversion,[],[f7404]) ).
cnf(s3895,plain,
( ~ spl5_11
| spl5_298
| ~ spl5_299 ),
inference(sat_conversion,[],[f7416]) ).
cnf(s3900,plain,
( ~ spl5_295
| spl5_300 ),
inference(sat_conversion,[],[f7429]) ).
cnf(s3902,plain,
( spl5_299
| spl5_301 ),
inference(sat_conversion,[],[f7436]) ).
cnf(s3915,plain,
( ~ spl5_16
| ~ spl5_295
| ~ spl5_298
| spl5_302 ),
inference(sat_conversion,[],[f7458]) ).
cnf(s3929,plain,
( ~ spl5_17
| ~ spl5_302
| spl5_303 ),
inference(sat_conversion,[],[f7491]) ).
cnf(s3931,plain,
( ~ spl5_300
| spl5_301
| spl5_304 ),
inference(sat_conversion,[],[f7496]) ).
cnf(s3937,plain,
( ~ spl5_304
| spl5_305 ),
inference(sat_conversion,[],[f7516]) ).
cnf(s3944,plain,
( ~ spl5_297
| ~ spl5_305
| spl5_307 ),
inference(sat_conversion,[],[f7537]) ).
cnf(s3947,plain,
( ~ spl5_19
| spl5_294
| ~ spl5_307
| ~ spl5_308 ),
inference(sat_conversion,[],[f7545]) ).
cnf(s3973,plain,
( ~ spl5_57
| ~ spl5_295
| ~ spl5_299
| spl5_314 ),
inference(sat_conversion,[],[f7606]) ).
cnf(s3974,plain,
( ~ spl5_303
| ~ spl5_305
| spl5_308
| ~ spl5_314 ),
inference(sat_conversion,[],[f7607]) ).
cnf(s4048,plain,
( ~ spl5_9
| ~ spl5_301
| ~ spl5_315 ),
inference(sat_conversion,[],[f7680]) ).
cnf(s4353,plain,
( ~ spl5_287
| spl5_355 ),
inference(sat_conversion,[],[f8440]) ).
cnf(s4368,plain,
( ~ spl5_176
| ~ spl5_355
| spl5_356 ),
inference(sat_conversion,[],[f8464]) ).
cnf(s4377,plain,
( ~ spl5_15
| ~ spl5_356
| spl5_357 ),
inference(sat_conversion,[],[f8483]) ).
cnf(s4392,plain,
( ~ spl5_23
| ~ spl5_357
| spl5_359 ),
inference(sat_conversion,[],[f8515]) ).
cnf(s4401,plain,
( ~ spl5_359
| spl5_360 ),
inference(sat_conversion,[],[f8539]) ).
cnf(s4415,plain,
( ~ spl5_290
| ~ spl5_360
| ~ spl5_361
| spl5_362 ),
inference(sat_conversion,[],[f8569]) ).
cnf(s4436,plain,
( ~ spl5_4
| ~ spl5_18
| ~ spl5_24
| spl5_292
| ~ spl5_362 ),
inference(sat_conversion,[],[f8635]) ).
cnf(s4440,plain,
( ~ spl5_290
| spl5_361 ),
inference(sat_conversion,[],[f8641]) ).
cnf(s4462,plain,
( ~ spl5_29
| spl5_287
| spl5_292
| spl5_345 ),
inference(sat_conversion,[],[f8655]) ).
cnf(s4519,plain,
( spl5_292
| ~ spl5_345 ),
inference(sat_conversion,[],[f8749]) ).
cnf(s4781,plain,
( ~ spl5_42
| spl5_99
| ~ spl5_126
| spl5_174 ),
inference(sat_conversion,[],[f9108]) ).
cnf(s4853,plain,
( spl5_13
| ~ spl5_292
| spl5_315 ),
inference(sat_conversion,[],[f9192]) ).
cnf(s4971,plain,
~ spl5_143,
inference(rat,[],[s1591,s136]) ).
cnf(s4974,plain,
spl5_15,
inference(rat,[],[s146,s127]) ).
cnf(s4975,plain,
spl5_12,
inference(rat,[],[s134,s127]) ).
cnf(s4976,plain,
spl5_11,
inference(rat,[],[s132,s127]) ).
cnf(s4977,plain,
spl5_57,
inference(rat,[],[s511,s4975]) ).
cnf(s4978,plain,
spl5_37,
inference(rat,[],[s341,s122]) ).
cnf(s4979,plain,
spl5_20,
inference(rat,[],[s197,s122]) ).
cnf(s4980,plain,
spl5_38,
inference(rat,[],[s348,s4978]) ).
cnf(s4981,plain,
spl5_29,
inference(rat,[],[s244,s4979]) ).
cnf(s4986,plain,
spl5_8,
inference(rat,[],[s119,s108]) ).
cnf(s4999,plain,
spl5_28,
inference(rat,[],[s235,s108,s106]) ).
cnf(s5000,plain,
spl5_27,
inference(rat,[],[s233,s106]) ).
cnf(s5001,plain,
spl5_18,
inference(rat,[],[s157,s4986,s106]) ).
cnf(s5002,plain,
spl5_17,
inference(rat,[],[s155,s106]) ).
cnf(s5005,plain,
spl5_36,
inference(rat,[],[s339,s5000]) ).
cnf(s5012,plain,
spl5_23,
inference(rat,[],[s211,s102]) ).
cnf(s5013,plain,
spl5_16,
inference(rat,[],[s151,s102]) ).
cnf(s5014,plain,
spl5_14,
inference(rat,[],[s141,s102]) ).
cnf(s5023,plain,
spl5_24,
inference(rat,[],[s219,s100]) ).
cnf(s5024,plain,
spl5_22,
inference(rat,[],[s204,s100]) ).
cnf(s5025,plain,
spl5_7,
inference(rat,[],[s115,s100]) ).
cnf(s5032,plain,
spl5_19,
inference(rat,[],[s173,s5025]) ).
cnf(s5038,plain,
( ~ spl5_100
| spl5_142 ),
inference(rat,[],[s891,s1505]) ).
cnf(s5039,plain,
~ spl5_99,
inference(rat,[],[s5038,s1508,s880,s2673,s4971]) ).
cnf(s5042,plain,
~ spl5_49,
inference(rat,[],[s838,s5001,s5039]) ).
cnf(s5043,plain,
spl5_48,
inference(rat,[],[s457,s5002,s5042]) ).
cnf(s5044,plain,
spl5_98,
inference(rat,[],[s810,s5042,s5043]) ).
cnf(s5045,plain,
spl5_160,
inference(rat,[],[s2595,s5044]) ).
cnf(s5047,plain,
spl5_121,
inference(rat,[],[s1186,s5044]) ).
cnf(s5049,plain,
~ spl5_71,
inference(rat,[],[s2600,s5039,s5001,s5045]) ).
cnf(s5050,plain,
spl5_126,
inference(rat,[],[s1347,s5002,s5047]) ).
cnf(s5069,plain,
spl5_30,
inference(rat,[],[s2567,s2566,s2541,s2563,s2481,s2501,s2551,s1034,s2496,s247,s2534,s5049,s5002,s5013,s4977,s122,s5005,s4976,s4999]) ).
cnf(s5070,plain,
spl5_34,
inference(rat,[],[s264,s5069]) ).
cnf(s5071,plain,
spl5_33,
inference(rat,[],[s258,s5069]) ).
cnf(s5072,plain,
spl5_32,
inference(rat,[],[s255,s5069]) ).
cnf(s5074,plain,
spl5_93,
inference(rat,[],[s769,s5070]) ).
cnf(s5075,plain,
spl5_43,
inference(rat,[],[s394,s5070]) ).
cnf(s5077,plain,
spl5_42,
inference(rat,[],[s385,s5071]) ).
cnf(s5088,plain,
spl5_174,
inference(rat,[],[s4781,s5050,s5039,s5077]) ).
cnf(s5099,plain,
spl5_176,
inference(rat,[],[s2988,s5075,s5072,s5074,s5088]) ).
cnf(s5136,plain,
~ spl5_292,
inference(rat,[],[s3947,s3974,s3944,s3929,s3937,s3890,s3915,s3931,s3973,s3895,s3900,s3902,s3855,s4048,s3852,s4853,s5032,s5002,s5014,s5013,s4977,s4976,s4980,s122,s136]) ).
cnf(s5137,plain,
~ spl5_345,
inference(rat,[],[s4519,s5136]) ).
cnf(s5138,plain,
spl5_287,
inference(rat,[],[s4462,s5137,s4981,s5136]) ).
cnf(s5139,plain,
~ spl5_362,
inference(rat,[],[s4436,s5023,s5001,s108,s5136]) ).
cnf(s5140,plain,
spl5_290,
inference(rat,[],[s3845,s5024,s5136]) ).
cnf(s5141,plain,
spl5_355,
inference(rat,[],[s4353,s5138]) ).
cnf(s5143,plain,
spl5_361,
inference(rat,[],[s4440,s5140]) ).
cnf(s5144,plain,
spl5_356,
inference(rat,[],[s4368,s5099,s5141]) ).
cnf(s5147,plain,
~ spl5_360,
inference(rat,[],[s4415,s5140,s5139,s5143]) ).
cnf(s5148,plain,
spl5_357,
inference(rat,[],[s4377,s4974,s5144]) ).
cnf(s5152,plain,
~ spl5_359,
inference(rat,[],[s4401,s5147]) ).
cnf(s5153,plain,
$false,
inference(rat,[],[s4392,s5012,s5152,s5148]) ).
fof(f9287,plain,
$false,
inference(avatar_sat_refutation,[],[s5153]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET251-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 28 01:12:37 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.82/2.43 % (4057761)Input is clausal, will run a generic CNF schedule.
% 10.82/2.43 % (4057772)dis-21_1_sil=8000:lcm=predicate:random_seed=3593292741:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.82/2.43 % (4057772)Instruction limit reached!
% 10.82/2.43 % (4057772)------------------------------
% 10.82/2.43 % (4057772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.43 % (4057772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.43 % (4057772)CaDiCaL version: 2.1.3
% 10.82/2.43 % (4057772)Termination reason: Instruction limit
% 10.82/2.43 % (4057772)Termination phase: Saturation
% 10.82/2.43 % (4057772)Time elapsed: 0.039 s
% 10.82/2.43 % (4057772)Peak memory usage: 90 MB
% 10.82/2.43 % (4057772)Instructions burned: 117 (million)
% 10.82/2.43 % (4057770)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3774094373:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.82/2.43 % (4057767)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=109607800:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.82/2.43 % (4057769)lrs+10_1_sil=8000:sp=occurrence:random_seed=1960721296:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.82/2.43 % (4057768)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2874467876:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.82/2.43 % (4057766)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=2845243749:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.82/2.43 % (4057771)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1361756034:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.82/2.43 % (4057769)Instruction limit reached!
% 10.82/2.43 % (4057769)------------------------------
% 10.82/2.43 % (4057769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.43 % (4057769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.43 % (4057769)CaDiCaL version: 2.1.3
% 10.82/2.43 % (4057769)Termination reason: Instruction limit
% 10.82/2.43 % (4057769)Termination phase: Saturation
% 10.82/2.43 % (4057769)Time elapsed: 0.064 s
% 10.82/2.43 % (4057769)Peak memory usage: 90 MB
% 10.82/2.43 % (4057769)Instructions burned: 108 (million)
% 10.82/2.43 % (4057770)Instruction limit reached!
% 10.82/2.43 % (4057770)------------------------------
% 10.82/2.43 % (4057770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.43 % (4057770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.43 % (4057770)CaDiCaL version: 2.1.3
% 10.82/2.43 % (4057770)Termination reason: Instruction limit
% 10.82/2.43 % (4057770)Termination phase: Saturation
% 10.82/2.43 % (4057770)Time elapsed: 0.068 s
% 10.82/2.43 % (4057770)Peak memory usage: 89 MB
% 10.82/2.43 % (4057770)Instructions burned: 116 (million)
% 10.82/2.43 % (4057774)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=1343711875:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.82/2.43 % (4057774)Refutation not found, incomplete strategy
% 10.82/2.43 % (4057774)------------------------------
% 10.82/2.43 % (4057774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.43 % (4057774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.43 % (4057774)CaDiCaL version: 2.1.3
% 10.82/2.43 % (4057774)Termination reason: Refutation not found, incomplete strategy
% 10.82/2.43 % (4057774)Time elapsed: 0.002 s
% 10.82/2.43 % (4057774)Peak memory usage: 88 MB
% 10.82/2.43 % (4057774)Instructions burned: 4 (million)
% 10.82/2.43 % (4057771)Instruction limit reached!
% 10.82/2.43 % (4057771)------------------------------
% 10.82/2.43 % (4057771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.82/2.43 % (4057771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.82/2.43 % (4057771)CaDiCaL version: 2.1.3
% 10.82/2.43 % (4057771)Termination reason: Instruction limit
% 10.82/2.43 % (4057771)Termination phase: Saturation
% 10.82/2.43 % (4057771)Time elapsed: 0.133 s
% 10.82/2.43 % (4057771)Peak memory usage: 90 MB
% 10.82/2.43 % (4057771)Instructions burned: 180 (million)
% 10.82/2.43 % (4057782)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=942083438:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.06/3.53 % (4057781)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2230847659: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)
% 19.06/3.53 % (4057782)Refutation not found, incomplete strategy
% 19.06/3.53 % (4057782)------------------------------
% 19.06/3.53 % (4057782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.06/3.53 % (4057782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.06/3.53 % (4057782)CaDiCaL version: 2.1.3
% 19.06/3.53 % (4057782)Termination reason: Refutation not found, incomplete strategy
% 19.06/3.53 % (4057782)Time elapsed: 0.003 s
% 19.06/3.53 % (4057782)Peak memory usage: 88 MB
% 19.06/3.53 % (4057782)Instructions burned: 3 (million)
% 19.06/3.53 % (4057774)------------------------------
% 19.06/3.53 % (4057774)------------------------------
% 19.06/3.53 % (4057784)lrs+10_64_to=lpo:sil=8000:random_seed=3408082998:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 19.06/3.53 % (4057781)Instruction limit reached!
% 19.06/3.53 % (4057781)------------------------------
% 19.06/3.53 % (4057781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.06/3.53 % (4057781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.06/3.53 % (4057781)CaDiCaL version: 2.1.3
% 19.06/3.53 % (4057781)Termination reason: Instruction limit
% 19.06/3.53 % (4057781)Termination phase: Saturation
% 19.06/3.53 % (4057781)Time elapsed: 0.106 s
% 19.06/3.53 % (4057781)Peak memory usage: 91 MB
% 19.06/3.53 % (4057781)Instructions burned: 190 (million)
% 19.06/3.53 % (4057784)Instruction limit reached!
% 19.06/3.53 % (4057784)------------------------------
% 19.06/3.53 % (4057784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.06/3.53 % (4057784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.06/3.53 % (4057784)CaDiCaL version: 2.1.3
% 19.06/3.53 % (4057784)Termination reason: Instruction limit
% 19.06/3.53 % (4057784)Termination phase: Saturation
% 19.06/3.53 % (4057784)Time elapsed: 0.081 s
% 19.06/3.53 % (4057784)Peak memory usage: 90 MB
% 19.06/3.53 % (4057784)Instructions burned: 127 (million)
% 19.06/3.53 % (4057787)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=752392550:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.06/3.53 % (4057787)Instruction limit reached!
% 19.06/3.53 % (4057787)------------------------------
% 19.06/3.53 % (4057787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.06/3.53 % (4057787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.06/3.53 % (4057787)CaDiCaL version: 2.1.3
% 19.06/3.53 % (4057787)Termination reason: Instruction limit
% 19.06/3.53 % (4057787)Termination phase: Saturation
% 19.06/3.53 % (4057787)Time elapsed: 0.065 s
% 19.06/3.53 % (4057787)Peak memory usage: 89 MB
% 19.06/3.53 % (4057787)Instructions burned: 197 (million)
% 19.06/3.53 % (4057782)------------------------------
% 19.06/3.53 % (4057782)------------------------------
% 19.06/3.53 % (4057789)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3075032426:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 19.06/3.53 % (4057790)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4172425989:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 19.06/3.53 % (4057792)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=3212914722:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.06/3.53 % (4057789)Instruction limit reached!
% 19.06/3.53 % (4057789)------------------------------
% 19.06/3.53 % (4057789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.06/3.53 % (4057789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.06/3.53 % (4057789)CaDiCaL version: 2.1.3
% 19.06/3.53 % (4057789)Termination reason: Instruction limit
% 19.06/3.53 % (4057789)Termination phase: Saturation
% 19.06/3.53 % (4057789)Time elapsed: 0.109 s
% 19.06/3.53 % (4057789)Peak memory usage: 91 MB
% 19.06/3.53 % (4057789)Instructions burned: 158 (million)
% 19.06/3.53 % (4057792)Instruction limit reached!
% 19.06/3.53 % (4057792)------------------------------
% 19.06/3.53 % (4057792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057792)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057792)Termination reason: Instruction limit
% 28.72/4.95 % (4057792)Termination phase: Saturation
% 28.72/4.95 % (4057792)Time elapsed: 0.033 s
% 28.72/4.95 % (4057792)Peak memory usage: 90 MB
% 28.72/4.95 % (4057792)Instructions burned: 108 (million)
% 28.72/4.95 % (4057793)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1915219102:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 28.72/4.95 % (4057793)Instruction limit reached!
% 28.72/4.95 % (4057793)------------------------------
% 28.72/4.95 % (4057793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057793)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057793)Termination reason: Instruction limit
% 28.72/4.95 % (4057793)Termination phase: Saturation
% 28.72/4.95 % (4057793)Time elapsed: 0.071 s
% 28.72/4.95 % (4057793)Peak memory usage: 89 MB
% 28.72/4.95 % (4057793)Instructions burned: 108 (million)
% 28.72/4.95 % (4057798)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4255020330:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 28.72/4.95 % (4057797)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4183237423:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 28.72/4.95 % (4057801)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3292292771:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 28.72/4.95 % (4057797)Instruction limit reached!
% 28.72/4.95 % (4057797)------------------------------
% 28.72/4.95 % (4057797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057797)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057797)Termination reason: Instruction limit
% 28.72/4.95 % (4057797)Termination phase: Saturation
% 28.72/4.95 % (4057797)Time elapsed: 0.169 s
% 28.72/4.95 % (4057797)Peak memory usage: 90 MB
% 28.72/4.95 % (4057797)Instructions burned: 242 (million)
% 28.72/4.95 % (4057801)Instruction limit reached!
% 28.72/4.95 % (4057801)------------------------------
% 28.72/4.95 % (4057801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057801)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057801)Termination reason: Instruction limit
% 28.72/4.95 % (4057801)Termination phase: Saturation
% 28.72/4.95 % (4057801)Time elapsed: 0.095 s
% 28.72/4.95 % (4057801)Peak memory usage: 90 MB
% 28.72/4.95 % (4057801)Instructions burned: 135 (million)
% 28.72/4.95 % (4057804)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2172388828:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 28.72/4.95 % (4057805)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4236930071:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 28.72/4.95 % (4057805)Instruction limit reached!
% 28.72/4.95 % (4057805)------------------------------
% 28.72/4.95 % (4057805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057805)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057805)Termination reason: Instruction limit
% 28.72/4.95 % (4057805)Termination phase: Saturation
% 28.72/4.95 % (4057805)Time elapsed: 0.112 s
% 28.72/4.95 % (4057805)Peak memory usage: 89 MB
% 28.72/4.95 % (4057805)Instructions burned: 192 (million)
% 28.72/4.95 % (4057804)Instruction limit reached!
% 28.72/4.95 % (4057804)------------------------------
% 28.72/4.95 % (4057804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.72/4.95 % (4057804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.72/4.95 % (4057804)CaDiCaL version: 2.1.3
% 28.72/4.95 % (4057804)Termination reason: Instruction limit
% 28.72/4.95 % (4057804)Termination phase: Saturation
% 28.72/4.95 % (4057804)Time elapsed: 0.295 s
% 28.72/4.95 % (4057804)Peak memory usage: 96 MB
% 28.72/4.95 % (4057804)Instructions burned: 500 (million)
% 28.72/4.95 % (4057808)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1147236443:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 44.85/7.15 % (4057809)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1798215973:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 44.85/7.15 % (4057808)Instruction limit reached!
% 44.85/7.15 % (4057808)------------------------------
% 44.85/7.15 % (4057808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057808)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057808)Termination reason: Instruction limit
% 44.85/7.15 % (4057808)Termination phase: Saturation
% 44.85/7.15 % (4057808)Time elapsed: 0.166 s
% 44.85/7.15 % (4057808)Peak memory usage: 92 MB
% 44.85/7.15 % (4057808)Instructions burned: 266 (million)
% 44.85/7.15 % (4057809)Instruction limit reached!
% 44.85/7.15 % (4057809)------------------------------
% 44.85/7.15 % (4057809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057809)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057809)Termination reason: Instruction limit
% 44.85/7.15 % (4057809)Termination phase: Saturation
% 44.85/7.15 % (4057809)Time elapsed: 0.105 s
% 44.85/7.15 % (4057809)Peak memory usage: 90 MB
% 44.85/7.15 % (4057809)Instructions burned: 156 (million)
% 44.85/7.15 % (4057812)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=1672640717:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 44.85/7.15 % (4057813)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2928201039:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 44.85/7.15 % (4057813)Instruction limit reached!
% 44.85/7.15 % (4057813)------------------------------
% 44.85/7.15 % (4057813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057813)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057813)Termination reason: Instruction limit
% 44.85/7.15 % (4057813)Termination phase: Saturation
% 44.85/7.15 % (4057813)Time elapsed: 0.276 s
% 44.85/7.15 % (4057813)Peak memory usage: 89 MB
% 44.85/7.15 % (4057813)Instructions burned: 538 (million)
% 44.85/7.15 % (4057816)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1292059649:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 44.85/7.15 % (4057816)Instruction limit reached!
% 44.85/7.15 % (4057816)------------------------------
% 44.85/7.15 % (4057816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057816)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057816)Termination reason: Instruction limit
% 44.85/7.15 % (4057816)Termination phase: Saturation
% 44.85/7.15 % (4057816)Time elapsed: 0.093 s
% 44.85/7.15 % (4057816)Peak memory usage: 90 MB
% 44.85/7.15 % (4057816)Instructions burned: 180 (million)
% 44.85/7.15 % (4057798)Instruction limit reached!
% 44.85/7.15 % (4057798)------------------------------
% 44.85/7.15 % (4057798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057798)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057798)Termination reason: Instruction limit
% 44.85/7.15 % (4057798)Termination phase: Saturation
% 44.85/7.15 % (4057798)Time elapsed: 1.783 s
% 44.85/7.15 % (4057798)Peak memory usage: 160 MB
% 44.85/7.15 % (4057798)Instructions burned: 5209 (million)
% 44.85/7.15 % (4057790)Instruction limit reached!
% 44.85/7.15 % (4057790)------------------------------
% 44.85/7.15 % (4057790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.85/7.15 % (4057790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.85/7.15 % (4057790)CaDiCaL version: 2.1.3
% 44.85/7.15 % (4057790)Termination reason: Instruction limit
% 44.85/7.15 % (4057790)Termination phase: Saturation
% 44.85/7.15 % (4057790)Time elapsed: 1.993 s
% 44.85/7.15 % (4057790)Peak memory usage: 142 MB
% 44.85/7.15 % (4057790)Instructions burned: 3394 (million)
% 44.85/7.15 % (4057818)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=3625226816:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 67.27/10.34 % (4057819)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=1786234193:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 67.27/10.34 % (4057821)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=3025621749:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 67.27/10.34 % (4057819)Instruction limit reached!
% 67.27/10.34 % (4057819)------------------------------
% 67.27/10.34 % (4057819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.27/10.34 % (4057819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.27/10.34 % (4057819)CaDiCaL version: 2.1.3
% 67.27/10.34 % (4057819)Termination reason: Instruction limit
% 67.27/10.34 % (4057819)Termination phase: Saturation
% 67.27/10.34 % (4057819)Time elapsed: 0.098 s
% 67.27/10.34 % (4057819)Peak memory usage: 90 MB
% 67.27/10.34 % (4057819)Instructions burned: 415 (million)
% 67.27/10.34 % (4057824)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=1694455755:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 67.27/10.34 % (4057824)Instruction limit reached!
% 67.27/10.34 % (4057824)------------------------------
% 67.27/10.34 % (4057824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.27/10.34 % (4057824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.27/10.34 % (4057824)CaDiCaL version: 2.1.3
% 67.27/10.34 % (4057824)Termination reason: Instruction limit
% 67.27/10.34 % (4057824)Termination phase: Saturation
% 67.27/10.34 % (4057824)Time elapsed: 0.081 s
% 67.27/10.34 % (4057824)Peak memory usage: 93 MB
% 67.27/10.34 % (4057824)Instructions burned: 305 (million)
% 67.27/10.34 % (4057826)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3943929379:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 67.27/10.34 % (4057826)Instruction limit reached!
% 67.27/10.34 % (4057826)------------------------------
% 67.27/10.34 % (4057826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.27/10.34 % (4057826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.27/10.34 % (4057826)CaDiCaL version: 2.1.3
% 67.27/10.34 % (4057826)Termination reason: Instruction limit
% 67.27/10.34 % (4057826)Termination phase: Saturation
% 67.27/10.34 % (4057826)Time elapsed: 0.206 s
% 67.27/10.34 % (4057826)Peak memory usage: 98 MB
% 67.27/10.34 % (4057826)Instructions burned: 721 (million)
% 67.27/10.34 % (4057828)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3121051094:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi)
% 67.27/10.34 % (4057812)Instruction limit reached!
% 67.27/10.34 % (4057812)------------------------------
% 67.27/10.34 % (4057812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.27/10.34 % (4057812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.27/10.34 % (4057812)CaDiCaL version: 2.1.3
% 67.27/10.34 % (4057812)Termination reason: Instruction limit
% 67.27/10.34 % (4057812)Termination phase: Saturation
% 67.27/10.34 % (4057812)Time elapsed: 1.852 s
% 67.27/10.34 % (4057812)Peak memory usage: 152 MB
% 67.27/10.34 % (4057812)Instructions burned: 3256 (million)
% 67.27/10.34 % (4057830)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1879858637:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi)
% 67.27/10.34 % (4057828)Instruction limit reached!
% 67.27/10.34 % (4057828)------------------------------
% 67.27/10.34 % (4057828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.27/10.34 % (4057828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.27/10.34 % (4057828)CaDiCaL version: 2.1.3
% 67.27/10.34 % (4057828)Termination reason: Instruction limit
% 67.27/10.34 % (4057828)Termination phase: Saturation
% 67.27/10.34 % (4057828)Time elapsed: 0.333 s
% 67.27/10.34 % (4057828)Peak memory usage: 92 MB
% 67.27/10.34 % (4057828)Instructions burned: 598 (million)
% 67.27/10.34 % (4057832)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=3113751127:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 82.50/12.85 % (4057821)Instruction limit reached!
% 82.50/12.85 % (4057821)------------------------------
% 82.50/12.85 % (4057821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057821)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057821)Termination reason: Instruction limit
% 82.50/12.85 % (4057821)Termination phase: Saturation
% 82.50/12.85 % (4057821)Time elapsed: 2.536 s
% 82.50/12.85 % (4057821)Peak memory usage: 178 MB
% 82.50/12.85 % (4057821)Instructions burned: 8482 (million)
% 82.50/12.85 % (4057832)Instruction limit reached!
% 82.50/12.85 % (4057832)------------------------------
% 82.50/12.85 % (4057832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057832)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057832)Termination reason: Instruction limit
% 82.50/12.85 % (4057832)Termination phase: Saturation
% 82.50/12.85 % (4057832)Time elapsed: 1.286 s
% 82.50/12.85 % (4057832)Peak memory usage: 137 MB
% 82.50/12.85 % (4057832)Instructions burned: 1998 (million)
% 82.50/12.85 % (4057834)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=1171895341:i=2088:bd=preordered:av=off_2946 on theBenchmark for (2946ds/2088Mi)
% 82.50/12.85 % (4057835)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1991747371:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi)
% 82.50/12.85 % (4057830)Instruction limit reached!
% 82.50/12.85 % (4057830)------------------------------
% 82.50/12.85 % (4057830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057830)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057830)Termination reason: Instruction limit
% 82.50/12.85 % (4057830)Termination phase: Saturation
% 82.50/12.85 % (4057830)Time elapsed: 1.766 s
% 82.50/12.85 % (4057830)Peak memory usage: 141 MB
% 82.50/12.85 % (4057830)Instructions burned: 2989 (million)
% 82.50/12.85 % (4057838)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2509537632:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi)
% 82.50/12.85 % (4057838)Refutation not found, incomplete strategy
% 82.50/12.85 % (4057838)------------------------------
% 82.50/12.85 % (4057838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057838)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057838)Termination reason: Refutation not found, incomplete strategy
% 82.50/12.85 % (4057838)Time elapsed: 0.011 s
% 82.50/12.85 % (4057838)Peak memory usage: 89 MB
% 82.50/12.85 % (4057838)Instructions burned: 17 (million)
% 82.50/12.85 % (4057838)------------------------------
% 82.50/12.85 % (4057838)------------------------------
% 82.50/12.85 % (4057835)Instruction limit reached!
% 82.50/12.85 % (4057835)------------------------------
% 82.50/12.85 % (4057835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057835)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057835)Termination reason: Instruction limit
% 82.50/12.85 % (4057835)Termination phase: Saturation
% 82.50/12.85 % (4057835)Time elapsed: 0.644 s
% 82.50/12.85 % (4057835)Peak memory usage: 103 MB
% 82.50/12.85 % (4057835)Instructions burned: 1098 (million)
% 82.50/12.85 % (4057834)Instruction limit reached!
% 82.50/12.85 % (4057834)------------------------------
% 82.50/12.85 % (4057834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057834)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057834)Termination reason: Instruction limit
% 82.50/12.85 % (4057834)Termination phase: Saturation
% 82.50/12.85 % (4057834)Time elapsed: 0.733 s
% 82.50/12.85 % (4057834)Peak memory usage: 137 MB
% 82.50/12.85 % (4057834)Instructions burned: 2089 (million)
% 82.50/12.85 % (4057840)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1065579877:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2938 on theBenchmark for (2938ds/2942Mi)
% 82.50/12.85 % (4057841)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=837929376:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2937 on theBenchmark for (2937ds/6922Mi)
% 82.50/12.85 % (4057842)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=180833092:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2937 on theBenchmark for (2937ds/596Mi)
% 82.50/12.85 % (4057842)Instruction limit reached!
% 82.50/12.85 % (4057842)------------------------------
% 82.50/12.85 % (4057842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057842)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057842)Termination reason: Instruction limit
% 82.50/12.85 % (4057842)Termination phase: Saturation
% 82.50/12.85 % (4057842)Time elapsed: 0.169 s
% 82.50/12.85 % (4057842)Peak memory usage: 100 MB
% 82.50/12.85 % (4057842)Instructions burned: 600 (million)
% 82.50/12.85 % (4057846)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=3730200918:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2934 on theBenchmark for (2934ds/4123Mi)
% 82.50/12.85 % (4057846)Instruction limit reached!
% 82.50/12.85 % (4057846)------------------------------
% 82.50/12.85 % (4057846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057846)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057846)Termination reason: Instruction limit
% 82.50/12.85 % (4057846)Termination phase: Saturation
% 82.50/12.85 % (4057846)Time elapsed: 1.207 s
% 82.50/12.85 % (4057846)Peak memory usage: 170 MB
% 82.50/12.85 % (4057846)Instructions burned: 4124 (million)
% 82.50/12.85 % (4057848)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=304162865:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi)
% 82.50/12.85 % (4057840)Instruction limit reached!
% 82.50/12.85 % (4057840)------------------------------
% 82.50/12.85 % (4057840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057840)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057840)Termination reason: Instruction limit
% 82.50/12.85 % (4057840)Termination phase: Saturation
% 82.50/12.85 % (4057840)Time elapsed: 1.826 s
% 82.50/12.85 % (4057840)Peak memory usage: 140 MB
% 82.50/12.85 % (4057840)Instructions burned: 2943 (million)
% 82.50/12.85 % (4057850)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3209874727:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2918 on theBenchmark for (2918ds/1670Mi)
% 82.50/12.85 % (4057818)Instruction limit reached!
% 82.50/12.85 % (4057818)------------------------------
% 82.50/12.85 % (4057818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057818)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057818)Termination reason: Instruction limit
% 82.50/12.85 % (4057818)Termination phase: Saturation
% 82.50/12.85 % (4057818)Time elapsed: 6.346 s
% 82.50/12.85 % (4057818)Peak memory usage: 178 MB
% 82.50/12.85 % (4057818)Instructions burned: 10308 (million)
% 82.50/12.85 % (4057852)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=1961666371:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2909 on theBenchmark for (2909ds/1722Mi)
% 82.50/12.85 % (4057850)Instruction limit reached!
% 82.50/12.85 % (4057850)------------------------------
% 82.50/12.85 % (4057850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057850)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057850)Termination reason: Instruction limit
% 82.50/12.85 % (4057850)Termination phase: Saturation
% 82.50/12.85 % (4057850)Time elapsed: 1.034 s
% 82.50/12.85 % (4057850)Peak memory usage: 137 MB
% 82.50/12.85 % (4057850)Instructions burned: 1672 (million)
% 82.50/12.85 % (4057854)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=2087965331:cts=off:cond=on:i=9530:bs=on:fsd=on_2906 on theBenchmark for (2906ds/9530Mi)
% 82.50/12.85 % (4057841)Instruction limit reached!
% 82.50/12.85 % (4057841)------------------------------
% 82.50/12.85 % (4057841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057841)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057841)Termination reason: Instruction limit
% 82.50/12.85 % (4057841)Termination phase: Saturation
% 82.50/12.85 % (4057841)Time elapsed: 3.743 s
% 82.50/12.85 % (4057841)Peak memory usage: 178 MB
% 82.50/12.85 % (4057841)Instructions burned: 6923 (million)
% 82.50/12.85 % (4057856)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=508593752:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi)
% 82.50/12.85 % (4057852)Instruction limit reached!
% 82.50/12.85 % (4057852)------------------------------
% 82.50/12.85 % (4057852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.50/12.85 % (4057852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.50/12.85 % (4057852)CaDiCaL version: 2.1.3
% 82.50/12.85 % (4057852)Termination reason: Instruction limit
% 82.50/12.85 % (4057852)Termination phase: Saturation
% 82.50/12.85 % (4057852)Time elapsed: 1.207 s
% 82.50/12.85 % (4057852)Peak memory usage: 135 MB
% 82.50/12.85 % (4057852)Instructions burned: 1722 (million)
% 82.50/12.85 % (4057858)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=4260246355:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 82.50/12.85 % (4057854)First to succeed.
% 82.50/12.85 % (4057854)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4057761"
% 82.50/12.85 % (4057854)Refutation found. Thanks to Tanya!
% 82.50/12.85 % SZS status Unsatisfiable for theBenchmark
% 82.50/12.85 % SZS output start Proof for theBenchmark
% See solution above
% 85.45/13.02 % (4057854)------------------------------
% 85.45/13.02 % (4057854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.45/13.02 % (4057854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.45/13.02 % (4057854)CaDiCaL version: 2.1.3
% 85.45/13.02 % (4057854)Termination reason: Refutation
% 85.45/13.02 % (4057854)Time elapsed: 2.212 s
% 85.45/13.02 % (4057854)Peak memory usage: 143 MB
% 85.45/13.02 % (4057854)Instructions burned: 3146 (million)
% 85.45/13.02 % (4057854)------------------------------
% 85.45/13.02 % (4057854)------------------------------
% 85.45/13.02 % (4057761)Success in time 12.007 s
% 85.45/13.02 % Vampire exiting
%------------------------------------------------------------------------------