%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET350-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:49 PM UTC 2026
% Result : Unsatisfiable 13.69s 3.70s
% Output : Refutation 19.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 34
% Syntax : Number of formulae : 152 ( 41 unt; 10 def)
% Number of atoms : 394 ( 71 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 454 ( 212 ~; 236 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 7 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-3 aty)
% Number of variables : 172 ( 0 sgn 172 !; 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(f11,axiom,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pairs_in_universal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f20,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation3) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
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(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(f54,axiom,
! [X0] : domain_of(restrict(element_relation,universal_class,X0)) = sum_class(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_class_definition) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,negated_conjecture,
sum_class(x) = null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_sum_class_is_null_class_1) ).
fof(f123,plain,
null_class = sum_class(x),
inference(reorient_equations,[],[f122]) ).
fof(f124,negated_conjecture,
x != null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_sum_class_is_null_class_2) ).
fof(f125,plain,
null_class != x,
inference(reorient_equations,[],[f124]) ).
fof(f126,negated_conjecture,
x != singleton(null_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_sum_class_is_null_class_3) ).
fof(f127,plain,
! [X0] : sum_class(X0) = domain_of(intersection(element_relation,cross_product(universal_class,X0))),
inference(definition_unfolding,[],[f54,f28]) ).
fof(f131,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f131]) ).
fof(f145,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation) ),
inference(definition_unfolding,[],[f20,f131,f131]) ).
fof(f147,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(f148,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(f189,plain,
null_class = domain_of(intersection(element_relation,cross_product(universal_class,x))),
inference(definition_unfolding,[],[f123,f127]) ).
fof(f190,plain,
x != unordered_pair(null_class,null_class),
inference(definition_unfolding,[],[f126,f12]) ).
fof(f195,definition,
sF0 = cross_product(universal_class,x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f196,plain,
cross_product(universal_class,x) = sF0,
inference(reorient_equations,[],[f195]) ).
fof(f197,definition,
sF1 = intersection(element_relation,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f198,plain,
intersection(element_relation,sF0) = sF1,
inference(reorient_equations,[],[f197]) ).
fof(f199,definition,
sF2 = domain_of(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f200,plain,
domain_of(sF1) = sF2,
inference(reorient_equations,[],[f199]) ).
fof(f201,plain,
null_class = sF2,
inference(definition_folding,[],[f189,f200,f198,f196]) ).
fof(f202,definition,
sF3 = unordered_pair(null_class,null_class),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f203,plain,
unordered_pair(null_class,null_class) = sF3,
inference(reorient_equations,[],[f202]) ).
fof(f204,plain,
x != sF3,
inference(definition_folding,[],[f190,f203]) ).
fof(f205,plain,
null_class = domain_of(sF1),
inference(forward_demodulation,[],[f200,f201]) ).
fof(f208,definition,
( spl4_1
<=> member(null_class,universal_class) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f210,plain,
( ~ member(null_class,universal_class)
| spl4_1 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f212,definition,
( spl4_2
<=> member(null_class,sF3) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f213,plain,
( ~ member(null_class,sF3)
| spl4_2 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f214,plain,
( member(null_class,sF3)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f219,plain,
! [X0] :
( ~ member(X0,sF3)
| null_class = X0
| null_class = X0 ),
inference(superposition,[],[f8,f203]) ).
fof(f220,plain,
! [X0] :
( ~ member(X0,sF3)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f219]) ).
fof(f221,plain,
! [X2,X0,X1] :
( not_subclass_element(unordered_pair(X0,X1),X2) = X1
| not_subclass_element(unordered_pair(X0,X1),X2) = X0
| subclass(unordered_pair(X0,X1),X2) ),
inference(resolution,[],[f2,f8]) ).
fof(f223,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f21,f2]) ).
fof(f228,plain,
( null_class = regular(sF3)
| null_class = sF3 ),
inference(resolution,[],[f220,f68]) ).
fof(f230,definition,
( spl4_3
<=> null_class = sF3 ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f231,plain,
( null_class != sF3
| spl4_3 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f232,plain,
( null_class = sF3
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl4_4
<=> null_class = regular(sF3) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f236,plain,
( null_class = regular(sF3)
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f237,plain,
( spl4_3
| spl4_4 ),
inference(avatar_split_clause,[],[f228,f234,f230]) ).
fof(f244,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,null_class)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f269,plain,
! [X0] :
( member(X0,sF1)
| ~ member(X0,sF0)
| ~ member(X0,element_relation) ),
inference(superposition,[],[f23,f198]) ).
fof(f282,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),null_class)
| null_class = X1
| subclass(X0,X1) ),
inference(resolution,[],[f244,f3]) ).
fof(f642,plain,
! [X0] :
( null_class = X0
| subclass(null_class,X0)
| subclass(null_class,X0) ),
inference(resolution,[],[f282,f2]) ).
fof(f645,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f642]) ).
fof(f646,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f645,f7]) ).
fof(f647,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f646]) ).
fof(f657,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f223,f3]) ).
fof(f665,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f657]) ).
fof(f707,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| subclass(unordered_pair(X1,X0),X2)
| not_subclass_element(unordered_pair(X1,X0),X2) = X1
| subclass(unordered_pair(X1,X0),X2) ),
inference(superposition,[],[f3,f221]) ).
fof(f711,plain,
! [X2,X0,X1] :
( not_subclass_element(unordered_pair(X1,X0),X2) = X1
| subclass(unordered_pair(X1,X0),X2)
| ~ member(X0,X2) ),
inference(duplicate_literal_removal,[],[f707]) ).
fof(f726,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f665,f647]) ).
fof(f991,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,f148]) ).
fof(f1084,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f147,f726]) ).
fof(f1085,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f1084]) ).
fof(f1400,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| subclass(unordered_pair(X0,X1),X2)
| subclass(unordered_pair(X0,X1),X2)
| ~ member(X1,X2) ),
inference(superposition,[],[f3,f711]) ).
fof(f1403,plain,
! [X2,X0,X1] :
( subclass(unordered_pair(X0,X1),X2)
| ~ member(X0,X2)
| ~ member(X1,X2) ),
inference(duplicate_literal_removal,[],[f1400]) ).
fof(f1405,plain,
! [X2,X0,X1] :
( ~ subclass(X1,unordered_pair(X0,X2))
| ~ member(X2,X1)
| ~ member(X0,X1)
| unordered_pair(X0,X2) = X1 ),
inference(resolution,[],[f1403,f7]) ).
fof(f1883,plain,
( member(null_class,sF3)
| ~ member(null_class,universal_class) ),
inference(superposition,[],[f9,f203]) ).
fof(f1885,plain,
member(sF3,universal_class),
inference(superposition,[],[f11,f203]) ).
fof(f1895,plain,
! [X0] :
( ~ subclass(X0,sF3)
| ~ member(null_class,X0)
| ~ member(null_class,X0)
| sF3 = X0 ),
inference(superposition,[],[f1405,f203]) ).
fof(f1906,plain,
! [X0] :
( ~ member(null_class,X0)
| ~ subclass(X0,sF3)
| sF3 = X0 ),
inference(duplicate_literal_removal,[],[f1895]) ).
fof(f1946,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,x)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f142,f196]) ).
fof(f1967,definition,
( spl4_33
<=> member(null_class,x) ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f1968,plain,
( ~ member(null_class,x)
| spl4_33 ),
inference(avatar_component_clause,[],[f1967]) ).
fof(f1969,plain,
( member(null_class,x)
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f1967]) ).
fof(f2794,definition,
( spl4_45
<=> ! [X0] : ~ member(X0,null_class) ),
introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition]) ).
fof(f2795,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl4_45 ),
inference(avatar_component_clause,[],[f2794]) ).
fof(f3393,plain,
( ~ spl4_1
| spl4_2 ),
inference(avatar_split_clause,[],[f1883,f212,f208]) ).
fof(f3532,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f1085,f68]) ).
fof(f3538,plain,
! [X0] : ~ member(X0,null_class),
inference(backward_demodulation,[],[f1085,f3532]) ).
fof(f4404,plain,
spl4_45,
inference(avatar_split_clause,[],[f3538,f2794]) ).
fof(f4712,plain,
( ! [X2,X0,X1] :
( ~ member(X0,cross_product(unordered_pair(X2,X2),universal_class))
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1)) )
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f991,f2795]) ).
fof(f4914,plain,
( ! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) )
| ~ spl4_45 ),
inference(resolution,[],[f4712,f142]) ).
fof(f4934,plain,
( ! [X2,X0,X1] :
( ~ member(X0,universal_class)
| member(X0,domain_of(sF1))
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF0)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) )
| ~ spl4_45 ),
inference(resolution,[],[f4914,f269]) ).
fof(f4939,plain,
( ! [X2,X0,X1] :
( member(X0,null_class)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF0)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) )
| ~ spl4_45 ),
inference(forward_demodulation,[],[f4934,f205]) ).
fof(f4942,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) )
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f4939,f2795]) ).
fof(f4943,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),element_relation)
| ~ member(X1,unordered_pair(X2,X2))
| ~ member(X2,universal_class)
| ~ member(X0,universal_class)
| ~ member(X0,x)
| ~ member(X1,universal_class) )
| ~ spl4_45 ),
inference(resolution,[],[f4942,f1946]) ).
fof(f5008,plain,
( member(null_class,sF3)
| null_class = sF3
| ~ spl4_4 ),
inference(superposition,[],[f68,f236]) ).
fof(f5649,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation)
| ~ member(X0,X1)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(resolution,[],[f145,f142]) ).
fof(f5662,plain,
( ! [X2,X0,X1] :
( ~ member(X0,X1)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class)
| ~ member(X0,unordered_pair(X2,X2))
| ~ member(X2,universal_class)
| ~ member(X1,universal_class)
| ~ member(X1,x)
| ~ member(X0,universal_class) )
| ~ spl4_45 ),
inference(resolution,[],[f5649,f4943]) ).
fof(f5680,plain,
( ! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X2,X2))
| ~ member(X1,universal_class)
| ~ member(X0,universal_class)
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| ~ member(X1,x) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5662]) ).
fof(f5727,plain,
( ! [X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(X1,X0)
| ~ member(X1,universal_class)
| ~ member(X0,x)
| ~ member(X1,universal_class) )
| ~ spl4_45 ),
inference(resolution,[],[f5680,f10]) ).
fof(f5738,plain,
( ! [X0,X1] :
( ~ member(X1,universal_class)
| ~ member(X0,universal_class)
| ~ member(X1,X0)
| ~ member(X0,x) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5727]) ).
fof(f5764,plain,
( ! [X2,X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,X0)
| ~ member(X0,x)
| ~ member(X1,X2)
| ~ subclass(X2,universal_class) )
| ~ spl4_45 ),
inference(resolution,[],[f5738,f1]) ).
fof(f5767,plain,
( ! [X2,X0,X1] :
( ~ member(X1,X2)
| ~ member(X1,X0)
| ~ member(X0,x)
| ~ member(X0,universal_class) )
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f5764,f4]) ).
fof(f5776,plain,
( ! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| ~ member(X2,x)
| ~ member(X2,universal_class)
| subclass(X0,X1) )
| ~ spl4_45 ),
inference(resolution,[],[f5767,f2]) ).
fof(f5811,plain,
( ! [X0,X1] :
( ~ member(X0,x)
| ~ member(X0,universal_class)
| subclass(X0,X1)
| subclass(X0,X1) )
| ~ spl4_45 ),
inference(resolution,[],[f5776,f2]) ).
fof(f5837,plain,
( ! [X0,X1] :
( ~ member(X0,x)
| ~ member(X0,universal_class)
| subclass(X0,X1) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5811]) ).
fof(f5888,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(x,X0),universal_class)
| subclass(not_subclass_element(x,X0),X1)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(resolution,[],[f5837,f2]) ).
fof(f5897,plain,
( ! [X2,X0,X1] :
( subclass(not_subclass_element(x,X0),X1)
| subclass(x,X0)
| ~ member(not_subclass_element(x,X0),X2)
| ~ subclass(X2,universal_class) )
| ~ spl4_45 ),
inference(resolution,[],[f5888,f1]) ).
fof(f5898,plain,
( ! [X2,X0,X1] :
( ~ member(not_subclass_element(x,X0),X2)
| subclass(x,X0)
| subclass(not_subclass_element(x,X0),X1) )
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f5897,f4]) ).
fof(f5899,plain,
( ! [X0,X1] :
( subclass(x,X0)
| subclass(not_subclass_element(x,X0),X1)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(resolution,[],[f5898,f2]) ).
fof(f5913,plain,
( ! [X0,X1] :
( subclass(not_subclass_element(x,X0),X1)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5899]) ).
fof(f5918,plain,
( ! [X0] :
( null_class = not_subclass_element(x,X0)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(resolution,[],[f5913,f647]) ).
fof(f5925,plain,
( ! [X0] :
( ~ member(null_class,X0)
| subclass(x,X0)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(superposition,[],[f3,f5918]) ).
fof(f5926,plain,
( ! [X0] :
( member(null_class,x)
| subclass(x,X0)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(superposition,[],[f2,f5918]) ).
fof(f5929,plain,
( ! [X0] :
( member(null_class,x)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5926]) ).
fof(f5930,plain,
( ! [X0] :
( ~ member(null_class,X0)
| subclass(x,X0) )
| ~ spl4_45 ),
inference(duplicate_literal_removal,[],[f5925]) ).
fof(f5936,plain,
( ! [X0] : subclass(x,X0)
| spl4_33
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f5929,f1968]) ).
fof(f5942,plain,
( null_class = x
| spl4_33
| ~ spl4_45 ),
inference(resolution,[],[f5936,f647]) ).
fof(f5946,plain,
( $false
| spl4_33
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f5942,f125]) ).
fof(f5947,plain,
( spl4_33
| ~ spl4_45 ),
inference(avatar_contradiction_clause,[],[f5946]) ).
fof(f5983,plain,
( subclass(x,sF3)
| ~ spl4_2
| ~ spl4_45 ),
inference(resolution,[],[f5930,f214]) ).
fof(f5995,plain,
( ~ subclass(x,sF3)
| x = sF3
| ~ spl4_33 ),
inference(resolution,[],[f1969,f1906]) ).
fof(f6003,plain,
( x = sF3
| ~ spl4_2
| ~ spl4_33
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f5995,f5983]) ).
fof(f6004,plain,
( $false
| ~ spl4_2
| ~ spl4_33
| ~ spl4_45 ),
inference(forward_subsumption_resolution,[],[f6003,f204]) ).
fof(f6005,plain,
( ~ spl4_2
| ~ spl4_33
| ~ spl4_45 ),
inference(avatar_contradiction_clause,[],[f6004]) ).
fof(f6009,plain,
( null_class = sF3
| spl4_2
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f5008,f213]) ).
fof(f6043,plain,
( $false
| spl4_2
| spl4_3
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f6009,f231]) ).
fof(f6044,plain,
( spl4_2
| spl4_3
| ~ spl4_4 ),
inference(avatar_contradiction_clause,[],[f6043]) ).
fof(f6055,plain,
( member(null_class,universal_class)
| ~ spl4_3 ),
inference(backward_demodulation,[],[f1885,f232]) ).
fof(f6190,plain,
( $false
| spl4_1
| ~ spl4_3 ),
inference(forward_subsumption_resolution,[],[f6055,f210]) ).
fof(f6191,plain,
( spl4_1
| ~ spl4_3 ),
inference(avatar_contradiction_clause,[],[f6190]) ).
cnf(s2,plain,
( spl4_3
| spl4_4 ),
inference(sat_conversion,[],[f237]) ).
cnf(s91,plain,
( ~ spl4_1
| spl4_2 ),
inference(sat_conversion,[],[f3393]) ).
cnf(s136,plain,
spl4_45,
inference(sat_conversion,[],[f4404]) ).
cnf(s175,plain,
( spl4_33
| ~ spl4_45 ),
inference(sat_conversion,[],[f5947]) ).
cnf(s182,plain,
( ~ spl4_2
| ~ spl4_33
| ~ spl4_45 ),
inference(sat_conversion,[],[f6005]) ).
cnf(s202,plain,
( spl4_2
| spl4_3
| ~ spl4_4 ),
inference(sat_conversion,[],[f6044]) ).
cnf(s205,plain,
( spl4_1
| ~ spl4_3 ),
inference(sat_conversion,[],[f6191]) ).
cnf(s210,plain,
spl4_33,
inference(rat,[],[s175,s136]) ).
cnf(s211,plain,
~ spl4_2,
inference(rat,[],[s182,s136,s210]) ).
cnf(s218,plain,
~ spl4_1,
inference(rat,[],[s91,s211]) ).
cnf(s219,plain,
~ spl4_3,
inference(rat,[],[s205,s218]) ).
cnf(s223,plain,
~ spl4_4,
inference(rat,[],[s202,s211,s219]) ).
cnf(s240,plain,
$false,
inference(rat,[],[s2,s223,s219]) ).
fof(f6203,plain,
$false,
inference(avatar_sat_refutation,[],[s240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET350-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.41 % Computer : n002.cluster.edu
% 0.18/0.41 % Model : x86_64 x86_64
% 0.18/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.41 % Memory : 8046.5625MB
% 0.18/0.41 % OS : Linux 6.8.0-71-generic
% 0.18/0.41 % CPULimit : 300
% 0.18/0.41 % WCLimit : 300
% 0.18/0.41 % DateTime : Mon Sep 28 01:35:22 UTC 2026
% 0.18/0.42 % CPUTime :
% 0.18/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.46 Running first-order theorem proving
% 0.18/0.46 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
% 18.88/3.65 % (4073932)Input is clausal, will run a generic CNF schedule.
% 18.88/3.65 % (4073938)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=349995136:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.88/3.65 % (4073942)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=853182378:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.88/3.65 % (4073937)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=57033903:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.88/3.65 % (4073940)lrs+10_1_sil=8000:sp=occurrence:random_seed=2159739547:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.88/3.65 % (4073939)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2948706816:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.88/3.65 % (4073941)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3520762911:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.88/3.65 % (4073943)dis-21_1_sil=8000:lcm=predicate:random_seed=3632323744: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)
% 18.88/3.65 % (4073941)Instruction limit reached!
% 18.88/3.65 % (4073941)------------------------------
% 18.88/3.65 % (4073941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.65 % (4073941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.65 % (4073941)CaDiCaL version: 2.1.3
% 18.88/3.65 % (4073941)Termination reason: Instruction limit
% 18.88/3.65 % (4073941)Termination phase: Saturation
% 18.88/3.65 % (4073941)Time elapsed: 0.116 s
% 18.88/3.65 % (4073941)Peak memory usage: 89 MB
% 18.88/3.65 % (4073941)Instructions burned: 114 (million)
% 18.88/3.65 % (4073940)Instruction limit reached!
% 18.88/3.65 % (4073940)------------------------------
% 18.88/3.65 % (4073940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.65 % (4073940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.65 % (4073940)CaDiCaL version: 2.1.3
% 18.88/3.65 % (4073940)Termination reason: Instruction limit
% 18.88/3.65 % (4073940)Termination phase: Saturation
% 18.88/3.65 % (4073940)Time elapsed: 0.116 s
% 18.88/3.65 % (4073940)Peak memory usage: 89 MB
% 18.88/3.65 % (4073940)Instructions burned: 107 (million)
% 18.88/3.65 % (4073943)Instruction limit reached!
% 18.88/3.65 % (4073943)------------------------------
% 18.88/3.65 % (4073943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.65 % (4073943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.65 % (4073943)CaDiCaL version: 2.1.3
% 18.88/3.65 % (4073943)Termination reason: Instruction limit
% 18.88/3.65 % (4073943)Termination phase: Saturation
% 18.88/3.65 % (4073943)Time elapsed: 0.111 s
% 18.88/3.65 % (4073943)Peak memory usage: 90 MB
% 18.88/3.65 % (4073943)Instructions burned: 117 (million)
% 18.88/3.65 % (4073942)Instruction limit reached!
% 18.88/3.65 % (4073942)------------------------------
% 18.88/3.65 % (4073942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.65 % (4073942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.65 % (4073942)CaDiCaL version: 2.1.3
% 18.88/3.65 % (4073942)Termination reason: Instruction limit
% 18.88/3.65 % (4073942)Termination phase: Saturation
% 18.88/3.65 % (4073942)Time elapsed: 0.199 s
% 18.88/3.65 % (4073942)Peak memory usage: 91 MB
% 18.88/3.65 % (4073942)Instructions burned: 181 (million)
% 18.88/3.65 % (4073951)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=4091020774:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.88/3.65 % (4073951)Refutation not found, incomplete strategy
% 18.88/3.65 % (4073951)------------------------------
% 18.88/3.65 % (4073951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.88/3.65 % (4073951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.88/3.65 % (4073951)CaDiCaL version: 2.1.3
% 18.88/3.65 % (4073951)Termination reason: Refutation not found, incomplete strategy
% 18.88/3.65 % (4073951)Time elapsed: 0.006 s
% 18.88/3.65 % (4073951)Peak memory usage: 88 MB
% 18.88/3.65 % (4073951)Instructions burned: 4 (million)
% 18.88/3.65 % (4073952)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3363804881:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 13.69/3.70 % (4073953)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3647133027:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 13.69/3.70 % (4073954)lrs+10_64_to=lpo:sil=8000:random_seed=2425916750:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 13.69/3.70 % (4073953)Refutation not found, incomplete strategy
% 13.69/3.70 % (4073953)------------------------------
% 13.69/3.70 % (4073953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073953)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073953)Termination reason: Refutation not found, incomplete strategy
% 13.69/3.70 % (4073953)Time elapsed: 0.007 s
% 13.69/3.70 % (4073953)Peak memory usage: 88 MB
% 13.69/3.70 % (4073953)Instructions burned: 5 (million)
% 13.69/3.70 % (4073954)Instruction limit reached!
% 13.69/3.70 % (4073954)------------------------------
% 13.69/3.70 % (4073954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073954)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073954)Termination reason: Instruction limit
% 13.69/3.70 % (4073954)Termination phase: Saturation
% 13.69/3.70 % (4073954)Time elapsed: 0.126 s
% 13.69/3.70 % (4073954)Peak memory usage: 89 MB
% 13.69/3.70 % (4073954)Instructions burned: 126 (million)
% 13.69/3.70 % (4073952)Instruction limit reached!
% 13.69/3.70 % (4073952)------------------------------
% 13.69/3.70 % (4073952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073952)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073952)Termination reason: Instruction limit
% 13.69/3.70 % (4073952)Termination phase: Saturation
% 13.69/3.70 % (4073952)Time elapsed: 0.168 s
% 13.69/3.70 % (4073952)Peak memory usage: 90 MB
% 13.69/3.70 % (4073952)Instructions burned: 190 (million)
% 13.69/3.70 % (4073951)------------------------------
% 13.69/3.70 % (4073951)------------------------------
% 13.69/3.70 % (4073953)------------------------------
% 13.69/3.70 % (4073953)------------------------------
% 13.69/3.70 % (4073959)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3343182166:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 13.69/3.70 % (4073960)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1959425258:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 13.69/3.70 % (4073961)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3519698548:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 13.69/3.70 % (4073959)Instruction limit reached!
% 13.69/3.70 % (4073959)------------------------------
% 13.69/3.70 % (4073959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073959)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073959)Termination reason: Instruction limit
% 13.69/3.70 % (4073959)Termination phase: Saturation
% 13.69/3.70 % (4073959)Time elapsed: 0.182 s
% 13.69/3.70 % (4073959)Peak memory usage: 89 MB
% 13.69/3.70 % (4073959)Instructions burned: 194 (million)
% 13.69/3.70 % (4073960)Instruction limit reached!
% 13.69/3.70 % (4073960)------------------------------
% 13.69/3.70 % (4073960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073960)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073960)Termination reason: Instruction limit
% 13.69/3.70 % (4073960)Termination phase: Saturation
% 13.69/3.70 % (4073960)Time elapsed: 0.174 s
% 13.69/3.70 % (4073960)Peak memory usage: 91 MB
% 13.69/3.70 % (4073960)Instructions burned: 157 (million)
% 13.69/3.70 % (4073963)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=4160605043:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 13.69/3.70 % (4073963)Instruction limit reached!
% 13.69/3.70 % (4073963)------------------------------
% 13.69/3.70 % (4073963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073963)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073963)Termination reason: Instruction limit
% 13.69/3.70 % (4073963)Termination phase: Saturation
% 13.69/3.70 % (4073963)Time elapsed: 0.085 s
% 13.69/3.70 % (4073963)Peak memory usage: 94 MB
% 13.69/3.70 % (4073963)Instructions burned: 106 (million)
% 13.69/3.70 % (4073966)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1862029307:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 13.69/3.70 % (4073968)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2683396947:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 13.69/3.70 % (4073966)Instruction limit reached!
% 13.69/3.70 % (4073966)------------------------------
% 13.69/3.70 % (4073966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073966)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073966)Termination reason: Instruction limit
% 13.69/3.70 % (4073966)Termination phase: Saturation
% 13.69/3.70 % (4073966)Time elapsed: 0.109 s
% 13.69/3.70 % (4073966)Peak memory usage: 89 MB
% 13.69/3.70 % (4073966)Instructions burned: 107 (million)
% 13.69/3.70 % (4073969)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=171113118:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 13.69/3.70 % (4073968)Instruction limit reached!
% 13.69/3.70 % (4073968)------------------------------
% 13.69/3.70 % (4073968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073968)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073968)Termination reason: Instruction limit
% 13.69/3.70 % (4073968)Termination phase: Saturation
% 13.69/3.70 % (4073968)Time elapsed: 0.265 s
% 13.69/3.70 % (4073968)Peak memory usage: 90 MB
% 13.69/3.70 % (4073968)Instructions burned: 242 (million)
% 13.69/3.70 % (4073972)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=103385851:i=134:sd=2:doe=on:ss=axioms:sgt=14_2983 on theBenchmark for (2983ds/134Mi)
% 13.69/3.70 % (4073972)Instruction limit reached!
% 13.69/3.70 % (4073972)------------------------------
% 13.69/3.70 % (4073972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073972)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073972)Termination reason: Instruction limit
% 13.69/3.70 % (4073972)Termination phase: Saturation
% 13.69/3.70 % (4073972)Time elapsed: 0.145 s
% 13.69/3.70 % (4073972)Peak memory usage: 90 MB
% 13.69/3.70 % (4073972)Instructions burned: 135 (million)
% 13.69/3.70 % (4073974)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=218484693:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 13.69/3.70 % (4073939)First to succeed.
% 13.69/3.70 % (4073939)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4073932"
% 13.69/3.70 % (4073976)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2803162862:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 13.69/3.70 % (4073976)Instruction limit reached!
% 13.69/3.70 % (4073976)------------------------------
% 13.69/3.70 % (4073976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073976)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073976)Termination reason: Instruction limit
% 13.69/3.70 % (4073976)Termination phase: Saturation
% 13.69/3.70 % (4073976)Time elapsed: 0.177 s
% 13.69/3.70 % (4073976)Peak memory usage: 89 MB
% 13.69/3.70 % (4073976)Instructions burned: 191 (million)
% 13.69/3.70 % (4073974)Instruction limit reached!
% 13.69/3.70 % (4073974)------------------------------
% 13.69/3.70 % (4073974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.69/3.70 % (4073974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.69/3.70 % (4073974)CaDiCaL version: 2.1.3
% 13.69/3.70 % (4073974)Termination reason: Instruction limit
% 13.69/3.70 % (4073974)Termination phase: Saturation
% 13.69/3.70 % (4073974)Time elapsed: 0.526 s
% 13.69/3.70 % (4073974)Peak memory usage: 95 MB
% 13.69/3.70 % (4073974)Instructions burned: 499 (million)
% 13.69/3.70 % (4073939)Refutation found. Thanks to Tanya!
% 13.69/3.70 % SZS status Unsatisfiable for theBenchmark
% 13.69/3.70 % SZS output start Proof for theBenchmark
% See solution above
% 19.87/4.01 % (4073939)------------------------------
% 19.87/4.01 % (4073939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/4.01 % (4073939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/4.01 % (4073939)CaDiCaL version: 2.1.3
% 19.87/4.01 % (4073939)Termination reason: Refutation
% 19.87/4.01 % (4073939)Time elapsed: 2.003 s
% 19.87/4.01 % (4073939)Peak memory usage: 136 MB
% 19.87/4.01 % (4073939)Instructions burned: 1865 (million)
% 19.87/4.01 % (4073939)------------------------------
% 19.87/4.01 % (4073939)------------------------------
% 19.87/4.01 % (4073932)Success in time 2.696 s
% 19.87/4.01 % Vampire exiting
%------------------------------------------------------------------------------