%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU318+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:52:51 PM UTC 2026
% Result : Theorem 12.82s 5.84s
% Output : Refutation 12.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 13
% Syntax : Number of formulae : 139 ( 22 unt; 3 def)
% Number of atoms : 572 ( 51 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 732 ( 299 ~; 324 |; 74 &)
% ( 10 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 200 ( 185 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f18,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f22,axiom,
! [X0,X1] :
( ( top_str(X0)
& element(X1,powerset(the_carrier(X0))) )
=> element(topstr_closure(X0,X1),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_pre_topc) ).
fof(f38,axiom,
! [X0,X1] : subset(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f41,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f42,axiom,
! [X0] :
( ( topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,powerset(powerset(the_carrier(X0))))
=> ( ! [X2] :
( element(X2,powerset(the_carrier(X0)))
=> ( in(X2,X1)
=> closed_subset(X2,X0) ) )
=> closed_subset(meet_of_subsets(the_carrier(X0),X1),X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t44_pre_topc) ).
fof(f43,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ! [X2] :
( in(X2,the_carrier(X0))
=> ( in(X2,topstr_closure(X0,X1))
<=> ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( ( closed_subset(X3,X0)
& subset(X1,X3) )
=> in(X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_pre_topc) ).
fof(f44,axiom,
! [X0] :
( ( topological_space(X0)
& top_str(X0) )
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( element(X3,powerset(the_carrier(X0)))
=> ( in(X3,X2)
<=> ( closed_subset(X3,X0)
& subset(X1,X3) ) ) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_pre_topc) ).
fof(f45,axiom,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset(X1,topstr_closure(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_pre_topc) ).
fof(f47,conjecture,
! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( ( closed_subset(X1,X0)
=> topstr_closure(X0,X1) = X1 )
& ( ( topological_space(X0)
& topstr_closure(X0,X1) = X1 )
=> closed_subset(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t52_pre_topc) ).
fof(f48,negated_conjecture,
~ ! [X0] :
( top_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> ( ( closed_subset(X1,X0)
=> topstr_closure(X0,X1) = X1 )
& ( ( topological_space(X0)
& topstr_closure(X0,X1) = X1 )
=> closed_subset(X1,X0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f53,plain,
! [X0] : subset(X0,X0),
inference(rectify,[],[f38]) ).
fof(f82,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f83,plain,
! [X0,X1] :
( element(topstr_closure(X0,X1),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f22]) ).
fof(f84,plain,
! [X0,X1] :
( element(topstr_closure(X0,X1),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(flattening,[],[f83]) ).
fof(f93,plain,
! [X0] :
( ! [X1] :
( closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ? [X2] :
( ~ closed_subset(X2,X0)
& in(X2,X1)
& element(X2,powerset(the_carrier(X0))) )
| ~ element(X1,powerset(powerset(the_carrier(X0)))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f94,plain,
! [X0] :
( ! [X1] :
( closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ? [X2] :
( ~ closed_subset(X2,X0)
& in(X2,X1)
& element(X2,powerset(the_carrier(X0))) )
| ~ element(X1,powerset(powerset(the_carrier(X0)))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f93]) ).
fof(f95,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,topstr_closure(X0,X1))
<=> ! [X3] :
( in(X2,X3)
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3)
| ~ element(X3,powerset(the_carrier(X0))) ) )
| ~ in(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f96,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( in(X2,topstr_closure(X0,X1))
<=> ! [X3] :
( in(X2,X3)
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3)
| ~ element(X3,powerset(the_carrier(X0))) ) )
| ~ in(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( ( in(X3,X2)
<=> ( closed_subset(X3,X0)
& subset(X1,X3) ) )
| ~ element(X3,powerset(the_carrier(X0))) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),X2) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f98,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( ( in(X3,X2)
<=> ( closed_subset(X3,X0)
& subset(X1,X3) ) )
| ~ element(X3,powerset(the_carrier(X0))) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),X2) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f97]) ).
fof(f99,plain,
! [X0] :
( ! [X1] :
( subset(X1,topstr_closure(X0,X1))
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f45]) ).
fof(f102,plain,
? [X0] :
( ? [X1] :
( ( ( topstr_closure(X0,X1) != X1
& closed_subset(X1,X0) )
| ( ~ closed_subset(X1,X0)
& topological_space(X0)
& topstr_closure(X0,X1) = X1 ) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f103,plain,
? [X0] :
( ? [X1] :
( ( ( topstr_closure(X0,X1) != X1
& closed_subset(X1,X0) )
| ( ~ closed_subset(X1,X0)
& topological_space(X0)
& topstr_closure(X0,X1) = X1 ) )
& element(X1,powerset(the_carrier(X0))) )
& top_str(X0) ),
inference(flattening,[],[f102]) ).
fof(f108,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f109,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f82]) ).
fof(f111,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK0(X0,X1),X1)
& in(sK0(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[f111]) ).
fof(f119,plain,
! [X0,X1] :
( ( element(X0,powerset(X1))
| ~ subset(X0,X1) )
& ( subset(X0,X1)
| ~ element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f120,plain,
! [X0] :
( ! [X1] :
( closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ( ~ closed_subset(sK7(X0,X1),X0)
& in(sK7(X0,X1),X1)
& element(sK7(X0,X1),powerset(the_carrier(X0))) )
| ~ element(X1,powerset(powerset(the_carrier(X0)))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f94]) ).
fof(f121,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( in(X2,topstr_closure(X0,X1))
| ? [X3] :
( ~ in(X2,X3)
& closed_subset(X3,X0)
& subset(X1,X3)
& element(X3,powerset(the_carrier(X0))) ) )
& ( ! [X3] :
( in(X2,X3)
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3)
| ~ element(X3,powerset(the_carrier(X0))) )
| ~ in(X2,topstr_closure(X0,X1)) ) )
| ~ in(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f96]) ).
fof(f122,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( in(X2,topstr_closure(X0,X1))
| ? [X3] :
( ~ in(X2,X3)
& closed_subset(X3,X0)
& subset(X1,X3)
& element(X3,powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( in(X2,X4)
| ~ closed_subset(X4,X0)
| ~ subset(X1,X4)
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X2,topstr_closure(X0,X1)) ) )
| ~ in(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(rectify,[],[f121]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( in(X2,topstr_closure(X0,X1))
| ( ~ in(X2,sK8(X0,X1,X2))
& closed_subset(sK8(X0,X1,X2),X0)
& subset(X1,sK8(X0,X1,X2))
& element(sK8(X0,X1,X2),powerset(the_carrier(X0))) ) )
& ( ! [X4] :
( in(X2,X4)
| ~ closed_subset(X4,X0)
| ~ subset(X1,X4)
| ~ element(X4,powerset(the_carrier(X0))) )
| ~ in(X2,topstr_closure(X0,X1)) ) )
| ~ in(X2,the_carrier(X0)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ top_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f122]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( ( ( in(X3,X2)
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3) )
& ( ( closed_subset(X3,X0)
& subset(X1,X3) )
| ~ in(X3,X2) ) )
| ~ element(X3,powerset(the_carrier(X0))) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),X2) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(nnf_transformation,[],[f98]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( element(X2,powerset(powerset(the_carrier(X0))))
& ! [X3] :
( ( ( in(X3,X2)
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3) )
& ( ( closed_subset(X3,X0)
& subset(X1,X3) )
| ~ in(X3,X2) ) )
| ~ element(X3,powerset(the_carrier(X0))) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),X2) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0] :
( ! [X1] :
( ( element(sK9(X0,X1),powerset(powerset(the_carrier(X0))))
& ! [X3] :
( ( ( in(X3,sK9(X0,X1))
| ~ closed_subset(X3,X0)
| ~ subset(X1,X3) )
& ( ( closed_subset(X3,X0)
& subset(X1,X3) )
| ~ in(X3,sK9(X0,X1)) ) )
| ~ element(X3,powerset(the_carrier(X0))) )
& topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),sK9(X0,X1)) )
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X2,sK9(X0,X1))],[f125]) ).
fof(f127,plain,
( ( ( sK11 != topstr_closure(sK10,sK11)
& closed_subset(sK11,sK10) )
| ( ~ closed_subset(sK11,sK10)
& topological_space(sK10)
& sK11 = topstr_closure(sK10,sK11) ) )
& element(sK11,powerset(the_carrier(sK10)))
& top_str(sK10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11]),skolemize(X0,sK10),skolemize(X1,sK11)],[f103]) ).
fof(f155,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f156,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ in(X3,X0)
| in(X3,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f157,plain,
! [X0,X1] :
( in(sK0(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f158,plain,
! [X0,X1] :
( ~ in(sK0(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f159,plain,
! [X0,X1] :
( element(topstr_closure(X0,X1),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f84]) ).
fof(f183,plain,
! [X0] : subset(X0,X0),
inference(cnf_transformation,[],[f53]) ).
fof(f186,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f188,plain,
! [X0,X1] :
( element(sK7(X0,X1),powerset(the_carrier(X0)))
| closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f189,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| in(sK7(X0,X1),X1)
| closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f190,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ closed_subset(sK7(X0,X1),X0)
| closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f191,plain,
! [X2,X0,X1,X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| ~ closed_subset(X4,X0)
| ~ subset(X1,X4)
| in(X2,X4)
| ~ in(X2,topstr_closure(X0,X1))
| ~ in(X2,the_carrier(X0))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f196,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| topstr_closure(X0,X1) = meet_of_subsets(the_carrier(X0),sK9(X0,X1))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f198,plain,
! [X3,X0,X1] :
( ~ element(X3,powerset(the_carrier(X0)))
| ~ in(X3,sK9(X0,X1))
| closed_subset(X3,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f200,plain,
! [X0,X1] :
( element(sK9(X0,X1),powerset(powerset(the_carrier(X0))))
| ~ element(X1,powerset(the_carrier(X0)))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f201,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| subset(X1,topstr_closure(X0,X1))
| ~ top_str(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f203,plain,
top_str(sK10),
inference(cnf_transformation,[],[f127]) ).
fof(f204,plain,
element(sK11,powerset(the_carrier(sK10))),
inference(cnf_transformation,[],[f127]) ).
fof(f205,plain,
( closed_subset(sK11,sK10)
| sK11 = topstr_closure(sK10,sK11) ),
inference(cnf_transformation,[],[f127]) ).
fof(f206,plain,
( closed_subset(sK11,sK10)
| topological_space(sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f209,plain,
( sK11 != topstr_closure(sK10,sK11)
| topological_space(sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f210,plain,
( sK11 != topstr_closure(sK10,sK11)
| ~ closed_subset(sK11,sK10) ),
inference(cnf_transformation,[],[f127]) ).
fof(f217,definition,
sF12 = topstr_closure(sK10,sK11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f218,plain,
topstr_closure(sK10,sK11) = sF12,
inference(reorient_equations,[],[f217]) ).
fof(f219,plain,
( sK11 != sF12
| ~ closed_subset(sK11,sK10) ),
inference(definition_folding,[],[f210,f218]) ).
fof(f220,plain,
( sK11 != sF12
| topological_space(sK10) ),
inference(definition_folding,[],[f209,f218]) ).
fof(f222,plain,
( closed_subset(sK11,sK10)
| sK11 = sF12 ),
inference(definition_folding,[],[f205,f218]) ).
fof(f223,definition,
sF13 = the_carrier(sK10),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f224,plain,
the_carrier(sK10) = sF13,
inference(reorient_equations,[],[f223]) ).
fof(f225,definition,
sF14 = powerset(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f226,plain,
powerset(sF13) = sF14,
inference(reorient_equations,[],[f225]) ).
fof(f227,plain,
element(sK11,sF14),
inference(definition_folding,[],[f204,f226,f224]) ).
fof(f268,plain,
! [X0] :
( ~ element(X0,sF14)
| subset(X0,sF13) ),
inference(superposition,[],[f186,f226]) ).
fof(f523,plain,
! [X0] :
( ~ element(X0,powerset(sF13))
| subset(X0,topstr_closure(sK10,X0))
| ~ top_str(sK10) ),
inference(superposition,[],[f201,f224]) ).
fof(f525,plain,
! [X0] :
( ~ element(X0,powerset(sF13))
| subset(X0,topstr_closure(sK10,X0)) ),
inference(forward_subsumption_resolution,[],[f523,f203]) ).
fof(f527,plain,
! [X0] :
( subset(X0,topstr_closure(sK10,X0))
| ~ element(X0,sF14) ),
inference(forward_demodulation,[],[f525,f226]) ).
fof(f548,plain,
( element(sF12,powerset(the_carrier(sK10)))
| ~ top_str(sK10)
| ~ element(sK11,powerset(the_carrier(sK10))) ),
inference(superposition,[],[f159,f218]) ).
fof(f552,plain,
( element(sF12,powerset(the_carrier(sK10)))
| ~ element(sK11,powerset(the_carrier(sK10))) ),
inference(forward_subsumption_resolution,[],[f548,f203]) ).
fof(f555,plain,
( element(sF12,powerset(sF13))
| ~ element(sK11,powerset(the_carrier(sK10))) ),
inference(forward_demodulation,[],[f552,f224]) ).
fof(f557,plain,
( element(sF12,sF14)
| ~ element(sK11,powerset(the_carrier(sK10))) ),
inference(forward_demodulation,[],[f555,f226]) ).
fof(f558,plain,
( ~ element(sK11,powerset(sF13))
| element(sF12,sF14) ),
inference(forward_demodulation,[],[f557,f224]) ).
fof(f559,plain,
( ~ element(sK11,sF14)
| element(sF12,sF14) ),
inference(forward_demodulation,[],[f558,f226]) ).
fof(f560,plain,
element(sF12,sF14),
inference(forward_subsumption_resolution,[],[f559,f227]) ).
fof(f561,plain,
subset(sF12,sF13),
inference(resolution,[],[f560,f268]) ).
fof(f584,plain,
! [X0] :
( element(sK9(sK10,X0),powerset(powerset(sF13)))
| ~ element(X0,powerset(sF13))
| ~ topological_space(sK10)
| ~ top_str(sK10) ),
inference(superposition,[],[f200,f224]) ).
fof(f585,plain,
! [X0] :
( element(sK9(sK10,X0),powerset(powerset(sF13)))
| ~ element(X0,powerset(sF13))
| ~ topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f584,f203]) ).
fof(f587,plain,
! [X0] :
( element(sK9(sK10,X0),powerset(sF14))
| ~ element(X0,powerset(sF13))
| ~ topological_space(sK10) ),
inference(forward_demodulation,[],[f585,f226]) ).
fof(f588,plain,
! [X0] :
( element(sK9(sK10,X0),powerset(sF14))
| ~ element(X0,sF14)
| ~ topological_space(sK10) ),
inference(forward_demodulation,[],[f587,f226]) ).
fof(f590,plain,
! [X0] :
( ~ in(X0,sF12)
| in(X0,sF13) ),
inference(resolution,[],[f561,f156]) ).
fof(f600,plain,
! [X0] :
( ~ element(X0,powerset(sF13))
| topstr_closure(sK10,X0) = meet_of_subsets(sF13,sK9(sK10,X0))
| ~ topological_space(sK10)
| ~ top_str(sK10) ),
inference(superposition,[],[f196,f224]) ).
fof(f603,plain,
! [X0] :
( ~ element(X0,powerset(sF13))
| topstr_closure(sK10,X0) = meet_of_subsets(sF13,sK9(sK10,X0))
| ~ topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f600,f203]) ).
fof(f605,plain,
! [X0] :
( ~ element(X0,sF14)
| topstr_closure(sK10,X0) = meet_of_subsets(sF13,sK9(sK10,X0))
| ~ topological_space(sK10) ),
inference(forward_demodulation,[],[f603,f226]) ).
fof(f616,plain,
! [X0] :
( ~ element(X0,powerset(powerset(sF13)))
| in(sK7(sK10,X0),X0)
| closed_subset(meet_of_subsets(sF13,X0),sK10)
| ~ topological_space(sK10)
| ~ top_str(sK10) ),
inference(superposition,[],[f189,f224]) ).
fof(f618,plain,
! [X0] :
( ~ element(X0,powerset(powerset(sF13)))
| in(sK7(sK10,X0),X0)
| closed_subset(meet_of_subsets(sF13,X0),sK10)
| ~ topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f616,f203]) ).
fof(f623,plain,
! [X0] :
( closed_subset(meet_of_subsets(sF13,X0),sK10)
| in(sK7(sK10,X0),X0)
| ~ element(X0,powerset(sF14))
| ~ topological_space(sK10) ),
inference(forward_demodulation,[],[f618,f226]) ).
fof(f651,plain,
( subset(sK11,sF12)
| ~ element(sK11,sF14) ),
inference(superposition,[],[f527,f218]) ).
fof(f652,plain,
subset(sK11,sF12),
inference(forward_subsumption_resolution,[],[f651,f227]) ).
fof(f670,plain,
( ~ subset(sF12,sK11)
| sK11 = sF12 ),
inference(resolution,[],[f652,f155]) ).
fof(f688,plain,
! [X2,X0,X1] :
( closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ in(sK7(X0,X1),sK9(X0,X2))
| closed_subset(sK7(X0,X1),X0)
| ~ element(X2,powerset(the_carrier(X0)))
| ~ topological_space(X0)
| ~ top_str(X0) ),
inference(resolution,[],[f188,f198]) ).
fof(f715,plain,
! [X2,X0,X1] :
( closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ in(sK7(X0,X1),sK9(X0,X2))
| closed_subset(sK7(X0,X1),X0)
| ~ element(X2,powerset(the_carrier(X0))) ),
inference(duplicate_literal_removal,[],[f688]) ).
fof(f718,plain,
! [X2,X0,X1] :
( ~ in(sK7(X0,X1),sK9(X0,X2))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ topological_space(X0)
| ~ top_str(X0)
| closed_subset(meet_of_subsets(the_carrier(X0),X1),X0)
| ~ element(X2,powerset(the_carrier(X0))) ),
inference(forward_subsumption_resolution,[],[f715,f190]) ).
fof(f792,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(sF13))
| ~ closed_subset(X0,sK10)
| ~ subset(X1,X0)
| in(X2,X0)
| ~ in(X2,topstr_closure(sK10,X1))
| ~ in(X2,sF13)
| ~ element(X1,powerset(sF13))
| ~ top_str(sK10) ),
inference(superposition,[],[f191,f224]) ).
fof(f797,plain,
! [X2,X0,X1] :
( ~ element(X0,powerset(sF13))
| ~ closed_subset(X0,sK10)
| ~ subset(X1,X0)
| in(X2,X0)
| ~ in(X2,topstr_closure(sK10,X1))
| ~ in(X2,sF13)
| ~ element(X1,powerset(sF13)) ),
inference(forward_subsumption_resolution,[],[f792,f203]) ).
fof(f802,plain,
! [X2,X0,X1] :
( ~ element(X0,sF14)
| ~ closed_subset(X0,sK10)
| ~ subset(X1,X0)
| in(X2,X0)
| ~ in(X2,topstr_closure(sK10,X1))
| ~ in(X2,sF13)
| ~ element(X1,powerset(sF13)) ),
inference(forward_demodulation,[],[f797,f226]) ).
fof(f804,plain,
! [X2,X0,X1] :
( ~ in(X2,topstr_closure(sK10,X1))
| ~ element(X0,sF14)
| ~ closed_subset(X0,sK10)
| ~ subset(X1,X0)
| in(X2,X0)
| ~ element(X1,sF14)
| ~ in(X2,sF13) ),
inference(forward_demodulation,[],[f802,f226]) ).
fof(f841,plain,
( topstr_closure(sK10,sK11) = meet_of_subsets(sF13,sK9(sK10,sK11))
| ~ topological_space(sK10) ),
inference(resolution,[],[f605,f227]) ).
fof(f845,plain,
( ~ topological_space(sK10)
| sF12 = meet_of_subsets(sF13,sK9(sK10,sK11)) ),
inference(forward_demodulation,[],[f841,f218]) ).
fof(f899,plain,
! [X0,X1] :
( ~ in(X0,sF12)
| ~ element(X1,sF14)
| ~ closed_subset(X1,sK10)
| ~ subset(sK11,X1)
| in(X0,X1)
| ~ element(sK11,sF14)
| ~ in(X0,sF13) ),
inference(superposition,[],[f804,f218]) ).
fof(f900,plain,
! [X0,X1] :
( ~ in(X0,sF12)
| ~ element(X1,sF14)
| ~ closed_subset(X1,sK10)
| ~ subset(sK11,X1)
| in(X0,X1)
| ~ element(sK11,sF14) ),
inference(forward_subsumption_resolution,[],[f899,f590]) ).
fof(f901,plain,
! [X0,X1] :
( ~ closed_subset(X1,sK10)
| ~ element(X1,sF14)
| ~ in(X0,sF12)
| ~ subset(sK11,X1)
| in(X0,X1) ),
inference(forward_subsumption_resolution,[],[f900,f227]) ).
fof(f4077,plain,
! [X0] :
( ~ element(sK9(sK10,X0),powerset(powerset(the_carrier(sK10))))
| ~ topological_space(sK10)
| ~ top_str(sK10)
| closed_subset(meet_of_subsets(the_carrier(sK10),sK9(sK10,X0)),sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(sK9(sK10,X0),powerset(sF14))
| ~ topological_space(sK10) ),
inference(resolution,[],[f718,f623]) ).
fof(f4080,plain,
! [X0] :
( ~ element(sK9(sK10,X0),powerset(powerset(the_carrier(sK10))))
| ~ topological_space(sK10)
| ~ top_str(sK10)
| closed_subset(meet_of_subsets(the_carrier(sK10),sK9(sK10,X0)),sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(duplicate_literal_removal,[],[f4077]) ).
fof(f4082,plain,
! [X0] :
( ~ topological_space(sK10)
| ~ top_str(sK10)
| closed_subset(meet_of_subsets(the_carrier(sK10),sK9(sK10,X0)),sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(forward_subsumption_resolution,[],[f4080,f200]) ).
fof(f4084,plain,
! [X0] :
( ~ topological_space(sK10)
| closed_subset(meet_of_subsets(the_carrier(sK10),sK9(sK10,X0)),sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(forward_subsumption_resolution,[],[f4082,f203]) ).
fof(f4085,plain,
! [X0] :
( closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ topological_space(sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(forward_demodulation,[],[f4084,f224]) ).
fof(f4086,plain,
! [X0] :
( closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ topological_space(sK10)
| ~ element(X0,powerset(the_carrier(sK10)))
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(duplicate_literal_removal,[],[f4085]) ).
fof(f4087,plain,
! [X0] :
( ~ element(X0,powerset(sF13))
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ topological_space(sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(forward_demodulation,[],[f4086,f224]) ).
fof(f4088,plain,
! [X0] :
( ~ element(X0,sF14)
| closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ topological_space(sK10)
| ~ element(sK9(sK10,X0),powerset(sF14)) ),
inference(forward_demodulation,[],[f4087,f226]) ).
fof(f4089,plain,
! [X0] :
( closed_subset(meet_of_subsets(sF13,sK9(sK10,X0)),sK10)
| ~ element(X0,sF14)
| ~ topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f4088,f588]) ).
fof(f4883,plain,
! [X0] :
( ~ element(sK11,sF14)
| ~ in(X0,sF12)
| ~ subset(sK11,sK11)
| in(X0,sK11)
| sK11 = sF12 ),
inference(resolution,[],[f901,f222]) ).
fof(f4884,plain,
! [X0] :
( ~ element(sK11,sF14)
| ~ in(X0,sF12)
| ~ subset(sK11,sK11)
| in(X0,sK11)
| topological_space(sK10) ),
inference(resolution,[],[f901,f206]) ).
fof(f4885,plain,
! [X0] :
( ~ in(X0,sF12)
| ~ subset(sK11,sK11)
| in(X0,sK11)
| topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f4884,f227]) ).
fof(f4886,plain,
! [X0] :
( ~ in(X0,sF12)
| ~ subset(sK11,sK11)
| in(X0,sK11)
| sK11 = sF12 ),
inference(forward_subsumption_resolution,[],[f4883,f227]) ).
fof(f4895,plain,
! [X0] :
( ~ in(X0,sF12)
| in(X0,sK11)
| topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f4885,f183]) ).
fof(f4896,plain,
! [X0] :
( ~ in(X0,sF12)
| in(X0,sK11)
| sK11 = sF12 ),
inference(forward_subsumption_resolution,[],[f4886,f183]) ).
fof(f4923,plain,
! [X0] :
( in(sK0(sF12,X0),sK11)
| topological_space(sK10)
| subset(sF12,X0) ),
inference(resolution,[],[f4895,f157]) ).
fof(f5020,plain,
! [X0] :
( in(sK0(sF12,X0),sK11)
| sK11 = sF12
| subset(sF12,X0) ),
inference(resolution,[],[f4896,f157]) ).
fof(f5631,plain,
( topological_space(sK10)
| subset(sF12,sK11)
| subset(sF12,sK11) ),
inference(resolution,[],[f4923,f158]) ).
fof(f5635,plain,
( subset(sF12,sK11)
| topological_space(sK10) ),
inference(duplicate_literal_removal,[],[f5631]) ).
fof(f5637,plain,
( topological_space(sK10)
| sK11 = sF12 ),
inference(resolution,[],[f5635,f670]) ).
fof(f5660,plain,
topological_space(sK10),
inference(forward_subsumption_resolution,[],[f5637,f220]) ).
fof(f5667,plain,
sF12 = meet_of_subsets(sF13,sK9(sK10,sK11)),
inference(resolution,[],[f5660,f845]) ).
fof(f6017,plain,
( closed_subset(sF12,sK10)
| ~ element(sK11,sF14)
| ~ topological_space(sK10) ),
inference(superposition,[],[f4089,f5667]) ).
fof(f6065,plain,
( closed_subset(sF12,sK10)
| ~ topological_space(sK10) ),
inference(forward_subsumption_resolution,[],[f6017,f227]) ).
fof(f6066,plain,
closed_subset(sF12,sK10),
inference(forward_subsumption_resolution,[],[f6065,f5660]) ).
fof(f14894,plain,
( sK11 = sF12
| subset(sF12,sK11)
| subset(sF12,sK11) ),
inference(resolution,[],[f5020,f158]) ).
fof(f14898,plain,
( sK11 = sF12
| subset(sF12,sK11) ),
inference(duplicate_literal_removal,[],[f14894]) ).
fof(f14899,plain,
sK11 = sF12,
inference(forward_subsumption_resolution,[],[f14898,f670]) ).
fof(f14914,plain,
( sK11 != sK11
| ~ closed_subset(sK11,sK10) ),
inference(superposition,[],[f219,f14899]) ).
fof(f15016,plain,
closed_subset(sK11,sK10),
inference(superposition,[],[f6066,f14899]) ).
fof(f15065,plain,
~ closed_subset(sK11,sK10),
inference(trivial_inequality_removal,[],[f14914]) ).
fof(f15123,plain,
$false,
inference(forward_subsumption_resolution,[],[f15065,f15016]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU318+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 04:39:51 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.64/4.61 % (805872)Will run a generic schedule for satisfiability detection.
% 29.64/4.61 % (805877)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=811303093_2999 on theBenchmark for (2999ds/0Mi)
% 29.64/4.61 % (805878)% WARNING: option uhcvi not known.
% 29.64/4.61 % TRYING [1]
% 29.64/4.61 % TRYING [2]
% 29.64/4.61 % TRYING [3]
% 29.64/4.61 % (805878)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1177289795:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 29.64/4.61 % (805879)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1661468:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 29.64/4.61 % (805880)dis+10_1_sil=32000:sp=arity:random_seed=3889965461:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 29.64/4.61 % (805881)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3330800663:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 29.64/4.61 % TRYING [4]
% 29.64/4.61 % (805883)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3394643581:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 29.64/4.61 % (805882)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=180456340:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 29.64/4.61 % TRYING [5]
% 29.64/4.61 % TRYING [6]
% 29.64/4.61 % TRYING [7]
% 29.64/4.61 % (805880)Instruction limit reached!
% 29.64/4.61 % (805880)------------------------------
% 29.64/4.61 % (805880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.64/4.61 % (805880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.64/4.61 % (805880)CaDiCaL version: 2.1.3
% 29.64/4.61 % (805880)Termination reason: Instruction limit
% 29.64/4.61 % (805880)Termination phase: Saturation
% 29.64/4.61 % (805880)Time elapsed: 0.067 s
% 29.64/4.61 % (805880)Peak memory usage: 12 MB
% 29.64/4.61 % (805880)Instructions burned: 104 (million)
% 29.64/4.61 % (805881)Instruction limit reached!
% 29.64/4.61 % (805881)------------------------------
% 29.64/4.61 % (805881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.64/4.61 % (805881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.64/4.61 % (805881)CaDiCaL version: 2.1.3
% 29.64/4.61 % (805881)Termination reason: Instruction limit
% 29.64/4.61 % (805881)Termination phase: Saturation
% 29.64/4.61 % (805881)Time elapsed: 0.079 s
% 29.64/4.61 % (805881)Peak memory usage: 12 MB
% 29.64/4.61 % (805881)Instructions burned: 123 (million)
% 29.64/4.61 % TRYING [8]
% 29.64/4.61 % (805882)Instruction limit reached!
% 29.64/4.61 % (805882)------------------------------
% 29.64/4.61 % (805882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.64/4.61 % (805882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.64/4.61 % (805882)CaDiCaL version: 2.1.3
% 29.64/4.61 % (805882)Termination reason: Instruction limit
% 29.64/4.61 % (805882)Termination phase: Saturation
% 29.64/4.61 % (805882)Time elapsed: 0.087 s
% 29.64/4.61 % (805882)Peak memory usage: 13 MB
% 29.64/4.61 % (805882)Instructions burned: 131 (million)
% 29.64/4.61 % (805891)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2694236911:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 29.64/4.61 % TRYING [1]
% 29.64/4.61 % TRYING [2]
% 29.64/4.61 % TRYING [3]
% 29.64/4.61 % (805892)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2189056899:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 29.64/4.61 % TRYING [4]
% 29.64/4.61 % (805894)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=1714100402:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 29.64/4.61 % (805883)Instruction limit reached!
% 29.64/4.61 % (805883)------------------------------
% 29.64/4.61 % (805883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.64/4.61 % (805883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.64/4.61 % (805883)CaDiCaL version: 2.1.3
% 29.64/4.61 % (805883)Termination reason: Instruction limit
% 29.64/4.61 % (805883)Termination phase: Saturation
% 29.64/4.61 % (805883)Time elapsed: 0.108 s
% 29.64/4.61 % (805883)Peak memory usage: 14 MB
% 29.64/4.61 % (805883)Instructions burned: 160 (million)
% 29.64/4.61 % TRYING [5]
% 29.64/4.61 % (805897)ott-21_1_sil=16000:fs=off:random_seed=3904830196:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 29.64/4.61 % TRYING [6]
% 29.64/4.61 % (805892)Instruction limit reached!
% 29.64/4.61 % (805892)------------------------------
% 29.64/4.61 % (805892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805892)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805892)Termination reason: Instruction limit
% 12.82/5.84 % (805892)Termination phase: Saturation
% 12.82/5.84 % (805892)Time elapsed: 0.084 s
% 12.82/5.84 % (805892)Peak memory usage: 13 MB
% 12.82/5.84 % (805892)Instructions burned: 132 (million)
% 12.82/5.84 % (805899)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1098875464:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 12.82/5.84 % TRYING [9]
% 12.82/5.84 % TRYING [7]
% 12.82/5.84 % (805897)Instruction limit reached!
% 12.82/5.84 % (805897)------------------------------
% 12.82/5.84 % (805897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805897)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805897)Termination reason: Instruction limit
% 12.82/5.84 % (805897)Termination phase: Saturation
% 12.82/5.84 % (805897)Time elapsed: 0.094 s
% 12.82/5.84 % (805897)Peak memory usage: 13 MB
% 12.82/5.84 % (805897)Instructions burned: 180 (million)
% 12.82/5.84 % (805901)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3801747640:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 12.82/5.84 % TRYING [1]
% 12.82/5.84 % TRYING [2]
% 12.82/5.84 % TRYING [3]
% 12.82/5.84 % TRYING [4]
% 12.82/5.84 % TRYING [5]
% 12.82/5.84 % (805891)Instruction limit reached!
% 12.82/5.84 % (805891)------------------------------
% 12.82/5.84 % (805891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805891)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805891)Termination reason: Instruction limit
% 12.82/5.84 % (805891)Termination phase: Finite model building constraint generation
% 12.82/5.84 % (805891)Time elapsed: 0.311 s
% 12.82/5.84 % (805891)Peak memory usage: 27 MB
% 12.82/5.84 % (805891)Instructions burned: 716 (million)
% 12.82/5.84 % TRYING [6]
% 12.82/5.84 % (805903)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3858995793:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 12.82/5.84 % TRYING [7]
% 12.82/5.84 % (805899)Instruction limit reached!
% 12.82/5.84 % (805899)------------------------------
% 12.82/5.84 % (805899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805899)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805899)Termination reason: Instruction limit
% 12.82/5.84 % (805899)Termination phase: Saturation
% 12.82/5.84 % (805899)Time elapsed: 0.342 s
% 12.82/5.84 % (805899)Peak memory usage: 14 MB
% 12.82/5.84 % (805899)Instructions burned: 482 (million)
% 12.82/5.84 % (805894)Instruction limit reached!
% 12.82/5.84 % (805894)------------------------------
% 12.82/5.84 % (805894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805894)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805894)Termination reason: Instruction limit
% 12.82/5.84 % (805894)Termination phase: Saturation
% 12.82/5.84 % (805894)Time elapsed: 0.441 s
% 12.82/5.84 % (805894)Peak memory usage: 18 MB
% 12.82/5.84 % (805894)Instructions burned: 685 (million)
% 12.82/5.84 % (805905)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3151611026:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 12.82/5.84 % (805906)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=1770889760: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)
% 12.82/5.84 % (805901)Instruction limit reached!
% 12.82/5.84 % (805901)------------------------------
% 12.82/5.84 % (805901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805901)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805901)Termination reason: Instruction limit
% 12.82/5.84 % (805901)Termination phase: Finite model building constraint generation
% 12.82/5.84 % (805901)Time elapsed: 0.330 s
% 12.82/5.84 % (805901)Peak memory usage: 17 MB
% 12.82/5.84 % (805901)Instructions burned: 866 (million)
% 12.82/5.84 % (805909)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1845019040:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 12.82/5.84 % TRYING [14]
% 12.82/5.84 % TRYING [10]
% 12.82/5.84 % (805905)Instruction limit reached!
% 12.82/5.84 % (805905)------------------------------
% 12.82/5.84 % (805905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805905)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805905)Termination reason: Instruction limit
% 12.82/5.84 % (805905)Termination phase: Finite model building SAT solving
% 12.82/5.84 % (805905)Time elapsed: 0.393 s
% 12.82/5.84 % (805905)Peak memory usage: 59 MB
% 12.82/5.84 % (805905)Instructions burned: 891 (million)
% 12.82/5.84 % (805906)Instruction limit reached!
% 12.82/5.84 % (805906)------------------------------
% 12.82/5.84 % (805906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805906)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805906)Termination reason: Instruction limit
% 12.82/5.84 % (805906)Termination phase: Saturation
% 12.82/5.84 % (805906)Time elapsed: 0.398 s
% 12.82/5.84 % (805906)Peak memory usage: 23 MB
% 12.82/5.84 % (805906)Instructions burned: 694 (million)
% 12.82/5.84 % (805911)fmb+10_1_sil=64000:random_seed=3423153094:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 12.82/5.84 % (805912)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4070187415:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 12.82/5.84 % TRYING [1]
% 12.82/5.84 % TRYING [2]
% 12.82/5.84 % TRYING [20]
% 12.82/5.84 % TRYING [3]
% 12.82/5.84 % TRYING [4]
% 12.82/5.84 % TRYING [5]
% 12.82/5.84 % TRYING [6]
% 12.82/5.84 % (805909)Instruction limit reached!
% 12.82/5.84 % (805909)------------------------------
% 12.82/5.84 % (805909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805909)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805909)Termination reason: Instruction limit
% 12.82/5.84 % (805909)Termination phase: Saturation
% 12.82/5.84 % (805909)Time elapsed: 0.536 s
% 12.82/5.84 % (805909)Peak memory usage: 19 MB
% 12.82/5.84 % (805909)Instructions burned: 879 (million)
% 12.82/5.84 % TRYING [7]
% 12.82/5.84 % (805915)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2050018804:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 12.82/5.84 % TRYING [8]
% 12.82/5.84 % (805903)Instruction limit reached!
% 12.82/5.84 % (805903)------------------------------
% 12.82/5.84 % (805903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805903)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805903)Termination reason: Instruction limit
% 12.82/5.84 % (805903)Termination phase: Saturation
% 12.82/5.84 % (805903)Time elapsed: 0.751 s
% 12.82/5.84 % (805903)Peak memory usage: 24 MB
% 12.82/5.84 % (805903)Instructions burned: 1180 (million)
% 12.82/5.84 % (805917)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1199234009:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 12.82/5.84 % TRYING [8]
% 12.82/5.84 % TRYING [9]
% 12.82/5.84 % TRYING [9]
% 12.82/5.84 % (805915)Instruction limit reached!
% 12.82/5.84 % (805915)------------------------------
% 12.82/5.84 % (805915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805915)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805915)Termination reason: Instruction limit
% 12.82/5.84 % (805915)Termination phase: Finite model building SAT solving
% 12.82/5.84 % (805915)Time elapsed: 0.453 s
% 12.82/5.84 % (805915)Peak memory usage: 35 MB
% 12.82/5.84 % (805915)Instructions burned: 920 (million)
% 12.82/5.84 % (805919)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2185489303:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 12.82/5.84 % TRYING [10]
% 12.82/5.84 % (805919)Instruction limit reached!
% 12.82/5.84 % (805919)------------------------------
% 12.82/5.84 % (805919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805919)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805919)Termination reason: Instruction limit
% 12.82/5.84 % (805919)Termination phase: Saturation
% 12.82/5.84 % (805919)Time elapsed: 0.644 s
% 12.82/5.84 % (805919)Peak memory usage: 21 MB
% 12.82/5.84 % (805919)Instructions burned: 1475 (million)
% 12.82/5.84 % (805921)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3902226354:i=6324_2976 on theBenchmark for (2976ds/6324Mi)
% 12.82/5.84 % TRYING [77]
% 12.82/5.84 % TRYING [11]
% 12.82/5.84 % (805917)Instruction limit reached!
% 12.82/5.84 % (805917)------------------------------
% 12.82/5.84 % (805917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805917)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805917)Termination reason: Instruction limit
% 12.82/5.84 % (805917)Termination phase: Saturation
% 12.82/5.84 % (805917)Time elapsed: 2.953 s
% 12.82/5.84 % (805917)Peak memory usage: 25 MB
% 12.82/5.84 % (805917)Instructions burned: 5132 (million)
% 12.82/5.84 % (805923)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3355043069:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 12.82/5.84 % TRYING [16]
% 12.82/5.84 % (805921)Instruction limit reached!
% 12.82/5.84 % (805921)------------------------------
% 12.82/5.84 % (805921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805921)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805921)Termination reason: Instruction limit
% 12.82/5.84 % (805921)Termination phase: Finite model building constraint generation
% 12.82/5.84 % (805921)Time elapsed: 2.190 s
% 12.82/5.84 % (805921)Peak memory usage: 384 MB
% 12.82/5.84 % (805921)Instructions burned: 6326 (million)
% 12.82/5.84 % (805925)ott-2_1_sil=16000:newcnf=on:random_seed=1209405412:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 12.82/5.84 % (805923)Instruction limit reached!
% 12.82/5.84 % (805923)------------------------------
% 12.82/5.84 % (805923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805923)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805923)Termination reason: Instruction limit
% 12.82/5.84 % (805923)Termination phase: Finite model building constraint generation
% 12.82/5.84 % (805923)Time elapsed: 0.749 s
% 12.82/5.84 % (805923)Peak memory usage: 138 MB
% 12.82/5.84 % (805923)Instructions burned: 2174 (million)
% 12.82/5.84 % (805927)ott+10_1_sil=32000:tgt=ground:random_seed=2199705926:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 12.82/5.84 % (805925)Instruction limit reached!
% 12.82/5.84 % (805925)------------------------------
% 12.82/5.84 % (805925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805925)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805925)Termination reason: Instruction limit
% 12.82/5.84 % (805925)Termination phase: Saturation
% 12.82/5.84 % (805925)Time elapsed: 0.529 s
% 12.82/5.84 % (805925)Peak memory usage: 16 MB
% 12.82/5.84 % (805925)Instructions burned: 869 (million)
% 12.82/5.84 % (805929)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3727613908:i=54282_2948 on theBenchmark for (2948ds/54282Mi)
% 12.82/5.84 % TRYING [1]
% 12.82/5.84 % TRYING [2]
% 12.82/5.84 % TRYING [3]
% 12.82/5.84 % TRYING [4]
% 12.82/5.84 % TRYING [5]
% 12.82/5.84 % TRYING [6]
% 12.82/5.84 % TRYING [7]
% 12.82/5.84 % TRYING [8]
% 12.82/5.84 % (805927) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-805872-805927"...
% 12.82/5.84 % (805927)...printing done.
% 12.82/5.84 % (805927)Refutation found. Thanks to Tanya!
% 12.82/5.84 % SZS status Theorem for theBenchmark
% 12.82/5.84 % SZS output start Proof for theBenchmark
% See solution above
% 12.82/5.84 % (805927)------------------------------
% 12.82/5.84 % (805927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/5.84 % (805927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/5.84 % (805927)CaDiCaL version: 2.1.3
% 12.82/5.84 % (805927)Termination reason: Refutation
% 12.82/5.84 % (805927)Time elapsed: 0.370 s
% 12.82/5.84 % (805927)Peak memory usage: 17 MB
% 12.82/5.84 % (805927)Instructions burned: 623 (million)
% 12.82/5.84 % (805872)Success in time 5.416 s
% 12.82/5.84 % Vampire exiting
%------------------------------------------------------------------------------