%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM624+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 : n013.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:14 PM UTC 2026
% Result : Theorem 0.09s 0.42s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 16
% Syntax : Number of formulae : 57 ( 22 unt; 8 def)
% Number of atoms : 135 ( 38 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 133 ( 55 ~; 59 |; 9 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 10 ( 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f49,axiom,
! [W0,W1] :
( ( W1 != slcrc0
& W0 != slcrc0
& aSubsetOf0(W1,szNzAzT0)
& aSubsetOf0(W0,szNzAzT0) )
=> ( ( aElementOf0(szmzizndt0(W1),W0)
& aElementOf0(szmzizndt0(W0),W1) )
=> szmzizndt0(W0) = szmzizndt0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,hypothesis,
( xQ != slcrc0
& aSubsetOf0(xQ,xO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,hypothesis,
aSubsetOf0(xQ,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,hypothesis,
xp = szmzizndt0(xQ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,hypothesis,
xx = szmzizndt0(sdtlpdtrp0(xN,xm)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,hypothesis,
( aElementOf0(xx,xQ)
& aElementOf0(xp,sdtlpdtrp0(xN,xm)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,hypothesis,
( sdtlpdtrp0(xN,xm) != slcrc0
& xQ != slcrc0
& aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)
& aSubsetOf0(xQ,szNzAzT0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,conjecture,
xp = xx,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,negated_conjecture,
xp != xx,
inference(negated_conjecture,[status(cth)],[f121]) ).
fof(f273,plain,
! [W0,W1] :
( szmzizndt0(W0) = szmzizndt0(W1)
| ~ aElementOf0(szmzizndt0(W1),W0)
| ~ aElementOf0(szmzizndt0(W0),W1)
| W1 = slcrc0
| W0 = slcrc0
| ~ aSubsetOf0(W1,szNzAzT0)
| ~ aSubsetOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f274,plain,
! [X0,X1] :
( szmzizndt0(X0) = szmzizndt0(X1)
| ~ aElementOf0(szmzizndt0(X1),X0)
| ~ aElementOf0(szmzizndt0(X0),X1)
| X1 = slcrc0
| X0 = slcrc0
| ~ aSubsetOf0(X1,szNzAzT0)
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f455,plain,
xQ != slcrc0,
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f456,plain,
aSubsetOf0(xQ,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f458,plain,
xp = szmzizndt0(xQ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f476,plain,
xx = szmzizndt0(sdtlpdtrp0(xN,xm)),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f479,plain,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f480,plain,
aElementOf0(xx,xQ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f482,plain,
aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f484,plain,
sdtlpdtrp0(xN,xm) != slcrc0,
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f485,plain,
xp != xx,
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f571,definition,
( sQ4_spl
<=> aSubsetOf0(xQ,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( sQ4_spl
| ~ aSubsetOf0(xQ,szNzAzT0) ),
inference(component_clause,[status(thm)],[f571]) ).
fof(f574,definition,
( sQ5_spl
<=> xQ = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f575,plain,
( ~ sQ5_spl
| xQ = slcrc0 ),
inference(component_clause,[status(thm)],[f574]) ).
fof(f611,plain,
( ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f575,f455]) ).
fof(f612,plain,
~ sQ5_spl,
inference(contradiction_clause,[status(thm)],[f611]) ).
fof(f613,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f573,f456]) ).
fof(f614,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f613]) ).
fof(f643,plain,
! [X0] :
( xp = szmzizndt0(X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| ~ aElementOf0(szmzizndt0(xQ),X0)
| X0 = slcrc0
| xQ = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0)
| ~ aSubsetOf0(xQ,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f458,f274]) ).
fof(f645,definition,
! [X0] :
( sQ18_spl
<=> ( xp = szmzizndt0(X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| ~ aElementOf0(szmzizndt0(xQ),X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f646,plain,
! [X0] :
( ~ sQ18_spl
| xp = szmzizndt0(X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| ~ aElementOf0(szmzizndt0(xQ),X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,plain,
( sQ5_spl
| sQ18_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f643,f571,f645,f574]) ).
fof(f650,plain,
! [X0] :
( ~ sQ18_spl
| xp = szmzizndt0(X0)
| ~ aElementOf0(szmzizndt0(X0),xQ)
| ~ aElementOf0(xp,X0)
| X0 = slcrc0
| ~ aSubsetOf0(X0,szNzAzT0) ),
inference(forward_demodulation,[status(thm)],[f458,f646]) ).
fof(f709,plain,
( ~ sQ18_spl
| xp = xx
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),xQ)
| ~ aElementOf0(xp,sdtlpdtrp0(xN,xm))
| sdtlpdtrp0(xN,xm) = slcrc0
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(paramodulation,[status(thm)],[f476,f650]) ).
fof(f715,definition,
( sQ30_spl
<=> aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f717,plain,
( sQ30_spl
| ~ aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0) ),
inference(component_clause,[status(thm)],[f715]) ).
fof(f718,definition,
( sQ31_spl
<=> sdtlpdtrp0(xN,xm) = slcrc0 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( ~ sQ31_spl
| sdtlpdtrp0(xN,xm) = slcrc0 ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f721,definition,
( sQ32_spl
<=> aElementOf0(xp,sdtlpdtrp0(xN,xm)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f723,plain,
( sQ32_spl
| ~ aElementOf0(xp,sdtlpdtrp0(xN,xm)) ),
inference(component_clause,[status(thm)],[f721]) ).
fof(f724,definition,
( sQ33_spl
<=> aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),xQ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f726,plain,
( sQ33_spl
| ~ aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),xQ) ),
inference(component_clause,[status(thm)],[f724]) ).
fof(f727,definition,
( sQ34_spl
<=> xp = xx ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( ~ sQ34_spl
| xp = xx ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f730,plain,
( ~ sQ18_spl
| sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f709,f715,f718,f721,f724,f727,f645]) ).
fof(f748,plain,
( ~ sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f484]) ).
fof(f749,plain,
~ sQ31_spl,
inference(contradiction_clause,[status(thm)],[f748]) ).
fof(f750,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f482]) ).
fof(f751,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f750]) ).
fof(f753,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f485]) ).
fof(f754,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f753]) ).
fof(f755,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f479]) ).
fof(f756,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f755]) ).
fof(f757,plain,
( sQ33_spl
| ~ aElementOf0(xx,xQ) ),
inference(forward_demodulation,[status(thm)],[f476,f726]) ).
fof(f758,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f757,f480]) ).
fof(f759,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f758]) ).
fof(f760,plain,
$false,
inference(sat_refutation,[status(thm)],[f612,f614,f648,f730,f749,f751,f754,f756,f759]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM624+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 : n013.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:44:51 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.42 % Refutation found
% 0.09/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.46 % Elapsed time: 0.078501 seconds
% 0.09/0.46 % CPU time: 0.261509 seconds
% 0.09/0.46 % Total memory used: 113.887 MB
% 0.09/0.46 % Net memory used: 113.606 MB
%------------------------------------------------------------------------------