%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LDA002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 01:24:41 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LDA002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 01:19:22 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.13/0.44 % Refutation found
% 0.13/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.44 fof(f1,axiom,(
% 0.13/0.44 (![X,Y,Z]: (f(X,f(Y,Z)) = f(f(X,Y),f(X,Z)) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f2,axiom,(
% 0.13/0.44 n2 = f(n1,n1) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f3,axiom,(
% 0.13/0.44 n3 = f(n2,n1) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f4,axiom,(
% 0.13/0.44 u = f(n2,n2) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f5,axiom,(
% 0.13/0.44 u1 = f(u,n1) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f6,axiom,(
% 0.13/0.44 u2 = f(u,n2) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f7,axiom,(
% 0.13/0.44 u3 = f(u,n3) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f8,axiom,(
% 0.13/0.44 uu = f(u,u) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f9,axiom,(
% 0.13/0.44 a = f(f(n3,n2),u2) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f10,axiom,(
% 0.13/0.44 b = f(u1,u3) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f11,axiom,(
% 0.13/0.44 v = f(uu,uu) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f12,negated_conjecture,(
% 0.13/0.44 f(a,v) != f(b,v) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f13,plain,(
% 0.13/0.44 ![X0,X1,X2]: (f(X0,f(X1,X2))=f(f(X0,X1),f(X0,X2)))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.44 fof(f14,plain,(
% 0.13/0.44 n2=f(n1,n1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f15,plain,(
% 0.13/0.44 n3=f(n2,n1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.44 fof(f16,plain,(
% 0.13/0.44 u=f(n2,n2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.44 fof(f17,plain,(
% 0.13/0.44 u1=f(u,n1)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.44 fof(f18,plain,(
% 0.13/0.44 u2=f(u,n2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.44 fof(f19,plain,(
% 0.13/0.44 u3=f(u,n3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.44 fof(f20,plain,(
% 0.13/0.44 uu=f(u,u)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.44 fof(f21,plain,(
% 0.13/0.44 a=f(f(n3,n2),u2)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.44 fof(f22,plain,(
% 0.13/0.44 b=f(u1,u3)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.44 fof(f23,plain,(
% 0.13/0.44 v=f(uu,uu)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.44 fof(f24,plain,(
% 0.13/0.44 ~f(a,v)=f(b,v)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.44 fof(f29,plain,(
% 0.13/0.44 ![X0]: (f(n1,f(n1,X0))=f(n2,f(n1,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f14,f13])).
% 0.13/0.44 fof(f32,plain,(
% 0.13/0.44 ![X0]: (f(n2,f(X0,n1))=f(f(n2,X0),n3))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f15,f13])).
% 0.13/0.44 fof(f33,plain,(
% 0.13/0.44 ![X0]: (f(n2,f(n1,X0))=f(n3,f(n2,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f15,f13])).
% 0.13/0.44 fof(f34,plain,(
% 0.13/0.44 ![X0]: (f(n2,f(X0,n2))=f(f(n2,X0),u))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f16,f13])).
% 0.13/0.44 fof(f35,plain,(
% 0.13/0.44 ![X0]: (f(n2,f(n2,X0))=f(u,f(n2,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f16,f13])).
% 0.13/0.44 fof(f37,plain,(
% 0.13/0.44 ![X0]: (f(u,f(n1,X0))=f(u1,f(u,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f17,f13])).
% 0.13/0.44 fof(f43,plain,(
% 0.13/0.44 ![X0]: (f(u,f(X0,u))=f(f(u,X0),uu))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f20,f13])).
% 0.13/0.44 fof(f46,plain,(
% 0.13/0.44 ![X0]: (f(u1,f(u3,X0))=f(b,f(u1,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f22,f13])).
% 0.13/0.44 fof(f48,plain,(
% 0.13/0.44 ![X0]: (f(f(n3,n2),f(u2,X0))=f(a,f(f(n3,n2),X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f21,f13])).
% 0.13/0.44 fof(f52,plain,(
% 0.13/0.44 f(n1,n2)=f(n2,f(n1,n1))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f14,f29])).
% 0.13/0.44 fof(f56,plain,(
% 0.13/0.44 f(n1,n2)=f(n2,n2)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f14,f52])).
% 0.13/0.44 fof(f57,plain,(
% 0.13/0.44 f(n1,n2)=u),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f16,f56])).
% 0.13/0.44 fof(f117,plain,(
% 0.13/0.44 f(n1,u)=f(n2,f(n1,n2))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f57,f29])).
% 0.13/0.44 fof(f121,plain,(
% 0.13/0.44 ![X0]: (f(n1,f(n2,X0))=f(u,f(n1,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f57,f13])).
% 0.13/0.44 fof(f122,plain,(
% 0.13/0.44 f(n1,u)=f(n2,u)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f57,f117])).
% 0.13/0.44 fof(f126,plain,(
% 0.13/0.44 ![X0]: (f(n1,f(n2,X0))=f(u1,f(u,X0)))),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f121,f37])).
% 0.13/0.44 fof(f209,plain,(
% 0.13/0.44 f(n1,f(n2,u))=f(n2,f(n1,u))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f122,f29])).
% 0.13/0.44 fof(f216,plain,(
% 0.13/0.44 f(n1,f(n2,u))=f(n2,f(n2,u))),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f122,f209])).
% 0.13/0.44 fof(f258,plain,(
% 0.13/0.44 f(n2,f(n1,n1))=f(n3,n3)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f15,f32])).
% 0.13/0.44 fof(f269,plain,(
% 0.13/0.44 f(n2,n2)=f(n3,n3)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f14,f258])).
% 0.13/0.44 fof(f270,plain,(
% 0.13/0.44 u=f(n3,n3)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f16,f269])).
% 0.13/0.44 fof(f314,plain,(
% 0.13/0.44 ![X0]: (f(n3,f(n3,X0))=f(u,f(n3,X0)))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f270,f13])).
% 0.13/0.44 fof(f322,plain,(
% 0.13/0.44 f(n2,f(n2,n2))=f(u,u)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f16,f34])).
% 0.13/0.44 fof(f323,plain,(
% 0.13/0.44 f(n2,f(n1,n2))=f(n3,u)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f15,f34])).
% 0.13/0.44 fof(f332,plain,(
% 0.13/0.44 f(n2,u)=f(u,u)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f16,f322])).
% 0.13/0.44 fof(f333,plain,(
% 0.13/0.44 f(n1,u)=uu),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f343,f122])).
% 0.13/0.44 fof(f342,plain,(
% 0.13/0.44 f(n1,f(n2,u))=f(n2,uu)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f343,f216])).
% 0.13/0.44 fof(f343,plain,(
% 0.13/0.44 f(n2,u)=uu),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f20,f332])).
% 0.13/0.44 fof(f344,plain,(
% 0.13/0.44 f(n2,u)=f(n3,u)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f57,f323])).
% 0.13/0.44 fof(f345,plain,(
% 0.13/0.44 uu=f(n3,u)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f343,f344])).
% 0.13/0.44 fof(f360,plain,(
% 0.13/0.44 f(n1,uu)=f(n2,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f343,f342])).
% 0.13/0.44 fof(f362,plain,(
% 0.13/0.44 f(n2,f(n1,u))=f(n3,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f343,f33])).
% 0.13/0.44 fof(f371,plain,(
% 0.13/0.44 f(n2,uu)=f(n3,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f333,f362])).
% 0.13/0.44 fof(f375,plain,(
% 0.13/0.44 f(n2,f(n2,u))=f(u,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f343,f35])).
% 0.13/0.44 fof(f387,plain,(
% 0.13/0.44 f(n2,uu)=f(u,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f343,f375])).
% 0.13/0.44 fof(f403,plain,(
% 0.13/0.44 ![X0]: (f(n3,f(X0,u))=f(f(n3,X0),uu))),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f345,f13])).
% 0.13/0.44 fof(f573,plain,(
% 0.13/0.44 f(u,f(u,u))=f(uu,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f20,f43])).
% 0.13/0.44 fof(f574,plain,(
% 0.13/0.44 f(u,f(n3,u))=f(u3,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f19,f43])).
% 0.13/0.44 fof(f575,plain,(
% 0.13/0.44 f(u,f(n2,u))=f(u2,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f18,f43])).
% 0.13/0.44 fof(f576,plain,(
% 0.13/0.44 f(u,f(n1,u))=f(u1,uu)),
% 0.13/0.44 inference(paramodulation,[status(thm)],[f17,f43])).
% 0.13/0.44 fof(f588,plain,(
% 0.13/0.44 f(u,uu)=f(uu,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f20,f573])).
% 0.13/0.44 fof(f589,plain,(
% 0.13/0.44 f(n2,uu)=f(uu,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f387,f588])).
% 0.13/0.44 fof(f591,plain,(
% 0.13/0.44 v=f(u,uu)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f594,f387])).
% 0.13/0.44 fof(f592,plain,(
% 0.13/0.44 v=f(n3,uu)),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f594,f371])).
% 0.13/0.44 fof(f593,plain,(
% 0.13/0.44 f(n1,uu)=v),
% 0.13/0.44 inference(backward_demodulation,[status(thm)],[f594,f360])).
% 0.13/0.44 fof(f594,plain,(
% 0.13/0.44 f(n2,uu)=v),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f23,f589])).
% 0.13/0.44 fof(f595,plain,(
% 0.13/0.44 f(n3,f(n3,u))=f(u3,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f314,f574])).
% 0.13/0.44 fof(f596,plain,(
% 0.13/0.44 f(n3,uu)=f(u3,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f345,f595])).
% 0.13/0.44 fof(f597,plain,(
% 0.13/0.44 f(n2,uu)=f(u3,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f371,f596])).
% 0.13/0.44 fof(f598,plain,(
% 0.13/0.44 v=f(u3,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f594,f597])).
% 0.13/0.44 fof(f599,plain,(
% 0.13/0.44 f(n2,f(n2,u))=f(u2,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f35,f575])).
% 0.13/0.44 fof(f600,plain,(
% 0.13/0.44 f(n2,uu)=f(u2,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f343,f599])).
% 0.13/0.44 fof(f601,plain,(
% 0.13/0.44 v=f(u2,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f594,f600])).
% 0.13/0.44 fof(f602,plain,(
% 0.13/0.44 f(n1,f(n2,u))=f(u1,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f121,f576])).
% 0.13/0.44 fof(f603,plain,(
% 0.13/0.44 f(n1,uu)=f(u1,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f343,f602])).
% 0.13/0.44 fof(f604,plain,(
% 0.13/0.44 f(n2,uu)=f(u1,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f360,f603])).
% 0.13/0.44 fof(f605,plain,(
% 0.13/0.44 v=f(u1,uu)),
% 0.13/0.44 inference(forward_demodulation,[status(thm)],[f594,f604])).
% 0.13/0.45 fof(f788,plain,(
% 0.13/0.45 f(f(n3,n2),v)=f(a,f(f(n3,n2),uu))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f601,f48])).
% 0.13/0.45 fof(f795,plain,(
% 0.13/0.45 f(f(n3,n2),v)=f(a,f(n3,f(n2,u)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f403,f788])).
% 0.13/0.45 fof(f796,plain,(
% 0.13/0.45 f(f(n3,n2),v)=f(a,f(n2,f(n1,u)))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f33,f795])).
% 0.13/0.45 fof(f797,plain,(
% 0.13/0.45 f(f(n3,n2),v)=f(a,f(n2,uu))),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f333,f796])).
% 0.13/0.45 fof(f798,plain,(
% 0.13/0.45 f(f(n3,n2),v)=f(a,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f594,f797])).
% 0.13/0.45 fof(f826,plain,(
% 0.13/0.45 f(u1,f(u3,uu))=f(b,v)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f605,f46])).
% 0.13/0.45 fof(f834,plain,(
% 0.13/0.45 ~f(a,v)=f(u1,v)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f835,f24])).
% 0.13/0.45 fof(f835,plain,(
% 0.13/0.45 f(u1,v)=f(b,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f598,f826])).
% 0.13/0.45 fof(f886,plain,(
% 0.13/0.45 ![X0]: (f(n3,f(X0,uu))=f(f(n3,X0),v))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f592,f13])).
% 0.13/0.45 fof(f890,plain,(
% 0.13/0.45 f(n3,f(n2,uu))=f(a,v)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f886,f798])).
% 0.13/0.45 fof(f891,plain,(
% 0.13/0.45 f(n2,f(n1,uu))=f(a,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f33,f890])).
% 0.13/0.45 fof(f892,plain,(
% 0.13/0.45 ~f(n2,v)=f(u1,v)),
% 0.13/0.45 inference(backward_demodulation,[status(thm)],[f893,f834])).
% 0.13/0.45 fof(f893,plain,(
% 0.13/0.45 f(n2,v)=f(a,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f593,f891])).
% 0.13/0.45 fof(f895,plain,(
% 0.13/0.45 f(n1,v)=f(n2,f(n1,uu))),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f593,f29])).
% 0.13/0.45 fof(f902,plain,(
% 0.13/0.45 f(n1,v)=f(n2,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f593,f895])).
% 0.13/0.45 fof(f905,plain,(
% 0.13/0.45 f(n1,f(n2,uu))=f(u1,v)),
% 0.13/0.45 inference(paramodulation,[status(thm)],[f591,f126])).
% 0.13/0.45 fof(f921,plain,(
% 0.13/0.45 f(n1,v)=f(u1,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f594,f905])).
% 0.13/0.45 fof(f922,plain,(
% 0.13/0.45 f(n2,v)=f(u1,v)),
% 0.13/0.45 inference(forward_demodulation,[status(thm)],[f902,f921])).
% 0.13/0.45 fof(f923,plain,(
% 0.13/0.45 $false),
% 0.13/0.45 inference(forward_subsumption_resolution,[status(thm)],[f922,f892])).
% 0.13/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.47 % Elapsed time: 0.091144 seconds
% 0.13/0.47 % CPU time: 0.606603 seconds
% 0.13/0.47 % Total memory used: 37.016 MB
% 0.13/0.47 % Net memory used: 36.845 MB
%------------------------------------------------------------------------------