%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET133-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:14 PM UTC 2026
% Result : Unsatisfiable 13.34s 3.20s
% Output : Refutation 18.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 50
% Syntax : Number of formulae : 293 ( 79 unt; 30 def)
% Number of atoms : 688 ( 120 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 608 ( 213 ~; 380 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 11 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 16 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 21 con; 0-2 aty)
% Number of variables : 244 ( 0 sgn 244 !; 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(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(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,
member(u,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_member_of_triple_1) ).
fof(f103,negated_conjecture,
member(v,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_member_of_triple_2) ).
fof(f104,negated_conjecture,
member(w,x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_member_of_triple_3) ).
fof(f105,negated_conjecture,
~ subclass(set_builder(u,set_builder(v,set_builder(w,null_class))),x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1_to_member_of_triple_4) ).
fof(f111,plain,
! [X0,X1] : set_builder(X0,X1) = complement(intersection(complement(unordered_pair(X0,X0)),complement(X1))),
inference(definition_unfolding,[],[f101,f26,f12]) ).
fof(f155,plain,
~ subclass(complement(intersection(complement(unordered_pair(u,u)),complement(complement(intersection(complement(unordered_pair(v,v)),complement(complement(intersection(complement(unordered_pair(w,w)),complement(null_class))))))))),x),
inference(definition_unfolding,[],[f105,f111,f111,f111]) ).
fof(f159,definition,
sF0 = unordered_pair(u,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f160,plain,
unordered_pair(u,u) = sF0,
inference(reorient_equations,[],[f159]) ).
fof(f161,definition,
sF1 = complement(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f162,plain,
complement(sF0) = sF1,
inference(reorient_equations,[],[f161]) ).
fof(f163,definition,
sF2 = unordered_pair(v,v),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f164,plain,
unordered_pair(v,v) = sF2,
inference(reorient_equations,[],[f163]) ).
fof(f165,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f166,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f165]) ).
fof(f167,definition,
sF4 = unordered_pair(w,w),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f168,plain,
unordered_pair(w,w) = sF4,
inference(reorient_equations,[],[f167]) ).
fof(f169,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f170,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f169]) ).
fof(f171,definition,
sF6 = complement(null_class),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f172,plain,
complement(null_class) = sF6,
inference(reorient_equations,[],[f171]) ).
fof(f173,definition,
sF7 = intersection(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f174,plain,
intersection(sF5,sF6) = sF7,
inference(reorient_equations,[],[f173]) ).
fof(f175,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f176,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f175]) ).
fof(f177,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f178,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f177]) ).
fof(f179,definition,
sF10 = intersection(sF3,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f180,plain,
intersection(sF3,sF9) = sF10,
inference(reorient_equations,[],[f179]) ).
fof(f181,definition,
sF11 = complement(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f182,plain,
complement(sF10) = sF11,
inference(reorient_equations,[],[f181]) ).
fof(f183,definition,
sF12 = complement(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f184,plain,
complement(sF11) = sF12,
inference(reorient_equations,[],[f183]) ).
fof(f185,definition,
sF13 = intersection(sF1,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f186,plain,
intersection(sF1,sF12) = sF13,
inference(reorient_equations,[],[f185]) ).
fof(f187,definition,
sF14 = complement(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f188,plain,
complement(sF13) = sF14,
inference(reorient_equations,[],[f187]) ).
fof(f189,plain,
~ subclass(sF14,x),
inference(definition_folding,[],[f155,f188,f186,f184,f182,f180,f178,f176,f174,f172,f170,f168,f166,f164,f162,f160]) ).
fof(f193,plain,
! [X0] :
( ~ member(X0,sF13)
| member(X0,sF12) ),
inference(superposition,[],[f22,f186]) ).
fof(f194,plain,
! [X0] :
( ~ member(X0,sF10)
| member(X0,sF9) ),
inference(superposition,[],[f22,f180]) ).
fof(f195,plain,
! [X0] :
( ~ member(X0,sF7)
| member(X0,sF6) ),
inference(superposition,[],[f22,f174]) ).
fof(f196,plain,
! [X0] :
( ~ member(X0,sF12)
| ~ member(X0,sF11) ),
inference(superposition,[],[f24,f184]) ).
fof(f201,plain,
! [X0] :
( ~ member(X0,sF11)
| ~ member(X0,sF10) ),
inference(superposition,[],[f24,f182]) ).
fof(f203,plain,
! [X0] :
( ~ member(X0,sF14)
| ~ member(X0,sF13) ),
inference(superposition,[],[f24,f188]) ).
fof(f204,plain,
! [X0,X1] :
( ~ member(not_subclass_element(complement(X0),X1),X0)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f2,f24]) ).
fof(f205,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f206,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f207,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,null_class) ),
inference(superposition,[],[f24,f172]) ).
fof(f223,plain,
! [X0] :
( ~ member(not_subclass_element(sF14,X0),sF13)
| subclass(sF14,X0) ),
inference(resolution,[],[f203,f2]) ).
fof(f227,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X2)
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f23,f3]) ).
fof(f228,plain,
! [X0] :
( ~ member(X0,sF12)
| member(X0,sF13)
| ~ member(X0,sF1) ),
inference(superposition,[],[f23,f186]) ).
fof(f229,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF10)
| ~ member(X0,sF3) ),
inference(superposition,[],[f23,f180]) ).
fof(f235,plain,
! [X0] :
( ~ member(X0,sF2)
| v = X0
| v = X0 ),
inference(superposition,[],[f8,f164]) ).
fof(f236,plain,
! [X0] :
( ~ member(X0,sF4)
| w = X0
| w = X0 ),
inference(superposition,[],[f8,f168]) ).
fof(f237,plain,
! [X0] :
( ~ member(X0,sF0)
| u = X0
| u = X0 ),
inference(superposition,[],[f8,f160]) ).
fof(f238,plain,
! [X0] :
( ~ member(X0,sF0)
| u = X0 ),
inference(duplicate_literal_removal,[],[f237]) ).
fof(f239,plain,
! [X0] :
( ~ member(X0,sF4)
| w = X0 ),
inference(duplicate_literal_removal,[],[f236]) ).
fof(f240,plain,
! [X0] :
( ~ member(X0,sF2)
| v = X0 ),
inference(duplicate_literal_removal,[],[f235]) ).
fof(f246,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF6)
| member(X0,null_class) ),
inference(superposition,[],[f25,f172]) ).
fof(f247,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF1)
| member(X0,sF0) ),
inference(superposition,[],[f25,f162]) ).
fof(f248,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF3)
| member(X0,sF2) ),
inference(superposition,[],[f25,f166]) ).
fof(f249,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF5)
| member(X0,sF4) ),
inference(superposition,[],[f25,f170]) ).
fof(f251,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF9)
| member(X0,sF8) ),
inference(superposition,[],[f25,f178]) ).
fof(f253,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF12)
| member(X0,sF11) ),
inference(superposition,[],[f25,f184]) ).
fof(f254,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF14)
| member(X0,sF13) ),
inference(superposition,[],[f25,f188]) ).
fof(f264,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X2),X1)
| ~ subclass(X0,X1)
| subclass(X0,X2) ),
inference(resolution,[],[f1,f2]) ).
fof(f265,plain,
! [X2,X3,X0,X1] :
( ~ subclass(intersection(X0,X1),X2)
| member(X3,X2)
| ~ member(X3,X1)
| ~ member(X3,X0) ),
inference(resolution,[],[f1,f23]) ).
fof(f269,plain,
! [X0] :
( ~ subclass(x,X0)
| member(w,X0) ),
inference(resolution,[],[f1,f104]) ).
fof(f270,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,universal_class) ),
inference(resolution,[],[f265,f4]) ).
fof(f309,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f310,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(resolution,[],[f270,f2]) ).
fof(f335,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f310,f2]) ).
fof(f339,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f335]) ).
fof(f342,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),null_class)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) ),
inference(resolution,[],[f339,f246]) ).
fof(f343,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF1)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0) ),
inference(resolution,[],[f339,f247]) ).
fof(f344,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF3)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2) ),
inference(resolution,[],[f339,f248]) ).
fof(f345,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF5)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF4) ),
inference(resolution,[],[f339,f249]) ).
fof(f347,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF8) ),
inference(resolution,[],[f339,f251]) ).
fof(f349,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF11) ),
inference(resolution,[],[f339,f253]) ).
fof(f350,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF14)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF13) ),
inference(resolution,[],[f339,f254]) ).
fof(f357,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF3)
| member(not_subclass_element(X0,X1),sF8)
| member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1) ),
inference(resolution,[],[f347,f229]) ).
fof(f367,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF1)
| member(not_subclass_element(X0,X1),sF11)
| member(not_subclass_element(X0,X1),sF13)
| subclass(X0,X1) ),
inference(resolution,[],[f349,f228]) ).
fof(f375,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0)
| member(not_subclass_element(X0,X1),sF11)
| member(not_subclass_element(X0,X1),sF13)
| subclass(X0,X1) ),
inference(resolution,[],[f343,f367]) ).
fof(f383,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF13)
| member(not_subclass_element(X0,X1),sF0)
| member(not_subclass_element(X0,X1),sF11)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f375]) ).
fof(f391,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF8)
| member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1) ),
inference(resolution,[],[f344,f357]) ).
fof(f399,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF8)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f391]) ).
fof(f414,plain,
! [X0] :
( subclass(X0,sF14)
| member(not_subclass_element(X0,sF14),sF13)
| subclass(X0,sF14) ),
inference(resolution,[],[f350,f3]) ).
fof(f420,plain,
! [X0] :
( member(not_subclass_element(X0,sF14),sF13)
| subclass(X0,sF14) ),
inference(duplicate_literal_removal,[],[f414]) ).
fof(f423,plain,
! [X0] :
( member(not_subclass_element(X0,sF14),sF12)
| subclass(X0,sF14) ),
inference(resolution,[],[f420,f193]) ).
fof(f426,plain,
! [X0,X1] :
( member(not_subclass_element(X0,sF14),X1)
| ~ subclass(sF13,X1)
| subclass(X0,sF14) ),
inference(resolution,[],[f420,f1]) ).
fof(f431,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF14),sF11)
| subclass(X0,sF14) ),
inference(resolution,[],[f423,f196]) ).
fof(f514,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| member(not_subclass_element(X0,X1),X2)
| subclass(X0,X1)
| null_class = X2 ),
inference(resolution,[],[f342,f309]) ).
fof(f587,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f206,f3]) ).
fof(f647,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f587]) ).
fof(f648,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f205,f3]) ).
fof(f708,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f648]) ).
fof(f738,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f739,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f777,definition,
( spl15_12
<=> null_class = sF13 ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
fof(f779,plain,
( null_class = sF13
| ~ spl15_12 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f809,definition,
( spl15_19
<=> null_class = sF11 ),
introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition]) ).
fof(f811,plain,
( null_class = sF11
| ~ spl15_19 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f818,definition,
( spl15_21
<=> null_class = sF10 ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
fof(f819,plain,
( null_class != sF10
| spl15_21 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f820,plain,
( null_class = sF10
| ~ spl15_21 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f859,definition,
( spl15_30
<=> null_class = sF7 ),
introduced(definition,[new_symbols(definition,[spl15_30])],[avatar_definition]) ).
fof(f860,plain,
( null_class != sF7
| spl15_30 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f861,plain,
( null_class = sF7
| ~ spl15_30 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f873,definition,
( spl15_33
<=> null_class = sF6 ),
introduced(definition,[new_symbols(definition,[spl15_33])],[avatar_definition]) ).
fof(f875,plain,
( null_class = sF6
| ~ spl15_33 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ member(regular(intersection(complement(X0),X1)),X0)
| null_class = intersection(complement(X0),X1) ),
inference(resolution,[],[f739,f24]) ).
fof(f1589,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,[],[f204,f25]) ).
fof(f1644,plain,
! [X0,X1] :
( member(not_subclass_element(complement(complement(X0)),X1),X0)
| subclass(complement(complement(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f1589,f339]) ).
fof(f1735,plain,
! [X0] :
( member(not_subclass_element(sF14,X0),sF0)
| member(not_subclass_element(sF14,X0),sF11)
| subclass(sF14,X0)
| subclass(sF14,X0) ),
inference(resolution,[],[f383,f223]) ).
fof(f1748,plain,
! [X0] :
( member(not_subclass_element(sF14,X0),sF11)
| member(not_subclass_element(sF14,X0),sF0)
| subclass(sF14,X0) ),
inference(duplicate_literal_removal,[],[f1735]) ).
fof(f1770,plain,
! [X0] :
( ~ member(not_subclass_element(sF14,X0),sF10)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0) ),
inference(resolution,[],[f1748,f201]) ).
fof(f1888,plain,
( sF7 = sF10
| ~ spl15_21
| ~ spl15_30 ),
inference(forward_demodulation,[],[f861,f820]) ).
fof(f2209,plain,
! [X0] :
( member(not_subclass_element(sF14,X0),sF2)
| member(not_subclass_element(sF14,X0),sF8)
| subclass(sF14,X0)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0) ),
inference(resolution,[],[f399,f1770]) ).
fof(f2222,plain,
! [X0] :
( member(not_subclass_element(sF14,X0),sF8)
| member(not_subclass_element(sF14,X0),sF2)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0) ),
inference(duplicate_literal_removal,[],[f2209]) ).
fof(f2617,plain,
! [X0] :
( null_class = intersection(complement(X0),X0)
| null_class = intersection(complement(X0),X0) ),
inference(resolution,[],[f1042,f738]) ).
fof(f2629,plain,
! [X0] : null_class = intersection(complement(X0),X0),
inference(duplicate_literal_removal,[],[f2617]) ).
fof(f2797,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF7
| member(not_subclass_element(X0,X1),sF6) ),
inference(resolution,[],[f514,f195]) ).
fof(f2802,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF10
| member(not_subclass_element(X0,X1),sF9) ),
inference(resolution,[],[f514,f194]) ).
fof(f2804,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF11
| ~ member(not_subclass_element(X0,X1),sF10) ),
inference(resolution,[],[f514,f201]) ).
fof(f2807,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF13
| member(not_subclass_element(X0,X1),sF12) ),
inference(resolution,[],[f514,f193]) ).
fof(f2810,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF6 ),
inference(factoring,[],[f514]) ).
fof(f2812,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF7 ),
inference(duplicate_literal_removal,[],[f2797]) ).
fof(f2840,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| spl15_30 ),
inference(forward_subsumption_resolution,[],[f2812,f860]) ).
fof(f3817,plain,
! [X0] :
( subclass(complement(complement(X0)),X0)
| subclass(complement(complement(X0)),X0) ),
inference(resolution,[],[f1644,f3]) ).
fof(f3887,plain,
! [X0] : subclass(complement(complement(X0)),X0),
inference(duplicate_literal_removal,[],[f3817]) ).
fof(f3961,plain,
subclass(complement(sF8),sF7),
inference(superposition,[],[f3887,f176]) ).
fof(f3963,plain,
subclass(complement(sF11),sF10),
inference(superposition,[],[f3887,f182]) ).
fof(f3967,plain,
subclass(sF12,sF10),
inference(forward_demodulation,[],[f3963,f184]) ).
fof(f3968,plain,
subclass(sF9,sF7),
inference(forward_demodulation,[],[f3961,f178]) ).
fof(f3972,plain,
( ~ subclass(sF10,sF12)
| sF10 = sF12 ),
inference(resolution,[],[f3967,f7]) ).
fof(f3974,definition,
( spl15_127
<=> sF10 = sF12 ),
introduced(definition,[new_symbols(definition,[spl15_127])],[avatar_definition]) ).
fof(f3976,plain,
( sF10 = sF12
| ~ spl15_127 ),
inference(avatar_component_clause,[],[f3974]) ).
fof(f3978,definition,
( spl15_128
<=> subclass(sF10,sF12) ),
introduced(definition,[new_symbols(definition,[spl15_128])],[avatar_definition]) ).
fof(f3980,plain,
( ~ subclass(sF10,sF12)
| spl15_128 ),
inference(avatar_component_clause,[],[f3978]) ).
fof(f3981,plain,
( spl15_127
| ~ spl15_128 ),
inference(avatar_split_clause,[],[f3972,f3978,f3974]) ).
fof(f3982,plain,
( ~ subclass(sF7,sF9)
| sF7 = sF9 ),
inference(resolution,[],[f3968,f7]) ).
fof(f3984,definition,
( spl15_129
<=> sF7 = sF9 ),
introduced(definition,[new_symbols(definition,[spl15_129])],[avatar_definition]) ).
fof(f3986,plain,
( sF7 = sF9
| ~ spl15_129 ),
inference(avatar_component_clause,[],[f3984]) ).
fof(f3988,definition,
( spl15_130
<=> subclass(sF7,sF9) ),
introduced(definition,[new_symbols(definition,[spl15_130])],[avatar_definition]) ).
fof(f3990,plain,
( ~ subclass(sF7,sF9)
| spl15_130 ),
inference(avatar_component_clause,[],[f3988]) ).
fof(f3991,plain,
( spl15_129
| ~ spl15_130 ),
inference(avatar_split_clause,[],[f3982,f3988,f3984]) ).
fof(f4131,definition,
( spl15_131
<=> ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl15_131])],[avatar_definition]) ).
fof(f4132,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_131 ),
inference(avatar_component_clause,[],[f4131]) ).
fof(f4133,plain,
( spl15_33
| spl15_131 ),
inference(avatar_split_clause,[],[f2810,f4131,f873]) ).
fof(f4144,definition,
( spl15_134
<=> ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| ~ member(not_subclass_element(X0,X1),sF10)
| subclass(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl15_134])],[avatar_definition]) ).
fof(f4145,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_134 ),
inference(avatar_component_clause,[],[f4144]) ).
fof(f4146,plain,
( spl15_19
| spl15_134 ),
inference(avatar_split_clause,[],[f2804,f4144,f809]) ).
fof(f4159,plain,
( spl15_131
| spl15_30 ),
inference(avatar_split_clause,[],[f2840,f859,f4131]) ).
fof(f4169,definition,
( spl15_138
<=> ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl15_138])],[avatar_definition]) ).
fof(f4170,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| member(not_subclass_element(X0,X1),sF12)
| subclass(X0,X1) )
| ~ spl15_138 ),
inference(avatar_component_clause,[],[f4169]) ).
fof(f4171,plain,
( spl15_12
| spl15_138 ),
inference(avatar_split_clause,[],[f2807,f4169,f777]) ).
fof(f4322,plain,
( ! [X0] :
( subclass(X0,sF6)
| subclass(X0,sF6) )
| ~ spl15_131 ),
inference(resolution,[],[f4132,f3]) ).
fof(f4412,plain,
! [X0] : subclass(null_class,X0),
inference(superposition,[],[f708,f2629]) ).
fof(f4415,plain,
( ! [X0] : subclass(sF13,X0)
| ~ spl15_12 ),
inference(forward_demodulation,[],[f4412,f779]) ).
fof(f5017,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF10 )
| ~ spl15_134 ),
inference(resolution,[],[f4145,f514]) ).
fof(f5020,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| null_class = sF10 )
| ~ spl15_134 ),
inference(duplicate_literal_removal,[],[f5017]) ).
fof(f5029,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| spl15_21
| ~ spl15_134 ),
inference(forward_subsumption_resolution,[],[f5020,f819]) ).
fof(f5447,plain,
( spl15_131
| spl15_21
| ~ spl15_134 ),
inference(avatar_split_clause,[],[f5029,f4144,f818,f4131]) ).
fof(f6415,plain,
! [X0] :
( ~ subclass(sF13,sF11)
| subclass(X0,sF14)
| subclass(X0,sF14) ),
inference(resolution,[],[f426,f431]) ).
fof(f6461,plain,
! [X0] :
( ~ subclass(sF13,sF11)
| subclass(X0,sF14) ),
inference(duplicate_literal_removal,[],[f6415]) ).
fof(f6492,plain,
( ! [X0] : subclass(X0,sF14)
| ~ spl15_12 ),
inference(forward_subsumption_resolution,[],[f6461,f4415]) ).
fof(f6638,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2))
| ~ subclass(X0,X2)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f227,f264]) ).
fof(f6641,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,complement(X2))),X1)
| subclass(X0,intersection(X1,complement(X2)))
| ~ member(not_subclass_element(X0,intersection(X1,complement(X2))),universal_class)
| member(not_subclass_element(X0,intersection(X1,complement(X2))),X2) ),
inference(resolution,[],[f227,f25]) ).
fof(f6682,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,[],[f6638]) ).
fof(f6705,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,complement(X2))),X1)
| subclass(X0,intersection(X1,complement(X2)))
| member(not_subclass_element(X0,intersection(X1,complement(X2))),X2) ),
inference(forward_subsumption_resolution,[],[f6641,f310]) ).
fof(f7685,plain,
( ! [X0] : subclass(X0,sF6)
| ~ spl15_131 ),
inference(duplicate_literal_removal,[],[f4322]) ).
fof(f8839,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,complement(X1)))
| member(not_subclass_element(X0,intersection(X0,complement(X1))),X1)
| subclass(X0,intersection(X0,complement(X1))) ),
inference(resolution,[],[f6705,f2]) ).
fof(f8913,plain,
! [X0,X1] :
( member(not_subclass_element(X0,intersection(X0,complement(X1))),X1)
| subclass(X0,intersection(X0,complement(X1))) ),
inference(duplicate_literal_removal,[],[f8839]) ).
fof(f9022,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X0,complement(complement(X1)))),X1)
| subclass(X0,intersection(X0,complement(complement(X1)))) ),
inference(resolution,[],[f8913,f24]) ).
fof(f9175,plain,
! [X0] :
( subclass(X0,intersection(X0,complement(complement(X0))))
| subclass(X0,intersection(X0,complement(complement(X0)))) ),
inference(resolution,[],[f9022,f2]) ).
fof(f9249,plain,
! [X0] : subclass(X0,intersection(X0,complement(complement(X0)))),
inference(duplicate_literal_removal,[],[f9175]) ).
fof(f9399,plain,
! [X0] :
( ~ subclass(intersection(X0,complement(complement(X0))),X0)
| intersection(X0,complement(complement(X0))) = X0 ),
inference(resolution,[],[f9249,f7]) ).
fof(f9421,plain,
! [X0] : intersection(X0,complement(complement(X0))) = X0,
inference(forward_subsumption_resolution,[],[f9399,f647]) ).
fof(f9813,plain,
sF7 = intersection(sF7,complement(sF8)),
inference(superposition,[],[f9421,f176]) ).
fof(f9815,plain,
sF10 = intersection(sF10,complement(sF11)),
inference(superposition,[],[f9421,f182]) ).
fof(f9845,plain,
sF10 = intersection(sF10,sF12),
inference(forward_demodulation,[],[f9815,f184]) ).
fof(f9846,plain,
sF7 = intersection(sF7,sF9),
inference(forward_demodulation,[],[f9813,f178]) ).
fof(f9865,plain,
subclass(sF7,sF9),
inference(superposition,[],[f708,f9846]) ).
fof(f9869,plain,
( $false
| spl15_130 ),
inference(forward_subsumption_resolution,[],[f9865,f3990]) ).
fof(f9870,plain,
spl15_130,
inference(avatar_contradiction_clause,[],[f9869]) ).
fof(f10203,plain,
subclass(sF10,sF12),
inference(superposition,[],[f708,f9845]) ).
fof(f10207,plain,
( $false
| spl15_128 ),
inference(forward_subsumption_resolution,[],[f10203,f3980]) ).
fof(f10208,plain,
spl15_128,
inference(avatar_contradiction_clause,[],[f10207]) ).
fof(f11883,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f6682,f2]) ).
fof(f11972,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f11883]) ).
fof(f12031,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f11972,f7]) ).
fof(f12055,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f12031,f647]) ).
fof(f12111,plain,
( ! [X0] : intersection(X0,sF6) = X0
| ~ spl15_131 ),
inference(resolution,[],[f12055,f7685]) ).
fof(f12461,plain,
( sF5 = sF7
| ~ spl15_131 ),
inference(superposition,[],[f174,f12111]) ).
fof(f14530,plain,
( sF6 = complement(sF13)
| ~ spl15_12 ),
inference(superposition,[],[f172,f779]) ).
fof(f14542,plain,
( sF6 = sF14
| ~ spl15_12 ),
inference(forward_demodulation,[],[f14530,f188]) ).
fof(f15532,plain,
( member(w,sF14)
| ~ spl15_12 ),
inference(resolution,[],[f6492,f269]) ).
fof(f15536,plain,
( member(w,sF6)
| ~ spl15_12 ),
inference(forward_demodulation,[],[f15532,f14542]) ).
fof(f17654,definition,
( spl15_230
<=> member(w,sF6) ),
introduced(definition,[new_symbols(definition,[spl15_230])],[avatar_definition]) ).
fof(f17656,plain,
( member(w,sF6)
| ~ spl15_230 ),
inference(avatar_component_clause,[],[f17654]) ).
fof(f17667,plain,
( spl15_230
| ~ spl15_12 ),
inference(avatar_split_clause,[],[f15536,f777,f17654]) ).
fof(f18009,plain,
( sF8 = complement(sF5)
| ~ spl15_131 ),
inference(superposition,[],[f176,f12461]) ).
fof(f18349,plain,
( ~ member(w,null_class)
| ~ spl15_230 ),
inference(resolution,[],[f17656,f207]) ).
fof(f19684,plain,
( ! [X0] :
( ~ member(X0,sF8)
| ~ member(X0,sF5) )
| ~ spl15_131 ),
inference(superposition,[],[f24,f18009]) ).
fof(f21281,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF10)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_127
| ~ spl15_138 ),
inference(forward_demodulation,[],[f4170,f3976]) ).
fof(f22063,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_21
| ~ spl15_30
| ~ spl15_127
| ~ spl15_138 ),
inference(forward_demodulation,[],[f21281,f1888]) ).
fof(f22647,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_21
| ~ spl15_30
| ~ spl15_127
| ~ spl15_138 ),
inference(forward_subsumption_resolution,[],[f22063,f195]) ).
fof(f22966,plain,
( spl15_131
| ~ spl15_21
| ~ spl15_30
| ~ spl15_127
| ~ spl15_138 ),
inference(avatar_split_clause,[],[f22647,f4169,f3974,f859,f818,f4131]) ).
fof(f23411,plain,
( sF10 != sF11
| ~ spl15_19
| spl15_21 ),
inference(forward_demodulation,[],[f819,f811]) ).
fof(f23423,plain,
( ! [X0,X1] :
( sF10 = sF11
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF9) )
| ~ spl15_19 ),
inference(forward_demodulation,[],[f2802,f811]) ).
fof(f23964,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF9) )
| ~ spl15_19
| spl15_21 ),
inference(forward_subsumption_resolution,[],[f23423,f23411]) ).
fof(f24272,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_19
| spl15_21
| ~ spl15_129 ),
inference(forward_demodulation,[],[f23964,f3986]) ).
fof(f24469,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1) )
| ~ spl15_19
| spl15_21
| ~ spl15_129 ),
inference(forward_subsumption_resolution,[],[f24272,f195]) ).
fof(f24641,plain,
( spl15_131
| ~ spl15_19
| spl15_21
| ~ spl15_129 ),
inference(avatar_split_clause,[],[f24469,f3984,f818,f809,f4131]) ).
fof(f26347,plain,
( ~ member(w,sF6)
| ~ spl15_33
| ~ spl15_230 ),
inference(forward_demodulation,[],[f18349,f875]) ).
fof(f26563,plain,
( $false
| ~ spl15_33
| ~ spl15_230 ),
inference(forward_subsumption_resolution,[],[f26347,f17656]) ).
fof(f26564,plain,
( ~ spl15_33
| ~ spl15_230 ),
inference(avatar_contradiction_clause,[],[f26563]) ).
fof(f27791,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF14,X0),sF5)
| member(not_subclass_element(sF14,X0),sF2)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0) )
| ~ spl15_131 ),
inference(resolution,[],[f19684,f2222]) ).
fof(f28260,definition,
( spl15_354
<=> u = not_subclass_element(sF14,x) ),
introduced(definition,[new_symbols(definition,[spl15_354])],[avatar_definition]) ).
fof(f28261,plain,
( u != not_subclass_element(sF14,x)
| spl15_354 ),
inference(avatar_component_clause,[],[f28260]) ).
fof(f28262,plain,
( u = not_subclass_element(sF14,x)
| ~ spl15_354 ),
inference(avatar_component_clause,[],[f28260]) ).
fof(f28264,definition,
( spl15_355
<=> v = not_subclass_element(sF14,x) ),
introduced(definition,[new_symbols(definition,[spl15_355])],[avatar_definition]) ).
fof(f28265,plain,
( v != not_subclass_element(sF14,x)
| spl15_355 ),
inference(avatar_component_clause,[],[f28264]) ).
fof(f28266,plain,
( v = not_subclass_element(sF14,x)
| ~ spl15_355 ),
inference(avatar_component_clause,[],[f28264]) ).
fof(f28294,plain,
( ~ member(u,x)
| subclass(sF14,x)
| ~ spl15_354 ),
inference(superposition,[],[f3,f28262]) ).
fof(f28321,plain,
( subclass(sF14,x)
| ~ spl15_354 ),
inference(forward_subsumption_resolution,[],[f28294,f102]) ).
fof(f28324,plain,
( $false
| ~ spl15_354 ),
inference(forward_subsumption_resolution,[],[f28321,f189]) ).
fof(f28325,plain,
~ spl15_354,
inference(avatar_contradiction_clause,[],[f28324]) ).
fof(f28336,plain,
( ~ member(v,x)
| subclass(sF14,x)
| ~ spl15_355 ),
inference(superposition,[],[f3,f28266]) ).
fof(f28361,plain,
( subclass(sF14,x)
| ~ spl15_355 ),
inference(forward_subsumption_resolution,[],[f28336,f103]) ).
fof(f28364,plain,
( $false
| ~ spl15_355 ),
inference(forward_subsumption_resolution,[],[f28361,f189]) ).
fof(f28365,plain,
~ spl15_355,
inference(avatar_contradiction_clause,[],[f28364]) ).
fof(f29500,plain,
( ! [X0] :
( member(not_subclass_element(sF14,X0),sF2)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF4) )
| ~ spl15_131 ),
inference(resolution,[],[f27791,f345]) ).
fof(f29513,plain,
( ! [X0] :
( member(not_subclass_element(sF14,X0),sF4)
| subclass(sF14,X0)
| member(not_subclass_element(sF14,X0),sF0)
| member(not_subclass_element(sF14,X0),sF2) )
| ~ spl15_131 ),
inference(duplicate_literal_removal,[],[f29500]) ).
fof(f29750,plain,
( ! [X0] :
( member(not_subclass_element(sF14,X0),sF2)
| member(not_subclass_element(sF14,X0),sF0)
| subclass(sF14,X0)
| w = not_subclass_element(sF14,X0) )
| ~ spl15_131 ),
inference(resolution,[],[f29513,f239]) ).
fof(f29785,plain,
( ! [X0] :
( member(not_subclass_element(sF14,X0),sF0)
| subclass(sF14,X0)
| w = not_subclass_element(sF14,X0)
| v = not_subclass_element(sF14,X0) )
| ~ spl15_131 ),
inference(resolution,[],[f29750,f240]) ).
fof(f29837,plain,
( ! [X0] :
( subclass(sF14,X0)
| w = not_subclass_element(sF14,X0)
| v = not_subclass_element(sF14,X0)
| u = not_subclass_element(sF14,X0) )
| ~ spl15_131 ),
inference(resolution,[],[f29785,f238]) ).
fof(f29865,plain,
( w = not_subclass_element(sF14,x)
| v = not_subclass_element(sF14,x)
| u = not_subclass_element(sF14,x)
| ~ spl15_131 ),
inference(resolution,[],[f29837,f189]) ).
fof(f29888,plain,
( w = not_subclass_element(sF14,x)
| u = not_subclass_element(sF14,x)
| ~ spl15_131
| spl15_355 ),
inference(forward_subsumption_resolution,[],[f29865,f28265]) ).
fof(f29889,plain,
( w = not_subclass_element(sF14,x)
| ~ spl15_131
| spl15_354
| spl15_355 ),
inference(forward_subsumption_resolution,[],[f29888,f28261]) ).
fof(f29901,plain,
( ~ member(w,x)
| subclass(sF14,x)
| ~ spl15_131
| spl15_354
| spl15_355 ),
inference(superposition,[],[f3,f29889]) ).
fof(f29929,plain,
( subclass(sF14,x)
| ~ spl15_131
| spl15_354
| spl15_355 ),
inference(forward_subsumption_resolution,[],[f29901,f104]) ).
fof(f29931,plain,
( $false
| ~ spl15_131
| spl15_354
| spl15_355 ),
inference(forward_subsumption_resolution,[],[f29929,f189]) ).
fof(f29932,plain,
( ~ spl15_131
| spl15_354
| spl15_355 ),
inference(avatar_contradiction_clause,[],[f29931]) ).
cnf(s147,plain,
( spl15_127
| ~ spl15_128 ),
inference(sat_conversion,[],[f3981]) ).
cnf(s148,plain,
( spl15_129
| ~ spl15_130 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s177,plain,
( spl15_33
| spl15_131 ),
inference(sat_conversion,[],[f4133]) ).
cnf(s180,plain,
( spl15_19
| spl15_134 ),
inference(sat_conversion,[],[f4146]) ).
cnf(s183,plain,
( spl15_30
| spl15_131 ),
inference(sat_conversion,[],[f4159]) ).
cnf(s185,plain,
( spl15_12
| spl15_138 ),
inference(sat_conversion,[],[f4171]) ).
cnf(s228,plain,
( spl15_21
| spl15_131
| ~ spl15_134 ),
inference(sat_conversion,[],[f5447]) ).
cnf(s276,plain,
spl15_130,
inference(sat_conversion,[],[f9870]) ).
cnf(s281,plain,
spl15_128,
inference(sat_conversion,[],[f10208]) ).
cnf(s409,plain,
( ~ spl15_12
| spl15_230 ),
inference(sat_conversion,[],[f17667]) ).
cnf(s618,plain,
( ~ spl15_21
| ~ spl15_30
| ~ spl15_127
| spl15_131
| ~ spl15_138 ),
inference(sat_conversion,[],[f22966]) ).
cnf(s680,plain,
( ~ spl15_19
| spl15_21
| ~ spl15_129
| spl15_131 ),
inference(sat_conversion,[],[f24641]) ).
cnf(s782,plain,
( ~ spl15_33
| ~ spl15_230 ),
inference(sat_conversion,[],[f26564]) ).
cnf(s812,plain,
~ spl15_354,
inference(sat_conversion,[],[f28325]) ).
cnf(s814,plain,
~ spl15_355,
inference(sat_conversion,[],[f28365]) ).
cnf(s890,plain,
( ~ spl15_131
| spl15_354
| spl15_355 ),
inference(sat_conversion,[],[f29932]) ).
cnf(s892,plain,
~ spl15_131,
inference(rat,[],[s890,s814,s812]) ).
cnf(s895,plain,
( ~ spl15_19
| spl15_21
| ~ spl15_129 ),
inference(rat,[],[s680,s892]) ).
cnf(s903,plain,
( ~ spl15_21
| ~ spl15_30
| ~ spl15_127
| ~ spl15_138 ),
inference(rat,[],[s618,s892]) ).
cnf(s911,plain,
( spl15_21
| ~ spl15_134 ),
inference(rat,[],[s228,s892]) ).
cnf(s915,plain,
spl15_30,
inference(rat,[],[s183,s892]) ).
cnf(s918,plain,
spl15_33,
inference(rat,[],[s177,s892]) ).
cnf(s919,plain,
~ spl15_230,
inference(rat,[],[s782,s918]) ).
cnf(s922,plain,
~ spl15_12,
inference(rat,[],[s409,s919]) ).
cnf(s924,plain,
spl15_138,
inference(rat,[],[s185,s922]) ).
cnf(s929,plain,
spl15_129,
inference(rat,[],[s148,s276]) ).
cnf(s930,plain,
spl15_127,
inference(rat,[],[s147,s281]) ).
cnf(s931,plain,
~ spl15_21,
inference(rat,[],[s903,s924,s915,s930]) ).
cnf(s933,plain,
~ spl15_19,
inference(rat,[],[s895,s929,s931]) ).
cnf(s934,plain,
~ spl15_134,
inference(rat,[],[s911,s931]) ).
cnf(s937,plain,
$false,
inference(rat,[],[s180,s934,s933]) ).
fof(f29936,plain,
$false,
inference(avatar_sat_refutation,[],[s937]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET133-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.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 00:47:06 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 7.77/1.96 % (3118587)Input is clausal, will run a generic CNF schedule.
% 7.77/1.96 % (3118597)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3131771652:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.77/1.96 % (3118598)dis-21_1_sil=8000:lcm=predicate:random_seed=432411508: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)
% 7.77/1.96 % (3118596)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=957013993:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.77/1.96 % (3118595)lrs+10_1_sil=8000:sp=occurrence:random_seed=3501645872:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.77/1.96 % (3118593)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2850823633:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.77/1.96 % (3118592)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=243373313:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.77/1.96 % (3118594)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=354400568:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.77/1.96 % (3118595)Refutation not found, incomplete strategy
% 7.77/1.96 % (3118595)------------------------------
% 7.77/1.96 % (3118595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.77/1.96 % (3118595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.96 % (3118595)CaDiCaL version: 2.1.3
% 7.77/1.96 % (3118595)Termination reason: Refutation not found, incomplete strategy
% 7.77/1.96 % (3118595)Time elapsed: 0.004 s
% 7.77/1.96 % (3118595)Peak memory usage: 88 MB
% 7.77/1.96 % (3118595)Instructions burned: 4 (million)
% 7.77/1.96 % (3118597)Instruction limit reached!
% 7.77/1.96 % (3118597)------------------------------
% 7.77/1.96 % (3118597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.77/1.96 % (3118597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.96 % (3118597)CaDiCaL version: 2.1.3
% 7.77/1.96 % (3118597)Termination reason: Instruction limit
% 7.77/1.96 % (3118597)Termination phase: Saturation
% 7.77/1.96 % (3118597)Time elapsed: 0.072 s
% 7.77/1.96 % (3118597)Peak memory usage: 90 MB
% 7.77/1.96 % (3118597)Instructions burned: 182 (million)
% 7.77/1.96 % (3118598)Instruction limit reached!
% 7.77/1.96 % (3118598)------------------------------
% 7.77/1.96 % (3118598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.77/1.96 % (3118598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.96 % (3118598)CaDiCaL version: 2.1.3
% 7.77/1.96 % (3118598)Termination reason: Instruction limit
% 7.77/1.96 % (3118598)Termination phase: Saturation
% 7.77/1.96 % (3118598)Time elapsed: 0.063 s
% 7.77/1.96 % (3118598)Peak memory usage: 88 MB
% 7.77/1.96 % (3118598)Instructions burned: 117 (million)
% 7.77/1.96 % (3118596)Instruction limit reached!
% 7.77/1.96 % (3118596)------------------------------
% 7.77/1.96 % (3118596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.77/1.96 % (3118596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.96 % (3118596)CaDiCaL version: 2.1.3
% 7.77/1.96 % (3118596)Termination reason: Instruction limit
% 7.77/1.96 % (3118596)Termination phase: Saturation
% 7.77/1.96 % (3118596)Time elapsed: 0.069 s
% 7.77/1.96 % (3118596)Peak memory usage: 89 MB
% 7.77/1.96 % (3118596)Instructions burned: 114 (million)
% 7.77/1.96 % (3118606)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=1213905785:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.77/1.96 % (3118606)Refutation not found, incomplete strategy
% 7.77/1.96 % (3118606)------------------------------
% 7.77/1.96 % (3118606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.77/1.96 % (3118606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.77/1.96 % (3118606)CaDiCaL version: 2.1.3
% 7.77/1.96 % (3118606)Termination reason: Refutation not found, incomplete strategy
% 7.77/1.96 % (3118606)Time elapsed: 0.002 s
% 7.77/1.96 % (3118606)Peak memory usage: 88 MB
% 7.77/1.96 % (3118606)Instructions burned: 4 (million)
% 7.77/1.96 % (3118607)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3122375802:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 15.06/2.91 % (3118608)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3194804264:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 15.06/2.91 % (3118608)Refutation not found, incomplete strategy
% 15.06/2.91 % (3118608)------------------------------
% 15.06/2.91 % (3118608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/2.91 % (3118608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.91 % (3118608)CaDiCaL version: 2.1.3
% 15.06/2.91 % (3118608)Termination reason: Refutation not found, incomplete strategy
% 15.06/2.91 % (3118608)Time elapsed: 0.003 s
% 15.06/2.91 % (3118608)Peak memory usage: 88 MB
% 15.06/2.91 % (3118608)Instructions burned: 3 (million)
% 15.06/2.91 % (3118595)------------------------------
% 15.06/2.91 % (3118595)------------------------------
% 15.06/2.91 % (3118607)Instruction limit reached!
% 15.06/2.91 % (3118607)------------------------------
% 15.06/2.91 % (3118607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/2.91 % (3118607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.91 % (3118607)CaDiCaL version: 2.1.3
% 15.06/2.91 % (3118607)Termination reason: Instruction limit
% 15.06/2.91 % (3118607)Termination phase: Saturation
% 15.06/2.91 % (3118607)Time elapsed: 0.095 s
% 15.06/2.91 % (3118607)Peak memory usage: 91 MB
% 15.06/2.91 % (3118607)Instructions burned: 190 (million)
% 15.06/2.91 % (3118606)------------------------------
% 15.06/2.91 % (3118606)------------------------------
% 15.06/2.91 % (3118614)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=632964056:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 15.06/2.91 % (3118612)lrs+10_64_to=lpo:sil=8000:random_seed=1039172980:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 15.06/2.91 % (3118613)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=226436463:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 15.06/2.91 % (3118608)------------------------------
% 15.06/2.91 % (3118608)------------------------------
% 15.06/2.91 % (3118614)Instruction limit reached!
% 15.06/2.91 % (3118614)------------------------------
% 15.06/2.91 % (3118614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/2.91 % (3118614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.91 % (3118614)CaDiCaL version: 2.1.3
% 15.06/2.91 % (3118614)Termination reason: Instruction limit
% 15.06/2.91 % (3118614)Termination phase: Saturation
% 15.06/2.91 % (3118614)Time elapsed: 0.058 s
% 15.06/2.91 % (3118614)Peak memory usage: 91 MB
% 15.06/2.91 % (3118614)Instructions burned: 159 (million)
% 15.06/2.91 % (3118612)Instruction limit reached!
% 15.06/2.91 % (3118612)------------------------------
% 15.06/2.91 % (3118612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/2.91 % (3118612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.91 % (3118612)CaDiCaL version: 2.1.3
% 15.06/2.91 % (3118612)Termination reason: Instruction limit
% 15.06/2.91 % (3118612)Termination phase: Saturation
% 15.06/2.91 % (3118612)Time elapsed: 0.079 s
% 15.06/2.91 % (3118612)Peak memory usage: 89 MB
% 15.06/2.91 % (3118612)Instructions burned: 126 (million)
% 15.06/2.91 % (3118613)Instruction limit reached!
% 15.06/2.91 % (3118613)------------------------------
% 15.06/2.91 % (3118613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.06/2.91 % (3118613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.91 % (3118613)CaDiCaL version: 2.1.3
% 15.06/2.91 % (3118613)Termination reason: Instruction limit
% 15.06/2.91 % (3118613)Termination phase: Saturation
% 15.06/2.91 % (3118613)Time elapsed: 0.114 s
% 15.06/2.91 % (3118613)Peak memory usage: 90 MB
% 15.06/2.91 % (3118613)Instructions burned: 195 (million)
% 15.06/2.91 % (3118618)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4035815016:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 15.06/2.91 % (3118619)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=3812700670:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 15.06/2.91 % (3118620)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2232117016:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 13.34/3.20 % (3118622)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3785651307:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 13.34/3.20 % (3118619)Instruction limit reached!
% 13.34/3.20 % (3118619)------------------------------
% 13.34/3.20 % (3118619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118619)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118619)Termination reason: Instruction limit
% 13.34/3.20 % (3118619)Termination phase: Saturation
% 13.34/3.20 % (3118619)Time elapsed: 0.067 s
% 13.34/3.20 % (3118619)Peak memory usage: 90 MB
% 13.34/3.20 % (3118619)Instructions burned: 107 (million)
% 13.34/3.20 % (3118620)Instruction limit reached!
% 13.34/3.20 % (3118620)------------------------------
% 13.34/3.20 % (3118620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118620)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118620)Termination reason: Instruction limit
% 13.34/3.20 % (3118620)Termination phase: Saturation
% 13.34/3.20 % (3118620)Time elapsed: 0.074 s
% 13.34/3.20 % (3118620)Peak memory usage: 89 MB
% 13.34/3.20 % (3118620)Instructions burned: 108 (million)
% 13.34/3.20 % (3118626)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=351254543:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 13.34/3.20 % (3118622)Instruction limit reached!
% 13.34/3.20 % (3118622)------------------------------
% 13.34/3.20 % (3118622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118622)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118622)Termination reason: Instruction limit
% 13.34/3.20 % (3118622)Termination phase: Saturation
% 13.34/3.20 % (3118622)Time elapsed: 0.162 s
% 13.34/3.20 % (3118622)Peak memory usage: 91 MB
% 13.34/3.20 % (3118622)Instructions burned: 243 (million)
% 13.34/3.20 % (3118627)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2545509744:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 13.34/3.20 % (3118627)Instruction limit reached!
% 13.34/3.20 % (3118627)------------------------------
% 13.34/3.20 % (3118627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118627)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118627)Termination reason: Instruction limit
% 13.34/3.20 % (3118627)Termination phase: Saturation
% 13.34/3.20 % (3118627)Time elapsed: 0.096 s
% 13.34/3.20 % (3118627)Peak memory usage: 89 MB
% 13.34/3.20 % (3118627)Instructions burned: 134 (million)
% 13.34/3.20 % (3118630)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2985166634:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 13.34/3.20 % (3118631)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3306438171:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 13.34/3.20 % (3118631)Instruction limit reached!
% 13.34/3.20 % (3118631)------------------------------
% 13.34/3.20 % (3118631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118631)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118631)Termination reason: Instruction limit
% 13.34/3.20 % (3118631)Termination phase: Saturation
% 13.34/3.20 % (3118631)Time elapsed: 0.118 s
% 13.34/3.20 % (3118631)Peak memory usage: 90 MB
% 13.34/3.20 % (3118631)Instructions burned: 192 (million)
% 13.34/3.20 % (3118630)Instruction limit reached!
% 13.34/3.20 % (3118630)------------------------------
% 13.34/3.20 % (3118630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118630)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118630)Termination reason: Instruction limit
% 13.34/3.20 % (3118630)Termination phase: Saturation
% 13.34/3.20 % (3118630)Time elapsed: 0.274 s
% 13.34/3.20 % (3118630)Peak memory usage: 95 MB
% 13.34/3.20 % (3118630)Instructions burned: 500 (million)
% 13.34/3.20 % (3118634)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=467173337:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 13.34/3.20 % (3118635)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2637631628:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 13.34/3.20 % (3118634)Instruction limit reached!
% 13.34/3.20 % (3118634)------------------------------
% 13.34/3.20 % (3118634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118634)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118634)Termination reason: Instruction limit
% 13.34/3.20 % (3118634)Termination phase: Saturation
% 13.34/3.20 % (3118634)Time elapsed: 0.169 s
% 13.34/3.20 % (3118634)Peak memory usage: 91 MB
% 13.34/3.20 % (3118634)Instructions burned: 265 (million)
% 13.34/3.20 % (3118635)Instruction limit reached!
% 13.34/3.20 % (3118635)------------------------------
% 13.34/3.20 % (3118635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118635)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118635)Termination reason: Instruction limit
% 13.34/3.20 % (3118635)Termination phase: Saturation
% 13.34/3.20 % (3118635)Time elapsed: 0.096 s
% 13.34/3.20 % (3118635)Peak memory usage: 89 MB
% 13.34/3.20 % (3118635)Instructions burned: 156 (million)
% 13.34/3.20 % (3118638)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=1693807467:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 13.34/3.20 % (3118639)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=603717384:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 13.34/3.20 % (3118618)Instruction limit reached!
% 13.34/3.20 % (3118618)------------------------------
% 13.34/3.20 % (3118618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118618)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118618)Termination reason: Instruction limit
% 13.34/3.20 % (3118618)Termination phase: Saturation
% 13.34/3.20 % (3118618)Time elapsed: 1.170 s
% 13.34/3.20 % (3118618)Peak memory usage: 146 MB
% 13.34/3.20 % (3118618)Instructions burned: 3397 (million)
% 13.34/3.20 % (3118642)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3808557589:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 13.34/3.20 % (3118639)Instruction limit reached!
% 13.34/3.20 % (3118639)------------------------------
% 13.34/3.20 % (3118639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118639)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118639)Termination reason: Instruction limit
% 13.34/3.20 % (3118639)Termination phase: Saturation
% 13.34/3.20 % (3118639)Time elapsed: 0.268 s
% 13.34/3.20 % (3118639)Peak memory usage: 89 MB
% 13.34/3.20 % (3118639)Instructions burned: 538 (million)
% 13.34/3.20 % (3118642)Instruction limit reached!
% 13.34/3.20 % (3118642)------------------------------
% 13.34/3.20 % (3118642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118642)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118642)Termination reason: Instruction limit
% 13.34/3.20 % (3118642)Termination phase: Saturation
% 13.34/3.20 % (3118642)Time elapsed: 0.050 s
% 13.34/3.20 % (3118642)Peak memory usage: 90 MB
% 13.34/3.20 % (3118642)Instructions burned: 180 (million)
% 13.34/3.20 % (3118644)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=969171163:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 13.34/3.20 % (3118645)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3581619701:i=412:gtgl=4:gtg=exists_all_2980 on theBenchmark for (2980ds/412Mi)
% 13.34/3.20 % (3118645)Instruction limit reached!
% 13.34/3.20 % (3118645)------------------------------
% 13.34/3.20 % (3118645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.34/3.20 % (3118645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.34/3.20 % (3118645)CaDiCaL version: 2.1.3
% 13.34/3.20 % (3118645)Termination reason: Instruction limit
% 13.34/3.20 % (3118645)Termination phase: Saturation
% 13.34/3.20 % (3118645)Time elapsed: 0.190 s
% 13.34/3.20 % (3118645)Peak memory usage: 90 MB
% 13.34/3.20 % (3118645)Instructions burned: 414 (million)
% 13.34/3.20 % (3118592)First to succeed.
% 13.34/3.20 % (3118592)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3118587"
% 13.34/3.20 % (3118648)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=100325458:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi)
% 13.34/3.20 % (3118592)Refutation found. Thanks to Tanya!
% 13.34/3.20 % SZS status Unsatisfiable for theBenchmark
% 13.34/3.20 % SZS output start Proof for theBenchmark
% See solution above
% 18.75/3.42 % (3118592)------------------------------
% 18.75/3.42 % (3118592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.75/3.42 % (3118592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.75/3.42 % (3118592)CaDiCaL version: 2.1.3
% 18.75/3.42 % (3118592)Termination reason: Refutation
% 18.75/3.42 % (3118592)Time elapsed: 2.193 s
% 18.75/3.42 % (3118592)Peak memory usage: 150 MB
% 18.75/3.42 % (3118592)Instructions burned: 3401 (million)
% 18.75/3.42 % (3118592)------------------------------
% 18.75/3.42 % (3118592)------------------------------
% 18.75/3.42 % (3118587)Success in time 2.594 s
% 18.75/3.42 % Vampire exiting
%------------------------------------------------------------------------------