%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM477+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 : n020.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:00 PM UTC 2026
% Result : Theorem 0.30s 1.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM477+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n020.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 02:34:17 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 0.30/1.05 % Refutation found
% 0.30/1.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.30/1.05 % SZS output start CNFRefutation for theBenchmark
% 0.30/1.05 fof(f2,axiom,(
% 0.30/1.05 aNaturalNumber0(sz00) ),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f3,axiom,(
% 0.30/1.05 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f8,axiom,(
% 0.30/1.05 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f11,axiom,(
% 0.30/1.05 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f12,axiom,(
% 0.30/1.05 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f25,axiom,(
% 0.30/1.05 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( W0 != sz00& W1 != W2& sdtlseqdt0(W1,W2) )=> ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2)& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)& sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) )),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f26,axiom,(
% 0.30/1.05 (! [W0] :( aNaturalNumber0(W0)=> ( W0 = sz00| W0 = sz10| ( sz10 != W0& sdtlseqdt0(sz10,W0) ) ) ) )),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f35,hypothesis,(
% 0.30/1.05 ( aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f36,hypothesis,(
% 0.30/1.05 ( (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xm,W0) ))& doDivides0(xm,xn)& xn != sz00 ) ),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f37,conjecture,(
% 0.30/1.05 ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))| sdtlseqdt0(xm,xn) ) ),
% 0.30/1.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.30/1.05 fof(f38,negated_conjecture,(
% 0.30/1.05 ~(( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))| sdtlseqdt0(xm,xn) ) )),
% 0.30/1.05 inference(negated_conjecture,[status(cth)],[f37])).
% 0.30/1.05 fof(f42,plain,(
% 0.30/1.05 aNaturalNumber0(sz00)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f2])).
% 0.30/1.05 fof(f43,plain,(
% 0.30/1.05 aNaturalNumber0(sz10)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f3])).
% 0.30/1.05 fof(f53,plain,(
% 0.30/1.05 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.30/1.05 fof(f54,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|sdtpldt0(X0,sz00)=X0)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f53])).
% 0.30/1.05 fof(f55,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|X0=sdtpldt0(sz00,X0))),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f53])).
% 0.30/1.05 fof(f60,plain,(
% 0.30/1.05 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.30/1.05 fof(f61,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f60])).
% 0.30/1.05 fof(f63,plain,(
% 0.30/1.05 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.30/1.05 fof(f64,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f63])).
% 0.30/1.05 fof(f106,plain,(
% 0.30/1.05 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|(((W0=sz00|W1=W2)|~sdtlseqdt0(W1,W2))|(((~sdtasdt0(W0,W1)=sdtasdt0(W0,W2)&sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)))&~sdtasdt0(W1,W0)=sdtasdt0(W2,W0))&sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)))))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.30/1.05 fof(f108,plain,(
% 0.30/1.05 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X0=sz00|X1=X2|~sdtlseqdt0(X1,X2)|sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f106])).
% 0.30/1.05 fof(f111,plain,(
% 0.30/1.05 ![W0]: (~aNaturalNumber0(W0)|((W0=sz00|W0=sz10)|(~sz10=W0&sdtlseqdt0(sz10,W0))))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.30/1.05 fof(f113,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|X0=sz10|sdtlseqdt0(sz10,X0))),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f111])).
% 0.30/1.05 fof(f138,plain,(
% 0.30/1.05 aNaturalNumber0(xm)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f35])).
% 0.30/1.05 fof(f139,plain,(
% 0.30/1.05 aNaturalNumber0(xn)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f35])).
% 0.30/1.05 fof(f140,plain,(
% 0.30/1.05 ((aNaturalNumber0(sK2_skl)&xn=sdtasdt0(xm,sK2_skl))&doDivides0(xm,xn))&~xn=sz00),
% 0.30/1.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W0,sK2_skl)],[f36])).
% 0.30/1.05 fof(f141,plain,(
% 0.30/1.05 aNaturalNumber0(sK2_skl)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f140])).
% 0.30/1.05 fof(f142,plain,(
% 0.30/1.05 xn=sdtasdt0(xm,sK2_skl)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f140])).
% 0.30/1.05 fof(f144,plain,(
% 0.30/1.05 ~xn=sz00),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f140])).
% 0.30/1.05 fof(f145,plain,(
% 0.30/1.05 ((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(xm,W0)=xn))&~sdtlseqdt0(xm,xn))),
% 0.30/1.05 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.30/1.05 fof(f146,plain,(
% 0.30/1.05 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xm,X0)=xn)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f145])).
% 0.30/1.05 fof(f147,plain,(
% 0.30/1.05 ~sdtlseqdt0(xm,xn)),
% 0.30/1.05 inference(cnf_transformation,[status(thm)],[f145])).
% 0.30/1.05 fof(f151,plain,(
% 0.30/1.05 ~sdtpldt0(xm,xn)=xn),
% 0.30/1.05 inference(resolution,[status(thm)],[f139,f146])).
% 0.30/1.05 fof(f173,plain,(
% 0.30/1.05 sdtpldt0(xm,sz00)=xm),
% 0.30/1.05 inference(resolution,[status(thm)],[f54,f138])).
% 0.30/1.05 fof(f198,plain,(
% 0.30/1.05 xn=sdtpldt0(sz00,xn)),
% 0.30/1.05 inference(resolution,[status(thm)],[f55,f139])).
% 0.30/1.05 fof(f224,plain,(
% 0.30/1.05 sdtasdt0(xm,sz10)=xm),
% 0.30/1.05 inference(resolution,[status(thm)],[f61,f138])).
% 0.30/1.05 fof(f234,plain,(
% 0.30/1.05 sdtasdt0(xm,sz00)=sz00),
% 0.30/1.05 inference(resolution,[status(thm)],[f64,f138])).
% 0.30/1.05 fof(f276,definition,(
% 0.30/1.05 sQ9_spl <=> (aNaturalNumber0(sz10))),
% 0.30/1.05 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.30/1.05 fof(f278,plain,(
% 0.30/1.05 ~aNaturalNumber0(sz10)|sQ9_spl),
% 0.30/1.05 inference(component_clause,[status(thm)],[f276])).
% 0.30/1.05 fof(f286,definition,(
% 0.30/1.05 sQ12_spl <=> (aNaturalNumber0(sK2_skl))),
% 0.30/1.05 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.30/1.05 fof(f288,plain,(
% 0.30/1.05 ~aNaturalNumber0(sK2_skl)|sQ12_spl),
% 0.30/1.05 inference(component_clause,[status(thm)],[f286])).
% 0.30/1.05 fof(f298,plain,(
% 0.30/1.05 $false|sQ12_spl),
% 0.30/1.05 inference(forward_subsumption_resolution,[status(thm)],[f288,f141])).
% 0.30/1.05 fof(f299,plain,(
% 0.30/1.05 sQ12_spl),
% 0.30/1.05 inference(contradiction_clause,[status(thm)],[f298])).
% 0.30/1.05 fof(f302,plain,(
% 0.30/1.05 $false|sQ9_spl),
% 0.30/1.05 inference(forward_subsumption_resolution,[status(thm)],[f278,f43])).
% 0.30/1.05 fof(f303,plain,(
% 0.30/1.05 sQ9_spl),
% 0.30/1.05 inference(contradiction_clause,[status(thm)],[f302])).
% 0.30/1.05 fof(f351,definition,(
% 0.30/1.05 sQ20_spl <=> (sK2_skl=sz00)),
% 0.30/1.05 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.30/1.05 fof(f352,plain,(
% 0.30/1.05 sK2_skl=sz00|~sQ20_spl),
% 0.30/1.05 inference(component_clause,[status(thm)],[f351])).
% 0.30/1.05 fof(f369,definition,(
% 0.30/1.05 sQ25_spl <=> (xn=sz00)),
% 0.30/1.05 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.30/1.05 fof(f370,plain,(
% 0.30/1.05 xn=sz00|~sQ25_spl),
% 0.30/1.05 inference(component_clause,[status(thm)],[f369])).
% 0.30/1.05 fof(f376,definition,(
% 0.30/1.05 sQ27_spl <=> (xm=sz00)),
% 0.30/1.05 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.30/1.05 fof(f377,plain,(
% 0.30/1.05 xm=sz00|~sQ27_spl),
% 0.30/1.05 inference(component_clause,[status(thm)],[f376])).
% 0.30/1.05 fof(f383,plain,(
% 0.30/1.05 $false|~sQ25_spl),
% 0.30/1.05 inference(forward_subsumption_resolution,[status(thm)],[f370,f144])).
% 0.30/1.05 fof(f384,plain,(
% 0.30/1.05 ~sQ25_spl),
% 0.30/1.05 inference(contradiction_clause,[status(thm)],[f383])).
% 0.30/1.05 fof(f419,plain,(
% 0.30/1.05 ~sdtpldt0(sz00,xn)=xn|~sQ27_spl),
% 0.30/1.05 inference(backward_demodulation,[status(thm)],[f377,f151])).
% 0.30/1.05 fof(f540,plain,(
% 0.30/1.05 ~xn=xn|~sQ27_spl),
% 0.30/1.05 inference(forward_demodulation,[status(thm)],[f198,f419])).
% 0.30/1.05 fof(f541,plain,(
% 0.30/1.05 $false|~sQ27_spl),
% 0.30/1.05 inference(trivial_equality_resolution,[status(thm)],[f540])).
% 0.30/1.05 fof(f542,plain,(
% 0.30/1.05 ~sQ27_spl),
% 0.30/1.05 inference(contradiction_clause,[status(thm)],[f541])).
% 0.30/1.05 fof(f663,plain,(
% 0.30/1.05 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|xm=sz00|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1)))),
% 0.30/1.05 inference(resolution,[status(thm)],[f108,f138])).
% 0.30/1.05 fof(f667,definition,(
% 0.30/1.05 ![X0,X1]: (sQ66_spl <=> (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1))))),
% 0.30/1.07 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.30/1.07 fof(f668,plain,(
% 0.30/1.07 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|sdtlseqdt0(sdtasdt0(xm,X0),sdtasdt0(xm,X1))|~sQ66_spl)),
% 0.30/1.07 inference(component_clause,[status(thm)],[f667])).
% 0.30/1.07 fof(f670,plain,(
% 0.30/1.07 sQ66_spl|sQ27_spl),
% 0.30/1.07 inference(split_clause,[status(thm)],[f663,f667,f376])).
% 0.30/1.07 fof(f855,plain,(
% 0.30/1.07 ~sdtpldt0(xm,sz00)=xn),
% 0.30/1.07 inference(resolution,[status(thm)],[f146,f42])).
% 0.30/1.07 fof(f1143,plain,(
% 0.30/1.07 sK2_skl=sz00|sK2_skl=sz10|sdtlseqdt0(sz10,sK2_skl)),
% 0.30/1.07 inference(resolution,[status(thm)],[f141,f113])).
% 0.30/1.07 fof(f1179,definition,(
% 0.30/1.07 sQ121_spl <=> (sK2_skl=sz10)),
% 0.30/1.07 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.30/1.07 fof(f1180,plain,(
% 0.30/1.07 sK2_skl=sz10|~sQ121_spl),
% 0.30/1.07 inference(component_clause,[status(thm)],[f1179])).
% 0.30/1.07 fof(f1182,definition,(
% 0.30/1.07 sQ122_spl <=> (sdtlseqdt0(sz10,sK2_skl))),
% 0.30/1.07 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.30/1.07 fof(f1183,plain,(
% 0.30/1.07 sdtlseqdt0(sz10,sK2_skl)|~sQ122_spl),
% 0.30/1.07 inference(component_clause,[status(thm)],[f1182])).
% 0.30/1.07 fof(f1185,plain,(
% 0.30/1.07 sQ20_spl|sQ121_spl|sQ122_spl),
% 0.30/1.07 inference(split_clause,[status(thm)],[f1143,f351,f1179,f1182])).
% 0.30/1.07 fof(f1666,plain,(
% 0.30/1.07 ~xm=xn),
% 0.30/1.07 inference(forward_demodulation,[status(thm)],[f173,f855])).
% 0.30/1.07 fof(f1675,plain,(
% 0.30/1.07 xn=sdtasdt0(xm,sz00)|~sQ20_spl),
% 0.30/1.07 inference(forward_demodulation,[status(thm)],[f352,f142])).
% 0.30/1.07 fof(f1676,plain,(
% 0.30/1.07 xn=sz00|~sQ20_spl),
% 0.30/1.07 inference(forward_demodulation,[status(thm)],[f234,f1675])).
% 0.30/1.07 fof(f1945,plain,(
% 0.30/1.07 xn=sdtasdt0(xm,sz10)|~sQ121_spl),
% 0.30/1.07 inference(backward_demodulation,[status(thm)],[f1180,f142])).
% 0.30/1.07 fof(f1983,plain,(
% 0.30/1.07 sQ25_spl|~sQ20_spl),
% 0.30/1.07 inference(split_clause,[status(thm)],[f1676,f369,f351])).
% 0.30/1.07 fof(f2500,definition,(
% 0.30/1.07 sQ235_spl <=> (xn=xm)),
% 0.30/1.07 introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition])).
% 0.30/1.07 fof(f2501,plain,(
% 0.30/1.07 xn=xm|~sQ235_spl),
% 0.30/1.07 inference(component_clause,[status(thm)],[f2500])).
% 0.30/1.07 fof(f2614,plain,(
% 0.30/1.07 $false|~sQ235_spl),
% 0.30/1.07 inference(forward_subsumption_resolution,[status(thm)],[f2501,f1666])).
% 0.30/1.07 fof(f2615,plain,(
% 0.30/1.07 ~sQ235_spl),
% 0.30/1.07 inference(contradiction_clause,[status(thm)],[f2614])).
% 0.30/1.07 fof(f4202,plain,(
% 0.30/1.07 xn=xm|~sQ121_spl),
% 0.30/1.07 inference(backward_demodulation,[status(thm)],[f224,f1945])).
% 0.30/1.07 fof(f4203,plain,(
% 0.30/1.07 sQ235_spl|~sQ121_spl),
% 0.30/1.07 inference(split_clause,[status(thm)],[f4202,f2500,f1179])).
% 0.30/1.07 fof(f4903,plain,(
% 0.30/1.07 ~aNaturalNumber0(sz10)|~aNaturalNumber0(sK2_skl)|sz10=sK2_skl|sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK2_skl))|~sQ66_spl|~sQ122_spl),
% 0.30/1.07 inference(resolution,[status(thm)],[f668,f1183])).
% 0.30/1.07 fof(f4918,definition,(
% 0.30/1.07 sQ538_spl <=> (sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK2_skl)))),
% 0.30/1.07 introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition])).
% 0.30/1.07 fof(f4919,plain,(
% 0.30/1.07 sdtlseqdt0(sdtasdt0(xm,sz10),sdtasdt0(xm,sK2_skl))|~sQ538_spl),
% 0.30/1.07 inference(component_clause,[status(thm)],[f4918])).
% 0.30/1.07 fof(f4921,plain,(
% 0.30/1.07 ~sQ9_spl|~sQ12_spl|sQ121_spl|sQ538_spl|~sQ66_spl|~sQ122_spl),
% 0.30/1.07 inference(split_clause,[status(thm)],[f4903,f276,f286,f1179,f4918,f667,f1182])).
% 0.30/1.07 fof(f4930,plain,(
% 0.30/1.07 sdtlseqdt0(xm,sdtasdt0(xm,sK2_skl))|~sQ538_spl),
% 0.30/1.07 inference(forward_demodulation,[status(thm)],[f224,f4919])).
% 0.30/1.07 fof(f4931,plain,(
% 0.30/1.07 sdtlseqdt0(xm,xn)|~sQ538_spl),
% 0.30/1.07 inference(forward_demodulation,[status(thm)],[f142,f4930])).
% 0.30/1.07 fof(f4932,plain,(
% 0.30/1.07 $false|~sQ538_spl),
% 0.30/1.07 inference(forward_subsumption_resolution,[status(thm)],[f4931,f147])).
% 0.30/1.07 fof(f4933,plain,(
% 0.30/1.07 ~sQ538_spl),
% 0.30/1.07 inference(contradiction_clause,[status(thm)],[f4932])).
% 0.30/1.07 fof(f4934,plain,(
% 0.30/1.07 $false),
% 0.30/1.07 inference(sat_refutation,[status(thm)],[f299,f303,f384,f542,f670,f1185,f1983,f2615,f4203,f4921,f4933])).
% 0.30/1.07 % SZS output end CNFRefutation for theBenchmark.p
% 0.30/1.11 % Elapsed time: 0.637764 seconds
% 0.30/1.11 % CPU time: 3.989009 seconds
% 0.30/1.11 % Total memory used: 131.842 MB
% 0.30/1.11 % Net memory used: 129.626 MB
%------------------------------------------------------------------------------