%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET139-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 : n005.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:15 PM UTC 2026
% Result : Unsatisfiable 16.44s 3.27s
% Output : Refutation 17.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 66
% Syntax : Number of formulae : 541 ( 82 unt; 45 def)
% Number of atoms : 1330 ( 238 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1284 ( 495 ~; 758 |; 0 &)
% ( 31 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 11 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 32 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 18 con; 0-3 aty)
% Number of variables : 277 ( 0 sgn 277 !; 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(x,set_builder(y,null_class))) != unordered_pair(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_triple_reduction1_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(x,x)),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(sF2,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f175,plain,
intersection(sF2,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,f161,f159,f161,f159,f157]) ).
fof(f185,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF2) ),
inference(superposition,[],[f21,f175]) ).
fof(f186,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(f197,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(f202,plain,
! [X0] :
( ~ member(X0,sF4)
| ~ member(X0,sF3) ),
inference(superposition,[],[f24,f165]) ).
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(f216,plain,
( member(y,sF3)
| ~ member(y,universal_class) ),
inference(superposition,[],[f9,f163]) ).
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(f220,plain,
( member(x,universal_class)
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f219]) ).
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(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(f233,plain,
( ~ member(y,sF3)
| spl14_4 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( member(y,sF3)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f235,plain,
( ~ spl14_3
| spl14_4 ),
inference(avatar_split_clause,[],[f216,f232,f228]) ).
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(f247,plain,
! [X0] :
( ~ member(X0,sF8)
| member(X0,sF9)
| ~ member(X0,sF2) ),
inference(superposition,[],[f23,f175]) ).
fof(f248,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(f268,plain,
! [X0] :
( subclass(sF1,X0)
| x = not_subclass_element(sF1,X0) ),
inference(resolution,[],[f2,f211]) ).
fof(f270,plain,
! [X0] :
( subclass(sF3,X0)
| y = not_subclass_element(sF3,X0) ),
inference(resolution,[],[f2,f212]) ).
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(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),sF4)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF3) ),
inference(forward_subsumption_resolution,[],[f297,f4]) ).
fof(f335,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF1)
| member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1) ),
inference(forward_subsumption_resolution,[],[f296,f4]) ).
fof(f345,plain,
! [X0] :
( subclass(X0,sF13)
| member(not_subclass_element(X0,sF13),sF12)
| subclass(X0,sF13) ),
inference(resolution,[],[f329,f3]) ).
fof(f347,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| member(not_subclass_element(X0,X1),X2)
| ~ subclass(sF13,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f329,f1]) ).
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,f197]) ).
fof(f351,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF2)
| subclass(X0,sF13) ),
inference(resolution,[],[f348,f186]) ).
fof(f355,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,[],[f355,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,f248]) ).
fof(f379,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1) ),
inference(resolution,[],[f332,f247]) ).
fof(f394,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1)
| not_subclass_element(X0,X1) = x ),
inference(resolution,[],[f335,f211]) ).
fof(f402,plain,
! [X0] :
( subclass(X0,sF13)
| member(not_subclass_element(X0,sF13),sF9)
| subclass(X0,sF13) ),
inference(resolution,[],[f331,f355]) ).
fof(f407,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF9)
| subclass(X0,sF13) ),
inference(duplicate_literal_removal,[],[f402]) ).
fof(f408,plain,
! [X0] :
( member(not_subclass_element(X0,sF13),sF8)
| subclass(X0,sF13) ),
inference(resolution,[],[f407,f196]) ).
fof(f412,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF13),sF7)
| subclass(X0,sF13) ),
inference(resolution,[],[f408,f204]) ).
fof(f414,plain,
( subclass(sF7,sF13)
| subclass(sF7,sF13) ),
inference(resolution,[],[f412,f2]) ).
fof(f417,plain,
subclass(sF7,sF13),
inference(duplicate_literal_removal,[],[f414]) ).
fof(f436,plain,
! [X0,X1] :
( subclass(X0,X1)
| not_subclass_element(X0,X1) = x
| member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1) ),
inference(resolution,[],[f394,f379]) ).
fof(f437,plain,
! [X0,X1] :
( subclass(X0,X1)
| not_subclass_element(X0,X1) = x
| member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1) ),
inference(resolution,[],[f394,f368]) ).
fof(f442,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| not_subclass_element(X0,X1) = x
| member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f437]) ).
fof(f443,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF9)
| not_subclass_element(X0,X1) = x
| member(not_subclass_element(X0,X1),sF7)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f436]) ).
fof(f449,plain,
! [X0] :
( x = not_subclass_element(sF13,X0)
| member(not_subclass_element(sF13,X0),sF10)
| subclass(sF13,X0)
| subclass(sF13,X0) ),
inference(resolution,[],[f442,f286]) ).
fof(f455,plain,
! [X0] :
( member(not_subclass_element(sF13,X0),sF10)
| x = not_subclass_element(sF13,X0)
| subclass(sF13,X0) ),
inference(duplicate_literal_removal,[],[f449]) ).
fof(f457,plain,
( x = not_subclass_element(sF13,sF10)
| subclass(sF13,sF10)
| subclass(sF13,sF10) ),
inference(resolution,[],[f455,f3]) ).
fof(f458,plain,
! [X0] :
( ~ member(not_subclass_element(sF13,X0),sF9)
| subclass(sF13,X0)
| x = not_subclass_element(sF13,X0) ),
inference(resolution,[],[f455,f205]) ).
fof(f460,plain,
( x = not_subclass_element(sF13,sF10)
| subclass(sF13,sF10) ),
inference(duplicate_literal_removal,[],[f457]) ).
fof(f463,definition,
( spl14_8
<=> subclass(sF13,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f464,plain,
( ~ subclass(sF13,sF10)
| spl14_8 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f465,plain,
( subclass(sF13,sF10)
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f467,definition,
( spl14_9
<=> x = not_subclass_element(sF13,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f469,plain,
( x = not_subclass_element(sF13,sF10)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f470,plain,
( spl14_8
| spl14_9 ),
inference(avatar_split_clause,[],[f460,f467,f463]) ).
fof(f471,plain,
! [X0] :
( subclass(sF13,X0)
| x = not_subclass_element(sF13,X0)
| x = not_subclass_element(sF13,X0)
| member(not_subclass_element(sF13,X0),sF7)
| subclass(sF13,X0) ),
inference(resolution,[],[f458,f443]) ).
fof(f478,plain,
! [X0] :
( member(not_subclass_element(sF13,X0),sF7)
| x = not_subclass_element(sF13,X0)
| subclass(sF13,X0) ),
inference(duplicate_literal_removal,[],[f471]) ).
fof(f488,plain,
( x = not_subclass_element(sF13,sF7)
| subclass(sF13,sF7)
| subclass(sF13,sF7) ),
inference(resolution,[],[f478,f3]) ).
fof(f491,plain,
( x = not_subclass_element(sF13,sF7)
| subclass(sF13,sF7) ),
inference(duplicate_literal_removal,[],[f488]) ).
fof(f494,definition,
( spl14_12
<=> subclass(sF13,sF7) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f495,plain,
( ~ subclass(sF13,sF7)
| spl14_12 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f496,plain,
( subclass(sF13,sF7)
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f498,definition,
( spl14_13
<=> x = not_subclass_element(sF13,sF7) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f500,plain,
( x = not_subclass_element(sF13,sF7)
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,plain,
( spl14_12
| spl14_13 ),
inference(avatar_split_clause,[],[f491,f498,f494]) ).
fof(f515,plain,
( ~ subclass(sF10,sF13)
| sF10 = sF13
| ~ spl14_8 ),
inference(resolution,[],[f465,f7]) ).
fof(f516,plain,
( sF10 = sF13
| ~ spl14_8 ),
inference(forward_subsumption_resolution,[],[f515,f366]) ).
fof(f517,plain,
( sF0 != sF10
| ~ spl14_8 ),
inference(superposition,[],[f184,f516]) ).
fof(f549,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(f582,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,[],[f549]) ).
fof(f608,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f265,f3]) ).
fof(f609,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,X1),intersection(X2,X0))
| subclass(intersection(X0,X1),intersection(X2,X0))
| ~ member(not_subclass_element(intersection(X0,X1),intersection(X2,X0)),X2) ),
inference(resolution,[],[f265,f290]) ).
fof(f662,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(intersection(X0,X1),intersection(X2,X0)),X2)
| subclass(intersection(X0,X1),intersection(X2,X0)) ),
inference(duplicate_literal_removal,[],[f609]) ).
fof(f663,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f608]) ).
fof(f675,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f663,f70]) ).
fof(f676,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f675,f7]) ).
fof(f677,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f676]) ).
fof(f678,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f677,f663]) ).
fof(f699,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f22,f678]) ).
fof(f726,definition,
( spl14_20
<=> x = y ),
introduced(definition,[new_symbols(definition,[spl14_20])],[avatar_definition]) ).
fof(f727,plain,
( x != y
| spl14_20 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f728,plain,
( x = y
| ~ spl14_20 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f757,definition,
( spl14_26
<=> member(y,sF4) ),
introduced(definition,[new_symbols(definition,[spl14_26])],[avatar_definition]) ).
fof(f758,plain,
( ~ member(y,sF4)
| spl14_26 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( member(y,sF4)
| ~ spl14_26 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f788,definition,
( spl14_32
<=> member(y,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
fof(f790,plain,
( member(y,sF0)
| ~ spl14_32 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f793,definition,
( spl14_33
<=> member(y,sF5) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
fof(f795,plain,
( member(y,sF5)
| ~ spl14_33 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f812,definition,
( spl14_34
<=> member(x,sF9) ),
introduced(definition,[new_symbols(definition,[spl14_34])],[avatar_definition]) ).
fof(f813,plain,
( ~ member(x,sF9)
| spl14_34 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f814,plain,
( member(x,sF9)
| ~ spl14_34 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f820,definition,
( spl14_36
<=> member(x,sF2) ),
introduced(definition,[new_symbols(definition,[spl14_36])],[avatar_definition]) ).
fof(f821,plain,
( member(x,sF2)
| ~ spl14_36 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f822,plain,
( ~ member(x,sF2)
| spl14_36 ),
inference(avatar_component_clause,[],[f820]) ).
fof(f825,definition,
( spl14_37
<=> member(x,sF12) ),
introduced(definition,[new_symbols(definition,[spl14_37])],[avatar_definition]) ).
fof(f826,plain,
( ~ member(x,sF12)
| spl14_37 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f829,definition,
( spl14_38
<=> member(x,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_38])],[avatar_definition]) ).
fof(f830,plain,
( ~ member(x,sF10)
| spl14_38 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f831,plain,
( member(x,sF10)
| ~ spl14_38 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f836,definition,
( spl14_39
<=> member(x,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition]) ).
fof(f837,plain,
( ~ member(x,sF3)
| spl14_39 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f838,plain,
( member(x,sF3)
| ~ spl14_39 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f880,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f264,f3]) ).
fof(f936,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f880]) ).
fof(f947,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f582,f2]) ).
fof(f987,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f947]) ).
fof(f997,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f987,f7]) ).
fof(f1031,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f997,f663]) ).
fof(f1032,plain,
! [X0] : intersection(X0,universal_class) = X0,
inference(resolution,[],[f1031,f4]) ).
fof(f1036,plain,
! [X0] :
( y = not_subclass_element(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(resolution,[],[f1031,f267]) ).
fof(f1041,plain,
! [X0,X1] :
( ~ member(X1,X0)
| member(X1,universal_class) ),
inference(superposition,[],[f22,f1032]) ).
fof(f1043,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(superposition,[],[f264,f1032]) ).
fof(f1060,plain,
! [X0,X1] : intersection(X0,X1) = intersection(intersection(X0,X1),X1),
inference(resolution,[],[f936,f1031]) ).
fof(f1061,plain,
! [X0,X1] :
( ~ subclass(X0,intersection(X1,X0))
| intersection(X1,X0) = X0 ),
inference(resolution,[],[f936,f7]) ).
fof(f1062,plain,
! [X0] : null_class = intersection(X0,null_class),
inference(resolution,[],[f936,f677]) ).
fof(f1076,plain,
( ~ subclass(sF7,sF13)
| sF7 = sF13
| ~ spl14_12 ),
inference(resolution,[],[f496,f7]) ).
fof(f1078,plain,
( sF7 = sF13
| ~ spl14_12 ),
inference(forward_subsumption_resolution,[],[f1076,f417]) ).
fof(f1080,plain,
( sF7 = sF10
| ~ spl14_8
| ~ spl14_12 ),
inference(forward_demodulation,[],[f1078,f516]) ).
fof(f1110,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f121,f678]) ).
fof(f1111,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f1110]) ).
fof(f1178,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f1179,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f1183,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f68,f1111]) ).
fof(f1187,plain,
( null_class = sF3
| y = regular(sF3) ),
inference(resolution,[],[f68,f212]) ).
fof(f1293,definition,
( spl14_71
<=> y = regular(sF3) ),
introduced(definition,[new_symbols(definition,[spl14_71])],[avatar_definition]) ).
fof(f1295,plain,
( y = regular(sF3)
| ~ spl14_71 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1297,definition,
( spl14_72
<=> null_class = sF3 ),
introduced(definition,[new_symbols(definition,[spl14_72])],[avatar_definition]) ).
fof(f1298,plain,
( null_class != sF3
| spl14_72 ),
inference(avatar_component_clause,[],[f1297]) ).
fof(f1299,plain,
( null_class = sF3
| ~ spl14_72 ),
inference(avatar_component_clause,[],[f1297]) ).
fof(f1300,plain,
( spl14_71
| spl14_72 ),
inference(avatar_split_clause,[],[f1187,f1297,f1293]) ).
fof(f1398,plain,
! [X0] : ~ member(X0,null_class),
inference(superposition,[],[f1111,f1183]) ).
fof(f1459,plain,
! [X0,X1] :
( ~ member(regular(intersection(complement(X0),X1)),X0)
| null_class = intersection(complement(X0),X1) ),
inference(resolution,[],[f1179,f24]) ).
fof(f1651,plain,
! [X0] :
( null_class = intersection(X0,universal_class)
| member(regular(intersection(X0,universal_class)),sF5)
| member(regular(intersection(X0,universal_class)),null_class) ),
inference(resolution,[],[f1178,f188]) ).
fof(f1724,plain,
! [X0] :
( null_class = intersection(X0,universal_class)
| member(regular(intersection(X0,universal_class)),sF5) ),
inference(forward_subsumption_resolution,[],[f1651,f699]) ).
fof(f1758,plain,
! [X0] :
( null_class = X0
| member(regular(intersection(X0,universal_class)),sF5) ),
inference(forward_demodulation,[],[f1724,f1032]) ).
fof(f2294,plain,
! [X0] :
( member(regular(X0),sF5)
| null_class = X0 ),
inference(forward_demodulation,[],[f1758,f1032]) ).
fof(f2421,plain,
! [X0] :
( null_class = intersection(complement(X0),X0)
| null_class = intersection(complement(X0),X0) ),
inference(resolution,[],[f1459,f1178]) ).
fof(f2433,plain,
! [X0] : null_class = intersection(complement(X0),X0),
inference(duplicate_literal_removal,[],[f2421]) ).
fof(f2456,definition,
( spl14_90
<=> sF1 = sF3 ),
introduced(definition,[new_symbols(definition,[spl14_90])],[avatar_definition]) ).
fof(f2457,plain,
( sF1 != sF3
| spl14_90 ),
inference(avatar_component_clause,[],[f2456]) ).
fof(f2458,plain,
( sF1 = sF3
| ~ spl14_90 ),
inference(avatar_component_clause,[],[f2456]) ).
fof(f2468,plain,
( complement(sF1) = sF4
| ~ spl14_90 ),
inference(superposition,[],[f165,f2458]) ).
fof(f2469,plain,
( sF2 = sF4
| ~ spl14_90 ),
inference(forward_demodulation,[],[f2468,f161]) ).
fof(f2582,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(f2585,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(f2595,plain,
! [X0,X1] :
( subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1)
| ~ subclass(X0,universal_class) ),
inference(duplicate_literal_removal,[],[f2582]) ).
fof(f2603,plain,
! [X0] :
( subclass(X0,sF5)
| member(not_subclass_element(X0,sF5),null_class) ),
inference(forward_subsumption_resolution,[],[f2585,f1043]) ).
fof(f2605,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(forward_subsumption_resolution,[],[f2595,f4]) ).
fof(f2606,plain,
! [X0] : subclass(X0,sF5),
inference(forward_subsumption_resolution,[],[f2603,f1398]) ).
fof(f2629,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(complement(X1))),X1)
| subclass(X0,complement(complement(X1))) ),
inference(resolution,[],[f2605,f24]) ).
fof(f2646,plain,
! [X0] :
( subclass(X0,complement(sF9))
| member(not_subclass_element(X0,complement(sF9)),sF8) ),
inference(resolution,[],[f2605,f196]) ).
fof(f2674,plain,
! [X0] :
( subclass(X0,sF10)
| member(not_subclass_element(X0,complement(sF9)),sF8) ),
inference(forward_demodulation,[],[f2646,f177]) ).
fof(f3004,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(f3039,plain,
! [X0,X1] :
( member(not_subclass_element(complement(complement(X0)),X1),X0)
| subclass(complement(complement(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f3004,f1043]) ).
fof(f3556,plain,
! [X0] :
( x = not_subclass_element(sF1,X0)
| sF1 = intersection(sF1,X0) ),
inference(resolution,[],[f268,f1031]) ).
fof(f3603,plain,
! [X0] :
( y = not_subclass_element(sF3,X0)
| sF3 = intersection(sF3,X0) ),
inference(resolution,[],[f270,f1031]) ).
fof(f3780,plain,
! [X0] :
( subclass(X0,complement(complement(X0)))
| subclass(X0,complement(complement(X0))) ),
inference(resolution,[],[f2629,f2]) ).
fof(f3833,plain,
! [X0] : subclass(X0,complement(complement(X0))),
inference(duplicate_literal_removal,[],[f3780]) ).
fof(f4038,plain,
! [X0] :
( subclass(complement(complement(X0)),X0)
| subclass(complement(complement(X0)),X0) ),
inference(resolution,[],[f3039,f3]) ).
fof(f4121,plain,
! [X0] : subclass(complement(complement(X0)),X0),
inference(duplicate_literal_removal,[],[f4038]) ).
fof(f4227,plain,
! [X0] :
( ~ subclass(X0,complement(complement(X0)))
| complement(complement(X0)) = X0 ),
inference(resolution,[],[f4121,f7]) ).
fof(f4247,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f4227,f3833]) ).
fof(f4279,definition,
( spl14_94
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl14_94])],[avatar_definition]) ).
fof(f4281,plain,
( sF0 = sF1
| ~ spl14_94 ),
inference(avatar_component_clause,[],[f4279]) ).
fof(f4679,plain,
! [X0] :
( member(not_subclass_element(X0,sF10),sF8)
| subclass(X0,sF10) ),
inference(forward_demodulation,[],[f2674,f177]) ).
fof(f4959,plain,
sF1 = complement(sF2),
inference(superposition,[],[f4247,f161]) ).
fof(f4960,plain,
sF3 = complement(sF4),
inference(superposition,[],[f4247,f165]) ).
fof(f4961,plain,
sF6 = complement(sF7),
inference(superposition,[],[f4247,f171]) ).
fof(f4963,plain,
sF9 = complement(sF10),
inference(superposition,[],[f4247,f177]) ).
fof(f4989,plain,
sF9 = sF11,
inference(forward_demodulation,[],[f4963,f179]) ).
fof(f4991,plain,
sF6 = sF8,
inference(forward_demodulation,[],[f4961,f173]) ).
fof(f5022,plain,
( sF0 != sF7
| ~ spl14_12 ),
inference(superposition,[],[f184,f1078]) ).
fof(f5060,plain,
( ~ member(x,sF10)
| subclass(sF13,sF10)
| ~ spl14_9 ),
inference(superposition,[],[f3,f469]) ).
fof(f5072,plain,
( member(x,universal_class)
| subclass(sF13,sF10)
| ~ spl14_9 ),
inference(superposition,[],[f1043,f469]) ).
fof(f5075,plain,
( subclass(sF13,sF10)
| spl14_1
| ~ spl14_9 ),
inference(forward_subsumption_resolution,[],[f5072,f221]) ).
fof(f5087,plain,
( ~ member(x,sF10)
| spl14_8
| ~ spl14_9 ),
inference(forward_subsumption_resolution,[],[f5060,f464]) ).
fof(f5092,plain,
( $false
| spl14_1
| spl14_8
| ~ spl14_9 ),
inference(forward_subsumption_resolution,[],[f5075,f464]) ).
fof(f5093,plain,
( spl14_1
| spl14_8
| ~ spl14_9 ),
inference(avatar_contradiction_clause,[],[f5092]) ).
fof(f5207,plain,
( sF6 = intersection(sF2,sF5)
| ~ spl14_90 ),
inference(superposition,[],[f169,f2469]) ).
fof(f5328,plain,
! [X0] :
( member(y,sF0)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(superposition,[],[f2,f1036]) ).
fof(f5329,plain,
! [X0] :
( ~ member(y,X0)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(superposition,[],[f3,f1036]) ).
fof(f5344,plain,
! [X0] :
( member(y,universal_class)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(superposition,[],[f1043,f1036]) ).
fof(f5385,plain,
! [X0] :
( member(y,universal_class)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f5344,f1031]) ).
fof(f5400,plain,
! [X0] :
( ~ member(y,X0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f5329,f1031]) ).
fof(f5401,plain,
! [X0] :
( member(y,sF0)
| x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f5328,f1031]) ).
fof(f5416,plain,
( ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) )
| spl14_3 ),
inference(forward_subsumption_resolution,[],[f5385,f230]) ).
fof(f5431,definition,
( spl14_119
<=> ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl14_119])],[avatar_definition]) ).
fof(f5432,plain,
( ! [X0] :
( x = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) )
| ~ spl14_119 ),
inference(avatar_component_clause,[],[f5431]) ).
fof(f5434,plain,
( spl14_119
| spl14_32 ),
inference(avatar_split_clause,[],[f5401,f788,f5431]) ).
fof(f5446,plain,
( spl14_119
| spl14_3 ),
inference(avatar_split_clause,[],[f5416,f228,f5431]) ).
fof(f5662,plain,
( member(x,sF11)
| subclass(sF0,sF13)
| sF0 = intersection(sF0,sF13)
| ~ spl14_119 ),
inference(superposition,[],[f350,f5432]) ).
fof(f5663,plain,
( member(x,sF2)
| subclass(sF0,sF13)
| sF0 = intersection(sF0,sF13)
| ~ spl14_119 ),
inference(superposition,[],[f351,f5432]) ).
fof(f5685,plain,
( member(x,sF2)
| sF0 = intersection(sF0,sF13)
| ~ spl14_119 ),
inference(forward_subsumption_resolution,[],[f5663,f1031]) ).
fof(f5686,plain,
( member(x,sF11)
| sF0 = intersection(sF0,sF13)
| ~ spl14_119 ),
inference(forward_subsumption_resolution,[],[f5662,f1031]) ).
fof(f5718,plain,
( sF0 = intersection(sF0,sF7)
| member(x,sF2)
| ~ spl14_12
| ~ spl14_119 ),
inference(forward_demodulation,[],[f5685,f1078]) ).
fof(f5807,plain,
( ~ member(x,sF1)
| ~ spl14_36 ),
inference(resolution,[],[f821,f201]) ).
fof(f5809,plain,
( member(x,universal_class)
| ~ spl14_36 ),
inference(resolution,[],[f821,f1041]) ).
fof(f5811,plain,
( $false
| spl14_1
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f5809,f221]) ).
fof(f5812,plain,
( spl14_1
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f5811]) ).
fof(f6032,plain,
( ~ member(x,sF12)
| subclass(sF13,sF7)
| ~ spl14_13 ),
inference(superposition,[],[f286,f500]) ).
fof(f6046,plain,
( member(x,universal_class)
| subclass(sF13,sF7)
| ~ spl14_13 ),
inference(superposition,[],[f1043,f500]) ).
fof(f6051,plain,
( subclass(sF13,sF7)
| spl14_1
| ~ spl14_13 ),
inference(forward_subsumption_resolution,[],[f6046,f221]) ).
fof(f6063,plain,
( ~ member(x,sF12)
| spl14_12
| ~ spl14_13 ),
inference(forward_subsumption_resolution,[],[f6032,f495]) ).
fof(f6068,plain,
( $false
| spl14_1
| spl14_12
| ~ spl14_13 ),
inference(forward_subsumption_resolution,[],[f6051,f495]) ).
fof(f6069,plain,
( spl14_1
| spl14_12
| ~ spl14_13 ),
inference(avatar_contradiction_clause,[],[f6068]) ).
fof(f6729,plain,
! [X0] :
( ~ member(X0,sF6)
| member(X0,sF9)
| ~ member(X0,sF2) ),
inference(superposition,[],[f247,f4991]) ).
fof(f6789,plain,
( unordered_pair(x,x) = sF0
| ~ spl14_20 ),
inference(superposition,[],[f157,f728]) ).
fof(f6790,plain,
( sF0 = sF1
| ~ spl14_20 ),
inference(forward_demodulation,[],[f6789,f159]) ).
fof(f6792,plain,
( spl14_94
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f6790,f726,f4279]) ).
fof(f6799,plain,
( sF1 != sF7
| ~ spl14_12
| ~ spl14_94 ),
inference(superposition,[],[f5022,f4281]) ).
fof(f6834,plain,
null_class = complement(universal_class),
inference(superposition,[],[f1032,f2433]) ).
fof(f6952,plain,
! [X0] : intersection(X0,sF5) = X0,
inference(resolution,[],[f2606,f1031]) ).
fof(f6961,plain,
! [X0,X1] :
( ~ member(X1,X0)
| member(X1,sF5) ),
inference(superposition,[],[f22,f6952]) ).
fof(f6977,plain,
( sF2 = sF6
| ~ spl14_90 ),
inference(superposition,[],[f5207,f6952]) ).
fof(f6978,plain,
sF4 = sF6,
inference(superposition,[],[f169,f6952]) ).
fof(f6981,plain,
( sF7 = complement(sF2)
| ~ spl14_90 ),
inference(superposition,[],[f171,f6977]) ).
fof(f6990,plain,
( sF1 = sF7
| ~ spl14_90 ),
inference(forward_demodulation,[],[f6981,f4959]) ).
fof(f6993,plain,
( $false
| ~ spl14_12
| ~ spl14_90
| ~ spl14_94 ),
inference(forward_subsumption_resolution,[],[f6990,f6799]) ).
fof(f6994,plain,
( ~ spl14_12
| ~ spl14_90
| ~ spl14_94 ),
inference(avatar_contradiction_clause,[],[f6993]) ).
fof(f7005,definition,
( spl14_131
<=> sF0 = sF3 ),
introduced(definition,[new_symbols(definition,[spl14_131])],[avatar_definition]) ).
fof(f7006,plain,
( sF0 != sF3
| spl14_131 ),
inference(avatar_component_clause,[],[f7005]) ).
fof(f7007,plain,
( sF0 = sF3
| ~ spl14_131 ),
inference(avatar_component_clause,[],[f7005]) ).
fof(f7009,definition,
( spl14_132
<=> x = not_subclass_element(sF0,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_132])],[avatar_definition]) ).
fof(f7010,plain,
( x != not_subclass_element(sF0,sF3)
| spl14_132 ),
inference(avatar_component_clause,[],[f7009]) ).
fof(f7011,plain,
( x = not_subclass_element(sF0,sF3)
| ~ spl14_132 ),
inference(avatar_component_clause,[],[f7009]) ).
fof(f7049,plain,
sF7 = complement(sF4),
inference(superposition,[],[f171,f6978]) ).
fof(f7057,plain,
sF3 = sF7,
inference(forward_demodulation,[],[f7049,f4960]) ).
fof(f7186,plain,
( member(x,sF11)
| member(x,sF10)
| ~ spl14_1 ),
inference(resolution,[],[f220,f194]) ).
fof(f7245,plain,
( ! [X0] : sF3 = intersection(X0,sF3)
| ~ spl14_72 ),
inference(superposition,[],[f1062,f1299]) ).
fof(f7402,plain,
( member(x,sF11)
| subclass(sF0,sF3)
| member(x,sF10)
| ~ spl14_132 ),
inference(superposition,[],[f330,f7011]) ).
fof(f7450,plain,
( member(y,sF5)
| null_class = sF3
| ~ spl14_71 ),
inference(superposition,[],[f2294,f1295]) ).
fof(f7589,plain,
( sF0 = intersection(sF0,sF7)
| ~ spl14_12
| spl14_36
| ~ spl14_119 ),
inference(forward_subsumption_resolution,[],[f5718,f822]) ).
fof(f7608,plain,
( sF0 = intersection(sF0,sF3)
| ~ spl14_12
| spl14_36
| ~ spl14_119 ),
inference(forward_demodulation,[],[f7589,f7057]) ).
fof(f7621,plain,
( sF0 = sF3
| ~ spl14_12
| spl14_36
| ~ spl14_72
| ~ spl14_119 ),
inference(forward_demodulation,[],[f7608,f7245]) ).
fof(f7630,plain,
( spl14_131
| ~ spl14_12
| spl14_36
| ~ spl14_72
| ~ spl14_119 ),
inference(avatar_split_clause,[],[f7621,f5431,f1297,f820,f494,f7005]) ).
fof(f7648,plain,
( sF3 != sF7
| ~ spl14_12
| ~ spl14_131 ),
inference(superposition,[],[f5022,f7007]) ).
fof(f7653,plain,
( $false
| ~ spl14_12
| ~ spl14_131 ),
inference(forward_subsumption_resolution,[],[f7648,f7057]) ).
fof(f7654,plain,
( ~ spl14_12
| ~ spl14_131 ),
inference(avatar_contradiction_clause,[],[f7653]) ).
fof(f7669,plain,
( member(y,sF5)
| ~ spl14_71
| spl14_72 ),
inference(forward_subsumption_resolution,[],[f7450,f1298]) ).
fof(f7685,plain,
( spl14_33
| ~ spl14_71
| spl14_72 ),
inference(avatar_split_clause,[],[f7669,f1297,f1293,f793]) ).
fof(f7695,plain,
( x = not_subclass_element(sF0,sF3)
| sF0 = intersection(sF0,sF3)
| ~ spl14_4 ),
inference(resolution,[],[f234,f5400]) ).
fof(f7699,plain,
( member(y,universal_class)
| ~ spl14_4 ),
inference(resolution,[],[f234,f1041]) ).
fof(f7701,plain,
( $false
| spl14_3
| ~ spl14_4 ),
inference(forward_subsumption_resolution,[],[f7699,f230]) ).
fof(f7702,plain,
( spl14_3
| ~ spl14_4 ),
inference(avatar_contradiction_clause,[],[f7701]) ).
fof(f7703,plain,
( member(y,sF0)
| ~ spl14_3 ),
inference(forward_subsumption_resolution,[],[f242,f229]) ).
fof(f7704,plain,
( spl14_32
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f7703,f228,f788]) ).
fof(f7852,plain,
( unordered_pair(x,x) = sF3
| ~ spl14_20 ),
inference(superposition,[],[f163,f728]) ).
fof(f7860,plain,
( sF1 = sF3
| ~ spl14_20 ),
inference(forward_demodulation,[],[f7852,f159]) ).
fof(f7862,plain,
( $false
| ~ spl14_20
| spl14_90 ),
inference(forward_subsumption_resolution,[],[f7860,f2457]) ).
fof(f7863,plain,
( ~ spl14_20
| spl14_90 ),
inference(avatar_contradiction_clause,[],[f7862]) ).
fof(f8178,plain,
( member(x,sF7)
| ~ spl14_8
| ~ spl14_12
| ~ spl14_38 ),
inference(forward_demodulation,[],[f831,f1080]) ).
fof(f8186,plain,
( member(x,sF3)
| ~ spl14_8
| ~ spl14_12
| ~ spl14_38 ),
inference(forward_demodulation,[],[f8178,f7057]) ).
fof(f8192,plain,
( $false
| ~ spl14_8
| ~ spl14_12
| ~ spl14_38
| spl14_39 ),
inference(forward_subsumption_resolution,[],[f8186,f837]) ).
fof(f8193,plain,
( ~ spl14_8
| ~ spl14_12
| ~ spl14_38
| spl14_39 ),
inference(avatar_contradiction_clause,[],[f8192]) ).
fof(f8219,plain,
( x = y
| ~ spl14_39 ),
inference(resolution,[],[f838,f212]) ).
fof(f8224,plain,
( $false
| spl14_20
| ~ spl14_39 ),
inference(forward_subsumption_resolution,[],[f8219,f727]) ).
fof(f8225,plain,
( spl14_20
| ~ spl14_39 ),
inference(avatar_contradiction_clause,[],[f8224]) ).
fof(f8314,plain,
( ~ member(y,sF3)
| ~ spl14_26 ),
inference(resolution,[],[f759,f202]) ).
fof(f8317,plain,
( member(y,universal_class)
| ~ spl14_26 ),
inference(resolution,[],[f759,f1041]) ).
fof(f8319,plain,
( $false
| ~ spl14_4
| ~ spl14_26 ),
inference(forward_subsumption_resolution,[],[f8314,f234]) ).
fof(f8320,plain,
( ~ spl14_4
| ~ spl14_26 ),
inference(avatar_contradiction_clause,[],[f8319]) ).
fof(f8690,plain,
universal_class = complement(null_class),
inference(superposition,[],[f4247,f6834]) ).
fof(f8691,plain,
universal_class = sF5,
inference(forward_demodulation,[],[f8690,f167]) ).
fof(f8702,plain,
( member(y,universal_class)
| ~ spl14_33 ),
inference(superposition,[],[f795,f8691]) ).
fof(f10445,plain,
( $false
| ~ spl14_2
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f5807,f225]) ).
fof(f10446,plain,
( ~ spl14_2
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f10445]) ).
fof(f10494,plain,
( ~ spl14_38
| spl14_8
| ~ spl14_9 ),
inference(avatar_split_clause,[],[f5087,f467,f463,f829]) ).
fof(f10605,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF9)
| ~ member(X0,sF2) ),
inference(forward_demodulation,[],[f6729,f6978]) ).
fof(f10621,plain,
( member(x,sF9)
| member(x,sF10)
| ~ spl14_1 ),
inference(forward_demodulation,[],[f7186,f4989]) ).
fof(f10625,definition,
( spl14_167
<=> subclass(sF0,sF3) ),
introduced(definition,[new_symbols(definition,[spl14_167])],[avatar_definition]) ).
fof(f10627,plain,
( subclass(sF0,sF3)
| ~ spl14_167 ),
inference(avatar_component_clause,[],[f10625]) ).
fof(f10629,plain,
( member(x,sF9)
| subclass(sF0,sF3)
| member(x,sF10)
| ~ spl14_132 ),
inference(forward_demodulation,[],[f7402,f4989]) ).
fof(f10766,plain,
( member(x,sF9)
| ~ spl14_1
| spl14_38 ),
inference(forward_subsumption_resolution,[],[f10621,f830]) ).
fof(f10768,plain,
( member(x,sF9)
| subclass(sF0,sF3)
| spl14_38
| ~ spl14_132 ),
inference(forward_subsumption_resolution,[],[f10629,f830]) ).
fof(f10838,plain,
( spl14_34
| ~ spl14_1
| spl14_38 ),
inference(avatar_split_clause,[],[f10766,f829,f219,f812]) ).
fof(f10839,plain,
( spl14_167
| spl14_34
| spl14_38
| ~ spl14_132 ),
inference(avatar_split_clause,[],[f10768,f7009,f829,f812,f10625]) ).
fof(f10978,plain,
( sF0 = intersection(sF0,sF3)
| ~ spl14_4
| spl14_132 ),
inference(forward_subsumption_resolution,[],[f7695,f7010]) ).
fof(f11403,plain,
( member(x,sF2)
| ~ spl14_34 ),
inference(resolution,[],[f814,f185]) ).
fof(f11405,plain,
( member(x,sF5)
| ~ spl14_34 ),
inference(resolution,[],[f814,f6961]) ).
fof(f11414,plain,
( member(x,universal_class)
| ~ spl14_34 ),
inference(forward_demodulation,[],[f11405,f8691]) ).
fof(f11415,plain,
( $false
| ~ spl14_34
| spl14_36 ),
inference(forward_subsumption_resolution,[],[f11403,f822]) ).
fof(f11416,plain,
( ~ spl14_34
| spl14_36 ),
inference(avatar_contradiction_clause,[],[f11415]) ).
fof(f11418,plain,
( $false
| spl14_1
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f11414,f221]) ).
fof(f11419,plain,
( spl14_1
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f11418]) ).
fof(f11447,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF3) ),
inference(resolution,[],[f10605,f334]) ).
fof(f12015,plain,
( sF0 = intersection(sF0,sF3)
| ~ spl14_167 ),
inference(resolution,[],[f10627,f1031]) ).
fof(f12866,plain,
( member(y,sF8)
| subclass(sF0,sF10)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(superposition,[],[f4679,f1036]) ).
fof(f12874,plain,
( member(y,sF8)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(forward_subsumption_resolution,[],[f12866,f1031]) ).
fof(f12881,plain,
( member(y,sF6)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(forward_demodulation,[],[f12874,f4991]) ).
fof(f12888,plain,
( member(y,sF4)
| x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10) ),
inference(forward_demodulation,[],[f12881,f6978]) ).
fof(f12894,plain,
( x = not_subclass_element(sF0,sF10)
| sF0 = intersection(sF0,sF10)
| spl14_26 ),
inference(forward_subsumption_resolution,[],[f12888,f758]) ).
fof(f15998,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),intersection(X1,X0))
| subclass(intersection(X0,X1),intersection(X1,X0)) ),
inference(resolution,[],[f662,f264]) ).
fof(f16120,plain,
! [X0,X1] : subclass(intersection(X0,X1),intersection(X1,X0)),
inference(duplicate_literal_removal,[],[f15998]) ).
fof(f16231,plain,
! [X0,X1] : intersection(X0,X1) = intersection(intersection(X0,X1),intersection(X1,X0)),
inference(resolution,[],[f16120,f1031]) ).
fof(f16232,plain,
! [X0,X1] :
( ~ subclass(intersection(X0,X1),intersection(X1,X0))
| intersection(X0,X1) = intersection(X1,X0) ),
inference(resolution,[],[f16120,f7]) ).
fof(f16333,plain,
! [X0,X1] : intersection(X0,X1) = intersection(X1,X0),
inference(forward_subsumption_resolution,[],[f16232,f16120]) ).
fof(f16526,plain,
! [X0,X1] : intersection(X1,X0) = intersection(X0,intersection(X1,X0)),
inference(superposition,[],[f1060,f16333]) ).
fof(f16535,plain,
( sF0 = intersection(sF3,sF0)
| ~ spl14_4
| spl14_132 ),
inference(superposition,[],[f10978,f16333]) ).
fof(f18251,plain,
! [X0] :
( ~ member(x,X0)
| subclass(sF1,X0)
| sF1 = intersection(sF1,X0) ),
inference(superposition,[],[f3,f3556]) ).
fof(f19686,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| ~ subclass(sF13,X1)
| subclass(X0,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f347,f3]) ).
fof(f19757,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| ~ subclass(sF13,X1)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f19686]) ).
fof(f20144,plain,
! [X0] :
( ~ member(y,X0)
| subclass(sF3,X0)
| sF3 = intersection(sF3,X0) ),
inference(superposition,[],[f3,f3603]) ).
fof(f20220,plain,
! [X0] :
( ~ member(y,X0)
| sF3 = intersection(sF3,X0) ),
inference(forward_subsumption_resolution,[],[f20144,f1031]) ).
fof(f20256,plain,
( sF3 = intersection(sF3,sF0)
| ~ spl14_32 ),
inference(resolution,[],[f20220,f790]) ).
fof(f20280,plain,
( sF0 = sF3
| ~ spl14_4
| ~ spl14_32
| spl14_132 ),
inference(forward_demodulation,[],[f20256,f16535]) ).
fof(f20282,plain,
( $false
| ~ spl14_4
| ~ spl14_32
| spl14_131
| spl14_132 ),
inference(forward_subsumption_resolution,[],[f20280,f7006]) ).
fof(f20283,plain,
( ~ spl14_4
| ~ spl14_32
| spl14_131
| spl14_132 ),
inference(avatar_contradiction_clause,[],[f20282]) ).
fof(f20431,plain,
( sF3 = intersection(sF3,intersection(sF0,sF3))
| ~ spl14_32 ),
inference(superposition,[],[f16231,f20256]) ).
fof(f20435,plain,
( sF3 = intersection(sF0,sF3)
| ~ spl14_32 ),
inference(forward_demodulation,[],[f20431,f16526]) ).
fof(f20446,plain,
( sF0 = sF3
| ~ spl14_32
| ~ spl14_167 ),
inference(forward_demodulation,[],[f20435,f12015]) ).
fof(f20453,plain,
( $false
| ~ spl14_32
| spl14_131
| ~ spl14_167 ),
inference(forward_subsumption_resolution,[],[f20446,f7006]) ).
fof(f20454,plain,
( ~ spl14_32
| spl14_131
| ~ spl14_167 ),
inference(avatar_contradiction_clause,[],[f20453]) ).
fof(f20461,plain,
( ~ spl14_37
| spl14_12
| ~ spl14_13 ),
inference(avatar_split_clause,[],[f6063,f498,f494,f825]) ).
fof(f20766,plain,
! [X0] :
( ~ member(x,X0)
| sF1 = intersection(sF1,X0) ),
inference(forward_subsumption_resolution,[],[f18251,f1031]) ).
fof(f20851,definition,
( spl14_256
<=> sF0 = intersection(sF0,sF13) ),
introduced(definition,[new_symbols(definition,[spl14_256])],[avatar_definition]) ).
fof(f20852,plain,
( sF0 != intersection(sF0,sF13)
| spl14_256 ),
inference(avatar_component_clause,[],[f20851]) ).
fof(f20853,plain,
( sF0 = intersection(sF0,sF13)
| ~ spl14_256 ),
inference(avatar_component_clause,[],[f20851]) ).
fof(f20884,definition,
( spl14_258
<=> sF10 = sF13 ),
introduced(definition,[new_symbols(definition,[spl14_258])],[avatar_definition]) ).
fof(f20886,plain,
( sF10 = sF13
| ~ spl14_258 ),
inference(avatar_component_clause,[],[f20884]) ).
fof(f20899,plain,
( spl14_258
| ~ spl14_8 ),
inference(avatar_split_clause,[],[f516,f463,f20884]) ).
fof(f21188,definition,
( spl14_284
<=> subclass(sF13,sF0) ),
introduced(definition,[new_symbols(definition,[spl14_284])],[avatar_definition]) ).
fof(f21189,plain,
( subclass(sF13,sF0)
| ~ spl14_284 ),
inference(avatar_component_clause,[],[f21188]) ).
fof(f21190,plain,
( ~ subclass(sF13,sF0)
| spl14_284 ),
inference(avatar_component_clause,[],[f21188]) ).
fof(f21805,plain,
( ~ subclass(sF10,sF0)
| ~ spl14_258
| spl14_284 ),
inference(forward_demodulation,[],[f21190,f20886]) ).
fof(f21926,definition,
( spl14_308
<=> sF0 = intersection(sF0,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_308])],[avatar_definition]) ).
fof(f21927,plain,
( sF0 != intersection(sF0,sF10)
| spl14_308 ),
inference(avatar_component_clause,[],[f21926]) ).
fof(f21930,definition,
( spl14_309
<=> x = not_subclass_element(sF0,sF10) ),
introduced(definition,[new_symbols(definition,[spl14_309])],[avatar_definition]) ).
fof(f21932,plain,
( x = not_subclass_element(sF0,sF10)
| ~ spl14_309 ),
inference(avatar_component_clause,[],[f21930]) ).
fof(f21942,plain,
( spl14_308
| spl14_309
| spl14_26 ),
inference(avatar_split_clause,[],[f12894,f757,f21930,f21926]) ).
fof(f22509,plain,
( ~ subclass(sF13,sF0)
| sF0 = sF13
| ~ spl14_256 ),
inference(superposition,[],[f1061,f20853]) ).
fof(f22534,plain,
( ~ subclass(sF13,sF0)
| ~ spl14_256 ),
inference(forward_subsumption_resolution,[],[f22509,f184]) ).
fof(f22544,plain,
( ~ subclass(sF10,sF0)
| ~ spl14_256
| ~ spl14_258 ),
inference(forward_demodulation,[],[f22534,f20886]) ).
fof(f22727,plain,
( sF1 = intersection(sF1,sF0)
| ~ spl14_5 ),
inference(resolution,[],[f20766,f239]) ).
fof(f23413,plain,
( ! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) )
| ~ spl14_5 ),
inference(superposition,[],[f22,f22727]) ).
fof(f23458,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF0)
| member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1) )
| ~ spl14_5 ),
inference(resolution,[],[f23413,f335]) ).
fof(f23495,plain,
( ! [X0] :
( member(not_subclass_element(X0,sF0),sF2)
| subclass(X0,sF0)
| subclass(X0,sF0) )
| ~ spl14_5 ),
inference(resolution,[],[f23458,f3]) ).
fof(f23531,plain,
( ! [X0] :
( member(not_subclass_element(X0,sF0),sF2)
| subclass(X0,sF0) )
| ~ spl14_5 ),
inference(duplicate_literal_removal,[],[f23495]) ).
fof(f23536,plain,
( ! [X0] :
( subclass(X0,sF0)
| member(not_subclass_element(X0,sF0),sF9)
| subclass(X0,sF0)
| member(not_subclass_element(X0,sF0),sF3) )
| ~ spl14_5 ),
inference(resolution,[],[f23531,f11447]) ).
fof(f23555,plain,
( ! [X0] :
( member(not_subclass_element(X0,sF0),sF9)
| subclass(X0,sF0)
| member(not_subclass_element(X0,sF0),sF3) )
| ~ spl14_5 ),
inference(duplicate_literal_removal,[],[f23536]) ).
fof(f23587,plain,
( subclass(complement(sF9),sF0)
| member(not_subclass_element(complement(sF9),sF0),sF3)
| subclass(complement(sF9),sF0)
| ~ spl14_5 ),
inference(resolution,[],[f23555,f266]) ).
fof(f23603,plain,
( subclass(complement(sF9),sF0)
| member(not_subclass_element(complement(sF9),sF0),sF3)
| ~ spl14_5 ),
inference(duplicate_literal_removal,[],[f23587]) ).
fof(f23610,plain,
( subclass(sF10,sF0)
| member(not_subclass_element(complement(sF9),sF0),sF3)
| ~ spl14_5 ),
inference(forward_demodulation,[],[f23603,f177]) ).
fof(f23614,plain,
( member(not_subclass_element(complement(sF9),sF0),sF3)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f23610,f21805]) ).
fof(f23615,plain,
( member(not_subclass_element(sF10,sF0),sF3)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(forward_demodulation,[],[f23614,f177]) ).
fof(f24877,plain,
( member(x,sF12)
| ~ subclass(sF13,sF10)
| subclass(sF0,sF10)
| ~ spl14_309 ),
inference(superposition,[],[f19757,f21932]) ).
fof(f27569,plain,
( sF0 != intersection(sF0,sF10)
| spl14_256
| ~ spl14_258 ),
inference(forward_demodulation,[],[f20852,f20886]) ).
fof(f27582,plain,
( ~ subclass(sF13,sF10)
| subclass(sF0,sF10)
| spl14_37
| ~ spl14_309 ),
inference(forward_subsumption_resolution,[],[f24877,f826]) ).
fof(f27679,plain,
( subclass(sF0,sF10)
| ~ spl14_8
| spl14_37
| ~ spl14_309 ),
inference(forward_subsumption_resolution,[],[f27582,f465]) ).
fof(f29594,plain,
( y = not_subclass_element(sF10,sF0)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(resolution,[],[f23615,f212]) ).
fof(f29610,plain,
( ~ member(y,sF0)
| subclass(sF10,sF0)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(superposition,[],[f3,f29594]) ).
fof(f29615,plain,
( member(y,sF8)
| subclass(sF10,sF0)
| member(y,sF7)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(superposition,[],[f332,f29594]) ).
fof(f29651,plain,
( member(y,sF8)
| member(y,sF7)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f29615,f21805]) ).
fof(f29653,plain,
( subclass(sF10,sF0)
| ~ spl14_5
| ~ spl14_32
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f29610,f790]) ).
fof(f29663,plain,
( member(y,sF6)
| member(y,sF7)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(forward_demodulation,[],[f29651,f4991]) ).
fof(f29665,plain,
( $false
| ~ spl14_5
| ~ spl14_32
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f29653,f21805]) ).
fof(f29666,plain,
( ~ spl14_5
| ~ spl14_32
| ~ spl14_258
| spl14_284 ),
inference(avatar_contradiction_clause,[],[f29665]) ).
fof(f29673,plain,
( member(y,sF4)
| member(y,sF7)
| ~ spl14_5
| ~ spl14_258
| spl14_284 ),
inference(forward_demodulation,[],[f29663,f6978]) ).
fof(f29677,plain,
( member(y,sF7)
| ~ spl14_5
| spl14_26
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f29673,f758]) ).
fof(f29678,plain,
( member(y,sF3)
| ~ spl14_5
| spl14_26
| ~ spl14_258
| spl14_284 ),
inference(forward_demodulation,[],[f29677,f7057]) ).
fof(f29679,plain,
( subclass(sF10,sF0)
| ~ spl14_258
| ~ spl14_284 ),
inference(forward_demodulation,[],[f21189,f20886]) ).
fof(f29684,plain,
( $false
| ~ spl14_256
| ~ spl14_258
| ~ spl14_284 ),
inference(forward_subsumption_resolution,[],[f29679,f22544]) ).
fof(f29685,plain,
( ~ spl14_256
| ~ spl14_258
| ~ spl14_284 ),
inference(avatar_contradiction_clause,[],[f29684]) ).
fof(f29688,plain,
( ~ spl14_308
| spl14_256
| ~ spl14_258 ),
inference(avatar_split_clause,[],[f27569,f20884,f20851,f21926]) ).
fof(f29736,plain,
( ~ subclass(sF10,sF0)
| sF0 = sF10
| ~ spl14_8
| spl14_37
| ~ spl14_309 ),
inference(resolution,[],[f27679,f7]) ).
fof(f29737,plain,
( sF0 = sF10
| ~ spl14_8
| spl14_37
| ~ spl14_258
| ~ spl14_284
| ~ spl14_309 ),
inference(forward_subsumption_resolution,[],[f29736,f29679]) ).
fof(f29740,plain,
( $false
| ~ spl14_8
| spl14_37
| ~ spl14_258
| ~ spl14_284
| ~ spl14_309 ),
inference(forward_subsumption_resolution,[],[f29737,f517]) ).
fof(f29741,plain,
( ~ spl14_8
| spl14_37
| ~ spl14_258
| ~ spl14_284
| ~ spl14_309 ),
inference(avatar_contradiction_clause,[],[f29740]) ).
fof(f29747,plain,
( $false
| spl14_3
| ~ spl14_26 ),
inference(forward_subsumption_resolution,[],[f8317,f230]) ).
fof(f29748,plain,
( spl14_3
| ~ spl14_26 ),
inference(avatar_contradiction_clause,[],[f29747]) ).
fof(f29765,plain,
( member(x,sF9)
| sF0 = intersection(sF0,sF13)
| ~ spl14_119 ),
inference(forward_demodulation,[],[f5686,f4989]) ).
fof(f29916,plain,
( $false
| spl14_3
| ~ spl14_33 ),
inference(forward_subsumption_resolution,[],[f8702,f230]) ).
fof(f29917,plain,
( spl14_3
| ~ spl14_33 ),
inference(avatar_contradiction_clause,[],[f29916]) ).
fof(f29942,plain,
( sF0 = intersection(sF0,sF13)
| spl14_34
| ~ spl14_119 ),
inference(forward_subsumption_resolution,[],[f29765,f813]) ).
fof(f30038,plain,
( sF0 = intersection(sF0,sF10)
| spl14_34
| ~ spl14_119
| ~ spl14_258 ),
inference(forward_demodulation,[],[f29942,f20886]) ).
fof(f30074,plain,
( $false
| spl14_34
| ~ spl14_119
| ~ spl14_258
| spl14_308 ),
inference(forward_subsumption_resolution,[],[f30038,f21927]) ).
fof(f30075,plain,
( spl14_34
| ~ spl14_119
| ~ spl14_258
| spl14_308 ),
inference(avatar_contradiction_clause,[],[f30074]) ).
fof(f30089,plain,
( $false
| spl14_4
| ~ spl14_5
| spl14_26
| ~ spl14_258
| spl14_284 ),
inference(forward_subsumption_resolution,[],[f29678,f233]) ).
fof(f30090,plain,
( spl14_4
| ~ spl14_5
| spl14_26
| ~ spl14_258
| spl14_284 ),
inference(avatar_contradiction_clause,[],[f30089]) ).
cnf(s1,plain,
( ~ spl14_1
| spl14_2 ),
inference(sat_conversion,[],[f226]) ).
cnf(s2,plain,
( ~ spl14_3
| spl14_4 ),
inference(sat_conversion,[],[f235]) ).
cnf(s3,plain,
( ~ spl14_1
| spl14_5 ),
inference(sat_conversion,[],[f240]) ).
cnf(s5,plain,
( spl14_8
| spl14_9 ),
inference(sat_conversion,[],[f470]) ).
cnf(s7,plain,
( spl14_12
| spl14_13 ),
inference(sat_conversion,[],[f501]) ).
cnf(s52,plain,
( spl14_71
| spl14_72 ),
inference(sat_conversion,[],[f1300]) ).
cnf(s114,plain,
( spl14_1
| spl14_8
| ~ spl14_9 ),
inference(sat_conversion,[],[f5093]) ).
cnf(s123,plain,
( spl14_32
| spl14_119 ),
inference(sat_conversion,[],[f5434]) ).
cnf(s125,plain,
( spl14_3
| spl14_119 ),
inference(sat_conversion,[],[f5446]) ).
cnf(s158,plain,
( spl14_1
| ~ spl14_36 ),
inference(sat_conversion,[],[f5812]) ).
cnf(s161,plain,
( spl14_1
| spl14_12
| ~ spl14_13 ),
inference(sat_conversion,[],[f6069]) ).
cnf(s190,plain,
( ~ spl14_20
| spl14_94 ),
inference(sat_conversion,[],[f6792]) ).
cnf(s192,plain,
( ~ spl14_12
| ~ spl14_90
| ~ spl14_94 ),
inference(sat_conversion,[],[f6994]) ).
cnf(s218,plain,
( ~ spl14_12
| spl14_36
| ~ spl14_72
| ~ spl14_119
| spl14_131 ),
inference(sat_conversion,[],[f7630]) ).
cnf(s221,plain,
( ~ spl14_12
| ~ spl14_131 ),
inference(sat_conversion,[],[f7654]) ).
cnf(s226,plain,
( spl14_33
| ~ spl14_71
| spl14_72 ),
inference(sat_conversion,[],[f7685]) ).
cnf(s227,plain,
( spl14_3
| ~ spl14_4 ),
inference(sat_conversion,[],[f7702]) ).
cnf(s228,plain,
( ~ spl14_3
| spl14_32 ),
inference(sat_conversion,[],[f7704]) ).
cnf(s237,plain,
( ~ spl14_20
| spl14_90 ),
inference(sat_conversion,[],[f7863]) ).
cnf(s250,plain,
( ~ spl14_8
| ~ spl14_12
| ~ spl14_38
| spl14_39 ),
inference(sat_conversion,[],[f8193]) ).
cnf(s251,plain,
( spl14_20
| ~ spl14_39 ),
inference(sat_conversion,[],[f8225]) ).
cnf(s260,plain,
( ~ spl14_4
| ~ spl14_26 ),
inference(sat_conversion,[],[f8320]) ).
cnf(s273,plain,
( ~ spl14_2
| ~ spl14_36 ),
inference(sat_conversion,[],[f10446]) ).
cnf(s275,plain,
( spl14_8
| ~ spl14_9
| ~ spl14_38 ),
inference(sat_conversion,[],[f10494]) ).
cnf(s309,plain,
( ~ spl14_1
| spl14_34
| spl14_38 ),
inference(sat_conversion,[],[f10838]) ).
cnf(s310,plain,
( spl14_34
| spl14_38
| ~ spl14_132
| spl14_167 ),
inference(sat_conversion,[],[f10839]) ).
cnf(s337,plain,
( ~ spl14_34
| spl14_36 ),
inference(sat_conversion,[],[f11416]) ).
cnf(s338,plain,
( spl14_1
| ~ spl14_34 ),
inference(sat_conversion,[],[f11419]) ).
cnf(s403,plain,
( ~ spl14_4
| ~ spl14_32
| spl14_131
| spl14_132 ),
inference(sat_conversion,[],[f20283]) ).
cnf(s409,plain,
( ~ spl14_32
| spl14_131
| ~ spl14_167 ),
inference(sat_conversion,[],[f20454]) ).
cnf(s410,plain,
( spl14_12
| ~ spl14_13
| ~ spl14_37 ),
inference(sat_conversion,[],[f20461]) ).
cnf(s449,plain,
( ~ spl14_8
| spl14_258 ),
inference(sat_conversion,[],[f20899]) ).
cnf(s553,plain,
( spl14_26
| spl14_308
| spl14_309 ),
inference(sat_conversion,[],[f21942]) ).
cnf(s687,plain,
( ~ spl14_5
| ~ spl14_32
| ~ spl14_258
| spl14_284 ),
inference(sat_conversion,[],[f29666]) ).
cnf(s688,plain,
( ~ spl14_256
| ~ spl14_258
| ~ spl14_284 ),
inference(sat_conversion,[],[f29685]) ).
cnf(s689,plain,
( spl14_256
| ~ spl14_258
| ~ spl14_308 ),
inference(sat_conversion,[],[f29688]) ).
cnf(s692,plain,
( ~ spl14_8
| spl14_37
| ~ spl14_258
| ~ spl14_284
| ~ spl14_309 ),
inference(sat_conversion,[],[f29741]) ).
cnf(s693,plain,
( spl14_3
| ~ spl14_26 ),
inference(sat_conversion,[],[f29748]) ).
cnf(s721,plain,
( spl14_3
| ~ spl14_33 ),
inference(sat_conversion,[],[f29917]) ).
cnf(s752,plain,
( spl14_34
| ~ spl14_119
| ~ spl14_258
| spl14_308 ),
inference(sat_conversion,[],[f30075]) ).
cnf(s755,plain,
( spl14_4
| ~ spl14_5
| spl14_26
| ~ spl14_258
| spl14_284 ),
inference(sat_conversion,[],[f30090]) ).
cnf(s765,plain,
( spl14_8
| spl14_1 ),
inference(rat,[],[s114,s5]) ).
cnf(s766,plain,
( spl14_12
| spl14_1 ),
inference(rat,[],[s7,s161]) ).
cnf(s767,plain,
( spl14_3
| spl14_1 ),
inference(rat,[],[s226,s52,s218,s125,s721,s158,s221,s766]) ).
cnf(s768,plain,
( ~ spl14_38
| ~ spl14_8
| ~ spl14_12 ),
inference(rat,[],[s192,s190,s237,s251,s250]) ).
cnf(s769,plain,
spl14_1,
inference(rat,[],[s768,s310,s403,s409,s2,s228,s767,s221,s766,s765,s338]) ).
cnf(s770,plain,
spl14_5,
inference(rat,[],[s3,s769]) ).
cnf(s771,plain,
spl14_2,
inference(rat,[],[s1,s769]) ).
cnf(s773,plain,
~ spl14_36,
inference(rat,[],[s273,s771]) ).
cnf(s777,plain,
~ spl14_34,
inference(rat,[],[s337,s773]) ).
cnf(s782,plain,
spl14_38,
inference(rat,[],[s309,s769,s777]) ).
cnf(s783,plain,
( spl14_119
| ~ spl14_8
| spl14_37 ),
inference(rat,[],[s553,s689,s692,s688,s260,s687,s2,s123,s125,s449,s770]) ).
cnf(s784,plain,
( spl14_3
| spl14_284
| ~ spl14_258 ),
inference(rat,[],[s755,s227,s693,s770]) ).
cnf(s785,plain,
( spl14_284
| ~ spl14_258 ),
inference(rat,[],[s228,s687,s784,s770]) ).
cnf(s786,plain,
( ~ spl14_256
| ~ spl14_258 ),
inference(rat,[],[s785,s688]) ).
cnf(s787,plain,
( ~ spl14_308
| ~ spl14_258 ),
inference(rat,[],[s786,s689]) ).
cnf(s788,plain,
( ~ spl14_119
| ~ spl14_258 ),
inference(rat,[],[s787,s752,s777]) ).
cnf(s789,plain,
( ~ spl14_8
| spl14_37 ),
inference(rat,[],[s788,s783,s449]) ).
cnf(s790,plain,
spl14_8,
inference(rat,[],[s275,s5,s782]) ).
cnf(s792,plain,
~ spl14_12,
inference(rat,[],[s768,s782,s790]) ).
cnf(s793,plain,
spl14_37,
inference(rat,[],[s789,s790]) ).
cnf(s799,plain,
spl14_13,
inference(rat,[],[s7,s792]) ).
cnf(s800,plain,
$false,
inference(rat,[],[s410,s792,s793,s799]) ).
fof(f30366,plain,
$false,
inference(avatar_sat_refutation,[],[s800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET139-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n005.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 00:52:17 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 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
% 12.50/2.61 % (332974)Input is clausal, will run a generic CNF schedule.
% 12.50/2.61 % (332983)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1830988452:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.50/2.61 % (332979)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=2400547160:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.50/2.61 % (332980)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=820565465:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.50/2.61 % (332981)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=767652352:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.50/2.61 % (332982)lrs+10_1_sil=8000:sp=occurrence:random_seed=299336485:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.50/2.61 % (332983)Instruction limit reached!
% 12.50/2.61 % (332983)------------------------------
% 12.50/2.61 % (332983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.50/2.61 % (332983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.50/2.61 % (332983)CaDiCaL version: 2.1.3
% 12.50/2.61 % (332983)Termination reason: Instruction limit
% 12.50/2.61 % (332983)Termination phase: Saturation
% 12.50/2.61 % (332983)Time elapsed: 0.037 s
% 12.50/2.61 % (332983)Peak memory usage: 89 MB
% 12.50/2.61 % (332983)Instructions burned: 117 (million)
% 12.50/2.61 % (332982)Refutation not found, incomplete strategy
% 12.50/2.61 % (332982)------------------------------
% 12.50/2.61 % (332982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.50/2.61 % (332982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.50/2.61 % (332982)CaDiCaL version: 2.1.3
% 12.50/2.61 % (332982)Termination reason: Refutation not found, incomplete strategy
% 12.50/2.61 % (332982)Time elapsed: 0.003 s
% 12.50/2.61 % (332982)Peak memory usage: 88 MB
% 12.50/2.61 % (332982)Instructions burned: 3 (million)
% 12.50/2.61 % (332984)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1182539868:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.50/2.61 % (332985)dis-21_1_sil=8000:lcm=predicate:random_seed=2707139027:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.50/2.61 % (332985)Instruction limit reached!
% 12.50/2.61 % (332985)------------------------------
% 12.50/2.61 % (332985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.50/2.61 % (332985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.50/2.61 % (332985)CaDiCaL version: 2.1.3
% 12.50/2.61 % (332985)Termination reason: Instruction limit
% 12.50/2.61 % (332985)Termination phase: Saturation
% 12.50/2.61 % (332985)Time elapsed: 0.065 s
% 12.50/2.61 % (332985)Peak memory usage: 89 MB
% 12.50/2.61 % (332985)Instructions burned: 118 (million)
% 12.50/2.61 % (332991)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=2840074025:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 12.50/2.61 % (332991)Refutation not found, incomplete strategy
% 12.50/2.61 % (332991)------------------------------
% 12.50/2.61 % (332991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.50/2.61 % (332991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.50/2.61 % (332991)CaDiCaL version: 2.1.3
% 12.50/2.61 % (332991)Termination reason: Refutation not found, incomplete strategy
% 12.50/2.61 % (332991)Time elapsed: 0.002 s
% 12.50/2.61 % (332991)Peak memory usage: 88 MB
% 12.50/2.61 % (332991)Instructions burned: 3 (million)
% 12.50/2.61 % (332984)Instruction limit reached!
% 12.50/2.61 % (332984)------------------------------
% 12.50/2.61 % (332984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.50/2.61 % (332984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.50/2.61 % (332984)CaDiCaL version: 2.1.3
% 12.50/2.61 % (332984)Termination reason: Instruction limit
% 12.50/2.61 % (332984)Termination phase: Saturation
% 12.50/2.61 % (332984)Time elapsed: 0.135 s
% 12.50/2.61 % (332984)Peak memory usage: 90 MB
% 12.50/2.61 % (332984)Instructions burned: 181 (million)
% 12.50/2.61 % (332982)------------------------------
% 12.50/2.61 % (332982)------------------------------
% 16.44/3.27 % (332994)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3580499107: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.44/3.27 % (332991)------------------------------
% 16.44/3.27 % (332991)------------------------------
% 16.44/3.27 % (332996)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3710845508:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 16.44/3.27 % (332996)Refutation not found, incomplete strategy
% 16.44/3.27 % (332996)------------------------------
% 16.44/3.27 % (332996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (332996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (332996)CaDiCaL version: 2.1.3
% 16.44/3.27 % (332996)Termination reason: Refutation not found, incomplete strategy
% 16.44/3.27 % (332996)Time elapsed: 0.003 s
% 16.44/3.27 % (332996)Peak memory usage: 88 MB
% 16.44/3.27 % (332996)Instructions burned: 3 (million)
% 16.44/3.27 % (332994)Instruction limit reached!
% 16.44/3.27 % (332994)------------------------------
% 16.44/3.27 % (332994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (332994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (332994)CaDiCaL version: 2.1.3
% 16.44/3.27 % (332994)Termination reason: Instruction limit
% 16.44/3.27 % (332994)Termination phase: Saturation
% 16.44/3.27 % (332994)Time elapsed: 0.106 s
% 16.44/3.27 % (332994)Peak memory usage: 90 MB
% 16.44/3.27 % (332994)Instructions burned: 190 (million)
% 16.44/3.27 % (332999)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=990808359:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.44/3.27 % (332997)lrs+10_64_to=lpo:sil=8000:random_seed=33370670:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 16.44/3.27 % (332999)Instruction limit reached!
% 16.44/3.27 % (332999)------------------------------
% 16.44/3.27 % (332999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (332999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (332999)CaDiCaL version: 2.1.3
% 16.44/3.27 % (332999)Termination reason: Instruction limit
% 16.44/3.27 % (332999)Termination phase: Saturation
% 16.44/3.27 % (332999)Time elapsed: 0.067 s
% 16.44/3.27 % (332999)Peak memory usage: 90 MB
% 16.44/3.27 % (332999)Instructions burned: 198 (million)
% 16.44/3.27 % (332997)Instruction limit reached!
% 16.44/3.27 % (332997)------------------------------
% 16.44/3.27 % (332997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (332997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (332997)CaDiCaL version: 2.1.3
% 16.44/3.27 % (332997)Termination reason: Instruction limit
% 16.44/3.27 % (332997)Termination phase: Saturation
% 16.44/3.27 % (332997)Time elapsed: 0.077 s
% 16.44/3.27 % (332997)Peak memory usage: 89 MB
% 16.44/3.27 % (332997)Instructions burned: 128 (million)
% 16.44/3.27 % (333001)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=267122863:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 16.44/3.27 % (332996)------------------------------
% 16.44/3.27 % (332996)------------------------------
% 16.44/3.27 % (333004)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1562561730:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 16.44/3.27 % (333001)Instruction limit reached!
% 16.44/3.27 % (333001)------------------------------
% 16.44/3.27 % (333001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333001)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333001)Termination reason: Instruction limit
% 16.44/3.27 % (333001)Termination phase: Saturation
% 16.44/3.27 % (333001)Time elapsed: 0.109 s
% 16.44/3.27 % (333001)Peak memory usage: 91 MB
% 16.44/3.27 % (333001)Instructions burned: 157 (million)
% 16.44/3.27 % (333005)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=2575667952:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 16.44/3.27 % (333005)Instruction limit reached!
% 16.44/3.27 % (333005)------------------------------
% 16.44/3.27 % (333005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333005)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333005)Termination reason: Instruction limit
% 16.44/3.27 % (333005)Termination phase: Saturation
% 16.44/3.27 % (333005)Time elapsed: 0.068 s
% 16.44/3.27 % (333005)Peak memory usage: 90 MB
% 16.44/3.27 % (333005)Instructions burned: 107 (million)
% 16.44/3.27 % (333007)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2080555900:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 16.44/3.27 % (333007)Refutation not found, incomplete strategy
% 16.44/3.27 % (333007)------------------------------
% 16.44/3.27 % (333007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333007)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333007)Termination reason: Refutation not found, incomplete strategy
% 16.44/3.27 % (333007)Time elapsed: 0.005 s
% 16.44/3.27 % (333007)Peak memory usage: 88 MB
% 16.44/3.27 % (333007)Instructions burned: 7 (million)
% 16.44/3.27 % (333009)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=376900156:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 16.44/3.27 % (333011)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2033478651:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 16.44/3.27 % (333009)Instruction limit reached!
% 16.44/3.27 % (333009)------------------------------
% 16.44/3.27 % (333009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333009)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333009)Termination reason: Instruction limit
% 16.44/3.27 % (333009)Termination phase: Saturation
% 16.44/3.27 % (333009)Time elapsed: 0.167 s
% 16.44/3.27 % (333009)Peak memory usage: 90 MB
% 16.44/3.27 % (333009)Instructions burned: 242 (million)
% 16.44/3.27 % (333007)------------------------------
% 16.44/3.27 % (333007)------------------------------
% 16.44/3.27 % (333015)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=877998064:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 16.44/3.27 % (333016)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3184738821:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 16.44/3.27 % (333015)Instruction limit reached!
% 16.44/3.27 % (333015)------------------------------
% 16.44/3.27 % (333015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333015)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333015)Termination reason: Instruction limit
% 16.44/3.27 % (333015)Termination phase: Saturation
% 16.44/3.27 % (333015)Time elapsed: 0.099 s
% 16.44/3.27 % (333015)Peak memory usage: 90 MB
% 16.44/3.27 % (333015)Instructions burned: 135 (million)
% 16.44/3.27 % (333019)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=976582765:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 16.44/3.27 % (333016)Instruction limit reached!
% 16.44/3.27 % (333016)------------------------------
% 16.44/3.27 % (333016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333016)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333016)Termination reason: Instruction limit
% 16.44/3.27 % (333016)Termination phase: Saturation
% 16.44/3.27 % (333016)Time elapsed: 0.293 s
% 16.44/3.27 % (333016)Peak memory usage: 93 MB
% 16.44/3.27 % (333016)Instructions burned: 499 (million)
% 16.44/3.27 % (333019)Instruction limit reached!
% 16.44/3.27 % (333019)------------------------------
% 16.44/3.27 % (333019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333019)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333019)Termination reason: Instruction limit
% 16.44/3.27 % (333019)Termination phase: Saturation
% 16.44/3.27 % (333019)Time elapsed: 0.124 s
% 16.44/3.27 % (333019)Peak memory usage: 90 MB
% 16.44/3.27 % (333019)Instructions burned: 192 (million)
% 16.44/3.27 % (333021)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3032563138:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 16.44/3.27 % (333022)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1744487302:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 16.44/3.27 % (333004)Instruction limit reached!
% 16.44/3.27 % (333004)------------------------------
% 16.44/3.27 % (333004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333004)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333004)Termination reason: Instruction limit
% 16.44/3.27 % (333004)Termination phase: Saturation
% 16.44/3.27 % (333004)Time elapsed: 1.137 s
% 16.44/3.27 % (333004)Peak memory usage: 150 MB
% 16.44/3.27 % (333004)Instructions burned: 3395 (million)
% 16.44/3.27 % (333021)Instruction limit reached!
% 16.44/3.27 % (333021)------------------------------
% 16.44/3.27 % (333021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333021)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333021)Termination reason: Instruction limit
% 16.44/3.27 % (333021)Termination phase: Saturation
% 16.44/3.27 % (333021)Time elapsed: 0.177 s
% 16.44/3.27 % (333021)Peak memory usage: 92 MB
% 16.44/3.27 % (333021)Instructions burned: 265 (million)
% 16.44/3.27 % (333022)Instruction limit reached!
% 16.44/3.27 % (333022)------------------------------
% 16.44/3.27 % (333022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333022)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333022)Termination reason: Instruction limit
% 16.44/3.27 % (333022)Termination phase: Saturation
% 16.44/3.27 % (333022)Time elapsed: 0.115 s
% 16.44/3.27 % (333022)Peak memory usage: 90 MB
% 16.44/3.27 % (333022)Instructions burned: 157 (million)
% 16.44/3.27 % (333025)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=4171104712:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 16.44/3.27 % (333026)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2931103723:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 16.44/3.27 % (333027)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1959456697:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 16.44/3.27 % (332979)First to succeed.
% 16.44/3.27 % (332979)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-332974"
% 16.44/3.27 % (333027)Instruction limit reached!
% 16.44/3.27 % (333027)------------------------------
% 16.44/3.27 % (333027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333027)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333027)Termination reason: Instruction limit
% 16.44/3.27 % (333027)Termination phase: Saturation
% 16.44/3.27 % (333027)Time elapsed: 0.103 s
% 16.44/3.27 % (333027)Peak memory usage: 90 MB
% 16.44/3.27 % (333027)Instructions burned: 180 (million)
% 16.44/3.27 % (333026)Instruction limit reached!
% 16.44/3.27 % (333026)------------------------------
% 16.44/3.27 % (333026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.27 % (333026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.27 % (333026)CaDiCaL version: 2.1.3
% 16.44/3.27 % (333026)Termination reason: Instruction limit
% 16.44/3.27 % (333026)Termination phase: Saturation
% 16.44/3.27 % (333026)Time elapsed: 0.254 s
% 16.44/3.27 % (333026)Peak memory usage: 89 MB
% 16.44/3.27 % (333026)Instructions burned: 539 (million)
% 16.44/3.27 % (332979)Refutation found. Thanks to Tanya!
% 16.44/3.27 % SZS status Unsatisfiable for theBenchmark
% 16.44/3.27 % SZS output start Proof for theBenchmark
% See solution above
% 17.56/3.46 % (332979)------------------------------
% 17.56/3.46 % (332979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.46 % (332979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.46 % (332979)CaDiCaL version: 2.1.3
% 17.56/3.46 % (332979)Termination reason: Refutation
% 17.56/3.46 % (332979)Time elapsed: 1.976 s
% 17.56/3.46 % (332979)Peak memory usage: 145 MB
% 17.56/3.46 % (332979)Instructions burned: 2995 (million)
% 17.56/3.46 % (332979)------------------------------
% 17.56/3.46 % (332979)------------------------------
% 17.56/3.46 % (332974)Success in time 2.404 s
% 17.56/3.46 % Vampire exiting
%------------------------------------------------------------------------------