%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP683-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:37:10 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP683-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:32:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 0.12/0.49 % Refutation found
% 0.12/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.49 fof(f1,axiom,(
% 0.12/0.49 (![A]: (ld(A,mult(A,A)) = A ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f2,axiom,(
% 0.12/0.49 (![A]: (rd(mult(A,A),A) = A ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f3,axiom,(
% 0.12/0.49 (![A,B]: (mult(A,ld(A,B)) = ld(A,mult(A,B)) ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f4,axiom,(
% 0.12/0.49 (![A,B]: (mult(rd(A,B),B) = rd(mult(A,B),B) ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f5,axiom,(
% 0.12/0.49 (![A,B,C,D]: (ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D) ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f7,axiom,(
% 0.12/0.49 (![A,B]: (ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B) ))),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f8,negated_conjecture,(
% 0.12/0.49 mult(x3,ld(x4,mult(x4,x5))) != mult(x3,x5) ),
% 0.12/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.49 fof(f9,plain,(
% 0.12/0.49 ![X0]: (ld(X0,mult(X0,X0))=X0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.12/0.49 fof(f10,plain,(
% 0.12/0.49 ![X0]: (rd(mult(X0,X0),X0)=X0)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f2])).
% 0.12/0.49 fof(f11,plain,(
% 0.12/0.49 ![X0,X1]: (mult(X0,ld(X0,X1))=ld(X0,mult(X0,X1)))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.12/0.49 fof(f12,plain,(
% 0.12/0.49 ![X0,X1]: (mult(rd(X0,X1),X1)=rd(mult(X0,X1),X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.12/0.49 fof(f13,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (ld(ld(X0,X1),mult(ld(X0,X1),mult(X2,X3)))=mult(ld(X0,mult(X0,X2)),X3))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f5])).
% 0.12/0.49 fof(f15,plain,(
% 0.12/0.49 ![X0,X1]: (ld(X0,mult(X0,ld(X1,X1)))=rd(mult(rd(X0,X0),X1),X1))),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.49 fof(f16,plain,(
% 0.12/0.49 ~mult(x3,ld(x4,mult(x4,x5)))=mult(x3,x5)),
% 0.12/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.49 fof(f22,plain,(
% 0.12/0.49 ![X0]: (mult(X0,ld(X0,X0))=X0)),
% 0.12/0.49 inference(backward_demodulation,[status(thm)],[f11,f9])).
% 0.12/0.49 fof(f23,plain,(
% 0.12/0.49 ![X0]: (mult(rd(X0,X0),X0)=X0)),
% 0.12/0.49 inference(backward_demodulation,[status(thm)],[f12,f10])).
% 0.12/0.49 fof(f24,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3)))=mult(ld(X0,mult(X0,X2)),X3))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f11,f13])).
% 0.12/0.49 fof(f25,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(ld(X0,X1),ld(ld(X0,X1),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f11,f24])).
% 0.12/0.49 fof(f28,plain,(
% 0.12/0.49 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=rd(mult(rd(X0,X0),X1),X1))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f11,f15])).
% 0.12/0.49 fof(f29,plain,(
% 0.12/0.49 ![X0,X1]: (mult(X0,ld(X0,ld(X1,X1)))=mult(rd(rd(X0,X0),X1),X1))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f12,f28])).
% 0.12/0.49 fof(f30,plain,(
% 0.12/0.49 ~mult(x3,mult(x4,ld(x4,x5)))=mult(x3,x5)),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f11,f16])).
% 0.12/0.49 fof(f32,plain,(
% 0.12/0.49 ![X0]: (mult(X0,ld(X0,ld(X0,X0)))=ld(X0,X0))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f22,f11])).
% 0.12/0.49 fof(f33,plain,(
% 0.12/0.49 ![X0]: (mult(rd(rd(X0,X0),X0),X0)=rd(X0,X0))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f23,f12])).
% 0.12/0.49 fof(f35,plain,(
% 0.12/0.49 ![X0]: (mult(X0,ld(X0,ld(X0,X0)))=rd(X0,X0))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f29,f33])).
% 0.12/0.49 fof(f36,plain,(
% 0.12/0.49 ![X0]: (mult(ld(X0,X0),X0)=X0)),
% 0.12/0.49 inference(backward_demodulation,[status(thm)],[f39,f23])).
% 0.12/0.49 fof(f39,plain,(
% 0.12/0.49 ![X0]: (ld(X0,X0)=rd(X0,X0))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f32,f35])).
% 0.12/0.49 fof(f46,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(ld(X0,mult(X0,X1)),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f11,f25])).
% 0.12/0.49 fof(f50,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(mult(X0,ld(X0,ld(X2,X2))),X2))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f36,f25])).
% 0.12/0.49 fof(f54,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3)))=mult(mult(X0,ld(X0,X2)),X3))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f11,f46])).
% 0.12/0.49 fof(f123,plain,(
% 0.12/0.49 ![X0,X1]: (mult(ld(ld(X0,X0),X1),ld(ld(ld(X0,X0),X1),X0))=mult(ld(X0,X0),X0))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f22,f50])).
% 0.12/0.49 fof(f137,plain,(
% 0.12/0.49 ![X0,X1]: (mult(ld(ld(X0,X0),X1),ld(ld(ld(X0,X0),X1),X0))=X0)),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f36,f123])).
% 0.12/0.49 fof(f323,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(X0,ld(mult(X0,ld(X0,X0)),mult(X1,X2)))=mult(mult(X0,ld(X0,X1)),X2))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f22,f54])).
% 0.12/0.49 fof(f339,plain,(
% 0.12/0.49 ![X0,X1,X2,X3,X4]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(ld(X2,X3),ld(ld(X2,X3),X4))))=mult(mult(X0,ld(X0,mult(X2,ld(X2,ld(X4,X4))))),X4))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f50,f54])).
% 0.12/0.49 fof(f344,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))=mult(mult(X0,ld(X0,ld(ld(X2,X2),X3))),ld(ld(ld(X2,X2),X3),X2)))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f137,f54])).
% 0.12/0.49 fof(f360,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.12/0.49 inference(paramodulation,[status(thm)],[f54,f11])).
% 0.12/0.49 fof(f376,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(X0,ld(X0,mult(ld(X2,X2),X2))))),
% 0.12/0.49 inference(backward_demodulation,[status(thm)],[f411,f50])).
% 0.12/0.49 fof(f411,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,X2)))=mult(mult(X0,ld(X0,X1)),X2))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f22,f323])).
% 0.12/0.49 fof(f469,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(mult(X0,ld(X0,ld(X1,X2))),ld(ld(X1,X2),X3))=mult(mult(X0,ld(X0,mult(X1,ld(X1,ld(X3,X3))))),X3))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f54,f339])).
% 0.12/0.49 fof(f470,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(mult(X0,ld(X0,mult(X1,ld(X1,ld(X3,X3))))),X3))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f469])).
% 0.12/0.49 fof(f471,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(mult(X1,ld(X1,ld(X3,X3))),X3))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f470])).
% 0.12/0.49 fof(f472,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(X1,ld(X1,mult(ld(X3,X3),X3))))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f471])).
% 0.12/0.49 fof(f473,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(ld(X1,X2),ld(ld(X1,X2),X3))))=mult(X0,ld(X0,mult(X1,ld(X1,X3)))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f36,f472])).
% 0.12/0.49 fof(f488,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(mult(X0,ld(X0,ld(ld(X2,X2),X3))),ld(ld(ld(X2,X2),X3),X2)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f344])).
% 0.12/0.49 fof(f489,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(ld(ld(X2,X2),X3),ld(ld(ld(X2,X2),X3),X2)))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f488])).
% 0.12/0.49 fof(f490,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(ld(X2,X2),ld(ld(X2,X2),X2)))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f473,f489])).
% 0.12/0.49 fof(f491,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,mult(X2,ld(X2,X2)))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f473,f490])).
% 0.12/0.49 fof(f494,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=mult(X0,ld(X0,X2)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f22,f491])).
% 0.12/0.49 fof(f550,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),mult(X2,X3))))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f360])).
% 0.12/0.49 fof(f551,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(mult(X0,ld(X0,X2)),X3)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f494,f550])).
% 0.12/0.49 fof(f552,plain,(
% 0.12/0.49 ![X0,X1,X2,X3]: (mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),mult(X2,X3))))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X2,X3)))))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f411,f551])).
% 0.12/0.49 fof(f584,plain,(
% 0.12/0.49 ![X0,X1,X2]: (mult(ld(X0,X1),ld(ld(X0,X1),X2))=mult(X0,ld(X0,X2)))),
% 0.12/0.49 inference(forward_demodulation,[status(thm)],[f36,f376])).
% 0.12/0.50 fof(f710,plain,(
% 0.12/0.50 ![X0,X1]: (mult(X0,ld(X0,mult(X0,X1)))=mult(X0,X1))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f22,f411])).
% 0.12/0.50 fof(f719,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X1,X2)))))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f411,f11])).
% 0.12/0.50 fof(f735,plain,(
% 0.12/0.50 ![X0,X1]: (mult(X0,mult(X0,ld(X0,X1)))=mult(X0,X1))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f11,f710])).
% 0.12/0.50 fof(f752,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),X2))))=ld(mult(X0,ld(X0,X1)),mult(X0,ld(X0,mult(X1,X2)))))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f411,f719])).
% 0.12/0.50 fof(f753,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=ld(mult(X0,ld(X0,X2)),mult(X0,ld(X0,mult(X2,X1)))))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f494,f752])).
% 0.12/0.50 fof(f754,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=mult(X0,ld(X0,ld(mult(X0,ld(X0,X2)),mult(X2,X1)))))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f552,f753])).
% 0.12/0.50 fof(f805,plain,(
% 0.12/0.50 ![X0,X1]: (ld(X0,X1)=mult(X0,ld(X0,ld(X0,X1))))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f22,f584])).
% 0.12/0.50 fof(f817,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(ld(X0,X1),mult(X0,ld(X0,X2)))=mult(ld(X0,X1),X2))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f584,f735])).
% 0.12/0.50 fof(f839,plain,(
% 0.12/0.50 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=mult(X0,ld(X0,mult(X1,ld(mult(X0,ld(X0,X1)),ld(mult(X0,ld(X0,X1)),X2))))))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f411,f805])).
% 0.12/0.50 fof(f852,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,ld(X0,X1))=ld(mult(X0,ld(X0,X2)),mult(X2,X1)))),
% 0.12/0.50 inference(backward_demodulation,[status(thm)],[f854,f754])).
% 0.12/0.50 fof(f854,plain,(
% 0.12/0.50 ![X0,X1,X2]: (ld(mult(X0,ld(X0,X1)),X2)=mult(X0,ld(X0,ld(mult(X0,ld(X0,X1)),X2))))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f494,f839])).
% 0.12/0.50 fof(f1656,plain,(
% 0.12/0.50 ![X0,X1,X2,X3]: (mult(X0,ld(X0,mult(X1,ld(X1,X2))))=ld(mult(X0,ld(X0,ld(X1,X3))),mult(ld(X1,X3),X2)))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f817,f852])).
% 0.12/0.50 fof(f1720,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,ld(X0,mult(X1,ld(X1,X2))))=mult(X0,ld(X0,X2)))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f852,f1656])).
% 0.12/0.50 fof(f2703,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,mult(X0,ld(X0,X1)))=mult(X0,mult(X2,ld(X2,X1))))),
% 0.12/0.50 inference(paramodulation,[status(thm)],[f1720,f735])).
% 0.12/0.50 fof(f2787,plain,(
% 0.12/0.50 ~mult(x3,x5)=mult(x3,x5)),
% 0.12/0.50 inference(backward_demodulation,[status(thm)],[f2797,f30])).
% 0.12/0.50 fof(f2797,plain,(
% 0.12/0.50 ![X0,X1,X2]: (mult(X0,X1)=mult(X0,mult(X2,ld(X2,X1))))),
% 0.12/0.50 inference(forward_demodulation,[status(thm)],[f735,f2703])).
% 0.12/0.50 fof(f2827,plain,(
% 0.12/0.50 $false),
% 0.12/0.50 inference(trivial_equality_resolution,[status(thm)],[f2787])).
% 0.12/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.51 % Elapsed time: 0.146411 seconds
% 0.12/0.51 % CPU time: 0.998582 seconds
% 0.12/0.51 % Total memory used: 39.763 MB
% 0.12/0.51 % Net memory used: 38.048 MB
%------------------------------------------------------------------------------