%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM586+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 01:41:05 PM UTC 2026
% Result : Theorem 79.08s 10.47s
% Output : CNFRefutation 47.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 57 ( 10 unt; 6 def)
% Number of atoms : 190 ( 44 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 220 ( 87 ~; 85 |; 33 &)
% ( 9 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 6 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-4 aty)
% Number of variables : 70 ( 60 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [W0] :
( aFunction0(W0)
=> aSet0(szDzozmdt0(W0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,definition,
! [W0] :
( aFunction0(W0)
=> ! [W1] :
( aSubsetOf0(W1,szDzozmdt0(W0))
=> ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( ! [W1] :
( ( aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
& aSet0(W1) )
=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) ) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,hypothesis,
aElementOf0(xi,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,hypothesis,
aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,conjecture,
? [W0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0) = xx
& aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
~ ? [W0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0) = xx
& aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ),
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f125,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f126,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f299,plain,
! [W0] :
( aSet0(szDzozmdt0(W0))
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f300,plain,
! [X0] :
( aSet0(szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f316,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( W2 = sdtlcdtrc0(W0,W1)
<=> ( ! [W3] :
( aElementOf0(W3,W2)
<=> ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) ) )
& aSet0(W2) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f317,plain,
! [W0] :
( ! [W1] :
( ! [W2] :
( ( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ( ( ! [W3] :
( ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(NNF_transformation,[status(thm)],[f316]) ).
fof(f318,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ? [W3] :
( ( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ? [W4] :
( sdtlpdtrp0(W0,W4) = W3
& aElementOf0(W4,W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(miniscoping,[status(thm)],[f317]) ).
fof(f319,plain,
! [W0] :
( ! [W1] :
( ( ! [W2] :
( ( ( ( sdtlpdtrp0(W0,sK15_skl(W2,W1,W0)) = sK14_skl(W2,W1,W0)
& aElementOf0(sK15_skl(W2,W1,W0),W1) )
| aElementOf0(sK14_skl(W2,W1,W0),W2) )
& ( ! [W4] :
( sdtlpdtrp0(W0,W4) != sK14_skl(W2,W1,W0)
| ~ aElementOf0(W4,W1) )
| ~ aElementOf0(sK14_skl(W2,W1,W0),W2) ) )
| ~ aSet0(W2)
| W2 = sdtlcdtrc0(W0,W1) )
& ! [W2] :
( ( ! [W3] :
( ! [W4] :
( sdtlpdtrp0(W0,W4) != W3
| ~ aElementOf0(W4,W1) )
| aElementOf0(W3,W2) )
& ! [W3] :
( ( sdtlpdtrp0(W0,sK13_skl(W3,W2,W1,W0)) = W3
& aElementOf0(sK13_skl(W3,W2,W1,W0),W1) )
| ~ aElementOf0(W3,W2) )
& aSet0(W2) )
| W2 != sdtlcdtrc0(W0,W1) ) )
| ~ aSubsetOf0(W1,szDzozmdt0(W0)) )
| ~ aFunction0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W4,sK13_skl(W3,W2,W1,W0)),skolemize(W3,sK14_skl(W2,W1,W0)),skolemize(W4,sK15_skl(W2,W1,W0))],[f318]) ).
fof(f321,plain,
! [X0,X1,X2,X3] :
( aElementOf0(sK13_skl(X3,X2,X1,X0),X1)
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f322,plain,
! [X0,X1,X2,X3] :
( sdtlpdtrp0(X0,sK13_skl(X3,X2,X1,X0)) = X3
| ~ aElementOf0(X3,X2)
| X2 != sdtlcdtrc0(X0,X1)
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f380,plain,
( ! [W0] :
( ( ! [W1] :
( sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))
| ~ aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))
| ~ aSet0(W1) )
& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)
& aFunction0(sdtlpdtrp0(xC,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xC) = szNzAzT0
& aFunction0(xC) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f383,plain,
! [X0] :
( aFunction0(sdtlpdtrp0(xC,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f384,plain,
! [X0] :
( szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f386,plain,
aElementOf0(xi,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f387,plain,
aElementOf0(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi)))),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f388,plain,
! [W0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),W0) != xx
| ~ aElementOf0(W0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ),
inference(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f389,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx
| ~ aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f428,plain,
! [X0,X1,X2] :
( aElementOf0(sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0),X1)
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f321]) ).
fof(f429,plain,
! [X0,X1,X2] :
( sdtlpdtrp0(X0,sK13_skl(X2,sdtlcdtrc0(X0,X1),X1,X0)) = X2
| ~ aElementOf0(X2,sdtlcdtrc0(X0,X1))
| ~ aSubsetOf0(X1,szDzozmdt0(X0))
| ~ aFunction0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f322]) ).
fof(f545,plain,
szDzozmdt0(sdtlpdtrp0(xC,xi)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk),
inference(resolution,[status(thm)],[f384,f386]) ).
fof(f925,definition,
( sQ71_spl
<=> aElementOf0(xi,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f927,plain,
( sQ71_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(component_clause,[status(thm)],[f925]) ).
fof(f941,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f927,f386]) ).
fof(f942,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f941]) ).
fof(f1221,plain,
! [X0] :
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),X0) != xx
| ~ aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(backward_demodulation,[status(thm)],[f545,f389]) ).
fof(f2903,plain,
! [X0] :
( ~ aElementOf0(X0,szNzAzT0)
| aSet0(szDzozmdt0(sdtlpdtrp0(xC,X0))) ),
inference(resolution,[status(thm)],[f300,f383]) ).
fof(f3452,plain,
( aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))
| ~ aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))
| ~ aFunction0(sdtlpdtrp0(xC,xi)) ),
inference(resolution,[status(thm)],[f428,f387]) ).
fof(f3453,definition,
( sQ394_spl
<=> aFunction0(sdtlpdtrp0(xC,xi)) ),
introduced(definition,[new_symbols(definition,[sQ394_spl])],[split_symbol_definition]) ).
fof(f3455,plain,
( sQ394_spl
| ~ aFunction0(sdtlpdtrp0(xC,xi)) ),
inference(component_clause,[status(thm)],[f3453]) ).
fof(f3456,definition,
( sQ395_spl
<=> aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
introduced(definition,[new_symbols(definition,[sQ395_spl])],[split_symbol_definition]) ).
fof(f3458,plain,
( sQ395_spl
| ~ aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(component_clause,[status(thm)],[f3456]) ).
fof(f3459,definition,
( sQ396_spl
<=> aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
introduced(definition,[new_symbols(definition,[sQ396_spl])],[split_symbol_definition]) ).
fof(f3460,plain,
( ~ sQ396_spl
| aElementOf0(sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))) ),
inference(component_clause,[status(thm)],[f3459]) ).
fof(f3462,plain,
( sQ396_spl
| ~ sQ395_spl
| ~ sQ394_spl ),
inference(split_clause,[status(thm)],[f3452,f3453,f3456,f3459]) ).
fof(f3463,plain,
( sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi))) = xx
| ~ aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi)))
| ~ aFunction0(sdtlpdtrp0(xC,xi)) ),
inference(resolution,[status(thm)],[f429,f387]) ).
fof(f3464,definition,
( sQ397_spl
<=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi))) = xx ),
introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition]) ).
fof(f3465,plain,
( ~ sQ397_spl
| sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi))) = xx ),
inference(component_clause,[status(thm)],[f3464]) ).
fof(f3467,plain,
( sQ397_spl
| ~ sQ395_spl
| ~ sQ394_spl ),
inference(split_clause,[status(thm)],[f3463,f3453,f3456,f3464]) ).
fof(f5454,plain,
aSet0(szDzozmdt0(sdtlpdtrp0(xC,xi))),
inference(resolution,[status(thm)],[f2903,f386]) ).
fof(f7394,plain,
( sQ394_spl
| ~ aElementOf0(xi,szNzAzT0) ),
inference(resolution,[status(thm)],[f3455,f383]) ).
fof(f7395,plain,
( sQ394_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f7394,f925,f3453]) ).
fof(f17849,plain,
aSubsetOf0(szDzozmdt0(sdtlpdtrp0(xC,xi)),szDzozmdt0(sdtlpdtrp0(xC,xi))),
inference(resolution,[status(thm)],[f5454,f126]) ).
fof(f17908,plain,
( sQ395_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17849,f3458]) ).
fof(f17909,plain,
sQ395_spl,
inference(contradiction_clause,[status(thm)],[f17908]) ).
fof(f17998,plain,
( ~ sQ396_spl
| sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK13_skl(xx,sdtlcdtrc0(sdtlpdtrp0(xC,xi),szDzozmdt0(sdtlpdtrp0(xC,xi))),szDzozmdt0(sdtlpdtrp0(xC,xi)),sdtlpdtrp0(xC,xi))) != xx ),
inference(resolution,[status(thm)],[f3460,f1221]) ).
fof(f18003,plain,
( ~ sQ396_spl
| ~ sQ397_spl
| xx != xx ),
inference(forward_demodulation,[status(thm)],[f3465,f17998]) ).
fof(f18004,plain,
( ~ sQ396_spl
| ~ sQ397_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f18003]) ).
fof(f18005,plain,
( ~ sQ396_spl
| ~ sQ397_spl ),
inference(contradiction_clause,[status(thm)],[f18004]) ).
fof(f18006,plain,
$false,
inference(sat_refutation,[status(thm)],[f942,f3462,f3467,f7395,f17909,f18005]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM586+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:40:21 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 79.08/10.47 % Refutation found
% 79.08/10.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 79.08/10.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 47.20/10.55 % Elapsed time: 10.170265 seconds
% 47.20/10.55 % CPU time: 79.979449 seconds
% 47.20/10.55 % Total memory used: 376.080 MB
% 47.20/10.55 % Net memory used: 345.750 MB
%------------------------------------------------------------------------------