%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU147+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:19:23 PM UTC 2026
% Result : Theorem 0.15s 0.71s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 34
% Syntax : Number of formulae : 139 ( 17 unt; 22 def)
% Number of atoms : 411 ( 102 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 458 ( 186 ~; 192 |; 47 &)
% ( 32 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-3 aty)
% Number of variables : 165 ( 157 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B] :
( A = B
<=> ( subset(B,A)
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A,B] :
( B = singleton(A)
<=> ! [C] :
( in(C,B)
<=> C = A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B,C] :
( C = set_union2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
| in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B] : set_union2(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,lemma,
! [A,B] :
( set_difference(A,B) = empty_set
<=> subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,lemma,
! [A,B] :
( subset(A,singleton(B))
<=> ( A = singleton(B)
| A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
powerset(empty_set) = singleton(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
powerset(empty_set) != singleton(empty_set),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f50,lemma,
! [A] : subset(empty_set,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f73,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f79,plain,
! [A,B] :
( ( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f80,plain,
( ! [A,B] :
( ~ subset(B,A)
| ~ subset(A,B)
| A = B )
& ! [A,B] :
( ( subset(B,A)
& subset(A,B) )
| A != B ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f83,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f84,plain,
! [A,B] :
( ( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ( ! [C] :
( ( C != A
| in(C,B) )
& ( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f85,plain,
( ! [A,B] :
( ? [C] :
( ( C = A
| in(C,B) )
& ( C != A
| ~ in(C,B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(miniscoping,[status(thm)],[f84]) ).
fof(f86,plain,
( ! [A,B] :
( ( ( sK0_skl(B,A) = A
| in(sK0_skl(B,A),B) )
& ( sK0_skl(B,A) != A
| ~ in(sK0_skl(B,A),B) ) )
| B = singleton(A) )
& ! [A,B] :
( ( ! [C] :
( C != A
| in(C,B) )
& ! [C] :
( C = A
| ~ in(C,B) ) )
| B != singleton(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f85]) ).
fof(f87,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ in(X2,X0)
| X0 != singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f89,plain,
! [X0,X1] :
( sK0_skl(X0,X1) != X1
| ~ in(sK0_skl(X0,X1),X0)
| X0 = singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f90,plain,
! [X0,X1] :
( sK0_skl(X0,X1) = X1
| in(sK0_skl(X0,X1),X0)
| X0 = singleton(X1) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f91,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f92,plain,
( ! [A] :
( ? [B] : in(B,A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f93,plain,
( ! [A] :
( in(sK1_skl(A),A)
| A = empty_set )
& ! [A] :
( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B,sK1_skl(A))],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f96,plain,
! [A,B] :
( ( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ( ! [C] :
( ( ~ subset(C,A)
| in(C,B) )
& ( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f97,plain,
( ! [A,B] :
( ? [C] :
( ( subset(C,A)
| in(C,B) )
& ( ~ subset(C,A)
| ~ in(C,B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(miniscoping,[status(thm)],[f96]) ).
fof(f98,plain,
( ! [A,B] :
( ( ( subset(sK2_skl(B,A),A)
| in(sK2_skl(B,A),B) )
& ( ~ subset(sK2_skl(B,A),A)
| ~ in(sK2_skl(B,A),B) ) )
| B = powerset(A) )
& ! [A,B] :
( ( ! [C] :
( ~ subset(C,A)
| in(C,B) )
& ! [C] :
( subset(C,A)
| ~ in(C,B) ) )
| B != powerset(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f97]) ).
fof(f99,plain,
! [X0,X1,X2] :
( subset(X2,X1)
| ~ in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ subset(X2,X1)
| in(X2,X0)
| X0 != powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
! [X0,X1] :
( ~ subset(sK2_skl(X0,X1),X1)
| ~ in(sK2_skl(X0,X1),X0)
| X0 = powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f102,plain,
! [X0,X1] :
( subset(sK2_skl(X0,X1),X1)
| in(sK2_skl(X0,X1),X0)
| X0 = powerset(X1) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f112,plain,
! [A,B,C] :
( ( ? [D] :
( ( in(D,B)
| in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& ~ in(D,A) )
| ~ in(D,C) ) )
| C = set_union2(A,B) )
& ( ! [D] :
( ( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f113,plain,
( ! [A,B,C] :
( ? [D] :
( ( in(D,B)
| in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& ~ in(D,A) )
| ~ in(D,C) ) )
| C = set_union2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ! [D] :
( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(miniscoping,[status(thm)],[f112]) ).
fof(f114,plain,
( ! [A,B,C] :
( ( ( in(sK4_skl(C,B,A),B)
| in(sK4_skl(C,B,A),A)
| in(sK4_skl(C,B,A),C) )
& ( ( ~ in(sK4_skl(C,B,A),B)
& ~ in(sK4_skl(C,B,A),A) )
| ~ in(sK4_skl(C,B,A),C) ) )
| C = set_union2(A,B) )
& ! [A,B,C] :
( ( ! [D] :
( ( ~ in(D,B)
& ~ in(D,A) )
| in(D,C) )
& ! [D] :
( in(D,B)
| in(D,A)
| ~ in(D,C) ) )
| C != set_union2(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(D,sK4_skl(C,B,A))],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( in(X3,X2)
| in(X3,X1)
| ~ in(X3,X0)
| X0 != set_union2(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f162,plain,
! [A] : set_union2(A,A) = A,
inference(miniscoping,[status(thm)],[f27]) ).
fof(f163,plain,
! [X0] : set_union2(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f168,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f173,plain,
! [A,B] :
( ( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(NNF_transformation,[status(thm)],[f32]) ).
fof(f174,plain,
( ! [A,B] :
( ~ subset(A,B)
| set_difference(A,B) = empty_set )
& ! [A,B] :
( subset(A,B)
| set_difference(A,B) != empty_set ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1] :
( subset(X0,X1)
| set_difference(X0,X1) != empty_set ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f180,plain,
! [A,B] :
( ( ( A != singleton(B)
& A != empty_set )
| subset(A,singleton(B)) )
& ( A = singleton(B)
| A = empty_set
| ~ subset(A,singleton(B)) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f181,plain,
( ! [A,B] :
( ( A != singleton(B)
& A != empty_set )
| subset(A,singleton(B)) )
& ! [A,B] :
( A = singleton(B)
| A = empty_set
| ~ subset(A,singleton(B)) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f182,plain,
! [X0,X1] :
( X0 = singleton(X1)
| X0 = empty_set
| ~ subset(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f202,plain,
powerset(empty_set) != singleton(empty_set),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f214,plain,
! [X0] : subset(empty_set,X0),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f266,plain,
! [X0,X1] :
( X0 = X1
| ~ in(X0,singleton(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f87]) ).
fof(f268,plain,
! [X0] : ~ in(X0,empty_set),
inference(destructive_equality_resolution,[status(thm)],[f94]) ).
fof(f269,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f99]) ).
fof(f270,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| in(X0,powerset(X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f100]) ).
fof(f274,plain,
! [X0,X1,X2] :
( in(X0,X2)
| in(X0,X1)
| ~ in(X0,set_union2(X1,X2)) ),
inference(destructive_equality_resolution,[status(thm)],[f115]) ).
fof(f287,plain,
~ in(powerset(empty_set),singleton(singleton(empty_set))),
inference(resolution,[status(thm)],[f266,f202]) ).
fof(f297,plain,
( powerset(empty_set) = empty_set
| ~ subset(powerset(empty_set),singleton(empty_set)) ),
inference(resolution,[status(thm)],[f182,f202]) ).
fof(f298,plain,
! [X0] :
( empty_set = empty_set
| ~ subset(empty_set,singleton(X0)) ),
inference(resolution,[status(thm)],[f182,f168]) ).
fof(f300,definition,
( sQ0_spl
<=> subset(powerset(empty_set),singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( sQ0_spl
| ~ subset(powerset(empty_set),singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f300]) ).
fof(f303,definition,
( sQ1_spl
<=> powerset(empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f304,plain,
( ~ sQ1_spl
| powerset(empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f305,plain,
( sQ1_spl
| powerset(empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f306,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f297,f300,f303]) ).
fof(f307,definition,
! [X0] :
( sQ2_spl
<=> ~ subset(empty_set,singleton(X0)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f308,plain,
! [X0] :
( ~ sQ2_spl
| ~ subset(empty_set,singleton(X0)) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f310,definition,
( sQ3_spl
<=> empty_set = empty_set ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f298,f307,f310]) ).
fof(f314,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f214]) ).
fof(f315,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f314]) ).
fof(f456,plain,
! [X0] :
( in(powerset(empty_set),X0)
| ~ in(powerset(empty_set),set_union2(singleton(singleton(empty_set)),X0)) ),
inference(resolution,[status(thm)],[f287,f274]) ).
fof(f458,plain,
( sQ0_spl
| ~ in(powerset(empty_set),powerset(singleton(empty_set))) ),
inference(resolution,[status(thm)],[f302,f269]) ).
fof(f464,plain,
! [X0] :
( sQ0_spl
| in(powerset(empty_set),X0)
| ~ in(powerset(empty_set),set_union2(powerset(singleton(empty_set)),X0)) ),
inference(resolution,[status(thm)],[f458,f274]) ).
fof(f469,plain,
! [X0] :
( ~ in(X0,powerset(empty_set))
| ~ in(powerset(empty_set),set_union2(singleton(singleton(empty_set)),X0)) ),
inference(resolution,[status(thm)],[f456,f73]) ).
fof(f530,plain,
! [X0] :
( sQ0_spl
| ~ in(X0,powerset(empty_set))
| ~ in(powerset(empty_set),set_union2(powerset(singleton(empty_set)),X0)) ),
inference(resolution,[status(thm)],[f464,f73]) ).
fof(f566,plain,
! [X0] :
( sQ0_spl
| ~ in(powerset(empty_set),set_union2(powerset(singleton(empty_set)),set_union2(singleton(singleton(empty_set)),X0)))
| ~ in(X0,powerset(empty_set)) ),
inference(resolution,[status(thm)],[f469,f464]) ).
fof(f572,plain,
( ~ in(singleton(singleton(empty_set)),powerset(empty_set))
| ~ in(powerset(empty_set),singleton(singleton(empty_set))) ),
inference(paramodulation,[status(thm)],[f163,f469]) ).
fof(f573,definition,
( sQ5_spl
<=> in(powerset(empty_set),singleton(singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f576,definition,
( sQ6_spl
<=> in(singleton(singleton(empty_set)),powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f579,plain,
( ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f572,f573,f576]) ).
fof(f629,plain,
( sQ0_spl
| ~ in(powerset(singleton(empty_set)),powerset(empty_set))
| ~ in(powerset(empty_set),powerset(singleton(empty_set))) ),
inference(paramodulation,[status(thm)],[f163,f530]) ).
fof(f630,definition,
( sQ9_spl
<=> in(powerset(empty_set),powerset(singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f633,definition,
( sQ10_spl
<=> in(powerset(singleton(empty_set)),powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f636,plain,
( sQ0_spl
| ~ sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f629,f630,f633,f300]) ).
fof(f814,plain,
( sQ0_spl
| ~ in(powerset(empty_set),set_union2(powerset(singleton(empty_set)),singleton(singleton(empty_set))))
| ~ in(singleton(singleton(empty_set)),powerset(empty_set)) ),
inference(paramodulation,[status(thm)],[f163,f566]) ).
fof(f815,definition,
( sQ11_spl
<=> in(powerset(empty_set),set_union2(powerset(singleton(empty_set)),singleton(singleton(empty_set)))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f818,plain,
( sQ0_spl
| ~ sQ11_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f814,f576,f815,f300]) ).
fof(f1251,plain,
! [X0] :
( ~ sQ1_spl
| ~ subset(X0,empty_set)
| in(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f304,f270]) ).
fof(f1252,plain,
! [X0] :
( ~ sQ1_spl
| ~ subset(X0,empty_set) ),
inference(forward_subsumption_resolution,[status(thm)],[f1251,f268]) ).
fof(f1254,plain,
( ~ sQ1_spl
| $false ),
inference(resolution,[status(thm)],[f1252,f214]) ).
fof(f1260,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1254]) ).
fof(f1261,plain,
( sK0_skl(powerset(empty_set),empty_set) != empty_set
| ~ in(sK0_skl(powerset(empty_set),empty_set),powerset(empty_set)) ),
inference(resolution,[status(thm)],[f202,f89]) ).
fof(f1266,plain,
( ~ subset(sK2_skl(singleton(empty_set),empty_set),empty_set)
| ~ in(sK2_skl(singleton(empty_set),empty_set),singleton(empty_set)) ),
inference(resolution,[status(thm)],[f202,f101]) ).
fof(f1270,definition,
( sQ12_spl
<=> in(sK0_skl(powerset(empty_set),empty_set),powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1272,plain,
( sQ12_spl
| ~ in(sK0_skl(powerset(empty_set),empty_set),powerset(empty_set)) ),
inference(component_clause,[status(thm)],[f1270]) ).
fof(f1273,definition,
( sQ13_spl
<=> sK0_skl(powerset(empty_set),empty_set) = empty_set ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
( ~ sQ13_spl
| sK0_skl(powerset(empty_set),empty_set) = empty_set ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1275,plain,
( sQ13_spl
| sK0_skl(powerset(empty_set),empty_set) != empty_set ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1276,plain,
( ~ sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1261,f1270,f1273]) ).
fof(f1279,definition,
( sQ14_spl
<=> in(sK2_skl(singleton(empty_set),empty_set),singleton(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1281,plain,
( sQ14_spl
| ~ in(sK2_skl(singleton(empty_set),empty_set),singleton(empty_set)) ),
inference(component_clause,[status(thm)],[f1279]) ).
fof(f1282,definition,
( sQ15_spl
<=> subset(sK2_skl(singleton(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1285,plain,
( ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f1266,f1279,f1282]) ).
fof(f1294,plain,
( sQ1_spl
| ~ subset(empty_set,powerset(empty_set))
| ~ subset(powerset(empty_set),empty_set) ),
inference(resolution,[status(thm)],[f305,f83]) ).
fof(f1297,plain,
( sQ1_spl
| ~ subset(sK2_skl(empty_set,empty_set),empty_set)
| ~ in(sK2_skl(empty_set,empty_set),empty_set) ),
inference(resolution,[status(thm)],[f305,f101]) ).
fof(f1301,definition,
( sQ16_spl
<=> subset(powerset(empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1304,definition,
( sQ17_spl
<=> subset(empty_set,powerset(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1307,plain,
( sQ1_spl
| ~ sQ17_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f1294,f1301,f1304,f303]) ).
fof(f1308,definition,
( sQ18_spl
<=> in(sK2_skl(empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1311,definition,
( sQ19_spl
<=> subset(sK2_skl(empty_set,empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1314,plain,
( sQ1_spl
| ~ sQ19_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1297,f1308,f1311,f303]) ).
fof(f1316,plain,
( sQ0_spl
| set_difference(powerset(empty_set),singleton(empty_set)) != empty_set ),
inference(resolution,[status(thm)],[f302,f175]) ).
fof(f1329,plain,
( sQ14_spl
| subset(sK2_skl(singleton(empty_set),empty_set),empty_set)
| singleton(empty_set) = powerset(empty_set) ),
inference(resolution,[status(thm)],[f1281,f102]) ).
fof(f1332,definition,
( sQ20_spl
<=> singleton(empty_set) = powerset(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1333,plain,
( ~ sQ20_spl
| singleton(empty_set) = powerset(empty_set) ),
inference(component_clause,[status(thm)],[f1332]) ).
fof(f1335,plain,
( sQ14_spl
| sQ15_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1329,f1332,f1282,f1279]) ).
fof(f1336,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1333,f202]) ).
fof(f1337,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1336]) ).
fof(f1338,plain,
( sQ12_spl
| sK0_skl(powerset(empty_set),empty_set) = empty_set
| powerset(empty_set) = singleton(empty_set) ),
inference(resolution,[status(thm)],[f1272,f90]) ).
fof(f1339,plain,
( sQ12_spl
| ~ subset(sK0_skl(powerset(empty_set),empty_set),empty_set) ),
inference(resolution,[status(thm)],[f1272,f270]) ).
fof(f1342,plain,
( sQ12_spl
| sQ13_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1338,f1332,f1273,f1270]) ).
fof(f1346,plain,
( sQ12_spl
| ~ sQ13_spl
| ~ subset(empty_set,empty_set) ),
inference(backward_demodulation,[status(thm)],[f1274,f1339]) ).
fof(f1348,plain,
( sQ12_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1346,f214]) ).
fof(f1349,plain,
( sQ12_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f1348]) ).
fof(f1352,plain,
( sQ13_spl
| ~ subset(empty_set,sK0_skl(powerset(empty_set),empty_set))
| ~ subset(sK0_skl(powerset(empty_set),empty_set),empty_set) ),
inference(resolution,[status(thm)],[f1275,f83]) ).
fof(f1362,definition,
( sQ22_spl
<=> subset(sK0_skl(powerset(empty_set),empty_set),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1364,plain,
( sQ22_spl
| ~ subset(sK0_skl(powerset(empty_set),empty_set),empty_set) ),
inference(component_clause,[status(thm)],[f1362]) ).
fof(f1365,definition,
( sQ23_spl
<=> subset(empty_set,sK0_skl(powerset(empty_set),empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1367,plain,
( sQ23_spl
| ~ subset(empty_set,sK0_skl(powerset(empty_set),empty_set)) ),
inference(component_clause,[status(thm)],[f1365]) ).
fof(f1368,plain,
( sQ13_spl
| ~ sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f1352,f1362,f1365,f1273]) ).
fof(f1390,plain,
( sQ0_spl
| ~ subset(empty_set,set_difference(powerset(empty_set),singleton(empty_set)))
| ~ subset(set_difference(powerset(empty_set),singleton(empty_set)),empty_set) ),
inference(resolution,[status(thm)],[f1316,f83]) ).
fof(f1396,definition,
( sQ24_spl
<=> subset(set_difference(powerset(empty_set),singleton(empty_set)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f1399,definition,
( sQ25_spl
<=> subset(empty_set,set_difference(powerset(empty_set),singleton(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ0_spl
| ~ sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f1390,f1396,f1399,f300]) ).
fof(f1411,plain,
( sQ22_spl
| ~ in(sK0_skl(powerset(empty_set),empty_set),powerset(empty_set)) ),
inference(resolution,[status(thm)],[f1364,f269]) ).
fof(f1413,plain,
( sQ22_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f1411,f1270,f1362]) ).
fof(f1414,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1367,f214]) ).
fof(f1415,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1414]) ).
fof(f1416,plain,
$false,
inference(sat_refutation,[status(thm)],[f306,f313,f315,f579,f636,f818,f1260,f1276,f1285,f1307,f1314,f1335,f1337,f1342,f1349,f1368,f1402,f1413,f1415]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU147+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.58 % Computer : n008.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Mon Sep 21 05:53:40 UTC 2026
% 0.11/0.58 % CPUTime :
% 0.11/0.60 % Drodi V4.1.1
% 0.15/0.71 % Refutation found
% 0.15/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.74 % Elapsed time: 0.139771 seconds
% 0.15/0.74 % CPU time: 0.788718 seconds
% 0.15/0.74 % Total memory used: 117.452 MB
% 0.15/0.74 % Net memory used: 115.833 MB
%------------------------------------------------------------------------------