%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM453+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:42:56 PM UTC 2026
% Result : Theorem 3.24s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM453+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n018.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 02:33:29 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 3.24/0.95 % Refutation found
% 3.24/0.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.24/0.95 % SZS output start CNFRefutation for theBenchmark
% 3.24/0.95 fof(f3,axiom,(
% 3.24/0.95 aInteger0(sz10) ),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f4,axiom,(
% 3.24/0.95 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f7,axiom,(
% 3.24/0.95 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f8,axiom,(
% 3.24/0.95 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f9,axiom,(
% 3.24/0.95 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f10,axiom,(
% 3.24/0.95 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f46,hypothesis,(
% 3.24/0.95 ( aInteger0(xp)& xp != sz00& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ) ),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f48,conjecture,(
% 3.24/0.95 ( sdtpldt0(sz10,xp) != sz10& sdtpldt0(sz10,smndt0(xp)) != sz10 ) ),
% 3.24/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.24/0.95 fof(f49,negated_conjecture,(
% 3.24/0.95 ~(( sdtpldt0(sz10,xp) != sz10& sdtpldt0(sz10,smndt0(xp)) != sz10 ) )),
% 3.24/0.95 inference(negated_conjecture,[status(cth)],[f48])).
% 3.24/0.95 fof(f54,plain,(
% 3.24/0.95 aInteger0(sz10)),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f3])).
% 3.24/0.95 fof(f55,plain,(
% 3.24/0.95 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 3.24/0.95 fof(f56,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f55])).
% 3.24/0.95 fof(f61,plain,(
% 3.24/0.95 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 3.24/0.95 fof(f62,plain,(
% 3.24/0.95 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f61])).
% 3.24/0.95 fof(f63,plain,(
% 3.24/0.95 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.24/0.95 fof(f64,plain,(
% 3.24/0.95 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f63])).
% 3.24/0.95 fof(f65,plain,(
% 3.24/0.95 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 3.24/0.95 fof(f67,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f65])).
% 3.24/0.95 fof(f68,plain,(
% 3.24/0.95 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 3.24/0.95 fof(f69,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f68])).
% 3.24/0.95 fof(f70,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f68])).
% 3.24/0.95 fof(f229,plain,(
% 3.24/0.95 aInteger0(xp)),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f46])).
% 3.24/0.95 fof(f230,plain,(
% 3.24/0.95 ~xp=sz00),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f46])).
% 3.24/0.95 fof(f234,plain,(
% 3.24/0.95 (sdtpldt0(sz10,xp)=sz10|sdtpldt0(sz10,smndt0(xp))=sz10)),
% 3.24/0.95 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 3.24/0.95 fof(f235,plain,(
% 3.24/0.95 sdtpldt0(sz10,xp)=sz10|sdtpldt0(sz10,smndt0(xp))=sz10),
% 3.24/0.95 inference(cnf_transformation,[status(thm)],[f234])).
% 3.24/0.95 fof(f247,definition,(
% 3.24/0.95 sQ0_spl <=> (sdtpldt0(sz10,xp)=sz10)),
% 3.24/0.95 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 3.24/0.95 fof(f248,plain,(
% 3.24/0.95 sdtpldt0(sz10,xp)=sz10|~sQ0_spl),
% 3.24/0.95 inference(component_clause,[status(thm)],[f247])).
% 3.24/0.95 fof(f249,plain,(
% 3.24/0.95 ~sdtpldt0(sz10,xp)=sz10|sQ0_spl),
% 3.24/0.95 inference(component_clause,[status(thm)],[f247])).
% 3.24/0.95 fof(f250,definition,(
% 3.24/0.95 sQ1_spl <=> (sdtpldt0(sz10,smndt0(xp))=sz10)),
% 3.24/0.95 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 3.24/0.95 fof(f251,plain,(
% 3.24/0.95 sdtpldt0(sz10,smndt0(xp))=sz10|~sQ1_spl),
% 3.24/0.95 inference(component_clause,[status(thm)],[f250])).
% 3.24/0.95 fof(f253,plain,(
% 3.24/0.95 sQ0_spl|sQ1_spl),
% 3.24/0.95 inference(split_clause,[status(thm)],[f235,f247,f250])).
% 3.24/0.95 fof(f255,plain,(
% 3.24/0.95 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(sz10,X1))=sdtpldt0(sdtpldt0(X0,sz10),X1))),
% 3.24/0.95 inference(resolution,[status(thm)],[f62,f54])).
% 3.24/0.95 fof(f257,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sz10,X0))),
% 3.24/0.95 inference(resolution,[status(thm)],[f64,f54])).
% 3.24/0.95 fof(f259,plain,(
% 3.24/0.95 aInteger0(smndt0(sz10))),
% 3.24/0.95 inference(resolution,[status(thm)],[f56,f54])).
% 3.24/0.95 fof(f269,plain,(
% 3.24/0.95 xp=sdtpldt0(sz00,xp)),
% 3.24/0.95 inference(resolution,[status(thm)],[f229,f67])).
% 3.24/0.95 fof(f270,plain,(
% 3.24/0.95 aInteger0(smndt0(xp))),
% 3.24/0.95 inference(resolution,[status(thm)],[f229,f56])).
% 3.24/0.95 fof(f274,plain,(
% 3.24/0.95 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xp))=sdtpldt0(sdtpldt0(X0,X1),xp))),
% 3.24/0.95 inference(resolution,[status(thm)],[f229,f62])).
% 3.24/0.95 fof(f279,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,xp))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 3.24/0.95 inference(resolution,[status(thm)],[f255,f229])).
% 3.24/0.95 fof(f281,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sdtpldt0(X0,sz10),xp)|~sQ0_spl)),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f248,f279])).
% 3.24/0.95 fof(f290,plain,(
% 3.24/0.95 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 3.24/0.95 inference(resolution,[status(thm)],[f69,f54])).
% 3.24/0.95 fof(f296,plain,(
% 3.24/0.95 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sz10,smndt0(sz10))),
% 3.24/0.95 inference(resolution,[status(thm)],[f259,f257])).
% 3.24/0.95 fof(f305,plain,(
% 3.24/0.95 aInteger0(smndt0(smndt0(sz10)))),
% 3.24/0.95 inference(resolution,[status(thm)],[f259,f56])).
% 3.24/0.95 fof(f317,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,smndt0(xp)))=sdtpldt0(sdtpldt0(X0,sz10),smndt0(xp)))),
% 3.24/0.95 inference(resolution,[status(thm)],[f270,f255])).
% 3.24/0.95 fof(f323,plain,(
% 3.24/0.95 smndt0(xp)=sdtpldt0(sz00,smndt0(xp))),
% 3.24/0.95 inference(resolution,[status(thm)],[f270,f67])).
% 3.24/0.95 fof(f362,plain,(
% 3.24/0.95 sz00=sdtpldt0(smndt0(xp),xp)),
% 3.24/0.95 inference(resolution,[status(thm)],[f70,f229])).
% 3.24/0.95 fof(f363,plain,(
% 3.24/0.95 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 3.24/0.95 inference(resolution,[status(thm)],[f70,f54])).
% 3.24/0.95 fof(f366,plain,(
% 3.24/0.95 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)|~sQ0_spl),
% 3.24/0.95 inference(resolution,[status(thm)],[f281,f259])).
% 3.24/0.95 fof(f389,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(smndt0(xp),xp))=sdtpldt0(sdtpldt0(X0,smndt0(xp)),xp))),
% 3.24/0.95 inference(resolution,[status(thm)],[f274,f270])).
% 3.24/0.95 fof(f470,plain,(
% 3.24/0.95 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sz00,xp)|~sQ0_spl),
% 3.24/0.95 inference(backward_demodulation,[status(thm)],[f471,f366])).
% 3.24/0.95 fof(f471,plain,(
% 3.24/0.95 sdtpldt0(smndt0(sz10),sz10)=sz00),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f290,f296])).
% 3.24/0.95 fof(f472,plain,(
% 3.24/0.95 sz00=sdtpldt0(sz00,xp)|~sQ0_spl),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f471,f470])).
% 3.24/0.95 fof(f473,plain,(
% 3.24/0.95 sz00=xp|~sQ0_spl),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f269,f472])).
% 3.24/0.95 fof(f623,plain,(
% 3.24/0.95 ~xp=xp|~sQ0_spl),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f473,f230])).
% 3.24/0.95 fof(f624,plain,(
% 3.24/0.95 $false|~sQ0_spl),
% 3.24/0.95 inference(trivial_equality_resolution,[status(thm)],[f623])).
% 3.24/0.95 fof(f625,plain,(
% 3.24/0.95 ~sQ0_spl),
% 3.24/0.95 inference(contradiction_clause,[status(thm)],[f624])).
% 3.24/0.95 fof(f749,definition,(
% 3.24/0.95 sQ11_spl <=> (xp=sz00)),
% 3.24/0.95 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 3.24/0.95 fof(f750,plain,(
% 3.24/0.95 xp=sz00|~sQ11_spl),
% 3.24/0.95 inference(component_clause,[status(thm)],[f749])).
% 3.24/0.95 fof(f761,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sdtpldt0(X0,sz10),smndt0(xp))|~sQ1_spl)),
% 3.24/0.95 inference(backward_demodulation,[status(thm)],[f251,f317])).
% 3.24/0.95 fof(f767,plain,(
% 3.24/0.95 sdtpldt0(smndt0(sz10),sz10)=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),smndt0(xp))|~sQ1_spl),
% 3.24/0.95 inference(resolution,[status(thm)],[f761,f259])).
% 3.24/0.95 fof(f789,plain,(
% 3.24/0.95 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,smndt0(xp)),xp))),
% 3.24/0.95 inference(forward_demodulation,[status(thm)],[f362,f389])).
% 3.24/0.95 fof(f795,plain,(
% 3.24/0.95 sdtpldt0(sz10,sz00)=sdtpldt0(sdtpldt0(sz10,smndt0(xp)),xp)),
% 3.24/0.96 inference(resolution,[status(thm)],[f789,f54])).
% 3.24/0.96 fof(f799,plain,(
% 3.24/0.96 sdtpldt0(sz10,sz00)=sdtpldt0(sz10,xp)|~sQ1_spl),
% 3.24/0.96 inference(forward_demodulation,[status(thm)],[f251,f795])).
% 3.24/0.96 fof(f1034,plain,(
% 3.24/0.96 sz00=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),smndt0(xp))|~sQ1_spl),
% 3.24/0.96 inference(forward_demodulation,[status(thm)],[f363,f767])).
% 3.24/0.96 fof(f1035,plain,(
% 3.24/0.96 smndt0(xp)=sz00|~sQ1_spl),
% 3.24/0.96 inference(backward_demodulation,[status(thm)],[f1036,f323])).
% 3.24/0.96 fof(f1036,plain,(
% 3.24/0.96 sz00=sdtpldt0(sz00,smndt0(xp))|~sQ1_spl),
% 3.24/0.96 inference(forward_demodulation,[status(thm)],[f363,f1034])).
% 3.24/0.96 fof(f1053,plain,(
% 3.24/0.96 sdtpldt0(sz10,sz00)=sz10|~sQ1_spl),
% 3.24/0.96 inference(backward_demodulation,[status(thm)],[f1035,f251])).
% 3.24/0.96 fof(f1312,definition,(
% 3.24/0.96 sQ24_spl <=> (aInteger0(smndt0(smndt0(sz10))))),
% 3.24/0.96 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 3.24/0.96 fof(f1314,plain,(
% 3.24/0.96 ~aInteger0(smndt0(smndt0(sz10)))|sQ24_spl),
% 3.24/0.96 inference(component_clause,[status(thm)],[f1312])).
% 3.24/0.96 fof(f1315,definition,(
% 3.24/0.96 sQ25_spl <=> (aInteger0(sz10))),
% 3.24/0.96 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 3.24/0.96 fof(f1317,plain,(
% 3.24/0.96 ~aInteger0(sz10)|sQ25_spl),
% 3.24/0.96 inference(component_clause,[status(thm)],[f1315])).
% 3.24/0.96 fof(f1343,plain,(
% 3.24/0.96 $false|sQ25_spl),
% 3.24/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1317,f54])).
% 3.24/0.96 fof(f1344,plain,(
% 3.24/0.96 sQ25_spl),
% 3.24/0.96 inference(contradiction_clause,[status(thm)],[f1343])).
% 3.24/0.96 fof(f1345,plain,(
% 3.24/0.96 $false|sQ24_spl),
% 3.24/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1314,f305])).
% 3.24/0.96 fof(f1346,plain,(
% 3.24/0.96 sQ24_spl),
% 3.24/0.96 inference(contradiction_clause,[status(thm)],[f1345])).
% 3.24/0.96 fof(f1539,definition,(
% 3.24/0.96 sQ35_spl <=> (aInteger0(smndt0(sz10)))),
% 3.24/0.96 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 3.24/0.96 fof(f1541,plain,(
% 3.24/0.96 ~aInteger0(smndt0(sz10))|sQ35_spl),
% 3.24/0.96 inference(component_clause,[status(thm)],[f1539])).
% 3.24/0.96 fof(f1546,plain,(
% 3.24/0.96 $false|sQ35_spl),
% 3.24/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1541,f259])).
% 3.24/0.96 fof(f1547,plain,(
% 3.24/0.96 sQ35_spl),
% 3.24/0.96 inference(contradiction_clause,[status(thm)],[f1546])).
% 3.24/0.96 fof(f1783,plain,(
% 3.24/0.96 $false|~sQ11_spl),
% 3.24/0.96 inference(forward_subsumption_resolution,[status(thm)],[f750,f230])).
% 3.24/0.96 fof(f1784,plain,(
% 3.24/0.96 ~sQ11_spl),
% 3.24/0.96 inference(contradiction_clause,[status(thm)],[f1783])).
% 3.24/0.96 fof(f1786,plain,(
% 3.24/0.96 sz10=sdtpldt0(sz10,xp)|~sQ1_spl),
% 3.24/0.96 inference(forward_demodulation,[status(thm)],[f1053,f799])).
% 3.24/0.96 fof(f1787,plain,(
% 3.24/0.96 $false|sQ0_spl|~sQ1_spl),
% 3.24/0.96 inference(forward_subsumption_resolution,[status(thm)],[f1786,f249])).
% 3.24/0.96 fof(f1788,plain,(
% 3.24/0.96 sQ0_spl|~sQ1_spl),
% 3.24/0.96 inference(contradiction_clause,[status(thm)],[f1787])).
% 3.24/0.96 fof(f1789,plain,(
% 3.24/0.96 $false),
% 3.24/0.96 inference(sat_refutation,[status(thm)],[f253,f625,f1344,f1346,f1547,f1784,f1788])).
% 3.24/0.96 % SZS output end CNFRefutation for theBenchmark.p
% 3.24/0.98 % Elapsed time: 0.508068 seconds
% 3.24/0.98 % CPU time: 3.582720 seconds
% 3.24/0.98 % Total memory used: 141.665 MB
% 3.24/0.98 % Net memory used: 138.697 MB
%------------------------------------------------------------------------------