%------------------------------------------------------------------------------
% 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/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:45 PM UTC 2026
% Result : Unsatisfiable 153.54s 25.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX190-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n002.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Mon Sep 21 10:33:54 UTC 2026
% 0.18/5.46 % CPUTime :
% 0.18/5.47 % Drodi V4.1.1
% 153.54/25.01 % Refutation found
% 153.54/25.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 153.54/25.01 % SZS output start CNFRefutation for theBenchmark
% 153.54/25.01 fof(f5,axiom,(
% 153.54/25.01 (![E]: (aux(x2,E,bfalse) = x(opt(x2),opt(E)) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f6,axiom,(
% 153.54/25.01 (![Y,E]: (fail2(Y,E) = aux(Y,E,eq2(Y,E)) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f15,axiom,(
% 153.54/25.01 (![Y]: (fail(Y,n(z)) = Y ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f44,axiom,(
% 153.54/25.01 (![Y]: (d(n(Y)) = n(z) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f45,axiom,(
% 153.54/25.01 (![F,G]: (d(x(F,G)) = x(d(F),d(G)) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f47,axiom,(
% 153.54/25.01 d(x2) = n(s(z)) ),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f52,axiom,(
% 153.54/25.01 (![X4,E]: (opt(x(n(s(X4)),E)) = fail(n(s(X4)),E) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f53,axiom,(
% 153.54/25.01 (![E]: (opt(x(n(z),E)) = E ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f62,axiom,(
% 153.54/25.01 (![X]: (opt(n(X)) = n(X) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f63,axiom,(
% 153.54/25.01 opt(x2) = x2 ),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f64,axiom,(
% 153.54/25.01 (![X]: (prop4(X) = eq2(opt(d(X)),opt(d(opt(X)))) ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f75,axiom,(
% 153.54/25.01 (![X,Y,Z]: (eq2(x(X,Y),n(Z)) = bfalse ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f81,axiom,(
% 153.54/25.01 (![X]: (eq2(x2,n(X)) = bfalse ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f89,axiom,(
% 153.54/25.01 (![X]: (eq3(X,X) = btrue ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f90,negated_conjecture,(
% 153.54/25.01 (![X]: (eq3(prop4(X),bfalse) != btrue ))),
% 153.54/25.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 153.54/25.01 fof(f95,plain,(
% 153.54/25.01 ![X0]: (aux(x2,X0,bfalse)=x(opt(x2),opt(X0)))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f5])).
% 153.54/25.01 fof(f96,plain,(
% 153.54/25.01 ![X0,X1]: (fail2(X0,X1)=aux(X0,X1,eq2(X0,X1)))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f6])).
% 153.54/25.01 fof(f105,plain,(
% 153.54/25.01 ![X0]: (fail(X0,n(z))=X0)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f15])).
% 153.54/25.01 fof(f134,plain,(
% 153.54/25.01 ![X0]: (d(n(X0))=n(z))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f44])).
% 153.54/25.01 fof(f135,plain,(
% 153.54/25.01 ![X0,X1]: (d(x(X0,X1))=x(d(X0),d(X1)))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f45])).
% 153.54/25.01 fof(f137,plain,(
% 153.54/25.01 d(x2)=n(s(z))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f47])).
% 153.54/25.01 fof(f142,plain,(
% 153.54/25.01 ![X0,X1]: (opt(x(n(s(X0)),X1))=fail(n(s(X0)),X1))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f52])).
% 153.54/25.01 fof(f143,plain,(
% 153.54/25.01 ![X0]: (opt(x(n(z),X0))=X0)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f53])).
% 153.54/25.01 fof(f152,plain,(
% 153.54/25.01 ![X0]: (opt(n(X0))=n(X0))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f62])).
% 153.54/25.01 fof(f153,plain,(
% 153.54/25.01 opt(x2)=x2),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f63])).
% 153.54/25.01 fof(f154,plain,(
% 153.54/25.01 ![X0]: (prop4(X0)=eq2(opt(d(X0)),opt(d(opt(X0)))))),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f64])).
% 153.54/25.01 fof(f169,plain,(
% 153.54/25.01 ![X0,X1,X2]: (eq2(x(X0,X1),n(X2))=bfalse)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f75])).
% 153.54/25.01 fof(f175,plain,(
% 153.54/25.01 ![X0]: (eq2(x2,n(X0))=bfalse)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f81])).
% 153.54/25.01 fof(f183,plain,(
% 153.54/25.01 ![X0]: (eq3(X0,X0)=btrue)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f89])).
% 153.54/25.01 fof(f184,plain,(
% 153.54/25.01 ![X0]: (~eq3(prop4(X0),bfalse)=btrue)),
% 153.54/25.01 inference(cnf_transformation,[status(thm)],[f90])).
% 153.54/25.01 fof(f217,plain,(
% 153.54/25.01 ![X0]: (aux(x2,X0,bfalse)=x(x2,opt(X0)))),
% 153.54/25.01 inference(forward_demodulation,[status(thm)],[f153,f95])).
% 153.54/25.01 fof(f219,plain,(
% 153.54/25.01 ![X0]: (aux(x2,n(X0),bfalse)=x(x2,n(X0)))),
% 153.54/25.01 inference(paramodulation,[status(thm)],[f152,f217])).
% 153.54/25.01 fof(f239,plain,(
% 153.54/25.01 ![X0]: (fail2(x2,n(X0))=aux(x2,n(X0),bfalse))),
% 153.54/25.01 inference(paramodulation,[status(thm)],[f175,f96])).
% 153.54/25.01 fof(f277,plain,(
% 153.54/25.01 ![X0,X1]: (eq2(x(X0,X1),d(x2))=bfalse)),
% 153.54/25.01 inference(paramodulation,[status(thm)],[f137,f169])).
% 153.54/25.01 fof(f738,plain,(
% 153.54/25.01 ![X0,X1]: (d(x(n(X0),X1))=x(n(z),d(X1)))),
% 153.54/25.01 inference(paramodulation,[status(thm)],[f134,f135])).
% 55.12/25.11 fof(f740,plain,(
% 55.12/25.11 ![X0,X1]: (d(x(X0,n(X1)))=x(d(X0),n(z)))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f134,f135])).
% 55.12/25.11 fof(f747,plain,(
% 55.12/25.11 ![X0,X1]: (eq2(d(x(X0,X1)),d(x2))=bfalse)),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f135,f277])).
% 55.12/25.11 fof(f870,plain,(
% 55.12/25.11 ![X0]: (opt(x(d(x2),X0))=fail(n(s(z)),X0))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f137,f142])).
% 55.12/25.11 fof(f881,plain,(
% 55.12/25.11 ![X0]: (opt(x(d(x2),X0))=fail(d(x2),X0))),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f137,f870])).
% 55.12/25.11 fof(f1297,plain,(
% 55.12/25.11 ![X0]: (prop4(x(n(z),X0))=eq2(opt(d(x(n(z),X0))),opt(d(X0))))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f143,f154])).
% 55.12/25.11 fof(f6358,plain,(
% 55.12/25.11 ![X0]: (fail2(x2,n(X0))=x(x2,n(X0)))),
% 55.12/25.11 inference(backward_demodulation,[status(thm)],[f239,f219])).
% 55.12/25.11 fof(f6448,plain,(
% 55.12/25.11 ![X0]: (eq2(d(fail2(x2,n(X0))),d(x2))=bfalse)),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f6358,f747])).
% 55.12/25.11 fof(f28744,plain,(
% 55.12/25.11 ![X0,X1]: (opt(d(x(n(X0),X1)))=d(X1))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f738,f143])).
% 55.12/25.11 fof(f29059,plain,(
% 55.12/25.11 ![X0]: (opt(d(x(x2,n(X0))))=fail(d(x2),n(z)))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f740,f881])).
% 55.12/25.11 fof(f29181,plain,(
% 55.12/25.11 ![X0]: (opt(d(fail2(x2,n(X0))))=fail(d(x2),n(z)))),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f6358,f29059])).
% 55.12/25.11 fof(f29182,plain,(
% 55.12/25.11 ![X0]: (opt(d(fail2(x2,n(X0))))=d(x2))),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f105,f29181])).
% 55.12/25.11 fof(f56784,plain,(
% 55.12/25.11 ![X0]: (prop4(x(n(z),X0))=eq2(d(X0),opt(d(X0))))),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f28744,f1297])).
% 55.12/25.11 fof(f56799,plain,(
% 55.12/25.11 ![X0]: (prop4(x(n(z),fail2(x2,n(X0))))=eq2(d(fail2(x2,n(X0))),d(x2)))),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f29182,f56784])).
% 55.12/25.11 fof(f56843,plain,(
% 55.12/25.11 ![X0]: (prop4(x(n(z),fail2(x2,n(X0))))=bfalse)),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f6448,f56799])).
% 55.12/25.11 fof(f78954,plain,(
% 55.12/25.11 ~eq3(bfalse,bfalse)=btrue),
% 55.12/25.11 inference(paramodulation,[status(thm)],[f56843,f184])).
% 55.12/25.11 fof(f78987,plain,(
% 55.12/25.11 ~btrue=btrue),
% 55.12/25.11 inference(forward_demodulation,[status(thm)],[f183,f78954])).
% 55.12/25.11 fof(f78988,plain,(
% 55.12/25.12 $false),
% 55.12/25.12 inference(trivial_equality_resolution,[status(thm)],[f78987])).
% 55.12/25.12 % SZS output end CNFRefutation for theBenchmark.p
% 30.29/25.25 % Elapsed time: 19.776802 seconds
% 30.29/25.25 % CPU time: 155.344089 seconds
% 30.29/25.25 % Total memory used: 1.034 GB
% 30.29/25.25 % Net memory used: 1.009 GB
%------------------------------------------------------------------------------