%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM012+1 : 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 : n014.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 12:10:42 PM UTC 2026
% Result : Theorem 0.10s 5.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM012+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.36 % Computer : n014.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 14:14:25 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.37 % Drodi V4.1.1
% 0.10/5.40 % Refutation found
% 0.10/5.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/5.40 % SZS output start CNFRefutation for theBenchmark
% 0.10/5.40 fof(f7,axiom,(
% 0.10/5.40 (! [W0,W1,W2,W3] :( ( aElement0(W0)& aRewritingSystem0(W1)& aElement0(W2)& aElement0(W3) )=> ( ( sdtmndtplgtdt0(W0,W1,W2)& sdtmndtplgtdt0(W2,W1,W3) )=> sdtmndtplgtdt0(W0,W1,W3) ) ) )),
% 0.10/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/5.40 fof(f8,definition,(
% 0.10/5.40 (! [W0,W1,W2] :( ( aElement0(W0)& aRewritingSystem0(W1)& aElement0(W2) )=> ( sdtmndtasgtdt0(W0,W1,W2)<=> ( W0 = W2| sdtmndtplgtdt0(W0,W1,W2) ) ) ) )),
% 0.10/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/5.40 fof(f9,hypothesis,(
% 0.10/5.40 ( aElement0(xx)& aRewritingSystem0(xR)& aElement0(xy)& aElement0(xz) ) ),
% 0.10/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/5.40 fof(f10,conjecture,(
% 0.10/5.40 ( ( sdtmndtasgtdt0(xx,xR,xy)& sdtmndtasgtdt0(xy,xR,xz) )=> sdtmndtasgtdt0(xx,xR,xz) ) ),
% 0.10/5.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/5.40 fof(f11,negated_conjecture,(
% 0.10/5.40 ~(( ( sdtmndtasgtdt0(xx,xR,xy)& sdtmndtasgtdt0(xy,xR,xz) )=> sdtmndtasgtdt0(xx,xR,xz) ) )),
% 0.10/5.40 inference(negated_conjecture,[status(cth)],[f10])).
% 0.10/5.40 fof(f32,plain,(
% 0.10/5.40 ![W0,W1,W2,W3]: ((((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|~aElement0(W3))|((~sdtmndtplgtdt0(W0,W1,W2)|~sdtmndtplgtdt0(W2,W1,W3))|sdtmndtplgtdt0(W0,W1,W3)))),
% 0.10/5.40 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.10/5.40 fof(f33,plain,(
% 0.10/5.40 ![X0,X1,X2,X3]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|~aElement0(X3)|~sdtmndtplgtdt0(X0,X1,X2)|~sdtmndtplgtdt0(X2,X1,X3)|sdtmndtplgtdt0(X0,X1,X3))),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f32])).
% 0.10/5.40 fof(f34,plain,(
% 0.10/5.40 ![W0,W1,W2]: (((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|(sdtmndtasgtdt0(W0,W1,W2)<=>(W0=W2|sdtmndtplgtdt0(W0,W1,W2))))),
% 0.10/5.40 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.10/5.40 fof(f35,plain,(
% 0.10/5.40 ![W0,W1,W2]: (((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|((~sdtmndtasgtdt0(W0,W1,W2)|(W0=W2|sdtmndtplgtdt0(W0,W1,W2)))&(sdtmndtasgtdt0(W0,W1,W2)|(~W0=W2&~sdtmndtplgtdt0(W0,W1,W2)))))),
% 0.10/5.40 inference(NNF_transformation,[status(thm)],[f34])).
% 0.10/5.40 fof(f36,plain,(
% 0.10/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|~sdtmndtasgtdt0(X0,X1,X2)|X0=X2|sdtmndtplgtdt0(X0,X1,X2))),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/5.40 fof(f38,plain,(
% 0.10/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|sdtmndtasgtdt0(X0,X1,X2)|~sdtmndtplgtdt0(X0,X1,X2))),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/5.40 fof(f39,plain,(
% 0.10/5.40 aElement0(xx)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/5.40 fof(f40,plain,(
% 0.10/5.40 aRewritingSystem0(xR)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/5.40 fof(f41,plain,(
% 0.10/5.40 aElement0(xy)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/5.40 fof(f42,plain,(
% 0.10/5.40 aElement0(xz)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/5.40 fof(f43,plain,(
% 0.10/5.40 ((sdtmndtasgtdt0(xx,xR,xy)&sdtmndtasgtdt0(xy,xR,xz))&~sdtmndtasgtdt0(xx,xR,xz))),
% 0.10/5.40 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.10/5.40 fof(f44,plain,(
% 0.10/5.40 sdtmndtasgtdt0(xx,xR,xy)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/5.40 fof(f45,plain,(
% 0.10/5.40 sdtmndtasgtdt0(xy,xR,xz)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/5.40 fof(f46,plain,(
% 0.10/5.40 ~sdtmndtasgtdt0(xx,xR,xz)),
% 0.10/5.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/5.40 fof(f51,plain,(
% 0.10/5.40 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~sdtmndtasgtdt0(X0,xR,X1)|X0=X1|sdtmndtplgtdt0(X0,xR,X1))),
% 0.10/5.40 inference(resolution,[status(thm)],[f40,f36])).
% 0.10/5.40 fof(f54,plain,(
% 0.10/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtmndtplgtdt0(X0,xR,X1)|~sdtmndtplgtdt0(X1,xR,X2)|sdtmndtplgtdt0(X0,xR,X2))),
% 0.10/5.40 inference(resolution,[status(thm)],[f33,f40])).
% 0.10/5.40 fof(f58,plain,(
% 0.10/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtmndtplgtdt0(X0,xR,X1)|~sdtmndtplgtdt0(X1,xR,X2)|~aElement0(X0)|~aRewritingSystem0(xR)|~aElement0(X2)|sdtmndtasgtdt0(X0,xR,X2))),
% 0.10/5.40 inference(resolution,[status(thm)],[f54,f38])).
% 0.10/5.40 fof(f62,plain,(
% 0.10/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtmndtplgtdt0(X0,xR,X1)|~sdtmndtplgtdt0(X1,xR,X2)|~aRewritingSystem0(xR)|sdtmndtasgtdt0(X0,xR,X2))),
% 0.14/5.40 inference(duplicate_literals_removal,[status(thm)],[f58])).
% 0.14/5.40 fof(f63,plain,(
% 0.14/5.40 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtmndtplgtdt0(X0,xR,X1)|~sdtmndtplgtdt0(X1,xR,X2)|sdtmndtasgtdt0(X0,xR,X2))),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f62,f40])).
% 0.14/5.40 fof(f64,plain,(
% 0.14/5.40 ![X0]: (~aElement0(xx)|~aElement0(X0)|~aElement0(xz)|~sdtmndtplgtdt0(xx,xR,X0)|~sdtmndtplgtdt0(X0,xR,xz))),
% 0.14/5.40 inference(resolution,[status(thm)],[f63,f46])).
% 0.14/5.40 fof(f65,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~aElement0(xz)|~sdtmndtplgtdt0(xx,xR,X0)|~sdtmndtplgtdt0(X0,xR,xz))),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f64,f39])).
% 0.14/5.40 fof(f66,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtplgtdt0(xx,xR,X0)|~sdtmndtplgtdt0(X0,xR,xz))),
% 0.14/5.40 inference(resolution,[status(thm)],[f65,f42])).
% 0.14/5.40 fof(f68,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtplgtdt0(X0,xR,xz)|~aElement0(xx)|~aElement0(X0)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0)),
% 0.14/5.40 inference(resolution,[status(thm)],[f66,f51])).
% 0.14/5.40 fof(f71,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtplgtdt0(X0,xR,xz)|~aElement0(xx)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0)),
% 0.14/5.40 inference(duplicate_literals_removal,[status(thm)],[f68])).
% 0.14/5.40 fof(f72,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtplgtdt0(X0,xR,xz)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0)),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f71,f39])).
% 0.14/5.40 fof(f74,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0|~aElement0(X0)|~aElement0(xz)|~sdtmndtasgtdt0(X0,xR,xz)|X0=xz)),
% 0.14/5.40 inference(resolution,[status(thm)],[f72,f51])).
% 0.14/5.40 fof(f77,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0|~aElement0(xz)|~sdtmndtasgtdt0(X0,xR,xz)|X0=xz)),
% 0.14/5.40 inference(duplicate_literals_removal,[status(thm)],[f74])).
% 0.14/5.40 fof(f78,plain,(
% 0.14/5.40 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(xx,xR,X0)|xx=X0|~sdtmndtasgtdt0(X0,xR,xz)|X0=xz)),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f77,f42])).
% 0.14/5.40 fof(f79,plain,(
% 0.14/5.40 ~aElement0(xy)|xx=xy|~sdtmndtasgtdt0(xy,xR,xz)|xy=xz),
% 0.14/5.40 inference(resolution,[status(thm)],[f78,f44])).
% 0.14/5.40 fof(f82,plain,(
% 0.14/5.40 xx=xy|~sdtmndtasgtdt0(xy,xR,xz)|xy=xz),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f79,f41])).
% 0.14/5.40 fof(f85,plain,(
% 0.14/5.40 xx=xy|xy=xz),
% 0.14/5.40 inference(resolution,[status(thm)],[f82,f45])).
% 0.14/5.40 fof(f90,plain,(
% 0.14/5.40 ~sdtmndtasgtdt0(xy,xR,xz)|xy=xz),
% 0.14/5.40 inference(paramodulation,[status(thm)],[f85,f46])).
% 0.14/5.40 fof(f95,plain,(
% 0.14/5.40 sdtmndtasgtdt0(xx,xR,xz)),
% 0.14/5.40 inference(backward_demodulation,[status(thm)],[f98,f44])).
% 0.14/5.40 fof(f98,plain,(
% 0.14/5.40 xy=xz),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f90,f45])).
% 0.14/5.40 fof(f101,plain,(
% 0.14/5.40 $false),
% 0.14/5.40 inference(forward_subsumption_resolution,[status(thm)],[f95,f46])).
% 0.14/5.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.42 % Elapsed time: 0.053698 seconds
% 0.14/5.42 % CPU time: 0.152910 seconds
% 0.14/5.42 % Total memory used: 80.528 MB
% 0.14/5.42 % Net memory used: 80.160 MB
%------------------------------------------------------------------------------