%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET141-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:16 PM UTC 2026
% Result : Unsatisfiable 6.93s 1.93s
% Output : Refutation 8.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 61
% Syntax : Number of formulae : 441 ( 90 unt; 40 def)
% Number of atoms : 1005 ( 183 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 902 ( 338 ~; 538 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 27 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 18 con; 0-3 aty)
% Number of variables : 246 ( 0 sgn 246 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f101,axiom,
! [X0,X1] : union(singleton(X0),X1) = set_builder(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_set_builder) ).
fof(f102,negated_conjecture,
set_builder(x,set_builder(y,set_builder(y,null_class))) != unordered_pair(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_triple_reduction3_1) ).
fof(f108,plain,
! [X0,X1] : set_builder(X0,X1) = complement(intersection(complement(unordered_pair(X0,X0)),complement(X1))),
inference(definition_unfolding,[],[f101,f26,f12]) ).
fof(f121,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(f152,plain,
unordered_pair(x,y) != complement(intersection(complement(unordered_pair(x,x)),complement(complement(intersection(complement(unordered_pair(y,y)),complement(complement(intersection(complement(unordered_pair(y,y)),complement(null_class))))))))),
inference(definition_unfolding,[],[f102,f108,f108,f108]) ).
fof(f156,definition,
sF0 = unordered_pair(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f157,plain,
unordered_pair(x,y) = sF0,
inference(reorient_equations,[],[f156]) ).
fof(f158,definition,
sF1 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f159,plain,
unordered_pair(x,x) = sF1,
inference(reorient_equations,[],[f158]) ).
fof(f160,definition,
sF2 = complement(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f161,plain,
complement(sF1) = sF2,
inference(reorient_equations,[],[f160]) ).
fof(f162,definition,
sF3 = unordered_pair(y,y),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f163,plain,
unordered_pair(y,y) = sF3,
inference(reorient_equations,[],[f162]) ).
fof(f164,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f165,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f164]) ).
fof(f166,definition,
sF5 = complement(null_class),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f167,plain,
complement(null_class) = sF5,
inference(reorient_equations,[],[f166]) ).
fof(f168,definition,
sF6 = intersection(sF4,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f169,plain,
intersection(sF4,sF5) = sF6,
inference(reorient_equations,[],[f168]) ).
fof(f170,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f171,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f170]) ).
fof(f172,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f173,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f172]) ).
fof(f174,definition,
sF9 = intersection(sF4,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f175,plain,
intersection(sF4,sF8) = sF9,
inference(reorient_equations,[],[f174]) ).
fof(f176,definition,
sF10 = complement(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f177,plain,
complement(sF9) = sF10,
inference(reorient_equations,[],[f176]) ).
fof(f178,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f179,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f178]) ).
fof(f180,definition,
sF12 = intersection(sF2,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f181,plain,
intersection(sF2,sF11) = sF12,
inference(reorient_equations,[],[f180]) ).
fof(f182,definition,
sF13 = complement(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f183,plain,
complement(sF12) = sF13,
inference(reorient_equations,[],[f182]) ).
fof(f184,plain,
sF0 != sF13,
inference(definition_folding,[],[f152,f183,f181,f179,f177,f175,f173,f171,f169,f167,f165,f163,f165,f163,f161,f159,f157]) ).
fof(f185,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF4) ),
inference(superposition,[],[f21,f175]) ).
fof(f187,plain,
! [X0] :
( ~ member(X0,sF12)
| member(X0,sF2) ),
inference(superposition,[],[f21,f181]) ).
fof(f188,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF5)
| member(X0,null_class) ),
inference(superposition,[],[f25,f167]) ).
fof(f189,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF2)
| member(X0,sF1) ),
inference(superposition,[],[f25,f161]) ).
fof(f190,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF4)
| member(X0,sF3) ),
inference(superposition,[],[f25,f165]) ).
fof(f192,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF8)
| member(X0,sF7) ),
inference(superposition,[],[f25,f173]) ).
fof(f193,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF10)
| member(X0,sF9) ),
inference(superposition,[],[f25,f177]) ).
fof(f194,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF11)
| member(X0,sF10) ),
inference(superposition,[],[f25,f179]) ).
fof(f195,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF13)
| member(X0,sF12) ),
inference(superposition,[],[f25,f183]) ).
fof(f196,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF8) ),
inference(superposition,[],[f22,f175]) ).
fof(f198,plain,
! [X0] :
( ~ member(X0,sF12)
| member(X0,sF11) ),
inference(superposition,[],[f22,f181]) ).
fof(f201,plain,
! [X0] :
( ~ member(X0,sF2)
| ~ member(X0,sF1) ),
inference(superposition,[],[f24,f161]) ).
fof(f203,plain,
! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sF6) ),
inference(superposition,[],[f24,f171]) ).
fof(f204,plain,
! [X0] :
( ~ member(X0,sF8)
| ~ member(X0,sF7) ),
inference(superposition,[],[f24,f173]) ).
fof(f205,plain,
! [X0] :
( ~ member(X0,sF10)
| ~ member(X0,sF9) ),
inference(superposition,[],[f24,f177]) ).
fof(f206,plain,
! [X0] :
( ~ member(X0,sF11)
| ~ member(X0,sF10) ),
inference(superposition,[],[f24,f179]) ).
fof(f207,plain,
! [X0] :
( ~ member(X0,sF13)
| ~ member(X0,sF12) ),
inference(superposition,[],[f24,f183]) ).
fof(f208,plain,
! [X0] :
( ~ member(X0,sF0)
| x = X0
| y = X0 ),
inference(superposition,[],[f8,f157]) ).
fof(f209,plain,
! [X0] :
( ~ member(X0,sF3)
| y = X0
| y = X0 ),
inference(superposition,[],[f8,f163]) ).
fof(f210,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0
| x = X0 ),
inference(superposition,[],[f8,f159]) ).
fof(f211,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0 ),
inference(duplicate_literal_removal,[],[f210]) ).
fof(f212,plain,
! [X0] :
( ~ member(X0,sF3)
| y = X0 ),
inference(duplicate_literal_removal,[],[f209]) ).
fof(f215,plain,
( member(x,sF0)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f157]) ).
fof(f217,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f159]) ).
fof(f219,definition,
( spl14_1
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f221,plain,
( ~ member(x,universal_class)
| spl14_1 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f223,definition,
( spl14_2
<=> member(x,sF1) ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f224,plain,
( ~ member(x,sF1)
| spl14_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( member(x,sF1)
| ~ spl14_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,plain,
( ~ spl14_1
| spl14_2 ),
inference(avatar_split_clause,[],[f217,f223,f219]) ).
fof(f228,definition,
( spl14_3
<=> member(y,universal_class) ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f229,plain,
( member(y,universal_class)
| ~ spl14_3 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( ~ member(y,universal_class)
| spl14_3 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f232,definition,
( spl14_4
<=> member(y,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f234,plain,
( member(y,sF3)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f237,definition,
( spl14_5
<=> member(x,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f239,plain,
( member(x,sF0)
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,plain,
( ~ spl14_1
| spl14_5 ),
inference(avatar_split_clause,[],[f215,f237,f219]) ).
fof(f242,plain,
( member(y,sF0)
| ~ member(y,universal_class) ),
inference(superposition,[],[f10,f157]) ).
fof(f243,plain,
( member(y,sF3)
| ~ member(y,universal_class) ),
inference(superposition,[],[f10,f163]) ).
fof(f247,plain,
! [X0] :
( ~ member(X0,sF8)
| member(X0,sF9)
| ~ member(X0,sF4) ),
inference(superposition,[],[f23,f175]) ).
fof(f249,plain,
! [X0] :
( ~ member(X0,sF11)
| member(X0,sF12)
| ~ member(X0,sF2) ),
inference(superposition,[],[f23,f181]) ).
fof(f254,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),X2)
| ~ subclass(X0,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f2,f1]) ).
fof(f264,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f265,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f266,plain,
! [X0,X1] :
( ~ member(not_subclass_element(complement(X0),X1),X0)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f2,f24]) ).
fof(f267,plain,
! [X0] :
( subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| y = not_subclass_element(sF0,X0) ),
inference(resolution,[],[f2,f208]) ).
fof(f286,plain,
! [X0] :
( ~ member(not_subclass_element(sF13,X0),sF12)
| subclass(sF13,X0) ),
inference(resolution,[],[f2,f207]) ).
fof(f289,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(X1)),universal_class)
| subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1) ),
inference(resolution,[],[f3,f25]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X2)
| subclass(X0,intersection(X1,X2))
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1) ),
inference(resolution,[],[f3,f23]) ).
fof(f295,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF5)
| member(not_subclass_element(X0,X1),null_class) ),
inference(resolution,[],[f254,f188]) ).
fof(f296,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF1) ),
inference(resolution,[],[f254,f189]) ).
fof(f297,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF4)
| member(not_subclass_element(X0,X1),sF3) ),
inference(resolution,[],[f254,f190]) ).
fof(f299,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF8)
| member(not_subclass_element(X0,X1),sF7) ),
inference(resolution,[],[f254,f192]) ).
fof(f300,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF9) ),
inference(resolution,[],[f254,f193]) ).
fof(f301,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF11)
| member(not_subclass_element(X0,X1),sF10) ),
inference(resolution,[],[f254,f194]) ).
fof(f302,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF13)
| member(not_subclass_element(X0,X1),sF12) ),
inference(resolution,[],[f254,f195]) ).
fof(f329,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF13)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF12) ),
inference(forward_subsumption_resolution,[],[f302,f4]) ).
fof(f330,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF11)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF10) ),
inference(forward_subsumption_resolution,[],[f301,f4]) ).
fof(f331,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF9) ),
inference(forward_subsumption_resolution,[],[f300,f4]) ).
fof(f332,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF8)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF7) ),
inference(forward_subsumption_resolution,[],[f299,f4]) ).
fof(f334,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF3)
| member(not_subclass_element(X0,X1),sF4)
| subclass(X0,X1) ),
inference(forward_subsumption_resolution,[],[f297,f4]) ).
fof(f335,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF1) ),
inference(forward_subsumption_resolution,[],[f296,f4]) ).
fof(f336,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),null_class)
| member(not_subclass_element(X0,X1),sF5)
| subclass(X0,X1) ),
inference(forward_subsumption_resolution,[],[f295,f4]) ).
fof(f345,plain,
! [X0] :
( subclass(X0,sF13)
| member(not_subclass_element(X0,sF13),sF12)
| subclass(X0,sF13) ),
inference(resolution,[],[f329,f3]) ).
fof(f348,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF12)
| subclass(X0,sF13) ),
inference(duplicate_literal_removal,[],[f345]) ).
fof(f350,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF11)
| subclass(X0,sF13) ),
inference(resolution,[],[f348,f198]) ).
fof(f351,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF2)
| subclass(X0,sF13) ),
inference(resolution,[],[f348,f187]) ).
fof(f354,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF13),sF1)
| subclass(X0,sF13) ),
inference(resolution,[],[f351,f201]) ).
fof(f357,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF13),sF10)
| subclass(X0,sF13) ),
inference(resolution,[],[f350,f206]) ).
fof(f363,plain,
( subclass(sF10,sF13)
| subclass(sF10,sF13) ),
inference(resolution,[],[f357,f2]) ).
fof(f366,plain,
subclass(sF10,sF13),
inference(duplicate_literal_removal,[],[f363]) ).
fof(f368,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1) ),
inference(resolution,[],[f330,f249]) ).
fof(f379,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF4)
| subclass(X0,X1)
| not_subclass_element(X0,X1) = y ),
inference(resolution,[],[f334,f212]) ).
fof(f383,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF4)
| member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1) ),
inference(resolution,[],[f332,f247]) ).
fof(f391,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF1)
| member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1) ),
inference(resolution,[],[f335,f368]) ).
fof(f396,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| member(not_subclass_element(X0,X1),sF1)
| member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f391]) ).
fof(f397,plain,
! [X0] :
( subclass(X0,sF13)
| member(not_subclass_element(X0,sF13),sF9)
| subclass(X0,sF13) ),
inference(resolution,[],[f331,f357]) ).
fof(f402,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF9)
| subclass(X0,sF13) ),
inference(duplicate_literal_removal,[],[f397]) ).
fof(f403,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF8)
| subclass(X0,sF13) ),
inference(resolution,[],[f402,f196]) ).
fof(f404,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF4)
| subclass(X0,sF13) ),
inference(resolution,[],[f402,f185]) ).
fof(f407,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF13),sF7)
| subclass(X0,sF13) ),
inference(resolution,[],[f403,f204]) ).
fof(f409,plain,
( subclass(sF7,sF13)
| subclass(sF7,sF13) ),
inference(resolution,[],[f407,f2]) ).
fof(f412,plain,
subclass(sF7,sF13),
inference(duplicate_literal_removal,[],[f409]) ).
fof(f435,plain,
! [X0,X1] :
( subclass(X0,X1)
| not_subclass_element(X0,X1) = y
| member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1) ),
inference(resolution,[],[f379,f383]) ).
fof(f440,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF9)
| not_subclass_element(X0,X1) = y
| member(not_subclass_element(X0,X1),sF7)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f435]) ).
fof(f446,plain,
! [X0] :
( member(not_subclass_element(sF13,X0),sF1)
| member(not_subclass_element(sF13,X0),sF10)
| subclass(sF13,X0)
| subclass(sF13,X0) ),
inference(resolution,[],[f396,f286]) ).
fof(f452,plain,
! [X0] :
( member(not_subclass_element(sF13,X0),sF10)
| member(not_subclass_element(sF13,X0),sF1)
| subclass(sF13,X0) ),
inference(duplicate_literal_removal,[],[f446]) ).
fof(f455,plain,
! [X0] :
( ~ member(not_subclass_element(sF13,X0),sF9)
| subclass(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1) ),
inference(resolution,[],[f452,f205]) ).
fof(f460,definition,
( spl14_8
<=> subclass(sF13,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f461,plain,
( ~ subclass(sF13,sF10)
| spl14_8 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f462,plain,
( subclass(sF13,sF10)
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f460]) ).
fof(f468,plain,
! [X0] :
( subclass(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1)
| y = not_subclass_element(sF13,X0)
| member(not_subclass_element(sF13,X0),sF7)
| subclass(sF13,X0) ),
inference(resolution,[],[f455,f440]) ).
fof(f473,plain,
! [X0] :
( member(not_subclass_element(sF13,X0),sF7)
| member(not_subclass_element(sF13,X0),sF1)
| y = not_subclass_element(sF13,X0)
| subclass(sF13,X0) ),
inference(duplicate_literal_removal,[],[f468]) ).
fof(f484,plain,
! [X0] :
( ~ member(not_subclass_element(sF13,X0),sF6)
| y = not_subclass_element(sF13,X0)
| subclass(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1) ),
inference(resolution,[],[f473,f203]) ).
fof(f489,definition,
( spl14_12
<=> subclass(sF13,sF7) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f490,plain,
( ~ subclass(sF13,sF7)
| spl14_12 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( subclass(sF13,sF7)
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f510,definition,
( spl14_16
<=> ! [X0] :
( y = not_subclass_element(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1)
| subclass(sF13,X0) ) ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
fof(f511,plain,
( ! [X0] :
( member(not_subclass_element(sF13,X0),sF1)
| y = not_subclass_element(sF13,X0)
| subclass(sF13,X0) )
| ~ spl14_16 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f525,plain,
! [X0,X1] :
( subclass(X0,intersection(X1,X0))
| ~ member(not_subclass_element(X0,intersection(X1,X0)),X1)
| subclass(X0,intersection(X1,X0)) ),
inference(resolution,[],[f290,f2]) ).
fof(f526,plain,
! [X2,X0,X1] :
( subclass(X0,intersection(X1,X2))
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| ~ subclass(X0,X2)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f290,f254]) ).
fof(f559,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2))
| ~ subclass(X0,X2) ),
inference(duplicate_literal_removal,[],[f526]) ).
fof(f560,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X0)),X1)
| subclass(X0,intersection(X1,X0)) ),
inference(duplicate_literal_removal,[],[f525]) ).
fof(f576,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f265,f3]) ).
fof(f631,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f576]) ).
fof(f632,plain,
( ~ subclass(sF10,sF13)
| sF10 = sF13
| ~ spl14_8 ),
inference(resolution,[],[f462,f7]) ).
fof(f633,plain,
( sF10 = sF13
| ~ spl14_8 ),
inference(forward_subsumption_resolution,[],[f632,f366]) ).
fof(f660,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f631,f70]) ).
fof(f661,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f660,f7]) ).
fof(f662,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f661]) ).
fof(f663,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f662,f631]) ).
fof(f684,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f22,f663]) ).
fof(f726,definition,
( spl14_26
<=> member(y,sF4) ),
introduced(definition,[new_symbols(definition,[spl14_26])],[avatar_definition]) ).
fof(f728,plain,
( ~ member(y,sF4)
| spl14_26 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f750,definition,
( spl14_30
<=> member(y,sF11) ),
introduced(definition,[new_symbols(definition,[spl14_30])],[avatar_definition]) ).
fof(f751,plain,
( ~ member(y,sF11)
| spl14_30 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f752,plain,
( member(y,sF11)
| ~ spl14_30 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f765,definition,
( spl14_33
<=> member(y,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
fof(f767,plain,
( member(y,sF0)
| ~ spl14_33 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f809,definition,
( spl14_39
<=> member(x,sF12) ),
introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition]) ).
fof(f810,plain,
( ~ member(x,sF12)
| spl14_39 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f811,plain,
( member(x,sF12)
| ~ spl14_39 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f843,definition,
( spl14_45
<=> member(x,sF11) ),
introduced(definition,[new_symbols(definition,[spl14_45])],[avatar_definition]) ).
fof(f844,plain,
( ~ member(x,sF11)
| spl14_45 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f845,plain,
( member(x,sF11)
| ~ spl14_45 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f867,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f264,f3]) ).
fof(f923,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f867]) ).
fof(f934,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f559,f2]) ).
fof(f974,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f934]) ).
fof(f985,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f974,f7]) ).
fof(f1019,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f985,f631]) ).
fof(f1020,plain,
! [X0] : intersection(X0,universal_class) = X0,
inference(resolution,[],[f1019,f4]) ).
fof(f1024,plain,
! [X0] :
( y = not_subclass_element(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(resolution,[],[f1019,f267]) ).
fof(f1029,plain,
! [X0,X1] :
( ~ member(X1,X0)
| member(X1,universal_class) ),
inference(superposition,[],[f22,f1020]) ).
fof(f1031,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(superposition,[],[f264,f1020]) ).
fof(f1065,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f121,f663]) ).
fof(f1066,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f1065]) ).
fof(f1124,plain,
( ~ subclass(sF7,sF13)
| sF7 = sF13
| ~ spl14_12 ),
inference(resolution,[],[f491,f7]) ).
fof(f1126,plain,
( sF7 = sF13
| ~ spl14_12 ),
inference(forward_subsumption_resolution,[],[f1124,f412]) ).
fof(f1174,plain,
! [X0,X1] :
( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(resolution,[],[f68,f8]) ).
fof(f1180,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f68,f1066]) ).
fof(f1320,definition,
( spl14_81
<=> null_class = sF1 ),
introduced(definition,[new_symbols(definition,[spl14_81])],[avatar_definition]) ).
fof(f1322,plain,
( null_class = sF1
| ~ spl14_81 ),
inference(avatar_component_clause,[],[f1320]) ).
fof(f1405,plain,
( ~ subclass(sF10,sF7)
| ~ spl14_8
| spl14_12 ),
inference(forward_demodulation,[],[f490,f633]) ).
fof(f1497,plain,
! [X0] : ~ member(X0,null_class),
inference(superposition,[],[f1066,f1180]) ).
fof(f1509,plain,
! [X0,X1] :
( X0 != X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(equality_factoring,[],[f1174]) ).
fof(f1771,plain,
( ! [X0] : ~ member(X0,domain_of(sF1))
| ~ spl14_81 ),
inference(superposition,[],[f1066,f1322]) ).
fof(f1772,plain,
( sF1 = domain_of(sF1)
| ~ spl14_81 ),
inference(superposition,[],[f1180,f1322]) ).
fof(f1773,plain,
( ! [X0] : ~ member(X0,sF1)
| ~ spl14_81 ),
inference(forward_demodulation,[],[f1771,f1772]) ).
fof(f1798,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF5)
| subclass(X0,X1) ),
inference(resolution,[],[f1497,f336]) ).
fof(f1810,plain,
! [X0] :
( regular(unordered_pair(X0,X0)) = X0
| unordered_pair(X0,X0) = null_class ),
inference(equality_resolution,[],[f1509]) ).
fof(f1984,plain,
! [X0,X1] :
( subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1)
| ~ subclass(X0,universal_class)
| subclass(X0,complement(X1)) ),
inference(resolution,[],[f289,f254]) ).
fof(f1987,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF5),universal_class)
| subclass(X0,sF5)
| member(not_subclass_element(X0,sF5),null_class) ),
inference(superposition,[],[f289,f167]) ).
fof(f1997,plain,
! [X0,X1] :
( subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1)
| ~ subclass(X0,universal_class) ),
inference(duplicate_literal_removal,[],[f1984]) ).
fof(f2006,plain,
! [X0] :
( subclass(X0,sF5)
| member(not_subclass_element(X0,sF5),null_class) ),
inference(forward_subsumption_resolution,[],[f1987,f1031]) ).
fof(f2008,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(forward_subsumption_resolution,[],[f1997,f4]) ).
fof(f2010,plain,
! [X0] : subclass(X0,sF5),
inference(forward_subsumption_resolution,[],[f2006,f1497]) ).
fof(f2019,plain,
( subclass(sF13,complement(sF9))
| subclass(sF13,complement(sF9))
| member(not_subclass_element(sF13,complement(sF9)),sF1) ),
inference(resolution,[],[f2008,f455]) ).
fof(f2034,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(complement(X1))),X1)
| subclass(X0,complement(complement(X1))) ),
inference(resolution,[],[f2008,f24]) ).
fof(f2051,plain,
! [X0] :
( subclass(X0,complement(sF9))
| member(not_subclass_element(X0,complement(sF9)),sF8) ),
inference(resolution,[],[f2008,f196]) ).
fof(f2069,plain,
( subclass(sF13,complement(sF9))
| member(not_subclass_element(sF13,complement(sF9)),sF1) ),
inference(duplicate_literal_removal,[],[f2019]) ).
fof(f2081,plain,
! [X0] :
( subclass(X0,sF10)
| member(not_subclass_element(X0,complement(sF9)),sF8) ),
inference(forward_demodulation,[],[f2051,f177]) ).
fof(f2093,plain,
( subclass(sF13,complement(sF9))
| ~ spl14_81 ),
inference(forward_subsumption_resolution,[],[f2069,f1773]) ).
fof(f2099,plain,
! [X0] :
( member(not_subclass_element(X0,sF10),sF8)
| subclass(X0,sF10) ),
inference(forward_demodulation,[],[f2081,f177]) ).
fof(f2106,plain,
( subclass(sF13,sF10)
| ~ spl14_81 ),
inference(forward_demodulation,[],[f2093,f177]) ).
fof(f2701,plain,
! [X0] :
( member(y,null_class)
| member(y,sF5)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(superposition,[],[f336,f1024]) ).
fof(f2721,plain,
( member(y,sF4)
| subclass(sF0,sF13)
| x = not_subclass_element(sF0,sF13)
| sF0 = intersection(sF0,sF13) ),
inference(superposition,[],[f404,f1024]) ).
fof(f2729,definition,
( spl14_120
<=> ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl14_120])],[avatar_definition]) ).
fof(f2730,plain,
( ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) )
| ~ spl14_120 ),
inference(avatar_component_clause,[],[f2729]) ).
fof(f2735,plain,
( member(y,sF4)
| x = not_subclass_element(sF0,sF13)
| sF0 = intersection(sF0,sF13) ),
inference(forward_subsumption_resolution,[],[f2721,f1019]) ).
fof(f2753,plain,
! [X0] :
( member(y,sF5)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f2701,f684]) ).
fof(f2781,plain,
! [X0] :
( member(y,sF5)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f2753,f1019]) ).
fof(f2855,plain,
( ! [X0] :
( ~ member(x,X0)
| subclass(sF0,X0)
| sF0 = intersection(sF0,X0) )
| ~ spl14_120 ),
inference(superposition,[],[f3,f2730]) ).
fof(f2880,plain,
( member(x,sF12)
| subclass(sF0,sF13)
| sF0 = intersection(sF0,sF13)
| ~ spl14_120 ),
inference(superposition,[],[f348,f2730]) ).
fof(f2903,plain,
( member(x,sF12)
| sF0 = intersection(sF0,sF13)
| ~ spl14_120 ),
inference(forward_subsumption_resolution,[],[f2880,f1019]) ).
fof(f2927,plain,
( ! [X0] :
( ~ member(x,X0)
| sF0 = intersection(sF0,X0) )
| ~ spl14_120 ),
inference(forward_subsumption_resolution,[],[f2855,f1019]) ).
fof(f3146,plain,
( $false
| spl14_8
| ~ spl14_81 ),
inference(forward_subsumption_resolution,[],[f2106,f461]) ).
fof(f3147,plain,
( spl14_8
| ~ spl14_81 ),
inference(avatar_contradiction_clause,[],[f3146]) ).
fof(f3216,plain,
( member(y,sF3)
| ~ spl14_3 ),
inference(forward_subsumption_resolution,[],[f243,f229]) ).
fof(f3518,plain,
( member(y,sF0)
| ~ spl14_3 ),
inference(forward_subsumption_resolution,[],[f242,f229]) ).
fof(f3527,plain,
( member(x,universal_class)
| ~ spl14_2 ),
inference(resolution,[],[f225,f1029]) ).
fof(f3647,plain,
! [X0] : intersection(X0,sF5) = X0,
inference(resolution,[],[f2010,f1019]) ).
fof(f3667,plain,
sF4 = sF6,
inference(superposition,[],[f169,f3647]) ).
fof(f3668,plain,
sF7 = complement(sF4),
inference(superposition,[],[f171,f3667]) ).
fof(f3672,plain,
! [X0] :
( ~ member(not_subclass_element(sF13,X0),sF4)
| y = not_subclass_element(sF13,X0)
| subclass(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1) ),
inference(superposition,[],[f484,f3667]) ).
fof(f3839,plain,
( ~ member(y,sF10)
| ~ spl14_30 ),
inference(resolution,[],[f752,f206]) ).
fof(f3852,plain,
( member(x,universal_class)
| ~ spl14_45 ),
inference(resolution,[],[f845,f1029]) ).
fof(f3856,plain,
! [X0] :
( member(X0,unordered_pair(X0,X0))
| unordered_pair(X0,X0) = null_class
| unordered_pair(X0,X0) = null_class ),
inference(superposition,[],[f68,f1810]) ).
fof(f3859,plain,
! [X0] :
( member(X0,unordered_pair(X0,X0))
| unordered_pair(X0,X0) = null_class ),
inference(duplicate_literal_removal,[],[f3856]) ).
fof(f4180,plain,
( member(x,sF11)
| ~ spl14_39 ),
inference(resolution,[],[f811,f198]) ).
fof(f4186,plain,
( $false
| ~ spl14_39
| spl14_45 ),
inference(forward_subsumption_resolution,[],[f4180,f844]) ).
fof(f4187,plain,
( ~ spl14_39
| spl14_45 ),
inference(avatar_contradiction_clause,[],[f4186]) ).
fof(f4191,plain,
( sF0 = intersection(sF0,sF13)
| spl14_39
| ~ spl14_120 ),
inference(forward_subsumption_resolution,[],[f2903,f810]) ).
fof(f4302,plain,
! [X0,X1] :
( subclass(complement(complement(X0)),X1)
| ~ member(not_subclass_element(complement(complement(X0)),X1),universal_class)
| member(not_subclass_element(complement(complement(X0)),X1),X0) ),
inference(resolution,[],[f266,f25]) ).
fof(f4335,plain,
! [X0,X1] :
( member(not_subclass_element(complement(complement(X0)),X1),X0)
| subclass(complement(complement(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f4302,f1031]) ).
fof(f4945,plain,
! [X0] :
( subclass(X0,intersection(sF5,X0))
| subclass(X0,intersection(sF5,X0)) ),
inference(resolution,[],[f1798,f560]) ).
fof(f4955,plain,
! [X0] : subclass(X0,intersection(sF5,X0)),
inference(duplicate_literal_removal,[],[f4945]) ).
fof(f5032,plain,
! [X0] :
( subclass(X0,complement(complement(X0)))
| subclass(X0,complement(complement(X0))) ),
inference(resolution,[],[f2034,f2]) ).
fof(f5089,plain,
! [X0] : subclass(X0,complement(complement(X0))),
inference(duplicate_literal_removal,[],[f5032]) ).
fof(f5187,plain,
! [X0] : intersection(X0,complement(complement(X0))) = X0,
inference(resolution,[],[f5089,f1019]) ).
fof(f5197,plain,
subclass(sF9,complement(sF10)),
inference(superposition,[],[f5089,f177]) ).
fof(f5201,plain,
subclass(sF9,sF11),
inference(forward_demodulation,[],[f5197,f179]) ).
fof(f5219,plain,
sF4 = intersection(sF4,complement(sF7)),
inference(superposition,[],[f5187,f3668]) ).
fof(f5245,plain,
sF4 = intersection(sF4,sF8),
inference(forward_demodulation,[],[f5219,f173]) ).
fof(f5251,plain,
sF4 = sF9,
inference(forward_demodulation,[],[f5245,f175]) ).
fof(f5255,plain,
sF10 = complement(sF4),
inference(superposition,[],[f177,f5251]) ).
fof(f5266,plain,
sF7 = sF10,
inference(forward_demodulation,[],[f5255,f3668]) ).
fof(f5271,plain,
complement(sF7) = sF11,
inference(superposition,[],[f179,f5266]) ).
fof(f5276,plain,
( subclass(sF13,sF7)
| ~ spl14_8 ),
inference(superposition,[],[f462,f5266]) ).
fof(f5279,plain,
( subclass(sF10,sF7)
| ~ spl14_8 ),
inference(forward_demodulation,[],[f5276,f633]) ).
fof(f5283,plain,
sF8 = sF11,
inference(forward_demodulation,[],[f5271,f173]) ).
fof(f5284,plain,
( $false
| ~ spl14_8
| spl14_12 ),
inference(forward_subsumption_resolution,[],[f5279,f1405]) ).
fof(f5285,plain,
( ~ spl14_8
| spl14_12 ),
inference(avatar_contradiction_clause,[],[f5284]) ).
fof(f5400,plain,
( ~ subclass(sF11,sF9)
| sF9 = sF11 ),
inference(resolution,[],[f5201,f7]) ).
fof(f5405,plain,
( ~ subclass(sF11,sF4)
| sF9 = sF11 ),
inference(forward_demodulation,[],[f5400,f5251]) ).
fof(f5406,plain,
( ~ subclass(sF8,sF4)
| sF9 = sF11 ),
inference(forward_demodulation,[],[f5405,f5283]) ).
fof(f5407,plain,
( sF8 = sF9
| ~ subclass(sF8,sF4) ),
inference(forward_demodulation,[],[f5406,f5283]) ).
fof(f5408,plain,
( sF4 = sF8
| ~ subclass(sF8,sF4) ),
inference(forward_demodulation,[],[f5407,f5251]) ).
fof(f5410,definition,
( spl14_157
<=> subclass(sF8,sF4) ),
introduced(definition,[new_symbols(definition,[spl14_157])],[avatar_definition]) ).
fof(f5412,plain,
( ~ subclass(sF8,sF4)
| spl14_157 ),
inference(avatar_component_clause,[],[f5410]) ).
fof(f5414,definition,
( spl14_158
<=> sF4 = sF8 ),
introduced(definition,[new_symbols(definition,[spl14_158])],[avatar_definition]) ).
fof(f5416,plain,
( sF4 = sF8
| ~ spl14_158 ),
inference(avatar_component_clause,[],[f5414]) ).
fof(f5417,plain,
( ~ spl14_157
| spl14_158 ),
inference(avatar_split_clause,[],[f5408,f5414,f5410]) ).
fof(f5429,plain,
( member(x,sF1)
| null_class = sF1 ),
inference(superposition,[],[f3859,f159]) ).
fof(f5478,plain,
! [X0] :
( ~ subclass(intersection(sF5,X0),X0)
| intersection(sF5,X0) = X0 ),
inference(resolution,[],[f4955,f7]) ).
fof(f5494,plain,
! [X0] : intersection(sF5,X0) = X0,
inference(forward_subsumption_resolution,[],[f5478,f923]) ).
fof(f5518,plain,
universal_class = sF5,
inference(superposition,[],[f1020,f5494]) ).
fof(f5589,plain,
! [X0] :
( subclass(complement(complement(X0)),X0)
| subclass(complement(complement(X0)),X0) ),
inference(resolution,[],[f4335,f3]) ).
fof(f5672,plain,
! [X0] : subclass(complement(complement(X0)),X0),
inference(duplicate_literal_removal,[],[f5589]) ).
fof(f5862,plain,
! [X0] :
( ~ subclass(X0,complement(complement(X0)))
| complement(complement(X0)) = X0 ),
inference(resolution,[],[f5672,f7]) ).
fof(f5872,plain,
subclass(complement(sF10),sF9),
inference(superposition,[],[f5672,f177]) ).
fof(f5876,plain,
subclass(complement(sF10),sF4),
inference(forward_demodulation,[],[f5872,f5251]) ).
fof(f5884,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f5862,f5089]) ).
fof(f5886,plain,
subclass(sF11,sF4),
inference(forward_demodulation,[],[f5876,f179]) ).
fof(f5894,plain,
subclass(sF8,sF4),
inference(forward_demodulation,[],[f5886,f5283]) ).
fof(f5898,plain,
( $false
| spl14_157 ),
inference(forward_subsumption_resolution,[],[f5894,f5412]) ).
fof(f5899,plain,
spl14_157,
inference(avatar_contradiction_clause,[],[f5898]) ).
fof(f5905,plain,
sF3 = complement(sF4),
inference(superposition,[],[f5884,f165]) ).
fof(f5940,plain,
sF3 = sF7,
inference(forward_demodulation,[],[f5905,f3668]) ).
fof(f8398,plain,
( member(y,sF8)
| subclass(sF0,sF10)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(superposition,[],[f2099,f1024]) ).
fof(f8401,plain,
( member(y,sF8)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(forward_subsumption_resolution,[],[f8398,f1019]) ).
fof(f8403,plain,
( member(y,sF4)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10)
| ~ spl14_158 ),
inference(forward_demodulation,[],[f8401,f5416]) ).
fof(f9142,plain,
! [X0] :
( y = not_subclass_element(sF13,X0)
| subclass(sF13,X0)
| member(not_subclass_element(sF13,X0),sF1) ),
inference(forward_subsumption_resolution,[],[f3672,f379]) ).
fof(f9848,plain,
( spl14_33
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f3518,f228,f765]) ).
fof(f9858,definition,
( spl14_184
<=> sF0 = intersection(sF0,sF13) ),
introduced(definition,[new_symbols(definition,[spl14_184])],[avatar_definition]) ).
fof(f9860,plain,
( sF0 = intersection(sF0,sF13)
| ~ spl14_184 ),
inference(avatar_component_clause,[],[f9858]) ).
fof(f9862,definition,
( spl14_185
<=> x = not_subclass_element(sF0,sF13) ),
introduced(definition,[new_symbols(definition,[spl14_185])],[avatar_definition]) ).
fof(f9864,plain,
( x = not_subclass_element(sF0,sF13)
| ~ spl14_185 ),
inference(avatar_component_clause,[],[f9862]) ).
fof(f9865,plain,
( spl14_184
| spl14_185
| spl14_26 ),
inference(avatar_split_clause,[],[f2735,f726,f9862,f9858]) ).
fof(f9875,plain,
! [X0] :
( member(y,universal_class)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_demodulation,[],[f2781,f5518]) ).
fof(f9876,plain,
( ~ member(y,sF8)
| spl14_30 ),
inference(forward_demodulation,[],[f751,f5283]) ).
fof(f9932,definition,
( spl14_193
<=> x = not_subclass_element(sF0,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_193])],[avatar_definition]) ).
fof(f9934,plain,
( x = not_subclass_element(sF0,sF3)
| ~ spl14_193 ),
inference(avatar_component_clause,[],[f9932]) ).
fof(f9969,plain,
( spl14_184
| spl14_39
| ~ spl14_120 ),
inference(avatar_split_clause,[],[f4191,f2729,f809,f9858]) ).
fof(f10030,plain,
( ~ member(y,sF4)
| spl14_30
| ~ spl14_158 ),
inference(forward_demodulation,[],[f9876,f5416]) ).
fof(f10072,plain,
( ~ spl14_26
| spl14_30
| ~ spl14_158 ),
inference(avatar_split_clause,[],[f10030,f5414,f750,f726]) ).
fof(f10092,plain,
( ~ member(y,sF7)
| ~ spl14_30 ),
inference(forward_demodulation,[],[f3839,f5266]) ).
fof(f10130,plain,
( ~ member(y,sF3)
| ~ spl14_30 ),
inference(forward_demodulation,[],[f10092,f5940]) ).
fof(f10163,plain,
( $false
| ~ spl14_4
| ~ spl14_30 ),
inference(forward_subsumption_resolution,[],[f10130,f234]) ).
fof(f10164,plain,
( ~ spl14_4
| ~ spl14_30 ),
inference(avatar_contradiction_clause,[],[f10163]) ).
fof(f10226,plain,
( ~ member(x,sF1)
| subclass(sF0,sF13)
| ~ spl14_185 ),
inference(superposition,[],[f354,f9864]) ).
fof(f10273,plain,
( subclass(sF0,sF13)
| ~ spl14_2
| ~ spl14_185 ),
inference(forward_subsumption_resolution,[],[f10226,f225]) ).
fof(f10315,definition,
( spl14_204
<=> subclass(sF0,sF13) ),
introduced(definition,[new_symbols(definition,[spl14_204])],[avatar_definition]) ).
fof(f10316,plain,
( ~ subclass(sF0,sF13)
| spl14_204 ),
inference(avatar_component_clause,[],[f10315]) ).
fof(f10317,plain,
( subclass(sF0,sF13)
| ~ spl14_204 ),
inference(avatar_component_clause,[],[f10315]) ).
fof(f10319,definition,
( spl14_205
<=> member(x,sF13) ),
introduced(definition,[new_symbols(definition,[spl14_205])],[avatar_definition]) ).
fof(f10320,plain,
( member(x,sF13)
| ~ spl14_205 ),
inference(avatar_component_clause,[],[f10319]) ).
fof(f10321,plain,
( ~ member(x,sF13)
| spl14_205 ),
inference(avatar_component_clause,[],[f10319]) ).
fof(f10323,plain,
( spl14_204
| ~ spl14_2
| ~ spl14_185 ),
inference(avatar_split_clause,[],[f10273,f9862,f223,f10315]) ).
fof(f10327,plain,
( ~ subclass(sF13,sF0)
| sF0 = sF13
| ~ spl14_204 ),
inference(resolution,[],[f10317,f7]) ).
fof(f10328,plain,
( ~ subclass(sF13,sF0)
| ~ spl14_204 ),
inference(forward_subsumption_resolution,[],[f10327,f184]) ).
fof(f10499,plain,
( subclass(sF0,sF13)
| ~ spl14_184 ),
inference(superposition,[],[f923,f9860]) ).
fof(f10513,plain,
( spl14_204
| ~ spl14_184 ),
inference(avatar_split_clause,[],[f10499,f9858,f10315]) ).
fof(f10562,plain,
( member(x,universal_class)
| ~ spl14_205 ),
inference(resolution,[],[f10320,f1029]) ).
fof(f10593,plain,
spl14_16,
inference(avatar_split_clause,[],[f9142,f510]) ).
fof(f10848,plain,
( sF3 = sF13
| ~ spl14_12 ),
inference(forward_demodulation,[],[f1126,f5940]) ).
fof(f10859,plain,
( sF0 = intersection(sF0,sF1)
| ~ spl14_2
| ~ spl14_120 ),
inference(resolution,[],[f2927,f225]) ).
fof(f10881,plain,
( ! [X0] :
( member(not_subclass_element(sF0,X0),sF1)
| subclass(sF0,X0) )
| ~ spl14_2
| ~ spl14_120 ),
inference(superposition,[],[f264,f10859]) ).
fof(f10910,plain,
( subclass(sF0,sF13)
| subclass(sF0,sF13)
| ~ spl14_2
| ~ spl14_120 ),
inference(resolution,[],[f10881,f354]) ).
fof(f10996,plain,
( x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10)
| spl14_26
| ~ spl14_158 ),
inference(forward_subsumption_resolution,[],[f8403,f728]) ).
fof(f11001,definition,
( spl14_209
<=> sF0 = intersection(sF0,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_209])],[avatar_definition]) ).
fof(f11003,plain,
( sF0 = intersection(sF0,sF3)
| ~ spl14_209 ),
inference(avatar_component_clause,[],[f11001]) ).
fof(f11024,plain,
( x = not_subclass_element(sF0,sF7)
| sF0 = intersection(sF0,sF10)
| spl14_26
| ~ spl14_158 ),
inference(forward_demodulation,[],[f10996,f5266]) ).
fof(f11032,plain,
( x = not_subclass_element(sF0,sF3)
| sF0 = intersection(sF0,sF10)
| spl14_26
| ~ spl14_158 ),
inference(forward_demodulation,[],[f11024,f5940]) ).
fof(f11039,plain,
( sF0 = intersection(sF0,sF7)
| x = not_subclass_element(sF0,sF3)
| spl14_26
| ~ spl14_158 ),
inference(forward_demodulation,[],[f11032,f5266]) ).
fof(f11044,plain,
( sF0 = intersection(sF0,sF3)
| x = not_subclass_element(sF0,sF3)
| spl14_26
| ~ spl14_158 ),
inference(forward_demodulation,[],[f11039,f5940]) ).
fof(f11047,plain,
( spl14_193
| spl14_209
| spl14_26
| ~ spl14_158 ),
inference(avatar_split_clause,[],[f11044,f5414,f726,f11001,f9932]) ).
fof(f11096,plain,
( subclass(sF0,sF3)
| ~ spl14_209 ),
inference(superposition,[],[f923,f11003]) ).
fof(f11360,plain,
( member(x,sF13)
| subclass(sF0,sF3)
| member(x,sF12)
| ~ spl14_193 ),
inference(superposition,[],[f329,f9934]) ).
fof(f11661,plain,
( ! [X0] :
( subclass(sF13,X0)
| y = not_subclass_element(sF13,X0)
| x = not_subclass_element(sF13,X0) )
| ~ spl14_16 ),
inference(resolution,[],[f511,f211]) ).
fof(f11676,plain,
( y = not_subclass_element(sF13,sF0)
| x = not_subclass_element(sF13,sF0)
| ~ spl14_16
| ~ spl14_204 ),
inference(resolution,[],[f11661,f10328]) ).
fof(f11686,definition,
( spl14_220
<=> x = not_subclass_element(sF13,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_220])],[avatar_definition]) ).
fof(f11688,plain,
( x = not_subclass_element(sF13,sF0)
| ~ spl14_220 ),
inference(avatar_component_clause,[],[f11686]) ).
fof(f11690,definition,
( spl14_221
<=> y = not_subclass_element(sF13,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_221])],[avatar_definition]) ).
fof(f11692,plain,
( y = not_subclass_element(sF13,sF0)
| ~ spl14_221 ),
inference(avatar_component_clause,[],[f11690]) ).
fof(f11693,plain,
( spl14_220
| spl14_221
| ~ spl14_16
| ~ spl14_204 ),
inference(avatar_split_clause,[],[f11676,f10315,f510,f11690,f11686]) ).
fof(f11731,plain,
( ~ member(y,sF0)
| subclass(sF13,sF0)
| ~ spl14_221 ),
inference(superposition,[],[f3,f11692]) ).
fof(f11740,plain,
( member(y,null_class)
| member(y,sF5)
| subclass(sF13,sF0)
| ~ spl14_221 ),
inference(superposition,[],[f336,f11692]) ).
fof(f11758,plain,
( member(y,sF5)
| subclass(sF13,sF0)
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f11740,f684]) ).
fof(f11763,plain,
( subclass(sF13,sF0)
| ~ spl14_33
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f11731,f767]) ).
fof(f11773,plain,
( member(y,sF5)
| ~ spl14_204
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f11758,f10328]) ).
fof(f11778,plain,
( $false
| ~ spl14_33
| ~ spl14_204
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f11763,f10328]) ).
fof(f11779,plain,
( ~ spl14_33
| ~ spl14_204
| ~ spl14_221 ),
inference(avatar_contradiction_clause,[],[f11778]) ).
fof(f11787,plain,
( member(y,universal_class)
| ~ spl14_204
| ~ spl14_221 ),
inference(forward_demodulation,[],[f11773,f5518]) ).
fof(f11812,plain,
( ~ member(x,sF0)
| subclass(sF13,sF0)
| ~ spl14_220 ),
inference(superposition,[],[f3,f11688]) ).
fof(f11829,plain,
( member(x,universal_class)
| subclass(sF13,sF0)
| ~ spl14_220 ),
inference(superposition,[],[f1031,f11688]) ).
fof(f11841,plain,
( subclass(sF13,sF0)
| ~ spl14_5
| ~ spl14_220 ),
inference(forward_subsumption_resolution,[],[f11812,f239]) ).
fof(f11849,plain,
( $false
| ~ spl14_5
| ~ spl14_204
| ~ spl14_220 ),
inference(forward_subsumption_resolution,[],[f11841,f10328]) ).
fof(f11850,plain,
( ~ spl14_5
| ~ spl14_204
| ~ spl14_220 ),
inference(avatar_contradiction_clause,[],[f11849]) ).
fof(f11868,plain,
( $false
| spl14_1
| ~ spl14_2 ),
inference(forward_subsumption_resolution,[],[f3527,f221]) ).
fof(f11869,plain,
( spl14_1
| ~ spl14_2 ),
inference(avatar_contradiction_clause,[],[f11868]) ).
fof(f11880,plain,
( $false
| spl14_1
| ~ spl14_45 ),
inference(forward_subsumption_resolution,[],[f3852,f221]) ).
fof(f11881,plain,
( spl14_1
| ~ spl14_45 ),
inference(avatar_contradiction_clause,[],[f11880]) ).
fof(f11884,plain,
( $false
| spl14_1
| ~ spl14_205 ),
inference(forward_subsumption_resolution,[],[f10562,f221]) ).
fof(f11885,plain,
( spl14_1
| ~ spl14_205 ),
inference(avatar_contradiction_clause,[],[f11884]) ).
fof(f11887,plain,
( subclass(sF13,sF0)
| spl14_1
| ~ spl14_220 ),
inference(forward_subsumption_resolution,[],[f11829,f221]) ).
fof(f11895,plain,
( $false
| spl14_1
| ~ spl14_204
| ~ spl14_220 ),
inference(forward_subsumption_resolution,[],[f11887,f10328]) ).
fof(f11896,plain,
( spl14_1
| ~ spl14_204
| ~ spl14_220 ),
inference(avatar_contradiction_clause,[],[f11895]) ).
fof(f11904,plain,
( subclass(sF0,sF3)
| member(x,sF12)
| ~ spl14_193
| spl14_205 ),
inference(forward_subsumption_resolution,[],[f11360,f10321]) ).
fof(f11923,definition,
( spl14_230
<=> subclass(sF0,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_230])],[avatar_definition]) ).
fof(f11925,plain,
( subclass(sF0,sF3)
| ~ spl14_230 ),
inference(avatar_component_clause,[],[f11923]) ).
fof(f11969,plain,
( null_class = sF1
| spl14_2 ),
inference(forward_subsumption_resolution,[],[f5429,f224]) ).
fof(f11985,plain,
( subclass(sF0,sF3)
| spl14_39
| ~ spl14_193
| spl14_205 ),
inference(forward_subsumption_resolution,[],[f11904,f810]) ).
fof(f12034,plain,
( spl14_230
| spl14_39
| ~ spl14_193
| spl14_205 ),
inference(avatar_split_clause,[],[f11985,f10319,f9932,f809,f11923]) ).
fof(f12289,plain,
( ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) )
| spl14_3 ),
inference(forward_subsumption_resolution,[],[f9875,f230]) ).
fof(f12416,plain,
( spl14_120
| spl14_3 ),
inference(avatar_split_clause,[],[f12289,f228,f2729]) ).
fof(f12532,plain,
( subclass(sF0,sF13)
| ~ spl14_2
| ~ spl14_120 ),
inference(duplicate_literal_removal,[],[f10910]) ).
fof(f12564,plain,
( spl14_204
| ~ spl14_2
| ~ spl14_120 ),
inference(avatar_split_clause,[],[f12532,f2729,f223,f10315]) ).
fof(f12586,plain,
( $false
| spl14_3
| ~ spl14_204
| ~ spl14_221 ),
inference(forward_subsumption_resolution,[],[f11787,f230]) ).
fof(f12587,plain,
( spl14_3
| ~ spl14_204
| ~ spl14_221 ),
inference(avatar_contradiction_clause,[],[f12586]) ).
fof(f12617,plain,
( spl14_81
| spl14_2 ),
inference(avatar_split_clause,[],[f11969,f223,f1320]) ).
fof(f12618,plain,
( spl14_4
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f3216,f228,f232]) ).
fof(f12652,plain,
( ~ subclass(sF0,sF3)
| ~ spl14_12
| spl14_204 ),
inference(forward_demodulation,[],[f10316,f10848]) ).
fof(f12778,plain,
( $false
| ~ spl14_12
| spl14_204
| ~ spl14_230 ),
inference(forward_subsumption_resolution,[],[f12652,f11925]) ).
fof(f12779,plain,
( ~ spl14_12
| spl14_204
| ~ spl14_230 ),
inference(avatar_contradiction_clause,[],[f12778]) ).
fof(f12944,plain,
( spl14_230
| ~ spl14_209 ),
inference(avatar_split_clause,[],[f11096,f11001,f11923]) ).
cnf(s1,plain,
( ~ spl14_1
| spl14_2 ),
inference(sat_conversion,[],[f226]) ).
cnf(s3,plain,
( ~ spl14_1
| spl14_5 ),
inference(sat_conversion,[],[f240]) ).
cnf(s156,plain,
( spl14_8
| ~ spl14_81 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s222,plain,
( ~ spl14_39
| spl14_45 ),
inference(sat_conversion,[],[f4187]) ).
cnf(s248,plain,
( ~ spl14_8
| spl14_12 ),
inference(sat_conversion,[],[f5285]) ).
cnf(s251,plain,
( ~ spl14_157
| spl14_158 ),
inference(sat_conversion,[],[f5417]) ).
cnf(s255,plain,
spl14_157,
inference(sat_conversion,[],[f5899]) ).
cnf(s311,plain,
( ~ spl14_3
| spl14_33 ),
inference(sat_conversion,[],[f9848]) ).
cnf(s313,plain,
( spl14_26
| spl14_184
| spl14_185 ),
inference(sat_conversion,[],[f9865]) ).
cnf(s321,plain,
( spl14_39
| ~ spl14_120
| spl14_184 ),
inference(sat_conversion,[],[f9969]) ).
cnf(s335,plain,
( ~ spl14_26
| spl14_30
| ~ spl14_158 ),
inference(sat_conversion,[],[f10072]) ).
cnf(s345,plain,
( ~ spl14_4
| ~ spl14_30 ),
inference(sat_conversion,[],[f10164]) ).
cnf(s354,plain,
( ~ spl14_2
| ~ spl14_185
| spl14_204 ),
inference(sat_conversion,[],[f10323]) ).
cnf(s358,plain,
( ~ spl14_184
| spl14_204 ),
inference(sat_conversion,[],[f10513]) ).
cnf(s371,plain,
spl14_16,
inference(sat_conversion,[],[f10593]) ).
cnf(s396,plain,
( spl14_26
| ~ spl14_158
| spl14_193
| spl14_209 ),
inference(sat_conversion,[],[f11047]) ).
cnf(s405,plain,
( ~ spl14_16
| ~ spl14_204
| spl14_220
| spl14_221 ),
inference(sat_conversion,[],[f11693]) ).
cnf(s409,plain,
( ~ spl14_33
| ~ spl14_204
| ~ spl14_221 ),
inference(sat_conversion,[],[f11779]) ).
cnf(s410,plain,
( ~ spl14_5
| ~ spl14_204
| ~ spl14_220 ),
inference(sat_conversion,[],[f11850]) ).
cnf(s411,plain,
( spl14_1
| ~ spl14_2 ),
inference(sat_conversion,[],[f11869]) ).
cnf(s417,plain,
( spl14_1
| ~ spl14_45 ),
inference(sat_conversion,[],[f11881]) ).
cnf(s419,plain,
( spl14_1
| ~ spl14_205 ),
inference(sat_conversion,[],[f11885]) ).
cnf(s422,plain,
( spl14_1
| ~ spl14_204
| ~ spl14_220 ),
inference(sat_conversion,[],[f11896]) ).
cnf(s439,plain,
( spl14_39
| ~ spl14_193
| spl14_205
| spl14_230 ),
inference(sat_conversion,[],[f12034]) ).
cnf(s506,plain,
( spl14_3
| spl14_120 ),
inference(sat_conversion,[],[f12416]) ).
cnf(s523,plain,
( ~ spl14_2
| ~ spl14_120
| spl14_204 ),
inference(sat_conversion,[],[f12564]) ).
cnf(s539,plain,
( spl14_3
| ~ spl14_204
| ~ spl14_221 ),
inference(sat_conversion,[],[f12587]) ).
cnf(s548,plain,
( spl14_2
| spl14_81 ),
inference(sat_conversion,[],[f12617]) ).
cnf(s550,plain,
( ~ spl14_3
| spl14_4 ),
inference(sat_conversion,[],[f12618]) ).
cnf(s568,plain,
( ~ spl14_12
| spl14_204
| ~ spl14_230 ),
inference(sat_conversion,[],[f12779]) ).
cnf(s575,plain,
( ~ spl14_209
| spl14_230 ),
inference(sat_conversion,[],[f12944]) ).
cnf(s581,plain,
spl14_158,
inference(rat,[],[s251,s255]) ).
cnf(s586,plain,
( spl14_3
| spl14_1 ),
inference(rat,[],[s405,s422,s539,s358,s321,s506,s222,s417,s371]) ).
cnf(s587,plain,
( ~ spl14_204
| spl14_1 ),
inference(rat,[],[s405,s409,s422,s311,s586,s371]) ).
cnf(s588,plain,
spl14_1,
inference(rat,[],[s396,s439,s575,s568,s587,s335,s345,s550,s586,s248,s156,s548,s222,s411,s417,s419,s581]) ).
cnf(s590,plain,
spl14_5,
inference(rat,[],[s3,s588]) ).
cnf(s591,plain,
spl14_2,
inference(rat,[],[s1,s588]) ).
cnf(s601,plain,
( ~ spl14_221
| ~ spl14_204 ),
inference(rat,[],[s311,s539,s409]) ).
cnf(s602,plain,
( ~ spl14_204
| spl14_220 ),
inference(rat,[],[s601,s405,s371]) ).
cnf(s603,plain,
~ spl14_204,
inference(rat,[],[s602,s410,s590]) ).
cnf(s604,plain,
~ spl14_184,
inference(rat,[],[s358,s603]) ).
cnf(s605,plain,
~ spl14_120,
inference(rat,[],[s523,s591,s603]) ).
cnf(s606,plain,
~ spl14_185,
inference(rat,[],[s354,s591,s603]) ).
cnf(s608,plain,
spl14_3,
inference(rat,[],[s506,s605]) ).
cnf(s614,plain,
spl14_26,
inference(rat,[],[s313,s604,s606]) ).
cnf(s615,plain,
spl14_4,
inference(rat,[],[s550,s608]) ).
cnf(s619,plain,
spl14_30,
inference(rat,[],[s335,s581,s614]) ).
cnf(s620,plain,
$false,
inference(rat,[],[s345,s619,s615]) ).
fof(f12991,plain,
$false,
inference(avatar_sat_refutation,[],[s620]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET141-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 00:52:46 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.93/1.93 % (1329290)Input is clausal, will run a generic CNF schedule.
% 6.93/1.93 % (1329295)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=4089133039:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.93/1.93 % (1329297)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2065665382:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.93/1.93 % (1329296)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3484450012:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.93/1.93 % (1329299)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1717137347:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.93/1.93 % (1329298)lrs+10_1_sil=8000:sp=occurrence:random_seed=3441813316:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.93/1.93 % (1329301)dis-21_1_sil=8000:lcm=predicate:random_seed=1744589169: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)
% 6.93/1.93 % (1329300)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2770423843:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.93/1.93 % (1329298)Refutation not found, incomplete strategy
% 6.93/1.93 % (1329298)------------------------------
% 6.93/1.93 % (1329298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329298)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329298)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.93 % (1329298)Time elapsed: 0.003 s
% 6.93/1.93 % (1329298)Peak memory usage: 88 MB
% 6.93/1.93 % (1329298)Instructions burned: 3 (million)
% 6.93/1.93 % (1329301)Instruction limit reached!
% 6.93/1.93 % (1329301)------------------------------
% 6.93/1.93 % (1329301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329301)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329301)Termination reason: Instruction limit
% 6.93/1.93 % (1329301)Termination phase: Saturation
% 6.93/1.93 % (1329301)Time elapsed: 0.064 s
% 6.93/1.93 % (1329301)Peak memory usage: 88 MB
% 6.93/1.93 % (1329301)Instructions burned: 117 (million)
% 6.93/1.93 % (1329299)Instruction limit reached!
% 6.93/1.93 % (1329299)------------------------------
% 6.93/1.93 % (1329299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329299)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329299)Termination reason: Instruction limit
% 6.93/1.93 % (1329299)Termination phase: Saturation
% 6.93/1.93 % (1329299)Time elapsed: 0.067 s
% 6.93/1.93 % (1329299)Peak memory usage: 89 MB
% 6.93/1.93 % (1329299)Instructions burned: 115 (million)
% 6.93/1.93 % (1329300)Instruction limit reached!
% 6.93/1.93 % (1329300)------------------------------
% 6.93/1.93 % (1329300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329300)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329300)Termination reason: Instruction limit
% 6.93/1.93 % (1329300)Termination phase: Saturation
% 6.93/1.93 % (1329300)Time elapsed: 0.134 s
% 6.93/1.93 % (1329300)Peak memory usage: 90 MB
% 6.93/1.93 % (1329300)Instructions burned: 181 (million)
% 6.93/1.93 % (1329309)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=237500991:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.93/1.93 % (1329310)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4036461310: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)
% 6.93/1.93 % (1329309)Refutation not found, incomplete strategy
% 6.93/1.93 % (1329309)------------------------------
% 6.93/1.93 % (1329309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329309)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329309)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.93 % (1329309)Time elapsed: 0.003 s
% 6.93/1.93 % (1329309)Peak memory usage: 88 MB
% 6.93/1.93 % (1329309)Instructions burned: 3 (million)
% 6.93/1.93 % (1329298)------------------------------
% 6.93/1.93 % (1329298)------------------------------
% 6.93/1.93 % (1329311)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1458890196:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 6.93/1.93 % (1329311)Refutation not found, incomplete strategy
% 6.93/1.93 % (1329311)------------------------------
% 6.93/1.93 % (1329311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329311)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329311)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.93 % (1329311)Time elapsed: 0.003 s
% 6.93/1.93 % (1329311)Peak memory usage: 88 MB
% 6.93/1.93 % (1329311)Instructions burned: 3 (million)
% 6.93/1.93 % (1329310)Instruction limit reached!
% 6.93/1.93 % (1329310)------------------------------
% 6.93/1.93 % (1329310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329310)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329310)Termination reason: Instruction limit
% 6.93/1.93 % (1329310)Termination phase: Saturation
% 6.93/1.93 % (1329310)Time elapsed: 0.104 s
% 6.93/1.93 % (1329310)Peak memory usage: 90 MB
% 6.93/1.93 % (1329310)Instructions burned: 189 (million)
% 6.93/1.93 % (1329314)lrs+10_64_to=lpo:sil=8000:random_seed=358848585:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.93/1.93 % (1329309)------------------------------
% 6.93/1.93 % (1329309)------------------------------
% 6.93/1.93 % (1329316)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2029772256:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.93/1.93 % (1329314)Instruction limit reached!
% 6.93/1.93 % (1329314)------------------------------
% 6.93/1.93 % (1329314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329314)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329314)Termination reason: Instruction limit
% 6.93/1.93 % (1329314)Termination phase: Saturation
% 6.93/1.93 % (1329314)Time elapsed: 0.080 s
% 6.93/1.93 % (1329314)Peak memory usage: 89 MB
% 6.93/1.93 % (1329314)Instructions burned: 127 (million)
% 6.93/1.93 % (1329311)------------------------------
% 6.93/1.93 % (1329311)------------------------------
% 6.93/1.93 % (1329316)Instruction limit reached!
% 6.93/1.93 % (1329316)------------------------------
% 6.93/1.93 % (1329316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329316)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329316)Termination reason: Instruction limit
% 6.93/1.93 % (1329316)Termination phase: Saturation
% 6.93/1.93 % (1329316)Time elapsed: 0.124 s
% 6.93/1.93 % (1329316)Peak memory usage: 90 MB
% 6.93/1.93 % (1329316)Instructions burned: 195 (million)
% 6.93/1.93 % (1329318)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2429443829:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 6.93/1.93 % (1329320)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2446056282:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.93/1.93 % (1329321)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=1572854338:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 6.93/1.93 % (1329295)First to succeed.
% 6.93/1.93 % (1329318)Instruction limit reached!
% 6.93/1.93 % (1329318)------------------------------
% 6.93/1.93 % (1329318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329318)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329318)Termination reason: Instruction limit
% 6.93/1.93 % (1329318)Termination phase: Saturation
% 6.93/1.93 % (1329318)Time elapsed: 0.108 s
% 6.93/1.93 % (1329318)Peak memory usage: 91 MB
% 6.93/1.93 % (1329318)Instructions burned: 158 (million)
% 6.93/1.93 % (1329295)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1329290"
% 6.93/1.93 % (1329321)Instruction limit reached!
% 6.93/1.93 % (1329321)------------------------------
% 6.93/1.93 % (1329321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329321)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329321)Termination reason: Instruction limit
% 6.93/1.93 % (1329321)Termination phase: Saturation
% 6.93/1.93 % (1329321)Time elapsed: 0.066 s
% 6.93/1.93 % (1329321)Peak memory usage: 90 MB
% 6.93/1.93 % (1329321)Instructions burned: 107 (million)
% 6.93/1.93 % (1329322)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3025522843:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.93/1.93 % (1329322)Refutation not found, incomplete strategy
% 6.93/1.93 % (1329322)------------------------------
% 6.93/1.93 % (1329322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.93/1.93 % (1329322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.93/1.93 % (1329322)CaDiCaL version: 2.1.3
% 6.93/1.93 % (1329322)Termination reason: Refutation not found, incomplete strategy
% 6.93/1.93 % (1329322)Time elapsed: 0.005 s
% 6.93/1.93 % (1329322)Peak memory usage: 88 MB
% 6.93/1.93 % (1329322)Instructions burned: 7 (million)
% 6.93/1.93 % (1329326)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1943632542:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 6.93/1.93 % (1329295)Refutation found. Thanks to Tanya!
% 6.93/1.93 % SZS status Unsatisfiable for theBenchmark
% 6.93/1.93 % SZS output start Proof for theBenchmark
% See solution above
% 8.11/2.12 % (1329295)------------------------------
% 8.11/2.12 % (1329295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.11/2.12 % (1329295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.11/2.12 % (1329295)CaDiCaL version: 2.1.3
% 8.11/2.12 % (1329295)Termination reason: Refutation
% 8.11/2.12 % (1329295)Time elapsed: 0.786 s
% 8.11/2.12 % (1329295)Peak memory usage: 139 MB
% 8.11/2.12 % (1329295)Instructions burned: 1990 (million)
% 8.11/2.12 % (1329295)------------------------------
% 8.11/2.12 % (1329295)------------------------------
% 8.11/2.12 % (1329290)Success in time 1.079 s
% 8.11/2.12 % Vampire exiting
%------------------------------------------------------------------------------