%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM627+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:15 PM UTC 2026
% Result : Theorem 36.07s 5.06s
% Output : CNFRefutation 36.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 16
% Syntax : Number of formulae : 59 ( 9 unt; 7 def)
% Number of atoms : 175 ( 5 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 191 ( 75 ~; 67 |; 31 &)
% ( 8 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 7 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 11 con; 0-2 aty)
% Number of variables : 47 ( 43 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,definition,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W1)
=> aElementOf0(W2,W0) )
& aSet0(W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [W0] :
( aSet0(W0)
=> aSubsetOf0(W0,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( isCountable0(szNzAzT0)
& aSet0(szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,hypothesis,
! [W0,W1] :
( ( aElementOf0(W1,szNzAzT0)
& aElementOf0(W0,szNzAzT0) )
=> ( sdtlseqdt0(W1,W0)
=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W0))
=> aElementOf0(W2,sdtlpdtrp0(xN,W1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,hypothesis,
( sdtlpdtrp0(xe,xn) = xp
& aElementOf0(xn,szNzAzT0)
& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))
& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)
& aElementOf0(xn,szDzozmdt0(xd)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
( xx = sdtlpdtrp0(xe,xm)
& aElementOf0(xm,szNzAzT0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f117,hypothesis,
~ ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xm))
=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f118,hypothesis,
~ ( aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
| ! [W0] :
( aElementOf0(W0,sdtlpdtrp0(xN,xn))
=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,plain,
! [W0] :
( ! [W1] :
( aSubsetOf0(W1,W0)
<=> ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) ) )
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f146,plain,
! [W0] :
( ! [W1] :
( ( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(NNF_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
! [W0] :
( ( ! [W1] :
( ? [W2] :
( ~ aElementOf0(W2,W0)
& aElementOf0(W2,W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f148,plain,
! [W0] :
( ( ! [W1] :
( ( ~ aElementOf0(sK1_skl(W1,W0),W0)
& aElementOf0(sK1_skl(W1,W0),W1) )
| ~ aSet0(W1)
| aSubsetOf0(W1,W0) )
& ! [W1] :
( ( ! [W2] :
( aElementOf0(W2,W0)
| ~ aElementOf0(W2,W1) )
& aSet0(W1) )
| ~ aSubsetOf0(W1,W0) ) )
| ~ aSet0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f147]) ).
fof(f150,plain,
! [X0,X1,X2] :
( aElementOf0(X2,X0)
| ~ aElementOf0(X2,X1)
| ~ aSubsetOf0(X1,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f155,plain,
! [W0] :
( aSubsetOf0(W0,W0)
| ~ aSet0(W0) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f156,plain,
! [X0] :
( aSubsetOf0(X0,X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f197,plain,
aSet0(szNzAzT0),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f200,plain,
! [W0] :
( ( szszuzczcdt0(W0) != sz00
& aElementOf0(szszuzczcdt0(W0),szNzAzT0) )
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f201,plain,
! [X0] :
( aElementOf0(szszuzczcdt0(X0),szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f229,plain,
! [W0,W1] :
( sdtlseqdt0(szszuzczcdt0(W1),W0)
| sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f230,plain,
! [X0,X1] :
( sdtlseqdt0(szszuzczcdt0(X1),X0)
| sdtlseqdt0(X0,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f441,plain,
! [W0,W1] :
( ( aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1))
& ! [W2] :
( aElementOf0(W2,sdtlpdtrp0(xN,W1))
| ~ aElementOf0(W2,sdtlpdtrp0(xN,W0)) ) )
| ~ sdtlseqdt0(W1,W0)
| ~ aElementOf0(W1,szNzAzT0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f443,plain,
! [X0,X1] :
( aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f657,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f668,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f672,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ? [W0] :
( ~ aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& aElementOf0(W0,sdtlpdtrp0(xN,xm)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f117]) ).
fof(f673,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& ~ aElementOf0(sK39_skl,sdtlpdtrp0(xN,szszuzczcdt0(xn)))
& aElementOf0(sK39_skl,sdtlpdtrp0(xN,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl]),skolemize(W0,sK39_skl)],[f672]) ).
fof(f676,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))),
inference(cnf_transformation,[status(thm)],[f673]) ).
fof(f677,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ? [W0] :
( ~ aElementOf0(W0,sdtlpdtrp0(xN,xm))
& aElementOf0(W0,sdtlpdtrp0(xN,xn)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f118]) ).
fof(f678,plain,
( ~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))
& ~ aElementOf0(sK40_skl,sdtlpdtrp0(xN,xm))
& aElementOf0(sK40_skl,sdtlpdtrp0(xN,xn)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(W0,sK40_skl)],[f677]) ).
fof(f681,plain,
~ aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)),
inference(cnf_transformation,[status(thm)],[f678]) ).
fof(f943,definition,
( sQ0_spl
<=> aSet0(szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f945,plain,
( sQ0_spl
| ~ aSet0(szNzAzT0) ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f974,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f945,f197]) ).
fof(f975,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f1094,plain,
! [X0] :
( aElementOf0(xn,X0)
| ~ aSubsetOf0(szNzAzT0,X0)
| ~ aSet0(X0) ),
inference(resolution,[status(thm)],[f150,f657]) ).
fof(f1229,plain,
( aElementOf0(xn,szNzAzT0)
| ~ aSet0(szNzAzT0)
| ~ aSet0(szNzAzT0) ),
inference(resolution,[status(thm)],[f156,f1094]) ).
fof(f1245,definition,
( sQ51_spl
<=> aElementOf0(xn,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1248,plain,
( sQ51_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f1229,f943,f1245]) ).
fof(f3510,definition,
( sQ310_spl
<=> sdtlseqdt0(xm,xn) ),
introduced(definition,[new_symbols(definition,[sQ310_spl])],[split_symbol_definition]) ).
fof(f3704,definition,
( sQ330_spl
<=> aElementOf0(xm,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition]) ).
fof(f3706,plain,
( sQ330_spl
| ~ aElementOf0(xm,szNzAzT0) ),
inference(component_clause,[status(thm)],[f3704]) ).
fof(f8746,plain,
( sQ330_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3706,f668]) ).
fof(f8747,plain,
sQ330_spl,
inference(contradiction_clause,[status(thm)],[f8746]) ).
fof(f14793,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f676,f443]) ).
fof(f14794,definition,
( sQ1332_spl
<=> aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ1332_spl])],[split_symbol_definition]) ).
fof(f14796,plain,
( sQ1332_spl
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(component_clause,[status(thm)],[f14794]) ).
fof(f14797,definition,
( sQ1333_spl
<=> sdtlseqdt0(szszuzczcdt0(xn),xm) ),
introduced(definition,[new_symbols(definition,[sQ1333_spl])],[split_symbol_definition]) ).
fof(f14799,plain,
( sQ1333_spl
| ~ sdtlseqdt0(szszuzczcdt0(xn),xm) ),
inference(component_clause,[status(thm)],[f14797]) ).
fof(f14800,plain,
( ~ sQ1333_spl
| ~ sQ1332_spl
| ~ sQ330_spl ),
inference(split_clause,[status(thm)],[f14793,f3704,f14794,f14797]) ).
fof(f14841,plain,
( ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f681,f443]) ).
fof(f14842,plain,
( ~ sQ310_spl
| ~ sQ330_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f14841,f1245,f3704,f3510]) ).
fof(f16153,plain,
( sQ1332_spl
| ~ aElementOf0(xn,szNzAzT0) ),
inference(resolution,[status(thm)],[f14796,f201]) ).
fof(f16155,plain,
( sQ1332_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16153,f657]) ).
fof(f16156,plain,
sQ1332_spl,
inference(contradiction_clause,[status(thm)],[f16155]) ).
fof(f16157,plain,
( sQ1333_spl
| sdtlseqdt0(xm,xn)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f14799,f230]) ).
fof(f16158,plain,
( sQ1333_spl
| sQ310_spl
| ~ sQ51_spl
| ~ sQ330_spl ),
inference(split_clause,[status(thm)],[f16157,f3704,f1245,f3510,f14797]) ).
fof(f16159,plain,
$false,
inference(sat_refutation,[status(thm)],[f975,f1248,f8747,f14800,f14842,f16156,f16158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM627+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n018.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 02:47:43 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 36.07/5.06 % Refutation found
% 36.07/5.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.07/5.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.40/5.12 % Elapsed time: 4.682244 seconds
% 2.40/5.12 % CPU time: 36.461780 seconds
% 2.40/5.12 % Total memory used: 322.323 MB
% 2.40/5.12 % Net memory used: 302.873 MB
%------------------------------------------------------------------------------