%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU101+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:13 PM UTC 2026
% Result : Theorem 0.20s 10.55s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 26
% Syntax : Number of formulae : 116 ( 8 unt; 17 def)
% Number of atoms : 344 ( 2 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 369 ( 141 ~; 151 |; 46 &)
% ( 23 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 18 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 107 ( 93 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [A] :
( preboolean(A)
=> ( diff_closed(A)
& cup_closed(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A] :
( ( diff_closed(A)
& cup_closed(A) )
=> preboolean(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] :
( cup_closed(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> in(set_union2(B,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] :
( diff_closed(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> in(set_difference(B,C),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B] :
( ~ empty(A)
=> ~ empty(set_union2(B,A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
? [A] :
( preboolean(A)
& diff_closed(A)
& cap_closed(A)
& cup_closed(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
? [B] :
( empty(B)
& element(B,powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,conjecture,
! [A] :
( preboolean(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
~ ! [A] :
( preboolean(A)
<=> ! [B,C] :
( ( in(C,A)
& in(B,A) )
=> ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f30,axiom,
! [A] : set_union2(A,empty_set) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,plain,
! [A] :
( ( diff_closed(A)
& cup_closed(A) )
| ~ preboolean(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f46,plain,
! [X0] :
( cup_closed(X0)
| ~ preboolean(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0] :
( diff_closed(X0)
| ~ preboolean(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f50,plain,
! [A] :
( preboolean(A)
| ~ diff_closed(A)
| ~ cup_closed(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f51,plain,
! [X0] :
( preboolean(X0)
| ~ diff_closed(X0)
| ~ cup_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
! [A] :
( cup_closed(A)
<=> ! [B,C] :
( in(set_union2(B,C),A)
| ~ in(C,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f54,plain,
! [A] :
( ( ? [B,C] :
( ~ in(set_union2(B,C),A)
& in(C,A)
& in(B,A) )
| cup_closed(A) )
& ( ! [B,C] :
( in(set_union2(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ cup_closed(A) ) ),
inference(NNF_transformation,[status(thm)],[f53]) ).
fof(f55,plain,
( ! [A] :
( ? [B,C] :
( ~ in(set_union2(B,C),A)
& in(C,A)
& in(B,A) )
| cup_closed(A) )
& ! [A] :
( ! [B,C] :
( in(set_union2(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ cup_closed(A) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
( ! [A] :
( ( ~ in(set_union2(sK0_skl(A),sK1_skl(A)),A)
& in(sK1_skl(A),A)
& in(sK0_skl(A),A) )
| cup_closed(A) )
& ! [A] :
( ! [B,C] :
( in(set_union2(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ cup_closed(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(B,sK0_skl(A)),skolemize(C,sK1_skl(A))],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( in(set_union2(X1,X2),X0)
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ cup_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [X0] :
( in(sK0_skl(X0),X0)
| cup_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f59,plain,
! [X0] :
( in(sK1_skl(X0),X0)
| cup_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f60,plain,
! [X0] :
( ~ in(set_union2(sK0_skl(X0),sK1_skl(X0)),X0)
| cup_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f61,plain,
! [A] :
( diff_closed(A)
<=> ! [B,C] :
( in(set_difference(B,C),A)
| ~ in(C,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f62,plain,
! [A] :
( ( ? [B,C] :
( ~ in(set_difference(B,C),A)
& in(C,A)
& in(B,A) )
| diff_closed(A) )
& ( ! [B,C] :
( in(set_difference(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ diff_closed(A) ) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
( ! [A] :
( ? [B,C] :
( ~ in(set_difference(B,C),A)
& in(C,A)
& in(B,A) )
| diff_closed(A) )
& ! [A] :
( ! [B,C] :
( in(set_difference(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ diff_closed(A) ) ),
inference(miniscoping,[status(thm)],[f62]) ).
fof(f64,plain,
( ! [A] :
( ( ~ in(set_difference(sK2_skl(A),sK3_skl(A)),A)
& in(sK3_skl(A),A)
& in(sK2_skl(A),A) )
| diff_closed(A) )
& ! [A] :
( ! [B,C] :
( in(set_difference(B,C),A)
| ~ in(C,A)
| ~ in(B,A) )
| ~ diff_closed(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(B,sK2_skl(A)),skolemize(C,sK3_skl(A))],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( in(set_difference(X1,X2),X0)
| ~ in(X2,X0)
| ~ in(X1,X0)
| ~ diff_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0] :
( in(sK2_skl(X0),X0)
| diff_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f67,plain,
! [X0] :
( in(sK3_skl(X0),X0)
| diff_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f68,plain,
! [X0] :
( ~ in(set_difference(sK2_skl(X0),sK3_skl(X0)),X0)
| diff_closed(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f84,plain,
! [A,B] :
( ~ empty(set_union2(B,A))
| empty(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f85,plain,
! [A] :
( ! [B] : ~ empty(set_union2(B,A))
| empty(A) ),
inference(miniscoping,[status(thm)],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( ~ empty(set_union2(X1,X0))
| empty(X0) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f94,plain,
( preboolean(sK6_skl)
& diff_closed(sK6_skl)
& cap_closed(sK6_skl)
& cup_closed(sK6_skl)
& ~ empty(sK6_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f19]) ).
fof(f96,plain,
cup_closed(sK6_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
diff_closed(sK6_skl),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f117,plain,
! [A] :
( empty(sK10_skl(A))
& element(sK10_skl(A),powerset(A)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f23]) ).
fof(f119,plain,
! [X0] : empty(sK10_skl(X0)),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f134,plain,
? [A] :
( preboolean(A)
<~> ! [B,C] :
( ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) )
| ~ in(C,A)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f135,plain,
? [A] :
( ( ? [B,C] :
( ( ~ in(set_difference(B,C),A)
| ~ in(set_union2(B,C),A) )
& in(C,A)
& in(B,A) )
| ~ preboolean(A) )
& ( ! [B,C] :
( ( in(set_difference(B,C),A)
& in(set_union2(B,C),A) )
| ~ in(C,A)
| ~ in(B,A) )
| preboolean(A) ) ),
inference(NNF_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
( ( ( ( ~ in(set_difference(sK15_skl,sK16_skl),sK14_skl)
| ~ in(set_union2(sK15_skl,sK16_skl),sK14_skl) )
& in(sK16_skl,sK14_skl)
& in(sK15_skl,sK14_skl) )
| ~ preboolean(sK14_skl) )
& ( ! [B,C] :
( ( in(set_difference(B,C),sK14_skl)
& in(set_union2(B,C),sK14_skl) )
| ~ in(C,sK14_skl)
| ~ in(B,sK14_skl) )
| preboolean(sK14_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(A,sK14_skl),skolemize(B,sK15_skl),skolemize(C,sK16_skl)],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( in(set_union2(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl)
| preboolean(sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( in(set_difference(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl)
| preboolean(sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f139,plain,
( in(sK15_skl,sK14_skl)
| ~ preboolean(sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f140,plain,
( in(sK16_skl,sK14_skl)
| ~ preboolean(sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f141,plain,
( ~ in(set_difference(sK15_skl,sK16_skl),sK14_skl)
| ~ in(set_union2(sK15_skl,sK16_skl),sK14_skl)
| ~ preboolean(sK14_skl) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f142,plain,
! [X0] : set_union2(X0,empty_set) = X0,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f167,definition,
( sQ0_spl
<=> preboolean(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f170,definition,
! [X0,X1] :
( sQ1_spl
<=> ( in(set_union2(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f171,plain,
! [X0,X1] :
( ~ sQ1_spl
| in(set_union2(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f170]) ).
fof(f173,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f137,f167,f170]) ).
fof(f174,definition,
! [X0,X1] :
( sQ2_spl
<=> ( in(set_difference(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f175,plain,
! [X0,X1] :
( ~ sQ2_spl
| in(set_difference(X0,X1),sK14_skl)
| ~ in(X1,sK14_skl)
| ~ in(X0,sK14_skl) ),
inference(component_clause,[status(thm)],[f174]) ).
fof(f177,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f138,f167,f174]) ).
fof(f178,definition,
( sQ3_spl
<=> in(sK15_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f181,plain,
( sQ3_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f139,f167,f178]) ).
fof(f182,definition,
( sQ4_spl
<=> in(sK16_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f185,plain,
( sQ4_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f140,f167,f182]) ).
fof(f186,definition,
( sQ5_spl
<=> in(set_union2(sK15_skl,sK16_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f188,plain,
( sQ5_spl
| ~ in(set_union2(sK15_skl,sK16_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f186]) ).
fof(f189,definition,
( sQ6_spl
<=> in(set_difference(sK15_skl,sK16_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ6_spl
| ~ in(set_difference(sK15_skl,sK16_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f189]) ).
fof(f192,plain,
( ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f141,f167,f186,f189]) ).
fof(f220,plain,
( sQ5_spl
| ~ in(sK16_skl,sK14_skl)
| ~ in(sK15_skl,sK14_skl)
| ~ cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f188,f57]) ).
fof(f221,definition,
( sQ9_spl
<=> cup_closed(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( sQ9_spl
| ~ cup_closed(sK14_skl) ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f224,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f220,f221,f178,f182,f186]) ).
fof(f231,plain,
( preboolean(sK6_skl)
| ~ cup_closed(sK6_skl) ),
inference(resolution,[status(thm)],[f98,f51]) ).
fof(f232,definition,
( sQ10_spl
<=> cup_closed(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( sQ10_spl
| ~ cup_closed(sK6_skl) ),
inference(component_clause,[status(thm)],[f232]) ).
fof(f235,definition,
( sQ11_spl
<=> preboolean(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f238,plain,
( sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f231,f232,f235]) ).
fof(f239,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f234,f96]) ).
fof(f240,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f239]) ).
fof(f246,plain,
( sQ9_spl
| ~ preboolean(sK14_skl) ),
inference(resolution,[status(thm)],[f223,f46]) ).
fof(f247,plain,
( sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f246,f167,f221]) ).
fof(f254,plain,
( sQ6_spl
| ~ in(sK16_skl,sK14_skl)
| ~ in(sK15_skl,sK14_skl)
| ~ diff_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f191,f65]) ).
fof(f255,definition,
( sQ12_spl
<=> diff_closed(sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f256,plain,
( ~ sQ12_spl
| diff_closed(sK14_skl) ),
inference(component_clause,[status(thm)],[f255]) ).
fof(f257,plain,
( sQ12_spl
| ~ diff_closed(sK14_skl) ),
inference(component_clause,[status(thm)],[f255]) ).
fof(f258,plain,
( sQ6_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f254,f255,f178,f182,f189]) ).
fof(f264,plain,
( sQ12_spl
| ~ preboolean(sK14_skl) ),
inference(resolution,[status(thm)],[f257,f47]) ).
fof(f265,plain,
( sQ12_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f264,f167,f255]) ).
fof(f266,plain,
( ~ sQ1_spl
| cup_closed(sK14_skl)
| ~ in(sK1_skl(sK14_skl),sK14_skl)
| ~ in(sK0_skl(sK14_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f171,f60]) ).
fof(f272,definition,
( sQ13_spl
<=> in(sK0_skl(sK14_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( sQ13_spl
| ~ in(sK0_skl(sK14_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,definition,
( sQ14_spl
<=> in(sK1_skl(sK14_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f277,plain,
( sQ14_spl
| ~ in(sK1_skl(sK14_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f275]) ).
fof(f278,plain,
( ~ sQ1_spl
| sQ9_spl
| ~ sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f266,f272,f275,f221,f170]) ).
fof(f280,plain,
( sQ14_spl
| cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f277,f59]) ).
fof(f281,plain,
( ~ sQ2_spl
| diff_closed(sK14_skl)
| ~ in(sK3_skl(sK14_skl),sK14_skl)
| ~ in(sK2_skl(sK14_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f175,f68]) ).
fof(f284,definition,
( sQ15_spl
<=> in(sK2_skl(sK14_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( sQ15_spl
| ~ in(sK2_skl(sK14_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,definition,
( sQ16_spl
<=> in(sK3_skl(sK14_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f289,plain,
( sQ16_spl
| ~ in(sK3_skl(sK14_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,plain,
( ~ sQ2_spl
| sQ12_spl
| ~ sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f281,f284,f287,f255,f174]) ).
fof(f312,plain,
( sQ16_spl
| diff_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f289,f67]) ).
fof(f313,plain,
( sQ16_spl
| preboolean(sK14_skl)
| ~ cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f312,f51]) ).
fof(f314,plain,
( sQ16_spl
| sQ0_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f313,f221,f167,f287]) ).
fof(f319,plain,
( sQ15_spl
| diff_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f286,f66]) ).
fof(f324,plain,
( sQ15_spl
| preboolean(sK14_skl)
| ~ cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f319,f51]) ).
fof(f325,plain,
( sQ15_spl
| sQ0_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f324,f221,f167,f284]) ).
fof(f326,plain,
( sQ14_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f280,f221,f275]) ).
fof(f327,plain,
( ~ sQ12_spl
| preboolean(sK14_skl)
| ~ cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f256,f51]) ).
fof(f328,plain,
( ~ sQ12_spl
| sQ0_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f327,f221,f167,f255]) ).
fof(f370,plain,
! [X0] :
( ~ empty(X0)
| empty(empty_set) ),
inference(paramodulation,[status(thm)],[f142,f86]) ).
fof(f390,definition,
( sQ21_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f393,definition,
! [X0] :
( sQ22_spl
<=> ~ empty(X0) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f394,plain,
! [X0] :
( ~ sQ22_spl
| ~ empty(X0) ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f396,plain,
( sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f370,f390,f393]) ).
fof(f400,plain,
( ~ sQ22_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f119,f394]) ).
fof(f404,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f400]) ).
fof(f452,plain,
( sQ13_spl
| cup_closed(sK14_skl) ),
inference(resolution,[status(thm)],[f274,f58]) ).
fof(f453,plain,
( sQ13_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f452,f221,f272]) ).
fof(f454,plain,
$false,
inference(sat_refutation,[status(thm)],[f173,f177,f181,f185,f192,f224,f238,f240,f247,f258,f265,f278,f290,f314,f325,f326,f328,f396,f404,f453]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU101+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/10.48 % Computer : n003.cluster.edu
% 0.17/10.48 % Model : x86_64 x86_64
% 0.17/10.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.48 % Memory : 8046.5625MB
% 0.17/10.48 % OS : Linux 6.8.0-71-generic
% 0.17/10.48 % CPULimit : 300
% 0.17/10.48 % WCLimit : 300
% 0.17/10.48 % DateTime : Mon Sep 21 05:52:26 UTC 2026
% 0.17/10.49 % CPUTime :
% 0.20/10.50 % Drodi V4.1.1
% 0.20/10.55 % Refutation found
% 0.20/10.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/10.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/10.59 % Elapsed time: 0.084862 seconds
% 0.20/10.59 % CPU time: 0.242573 seconds
% 0.20/10.59 % Total memory used: 75.914 MB
% 0.20/10.59 % Net memory used: 75.787 MB
%------------------------------------------------------------------------------