%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM426+3 : 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 : n001.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:52 PM UTC 2026
% Result : Theorem 191.02s 24.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM426+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n001.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 02:33:58 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 191.02/24.72 % Refutation found
% 191.02/24.72 % SZS status Theorem for theBenchmark: Theorem is valid
% 191.02/24.72 % SZS output start CNFRefutation for theBenchmark
% 191.02/24.72 fof(f2,axiom,(
% 191.02/24.72 aInteger0(sz00) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f3,axiom,(
% 191.02/24.72 aInteger0(sz10) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f4,axiom,(
% 191.02/24.72 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f7,axiom,(
% 191.02/24.72 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f8,axiom,(
% 191.02/24.72 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f9,axiom,(
% 191.02/24.72 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f10,axiom,(
% 191.02/24.72 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f11,axiom,(
% 191.02/24.72 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f12,axiom,(
% 191.02/24.72 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f14,axiom,(
% 191.02/24.72 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f15,axiom,(
% 191.02/24.72 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f16,axiom,(
% 191.02/24.72 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0)& smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) )),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f21,hypothesis,(
% 191.02/24.72 ( aInteger0(xa)& aInteger0(xb)& aInteger0(xq)& xq != sz00 ) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f22,hypothesis,(
% 191.02/24.72 ( (? [W0] :( aInteger0(W0)& sdtasdt0(xq,W0) = sdtpldt0(xa,smndt0(xb)) ))& aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb)))& sdteqdtlpzmzozddtrp0(xa,xb,xq) ) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f23,hypothesis,(
% 191.02/24.72 ( aInteger0(xn)& sdtasdt0(xq,xn) = sdtpldt0(xa,smndt0(xb)) ) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f24,conjecture,(
% 191.02/24.72 sdtasdt0(xq,smndt0(xn)) = sdtpldt0(xb,smndt0(xa)) ),
% 191.02/24.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 191.02/24.72 fof(f25,negated_conjecture,(
% 191.02/24.72 ~(sdtasdt0(xq,smndt0(xn)) = sdtpldt0(xb,smndt0(xa)) )),
% 191.02/24.72 inference(negated_conjecture,[status(cth)],[f24])).
% 191.02/24.72 fof(f29,plain,(
% 191.02/24.72 aInteger0(sz00)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f2])).
% 191.80/24.72 fof(f30,plain,(
% 191.80/24.72 aInteger0(sz10)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f3])).
% 191.80/24.72 fof(f31,plain,(
% 191.80/24.72 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 191.80/24.72 fof(f32,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f31])).
% 191.80/24.72 fof(f37,plain,(
% 191.80/24.72 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 191.80/24.72 fof(f38,plain,(
% 191.80/24.72 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f37])).
% 191.80/24.72 fof(f39,plain,(
% 191.80/24.72 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 191.80/24.72 fof(f40,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f39])).
% 191.80/24.72 fof(f41,plain,(
% 191.80/24.72 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 191.80/24.72 fof(f43,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f41])).
% 191.80/24.72 fof(f44,plain,(
% 191.80/24.72 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 191.80/24.72 fof(f46,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f44])).
% 191.80/24.72 fof(f47,plain,(
% 191.80/24.72 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtasdt0(W0,sdtasdt0(W1,W2))=sdtasdt0(sdtasdt0(W0,W1),W2))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 191.80/24.72 fof(f48,plain,(
% 191.80/24.72 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtasdt0(X1,X2))=sdtasdt0(sdtasdt0(X0,X1),X2))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f47])).
% 191.80/24.72 fof(f49,plain,(
% 191.80/24.72 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 191.80/24.72 fof(f50,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f49])).
% 191.80/24.72 fof(f54,plain,(
% 191.80/24.72 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W0,W1),W2)=sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 191.80/24.72 fof(f56,plain,(
% 191.80/24.72 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f54])).
% 191.80/24.72 fof(f57,plain,(
% 191.80/24.72 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 191.80/24.72 fof(f59,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sz00=sdtasdt0(sz00,X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f57])).
% 191.80/24.72 fof(f60,plain,(
% 191.80/24.72 ![W0]: (~aInteger0(W0)|(sdtasdt0(smndt0(sz10),W0)=smndt0(W0)&smndt0(W0)=sdtasdt0(W0,smndt0(sz10))))),
% 191.80/24.72 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 191.80/24.72 fof(f61,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(smndt0(sz10),X0)=smndt0(X0))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f60])).
% 191.80/24.72 fof(f62,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|smndt0(X0)=sdtasdt0(X0,smndt0(sz10)))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f60])).
% 191.80/24.72 fof(f80,plain,(
% 191.80/24.72 aInteger0(xa)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f21])).
% 191.80/24.72 fof(f81,plain,(
% 191.80/24.72 aInteger0(xb)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f21])).
% 191.80/24.72 fof(f82,plain,(
% 191.80/24.72 aInteger0(xq)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f21])).
% 191.80/24.72 fof(f84,plain,(
% 191.80/24.72 ((aInteger0(sK1_skl)&sdtasdt0(xq,sK1_skl)=sdtpldt0(xa,smndt0(xb)))&aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb))))&sdteqdtlpzmzozddtrp0(xa,xb,xq)),
% 191.80/24.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W0,sK1_skl)],[f22])).
% 191.80/24.72 fof(f85,plain,(
% 191.80/24.72 aInteger0(sK1_skl)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f84])).
% 191.80/24.72 fof(f86,plain,(
% 191.80/24.72 sdtasdt0(xq,sK1_skl)=sdtpldt0(xa,smndt0(xb))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f84])).
% 191.80/24.72 fof(f89,plain,(
% 191.80/24.72 aInteger0(xn)),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f23])).
% 191.80/24.72 fof(f90,plain,(
% 191.80/24.72 sdtasdt0(xq,xn)=sdtpldt0(xa,smndt0(xb))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f23])).
% 191.80/24.72 fof(f91,plain,(
% 191.80/24.72 ~sdtasdt0(xq,smndt0(xn))=sdtpldt0(xb,smndt0(xa))),
% 191.80/24.72 inference(cnf_transformation,[status(thm)],[f25])).
% 191.80/24.72 fof(f96,plain,(
% 191.80/24.72 sdtasdt0(xq,sK1_skl)=sdtasdt0(xq,xn)),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f90,f86])).
% 191.80/24.72 fof(f102,plain,(
% 191.80/24.72 aInteger0(smndt0(xa))),
% 191.80/24.72 inference(resolution,[status(thm)],[f80,f32])).
% 191.80/24.72 fof(f113,plain,(
% 191.80/24.72 aInteger0(smndt0(xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f81,f32])).
% 191.80/24.72 fof(f129,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xq)=sdtasdt0(xq,X0))),
% 191.80/24.72 inference(resolution,[status(thm)],[f82,f50])).
% 191.80/24.72 fof(f135,plain,(
% 191.80/24.72 aInteger0(smndt0(xn))),
% 191.80/24.72 inference(resolution,[status(thm)],[f89,f32])).
% 191.80/24.72 fof(f160,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xb))=sdtpldt0(sdtpldt0(X0,X1),xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f38,f81])).
% 191.80/24.72 fof(f172,plain,(
% 191.80/24.72 xb=sdtpldt0(sz00,xb)),
% 191.80/24.72 inference(resolution,[status(thm)],[f43,f81])).
% 191.80/24.72 fof(f174,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),xn)=smndt0(xn)),
% 191.80/24.72 inference(resolution,[status(thm)],[f61,f89])).
% 191.80/24.72 fof(f175,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),xq)=smndt0(xq)),
% 191.80/24.72 inference(resolution,[status(thm)],[f61,f82])).
% 191.80/24.72 fof(f178,plain,(
% 191.80/24.72 smndt0(xn)=sdtasdt0(xn,smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f62,f89])).
% 191.80/24.72 fof(f181,plain,(
% 191.80/24.72 smndt0(xa)=sdtasdt0(xa,smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f62,f80])).
% 191.80/24.72 fof(f216,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(sdtpldt0(X0,sz00),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(sz00,X1)))),
% 191.80/24.72 inference(resolution,[status(thm)],[f29,f56])).
% 191.80/24.72 fof(f223,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sz00,X0))),
% 191.80/24.72 inference(resolution,[status(thm)],[f29,f40])).
% 191.80/24.72 fof(f251,plain,(
% 191.80/24.72 aInteger0(smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f30,f32])).
% 191.80/24.72 fof(f262,plain,(
% 191.80/24.72 sz00=sdtpldt0(smndt0(xb),xb)),
% 191.80/24.72 inference(resolution,[status(thm)],[f46,f81])).
% 191.80/24.72 fof(f279,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(X1,xq))=sdtasdt0(sdtasdt0(X0,X1),xq))),
% 191.80/24.72 inference(resolution,[status(thm)],[f48,f82])).
% 191.80/24.72 fof(f359,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xn,xq))=sdtasdt0(sdtasdt0(X0,xn),xq))),
% 191.80/24.72 inference(resolution,[status(thm)],[f279,f89])).
% 191.80/24.72 fof(f628,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(sK1_skl,xq))=sdtasdt0(sdtasdt0(X0,sK1_skl),xq))),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f279])).
% 191.80/24.72 fof(f640,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(sK1_skl,X1))=sdtasdt0(sdtasdt0(X0,sK1_skl),X1))),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f48])).
% 191.80/24.72 fof(f646,plain,(
% 191.80/24.72 smndt0(sK1_skl)=sdtasdt0(sK1_skl,smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f62])).
% 191.80/24.72 fof(f647,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),sK1_skl)=smndt0(sK1_skl)),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f61])).
% 191.80/24.72 fof(f661,plain,(
% 191.80/24.72 aInteger0(smndt0(sK1_skl))),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f32])).
% 191.80/24.72 fof(f666,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sK1_skl)=sdtasdt0(sK1_skl,X0))),
% 191.80/24.72 inference(resolution,[status(thm)],[f85,f50])).
% 191.80/24.72 fof(f908,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(xa))=sdtpldt0(smndt0(xa),X0))),
% 191.80/24.72 inference(resolution,[status(thm)],[f102,f40])).
% 191.80/24.72 fof(f1055,plain,(
% 191.80/24.72 sdtasdt0(xq,sK1_skl)=sdtasdt0(sK1_skl,xq)),
% 191.80/24.72 inference(resolution,[status(thm)],[f666,f82])).
% 191.80/24.72 fof(f1080,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xq,xn))=sdtasdt0(sdtasdt0(X0,sK1_skl),xq))),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f1090,f628])).
% 191.80/24.72 fof(f1090,plain,(
% 191.80/24.72 sdtasdt0(xq,xn)=sdtasdt0(sK1_skl,xq)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f96,f1055])).
% 191.80/24.72 fof(f1458,plain,(
% 191.80/24.72 sdtpldt0(xb,smndt0(xa))=sdtpldt0(smndt0(xa),xb)),
% 191.80/24.72 inference(resolution,[status(thm)],[f908,f81])).
% 191.80/24.72 fof(f1513,plain,(
% 191.80/24.72 sz00=sdtasdt0(sz00,smndt0(xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f59])).
% 191.80/24.72 fof(f1532,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,sz00),smndt0(xb))=sdtpldt0(sdtasdt0(X0,smndt0(xb)),sdtasdt0(sz00,smndt0(xb))))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f216])).
% 191.80/24.72 fof(f1541,plain,(
% 191.80/24.72 sz00=sdtpldt0(smndt0(smndt0(xb)),smndt0(xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f46])).
% 191.80/24.72 fof(f1543,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(smndt0(xb),xb))=sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f160])).
% 191.80/24.72 fof(f1546,plain,(
% 191.80/24.72 smndt0(smndt0(xb))=sdtasdt0(smndt0(xb),smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f62])).
% 191.80/24.72 fof(f1547,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),smndt0(xb))=smndt0(smndt0(xb))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f61])).
% 191.80/24.72 fof(f1560,plain,(
% 191.80/24.72 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(smndt0(xb),X1)))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f56])).
% 191.80/24.72 fof(f1561,plain,(
% 191.80/24.72 aInteger0(smndt0(smndt0(xb)))),
% 191.80/24.72 inference(resolution,[status(thm)],[f113,f32])).
% 191.80/24.72 fof(f1614,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,sz00),smndt0(xb))=sdtpldt0(sdtasdt0(X0,smndt0(xb)),sz00))),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f1513,f1532])).
% 191.80/24.72 fof(f1622,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb))),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f262,f1543])).
% 191.80/24.72 fof(f2586,plain,(
% 191.80/24.72 sdtasdt0(xn,xq)=sdtasdt0(xq,xn)),
% 191.80/24.72 inference(resolution,[status(thm)],[f129,f89])).
% 191.80/24.72 fof(f2604,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xn,xq))=sdtasdt0(sdtasdt0(X0,sK1_skl),xq))),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f2586,f1080])).
% 191.80/24.72 fof(f2606,plain,(
% 191.80/24.72 sdtasdt0(xq,sK1_skl)=sdtasdt0(xn,xq)),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f2586,f96])).
% 191.80/24.72 fof(f2607,plain,(
% 191.80/24.72 sdtasdt0(xn,xq)=sdtpldt0(xa,smndt0(xb))),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f2586,f90])).
% 191.80/24.72 fof(f3184,plain,(
% 191.80/24.72 sdtasdt0(smndt0(xn),xq)=sdtasdt0(xq,smndt0(xn))),
% 191.80/24.72 inference(resolution,[status(thm)],[f135,f129])).
% 191.80/24.72 fof(f6826,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),sdtasdt0(xn,xq))=sdtasdt0(sdtasdt0(smndt0(sz10),sK1_skl),xq)),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f2604])).
% 191.80/24.72 fof(f6870,plain,(
% 191.80/24.72 sdtasdt0(sdtpldt0(smndt0(sz10),sz00),smndt0(xb))=sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xb)),sz00)),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f1614])).
% 191.80/24.72 fof(f6952,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(sK1_skl,smndt0(sz10)))=sdtasdt0(sdtasdt0(X0,sK1_skl),smndt0(sz10)))),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f640])).
% 191.80/24.72 fof(f6974,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(smndt0(sz10),xq))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xq))),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f279])).
% 191.80/24.72 fof(f6976,plain,(
% 191.80/24.72 sdtpldt0(smndt0(sz10),sz00)=sdtpldt0(sz00,smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f223])).
% 191.80/24.72 fof(f6994,plain,(
% 191.80/24.72 smndt0(sz10)=sdtpldt0(sz00,smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f251,f43])).
% 191.80/24.72 fof(f7063,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),sdtasdt0(xn,xq))=sdtasdt0(smndt0(sK1_skl),xq)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f647,f6826])).
% 191.80/24.72 fof(f7108,plain,(
% 191.80/24.72 sdtasdt0(sdtpldt0(smndt0(sz10),sz00),smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sz00)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f1547,f6870])).
% 191.80/24.72 fof(f7232,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(sK1_skl))=sdtasdt0(sdtasdt0(X0,sK1_skl),smndt0(sz10)))),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f646,f6952])).
% 191.80/24.72 fof(f7259,plain,(
% 191.80/24.72 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xq))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xq))),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f175,f6974])).
% 191.80/24.72 fof(f7269,plain,(
% 191.80/24.72 sdtasdt0(sdtpldt0(sz00,smndt0(sz10)),smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sz00)),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f6976,f7108])).
% 191.80/24.72 fof(f7322,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sz00)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f6994,f7269])).
% 191.80/24.72 fof(f7323,plain,(
% 191.80/24.72 smndt0(smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sz00)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f1547,f7322])).
% 191.80/24.72 fof(f8192,plain,(
% 191.80/24.72 sdtasdt0(xq,smndt0(sK1_skl))=sdtasdt0(sdtasdt0(xq,sK1_skl),smndt0(sz10))),
% 191.80/24.72 inference(resolution,[status(thm)],[f7232,f82])).
% 191.80/24.72 fof(f8204,plain,(
% 191.80/24.72 sdtasdt0(xq,smndt0(sK1_skl))=sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f2606,f8192])).
% 191.80/24.72 fof(f8397,plain,(
% 191.80/24.72 sdtasdt0(sK1_skl,smndt0(xq))=sdtasdt0(sdtasdt0(sK1_skl,smndt0(sz10)),xq)),
% 191.80/24.72 inference(resolution,[status(thm)],[f7259,f85])).
% 191.80/24.72 fof(f8400,plain,(
% 191.80/24.72 sdtasdt0(xn,smndt0(xq))=sdtasdt0(sdtasdt0(xn,smndt0(sz10)),xq)),
% 191.80/24.72 inference(resolution,[status(thm)],[f7259,f89])).
% 191.80/24.72 fof(f8410,plain,(
% 191.80/24.72 sdtasdt0(smndt0(sz10),sdtasdt0(xn,xq))=sdtasdt0(sK1_skl,smndt0(xq))),
% 191.80/24.72 inference(backward_demodulation,[status(thm)],[f8411,f7063])).
% 191.80/24.72 fof(f8411,plain,(
% 191.80/24.72 sdtasdt0(sK1_skl,smndt0(xq))=sdtasdt0(smndt0(sK1_skl),xq)),
% 191.80/24.72 inference(forward_demodulation,[status(thm)],[f646,f8397])).
% 191.80/24.72 fof(f8416,plain,(
% 191.80/24.72 sdtasdt0(xn,smndt0(xq))=sdtasdt0(xq,smndt0(xn))),
% 191.80/24.85 inference(backward_demodulation,[status(thm)],[f8417,f3184])).
% 191.80/24.85 fof(f8417,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtasdt0(smndt0(xn),xq)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f178,f8400])).
% 191.80/24.85 fof(f8421,plain,(
% 191.80/24.85 ~sdtasdt0(xn,smndt0(xq))=sdtpldt0(xb,smndt0(xa))),
% 191.80/24.85 inference(backward_demodulation,[status(thm)],[f8416,f91])).
% 191.80/24.85 fof(f9301,plain,(
% 191.80/24.85 sdtasdt0(smndt0(sz10),sdtasdt0(xn,xq))=sdtasdt0(sdtasdt0(smndt0(sz10),xn),xq)),
% 191.80/24.85 inference(resolution,[status(thm)],[f359,f251])).
% 191.80/24.85 fof(f9313,plain,(
% 191.80/24.85 sdtasdt0(sK1_skl,smndt0(xq))=sdtasdt0(sdtasdt0(smndt0(sz10),xn),xq)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f8410,f9301])).
% 191.80/24.85 fof(f9314,plain,(
% 191.80/24.85 sdtasdt0(sK1_skl,smndt0(xq))=sdtasdt0(smndt0(xn),xq)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f174,f9313])).
% 191.80/24.85 fof(f9343,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtasdt0(smndt0(sK1_skl),xq)),
% 191.80/24.85 inference(backward_demodulation,[status(thm)],[f9412,f8411])).
% 191.80/24.85 fof(f9412,plain,(
% 191.80/24.85 sdtasdt0(sK1_skl,smndt0(xq))=sdtasdt0(xn,smndt0(xq))),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f8417,f9314])).
% 191.80/24.85 fof(f10465,plain,(
% 191.80/24.85 sdtasdt0(smndt0(sK1_skl),xq)=sdtasdt0(xq,smndt0(sK1_skl))),
% 191.80/24.85 inference(resolution,[status(thm)],[f661,f129])).
% 191.80/24.85 fof(f10839,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))),
% 191.80/24.85 inference(backward_demodulation,[status(thm)],[f10840,f8204])).
% 191.80/24.85 fof(f10840,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtasdt0(xq,smndt0(sK1_skl))),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f9343,f10465])).
% 191.80/24.85 fof(f18742,plain,(
% 191.80/24.85 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(smndt0(xb),smndt0(sz10))))),
% 191.80/24.85 inference(resolution,[status(thm)],[f1560,f251])).
% 191.80/24.85 fof(f18754,plain,(
% 191.80/24.85 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),smndt0(smndt0(xb))))),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f1546,f18742])).
% 191.80/24.85 fof(f19055,plain,(
% 191.80/24.85 sdtpldt0(smndt0(smndt0(xb)),sz00)=sdtpldt0(sdtpldt0(smndt0(smndt0(xb)),smndt0(xb)),xb)),
% 191.80/24.85 inference(resolution,[status(thm)],[f1561,f1622])).
% 191.80/24.85 fof(f19533,plain,(
% 191.80/24.85 smndt0(smndt0(xb))=sdtpldt0(sdtpldt0(smndt0(smndt0(xb)),smndt0(xb)),xb)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f7323,f19055])).
% 191.80/24.85 fof(f19534,plain,(
% 191.80/24.85 smndt0(smndt0(xb))=sdtpldt0(sz00,xb)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f1541,f19533])).
% 191.80/24.85 fof(f19724,plain,(
% 191.80/24.85 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),xb))),
% 191.80/24.85 inference(backward_demodulation,[status(thm)],[f19747,f18754])).
% 191.80/24.85 fof(f19747,plain,(
% 191.80/24.85 smndt0(smndt0(xb))=xb),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f172,f19534])).
% 191.80/24.85 fof(f20954,plain,(
% 191.80/24.85 sdtasdt0(sdtpldt0(xa,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xb)),
% 191.80/24.85 inference(resolution,[status(thm)],[f19724,f80])).
% 191.80/24.85 fof(f20979,plain,(
% 191.80/24.85 sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xb)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f2607,f20954])).
% 191.80/24.85 fof(f20980,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xb)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f10839,f20979])).
% 191.80/24.85 fof(f20981,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtpldt0(smndt0(xa),xb)),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f181,f20980])).
% 191.80/24.85 fof(f20982,plain,(
% 191.80/24.85 sdtasdt0(xn,smndt0(xq))=sdtpldt0(xb,smndt0(xa))),
% 191.80/24.85 inference(forward_demodulation,[status(thm)],[f1458,f20981])).
% 191.80/24.85 fof(f20983,plain,(
% 191.80/24.85 $false),
% 191.80/24.85 inference(forward_subsumption_resolution,[status(thm)],[f20982,f8421])).
% 191.80/24.85 % SZS output end CNFRefutation for theBenchmark.p
% 55.78/24.95 % Elapsed time: 24.469465 seconds
% 55.78/24.95 % CPU time: 192.888324 seconds
% 55.78/24.95 % Total memory used: 1.179 GB
% 55.78/24.95 % Net memory used: 1.072 GB
%------------------------------------------------------------------------------