%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET774+4 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:10:35 PM UTC 2026
% Result : Theorem 87.18s 11.66s
% Output : CNFRefutation 87.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 28
% Syntax : Number of formulae : 157 ( 10 unt; 22 def)
% Number of atoms : 526 ( 13 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 608 ( 239 ~; 257 |; 72 &)
% ( 30 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 21 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 235 ( 209 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,A)
=> member(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : ~ member(X,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( ( member(Y,A)
& member(X,A) )
=> ( ? [Z] :
( member(Z,Y)
& member(Z,X) )
=> X = Y ) )
& ! [X] :
( member(X,E)
=> ? [Y] :
( member(X,Y)
& member(Y,A) ) )
& ! [X] :
( member(X,A)
=> subset(X,E) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [R,E] :
( pre_order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X] :
( member(X,E)
=> apply(R,X,X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [E,X,R] :
( ( subset(X,E)
& pre_order(R,E) )
=> pre_order(R,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [E,X,R] :
( ( subset(X,E)
& pre_order(R,E) )
=> pre_order(R,X) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [A,B] :
( subset(A,B)
<=> ! [X] :
( member(X,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [A,B] :
( ( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
( ! [A,B] :
( ? [X] :
( ~ member(X,B)
& member(X,A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f22,plain,
( ! [A,B] :
( ( ~ member(sK0_skl(B,A),B)
& member(sK0_skl(B,A),A) )
| subset(A,B) )
& ! [A,B] :
( ! [X] :
( member(X,B)
| ~ member(X,A) )
| ~ subset(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X,sK0_skl(B,A))],[f21]) ).
fof(f23,plain,
! [X0,X1,X2] :
( ~ member(X2,X0)
| member(X2,X1)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( member(sK0_skl(X1,X0),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f45,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f51,plain,
! [X,A] :
( ( X != A
| member(X,singleton(A)) )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f52,plain,
( ! [X,A] :
( X != A
| member(X,singleton(A)) )
& ! [X,A] :
( X = A
| ~ member(X,singleton(A)) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f53,plain,
! [X0,X1] :
( ~ member(X1,singleton(X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( X0 != X1
| member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f80,plain,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f81,definition,
! [A,E] :
( sP0_prd(E,A)
<=> ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f112,plain,
! [R,E] :
( pre_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,E) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f113,definition,
! [R,E,X] :
( sP2_prd(X,E,R)
<=> ( apply(R,X,X)
| ~ member(X,E) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f114,plain,
! [R,E] :
( pre_order(R,E)
<=> ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP2_prd(X,E,R) ) ),
inference(formula_renaming,[status(thm)],[f112,f113]) ).
fof(f115,plain,
! [R,E] :
( ( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X] : ~ sP2_prd(X,E,R)
| pre_order(R,E) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP2_prd(X,E,R) )
| ~ pre_order(R,E) ) ),
inference(NNF_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
( ! [R,E] :
( ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X] : ~ sP2_prd(X,E,R)
| pre_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP2_prd(X,E,R) )
| ~ pre_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f115]) ).
fof(f117,plain,
( ! [R,E] :
( ( ~ apply(R,sK11_skl(E,R),sK13_skl(E,R))
& apply(R,sK12_skl(E,R),sK13_skl(E,R))
& apply(R,sK11_skl(E,R),sK12_skl(E,R))
& member(sK13_skl(E,R),E)
& member(sK12_skl(E,R),E)
& member(sK11_skl(E,R),E) )
| ~ sP2_prd(sK10_skl(E,R),E,R)
| pre_order(R,E) )
& ! [R,E] :
( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] : sP2_prd(X,E,R) )
| ~ pre_order(R,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(X,sK10_skl(E,R)),skolemize(X,sK11_skl(E,R)),skolemize(Y,sK12_skl(E,R)),skolemize(Z,sK13_skl(E,R))],[f116]) ).
fof(f118,plain,
! [X0,X1,X2] :
( sP2_prd(X2,X1,X0)
| ~ pre_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f119,plain,
! [X0,X1,X2,X3,X4] :
( ~ member(X4,X1)
| ~ member(X3,X1)
| ~ member(X2,X1)
| ~ apply(X0,X4,X3)
| ~ apply(X0,X2,X4)
| apply(X0,X2,X3)
| ~ pre_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f120,plain,
! [X0,X1] :
( pre_order(X1,X0)
| ~ sP2_prd(sK10_skl(X0,X1),X0,X1)
| member(sK11_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f121,plain,
! [X0,X1] :
( ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| member(sK12_skl(X1,X0),X1)
| pre_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f122,plain,
! [X0,X1] :
( member(sK13_skl(X0,X1),X0)
| pre_order(X1,X0)
| ~ sP2_prd(sK10_skl(X0,X1),X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f123,plain,
! [X0,X1] :
( apply(X1,sK11_skl(X0,X1),sK12_skl(X0,X1))
| pre_order(X1,X0)
| ~ sP2_prd(sK10_skl(X0,X1),X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f124,plain,
! [X0,X1] :
( pre_order(X0,X1)
| ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| apply(X0,sK12_skl(X1,X0),sK13_skl(X1,X0)) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f125,plain,
! [X0,X1] :
( ~ sP2_prd(sK10_skl(X1,X0),X1,X0)
| ~ apply(X0,sK11_skl(X1,X0),sK13_skl(X1,X0))
| pre_order(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f126,plain,
? [E,X,R] :
( ~ pre_order(R,X)
& subset(X,E)
& pre_order(R,E) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f127,plain,
? [X,R] :
( ~ pre_order(R,X)
& ? [E] :
( subset(X,E)
& pre_order(R,E) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
( ~ pre_order(sK15_skl,sK14_skl)
& subset(sK14_skl,sK16_skl)
& pre_order(sK15_skl,sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(X,sK14_skl),skolemize(R,sK15_skl),skolemize(E,sK16_skl)],[f127]) ).
fof(f129,plain,
pre_order(sK15_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
subset(sK14_skl,sK16_skl),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
~ pre_order(sK15_skl,sK14_skl),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f132,plain,
! [A,E] :
( ( ? [X] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
& member(X,E) )
| ? [X] :
( ~ subset(X,E)
& member(X,A) )
| sP0_prd(E,A) )
& ( ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(NNF_transformation,[status(thm)],[f81]) ).
fof(f133,plain,
( ! [A,E] :
( ? [X] :
( ! [Y] :
( ~ member(X,Y)
| ~ member(Y,A) )
& member(X,E) )
| ? [X] :
( ~ subset(X,E)
& member(X,A) )
| sP0_prd(E,A) )
& ! [A,E] :
( ( ! [X] :
( ? [Y] :
( member(X,Y)
& member(Y,A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(miniscoping,[status(thm)],[f132]) ).
fof(f134,plain,
( ! [A,E] :
( ( ! [Y] :
( ~ member(sK19_skl(E,A),Y)
| ~ member(Y,A) )
& member(sK19_skl(E,A),E) )
| ( ~ subset(sK18_skl(E,A),E)
& member(sK18_skl(E,A),A) )
| sP0_prd(E,A) )
& ! [A,E] :
( ( ! [X] :
( ( member(X,sK17_skl(X,E,A))
& member(sK17_skl(X,E,A),A) )
| ~ member(X,E) )
& ! [X] :
( subset(X,E)
| ~ member(X,A) ) )
| ~ sP0_prd(E,A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(Y,sK17_skl(X,E,A)),skolemize(X,sK18_skl(E,A)),skolemize(X,sK19_skl(E,A))],[f133]) ).
fof(f135,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ sP0_prd(X2,X1)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f138,plain,
! [X0,X1] :
( member(sK19_skl(X0,X1),X0)
| sP0_prd(X0,X1)
| member(sK18_skl(X0,X1),X1) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f140,plain,
! [X0,X1] :
( sP0_prd(X0,X1)
| member(sK19_skl(X0,X1),X0)
| ~ subset(sK18_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f153,plain,
! [R,E,X] :
( ( ( ~ apply(R,X,X)
& member(X,E) )
| sP2_prd(X,E,R) )
& ( apply(R,X,X)
| ~ member(X,E)
| ~ sP2_prd(X,E,R) ) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f154,plain,
( ! [R,E,X] :
( ( ~ apply(R,X,X)
& member(X,E) )
| sP2_prd(X,E,R) )
& ! [R,E,X] :
( apply(R,X,X)
| ~ member(X,E)
| ~ sP2_prd(X,E,R) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f155,plain,
! [X0,X1,X2] :
( apply(X2,X0,X0)
| ~ member(X0,X1)
| ~ sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0,X1,X2] :
( member(X0,X1)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
! [X0,X1,X2] :
( ~ apply(X2,X0,X0)
| sP2_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f165,plain,
! [X0] : member(X0,singleton(X0)),
inference(destructive_equality_resolution,[status(thm)],[f54]) ).
fof(f168,plain,
! [X0,X1] :
( ~ subset(X1,empty_set)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f45,f23]) ).
fof(f169,plain,
! [X0,X1,X2] :
( ~ sP0_prd(empty_set,X1)
| ~ member(X2,X0)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f168,f135]) ).
fof(f176,plain,
( ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl)
| member(sK12_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f121,f131]) ).
fof(f177,definition,
( sQ0_spl
<=> member(sK12_skl(sK14_skl,sK15_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f178,plain,
( ~ sQ0_spl
| member(sK12_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,definition,
( sQ1_spl
<=> sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f182,plain,
( sQ1_spl
| ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl) ),
inference(component_clause,[status(thm)],[f180]) ).
fof(f183,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f176,f177,f180]) ).
fof(f204,plain,
( ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl)
| apply(sK15_skl,sK12_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl)) ),
inference(resolution,[status(thm)],[f124,f131]) ).
fof(f205,definition,
( sQ2_spl
<=> apply(sK15_skl,sK12_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f206,plain,
( ~ sQ2_spl
| apply(sK15_skl,sK12_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,plain,
( ~ sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f204,f205,f180]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ member(X2,X1)
| ~ member(X1,X0)
| member(sK19_skl(empty_set,X0),empty_set)
| member(sK18_skl(empty_set,X0),X0) ),
inference(resolution,[status(thm)],[f138,f169]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ~ member(X1,X2)
| member(sK18_skl(empty_set,X2),X2)
| ~ member(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f214,f45]) ).
fof(f222,plain,
( ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl)
| member(sK11_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f120,f131]) ).
fof(f223,definition,
( sQ3_spl
<=> member(sK11_skl(sK14_skl,sK15_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f226,plain,
( ~ sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f222,f223,f180]) ).
fof(f229,plain,
! [X0,X1,X2] :
( ~ member(X2,X0)
| sK18_skl(empty_set,singleton(X1)) = X1
| ~ member(X0,singleton(X1)) ),
inference(resolution,[status(thm)],[f217,f53]) ).
fof(f277,plain,
! [X0,X1] :
( sK18_skl(empty_set,singleton(X1)) = X1
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f229,f165]) ).
fof(f280,plain,
( sQ1_spl
| member(sK10_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f156,f182]) ).
fof(f300,plain,
! [X0,X1] :
( member(sK0_skl(X0,sK18_skl(X0,X1)),sK18_skl(X0,X1))
| sP0_prd(X0,X1)
| member(sK19_skl(X0,X1),X0) ),
inference(resolution,[status(thm)],[f24,f140]) ).
fof(f358,plain,
( apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK12_skl(sK14_skl,sK15_skl))
| ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f123,f131]) ).
fof(f359,definition,
( sQ4_spl
<=> apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK12_skl(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f360,plain,
( ~ sQ4_spl
| apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK12_skl(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( sQ4_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f358,f180,f359]) ).
fof(f383,plain,
! [X0,X1,X2] :
( apply(X0,X2,X2)
| ~ member(X2,X1)
| ~ pre_order(X0,X1) ),
inference(resolution,[status(thm)],[f155,f118]) ).
fof(f392,plain,
( sQ1_spl
| sK18_skl(empty_set,singleton(sK14_skl)) = sK14_skl ),
inference(resolution,[status(thm)],[f277,f280]) ).
fof(f417,plain,
( member(sK13_skl(sK14_skl,sK15_skl),sK14_skl)
| ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl) ),
inference(resolution,[status(thm)],[f122,f131]) ).
fof(f418,definition,
( sQ5_spl
<=> member(sK13_skl(sK14_skl,sK15_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f419,plain,
( ~ sQ5_spl
| member(sK13_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,plain,
( sQ5_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f417,f180,f418]) ).
fof(f424,plain,
( sQ1_spl
| sP0_prd(empty_set,singleton(sK14_skl))
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set)
| ~ subset(sK14_skl,empty_set) ),
inference(paramodulation,[status(thm)],[f392,f140]) ).
fof(f429,definition,
( sQ7_spl
<=> subset(sK14_skl,empty_set) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f432,definition,
( sQ8_spl
<=> sP0_prd(empty_set,singleton(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( ~ sQ8_spl
| sP0_prd(empty_set,singleton(sK14_skl)) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f434,plain,
( sQ8_spl
| ~ sP0_prd(empty_set,singleton(sK14_skl)) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f436,definition,
( sQ9_spl
<=> member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f437,plain,
( ~ sQ9_spl
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set) ),
inference(component_clause,[status(thm)],[f436]) ).
fof(f439,plain,
( sQ1_spl
| sQ8_spl
| sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f424,f429,f436,f432,f180]) ).
fof(f450,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,X3)
| ~ pre_order(X2,X3)
| sP2_prd(X0,X1,X2) ),
inference(resolution,[status(thm)],[f383,f157]) ).
fof(f454,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ member(sK13_skl(sK14_skl,sK15_skl),X1)
| ~ member(X0,X1)
| apply(sK15_skl,X0,sK13_skl(sK14_skl,sK15_skl))
| ~ pre_order(sK15_skl,X1)
| ~ member(sK12_skl(sK14_skl,sK15_skl),X1)
| ~ apply(sK15_skl,X0,sK12_skl(sK14_skl,sK15_skl)) ),
inference(resolution,[status(thm)],[f206,f119]) ).
fof(f465,plain,
! [X0,X1] :
( ~ sQ8_spl
| ~ member(X1,X0)
| ~ member(X0,singleton(sK14_skl)) ),
inference(resolution,[status(thm)],[f433,f169]) ).
fof(f472,plain,
( ~ sQ0_spl
| sK14_skl = sK18_skl(empty_set,singleton(sK14_skl)) ),
inference(resolution,[status(thm)],[f178,f277]) ).
fof(f485,plain,
! [X0] :
( ~ sQ8_spl
| ~ member(X0,sK14_skl) ),
inference(resolution,[status(thm)],[f465,f165]) ).
fof(f531,definition,
! [X0] :
( sQ13_spl
<=> ~ member(X0,singleton(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f532,plain,
! [X0] :
( ~ sQ13_spl
| ~ member(X0,singleton(sK14_skl)) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f560,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f437,f45]) ).
fof(f561,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f560]) ).
fof(f563,definition,
( sQ17_spl
<=> member(sK10_skl(sK14_skl,sK15_skl),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f565,plain,
( sQ17_spl
| ~ member(sK10_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(component_clause,[status(thm)],[f563]) ).
fof(f577,plain,
( sQ8_spl
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set)
| member(sK18_skl(empty_set,singleton(sK14_skl)),singleton(sK14_skl)) ),
inference(resolution,[status(thm)],[f434,f138]) ).
fof(f578,definition,
( sQ19_spl
<=> member(sK18_skl(empty_set,singleton(sK14_skl)),singleton(sK14_skl)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ8_spl
| sQ9_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f577,f578,f436,f432]) ).
fof(f612,plain,
( sQ1_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f485]) ).
fof(f613,plain,
( sQ1_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f612]) ).
fof(f614,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f485]) ).
fof(f615,plain,
( ~ sQ5_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f614]) ).
fof(f626,plain,
( ~ sQ13_spl
| $false ),
inference(resolution,[status(thm)],[f532,f165]) ).
fof(f628,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f626]) ).
fof(f639,plain,
( ~ sQ0_spl
| sP0_prd(empty_set,singleton(sK14_skl))
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set)
| ~ subset(sK14_skl,empty_set) ),
inference(paramodulation,[status(thm)],[f472,f140]) ).
fof(f641,plain,
( ~ sQ0_spl
| sQ8_spl
| sQ9_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f639,f429,f436,f432,f177]) ).
fof(f787,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ2_spl
| ~ member(sK12_skl(sK14_skl,sK15_skl),X0)
| ~ member(sK13_skl(sK14_skl,sK15_skl),X0)
| apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl))
| ~ pre_order(sK15_skl,X0)
| ~ member(sK11_skl(sK14_skl,sK15_skl),X0) ),
inference(resolution,[status(thm)],[f454,f360]) ).
fof(f790,definition,
! [X0] :
( sQ21_spl
<=> ( ~ member(sK12_skl(sK14_skl,sK15_skl),X0)
| ~ member(sK13_skl(sK14_skl,sK15_skl),X0)
| ~ pre_order(sK15_skl,X0)
| ~ member(sK11_skl(sK14_skl,sK15_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f791,plain,
! [X0] :
( ~ sQ21_spl
| ~ member(sK11_skl(sK14_skl,sK15_skl),X0)
| ~ member(sK12_skl(sK14_skl,sK15_skl),X0)
| ~ pre_order(sK15_skl,X0)
| ~ member(sK13_skl(sK14_skl,sK15_skl),X0) ),
inference(component_clause,[status(thm)],[f790]) ).
fof(f793,definition,
( sQ22_spl
<=> apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f794,plain,
( ~ sQ22_spl
| apply(sK15_skl,sK11_skl(sK14_skl,sK15_skl),sK13_skl(sK14_skl,sK15_skl)) ),
inference(component_clause,[status(thm)],[f793]) ).
fof(f796,plain,
( ~ sQ4_spl
| ~ sQ2_spl
| sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f787,f790,f793,f205,f359]) ).
fof(f977,plain,
( ~ sQ0_spl
| member(sK0_skl(empty_set,sK14_skl),sK18_skl(empty_set,singleton(sK14_skl)))
| sP0_prd(empty_set,singleton(sK14_skl))
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set) ),
inference(paramodulation,[status(thm)],[f472,f300]) ).
fof(f979,plain,
( ~ sQ0_spl
| member(sK0_skl(empty_set,sK18_skl(empty_set,singleton(sK14_skl))),sK14_skl)
| sP0_prd(empty_set,singleton(sK14_skl))
| member(sK19_skl(empty_set,singleton(sK14_skl)),empty_set) ),
inference(paramodulation,[status(thm)],[f472,f300]) ).
fof(f980,definition,
( sQ25_spl
<=> member(sK0_skl(empty_set,sK14_skl),sK18_skl(empty_set,singleton(sK14_skl))) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f983,plain,
( ~ sQ0_spl
| sQ25_spl
| sQ8_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f977,f436,f432,f980,f177]) ).
fof(f984,definition,
( sQ26_spl
<=> member(sK0_skl(empty_set,sK18_skl(empty_set,singleton(sK14_skl))),sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f987,plain,
( ~ sQ0_spl
| sQ26_spl
| sQ8_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f979,f436,f432,f984,f177]) ).
fof(f1050,plain,
! [X0] :
( sQ1_spl
| ~ member(sK10_skl(sK14_skl,sK15_skl),X0)
| ~ pre_order(sK15_skl,X0) ),
inference(resolution,[status(thm)],[f182,f450]) ).
fof(f1139,plain,
( ~ sQ21_spl
| ~ member(sK11_skl(sK14_skl,sK15_skl),sK16_skl)
| ~ member(sK13_skl(sK14_skl,sK15_skl),sK16_skl)
| ~ member(sK12_skl(sK14_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f791,f129]) ).
fof(f1145,definition,
( sQ27_spl
<=> member(sK12_skl(sK14_skl,sK15_skl),sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1147,plain,
( sQ27_spl
| ~ member(sK12_skl(sK14_skl,sK15_skl),sK16_skl) ),
inference(component_clause,[status(thm)],[f1145]) ).
fof(f1148,definition,
( sQ28_spl
<=> member(sK13_skl(sK14_skl,sK15_skl),sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ28_spl
| ~ member(sK13_skl(sK14_skl,sK15_skl),sK16_skl) ),
inference(component_clause,[status(thm)],[f1148]) ).
fof(f1151,definition,
( sQ29_spl
<=> member(sK11_skl(sK14_skl,sK15_skl),sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1153,plain,
( sQ29_spl
| ~ member(sK11_skl(sK14_skl,sK15_skl),sK16_skl) ),
inference(component_clause,[status(thm)],[f1151]) ).
fof(f1154,plain,
( ~ sQ21_spl
| ~ sQ29_spl
| ~ sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f1139,f1145,f1148,f1151,f790]) ).
fof(f1155,plain,
( sQ17_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f565,f280]) ).
fof(f1156,plain,
( sQ17_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1155]) ).
fof(f1246,plain,
! [X0] :
( sQ29_spl
| ~ member(sK11_skl(sK14_skl,sK15_skl),X0)
| ~ subset(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1153,f23]) ).
fof(f1263,plain,
! [X0] :
( sQ28_spl
| ~ member(sK13_skl(sK14_skl,sK15_skl),X0)
| ~ subset(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1150,f23]) ).
fof(f1289,plain,
( sQ1_spl
| ~ member(sK10_skl(sK14_skl,sK15_skl),sK16_skl) ),
inference(resolution,[status(thm)],[f1050,f129]) ).
fof(f1295,plain,
! [X0] :
( sQ27_spl
| ~ subset(X0,sK16_skl)
| ~ member(sK12_skl(sK14_skl,sK15_skl),X0) ),
inference(resolution,[status(thm)],[f1147,f23]) ).
fof(f1297,plain,
! [X0] :
( sQ1_spl
| ~ member(sK10_skl(sK14_skl,sK15_skl),X0)
| ~ subset(X0,sK16_skl) ),
inference(resolution,[status(thm)],[f1289,f23]) ).
fof(f1470,plain,
( ~ sQ22_spl
| ~ sP2_prd(sK10_skl(sK14_skl,sK15_skl),sK14_skl,sK15_skl)
| pre_order(sK15_skl,sK14_skl) ),
inference(resolution,[status(thm)],[f794,f125]) ).
fof(f1473,definition,
( sQ30_spl
<=> pre_order(sK15_skl,sK14_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1474,plain,
( ~ sQ30_spl
| pre_order(sK15_skl,sK14_skl) ),
inference(component_clause,[status(thm)],[f1473]) ).
fof(f1476,plain,
( ~ sQ22_spl
| ~ sQ1_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f1470,f1473,f180,f793]) ).
fof(f1478,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1474,f131]) ).
fof(f1479,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1478]) ).
fof(f1570,plain,
( sQ29_spl
| ~ member(sK11_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f1246,f130]) ).
fof(f1680,plain,
( sQ28_spl
| ~ member(sK13_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f1263,f130]) ).
fof(f1688,plain,
( sQ27_spl
| ~ member(sK12_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f1295,f130]) ).
fof(f1692,plain,
( sQ1_spl
| ~ member(sK10_skl(sK14_skl,sK15_skl),sK14_skl) ),
inference(resolution,[status(thm)],[f1297,f130]) ).
fof(f1696,plain,
( sQ1_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1692,f563,f180]) ).
fof(f1697,plain,
( sQ29_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1570,f223,f1151]) ).
fof(f1698,plain,
( sQ27_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1688,f177,f1145]) ).
fof(f1819,plain,
( sQ28_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1680,f419]) ).
fof(f1820,plain,
( sQ28_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1819]) ).
fof(f1821,plain,
$false,
inference(sat_refutation,[status(thm)],[f183,f208,f226,f362,f421,f439,f561,f581,f613,f615,f628,f641,f796,f983,f987,f1154,f1156,f1476,f1479,f1696,f1697,f1698,f1820]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET774+4 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n005.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 05:37:04 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 87.18/11.66 % Refutation found
% 87.18/11.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 87.18/11.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 63.34/11.71 % Elapsed time: 11.256867 seconds
% 63.34/11.71 % CPU time: 88.702770 seconds
% 63.34/11.71 % Total memory used: 359.812 MB
% 63.34/11.71 % Net memory used: 301.414 MB
%------------------------------------------------------------------------------