%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX190+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:45 PM UTC 2026
% Result : Theorem 0.14s 5.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX190+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.79 % Computer : n016.cluster.edu
% 0.11/5.79 % Model : x86_64 x86_64
% 0.11/5.79 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.79 % Memory : 8046.5625MB
% 0.11/5.79 % OS : Linux 6.8.0-71-generic
% 0.11/5.79 % CPULimit : 300
% 0.11/5.79 % WCLimit : 300
% 0.11/5.79 % DateTime : Mon Sep 21 10:36:00 UTC 2026
% 0.11/5.79 % CPUTime :
% 0.14/5.80 % Drodi V4.1.1
% 0.14/5.83 % Refutation found
% 0.14/5.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.83 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.83 fof(f8,axiom,(
% 0.14/5.83 (! [X,X2,X3] : n(X) != x(X2,X3) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f39,axiom,(
% 0.14/5.83 (! [Y] : d(n(Y)) = n(z) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f40,axiom,(
% 0.14/5.83 (! [F,G] : d(x(F,G)) = x(d(F),d(G)) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f41,axiom,(
% 0.14/5.83 (! [H,G2] : d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2))) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f50,axiom,(
% 0.14/5.83 (! [E] : opt(x(n(z),E)) = E )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f53,axiom,(
% 0.14/5.83 (! [E2] : opt(y(n(z),E2)) = n(z) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f54,conjecture,(
% 0.14/5.83 (? [E] : opt(d(E)) != opt(d(opt(E))) )),
% 0.14/5.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.83 fof(f55,negated_conjecture,(
% 0.14/5.83 ~((? [E] : opt(d(E)) != opt(d(opt(E))) ))),
% 0.14/5.83 inference(negated_conjecture,[status(cth)],[f54])).
% 0.14/5.83 fof(f63,plain,(
% 0.14/5.83 ![X0,X1,X2]: (~n(X0)=x(X1,X2))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/5.83 fof(f113,plain,(
% 0.14/5.83 ![X0]: (d(n(X0))=n(z))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f39])).
% 0.14/5.83 fof(f114,plain,(
% 0.14/5.83 ![X0,X1]: (d(x(X0,X1))=x(d(X0),d(X1)))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f40])).
% 0.14/5.83 fof(f115,plain,(
% 0.14/5.83 ![X0,X1]: (d(y(X0,X1))=x(y(d(X0),X1),y(X0,d(X1))))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/5.83 fof(f127,plain,(
% 0.14/5.83 ![X0]: (opt(x(n(z),X0))=X0)),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.83 fof(f132,plain,(
% 0.14/5.83 ![X0]: (opt(y(n(z),X0))=n(z))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/5.83 fof(f133,plain,(
% 0.14/5.83 (![E]: opt(d(E))=opt(d(opt(E))))),
% 0.14/5.83 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.14/5.83 fof(f134,plain,(
% 0.14/5.83 ![X0]: (opt(d(X0))=opt(d(opt(X0))))),
% 0.14/5.83 inference(cnf_transformation,[status(thm)],[f133])).
% 0.14/5.83 fof(f156,plain,(
% 0.14/5.83 ![X0]: (opt(d(x(n(z),X0)))=opt(d(X0)))),
% 0.14/5.83 inference(paramodulation,[status(thm)],[f127,f134])).
% 0.14/5.83 fof(f157,plain,(
% 0.14/5.83 ![X0,X1]: (d(x(n(X0),X1))=x(n(z),d(X1)))),
% 0.14/5.83 inference(paramodulation,[status(thm)],[f113,f114])).
% 0.14/5.83 fof(f181,plain,(
% 0.14/5.83 ![X0,X1,X2]: (~n(X0)=d(y(X1,X2)))),
% 0.14/5.83 inference(paramodulation,[status(thm)],[f115,f63])).
% 0.14/5.83 fof(f224,plain,(
% 0.14/5.83 ![X0]: (opt(x(n(z),d(X0)))=opt(d(X0)))),
% 0.14/5.83 inference(backward_demodulation,[status(thm)],[f157,f156])).
% 0.14/5.83 fof(f230,plain,(
% 0.14/5.83 ![X0]: (d(X0)=opt(d(X0)))),
% 0.14/5.83 inference(forward_demodulation,[status(thm)],[f127,f224])).
% 0.14/5.83 fof(f330,plain,(
% 0.14/5.83 ![X0]: (opt(d(X0))=d(opt(X0)))),
% 0.14/5.83 inference(backward_demodulation,[status(thm)],[f230,f134])).
% 0.14/5.83 fof(f338,plain,(
% 0.14/5.83 ![X0]: (d(X0)=d(opt(X0)))),
% 0.14/5.83 inference(forward_demodulation,[status(thm)],[f230,f330])).
% 0.14/5.83 fof(f343,plain,(
% 0.14/5.83 ![X0]: (d(y(n(z),X0))=d(n(z)))),
% 0.14/5.83 inference(paramodulation,[status(thm)],[f132,f338])).
% 0.14/5.83 fof(f354,plain,(
% 0.14/5.83 ![X0]: (d(y(n(z),X0))=n(z))),
% 0.14/5.83 inference(forward_demodulation,[status(thm)],[f113,f343])).
% 0.14/5.83 fof(f355,plain,(
% 0.14/5.83 $false),
% 0.14/5.83 inference(forward_subsumption_resolution,[status(thm)],[f354,f181])).
% 0.14/5.83 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.85 % Elapsed time: 0.059267 seconds
% 0.14/5.85 % CPU time: 0.159359 seconds
% 0.14/5.85 % Total memory used: 103.214 MB
% 0.14/5.85 % Net memory used: 103.166 MB
%------------------------------------------------------------------------------