%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET263-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 : n011.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:38 PM UTC 2026
% Result : Unsatisfiable 16.86s 3.29s
% Output : Refutation 17.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 29
% Syntax : Number of formulae : 175 ( 44 unt; 11 def)
% Number of atoms : 435 ( 75 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 384 ( 124 ~; 260 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-3 aty)
% Number of variables : 229 ( 229 !; 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(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f122,negated_conjecture,
union(domain_of(x),domain_of(y)) != domain_of(union(x,y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_domain_preserves_union_1) ).
fof(f143,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f144,plain,
! [X0,X1] :
( null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f185,plain,
complement(intersection(complement(domain_of(x)),complement(domain_of(y)))) != domain_of(complement(intersection(complement(x),complement(y)))),
inference(definition_unfolding,[],[f122,f26,f26]) ).
fof(f190,definition,
sF0 = domain_of(x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
domain_of(x) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = complement(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
complement(sF0) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF2 = domain_of(y),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f195,plain,
domain_of(y) = sF2,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF3 = complement(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f197,plain,
complement(sF2) = sF3,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF4 = intersection(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f199,plain,
intersection(sF1,sF3) = sF4,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF5 = complement(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f201,plain,
complement(sF4) = sF5,
inference(reorient_equations,[],[f200]) ).
fof(f202,definition,
sF6 = complement(x),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f203,plain,
complement(x) = sF6,
inference(reorient_equations,[],[f202]) ).
fof(f204,definition,
sF7 = complement(y),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f205,plain,
complement(y) = sF7,
inference(reorient_equations,[],[f204]) ).
fof(f206,definition,
sF8 = intersection(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f207,plain,
intersection(sF6,sF7) = sF8,
inference(reorient_equations,[],[f206]) ).
fof(f208,definition,
sF9 = complement(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f209,plain,
complement(sF8) = sF9,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF10 = domain_of(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f211,plain,
domain_of(sF9) = sF10,
inference(reorient_equations,[],[f210]) ).
fof(f212,plain,
sF5 != sF10,
inference(definition_folding,[],[f185,f211,f209,f207,f205,f203,f201,f199,f197,f195,f193,f191]) ).
fof(f213,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,x) ),
inference(superposition,[],[f24,f203]) ).
fof(f215,plain,
! [X0] :
( ~ member(X0,sF1)
| ~ member(X0,sF0) ),
inference(superposition,[],[f24,f193]) ).
fof(f216,plain,
! [X0,X1] :
( ~ member(not_subclass_element(complement(X0),X1),X0)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f2,f24]) ).
fof(f217,plain,
! [X0] :
( ~ member(X0,sF3)
| ~ member(X0,sF2) ),
inference(superposition,[],[f24,f197]) ).
fof(f222,plain,
! [X0] :
( ~ member(X0,sF5)
| ~ member(X0,sF4) ),
inference(superposition,[],[f24,f201]) ).
fof(f223,plain,
! [X2,X3,X0,X1] :
( ~ subclass(intersection(X2,X1),X3)
| ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,X3) ),
inference(resolution,[],[f23,f1]) ).
fof(f225,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,sF4)
| ~ member(X0,sF1) ),
inference(superposition,[],[f23,f199]) ).
fof(f226,plain,
! [X0] :
( ~ member(X0,sF7)
| member(X0,sF8)
| ~ member(X0,sF6) ),
inference(superposition,[],[f23,f207]) ).
fof(f229,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(X1)),universal_class)
| member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(resolution,[],[f25,f3]) ).
fof(f230,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF6)
| member(X0,x) ),
inference(superposition,[],[f25,f203]) ).
fof(f231,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF7)
| member(X0,y) ),
inference(superposition,[],[f25,f205]) ).
fof(f232,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF1)
| member(X0,sF0) ),
inference(superposition,[],[f25,f193]) ).
fof(f233,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF3)
| member(X0,sF2) ),
inference(superposition,[],[f25,f197]) ).
fof(f234,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF5)
| member(X0,sF4) ),
inference(superposition,[],[f25,f201]) ).
fof(f235,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF9)
| member(X0,sF8) ),
inference(superposition,[],[f25,f209]) ).
fof(f237,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f21,f2]) ).
fof(f239,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF1) ),
inference(superposition,[],[f21,f199]) ).
fof(f240,plain,
! [X0] :
( ~ member(X0,sF8)
| member(X0,sF6) ),
inference(superposition,[],[f21,f207]) ).
fof(f243,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f22,f2]) ).
fof(f245,plain,
! [X0] :
( ~ member(X0,sF4)
| member(X0,sF3) ),
inference(superposition,[],[f22,f199]) ).
fof(f246,plain,
! [X0] :
( ~ member(X0,sF8)
| member(X0,sF7) ),
inference(superposition,[],[f22,f207]) ).
fof(f252,plain,
! [X0] :
( ~ member(not_subclass_element(sF5,X0),sF4)
| subclass(sF5,X0) ),
inference(resolution,[],[f222,f2]) ).
fof(f261,plain,
! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,X2)
| member(X0,universal_class) ),
inference(resolution,[],[f223,f4]) ).
fof(f264,plain,
! [X2,X0] :
( ~ member(X0,X2)
| member(X0,universal_class) ),
inference(condensation,[],[f261]) ).
fof(f267,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(resolution,[],[f264,f2]) ).
fof(f272,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF7)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),y) ),
inference(resolution,[],[f267,f231]) ).
fof(f273,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF6)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),x) ),
inference(resolution,[],[f267,f230]) ).
fof(f274,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF3)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2) ),
inference(resolution,[],[f267,f233]) ).
fof(f275,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF9)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF8) ),
inference(resolution,[],[f267,f235]) ).
fof(f276,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF1)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0) ),
inference(resolution,[],[f267,f232]) ).
fof(f277,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF5)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF4) ),
inference(resolution,[],[f267,f234]) ).
fof(f281,plain,
! [X0] :
( subclass(X0,sF5)
| member(not_subclass_element(X0,sF5),sF4)
| subclass(X0,sF5) ),
inference(resolution,[],[f277,f3]) ).
fof(f285,plain,
! [X0] :
( member(not_subclass_element(X0,sF5),sF4)
| subclass(X0,sF5) ),
inference(duplicate_literal_removal,[],[f281]) ).
fof(f287,plain,
! [X0] :
( member(not_subclass_element(X0,sF5),sF3)
| subclass(X0,sF5) ),
inference(resolution,[],[f285,f245]) ).
fof(f288,plain,
! [X0] :
( member(not_subclass_element(X0,sF5),sF1)
| subclass(X0,sF5) ),
inference(resolution,[],[f285,f239]) ).
fof(f297,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF5),sF0)
| subclass(X0,sF5) ),
inference(resolution,[],[f288,f215]) ).
fof(f307,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF1)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF4)
| subclass(X0,X1) ),
inference(resolution,[],[f274,f225]) ).
fof(f313,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF5),sF2)
| subclass(X0,sF5) ),
inference(resolution,[],[f287,f217]) ).
fof(f317,plain,
! [X0] :
( subclass(X0,sF9)
| member(not_subclass_element(X0,sF9),sF8)
| subclass(X0,sF9) ),
inference(resolution,[],[f275,f3]) ).
fof(f321,plain,
! [X0] :
( member(not_subclass_element(X0,sF9),sF8)
| subclass(X0,sF9) ),
inference(duplicate_literal_removal,[],[f317]) ).
fof(f324,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),sF6)
| member(not_subclass_element(X0,X1),y)
| member(not_subclass_element(X0,X1),sF8)
| subclass(X0,X1) ),
inference(resolution,[],[f272,f226]) ).
fof(f330,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF4)
| subclass(X0,X1)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0) ),
inference(resolution,[],[f307,f276]) ).
fof(f335,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF4)
| member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0) ),
inference(duplicate_literal_removal,[],[f330]) ).
fof(f336,plain,
! [X0] :
( member(not_subclass_element(sF5,X0),sF2)
| subclass(sF5,X0)
| member(not_subclass_element(sF5,X0),sF0)
| subclass(sF5,X0) ),
inference(resolution,[],[f335,f252]) ).
fof(f343,plain,
! [X0] :
( member(not_subclass_element(sF5,X0),sF2)
| subclass(sF5,X0)
| member(not_subclass_element(sF5,X0),sF0) ),
inference(duplicate_literal_removal,[],[f336]) ).
fof(f350,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),y)
| member(not_subclass_element(X0,X1),sF8)
| subclass(X0,X1)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),x) ),
inference(resolution,[],[f324,f273]) ).
fof(f353,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF8)
| member(not_subclass_element(X0,X1),y)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),x) ),
inference(duplicate_literal_removal,[],[f350]) ).
fof(f364,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(unordered_pair(X2,X2),universal_class))
| member(X0,null_class)
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1)) ),
inference(superposition,[],[f23,f144]) ).
fof(f369,plain,
! [X0] :
( member(not_subclass_element(X0,sF9),sF7)
| subclass(X0,sF9) ),
inference(resolution,[],[f321,f246]) ).
fof(f370,plain,
! [X0] :
( member(not_subclass_element(X0,sF9),sF6)
| subclass(X0,sF9) ),
inference(resolution,[],[f321,f240]) ).
fof(f383,plain,
! [X0] :
( member(regular(X0),universal_class)
| null_class = X0 ),
inference(resolution,[],[f68,f264]) ).
fof(f384,plain,
! [X0,X1] :
( member(regular(X0),X1)
| ~ subclass(X0,X1)
| null_class = X0 ),
inference(resolution,[],[f68,f1]) ).
fof(f391,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f393,plain,
! [X0] :
( ~ member(regular(complement(X0)),X0)
| complement(X0) = null_class ),
inference(resolution,[],[f68,f24]) ).
fof(f421,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1))
| subclass(X0,complement(X1)) ),
inference(resolution,[],[f229,f267]) ).
fof(f430,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(duplicate_literal_removal,[],[f421]) ).
fof(f463,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(complement(X1))),X1)
| subclass(X0,complement(complement(X1))) ),
inference(resolution,[],[f430,f24]) ).
fof(f560,plain,
! [X0] :
( subclass(X0,complement(complement(X0)))
| subclass(X0,complement(complement(X0))) ),
inference(resolution,[],[f463,f2]) ).
fof(f591,plain,
! [X0] : subclass(X0,complement(complement(X0))),
inference(duplicate_literal_removal,[],[f560]) ).
fof(f794,plain,
! [X2,X0,X1] :
( ~ subclass(X0,unordered_pair(X1,X2))
| null_class = X0
| regular(X0) = X1
| regular(X0) = X2 ),
inference(resolution,[],[f384,f8]) ).
fof(f1085,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF9),x)
| subclass(X0,sF9) ),
inference(resolution,[],[f370,f213]) ).
fof(f1136,plain,
( null_class = complement(universal_class)
| null_class = complement(universal_class) ),
inference(resolution,[],[f383,f393]) ).
fof(f1147,plain,
null_class = complement(universal_class),
inference(duplicate_literal_removal,[],[f1136]) ).
fof(f1148,plain,
! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f24,f1147]) ).
fof(f1158,plain,
! [X0] : ~ member(X0,null_class),
inference(forward_subsumption_resolution,[],[f1148,f264]) ).
fof(f1313,plain,
! [X0] :
( subclass(intersection(x,X0),sF9)
| subclass(intersection(x,X0),sF9) ),
inference(resolution,[],[f237,f1085]) ).
fof(f1336,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(intersection(complement(X0),X1),X2),X0)
| subclass(intersection(complement(X0),X1),X2) ),
inference(resolution,[],[f237,f24]) ).
fof(f1366,plain,
! [X0] : subclass(intersection(x,X0),sF9),
inference(duplicate_literal_removal,[],[f1313]) ).
fof(f1387,plain,
! [X0,X1] :
( subclass(intersection(complement(sF8),X0),X1)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),y)
| subclass(intersection(complement(sF8),X0),X1)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),x) ),
inference(resolution,[],[f1336,f353]) ).
fof(f1429,plain,
! [X0,X1] :
( subclass(intersection(complement(sF8),X0),X1)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),y)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),x) ),
inference(duplicate_literal_removal,[],[f1387]) ).
fof(f1455,plain,
! [X0,X1] :
( subclass(intersection(sF9,X0),X1)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),y)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),x) ),
inference(forward_demodulation,[],[f1429,f209]) ).
fof(f1461,plain,
! [X0,X1] :
( member(not_subclass_element(intersection(sF9,X0),X1),y)
| subclass(intersection(sF9,X0),X1)
| member(not_subclass_element(intersection(complement(sF8),X0),X1),x) ),
inference(forward_demodulation,[],[f1455,f209]) ).
fof(f1465,plain,
! [X0,X1] :
( member(not_subclass_element(intersection(sF9,X0),X1),y)
| member(not_subclass_element(intersection(sF9,X0),X1),x)
| subclass(intersection(sF9,X0),X1) ),
inference(forward_demodulation,[],[f1461,f209]) ).
fof(f1686,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,[],[f216,f25]) ).
fof(f1726,plain,
! [X0,X1] :
( member(not_subclass_element(complement(complement(X0)),X1),X0)
| subclass(complement(complement(X0)),X1) ),
inference(forward_subsumption_resolution,[],[f1686,f267]) ).
fof(f1744,plain,
! [X0] :
( subclass(complement(complement(X0)),X0)
| subclass(complement(complement(X0)),X0) ),
inference(resolution,[],[f1726,f3]) ).
fof(f1812,plain,
! [X0] : subclass(complement(complement(X0)),X0),
inference(duplicate_literal_removal,[],[f1744]) ).
fof(f1838,plain,
! [X0] :
( ~ subclass(X0,complement(complement(X0)))
| complement(complement(X0)) = X0 ),
inference(resolution,[],[f1812,f7]) ).
fof(f1847,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f1838,f591]) ).
fof(f1850,plain,
y = complement(sF7),
inference(superposition,[],[f1847,f205]) ).
fof(f2419,plain,
! [X0] :
( subclass(intersection(complement(sF7),X0),sF9)
| subclass(intersection(complement(sF7),X0),sF9) ),
inference(resolution,[],[f369,f1336]) ).
fof(f2428,plain,
! [X0] : subclass(intersection(complement(sF7),X0),sF9),
inference(duplicate_literal_removal,[],[f2419]) ).
fof(f2431,plain,
! [X0] : subclass(intersection(y,X0),sF9),
inference(forward_demodulation,[],[f2428,f1850]) ).
fof(f2535,plain,
! [X2,X3,X0,X1] :
( subclass(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2)
| member(not_subclass_element(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2),null_class)
| ~ member(not_subclass_element(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2),X3)
| ~ member(X1,universal_class)
| member(X1,domain_of(X3)) ),
inference(resolution,[],[f243,f364]) ).
fof(f2587,plain,
! [X2,X3,X0,X1] :
( ~ member(not_subclass_element(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2),X3)
| subclass(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X3)) ),
inference(forward_subsumption_resolution,[],[f2535,f1158]) ).
fof(f2623,plain,
! [X0,X1] :
( subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,domain_of(y))
| member(not_subclass_element(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1),x)
| subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1) ),
inference(resolution,[],[f2587,f1465]) ).
fof(f2703,plain,
! [X0,X1] :
( subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,domain_of(y))
| member(not_subclass_element(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1),x) ),
inference(duplicate_literal_removal,[],[f2623]) ).
fof(f2717,plain,
! [X0,X1] :
( member(not_subclass_element(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1),x)
| subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,sF2) ),
inference(forward_demodulation,[],[f2703,f195]) ).
fof(f2749,plain,
! [X0,X1] :
( subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,sF2)
| subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,domain_of(x)) ),
inference(resolution,[],[f2717,f2587]) ).
fof(f2755,plain,
! [X0,X1] :
( subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| ~ member(X0,universal_class)
| member(X0,sF2)
| member(X0,domain_of(x)) ),
inference(duplicate_literal_removal,[],[f2749]) ).
fof(f2761,plain,
! [X0,X1] :
( subclass(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class)),X1)
| member(X0,sF0)
| ~ member(X0,universal_class)
| member(X0,sF2) ),
inference(forward_demodulation,[],[f2755,f191]) ).
fof(f2766,plain,
! [X2,X0,X1] :
( member(X0,sF0)
| ~ member(X0,universal_class)
| member(X0,sF2)
| null_class = intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))
| regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = X1
| regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = X2 ),
inference(resolution,[],[f2761,f794]) ).
fof(f2769,plain,
! [X2,X0] :
( regular(intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))) = X2
| ~ member(X0,universal_class)
| member(X0,sF2)
| null_class = intersection(sF9,cross_product(unordered_pair(X0,X0),universal_class))
| member(X0,sF0) ),
inference(condensation,[],[f2766]) ).
fof(f2820,plain,
! [X2,X0,X1] :
( X0 = X2
| ~ member(X1,universal_class)
| member(X1,sF2)
| null_class = intersection(sF9,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,sF0)
| ~ member(X1,universal_class)
| member(X1,sF2)
| null_class = intersection(sF9,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,sF0) ),
inference(superposition,[],[f2769,f2769]) ).
fof(f3124,plain,
! [X2,X0,X1] :
( X0 = X2
| ~ member(X1,universal_class)
| member(X1,sF2)
| null_class = intersection(sF9,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,sF0) ),
inference(duplicate_literal_removal,[],[f2820]) ).
fof(f3125,plain,
! [X1] :
( null_class = intersection(sF9,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,sF2)
| ~ member(X1,universal_class)
| member(X1,sF0) ),
inference(condensation,[],[f3124]) ).
fof(f3171,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(sF9))
| member(X0,sF2)
| ~ member(X0,universal_class)
| member(X0,sF0) ),
inference(superposition,[],[f143,f3125]) ).
fof(f3194,plain,
! [X0] :
( ~ member(X0,domain_of(sF9))
| member(X0,sF2)
| ~ member(X0,universal_class)
| member(X0,sF0) ),
inference(trivial_inequality_removal,[],[f3171]) ).
fof(f3202,plain,
! [X0] :
( ~ member(X0,domain_of(sF9))
| member(X0,sF2)
| member(X0,sF0) ),
inference(forward_subsumption_resolution,[],[f3194,f264]) ).
fof(f3203,plain,
! [X0] :
( ~ member(X0,sF10)
| member(X0,sF2)
| member(X0,sF0) ),
inference(forward_demodulation,[],[f3202,f211]) ).
fof(f3204,plain,
! [X0] :
( member(not_subclass_element(sF10,X0),sF2)
| member(not_subclass_element(sF10,X0),sF0)
| subclass(sF10,X0) ),
inference(resolution,[],[f3203,f2]) ).
fof(f3226,plain,
( member(not_subclass_element(sF10,sF5),sF0)
| subclass(sF10,sF5)
| subclass(sF10,sF5) ),
inference(resolution,[],[f3204,f313]) ).
fof(f3239,plain,
( member(not_subclass_element(sF10,sF5),sF0)
| subclass(sF10,sF5) ),
inference(duplicate_literal_removal,[],[f3226]) ).
fof(f3242,plain,
subclass(sF10,sF5),
inference(forward_subsumption_resolution,[],[f3239,f297]) ).
fof(f3258,plain,
( ~ subclass(sF5,sF10)
| sF5 = sF10 ),
inference(resolution,[],[f3242,f7]) ).
fof(f3259,plain,
~ subclass(sF5,sF10),
inference(forward_subsumption_resolution,[],[f3258,f212]) ).
fof(f4197,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),null_class)
| ~ member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2)) ),
inference(resolution,[],[f391,f364]) ).
fof(f4241,plain,
! [X2,X0,X1] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X2)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class)
| member(X1,domain_of(X2)) ),
inference(forward_subsumption_resolution,[],[f4197,f1158]) ).
fof(f4245,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| ~ subclass(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)) ),
inference(resolution,[],[f4241,f384]) ).
fof(f4273,plain,
! [X2,X0,X1] :
( ~ subclass(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)) ),
inference(duplicate_literal_removal,[],[f4245]) ).
fof(f4341,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,domain_of(sF9))
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class)) ),
inference(resolution,[],[f4273,f1366]) ).
fof(f4342,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,domain_of(sF9))
| null_class = intersection(y,cross_product(unordered_pair(X0,X0),universal_class)) ),
inference(resolution,[],[f4273,f2431]) ).
fof(f4370,plain,
! [X0] :
( null_class = intersection(y,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(forward_demodulation,[],[f4342,f211]) ).
fof(f4371,plain,
! [X0] :
( null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(forward_demodulation,[],[f4341,f211]) ).
fof(f4379,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(y))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(superposition,[],[f143,f4370]) ).
fof(f4413,plain,
! [X0] :
( ~ member(X0,domain_of(y))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(trivial_inequality_removal,[],[f4379]) ).
fof(f4417,plain,
! [X0] :
( ~ member(X0,domain_of(y))
| member(X0,sF10) ),
inference(forward_subsumption_resolution,[],[f4413,f264]) ).
fof(f4418,plain,
! [X0] :
( ~ member(X0,sF2)
| member(X0,sF10) ),
inference(forward_demodulation,[],[f4417,f195]) ).
fof(f4436,plain,
! [X0] :
( member(not_subclass_element(sF5,X0),sF10)
| subclass(sF5,X0)
| member(not_subclass_element(sF5,X0),sF0) ),
inference(resolution,[],[f4418,f343]) ).
fof(f4454,plain,
( subclass(sF5,sF10)
| member(not_subclass_element(sF5,sF10),sF0)
| subclass(sF5,sF10) ),
inference(resolution,[],[f4436,f3]) ).
fof(f4469,plain,
( subclass(sF5,sF10)
| member(not_subclass_element(sF5,sF10),sF0) ),
inference(duplicate_literal_removal,[],[f4454]) ).
fof(f4471,plain,
member(not_subclass_element(sF5,sF10),sF0),
inference(forward_subsumption_resolution,[],[f4469,f3259]) ).
fof(f4812,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(x))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(superposition,[],[f143,f4371]) ).
fof(f4846,plain,
! [X0] :
( ~ member(X0,domain_of(x))
| ~ member(X0,universal_class)
| member(X0,sF10) ),
inference(trivial_inequality_removal,[],[f4812]) ).
fof(f4850,plain,
! [X0] :
( ~ member(X0,domain_of(x))
| member(X0,sF10) ),
inference(forward_subsumption_resolution,[],[f4846,f264]) ).
fof(f4851,plain,
! [X0] :
( ~ member(X0,sF0)
| member(X0,sF10) ),
inference(forward_demodulation,[],[f4850,f191]) ).
fof(f4870,plain,
member(not_subclass_element(sF5,sF10),sF10),
inference(resolution,[],[f4851,f4471]) ).
fof(f4893,plain,
subclass(sF5,sF10),
inference(resolution,[],[f4870,f3]) ).
fof(f4900,plain,
$false,
inference(forward_subsumption_resolution,[],[f4893,f3259]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET263-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n011.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 28 01:14:46 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.43 Running first-order theorem proving
% 0.11/0.43 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
% 11.62/2.53 % (2930460)Input is clausal, will run a generic CNF schedule.
% 11.62/2.53 % (2930466)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2831813048:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.62/2.53 % (2930467)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=288076128:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.62/2.53 % (2930470)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1000850780:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.62/2.53 % (2930465)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=1802667942:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.62/2.53 % (2930469)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2703868137:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.62/2.53 % (2930468)lrs+10_1_sil=8000:sp=occurrence:random_seed=2945266701:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.62/2.53 % (2930468)Refutation not found, incomplete strategy
% 11.62/2.53 % (2930468)------------------------------
% 11.62/2.53 % (2930468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.62/2.53 % (2930468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.53 % (2930468)CaDiCaL version: 2.1.3
% 11.62/2.53 % (2930468)Termination reason: Refutation not found, incomplete strategy
% 11.62/2.53 % (2930468)Time elapsed: 0.004 s
% 11.62/2.53 % (2930468)Peak memory usage: 88 MB
% 11.62/2.53 % (2930468)Instructions burned: 4 (million)
% 11.62/2.53 % (2930471)dis-21_1_sil=8000:lcm=predicate:random_seed=3527800814: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)
% 11.62/2.53 % (2930469)Instruction limit reached!
% 11.62/2.53 % (2930469)------------------------------
% 11.62/2.53 % (2930469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.62/2.53 % (2930469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.53 % (2930469)CaDiCaL version: 2.1.3
% 11.62/2.53 % (2930469)Termination reason: Instruction limit
% 11.62/2.53 % (2930469)Termination phase: Saturation
% 11.62/2.53 % (2930469)Time elapsed: 0.068 s
% 11.62/2.53 % (2930469)Peak memory usage: 89 MB
% 11.62/2.53 % (2930469)Instructions burned: 114 (million)
% 11.62/2.53 % (2930471)Instruction limit reached!
% 11.62/2.53 % (2930471)------------------------------
% 11.62/2.53 % (2930471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.62/2.53 % (2930471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.53 % (2930471)CaDiCaL version: 2.1.3
% 11.62/2.53 % (2930471)Termination reason: Instruction limit
% 11.62/2.53 % (2930471)Termination phase: Saturation
% 11.62/2.53 % (2930471)Time elapsed: 0.074 s
% 11.62/2.53 % (2930471)Peak memory usage: 89 MB
% 11.62/2.53 % (2930471)Instructions burned: 118 (million)
% 11.62/2.53 % (2930470)Instruction limit reached!
% 11.62/2.53 % (2930470)------------------------------
% 11.62/2.53 % (2930470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.62/2.53 % (2930470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.53 % (2930470)CaDiCaL version: 2.1.3
% 11.62/2.53 % (2930470)Termination reason: Instruction limit
% 11.62/2.53 % (2930470)Termination phase: Saturation
% 11.62/2.53 % (2930470)Time elapsed: 0.134 s
% 11.62/2.53 % (2930470)Peak memory usage: 91 MB
% 11.62/2.53 % (2930470)Instructions burned: 182 (million)
% 11.62/2.53 % (2930479)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=637037918:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.62/2.53 % (2930479)Refutation not found, incomplete strategy
% 11.62/2.53 % (2930479)------------------------------
% 11.62/2.53 % (2930479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.62/2.53 % (2930479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.62/2.53 % (2930479)CaDiCaL version: 2.1.3
% 11.62/2.53 % (2930479)Termination reason: Refutation not found, incomplete strategy
% 11.62/2.53 % (2930479)Time elapsed: 0.002 s
% 11.62/2.53 % (2930479)Peak memory usage: 88 MB
% 11.62/2.53 % (2930479)Instructions burned: 2 (million)
% 11.62/2.53 % (2930480)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=17035113:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 16.86/3.29 % (2930468)------------------------------
% 16.86/3.29 % (2930468)------------------------------
% 16.86/3.29 % (2930481)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=773197909:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.86/3.29 % (2930480)Instruction limit reached!
% 16.86/3.29 % (2930480)------------------------------
% 16.86/3.29 % (2930480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930480)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930480)Termination reason: Instruction limit
% 16.86/3.29 % (2930480)Termination phase: Saturation
% 16.86/3.29 % (2930480)Time elapsed: 0.102 s
% 16.86/3.29 % (2930480)Peak memory usage: 91 MB
% 16.86/3.29 % (2930480)Instructions burned: 189 (million)
% 16.86/3.29 % (2930481)Instruction limit reached!
% 16.86/3.29 % (2930481)------------------------------
% 16.86/3.29 % (2930481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930481)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930481)Termination reason: Instruction limit
% 16.86/3.29 % (2930481)Termination phase: Saturation
% 16.86/3.29 % (2930481)Time elapsed: 0.118 s
% 16.86/3.29 % (2930481)Peak memory usage: 88 MB
% 16.86/3.29 % (2930481)Instructions burned: 220 (million)
% 16.86/3.29 % (2930485)lrs+10_64_to=lpo:sil=8000:random_seed=3687745405:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 16.86/3.29 % (2930479)------------------------------
% 16.86/3.29 % (2930479)------------------------------
% 16.86/3.29 % (2930486)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1239705850:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.86/3.29 % (2930485)Instruction limit reached!
% 16.86/3.29 % (2930485)------------------------------
% 16.86/3.29 % (2930485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930485)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930485)Termination reason: Instruction limit
% 16.86/3.29 % (2930485)Termination phase: Saturation
% 16.86/3.29 % (2930485)Time elapsed: 0.080 s
% 16.86/3.29 % (2930485)Peak memory usage: 89 MB
% 16.86/3.29 % (2930485)Instructions burned: 126 (million)
% 16.86/3.29 % (2930487)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=538023276:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 16.86/3.29 % (2930489)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4257309742:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 16.86/3.29 % (2930486)Instruction limit reached!
% 16.86/3.29 % (2930486)------------------------------
% 16.86/3.29 % (2930486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930486)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930486)Termination reason: Instruction limit
% 16.86/3.29 % (2930486)Termination phase: Saturation
% 16.86/3.29 % (2930486)Time elapsed: 0.121 s
% 16.86/3.29 % (2930486)Peak memory usage: 89 MB
% 16.86/3.29 % (2930486)Instructions burned: 196 (million)
% 16.86/3.29 % (2930491)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=2883826643:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 16.86/3.29 % (2930487)Instruction limit reached!
% 16.86/3.29 % (2930487)------------------------------
% 16.86/3.29 % (2930487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930487)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930487)Termination reason: Instruction limit
% 16.86/3.29 % (2930487)Termination phase: Saturation
% 16.86/3.29 % (2930487)Time elapsed: 0.104 s
% 16.86/3.29 % (2930487)Peak memory usage: 91 MB
% 16.86/3.29 % (2930487)Instructions burned: 158 (million)
% 16.86/3.29 % (2930491)Instruction limit reached!
% 16.86/3.29 % (2930491)------------------------------
% 16.86/3.29 % (2930491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930491)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930491)Termination reason: Instruction limit
% 16.86/3.29 % (2930491)Termination phase: Saturation
% 16.86/3.29 % (2930491)Time elapsed: 0.063 s
% 16.86/3.29 % (2930491)Peak memory usage: 90 MB
% 16.86/3.29 % (2930491)Instructions burned: 107 (million)
% 16.86/3.29 % (2930494)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2872328453:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 16.86/3.29 % (2930494)Refutation not found, incomplete strategy
% 16.86/3.29 % (2930494)------------------------------
% 16.86/3.29 % (2930494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930494)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930494)Termination reason: Refutation not found, incomplete strategy
% 16.86/3.29 % (2930494)Time elapsed: 0.005 s
% 16.86/3.29 % (2930494)Peak memory usage: 88 MB
% 16.86/3.29 % (2930494)Instructions burned: 8 (million)
% 16.86/3.29 % (2930496)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2064499658:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 16.86/3.29 % (2930497)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1866007395:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 16.86/3.29 % (2930496)Instruction limit reached!
% 16.86/3.29 % (2930496)------------------------------
% 16.86/3.29 % (2930496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930496)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930496)Termination reason: Instruction limit
% 16.86/3.29 % (2930496)Termination phase: Saturation
% 16.86/3.29 % (2930496)Time elapsed: 0.159 s
% 16.86/3.29 % (2930496)Peak memory usage: 91 MB
% 16.86/3.29 % (2930496)Instructions burned: 244 (million)
% 16.86/3.29 % (2930494)------------------------------
% 16.86/3.29 % (2930494)------------------------------
% 16.86/3.29 % (2930501)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1364122496:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 16.86/3.29 % (2930501)Refutation not found, incomplete strategy
% 16.86/3.29 % (2930501)------------------------------
% 16.86/3.29 % (2930501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930501)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930501)Termination reason: Refutation not found, incomplete strategy
% 16.86/3.29 % (2930501)Time elapsed: 0.004 s
% 16.86/3.29 % (2930501)Peak memory usage: 88 MB
% 16.86/3.29 % (2930501)Instructions burned: 4 (million)
% 16.86/3.29 % (2930502)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4088431248:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 16.86/3.29 % (2930501)------------------------------
% 16.86/3.29 % (2930501)------------------------------
% 16.86/3.29 % (2930502)Instruction limit reached!
% 16.86/3.29 % (2930502)------------------------------
% 16.86/3.29 % (2930502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930502)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930502)Termination reason: Instruction limit
% 16.86/3.29 % (2930502)Termination phase: Saturation
% 16.86/3.29 % (2930502)Time elapsed: 0.284 s
% 16.86/3.29 % (2930502)Peak memory usage: 93 MB
% 16.86/3.29 % (2930502)Instructions burned: 500 (million)
% 16.86/3.29 % (2930505)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4134288892:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 16.86/3.29 % (2930505)Instruction limit reached!
% 16.86/3.29 % (2930505)------------------------------
% 16.86/3.29 % (2930505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930505)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930505)Termination reason: Instruction limit
% 16.86/3.29 % (2930505)Termination phase: Saturation
% 16.86/3.29 % (2930505)Time elapsed: 0.115 s
% 16.86/3.29 % (2930505)Peak memory usage: 89 MB
% 16.86/3.29 % (2930505)Instructions burned: 192 (million)
% 16.86/3.29 % (2930507)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=93555742:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 16.86/3.29 % (2930508)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1915558863:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 16.86/3.29 % (2930507)Instruction limit reached!
% 16.86/3.29 % (2930507)------------------------------
% 16.86/3.29 % (2930507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930507)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930507)Termination reason: Instruction limit
% 16.86/3.29 % (2930507)Termination phase: Saturation
% 16.86/3.29 % (2930507)Time elapsed: 0.170 s
% 16.86/3.29 % (2930507)Peak memory usage: 91 MB
% 16.86/3.29 % (2930507)Instructions burned: 264 (million)
% 16.86/3.29 % (2930508)Instruction limit reached!
% 16.86/3.29 % (2930508)------------------------------
% 16.86/3.29 % (2930508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930508)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930508)Termination reason: Instruction limit
% 16.86/3.29 % (2930508)Termination phase: Saturation
% 16.86/3.29 % (2930508)Time elapsed: 0.104 s
% 16.86/3.29 % (2930508)Peak memory usage: 89 MB
% 16.86/3.29 % (2930508)Instructions burned: 157 (million)
% 16.86/3.29 % (2930511)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=204765364:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 16.86/3.29 % (2930512)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1617175268:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 16.86/3.29 % (2930497)First to succeed.
% 16.86/3.29 % (2930497)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2930460"
% 16.86/3.29 % (2930512)Instruction limit reached!
% 16.86/3.29 % (2930512)------------------------------
% 16.86/3.29 % (2930512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.86/3.29 % (2930512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.86/3.29 % (2930512)CaDiCaL version: 2.1.3
% 16.86/3.29 % (2930512)Termination reason: Instruction limit
% 16.86/3.29 % (2930512)Termination phase: Saturation
% 16.86/3.29 % (2930512)Time elapsed: 0.267 s
% 16.86/3.29 % (2930512)Peak memory usage: 89 MB
% 16.86/3.29 % (2930512)Instructions burned: 539 (million)
% 16.86/3.29 % (2930497)Refutation found. Thanks to Tanya!
% 16.86/3.29 % SZS status Unsatisfiable for theBenchmark
% 16.86/3.29 % SZS output start Proof for theBenchmark
% See solution above
% 17.57/3.38 % (2930497)------------------------------
% 17.57/3.38 % (2930497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.57/3.38 % (2930497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.57/3.38 % (2930497)CaDiCaL version: 2.1.3
% 17.57/3.38 % (2930497)Termination reason: Refutation
% 17.57/3.38 % (2930497)Time elapsed: 1.225 s
% 17.57/3.38 % (2930497)Peak memory usage: 137 MB
% 17.57/3.38 % (2930497)Instructions burned: 1911 (million)
% 17.57/3.38 % (2930497)------------------------------
% 17.57/3.38 % (2930497)------------------------------
% 17.57/3.38 % (2930460)Success in time 2.427 s
% 17.57/3.38 % Vampire exiting
%------------------------------------------------------------------------------