%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM460+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 : n017.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 86.09s 11.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM460+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.41 % Computer : n017.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 02:27:27 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 86.09/11.37 % Refutation found
% 86.09/11.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 86.09/11.37 % SZS output start CNFRefutation for theBenchmark
% 86.09/11.37 fof(f2,axiom,(
% 86.09/11.37 aNaturalNumber0(sz00) ),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f3,axiom,(
% 86.09/11.37 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f4,axiom,(
% 86.09/11.37 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f6,axiom,(
% 86.09/11.37 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f7,axiom,(
% 86.09/11.37 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f8,axiom,(
% 86.09/11.37 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f11,axiom,(
% 86.09/11.37 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f12,axiom,(
% 86.09/11.37 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f22,hypothesis,(
% 86.09/11.37 ( aNaturalNumber0(xm)& aNaturalNumber0(xn)& aNaturalNumber0(xl) ) ),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f23,conjecture,(
% 86.09/11.37 ( ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))& sdtlseqdt0(xm,xn)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xl ))& sdtlseqdt0(xn,xl) )=> ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xl ))| sdtlseqdt0(xm,xl) ) ) ),
% 86.09/11.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 86.09/11.37 fof(f24,negated_conjecture,(
% 86.09/11.37 ~(( ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))& sdtlseqdt0(xm,xn)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xn,W0) = xl ))& sdtlseqdt0(xn,xl) )=> ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xl ))| sdtlseqdt0(xm,xl) ) ) )),
% 86.09/11.37 inference(negated_conjecture,[status(cth)],[f23])).
% 86.09/11.37 fof(f28,plain,(
% 86.09/11.37 aNaturalNumber0(sz00)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f2])).
% 86.09/11.37 fof(f29,plain,(
% 86.09/11.37 aNaturalNumber0(sz10)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f3])).
% 86.09/11.37 fof(f30,plain,(
% 86.09/11.37 ~sz10=sz00),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f3])).
% 86.09/11.37 fof(f31,plain,(
% 86.09/11.37 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 86.09/11.37 fof(f32,plain,(
% 86.09/11.37 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f31])).
% 86.09/11.37 fof(f35,plain,(
% 86.09/11.37 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 86.09/11.37 fof(f36,plain,(
% 86.09/11.37 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f35])).
% 86.09/11.37 fof(f37,plain,(
% 86.09/11.37 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 86.09/11.37 fof(f38,plain,(
% 86.09/11.37 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f37])).
% 86.09/11.37 fof(f39,plain,(
% 86.09/11.37 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 86.09/11.37 fof(f40,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f39])).
% 86.09/11.37 fof(f41,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|X0=sdtpldt0(sz00,X0))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f39])).
% 86.09/11.37 fof(f46,plain,(
% 86.09/11.37 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 86.09/11.37 fof(f47,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f46])).
% 86.09/11.37 fof(f48,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|X0=sdtasdt0(sz10,X0))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f46])).
% 86.09/11.37 fof(f49,plain,(
% 86.09/11.37 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 86.09/11.37 fof(f50,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f49])).
% 86.09/11.37 fof(f51,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sz00=sdtasdt0(sz00,X0))),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f49])).
% 86.09/11.37 fof(f82,plain,(
% 86.09/11.37 aNaturalNumber0(xm)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f22])).
% 86.09/11.37 fof(f83,plain,(
% 86.09/11.37 aNaturalNumber0(xn)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f22])).
% 86.09/11.37 fof(f84,plain,(
% 86.09/11.37 aNaturalNumber0(xl)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f22])).
% 86.09/11.37 fof(f85,plain,(
% 86.09/11.37 (((((?[W0]: (aNaturalNumber0(W0)&sdtpldt0(xm,W0)=xn))&sdtlseqdt0(xm,xn))&(?[W0]: (aNaturalNumber0(W0)&sdtpldt0(xn,W0)=xl)))&sdtlseqdt0(xn,xl))&((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,W0)=xl))&~sdtlseqdt0(xm,xl)))),
% 86.09/11.37 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 86.09/11.37 fof(f86,plain,(
% 86.09/11.37 ((((aNaturalNumber0(sK1_skl)&sdtpldt0(xm,sK1_skl)=xn)&sdtlseqdt0(xm,xn))&(aNaturalNumber0(sK2_skl)&sdtpldt0(xn,sK2_skl)=xl))&sdtlseqdt0(xn,xl))&((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,W0)=xl))&~sdtlseqdt0(xm,xl))),
% 86.09/11.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(W0,sK1_skl),skolemize(W0,sK2_skl)],[f85])).
% 86.09/11.37 fof(f87,plain,(
% 86.09/11.37 aNaturalNumber0(sK1_skl)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f86])).
% 86.09/11.37 fof(f88,plain,(
% 86.09/11.37 sdtpldt0(xm,sK1_skl)=xn),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f86])).
% 86.09/11.37 fof(f90,plain,(
% 86.09/11.37 aNaturalNumber0(sK2_skl)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f86])).
% 86.09/11.37 fof(f91,plain,(
% 86.09/11.37 sdtpldt0(xn,sK2_skl)=xl),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f86])).
% 86.09/11.37 fof(f93,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xm,X0)=xl)),
% 86.09/11.37 inference(cnf_transformation,[status(thm)],[f86])).
% 86.09/11.37 fof(f97,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(sK2_skl,X0)))),
% 86.09/11.37 inference(resolution,[status(thm)],[f32,f90])).
% 86.09/11.37 fof(f99,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sK2_skl)=sdtpldt0(sK2_skl,X0))),
% 86.09/11.37 inference(resolution,[status(thm)],[f36,f90])).
% 86.09/11.37 fof(f110,definition,(
% 86.09/11.37 sQ0_spl <=> (aNaturalNumber0(xn))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f111,plain,(
% 86.09/11.37 aNaturalNumber0(xn)|~sQ0_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f110])).
% 86.09/11.37 fof(f112,plain,(
% 86.09/11.37 ~aNaturalNumber0(xn)|sQ0_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f110])).
% 86.09/11.37 fof(f113,definition,(
% 86.09/11.37 sQ1_spl <=> (aNaturalNumber0(xl))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f115,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ1_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f113])).
% 86.09/11.37 fof(f123,definition,(
% 86.09/11.37 sQ4_spl <=> (aNaturalNumber0(xm))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f124,plain,(
% 86.09/11.37 aNaturalNumber0(xm)|~sQ4_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f123])).
% 86.09/11.37 fof(f125,plain,(
% 86.09/11.37 ~aNaturalNumber0(xm)|sQ4_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f123])).
% 86.09/11.37 fof(f147,plain,(
% 86.09/11.37 sz00=sdtpldt0(sz00,sz00)),
% 86.09/11.37 inference(resolution,[status(thm)],[f28,f41])).
% 86.09/11.37 fof(f153,plain,(
% 86.09/11.37 sz10=sdtpldt0(sz00,sz10)),
% 86.09/11.37 inference(resolution,[status(thm)],[f29,f41])).
% 86.09/11.37 fof(f154,plain,(
% 86.09/11.37 sdtpldt0(sz10,sz00)=sz10),
% 86.09/11.37 inference(resolution,[status(thm)],[f29,f40])).
% 86.09/11.37 fof(f184,plain,(
% 86.09/11.37 aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))),
% 86.09/11.37 inference(resolution,[status(thm)],[f97,f87])).
% 86.09/11.37 fof(f395,definition,(
% 86.09/11.37 sQ31_spl <=> (aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f397,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))|sQ31_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f395])).
% 86.09/11.37 fof(f413,plain,(
% 86.09/11.37 $false|sQ31_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f397,f184])).
% 86.09/11.37 fof(f414,plain,(
% 86.09/11.37 sQ31_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f413])).
% 86.09/11.37 fof(f867,plain,(
% 86.09/11.37 $false|sQ4_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f82,f125])).
% 86.09/11.37 fof(f868,plain,(
% 86.09/11.37 sQ4_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f867])).
% 86.09/11.37 fof(f869,plain,(
% 86.09/11.37 $false|sQ0_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f83,f112])).
% 86.09/11.37 fof(f870,plain,(
% 86.09/11.37 sQ0_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f869])).
% 86.09/11.37 fof(f881,plain,(
% 86.09/11.37 xl=sdtpldt0(sz00,xl)),
% 86.09/11.37 inference(resolution,[status(thm)],[f84,f41])).
% 86.09/11.37 fof(f882,plain,(
% 86.09/11.37 sdtpldt0(xl,sz00)=xl),
% 86.09/11.37 inference(resolution,[status(thm)],[f84,f40])).
% 86.09/11.37 fof(f911,plain,(
% 86.09/11.37 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(sdtpldt0(X0,sK2_skl),X1)=sdtpldt0(X0,sdtpldt0(sK2_skl,X1)))),
% 86.09/11.37 inference(resolution,[status(thm)],[f38,f90])).
% 86.09/11.37 fof(f927,plain,(
% 86.09/11.37 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtpldt0(sdtpldt0(X0,X1),sK1_skl)=sdtpldt0(X0,sdtpldt0(X1,sK1_skl)))),
% 86.09/11.37 inference(resolution,[status(thm)],[f38,f87])).
% 86.09/11.37 fof(f1049,definition,(
% 86.09/11.37 ![X0]: (sQ111_spl <=> (~aNaturalNumber0(X0)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f1050,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|~sQ111_spl)),
% 86.09/11.37 inference(component_clause,[status(thm)],[f1049])).
% 86.09/11.37 fof(f1281,plain,(
% 86.09/11.37 sdtpldt0(xm,sK2_skl)=sdtpldt0(sK2_skl,xm)|~sQ4_spl),
% 86.09/11.37 inference(resolution,[status(thm)],[f124,f99])).
% 86.09/11.37 fof(f1295,definition,(
% 86.09/11.37 sQ139_spl <=> (aNaturalNumber0(sdtpldt0(xm,sK1_skl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f1297,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(xm,sK1_skl))|sQ139_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f1295])).
% 86.09/11.37 fof(f1303,plain,(
% 86.09/11.37 ~aNaturalNumber0(xn)|sQ139_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f88,f1297])).
% 86.09/11.37 fof(f1308,definition,(
% 86.09/11.37 sQ141_spl <=> (aNaturalNumber0(sdtpldt0(sz00,xl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f1310,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(sz00,xl))|sQ141_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f1308])).
% 86.09/11.37 fof(f1315,definition,(
% 86.09/11.37 sQ143_spl <=> (aNaturalNumber0(sdtpldt0(xl,sz00)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f1317,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(xl,sz00))|sQ143_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f1315])).
% 86.09/11.37 fof(f1322,definition,(
% 86.09/11.37 sQ145_spl <=> (aNaturalNumber0(sdtpldt0(xn,sK2_skl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f1324,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(xn,sK2_skl))|sQ145_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f1322])).
% 86.09/11.37 fof(f1330,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ141_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f881,f1310])).
% 86.09/11.37 fof(f1331,plain,(
% 86.09/11.37 $false|sQ141_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f1330,f84])).
% 86.09/11.37 fof(f1332,plain,(
% 86.09/11.37 sQ141_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f1331])).
% 86.09/11.37 fof(f1333,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ143_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f882,f1317])).
% 86.09/11.37 fof(f1334,plain,(
% 86.09/11.37 $false|sQ143_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f1333,f84])).
% 86.09/11.37 fof(f1335,plain,(
% 86.09/11.37 sQ143_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f1334])).
% 86.09/11.37 fof(f1336,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ145_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f91,f1324])).
% 86.09/11.37 fof(f1337,plain,(
% 86.09/11.37 $false|sQ145_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f1336,f84])).
% 86.09/11.37 fof(f1338,plain,(
% 86.09/11.37 sQ145_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f1337])).
% 86.09/11.37 fof(f1345,plain,(
% 86.09/11.37 $false|sQ1_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f115,f84])).
% 86.09/11.37 fof(f1346,plain,(
% 86.09/11.37 sQ1_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f1345])).
% 86.09/11.37 fof(f1363,plain,(
% 86.09/11.37 sdtpldt0(xn,sK2_skl)=sdtpldt0(sK2_skl,xn)|~sQ0_spl),
% 86.09/11.37 inference(resolution,[status(thm)],[f111,f99])).
% 86.09/11.37 fof(f1374,plain,(
% 86.09/11.37 xl=sdtpldt0(sK2_skl,xn)|~sQ0_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f91,f1363])).
% 86.09/11.37 fof(f1622,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,sK2_skl),sK1_skl)=sdtpldt0(X0,sdtpldt0(sK2_skl,sK1_skl)))),
% 86.09/11.37 inference(resolution,[status(thm)],[f911,f87])).
% 86.09/11.37 fof(f1693,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,xm),sK1_skl)=sdtpldt0(X0,sdtpldt0(xm,sK1_skl))|~sQ4_spl)),
% 86.09/11.37 inference(resolution,[status(thm)],[f927,f124])).
% 86.09/11.37 fof(f1708,plain,(
% 86.09/11.37 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(sdtpldt0(X0,xm),sK1_skl)=sdtpldt0(X0,xn)|~sQ4_spl)),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f88,f1693])).
% 86.09/11.37 fof(f3057,plain,(
% 86.09/11.37 sdtasdt0(xl,sz10)=xl),
% 86.09/11.37 inference(resolution,[status(thm)],[f47,f84])).
% 86.09/11.37 fof(f3062,plain,(
% 86.09/11.37 xl=sdtasdt0(sz10,xl)),
% 86.09/11.37 inference(resolution,[status(thm)],[f48,f84])).
% 86.09/11.37 fof(f3079,plain,(
% 86.09/11.37 sdtasdt0(sK1_skl,sz00)=sz00),
% 86.09/11.37 inference(resolution,[status(thm)],[f87,f50])).
% 86.09/11.37 fof(f3166,plain,(
% 86.09/11.37 sdtasdt0(sK2_skl,sz00)=sz00),
% 86.09/11.37 inference(resolution,[status(thm)],[f90,f50])).
% 86.09/11.37 fof(f3800,plain,(
% 86.09/11.37 $false|~sQ111_spl),
% 86.09/11.37 inference(backward_subsumption_resolution,[status(thm)],[f90,f1050])).
% 86.09/11.37 fof(f3806,plain,(
% 86.09/11.37 ~sQ111_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f3800])).
% 86.09/11.37 fof(f3807,plain,(
% 86.09/11.37 sz00=sdtasdt0(sz00,sK2_skl)),
% 86.09/11.37 inference(resolution,[status(thm)],[f51,f90])).
% 86.09/11.37 fof(f3808,plain,(
% 86.09/11.37 sz00=sdtasdt0(sz00,sK1_skl)),
% 86.09/11.37 inference(resolution,[status(thm)],[f51,f87])).
% 86.09/11.37 fof(f3933,definition,(
% 86.09/11.37 sQ380_spl <=> (sz10=sz00)),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f3934,plain,(
% 86.09/11.37 sz10=sz00|~sQ380_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f3933])).
% 86.09/11.37 fof(f3947,plain,(
% 86.09/11.37 $false|~sQ380_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f3934,f30])).
% 86.09/11.37 fof(f3948,plain,(
% 86.09/11.37 ~sQ380_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f3947])).
% 86.09/11.37 fof(f9046,definition,(
% 86.09/11.37 sQ718_spl <=> (aNaturalNumber0(sdtasdt0(sz00,sK1_skl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f9048,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(sz00,sK1_skl))|sQ718_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f9046])).
% 86.09/11.37 fof(f9053,definition,(
% 86.09/11.37 sQ720_spl <=> (aNaturalNumber0(sdtasdt0(sz00,sK2_skl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f9055,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(sz00,sK2_skl))|sQ720_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f9053])).
% 86.09/11.37 fof(f9060,definition,(
% 86.09/11.37 sQ722_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sz00)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f9062,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(sz00,sz00))|sQ722_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f9060])).
% 86.09/11.37 fof(f9067,definition,(
% 86.09/11.37 sQ724_spl <=> (aNaturalNumber0(sdtasdt0(sK1_skl,sz00)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f9069,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(sK1_skl,sz00))|sQ724_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f9067])).
% 86.09/11.37 fof(f9074,definition,(
% 86.09/11.37 sQ726_spl <=> (aNaturalNumber0(sdtasdt0(sK2_skl,sz00)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ726_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f9076,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(sK2_skl,sz00))|sQ726_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f9074])).
% 86.09/11.37 fof(f9083,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz00)|sQ726_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3166,f9076])).
% 86.09/11.37 fof(f9084,plain,(
% 86.09/11.37 $false|sQ726_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f9083,f28])).
% 86.09/11.37 fof(f9085,plain,(
% 86.09/11.37 sQ726_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f9084])).
% 86.09/11.37 fof(f9087,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz00)|sQ724_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3079,f9069])).
% 86.09/11.37 fof(f9088,plain,(
% 86.09/11.37 $false|sQ724_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f9087,f28])).
% 86.09/11.37 fof(f9089,plain,(
% 86.09/11.37 sQ724_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f9088])).
% 86.09/11.37 fof(f9091,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz00)|sQ722_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f147,f9062])).
% 86.09/11.37 fof(f9092,plain,(
% 86.09/11.37 $false|sQ722_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f9091,f28])).
% 86.09/11.37 fof(f9093,plain,(
% 86.09/11.37 sQ722_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f9092])).
% 86.09/11.37 fof(f9095,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz00)|sQ720_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3807,f9055])).
% 86.09/11.37 fof(f9096,plain,(
% 86.09/11.37 $false|sQ720_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f9095,f28])).
% 86.09/11.37 fof(f9097,plain,(
% 86.09/11.37 sQ720_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f9096])).
% 86.09/11.37 fof(f9099,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz00)|sQ718_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3808,f9048])).
% 86.09/11.37 fof(f9100,plain,(
% 86.09/11.37 $false|sQ718_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f9099,f28])).
% 86.09/11.37 fof(f9101,plain,(
% 86.09/11.37 sQ718_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f9100])).
% 86.09/11.37 fof(f10780,plain,(
% 86.09/11.37 sdtpldt0(sdtpldt0(sK2_skl,xm),sK1_skl)=sdtpldt0(sK2_skl,xn)|~sQ4_spl),
% 86.09/11.37 inference(resolution,[status(thm)],[f1708,f90])).
% 86.09/11.37 fof(f10786,plain,(
% 86.09/11.37 sdtpldt0(sdtpldt0(xm,sK2_skl),sK1_skl)=sdtpldt0(sK2_skl,xn)|~sQ4_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f1281,f10780])).
% 86.09/11.37 fof(f10787,plain,(
% 86.09/11.37 sdtpldt0(sdtpldt0(xm,sK2_skl),sK1_skl)=xl|~sQ0_spl|~sQ4_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f1374,f10786])).
% 86.09/11.37 fof(f12285,definition,(
% 86.09/11.37 sQ1018_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sz10)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f12287,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(sz00,sz10))|sQ1018_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f12285])).
% 86.09/11.37 fof(f12292,definition,(
% 86.09/11.37 sQ1020_spl <=> (aNaturalNumber0(sdtpldt0(sz10,sz00)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ1020_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f12294,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtpldt0(sz10,sz00))|sQ1020_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f12292])).
% 86.09/11.37 fof(f12301,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz10)|sQ1018_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f153,f12287])).
% 86.09/11.37 fof(f12302,plain,(
% 86.09/11.37 $false|sQ1018_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f12301,f29])).
% 86.09/11.37 fof(f12303,plain,(
% 86.09/11.37 sQ1018_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f12302])).
% 86.09/11.37 fof(f12304,plain,(
% 86.09/11.37 ~aNaturalNumber0(sz10)|sQ1020_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f154,f12294])).
% 86.09/11.37 fof(f12305,plain,(
% 86.09/11.37 $false|sQ1020_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f12304,f29])).
% 86.09/11.37 fof(f12306,plain,(
% 86.09/11.37 sQ1020_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f12305])).
% 86.09/11.37 fof(f13627,definition,(
% 86.09/11.37 sQ1153_spl <=> (aNaturalNumber0(sdtasdt0(xl,sz10)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ1153_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f13629,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(xl,sz10))|sQ1153_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f13627])).
% 86.09/11.37 fof(f13645,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ1153_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3057,f13629])).
% 86.09/11.37 fof(f13646,plain,(
% 86.09/11.37 $false|sQ1153_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f13645,f84])).
% 86.09/11.37 fof(f13647,plain,(
% 86.09/11.37 sQ1153_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f13646])).
% 86.09/11.37 fof(f14369,definition,(
% 86.09/11.37 sQ1174_spl <=> (aNaturalNumber0(sdtasdt0(sz10,xl)))),
% 86.09/11.37 introduced(definition,[new_symbols(definition,[sQ1174_spl])],[split_symbol_definition])).
% 86.09/11.37 fof(f14371,plain,(
% 86.09/11.37 ~aNaturalNumber0(sdtasdt0(sz10,xl))|sQ1174_spl),
% 86.09/11.37 inference(component_clause,[status(thm)],[f14369])).
% 86.09/11.37 fof(f14387,plain,(
% 86.09/11.37 ~aNaturalNumber0(xl)|sQ1174_spl),
% 86.09/11.37 inference(forward_demodulation,[status(thm)],[f3062,f14371])).
% 86.09/11.37 fof(f14388,plain,(
% 86.09/11.37 $false|sQ1174_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f14387,f84])).
% 86.09/11.37 fof(f14389,plain,(
% 86.09/11.37 sQ1174_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f14388])).
% 86.09/11.37 fof(f29880,plain,(
% 86.09/11.37 $false|sQ139_spl),
% 86.09/11.37 inference(forward_subsumption_resolution,[status(thm)],[f1303,f83])).
% 86.09/11.37 fof(f29881,plain,(
% 86.09/11.37 sQ139_spl),
% 86.09/11.37 inference(contradiction_clause,[status(thm)],[f29880])).
% 86.09/11.43 fof(f31129,plain,(
% 86.09/11.43 sdtpldt0(sdtpldt0(xm,sK2_skl),sK1_skl)=sdtpldt0(xm,sdtpldt0(sK2_skl,sK1_skl))),
% 86.09/11.43 inference(resolution,[status(thm)],[f1622,f82])).
% 86.09/11.43 fof(f31134,plain,(
% 86.09/11.43 xl=sdtpldt0(xm,sdtpldt0(sK2_skl,sK1_skl))|~sQ0_spl|~sQ4_spl),
% 86.09/11.43 inference(forward_demodulation,[status(thm)],[f10787,f31129])).
% 86.09/11.43 fof(f31452,plain,(
% 86.09/11.43 ~aNaturalNumber0(sdtpldt0(sK2_skl,sK1_skl))|~sQ0_spl|~sQ4_spl),
% 86.09/11.43 inference(resolution,[status(thm)],[f31134,f93])).
% 86.09/11.43 fof(f31472,plain,(
% 86.09/11.43 ~sQ31_spl|~sQ0_spl|~sQ4_spl),
% 86.09/11.43 inference(split_clause,[status(thm)],[f31452,f395,f110,f123])).
% 86.09/11.43 fof(f31500,plain,(
% 86.09/11.43 $false),
% 86.09/11.43 inference(sat_refutation,[status(thm)],[f414,f868,f870,f1332,f1335,f1338,f1346,f3806,f3948,f9085,f9089,f9093,f9097,f9101,f12303,f12306,f13647,f14389,f29881,f31472])).
% 86.09/11.43 % SZS output end CNFRefutation for theBenchmark.p
% 25.28/11.49 % Elapsed time: 11.045314 seconds
% 25.28/11.49 % CPU time: 86.886056 seconds
% 25.28/11.49 % Total memory used: 489.724 MB
% 25.28/11.49 % Net memory used: 458.149 MB
%------------------------------------------------------------------------------