%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET274-6 : 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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:40 PM UTC 2026
% Result : Unsatisfiable 39.22s 11.14s
% Output : Refutation 73.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 87
% Syntax : Number of formulae : 449 ( 77 unt; 66 def)
% Number of atoms : 1159 ( 149 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1293 ( 583 ~; 649 |; 0 &)
% ( 61 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 65 ( 63 usr; 62 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-3 aty)
% Number of variables : 254 ( 0 sgn 254 !; 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(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(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(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(f122,negated_conjecture,
domain_of(restrict(x,y,universal_class)) != intersection(domain_of(x),y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_domain_property4_1) ).
fof(f127,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(f136,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,f127]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f127]) ).
fof(f138,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,f127]) ).
fof(f139,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,f127]) ).
fof(f143,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(f144,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(f185,plain,
intersection(domain_of(x),y) != domain_of(intersection(x,cross_product(y,universal_class))),
inference(definition_unfolding,[],[f122,f28]) ).
fof(f190,definition,
sF0 = domain_of(x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
domain_of(x) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = intersection(sF0,y),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
intersection(sF0,y) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF2 = cross_product(y,universal_class),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f195,plain,
cross_product(y,universal_class) = sF2,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF3 = intersection(x,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f197,plain,
intersection(x,sF2) = sF3,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF4 = domain_of(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f199,plain,
domain_of(sF3) = sF4,
inference(reorient_equations,[],[f198]) ).
fof(f200,plain,
sF1 != sF4,
inference(definition_folding,[],[f185,f199,f197,f195,f193,f191]) ).
fof(f202,definition,
( spl5_1
<=> intersection(sF0,y) = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f204,plain,
( intersection(sF0,y) = sF1
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,plain,
spl5_1,
inference(avatar_split_clause,[],[f193,f202]) ).
fof(f207,definition,
( spl5_2
<=> cross_product(y,universal_class) = sF2 ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f209,plain,
( cross_product(y,universal_class) = sF2
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
spl5_2,
inference(avatar_split_clause,[],[f195,f207]) ).
fof(f212,definition,
( spl5_3
<=> domain_of(x) = sF0 ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
fof(f214,plain,
( domain_of(x) = sF0
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,plain,
spl5_3,
inference(avatar_split_clause,[],[f191,f212]) ).
fof(f217,definition,
( spl5_4
<=> intersection(x,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
fof(f219,plain,
( intersection(x,sF2) = sF3
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f220,plain,
spl5_4,
inference(avatar_split_clause,[],[f197,f217]) ).
fof(f221,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) )
| ~ spl5_4 ),
inference(superposition,[],[f22,f219]) ).
fof(f222,plain,
( ! [X0] :
( ~ member(X0,sF3)
| member(X0,x) )
| ~ spl5_4 ),
inference(superposition,[],[f21,f219]) ).
fof(f224,definition,
( spl5_5
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
fof(f225,plain,
( ! [X0] :
( member(X0,sF2)
| ~ member(X0,sF3) )
| ~ spl5_5 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( spl5_5
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f221,f217,f224]) ).
fof(f227,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X1) ),
inference(resolution,[],[f2,f22]) ).
fof(f228,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),X2)
| member(not_subclass_element(intersection(X0,X1),X2),X0) ),
inference(resolution,[],[f2,f21]) ).
fof(f232,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,x) )
| ~ spl5_4 ),
inference(superposition,[],[f23,f219]) ).
fof(f234,definition,
( spl5_6
<=> ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).
fof(f235,plain,
( ! [X0] :
( member(X0,sF3)
| ~ member(X0,sF2)
| ~ member(X0,x) )
| ~ spl5_6 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f236,plain,
( spl5_6
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f232,f217,f234]) ).
fof(f237,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,y)
| ~ member(X0,sF0) )
| ~ spl5_1 ),
inference(superposition,[],[f23,f204]) ).
fof(f239,plain,
( ! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) )
| ~ spl5_1 ),
inference(superposition,[],[f21,f204]) ).
fof(f241,definition,
( spl5_7
<=> ! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition]) ).
fof(f242,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,sF1) )
| ~ spl5_7 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f243,plain,
( spl5_7
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f239,f202,f241]) ).
fof(f245,definition,
( spl5_8
<=> ! [X0] :
( member(X0,sF1)
| ~ member(X0,y)
| ~ member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition]) ).
fof(f246,plain,
( ! [X0] :
( member(X0,sF1)
| ~ member(X0,y)
| ~ member(X0,sF0) )
| ~ spl5_8 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f247,plain,
( spl5_8
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f237,f202,f245]) ).
fof(f253,definition,
( spl5_10
<=> domain_of(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition]) ).
fof(f255,plain,
( domain_of(sF3) = sF4
| ~ spl5_10 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,plain,
spl5_10,
inference(avatar_split_clause,[],[f199,f253]) ).
fof(f258,definition,
( spl5_11
<=> ! [X0] :
( ~ member(X0,sF3)
| member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition]) ).
fof(f259,plain,
( ! [X0] :
( member(X0,x)
| ~ member(X0,sF3) )
| ~ spl5_11 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f260,plain,
( spl5_11
| ~ spl5_4 ),
inference(avatar_split_clause,[],[f222,f217,f258]) ).
fof(f267,plain,
( ! [X0] :
( subclass(X0,sF1)
| ~ member(not_subclass_element(X0,sF1),y)
| ~ member(not_subclass_element(X0,sF1),sF0) )
| ~ spl5_8 ),
inference(resolution,[],[f3,f246]) ).
fof(f272,definition,
( spl5_12
<=> ! [X0] :
( subclass(X0,sF1)
| ~ member(not_subclass_element(X0,sF1),y)
| ~ member(not_subclass_element(X0,sF1),sF0) ) ),
introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition]) ).
fof(f273,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF1),sF0)
| ~ member(not_subclass_element(X0,sF1),y)
| subclass(X0,sF1) )
| ~ spl5_12 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f274,plain,
( spl5_12
| ~ spl5_8 ),
inference(avatar_split_clause,[],[f267,f245,f272]) ).
fof(f283,definition,
( spl5_13
<=> sF1 = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition]) ).
fof(f285,plain,
( sF1 != sF4
| spl5_13 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
~ spl5_13,
inference(avatar_split_clause,[],[f200,f283]) ).
fof(f299,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,universal_class) )
| ~ spl5_2 ),
inference(superposition,[],[f137,f209]) ).
fof(f301,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,[],[f144,f1]) ).
fof(f302,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,[],[f301,f4]) ).
fof(f304,plain,
( ! [X0,X1] :
( member(X0,sF0)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_3 ),
inference(superposition,[],[f302,f214]) ).
fof(f305,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_10 ),
inference(superposition,[],[f302,f255]) ).
fof(f307,definition,
( spl5_15
<=> ! [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_15])],[avatar_definition]) ).
fof(f308,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(sF3,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_15 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f309,plain,
( spl5_15
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f305,f253,f307]) ).
fof(f311,definition,
( spl5_16
<=> ! [X0,X1] :
( member(X0,sF0)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition]) ).
fof(f312,plain,
( ! [X0,X1] :
( member(X0,sF0)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl5_16 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f313,plain,
( spl5_16
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f304,f212,f311]) ).
fof(f314,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_15 ),
inference(resolution,[],[f308,f3]) ).
fof(f315,plain,
( ! [X0,X1] :
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ member(not_subclass_element(X0,sF1),X1)
| ~ member(not_subclass_element(X0,sF1),y)
| subclass(X0,sF1) )
| ~ spl5_12
| ~ spl5_16 ),
inference(resolution,[],[f312,f273]) ).
fof(f317,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF1),y)
| null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| subclass(X0,sF1) )
| ~ spl5_12
| ~ spl5_16 ),
inference(condensation,[],[f315]) ).
fof(f319,definition,
( spl5_17
<=> ! [X0] :
( ~ member(not_subclass_element(X0,sF1),y)
| null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| subclass(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition]) ).
fof(f320,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF1),y)
| null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| subclass(X0,sF1) )
| ~ spl5_17 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f321,plain,
( spl5_17
| ~ spl5_12
| ~ spl5_16 ),
inference(avatar_split_clause,[],[f317,f311,f272,f319]) ).
fof(f326,plain,
! [X2,X0,X1] :
( ~ subclass(X2,intersection(X0,X1))
| member(not_subclass_element(intersection(X0,X1),X2),X0)
| intersection(X0,X1) = X2 ),
inference(resolution,[],[f228,f7]) ).
fof(f338,definition,
( spl5_19
<=> ! [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_19])],[avatar_definition]) ).
fof(f339,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_19 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f340,plain,
( spl5_19
| ~ spl5_15 ),
inference(avatar_split_clause,[],[f314,f307,f338]) ).
fof(f341,plain,
( ! [X0,X1] :
( ~ 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))
| ~ subclass(sF4,X0)
| sF4 = X0 )
| ~ spl5_19 ),
inference(resolution,[],[f339,f7]) ).
fof(f342,plain,
! [X2,X0,X1] :
( ~ subclass(X2,intersection(X0,X1))
| member(not_subclass_element(intersection(X0,X1),X2),X1)
| intersection(X0,X1) = X2 ),
inference(resolution,[],[f227,f7]) ).
fof(f360,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,universal_class)
| ~ member(X0,y) )
| ~ spl5_2 ),
inference(superposition,[],[f138,f209]) ).
fof(f369,definition,
( spl5_23
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,universal_class)
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl5_23])],[avatar_definition]) ).
fof(f370,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| ~ member(X1,universal_class)
| ~ member(X0,y) )
| ~ spl5_23 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f371,plain,
( spl5_23
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f360,f207,f369]) ).
fof(f393,definition,
( spl5_25
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl5_25])],[avatar_definition]) ).
fof(f394,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF2)
| member(X1,universal_class) )
| ~ spl5_25 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f395,plain,
( spl5_25
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f299,f207,f393]) ).
fof(f397,plain,
( ! [X0,X1] :
( member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3) )
| ~ spl5_5
| ~ spl5_25 ),
inference(resolution,[],[f394,f225]) ).
fof(f399,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f400,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f438,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,[],[f399,f139]) ).
fof(f482,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,[],[f143,f438]) ).
fof(f491,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,[],[f482]) ).
fof(f500,plain,
( ! [X0] :
( ~ member(X0,sF0)
| regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl5_3 ),
inference(superposition,[],[f491,f214]) ).
fof(f501,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_10 ),
inference(superposition,[],[f491,f255]) ).
fof(f503,definition,
( spl5_28
<=> ! [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_28])],[avatar_definition]) ).
fof(f504,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_28 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f505,plain,
( spl5_28
| ~ spl5_10 ),
inference(avatar_split_clause,[],[f501,f253,f503]) ).
fof(f508,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_28 ),
inference(resolution,[],[f504,f2]) ).
fof(f513,definition,
( spl5_29
<=> ! [X0] :
( ~ member(X0,sF0)
| regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl5_29])],[avatar_definition]) ).
fof(f514,plain,
( ! [X0] :
( ~ member(X0,sF0)
| regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl5_29 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl5_29
| ~ spl5_3 ),
inference(avatar_split_clause,[],[f500,f212,f513]) ).
fof(f517,plain,
( ! [X0] :
( regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))))))
| ~ member(X0,sF1) )
| ~ spl5_7
| ~ spl5_29 ),
inference(resolution,[],[f514,f242]) ).
fof(f525,definition,
( spl5_30
<=> ! [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_30])],[avatar_definition]) ).
fof(f526,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_30 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f527,plain,
( spl5_30
| ~ spl5_28 ),
inference(avatar_split_clause,[],[f508,f503,f525]) ).
fof(f541,definition,
( spl5_32
<=> ! [X0] :
( regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))))))
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl5_32])],[avatar_definition]) ).
fof(f542,plain,
( ! [X0] :
( ~ member(X0,sF1)
| regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl5_32 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f543,plain,
( spl5_32
| ~ spl5_7
| ~ spl5_29 ),
inference(avatar_split_clause,[],[f517,f513,f241,f541]) ).
fof(f551,definition,
( spl5_33
<=> ! [X0,X1] :
( member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_33])],[avatar_definition]) ).
fof(f552,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF3)
| member(X0,universal_class) )
| ~ spl5_33 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f553,plain,
( spl5_33
| ~ spl5_5
| ~ spl5_25 ),
inference(avatar_split_clause,[],[f397,f393,f224,f551]) ).
fof(f569,plain,
! [X0,X1] :
( ~ member(regular(intersection(X0,complement(X1))),X1)
| null_class = intersection(X0,complement(X1)) ),
inference(resolution,[],[f24,f399]) ).
fof(f578,definition,
( spl5_34
<=> ! [X0,X1] :
( ~ 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))
| ~ subclass(sF4,X0)
| sF4 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_34])],[avatar_definition]) ).
fof(f579,plain,
( ! [X0,X1] :
( ~ subclass(sF4,X0)
| 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)
| sF4 = X0 )
| ~ spl5_34 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f580,plain,
( spl5_34
| ~ spl5_19 ),
inference(avatar_split_clause,[],[f341,f338,f578]) ).
fof(f968,plain,
( ! [X0] :
( ~ subclass(X0,sF1)
| member(not_subclass_element(sF1,X0),sF0)
| sF1 = X0 )
| ~ spl5_1 ),
inference(superposition,[],[f326,f204]) ).
fof(f1030,plain,
( ! [X0] :
( ~ subclass(X0,sF1)
| member(not_subclass_element(sF1,X0),y)
| sF1 = X0 )
| ~ spl5_1 ),
inference(superposition,[],[f342,f204]) ).
fof(f2127,plain,
! [X0] :
( null_class = intersection(X0,complement(X0))
| null_class = intersection(X0,complement(X0)) ),
inference(resolution,[],[f569,f400]) ).
fof(f2157,plain,
! [X0] : null_class = intersection(X0,complement(X0)),
inference(duplicate_literal_removal,[],[f2127]) ).
fof(f2181,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f21,f2157]) ).
fof(f2182,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,complement(X1)) ),
inference(superposition,[],[f22,f2157]) ).
fof(f3098,plain,
! [X0] : ~ member(X0,null_class),
inference(global_subsumption,[],[f2181,f2182,f24]) ).
fof(f3163,definition,
( spl5_157
<=> ! [X0] :
( ~ subclass(X0,sF1)
| member(not_subclass_element(sF1,X0),sF0)
| sF1 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_157])],[avatar_definition]) ).
fof(f3164,plain,
( ! [X0] :
( member(not_subclass_element(sF1,X0),sF0)
| ~ subclass(X0,sF1)
| sF1 = X0 )
| ~ spl5_157 ),
inference(avatar_component_clause,[],[f3163]) ).
fof(f3165,plain,
( spl5_157
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f968,f202,f3163]) ).
fof(f3169,plain,
( ! [X0] :
( ~ subclass(X0,sF1)
| sF1 = X0
| regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))))) )
| ~ spl5_29
| ~ spl5_157 ),
inference(resolution,[],[f3164,f514]) ).
fof(f3191,definition,
( spl5_158
<=> ! [X0] :
( ~ subclass(X0,sF1)
| member(not_subclass_element(sF1,X0),y)
| sF1 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl5_158])],[avatar_definition]) ).
fof(f3192,plain,
( ! [X0] :
( member(not_subclass_element(sF1,X0),y)
| ~ subclass(X0,sF1)
| sF1 = X0 )
| ~ spl5_158 ),
inference(avatar_component_clause,[],[f3191]) ).
fof(f3193,plain,
( spl5_158
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f1030,f202,f3191]) ).
fof(f3210,definition,
( spl5_161
<=> ! [X0] :
( ~ subclass(X0,sF1)
| sF1 = X0
| regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl5_161])],[avatar_definition]) ).
fof(f3211,plain,
( ! [X0] :
( ~ subclass(X0,sF1)
| sF1 = X0
| regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))))) )
| ~ spl5_161 ),
inference(avatar_component_clause,[],[f3210]) ).
fof(f3212,plain,
( spl5_161
| ~ spl5_29
| ~ spl5_157 ),
inference(avatar_split_clause,[],[f3169,f3163,f513,f3210]) ).
fof(f3220,plain,
( sF1 = sF4
| regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))))))
| regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))))))
| ~ spl5_30
| ~ spl5_161 ),
inference(resolution,[],[f3211,f526]) ).
fof(f3221,plain,
( regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))))))
| regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))))))
| spl5_13
| ~ spl5_30
| ~ spl5_161 ),
inference(forward_subsumption_resolution,[],[f3220,f285]) ).
fof(f3223,definition,
( spl5_162
<=> regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl5_162])],[avatar_definition]) ).
fof(f3225,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))))))
| ~ spl5_162 ),
inference(avatar_component_clause,[],[f3223]) ).
fof(f3227,definition,
( spl5_163
<=> regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl5_163])],[avatar_definition]) ).
fof(f3228,plain,
( regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) != unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))))))
| spl5_163 ),
inference(avatar_component_clause,[],[f3227]) ).
fof(f3229,plain,
( regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))))))
| ~ spl5_163 ),
inference(avatar_component_clause,[],[f3227]) ).
fof(f3230,plain,
( spl5_162
| spl5_163
| spl5_13
| ~ spl5_30
| ~ spl5_161 ),
inference(avatar_split_clause,[],[f3221,f3210,f525,f283,f3227,f3223]) ).
fof(f3238,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X0) )
| ~ spl5_163 ),
inference(superposition,[],[f136,f3229]) ).
fof(f3239,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X1) )
| ~ spl5_163 ),
inference(superposition,[],[f137,f3229]) ).
fof(f3242,plain,
( member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF2)
| ~ member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),universal_class)
| ~ member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),y)
| ~ spl5_23
| ~ spl5_163 ),
inference(superposition,[],[f370,f3229]) ).
fof(f3259,definition,
( spl5_164
<=> member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),y) ),
introduced(definition,[new_symbols(definition,[spl5_164])],[avatar_definition]) ).
fof(f3260,plain,
( ~ member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),y)
| spl5_164 ),
inference(avatar_component_clause,[],[f3259]) ).
fof(f3263,definition,
( spl5_165
<=> member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl5_165])],[avatar_definition]) ).
fof(f3264,plain,
( member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF2)
| ~ spl5_165 ),
inference(avatar_component_clause,[],[f3263]) ).
fof(f3275,definition,
( spl5_166
<=> member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF3) ),
introduced(definition,[new_symbols(definition,[spl5_166])],[avatar_definition]) ).
fof(f3276,plain,
( member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF3)
| ~ spl5_166 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3277,plain,
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF3)
| spl5_166 ),
inference(avatar_component_clause,[],[f3275]) ).
fof(f3279,plain,
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF2)
| ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),x)
| ~ spl5_6
| spl5_166 ),
inference(resolution,[],[f3277,f235]) ).
fof(f3287,definition,
( spl5_167
<=> ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_167])],[avatar_definition]) ).
fof(f3288,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X0) )
| ~ spl5_167 ),
inference(avatar_component_clause,[],[f3287]) ).
fof(f3289,plain,
( spl5_167
| ~ spl5_163 ),
inference(avatar_split_clause,[],[f3238,f3227,f3287]) ).
fof(f3290,plain,
( member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)))
| null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ spl5_167 ),
inference(resolution,[],[f3288,f399]) ).
fof(f3301,definition,
( spl5_168
<=> null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_168])],[avatar_definition]) ).
fof(f3302,plain,
( null_class != intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| spl5_168 ),
inference(avatar_component_clause,[],[f3301]) ).
fof(f3303,plain,
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ spl5_168 ),
inference(avatar_component_clause,[],[f3301]) ).
fof(f3305,definition,
( spl5_169
<=> member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4))) ),
introduced(definition,[new_symbols(definition,[spl5_169])],[avatar_definition]) ).
fof(f3307,plain,
( member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)))
| ~ spl5_169 ),
inference(avatar_component_clause,[],[f3305]) ).
fof(f3308,plain,
( spl5_168
| spl5_169
| ~ spl5_167 ),
inference(avatar_split_clause,[],[f3290,f3287,f3305,f3301]) ).
fof(f3309,plain,
( not_subclass_element(sF1,sF4) = first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))
| not_subclass_element(sF1,sF4) = first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))
| ~ spl5_169 ),
inference(resolution,[],[f3307,f8]) ).
fof(f3314,plain,
( not_subclass_element(sF1,sF4) = first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))
| ~ spl5_169 ),
inference(duplicate_literal_removal,[],[f3309]) ).
fof(f3318,definition,
( spl5_170
<=> not_subclass_element(sF1,sF4) = first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl5_170])],[avatar_definition]) ).
fof(f3320,plain,
( not_subclass_element(sF1,sF4) = first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))
| ~ spl5_170 ),
inference(avatar_component_clause,[],[f3318]) ).
fof(f3321,plain,
( spl5_170
| ~ spl5_169 ),
inference(avatar_split_clause,[],[f3314,f3305,f3318]) ).
fof(f3330,definition,
( spl5_171
<=> ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X1) ) ),
introduced(definition,[new_symbols(definition,[spl5_171])],[avatar_definition]) ).
fof(f3331,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),X1) )
| ~ spl5_171 ),
inference(avatar_component_clause,[],[f3330]) ).
fof(f3332,plain,
( spl5_171
| ~ spl5_163 ),
inference(avatar_split_clause,[],[f3239,f3227,f3330]) ).
fof(f3333,plain,
( member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),universal_class)
| null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ spl5_171 ),
inference(resolution,[],[f3331,f399]) ).
fof(f3344,definition,
( spl5_172
<=> member(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_172])],[avatar_definition]) ).
fof(f3347,plain,
( ~ spl5_164
| ~ spl5_172
| spl5_165
| ~ spl5_23
| ~ spl5_163 ),
inference(avatar_split_clause,[],[f3242,f3227,f369,f3263,f3344,f3259]) ).
fof(f3348,plain,
( ~ member(not_subclass_element(sF1,sF4),y)
| spl5_164
| ~ spl5_170 ),
inference(forward_demodulation,[],[f3260,f3320]) ).
fof(f3350,definition,
( spl5_173
<=> member(not_subclass_element(sF1,sF4),y) ),
introduced(definition,[new_symbols(definition,[spl5_173])],[avatar_definition]) ).
fof(f3352,plain,
( ~ member(not_subclass_element(sF1,sF4),y)
| spl5_173 ),
inference(avatar_component_clause,[],[f3350]) ).
fof(f3353,plain,
( ~ spl5_173
| spl5_164
| ~ spl5_170 ),
inference(avatar_split_clause,[],[f3348,f3318,f3259,f3350]) ).
fof(f3354,plain,
( ~ subclass(sF4,sF1)
| sF1 = sF4
| ~ spl5_158
| spl5_173 ),
inference(resolution,[],[f3352,f3192]) ).
fof(f3359,plain,
( ~ subclass(sF4,sF1)
| spl5_13
| ~ spl5_158
| spl5_173 ),
inference(forward_subsumption_resolution,[],[f3354,f285]) ).
fof(f3367,definition,
( spl5_175
<=> member(not_subclass_element(sF1,sF4),sF1) ),
introduced(definition,[new_symbols(definition,[spl5_175])],[avatar_definition]) ).
fof(f3368,plain,
( member(not_subclass_element(sF1,sF4),sF1)
| ~ spl5_175 ),
inference(avatar_component_clause,[],[f3367]) ).
fof(f3369,plain,
( ~ member(not_subclass_element(sF1,sF4),sF1)
| spl5_175 ),
inference(avatar_component_clause,[],[f3367]) ).
fof(f3371,plain,
( subclass(sF1,sF4)
| spl5_175 ),
inference(resolution,[],[f3369,f2]) ).
fof(f3375,definition,
( spl5_176
<=> subclass(sF4,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_176])],[avatar_definition]) ).
fof(f3376,plain,
( subclass(sF4,sF1)
| ~ spl5_176 ),
inference(avatar_component_clause,[],[f3375]) ).
fof(f3377,plain,
( ~ subclass(sF4,sF1)
| spl5_176 ),
inference(avatar_component_clause,[],[f3375]) ).
fof(f3378,plain,
( ~ spl5_176
| spl5_13
| ~ spl5_158
| spl5_173 ),
inference(avatar_split_clause,[],[f3359,f3350,f3191,f283,f3375]) ).
fof(f3379,plain,
( regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))),unordered_pair(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))))))
| ~ spl5_30
| spl5_176 ),
inference(resolution,[],[f3377,f526]) ).
fof(f3380,plain,
( spl5_168
| spl5_172
| ~ spl5_171 ),
inference(avatar_split_clause,[],[f3333,f3330,f3344,f3301]) ).
fof(f3381,plain,
( spl5_162
| ~ spl5_30
| spl5_176 ),
inference(avatar_split_clause,[],[f3379,f3375,f525,f3223]) ).
fof(f3387,definition,
( spl5_177
<=> member(not_subclass_element(sF1,sF4),sF0) ),
introduced(definition,[new_symbols(definition,[spl5_177])],[avatar_definition]) ).
fof(f3389,plain,
( ~ member(not_subclass_element(sF1,sF4),sF0)
| spl5_177 ),
inference(avatar_component_clause,[],[f3387]) ).
fof(f3391,plain,
( ! [X0] :
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(not_subclass_element(sF1,sF4),X0)
| sF1 = sF4 )
| ~ spl5_34
| ~ spl5_176 ),
inference(resolution,[],[f3376,f579]) ).
fof(f3393,plain,
( ~ subclass(sF1,sF4)
| sF1 = sF4
| ~ spl5_176 ),
inference(resolution,[],[f3376,f7]) ).
fof(f3394,plain,
( sF1 = sF4
| spl5_175
| ~ spl5_176 ),
inference(forward_subsumption_resolution,[],[f3393,f3371]) ).
fof(f3395,plain,
( ! [X0] :
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(not_subclass_element(sF1,sF4),X0) )
| spl5_13
| ~ spl5_34
| ~ spl5_176 ),
inference(forward_subsumption_resolution,[],[f3391,f285]) ).
fof(f3396,plain,
( $false
| spl5_13
| spl5_175
| ~ spl5_176 ),
inference(forward_subsumption_resolution,[],[f3394,f285]) ).
fof(f3397,plain,
( spl5_13
| spl5_175
| ~ spl5_176 ),
inference(avatar_contradiction_clause,[],[f3396]) ).
fof(f3400,definition,
( spl5_178
<=> ! [X0] : ~ member(not_subclass_element(sF1,sF4),X0) ),
introduced(definition,[new_symbols(definition,[spl5_178])],[avatar_definition]) ).
fof(f3401,plain,
( ! [X0] : ~ member(not_subclass_element(sF1,sF4),X0)
| ~ spl5_178 ),
inference(avatar_component_clause,[],[f3400]) ).
fof(f3403,definition,
( spl5_179
<=> null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_179])],[avatar_definition]) ).
fof(f3405,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ spl5_179 ),
inference(avatar_component_clause,[],[f3403]) ).
fof(f3406,plain,
( spl5_178
| spl5_179
| spl5_13
| ~ spl5_34
| ~ spl5_176 ),
inference(avatar_split_clause,[],[f3395,f3375,f578,f283,f3403,f3400]) ).
fof(f3442,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF1,sF4),domain_of(x))
| ~ spl5_168 ),
inference(superposition,[],[f143,f3303]) ).
fof(f3461,plain,
( ~ member(not_subclass_element(sF1,sF4),domain_of(x))
| ~ spl5_168 ),
inference(trivial_inequality_removal,[],[f3442]) ).
fof(f3464,plain,
( ~ member(not_subclass_element(sF1,sF4),sF0)
| ~ spl5_3
| ~ spl5_168 ),
inference(forward_demodulation,[],[f3461,f214]) ).
fof(f3468,plain,
( ~ subclass(sF4,sF1)
| sF1 = sF4
| ~ spl5_157
| spl5_177 ),
inference(resolution,[],[f3389,f3164]) ).
fof(f3480,plain,
( sF1 = sF4
| ~ spl5_157
| ~ spl5_176
| spl5_177 ),
inference(forward_subsumption_resolution,[],[f3468,f3376]) ).
fof(f3481,plain,
( $false
| spl5_13
| ~ spl5_157
| ~ spl5_176
| spl5_177 ),
inference(forward_subsumption_resolution,[],[f3480,f285]) ).
fof(f3482,plain,
( spl5_13
| ~ spl5_157
| ~ spl5_176
| spl5_177 ),
inference(avatar_contradiction_clause,[],[f3481]) ).
fof(f3486,plain,
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),x)
| ~ spl5_6
| ~ spl5_165
| spl5_166 ),
inference(forward_subsumption_resolution,[],[f3279,f3264]) ).
fof(f3488,definition,
( spl5_180
<=> member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),x) ),
introduced(definition,[new_symbols(definition,[spl5_180])],[avatar_definition]) ).
fof(f3490,plain,
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),x)
| spl5_180 ),
inference(avatar_component_clause,[],[f3488]) ).
fof(f3491,plain,
( ~ spl5_180
| ~ spl5_6
| ~ spl5_165
| spl5_166 ),
inference(avatar_split_clause,[],[f3486,f3275,f3263,f234,f3488]) ).
fof(f3512,plain,
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| spl5_180 ),
inference(resolution,[],[f3490,f400]) ).
fof(f3520,plain,
( $false
| spl5_168
| spl5_180 ),
inference(forward_subsumption_resolution,[],[f3512,f3302]) ).
fof(f3521,plain,
( spl5_168
| spl5_180 ),
inference(avatar_contradiction_clause,[],[f3520]) ).
fof(f3591,definition,
( spl5_183
<=> ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(X0,sF3) ) ),
introduced(definition,[new_symbols(definition,[spl5_183])],[avatar_definition]) ).
fof(f3592,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_183 ),
inference(avatar_component_clause,[],[f3591]) ).
fof(f3596,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(sF1,sF4),not_subclass_element(sF1,sF4))) )
| ~ spl5_183 ),
inference(resolution,[],[f3592,f138]) ).
fof(f3608,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X0,unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4))) )
| ~ spl5_33
| ~ spl5_183 ),
inference(forward_subsumption_resolution,[],[f3596,f552]) ).
fof(f3610,definition,
( spl5_184
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X0,unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4))) ) ),
introduced(definition,[new_symbols(definition,[spl5_184])],[avatar_definition]) ).
fof(f3611,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF3)
| ~ member(X0,unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4))) )
| ~ spl5_184 ),
inference(avatar_component_clause,[],[f3610]) ).
fof(f3612,plain,
( spl5_184
| ~ spl5_33
| ~ spl5_183 ),
inference(avatar_split_clause,[],[f3608,f3591,f551,f3610]) ).
fof(f3619,plain,
( ~ member(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))),sF3)
| ~ member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)))
| ~ spl5_163
| ~ spl5_184 ),
inference(superposition,[],[f3611,f3229]) ).
fof(f3624,plain,
( ~ member(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)))
| ~ spl5_163
| ~ spl5_166
| ~ spl5_184 ),
inference(forward_subsumption_resolution,[],[f3619,f3276]) ).
fof(f3625,plain,
( $false
| ~ spl5_163
| ~ spl5_166
| ~ spl5_169
| ~ spl5_184 ),
inference(forward_subsumption_resolution,[],[f3624,f3307]) ).
fof(f3626,plain,
( ~ spl5_163
| ~ spl5_166
| ~ spl5_169
| ~ spl5_184 ),
inference(avatar_contradiction_clause,[],[f3625]) ).
fof(f3647,plain,
( ~ subclass(sF4,sF1)
| sF1 = sF4
| ~ spl5_158
| ~ spl5_178 ),
inference(resolution,[],[f3401,f3192]) ).
fof(f3698,plain,
( sF1 = sF4
| ~ spl5_158
| ~ spl5_176
| ~ spl5_178 ),
inference(forward_subsumption_resolution,[],[f3647,f3376]) ).
fof(f3703,plain,
( $false
| spl5_13
| ~ spl5_158
| ~ spl5_176
| ~ spl5_178 ),
inference(forward_subsumption_resolution,[],[f3698,f285]) ).
fof(f3704,plain,
( spl5_13
| ~ spl5_158
| ~ spl5_176
| ~ spl5_178 ),
inference(avatar_contradiction_clause,[],[f3703]) ).
fof(f4562,plain,
( regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))))),unordered_pair(first(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),unordered_pair(second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))),second(regular(intersection(x,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class)))))))
| ~ spl5_32
| ~ spl5_175 ),
inference(resolution,[],[f3368,f542]) ).
fof(f4569,plain,
( $false
| ~ spl5_32
| spl5_163
| ~ spl5_175 ),
inference(forward_subsumption_resolution,[],[f4562,f3228]) ).
fof(f4570,plain,
( ~ spl5_32
| spl5_163
| ~ spl5_175 ),
inference(avatar_contradiction_clause,[],[f4569]) ).
fof(f4578,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X0) )
| ~ spl5_162 ),
inference(superposition,[],[f136,f3225]) ).
fof(f4579,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X1) )
| ~ spl5_162 ),
inference(superposition,[],[f137,f3225]) ).
fof(f4600,definition,
( spl5_203
<=> member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF2) ),
introduced(definition,[new_symbols(definition,[spl5_203])],[avatar_definition]) ).
fof(f4601,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF2)
| ~ spl5_203 ),
inference(avatar_component_clause,[],[f4600]) ).
fof(f4602,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF2)
| spl5_203 ),
inference(avatar_component_clause,[],[f4600]) ).
fof(f4656,definition,
( spl5_204
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl5_204])],[avatar_definition]) ).
fof(f4657,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X0) )
| ~ spl5_204 ),
inference(avatar_component_clause,[],[f4656]) ).
fof(f4658,plain,
( spl5_204
| ~ spl5_162 ),
inference(avatar_split_clause,[],[f4578,f3223,f4656]) ).
fof(f4659,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)))
| null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ spl5_204 ),
inference(resolution,[],[f4657,f399]) ).
fof(f4670,definition,
( spl5_205
<=> null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_205])],[avatar_definition]) ).
fof(f4671,plain,
( null_class != intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| spl5_205 ),
inference(avatar_component_clause,[],[f4670]) ).
fof(f4672,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ spl5_205 ),
inference(avatar_component_clause,[],[f4670]) ).
fof(f4674,definition,
( spl5_206
<=> member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1))) ),
introduced(definition,[new_symbols(definition,[spl5_206])],[avatar_definition]) ).
fof(f4676,plain,
( member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)))
| ~ spl5_206 ),
inference(avatar_component_clause,[],[f4674]) ).
fof(f4677,plain,
( spl5_205
| spl5_206
| ~ spl5_204 ),
inference(avatar_split_clause,[],[f4659,f4656,f4674,f4670]) ).
fof(f4678,plain,
( not_subclass_element(sF4,sF1) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))
| not_subclass_element(sF4,sF1) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))
| ~ spl5_206 ),
inference(resolution,[],[f4676,f8]) ).
fof(f4683,plain,
( not_subclass_element(sF4,sF1) = first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))))
| ~ spl5_206 ),
inference(duplicate_literal_removal,[],[f4678]) ).
fof(f4767,definition,
( spl5_211
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X1) ) ),
introduced(definition,[new_symbols(definition,[spl5_211])],[avatar_definition]) ).
fof(f4768,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),X1) )
| ~ spl5_211 ),
inference(avatar_component_clause,[],[f4767]) ).
fof(f4769,plain,
( spl5_211
| ~ spl5_162 ),
inference(avatar_split_clause,[],[f4579,f3223,f4767]) ).
fof(f4770,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),universal_class)
| null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ spl5_211 ),
inference(resolution,[],[f4768,f399]) ).
fof(f4895,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF3)
| ~ spl5_5
| spl5_203 ),
inference(resolution,[],[f225,f4602]) ).
fof(f4932,definition,
( spl5_216
<=> member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF3) ),
introduced(definition,[new_symbols(definition,[spl5_216])],[avatar_definition]) ).
fof(f4933,plain,
( member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF3)
| ~ spl5_216 ),
inference(avatar_component_clause,[],[f4932]) ).
fof(f4934,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF3)
| spl5_216 ),
inference(avatar_component_clause,[],[f4932]) ).
fof(f4935,plain,
( ~ spl5_216
| ~ spl5_5
| spl5_203 ),
inference(avatar_split_clause,[],[f4895,f4600,f224,f4932]) ).
fof(f4936,plain,
( null_class = intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| spl5_216 ),
inference(resolution,[],[f4934,f400]) ).
fof(f5214,plain,
( spl5_205
| spl5_216 ),
inference(avatar_split_clause,[],[f4936,f4932,f4670]) ).
fof(f5437,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF4,sF1),domain_of(sF3))
| ~ spl5_205 ),
inference(superposition,[],[f143,f4672]) ).
fof(f5456,plain,
( ~ member(not_subclass_element(sF4,sF1),domain_of(sF3))
| ~ spl5_205 ),
inference(trivial_inequality_removal,[],[f5437]) ).
fof(f5459,plain,
( ~ member(not_subclass_element(sF4,sF1),sF4)
| ~ spl5_10
| ~ spl5_205 ),
inference(forward_demodulation,[],[f5456,f255]) ).
fof(f5588,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),universal_class)
| spl5_205
| ~ spl5_211 ),
inference(forward_subsumption_resolution,[],[f4770,f4671]) ).
fof(f5689,plain,
( ~ spl5_177
| ~ spl5_3
| ~ spl5_168 ),
inference(avatar_split_clause,[],[f3464,f3301,f212,f3387]) ).
fof(f5707,plain,
( ! [X0,X1] :
( member(not_subclass_element(sF4,sF1),X0)
| ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1)) )
| ~ spl5_204
| ~ spl5_206 ),
inference(forward_demodulation,[],[f4657,f4683]) ).
fof(f5800,definition,
( spl5_220
<=> ! [X0,X1] :
( member(not_subclass_element(sF4,sF1),X0)
| ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl5_220])],[avatar_definition]) ).
fof(f5801,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),cross_product(X0,X1))
| member(not_subclass_element(sF4,sF1),X0) )
| ~ spl5_220 ),
inference(avatar_component_clause,[],[f5800]) ).
fof(f5802,plain,
( spl5_220
| ~ spl5_204
| ~ spl5_206 ),
inference(avatar_split_clause,[],[f5707,f4674,f4656,f5800]) ).
fof(f5808,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF2)
| member(not_subclass_element(sF4,sF1),y)
| ~ spl5_2
| ~ spl5_220 ),
inference(superposition,[],[f5801,f209]) ).
fof(f5811,plain,
( member(not_subclass_element(sF4,sF1),y)
| ~ spl5_2
| ~ spl5_203
| ~ spl5_220 ),
inference(forward_subsumption_resolution,[],[f5808,f4601]) ).
fof(f5814,definition,
( spl5_221
<=> member(not_subclass_element(sF4,sF1),y) ),
introduced(definition,[new_symbols(definition,[spl5_221])],[avatar_definition]) ).
fof(f5816,plain,
( member(not_subclass_element(sF4,sF1),y)
| ~ spl5_221 ),
inference(avatar_component_clause,[],[f5814]) ).
fof(f5817,plain,
( spl5_221
| ~ spl5_2
| ~ spl5_203
| ~ spl5_220 ),
inference(avatar_split_clause,[],[f5811,f5800,f4600,f207,f5814]) ).
fof(f5874,plain,
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| subclass(sF4,sF1)
| ~ spl5_17
| ~ spl5_221 ),
inference(resolution,[],[f320,f5816]) ).
fof(f5881,plain,
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ spl5_17
| spl5_176
| ~ spl5_221 ),
inference(forward_subsumption_resolution,[],[f5874,f3377]) ).
fof(f5883,definition,
( spl5_222
<=> null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl5_222])],[avatar_definition]) ).
fof(f5885,plain,
( null_class = intersection(x,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ spl5_222 ),
inference(avatar_component_clause,[],[f5883]) ).
fof(f5886,plain,
( spl5_222
| ~ spl5_17
| spl5_176
| ~ spl5_221 ),
inference(avatar_split_clause,[],[f5881,f5814,f3375,f319,f5883]) ).
fof(f5892,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ member(X0,x) )
| ~ spl5_222 ),
inference(superposition,[],[f23,f5885]) ).
fof(f5910,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ member(X0,x) )
| ~ spl5_222 ),
inference(forward_subsumption_resolution,[],[f5892,f3098]) ).
fof(f5984,definition,
( spl5_228
<=> member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_228])],[avatar_definition]) ).
fof(f5986,plain,
( member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),universal_class)
| ~ spl5_228 ),
inference(avatar_component_clause,[],[f5984]) ).
fof(f5987,plain,
( spl5_228
| spl5_205
| ~ spl5_211 ),
inference(avatar_split_clause,[],[f5588,f4767,f4670,f5984]) ).
fof(f6004,definition,
( spl5_230
<=> ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl5_230])],[avatar_definition]) ).
fof(f6005,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))
| ~ member(X0,x) )
| ~ spl5_230 ),
inference(avatar_component_clause,[],[f6004]) ).
fof(f6006,plain,
( spl5_230
| ~ spl5_222 ),
inference(avatar_split_clause,[],[f5910,f5883,f6004]) ).
fof(f6009,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),x)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1))) )
| ~ spl5_230 ),
inference(resolution,[],[f6005,f138]) ).
fof(f6022,definition,
( spl5_231
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),x)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1))) ) ),
introduced(definition,[new_symbols(definition,[spl5_231])],[avatar_definition]) ).
fof(f6023,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),x)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1))) )
| ~ spl5_231 ),
inference(avatar_component_clause,[],[f6022]) ).
fof(f6024,plain,
( spl5_231
| ~ spl5_230 ),
inference(avatar_split_clause,[],[f6009,f6004,f6022]) ).
fof(f6030,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),x)
| ~ member(second(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),universal_class)
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)))
| ~ spl5_162
| ~ spl5_231 ),
inference(superposition,[],[f6023,f3225]) ).
fof(f6036,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),x)
| ~ member(first(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class)))),unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)))
| ~ spl5_162
| ~ spl5_228
| ~ spl5_231 ),
inference(forward_subsumption_resolution,[],[f6030,f5986]) ).
fof(f6039,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),x)
| ~ spl5_162
| ~ spl5_206
| ~ spl5_228
| ~ spl5_231 ),
inference(forward_subsumption_resolution,[],[f6036,f4676]) ).
fof(f6041,definition,
( spl5_232
<=> member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),x) ),
introduced(definition,[new_symbols(definition,[spl5_232])],[avatar_definition]) ).
fof(f6043,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),x)
| spl5_232 ),
inference(avatar_component_clause,[],[f6041]) ).
fof(f6044,plain,
( ~ spl5_232
| ~ spl5_162
| ~ spl5_206
| ~ spl5_228
| ~ spl5_231 ),
inference(avatar_split_clause,[],[f6039,f6022,f5984,f4674,f3223,f6041]) ).
fof(f6047,plain,
( ~ member(regular(intersection(sF3,cross_product(unordered_pair(not_subclass_element(sF4,sF1),not_subclass_element(sF4,sF1)),universal_class))),sF3)
| ~ spl5_11
| spl5_232 ),
inference(resolution,[],[f6043,f259]) ).
fof(f6056,plain,
( $false
| ~ spl5_11
| ~ spl5_216
| spl5_232 ),
inference(forward_subsumption_resolution,[],[f6047,f4933]) ).
fof(f6057,plain,
( ~ spl5_11
| ~ spl5_216
| spl5_232 ),
inference(avatar_contradiction_clause,[],[f6056]) ).
fof(f6148,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_179 ),
inference(superposition,[],[f23,f3405]) ).
fof(f6342,definition,
( spl5_233
<=> member(not_subclass_element(sF4,sF1),sF4) ),
introduced(definition,[new_symbols(definition,[spl5_233])],[avatar_definition]) ).
fof(f6344,plain,
( ~ member(not_subclass_element(sF4,sF1),sF4)
| spl5_233 ),
inference(avatar_component_clause,[],[f6342]) ).
fof(f6345,plain,
( ~ spl5_233
| ~ spl5_10
| ~ spl5_205 ),
inference(avatar_split_clause,[],[f5459,f4670,f253,f6342]) ).
fof(f6347,plain,
( subclass(sF4,sF1)
| spl5_233 ),
inference(resolution,[],[f6344,f2]) ).
fof(f6351,plain,
( $false
| spl5_176
| spl5_233 ),
inference(forward_subsumption_resolution,[],[f6347,f3377]) ).
fof(f6352,plain,
( spl5_176
| spl5_233 ),
inference(avatar_contradiction_clause,[],[f6351]) ).
fof(f6359,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF1,sF4),not_subclass_element(sF1,sF4)),universal_class))
| ~ member(X0,sF3) )
| ~ spl5_179 ),
inference(forward_subsumption_resolution,[],[f6148,f3098]) ).
fof(f6409,plain,
( spl5_183
| ~ spl5_179 ),
inference(avatar_split_clause,[],[f6359,f3403,f3591]) ).
cnf(s99,plain,
spl5_1,
inference(sat_conversion,[],[f205]) ).
cnf(s101,plain,
spl5_2,
inference(sat_conversion,[],[f210]) ).
cnf(s103,plain,
spl5_3,
inference(sat_conversion,[],[f215]) ).
cnf(s105,plain,
spl5_4,
inference(sat_conversion,[],[f220]) ).
cnf(s109,plain,
( ~ spl5_4
| spl5_5 ),
inference(sat_conversion,[],[f226]) ).
cnf(s114,plain,
( ~ spl5_4
| spl5_6 ),
inference(sat_conversion,[],[f236]) ).
cnf(s119,plain,
( ~ spl5_1
| spl5_7 ),
inference(sat_conversion,[],[f243]) ).
cnf(s121,plain,
( ~ spl5_1
| spl5_8 ),
inference(sat_conversion,[],[f247]) ).
cnf(s125,plain,
spl5_10,
inference(sat_conversion,[],[f256]) ).
cnf(s127,plain,
( ~ spl5_4
| spl5_11 ),
inference(sat_conversion,[],[f260]) ).
cnf(s137,plain,
( ~ spl5_8
| spl5_12 ),
inference(sat_conversion,[],[f274]) ).
cnf(s144,plain,
~ spl5_13,
inference(sat_conversion,[],[f286]) ).
cnf(s162,plain,
( ~ spl5_10
| spl5_15 ),
inference(sat_conversion,[],[f309]) ).
cnf(s164,plain,
( ~ spl5_3
| spl5_16 ),
inference(sat_conversion,[],[f313]) ).
cnf(s169,plain,
( ~ spl5_12
| ~ spl5_16
| spl5_17 ),
inference(sat_conversion,[],[f321]) ).
cnf(s179,plain,
( ~ spl5_15
| spl5_19 ),
inference(sat_conversion,[],[f340]) ).
cnf(s197,plain,
( ~ spl5_2
| spl5_23 ),
inference(sat_conversion,[],[f371]) ).
cnf(s210,plain,
( ~ spl5_2
| spl5_25 ),
inference(sat_conversion,[],[f395]) ).
cnf(s266,plain,
( ~ spl5_10
| spl5_28 ),
inference(sat_conversion,[],[f505]) ).
cnf(s273,plain,
( ~ spl5_3
| spl5_29 ),
inference(sat_conversion,[],[f515]) ).
cnf(s282,plain,
( ~ spl5_28
| spl5_30 ),
inference(sat_conversion,[],[f527]) ).
cnf(s291,plain,
( ~ spl5_7
| ~ spl5_29
| spl5_32 ),
inference(sat_conversion,[],[f543]) ).
cnf(s297,plain,
( ~ spl5_5
| ~ spl5_25
| spl5_33 ),
inference(sat_conversion,[],[f553]) ).
cnf(s314,plain,
( ~ spl5_19
| spl5_34 ),
inference(sat_conversion,[],[f580]) ).
cnf(s1637,plain,
( ~ spl5_1
| spl5_157 ),
inference(sat_conversion,[],[f3165]) ).
cnf(s1640,plain,
( ~ spl5_1
| spl5_158 ),
inference(sat_conversion,[],[f3193]) ).
cnf(s1646,plain,
( ~ spl5_29
| ~ spl5_157
| spl5_161 ),
inference(sat_conversion,[],[f3212]) ).
cnf(s1655,plain,
( spl5_13
| ~ spl5_30
| ~ spl5_161
| spl5_162
| spl5_163 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s1687,plain,
( ~ spl5_163
| spl5_167 ),
inference(sat_conversion,[],[f3289]) ).
cnf(s1693,plain,
( ~ spl5_167
| spl5_168
| spl5_169 ),
inference(sat_conversion,[],[f3308]) ).
cnf(s1698,plain,
( ~ spl5_169
| spl5_170 ),
inference(sat_conversion,[],[f3321]) ).
cnf(s1703,plain,
( ~ spl5_163
| spl5_171 ),
inference(sat_conversion,[],[f3332]) ).
cnf(s1708,plain,
( ~ spl5_23
| ~ spl5_163
| ~ spl5_164
| spl5_165
| ~ spl5_172 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s1710,plain,
( spl5_164
| ~ spl5_170
| ~ spl5_173 ),
inference(sat_conversion,[],[f3353]) ).
cnf(s1722,plain,
( spl5_13
| ~ spl5_158
| spl5_173
| ~ spl5_176 ),
inference(sat_conversion,[],[f3378]) ).
cnf(s1725,plain,
( spl5_168
| ~ spl5_171
| spl5_172 ),
inference(sat_conversion,[],[f3380]) ).
cnf(s1727,plain,
( ~ spl5_30
| spl5_162
| spl5_176 ),
inference(sat_conversion,[],[f3381]) ).
cnf(s1743,plain,
( spl5_13
| spl5_175
| ~ spl5_176 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s1747,plain,
( spl5_13
| ~ spl5_34
| ~ spl5_176
| spl5_178
| spl5_179 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s1769,plain,
( spl5_13
| ~ spl5_157
| ~ spl5_176
| spl5_177 ),
inference(sat_conversion,[],[f3482]) ).
cnf(s1783,plain,
( ~ spl5_6
| ~ spl5_165
| spl5_166
| ~ spl5_180 ),
inference(sat_conversion,[],[f3491]) ).
cnf(s1791,plain,
( spl5_168
| spl5_180 ),
inference(sat_conversion,[],[f3521]) ).
cnf(s1834,plain,
( ~ spl5_33
| ~ spl5_183
| spl5_184 ),
inference(sat_conversion,[],[f3612]) ).
cnf(s1844,plain,
( ~ spl5_163
| ~ spl5_166
| ~ spl5_169
| ~ spl5_184 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s1874,plain,
( spl5_13
| ~ spl5_158
| ~ spl5_176
| ~ spl5_178 ),
inference(sat_conversion,[],[f3704]) ).
cnf(s2537,plain,
( ~ spl5_32
| spl5_163
| ~ spl5_175 ),
inference(sat_conversion,[],[f4570]) ).
cnf(s2637,plain,
( ~ spl5_162
| spl5_204 ),
inference(sat_conversion,[],[f4658]) ).
cnf(s2643,plain,
( ~ spl5_204
| spl5_205
| spl5_206 ),
inference(sat_conversion,[],[f4677]) ).
cnf(s2688,plain,
( ~ spl5_162
| spl5_211 ),
inference(sat_conversion,[],[f4769]) ).
cnf(s2737,plain,
( ~ spl5_5
| spl5_203
| ~ spl5_216 ),
inference(sat_conversion,[],[f4935]) ).
cnf(s2860,plain,
( spl5_205
| spl5_216 ),
inference(sat_conversion,[],[f5214]) ).
cnf(s3096,plain,
( ~ spl5_3
| ~ spl5_168
| ~ spl5_177 ),
inference(sat_conversion,[],[f5689]) ).
cnf(s3120,plain,
( ~ spl5_204
| ~ spl5_206
| spl5_220 ),
inference(sat_conversion,[],[f5802]) ).
cnf(s3125,plain,
( ~ spl5_2
| ~ spl5_203
| ~ spl5_220
| spl5_221 ),
inference(sat_conversion,[],[f5817]) ).
cnf(s3152,plain,
( ~ spl5_17
| spl5_176
| ~ spl5_221
| spl5_222 ),
inference(sat_conversion,[],[f5886]) ).
cnf(s3190,plain,
( spl5_205
| ~ spl5_211
| spl5_228 ),
inference(sat_conversion,[],[f5987]) ).
cnf(s3196,plain,
( ~ spl5_222
| spl5_230 ),
inference(sat_conversion,[],[f6006]) ).
cnf(s3209,plain,
( ~ spl5_230
| spl5_231 ),
inference(sat_conversion,[],[f6024]) ).
cnf(s3219,plain,
( ~ spl5_162
| ~ spl5_206
| ~ spl5_228
| ~ spl5_231
| ~ spl5_232 ),
inference(sat_conversion,[],[f6044]) ).
cnf(s3224,plain,
( ~ spl5_11
| ~ spl5_216
| spl5_232 ),
inference(sat_conversion,[],[f6057]) ).
cnf(s3345,plain,
( ~ spl5_10
| ~ spl5_205
| ~ spl5_233 ),
inference(sat_conversion,[],[f6345]) ).
cnf(s3349,plain,
( spl5_176
| spl5_233 ),
inference(sat_conversion,[],[f6352]) ).
cnf(s3395,plain,
( ~ spl5_179
| spl5_183 ),
inference(sat_conversion,[],[f6409]) ).
cnf(s3400,plain,
spl5_28,
inference(rat,[],[s266,s125]) ).
cnf(s3401,plain,
spl5_15,
inference(rat,[],[s162,s125]) ).
cnf(s3403,plain,
spl5_30,
inference(rat,[],[s282,s3400]) ).
cnf(s3404,plain,
spl5_19,
inference(rat,[],[s179,s3401]) ).
cnf(s3406,plain,
spl5_34,
inference(rat,[],[s314,s3404]) ).
cnf(s3415,plain,
spl5_11,
inference(rat,[],[s127,s105]) ).
cnf(s3416,plain,
spl5_6,
inference(rat,[],[s114,s105]) ).
cnf(s3417,plain,
spl5_5,
inference(rat,[],[s109,s105]) ).
cnf(s3423,plain,
spl5_29,
inference(rat,[],[s273,s103]) ).
cnf(s3424,plain,
spl5_16,
inference(rat,[],[s164,s103]) ).
cnf(s3427,plain,
spl5_25,
inference(rat,[],[s210,s101]) ).
cnf(s3428,plain,
spl5_23,
inference(rat,[],[s197,s101]) ).
cnf(s3432,plain,
spl5_33,
inference(rat,[],[s297,s3417,s3427]) ).
cnf(s3443,plain,
spl5_158,
inference(rat,[],[s1640,s99]) ).
cnf(s3444,plain,
spl5_157,
inference(rat,[],[s1637,s99]) ).
cnf(s3448,plain,
spl5_8,
inference(rat,[],[s121,s99]) ).
cnf(s3449,plain,
spl5_7,
inference(rat,[],[s119,s99]) ).
cnf(s3450,plain,
spl5_161,
inference(rat,[],[s1646,s3423,s3444]) ).
cnf(s3456,plain,
spl5_12,
inference(rat,[],[s137,s3448]) ).
cnf(s3458,plain,
spl5_32,
inference(rat,[],[s291,s3423,s3449]) ).
cnf(s3460,plain,
spl5_17,
inference(rat,[],[s169,s3424,s3456]) ).
cnf(s3463,plain,
spl5_162,
inference(rat,[],[s1783,s1708,s1844,s1710,s1834,s1698,s1791,s3395,s1693,s1725,s3096,s1747,s1687,s1703,s1722,s1769,s1874,s1655,s1727,s3416,s3428,s3432,s103,s144,s3406,s3443,s3444,s3403,s3450]) ).
cnf(s3464,plain,
spl5_211,
inference(rat,[],[s2688,s3463]) ).
cnf(s3465,plain,
spl5_204,
inference(rat,[],[s2637,s3463]) ).
cnf(s3466,plain,
spl5_176,
inference(rat,[],[s3152,s3196,s3125,s3209,s3120,s3219,s2737,s3224,s2643,s3190,s2860,s3345,s3349,s3460,s101,s3465,s3463,s3417,s3415,s3464,s125]) ).
cnf(s3467,plain,
~ spl5_178,
inference(rat,[],[s1874,s3443,s144,s3466]) ).
cnf(s3469,plain,
spl5_177,
inference(rat,[],[s1769,s3444,s144,s3466]) ).
cnf(s3470,plain,
spl5_175,
inference(rat,[],[s1743,s144,s3466]) ).
cnf(s3471,plain,
spl5_173,
inference(rat,[],[s1722,s3443,s144,s3466]) ).
cnf(s3472,plain,
spl5_179,
inference(rat,[],[s1747,s3466,s3406,s144,s3467]) ).
cnf(s3474,plain,
~ spl5_168,
inference(rat,[],[s3096,s103,s3469]) ).
cnf(s3475,plain,
spl5_163,
inference(rat,[],[s2537,s3458,s3470]) ).
cnf(s3476,plain,
spl5_183,
inference(rat,[],[s3395,s3472]) ).
cnf(s3479,plain,
spl5_180,
inference(rat,[],[s1791,s3474]) ).
cnf(s3480,plain,
spl5_171,
inference(rat,[],[s1703,s3475]) ).
cnf(s3481,plain,
spl5_167,
inference(rat,[],[s1687,s3475]) ).
cnf(s3482,plain,
spl5_184,
inference(rat,[],[s1834,s3432,s3476]) ).
cnf(s3484,plain,
spl5_172,
inference(rat,[],[s1725,s3474,s3480]) ).
cnf(s3485,plain,
spl5_169,
inference(rat,[],[s1693,s3474,s3481]) ).
cnf(s3486,plain,
~ spl5_166,
inference(rat,[],[s1844,s3485,s3475,s3482]) ).
cnf(s3488,plain,
spl5_170,
inference(rat,[],[s1698,s3485]) ).
cnf(s3489,plain,
~ spl5_165,
inference(rat,[],[s1783,s3479,s3416,s3486]) ).
cnf(s3490,plain,
spl5_164,
inference(rat,[],[s1710,s3471,s3488]) ).
cnf(s3491,plain,
$false,
inference(rat,[],[s1708,s3484,s3475,s3428,s3490,s3489]) ).
fof(f6410,plain,
$false,
inference(avatar_sat_refutation,[],[s3491]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET274-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n017.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 28 01:12:36 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 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
% 10.31/2.36 % (3130044)Input is clausal, will run a generic CNF schedule.
% 10.31/2.36 % (3130053)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1764641663:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.31/2.36 % (3130049)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=1199374994:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.31/2.36 % (3130051)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1823144458:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.31/2.36 % (3130050)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3233038283:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.31/2.36 % (3130052)lrs+10_1_sil=8000:sp=occurrence:random_seed=1820801434:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.31/2.36 % (3130053)Instruction limit reached!
% 10.31/2.36 % (3130053)------------------------------
% 10.31/2.36 % (3130053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.36 % (3130053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.36 % (3130053)CaDiCaL version: 2.1.3
% 10.31/2.36 % (3130053)Termination reason: Instruction limit
% 10.31/2.36 % (3130053)Termination phase: Saturation
% 10.31/2.36 % (3130053)Time elapsed: 0.037 s
% 10.31/2.36 % (3130053)Peak memory usage: 89 MB
% 10.31/2.36 % (3130053)Instructions burned: 117 (million)
% 10.31/2.36 % (3130052)Refutation not found, incomplete strategy
% 10.31/2.36 % (3130052)------------------------------
% 10.31/2.36 % (3130052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.36 % (3130052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.36 % (3130052)CaDiCaL version: 2.1.3
% 10.31/2.36 % (3130052)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.36 % (3130052)Time elapsed: 0.002 s
% 10.31/2.36 % (3130052)Peak memory usage: 88 MB
% 10.31/2.36 % (3130052)Instructions burned: 1 (million)
% 10.31/2.36 % (3130054)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4198012380:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.31/2.36 % (3130055)dis-21_1_sil=8000:lcm=predicate:random_seed=3070151622:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.31/2.36 % (3130055)Instruction limit reached!
% 10.31/2.36 % (3130055)------------------------------
% 10.31/2.36 % (3130055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.36 % (3130055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.36 % (3130055)CaDiCaL version: 2.1.3
% 10.31/2.36 % (3130055)Termination reason: Instruction limit
% 10.31/2.36 % (3130055)Termination phase: Saturation
% 10.31/2.36 % (3130055)Time elapsed: 0.071 s
% 10.31/2.36 % (3130055)Peak memory usage: 89 MB
% 10.31/2.36 % (3130055)Instructions burned: 117 (million)
% 10.31/2.36 % (3130063)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=2019759210:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.31/2.36 % (3130063)Refutation not found, incomplete strategy
% 10.31/2.36 % (3130063)------------------------------
% 10.31/2.36 % (3130063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.36 % (3130063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.36 % (3130063)CaDiCaL version: 2.1.3
% 10.31/2.36 % (3130063)Termination reason: Refutation not found, incomplete strategy
% 10.31/2.36 % (3130063)Time elapsed: 0.001 s
% 10.31/2.36 % (3130063)Peak memory usage: 88 MB
% 10.31/2.36 % (3130063)Instructions burned: 3 (million)
% 10.31/2.36 % (3130054)Instruction limit reached!
% 10.31/2.36 % (3130054)------------------------------
% 10.31/2.36 % (3130054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.36 % (3130054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.36 % (3130054)CaDiCaL version: 2.1.3
% 10.31/2.36 % (3130054)Termination reason: Instruction limit
% 10.31/2.36 % (3130054)Termination phase: Saturation
% 10.31/2.36 % (3130054)Time elapsed: 0.136 s
% 10.31/2.36 % (3130054)Peak memory usage: 90 MB
% 10.31/2.36 % (3130054)Instructions burned: 181 (million)
% 10.31/2.36 % (3130064)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1343649026: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)
% 16.33/3.17 % (3130052)------------------------------
% 16.33/3.17 % (3130052)------------------------------
% 16.33/3.17 % (3130063)------------------------------
% 16.33/3.17 % (3130063)------------------------------
% 16.33/3.17 % (3130066)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1391144698:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.33/3.17 % (3130066)Refutation not found, incomplete strategy
% 16.33/3.17 % (3130066)------------------------------
% 16.33/3.17 % (3130066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.33/3.17 % (3130066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/3.17 % (3130066)CaDiCaL version: 2.1.3
% 16.33/3.17 % (3130066)Termination reason: Refutation not found, incomplete strategy
% 16.33/3.17 % (3130066)Time elapsed: 0.003 s
% 16.33/3.17 % (3130066)Peak memory usage: 88 MB
% 16.33/3.17 % (3130066)Instructions burned: 3 (million)
% 16.33/3.17 % (3130064)Instruction limit reached!
% 16.33/3.17 % (3130064)------------------------------
% 16.33/3.17 % (3130064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.33/3.17 % (3130064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/3.17 % (3130064)CaDiCaL version: 2.1.3
% 16.33/3.17 % (3130064)Termination reason: Instruction limit
% 16.33/3.17 % (3130064)Termination phase: Saturation
% 16.33/3.17 % (3130064)Time elapsed: 0.107 s
% 16.33/3.17 % (3130064)Peak memory usage: 91 MB
% 16.33/3.17 % (3130064)Instructions burned: 189 (million)
% 16.33/3.17 % (3130068)lrs+10_64_to=lpo:sil=8000:random_seed=3014092307:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 16.33/3.17 % (3130068)Instruction limit reached!
% 16.33/3.17 % (3130068)------------------------------
% 16.33/3.17 % (3130068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.33/3.17 % (3130068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/3.17 % (3130068)CaDiCaL version: 2.1.3
% 16.33/3.17 % (3130068)Termination reason: Instruction limit
% 16.33/3.17 % (3130068)Termination phase: Saturation
% 16.33/3.17 % (3130068)Time elapsed: 0.044 s
% 16.33/3.17 % (3130068)Peak memory usage: 89 MB
% 16.33/3.17 % (3130068)Instructions burned: 128 (million)
% 16.33/3.17 % (3130069)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=783104846:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.33/3.17 % (3130071)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=515877809:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 16.33/3.17 % (3130073)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4190893274:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 16.33/3.17 % (3130069)Instruction limit reached!
% 16.33/3.17 % (3130069)------------------------------
% 16.33/3.17 % (3130069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.33/3.17 % (3130069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/3.17 % (3130069)CaDiCaL version: 2.1.3
% 16.33/3.17 % (3130069)Termination reason: Instruction limit
% 16.33/3.17 % (3130069)Termination phase: Saturation
% 16.33/3.17 % (3130069)Time elapsed: 0.122 s
% 16.33/3.17 % (3130069)Peak memory usage: 89 MB
% 16.33/3.17 % (3130069)Instructions burned: 194 (million)
% 16.33/3.17 % (3130066)------------------------------
% 16.33/3.17 % (3130066)------------------------------
% 16.33/3.17 % (3130071)Instruction limit reached!
% 16.33/3.17 % (3130071)------------------------------
% 16.33/3.17 % (3130071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.33/3.17 % (3130071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.33/3.17 % (3130071)CaDiCaL version: 2.1.3
% 16.33/3.17 % (3130071)Termination reason: Instruction limit
% 16.33/3.17 % (3130071)Termination phase: Saturation
% 16.33/3.17 % (3130071)Time elapsed: 0.107 s
% 16.33/3.17 % (3130071)Peak memory usage: 91 MB
% 16.33/3.17 % (3130071)Instructions burned: 158 (million)
% 16.33/3.17 % (3130077)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=1487946503:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 16.33/3.17 % (3130078)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4099489501:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 33.35/5.67 % (3130078)Refutation not found, incomplete strategy
% 33.35/5.67 % (3130078)------------------------------
% 33.35/5.67 % (3130078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130078)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130078)Termination reason: Refutation not found, incomplete strategy
% 33.35/5.67 % (3130078)Time elapsed: 0.005 s
% 33.35/5.67 % (3130078)Peak memory usage: 88 MB
% 33.35/5.67 % (3130078)Instructions burned: 8 (million)
% 33.35/5.67 % (3130079)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=919662975:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 33.35/5.67 % (3130077)Instruction limit reached!
% 33.35/5.67 % (3130077)------------------------------
% 33.35/5.67 % (3130077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130077)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130077)Termination reason: Instruction limit
% 33.35/5.67 % (3130077)Termination phase: Saturation
% 33.35/5.67 % (3130077)Time elapsed: 0.054 s
% 33.35/5.67 % (3130077)Peak memory usage: 89 MB
% 33.35/5.67 % (3130077)Instructions burned: 107 (million)
% 33.35/5.67 % (3130083)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=554025846:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 33.35/5.67 % (3130079)Instruction limit reached!
% 33.35/5.67 % (3130079)------------------------------
% 33.35/5.67 % (3130079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130079)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130079)Termination reason: Instruction limit
% 33.35/5.67 % (3130079)Termination phase: Saturation
% 33.35/5.67 % (3130079)Time elapsed: 0.165 s
% 33.35/5.67 % (3130079)Peak memory usage: 90 MB
% 33.35/5.67 % (3130079)Instructions burned: 243 (million)
% 33.35/5.67 % (3130078)------------------------------
% 33.35/5.67 % (3130078)------------------------------
% 33.35/5.67 % (3130085)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=258353093:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 33.35/5.67 % (3130086)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2625604313:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 33.35/5.67 % (3130085)Instruction limit reached!
% 33.35/5.67 % (3130085)------------------------------
% 33.35/5.67 % (3130085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130085)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130085)Termination reason: Instruction limit
% 33.35/5.67 % (3130085)Termination phase: Saturation
% 33.35/5.67 % (3130085)Time elapsed: 0.099 s
% 33.35/5.67 % (3130085)Peak memory usage: 90 MB
% 33.35/5.67 % (3130085)Instructions burned: 135 (million)
% 33.35/5.67 % (3130089)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=733095605:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 33.35/5.67 % (3130089)Instruction limit reached!
% 33.35/5.67 % (3130089)------------------------------
% 33.35/5.67 % (3130089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130089)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130089)Termination reason: Instruction limit
% 33.35/5.67 % (3130089)Termination phase: Saturation
% 33.35/5.67 % (3130089)Time elapsed: 0.115 s
% 33.35/5.67 % (3130089)Peak memory usage: 89 MB
% 33.35/5.67 % (3130089)Instructions burned: 192 (million)
% 33.35/5.67 % (3130086)Instruction limit reached!
% 33.35/5.67 % (3130086)------------------------------
% 33.35/5.67 % (3130086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.35/5.67 % (3130086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.35/5.67 % (3130086)CaDiCaL version: 2.1.3
% 33.35/5.67 % (3130086)Termination reason: Instruction limit
% 33.35/5.67 % (3130086)Termination phase: Saturation
% 33.35/5.67 % (3130086)Time elapsed: 0.296 s
% 46.84/7.58 % (3130086)Peak memory usage: 92 MB
% 46.84/7.58 % (3130086)Instructions burned: 500 (million)
% 46.84/7.58 % (3130091)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=474834591:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 46.84/7.58 % (3130092)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2531500337:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 46.84/7.58 % (3130092)Instruction limit reached!
% 46.84/7.58 % (3130092)------------------------------
% 46.84/7.58 % (3130092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.84/7.58 % (3130092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.84/7.58 % (3130092)CaDiCaL version: 2.1.3
% 46.84/7.58 % (3130092)Termination reason: Instruction limit
% 46.84/7.58 % (3130092)Termination phase: Saturation
% 46.84/7.58 % (3130092)Time elapsed: 0.105 s
% 46.84/7.58 % (3130092)Peak memory usage: 89 MB
% 46.84/7.58 % (3130092)Instructions burned: 156 (million)
% 46.84/7.58 % (3130091)Instruction limit reached!
% 46.84/7.58 % (3130091)------------------------------
% 46.84/7.58 % (3130091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.84/7.58 % (3130091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.84/7.58 % (3130091)CaDiCaL version: 2.1.3
% 46.84/7.58 % (3130091)Termination reason: Instruction limit
% 46.84/7.58 % (3130091)Termination phase: Saturation
% 46.84/7.58 % (3130091)Time elapsed: 0.175 s
% 46.84/7.58 % (3130091)Peak memory usage: 91 MB
% 46.84/7.58 % (3130091)Instructions burned: 265 (million)
% 46.84/7.58 % (3130073)Instruction limit reached!
% 46.84/7.58 % (3130073)------------------------------
% 46.84/7.58 % (3130073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.84/7.58 % (3130073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.84/7.58 % (3130073)CaDiCaL version: 2.1.3
% 46.84/7.58 % (3130073)Termination reason: Instruction limit
% 46.84/7.58 % (3130073)Termination phase: Saturation
% 46.84/7.58 % (3130073)Time elapsed: 1.167 s
% 46.84/7.58 % (3130073)Peak memory usage: 146 MB
% 46.84/7.58 % (3130073)Instructions burned: 3395 (million)
% 46.84/7.58 % (3130095)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=1809395270:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 46.84/7.58 % (3130097)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2313982476:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 46.84/7.58 % (3130096)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=999027252:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 46.84/7.58 % (3130096)Refutation not found, incomplete strategy
% 46.84/7.58 % (3130096)------------------------------
% 46.84/7.58 % (3130096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.84/7.58 % (3130096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.84/7.58 % (3130096)CaDiCaL version: 2.1.3
% 46.84/7.58 % (3130096)Termination reason: Refutation not found, incomplete strategy
% 46.84/7.58 % (3130096)Time elapsed: 0.002 s
% 46.84/7.58 % (3130096)Peak memory usage: 88 MB
% 46.84/7.58 % (3130096)Instructions burned: 2 (million)
% 46.84/7.58 % (3130097)Instruction limit reached!
% 46.84/7.58 % (3130097)------------------------------
% 46.84/7.58 % (3130097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.84/7.58 % (3130097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.84/7.58 % (3130097)CaDiCaL version: 2.1.3
% 46.84/7.58 % (3130097)Termination reason: Instruction limit
% 46.84/7.58 % (3130097)Termination phase: Saturation
% 46.84/7.58 % (3130097)Time elapsed: 0.059 s
% 46.84/7.58 % (3130097)Peak memory usage: 90 MB
% 46.84/7.58 % (3130097)Instructions burned: 181 (million)
% 46.84/7.58 % (3130101)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=2689589306:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 46.84/7.58 % (3130096)------------------------------
% 46.84/7.58 % (3130096)------------------------------
% 46.84/7.58 % (3130103)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=1548939499:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 61.84/9.63 % (3130103)Instruction limit reached!
% 61.84/9.63 % (3130103)------------------------------
% 61.84/9.63 % (3130103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.84/9.63 % (3130103)CaDiCaL version: 2.1.3
% 61.84/9.63 % (3130103)Termination reason: Instruction limit
% 61.84/9.63 % (3130103)Termination phase: Saturation
% 61.84/9.63 % (3130103)Time elapsed: 0.180 s
% 61.84/9.63 % (3130103)Peak memory usage: 90 MB
% 61.84/9.63 % (3130103)Instructions burned: 412 (million)
% 61.84/9.63 % (3130105)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=1445961018:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 61.84/9.63 % (3130095)Instruction limit reached!
% 61.84/9.63 % (3130095)------------------------------
% 61.84/9.63 % (3130095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.84/9.63 % (3130095)CaDiCaL version: 2.1.3
% 61.84/9.63 % (3130095)Termination reason: Instruction limit
% 61.84/9.63 % (3130095)Termination phase: Saturation
% 61.84/9.63 % (3130095)Time elapsed: 1.995 s
% 61.84/9.63 % (3130095)Peak memory usage: 147 MB
% 61.84/9.63 % (3130095)Instructions burned: 3257 (million)
% 61.84/9.63 % (3130107)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=4149296355:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi)
% 61.84/9.63 % (3130107)Refutation not found, incomplete strategy
% 61.84/9.63 % (3130107)------------------------------
% 61.84/9.63 % (3130107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.84/9.63 % (3130107)CaDiCaL version: 2.1.3
% 61.84/9.63 % (3130107)Termination reason: Refutation not found, incomplete strategy
% 61.84/9.63 % (3130107)Time elapsed: 0.002 s
% 61.84/9.63 % (3130107)Peak memory usage: 88 MB
% 61.84/9.63 % (3130107)Instructions burned: 1 (million)
% 61.84/9.63 % (3130083)Instruction limit reached!
% 61.84/9.63 % (3130083)------------------------------
% 61.84/9.63 % (3130083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.84/9.63 % (3130083)CaDiCaL version: 2.1.3
% 61.84/9.63 % (3130083)Termination reason: Instruction limit
% 61.84/9.63 % (3130083)Termination phase: Saturation
% 61.84/9.63 % (3130083)Time elapsed: 3.236 s
% 61.84/9.63 % (3130083)Peak memory usage: 161 MB
% 61.84/9.63 % (3130083)Instructions burned: 5208 (million)
% 61.84/9.63 % (3130107)------------------------------
% 61.84/9.63 % (3130107)------------------------------
% 61.84/9.63 % (3130109)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4041074071:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 61.84/9.63 % (3130110)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1002253635:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 61.84/9.63 % (3130110)Refutation not found, incomplete strategy
% 61.84/9.63 % (3130110)------------------------------
% 61.84/9.63 % (3130110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.84/9.63 % (3130110)CaDiCaL version: 2.1.3
% 61.84/9.63 % (3130110)Termination reason: Refutation not found, incomplete strategy
% 61.84/9.63 % (3130110)Time elapsed: 0.003 s
% 61.84/9.63 % (3130110)Peak memory usage: 88 MB
% 61.84/9.63 % (3130110)Instructions burned: 3 (million)
% 61.84/9.63 % (3130110)------------------------------
% 61.84/9.63 % (3130110)------------------------------
% 61.84/9.63 % (3130113)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2660110514:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi)
% 61.84/9.63 % (3130109)Instruction limit reached!
% 61.84/9.63 % (3130109)------------------------------
% 61.84/9.63 % (3130109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.84/9.63 % (3130109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130109)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130109)Termination reason: Instruction limit
% 39.22/11.14 % (3130109)Termination phase: Saturation
% 39.22/11.14 % (3130109)Time elapsed: 0.437 s
% 39.22/11.14 % (3130109)Peak memory usage: 95 MB
% 39.22/11.14 % (3130109)Instructions burned: 721 (million)
% 39.22/11.14 % (3130115)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=2619036782:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 39.22/11.14 % (3130101)Instruction limit reached!
% 39.22/11.14 % (3130101)------------------------------
% 39.22/11.14 % (3130101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130101)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130101)Termination reason: Instruction limit
% 39.22/11.14 % (3130101)Termination phase: Saturation
% 39.22/11.14 % (3130101)Time elapsed: 3.427 s
% 39.22/11.14 % (3130101)Peak memory usage: 163 MB
% 39.22/11.14 % (3130101)Instructions burned: 10310 (million)
% 39.22/11.14 % (3130117)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=612849867:i=2088:bd=preordered:av=off_2945 on theBenchmark for (2945ds/2088Mi)
% 39.22/11.14 % (3130115)Instruction limit reached!
% 39.22/11.14 % (3130115)------------------------------
% 39.22/11.14 % (3130115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130115)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130115)Termination reason: Instruction limit
% 39.22/11.14 % (3130115)Termination phase: Saturation
% 39.22/11.14 % (3130115)Time elapsed: 1.301 s
% 39.22/11.14 % (3130115)Peak memory usage: 137 MB
% 39.22/11.14 % (3130115)Instructions burned: 1997 (million)
% 39.22/11.14 % (3130117)Instruction limit reached!
% 39.22/11.14 % (3130117)------------------------------
% 39.22/11.14 % (3130117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130117)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130117)Termination reason: Instruction limit
% 39.22/11.14 % (3130117)Termination phase: Saturation
% 39.22/11.14 % (3130117)Time elapsed: 0.732 s
% 39.22/11.14 % (3130117)Peak memory usage: 137 MB
% 39.22/11.14 % (3130117)Instructions burned: 2090 (million)
% 39.22/11.14 % (3130119)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=457422549:i=1098:nicw=on_2937 on theBenchmark for (2937ds/1098Mi)
% 39.22/11.14 % (3130120)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2360474920:i=433:bd=preordered_2937 on theBenchmark for (2937ds/433Mi)
% 39.22/11.14 % (3130120)Refutation not found, incomplete strategy
% 39.22/11.14 % (3130120)------------------------------
% 39.22/11.14 % (3130120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130120)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130120)Termination reason: Refutation not found, incomplete strategy
% 39.22/11.14 % (3130120)Time elapsed: 0.005 s
% 39.22/11.14 % (3130120)Peak memory usage: 88 MB
% 39.22/11.14 % (3130120)Instructions burned: 16 (million)
% 39.22/11.14 % (3130120)------------------------------
% 39.22/11.14 % (3130120)------------------------------
% 39.22/11.14 % (3130113)Instruction limit reached!
% 39.22/11.14 % (3130113)------------------------------
% 39.22/11.14 % (3130113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130113)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130113)Termination reason: Instruction limit
% 39.22/11.14 % (3130113)Termination phase: Saturation
% 39.22/11.14 % (3130113)Time elapsed: 1.765 s
% 39.22/11.14 % (3130113)Peak memory usage: 147 MB
% 39.22/11.14 % (3130113)Instructions burned: 2990 (million)
% 39.22/11.14 % (3130123)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3678607346:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2934 on theBenchmark for (2934ds/2942Mi)
% 39.22/11.14 % (3130124)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1528519824:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2934 on theBenchmark for (2934ds/6922Mi)
% 39.22/11.14 % (3130119)Instruction limit reached!
% 39.22/11.14 % (3130119)------------------------------
% 39.22/11.14 % (3130119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130119)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130119)Termination reason: Instruction limit
% 39.22/11.14 % (3130119)Termination phase: Saturation
% 39.22/11.14 % (3130119)Time elapsed: 0.657 s
% 39.22/11.14 % (3130119)Peak memory usage: 102 MB
% 39.22/11.14 % (3130119)Instructions burned: 1099 (million)
% 39.22/11.14 % (3130127)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=2020524689:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2929 on theBenchmark for (2929ds/596Mi)
% 39.22/11.14 % (3130127)Instruction limit reached!
% 39.22/11.14 % (3130127)------------------------------
% 39.22/11.14 % (3130127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130127)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130127)Termination reason: Instruction limit
% 39.22/11.14 % (3130127)Termination phase: Saturation
% 39.22/11.14 % (3130127)Time elapsed: 0.323 s
% 39.22/11.14 % (3130127)Peak memory usage: 99 MB
% 39.22/11.14 % (3130127)Instructions burned: 596 (million)
% 39.22/11.14 % (3130105)Instruction limit reached!
% 39.22/11.14 % (3130105)------------------------------
% 39.22/11.14 % (3130105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130105)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130105)Termination reason: Instruction limit
% 39.22/11.14 % (3130105)Termination phase: Saturation
% 39.22/11.14 % (3130105)Time elapsed: 4.942 s
% 39.22/11.14 % (3130105)Peak memory usage: 162 MB
% 39.22/11.14 % (3130105)Instructions burned: 8478 (million)
% 39.22/11.14 % (3130129)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=641109064:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2925 on theBenchmark for (2925ds/4123Mi)
% 39.22/11.14 % (3130123)Instruction limit reached!
% 39.22/11.14 % (3130123)------------------------------
% 39.22/11.14 % (3130123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130123)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130123)Termination reason: Instruction limit
% 39.22/11.14 % (3130123)Termination phase: Saturation
% 39.22/11.14 % (3130123)Time elapsed: 1.007 s
% 39.22/11.14 % (3130123)Peak memory usage: 143 MB
% 39.22/11.14 % (3130123)Instructions burned: 2943 (million)
% 39.22/11.14 % (3130130)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1792398758:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 39.22/11.14 % (3130132)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2992836757:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2923 on theBenchmark for (2923ds/1670Mi)
% 39.22/11.14 % (3130132)Instruction limit reached!
% 39.22/11.14 % (3130132)------------------------------
% 39.22/11.14 % (3130132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130132)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130132)Termination reason: Instruction limit
% 39.22/11.14 % (3130132)Termination phase: Saturation
% 39.22/11.14 % (3130132)Time elapsed: 0.608 s
% 39.22/11.14 % (3130132)Peak memory usage: 137 MB
% 39.22/11.14 % (3130132)Instructions burned: 1671 (million)
% 39.22/11.14 % (3130135)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=1997641350:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2916 on theBenchmark for (2916ds/1722Mi)
% 39.22/11.14 % (3130135)Refutation not found, incomplete strategy
% 39.22/11.14 % (3130135)------------------------------
% 39.22/11.14 % (3130135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.22/11.14 % (3130135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.22/11.14 % (3130135)CaDiCaL version: 2.1.3
% 39.22/11.14 % (3130135)Termination reason: Refutation not found, incomplete strategy
% 39.22/11.14 % (3130135)Time elapsed: 0.342 s
% 39.22/11.14 % (3130135)Peak memory usage: 128 MB
% 39.22/11.14 % (3130135)Instructions burned: 916 (million)
% 39.22/11.14 % (3130135)------------------------------
% 39.22/11.14 % (3130135)------------------------------
% 39.22/11.14 % (3130137)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=1786178233:cts=off:cond=on:i=9530:bs=on:fsd=on_2910 on theBenchmark for (2910ds/9530Mi)
% 39.22/11.14 % (3130137)First to succeed.
% 39.22/11.14 % (3130137)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3130044"
% 39.22/11.14 % (3130137)Refutation found. Thanks to Tanya!
% 39.22/11.14 % SZS status Unsatisfiable for theBenchmark
% 39.22/11.14 % SZS output start Proof for theBenchmark
% See solution above
% 73.32/11.33 % (3130137)------------------------------
% 73.32/11.33 % (3130137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.32/11.33 % (3130137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.32/11.33 % (3130137)CaDiCaL version: 2.1.3
% 73.32/11.33 % (3130137)Termination reason: Refutation
% 73.32/11.33 % (3130137)Time elapsed: 1.082 s
% 73.32/11.33 % (3130137)Peak memory usage: 142 MB
% 73.32/11.33 % (3130137)Instructions burned: 2808 (million)
% 73.32/11.33 % (3130137)------------------------------
% 73.32/11.33 % (3130137)------------------------------
% 73.32/11.33 % (3130044)Success in time 10.27 s
% 73.32/11.33 % Vampire exiting
%------------------------------------------------------------------------------