%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM062-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:11:41 PM UTC 2026
% Result : Unsatisfiable 57.68s 13.02s
% Output : Refutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 107
% Syntax : Number of formulae : 531 ( 90 unt; 77 def)
% Number of atoms : 1387 ( 147 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 1609 ( 753 ~; 784 |; 0 &)
% ( 72 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 76 ( 74 usr; 73 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-3 aty)
% Number of variables : 308 ( 0 sgn 308 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f10,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f19,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),element_relation)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation2) ).
fof(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/sandbox/benchmark/theBenchmark.p',element_relation3) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f133,axiom,
! [X2,X0,X1] : segment(X0,X1,X2) = domain_of(restrict(X0,X1,singleton(X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment) ).
fof(f176,negated_conjecture,
member(z,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_segments_property6_1) ).
fof(f177,negated_conjecture,
segment(element_relation,y,z) != intersection(y,z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_segments_property6_2) ).
fof(f178,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f192,plain,
! [X2,X0,X1] : segment(X0,X1,X2) = domain_of(intersection(X0,cross_product(X1,unordered_pair(X2,X2)))),
inference(definition_unfolding,[],[f133,f28,f12]) ).
fof(f195,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f178]) ).
fof(f196,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f178]) ).
fof(f197,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f178]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f178]) ).
fof(f199,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| member(X0,X1) ),
inference(definition_unfolding,[],[f19,f178]) ).
fof(f200,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,f178,f178]) ).
fof(f202,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f203,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f268,plain,
intersection(y,z) != domain_of(intersection(element_relation,cross_product(y,unordered_pair(z,z)))),
inference(definition_unfolding,[],[f177,f192]) ).
fof(f270,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f275,definition,
sF0 = intersection(y,z),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f276,plain,
intersection(y,z) = sF0,
inference(reorient_equations,[],[f275]) ).
fof(f277,definition,
sF1 = unordered_pair(z,z),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f278,plain,
unordered_pair(z,z) = sF1,
inference(reorient_equations,[],[f277]) ).
fof(f279,definition,
sF2 = cross_product(y,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f280,plain,
cross_product(y,sF1) = sF2,
inference(reorient_equations,[],[f279]) ).
fof(f281,definition,
sF3 = intersection(element_relation,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f282,plain,
intersection(element_relation,sF2) = sF3,
inference(reorient_equations,[],[f281]) ).
fof(f283,definition,
sF4 = domain_of(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f284,plain,
domain_of(sF3) = sF4,
inference(reorient_equations,[],[f283]) ).
fof(f285,plain,
sF0 != sF4,
inference(definition_folding,[],[f268,f284,f282,f280,f278,f276]) ).
fof(f287,definition,
( spl5_1
<=> intersection(y,z) = sF0 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f289,plain,
( intersection(y,z) = sF0
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,plain,
spl5_1,
inference(avatar_split_clause,[],[f276,f287]) ).
fof(f292,definition,
( spl5_2
<=> cross_product(y,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f294,plain,
( cross_product(y,sF1) = sF2
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
spl5_2,
inference(avatar_split_clause,[],[f280,f292]) ).
fof(f299,definition,
( spl5_3
<=> unordered_pair(z,z) = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
fof(f301,plain,
( unordered_pair(z,z) = sF1
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f302,plain,
spl5_3,
inference(avatar_split_clause,[],[f278,f299]) ).
fof(f312,definition,
( spl5_6
<=> member(z,universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).
fof(f314,plain,
( member(z,universal_class)
| ~ spl5_6 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,plain,
spl5_6,
inference(avatar_split_clause,[],[f176,f312]) ).
fof(f317,plain,
( ! [X0] : member(z,unordered_pair(z,X0))
| ~ spl5_6 ),
inference(resolution,[],[f314,f9]) ).
fof(f319,definition,
( spl5_7
<=> ! [X0] : member(z,unordered_pair(z,X0)) ),
introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition]) ).
fof(f320,plain,
( ! [X0] : member(z,unordered_pair(z,X0))
| ~ spl5_7 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( spl5_7
| ~ spl5_6 ),
inference(avatar_split_clause,[],[f317,f312,f319]) ).
fof(f322,plain,
( member(z,sF1)
| ~ spl5_3
| ~ spl5_7 ),
inference(superposition,[],[f320,f301]) ).
fof(f326,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,z)
| ~ member(X0,y) )
| ~ spl5_1 ),
inference(superposition,[],[f23,f289]) ).
fof(f328,definition,
( spl5_8
<=> ! [X0] :
( member(X0,sF0)
| ~ member(X0,z)
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition]) ).
fof(f329,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,z)
| ~ member(X0,y) )
| ~ spl5_8 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f330,plain,
( spl5_8
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f326,f287,f328]) ).
fof(f332,definition,
( spl5_9
<=> domain_of(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition]) ).
fof(f334,plain,
( domain_of(sF3) = sF4
| ~ spl5_9 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,plain,
spl5_9,
inference(avatar_split_clause,[],[f284,f332]) ).
fof(f337,plain,
( ! [X0] :
( ~ member(X0,sF1)
| z = X0
| z = X0 )
| ~ spl5_3 ),
inference(superposition,[],[f8,f301]) ).
fof(f338,plain,
( ! [X0] :
( ~ member(X0,sF1)
| z = X0 )
| ~ spl5_3 ),
inference(duplicate_literal_removal,[],[f337]) ).
fof(f340,definition,
( spl5_10
<=> intersection(element_relation,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition]) ).
fof(f342,plain,
( intersection(element_relation,sF2) = sF3
| ~ spl5_10 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,plain,
spl5_10,
inference(avatar_split_clause,[],[f282,f340]) ).
fof(f344,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) )
| ~ spl5_10 ),
inference(superposition,[],[f23,f342]) ).
fof(f345,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) )
| ~ spl5_10 ),
inference(superposition,[],[f22,f342]) ).
fof(f346,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,element_relation) )
| ~ spl5_10 ),
inference(superposition,[],[f21,f342]) ).
fof(f348,definition,
( spl5_11
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition]) ).
fof(f349,plain,
( ! [X0] :
( member(X0,sF2)
| ~ member(X0,sF3) )
| ~ spl5_11 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f350,plain,
( spl5_11
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f345,f340,f348]) ).
fof(f352,definition,
( spl5_12
<=> ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition]) ).
fof(f353,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,element_relation) )
| ~ spl5_12 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f354,plain,
( spl5_12
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f344,f340,f352]) ).
fof(f356,definition,
( spl5_13
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,element_relation) ) ),
introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition]) ).
fof(f357,plain,
( ! [X0] :
( member(X0,element_relation)
| ~ member(X0,sF3) )
| ~ spl5_13 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f358,plain,
( spl5_13
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f346,f340,f356]) ).
fof(f360,definition,
( spl5_14
<=> sF0 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_14])],[avatar_definition]) ).
fof(f362,plain,
( sF0 != sF4
| spl5_14 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
~ spl5_14,
inference(avatar_split_clause,[],[f285,f360]) ).
fof(f368,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,y) )
| ~ spl5_2 ),
inference(superposition,[],[f195,f294]) ).
fof(f370,definition,
( spl5_15
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl5_15])],[avatar_definition]) ).
fof(f371,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X0,y) )
| ~ spl5_15 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( spl5_15
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f368,f292,f370]) ).
fof(f373,plain,
( ! [X0,X1] :
( member(X0,y)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3) )
| ~ spl5_11
| ~ spl5_15 ),
inference(resolution,[],[f371,f349]) ).
fof(f377,definition,
( spl5_16
<=> member(z,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition]) ).
fof(f379,plain,
( member(z,sF1)
| ~ spl5_16 ),
inference(avatar_component_clause,[],[f377]) ).
fof(f380,plain,
( spl5_16
| ~ spl5_3
| ~ spl5_7 ),
inference(avatar_split_clause,[],[f322,f319,f299,f377]) ).
fof(f385,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X1) ),
inference(resolution,[],[f2,f22]) ).
fof(f386,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X0) ),
inference(resolution,[],[f2,f21]) ).
fof(f390,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,[],[f196,f294]) ).
fof(f392,definition,
( spl5_17
<=> ! [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_17])],[avatar_definition]) ).
fof(f393,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,sF1) )
| ~ spl5_17 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( spl5_17
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f390,f292,f392]) ).
fof(f395,plain,
( ! [X0,X1] :
( member(X0,sF1)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3) )
| ~ spl5_11
| ~ spl5_17 ),
inference(resolution,[],[f393,f349]) ).
fof(f404,plain,
( ! [X0] :
( subclass(X0,sF0)
| ~ member(not_subclass_element(X0,sF0),z)
| ~ member(not_subclass_element(X0,sF0),y) )
| ~ spl5_8 ),
inference(resolution,[],[f3,f329]) ).
fof(f409,definition,
( spl5_18
<=> ! [X0] :
( subclass(X0,sF0)
| ~ member(not_subclass_element(X0,sF0),z)
| ~ member(not_subclass_element(X0,sF0),y) ) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
fof(f410,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF0),y)
| ~ member(not_subclass_element(X0,sF0),z)
| subclass(X0,sF0) )
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f411,plain,
( spl5_18
| ~ spl5_8 ),
inference(avatar_split_clause,[],[f404,f328,f409]) ).
fof(f415,plain,
! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ subclass(X1,universal_class)
| member(X0,unordered_pair(X2,X0)) ),
inference(resolution,[],[f1,f10]) ).
fof(f429,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X2,X0))
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[],[f415,f4]) ).
fof(f433,definition,
( spl5_19
<=> ! [X0] :
( ~ member(X0,sF1)
| z = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( ~ member(X0,sF1)
| z = X0 )
| ~ spl5_19 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl5_19
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f338,f299,f433]) ).
fof(f439,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,domain_of(X0))
| ~ member(X1,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f203,f1]) ).
fof(f443,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,[],[f439,f4]) ).
fof(f445,plain,
( ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),y) )
| ~ spl5_1 ),
inference(superposition,[],[f386,f289]) ).
fof(f454,plain,
( ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),z) )
| ~ spl5_1 ),
inference(superposition,[],[f385,f289]) ).
fof(f457,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,[],[f443,f334]) ).
fof(f459,definition,
( spl5_21
<=> ! [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_21])],[avatar_definition]) ).
fof(f460,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_21 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( spl5_21
| ~ spl5_9 ),
inference(avatar_split_clause,[],[f457,f332,f459]) ).
fof(f465,definition,
( spl5_22
<=> ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),y) ) ),
introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition]) ).
fof(f466,plain,
( ! [X0] :
( member(not_subclass_element(sF0,X0),y)
| subclass(sF0,X0) )
| ~ spl5_22 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( spl5_22
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f445,f287,f465]) ).
fof(f478,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f479,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f481,plain,
( null_class = sF1
| z = regular(sF1)
| ~ spl5_19 ),
inference(resolution,[],[f68,f434]) ).
fof(f487,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,y) )
| ~ spl5_2 ),
inference(superposition,[],[f197,f294]) ).
fof(f489,definition,
( spl5_24
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition]) ).
fof(f490,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,sF1)
| ~ member(X0,y) )
| ~ spl5_24 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( spl5_24
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f487,f292,f489]) ).
fof(f498,definition,
( spl5_25
<=> ! [X0] :
( subclass(sF0,X0)
| member(not_subclass_element(sF0,X0),z) ) ),
introduced(definition,[new_symbols(definition,[spl5_25])],[avatar_definition]) ).
fof(f499,plain,
( ! [X0] :
( member(not_subclass_element(sF0,X0),z)
| subclass(sF0,X0) )
| ~ spl5_25 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( spl5_25
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f454,f287,f498]) ).
fof(f503,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_21 ),
inference(resolution,[],[f460,f3]) ).
fof(f510,definition,
( spl5_27
<=> ! [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_27])],[avatar_definition]) ).
fof(f511,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_27 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f512,plain,
( spl5_27
| ~ spl5_21 ),
inference(avatar_split_clause,[],[f503,f459,f510]) ).
fof(f603,definition,
( spl5_34
<=> ! [X0,X1] :
( member(X0,y)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_34])],[avatar_definition]) ).
fof(f604,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| member(X0,y) )
| ~ spl5_34 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f605,plain,
( spl5_34
| ~ spl5_11
| ~ spl5_15 ),
inference(avatar_split_clause,[],[f373,f370,f348,f603]) ).
fof(f630,plain,
! [X2,X0,X1] :
( member(regular(intersection(intersection(X0,X1),X2)),X1)
| null_class = intersection(intersection(X0,X1),X2) ),
inference(resolution,[],[f479,f22]) ).
fof(f640,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f646,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,[],[f478,f198]) ).
fof(f701,plain,
( ! [X0,X1] :
( member(X0,X1)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3) )
| ~ spl5_13 ),
inference(resolution,[],[f199,f357]) ).
fof(f705,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF1)),element_relation)
| member(X0,z) )
| ~ spl5_3 ),
inference(superposition,[],[f199,f301]) ).
fof(f746,definition,
( spl5_40
<=> z = regular(sF1) ),
introduced(definition,[new_symbols(definition,[spl5_40])],[avatar_definition]) ).
fof(f748,plain,
( z = regular(sF1)
| ~ spl5_40 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f750,definition,
( spl5_41
<=> null_class = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_41])],[avatar_definition]) ).
fof(f751,plain,
( null_class != sF1
| spl5_41 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f752,plain,
( null_class = sF1
| ~ spl5_41 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f753,plain,
( spl5_40
| spl5_41
| ~ spl5_19 ),
inference(avatar_split_clause,[],[f481,f433,f750,f746]) ).
fof(f757,definition,
( spl5_42
<=> ! [X0,X1] :
( member(X0,sF1)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_42])],[avatar_definition]) ).
fof(f758,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3)
| member(X0,sF1) )
| ~ spl5_42 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( spl5_42
| ~ spl5_11
| ~ spl5_17 ),
inference(avatar_split_clause,[],[f395,f392,f348,f757]) ).
fof(f856,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,[],[f200,f197]) ).
fof(f896,definition,
( spl5_50
<=> ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF1)),element_relation)
| member(X0,z) ) ),
introduced(definition,[new_symbols(definition,[spl5_50])],[avatar_definition]) ).
fof(f897,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF1)),element_relation)
| member(X0,z) )
| ~ spl5_50 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f898,plain,
( spl5_50
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f705,f299,f896]) ).
fof(f920,definition,
( spl5_52
<=> ! [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_52])],[avatar_definition]) ).
fof(f921,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| member(X0,X1) )
| ~ spl5_52 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f922,plain,
( spl5_52
| ~ spl5_13 ),
inference(avatar_split_clause,[],[f701,f356,f920]) ).
fof(f937,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(superposition,[],[f202,f646]) ).
fof(f950,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,[],[f937]) ).
fof(f960,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,[],[f950,f334]) ).
fof(f963,definition,
( spl5_53
<=> ! [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_53])],[avatar_definition]) ).
fof(f964,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_53 ),
inference(avatar_component_clause,[],[f963]) ).
fof(f965,plain,
( spl5_53
| ~ spl5_9 ),
inference(avatar_split_clause,[],[f960,f332,f963]) ).
fof(f968,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_53 ),
inference(resolution,[],[f964,f2]) ).
fof(f977,definition,
( spl5_55
<=> ! [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_55])],[avatar_definition]) ).
fof(f978,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_55 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f979,plain,
( spl5_55
| ~ spl5_53 ),
inference(avatar_split_clause,[],[f968,f963,f977]) ).
fof(f1042,definition,
( spl5_61
<=> member(z,z) ),
introduced(definition,[new_symbols(definition,[spl5_61])],[avatar_definition]) ).
fof(f1043,plain,
( member(z,z)
| ~ spl5_61 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1044,plain,
( ~ member(z,z)
| spl5_61 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1285,definition,
( spl5_80
<=> ! [X0] :
( member(z,X0)
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_80])],[avatar_definition]) ).
fof(f1286,plain,
( ! [X0] :
( member(z,X0)
| null_class = X0 )
| ~ spl5_80 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1296,plain,
( ! [X0] :
( complement(X0) = null_class
| ~ member(z,X0) )
| ~ spl5_80 ),
inference(resolution,[],[f1286,f24]) ).
fof(f1333,definition,
( spl5_84
<=> ! [X0] :
( complement(X0) = null_class
| ~ member(z,X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_84])],[avatar_definition]) ).
fof(f1334,plain,
( ! [X0] :
( ~ member(z,X0)
| complement(X0) = null_class )
| ~ spl5_84 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1335,plain,
( spl5_84
| ~ spl5_80 ),
inference(avatar_split_clause,[],[f1296,f1285,f1333]) ).
fof(f1336,plain,
( ! [X0] :
( complement(X0) = null_class
| null_class = X0 )
| ~ spl5_80
| ~ spl5_84 ),
inference(resolution,[],[f1334,f1286]) ).
fof(f1371,definition,
( spl5_85
<=> ! [X0] :
( complement(X0) = null_class
| null_class = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_85])],[avatar_definition]) ).
fof(f1372,plain,
( ! [X0] :
( complement(X0) = null_class
| null_class = X0 )
| ~ spl5_85 ),
inference(avatar_component_clause,[],[f1371]) ).
fof(f1373,plain,
( spl5_85
| ~ spl5_80
| ~ spl5_84 ),
inference(avatar_split_clause,[],[f1336,f1333,f1285,f1371]) ).
fof(f1465,plain,
( ! [X0,X1] :
( ~ member(X0,null_class)
| ~ member(X0,X1)
| null_class = X1 )
| ~ spl5_85 ),
inference(superposition,[],[f24,f1372]) ).
fof(f1466,plain,
( ! [X0,X1] :
( ~ member(X0,null_class)
| null_class = X1 )
| ~ spl5_85 ),
inference(forward_subsumption_resolution,[],[f1465,f640]) ).
fof(f1473,definition,
( spl5_89
<=> ! [X1] : null_class = X1 ),
introduced(definition,[new_symbols(definition,[spl5_89])],[avatar_definition]) ).
fof(f1474,plain,
( ! [X1] : null_class = X1
| ~ spl5_89 ),
inference(avatar_component_clause,[],[f1473]) ).
fof(f1476,definition,
( spl5_90
<=> ! [X0] : ~ member(X0,null_class) ),
introduced(definition,[new_symbols(definition,[spl5_90])],[avatar_definition]) ).
fof(f1477,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl5_90 ),
inference(avatar_component_clause,[],[f1476]) ).
fof(f1478,plain,
( spl5_89
| spl5_90
| ~ spl5_85 ),
inference(avatar_split_clause,[],[f1466,f1371,f1476,f1473]) ).
fof(f1682,plain,
( null_class != sF0
| spl5_14
| ~ spl5_89 ),
inference(superposition,[],[f362,f1474]) ).
fof(f1696,plain,
( $false
| spl5_14
| ~ spl5_89 ),
inference(forward_subsumption_resolution,[],[f1682,f1474]) ).
fof(f1697,plain,
( spl5_14
| ~ spl5_89 ),
inference(avatar_contradiction_clause,[],[f1696]) ).
fof(f2145,definition,
( spl5_93
<=> ! [X0] : null_class = intersection(null_class,X0) ),
introduced(definition,[new_symbols(definition,[spl5_93])],[avatar_definition]) ).
fof(f2146,plain,
( ! [X0] : null_class = intersection(null_class,X0)
| ~ spl5_93 ),
inference(avatar_component_clause,[],[f2145]) ).
fof(f2153,plain,
( ! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) )
| ~ spl5_93 ),
inference(superposition,[],[f202,f2146]) ).
fof(f2154,plain,
( ! [X0] : ~ member(X0,domain_of(null_class))
| ~ spl5_93 ),
inference(trivial_inequality_removal,[],[f2153]) ).
fof(f2156,definition,
( spl5_94
<=> ! [X0] : ~ member(X0,domain_of(null_class)) ),
introduced(definition,[new_symbols(definition,[spl5_94])],[avatar_definition]) ).
fof(f2157,plain,
( ! [X0] : ~ member(X0,domain_of(null_class))
| ~ spl5_94 ),
inference(avatar_component_clause,[],[f2156]) ).
fof(f2158,plain,
( spl5_94
| ~ spl5_93 ),
inference(avatar_split_clause,[],[f2154,f2145,f2156]) ).
fof(f2242,definition,
( spl5_100
<=> null_class = domain_of(null_class) ),
introduced(definition,[new_symbols(definition,[spl5_100])],[avatar_definition]) ).
fof(f2244,plain,
( null_class = domain_of(null_class)
| ~ spl5_100 ),
inference(avatar_component_clause,[],[f2242]) ).
fof(f2321,plain,
( null_class = domain_of(null_class)
| ~ spl5_94 ),
inference(resolution,[],[f68,f2157]) ).
fof(f2497,plain,
( ! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) )
| ~ spl5_93 ),
inference(superposition,[],[f202,f2146]) ).
fof(f2498,plain,
( ! [X0] : ~ member(X0,domain_of(null_class))
| ~ spl5_93 ),
inference(trivial_inequality_removal,[],[f2497]) ).
fof(f2499,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl5_93
| ~ spl5_100 ),
inference(forward_demodulation,[],[f2498,f2244]) ).
fof(f3000,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f3223,plain,
( member(z,null_class)
| ~ spl5_16
| ~ spl5_41 ),
inference(superposition,[],[f379,f752]) ).
fof(f3313,definition,
( spl5_131
<=> member(z,null_class) ),
introduced(definition,[new_symbols(definition,[spl5_131])],[avatar_definition]) ).
fof(f3314,plain,
( ~ member(z,null_class)
| spl5_131 ),
inference(avatar_component_clause,[],[f3313]) ).
fof(f3315,plain,
( member(z,null_class)
| ~ spl5_131 ),
inference(avatar_component_clause,[],[f3313]) ).
fof(f3316,plain,
( spl5_131
| ~ spl5_16
| ~ spl5_41 ),
inference(avatar_split_clause,[],[f3223,f750,f377,f3313]) ).
fof(f3317,plain,
( ! [X0] :
( member(z,X0)
| null_class = X0 )
| ~ spl5_131 ),
inference(resolution,[],[f3315,f3000]) ).
fof(f3318,plain,
( spl5_80
| ~ spl5_131 ),
inference(avatar_split_clause,[],[f3317,f3313,f1285]) ).
fof(f3490,plain,
( null_class = intersection(sF1,z)
| null_class = sF1
| ~ spl5_40 ),
inference(superposition,[],[f70,f748]) ).
fof(f3492,plain,
( null_class = intersection(sF1,z)
| ~ spl5_40
| spl5_41 ),
inference(forward_subsumption_resolution,[],[f3490,f751]) ).
fof(f3537,definition,
( spl5_133
<=> null_class = intersection(sF1,z) ),
introduced(definition,[new_symbols(definition,[spl5_133])],[avatar_definition]) ).
fof(f3539,plain,
( null_class = intersection(sF1,z)
| ~ spl5_133 ),
inference(avatar_component_clause,[],[f3537]) ).
fof(f3540,plain,
( spl5_133
| ~ spl5_40
| spl5_41 ),
inference(avatar_split_clause,[],[f3492,f750,f746,f3537]) ).
fof(f3868,plain,
( $false
| ~ spl5_90
| ~ spl5_131 ),
inference(forward_subsumption_resolution,[],[f3315,f1477]) ).
fof(f3869,plain,
( ~ spl5_90
| ~ spl5_131 ),
inference(avatar_contradiction_clause,[],[f3868]) ).
fof(f4159,plain,
( ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF1) )
| ~ spl5_133 ),
inference(superposition,[],[f21,f3539]) ).
fof(f4161,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,z)
| ~ member(X0,sF1) )
| ~ spl5_133 ),
inference(superposition,[],[f23,f3539]) ).
fof(f4167,definition,
( spl5_145
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,z)
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_145])],[avatar_definition]) ).
fof(f4168,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,z)
| ~ member(X0,sF1) )
| ~ spl5_145 ),
inference(avatar_component_clause,[],[f4167]) ).
fof(f4169,plain,
( spl5_145
| ~ spl5_133 ),
inference(avatar_split_clause,[],[f4161,f3537,f4167]) ).
fof(f4171,plain,
( ~ member(z,z)
| ~ member(z,sF1)
| spl5_131
| ~ spl5_145 ),
inference(resolution,[],[f4168,f3314]) ).
fof(f4174,definition,
( spl5_146
<=> ! [X0] :
( ~ member(X0,null_class)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_146])],[avatar_definition]) ).
fof(f4175,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,null_class) )
| ~ spl5_146 ),
inference(avatar_component_clause,[],[f4174]) ).
fof(f4176,plain,
( spl5_146
| ~ spl5_133 ),
inference(avatar_split_clause,[],[f4159,f3537,f4174]) ).
fof(f4177,plain,
( ! [X0] :
( ~ member(X0,null_class)
| z = X0 )
| ~ spl5_19
| ~ spl5_146 ),
inference(resolution,[],[f4175,f434]) ).
fof(f4180,definition,
( spl5_147
<=> ! [X0] :
( ~ member(X0,null_class)
| z = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_147])],[avatar_definition]) ).
fof(f4181,plain,
( ! [X0] :
( ~ member(X0,null_class)
| z = X0 )
| ~ spl5_147 ),
inference(avatar_component_clause,[],[f4180]) ).
fof(f4182,plain,
( spl5_147
| ~ spl5_19
| ~ spl5_146 ),
inference(avatar_split_clause,[],[f4177,f4174,f433,f4180]) ).
fof(f4187,plain,
( ! [X0] :
( z = regular(intersection(null_class,X0))
| null_class = intersection(null_class,X0) )
| ~ spl5_147 ),
inference(resolution,[],[f4181,f479]) ).
fof(f4216,plain,
( ~ member(z,sF1)
| ~ spl5_61
| spl5_131
| ~ spl5_145 ),
inference(forward_subsumption_resolution,[],[f4171,f1043]) ).
fof(f4218,plain,
( $false
| ~ spl5_16
| ~ spl5_61
| spl5_131
| ~ spl5_145 ),
inference(forward_subsumption_resolution,[],[f4216,f379]) ).
fof(f4219,plain,
( ~ spl5_16
| ~ spl5_61
| spl5_131
| ~ spl5_145 ),
inference(avatar_contradiction_clause,[],[f4218]) ).
fof(f4541,plain,
( spl5_100
| ~ spl5_94 ),
inference(avatar_split_clause,[],[f2321,f2156,f2242]) ).
fof(f5920,plain,
( ! [X0] :
( member(regular(intersection(null_class,X0)),z)
| null_class = intersection(null_class,X0) )
| ~ spl5_133 ),
inference(superposition,[],[f630,f3539]) ).
fof(f5928,plain,
( ! [X0] :
( member(z,z)
| null_class = intersection(null_class,X0) )
| ~ spl5_133
| ~ spl5_147 ),
inference(forward_subsumption_demodulation,[],[f5920,f4187]) ).
fof(f5940,plain,
( ! [X0] : null_class = intersection(null_class,X0)
| spl5_61
| ~ spl5_133
| ~ spl5_147 ),
inference(forward_subsumption_resolution,[],[f5928,f1044]) ).
fof(f5960,plain,
( spl5_93
| spl5_61
| ~ spl5_133
| ~ spl5_147 ),
inference(avatar_split_clause,[],[f5940,f4180,f3537,f1042,f2145]) ).
fof(f5996,plain,
( spl5_90
| ~ spl5_93
| ~ spl5_100 ),
inference(avatar_split_clause,[],[f2499,f2242,f2145,f1476]) ).
fof(f7128,definition,
( spl5_242
<=> 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_242])],[avatar_definition]) ).
fof(f7130,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_242 ),
inference(avatar_component_clause,[],[f7128]) ).
fof(f7132,definition,
( spl5_243
<=> ! [X0] : ~ member(not_subclass_element(sF0,sF4),X0) ),
introduced(definition,[new_symbols(definition,[spl5_243])],[avatar_definition]) ).
fof(f7133,plain,
( ! [X0] : ~ member(not_subclass_element(sF0,sF4),X0)
| ~ spl5_243 ),
inference(avatar_component_clause,[],[f7132]) ).
fof(f7137,plain,
( subclass(sF0,sF4)
| ~ spl5_22
| ~ spl5_243 ),
inference(resolution,[],[f7133,f466]) ).
fof(f7154,definition,
( spl5_244
<=> subclass(sF0,sF4) ),
introduced(definition,[new_symbols(definition,[spl5_244])],[avatar_definition]) ).
fof(f7155,plain,
( ~ subclass(sF0,sF4)
| spl5_244 ),
inference(avatar_component_clause,[],[f7154]) ).
fof(f7156,plain,
( subclass(sF0,sF4)
| ~ spl5_244 ),
inference(avatar_component_clause,[],[f7154]) ).
fof(f7157,plain,
( spl5_244
| ~ spl5_22
| ~ spl5_243 ),
inference(avatar_split_clause,[],[f7137,f7132,f465,f7154]) ).
fof(f7158,plain,
( ~ subclass(sF4,sF0)
| sF0 = sF4
| ~ spl5_244 ),
inference(resolution,[],[f7156,f7]) ).
fof(f7159,plain,
( ~ subclass(sF4,sF0)
| spl5_14
| ~ spl5_244 ),
inference(forward_subsumption_resolution,[],[f7158,f362]) ).
fof(f7161,definition,
( spl5_245
<=> subclass(sF4,sF0) ),
introduced(definition,[new_symbols(definition,[spl5_245])],[avatar_definition]) ).
fof(f7163,plain,
( ~ subclass(sF4,sF0)
| spl5_245 ),
inference(avatar_component_clause,[],[f7161]) ).
fof(f7164,plain,
( ~ spl5_245
| spl5_14
| ~ spl5_244 ),
inference(avatar_split_clause,[],[f7159,f7154,f360,f7161]) ).
fof(f7165,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_55
| spl5_245 ),
inference(resolution,[],[f7163,f978]) ).
fof(f7166,plain,
( spl5_242
| ~ spl5_55
| spl5_245 ),
inference(avatar_split_clause,[],[f7165,f7161,f977,f7128]) ).
fof(f8218,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_242 ),
inference(superposition,[],[f195,f7130]) ).
fof(f8224,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)))),y)
| ~ spl5_34
| ~ spl5_242 ),
inference(superposition,[],[f604,f7130]) ).
fof(f8225,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),element_relation)
| ~ 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(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ spl5_242 ),
inference(superposition,[],[f856,f7130]) ).
fof(f8226,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_52
| ~ spl5_242 ),
inference(superposition,[],[f921,f7130]) ).
fof(f8258,definition,
( spl5_249
<=> member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),y) ),
introduced(definition,[new_symbols(definition,[spl5_249])],[avatar_definition]) ).
fof(f8260,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),y)
| ~ spl5_249 ),
inference(avatar_component_clause,[],[f8258]) ).
fof(f8272,definition,
( spl5_251
<=> 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_251])],[avatar_definition]) ).
fof(f8273,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| ~ spl5_251 ),
inference(avatar_component_clause,[],[f8272]) ).
fof(f8274,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| spl5_251 ),
inference(avatar_component_clause,[],[f8272]) ).
fof(f8276,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| spl5_251 ),
inference(resolution,[],[f8274,f479]) ).
fof(f8283,definition,
( spl5_252
<=> ! [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_252])],[avatar_definition]) ).
fof(f8284,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_252 ),
inference(avatar_component_clause,[],[f8283]) ).
fof(f8285,plain,
( spl5_252
| ~ spl5_242 ),
inference(avatar_split_clause,[],[f8218,f7128,f8283]) ).
fof(f8303,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_27
| spl5_244 ),
inference(resolution,[],[f7155,f511]) ).
fof(f8442,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),sF3)
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_42
| ~ spl5_242 ),
inference(superposition,[],[f758,f7130]) ).
fof(f8464,definition,
( spl5_257
<=> 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_257])],[avatar_definition]) ).
fof(f8465,plain,
( null_class != intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| spl5_257 ),
inference(avatar_component_clause,[],[f8464]) ).
fof(f8466,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))
| ~ spl5_257 ),
inference(avatar_component_clause,[],[f8464]) ).
fof(f8467,plain,
( spl5_257
| spl5_251 ),
inference(avatar_split_clause,[],[f8276,f8272,f8464]) ).
fof(f8470,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_42
| ~ spl5_242
| ~ spl5_251 ),
inference(forward_subsumption_resolution,[],[f8442,f8273]) ).
fof(f8473,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_52
| ~ spl5_242
| ~ spl5_251 ),
inference(forward_subsumption_resolution,[],[f8226,f8273]) ).
fof(f8483,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_252 ),
inference(resolution,[],[f8284,f478]) ).
fof(f8489,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_252
| spl5_257 ),
inference(forward_subsumption_resolution,[],[f8483,f8465]) ).
fof(f8502,definition,
( spl5_258
<=> 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_258])],[avatar_definition]) ).
fof(f8504,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),sF1)
| ~ spl5_258 ),
inference(avatar_component_clause,[],[f8502]) ).
fof(f8505,plain,
( spl5_258
| ~ spl5_42
| ~ spl5_242
| ~ spl5_251 ),
inference(avatar_split_clause,[],[f8470,f8272,f7128,f757,f8502]) ).
fof(f8508,plain,
( z = second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_19
| ~ spl5_258 ),
inference(resolution,[],[f8504,f434]) ).
fof(f8518,definition,
( spl5_259
<=> z = 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_259])],[avatar_definition]) ).
fof(f8520,plain,
( z = second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ spl5_259 ),
inference(avatar_component_clause,[],[f8518]) ).
fof(f8521,plain,
( spl5_259
| ~ spl5_19
| ~ spl5_258 ),
inference(avatar_split_clause,[],[f8508,f8502,f433,f8518]) ).
fof(f8523,definition,
( spl5_260
<=> 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_260])],[avatar_definition]) ).
fof(f8525,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_260 ),
inference(avatar_component_clause,[],[f8523]) ).
fof(f8526,plain,
( spl5_260
| ~ spl5_252
| spl5_257 ),
inference(avatar_split_clause,[],[f8489,f8464,f8283,f8523]) ).
fof(f8532,definition,
( spl5_262
<=> member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_262])],[avatar_definition]) ).
fof(f8533,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ spl5_262 ),
inference(avatar_component_clause,[],[f8532]) ).
fof(f8544,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_260 ),
inference(resolution,[],[f8525,f8]) ).
fof(f8548,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_260 ),
inference(duplicate_literal_removal,[],[f8544]) ).
fof(f8550,definition,
( spl5_263
<=> 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_263])],[avatar_definition]) ).
fof(f8552,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_263 ),
inference(avatar_component_clause,[],[f8550]) ).
fof(f8553,plain,
( spl5_263
| ~ spl5_260 ),
inference(avatar_split_clause,[],[f8548,f8523,f8550]) ).
fof(f8558,plain,
( member(not_subclass_element(sF4,sF0),y)
| ~ spl5_249
| ~ spl5_263 ),
inference(superposition,[],[f8260,f8552]) ).
fof(f8559,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),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_242
| ~ spl5_263 ),
inference(superposition,[],[f7130,f8552]) ).
fof(f8561,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),unordered_pair(z,z)))
| ~ spl5_242
| ~ spl5_259
| ~ spl5_263 ),
inference(forward_demodulation,[],[f8559,f8520]) ).
fof(f8562,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))) = unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1))
| ~ spl5_3
| ~ spl5_242
| ~ spl5_259
| ~ spl5_263 ),
inference(forward_demodulation,[],[f8561,f301]) ).
fof(f8564,definition,
( spl5_264
<=> member(not_subclass_element(sF4,sF0),y) ),
introduced(definition,[new_symbols(definition,[spl5_264])],[avatar_definition]) ).
fof(f8566,plain,
( member(not_subclass_element(sF4,sF0),y)
| ~ spl5_264 ),
inference(avatar_component_clause,[],[f8564]) ).
fof(f8567,plain,
( spl5_264
| ~ spl5_249
| ~ spl5_263 ),
inference(avatar_split_clause,[],[f8558,f8550,f8258,f8564]) ).
fof(f8568,plain,
( ~ member(not_subclass_element(sF4,sF0),z)
| subclass(sF4,sF0)
| ~ spl5_18
| ~ spl5_264 ),
inference(resolution,[],[f8566,f410]) ).
fof(f8570,plain,
( ~ member(not_subclass_element(sF4,sF0),z)
| ~ spl5_18
| spl5_245
| ~ spl5_264 ),
inference(forward_subsumption_resolution,[],[f8568,f7163]) ).
fof(f8572,definition,
( spl5_265
<=> member(not_subclass_element(sF4,sF0),z) ),
introduced(definition,[new_symbols(definition,[spl5_265])],[avatar_definition]) ).
fof(f8574,plain,
( ~ member(not_subclass_element(sF4,sF0),z)
| spl5_265 ),
inference(avatar_component_clause,[],[f8572]) ).
fof(f8575,plain,
( ~ spl5_265
| ~ spl5_18
| spl5_245
| ~ spl5_264 ),
inference(avatar_split_clause,[],[f8570,f8564,f7161,f409,f8572]) ).
fof(f8716,definition,
( spl5_270
<=> 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_270])],[avatar_definition]) ).
fof(f8718,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ spl5_270 ),
inference(avatar_component_clause,[],[f8716]) ).
fof(f8719,plain,
( spl5_270
| spl5_243
| ~ spl5_27
| spl5_244 ),
inference(avatar_split_clause,[],[f8303,f7154,f510,f7132,f8716]) ).
fof(f8724,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_270 ),
inference(superposition,[],[f23,f8718]) ).
fof(f8734,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_90
| ~ spl5_270 ),
inference(forward_subsumption_resolution,[],[f8724,f1477]) ).
fof(f8777,definition,
( spl5_273
<=> ! [X0] :
( ~ 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_273])],[avatar_definition]) ).
fof(f8778,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF4),not_subclass_element(sF0,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_273 ),
inference(avatar_component_clause,[],[f8777]) ).
fof(f8779,plain,
( spl5_273
| ~ spl5_90
| ~ spl5_270 ),
inference(avatar_split_clause,[],[f8734,f8716,f1476,f8777]) ).
fof(f8782,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_273 ),
inference(resolution,[],[f8778,f197]) ).
fof(f8793,definition,
( spl5_274
<=> ! [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_274])],[avatar_definition]) ).
fof(f8794,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_274 ),
inference(avatar_component_clause,[],[f8793]) ).
fof(f8795,plain,
( spl5_274
| ~ spl5_273 ),
inference(avatar_split_clause,[],[f8782,f8777,f8793]) ).
fof(f8796,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_12
| ~ spl5_274 ),
inference(resolution,[],[f8794,f353]) ).
fof(f8877,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF4,sF0),domain_of(sF3))
| ~ spl5_257 ),
inference(superposition,[],[f202,f8466]) ).
fof(f8888,plain,
( ~ member(not_subclass_element(sF4,sF0),domain_of(sF3))
| ~ spl5_257 ),
inference(trivial_inequality_removal,[],[f8877]) ).
fof(f8891,plain,
( ~ member(not_subclass_element(sF4,sF0),sF4)
| ~ spl5_9
| ~ spl5_257 ),
inference(forward_demodulation,[],[f8888,f334]) ).
fof(f8893,definition,
( spl5_275
<=> member(not_subclass_element(sF4,sF0),sF4) ),
introduced(definition,[new_symbols(definition,[spl5_275])],[avatar_definition]) ).
fof(f8894,plain,
( member(not_subclass_element(sF4,sF0),sF4)
| ~ spl5_275 ),
inference(avatar_component_clause,[],[f8893]) ).
fof(f8895,plain,
( ~ member(not_subclass_element(sF4,sF0),sF4)
| spl5_275 ),
inference(avatar_component_clause,[],[f8893]) ).
fof(f8896,plain,
( ~ spl5_275
| ~ spl5_9
| ~ spl5_257 ),
inference(avatar_split_clause,[],[f8891,f8464,f332,f8893]) ).
fof(f8899,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF4,sF0),X0)
| ~ subclass(X0,sF4) )
| spl5_275 ),
inference(resolution,[],[f8895,f1]) ).
fof(f8901,definition,
( spl5_276
<=> ! [X0] :
( ~ member(not_subclass_element(sF4,sF0),X0)
| ~ subclass(X0,sF4) ) ),
introduced(definition,[new_symbols(definition,[spl5_276])],[avatar_definition]) ).
fof(f8902,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF4,sF0),X0)
| ~ subclass(X0,sF4) )
| ~ spl5_276 ),
inference(avatar_component_clause,[],[f8901]) ).
fof(f8903,plain,
( spl5_276
| spl5_275 ),
inference(avatar_split_clause,[],[f8899,f8893,f8901]) ).
fof(f8904,plain,
( ~ subclass(sF4,sF4)
| subclass(sF4,sF0)
| ~ spl5_276 ),
inference(resolution,[],[f8902,f2]) ).
fof(f9145,definition,
( spl5_280
<=> ! [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_280])],[avatar_definition]) ).
fof(f9146,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_280 ),
inference(avatar_component_clause,[],[f9145]) ).
fof(f9147,plain,
( spl5_280
| ~ spl5_12
| ~ spl5_274 ),
inference(avatar_split_clause,[],[f8796,f8793,f352,f9145]) ).
fof(f9148,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,y) )
| ~ spl5_24
| ~ spl5_280 ),
inference(resolution,[],[f9146,f490]) ).
fof(f9260,definition,
( spl5_284
<=> ! [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,y) ) ),
introduced(definition,[new_symbols(definition,[spl5_284])],[avatar_definition]) ).
fof(f9261,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,y) )
| ~ spl5_284 ),
inference(avatar_component_clause,[],[f9260]) ).
fof(f9262,plain,
( spl5_284
| ~ spl5_24
| ~ spl5_280 ),
inference(avatar_split_clause,[],[f9148,f9145,f489,f9260]) ).
fof(f9263,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,y)
| ~ member(X1,X0)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class) )
| ~ spl5_284 ),
inference(resolution,[],[f9261,f856]) ).
fof(f9274,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,y)
| ~ member(X1,X0)
| ~ member(X1,universal_class) )
| ~ spl5_284 ),
inference(duplicate_literal_removal,[],[f9263]) ).
fof(f9279,definition,
( spl5_285
<=> ! [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,y)
| ~ member(X1,X0)
| ~ member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl5_285])],[avatar_definition]) ).
fof(f9280,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,y)
| ~ member(X1,X0)
| ~ member(X1,universal_class) )
| ~ spl5_285 ),
inference(avatar_component_clause,[],[f9279]) ).
fof(f9281,plain,
( spl5_285
| ~ spl5_284 ),
inference(avatar_split_clause,[],[f9274,f9260,f9279]) ).
fof(f9283,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(not_subclass_element(sF0,sF4),y)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(not_subclass_element(sF0,sF4),universal_class)
| ~ member(not_subclass_element(sF0,sF4),X1) )
| ~ spl5_285 ),
inference(resolution,[],[f9280,f429]) ).
fof(f9296,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),y)
| ~ member(X0,universal_class)
| ~ member(X0,sF1)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(not_subclass_element(sF0,sF4),universal_class) )
| ~ spl5_285 ),
inference(condensation,[],[f9283]) ).
fof(f9301,definition,
( spl5_286
<=> member(not_subclass_element(sF0,sF4),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_286])],[avatar_definition]) ).
fof(f9303,plain,
( ~ member(not_subclass_element(sF0,sF4),universal_class)
| spl5_286 ),
inference(avatar_component_clause,[],[f9301]) ).
fof(f9305,definition,
( spl5_287
<=> ! [X0] :
( ~ member(X0,universal_class)
| ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_287])],[avatar_definition]) ).
fof(f9306,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),X0)
| ~ member(X0,universal_class)
| ~ member(X0,sF1) )
| ~ spl5_287 ),
inference(avatar_component_clause,[],[f9305]) ).
fof(f9308,definition,
( spl5_288
<=> member(not_subclass_element(sF0,sF4),y) ),
introduced(definition,[new_symbols(definition,[spl5_288])],[avatar_definition]) ).
fof(f9310,plain,
( ~ member(not_subclass_element(sF0,sF4),y)
| spl5_288 ),
inference(avatar_component_clause,[],[f9308]) ).
fof(f9311,plain,
( ~ spl5_286
| spl5_287
| ~ spl5_288
| ~ spl5_285 ),
inference(avatar_split_clause,[],[f9296,f9279,f9308,f9305,f9301]) ).
fof(f9312,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF0,sF4),X0)
| ~ subclass(X0,universal_class) )
| spl5_286 ),
inference(resolution,[],[f9303,f1]) ).
fof(f9313,plain,
( ! [X0] : ~ member(not_subclass_element(sF0,sF4),X0)
| spl5_286 ),
inference(forward_subsumption_resolution,[],[f9312,f4]) ).
fof(f9314,plain,
( spl5_243
| spl5_286 ),
inference(avatar_split_clause,[],[f9313,f9301,f7132]) ).
fof(f9316,plain,
( subclass(sF0,sF4)
| ~ spl5_22
| spl5_288 ),
inference(resolution,[],[f9310,f466]) ).
fof(f9321,plain,
( $false
| ~ spl5_22
| spl5_244
| spl5_288 ),
inference(forward_subsumption_resolution,[],[f9316,f7155]) ).
fof(f9322,plain,
( ~ spl5_22
| spl5_244
| spl5_288 ),
inference(avatar_contradiction_clause,[],[f9321]) ).
fof(f9347,plain,
( ~ member(z,universal_class)
| ~ member(z,sF1)
| subclass(sF0,sF4)
| ~ spl5_25
| ~ spl5_287 ),
inference(resolution,[],[f9306,f499]) ).
fof(f9375,plain,
( ~ member(z,sF1)
| subclass(sF0,sF4)
| ~ spl5_6
| ~ spl5_25
| ~ spl5_287 ),
inference(forward_subsumption_resolution,[],[f9347,f314]) ).
fof(f9387,plain,
( subclass(sF0,sF4)
| ~ spl5_6
| ~ spl5_16
| ~ spl5_25
| ~ spl5_287 ),
inference(forward_subsumption_resolution,[],[f9375,f379]) ).
fof(f9391,plain,
( $false
| ~ spl5_6
| ~ spl5_16
| ~ spl5_25
| spl5_244
| ~ spl5_287 ),
inference(forward_subsumption_resolution,[],[f9387,f7155]) ).
fof(f9392,plain,
( ~ spl5_6
| ~ spl5_16
| ~ spl5_25
| spl5_244
| ~ spl5_287 ),
inference(avatar_contradiction_clause,[],[f9391]) ).
fof(f9689,plain,
( z != second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))))
| ~ member(z,universal_class)
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f9705,plain,
( subclass(sF4,sF0)
| ~ spl5_276 ),
inference(forward_subsumption_resolution,[],[f8904,f270]) ).
fof(f9708,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),element_relation)
| ~ 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(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ spl5_242
| ~ spl5_262 ),
inference(forward_subsumption_resolution,[],[f8225,f8533]) ).
fof(f9717,plain,
( not_subclass_element(sF4,sF0) = first(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)))
| ~ spl5_3
| ~ spl5_242
| ~ spl5_259
| ~ spl5_260
| ~ spl5_263 ),
inference(forward_demodulation,[],[f8548,f8562]) ).
fof(f9719,plain,
( $false
| spl5_14
| ~ spl5_244
| ~ spl5_276 ),
inference(forward_subsumption_resolution,[],[f9705,f7159]) ).
fof(f9720,plain,
( spl5_14
| ~ spl5_244
| ~ spl5_276 ),
inference(avatar_contradiction_clause,[],[f9719]) ).
fof(f9722,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class))),element_relation)
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_262 ),
inference(forward_subsumption_resolution,[],[f9708,f8473]) ).
fof(f9725,plain,
( member(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)),element_relation)
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),universal_class)))),universal_class)
| ~ spl5_3
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_259
| ~ spl5_262
| ~ spl5_263 ),
inference(forward_demodulation,[],[f9722,f8562]) ).
fof(f9726,plain,
( ~ member(first(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1))),universal_class)
| member(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)),element_relation)
| ~ spl5_3
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_259
| ~ spl5_262
| ~ spl5_263 ),
inference(forward_demodulation,[],[f9725,f8562]) ).
fof(f9727,plain,
( ~ member(not_subclass_element(sF4,sF0),universal_class)
| member(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)),element_relation)
| ~ spl5_3
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_259
| ~ spl5_260
| ~ spl5_262
| ~ spl5_263 ),
inference(forward_demodulation,[],[f9726,f9717]) ).
fof(f10031,plain,
( spl5_249
| ~ spl5_251
| ~ spl5_34
| ~ spl5_242 ),
inference(avatar_split_clause,[],[f8224,f7128,f603,f8272,f8258]) ).
fof(f10176,definition,
( spl5_308
<=> member(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)),element_relation) ),
introduced(definition,[new_symbols(definition,[spl5_308])],[avatar_definition]) ).
fof(f10178,plain,
( member(unordered_pair(unordered_pair(not_subclass_element(sF4,sF0),not_subclass_element(sF4,sF0)),unordered_pair(not_subclass_element(sF4,sF0),sF1)),element_relation)
| ~ spl5_308 ),
inference(avatar_component_clause,[],[f10176]) ).
fof(f10180,definition,
( spl5_309
<=> member(not_subclass_element(sF4,sF0),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_309])],[avatar_definition]) ).
fof(f10182,plain,
( ~ member(not_subclass_element(sF4,sF0),universal_class)
| spl5_309 ),
inference(avatar_component_clause,[],[f10180]) ).
fof(f10183,plain,
( spl5_308
| ~ spl5_309
| ~ spl5_3
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_259
| ~ spl5_260
| ~ spl5_262
| ~ spl5_263 ),
inference(avatar_split_clause,[],[f9727,f8550,f8532,f8523,f8518,f8272,f7128,f920,f299,f10180,f10176]) ).
fof(f10184,plain,
( $false
| ~ spl5_275
| spl5_309 ),
inference(unit_resulting_resolution,[],[f1,f4,f8894,f10182]) ).
fof(f10187,plain,
( ~ spl5_275
| spl5_309 ),
inference(avatar_contradiction_clause,[],[f10184]) ).
fof(f10307,plain,
( member(not_subclass_element(sF4,sF0),z)
| ~ spl5_50
| ~ spl5_308 ),
inference(resolution,[],[f10178,f897]) ).
fof(f10313,plain,
( $false
| ~ spl5_50
| spl5_265
| ~ spl5_308 ),
inference(forward_subsumption_resolution,[],[f10307,f8574]) ).
fof(f10314,plain,
( ~ spl5_50
| spl5_265
| ~ spl5_308 ),
inference(avatar_contradiction_clause,[],[f10313]) ).
cnf(s142,plain,
spl5_1,
inference(sat_conversion,[],[f290]) ).
cnf(s144,plain,
spl5_2,
inference(sat_conversion,[],[f295]) ).
cnf(s148,plain,
spl5_3,
inference(sat_conversion,[],[f302]) ).
cnf(s154,plain,
spl5_6,
inference(sat_conversion,[],[f315]) ).
cnf(s157,plain,
( ~ spl5_6
| spl5_7 ),
inference(sat_conversion,[],[f321]) ).
cnf(s162,plain,
( ~ spl5_1
| spl5_8 ),
inference(sat_conversion,[],[f330]) ).
cnf(s164,plain,
spl5_9,
inference(sat_conversion,[],[f335]) ).
cnf(s167,plain,
spl5_10,
inference(sat_conversion,[],[f343]) ).
cnf(s172,plain,
( ~ spl5_10
| spl5_11 ),
inference(sat_conversion,[],[f350]) ).
cnf(s174,plain,
( ~ spl5_10
| spl5_12 ),
inference(sat_conversion,[],[f354]) ).
cnf(s176,plain,
( ~ spl5_10
| spl5_13 ),
inference(sat_conversion,[],[f358]) ).
cnf(s178,plain,
~ spl5_14,
inference(sat_conversion,[],[f363]) ).
cnf(s185,plain,
( ~ spl5_2
| spl5_15 ),
inference(sat_conversion,[],[f372]) ).
cnf(s190,plain,
( ~ spl5_3
| ~ spl5_7
| spl5_16 ),
inference(sat_conversion,[],[f380]) ).
cnf(s202,plain,
( ~ spl5_2
| spl5_17 ),
inference(sat_conversion,[],[f394]) ).
cnf(s214,plain,
( ~ spl5_8
| spl5_18 ),
inference(sat_conversion,[],[f411]) ).
cnf(s230,plain,
( ~ spl5_3
| spl5_19 ),
inference(sat_conversion,[],[f435]) ).
cnf(s247,plain,
( ~ spl5_9
| spl5_21 ),
inference(sat_conversion,[],[f461]) ).
cnf(s249,plain,
( ~ spl5_1
| spl5_22 ),
inference(sat_conversion,[],[f467]) ).
cnf(s264,plain,
( ~ spl5_2
| spl5_24 ),
inference(sat_conversion,[],[f491]) ).
cnf(s268,plain,
( ~ spl5_1
| spl5_25 ),
inference(sat_conversion,[],[f500]) ).
cnf(s275,plain,
( ~ spl5_21
| spl5_27 ),
inference(sat_conversion,[],[f512]) ).
cnf(s332,plain,
( ~ spl5_11
| ~ spl5_15
| spl5_34 ),
inference(sat_conversion,[],[f605]) ).
cnf(s430,plain,
( ~ spl5_19
| spl5_40
| spl5_41 ),
inference(sat_conversion,[],[f753]) ).
cnf(s433,plain,
( ~ spl5_11
| ~ spl5_17
| spl5_42 ),
inference(sat_conversion,[],[f759]) ).
cnf(s493,plain,
( ~ spl5_3
| spl5_50 ),
inference(sat_conversion,[],[f898]) ).
cnf(s508,plain,
( ~ spl5_13
| spl5_52 ),
inference(sat_conversion,[],[f922]) ).
cnf(s534,plain,
( ~ spl5_9
| spl5_53 ),
inference(sat_conversion,[],[f965]) ).
cnf(s543,plain,
( ~ spl5_53
| spl5_55 ),
inference(sat_conversion,[],[f979]) ).
cnf(s703,plain,
( ~ spl5_80
| spl5_84 ),
inference(sat_conversion,[],[f1335]) ).
cnf(s721,plain,
( ~ spl5_80
| ~ spl5_84
| spl5_85 ),
inference(sat_conversion,[],[f1373]) ).
cnf(s744,plain,
( ~ spl5_85
| spl5_89
| spl5_90 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s746,plain,
( spl5_14
| ~ spl5_89 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s1200,plain,
( ~ spl5_93
| spl5_94 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s1761,plain,
( ~ spl5_16
| ~ spl5_41
| spl5_131 ),
inference(sat_conversion,[],[f3316]) ).
cnf(s1764,plain,
( spl5_80
| ~ spl5_131 ),
inference(sat_conversion,[],[f3318]) ).
cnf(s1872,plain,
( ~ spl5_40
| spl5_41
| spl5_133 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s1999,plain,
( ~ spl5_90
| ~ spl5_131 ),
inference(sat_conversion,[],[f3869]) ).
cnf(s2169,plain,
( ~ spl5_133
| spl5_145 ),
inference(sat_conversion,[],[f4169]) ).
cnf(s2171,plain,
( ~ spl5_133
| spl5_146 ),
inference(sat_conversion,[],[f4176]) ).
cnf(s2175,plain,
( ~ spl5_19
| ~ spl5_146
| spl5_147 ),
inference(sat_conversion,[],[f4182]) ).
cnf(s2190,plain,
( ~ spl5_16
| ~ spl5_61
| spl5_131
| ~ spl5_145 ),
inference(sat_conversion,[],[f4219]) ).
cnf(s2341,plain,
( ~ spl5_94
| spl5_100 ),
inference(sat_conversion,[],[f4541]) ).
cnf(s2974,plain,
( spl5_61
| spl5_93
| ~ spl5_133
| ~ spl5_147 ),
inference(sat_conversion,[],[f5960]) ).
cnf(s2998,plain,
( spl5_90
| ~ spl5_93
| ~ spl5_100 ),
inference(sat_conversion,[],[f5996]) ).
cnf(s3496,plain,
( ~ spl5_22
| ~ spl5_243
| spl5_244 ),
inference(sat_conversion,[],[f7157]) ).
cnf(s3499,plain,
( spl5_14
| ~ spl5_244
| ~ spl5_245 ),
inference(sat_conversion,[],[f7164]) ).
cnf(s3502,plain,
( ~ spl5_55
| spl5_242
| spl5_245 ),
inference(sat_conversion,[],[f7166]) ).
cnf(s4022,plain,
( ~ spl5_242
| spl5_252 ),
inference(sat_conversion,[],[f8285]) ).
cnf(s4049,plain,
( spl5_251
| spl5_257 ),
inference(sat_conversion,[],[f8467]) ).
cnf(s4068,plain,
( ~ spl5_42
| ~ spl5_242
| ~ spl5_251
| spl5_258 ),
inference(sat_conversion,[],[f8505]) ).
cnf(s4072,plain,
( ~ spl5_19
| ~ spl5_258
| spl5_259 ),
inference(sat_conversion,[],[f8521]) ).
cnf(s4074,plain,
( ~ spl5_252
| spl5_257
| spl5_260 ),
inference(sat_conversion,[],[f8526]) ).
cnf(s4084,plain,
( ~ spl5_260
| spl5_263 ),
inference(sat_conversion,[],[f8553]) ).
cnf(s4090,plain,
( ~ spl5_249
| ~ spl5_263
| spl5_264 ),
inference(sat_conversion,[],[f8567]) ).
cnf(s4094,plain,
( ~ spl5_18
| spl5_245
| ~ spl5_264
| ~ spl5_265 ),
inference(sat_conversion,[],[f8575]) ).
cnf(s4201,plain,
( ~ spl5_27
| spl5_243
| spl5_244
| spl5_270 ),
inference(sat_conversion,[],[f8719]) ).
cnf(s4227,plain,
( ~ spl5_90
| ~ spl5_270
| spl5_273 ),
inference(sat_conversion,[],[f8779]) ).
cnf(s4240,plain,
( ~ spl5_273
| spl5_274 ),
inference(sat_conversion,[],[f8795]) ).
cnf(s4256,plain,
( ~ spl5_9
| ~ spl5_257
| ~ spl5_275 ),
inference(sat_conversion,[],[f8896]) ).
cnf(s4259,plain,
( spl5_275
| spl5_276 ),
inference(sat_conversion,[],[f8903]) ).
cnf(s4329,plain,
( ~ spl5_12
| ~ spl5_274
| spl5_280 ),
inference(sat_conversion,[],[f9147]) ).
cnf(s4367,plain,
( ~ spl5_24
| ~ spl5_280
| spl5_284 ),
inference(sat_conversion,[],[f9262]) ).
cnf(s4376,plain,
( ~ spl5_284
| spl5_285 ),
inference(sat_conversion,[],[f9281]) ).
cnf(s4389,plain,
( ~ spl5_285
| ~ spl5_286
| spl5_287
| ~ spl5_288 ),
inference(sat_conversion,[],[f9311]) ).
cnf(s4392,plain,
( spl5_243
| spl5_286 ),
inference(sat_conversion,[],[f9314]) ).
cnf(s4408,plain,
( ~ spl5_22
| spl5_244
| spl5_288 ),
inference(sat_conversion,[],[f9322]) ).
cnf(s4425,plain,
( ~ spl5_6
| ~ spl5_16
| ~ spl5_25
| spl5_244
| ~ spl5_287 ),
inference(sat_conversion,[],[f9392]) ).
cnf(s4515,plain,
( ~ spl5_6
| ~ spl5_259
| spl5_262 ),
inference(sat_conversion,[],[f9689]) ).
cnf(s4587,plain,
( spl5_14
| ~ spl5_244
| ~ spl5_276 ),
inference(sat_conversion,[],[f9720]) ).
cnf(s4693,plain,
( ~ spl5_34
| ~ spl5_242
| spl5_249
| ~ spl5_251 ),
inference(sat_conversion,[],[f10031]) ).
cnf(s4746,plain,
( ~ spl5_3
| ~ spl5_52
| ~ spl5_242
| ~ spl5_251
| ~ spl5_259
| ~ spl5_260
| ~ spl5_262
| ~ spl5_263
| spl5_308
| ~ spl5_309 ),
inference(sat_conversion,[],[f10183]) ).
cnf(s4748,plain,
( ~ spl5_275
| spl5_309 ),
inference(sat_conversion,[],[f10187]) ).
cnf(s4801,plain,
( ~ spl5_50
| spl5_265
| ~ spl5_308 ),
inference(sat_conversion,[],[f10314]) ).
cnf(s4803,plain,
~ spl5_89,
inference(rat,[],[s746,s178]) ).
cnf(s4805,plain,
spl5_13,
inference(rat,[],[s176,s167]) ).
cnf(s4806,plain,
spl5_12,
inference(rat,[],[s174,s167]) ).
cnf(s4807,plain,
spl5_11,
inference(rat,[],[s172,s167]) ).
cnf(s4808,plain,
spl5_52,
inference(rat,[],[s508,s4805]) ).
cnf(s4809,plain,
spl5_53,
inference(rat,[],[s534,s164]) ).
cnf(s4810,plain,
spl5_21,
inference(rat,[],[s247,s164]) ).
cnf(s4811,plain,
spl5_55,
inference(rat,[],[s543,s4809]) ).
cnf(s4812,plain,
spl5_27,
inference(rat,[],[s275,s4810]) ).
cnf(s4815,plain,
spl5_7,
inference(rat,[],[s157,s154]) ).
cnf(s4822,plain,
spl5_50,
inference(rat,[],[s493,s148]) ).
cnf(s4826,plain,
spl5_19,
inference(rat,[],[s230,s148]) ).
cnf(s4827,plain,
spl5_16,
inference(rat,[],[s190,s4815,s148]) ).
cnf(s4836,plain,
spl5_24,
inference(rat,[],[s264,s144]) ).
cnf(s4837,plain,
spl5_17,
inference(rat,[],[s202,s144]) ).
cnf(s4838,plain,
spl5_15,
inference(rat,[],[s185,s144]) ).
cnf(s4841,plain,
spl5_42,
inference(rat,[],[s433,s4807,s4837]) ).
cnf(s4844,plain,
spl5_34,
inference(rat,[],[s332,s4807,s4838]) ).
cnf(s4846,plain,
spl5_25,
inference(rat,[],[s268,s142]) ).
cnf(s4847,plain,
spl5_22,
inference(rat,[],[s249,s142]) ).
cnf(s4848,plain,
spl5_8,
inference(rat,[],[s162,s142]) ).
cnf(s4853,plain,
spl5_18,
inference(rat,[],[s214,s4848]) ).
cnf(s4857,plain,
( ~ spl5_80
| spl5_85 ),
inference(rat,[],[s703,s721]) ).
cnf(s4858,plain,
~ spl5_131,
inference(rat,[],[s4857,s744,s1764,s1999,s4803]) ).
cnf(s4860,plain,
~ spl5_41,
inference(rat,[],[s1761,s4827,s4858]) ).
cnf(s4861,plain,
spl5_40,
inference(rat,[],[s430,s4826,s4860]) ).
cnf(s4862,plain,
spl5_133,
inference(rat,[],[s1872,s4860,s4861]) ).
cnf(s4864,plain,
spl5_146,
inference(rat,[],[s2171,s4862]) ).
cnf(s4865,plain,
spl5_145,
inference(rat,[],[s2169,s4862]) ).
cnf(s4866,plain,
spl5_147,
inference(rat,[],[s2175,s4826,s4864]) ).
cnf(s4868,plain,
~ spl5_61,
inference(rat,[],[s2190,s4858,s4827,s4865]) ).
cnf(s4869,plain,
spl5_93,
inference(rat,[],[s2974,s4866,s4862,s4868]) ).
cnf(s4874,plain,
spl5_94,
inference(rat,[],[s1200,s4869]) ).
cnf(s4879,plain,
spl5_100,
inference(rat,[],[s2341,s4874]) ).
cnf(s4881,plain,
spl5_90,
inference(rat,[],[s2998,s4869,s4879]) ).
cnf(s4942,plain,
spl5_244,
inference(rat,[],[s4329,s4367,s4240,s4376,s4227,s4389,s4201,s4392,s3496,s4425,s4408,s4806,s4836,s4881,s4812,s4847,s154,s4827,s4846]) ).
cnf(s4943,plain,
~ spl5_276,
inference(rat,[],[s4587,s178,s4942]) ).
cnf(s4944,plain,
~ spl5_245,
inference(rat,[],[s3499,s178,s4942]) ).
cnf(s4945,plain,
spl5_275,
inference(rat,[],[s4259,s4943]) ).
cnf(s4946,plain,
spl5_242,
inference(rat,[],[s3502,s4811,s4944]) ).
cnf(s4947,plain,
spl5_309,
inference(rat,[],[s4748,s4945]) ).
cnf(s4948,plain,
~ spl5_257,
inference(rat,[],[s4256,s164,s4945]) ).
cnf(s4950,plain,
spl5_252,
inference(rat,[],[s4022,s4946]) ).
cnf(s4951,plain,
spl5_251,
inference(rat,[],[s4049,s4948]) ).
cnf(s4952,plain,
spl5_260,
inference(rat,[],[s4074,s4948,s4950]) ).
cnf(s4954,plain,
spl5_258,
inference(rat,[],[s4068,s4946,s4841,s4951]) ).
cnf(s4955,plain,
spl5_249,
inference(rat,[],[s4693,s4946,s4844,s4951]) ).
cnf(s4956,plain,
spl5_263,
inference(rat,[],[s4084,s4952]) ).
cnf(s4957,plain,
spl5_259,
inference(rat,[],[s4072,s4826,s4954]) ).
cnf(s4958,plain,
spl5_264,
inference(rat,[],[s4090,s4955,s4956]) ).
cnf(s4959,plain,
spl5_262,
inference(rat,[],[s4515,s154,s4957]) ).
cnf(s4963,plain,
~ spl5_265,
inference(rat,[],[s4094,s4944,s4853,s4958]) ).
cnf(s4964,plain,
spl5_308,
inference(rat,[],[s4746,s4947,s4957,s4956,s4951,s4952,s4946,s148,s4808,s4959]) ).
cnf(s4966,plain,
$false,
inference(rat,[],[s4801,s4822,s4964,s4963]) ).
fof(f10315,plain,
$false,
inference(avatar_sat_refutation,[],[s4966]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM062-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Sun Sep 27 18:46:19 UTC 2026
% 0.05/0.31 % CPUTime :
% 0.05/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.54/2.48 % (2662118)Input is clausal, will run a generic CNF schedule.
% 12.54/2.48 % (2662163)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2514906176:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.54/2.48 % (2662164)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1845741170:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.54/2.48 % (2662166)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2549109227:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.54/2.48 % (2662162)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=948825132:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.54/2.48 % (2662165)lrs+10_1_sil=8000:sp=occurrence:random_seed=2495914238:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.54/2.48 % (2662168)dis-21_1_sil=8000:lcm=predicate:random_seed=1423877639: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)
% 12.54/2.48 % (2662165)Instruction limit reached!
% 12.54/2.48 % (2662165)------------------------------
% 12.54/2.48 % (2662165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.48 % (2662165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.48 % (2662165)CaDiCaL version: 2.1.3
% 12.54/2.48 % (2662165)Termination reason: Instruction limit
% 12.54/2.48 % (2662165)Termination phase: Saturation
% 12.54/2.48 % (2662165)Time elapsed: 0.051 s
% 12.54/2.48 % (2662165)Peak memory usage: 89 MB
% 12.54/2.48 % (2662165)Instructions burned: 110 (million)
% 12.54/2.48 % (2662167)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3873304666:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.54/2.48 % (2662166)Instruction limit reached!
% 12.54/2.48 % (2662166)------------------------------
% 12.54/2.48 % (2662166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.48 % (2662166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.48 % (2662166)CaDiCaL version: 2.1.3
% 12.54/2.48 % (2662166)Termination reason: Instruction limit
% 12.54/2.48 % (2662166)Termination phase: Saturation
% 12.54/2.48 % (2662166)Time elapsed: 0.061 s
% 12.54/2.48 % (2662166)Peak memory usage: 89 MB
% 12.54/2.48 % (2662166)Instructions burned: 115 (million)
% 12.54/2.48 % (2662168)Instruction limit reached!
% 12.54/2.48 % (2662168)------------------------------
% 12.54/2.48 % (2662168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.48 % (2662168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.48 % (2662168)CaDiCaL version: 2.1.3
% 12.54/2.48 % (2662168)Termination reason: Instruction limit
% 12.54/2.48 % (2662168)Termination phase: Saturation
% 12.54/2.48 % (2662168)Time elapsed: 0.052 s
% 12.54/2.48 % (2662168)Peak memory usage: 89 MB
% 12.54/2.48 % (2662168)Instructions burned: 118 (million)
% 12.54/2.48 % (2662167)Instruction limit reached!
% 12.54/2.48 % (2662167)------------------------------
% 12.54/2.48 % (2662167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.48 % (2662167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.48 % (2662167)CaDiCaL version: 2.1.3
% 12.54/2.48 % (2662167)Termination reason: Instruction limit
% 12.54/2.48 % (2662167)Termination phase: Saturation
% 12.54/2.48 % (2662167)Time elapsed: 0.076 s
% 12.54/2.48 % (2662167)Peak memory usage: 90 MB
% 12.54/2.48 % (2662167)Instructions burned: 181 (million)
% 12.54/2.48 % (2662182)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=2020540935:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.54/2.48 % (2662182)Refutation not found, incomplete strategy
% 12.54/2.48 % (2662182)------------------------------
% 12.54/2.48 % (2662182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.54/2.48 % (2662182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.54/2.48 % (2662182)CaDiCaL version: 2.1.3
% 12.54/2.48 % (2662182)Termination reason: Refutation not found, incomplete strategy
% 12.54/2.48 % (2662182)Time elapsed: 0.003 s
% 12.54/2.48 % (2662182)Peak memory usage: 88 MB
% 12.54/2.48 % (2662182)Instructions burned: 4 (million)
% 12.54/2.48 % (2662183)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=555770803: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)
% 20.04/3.57 % (2662184)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3025805461:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.04/3.57 % (2662184)Refutation not found, incomplete strategy
% 20.04/3.57 % (2662184)------------------------------
% 20.04/3.57 % (2662184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/3.57 % (2662184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.57 % (2662184)CaDiCaL version: 2.1.3
% 20.04/3.57 % (2662184)Termination reason: Refutation not found, incomplete strategy
% 20.04/3.57 % (2662184)Time elapsed: 0.002 s
% 20.04/3.57 % (2662184)Peak memory usage: 88 MB
% 20.04/3.57 % (2662184)Instructions burned: 4 (million)
% 20.04/3.57 % (2662185)lrs+10_64_to=lpo:sil=8000:random_seed=626381205:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 20.04/3.57 % (2662183)Instruction limit reached!
% 20.04/3.57 % (2662183)------------------------------
% 20.04/3.57 % (2662183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/3.57 % (2662183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.57 % (2662183)CaDiCaL version: 2.1.3
% 20.04/3.57 % (2662183)Termination reason: Instruction limit
% 20.04/3.57 % (2662183)Termination phase: Saturation
% 20.04/3.57 % (2662183)Time elapsed: 0.099 s
% 20.04/3.57 % (2662183)Peak memory usage: 91 MB
% 20.04/3.57 % (2662183)Instructions burned: 190 (million)
% 20.04/3.57 % (2662185)Instruction limit reached!
% 20.04/3.57 % (2662185)------------------------------
% 20.04/3.57 % (2662185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/3.57 % (2662185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.57 % (2662185)CaDiCaL version: 2.1.3
% 20.04/3.57 % (2662185)Termination reason: Instruction limit
% 20.04/3.57 % (2662185)Termination phase: Saturation
% 20.04/3.57 % (2662185)Time elapsed: 0.074 s
% 20.04/3.57 % (2662185)Peak memory usage: 89 MB
% 20.04/3.57 % (2662185)Instructions burned: 127 (million)
% 20.04/3.57 % (2662182)------------------------------
% 20.04/3.57 % (2662182)------------------------------
% 20.04/3.57 % (2662184)------------------------------
% 20.04/3.57 % (2662184)------------------------------
% 20.04/3.57 % (2662194)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=919135494:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.04/3.57 % (2662195)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=650848181:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.04/3.57 % (2662194)Instruction limit reached!
% 20.04/3.57 % (2662194)------------------------------
% 20.04/3.57 % (2662194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/3.57 % (2662194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.57 % (2662194)CaDiCaL version: 2.1.3
% 20.04/3.57 % (2662194)Termination reason: Instruction limit
% 20.04/3.57 % (2662194)Termination phase: Saturation
% 20.04/3.57 % (2662194)Time elapsed: 0.105 s
% 20.04/3.57 % (2662194)Peak memory usage: 90 MB
% 20.04/3.57 % (2662194)Instructions burned: 194 (million)
% 20.04/3.57 % (2662195)Instruction limit reached!
% 20.04/3.57 % (2662195)------------------------------
% 20.04/3.57 % (2662195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.04/3.57 % (2662195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.04/3.57 % (2662195)CaDiCaL version: 2.1.3
% 20.04/3.57 % (2662195)Termination reason: Instruction limit
% 20.04/3.57 % (2662195)Termination phase: Saturation
% 20.04/3.57 % (2662195)Time elapsed: 0.088 s
% 20.04/3.57 % (2662195)Peak memory usage: 91 MB
% 20.04/3.57 % (2662195)Instructions burned: 158 (million)
% 20.04/3.57 % (2662198)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=650520613:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.04/3.57 % (2662199)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=3093721820:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 20.04/3.57 % (2662199)Instruction limit reached!
% 20.04/3.57 % (2662199)------------------------------
% 20.04/3.57 % (2662199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662199)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662199)Termination reason: Instruction limit
% 32.83/5.39 % (2662199)Termination phase: Saturation
% 32.83/5.39 % (2662199)Time elapsed: 0.051 s
% 32.83/5.39 % (2662199)Peak memory usage: 89 MB
% 32.83/5.39 % (2662199)Instructions burned: 107 (million)
% 32.83/5.39 % (2662206)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=857384118:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 32.83/5.39 % (2662207)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1037901078:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 32.83/5.39 % (2662206)Instruction limit reached!
% 32.83/5.39 % (2662206)------------------------------
% 32.83/5.39 % (2662206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662206)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662206)Termination reason: Instruction limit
% 32.83/5.39 % (2662206)Termination phase: Saturation
% 32.83/5.39 % (2662206)Time elapsed: 0.061 s
% 32.83/5.39 % (2662206)Peak memory usage: 89 MB
% 32.83/5.39 % (2662206)Instructions burned: 109 (million)
% 32.83/5.39 % (2662210)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3998207291:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 32.83/5.39 % (2662207)Instruction limit reached!
% 32.83/5.39 % (2662207)------------------------------
% 32.83/5.39 % (2662207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662207)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662207)Termination reason: Instruction limit
% 32.83/5.39 % (2662207)Termination phase: Saturation
% 32.83/5.39 % (2662207)Time elapsed: 0.145 s
% 32.83/5.39 % (2662207)Peak memory usage: 90 MB
% 32.83/5.39 % (2662207)Instructions burned: 242 (million)
% 32.83/5.39 % (2662215)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=307350499:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 32.83/5.39 % (2662217)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=393409216:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 32.83/5.39 % (2662215)Instruction limit reached!
% 32.83/5.39 % (2662215)------------------------------
% 32.83/5.39 % (2662215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662215)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662215)Termination reason: Instruction limit
% 32.83/5.39 % (2662215)Termination phase: Saturation
% 32.83/5.39 % (2662215)Time elapsed: 0.076 s
% 32.83/5.39 % (2662215)Peak memory usage: 89 MB
% 32.83/5.39 % (2662215)Instructions burned: 135 (million)
% 32.83/5.39 % (2662220)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1493112033:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 32.83/5.39 % (2662217)Instruction limit reached!
% 32.83/5.39 % (2662217)------------------------------
% 32.83/5.39 % (2662217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662217)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662217)Termination reason: Instruction limit
% 32.83/5.39 % (2662217)Termination phase: Saturation
% 32.83/5.39 % (2662217)Time elapsed: 0.285 s
% 32.83/5.39 % (2662217)Peak memory usage: 96 MB
% 32.83/5.39 % (2662217)Instructions burned: 499 (million)
% 32.83/5.39 % (2662220)Instruction limit reached!
% 32.83/5.39 % (2662220)------------------------------
% 32.83/5.39 % (2662220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.83/5.39 % (2662220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.83/5.39 % (2662220)CaDiCaL version: 2.1.3
% 32.83/5.39 % (2662220)Termination reason: Instruction limit
% 32.83/5.39 % (2662220)Termination phase: Saturation
% 32.83/5.39 % (2662220)Time elapsed: 0.100 s
% 32.83/5.39 % (2662220)Peak memory usage: 89 MB
% 32.83/5.39 % (2662220)Instructions burned: 191 (million)
% 32.83/5.39 % (2662222)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=573881066:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 50.61/7.95 % (2662224)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2539768121:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 50.61/7.95 % (2662222)Instruction limit reached!
% 50.61/7.95 % (2662222)------------------------------
% 50.61/7.95 % (2662222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.61/7.95 % (2662222)CaDiCaL version: 2.1.3
% 50.61/7.95 % (2662222)Termination reason: Instruction limit
% 50.61/7.95 % (2662222)Termination phase: Saturation
% 50.61/7.95 % (2662222)Time elapsed: 0.155 s
% 50.61/7.95 % (2662222)Peak memory usage: 92 MB
% 50.61/7.95 % (2662222)Instructions burned: 264 (million)
% 50.61/7.95 % (2662224)Instruction limit reached!
% 50.61/7.95 % (2662224)------------------------------
% 50.61/7.95 % (2662224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.61/7.95 % (2662224)CaDiCaL version: 2.1.3
% 50.61/7.95 % (2662224)Termination reason: Instruction limit
% 50.61/7.95 % (2662224)Termination phase: Saturation
% 50.61/7.95 % (2662224)Time elapsed: 0.092 s
% 50.61/7.95 % (2662224)Peak memory usage: 89 MB
% 50.61/7.95 % (2662224)Instructions burned: 157 (million)
% 50.61/7.95 % (2662231)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2703002571:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 50.61/7.95 % (2662230)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=474629776:i=3256:kws=precedence:bd=preordered:av=off_2979 on theBenchmark for (2979ds/3256Mi)
% 50.61/7.95 % (2662231)Instruction limit reached!
% 50.61/7.95 % (2662231)------------------------------
% 50.61/7.95 % (2662231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.61/7.95 % (2662231)CaDiCaL version: 2.1.3
% 50.61/7.95 % (2662231)Termination reason: Instruction limit
% 50.61/7.95 % (2662231)Termination phase: Saturation
% 50.61/7.95 % (2662231)Time elapsed: 0.222 s
% 50.61/7.95 % (2662231)Peak memory usage: 89 MB
% 50.61/7.95 % (2662231)Instructions burned: 539 (million)
% 50.61/7.95 % (2662234)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2319190319:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 50.61/7.95 % (2662198)Instruction limit reached!
% 50.61/7.95 % (2662198)------------------------------
% 50.61/7.95 % (2662198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.61/7.95 % (2662198)CaDiCaL version: 2.1.3
% 50.61/7.95 % (2662198)Termination reason: Instruction limit
% 50.61/7.95 % (2662198)Termination phase: Saturation
% 50.61/7.95 % (2662198)Time elapsed: 1.764 s
% 50.61/7.95 % (2662198)Peak memory usage: 143 MB
% 50.61/7.95 % (2662198)Instructions burned: 3395 (million)
% 50.61/7.95 % (2662234)Instruction limit reached!
% 50.61/7.95 % (2662234)------------------------------
% 50.61/7.95 % (2662234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.61/7.95 % (2662234)CaDiCaL version: 2.1.3
% 50.61/7.95 % (2662234)Termination reason: Instruction limit
% 50.61/7.95 % (2662234)Termination phase: Saturation
% 50.61/7.95 % (2662234)Time elapsed: 0.059 s
% 50.61/7.95 % (2662234)Peak memory usage: 90 MB
% 50.61/7.95 % (2662234)Instructions burned: 182 (million)
% 50.61/7.95 % (2662239)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=2006414112:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 50.61/7.95 % (2662238)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=1813286109:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2973 on theBenchmark for (2973ds/10307Mi)
% 50.61/7.95 % (2662239)Instruction limit reached!
% 50.61/7.95 % (2662239)------------------------------
% 50.61/7.95 % (2662239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.61/7.95 % (2662239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662239)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662239)Termination reason: Instruction limit
% 71.62/10.80 % (2662239)Termination phase: Saturation
% 71.62/10.80 % (2662239)Time elapsed: 0.137 s
% 71.62/10.80 % (2662239)Peak memory usage: 90 MB
% 71.62/10.80 % (2662239)Instructions burned: 414 (million)
% 71.62/10.80 % (2662242)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=3902020171:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 71.62/10.80 % (2662210)Instruction limit reached!
% 71.62/10.80 % (2662210)------------------------------
% 71.62/10.80 % (2662210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.62/10.80 % (2662210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662210)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662210)Termination reason: Instruction limit
% 71.62/10.80 % (2662210)Termination phase: Saturation
% 71.62/10.80 % (2662210)Time elapsed: 2.520 s
% 71.62/10.80 % (2662210)Peak memory usage: 160 MB
% 71.62/10.80 % (2662210)Instructions burned: 5210 (million)
% 71.62/10.80 % (2662248)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=2601237055:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2963 on theBenchmark for (2963ds/303Mi)
% 71.62/10.80 % (2662248)Instruction limit reached!
% 71.62/10.80 % (2662248)------------------------------
% 71.62/10.80 % (2662248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.62/10.80 % (2662248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662248)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662248)Termination reason: Instruction limit
% 71.62/10.80 % (2662248)Termination phase: Saturation
% 71.62/10.80 % (2662248)Time elapsed: 0.087 s
% 71.62/10.80 % (2662248)Peak memory usage: 93 MB
% 71.62/10.80 % (2662248)Instructions burned: 303 (million)
% 71.62/10.80 % (2662230)Instruction limit reached!
% 71.62/10.80 % (2662230)------------------------------
% 71.62/10.80 % (2662230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.62/10.80 % (2662230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662230)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662230)Termination reason: Instruction limit
% 71.62/10.80 % (2662230)Termination phase: Saturation
% 71.62/10.80 % (2662230)Time elapsed: 1.769 s
% 71.62/10.80 % (2662230)Peak memory usage: 150 MB
% 71.62/10.80 % (2662230)Instructions burned: 3258 (million)
% 71.62/10.80 % (2662250)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=187507183:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 71.62/10.80 % (2662253)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3111334798:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 71.62/10.80 % (2662250)Instruction limit reached!
% 71.62/10.80 % (2662250)------------------------------
% 71.62/10.80 % (2662250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.62/10.80 % (2662250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662250)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662250)Termination reason: Instruction limit
% 71.62/10.80 % (2662250)Termination phase: Saturation
% 71.62/10.80 % (2662250)Time elapsed: 0.375 s
% 71.62/10.80 % (2662250)Peak memory usage: 98 MB
% 71.62/10.80 % (2662250)Instructions burned: 722 (million)
% 71.62/10.80 % (2662253)Instruction limit reached!
% 71.62/10.80 % (2662253)------------------------------
% 71.62/10.80 % (2662253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.62/10.80 % (2662253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.62/10.80 % (2662253)CaDiCaL version: 2.1.3
% 71.62/10.80 % (2662253)Termination reason: Instruction limit
% 71.62/10.80 % (2662253)Termination phase: Saturation
% 71.62/10.80 % (2662253)Time elapsed: 0.325 s
% 71.62/10.80 % (2662253)Peak memory usage: 92 MB
% 71.62/10.80 % (2662253)Instructions burned: 598 (million)
% 71.62/10.80 % (2662256)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=687954078:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi)
% 71.62/10.80 % (2662257)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=3078526650:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi)
% 57.68/13.02 % (2662257)Instruction limit reached!
% 57.68/13.02 % (2662257)------------------------------
% 57.68/13.02 % (2662257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662257)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662257)Termination reason: Instruction limit
% 57.68/13.02 % (2662257)Termination phase: Saturation
% 57.68/13.02 % (2662257)Time elapsed: 1.189 s
% 57.68/13.02 % (2662257)Peak memory usage: 138 MB
% 57.68/13.02 % (2662257)Instructions burned: 1998 (million)
% 57.68/13.02 % (2662256)Instruction limit reached!
% 57.68/13.02 % (2662256)------------------------------
% 57.68/13.02 % (2662256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662256)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662256)Termination reason: Instruction limit
% 57.68/13.02 % (2662256)Termination phase: Saturation
% 57.68/13.02 % (2662256)Time elapsed: 1.414 s
% 57.68/13.02 % (2662256)Peak memory usage: 142 MB
% 57.68/13.02 % (2662256)Instructions burned: 2989 (million)
% 57.68/13.02 % (2662264)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=3590648509:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi)
% 57.68/13.02 % (2662265)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2248693159:i=1098:nicw=on_2939 on theBenchmark for (2939ds/1098Mi)
% 57.68/13.02 % (2662242)Instruction limit reached!
% 57.68/13.02 % (2662242)------------------------------
% 57.68/13.02 % (2662242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662242)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662242)Termination reason: Instruction limit
% 57.68/13.02 % (2662242)Termination phase: Saturation
% 57.68/13.02 % (2662242)Time elapsed: 3.731 s
% 57.68/13.02 % (2662242)Peak memory usage: 178 MB
% 57.68/13.02 % (2662242)Instructions burned: 8479 (million)
% 57.68/13.02 % (2662265)Instruction limit reached!
% 57.68/13.02 % (2662265)------------------------------
% 57.68/13.02 % (2662265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662265)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662265)Termination reason: Instruction limit
% 57.68/13.02 % (2662265)Termination phase: Saturation
% 57.68/13.02 % (2662265)Time elapsed: 0.589 s
% 57.68/13.02 % (2662265)Peak memory usage: 103 MB
% 57.68/13.02 % (2662265)Instructions burned: 1099 (million)
% 57.68/13.02 % (2662268)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3198911523:i=433:bd=preordered_2931 on theBenchmark for (2931ds/433Mi)
% 57.68/13.02 % (2662268)Refutation not found, incomplete strategy
% 57.68/13.02 % (2662268)------------------------------
% 57.68/13.02 % (2662268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662268)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662268)Termination reason: Refutation not found, incomplete strategy
% 57.68/13.02 % (2662268)Time elapsed: 0.012 s
% 57.68/13.02 % (2662268)Peak memory usage: 89 MB
% 57.68/13.02 % (2662268)Instructions burned: 22 (million)
% 57.68/13.02 % (2662270)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2477708809:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2930 on theBenchmark for (2930ds/2942Mi)
% 57.68/13.02 % (2662264)Instruction limit reached!
% 57.68/13.02 % (2662264)------------------------------
% 57.68/13.02 % (2662264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662264)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662264)Termination reason: Instruction limit
% 57.68/13.02 % (2662264)Termination phase: Saturation
% 57.68/13.02 % (2662264)Time elapsed: 1.089 s
% 57.68/13.02 % (2662264)Peak memory usage: 137 MB
% 57.68/13.02 % (2662264)Instructions burned: 2089 (million)
% 57.68/13.02 % (2662268)------------------------------
% 57.68/13.02 % (2662268)------------------------------
% 57.68/13.02 % (2662274)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1077225750:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2927 on theBenchmark for (2927ds/6922Mi)
% 57.68/13.02 % (2662275)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=3374348490:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2926 on theBenchmark for (2926ds/596Mi)
% 57.68/13.02 % (2662275)Instruction limit reached!
% 57.68/13.02 % (2662275)------------------------------
% 57.68/13.02 % (2662275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662275)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662275)Termination reason: Instruction limit
% 57.68/13.02 % (2662275)Termination phase: Saturation
% 57.68/13.02 % (2662275)Time elapsed: 0.279 s
% 57.68/13.02 % (2662275)Peak memory usage: 99 MB
% 57.68/13.02 % (2662275)Instructions burned: 597 (million)
% 57.68/13.02 % (2662280)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=3558105692:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2921 on theBenchmark for (2921ds/4123Mi)
% 57.68/13.02 % (2662270)Instruction limit reached!
% 57.68/13.02 % (2662270)------------------------------
% 57.68/13.02 % (2662270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662270)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662270)Termination reason: Instruction limit
% 57.68/13.02 % (2662270)Termination phase: Saturation
% 57.68/13.02 % (2662270)Time elapsed: 1.714 s
% 57.68/13.02 % (2662270)Peak memory usage: 146 MB
% 57.68/13.02 % (2662270)Instructions burned: 2943 (million)
% 57.68/13.02 % (2662238)Instruction limit reached!
% 57.68/13.02 % (2662238)------------------------------
% 57.68/13.02 % (2662238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662238)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662238)Termination reason: Instruction limit
% 57.68/13.02 % (2662238)Termination phase: Saturation
% 57.68/13.02 % (2662238)Time elapsed: 6.113 s
% 57.68/13.02 % (2662238)Peak memory usage: 175 MB
% 57.68/13.02 % (2662238)Instructions burned: 10307 (million)
% 57.68/13.02 % (2662283)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1622272690:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2911 on theBenchmark for (2911ds/16411Mi)
% 57.68/13.02 % (2662285)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=519169563:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2910 on theBenchmark for (2910ds/1670Mi)
% 57.68/13.02 % (2662280)Instruction limit reached!
% 57.68/13.02 % (2662280)------------------------------
% 57.68/13.02 % (2662280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662280)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662280)Termination reason: Instruction limit
% 57.68/13.02 % (2662280)Termination phase: Saturation
% 57.68/13.02 % (2662280)Time elapsed: 1.901 s
% 57.68/13.02 % (2662280)Peak memory usage: 165 MB
% 57.68/13.02 % (2662280)Instructions burned: 4124 (million)
% 57.68/13.02 % (2662285)Instruction limit reached!
% 57.68/13.02 % (2662285)------------------------------
% 57.68/13.02 % (2662285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662285)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662285)Termination reason: Instruction limit
% 57.68/13.02 % (2662285)Termination phase: Saturation
% 57.68/13.02 % (2662285)Time elapsed: 0.879 s
% 57.68/13.02 % (2662285)Peak memory usage: 136 MB
% 57.68/13.02 % (2662285)Instructions burned: 1670 (million)
% 57.68/13.02 % (2662291)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=1751113912:cts=off:cond=on:i=9530:bs=on:fsd=on_2899 on theBenchmark for (2899ds/9530Mi)
% 57.68/13.02 % (2662290)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=3143837368:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2899 on theBenchmark for (2899ds/1722Mi)
% 57.68/13.02 % (2662274)Instruction limit reached!
% 57.68/13.02 % (2662274)------------------------------
% 57.68/13.02 % (2662274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662274)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662274)Termination reason: Instruction limit
% 57.68/13.02 % (2662274)Termination phase: Saturation
% 57.68/13.02 % (2662274)Time elapsed: 3.635 s
% 57.68/13.02 % (2662274)Peak memory usage: 184 MB
% 57.68/13.02 % (2662274)Instructions burned: 6923 (million)
% 57.68/13.02 % (2662290)Instruction limit reached!
% 57.68/13.02 % (2662290)------------------------------
% 57.68/13.02 % (2662290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.68/13.02 % (2662290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.68/13.02 % (2662290)CaDiCaL version: 2.1.3
% 57.68/13.02 % (2662290)Termination reason: Instruction limit
% 57.68/13.02 % (2662290)Termination phase: Saturation
% 57.68/13.02 % (2662290)Time elapsed: 0.964 s
% 57.68/13.02 % (2662290)Peak memory usage: 134 MB
% 57.68/13.02 % (2662290)Instructions burned: 1724 (million)
% 57.68/13.02 % (2662294)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4252974898:st=2:i=4495:sd=10:ss=included_2889 on theBenchmark for (2889ds/4495Mi)
% 57.68/13.02 % (2662295)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=2646717919:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2888 on theBenchmark for (2888ds/4920Mi)
% 57.68/13.02 % (2662291)First to succeed.
% 57.68/13.02 % (2662291)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2662118"
% 57.68/13.02 % (2662291)Refutation found. Thanks to Tanya!
% 57.68/13.02 % SZS status Unsatisfiable for theBenchmark
% 57.68/13.02 % SZS output start Proof for theBenchmark
% See solution above
% 0.07/13.21 % (2662291)------------------------------
% 0.07/13.21 % (2662291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.07/13.21 % (2662291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/13.21 % (2662291)CaDiCaL version: 2.1.3
% 0.07/13.21 % (2662291)Termination reason: Refutation
% 0.07/13.21 % (2662291)Time elapsed: 1.921 s
% 0.07/13.21 % (2662291)Peak memory usage: 142 MB
% 0.07/13.21 % (2662291)Instructions burned: 3057 (million)
% 0.07/13.21 % (2662291)------------------------------
% 0.07/13.21 % (2662291)------------------------------
% 0.07/13.21 % (2662118)Success in time 12.416 s
% 0.07/13.21 % Vampire exiting
%------------------------------------------------------------------------------