%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU311+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:08 PM UTC 2026
% Result : Theorem 0.02s 0.41s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 50
% Syntax : Number of formulae : 240 ( 32 unt; 34 def)
% Number of atoms : 681 ( 20 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 727 ( 286 ~; 331 |; 52 &)
% ( 42 <=>; 15 =>; 0 <=; 1 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 43 ( 41 usr; 35 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-2 aty)
% Number of variables : 221 ( 201 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
( ! [D] :
( element(D,powerset(the_carrier(A)))
=> ( in(D,C)
<=> in(set_difference(cast_as_carrier_subset(A),D),B) ) )
& element(C,powerset(powerset(the_carrier(A)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A,B] :
( ( element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) )
=> ? [C] :
( ! [D] :
( element(D,powerset(the_carrier(A)))
=> ( in(D,C)
<=> in(set_difference(cast_as_carrier_subset(A),D),B) ) )
& element(C,powerset(powerset(the_carrier(A)))) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f24,axiom,
! [A] :
( ( top_str(A)
& topological_space(A) )
=> ? [B] :
( closed_subset(B,A)
& element(B,powerset(the_carrier(A))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A] :
( ~ empty(A)
=> ? [B] :
( ~ empty(B)
& element(B,powerset(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( one_sorted_str(A)
=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( top_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [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/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A,B] :
( ! [C] :
( in(C,A)
=> in(C,B) )
=> element(A,powerset(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [A,B] :
~ ( empty(B)
& A != B
& empty(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,plain,
? [A,B] :
( ! [C] :
( ? [D] :
( ( in(D,C)
<~> in(set_difference(cast_as_carrier_subset(A),D),B) )
& element(D,powerset(the_carrier(A))) )
| ~ element(C,powerset(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(f49,plain,
? [A,B] :
( ! [C] :
( ? [D] :
( ( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ~ in(D,C) )
& ( in(set_difference(cast_as_carrier_subset(A),D),B)
| in(D,C) )
& element(D,powerset(the_carrier(A))) )
| ~ element(C,powerset(powerset(the_carrier(A)))) )
& element(B,powerset(powerset(the_carrier(A))))
& top_str(A)
& topological_space(A) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
( ! [C] :
( ( ( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)
| ~ in(sK2_skl(C),C) )
& ( in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(C)),sK1_skl)
| in(sK2_skl(C),C) )
& element(sK2_skl(C),powerset(the_carrier(sK0_skl))) )
| ~ element(C,powerset(powerset(the_carrier(sK0_skl)))) )
& 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))],[f49]) ).
fof(f51,plain,
topological_space(sK0_skl),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
top_str(sK0_skl),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [X0] :
( element(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f55,plain,
! [X0] :
( in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f56,plain,
! [X0] :
( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| ~ in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f137,plain,
! [A] :
( ? [B] :
( closed_subset(B,A)
& element(B,powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
! [A] :
( ( closed_subset(sK4_skl(A),A)
& element(sK4_skl(A),powerset(the_carrier(A))) )
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f137]) ).
fof(f139,plain,
! [X0] :
( element(sK4_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
! [A] :
( ? [B] :
( ~ empty(B)
& element(B,powerset(A)) )
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f142,plain,
! [A] :
( ( ~ empty(sK5_skl(A))
& element(sK5_skl(A),powerset(A)) )
| empty(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f141]) ).
fof(f143,plain,
! [X0] :
( element(sK5_skl(X0),powerset(X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f145,plain,
! [A] :
( empty(sK6_skl(A))
& element(sK6_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f26]) ).
fof(f146,plain,
! [X0] : element(sK6_skl(X0),powerset(X0)),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
! [X0] : empty(sK6_skl(X0)),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f154,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f155,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f157,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f158,plain,
! [A] :
( one_sorted_str(A)
| ~ top_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f159,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f162,plain,
! [X0] : ~ empty(powerset(X0)),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f163,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)],[f37]) ).
fof(f164,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)],[f163]) ).
fof(f165,plain,
! [A,B] :
( ? [C] :
( ! [D] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ~ in(D,powerset(the_carrier(A)))
| in(D,C) )
& ! [D] :
( ( 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(miniscoping,[status(thm)],[f164]) ).
fof(f166,plain,
! [A,B] :
( ( ! [D] :
( ~ in(set_difference(cast_as_carrier_subset(A),D),B)
| ~ in(D,powerset(the_carrier(A)))
| in(D,sK7_skl(B,A)) )
& ! [D] :
( ( in(set_difference(cast_as_carrier_subset(A),D),B)
& in(D,powerset(the_carrier(A))) )
| ~ in(D,sK7_skl(B,A)) ) )
| ~ element(B,powerset(powerset(the_carrier(A))))
| ~ top_str(A)
| ~ topological_space(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B,A))],[f165]) ).
fof(f167,plain,
! [X0,X1,X2] :
( in(X2,powerset(the_carrier(X0)))
| ~ in(X2,sK7_skl(X1,X0))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0,X1,X2] :
( in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| ~ in(X2,sK7_skl(X1,X0))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f169,plain,
! [X0,X1,X2] :
( ~ in(set_difference(cast_as_carrier_subset(X0),X2),X1)
| ~ in(X2,powerset(the_carrier(X0)))
| in(X2,sK7_skl(X1,X0))
| ~ element(X1,powerset(powerset(the_carrier(X0))))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f170,plain,
! [A,B] :
( ( ( element(B,A)
<=> empty(B) )
| ~ empty(A) )
& ( ( element(B,A)
<=> in(B,A) )
| empty(A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f171,plain,
! [A,B] :
( ( ( ( ~ empty(B)
| element(B,A) )
& ( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ( ( ( ~ in(B,A)
| element(B,A) )
& ( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(NNF_transformation,[status(thm)],[f170]) ).
fof(f172,plain,
( ! [A] :
( ( ! [B] :
( ~ empty(B)
| element(B,A) )
& ! [B] :
( empty(B)
| ~ element(B,A) ) )
| ~ empty(A) )
& ! [A] :
( ( ! [B] :
( ~ in(B,A)
| element(B,A) )
& ! [B] :
( in(B,A)
| ~ element(B,A) ) )
| empty(A) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( in(X1,X0)
| ~ element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [X0,X1] :
( ~ in(X1,X0)
| element(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f175,plain,
! [X0,X1] :
( empty(X1)
| ~ element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f176,plain,
! [X0,X1] :
( ~ empty(X1)
| element(X1,X0)
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f177,plain,
! [A] : element(sK8_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f40]) ).
fof(f178,plain,
! [X0] : element(sK8_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f180,plain,
! [A,B] :
( element(A,powerset(B))
| ? [C] :
( ~ in(C,B)
& in(C,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f181,plain,
! [A,B] :
( element(A,powerset(B))
| ( ~ in(sK9_skl(B,A),B)
& in(sK9_skl(B,A),A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(C,sK9_skl(B,A))],[f180]) ).
fof(f182,plain,
! [X0,X1] :
( element(X1,powerset(X0))
| in(sK9_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( element(X1,powerset(X0))
| ~ in(sK9_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,plain,
empty(sK10_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f43]) ).
fof(f185,plain,
empty(sK10_skl),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f188,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f189,plain,
! [X0] :
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f190,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f191,plain,
! [B] :
( ~ empty(B)
| ! [A] : ~ in(A,B) ),
inference(miniscoping,[status(thm)],[f190]) ).
fof(f192,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
! [A,B] :
( ~ empty(B)
| A = B
| ~ empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f194,plain,
! [B] :
( ~ empty(B)
| ! [A] :
( A = B
| ~ empty(A) ) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f195,plain,
! [X0,X1] :
( ~ empty(X1)
| X0 = X1
| ~ empty(X0) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f198,plain,
! [X0] : ~ in(X0,sK10_skl),
inference(resolution,[status(thm)],[f185,f192]) ).
fof(f199,plain,
! [X0] :
( ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f173,f54]) ).
fof(f200,plain,
( in(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
| empty(powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f173,f53]) ).
fof(f201,definition,
( sQ0_spl
<=> empty(powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ0_spl
| empty(powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,definition,
! [X0] :
( sQ1_spl
<=> ( ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(X0),powerset(the_carrier(sK0_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f205,plain,
! [X0] :
( ~ sQ1_spl
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(X0),powerset(the_carrier(sK0_skl))) ),
inference(component_clause,[status(thm)],[f204]) ).
fof(f207,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f199,f201,f204]) ).
fof(f208,definition,
( sQ2_spl
<=> empty(powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f209,plain,
( ~ sQ2_spl
| empty(powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,definition,
( sQ3_spl
<=> in(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f200,f208,f211]) ).
fof(f217,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f174,f192]) ).
fof(f220,definition,
! [X0] :
( sQ4_spl
<=> ( in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f228,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f209,f162]) ).
fof(f229,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f202,f162]) ).
fof(f230,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f228]) ).
fof(f231,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f229]) ).
fof(f234,plain,
( ~ sQ1_spl
| in(sK2_skl(sK1_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f205,f53]) ).
fof(f235,plain,
( ~ sQ1_spl
| element(sK2_skl(sK1_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f234,f217]) ).
fof(f237,plain,
( ~ sQ1_spl
| in(sK2_skl(sK1_skl),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f235,f173]) ).
fof(f238,definition,
( sQ6_spl
<=> in(sK2_skl(sK1_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( ~ sQ1_spl
| sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f237,f201,f238,f204]) ).
fof(f242,plain,
( ~ sQ1_spl
| in(sK2_skl(sK8_skl(powerset(powerset(the_carrier(sK0_skl))))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f178,f205]) ).
fof(f243,plain,
! [X0] :
( in(sK8_skl(X0),X0)
| empty(X0) ),
inference(resolution,[status(thm)],[f178,f173]) ).
fof(f247,plain,
! [X0,X1] :
( ~ in(X1,X0)
| in(sK8_skl(X0),X0) ),
inference(resolution,[status(thm)],[f243,f192]) ).
fof(f250,plain,
( ~ sQ1_spl
| element(sK2_skl(sK8_skl(powerset(powerset(the_carrier(sK0_skl))))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f242,f217]) ).
fof(f254,plain,
! [X0] : sK6_skl(X0) = empty_set,
inference(resolution,[status(thm)],[f189,f147]) ).
fof(f255,plain,
sK10_skl = empty_set,
inference(resolution,[status(thm)],[f189,f185]) ).
fof(f257,plain,
! [X0] :
( in(sK8_skl(X0),X0)
| X0 = empty_set ),
inference(resolution,[status(thm)],[f189,f243]) ).
fof(f258,plain,
! [X0] :
( X0 = sK10_skl
| ~ empty(X0) ),
inference(backward_demodulation,[status(thm)],[f255,f189]) ).
fof(f263,plain,
! [X0] : sK6_skl(X0) = sK10_skl,
inference(forward_demodulation,[status(thm)],[f255,f254]) ).
fof(f267,plain,
! [X0] : element(sK10_skl,powerset(X0)),
inference(forward_demodulation,[status(thm)],[f263,f146]) ).
fof(f268,plain,
( ~ sQ1_spl
| in(sK2_skl(sK10_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f267,f205]) ).
fof(f274,plain,
! [X0,X1] :
( in(sK8_skl(X1),X1)
| X0 = X1
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f195,f243]) ).
fof(f277,plain,
( ~ sQ1_spl
| element(sK2_skl(sK10_skl),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f268,f217]) ).
fof(f279,plain,
( ~ sQ1_spl
| in(sK2_skl(sK10_skl),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f277,f173]) ).
fof(f280,definition,
( sQ7_spl
<=> in(sK2_skl(sK10_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f283,plain,
( ~ sQ1_spl
| sQ7_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f279,f201,f280,f204]) ).
fof(f284,plain,
( ~ sQ1_spl
| in(sK2_skl(sK8_skl(powerset(powerset(the_carrier(sK0_skl))))),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f250,f173]) ).
fof(f285,definition,
( sQ8_spl
<=> in(sK2_skl(sK8_skl(powerset(powerset(the_carrier(sK0_skl))))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ1_spl
| sQ8_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f284,f201,f285,f204]) ).
fof(f289,plain,
! [X0] :
( in(sK8_skl(X0),X0)
| X0 = sK10_skl ),
inference(forward_demodulation,[status(thm)],[f255,f257]) ).
fof(f299,plain,
! [X0,X1] :
( in(sK8_skl(X0),X0)
| in(sK8_skl(X1),X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f274,f243]) ).
fof(f303,plain,
! [X0] :
( empty(X0)
| ~ element(X0,sK10_skl) ),
inference(resolution,[status(thm)],[f175,f185]) ).
fof(f304,plain,
! [X0,X1] :
( in(sK8_skl(X1),X1)
| empty(X0)
| ~ element(X0,X1) ),
inference(resolution,[status(thm)],[f175,f243]) ).
fof(f305,plain,
empty(sK8_skl(sK10_skl)),
inference(resolution,[status(thm)],[f303,f178]) ).
fof(f309,plain,
sK8_skl(sK10_skl) = sK10_skl,
inference(resolution,[status(thm)],[f305,f258]) ).
fof(f313,plain,
! [X0] :
( in(sK8_skl(X0),X0)
| in(sK10_skl,sK10_skl)
| X0 = sK10_skl ),
inference(paramodulation,[status(thm)],[f309,f299]) ).
fof(f315,plain,
! [X0] :
( ~ in(X0,sK10_skl)
| in(sK10_skl,sK10_skl) ),
inference(paramodulation,[status(thm)],[f309,f247]) ).
fof(f317,plain,
( in(sK10_skl,sK10_skl)
| sK10_skl = sK10_skl ),
inference(paramodulation,[status(thm)],[f309,f289]) ).
fof(f318,plain,
element(sK10_skl,sK10_skl),
inference(paramodulation,[status(thm)],[f309,f178]) ).
fof(f319,definition,
! [X0] :
( sQ9_spl
<=> ( in(sK8_skl(X0),X0)
| X0 = sK10_skl ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f322,definition,
( sQ10_spl
<=> in(sK10_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( ~ sQ10_spl
| in(sK10_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f326,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f313,f319,f322]) ).
fof(f327,definition,
! [X0] :
( sQ11_spl
<=> ~ in(X0,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f315,f322,f327]) ).
fof(f332,definition,
( sQ12_spl
<=> sK10_skl = sK10_skl ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( sQ10_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f317,f332,f322]) ).
fof(f338,plain,
( in(sK10_skl,sK10_skl)
| empty(sK10_skl) ),
inference(resolution,[status(thm)],[f318,f173]) ).
fof(f339,definition,
( sQ13_spl
<=> empty(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f342,plain,
( sQ10_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f338,f339,f322]) ).
fof(f346,plain,
! [X0,X1] :
( in(sK8_skl(X1),X1)
| element(X1,X0)
| ~ empty(X0) ),
inference(resolution,[status(thm)],[f176,f243]) ).
fof(f353,definition,
( sQ14_spl
<=> in(sK8_skl(sK10_skl),sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( ~ sQ14_spl
| in(sK8_skl(sK10_skl),sK10_skl) ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f364,plain,
! [X0] :
( in(sK10_skl,sK10_skl)
| empty(X0)
| ~ element(X0,sK10_skl) ),
inference(paramodulation,[status(thm)],[f309,f304]) ).
fof(f365,definition,
! [X0] :
( sQ16_spl
<=> ( empty(X0)
| ~ element(X0,sK10_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( sQ10_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f364,f365,f322]) ).
fof(f369,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f323,f198]) ).
fof(f370,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f369]) ).
fof(f372,plain,
! [X0,X1] :
( in(sK8_skl(X1),X1)
| in(sK8_skl(X0),X0)
| element(X0,X1) ),
inference(resolution,[status(thm)],[f346,f243]) ).
fof(f381,plain,
! [X0] :
( empty(X0)
| in(sK8_skl(sK10_skl),sK10_skl)
| in(sK8_skl(X0),X0) ),
inference(resolution,[status(thm)],[f372,f303]) ).
fof(f384,definition,
! [X0] :
( sQ18_spl
<=> ( empty(X0)
| in(sK8_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( sQ14_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f381,f384,f353]) ).
fof(f392,plain,
( ~ sQ14_spl
| in(sK10_skl,sK10_skl) ),
inference(forward_demodulation,[status(thm)],[f309,f354]) ).
fof(f393,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f198]) ).
fof(f394,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f393]) ).
fof(f397,plain,
( ~ sQ1_spl
| in(sK2_skl(sK5_skl(powerset(the_carrier(sK0_skl)))),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f143,f205]) ).
fof(f399,definition,
( sQ20_spl
<=> in(sK2_skl(sK5_skl(powerset(the_carrier(sK0_skl)))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ1_spl
| sQ20_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f397,f201,f399,f204]) ).
fof(f410,plain,
! [X0] :
( in(sK4_skl(X0),powerset(the_carrier(X0)))
| empty(powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(resolution,[status(thm)],[f139,f173]) ).
fof(f411,plain,
! [X0] :
( in(sK4_skl(X0),powerset(the_carrier(X0)))
| ~ top_str(X0)
| ~ topological_space(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f162]) ).
fof(f412,plain,
( in(sK4_skl(sK0_skl),powerset(the_carrier(sK0_skl)))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f411,f51]) ).
fof(f413,definition,
( sQ21_spl
<=> top_str(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f415,plain,
( sQ21_spl
| ~ top_str(sK0_skl) ),
inference(component_clause,[status(thm)],[f413]) ).
fof(f416,definition,
( sQ22_spl
<=> in(sK4_skl(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f412,f413,f416]) ).
fof(f420,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f415,f52]) ).
fof(f421,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f420]) ).
fof(f426,plain,
! [X0] :
( in(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| empty(powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f157,f173]) ).
fof(f427,plain,
! [X0] :
( in(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f162]) ).
fof(f428,plain,
! [X0] :
( ~ top_str(X0)
| in(cast_as_carrier_subset(X0),powerset(the_carrier(X0))) ),
inference(resolution,[status(thm)],[f427,f159]) ).
fof(f429,plain,
in(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl))),
inference(resolution,[status(thm)],[f428,f52]) ).
fof(f430,plain,
element(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl))),
inference(resolution,[status(thm)],[f429,f217]) ).
fof(f432,plain,
( in(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f430,f173]) ).
fof(f433,definition,
( sQ23_spl
<=> in(cast_as_carrier_subset(sK0_skl),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f436,plain,
( sQ23_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f432,f201,f433]) ).
fof(f437,plain,
! [X0] :
( ~ sQ1_spl
| in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK9_skl(powerset(the_carrier(sK0_skl)),X0),X0) ),
inference(resolution,[status(thm)],[f182,f205]) ).
fof(f438,plain,
! [X0,X1] :
( in(X1,powerset(X0))
| empty(powerset(X0))
| in(sK9_skl(X0,X1),X1) ),
inference(resolution,[status(thm)],[f182,f173]) ).
fof(f439,plain,
! [X0,X1] :
( in(X1,powerset(X0))
| in(sK9_skl(X0,X1),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f162]) ).
fof(f440,plain,
! [X0] :
( element(X0,powerset(X0))
| in(X0,powerset(X0)) ),
inference(resolution,[status(thm)],[f439,f183]) ).
fof(f444,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_subsumption_resolution,[status(thm)],[f440,f217]) ).
fof(f445,plain,
( ~ sQ1_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
inference(resolution,[status(thm)],[f444,f205]) ).
fof(f450,plain,
! [X0,X1] :
( in(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f167,f51]) ).
fof(f451,definition,
! [X0,X1] :
( sQ24_spl
<=> ( in(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f452,plain,
! [X0,X1] :
( ~ sQ24_spl
| in(X1,powerset(the_carrier(sK0_skl)))
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ24_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f450,f413,f451]) ).
fof(f455,plain,
! [X0,X1] :
( in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f168,f51]) ).
fof(f456,definition,
! [X0,X1] :
( sQ25_spl
<=> ( in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f457,plain,
! [X0,X1] :
( ~ sQ25_spl
| in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,plain,
( sQ25_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f455,f413,f456]) ).
fof(f460,plain,
! [X0,X1] :
( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ top_str(sK0_skl) ),
inference(resolution,[status(thm)],[f169,f51]) ).
fof(f461,definition,
! [X0,X1] :
( sQ26_spl
<=> ( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f462,plain,
! [X0,X1] :
( ~ sQ26_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X1),X0)
| ~ in(X1,powerset(the_carrier(sK0_skl)))
| in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,plain,
( sQ26_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f460,f413,f461]) ).
fof(f465,plain,
( ~ sQ1_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl)))),sK1_skl)
| ~ element(powerset(the_carrier(sK0_skl)),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f445,f56]) ).
fof(f468,definition,
( sQ27_spl
<=> element(powerset(the_carrier(sK0_skl)),powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f470,plain,
( sQ27_spl
| ~ element(powerset(the_carrier(sK0_skl)),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f468]) ).
fof(f471,definition,
( sQ28_spl
<=> in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl)))),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( sQ28_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(powerset(the_carrier(sK0_skl)))),sK1_skl) ),
inference(component_clause,[status(thm)],[f471]) ).
fof(f474,plain,
( ~ sQ1_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f465,f468,f471,f204]) ).
fof(f475,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f470,f444]) ).
fof(f476,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f475]) ).
fof(f478,definition,
( sQ29_spl
<=> in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f482,plain,
! [X0,X1] :
( ~ sQ24_spl
| element(X1,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(sK9_skl(powerset(the_carrier(sK0_skl)),X1),sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f452,f183]) ).
fof(f486,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ in(powerset(the_carrier(sK0_skl)),X1)
| ~ in(X1,sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f452,f155]) ).
fof(f494,plain,
( sQ28_spl
| in(sK2_skl(powerset(the_carrier(sK0_skl))),powerset(the_carrier(sK0_skl)))
| ~ element(powerset(the_carrier(sK0_skl)),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f473,f55]) ).
fof(f495,plain,
( sQ28_spl
| sQ29_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f494,f468,f478,f471]) ).
fof(f497,plain,
! [X0] :
( ~ sQ1_spl
| element(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK9_skl(powerset(the_carrier(sK0_skl)),X0),X0) ),
inference(resolution,[status(thm)],[f437,f217]) ).
fof(f503,plain,
! [X0] :
( ~ sQ1_spl
| in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| empty(powerset(the_carrier(sK0_skl)))
| in(sK9_skl(powerset(the_carrier(sK0_skl)),X0),X0) ),
inference(resolution,[status(thm)],[f497,f173]) ).
fof(f504,definition,
! [X0] :
( sQ32_spl
<=> ( in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK9_skl(powerset(the_carrier(sK0_skl)),X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( ~ sQ1_spl
| sQ0_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f503,f504,f201,f204]) ).
fof(f513,plain,
! [X0] :
( ~ sQ26_spl
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),sK7_skl(sK1_skl,sK0_skl))
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f462,f55]) ).
fof(f514,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ sQ26_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK7_skl(X1,sK0_skl))
| ~ element(X1,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(X0,powerset(the_carrier(sK0_skl)))
| in(X0,sK7_skl(powerset(the_carrier(sK0_skl)),sK0_skl))
| ~ element(powerset(the_carrier(sK0_skl)),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f462,f452]) ).
fof(f516,definition,
( sQ33_spl
<=> element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f518,plain,
( sQ33_spl
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f519,definition,
! [X0] :
( sQ34_spl
<=> ( in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),sK7_skl(sK1_skl,sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f520,plain,
! [X0] :
( ~ sQ34_spl
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(sK2_skl(X0),powerset(the_carrier(sK0_skl)))
| in(sK2_skl(X0),sK7_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f519]) ).
fof(f522,plain,
( ~ sQ26_spl
| sQ34_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f513,f516,f519,f461]) ).
fof(f523,definition,
! [X0,X1] :
( sQ35_spl
<=> ( ~ in(set_difference(cast_as_carrier_subset(sK0_skl),X0),sK7_skl(X1,sK0_skl))
| ~ element(X1,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(X0,powerset(the_carrier(sK0_skl)))
| in(X0,sK7_skl(powerset(the_carrier(sK0_skl)),sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f526,plain,
( ~ sQ24_spl
| ~ sQ26_spl
| sQ35_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f514,f468,f523,f461,f451]) ).
fof(f527,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f53]) ).
fof(f528,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f529,plain,
! [X0] :
( ~ sQ34_spl
| ~ sQ1_spl
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(X0),sK7_skl(sK1_skl,sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f205]) ).
fof(f532,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ in(powerset(the_carrier(sK0_skl)),sK7_skl(X1,sK0_skl))
| ~ element(X1,powerset(powerset(the_carrier(sK0_skl))))
| ~ in(powerset(the_carrier(sK0_skl)),sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f486,f452]) ).
fof(f534,definition,
! [X0] :
( sQ36_spl
<=> ( ~ in(powerset(the_carrier(sK0_skl)),sK7_skl(X0,sK0_skl))
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f537,plain,
( ~ sQ24_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f532,f534,f451]) ).
fof(f538,plain,
( ~ sQ34_spl
| ~ sQ1_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl)
| ~ element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))
| ~ element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f529,f56]) ).
fof(f539,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ34_spl
| ~ sQ1_spl
| in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(X0)),sK1_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl))))
| in(sK2_skl(X0),X0)
| ~ element(X0,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f529,f457]) ).
fof(f542,definition,
( sQ37_spl
<=> element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( sQ37_spl
| ~ element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f545,definition,
( sQ38_spl
<=> in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f546,plain,
( ~ sQ38_spl
| in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f545]) ).
fof(f548,definition,
( sQ39_spl
<=> in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( sQ39_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl) ),
inference(component_clause,[status(thm)],[f548]) ).
fof(f551,plain,
( ~ sQ34_spl
| ~ sQ1_spl
| ~ sQ39_spl
| sQ38_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f538,f542,f545,f548,f204,f519]) ).
fof(f552,plain,
( ~ sQ25_spl
| ~ sQ34_spl
| ~ sQ1_spl
| ~ sQ33_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f539,f220,f516,f204,f519,f456]) ).
fof(f553,plain,
( sQ39_spl
| in(sK2_skl(sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl))
| ~ element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f550,f55]) ).
fof(f554,plain,
( sQ39_spl
| sQ38_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f553,f542,f545,f548]) ).
fof(f555,plain,
( ~ sQ38_spl
| ~ in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl)
| ~ element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f546,f56]) ).
fof(f556,plain,
( ~ sQ25_spl
| ~ sQ38_spl
| in(set_difference(cast_as_carrier_subset(sK0_skl),sK2_skl(sK7_skl(sK1_skl,sK0_skl))),sK1_skl)
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f546,f457]) ).
fof(f559,plain,
( ~ sQ38_spl
| ~ sQ39_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f555,f542,f548,f545]) ).
fof(f560,plain,
( ~ sQ25_spl
| ~ sQ38_spl
| sQ39_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f556,f516,f548,f545,f456]) ).
fof(f561,plain,
( sQ37_spl
| in(sK9_skl(powerset(the_carrier(sK0_skl)),sK7_skl(sK1_skl,sK0_skl)),sK7_skl(sK1_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f544,f182]) ).
fof(f593,plain,
( ~ sQ24_spl
| sQ37_spl
| element(sK7_skl(sK1_skl,sK0_skl),powerset(powerset(the_carrier(sK0_skl))))
| ~ element(sK1_skl,powerset(powerset(the_carrier(sK0_skl)))) ),
inference(resolution,[status(thm)],[f561,f482]) ).
fof(f597,plain,
( ~ sQ24_spl
| sQ37_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f593,f516,f542,f451]) ).
fof(f602,plain,
$false,
inference(sat_refutation,[status(thm)],[f207,f214,f230,f231,f241,f283,f288,f326,f331,f336,f342,f368,f370,f387,f394,f402,f419,f421,f436,f454,f459,f464,f474,f476,f495,f507,f522,f526,f528,f537,f551,f552,f554,f559,f560,f597]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU311+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n011.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 06:10:26 UTC 2026
% 0.02/0.35 % CPUTime :
% 0.02/0.37 % Drodi V4.1.1
% 0.02/0.41 % Refutation found
% 0.02/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.02/0.43 % Elapsed time: 0.073037 seconds
% 0.02/0.43 % CPU time: 0.278744 seconds
% 0.02/0.43 % Total memory used: 87.137 MB
% 0.02/0.43 % Net memory used: 86.729 MB
%------------------------------------------------------------------------------