%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM622+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 1.63s 1.11s
% Output : CNFRefutation 1.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 14
% Syntax : Number of formulae : 48 ( 12 unt; 6 def)
% Number of atoms : 120 ( 8 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 117 ( 45 ~; 41 |; 18 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 23 ( 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,axiom,
aElementOf0(sz00,szNzAzT0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [W0] :
( aElementOf0(W0,szNzAzT0)
=> sdtlseqdt0(W0,W0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f91,hypothesis,
( ! [W0] :
( aElementOf0(W0,szNzAzT0)
=> ( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
& ! [W1] :
( aElementOf0(W1,sdtlpdtrp0(xN,W0))
=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) )
& aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0)) ) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f115,hypothesis,
( xx = sdtlpdtrp0(xe,xm)
& aElementOf0(xm,szNzAzT0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f119,conjecture,
aElementOf0(xp,sdtlpdtrp0(xN,xm)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,negated_conjecture,
~ aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(negated_conjecture,[status(cth)],[f119]) ).
fof(f199,plain,
aElementOf0(sz00,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f223,plain,
! [W0] :
( sdtlseqdt0(W0,W0)
| ~ aElementOf0(W0,szNzAzT0) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f224,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
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(f442,plain,
! [X0,X1,X2] :
( aElementOf0(X2,sdtlpdtrp0(xN,X1))
| ~ aElementOf0(X2,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(X1,X0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f552,plain,
( ! [W0] :
( ( sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0))
& ! [W1] :
( sdtlseqdt0(sdtlpdtrp0(xe,W0),W1)
| ~ aElementOf0(W1,sdtlpdtrp0(xN,W0)) )
& aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0)) )
| ~ aElementOf0(W0,szNzAzT0) )
& szDzozmdt0(xe) = szNzAzT0
& aFunction0(xe) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f555,plain,
! [X0] :
( aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0))
| ~ aElementOf0(X0,szNzAzT0) ),
inference(cnf_transformation,[status(thm)],[f552]) ).
fof(f657,plain,
aElementOf0(xn,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f658,plain,
sdtlpdtrp0(xe,xn) = xp,
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f668,plain,
aElementOf0(xm,szNzAzT0),
inference(cnf_transformation,[status(thm)],[f115]) ).
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,
! [X0] :
( aElementOf0(X0,sdtlpdtrp0(xN,xm))
| ~ aElementOf0(X0,sdtlpdtrp0(xN,xn)) ),
inference(cnf_transformation,[status(thm)],[f677]) ).
fof(f680,plain,
~ aElementOf0(xp,sdtlpdtrp0(xN,xm)),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f1127,definition,
( sQ29_spl
<=> aElementOf0(xm,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1129,plain,
( sQ29_spl
| ~ aElementOf0(xm,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1127]) ).
fof(f1134,plain,
( sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1129,f668]) ).
fof(f1135,plain,
sQ29_spl,
inference(contradiction_clause,[status(thm)],[f1134]) ).
fof(f1510,definition,
( sQ83_spl
<=> aElementOf0(sz00,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1512,plain,
( sQ83_spl
| ~ aElementOf0(sz00,szNzAzT0) ),
inference(component_clause,[status(thm)],[f1510]) ).
fof(f4479,plain,
! [X0] :
( ~ aElementOf0(xp,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(xm,X0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(resolution,[status(thm)],[f680,f442]) ).
fof(f4480,definition,
! [X0] :
( sQ469_spl
<=> ( ~ aElementOf0(xp,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(xm,X0)
| ~ aElementOf0(X0,szNzAzT0) ) ),
introduced(definition,[new_symbols(definition,[sQ469_spl])],[split_symbol_definition]) ).
fof(f4481,plain,
! [X0] :
( ~ sQ469_spl
| ~ aElementOf0(xp,sdtlpdtrp0(xN,X0))
| ~ sdtlseqdt0(xm,X0)
| ~ aElementOf0(X0,szNzAzT0) ),
inference(component_clause,[status(thm)],[f4480]) ).
fof(f4483,plain,
( ~ sQ29_spl
| sQ469_spl ),
inference(split_clause,[status(thm)],[f4479,f4480,f1127]) ).
fof(f4546,definition,
( sQ475_spl
<=> aElementOf0(xn,szNzAzT0) ),
introduced(definition,[new_symbols(definition,[sQ475_spl])],[split_symbol_definition]) ).
fof(f4548,plain,
( sQ475_spl
| ~ aElementOf0(xn,szNzAzT0) ),
inference(component_clause,[status(thm)],[f4546]) ).
fof(f4641,plain,
( ~ sQ469_spl
| ~ sdtlseqdt0(xm,xm)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xp,sdtlpdtrp0(xN,xn)) ),
inference(resolution,[status(thm)],[f678,f4481]) ).
fof(f4644,definition,
( sQ484_spl
<=> aElementOf0(xp,sdtlpdtrp0(xN,xn)) ),
introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition]) ).
fof(f4651,definition,
( sQ486_spl
<=> sdtlseqdt0(xm,xm) ),
introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition]) ).
fof(f4653,plain,
( sQ486_spl
| ~ sdtlseqdt0(xm,xm) ),
inference(component_clause,[status(thm)],[f4651]) ).
fof(f4654,plain,
( ~ sQ469_spl
| ~ sQ486_spl
| ~ sQ29_spl
| ~ sQ484_spl ),
inference(split_clause,[status(thm)],[f4641,f4644,f1127,f4651,f4480]) ).
fof(f4799,plain,
( sQ486_spl
| ~ aElementOf0(xm,szNzAzT0) ),
inference(resolution,[status(thm)],[f4653,f224]) ).
fof(f4806,plain,
( sQ486_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f4799,f1127,f4651]) ).
fof(f5810,plain,
( sQ475_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f4548]) ).
fof(f5811,plain,
sQ475_spl,
inference(contradiction_clause,[status(thm)],[f5810]) ).
fof(f6011,plain,
( sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1512,f199]) ).
fof(f6012,plain,
sQ83_spl,
inference(contradiction_clause,[status(thm)],[f6011]) ).
fof(f6570,plain,
( aElementOf0(xp,sdtlpdtrp0(xN,xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(paramodulation,[status(thm)],[f658,f555]) ).
fof(f6574,plain,
( sQ484_spl
| ~ sQ475_spl ),
inference(split_clause,[status(thm)],[f6570,f4546,f4644]) ).
fof(f6579,plain,
$false,
inference(sat_refutation,[status(thm)],[f1135,f4483,f4654,f4806,f5811,f6012,f6574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM622+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.47 % Computer : n016.cluster.edu
% 0.19/0.47 % Model : x86_64 x86_64
% 0.19/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.47 % Memory : 8046.5625MB
% 0.19/0.47 % OS : Linux 6.8.0-71-generic
% 0.19/0.47 % CPULimit : 300
% 0.19/0.47 % WCLimit : 300
% 0.19/0.47 % DateTime : Mon Sep 21 02:49:52 UTC 2026
% 0.19/0.48 % CPUTime :
% 0.23/0.55 % Drodi V4.1.1
% 1.63/1.11 % Refutation found
% 1.63/1.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.63/1.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.63/1.17 % Elapsed time: 0.666383 seconds
% 1.63/1.17 % CPU time: 4.403315 seconds
% 1.63/1.17 % Total memory used: 159.887 MB
% 1.63/1.17 % Net memory used: 156.718 MB
%------------------------------------------------------------------------------