%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEV517+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:32:58 PM UTC 2026
% Result : Theorem 17.72s 2.89s
% Output : CNFRefutation 17.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 76 ( 7 unt; 6 def)
% Number of atoms : 293 ( 16 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 352 ( 135 ~; 128 |; 70 &)
% ( 13 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 190 ( 164 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X,A,B] :
( member(X,intersection(A,B))
<=> ( member(X,B)
& member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X,A,B] :
( member(X,union(A,B))
<=> ( member(X,B)
| member(X,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [B,A,E] :
( member(B,difference(E,A))
<=> ( ~ member(B,A)
& member(B,E) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,A] :
( member(X,singleton(A))
<=> X = A ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f20,conjecture,
! [X,A,B,P] :
( ( partition(P,A)
& member(X,difference(A,B)) )
=> ? [S] :
( member(X,S)
& member(S,difference(P,singleton(B))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
~ ! [X,A,B,P] :
( ( partition(P,A)
& member(X,difference(A,B)) )
=> ? [S] :
( member(X,S)
& member(S,difference(P,singleton(B))) ) ),
inference(negated_conjecture,[status(cth)],[f20]) ).
fof(f38,plain,
! [X,A,B] :
( ( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f39,plain,
( ! [X,A,B] :
( ~ member(X,B)
| ~ member(X,A)
| member(X,intersection(A,B)) )
& ! [X,A,B] :
( ( member(X,B)
& member(X,A) )
| ~ member(X,intersection(A,B)) ) ),
inference(miniscoping,[status(thm)],[f38]) ).
fof(f41,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f43,plain,
! [X,A,B] :
( ( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f44,plain,
( ! [X,A,B] :
( ( ~ member(X,B)
& ~ member(X,A) )
| member(X,union(A,B)) )
& ! [X,A,B] :
( member(X,B)
| member(X,A)
| ~ member(X,union(A,B)) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f45,plain,
! [X0,X1,X2] :
( member(X0,X2)
| member(X0,X1)
| ~ member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f47,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| member(X0,union(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f49,plain,
! [B,A,E] :
( ( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f50,plain,
( ! [B,A,E] :
( member(B,A)
| ~ member(B,E)
| member(B,difference(E,A)) )
& ! [B,A,E] :
( ( ~ member(B,A)
& member(B,E) )
| ~ member(B,difference(E,A)) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ member(X0,X2)
| ~ member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f53,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,X1)
| member(X0,difference(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f54,plain,
! [X,A] :
( ( X != A
| member(X,singleton(A)) )
& ( X = A
| ~ member(X,singleton(A)) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f55,plain,
( ! [X,A] :
( X != A
| member(X,singleton(A)) )
& ! [X,A] :
( X = A
| ~ member(X,singleton(A)) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f56,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f83,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(f84,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(f85,plain,
! [A,E] :
( partition(A,E)
<=> ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) ) ),
inference(formula_renaming,[status(thm)],[f83,f84]) ).
fof(f86,plain,
! [A,E] :
( ( ? [X,Y] :
( X != Y
& ? [Z] :
( member(Z,Y)
& member(Z,X) )
& member(Y,A)
& member(X,A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(NNF_transformation,[status(thm)],[f85]) ).
fof(f87,plain,
( ! [A,E] :
( ? [X,Y] :
( X != Y
& ? [Z] :
( member(Z,Y)
& member(Z,X) )
& member(Y,A)
& member(X,A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ! [A,E] :
( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
( ! [A,E] :
( ( sK4_skl(E,A) != sK5_skl(E,A)
& member(sK6_skl(E,A),sK5_skl(E,A))
& member(sK6_skl(E,A),sK4_skl(E,A))
& member(sK5_skl(E,A),A)
& member(sK4_skl(E,A),A) )
| ~ sP0_prd(E,A)
| partition(A,E) )
& ! [A,E] :
( ( ! [X,Y] :
( X = Y
| ! [Z] :
( ~ member(Z,Y)
| ~ member(Z,X) )
| ~ member(Y,A)
| ~ member(X,A) )
& sP0_prd(E,A) )
| ~ partition(A,E) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(X,sK4_skl(E,A)),skolemize(Y,sK5_skl(E,A)),skolemize(Z,sK6_skl(E,A))],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( sP0_prd(X1,X0)
| ~ partition(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f144,plain,
? [X,A,B,P] :
( ! [S] :
( ~ member(X,S)
| ~ member(S,difference(P,singleton(B))) )
& partition(P,A)
& member(X,difference(A,B)) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f145,plain,
? [X,B,P] :
( ! [S] :
( ~ member(X,S)
| ~ member(S,difference(P,singleton(B))) )
& ? [A] :
( partition(P,A)
& member(X,difference(A,B)) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f146,plain,
( ! [S] :
( ~ member(sK18_skl,S)
| ~ member(S,difference(sK20_skl,singleton(sK19_skl))) )
& partition(sK20_skl,sK21_skl)
& member(sK18_skl,difference(sK21_skl,sK19_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(X,sK18_skl),skolemize(B,sK19_skl),skolemize(P,sK20_skl),skolemize(A,sK21_skl)],[f145]) ).
fof(f147,plain,
member(sK18_skl,difference(sK21_skl,sK19_skl)),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
partition(sK20_skl,sK21_skl),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
! [X0] :
( ~ member(sK18_skl,X0)
| ~ member(X0,difference(sK20_skl,singleton(sK19_skl))) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f150,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)],[f84]) ).
fof(f151,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)],[f150]) ).
fof(f152,plain,
( ! [A,E] :
( ( ! [Y] :
( ~ member(sK24_skl(E,A),Y)
| ~ member(Y,A) )
& member(sK24_skl(E,A),E) )
| ( ~ subset(sK23_skl(E,A),E)
& member(sK23_skl(E,A),A) )
| sP0_prd(E,A) )
& ! [A,E] :
( ( ! [X] :
( ( member(X,sK22_skl(X,E,A))
& member(sK22_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,[sK22_skl,sK23_skl,sK24_skl]),skolemize(Y,sK22_skl(X,E,A)),skolemize(X,sK23_skl(E,A)),skolemize(X,sK24_skl(E,A))],[f151]) ).
fof(f154,plain,
! [X0,X1,X2] :
( member(sK22_skl(X2,X0,X1),X1)
| ~ member(X2,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f155,plain,
! [X0,X1,X2] :
( member(X2,sK22_skl(X2,X0,X1))
| ~ member(X2,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f187,plain,
member(sK18_skl,sK21_skl),
inference(resolution,[status(thm)],[f51,f147]) ).
fof(f189,plain,
~ member(sK18_skl,sK19_skl),
inference(resolution,[status(thm)],[f52,f147]) ).
fof(f210,plain,
! [X0] :
( ~ member(sK18_skl,X0)
| member(sK18_skl,intersection(X0,sK21_skl)) ),
inference(resolution,[status(thm)],[f42,f187]) ).
fof(f216,plain,
! [X0] :
( member(sK18_skl,sK21_skl)
| ~ member(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f210,f41]) ).
fof(f219,definition,
! [X0] :
( sQ0_spl
<=> ~ member(sK18_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f220,plain,
! [X0] :
( ~ sQ0_spl
| ~ member(sK18_skl,X0) ),
inference(component_clause,[status(thm)],[f219]) ).
fof(f222,definition,
( sQ1_spl
<=> member(sK18_skl,sK21_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( ~ sQ1_spl
| member(sK18_skl,sK21_skl) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f216,f219,f222]) ).
fof(f226,plain,
( ~ sQ0_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f187,f220]) ).
fof(f232,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f226]) ).
fof(f234,plain,
! [X0] :
( member(X0,singleton(sK19_skl))
| ~ member(X0,sK20_skl)
| ~ member(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f149,f53]) ).
fof(f314,definition,
! [X0] :
( sQ3_spl
<=> member(sK18_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f315,plain,
! [X0] :
( ~ sQ3_spl
| member(sK18_skl,X0) ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f347,plain,
( ~ sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f189,f315]) ).
fof(f363,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f347]) ).
fof(f1226,plain,
! [X0,X1,X2] :
( ~ partition(X2,X1)
| member(sK22_skl(X0,X1,X2),X2)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f154,f89]) ).
fof(f1227,plain,
! [X0,X1,X2] :
( ~ partition(X2,X1)
| member(X0,sK22_skl(X0,X1,X2))
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f155,f89]) ).
fof(f1322,plain,
! [X0] :
( member(sK22_skl(X0,sK21_skl,sK20_skl),sK20_skl)
| ~ member(X0,sK21_skl) ),
inference(resolution,[status(thm)],[f1226,f148]) ).
fof(f1324,plain,
! [X0] :
( member(X0,sK22_skl(X0,sK21_skl,sK20_skl))
| ~ member(X0,sK21_skl) ),
inference(resolution,[status(thm)],[f1227,f148]) ).
fof(f1330,plain,
( ~ sQ1_spl
| member(sK18_skl,sK22_skl(sK18_skl,sK21_skl,sK20_skl)) ),
inference(resolution,[status(thm)],[f1324,f223]) ).
fof(f1333,plain,
! [X0] :
( ~ sQ1_spl
| member(sK18_skl,union(X0,sK22_skl(sK18_skl,sK21_skl,sK20_skl))) ),
inference(resolution,[status(thm)],[f1330,f47]) ).
fof(f1337,plain,
! [X0] :
( ~ sQ1_spl
| member(sK18_skl,sK22_skl(sK18_skl,sK21_skl,sK20_skl))
| member(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f1333,f45]) ).
fof(f1344,definition,
( sQ17_spl
<=> member(sK18_skl,sK22_skl(sK18_skl,sK21_skl,sK20_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1347,plain,
( ~ sQ1_spl
| sQ17_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1337,f314,f1344,f222]) ).
fof(f1469,plain,
( ~ sQ1_spl
| member(sK22_skl(sK18_skl,sK21_skl,sK20_skl),sK20_skl) ),
inference(resolution,[status(thm)],[f1322,f223]) ).
fof(f1480,plain,
( ~ sQ1_spl
| member(sK22_skl(sK18_skl,sK21_skl,sK20_skl),singleton(sK19_skl))
| ~ member(sK18_skl,sK22_skl(sK18_skl,sK21_skl,sK20_skl)) ),
inference(resolution,[status(thm)],[f1469,f234]) ).
fof(f1488,definition,
( sQ18_spl
<=> member(sK22_skl(sK18_skl,sK21_skl,sK20_skl),singleton(sK19_skl)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1489,plain,
( ~ sQ18_spl
| member(sK22_skl(sK18_skl,sK21_skl,sK20_skl),singleton(sK19_skl)) ),
inference(component_clause,[status(thm)],[f1488]) ).
fof(f1491,plain,
( ~ sQ1_spl
| sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f1480,f1344,f1488,f222]) ).
fof(f1568,plain,
( ~ sQ18_spl
| sK22_skl(sK18_skl,sK21_skl,sK20_skl) = sK19_skl ),
inference(resolution,[status(thm)],[f1489,f56]) ).
fof(f1584,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| member(sK18_skl,sK19_skl) ),
inference(backward_demodulation,[status(thm)],[f1568,f1330]) ).
fof(f1585,plain,
( ~ sQ1_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1584,f189]) ).
fof(f1586,plain,
( ~ sQ1_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f1585]) ).
fof(f1587,plain,
$false,
inference(sat_refutation,[status(thm)],[f225,f232,f363,f1347,f1491,f1586]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV517+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n004.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 07:24:05 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 17.72/2.89 % Refutation found
% 17.72/2.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.72/2.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.40/2.93 % Elapsed time: 2.579254 seconds
% 16.40/2.93 % CPU time: 20.155028 seconds
% 16.40/2.93 % Total memory used: 234.688 MB
% 16.40/2.93 % Net memory used: 212.776 MB
%------------------------------------------------------------------------------