%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM459+2 : 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 : n004.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:57 PM UTC 2026
% Result : Theorem 9.82s 1.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM459+2 : 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.16/0.43 % Computer : n004.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 02:31:50 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 9.82/1.76 % Refutation found
% 9.82/1.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.82/1.76 % SZS output start CNFRefutation for theBenchmark
% 9.82/1.76 fof(f2,axiom,(
% 9.82/1.76 aNaturalNumber0(sz00) ),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f3,axiom,(
% 9.82/1.76 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f4,axiom,(
% 9.82/1.76 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f6,axiom,(
% 9.82/1.76 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f7,axiom,(
% 9.82/1.76 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f8,axiom,(
% 9.82/1.76 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f11,axiom,(
% 9.82/1.76 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f12,axiom,(
% 9.82/1.76 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f14,axiom,(
% 9.82/1.76 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2)| sdtpldt0(W1,W0) = sdtpldt0(W2,W0) )=> W1 = W2 ) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f16,axiom,(
% 9.82/1.76 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtpldt0(W0,W1) = sz00=> ( W0 = sz00& W1 = sz00 ) ) ) )),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f21,hypothesis,(
% 9.82/1.76 ( aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f22,conjecture,(
% 9.82/1.76 ( ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))& sdtlseqdt0(xm,xn)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xm ))& sdtlseqdt0(xn,xm) )=> xm = xn ) ),
% 9.82/1.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.82/1.76 fof(f23,negated_conjecture,(
% 9.82/1.76 ~(( ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))& sdtlseqdt0(xm,xn)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xm ))& sdtlseqdt0(xn,xm) )=> xm = xn ) )),
% 9.82/1.76 inference(negated_conjecture,[status(cth)],[f22])).
% 9.82/1.76 fof(f27,plain,(
% 9.82/1.76 aNaturalNumber0(sz00)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f2])).
% 9.82/1.76 fof(f29,plain,(
% 9.82/1.76 ~sz10=sz00),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f3])).
% 9.82/1.76 fof(f30,plain,(
% 9.82/1.76 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 9.82/1.76 fof(f31,plain,(
% 9.82/1.76 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f30])).
% 9.82/1.76 fof(f34,plain,(
% 9.82/1.76 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 9.82/1.76 fof(f35,plain,(
% 9.82/1.76 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f34])).
% 9.82/1.76 fof(f36,plain,(
% 9.82/1.76 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 9.82/1.76 fof(f37,plain,(
% 9.82/1.76 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f36])).
% 9.82/1.76 fof(f38,plain,(
% 9.82/1.76 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 9.82/1.76 fof(f39,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f38])).
% 9.82/1.76 fof(f40,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|X0=sdtpldt0(sz00,X0))),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f38])).
% 9.82/1.76 fof(f45,plain,(
% 9.82/1.76 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 9.82/1.76 fof(f46,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f45])).
% 9.82/1.76 fof(f48,plain,(
% 9.82/1.76 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 9.82/1.76 fof(f49,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f48])).
% 9.82/1.76 fof(f54,plain,(
% 9.82/1.76 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~sdtpldt0(W0,W1)=sdtpldt0(W0,W2)&~sdtpldt0(W1,W0)=sdtpldt0(W2,W0))|W1=W2))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 9.82/1.76 fof(f56,plain,(
% 9.82/1.76 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtpldt0(X1,X0)=sdtpldt0(X2,X0)|X1=X2)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f54])).
% 9.82/1.76 fof(f60,plain,(
% 9.82/1.76 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtpldt0(W0,W1)=sz00|(W0=sz00&W1=sz00)))),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 9.82/1.76 fof(f62,plain,(
% 9.82/1.76 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtpldt0(X0,X1)=sz00|X1=sz00)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f60])).
% 9.82/1.76 fof(f79,plain,(
% 9.82/1.76 aNaturalNumber0(xm)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f21])).
% 9.82/1.76 fof(f80,plain,(
% 9.82/1.76 aNaturalNumber0(xn)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f21])).
% 9.82/1.76 fof(f81,plain,(
% 9.82/1.76 (((((?[W0]: (aNaturalNumber0(W0)&sdtpldt0(xm,W0)=xn))&sdtlseqdt0(xm,xn))&(?[W0]: (aNaturalNumber0(W0)&sdtpldt0(xn,W0)=xm)))&sdtlseqdt0(xn,xm))&~xm=xn)),
% 9.82/1.76 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 9.82/1.76 fof(f82,plain,(
% 9.82/1.76 ((((aNaturalNumber0(sK1_skl)&sdtpldt0(xm,sK1_skl)=xn)&sdtlseqdt0(xm,xn))&(aNaturalNumber0(sK2_skl)&sdtpldt0(xn,sK2_skl)=xm))&sdtlseqdt0(xn,xm))&~xm=xn),
% 9.82/1.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(W0,sK1_skl),skolemize(W0,sK2_skl)],[f81])).
% 9.82/1.76 fof(f83,plain,(
% 9.82/1.76 aNaturalNumber0(sK1_skl)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f82])).
% 9.82/1.76 fof(f84,plain,(
% 9.82/1.76 sdtpldt0(xm,sK1_skl)=xn),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f82])).
% 9.82/1.76 fof(f86,plain,(
% 9.82/1.76 aNaturalNumber0(sK2_skl)),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f82])).
% 9.82/1.76 fof(f87,plain,(
% 9.82/1.76 sdtpldt0(xn,sK2_skl)=xm),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f82])).
% 9.82/1.76 fof(f89,plain,(
% 9.82/1.76 ~xm=xn),
% 9.82/1.76 inference(cnf_transformation,[status(thm)],[f82])).
% 9.82/1.76 fof(f92,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(sK2_skl,X0)))),
% 9.82/1.76 inference(resolution,[status(thm)],[f31,f86])).
% 9.82/1.76 fof(f94,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sK2_skl)=sdtpldt0(sK2_skl,X0))),
% 9.82/1.76 inference(resolution,[status(thm)],[f35,f86])).
% 9.82/1.76 fof(f95,plain,(
% 9.82/1.76 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sK1_skl)=sdtpldt0(sK1_skl,X0))),
% 9.82/1.76 inference(resolution,[status(thm)],[f35,f83])).
% 9.82/1.76 fof(f105,definition,(
% 9.82/1.76 sQ0_spl <=> (aNaturalNumber0(xn))),
% 9.82/1.76 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 9.82/1.76 fof(f106,plain,(
% 9.82/1.76 aNaturalNumber0(xn)|~sQ0_spl),
% 9.82/1.76 inference(component_clause,[status(thm)],[f105])).
% 9.82/1.76 fof(f107,plain,(
% 9.82/1.76 ~aNaturalNumber0(xn)|sQ0_spl),
% 9.82/1.76 inference(component_clause,[status(thm)],[f105])).
% 9.82/1.76 fof(f114,definition,(
% 9.82/1.76 sQ3_spl <=> (aNaturalNumber0(sK2_skl))),
% 9.82/1.76 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 9.82/1.76 fof(f116,plain,(
% 9.82/1.76 ~aNaturalNumber0(sK2_skl)|sQ3_spl),
% 9.82/1.76 inference(component_clause,[status(thm)],[f114])).
% 9.82/1.76 fof(f121,definition,(
% 9.82/1.76 sQ5_spl <=> (aNaturalNumber0(sK1_skl))),
% 9.82/1.76 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 9.82/1.76 fof(f123,plain,(
% 9.82/1.76 ~aNaturalNumber0(sK1_skl)|sQ5_spl),
% 9.82/1.76 inference(component_clause,[status(thm)],[f121])).
% 9.82/1.76 fof(f137,plain,(
% 9.82/1.76 sz00=sdtpldt0(sz00,sz00)),
% 9.82/1.76 inference(resolution,[status(thm)],[f27,f40])).
% 9.82/1.76 fof(f169,plain,(
% 9.82/1.76 aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))),
% 9.82/1.77 inference(resolution,[status(thm)],[f92,f83])).
% 9.82/1.77 fof(f177,plain,(
% 9.82/1.77 sdtpldt0(sK1_skl,sK2_skl)=sdtpldt0(sK2_skl,sK1_skl)),
% 9.82/1.77 inference(resolution,[status(thm)],[f94,f83])).
% 9.82/1.77 fof(f182,definition,(
% 9.82/1.77 sQ10_spl <=> (aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f184,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))|sQ10_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f182])).
% 9.82/1.77 fof(f200,plain,(
% 9.82/1.77 $false|sQ3_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f116,f86])).
% 9.82/1.77 fof(f201,plain,(
% 9.82/1.77 sQ3_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f200])).
% 9.82/1.77 fof(f202,plain,(
% 9.82/1.77 $false|sQ5_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f123,f83])).
% 9.82/1.77 fof(f203,plain,(
% 9.82/1.77 sQ5_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f202])).
% 9.82/1.77 fof(f501,plain,(
% 9.82/1.77 $false|sQ10_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f184,f169])).
% 9.82/1.77 fof(f502,plain,(
% 9.82/1.77 sQ10_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f501])).
% 9.82/1.77 fof(f860,plain,(
% 9.82/1.77 $false|sQ0_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f80,f107])).
% 9.82/1.77 fof(f861,plain,(
% 9.82/1.77 sQ0_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f860])).
% 9.82/1.77 fof(f865,plain,(
% 9.82/1.77 sdtpldt0(xm,sK1_skl)=sdtpldt0(sK1_skl,xm)),
% 9.82/1.77 inference(resolution,[status(thm)],[f79,f95])).
% 9.82/1.77 fof(f866,plain,(
% 9.82/1.77 sdtpldt0(xm,sK2_skl)=sdtpldt0(sK2_skl,xm)),
% 9.82/1.77 inference(resolution,[status(thm)],[f79,f94])).
% 9.82/1.77 fof(f868,plain,(
% 9.82/1.77 aNaturalNumber0(sdtpldt0(sK2_skl,xm))),
% 9.82/1.77 inference(resolution,[status(thm)],[f79,f92])).
% 9.82/1.77 fof(f873,plain,(
% 9.82/1.77 sdtpldt0(xm,sz00)=xm),
% 9.82/1.77 inference(resolution,[status(thm)],[f79,f39])).
% 9.82/1.77 fof(f877,plain,(
% 9.82/1.77 xn=sdtpldt0(sK1_skl,xm)),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f84,f865])).
% 9.82/1.77 fof(f905,plain,(
% 9.82/1.77 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(sdtpldt0(X0,sK1_skl),X1)=sdtpldt0(X0,sdtpldt0(sK1_skl,X1)))),
% 9.82/1.77 inference(resolution,[status(thm)],[f37,f83])).
% 9.82/1.77 fof(f919,plain,(
% 9.82/1.77 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(sdtpldt0(X0,X1),sK1_skl)=sdtpldt0(X0,sdtpldt0(X1,sK1_skl)))),
% 9.82/1.77 inference(resolution,[status(thm)],[f37,f83])).
% 9.82/1.77 fof(f1243,plain,(
% 9.82/1.77 sdtpldt0(xn,sK2_skl)=sdtpldt0(sK2_skl,xn)|~sQ0_spl),
% 9.82/1.77 inference(resolution,[status(thm)],[f106,f94])).
% 9.82/1.77 fof(f1249,plain,(
% 9.82/1.77 xn=sdtpldt0(sz00,xn)|~sQ0_spl),
% 9.82/1.77 inference(resolution,[status(thm)],[f106,f40])).
% 9.82/1.77 fof(f1254,plain,(
% 9.82/1.77 xm=sdtpldt0(sK2_skl,xn)|~sQ0_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f87,f1243])).
% 9.82/1.77 fof(f1285,definition,(
% 9.82/1.77 sQ139_spl <=> (aNaturalNumber0(sdtpldt0(xn,sK2_skl)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f1287,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(xn,sK2_skl))|sQ139_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f1285])).
% 9.82/1.77 fof(f1293,plain,(
% 9.82/1.77 ~aNaturalNumber0(xm)|sQ139_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f87,f1287])).
% 9.82/1.77 fof(f1294,plain,(
% 9.82/1.77 $false|sQ139_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f1293,f79])).
% 9.82/1.77 fof(f1295,plain,(
% 9.82/1.77 sQ139_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f1294])).
% 9.82/1.77 fof(f1587,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,sK1_skl),xm)=sdtpldt0(X0,sdtpldt0(sK1_skl,xm)))),
% 9.82/1.77 inference(resolution,[status(thm)],[f905,f79])).
% 9.82/1.77 fof(f1601,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,sK1_skl),xm)=sdtpldt0(X0,xn))),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f877,f1587])).
% 9.82/1.77 fof(f1628,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,xm),sK1_skl)=sdtpldt0(X0,sdtpldt0(xm,sK1_skl)))),
% 9.82/1.77 inference(resolution,[status(thm)],[f919,f79])).
% 9.82/1.77 fof(f1641,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,xm),sK1_skl)=sdtpldt0(X0,xn))),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f84,f1628])).
% 9.82/1.77 fof(f1663,definition,(
% 9.82/1.77 sQ183_spl <=> (sK2_skl=sz00)),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f1664,plain,(
% 9.82/1.77 sK2_skl=sz00|~sQ183_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f1663])).
% 9.82/1.77 fof(f1760,plain,(
% 9.82/1.77 sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xm)=sdtpldt0(sK2_skl,xn)),
% 9.82/1.77 inference(resolution,[status(thm)],[f1601,f86])).
% 9.82/1.77 fof(f1767,plain,(
% 9.82/1.77 sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xm)=xm|~sQ0_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f1254,f1760])).
% 9.82/1.77 fof(f2074,plain,(
% 9.82/1.77 sdtpldt0(sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xm),sK1_skl)=sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xn)),
% 9.82/1.77 inference(resolution,[status(thm)],[f1641,f169])).
% 9.82/1.77 fof(f2082,plain,(
% 9.82/1.77 sdtpldt0(xm,sK1_skl)=sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xn)|~sQ0_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f1767,f2074])).
% 9.82/1.77 fof(f2083,plain,(
% 9.82/1.77 xn=sdtpldt0(sdtpldt0(sK2_skl,sK1_skl),xn)|~sQ0_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f84,f2082])).
% 9.82/1.77 fof(f2395,plain,(
% 9.82/1.77 aNaturalNumber0(sdtpldt0(xm,sK2_skl))),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f866,f868])).
% 9.82/1.77 fof(f2436,plain,(
% 9.82/1.77 sdtpldt0(xm,sK2_skl)=sdtpldt0(sz00,sdtpldt0(xm,sK2_skl))),
% 9.82/1.77 inference(resolution,[status(thm)],[f2395,f40])).
% 9.82/1.77 fof(f2437,plain,(
% 9.82/1.77 sdtpldt0(sdtpldt0(xm,sK2_skl),sz00)=sdtpldt0(xm,sK2_skl)),
% 9.82/1.77 inference(resolution,[status(thm)],[f2395,f39])).
% 9.82/1.77 fof(f2500,definition,(
% 9.82/1.77 sQ291_spl <=> (sz00=sz10)),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ291_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f2501,plain,(
% 9.82/1.77 sz00=sz10|~sQ291_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f2500])).
% 9.82/1.77 fof(f2573,definition,(
% 9.82/1.77 sQ302_spl <=> (aNaturalNumber0(sdtpldt0(xm,sz00)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ302_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f2575,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(xm,sz00))|sQ302_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f2573])).
% 9.82/1.77 fof(f2590,plain,(
% 9.82/1.77 ~aNaturalNumber0(xm)|sQ302_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f873,f2575])).
% 9.82/1.77 fof(f2591,plain,(
% 9.82/1.77 $false|sQ302_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2590,f79])).
% 9.82/1.77 fof(f2592,plain,(
% 9.82/1.77 sQ302_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f2591])).
% 9.82/1.77 fof(f2629,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(xn)|~aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))|~aNaturalNumber0(X0)|~xn=sdtpldt0(X0,xn)|sdtpldt0(sK2_skl,sK1_skl)=X0|~sQ0_spl)),
% 9.82/1.77 inference(paramodulation,[status(thm)],[f2083,f56])).
% 9.82/1.77 fof(f2767,definition,(
% 9.82/1.77 ![X0]: (sQ321_spl <=> (~aNaturalNumber0(X0)|~xn=sdtpldt0(X0,xn)|sdtpldt0(sK2_skl,sK1_skl)=X0))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ321_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f2768,plain,(
% 9.82/1.77 ![X0]: (~aNaturalNumber0(X0)|~xn=sdtpldt0(X0,xn)|sdtpldt0(sK2_skl,sK1_skl)=X0|~sQ321_spl)),
% 9.82/1.77 inference(component_clause,[status(thm)],[f2767])).
% 9.82/1.77 fof(f2770,plain,(
% 9.82/1.77 ~sQ0_spl|~sQ10_spl|sQ321_spl),
% 9.82/1.77 inference(split_clause,[status(thm)],[f2629,f105,f182,f2767])).
% 9.82/1.77 fof(f3018,definition,(
% 9.82/1.77 sQ364_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sdtpldt0(xm,sK2_skl))))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ364_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3020,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(sz00,sdtpldt0(xm,sK2_skl)))|sQ364_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3018])).
% 9.82/1.77 fof(f3052,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(xm,sK2_skl))|sQ364_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f2436,f3020])).
% 9.82/1.77 fof(f3053,plain,(
% 9.82/1.77 $false|sQ364_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f3052,f2395])).
% 9.82/1.77 fof(f3054,plain,(
% 9.82/1.77 sQ364_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3053])).
% 9.82/1.77 fof(f3071,plain,(
% 9.82/1.77 sdtasdt0(sK2_skl,sz10)=sK2_skl),
% 9.82/1.77 inference(resolution,[status(thm)],[f46,f86])).
% 9.82/1.77 fof(f3072,plain,(
% 9.82/1.77 sdtasdt0(sK1_skl,sz10)=sK1_skl),
% 9.82/1.77 inference(resolution,[status(thm)],[f46,f83])).
% 9.82/1.77 fof(f3101,plain,(
% 9.82/1.77 sdtasdt0(sK2_skl,sz00)=sz00),
% 9.82/1.77 inference(resolution,[status(thm)],[f49,f86])).
% 9.82/1.77 fof(f3102,plain,(
% 9.82/1.77 sdtasdt0(sK1_skl,sz00)=sz00),
% 9.82/1.77 inference(resolution,[status(thm)],[f49,f83])).
% 9.82/1.77 fof(f3115,definition,(
% 9.82/1.77 sQ373_spl <=> (aNaturalNumber0(sdtpldt0(sdtpldt0(xm,sK2_skl),sz00)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3117,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(sdtpldt0(xm,sK2_skl),sz00))|sQ373_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3115])).
% 9.82/1.77 fof(f3140,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(xm,sK2_skl))|sQ373_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f2437,f3117])).
% 9.82/1.77 fof(f3141,plain,(
% 9.82/1.77 $false|sQ373_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f3140,f2395])).
% 9.82/1.77 fof(f3142,plain,(
% 9.82/1.77 sQ373_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3141])).
% 9.82/1.77 fof(f3158,plain,(
% 9.82/1.77 ~xn=sdtpldt0(sz00,xn)|sdtpldt0(sK2_skl,sK1_skl)=sz00|~sQ321_spl),
% 9.82/1.77 inference(resolution,[status(thm)],[f2768,f27])).
% 9.82/1.77 fof(f3245,definition,(
% 9.82/1.77 sQ403_spl <=> (xn=sdtpldt0(sz00,xn))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ403_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3247,plain,(
% 9.82/1.77 ~xn=sdtpldt0(sz00,xn)|sQ403_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3245])).
% 9.82/1.77 fof(f3248,definition,(
% 9.82/1.77 sQ404_spl <=> (sdtpldt0(sK2_skl,sK1_skl)=sz00)),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ404_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3249,plain,(
% 9.82/1.77 sdtpldt0(sK2_skl,sK1_skl)=sz00|~sQ404_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3248])).
% 9.82/1.77 fof(f3251,plain,(
% 9.82/1.77 ~sQ403_spl|sQ404_spl|~sQ321_spl),
% 9.82/1.77 inference(split_clause,[status(thm)],[f3158,f3245,f3248,f2767])).
% 9.82/1.77 fof(f3271,plain,(
% 9.82/1.77 ~xn=xn|~sQ0_spl|sQ403_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f1249,f3247])).
% 9.82/1.77 fof(f3272,plain,(
% 9.82/1.77 $false|~sQ0_spl|sQ403_spl),
% 9.82/1.77 inference(trivial_equality_resolution,[status(thm)],[f3271])).
% 9.82/1.77 fof(f3273,plain,(
% 9.82/1.77 ~sQ0_spl|sQ403_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3272])).
% 9.82/1.77 fof(f3287,plain,(
% 9.82/1.77 sdtpldt0(sK1_skl,sK2_skl)=sz00|~sQ404_spl),
% 9.82/1.77 inference(backward_demodulation,[status(thm)],[f3249,f177])).
% 9.82/1.77 fof(f3408,definition,(
% 9.82/1.77 sQ427_spl <=> (aNaturalNumber0(sdtasdt0(sK2_skl,sz10)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3410,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtasdt0(sK2_skl,sz10))|sQ427_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3408])).
% 9.82/1.77 fof(f3430,plain,(
% 9.82/1.77 $false|~sQ291_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f2501,f29])).
% 9.82/1.77 fof(f3431,plain,(
% 9.82/1.77 ~sQ291_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3430])).
% 9.82/1.77 fof(f3432,plain,(
% 9.82/1.77 ~aNaturalNumber0(sK2_skl)|sQ427_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f3071,f3410])).
% 9.82/1.77 fof(f3433,plain,(
% 9.82/1.77 $false|sQ427_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f3432,f86])).
% 9.82/1.77 fof(f3434,plain,(
% 9.82/1.77 sQ427_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3433])).
% 9.82/1.77 fof(f3445,definition,(
% 9.82/1.77 sQ432_spl <=> (aNaturalNumber0(sdtasdt0(sK1_skl,sz10)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f3447,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtasdt0(sK1_skl,sz10))|sQ432_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f3445])).
% 9.82/1.77 fof(f3467,plain,(
% 9.82/1.77 ~aNaturalNumber0(sK1_skl)|sQ432_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f3072,f3447])).
% 9.82/1.77 fof(f3468,plain,(
% 9.82/1.77 $false|sQ432_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f3467,f83])).
% 9.82/1.77 fof(f3469,plain,(
% 9.82/1.77 sQ432_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f3468])).
% 9.82/1.77 fof(f4002,definition,(
% 9.82/1.77 sQ466_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sz00)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ466_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f4004,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtpldt0(sz00,sz00))|sQ466_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f4002])).
% 9.82/1.77 fof(f4009,definition,(
% 9.82/1.77 sQ468_spl <=> (aNaturalNumber0(sdtasdt0(sK1_skl,sz00)))),
% 9.82/1.77 introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition])).
% 9.82/1.77 fof(f4011,plain,(
% 9.82/1.77 ~aNaturalNumber0(sdtasdt0(sK1_skl,sz00))|sQ468_spl),
% 9.82/1.77 inference(component_clause,[status(thm)],[f4009])).
% 9.82/1.77 fof(f4027,plain,(
% 9.82/1.77 ~aNaturalNumber0(sz00)|sQ466_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f137,f4004])).
% 9.82/1.77 fof(f4028,plain,(
% 9.82/1.77 $false|sQ466_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f4027,f27])).
% 9.82/1.77 fof(f4029,plain,(
% 9.82/1.77 sQ466_spl),
% 9.82/1.77 inference(contradiction_clause,[status(thm)],[f4028])).
% 9.82/1.77 fof(f4030,plain,(
% 9.82/1.77 ~aNaturalNumber0(sz00)|sQ468_spl),
% 9.82/1.77 inference(forward_demodulation,[status(thm)],[f3102,f4011])).
% 9.82/1.77 fof(f4031,plain,(
% 9.82/1.77 $false|sQ468_spl),
% 9.82/1.77 inference(forward_subsumption_resolution,[status(thm)],[f4030,f27])).
% 9.82/1.80 fof(f4032,plain,(
% 9.82/1.80 sQ468_spl),
% 9.82/1.80 inference(contradiction_clause,[status(thm)],[f4031])).
% 9.82/1.80 fof(f4697,definition,(
% 9.82/1.80 sQ489_spl <=> (aNaturalNumber0(sdtasdt0(sK2_skl,sz00)))),
% 9.82/1.80 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 9.82/1.80 fof(f4699,plain,(
% 9.82/1.80 ~aNaturalNumber0(sdtasdt0(sK2_skl,sz00))|sQ489_spl),
% 9.82/1.80 inference(component_clause,[status(thm)],[f4697])).
% 9.82/1.80 fof(f4719,plain,(
% 9.82/1.80 ~aNaturalNumber0(sz00)|sQ489_spl),
% 9.82/1.80 inference(forward_demodulation,[status(thm)],[f3101,f4699])).
% 9.82/1.80 fof(f4720,plain,(
% 9.82/1.80 $false|sQ489_spl),
% 9.82/1.80 inference(forward_subsumption_resolution,[status(thm)],[f4719,f27])).
% 9.82/1.80 fof(f4721,plain,(
% 9.82/1.80 sQ489_spl),
% 9.82/1.80 inference(contradiction_clause,[status(thm)],[f4720])).
% 9.82/1.80 fof(f5199,plain,(
% 9.82/1.80 ~aNaturalNumber0(sK1_skl)|~aNaturalNumber0(sK2_skl)|sK2_skl=sz00|~sQ404_spl),
% 9.82/1.80 inference(resolution,[status(thm)],[f3287,f62])).
% 9.82/1.80 fof(f5210,plain,(
% 9.82/1.80 ~sQ5_spl|~sQ3_spl|sQ183_spl|~sQ404_spl),
% 9.82/1.80 inference(split_clause,[status(thm)],[f5199,f121,f114,f1663,f3248])).
% 9.82/1.80 fof(f7685,plain,(
% 9.82/1.80 xm=sdtpldt0(sz00,xn)|~sQ183_spl|~sQ0_spl),
% 9.82/1.80 inference(backward_demodulation,[status(thm)],[f1664,f1254])).
% 9.82/1.80 fof(f7721,plain,(
% 9.82/1.80 xm=xn|~sQ183_spl|~sQ0_spl),
% 9.82/1.80 inference(forward_demodulation,[status(thm)],[f1249,f7685])).
% 9.82/1.80 fof(f7722,plain,(
% 9.82/1.80 $false|~sQ183_spl|~sQ0_spl),
% 9.82/1.80 inference(forward_subsumption_resolution,[status(thm)],[f7721,f89])).
% 9.82/1.80 fof(f7723,plain,(
% 9.82/1.80 ~sQ183_spl|~sQ0_spl),
% 9.82/1.80 inference(contradiction_clause,[status(thm)],[f7722])).
% 9.82/1.80 fof(f7724,plain,(
% 9.82/1.80 $false),
% 9.82/1.80 inference(sat_refutation,[status(thm)],[f201,f203,f502,f861,f1295,f2592,f2770,f3054,f3142,f3251,f3273,f3431,f3434,f3469,f4029,f4032,f4721,f5210,f7723])).
% 9.82/1.80 % SZS output end CNFRefutation for theBenchmark.p
% 9.82/1.80 % Elapsed time: 1.350861 seconds
% 9.82/1.80 % CPU time: 10.266349 seconds
% 9.82/1.80 % Total memory used: 178.991 MB
% 9.82/1.80 % Net memory used: 173.213 MB
%------------------------------------------------------------------------------