%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:20:07 PM UTC 2026
% Result : Theorem 0.15s 10.63s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 18
% Syntax : Number of formulae : 99 ( 12 unt; 15 def)
% Number of atoms : 396 ( 52 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 471 ( 174 ~; 213 |; 58 &)
% ( 20 <=>; 5 =>; 0 <=; 1 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 15 prp; 0-5 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-3 aty)
% Number of variables : 145 ( 115 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
! [D] :
( in(D,C)
<=> ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f36,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ( ! [C,D,E] :
( ( in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
=> D = E )
=> ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,plain,
? [A,B] :
( ! [C] :
? [D] :
( in(D,C)
<~> ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) ) )
& element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f39,plain,
? [A,B] :
( ! [C] :
? [D] :
( ( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ~ in(D,powerset(the_carrier(A)))
| ~ in(D,C) )
& ( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) )
| in(D,C) ) )
& element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) ),
inference(NNF_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
( ! [C] :
( ( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)
| ~ in(sK2_skl(C),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(C),C) )
& ( ( in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)
& in(sK2_skl(C),powerset(the_carrier(sK0_skl))) )
| in(sK2_skl(C),C) ) )
& element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
& top_str(sK0_skl)
& topological_space(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(D,sK2_skl(C))],[f39]) ).
fof(f41,plain,
topological_space(sK0_skl),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f42,plain,
top_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f43,plain,
element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f44,plain,
! [X0] :
( in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f45,plain,
! [X0] :
( in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f46,plain,
! [X0] :
( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| ~ in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f152,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f153,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) ) )
| ? [C,D,E] :
( D != E
& in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f154,definition,
! [A,B,C,D,E] :
( sP0_prd(E,D,C,B,A)
<=> ( D != E
& in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f155,plain,
! [A,B] :
( ? [C] :
! [D] :
( in(D,C)
<=> ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(formula_renaming,[status(thm)],[f153,f154]) ).
fof(f156,plain,
! [A,B] :
( ? [C] :
! [D] :
( ( ! [E] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,C) )
& ( ? [E] :
( in(set_difference(cast_as_carrier_subset(A),D),B)
& E = D
& in(E,powerset(the_carrier(A))) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(NNF_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ! [E] :
( E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,C) )
& ! [D] :
( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& ? [E] :
( E = D
& in(E,powerset(the_carrier(A))) ) )
| ~ in(D,C) ) )
| ? [C,D,E] : sP0_prd(E,D,C,B,A)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f158,plain,
! [A,B] :
( ( ! [D] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ! [E] :
( E != D
| ~ in(E,powerset(the_carrier(A))) )
| in(D,sK10_skl(B,A)) )
& ! [D] :
( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& sK11_skl(D,B,A) = D
& in(sK11_skl(D,B,A),powerset(the_carrier(A))) )
| ~ in(D,sK10_skl(B,A)) ) )
| sP0_prd(sK9_skl(B,A),sK8_skl(B,A),sK7_skl(B,A),B,A)
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(C,sK7_skl(B,A)),skolemize(D,sK8_skl(B,A)),skolemize(E,sK9_skl(B,A)),skolemize(C,sK10_skl(B,A)),skolemize(E,sK11_skl(D,B,A))],[f157]) ).
fof(f159,plain,
! [X0,X1,X2] :
( in(sK11_skl(X2,X1,X0),powerset(the_carrier(X0)))
| ~ in(X2,sK10_skl(X1,X0))
| sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
! [X0,X1,X2] :
( sK11_skl(X2,X1,X0) = X2
| ~ in(X2,sK10_skl(X1,X0))
| sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f161,plain,
! [X0,X1,X2] :
( in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| ~ in(X2,sK10_skl(X1,X0))
| sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( ~ in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| X3 != X2
| ~ in(X3,powerset(the_carrier(X0)))
| in(X2,sK10_skl(X1,X0))
| sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f163,plain,
! [A,B,C,D,E] :
( ( D = E
| ~ in(set_difference(cast_as_carrier_subset(A),E),B)
| C != E
| ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| C != D
| sP0_prd(E,D,C,B,A) )
& ( ( D != E
& in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f154]) ).
fof(f164,plain,
( ! [A,B,C,D,E] :
( D = E
| ~ in(set_difference(cast_as_carrier_subset(A),E),B)
| C != E
| ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| C != D
| sP0_prd(E,D,C,B,A) )
& ! [A,B,C,D,E] :
( ( D != E
& in(set_difference(cast_as_carrier_subset(A),E),B)
& C = E
& in(set_difference(cast_as_carrier_subset(A),D),B)
& C = D )
| ~ sP0_prd(E,D,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X1
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f167,plain,
! [X0,X1,X2,X3,X4] :
( X2 = X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f169,plain,
! [X0,X1,X2,X3,X4] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f171,plain,
! [X0,X1,X2] :
( ~ in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| ~ in(X2,powerset(the_carrier(X0)))
| in(X2,sK10_skl(X1,X0))
| sP0_prd(sK9_skl(X1,X0),sK8_skl(X1,X0),sK7_skl(X1,X0),X1,X0)
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f162]) ).
fof(f172,plain,
! [X0,X1,X2,X3] : ~ sP0_prd(X0,X0,X1,X2,X3),
inference(destructive_equality_resolution,[status(thm)],[f169]) ).
fof(f176,plain,
! [X0,X1] :
( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f171,f41]) ).
fof(f177,definition,
( sQ0_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f179,plain,
( sQ0_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,definition,
! [X0,X1] :
( sQ1_spl
<=> ( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f181,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f176,f177,f180]) ).
fof(f184,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f179,f42]) ).
fof(f185,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1] :
( ~ sQ1_spl
| in(sK2_skl(X1),X1)
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X1)),X0)
| in(sK2_skl(X1),sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f181,f44]) ).
fof(f187,plain,
! [X0] :
( ~ sQ1_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl))
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f186,f45]) ).
fof(f188,definition,
( sQ2_spl
<=> element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f190,plain,
( sQ2_spl
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,definition,
( sQ3_spl
<=> sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( ~ sQ3_spl
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f194,definition,
! [X0] :
( sQ4_spl
<=> ( in(sK2_skl(X0),X0)
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f195,plain,
! [X0] :
( ~ sQ4_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f197,plain,
( ~ sQ1_spl
| sQ4_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f187,f188,f191,f194,f180]) ).
fof(f198,plain,
! [X0] :
( ~ sQ4_spl
| in(sK2_skl(X0),X0)
| in(sK2_skl(X0),sK10_skl(sK1_skl,sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f195]) ).
fof(f201,plain,
! [X0] :
( ~ sQ4_spl
| sK11_skl(sK2_skl(X0),sK1_skl,sK0_skl) = sK2_skl(X0)
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl)
| in(sK2_skl(X0),X0) ),
inference(resolution,[status(thm)],[f198,f160]) ).
fof(f206,definition,
( sQ6_spl
<=> topological_space(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f208,plain,
( sQ6_spl
| ~ topological_space(sK0_skl) ),
inference(component_clause,[status(thm)],[f206]) ).
fof(f214,definition,
! [X0] :
( sQ8_spl
<=> ( sK11_skl(sK2_skl(X0),sK1_skl,sK0_skl) = sK2_skl(X0)
| in(sK2_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f215,plain,
! [X0] :
( ~ sQ8_spl
| sK11_skl(sK2_skl(X0),sK1_skl,sK0_skl) = sK2_skl(X0)
| in(sK2_skl(X0),X0) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,plain,
( ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f201,f214,f206,f177,f188,f191,f194]) ).
fof(f218,plain,
( ~ sQ3_spl
| sK7_skl(sK1_skl,sK0_skl) = sK9_skl(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f192,f167]) ).
fof(f219,plain,
( ~ sQ3_spl
| sK7_skl(sK1_skl,sK0_skl) = sK8_skl(sK1_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f192,f165]) ).
fof(f222,plain,
( ~ sQ3_spl
| sP0_prd(sK7_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f218,f192]) ).
fof(f227,plain,
( ~ sQ3_spl
| sP0_prd(sK7_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f219,f222]) ).
fof(f228,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f227,f172]) ).
fof(f229,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f228]) ).
fof(f230,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f190,f43]) ).
fof(f231,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f230]) ).
fof(f232,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f208,f41]) ).
fof(f233,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f232]) ).
fof(f246,plain,
! [X0,X1] :
( ~ sQ8_spl
| sK11_skl(sK2_skl(sK10_skl(X0,X1)),X0,X1) = sK2_skl(sK10_skl(X0,X1))
| sP0_prd(sK9_skl(X0,X1),sK8_skl(X0,X1),sK7_skl(X0,X1),X0,X1)
| ~ element(X0,powerset(powerset(the_carrier(X1))))
| ~ top_str(X1)
| ~ topological_space(X1)
| sK11_skl(sK2_skl(sK10_skl(X0,X1)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f215,f160]) ).
fof(f291,plain,
! [X0] :
( ~ sQ8_spl
| sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl)
| sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl)) ),
inference(resolution,[status(thm)],[f246,f41]) ).
fof(f292,definition,
! [X0] :
( sQ17_spl
<=> ( sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f293,plain,
! [X0] :
( ~ sQ17_spl
| sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),X0,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl))
| sP0_prd(sK9_skl(X0,sK0_skl),sK8_skl(X0,sK0_skl),sK7_skl(X0,sK0_skl),X0,sK0_skl)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| sK11_skl(sK2_skl(sK10_skl(X0,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(X0,sK0_skl)) ),
inference(component_clause,[status(thm)],[f292]) ).
fof(f295,plain,
( ~ sQ8_spl
| ~ sQ0_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f291,f292,f177,f214]) ).
fof(f308,definition,
( sQ21_spl
<=> empty(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f309,plain,
( ~ sQ21_spl
| empty(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f308]) ).
fof(f322,definition,
( sQ25_spl
<=> sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( ~ sQ25_spl
| sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f325,definition,
( sQ26_spl
<=> in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ26_spl
| in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f329,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f309,f152]) ).
fof(f330,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f329]) ).
fof(f331,plain,
( ~ sQ26_spl
| ~ in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl)))
| ~ in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f326,f46]) ).
fof(f334,definition,
( sQ27_spl
<=> in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f335,plain,
( ~ sQ27_spl
| in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f336,plain,
( sQ27_spl
| ~ in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f337,definition,
( sQ28_spl
<=> in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( sQ28_spl
| ~ in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f337]) ).
fof(f340,plain,
( ~ sQ26_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f331,f334,f337,f325]) ).
fof(f347,definition,
( sQ29_spl
<=> in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f348,plain,
( ~ sQ29_spl
| in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f357,plain,
( ~ sQ17_spl
| sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(sK1_skl,sK0_skl))
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl) = sK2_skl(sK10_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f293,f43]) ).
fof(f366,plain,
( ~ sQ17_spl
| sQ3_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f357,f322,f191,f292]) ).
fof(f390,plain,
( ~ sQ29_spl
| ~ sQ25_spl
| in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),powerset(the_carrier(sK0_skl))) ),
inference(forward_demodulation,[status(thm)],[f323,f348]) ).
fof(f391,plain,
( ~ sQ29_spl
| ~ sQ25_spl
| sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f390,f339]) ).
fof(f392,plain,
( ~ sQ29_spl
| ~ sQ25_spl
| sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f391]) ).
fof(f393,plain,
( ~ sQ27_spl
| in(sK11_skl(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(the_carrier(sK0_skl)))
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f335,f159]) ).
fof(f394,plain,
( ~ sQ27_spl
| in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK10_skl(sK1_skl,sK0_skl))),sK1_skl)
| sP0_prd(sK9_skl(sK1_skl,sK0_skl),sK8_skl(sK1_skl,sK0_skl),sK7_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl)
| ~ topological_space(sK0_skl) ),
inference(resolution,[status(thm)],[f335,f161]) ).
fof(f397,plain,
( ~ sQ27_spl
| sQ29_spl
| sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f393,f206,f177,f188,f191,f347,f334]) ).
fof(f398,plain,
( ~ sQ27_spl
| sQ26_spl
| sQ3_spl
| ~ sQ2_spl
| ~ sQ0_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f394,f206,f177,f188,f191,f325,f334]) ).
fof(f403,plain,
( ~ sQ4_spl
| sQ27_spl
| in(sK2_skl(sK10_skl(sK1_skl,sK0_skl)),sK10_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f336,f198]) ).
fof(f405,plain,
( ~ sQ4_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f403,f334,f194]) ).
fof(f406,plain,
$false,
inference(sat_refutation,[status(thm)],[f183,f185,f197,f217,f229,f231,f233,f295,f330,f340,f366,f392,f397,f398,f405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/10.59 % Computer : n001.cluster.edu
% 0.09/10.59 % Model : x86_64 x86_64
% 0.09/10.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.59 % Memory : 8046.5625MB
% 0.09/10.59 % OS : Linux 6.8.0-71-generic
% 0.09/10.59 % CPULimit : 300
% 0.09/10.59 % WCLimit : 300
% 0.09/10.59 % DateTime : Mon Sep 21 06:16:10 UTC 2026
% 0.09/10.59 % CPUTime :
% 0.15/10.60 % Drodi V4.1.1
% 0.15/10.63 % Refutation found
% 0.15/10.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/10.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/10.66 % Elapsed time: 0.052789 seconds
% 0.15/10.66 % CPU time: 0.183425 seconds
% 0.15/10.66 % Total memory used: 84.956 MB
% 0.15/10.66 % Net memory used: 84.823 MB
%------------------------------------------------------------------------------