%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM539+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:40:55 PM UTC 2026
% Result : Theorem 0.12s 15.61s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of formulae : 51 ( 12 unt; 6 def)
% Number of atoms : 172 ( 10 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 186 ( 65 ~; 55 |; 48 &)
% ( 6 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-1 aty)
% Number of variables : 36 ( 31 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f36,axiom,
! [W0,W1,W2] :
( ( aElementOf0(W2,szNzAzT0)
& aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,hypothesis,
( ~ ( xT = slcrc0
| ~ ? [W0] : aElementOf0(W0,xT) )
& ~ ( xS = slcrc0
| ~ ? [W0] : aElementOf0(W0,xS) )
& aSubsetOf0(xT,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xT)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xT)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,xS)
=> aElementOf0(W0,szNzAzT0) )
& aSet0(xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,hypothesis,
( aElementOf0(szmzizndt0(xT),xS)
& ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(szmzizndt0(xT),W0) )
& aElementOf0(szmzizndt0(xT),xT)
& aElementOf0(szmzizndt0(xS),xT)
& ! [W0] :
( aElementOf0(W0,xS)
=> sdtlseqdt0(szmzizndt0(xS),W0) )
& aElementOf0(szmzizndt0(xS),xS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,conjecture,
( ( ! [W0] :
( aElementOf0(W0,xS)
=> sdtlseqdt0(szmzizndt0(xS),W0) )
& aElementOf0(szmzizndt0(xS),xS) )
=> ( szmzizndt0(xS) = szmzizndt0(xT)
| ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(szmzizndt0(xS),W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
~ ( ( ! [W0] :
( aElementOf0(W0,xS)
=> sdtlseqdt0(szmzizndt0(xS),W0) )
& aElementOf0(szmzizndt0(xS),xS) )
=> ( szmzizndt0(xS) = szmzizndt0(xT)
| ! [W0] :
( aElementOf0(W0,xT)
=> sdtlseqdt0(szmzizndt0(xS),W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f51]) ).
fof(f159,plain,
! [W0,W1,W2] :
( sdtlseqdt0(W0,W2)
| ~ sdtlseqdt0(W1,W2)
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W2,szNzAzT0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f160,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f203,plain,
( xT != slcrc0
& ? [W0] : aElementOf0(W0,xT)
& xS != slcrc0
& ? [W0] : aElementOf0(W0,xS)
& aSubsetOf0(xT,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xT) )
& aSet0(xT)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f204,plain,
( xT != slcrc0
& aElementOf0(sK9_skl,xT)
& xS != slcrc0
& aElementOf0(sK8_skl,xS)
& aSubsetOf0(xT,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xT) )
& aSet0(xT)
& aSubsetOf0(xS,szNzAzT0)
& ! [W0] :
( aElementOf0(W0,szNzAzT0)
| ~ aElementOf0(W0,xS) )
& aSet0(xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(W0,sK8_skl),skolemize(W0,sK9_skl)],[f203]) ).
fof(f209,plain,
! [X0] :
( aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f204]) ).
fof(f215,plain,
( aElementOf0(szmzizndt0(xT),xS)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xT),W0)
| ~ aElementOf0(W0,xT) )
& aElementOf0(szmzizndt0(xT),xT)
& aElementOf0(szmzizndt0(xS),xT)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xS),W0)
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzizndt0(xS),xS) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f218,plain,
aElementOf0(szmzizndt0(xS),xT),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f219,plain,
aElementOf0(szmzizndt0(xT),xT),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f220,plain,
! [X0] :
( sdtlseqdt0(szmzizndt0(xT),X0)
| ~ aElementOf0(X0,xT) ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f221,plain,
aElementOf0(szmzizndt0(xT),xS),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f222,plain,
( szmzizndt0(xS) != szmzizndt0(xT)
& ? [W0] :
( ~ sdtlseqdt0(szmzizndt0(xS),W0)
& aElementOf0(W0,xT) )
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xS),W0)
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzizndt0(xS),xS) ),
inference(pre_NNF_transformation,[status(thm)],[f52]) ).
fof(f223,plain,
( szmzizndt0(xS) != szmzizndt0(xT)
& ~ sdtlseqdt0(szmzizndt0(xS),sK10_skl)
& aElementOf0(sK10_skl,xT)
& ! [W0] :
( sdtlseqdt0(szmzizndt0(xS),W0)
| ~ aElementOf0(W0,xS) )
& aElementOf0(szmzizndt0(xS),xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W0,sK10_skl)],[f222]) ).
fof(f225,plain,
! [X0] :
( sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f226,plain,
aElementOf0(sK10_skl,xT),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f227,plain,
~ sdtlseqdt0(szmzizndt0(xS),sK10_skl),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f304,plain,
sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)),
inference(resolution,[status(thm)],[f221,f225]) ).
fof(f310,plain,
! [X0] :
( ~ sdtlseqdt0(X0,sK10_skl)
| ~ sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(sK10_skl,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0)
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(resolution,[status(thm)],[f160,f227]) ).
fof(f311,definition,
( sQ10_spl
<=> aElementOf0(szmzizndt0(xS),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( sQ10_spl
| ~ aElementOf0(szmzizndt0(xS),szNzAzT0) ),
inference(component_clause,[status(thm)],[f311]) ).
fof(f314,definition,
! [X0] :
( sQ11_spl
<=> ( ~ sdtlseqdt0(X0,sK10_skl)
| ~ sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f315,plain,
! [X0] :
( ~ sQ11_spl
| ~ sdtlseqdt0(X0,sK10_skl)
| ~ sdtlseqdt0(szmzizndt0(xS),X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f317,definition,
( sQ12_spl
<=> aElementOf0(sK10_skl,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f319,plain,
( sQ12_spl
| ~ aElementOf0(sK10_skl,szNzAzT0) ),
inference(component_clause,[status(thm)],[f317]) ).
fof(f320,plain,
( ~ sQ12_spl
| sQ11_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f310,f311,f314,f317]) ).
fof(f353,plain,
( sQ12_spl
| ~ aElementOf0(sK10_skl,xT) ),
inference(resolution,[status(thm)],[f319,f209]) ).
fof(f355,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f226]) ).
fof(f356,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f355]) ).
fof(f372,plain,
( sQ10_spl
| ~ aElementOf0(szmzizndt0(xS),xT) ),
inference(resolution,[status(thm)],[f313,f209]) ).
fof(f374,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f218]) ).
fof(f375,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f374]) ).
fof(f390,definition,
( sQ21_spl
<=> aElementOf0(sK10_skl,xT) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f392,plain,
( sQ21_spl
| ~ aElementOf0(sK10_skl,xT) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f445,plain,
( ~ sQ11_spl
| ~ sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT))
| ~ aElementOf0(szmzizndt0(xT),szNzAzT0)
| ~ aElementOf0(sK10_skl,xT) ),
inference(resolution,[status(thm)],[f220,f315]) ).
fof(f446,definition,
( sQ30_spl
<=> aElementOf0(szmzizndt0(xT),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f448,plain,
( sQ30_spl
| ~ aElementOf0(szmzizndt0(xT),szNzAzT0) ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f449,definition,
( sQ31_spl
<=> sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( sQ31_spl
| ~ sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT)) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f456,plain,
( ~ sQ11_spl
| ~ sQ31_spl
| ~ sQ30_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f445,f390,f446,f449,f314]) ).
fof(f457,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f451,f304]) ).
fof(f458,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f457]) ).
fof(f459,plain,
( sQ30_spl
| ~ aElementOf0(szmzizndt0(xT),xT) ),
inference(resolution,[status(thm)],[f448,f209]) ).
fof(f461,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f459,f219]) ).
fof(f462,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f461]) ).
fof(f463,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f392,f226]) ).
fof(f464,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f463]) ).
fof(f465,plain,
$false,
inference(sat_refutation,[status(thm)],[f320,f356,f375,f456,f458,f462,f464]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM539+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/15.57 % Computer : n012.cluster.edu
% 0.09/15.57 % Model : x86_64 x86_64
% 0.09/15.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.57 % Memory : 8046.5625MB
% 0.09/15.57 % OS : Linux 6.8.0-71-generic
% 0.09/15.57 % CPULimit : 300
% 0.09/15.57 % WCLimit : 300
% 0.09/15.57 % DateTime : Mon Sep 21 02:38:39 UTC 2026
% 0.09/15.58 % CPUTime :
% 0.09/15.59 % Drodi V4.1.1
% 0.12/15.61 % Refutation found
% 0.12/15.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/15.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/15.63 % Elapsed time: 0.042508 seconds
% 0.12/15.63 % CPU time: 0.102001 seconds
% 0.12/15.63 % Total memory used: 84.548 MB
% 0.12/15.63 % Net memory used: 84.428 MB
%------------------------------------------------------------------------------