%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET127-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 : n002.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:13 PM UTC 2026
% Result : Unsatisfiable 5.28s 1.63s
% Output : Refutation 6.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 42
% Syntax : Number of formulae : 252 ( 34 unt; 24 def)
% Number of atoms : 645 ( 91 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 690 ( 297 ~; 376 |; 0 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 18 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 11 con; 0-2 aty)
% Number of variables : 129 ( 0 sgn 129 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,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(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,singleton(y)) != unordered_pair(x,y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_set_builder_and_unordered_pair_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(f152,plain,
unordered_pair(x,y) != complement(intersection(complement(unordered_pair(x,x)),complement(unordered_pair(y,y)))),
inference(definition_unfolding,[],[f102,f108,f12]) ).
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 = intersection(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f167,plain,
intersection(sF2,sF4) = sF5,
inference(reorient_equations,[],[f166]) ).
fof(f168,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f169,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f168]) ).
fof(f170,plain,
sF0 != sF6,
inference(definition_folding,[],[f152,f169,f167,f165,f163,f161,f159,f157]) ).
fof(f171,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,sF5) ),
inference(superposition,[],[f24,f169]) ).
fof(f172,plain,
! [X0] :
( ~ member(X0,sF2)
| ~ member(X0,sF1) ),
inference(superposition,[],[f24,f161]) ).
fof(f173,plain,
! [X0] :
( ~ member(X0,sF0)
| x = X0
| y = X0 ),
inference(superposition,[],[f8,f157]) ).
fof(f174,plain,
! [X0] :
( ~ member(X0,sF3)
| y = X0
| y = X0 ),
inference(superposition,[],[f8,f163]) ).
fof(f175,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0
| x = X0 ),
inference(superposition,[],[f8,f159]) ).
fof(f176,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0 ),
inference(duplicate_literal_removal,[],[f175]) ).
fof(f177,plain,
! [X0] :
( ~ member(X0,sF3)
| y = X0 ),
inference(duplicate_literal_removal,[],[f174]) ).
fof(f178,plain,
! [X0] :
( ~ member(X0,sF4)
| ~ member(X0,sF3) ),
inference(superposition,[],[f24,f165]) ).
fof(f179,plain,
! [X0] :
( member(X0,sF2)
| ~ member(X0,sF5) ),
inference(superposition,[],[f21,f167]) ).
fof(f181,plain,
! [X0] :
( member(X0,sF6)
| ~ member(X0,universal_class)
| member(X0,sF5) ),
inference(superposition,[],[f25,f169]) ).
fof(f182,plain,
! [X0] :
( member(X0,sF2)
| ~ member(X0,universal_class)
| member(X0,sF1) ),
inference(superposition,[],[f25,f161]) ).
fof(f183,plain,
! [X0] :
( member(X0,sF4)
| ~ member(X0,universal_class)
| member(X0,sF3) ),
inference(superposition,[],[f25,f165]) ).
fof(f184,plain,
! [X0] :
( member(X0,sF4)
| ~ member(X0,sF5) ),
inference(superposition,[],[f22,f167]) ).
fof(f186,plain,
( member(x,sF0)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f157]) ).
fof(f187,plain,
( member(y,sF3)
| ~ member(y,universal_class) ),
inference(superposition,[],[f9,f163]) ).
fof(f188,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f159]) ).
fof(f190,definition,
( spl7_1
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition]) ).
fof(f191,plain,
( member(x,universal_class)
| ~ spl7_1 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f192,plain,
( ~ member(x,universal_class)
| spl7_1 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f194,definition,
( spl7_2
<=> member(x,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f196,plain,
( member(x,sF1)
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f197,plain,
( ~ spl7_1
| spl7_2 ),
inference(avatar_split_clause,[],[f188,f194,f190]) ).
fof(f199,definition,
( spl7_3
<=> member(y,universal_class) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f200,plain,
( member(y,universal_class)
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f201,plain,
( ~ member(y,universal_class)
| spl7_3 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f203,definition,
( spl7_4
<=> member(y,sF3) ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
fof(f205,plain,
( member(y,sF3)
| ~ spl7_4 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
( ~ spl7_3
| spl7_4 ),
inference(avatar_split_clause,[],[f187,f203,f199]) ).
fof(f208,definition,
( spl7_5
<=> member(x,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition]) ).
fof(f210,plain,
( member(x,sF0)
| ~ spl7_5 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
( ~ spl7_1
| spl7_5 ),
inference(avatar_split_clause,[],[f186,f208,f190]) ).
fof(f215,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f217,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF5)
| subclass(sF6,X0) ),
inference(resolution,[],[f2,f171]) ).
fof(f219,plain,
( member(y,sF0)
| ~ member(y,universal_class) ),
inference(superposition,[],[f10,f157]) ).
fof(f224,plain,
! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF3) ),
inference(resolution,[],[f184,f178]) ).
fof(f226,plain,
! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF1) ),
inference(resolution,[],[f179,f172]) ).
fof(f237,plain,
! [X0] :
( member(not_subclass_element(X0,sF6),sF5)
| ~ member(not_subclass_element(X0,sF6),universal_class)
| subclass(X0,sF6) ),
inference(resolution,[],[f3,f181]) ).
fof(f240,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF6),sF1)
| subclass(X0,sF6)
| ~ member(not_subclass_element(X0,sF6),universal_class) ),
inference(resolution,[],[f237,f226]) ).
fof(f241,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF6),sF3)
| subclass(X0,sF6)
| ~ member(not_subclass_element(X0,sF6),universal_class) ),
inference(resolution,[],[f237,f224]) ).
fof(f281,plain,
! [X0] :
( member(X0,sF5)
| ~ member(X0,sF4)
| ~ member(X0,sF2) ),
inference(superposition,[],[f23,f167]) ).
fof(f284,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF4)
| ~ member(not_subclass_element(sF6,X0),sF2)
| subclass(sF6,X0) ),
inference(resolution,[],[f281,f217]) ).
fof(f286,plain,
! [X0] :
( member(not_subclass_element(sF6,X0),sF3)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| ~ member(not_subclass_element(sF6,X0),sF2) ),
inference(resolution,[],[f284,f183]) ).
fof(f311,plain,
! [X0] :
( y = not_subclass_element(sF0,X0)
| x = not_subclass_element(sF0,X0)
| subclass(sF0,X0) ),
inference(resolution,[],[f173,f2]) ).
fof(f312,plain,
! [X0] :
( ~ member(y,X0)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| subclass(sF0,X0) ),
inference(superposition,[],[f3,f311]) ).
fof(f313,plain,
! [X0] :
( member(y,sF0)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0)
| subclass(sF0,X0) ),
inference(superposition,[],[f2,f311]) ).
fof(f314,plain,
( ~ member(y,sF3)
| subclass(sF0,sF6)
| ~ member(y,universal_class)
| x = not_subclass_element(sF0,sF6)
| subclass(sF0,sF6) ),
inference(superposition,[],[f241,f311]) ).
fof(f320,plain,
( ~ member(y,sF3)
| subclass(sF0,sF6)
| ~ member(y,universal_class)
| x = not_subclass_element(sF0,sF6) ),
inference(duplicate_literal_removal,[],[f314]) ).
fof(f321,plain,
! [X0] :
( member(y,sF0)
| subclass(sF0,X0)
| x = not_subclass_element(sF0,X0) ),
inference(duplicate_literal_removal,[],[f313]) ).
fof(f322,plain,
! [X0] :
( x = not_subclass_element(sF0,X0)
| subclass(sF0,X0)
| ~ member(y,X0) ),
inference(duplicate_literal_removal,[],[f312]) ).
fof(f324,definition,
( spl7_13
<=> ! [X0] :
( x = not_subclass_element(sF0,X0)
| subclass(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition]) ).
fof(f325,plain,
( ! [X0] :
( x = not_subclass_element(sF0,X0)
| subclass(sF0,X0) )
| ~ spl7_13 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f332,definition,
( spl7_15
<=> member(y,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_15])],[avatar_definition]) ).
fof(f334,plain,
( member(y,sF0)
| ~ spl7_15 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f335,plain,
( spl7_13
| spl7_15 ),
inference(avatar_split_clause,[],[f321,f332,f324]) ).
fof(f338,plain,
! [X0] :
( member(x,sF0)
| subclass(sF0,X0)
| subclass(sF0,X0)
| ~ member(y,X0) ),
inference(superposition,[],[f2,f322]) ).
fof(f345,plain,
! [X0] :
( member(x,sF0)
| subclass(sF0,X0)
| ~ member(y,X0) ),
inference(duplicate_literal_removal,[],[f338]) ).
fof(f349,definition,
( spl7_16
<=> ! [X0] :
( subclass(sF0,X0)
| ~ member(y,X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_16])],[avatar_definition]) ).
fof(f350,plain,
( ! [X0] :
( ~ member(y,X0)
| subclass(sF0,X0) )
| ~ spl7_16 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( spl7_16
| spl7_5 ),
inference(avatar_split_clause,[],[f345,f208,f349]) ).
fof(f355,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),sF2)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0) ),
inference(resolution,[],[f177,f286]) ).
fof(f356,plain,
! [X0] :
( subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| member(not_subclass_element(sF6,X0),sF1) ),
inference(resolution,[],[f355,f182]) ).
fof(f359,plain,
! [X0] :
( member(not_subclass_element(sF6,X0),sF1)
| ~ member(not_subclass_element(sF6,X0),universal_class)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0) ),
inference(duplicate_literal_removal,[],[f356]) ).
fof(f379,plain,
! [X0] :
( ~ member(not_subclass_element(sF6,X0),universal_class)
| x = not_subclass_element(sF6,X0)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0) ),
inference(resolution,[],[f176,f359]) ).
fof(f380,plain,
! [X0,X1] :
( x = not_subclass_element(sF6,X0)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| ~ member(not_subclass_element(sF6,X0),X1)
| ~ subclass(X1,universal_class) ),
inference(resolution,[],[f379,f1]) ).
fof(f381,plain,
! [X0,X1] :
( ~ member(not_subclass_element(sF6,X0),X1)
| y = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(forward_subsumption_resolution,[],[f380,f4]) ).
fof(f399,definition,
( spl7_21
<=> null_class = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_21])],[avatar_definition]) ).
fof(f400,plain,
( null_class != sF6
| spl7_21 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f401,plain,
( null_class = sF6
| ~ spl7_21 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f462,definition,
( spl7_35
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl7_35])],[avatar_definition]) ).
fof(f463,plain,
( null_class != sF0
| spl7_35 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f464,plain,
( null_class = sF0
| ~ spl7_35 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f505,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f215,f3]) ).
fof(f519,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f505]) ).
fof(f521,plain,
! [X0] :
( y = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0)
| subclass(sF6,X0) ),
inference(resolution,[],[f381,f2]) ).
fof(f534,plain,
! [X0] :
( y = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(duplicate_literal_removal,[],[f521]) ).
fof(f540,plain,
! [X0] :
( ~ member(y,X0)
| subclass(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(superposition,[],[f3,f534]) ).
fof(f541,plain,
! [X0] :
( member(y,sF6)
| subclass(sF6,X0)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(superposition,[],[f2,f534]) ).
fof(f547,plain,
! [X0] :
( member(y,sF6)
| subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ),
inference(duplicate_literal_removal,[],[f541]) ).
fof(f548,plain,
! [X0] :
( x = not_subclass_element(sF6,X0)
| subclass(sF6,X0)
| ~ member(y,X0) ),
inference(duplicate_literal_removal,[],[f540]) ).
fof(f553,definition,
( spl7_38
<=> ! [X0] :
( subclass(sF6,X0)
| x = not_subclass_element(sF6,X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_38])],[avatar_definition]) ).
fof(f554,plain,
( ! [X0] :
( x = not_subclass_element(sF6,X0)
| subclass(sF6,X0) )
| ~ spl7_38 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f557,definition,
( spl7_39
<=> member(y,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_39])],[avatar_definition]) ).
fof(f559,plain,
( member(y,sF6)
| ~ spl7_39 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f560,plain,
( spl7_38
| spl7_39 ),
inference(avatar_split_clause,[],[f547,f557,f553]) ).
fof(f580,plain,
! [X0] :
( ~ member(x,X0)
| subclass(sF6,X0)
| subclass(sF6,X0)
| ~ member(y,X0) ),
inference(superposition,[],[f3,f548]) ).
fof(f587,plain,
! [X0] :
( ~ member(y,X0)
| subclass(sF6,X0)
| ~ member(x,X0) ),
inference(duplicate_literal_removal,[],[f580]) ).
fof(f594,definition,
( spl7_43
<=> ! [X0] :
( subclass(sF6,X0)
| ~ member(y,X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_43])],[avatar_definition]) ).
fof(f595,plain,
( ! [X0] :
( ~ member(y,X0)
| subclass(sF6,X0) )
| ~ spl7_43 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,definition,
( spl7_44
<=> member(x,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_44])],[avatar_definition]) ).
fof(f599,plain,
( member(x,sF6)
| ~ spl7_44 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f746,plain,
( null_class != sF6
| ~ spl7_35 ),
inference(backward_demodulation,[],[f170,f464]) ).
fof(f758,plain,
( ~ spl7_21
| ~ spl7_35 ),
inference(avatar_split_clause,[],[f746,f462,f399]) ).
fof(f774,plain,
( ! [X0] :
( member(x,sF6)
| subclass(sF6,X0)
| subclass(sF6,X0) )
| ~ spl7_38 ),
inference(superposition,[],[f2,f554]) ).
fof(f777,plain,
( ! [X0] :
( member(x,sF6)
| subclass(sF6,X0) )
| ~ spl7_38 ),
inference(duplicate_literal_removal,[],[f774]) ).
fof(f782,definition,
( spl7_51
<=> ! [X0] : subclass(sF6,X0) ),
introduced(definition,[new_symbols(definition,[spl7_51])],[avatar_definition]) ).
fof(f783,plain,
( ! [X0] : subclass(sF6,X0)
| ~ spl7_51 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f784,plain,
( spl7_51
| spl7_44
| ~ spl7_38 ),
inference(avatar_split_clause,[],[f777,f553,f597,f782]) ).
fof(f785,plain,
( ! [X0] :
( ~ subclass(X0,sF6)
| sF6 = X0 )
| ~ spl7_51 ),
inference(resolution,[],[f783,f7]) ).
fof(f813,plain,
( ! [X0] :
( ~ member(x,X0)
| ~ subclass(X0,universal_class) )
| spl7_1 ),
inference(resolution,[],[f192,f1]) ).
fof(f814,plain,
( ! [X0] : ~ member(x,X0)
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f813,f4]) ).
fof(f825,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f519,f70]) ).
fof(f828,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f825,f7]) ).
fof(f829,plain,
( null_class = sF6
| null_class = sF6
| ~ spl7_51 ),
inference(resolution,[],[f825,f785]) ).
fof(f830,plain,
( null_class = sF6
| ~ spl7_51 ),
inference(duplicate_literal_removal,[],[f829]) ).
fof(f831,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f828]) ).
fof(f832,plain,
( $false
| spl7_21
| ~ spl7_51 ),
inference(forward_subsumption_resolution,[],[f830,f400]) ).
fof(f833,plain,
( spl7_21
| ~ spl7_51 ),
inference(avatar_contradiction_clause,[],[f832]) ).
fof(f867,plain,
! [X0] :
( member(x,sF6)
| subclass(sF6,X0)
| subclass(sF6,X0)
| ~ member(y,X0) ),
inference(superposition,[],[f2,f548]) ).
fof(f870,plain,
! [X0] :
( member(x,sF6)
| subclass(sF6,X0)
| ~ member(y,X0) ),
inference(duplicate_literal_removal,[],[f867]) ).
fof(f885,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f831,f519]) ).
fof(f896,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,null_class) ),
inference(superposition,[],[f22,f885]) ).
fof(f910,plain,
( ! [X0] :
( ~ member(y,X0)
| ~ subclass(X0,universal_class) )
| spl7_3 ),
inference(resolution,[],[f201,f1]) ).
fof(f911,plain,
( ! [X0] : ~ member(y,X0)
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f910,f4]) ).
fof(f912,plain,
( $false
| spl7_3
| ~ spl7_39 ),
inference(resolution,[],[f911,f559]) ).
fof(f921,plain,
( spl7_3
| ~ spl7_39 ),
inference(avatar_contradiction_clause,[],[f912]) ).
fof(f923,plain,
( member(y,sF0)
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f219,f200]) ).
fof(f1000,plain,
( $false
| spl7_1
| ~ spl7_44 ),
inference(forward_subsumption_resolution,[],[f599,f814]) ).
fof(f1001,plain,
( spl7_1
| ~ spl7_44 ),
inference(avatar_contradiction_clause,[],[f1000]) ).
fof(f1002,plain,
( ! [X0] :
( subclass(sF6,X0)
| ~ member(y,X0) )
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f870,f814]) ).
fof(f1003,plain,
( spl7_43
| spl7_1 ),
inference(avatar_split_clause,[],[f1002,f190,f594]) ).
fof(f1287,plain,
( spl7_15
| ~ spl7_3 ),
inference(avatar_split_clause,[],[f923,f199,f332]) ).
fof(f1294,definition,
( spl7_58
<=> subclass(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_58])],[avatar_definition]) ).
fof(f1295,plain,
( ~ subclass(sF0,sF6)
| spl7_58 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1296,plain,
( subclass(sF0,sF6)
| ~ spl7_58 ),
inference(avatar_component_clause,[],[f1294]) ).
fof(f1588,plain,
( subclass(sF6,sF0)
| ~ spl7_15
| ~ spl7_43 ),
inference(resolution,[],[f334,f595]) ).
fof(f1592,plain,
( ~ subclass(sF0,sF6)
| sF0 = sF6
| ~ spl7_15
| ~ spl7_43 ),
inference(resolution,[],[f1588,f7]) ).
fof(f1593,plain,
( ~ subclass(sF0,sF6)
| ~ spl7_15
| ~ spl7_43 ),
inference(forward_subsumption_resolution,[],[f1592,f170]) ).
fof(f1594,plain,
( ~ spl7_58
| ~ spl7_15
| ~ spl7_43 ),
inference(avatar_split_clause,[],[f1593,f594,f332,f1294]) ).
fof(f1625,plain,
( ! [X0] :
( ~ member(x,X0)
| ~ subclass(X0,universal_class) )
| spl7_1 ),
inference(resolution,[],[f192,f1]) ).
fof(f1626,plain,
( ! [X0] : ~ member(x,X0)
| spl7_1 ),
inference(forward_subsumption_resolution,[],[f1625,f4]) ).
fof(f1627,plain,
( $false
| spl7_1
| ~ spl7_5 ),
inference(resolution,[],[f1626,f210]) ).
fof(f1642,plain,
( spl7_1
| ~ spl7_5 ),
inference(avatar_contradiction_clause,[],[f1627]) ).
fof(f1646,plain,
( subclass(sF0,sF6)
| ~ spl7_16
| ~ spl7_39 ),
inference(resolution,[],[f350,f559]) ).
fof(f1667,plain,
( $false
| ~ spl7_16
| ~ spl7_39
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f1646,f1295]) ).
fof(f1668,plain,
( ~ spl7_16
| ~ spl7_39
| spl7_58 ),
inference(avatar_contradiction_clause,[],[f1667]) ).
fof(f1677,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,universal_class)
| member(X0,sF5) )
| ~ spl7_21 ),
inference(backward_demodulation,[],[f181,f401]) ).
fof(f1763,plain,
( ! [X0] :
( member(X0,sF5)
| ~ member(X0,universal_class) )
| ~ spl7_21 ),
inference(forward_subsumption_resolution,[],[f1677,f896]) ).
fof(f1782,plain,
( ! [X0] :
( ~ member(X0,sF3)
| ~ member(X0,universal_class) )
| ~ spl7_21 ),
inference(resolution,[],[f1763,f224]) ).
fof(f1833,plain,
( ! [X0] :
( member(x,sF0)
| subclass(sF0,X0)
| subclass(sF0,X0) )
| ~ spl7_13 ),
inference(superposition,[],[f2,f325]) ).
fof(f1836,plain,
( ! [X0] :
( member(x,sF0)
| subclass(sF0,X0) )
| ~ spl7_13 ),
inference(duplicate_literal_removal,[],[f1833]) ).
fof(f1838,plain,
( ! [X0] : subclass(sF0,X0)
| spl7_1
| ~ spl7_13 ),
inference(forward_subsumption_resolution,[],[f1836,f1626]) ).
fof(f1840,plain,
( null_class = sF0
| spl7_1
| ~ spl7_13 ),
inference(resolution,[],[f1838,f831]) ).
fof(f1841,plain,
( $false
| spl7_1
| ~ spl7_13
| spl7_35 ),
inference(forward_subsumption_resolution,[],[f1840,f463]) ).
fof(f1842,plain,
( spl7_1
| ~ spl7_13
| spl7_35 ),
inference(avatar_contradiction_clause,[],[f1841]) ).
fof(f1863,plain,
( ~ member(y,universal_class)
| ~ spl7_4
| ~ spl7_21 ),
inference(resolution,[],[f1782,f205]) ).
fof(f1865,plain,
( $false
| ~ spl7_3
| ~ spl7_4
| ~ spl7_21 ),
inference(forward_subsumption_resolution,[],[f1863,f200]) ).
fof(f1866,plain,
( ~ spl7_3
| ~ spl7_4
| ~ spl7_21 ),
inference(avatar_contradiction_clause,[],[f1865]) ).
fof(f1876,plain,
( ! [X0] :
( ~ member(y,X0)
| ~ subclass(X0,universal_class) )
| spl7_3 ),
inference(resolution,[],[f201,f1]) ).
fof(f1877,plain,
( ! [X0] : ~ member(y,X0)
| spl7_3 ),
inference(forward_subsumption_resolution,[],[f1876,f4]) ).
fof(f1878,plain,
( $false
| spl7_3
| ~ spl7_15 ),
inference(resolution,[],[f1877,f334]) ).
fof(f1895,plain,
( spl7_3
| ~ spl7_15 ),
inference(avatar_contradiction_clause,[],[f1878]) ).
fof(f2280,plain,
( ! [X0] :
( ~ member(x,X0)
| subclass(sF6,X0)
| subclass(sF6,X0) )
| ~ spl7_38 ),
inference(superposition,[],[f3,f554]) ).
fof(f2289,plain,
( ! [X0] :
( ~ member(x,X0)
| subclass(sF6,X0) )
| ~ spl7_38 ),
inference(duplicate_literal_removal,[],[f2280]) ).
fof(f2298,plain,
( subclass(sF6,sF0)
| ~ spl7_5
| ~ spl7_38 ),
inference(resolution,[],[f2289,f210]) ).
fof(f2317,plain,
( ~ subclass(sF0,sF6)
| sF0 = sF6
| ~ spl7_5
| ~ spl7_38 ),
inference(resolution,[],[f2298,f7]) ).
fof(f2420,plain,
( ~ member(x,sF1)
| subclass(sF0,sF6)
| ~ member(x,universal_class)
| subclass(sF0,sF6)
| ~ spl7_13 ),
inference(superposition,[],[f240,f325]) ).
fof(f2423,plain,
( ~ member(x,sF1)
| subclass(sF0,sF6)
| ~ member(x,universal_class)
| ~ spl7_13 ),
inference(duplicate_literal_removal,[],[f2420]) ).
fof(f2429,plain,
( subclass(sF0,sF6)
| ~ member(x,universal_class)
| ~ spl7_2
| ~ spl7_13 ),
inference(forward_subsumption_resolution,[],[f2423,f196]) ).
fof(f2432,plain,
( ~ member(x,universal_class)
| ~ spl7_2
| ~ spl7_13
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f2429,f1295]) ).
fof(f2435,plain,
( $false
| ~ spl7_1
| ~ spl7_2
| ~ spl7_13
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f2432,f191]) ).
fof(f2436,plain,
( ~ spl7_1
| ~ spl7_2
| ~ spl7_13
| spl7_58 ),
inference(avatar_contradiction_clause,[],[f2435]) ).
fof(f2437,plain,
( sF0 = sF6
| ~ spl7_5
| ~ spl7_38
| ~ spl7_58 ),
inference(forward_subsumption_resolution,[],[f2317,f1296]) ).
fof(f2438,plain,
( $false
| ~ spl7_5
| ~ spl7_38
| ~ spl7_58 ),
inference(forward_subsumption_resolution,[],[f2437,f170]) ).
fof(f2439,plain,
( ~ spl7_5
| ~ spl7_38
| ~ spl7_58 ),
inference(avatar_contradiction_clause,[],[f2438]) ).
fof(f2449,plain,
( ~ member(y,sF3)
| ~ member(y,universal_class)
| x = not_subclass_element(sF0,sF6)
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f320,f1295]) ).
fof(f2466,plain,
( ~ member(y,sF3)
| x = not_subclass_element(sF0,sF6)
| ~ spl7_3
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f2449,f200]) ).
fof(f2477,definition,
( spl7_87
<=> x = not_subclass_element(sF0,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_87])],[avatar_definition]) ).
fof(f2479,plain,
( x = not_subclass_element(sF0,sF6)
| ~ spl7_87 ),
inference(avatar_component_clause,[],[f2477]) ).
fof(f2495,plain,
( x = not_subclass_element(sF0,sF6)
| ~ spl7_3
| ~ spl7_4
| spl7_58 ),
inference(forward_subsumption_resolution,[],[f2466,f205]) ).
fof(f2496,plain,
( spl7_87
| ~ spl7_3
| ~ spl7_4
| spl7_58 ),
inference(avatar_split_clause,[],[f2495,f1294,f203,f199,f2477]) ).
fof(f2593,plain,
( ~ member(x,sF1)
| subclass(sF0,sF6)
| ~ member(x,universal_class)
| ~ spl7_87 ),
inference(superposition,[],[f240,f2479]) ).
fof(f2599,plain,
( subclass(sF0,sF6)
| ~ member(x,universal_class)
| ~ spl7_2
| ~ spl7_87 ),
inference(forward_subsumption_resolution,[],[f2593,f196]) ).
fof(f2603,plain,
( ~ member(x,universal_class)
| ~ spl7_2
| spl7_58
| ~ spl7_87 ),
inference(forward_subsumption_resolution,[],[f2599,f1295]) ).
fof(f2606,plain,
( $false
| ~ spl7_1
| ~ spl7_2
| spl7_58
| ~ spl7_87 ),
inference(forward_subsumption_resolution,[],[f2603,f191]) ).
fof(f2607,plain,
( ~ spl7_1
| ~ spl7_2
| spl7_58
| ~ spl7_87 ),
inference(avatar_contradiction_clause,[],[f2606]) ).
fof(f2638,plain,
( ~ subclass(sF6,sF0)
| sF0 = sF6
| ~ spl7_58 ),
inference(resolution,[],[f1296,f7]) ).
fof(f2639,plain,
( ~ subclass(sF6,sF0)
| ~ spl7_58 ),
inference(forward_subsumption_resolution,[],[f2638,f170]) ).
fof(f2677,plain,
( subclass(sF6,sF0)
| ~ member(x,sF0)
| ~ spl7_15 ),
inference(resolution,[],[f587,f334]) ).
fof(f2691,plain,
( ~ member(x,sF0)
| ~ spl7_15
| ~ spl7_58 ),
inference(forward_subsumption_resolution,[],[f2677,f2639]) ).
fof(f2692,plain,
( $false
| ~ spl7_5
| ~ spl7_15
| ~ spl7_58 ),
inference(forward_subsumption_resolution,[],[f2691,f210]) ).
fof(f2693,plain,
( ~ spl7_5
| ~ spl7_15
| ~ spl7_58 ),
inference(avatar_contradiction_clause,[],[f2692]) ).
cnf(s1,plain,
( ~ spl7_1
| spl7_2 ),
inference(sat_conversion,[],[f197]) ).
cnf(s2,plain,
( ~ spl7_3
| spl7_4 ),
inference(sat_conversion,[],[f206]) ).
cnf(s3,plain,
( ~ spl7_1
| spl7_5 ),
inference(sat_conversion,[],[f211]) ).
cnf(s8,plain,
( spl7_13
| spl7_15 ),
inference(sat_conversion,[],[f335]) ).
cnf(s9,plain,
( spl7_5
| spl7_16 ),
inference(sat_conversion,[],[f351]) ).
cnf(s24,plain,
( spl7_38
| spl7_39 ),
inference(sat_conversion,[],[f560]) ).
cnf(s41,plain,
( ~ spl7_21
| ~ spl7_35 ),
inference(sat_conversion,[],[f758]) ).
cnf(s43,plain,
( ~ spl7_38
| spl7_44
| spl7_51 ),
inference(sat_conversion,[],[f784]) ).
cnf(s44,plain,
( spl7_21
| ~ spl7_51 ),
inference(sat_conversion,[],[f833]) ).
cnf(s46,plain,
( spl7_3
| ~ spl7_39 ),
inference(sat_conversion,[],[f921]) ).
cnf(s48,plain,
( spl7_1
| ~ spl7_44 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s49,plain,
( spl7_1
| spl7_43 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s58,plain,
( ~ spl7_3
| spl7_15 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s73,plain,
( ~ spl7_15
| ~ spl7_43
| ~ spl7_58 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s75,plain,
( spl7_1
| ~ spl7_5 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s76,plain,
( ~ spl7_16
| ~ spl7_39
| spl7_58 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s80,plain,
( spl7_1
| ~ spl7_13
| spl7_35 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s81,plain,
( ~ spl7_3
| ~ spl7_4
| ~ spl7_21 ),
inference(sat_conversion,[],[f1866]) ).
cnf(s84,plain,
( spl7_3
| ~ spl7_15 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s102,plain,
( ~ spl7_1
| ~ spl7_2
| ~ spl7_13
| spl7_58 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s103,plain,
( ~ spl7_5
| ~ spl7_38
| ~ spl7_58 ),
inference(sat_conversion,[],[f2439]) ).
cnf(s114,plain,
( ~ spl7_3
| ~ spl7_4
| spl7_58
| spl7_87 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s118,plain,
( ~ spl7_1
| ~ spl7_2
| spl7_58
| ~ spl7_87 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s119,plain,
( ~ spl7_5
| ~ spl7_15
| ~ spl7_58 ),
inference(sat_conversion,[],[f2693]) ).
cnf(s120,plain,
( spl7_3
| spl7_1 ),
inference(rat,[],[s44,s41,s43,s80,s24,s8,s46,s84,s48]) ).
cnf(s121,plain,
spl7_1,
inference(rat,[],[s43,s24,s44,s76,s81,s73,s2,s58,s120,s9,s48,s49,s75]) ).
cnf(s123,plain,
spl7_5,
inference(rat,[],[s3,s121]) ).
cnf(s124,plain,
spl7_2,
inference(rat,[],[s1,s121]) ).
cnf(s128,plain,
spl7_3,
inference(rat,[],[s103,s102,s24,s8,s46,s84,s123,s121,s124]) ).
cnf(s130,plain,
spl7_15,
inference(rat,[],[s58,s128]) ).
cnf(s131,plain,
spl7_4,
inference(rat,[],[s2,s128]) ).
cnf(s133,plain,
~ spl7_58,
inference(rat,[],[s119,s123,s130]) ).
cnf(s136,plain,
~ spl7_87,
inference(rat,[],[s118,s124,s121,s133]) ).
cnf(s138,plain,
$false,
inference(rat,[],[s114,s131,s128,s136,s133]) ).
fof(f2694,plain,
$false,
inference(avatar_sat_refutation,[],[s138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET127-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.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 00:53:52 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 5.28/1.63 % (4058988)Input is clausal, will run a generic CNF schedule.
% 5.28/1.63 % (4058995)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3832320712:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.28/1.63 % (4058996)lrs+10_1_sil=8000:sp=occurrence:random_seed=1386864398:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.28/1.63 % (4058994)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2566649927:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.28/1.63 % (4058999)dis-21_1_sil=8000:lcm=predicate:random_seed=1011709430: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)
% 5.28/1.63 % (4058998)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2417735234:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.28/1.63 % (4058993)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=1753631434:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.28/1.63 % (4058997)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2213263196:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.28/1.63 % (4058996)Refutation not found, incomplete strategy
% 5.28/1.63 % (4058996)------------------------------
% 5.28/1.63 % (4058996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4058996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4058996)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4058996)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.63 % (4058996)Time elapsed: 0.003 s
% 5.28/1.63 % (4058996)Peak memory usage: 88 MB
% 5.28/1.63 % (4058996)Instructions burned: 3 (million)
% 5.28/1.63 % (4058999)Instruction limit reached!
% 5.28/1.63 % (4058999)------------------------------
% 5.28/1.63 % (4058999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4058999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4058999)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4058999)Termination reason: Instruction limit
% 5.28/1.63 % (4058999)Termination phase: Saturation
% 5.28/1.63 % (4058999)Time elapsed: 0.065 s
% 5.28/1.63 % (4058999)Peak memory usage: 88 MB
% 5.28/1.63 % (4058999)Instructions burned: 118 (million)
% 5.28/1.63 % (4058997)Instruction limit reached!
% 5.28/1.63 % (4058997)------------------------------
% 5.28/1.63 % (4058997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4058997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4058997)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4058997)Termination reason: Instruction limit
% 5.28/1.63 % (4058997)Termination phase: Saturation
% 5.28/1.63 % (4058997)Time elapsed: 0.067 s
% 5.28/1.63 % (4058997)Peak memory usage: 89 MB
% 5.28/1.63 % (4058997)Instructions burned: 114 (million)
% 5.28/1.63 % (4058998)Instruction limit reached!
% 5.28/1.63 % (4058998)------------------------------
% 5.28/1.63 % (4058998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4058998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4058998)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4058998)Termination reason: Instruction limit
% 5.28/1.63 % (4058998)Termination phase: Saturation
% 5.28/1.63 % (4058998)Time elapsed: 0.133 s
% 5.28/1.63 % (4058998)Peak memory usage: 90 MB
% 5.28/1.63 % (4058998)Instructions burned: 181 (million)
% 5.28/1.63 % (4059007)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=3760840096:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.28/1.63 % (4059008)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2722528809: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)
% 5.28/1.63 % (4059007)Refutation not found, incomplete strategy
% 5.28/1.63 % (4059007)------------------------------
% 5.28/1.63 % (4059007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4059007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4059007)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4059007)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.63 % (4059007)Time elapsed: 0.003 s
% 5.28/1.63 % (4059007)Peak memory usage: 88 MB
% 5.28/1.63 % (4059007)Instructions burned: 3 (million)
% 5.28/1.63 % (4058996)------------------------------
% 5.28/1.63 % (4058996)------------------------------
% 5.28/1.63 % (4059009)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2211046364:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 5.28/1.63 % (4059009)Refutation not found, incomplete strategy
% 5.28/1.63 % (4059009)------------------------------
% 5.28/1.63 % (4059009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4059009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4059009)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4059009)Termination reason: Refutation not found, incomplete strategy
% 5.28/1.63 % (4059009)Time elapsed: 0.003 s
% 5.28/1.63 % (4059009)Peak memory usage: 88 MB
% 5.28/1.63 % (4059009)Instructions burned: 3 (million)
% 5.28/1.63 % (4059008)Instruction limit reached!
% 5.28/1.63 % (4059008)------------------------------
% 5.28/1.63 % (4059008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4059008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4059008)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4059008)Termination reason: Instruction limit
% 5.28/1.63 % (4059008)Termination phase: Saturation
% 5.28/1.63 % (4059008)Time elapsed: 0.099 s
% 5.28/1.63 % (4059008)Peak memory usage: 90 MB
% 5.28/1.63 % (4059008)Instructions burned: 189 (million)
% 5.28/1.63 % (4059012)lrs+10_64_to=lpo:sil=8000:random_seed=205536581:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.28/1.63 % (4058995)First to succeed.
% 5.28/1.63 % (4058995)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4058988"
% 5.28/1.63 % (4059007)------------------------------
% 5.28/1.63 % (4059007)------------------------------
% 5.28/1.63 % (4059014)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2573626089:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 5.28/1.63 % (4059012)Instruction limit reached!
% 5.28/1.63 % (4059012)------------------------------
% 5.28/1.63 % (4059012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.28/1.63 % (4059012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.28/1.63 % (4059012)CaDiCaL version: 2.1.3
% 5.28/1.63 % (4059012)Termination reason: Instruction limit
% 5.28/1.63 % (4059012)Termination phase: Saturation
% 5.28/1.63 % (4059012)Time elapsed: 0.083 s
% 5.28/1.63 % (4059012)Peak memory usage: 89 MB
% 5.28/1.63 % (4059012)Instructions burned: 126 (million)
% 5.28/1.63 % (4059009)------------------------------
% 5.28/1.63 % (4059009)------------------------------
% 5.28/1.63 % (4058995)Refutation found. Thanks to Tanya!
% 5.28/1.63 % SZS status Unsatisfiable for theBenchmark
% 5.28/1.63 % SZS output start Proof for theBenchmark
% See solution above
% 6.01/1.81 % (4058995)------------------------------
% 6.01/1.81 % (4058995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.01/1.81 % (4058995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.01/1.81 % (4058995)CaDiCaL version: 2.1.3
% 6.01/1.81 % (4058995)Termination reason: Refutation
% 6.01/1.81 % (4058995)Time elapsed: 0.475 s
% 6.01/1.81 % (4058995)Peak memory usage: 132 MB
% 6.01/1.81 % (4058995)Instructions burned: 1244 (million)
% 6.01/1.81 % (4058995)------------------------------
% 6.01/1.81 % (4058995)------------------------------
% 6.01/1.81 % (4058988)Success in time 0.764 s
% 6.01/1.81 % Vampire exiting
%------------------------------------------------------------------------------