%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 03:13:49 PM UTC 2026
% Result : Theorem 8.96s 2.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n016.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 10:39:37 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 8.96/2.19 % Refutation found
% 8.96/2.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.96/2.19 % SZS output start CNFRefutation for theBenchmark
% 8.96/2.19 fof(f4,axiom,(
% 8.96/2.19 (! [X] : proj1Suc(suc(X)) = X )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f7,axiom,(
% 8.96/2.19 half(zero) = zero ),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f8,axiom,(
% 8.96/2.19 half(suc(zero)) = zero ),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f9,axiom,(
% 8.96/2.19 (! [N] : half(suc(suc(N))) = suc(half(N)) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f10,axiom,(
% 8.96/2.19 evenNat(zero) ),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f11,axiom,(
% 8.96/2.19 (! [N] :( evenNat(suc(N))<=> ~ evenNat(N) ) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f12,axiom,(
% 8.96/2.19 shw(zero) = nil ),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f13,axiom,(
% 8.96/2.19 (! [Y] :( evenNat(suc(Y))=> shw(suc(Y)) = cons(o,shw(half(suc(Y)))) ) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f14,axiom,(
% 8.96/2.19 (! [Y] :( ~ evenNat(suc(Y))=> shw(suc(Y)) = cons(i,shw(half(suc(Y)))) ) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f15,axiom,(
% 8.96/2.19 (! [Y] : append(nil,Y) = Y )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f16,axiom,(
% 8.96/2.19 (! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f17,axiom,(
% 8.96/2.19 (! [Y] : addNat(zero,Y) = Y )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f18,axiom,(
% 8.96/2.19 (! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f19,axiom,(
% 8.96/2.19 (! [X] : double(X) = addNat(X,X) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f20,axiom,(
% 8.96/2.19 rd(nil) = zero ),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f21,axiom,(
% 8.96/2.19 (! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))) )),
% 8.96/2.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.19 fof(f22,axiom,(
% 8.96/2.20 (! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)) )),
% 8.96/2.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.20 fof(f23,axiom,(
% 8.96/2.20 (! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))) )),
% 8.96/2.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.20 fof(f24,conjecture,(
% 8.96/2.20 (? [X,Y] : x(X,Y) != x(Y,X) )),
% 8.96/2.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.96/2.20 fof(f25,negated_conjecture,(
% 8.96/2.20 ~((? [X,Y] : x(X,Y) != x(Y,X) ))),
% 8.96/2.20 inference(negated_conjecture,[status(cth)],[f24])).
% 8.96/2.20 fof(f29,plain,(
% 8.96/2.20 ![X0]: (proj1Suc(suc(X0))=X0)),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f4])).
% 8.96/2.20 fof(f32,plain,(
% 8.96/2.20 half(zero)=zero),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f7])).
% 8.96/2.20 fof(f33,plain,(
% 8.96/2.20 half(suc(zero))=zero),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f8])).
% 8.96/2.20 fof(f34,plain,(
% 8.96/2.20 ![X0]: (half(suc(suc(X0)))=suc(half(X0)))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f9])).
% 8.96/2.20 fof(f35,plain,(
% 8.96/2.20 evenNat(zero)),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f10])).
% 8.96/2.20 fof(f36,plain,(
% 8.96/2.20 ![N]: ((~evenNat(suc(N))|~evenNat(N))&(evenNat(suc(N))|evenNat(N)))),
% 8.96/2.20 inference(NNF_transformation,[status(thm)],[f11])).
% 8.96/2.20 fof(f37,plain,(
% 8.96/2.20 (![N]: (~evenNat(suc(N))|~evenNat(N)))&(![N]: (evenNat(suc(N))|evenNat(N)))),
% 8.96/2.20 inference(miniscoping,[status(thm)],[f36])).
% 8.96/2.20 fof(f38,plain,(
% 8.96/2.20 ![X0]: (~evenNat(suc(X0))|~evenNat(X0))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f37])).
% 8.96/2.20 fof(f39,plain,(
% 8.96/2.20 ![X0]: (evenNat(suc(X0))|evenNat(X0))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f37])).
% 8.96/2.20 fof(f40,plain,(
% 8.96/2.20 shw(zero)=nil),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f12])).
% 8.96/2.20 fof(f41,plain,(
% 8.96/2.20 ![Y]: (~evenNat(suc(Y))|shw(suc(Y))=cons(o,shw(half(suc(Y)))))),
% 8.96/2.20 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 8.96/2.20 fof(f42,plain,(
% 8.96/2.20 ![X0]: (~evenNat(suc(X0))|shw(suc(X0))=cons(o,shw(half(suc(X0)))))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f41])).
% 8.96/2.20 fof(f43,plain,(
% 8.96/2.20 ![Y]: (evenNat(suc(Y))|shw(suc(Y))=cons(i,shw(half(suc(Y)))))),
% 8.96/2.20 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 8.96/2.20 fof(f44,plain,(
% 8.96/2.20 ![X0]: (evenNat(suc(X0))|shw(suc(X0))=cons(i,shw(half(suc(X0)))))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f43])).
% 8.96/2.20 fof(f45,plain,(
% 8.96/2.20 ![X0]: (append(nil,X0)=X0)),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f15])).
% 8.96/2.20 fof(f46,plain,(
% 8.96/2.20 ![X0,X1,X2]: (append(cons(X0,X1),X2)=cons(X0,append(X1,X2)))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f16])).
% 8.96/2.20 fof(f47,plain,(
% 8.96/2.20 ![X0]: (addNat(zero,X0)=X0)),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f17])).
% 8.96/2.20 fof(f48,plain,(
% 8.96/2.20 ![X0,X1]: (addNat(suc(X0),X1)=suc(addNat(X0,X1)))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f18])).
% 8.96/2.20 fof(f49,plain,(
% 8.96/2.20 ![X0]: (double(X0)=addNat(X0,X0))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f19])).
% 8.96/2.20 fof(f50,plain,(
% 8.96/2.20 rd(nil)=zero),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f20])).
% 8.96/2.20 fof(f51,plain,(
% 8.96/2.20 ![X0]: (rd(cons(i,X0))=suc(double(rd(X0))))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f21])).
% 8.96/2.20 fof(f52,plain,(
% 8.96/2.20 ![X0]: (rd(cons(o,X0))=double(rd(X0)))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f22])).
% 8.96/2.20 fof(f53,plain,(
% 8.96/2.20 ![X0,X1]: (x(X0,X1)=rd(append(shw(X0),shw(X1))))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f23])).
% 8.96/2.20 fof(f54,plain,(
% 8.96/2.20 (![X,Y]: x(X,Y)=x(Y,X))),
% 8.96/2.20 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 8.96/2.20 fof(f55,plain,(
% 8.96/2.20 ![X0,X1]: (x(X0,X1)=x(X1,X0))),
% 8.96/2.20 inference(cnf_transformation,[status(thm)],[f54])).
% 8.96/2.20 fof(f80,plain,(
% 8.96/2.20 double(zero)=zero),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f47,f49])).
% 8.96/2.20 fof(f83,plain,(
% 8.96/2.20 ![X0]: (double(suc(X0))=suc(addNat(X0,suc(X0))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f49,f48])).
% 8.96/2.20 fof(f85,plain,(
% 8.96/2.20 ![X0]: (double(suc(suc(X0)))=suc(suc(addNat(X0,suc(suc(X0))))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f48,f83])).
% 8.96/2.20 fof(f86,plain,(
% 8.96/2.20 double(suc(zero))=suc(suc(zero))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f47,f83])).
% 8.96/2.20 fof(f92,plain,(
% 8.96/2.20 ![X0]: (proj1Suc(double(suc(X0)))=addNat(X0,suc(X0)))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f83,f29])).
% 8.96/2.20 fof(f101,plain,(
% 8.96/2.20 ![X0]: (shw(suc(X0))=cons(o,shw(half(suc(X0))))|evenNat(X0))),
% 8.96/2.20 inference(resolution,[status(thm)],[f42,f39])).
% 8.96/2.20 fof(f106,plain,(
% 8.96/2.20 ![X0]: (shw(suc(X0))=cons(i,shw(half(suc(X0))))|~evenNat(X0))),
% 8.96/2.20 inference(resolution,[status(thm)],[f44,f38])).
% 8.96/2.20 fof(f110,plain,(
% 8.96/2.20 ![X0]: (double(suc(X0))=suc(proj1Suc(double(suc(X0)))))),
% 8.96/2.20 inference(backward_demodulation,[status(thm)],[f92,f83])).
% 8.96/2.20 fof(f147,plain,(
% 8.96/2.20 ![X0]: (shw(suc(suc(X0)))=cons(o,shw(half(suc(suc(X0)))))|~evenNat(X0))),
% 8.96/2.20 inference(resolution,[status(thm)],[f101,f38])).
% 8.96/2.20 fof(f149,plain,(
% 8.96/2.20 ![X0]: (shw(suc(suc(X0)))=cons(o,shw(suc(half(X0))))|~evenNat(X0))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f34,f147])).
% 8.96/2.20 fof(f196,plain,(
% 8.96/2.20 ![X0]: (double(suc(suc(suc(X0))))=suc(suc(suc(addNat(X0,suc(suc(suc(X0))))))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f48,f85])).
% 8.96/2.20 fof(f197,plain,(
% 8.96/2.20 double(suc(suc(zero)))=suc(suc(suc(suc(zero))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f47,f85])).
% 8.96/2.20 fof(f256,plain,(
% 8.96/2.20 evenNat(double(suc(suc(zero))))|evenNat(suc(suc(suc(zero))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f197,f39])).
% 8.96/2.20 fof(f398,plain,(
% 8.96/2.20 shw(suc(zero))=cons(i,shw(half(suc(zero))))),
% 8.96/2.20 inference(resolution,[status(thm)],[f106,f35])).
% 8.96/2.20 fof(f404,plain,(
% 8.96/2.20 shw(suc(zero))=cons(i,shw(zero))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f33,f398])).
% 8.96/2.20 fof(f405,plain,(
% 8.96/2.20 shw(suc(zero))=cons(i,nil)),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f40,f404])).
% 8.96/2.20 fof(f428,plain,(
% 8.96/2.20 rd(shw(suc(zero)))=suc(double(rd(nil)))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f405,f51])).
% 8.96/2.20 fof(f429,plain,(
% 8.96/2.20 ![X0]: (append(shw(suc(zero)),X0)=cons(i,append(nil,X0)))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f405,f46])).
% 8.96/2.20 fof(f433,plain,(
% 8.96/2.20 rd(shw(suc(zero)))=suc(double(zero))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f50,f428])).
% 8.96/2.20 fof(f434,plain,(
% 8.96/2.20 rd(shw(suc(zero)))=suc(zero)),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f80,f433])).
% 8.96/2.20 fof(f435,plain,(
% 8.96/2.20 ![X0]: (append(shw(suc(zero)),X0)=cons(i,X0))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f45,f429])).
% 8.96/2.20 fof(f478,plain,(
% 8.96/2.20 ![X0]: (x(suc(zero),X0)=rd(cons(i,shw(X0))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f435,f53])).
% 8.96/2.20 fof(f482,plain,(
% 8.96/2.20 ![X0]: (x(suc(zero),X0)=suc(double(rd(shw(X0)))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f51,f478])).
% 8.96/2.20 fof(f587,plain,(
% 8.96/2.20 x(suc(zero),suc(zero))=suc(double(suc(zero)))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f434,f482])).
% 8.96/2.20 fof(f619,plain,(
% 8.96/2.20 ![X0]: (proj1Suc(x(suc(zero),X0))=double(rd(shw(X0))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f482,f29])).
% 8.96/2.20 fof(f621,plain,(
% 8.96/2.20 x(suc(zero),suc(zero))=suc(suc(suc(zero)))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f86,f587])).
% 8.96/2.20 fof(f718,plain,(
% 8.96/2.20 ![X0]: (proj1Suc(x(X0,suc(zero)))=double(rd(shw(X0))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f55,f619])).
% 8.96/2.20 fof(f1607,plain,(
% 8.96/2.20 shw(suc(suc(zero)))=cons(o,shw(suc(half(zero))))),
% 8.96/2.20 inference(resolution,[status(thm)],[f149,f35])).
% 8.96/2.20 fof(f1611,plain,(
% 8.96/2.20 shw(suc(suc(zero)))=cons(o,shw(suc(zero)))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f32,f1607])).
% 8.96/2.20 fof(f2061,plain,(
% 8.96/2.20 rd(shw(suc(suc(zero))))=double(rd(shw(suc(zero))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f1611,f52])).
% 8.96/2.20 fof(f2062,plain,(
% 8.96/2.20 ![X0]: (append(shw(suc(suc(zero))),X0)=cons(o,append(shw(suc(zero)),X0)))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f1611,f46])).
% 8.96/2.20 fof(f2066,plain,(
% 8.96/2.20 rd(shw(suc(suc(zero))))=double(suc(zero))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f434,f2061])).
% 8.96/2.20 fof(f2067,plain,(
% 8.96/2.20 rd(shw(suc(suc(zero))))=suc(suc(zero))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f86,f2066])).
% 8.96/2.20 fof(f2068,plain,(
% 8.96/2.20 ![X0]: (append(shw(suc(suc(zero))),X0)=cons(o,cons(i,X0)))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f435,f2062])).
% 8.96/2.20 fof(f11150,plain,(
% 8.96/2.20 ![X0]: (x(suc(suc(zero)),X0)=rd(cons(o,cons(i,shw(X0)))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f2068,f53])).
% 8.96/2.20 fof(f11156,plain,(
% 8.96/2.20 ![X0]: (x(suc(suc(zero)),X0)=double(rd(cons(i,shw(X0)))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f52,f11150])).
% 8.96/2.20 fof(f11157,plain,(
% 8.96/2.20 ![X0]: (x(suc(suc(zero)),X0)=double(suc(double(rd(shw(X0))))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f51,f11156])).
% 8.96/2.20 fof(f11158,plain,(
% 8.96/2.20 ![X0]: (x(suc(suc(zero)),X0)=double(x(suc(zero),X0)))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f482,f11157])).
% 8.96/2.20 fof(f11237,plain,(
% 8.96/2.20 proj1Suc(double(x(suc(zero),suc(zero))))=double(rd(shw(suc(suc(zero)))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f11158,f718])).
% 8.96/2.20 fof(f11330,plain,(
% 8.96/2.20 proj1Suc(double(suc(suc(suc(zero)))))=double(rd(shw(suc(suc(zero)))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f621,f11237])).
% 8.96/2.20 fof(f11331,plain,(
% 8.96/2.20 proj1Suc(double(suc(suc(suc(zero)))))=double(suc(suc(zero)))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f2067,f11330])).
% 8.96/2.20 fof(f12408,plain,(
% 8.96/2.20 double(suc(suc(suc(zero))))=suc(double(suc(suc(zero))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f11331,f110])).
% 8.96/2.20 fof(f16668,plain,(
% 8.96/2.20 double(suc(suc(suc(zero))))=suc(suc(suc(suc(suc(suc(zero))))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f47,f196])).
% 8.96/2.20 fof(f17008,plain,(
% 8.96/2.20 suc(double(suc(suc(zero))))=suc(suc(suc(suc(suc(suc(zero))))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f12408,f16668])).
% 8.96/2.20 fof(f17009,plain,(
% 8.96/2.20 suc(double(suc(suc(zero))))=suc(suc(double(suc(suc(zero)))))),
% 8.96/2.20 inference(forward_demodulation,[status(thm)],[f197,f17008])).
% 8.96/2.20 fof(f17948,plain,(
% 8.96/2.20 evenNat(suc(double(suc(suc(zero)))))|evenNat(suc(double(suc(suc(zero)))))),
% 8.96/2.20 inference(paramodulation,[status(thm)],[f17009,f39])).
% 8.96/2.20 fof(f18219,plain,(
% 8.96/2.20 evenNat(suc(double(suc(suc(zero)))))),
% 8.96/2.20 inference(duplicate_literals_removal,[status(thm)],[f17948])).
% 8.96/2.20 fof(f18223,plain,(
% 8.96/2.20 ~evenNat(double(suc(suc(zero))))),
% 8.96/2.20 inference(resolution,[status(thm)],[f18219,f38])).
% 8.96/2.20 fof(f18232,plain,(
% 8.96/2.20 evenNat(suc(suc(suc(zero))))),
% 8.96/2.20 inference(backward_subsumption_resolution,[status(thm)],[f256,f18223])).
% 8.96/2.20 fof(f18240,plain,(
% 8.96/2.20 ~evenNat(suc(suc(zero)))),
% 8.96/2.20 inference(resolution,[status(thm)],[f18232,f38])).
% 8.96/2.20 fof(f18254,plain,(
% 8.96/2.20 evenNat(suc(zero))),
% 8.96/2.20 inference(resolution,[status(thm)],[f18240,f39])).
% 8.96/2.20 fof(f18266,plain,(
% 8.96/2.20 ~evenNat(zero)),
% 8.96/2.20 inference(resolution,[status(thm)],[f18254,f38])).
% 8.96/2.20 fof(f18270,plain,(
% 8.96/2.20 $false),
% 8.96/2.20 inference(forward_subsumption_resolution,[status(thm)],[f18266,f35])).
% 8.96/2.20 % SZS output end CNFRefutation for theBenchmark.p
% 3.83/2.28 % Elapsed time: 1.798238 seconds
% 3.83/2.28 % CPU time: 13.690081 seconds
% 3.83/2.28 % Total memory used: 329.774 MB
% 3.83/2.28 % Net memory used: 325.570 MB
%------------------------------------------------------------------------------