%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM630+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:43:24 PM UTC 2026
% Result : Theorem 30.51s 4.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM630+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n013.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 02:45:06 UTC 2026
% 0.09/0.56 % CPUTime :
% 0.13/0.57 % Drodi V4.1.1
% 30.51/4.46 % Refutation found
% 30.51/4.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 30.51/4.46 % SZS output start CNFRefutation for theBenchmark
% 30.51/4.46 fof(f86,hypothesis,(
% 30.51/4.46 ( aFunction0(xC)& szDzozmdt0(xC) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aFunction0(sdtlpdtrp0(xC,W0))& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)& (! [W1] :( ( aSet0(W1)& aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) )) ) )) ),
% 30.51/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.46 fof(f91,hypothesis,(
% 30.51/4.46 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) )) ),
% 30.51/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.46 fof(f104,hypothesis,(
% 30.51/4.46 ( aSet0(xP)& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 30.51/4.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.46 fof(f111,hypothesis,(
% 30.51/4.47 ( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 30.51/4.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.47 fof(f114,hypothesis,(
% 30.51/4.47 xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) ),
% 30.51/4.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.47 fof(f115,hypothesis,(
% 30.51/4.47 aElementOf0(xP,slbdtsldtrb0(xD,xk)) ),
% 30.51/4.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.47 fof(f116,conjecture,(
% 30.51/4.47 sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) ),
% 30.51/4.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 30.51/4.47 fof(f117,negated_conjecture,(
% 30.51/4.47 ~(sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) )),
% 30.51/4.47 inference(negated_conjecture,[status(cth)],[f116])).
% 30.51/4.47 fof(f407,plain,(
% 30.51/4.47 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((aFunction0(sdtlpdtrp0(xC,W0))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|~aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)))|sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))))))))),
% 30.51/4.47 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 30.51/4.47 fof(f412,plain,(
% 30.51/4.47 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aSet0(X1)|~aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk))|sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1)=sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))))),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f407])).
% 30.51/4.47 fof(f427,plain,(
% 30.51/4.47 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0))))),
% 30.51/4.47 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 30.51/4.47 fof(f430,plain,(
% 30.51/4.47 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f427])).
% 30.51/4.47 fof(f454,plain,(
% 30.51/4.47 aSet0(xP)),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f104])).
% 30.51/4.47 fof(f463,plain,(
% 30.51/4.47 aElementOf0(xn,szNzAzT0)),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f111])).
% 30.51/4.47 fof(f464,plain,(
% 30.51/4.47 sdtlpdtrp0(xe,xn)=xp),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f111])).
% 30.51/4.47 fof(f467,plain,(
% 30.51/4.47 xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f114])).
% 30.51/4.47 fof(f468,plain,(
% 30.51/4.47 aElementOf0(xP,slbdtsldtrb0(xD,xk))),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f115])).
% 30.51/4.47 fof(f469,plain,(
% 30.51/4.47 ~sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 30.51/4.47 inference(cnf_transformation,[status(thm)],[f117])).
% 30.51/4.47 fof(f564,plain,(
% 30.51/4.47 sdtlpdtrp0(xe,xn)=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 30.51/4.47 inference(resolution,[status(thm)],[f430,f463])).
% 30.51/4.47 fof(f566,plain,(
% 30.51/4.47 xp=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 30.51/4.47 inference(forward_demodulation,[status(thm)],[f464,f564])).
% 30.51/4.47 fof(f574,plain,(
% 30.51/4.47 ~sdtlpdtrp0(xc,sdtpldt0(xP,xp))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 30.51/4.47 inference(backward_demodulation,[status(thm)],[f566,f469])).
% 30.51/4.48 fof(f580,definition,(
% 30.51/4.48 sQ12_spl <=> (aSet0(xP))),
% 30.51/4.48 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 30.51/4.48 fof(f582,plain,(
% 30.51/4.48 ~aSet0(xP)|sQ12_spl),
% 30.51/4.48 inference(component_clause,[status(thm)],[f580])).
% 30.51/4.48 fof(f818,plain,(
% 30.51/4.48 $false|sQ12_spl),
% 30.51/4.48 inference(forward_subsumption_resolution,[status(thm)],[f582,f454])).
% 30.51/4.48 fof(f819,plain,(
% 30.51/4.48 sQ12_spl),
% 30.51/4.48 inference(contradiction_clause,[status(thm)],[f818])).
% 30.51/4.48 fof(f820,plain,(
% 30.51/4.48 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),xk))|sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0)=sdtlpdtrp0(xc,sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xn)))))),
% 30.51/4.48 inference(resolution,[status(thm)],[f412,f463])).
% 30.51/4.48 fof(f822,plain,(
% 30.51/4.48 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xn),xp),xk))|sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0)=sdtlpdtrp0(xc,sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,xn)))))),
% 30.51/4.48 inference(forward_demodulation,[status(thm)],[f566,f820])).
% 30.51/4.48 fof(f823,plain,(
% 30.51/4.48 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xn),xp),xk))|sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0)=sdtlpdtrp0(xc,sdtpldt0(X0,xp)))),
% 30.51/4.48 inference(forward_demodulation,[status(thm)],[f566,f822])).
% 30.51/4.48 fof(f5097,plain,(
% 30.51/4.48 sdtlpdtrp0(xe,xn)=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 30.51/4.48 inference(resolution,[status(thm)],[f463,f430])).
% 30.51/4.48 fof(f6547,plain,(
% 30.51/4.48 xp=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 30.51/4.48 inference(forward_demodulation,[status(thm)],[f464,f5097])).
% 30.51/4.48 fof(f8799,plain,(
% 30.51/4.48 xD=sdtmndt0(sdtlpdtrp0(xN,xn),xp)),
% 30.51/4.48 inference(forward_demodulation,[status(thm)],[f6547,f467])).
% 30.51/4.48 fof(f12485,plain,(
% 30.51/4.48 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(xD,xk))|sdtlpdtrp0(sdtlpdtrp0(xC,xn),X0)=sdtlpdtrp0(xc,sdtpldt0(X0,xp)))),
% 30.51/4.48 inference(forward_demodulation,[status(thm)],[f8799,f823])).
% 30.51/4.48 fof(f12486,plain,(
% 30.51/4.48 ~aSet0(xP)|sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)=sdtlpdtrp0(xc,sdtpldt0(xP,xp))),
% 30.51/4.48 inference(resolution,[status(thm)],[f12485,f468])).
% 30.51/4.48 fof(f12488,definition,(
% 30.51/4.48 sQ1169_spl <=> (sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)=sdtlpdtrp0(xc,sdtpldt0(xP,xp)))),
% 30.51/4.48 introduced(definition,[new_symbols(definition,[sQ1169_spl])],[split_symbol_definition])).
% 30.51/4.48 fof(f12489,plain,(
% 30.51/4.48 sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)=sdtlpdtrp0(xc,sdtpldt0(xP,xp))|~sQ1169_spl),
% 30.51/4.48 inference(component_clause,[status(thm)],[f12488])).
% 30.51/4.48 fof(f12491,plain,(
% 30.51/4.48 ~sQ12_spl|sQ1169_spl),
% 30.51/4.48 inference(split_clause,[status(thm)],[f12486,f580,f12488])).
% 30.51/4.48 fof(f12502,plain,(
% 30.51/4.48 $false|~sQ1169_spl),
% 30.51/4.48 inference(forward_subsumption_resolution,[status(thm)],[f12489,f574])).
% 30.51/4.48 fof(f12503,plain,(
% 30.51/4.48 ~sQ1169_spl),
% 30.51/4.48 inference(contradiction_clause,[status(thm)],[f12502])).
% 30.51/4.48 fof(f12504,plain,(
% 30.51/4.48 $false),
% 30.51/4.48 inference(sat_refutation,[status(thm)],[f819,f12491,f12503])).
% 30.51/4.48 % SZS output end CNFRefutation for theBenchmark.p
% 30.51/4.52 % Elapsed time: 3.945612 seconds
% 30.51/4.52 % CPU time: 30.968023 seconds
% 30.51/4.52 % Total memory used: 372.986 MB
% 30.51/4.52 % Net memory used: 349.852 MB
%------------------------------------------------------------------------------