%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX199+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:46 PM UTC 2026
% Result : Theorem 0.14s 5.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX199+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.36 % Computer : n002.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Mon Sep 21 10:35:09 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.37 % Drodi V4.1.1
% 0.14/5.87 % Refutation found
% 0.14/5.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.87 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.87 fof(f1,axiom,(
% 0.14/5.87 (! [X,X2] : head(cons(X,X2)) = X )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f2,axiom,(
% 0.14/5.87 (! [X,X2] : tail(cons(X,X2)) = X2 )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f5,axiom,(
% 0.14/5.87 (! [X] : z != s(X) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f6,axiom,(
% 0.14/5.87 (! [Y] : leqNat(z,Y) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f7,axiom,(
% 0.14/5.87 (! [Z] : ~ leqNat(s(Z),z) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f9,axiom,(
% 0.14/5.87 (! [Y] : merge(nil,Y) = Y )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f10,axiom,(
% 0.14/5.87 (! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f11,axiom,(
% 0.14/5.87 (! [Z,Xs,Y2,Ys] :( leqNat(Z,Y2)=> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f12,axiom,(
% 0.14/5.87 (! [Z,Xs,Y2,Ys] :( ~ leqNat(Z,Y2)=> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)) ) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f13,conjecture,(
% 0.14/5.87 (? [Xs,Ys,Zs] :~ ( merge(Xs,Ys) = merge(Ys,Xs)=> ( merge(Xs,Zs) = merge(Zs,Xs)=> merge(Ys,Zs) = merge(Zs,Ys) ) ) )),
% 0.14/5.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f14,negated_conjecture,(
% 0.14/5.87 ~((? [Xs,Ys,Zs] :~ ( merge(Xs,Ys) = merge(Ys,Xs)=> ( merge(Xs,Zs) = merge(Zs,Xs)=> merge(Ys,Zs) = merge(Zs,Ys) ) ) ))),
% 0.14/5.87 inference(negated_conjecture,[status(cth)],[f13])).
% 0.14/5.87 fof(f15,plain,(
% 0.14/5.87 ![X0,X1]: (head(cons(X0,X1))=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/5.87 fof(f16,plain,(
% 0.14/5.87 ![X0,X1]: (tail(cons(X0,X1))=X1)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/5.87 fof(f19,plain,(
% 0.14/5.87 ![X0]: (~z=s(X0))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/5.87 fof(f20,plain,(
% 0.14/5.87 ![X0]: (leqNat(z,X0))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/5.87 fof(f21,plain,(
% 0.14/5.87 ![X0]: (~leqNat(s(X0),z))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/5.87 fof(f26,plain,(
% 0.14/5.87 ![X0]: (merge(nil,X0)=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/5.87 fof(f27,plain,(
% 0.14/5.87 ![X0,X1]: (merge(cons(X0,X1),nil)=cons(X0,X1))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/5.87 fof(f28,plain,(
% 0.14/5.87 ![Z,Xs,Y2,Ys]: (~leqNat(Z,Y2)|merge(cons(Z,Xs),cons(Y2,Ys))=cons(Z,merge(Xs,cons(Y2,Ys))))),
% 0.14/5.87 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.14/5.87 fof(f29,plain,(
% 0.14/5.87 ![Z,Y2]: (~leqNat(Z,Y2)|(![Xs,Ys]: merge(cons(Z,Xs),cons(Y2,Ys))=cons(Z,merge(Xs,cons(Y2,Ys)))))),
% 0.14/5.87 inference(miniscoping,[status(thm)],[f28])).
% 0.14/5.87 fof(f30,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (~leqNat(X0,X1)|merge(cons(X0,X2),cons(X1,X3))=cons(X0,merge(X2,cons(X1,X3))))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/5.87 fof(f31,plain,(
% 0.14/5.87 ![Z,Xs,Y2,Ys]: (leqNat(Z,Y2)|merge(cons(Z,Xs),cons(Y2,Ys))=cons(Y2,merge(cons(Z,Xs),Ys)))),
% 0.14/5.87 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/5.87 fof(f32,plain,(
% 0.14/5.87 ![Z,Y2]: (leqNat(Z,Y2)|(![Xs,Ys]: merge(cons(Z,Xs),cons(Y2,Ys))=cons(Y2,merge(cons(Z,Xs),Ys))))),
% 0.14/5.87 inference(miniscoping,[status(thm)],[f31])).
% 0.14/5.87 fof(f33,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (leqNat(X0,X1)|merge(cons(X0,X2),cons(X1,X3))=cons(X1,merge(cons(X0,X2),X3)))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f32])).
% 0.14/5.87 fof(f34,plain,(
% 0.14/5.87 (![Xs,Ys,Zs]: (~merge(Xs,Ys)=merge(Ys,Xs)|(~merge(Xs,Zs)=merge(Zs,Xs)|merge(Ys,Zs)=merge(Zs,Ys))))),
% 0.14/5.87 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.14/5.87 fof(f35,plain,(
% 0.14/5.87 ![Xs,Ys]: (~merge(Xs,Ys)=merge(Ys,Xs)|(![Zs]: (~merge(Xs,Zs)=merge(Zs,Xs)|merge(Ys,Zs)=merge(Zs,Ys))))),
% 0.14/5.87 inference(miniscoping,[status(thm)],[f34])).
% 0.14/5.87 fof(f36,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(X0,X1)=merge(X1,X0)|~merge(X0,X2)=merge(X2,X0)|merge(X1,X2)=merge(X2,X1))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.14/5.87 fof(f89,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(nil,X0)=merge(X0,nil)|~merge(nil,cons(X1,X2))=cons(X1,X2)|merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f27,f36])).
% 0.14/5.87 fof(f90,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(cons(X0,X1),X2)=merge(X2,cons(X0,X1))|~cons(X0,X1)=merge(nil,cons(X0,X1))|merge(X2,nil)=merge(nil,X2))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f27,f36])).
% 0.14/5.87 fof(f91,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~X0=merge(X0,nil)|~merge(nil,cons(X1,X2))=cons(X1,X2)|merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f26,f89])).
% 0.14/5.87 fof(f92,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~X0=merge(X0,nil)|~cons(X1,X2)=cons(X1,X2)|merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f26,f91])).
% 0.14/5.87 fof(f93,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~X0=merge(X0,nil)|merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(trivial_equality_resolution,[status(thm)],[f92])).
% 0.14/5.87 fof(f94,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(cons(X0,X1),X2)=merge(X2,cons(X0,X1))|~cons(X0,X1)=cons(X0,X1)|merge(X2,nil)=merge(nil,X2))),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f26,f90])).
% 0.14/5.87 fof(f95,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(cons(X0,X1),X2)=merge(X2,cons(X0,X1))|~cons(X0,X1)=cons(X0,X1)|merge(X2,nil)=X2)),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f26,f94])).
% 0.14/5.87 fof(f96,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~merge(cons(X0,X1),X2)=merge(X2,cons(X0,X1))|merge(X2,nil)=X2)),
% 0.14/5.87 inference(trivial_equality_resolution,[status(thm)],[f95])).
% 0.14/5.87 fof(f132,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (~X0=merge(X0,nil)|~merge(X0,X1)=merge(X1,X0)|merge(X1,cons(X2,X3))=merge(cons(X2,X3),X1))),
% 0.14/5.87 inference(resolution,[status(thm)],[f93,f36])).
% 0.14/5.87 fof(f149,plain,(
% 0.14/5.87 ![X0,X1,X2]: (merge(cons(z,X0),cons(X1,X2))=cons(z,merge(X0,cons(X1,X2))))),
% 0.14/5.87 inference(resolution,[status(thm)],[f30,f20])).
% 0.14/5.87 fof(f151,plain,(
% 0.14/5.87 ![X0,X1,X2]: (merge(cons(s(X0),X1),cons(z,X2))=cons(z,merge(cons(s(X0),X1),X2)))),
% 0.14/5.87 inference(resolution,[status(thm)],[f33,f21])).
% 0.14/5.87 fof(f152,plain,(
% 0.14/5.87 ![X0,X1,X2,X3,X4,X5]: (merge(cons(X0,X1),cons(X2,X3))=cons(X2,merge(cons(X0,X1),X3))|merge(cons(X0,X4),cons(X2,X5))=cons(X0,merge(X4,cons(X2,X5))))),
% 0.14/5.87 inference(resolution,[status(thm)],[f33,f30])).
% 0.14/5.87 fof(f177,plain,(
% 0.14/5.87 ![X0,X1,X2,X3,X4]: (~merge(cons(X0,X1),X2)=merge(X2,cons(X0,X1))|merge(X2,cons(X3,X4))=merge(cons(X3,X4),X2))),
% 0.14/5.87 inference(resolution,[status(thm)],[f132,f27])).
% 0.14/5.87 fof(f218,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (merge(cons(X0,X1),cons(X2,X3))=merge(cons(X2,X3),cons(X0,X1)))),
% 0.14/5.87 inference(equality_resolution,[status(thm)],[f177])).
% 0.14/5.87 fof(f318,plain,(
% 0.14/5.87 ![X0,X1,X2]: (tail(merge(cons(z,X0),cons(X1,X2)))=merge(X0,cons(X1,X2)))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f149,f16])).
% 0.14/5.87 fof(f320,plain,(
% 0.14/5.87 ![X0,X1,X2]: (head(merge(cons(z,X0),cons(X1,X2)))=z)),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f149,f15])).
% 0.14/5.87 fof(f347,plain,(
% 0.14/5.87 ![X0,X1,X2,X3,X4]: (head(merge(merge(cons(z,X0),cons(X1,X2)),cons(X3,X4)))=z)),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f149,f320])).
% 0.14/5.87 fof(f397,plain,(
% 0.14/5.87 ![X0,X1,X2]: (tail(merge(cons(s(X0),X1),cons(z,X2)))=merge(cons(s(X0),X1),X2))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f151,f16])).
% 0.14/5.87 fof(f580,plain,(
% 0.14/5.87 ![X0,X1,X2]: (tail(merge(cons(X0,X1),cons(z,X2)))=merge(X2,cons(X0,X1)))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f218,f318])).
% 0.14/5.87 fof(f1915,plain,(
% 0.14/5.87 ![X0,X1,X2,X3,X4]: (head(merge(merge(cons(X0,X1),cons(z,X2)),cons(X3,X4)))=z)),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f218,f347])).
% 0.14/5.87 fof(f3326,plain,(
% 0.14/5.87 ![X0,X1,X2]: (merge(X0,cons(s(X1),X2))=merge(cons(s(X1),X2),X0))),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f580,f397])).
% 0.14/5.87 fof(f3336,plain,(
% 0.14/5.87 ![X0]: (merge(X0,nil)=X0)),
% 0.14/5.87 inference(resolution,[status(thm)],[f3326,f96])).
% 0.14/5.87 fof(f3338,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (~merge(cons(s(X0),X1),X2)=merge(X2,cons(s(X0),X1))|merge(X2,X3)=merge(X3,X2))),
% 0.14/5.87 inference(resolution,[status(thm)],[f3326,f36])).
% 0.14/5.87 fof(f3498,plain,(
% 0.14/5.87 ![X0,X1]: (merge(X0,X1)=merge(X1,X0))),
% 0.14/5.87 inference(forward_subsumption_resolution,[status(thm)],[f3338,f3326])).
% 0.14/5.87 fof(f3608,plain,(
% 0.14/5.87 ![X0,X1,X2]: (~X0=X0|merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(backward_demodulation,[status(thm)],[f3336,f93])).
% 0.14/5.87 fof(f3635,plain,(
% 0.14/5.87 ![X0,X1,X2]: (merge(X0,cons(X1,X2))=merge(cons(X1,X2),X0))),
% 0.14/5.87 inference(trivial_equality_resolution,[status(thm)],[f3608])).
% 0.14/5.87 fof(f3741,plain,(
% 0.14/5.87 ![X0,X1,X2,X3,X4,X5]: (merge(cons(X0,X1),cons(X2,X3))=cons(X2,merge(X3,cons(X0,X1)))|merge(cons(X0,X4),cons(X2,X5))=cons(X0,merge(X4,cons(X2,X5))))),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f3635,f152])).
% 0.14/5.89 fof(f7358,plain,(
% 0.14/5.89 ![X0,X1,X2]: (~merge(cons(X0,X1),cons(X0,X2))=merge(cons(X0,X2),cons(X0,X1))|cons(X0,merge(X2,cons(X0,X1)))=merge(cons(X0,X2),cons(X0,X1)))),
% 0.14/5.89 inference(equality_factoring,[status(thm)],[f3741])).
% 0.14/5.89 fof(f7418,plain,(
% 0.14/5.89 ![X0,X1,X2]: (cons(X0,merge(X1,cons(X0,X2)))=merge(cons(X0,X1),cons(X0,X2)))),
% 0.14/5.89 inference(forward_subsumption_resolution,[status(thm)],[f7358,f3498])).
% 0.14/5.89 fof(f7436,plain,(
% 0.14/5.89 ![X0,X1]: (cons(X0,cons(X0,X1))=merge(cons(X0,nil),cons(X0,X1)))),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f26,f7418])).
% 0.14/5.89 fof(f7554,plain,(
% 0.14/5.89 ![X0,X1,X2]: (tail(merge(cons(X0,X1),cons(X0,X2)))=merge(X1,cons(X0,X2)))),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f7418,f16])).
% 0.14/5.89 fof(f8061,plain,(
% 0.14/5.89 ![X0,X1]: (cons(X0,cons(X0,X1))=merge(cons(X0,X1),cons(X0,nil)))),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f3498,f7436])).
% 0.14/5.89 fof(f8712,plain,(
% 0.14/5.89 ![X0,X1]: (tail(cons(X0,cons(X0,X1)))=merge(X1,cons(X0,nil)))),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f8061,f7554])).
% 0.14/5.89 fof(f8760,plain,(
% 0.14/5.89 ![X0,X1]: (cons(X0,X1)=merge(X1,cons(X0,nil)))),
% 0.14/5.89 inference(forward_demodulation,[status(thm)],[f16,f8712])).
% 0.14/5.89 fof(f8802,plain,(
% 0.14/5.89 ![X0,X1,X2,X3]: (head(cons(X0,merge(cons(X1,X2),cons(z,X3))))=z)),
% 0.14/5.89 inference(paramodulation,[status(thm)],[f8760,f1915])).
% 0.14/5.89 fof(f8861,plain,(
% 0.14/5.89 ![X0]: (X0=z)),
% 0.14/5.89 inference(forward_demodulation,[status(thm)],[f15,f8802])).
% 0.14/5.89 fof(f8884,plain,(
% 0.14/5.89 $false),
% 0.14/5.89 inference(backward_subsumption_resolution,[status(thm)],[f19,f8861])).
% 0.14/5.89 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.91 % Elapsed time: 0.528372 seconds
% 0.14/5.91 % CPU time: 4.019649 seconds
% 0.14/5.91 % Total memory used: 154.584 MB
% 0.14/5.91 % Net memory used: 152.798 MB
%------------------------------------------------------------------------------