%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:50 PM UTC 2026
% Result : Theorem 0.16s 0.52s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 13
% Syntax : Number of formulae : 181 ( 11 unt; 11 def)
% Number of atoms : 952 ( 119 equ)
% Maximal formula atoms : 21 ( 5 avg)
% Number of connectives : 1207 ( 436 ~; 578 |; 167 &)
% ( 16 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 10 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-3 aty)
% Number of variables : 198 ( 0 sgn 130 !; 68 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_xboole_0__e1_40__pre_topc__1) ).
fof(f2,negated_conjecture,
~ ! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f30,axiom,
! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) )
=> ( ! [X2,X3,X4] :
( ( X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& ? [X6] :
( element(X6,powerset(the_carrier(X0)))
& X6 = X4
& closed_subset(X6,X0)
& subset(X1,X4) ) )
=> X3 = X4 )
=> ? [X2] :
! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X4,powerset(the_carrier(X0)))
& X4 = X3
& ? [X7] :
( element(X7,powerset(the_carrier(X0)))
& X7 = X3
& closed_subset(X7,X0)
& subset(X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_tarski__e1_40__pre_topc__1) ).
fof(f32,plain,
! [X0,X1] :
( ( topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) )
=> ( ! [X2,X3,X4] :
( ( X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& ? [X6] :
( element(X6,powerset(the_carrier(X0)))
& X6 = X4
& closed_subset(X6,X0)
& subset(X1,X4) ) )
=> X3 = X4 )
=> ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(the_carrier(X0)))
& X8 = X9
& ? [X10] :
( element(X10,powerset(the_carrier(X0)))
& X8 = X10
& closed_subset(X10,X0)
& subset(X1,X8) ) ) ) ) ),
inference(rectify,[],[f30]) ).
fof(f49,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f2]) ).
fof(f50,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( in(X3,X2)
<~> ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) ),
inference(flattening,[],[f49]) ).
fof(f65,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(the_carrier(X0)))
& X8 = X9
& ? [X10] :
( element(X10,powerset(the_carrier(X0)))
& X8 = X10
& closed_subset(X10,X0)
& subset(X1,X8) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& ? [X6] :
( element(X6,powerset(the_carrier(X0)))
& X6 = X4
& closed_subset(X6,X0)
& subset(X1,X4) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(ennf_transformation,[],[f32]) ).
fof(f66,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(the_carrier(X0)))
& X8 = X9
& ? [X10] :
( element(X10,powerset(the_carrier(X0)))
& X8 = X10
& closed_subset(X10,X0)
& subset(X1,X8) ) ) )
| ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& ? [X6] :
( element(X6,powerset(the_carrier(X0)))
& X6 = X4
& closed_subset(X6,X0)
& subset(X1,X4) ) )
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(flattening,[],[f65]) ).
fof(f67,definition,
! [X0,X4,X1] :
( ? [X6] :
( element(X6,powerset(the_carrier(X0)))
& X6 = X4
& closed_subset(X6,X0)
& subset(X1,X4) )
| ~ sP0(X0,X4,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f68,definition,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& sP0(X0,X4,X1) )
| ~ sP1(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f69,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( in(X8,X7)
<=> ? [X9] :
( in(X9,powerset(the_carrier(X0)))
& X8 = X9
& ? [X10] :
( element(X10,powerset(the_carrier(X0)))
& X8 = X10
& closed_subset(X10,X0)
& subset(X1,X8) ) ) )
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(definition_folding,[],[f66,f68,f67]) ).
fof(f70,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(the_carrier(X0)))
| ! [X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| X3 != X4
| ~ closed_subset(X4,X0)
| ~ subset(X1,X3) )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) )
| in(X3,X2) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) ),
inference(nnf_transformation,[],[f50]) ).
fof(f71,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(the_carrier(X0)))
| ! [X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| X3 != X4
| ~ closed_subset(X4,X0)
| ~ subset(X1,X3) )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(the_carrier(X0)))
& ? [X4] :
( element(X4,powerset(the_carrier(X0)))
& X4 = X3
& closed_subset(X4,X0)
& subset(X1,X3) ) )
| in(X3,X2) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) ),
inference(flattening,[],[f70]) ).
fof(f72,plain,
? [X0,X1] :
( ! [X2] :
? [X3] :
( ( ~ in(X3,powerset(the_carrier(X0)))
| ! [X4] :
( ~ element(X4,powerset(the_carrier(X0)))
| X3 != X4
| ~ closed_subset(X4,X0)
| ~ subset(X1,X3) )
| ~ in(X3,X2) )
& ( ( in(X3,powerset(the_carrier(X0)))
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X3 = X5
& closed_subset(X5,X0)
& subset(X1,X3) ) )
| in(X3,X2) ) )
& topological_space(X0)
& top_str(X0)
& element(X1,powerset(the_carrier(X0))) ),
inference(rectify,[],[f71]) ).
fof(f73,plain,
( ! [X2] :
( ( ~ in(sK4(X2),powerset(the_carrier(sK2)))
| ! [X4] :
( ~ element(X4,powerset(the_carrier(sK2)))
| sK4(X2) != X4
| ~ closed_subset(X4,sK2)
| ~ subset(sK3,sK4(X2)) )
| ~ in(sK4(X2),X2) )
& ( ( in(sK4(X2),powerset(the_carrier(sK2)))
& element(sK5(X2),powerset(the_carrier(sK2)))
& sK4(X2) = sK5(X2)
& closed_subset(sK5(X2),sK2)
& subset(sK3,sK4(X2)) )
| in(sK4(X2),X2) ) )
& topological_space(sK2)
& top_str(sK2)
& element(sK3,powerset(the_carrier(sK2))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X3,sK4(X2)),skolemize(X5,sK5(X2))],[f72]) ).
fof(f78,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& X2 = X3
& ? [X5] :
( element(X5,powerset(the_carrier(X0)))
& X5 = X3
& closed_subset(X5,X0)
& subset(X1,X3) )
& X2 = X4
& sP0(X0,X4,X1) )
| ~ sP1(X0,X1) ),
inference(nnf_transformation,[],[f68]) ).
fof(f79,plain,
! [X0,X1] :
( ( sK11(X0,X1) != sK12(X0,X1)
& sK10(X0,X1) = sK11(X0,X1)
& element(sK13(X0,X1),powerset(the_carrier(X0)))
& sK11(X0,X1) = sK13(X0,X1)
& closed_subset(sK13(X0,X1),X0)
& subset(X1,sK11(X0,X1))
& sK10(X0,X1) = sK12(X0,X1)
& sP0(X0,sK12(X0,X1),X1) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13]),skolemize(X2,sK10(X0,X1)),skolemize(X3,sK11(X0,X1)),skolemize(X4,sK12(X0,X1)),skolemize(X5,sK13(X0,X1))],[f78]) ).
fof(f83,plain,
! [X0,X1] :
( ? [X7] :
! [X8] :
( ( in(X8,X7)
| ! [X9] :
( ~ in(X9,powerset(the_carrier(X0)))
| X8 != X9
| ! [X10] :
( ~ element(X10,powerset(the_carrier(X0)))
| X8 != X10
| ~ closed_subset(X10,X0)
| ~ subset(X1,X8) ) ) )
& ( ? [X9] :
( in(X9,powerset(the_carrier(X0)))
& X8 = X9
& ? [X10] :
( element(X10,powerset(the_carrier(X0)))
& X8 = X10
& closed_subset(X10,X0)
& subset(X1,X8) ) )
| ~ in(X8,X7) ) )
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(nnf_transformation,[],[f69]) ).
fof(f84,plain,
! [X0,X1] :
( ? [X2] :
! [X3] :
( ( in(X3,X2)
| ! [X4] :
( ~ in(X4,powerset(the_carrier(X0)))
| X3 != X4
| ! [X5] :
( ~ element(X5,powerset(the_carrier(X0)))
| X3 != X5
| ~ closed_subset(X5,X0)
| ~ subset(X1,X3) ) ) )
& ( ? [X6] :
( in(X6,powerset(the_carrier(X0)))
& X3 = X6
& ? [X7] :
( element(X7,powerset(the_carrier(X0)))
& X3 = X7
& closed_subset(X7,X0)
& subset(X1,X3) ) )
| ~ in(X3,X2) ) )
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(rectify,[],[f83]) ).
fof(f85,plain,
! [X0,X1] :
( ! [X3] :
( ( in(X3,sK15(X0,X1))
| ! [X4] :
( ~ in(X4,powerset(the_carrier(X0)))
| X3 != X4
| ! [X5] :
( ~ element(X5,powerset(the_carrier(X0)))
| X3 != X5
| ~ closed_subset(X5,X0)
| ~ subset(X1,X3) ) ) )
& ( ( in(sK16(X0,X1,X3),powerset(the_carrier(X0)))
& sK16(X0,X1,X3) = X3
& element(sK17(X0,X1,X3),powerset(the_carrier(X0)))
& sK17(X0,X1,X3) = X3
& closed_subset(sK17(X0,X1,X3),X0)
& subset(X1,X3) )
| ~ in(X3,sK15(X0,X1)) ) )
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16,sK17]),skolemize(X2,sK15(X0,X1)),skolemize(X6,sK16(X0,X1,X3)),skolemize(X7,sK17(X0,X1,X3))],[f84]) ).
fof(f86,plain,
element(sK3,powerset(the_carrier(sK2))),
inference(cnf_transformation,[],[f73]) ).
fof(f87,plain,
top_str(sK2),
inference(cnf_transformation,[],[f73]) ).
fof(f88,plain,
topological_space(sK2),
inference(cnf_transformation,[],[f73]) ).
fof(f89,plain,
! [X2] :
( subset(sK3,sK4(X2))
| in(sK4(X2),X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f90,plain,
! [X2] :
( closed_subset(sK5(X2),sK2)
| in(sK4(X2),X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f91,plain,
! [X2] :
( in(sK4(X2),X2)
| sK4(X2) = sK5(X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f92,plain,
! [X2] :
( element(sK5(X2),powerset(the_carrier(sK2)))
| in(sK4(X2),X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f93,plain,
! [X2] :
( in(sK4(X2),powerset(the_carrier(sK2)))
| in(sK4(X2),X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f94,plain,
! [X2,X4] :
( ~ in(sK4(X2),powerset(the_carrier(sK2)))
| ~ element(X4,powerset(the_carrier(sK2)))
| sK4(X2) != X4
| ~ closed_subset(X4,sK2)
| ~ subset(sK3,sK4(X2))
| ~ in(sK4(X2),X2) ),
inference(cnf_transformation,[],[f73]) ).
fof(f135,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK10(X0,X1) = sK12(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f140,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| sK10(X0,X1) = sK11(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f141,plain,
! [X0,X1] :
( sK11(X0,X1) != sK12(X0,X1)
| ~ sP1(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f146,plain,
! [X3,X0,X1] :
( ~ in(X3,sK15(X0,X1))
| subset(X1,X3)
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f147,plain,
! [X3,X0,X1] :
( closed_subset(sK17(X0,X1,X3),X0)
| ~ in(X3,sK15(X0,X1))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f148,plain,
! [X3,X0,X1] :
( ~ in(X3,sK15(X0,X1))
| sK17(X0,X1,X3) = X3
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f149,plain,
! [X3,X0,X1] :
( element(sK17(X0,X1,X3),powerset(the_carrier(X0)))
| ~ in(X3,sK15(X0,X1))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f150,plain,
! [X3,X0,X1] :
( ~ in(X3,sK15(X0,X1))
| sK16(X0,X1,X3) = X3
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f151,plain,
! [X3,X0,X1] :
( in(sK16(X0,X1,X3),powerset(the_carrier(X0)))
| ~ in(X3,sK15(X0,X1))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f152,plain,
! [X3,X0,X1,X4,X5] :
( in(X3,sK15(X0,X1))
| ~ in(X4,powerset(the_carrier(X0)))
| X3 != X4
| ~ element(X5,powerset(the_carrier(X0)))
| X3 != X5
| ~ closed_subset(X5,X0)
| ~ subset(X1,X3)
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
! [X2] :
( ~ in(sK4(X2),powerset(the_carrier(sK2)))
| ~ element(sK4(X2),powerset(the_carrier(sK2)))
| ~ closed_subset(sK4(X2),sK2)
| ~ subset(sK3,sK4(X2))
| ~ in(sK4(X2),X2) ),
inference(equality_resolution,[],[f94]) ).
fof(f154,plain,
! [X0,X1,X4,X5] :
( in(X4,sK15(X0,X1))
| ~ in(X4,powerset(the_carrier(X0)))
| ~ element(X5,powerset(the_carrier(X0)))
| X4 != X5
| ~ closed_subset(X5,X0)
| ~ subset(X1,X4)
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(equality_resolution,[],[f152]) ).
fof(f155,plain,
! [X0,X1,X5] :
( ~ in(X5,powerset(the_carrier(X0)))
| in(X5,sK15(X0,X1))
| ~ element(X5,powerset(the_carrier(X0)))
| ~ closed_subset(X5,X0)
| ~ subset(X1,X5)
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0))) ),
inference(equality_resolution,[],[f154]) ).
fof(f401,plain,
! [X0,X1] :
( subset(sK3,sK4(sK15(X1,X0)))
| subset(X0,sK4(sK15(X1,X0)))
| ~ topological_space(X1)
| ~ top_str(X1)
| ~ element(X0,powerset(the_carrier(X1)))
| sP1(X1,X0) ),
inference(resolution,[],[f146,f89]) ).
fof(f402,plain,
! [X0] :
( subset(sK3,sK4(sK15(X0,sK3)))
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(sK3,powerset(the_carrier(X0)))
| sP1(X0,sK3) ),
inference(factoring,[],[f401]) ).
fof(f404,plain,
! [X0,X1] :
( element(sK5(sK15(X0,X1)),powerset(the_carrier(sK2)))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| sK4(sK15(X0,X1)) = sK17(X0,X1,sK4(sK15(X0,X1))) ),
inference(resolution,[],[f148,f92]) ).
fof(f405,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| sK4(sK15(X0,X1)) = sK17(X0,X1,sK4(sK15(X0,X1)))
| sK4(sK15(X0,X1)) = sK5(sK15(X0,X1)) ),
inference(resolution,[],[f148,f91]) ).
fof(f406,plain,
! [X0,X1] :
( closed_subset(sK5(sK15(X0,X1)),sK2)
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| ~ element(X1,powerset(the_carrier(X0)))
| sK4(sK15(X0,X1)) = sK17(X0,X1,sK4(sK15(X0,X1))) ),
inference(resolution,[],[f148,f90]) ).
fof(f410,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| sP1(X0,X1)
| ~ topological_space(X0)
| ~ top_str(X0)
| sK4(sK15(X0,X1)) = sK16(X0,X1,sK4(sK15(X0,X1)))
| sK4(sK15(X0,X1)) = sK5(sK15(X0,X1)) ),
inference(resolution,[],[f150,f91]) ).
fof(f446,plain,
! [X0,X1] :
( in(sK4(X0),sK15(sK2,X1))
| ~ element(sK4(X0),powerset(the_carrier(sK2)))
| ~ closed_subset(sK4(X0),sK2)
| ~ subset(X1,sK4(X0))
| sP1(sK2,X1)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| in(sK4(X0),X0) ),
inference(resolution,[],[f155,f93]) ).
fof(f458,plain,
! [X0,X1] :
( in(sK4(X0),sK15(sK2,X1))
| ~ element(sK4(X0),powerset(the_carrier(sK2)))
| ~ closed_subset(sK4(X0),sK2)
| ~ subset(X1,sK4(X0))
| sP1(sK2,X1)
| ~ top_str(sK2)
| ~ element(X1,powerset(the_carrier(sK2)))
| in(sK4(X0),X0) ),
inference(forward_subsumption_resolution,[],[f446,f88]) ).
fof(f461,plain,
! [X0,X1] :
( ~ element(sK4(X0),powerset(the_carrier(sK2)))
| in(sK4(X0),sK15(sK2,X1))
| ~ closed_subset(sK4(X0),sK2)
| ~ subset(X1,sK4(X0))
| sP1(sK2,X1)
| ~ element(X1,powerset(the_carrier(sK2)))
| in(sK4(X0),X0) ),
inference(forward_subsumption_resolution,[],[f458,f87]) ).
fof(f508,plain,
( sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(resolution,[],[f405,f86]) ).
fof(f525,plain,
( sP1(sK2,sK3)
| ~ top_str(sK2)
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[],[f508,f88]) ).
fof(f530,plain,
( sP1(sK2,sK3)
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[],[f525,f87]) ).
fof(f532,definition,
( spl18_23
<=> sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl18_23])],[avatar_definition]) ).
fof(f534,plain,
( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3))
| ~ spl18_23 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f536,definition,
( spl18_24
<=> sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3))) ),
introduced(definition,[new_symbols(definition,[spl18_24])],[avatar_definition]) ).
fof(f538,plain,
( sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_24 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f540,definition,
( spl18_25
<=> sP1(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl18_25])],[avatar_definition]) ).
fof(f541,plain,
( ~ sP1(sK2,sK3)
| spl18_25 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( sP1(sK2,sK3)
| ~ spl18_25 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f543,plain,
( spl18_23
| spl18_24
| spl18_25 ),
inference(avatar_split_clause,[],[f530,f540,f536,f532]) ).
fof(f562,definition,
( spl18_26
<=> closed_subset(sK4(sK15(sK2,sK3)),sK2) ),
introduced(definition,[new_symbols(definition,[spl18_26])],[avatar_definition]) ).
fof(f564,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ spl18_26 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f567,definition,
( spl18_27
<=> sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3))) ),
introduced(definition,[new_symbols(definition,[spl18_27])],[avatar_definition]) ).
fof(f569,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_27 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f572,definition,
( spl18_28
<=> element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2))) ),
introduced(definition,[new_symbols(definition,[spl18_28])],[avatar_definition]) ).
fof(f574,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ spl18_28 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f577,plain,
( sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(resolution,[],[f410,f86]) ).
fof(f594,plain,
( sP1(sK2,sK3)
| ~ top_str(sK2)
| sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[],[f577,f88]) ).
fof(f599,plain,
( sP1(sK2,sK3)
| sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3)) ),
inference(forward_subsumption_resolution,[],[f594,f87]) ).
fof(f600,plain,
( spl18_23
| spl18_27
| spl18_25 ),
inference(avatar_split_clause,[],[f599,f540,f567,f532]) ).
fof(f603,plain,
( sK10(sK2,sK3) = sK12(sK2,sK3)
| ~ spl18_25 ),
inference(resolution,[],[f542,f135]) ).
fof(f607,plain,
( sK10(sK2,sK3) != sK11(sK2,sK3)
| ~ sP1(sK2,sK3)
| ~ spl18_25 ),
inference(superposition,[],[f141,f603]) ).
fof(f610,plain,
( ~ sP1(sK2,sK3)
| ~ spl18_25 ),
inference(forward_subsumption_resolution,[],[f607,f140]) ).
fof(f611,plain,
( $false
| ~ spl18_25 ),
inference(forward_subsumption_resolution,[],[f610,f542]) ).
fof(f612,plain,
~ spl18_25,
inference(avatar_contradiction_clause,[],[f611]) ).
fof(f613,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24 ),
inference(superposition,[],[f149,f538]) ).
fof(f614,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24 ),
inference(superposition,[],[f147,f538]) ).
fof(f615,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f614,f541]) ).
fof(f616,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f613,f541]) ).
fof(f617,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f615,f88]) ).
fof(f618,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f616,f88]) ).
fof(f619,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f617,f87]) ).
fof(f620,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f618,f87]) ).
fof(f621,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f619,f86]) ).
fof(f622,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ spl18_24
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f620,f86]) ).
fof(f624,definition,
( spl18_29
<=> in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl18_29])],[avatar_definition]) ).
fof(f625,plain,
( in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| ~ spl18_29 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f626,plain,
( ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| spl18_29 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f627,plain,
( ~ spl18_29
| spl18_26
| ~ spl18_24
| spl18_25 ),
inference(avatar_split_clause,[],[f621,f540,f536,f562,f624]) ).
fof(f628,plain,
( ~ spl18_29
| spl18_28
| ~ spl18_24
| spl18_25 ),
inference(avatar_split_clause,[],[f622,f540,f536,f572,f624]) ).
fof(f630,plain,
( element(sK5(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| spl18_29 ),
inference(resolution,[],[f626,f92]) ).
fof(f632,plain,
( closed_subset(sK5(sK15(sK2,sK3)),sK2)
| spl18_29 ),
inference(resolution,[],[f626,f90]) ).
fof(f633,plain,
( subset(sK3,sK4(sK15(sK2,sK3)))
| spl18_29 ),
inference(resolution,[],[f626,f89]) ).
fof(f660,definition,
( spl18_30
<=> ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ element(X0,powerset(the_carrier(sK2)))
| sP1(sK2,X0)
| ~ subset(X0,sK4(sK15(sK2,sK3))) ) ),
introduced(definition,[new_symbols(definition,[spl18_30])],[avatar_definition]) ).
fof(f661,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ element(X0,powerset(the_carrier(sK2)))
| sP1(sK2,X0)
| ~ subset(X0,sK4(sK15(sK2,sK3))) )
| ~ spl18_30 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f684,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_29 ),
inference(resolution,[],[f625,f150]) ).
fof(f688,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f684,f541]) ).
fof(f689,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f688,f88]) ).
fof(f690,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f689,f87]) ).
fof(f691,plain,
( sK4(sK15(sK2,sK3)) = sK16(sK2,sK3,sK4(sK15(sK2,sK3)))
| spl18_25
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f690,f86]) ).
fof(f692,plain,
( spl18_27
| spl18_25
| ~ spl18_29 ),
inference(avatar_split_clause,[],[f691,f624,f540,f567]) ).
fof(f693,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_27 ),
inference(superposition,[],[f151,f569]) ).
fof(f694,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| ~ spl18_27 ),
inference(forward_subsumption_resolution,[],[f693,f93]) ).
fof(f695,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_27 ),
inference(forward_subsumption_resolution,[],[f694,f541]) ).
fof(f696,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_27 ),
inference(forward_subsumption_resolution,[],[f695,f88]) ).
fof(f697,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ element(sK3,powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_27 ),
inference(forward_subsumption_resolution,[],[f696,f87]) ).
fof(f698,plain,
( in(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| spl18_25
| ~ spl18_27 ),
inference(forward_subsumption_resolution,[],[f697,f86]) ).
fof(f699,plain,
( ~ element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| spl18_25
| ~ spl18_27 ),
inference(resolution,[],[f698,f153]) ).
fof(f700,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(X0,powerset(the_carrier(sK2))) )
| spl18_25
| ~ spl18_27 ),
inference(resolution,[],[f698,f155]) ).
fof(f703,plain,
( ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| spl18_25
| ~ spl18_27
| ~ spl18_28 ),
inference(forward_subsumption_resolution,[],[f699,f574]) ).
fof(f705,plain,
( ~ subset(sK3,sK4(sK15(sK2,sK3)))
| ~ in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3))
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28 ),
inference(forward_subsumption_resolution,[],[f703,f564]) ).
fof(f707,plain,
( ~ subset(sK3,sK4(sK15(sK2,sK3)))
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f705,f625]) ).
fof(f710,plain,
( ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(resolution,[],[f707,f402]) ).
fof(f717,plain,
( ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f710,f88]) ).
fof(f720,plain,
( ~ element(sK3,powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f717,f87]) ).
fof(f723,plain,
( sP1(sK2,sK3)
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f720,f86]) ).
fof(f726,plain,
( $false
| spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(forward_subsumption_resolution,[],[f723,f541]) ).
fof(f727,plain,
( spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(avatar_contradiction_clause,[],[f726]) ).
fof(f731,definition,
( spl18_35
<=> subset(sK3,sK4(sK15(sK2,sK3))) ),
introduced(definition,[new_symbols(definition,[spl18_35])],[avatar_definition]) ).
fof(f732,plain,
( subset(sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_35 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f735,plain,
( spl18_35
| spl18_29 ),
inference(avatar_split_clause,[],[f633,f624,f731]) ).
fof(f738,plain,
( sK4(sK15(sK2,sK3)) = sK5(sK15(sK2,sK3))
| spl18_29 ),
inference(resolution,[],[f626,f91]) ).
fof(f741,plain,
( spl18_23
| spl18_29 ),
inference(avatar_split_clause,[],[f738,f624,f532]) ).
fof(f787,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ spl18_23
| spl18_29 ),
inference(superposition,[],[f630,f534]) ).
fof(f788,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ spl18_23
| spl18_29 ),
inference(superposition,[],[f632,f534]) ).
fof(f790,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23 ),
inference(superposition,[],[f404,f534]) ).
fof(f792,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| sP1(sK2,sK3)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23 ),
inference(superposition,[],[f406,f534]) ).
fof(f1008,plain,
( spl18_28
| ~ spl18_23
| spl18_29 ),
inference(avatar_split_clause,[],[f787,f624,f532,f572]) ).
fof(f1024,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f790,f541]) ).
fof(f1025,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1024,f88]) ).
fof(f1026,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1025,f87]) ).
fof(f1027,plain,
( element(sK4(sK15(sK2,sK3)),powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1026,f86]) ).
fof(f1028,plain,
( spl18_24
| spl18_28
| ~ spl18_23
| spl18_25 ),
inference(avatar_split_clause,[],[f1027,f540,f532,f572,f536]) ).
fof(f1030,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ element(X0,powerset(the_carrier(sK2)))
| in(sK4(sK15(sK2,sK3)),sK15(sK2,sK3)) )
| ~ spl18_28 ),
inference(resolution,[],[f574,f461]) ).
fof(f1093,plain,
( ~ element(sK3,powerset(the_carrier(sK2)))
| sP1(sK2,sK3)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| spl18_29
| ~ spl18_30 ),
inference(resolution,[],[f661,f626]) ).
fof(f1103,plain,
( sP1(sK2,sK3)
| ~ subset(sK3,sK4(sK15(sK2,sK3)))
| spl18_29
| ~ spl18_30 ),
inference(forward_subsumption_resolution,[],[f1093,f86]) ).
fof(f1106,plain,
( ~ subset(sK3,sK4(sK15(sK2,sK3)))
| spl18_25
| spl18_29
| ~ spl18_30 ),
inference(forward_subsumption_resolution,[],[f1103,f541]) ).
fof(f1107,plain,
( $false
| spl18_25
| spl18_29
| ~ spl18_30
| ~ spl18_35 ),
inference(forward_subsumption_resolution,[],[f1106,f732]) ).
fof(f1108,plain,
( spl18_25
| spl18_29
| ~ spl18_30
| ~ spl18_35 ),
inference(avatar_contradiction_clause,[],[f1107]) ).
fof(f1109,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f792,f541]) ).
fof(f1110,plain,
( spl18_26
| ~ spl18_23
| spl18_29 ),
inference(avatar_split_clause,[],[f788,f624,f532,f562]) ).
fof(f1111,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ topological_space(sK2)
| ~ top_str(sK2)
| ~ element(X0,powerset(the_carrier(sK2))) )
| spl18_25
| ~ spl18_27
| ~ spl18_28 ),
inference(forward_subsumption_resolution,[],[f700,f574]) ).
fof(f1112,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ element(X0,powerset(the_carrier(sK2))) )
| ~ spl18_28
| spl18_29 ),
inference(forward_subsumption_resolution,[],[f1030,f626]) ).
fof(f1113,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ top_str(sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1109,f88]) ).
fof(f1114,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ top_str(sK2)
| ~ element(X0,powerset(the_carrier(sK2))) )
| spl18_25
| ~ spl18_27
| ~ spl18_28 ),
inference(forward_subsumption_resolution,[],[f1111,f88]) ).
fof(f1115,plain,
( ~ spl18_26
| spl18_30
| ~ spl18_28
| spl18_29 ),
inference(avatar_split_clause,[],[f1112,f624,f572,f660,f562]) ).
fof(f1116,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ element(sK3,powerset(the_carrier(sK2)))
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1113,f87]) ).
fof(f1117,plain,
( ! [X0] :
( in(sK4(sK15(sK2,sK3)),sK15(sK2,X0))
| ~ closed_subset(sK4(sK15(sK2,sK3)),sK2)
| ~ subset(X0,sK4(sK15(sK2,sK3)))
| sP1(sK2,X0)
| ~ element(X0,powerset(the_carrier(sK2))) )
| spl18_25
| ~ spl18_27
| ~ spl18_28 ),
inference(forward_subsumption_resolution,[],[f1114,f87]) ).
fof(f1118,plain,
( closed_subset(sK4(sK15(sK2,sK3)),sK2)
| sK4(sK15(sK2,sK3)) = sK17(sK2,sK3,sK4(sK15(sK2,sK3)))
| ~ spl18_23
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f1116,f86]) ).
fof(f1119,plain,
( ~ spl18_26
| spl18_30
| spl18_25
| ~ spl18_27
| ~ spl18_28 ),
inference(avatar_split_clause,[],[f1117,f572,f567,f540,f660,f562]) ).
fof(f1120,plain,
( spl18_24
| spl18_26
| ~ spl18_23
| spl18_25 ),
inference(avatar_split_clause,[],[f1118,f540,f532,f562,f536]) ).
cnf(s16,plain,
( spl18_23
| spl18_24
| spl18_25 ),
inference(sat_conversion,[],[f543]) ).
cnf(s21,plain,
( spl18_23
| spl18_25
| spl18_27 ),
inference(sat_conversion,[],[f600]) ).
cnf(s22,plain,
~ spl18_25,
inference(sat_conversion,[],[f612]) ).
cnf(s23,plain,
( ~ spl18_24
| spl18_25
| spl18_26
| ~ spl18_29 ),
inference(sat_conversion,[],[f627]) ).
cnf(s24,plain,
( ~ spl18_24
| spl18_25
| spl18_28
| ~ spl18_29 ),
inference(sat_conversion,[],[f628]) ).
cnf(s29,plain,
( spl18_25
| spl18_27
| ~ spl18_29 ),
inference(sat_conversion,[],[f692]) ).
cnf(s31,plain,
( spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| ~ spl18_29 ),
inference(sat_conversion,[],[f727]) ).
cnf(s34,plain,
( spl18_29
| spl18_35 ),
inference(sat_conversion,[],[f735]) ).
cnf(s35,plain,
( spl18_23
| spl18_29 ),
inference(sat_conversion,[],[f741]) ).
cnf(s73,plain,
( ~ spl18_23
| spl18_28
| spl18_29 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s79,plain,
( ~ spl18_23
| spl18_24
| spl18_25
| spl18_28 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s86,plain,
( spl18_25
| spl18_29
| ~ spl18_30
| ~ spl18_35 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s87,plain,
( ~ spl18_23
| spl18_26
| spl18_29 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s88,plain,
( ~ spl18_26
| ~ spl18_28
| spl18_29
| spl18_30 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s89,plain,
( spl18_25
| ~ spl18_26
| ~ spl18_27
| ~ spl18_28
| spl18_30 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s90,plain,
( ~ spl18_23
| spl18_24
| spl18_25
| spl18_26 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s93,plain,
( spl18_23
| spl18_27 ),
inference(rat,[],[s21,s22]) ).
cnf(s98,plain,
( spl18_23
| spl18_24 ),
inference(rat,[],[s16,s22]) ).
cnf(s99,plain,
spl18_23,
inference(rat,[],[s31,s23,s24,s98,s93,s35,s22]) ).
cnf(s101,plain,
( spl18_29
| ~ spl18_30 ),
inference(rat,[],[s34,s86,s22]) ).
cnf(s102,plain,
( ~ spl18_28
| ~ spl18_27
| ~ spl18_26 ),
inference(rat,[],[s101,s31,s89,s22]) ).
cnf(s103,plain,
( spl18_28
| ~ spl18_24 ),
inference(rat,[],[s24,s73,s22,s99]) ).
cnf(s104,plain,
( ~ spl18_28
| ~ spl18_26 ),
inference(rat,[],[s88,s101,s29,s102,s22]) ).
cnf(s105,plain,
~ spl18_24,
inference(rat,[],[s23,s87,s104,s103,s22,s99]) ).
cnf(s106,plain,
spl18_26,
inference(rat,[],[s90,s99,s22,s105]) ).
cnf(s107,plain,
spl18_28,
inference(rat,[],[s79,s99,s22,s105]) ).
cnf(s108,plain,
$false,
inference(rat,[],[s104,s106,s107]) ).
fof(f1121,plain,
$false,
inference(avatar_sat_refutation,[],[s108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 % Computer : n001.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Mon Sep 28 04:45:03 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 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
% 0.16/0.52 % (22004)Will run a generic schedule for satisfiability detection.
% 0.16/0.52 % (22009)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1272567303_2999 on theBenchmark for (2999ds/0Mi)
% 0.16/0.52 % TRYING [1]
% 0.16/0.52 % TRYING [2]
% 0.16/0.52 % TRYING [3]
% 0.16/0.52 % (22010)% WARNING: option uhcvi not known.
% 0.16/0.52 % TRYING [4]
% 0.16/0.52 % (22010)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1547455526:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.16/0.52 % (22011)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1557723393:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.16/0.52 % (22012)dis+10_1_sil=32000:sp=arity:random_seed=874577657:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.16/0.52 % (22013)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3075121878:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.16/0.52 % (22014)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1419721089:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.16/0.52 % (22015)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3907186372:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.16/0.52 % TRYING [5]
% 0.16/0.52 % TRYING [6]
% 0.16/0.52 % (22012) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-22004-22012"...
% 0.16/0.52 % (22012)...printing done.
% 0.16/0.52 % (22012)Refutation found. Thanks to Tanya!
% 0.16/0.52 % SZS status Theorem for theBenchmark
% 0.16/0.52 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/0.52 % (22012)------------------------------
% 0.16/0.52 % (22012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.16/0.52 % (22012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/0.52 % (22012)CaDiCaL version: 2.1.3
% 0.16/0.52 % (22012)Termination reason: Refutation
% 0.16/0.52 % (22012)Time elapsed: 0.027 s
% 0.16/0.52 % (22012)Peak memory usage: 13 MB
% 0.16/0.52 % (22012)Instructions burned: 43 (million)
% 0.16/0.52 % (22004)Success in time 0.074 s
% 0.16/0.52 % Vampire exiting
%------------------------------------------------------------------------------