%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET206-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:43:27 PM UTC 2026
% Result : Unsatisfiable 4.80s 1.21s
% Output : Refutation 4.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 24
% Syntax : Number of formulae : 108 ( 24 unt; 8 def)
% Number of atoms : 254 ( 42 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 274 ( 128 ~; 139 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 69 ( 0 sgn 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',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/Axioms/SET004-0.ax',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product1) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',complement1) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',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/Axioms/SET004-0.ax',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f113,axiom,
intersection(complement(compose(element_relation,complement(identity_relation))),element_relation) = singleton_relation,
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-1.ax',compose_can_define_singleton) ).
fof(f122,negated_conjecture,
cross_product(null_class,y) != null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cross_product_with_null_class2_1) ).
fof(f123,plain,
null_class != cross_product(null_class,y),
inference(reorient_equations,[],[f122]) ).
fof(f128,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(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f128]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f128]) ).
fof(f187,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f190,definition,
sF0 = cross_product(null_class,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
cross_product(null_class,y) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,plain,
null_class != sF0,
inference(definition_folding,[],[f123,f191]) ).
fof(f194,plain,
! [X0] :
( ~ member(regular(complement(X0)),X0)
| complement(X0) = null_class ),
inference(resolution,[],[f68,f24]) ).
fof(f195,plain,
! [X0,X1] :
( ~ member(not_subclass_element(complement(X0),X1),X0)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f2,f24]) ).
fof(f207,plain,
! [X0,X1] :
( member(regular(X0),X1)
| ~ subclass(X0,X1)
| null_class = X0 ),
inference(resolution,[],[f1,f68]) ).
fof(f208,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X2),X1)
| ~ subclass(X0,X1)
| subclass(X0,X2) ),
inference(resolution,[],[f1,f2]) ).
fof(f275,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f291,plain,
! [X0] :
( ~ member(X0,singleton_relation)
| member(X0,element_relation) ),
inference(superposition,[],[f22,f113]) ).
fof(f293,plain,
! [X0] :
( member(X0,complement(compose(element_relation,complement(identity_relation))))
| ~ member(X0,singleton_relation) ),
inference(superposition,[],[f21,f113]) ).
fof(f352,plain,
! [X0] :
( ~ member(X0,complement(compose(element_relation,complement(identity_relation))))
| ~ member(X0,element_relation)
| member(X0,singleton_relation) ),
inference(superposition,[],[f23,f113]) ).
fof(f372,definition,
( spl1_22
<=> null_class = singleton_relation ),
introduced(definition,[new_symbols(definition,[spl1_22])],[avatar_definition]) ).
fof(f373,plain,
( null_class != singleton_relation
| spl1_22 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f374,plain,
( null_class = singleton_relation
| ~ spl1_22 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f450,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,null_class) ),
inference(superposition,[],[f137,f191]) ).
fof(f597,plain,
! [X0] :
( ~ member(X0,sF0)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(superposition,[],[f140,f191]) ).
fof(f1155,plain,
! [X0] :
( ~ subclass(complement(X0),X0)
| complement(X0) = null_class
| complement(X0) = null_class ),
inference(resolution,[],[f207,f194]) ).
fof(f1166,plain,
! [X0] :
( ~ subclass(complement(X0),X0)
| complement(X0) = null_class ),
inference(duplicate_literal_removal,[],[f1155]) ).
fof(f1175,plain,
! [X0] :
( ~ member(X0,compose(element_relation,complement(identity_relation)))
| ~ member(X0,singleton_relation) ),
inference(resolution,[],[f293,f24]) ).
fof(f1281,plain,
! [X0,X1] :
( ~ subclass(complement(X0),X0)
| subclass(complement(X0),X1)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f208,f195]) ).
fof(f1293,plain,
! [X0,X1] :
( ~ subclass(complement(X0),X0)
| subclass(complement(X0),X1) ),
inference(duplicate_literal_removal,[],[f1281]) ).
fof(f4098,plain,
( regular(sF0) = unordered_pair(unordered_pair(first(regular(sF0)),first(regular(sF0))),unordered_pair(first(regular(sF0)),unordered_pair(second(regular(sF0)),second(regular(sF0)))))
| null_class = sF0 ),
inference(resolution,[],[f597,f68]) ).
fof(f4109,plain,
regular(sF0) = unordered_pair(unordered_pair(first(regular(sF0)),first(regular(sF0))),unordered_pair(first(regular(sF0)),unordered_pair(second(regular(sF0)),second(regular(sF0))))),
inference(forward_subsumption_resolution,[],[f4098,f192]) ).
fof(f4527,definition,
( spl1_291
<=> null_class = complement(universal_class) ),
introduced(definition,[new_symbols(definition,[spl1_291])],[avatar_definition]) ).
fof(f4529,plain,
( null_class = complement(universal_class)
| ~ spl1_291 ),
inference(avatar_component_clause,[],[f4527]) ).
fof(f6510,definition,
( spl1_352
<=> null_class = complement(compose(element_relation,complement(identity_relation))) ),
introduced(definition,[new_symbols(definition,[spl1_352])],[avatar_definition]) ).
fof(f6512,plain,
( null_class = complement(compose(element_relation,complement(identity_relation)))
| ~ spl1_352 ),
inference(avatar_component_clause,[],[f6510]) ).
fof(f7217,plain,
( ~ member(regular(sF0),sF0)
| member(first(regular(sF0)),null_class) ),
inference(superposition,[],[f450,f4109]) ).
fof(f7314,definition,
( spl1_430
<=> member(first(regular(sF0)),null_class) ),
introduced(definition,[new_symbols(definition,[spl1_430])],[avatar_definition]) ).
fof(f7315,plain,
( member(first(regular(sF0)),null_class)
| ~ spl1_430 ),
inference(avatar_component_clause,[],[f7314]) ).
fof(f7322,definition,
( spl1_432
<=> member(regular(sF0),sF0) ),
introduced(definition,[new_symbols(definition,[spl1_432])],[avatar_definition]) ).
fof(f7323,plain,
( ~ member(regular(sF0),sF0)
| spl1_432 ),
inference(avatar_component_clause,[],[f7322]) ).
fof(f7327,plain,
( spl1_430
| ~ spl1_432 ),
inference(avatar_split_clause,[],[f7217,f7322,f7314]) ).
fof(f7578,plain,
( ~ subclass(sF0,sF0)
| null_class = sF0
| spl1_432 ),
inference(resolution,[],[f7323,f207]) ).
fof(f7579,plain,
( null_class = sF0
| spl1_432 ),
inference(forward_subsumption_resolution,[],[f7578,f187]) ).
fof(f7582,plain,
( $false
| spl1_432 ),
inference(forward_subsumption_resolution,[],[f7579,f192]) ).
fof(f7583,plain,
spl1_432,
inference(avatar_contradiction_clause,[],[f7582]) ).
fof(f7651,plain,
( ! [X0] :
( member(first(regular(sF0)),X0)
| null_class = X0 )
| ~ spl1_430 ),
inference(resolution,[],[f7315,f275]) ).
fof(f7653,plain,
( ! [X0] :
( member(first(regular(sF0)),X0)
| ~ subclass(null_class,X0) )
| ~ spl1_430 ),
inference(resolution,[],[f7315,f1]) ).
fof(f7882,plain,
( null_class = complement(compose(element_relation,complement(identity_relation)))
| ~ member(first(regular(sF0)),element_relation)
| member(first(regular(sF0)),singleton_relation)
| ~ spl1_430 ),
inference(resolution,[],[f7651,f352]) ).
fof(f7895,plain,
( null_class = singleton_relation
| member(first(regular(sF0)),element_relation)
| ~ spl1_430 ),
inference(resolution,[],[f7651,f291]) ).
fof(f7898,plain,
( member(first(regular(sF0)),element_relation)
| spl1_22
| ~ spl1_430 ),
inference(forward_subsumption_resolution,[],[f7895,f373]) ).
fof(f7919,definition,
( spl1_455
<=> member(first(regular(sF0)),singleton_relation) ),
introduced(definition,[new_symbols(definition,[spl1_455])],[avatar_definition]) ).
fof(f7920,plain,
( ~ member(first(regular(sF0)),singleton_relation)
| spl1_455 ),
inference(avatar_component_clause,[],[f7919]) ).
fof(f7921,plain,
( member(first(regular(sF0)),singleton_relation)
| ~ spl1_455 ),
inference(avatar_component_clause,[],[f7919]) ).
fof(f7923,definition,
( spl1_456
<=> member(first(regular(sF0)),element_relation) ),
introduced(definition,[new_symbols(definition,[spl1_456])],[avatar_definition]) ).
fof(f7924,plain,
( member(first(regular(sF0)),element_relation)
| ~ spl1_456 ),
inference(avatar_component_clause,[],[f7923]) ).
fof(f7925,plain,
( ~ member(first(regular(sF0)),element_relation)
| spl1_456 ),
inference(avatar_component_clause,[],[f7923]) ).
fof(f7926,plain,
( spl1_455
| ~ spl1_456
| spl1_352
| ~ spl1_430 ),
inference(avatar_split_clause,[],[f7882,f7314,f6510,f7923,f7919]) ).
fof(f7936,plain,
( spl1_456
| spl1_22
| ~ spl1_430 ),
inference(avatar_split_clause,[],[f7898,f7314,f372,f7923]) ).
fof(f8082,plain,
( ~ subclass(null_class,complement(compose(element_relation,complement(identity_relation))))
| ~ member(first(regular(sF0)),element_relation)
| member(first(regular(sF0)),singleton_relation)
| ~ spl1_430 ),
inference(resolution,[],[f7653,f352]) ).
fof(f8095,plain,
( ~ subclass(null_class,singleton_relation)
| member(first(regular(sF0)),element_relation)
| ~ spl1_430 ),
inference(resolution,[],[f7653,f291]) ).
fof(f8517,plain,
null_class = complement(universal_class),
inference(resolution,[],[f1166,f4]) ).
fof(f8535,plain,
! [X0] : subclass(complement(universal_class),X0),
inference(resolution,[],[f1293,f4]) ).
fof(f8679,plain,
( ~ member(first(regular(sF0)),singleton_relation)
| ~ subclass(null_class,compose(element_relation,complement(identity_relation)))
| ~ spl1_430 ),
inference(resolution,[],[f1175,f7653]) ).
fof(f8787,plain,
( ~ subclass(null_class,singleton_relation)
| ~ spl1_430
| spl1_456 ),
inference(forward_subsumption_resolution,[],[f8095,f7925]) ).
fof(f8853,plain,
spl1_291,
inference(avatar_split_clause,[],[f8517,f4527]) ).
fof(f8855,plain,
( ~ subclass(singleton_relation,singleton_relation)
| ~ spl1_22
| ~ spl1_430
| spl1_456 ),
inference(forward_demodulation,[],[f8787,f374]) ).
fof(f8860,plain,
( $false
| ~ spl1_22
| ~ spl1_430
| spl1_456 ),
inference(forward_subsumption_resolution,[],[f8855,f187]) ).
fof(f8861,plain,
( ~ spl1_22
| ~ spl1_430
| spl1_456 ),
inference(avatar_contradiction_clause,[],[f8860]) ).
fof(f8869,plain,
( ~ subclass(null_class,complement(compose(element_relation,complement(identity_relation))))
| member(first(regular(sF0)),singleton_relation)
| ~ spl1_430
| ~ spl1_456 ),
inference(forward_subsumption_resolution,[],[f8082,f7924]) ).
fof(f8877,plain,
( ~ subclass(null_class,compose(element_relation,complement(identity_relation)))
| ~ spl1_430
| ~ spl1_455 ),
inference(forward_subsumption_resolution,[],[f8679,f7921]) ).
fof(f8893,plain,
( complement(compose(element_relation,complement(identity_relation))) = complement(universal_class)
| ~ spl1_291
| ~ spl1_352 ),
inference(forward_demodulation,[],[f6512,f4529]) ).
fof(f8895,plain,
( ~ subclass(complement(universal_class),compose(element_relation,complement(identity_relation)))
| ~ spl1_291
| ~ spl1_430
| ~ spl1_455 ),
inference(forward_demodulation,[],[f8877,f4529]) ).
fof(f8896,plain,
( $false
| ~ spl1_291
| ~ spl1_430
| ~ spl1_455 ),
inference(forward_subsumption_resolution,[],[f8895,f8535]) ).
fof(f8897,plain,
( ~ spl1_291
| ~ spl1_430
| ~ spl1_455 ),
inference(avatar_contradiction_clause,[],[f8896]) ).
fof(f8898,plain,
( ~ subclass(null_class,complement(compose(element_relation,complement(identity_relation))))
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(forward_subsumption_resolution,[],[f8869,f7920]) ).
fof(f8899,plain,
( ~ subclass(null_class,complement(universal_class))
| ~ spl1_291
| ~ spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(forward_demodulation,[],[f8898,f8893]) ).
fof(f8900,plain,
( ~ subclass(complement(universal_class),complement(universal_class))
| ~ spl1_291
| ~ spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(forward_demodulation,[],[f8899,f4529]) ).
fof(f8901,plain,
( $false
| ~ spl1_291
| ~ spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(forward_subsumption_resolution,[],[f8900,f8535]) ).
fof(f8902,plain,
( ~ spl1_291
| ~ spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(avatar_contradiction_clause,[],[f8901]) ).
cnf(s408,plain,
( spl1_430
| ~ spl1_432 ),
inference(sat_conversion,[],[f7327]) ).
cnf(s434,plain,
spl1_432,
inference(sat_conversion,[],[f7583]) ).
cnf(s453,plain,
( spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(sat_conversion,[],[f7926]) ).
cnf(s456,plain,
( spl1_22
| ~ spl1_430
| spl1_456 ),
inference(sat_conversion,[],[f7936]) ).
cnf(s543,plain,
spl1_291,
inference(sat_conversion,[],[f8853]) ).
cnf(s545,plain,
( ~ spl1_22
| ~ spl1_430
| spl1_456 ),
inference(sat_conversion,[],[f8861]) ).
cnf(s550,plain,
( ~ spl1_291
| ~ spl1_430
| ~ spl1_455 ),
inference(sat_conversion,[],[f8897]) ).
cnf(s551,plain,
( ~ spl1_291
| ~ spl1_352
| ~ spl1_430
| spl1_455
| ~ spl1_456 ),
inference(sat_conversion,[],[f8902]) ).
cnf(s552,plain,
spl1_430,
inference(rat,[],[s408,s434]) ).
cnf(s553,plain,
~ spl1_455,
inference(rat,[],[s550,s543,s552]) ).
cnf(s569,plain,
~ spl1_456,
inference(rat,[],[s453,s551,s553,s552,s543]) ).
cnf(s570,plain,
~ spl1_22,
inference(rat,[],[s545,s552,s569]) ).
cnf(s571,plain,
$false,
inference(rat,[],[s456,s552,s569,s570]) ).
fof(f8903,plain,
$false,
inference(avatar_sat_refutation,[],[s571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET206-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 28 01:08:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.80/1.21 % (2899490)Will run a generic schedule for satisfiability detection.
% 4.80/1.21 % (2899497)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2325496564:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.80/1.21 % (2899496)% WARNING: option uhcvi not known.
% 4.80/1.21 % (2899495)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2387050704_2999 on theBenchmark for (2999ds/0Mi)
% 4.80/1.21 % (2899496)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2463736885:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.80/1.21 % (2899501)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1391479608:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.80/1.21 % (2899498)dis+10_1_sil=32000:sp=arity:random_seed=1741192271:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.80/1.21 % (2899499)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2925075698:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.80/1.21 % (2899500)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1631564800:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.80/1.21 % (2899498)Instruction limit reached!
% 4.80/1.21 % (2899498)------------------------------
% 4.80/1.21 % (2899498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899498)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899498)Termination reason: Instruction limit
% 4.80/1.21 % (2899498)Termination phase: Saturation
% 4.80/1.21 % (2899498)Time elapsed: 0.067 s
% 4.80/1.21 % (2899498)Peak memory usage: 13 MB
% 4.80/1.21 % (2899498)Instructions burned: 103 (million)
% 4.80/1.21 % (2899499)Instruction limit reached!
% 4.80/1.21 % (2899499)------------------------------
% 4.80/1.21 % (2899499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899499)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899499)Termination reason: Instruction limit
% 4.80/1.21 % (2899499)Termination phase: Saturation
% 4.80/1.21 % (2899499)Time elapsed: 0.071 s
% 4.80/1.21 % (2899499)Peak memory usage: 13 MB
% 4.80/1.21 % (2899499)Instructions burned: 117 (million)
% 4.80/1.21 % (2899500)Instruction limit reached!
% 4.80/1.21 % (2899500)------------------------------
% 4.80/1.21 % (2899500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899500)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899500)Termination reason: Instruction limit
% 4.80/1.21 % (2899500)Termination phase: Saturation
% 4.80/1.21 % (2899500)Time elapsed: 0.079 s
% 4.80/1.21 % (2899500)Peak memory usage: 13 MB
% 4.80/1.21 % (2899500)Instructions burned: 132 (million)
% 4.80/1.21 % (2899509)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2425231237:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.80/1.21 % (2899510)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2150247822:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.80/1.21 % (2899511)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4055894653:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.80/1.21 % (2899501)Instruction limit reached!
% 4.80/1.21 % (2899501)------------------------------
% 4.80/1.21 % (2899501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899501)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899501)Termination reason: Instruction limit
% 4.80/1.21 % (2899501)Termination phase: Saturation
% 4.80/1.21 % (2899501)Time elapsed: 0.113 s
% 4.80/1.21 % (2899501)Peak memory usage: 14 MB
% 4.80/1.21 % (2899501)Instructions burned: 159 (million)
% 4.80/1.21 % (2899515)ott-21_1_sil=16000:fs=off:random_seed=1827781525:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.80/1.21 % (2899510)Instruction limit reached!
% 4.80/1.21 % (2899510)------------------------------
% 4.80/1.21 % (2899510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899510)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899510)Termination reason: Instruction limit
% 4.80/1.21 % (2899510)Termination phase: Saturation
% 4.80/1.21 % (2899510)Time elapsed: 0.087 s
% 4.80/1.21 % (2899510)Peak memory usage: 13 MB
% 4.80/1.21 % (2899510)Instructions burned: 131 (million)
% 4.80/1.21 % (2899517)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1180969449:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 4.80/1.21 % TRYING [1]
% 4.80/1.21 % TRYING [2]
% 4.80/1.21 % TRYING [3]
% 4.80/1.21 % (2899515)Instruction limit reached!
% 4.80/1.21 % (2899515)------------------------------
% 4.80/1.21 % (2899515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899515)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899515)Termination reason: Instruction limit
% 4.80/1.21 % (2899515)Termination phase: Saturation
% 4.80/1.21 % (2899515)Time elapsed: 0.099 s
% 4.80/1.21 % (2899515)Peak memory usage: 13 MB
% 4.80/1.21 % (2899515)Instructions burned: 182 (million)
% 4.80/1.21 % (2899519)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3436004432:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.80/1.21 % TRYING [1]
% 4.80/1.21 % TRYING [2]
% 4.80/1.21 % TRYING [3]
% 4.80/1.21 % TRYING [4]
% 4.80/1.21 % (2899509)Instruction limit reached!
% 4.80/1.21 % (2899509)------------------------------
% 4.80/1.21 % (2899509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899509)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899509)Termination reason: Instruction limit
% 4.80/1.21 % (2899509)Termination phase: Finite model building constraint generation
% 4.80/1.21 % (2899509)Time elapsed: 0.328 s
% 4.80/1.21 % (2899509)Peak memory usage: 34 MB
% 4.80/1.21 % (2899509)Instructions burned: 714 (million)
% 4.80/1.21 % (2899521)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2317688647:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 4.80/1.21 % TRYING [1]
% 4.80/1.21 % TRYING [2]
% 4.80/1.21 % (2899517)Instruction limit reached!
% 4.80/1.21 % (2899517)------------------------------
% 4.80/1.21 % (2899517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899517)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899517)Termination reason: Instruction limit
% 4.80/1.21 % (2899517)Termination phase: Saturation
% 4.80/1.21 % (2899517)Time elapsed: 0.343 s
% 4.80/1.21 % (2899517)Peak memory usage: 14 MB
% 4.80/1.21 % (2899517)Instructions burned: 477 (million)
% 4.80/1.21 % (2899511)Instruction limit reached!
% 4.80/1.21 % (2899511)------------------------------
% 4.80/1.21 % (2899511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899511)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899511)Termination reason: Instruction limit
% 4.80/1.21 % (2899511)Termination phase: Saturation
% 4.80/1.21 % (2899511)Time elapsed: 0.451 s
% 4.80/1.21 % (2899511)Peak memory usage: 19 MB
% 4.80/1.21 % (2899511)Instructions burned: 684 (million)
% 4.80/1.21 % (2899523)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4056366841:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 4.80/1.21 % (2899524)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1578223921:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.80/1.21 % TRYING [3]
% 4.80/1.21 % (2899519)Instruction limit reached!
% 4.80/1.21 % (2899519)------------------------------
% 4.80/1.21 % (2899519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899519)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899519)Termination reason: Instruction limit
% 4.80/1.21 % (2899519)Termination phase: Finite model building constraint generation
% 4.80/1.21 % (2899519)Time elapsed: 0.400 s
% 4.80/1.21 % (2899519)Peak memory usage: 25 MB
% 4.80/1.21 % (2899519)Instructions burned: 865 (million)
% 4.80/1.21 % (2899527)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1826434553:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.80/1.21 % (2899521) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2899490-2899521"...
% 4.80/1.21 % (2899521)...printing done.
% 4.80/1.21 % (2899521)Refutation found. Thanks to Tanya!
% 4.80/1.21 % SZS status Unsatisfiable for theBenchmark
% 4.80/1.21 % SZS output start Proof for theBenchmark
% See solution above
% 4.80/1.21 % (2899521)------------------------------
% 4.80/1.21 % (2899521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.80/1.21 % (2899521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.80/1.21 % (2899521)CaDiCaL version: 2.1.3
% 4.80/1.21 % (2899521)Termination reason: Refutation
% 4.80/1.21 % (2899521)Time elapsed: 0.321 s
% 4.80/1.21 % (2899521)Peak memory usage: 17 MB
% 4.80/1.21 % (2899521)Instructions burned: 539 (million)
% 4.80/1.21 % (2899490)Success in time 0.808 s
% 4.80/1.21 % Vampire exiting
%------------------------------------------------------------------------------