%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP660-13 : 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 : n015.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:06 PM UTC 2026
% Result : Unsatisfiable 42.10s 5.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP660-13 : 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.07/0.35 % Computer : n015.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 20:33:20 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 42.10/5.81 % Refutation found
% 42.10/5.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 42.10/5.81 % SZS output start CNFRefutation for theBenchmark
% 42.10/5.81 fof(f1,axiom,(
% 42.10/5.81 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f2,axiom,(
% 42.10/5.81 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f3,axiom,(
% 42.10/5.81 (![A,B]: (mult(rd(A,B),B) = A ))),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f4,axiom,(
% 42.10/5.81 (![A,B]: (rd(mult(A,B),B) = A ))),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f5,axiom,(
% 42.10/5.81 (![A,B,C]: (mult(mult(mult(A,B),C),A) = mult(A,mult(B,mult(C,A))) ))),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f6,negated_conjecture,(
% 42.10/5.81 mult(x0,ld(x1,x1)) != x0 ),
% 42.10/5.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.10/5.81 fof(f7,plain,(
% 42.10/5.81 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f1])).
% 42.10/5.81 fof(f8,plain,(
% 42.10/5.81 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f2])).
% 42.10/5.81 fof(f9,plain,(
% 42.10/5.81 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f3])).
% 42.10/5.81 fof(f10,plain,(
% 42.10/5.81 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f4])).
% 42.10/5.81 fof(f11,plain,(
% 42.10/5.81 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(X0,mult(X1,mult(X2,X0))))),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f5])).
% 42.10/5.81 fof(f12,plain,(
% 42.10/5.81 ~mult(x0,ld(x1,x1))=x0),
% 42.10/5.81 inference(cnf_transformation,[status(thm)],[f6])).
% 42.10/5.81 fof(f21,plain,(
% 42.10/5.81 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X2,mult(ld(X2,X0),mult(X1,X2))))),
% 42.10/5.81 inference(paramodulation,[status(thm)],[f7,f11])).
% 42.10/5.81 fof(f22,plain,(
% 42.10/5.81 ![X0,X1,X2]: (ld(mult(mult(X0,X1),X2),mult(X0,mult(X1,mult(X2,X0))))=X0)),
% 42.10/5.81 inference(paramodulation,[status(thm)],[f11,f8])).
% 42.10/5.81 fof(f29,plain,(
% 42.10/5.81 ![X0,X1,X2]: (ld(X0,mult(mult(X1,X2),X0))=mult(ld(X0,X1),mult(X2,X0)))),
% 42.10/5.81 inference(paramodulation,[status(thm)],[f21,f8])).
% 42.10/5.81 fof(f86,plain,(
% 42.10/5.81 ![X0,X1]: (mult(X0,X1)=mult(ld(mult(X0,X1),X0),mult(X1,mult(X0,X1))))),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f8,f29])).
% 42.90/5.81 fof(f94,plain,(
% 42.90/5.81 ![X0,X1,X2]: (ld(X0,mult(X1,X0))=mult(ld(X0,X2),mult(ld(X2,X1),X0)))),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f7,f29])).
% 42.90/5.81 fof(f123,plain,(
% 42.90/5.81 ![X0,X1]: (ld(ld(mult(X0,X1),X0),mult(X0,X1))=mult(X1,mult(X0,X1)))),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f86,f8])).
% 42.90/5.81 fof(f217,plain,(
% 42.90/5.81 ![X0,X1]: (ld(ld(X0,X1),mult(X1,ld(X1,X0)))=mult(ld(X1,X0),mult(X1,ld(X1,X0))))),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f7,f123])).
% 42.90/5.81 fof(f238,plain,(
% 42.90/5.81 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),mult(X1,ld(X1,X0))))),
% 42.90/5.81 inference(forward_demodulation,[status(thm)],[f7,f217])).
% 42.90/5.81 fof(f245,plain,(
% 42.90/5.81 ![X0,X1]: (ld(ld(X0,X1),X0)=mult(ld(X1,X0),X0))),
% 42.90/5.81 inference(forward_demodulation,[status(thm)],[f7,f238])).
% 42.90/5.81 fof(f262,plain,(
% 42.90/5.81 ![X0,X1]: (ld(X0,X1)=mult(ld(mult(X1,X0),X1),X1))),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f8,f245])).
% 42.90/5.81 fof(f289,plain,(
% 42.90/5.81 ![X0,X1]: (ld(ld(mult(X0,X1),X0),ld(X1,X0))=X0)),
% 42.90/5.81 inference(paramodulation,[status(thm)],[f262,f8])).
% 42.90/5.82 fof(f312,plain,(
% 42.90/5.82 ![X0,X1]: (ld(ld(mult(mult(X0,X1),X0),mult(X0,X1)),X1)=mult(X0,X1))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f8,f289])).
% 42.90/5.82 fof(f616,plain,(
% 42.90/5.82 ![X0,X1,X2]: (ld(mult(mult(X0,rd(X1,mult(X2,X0))),X2),mult(X0,X1))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f22])).
% 42.90/5.82 fof(f628,plain,(
% 42.90/5.82 ![X0,X1,X2]: (ld(mult(mult(X0,X1),rd(X2,X0)),mult(X0,mult(X1,X2)))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f22])).
% 42.90/5.82 fof(f632,plain,(
% 42.90/5.82 ![X0,X1,X2]: (mult(mult(X0,rd(X1,X2)),X2)=mult(X2,mult(ld(X2,X0),X1)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f21])).
% 42.90/5.82 fof(f633,plain,(
% 42.90/5.82 ![X0,X1,X2]: (mult(mult(X0,X1),rd(X0,X2))=mult(rd(X0,X2),mult(X2,mult(X1,rd(X0,X2)))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f11])).
% 42.90/5.82 fof(f634,plain,(
% 42.90/5.82 ![X0,X1]: (ld(rd(X0,X1),X0)=X1)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f8])).
% 42.90/5.82 fof(f653,plain,(
% 42.90/5.82 ![X0,X1]: (rd(ld(X0,X1),X1)=ld(mult(X1,X0),X1))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f262,f10])).
% 42.90/5.82 fof(f660,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,ld(X1,X0))=X1)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f7,f10])).
% 42.90/5.82 fof(f673,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(mult(mult(X1,X0),X1),mult(X1,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f312,f660])).
% 42.90/5.82 fof(f675,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,mult(ld(X1,X0),X0))=ld(X0,X1))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f245,f660])).
% 42.90/5.82 fof(f686,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,X1)=ld(mult(X1,rd(X1,X0)),X1))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f634,f653])).
% 42.90/5.82 fof(f700,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,mult(X1,X0))=ld(X0,rd(X0,X1)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f634,f675])).
% 42.90/5.82 fof(f711,plain,(
% 42.90/5.82 ![X0,X1]: (ld(X0,rd(X0,X1))=ld(mult(mult(X1,X0),X1),mult(X1,X0)))),
% 42.90/5.82 inference(backward_demodulation,[status(thm)],[f700,f673])).
% 42.90/5.82 fof(f725,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,rd(X1,X0))=mult(X0,rd(X0,X1)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f686,f660])).
% 42.90/5.82 fof(f732,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(X0,rd(X0,X1)),rd(X1,X0))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f686,f7])).
% 42.90/5.82 fof(f769,plain,(
% 42.90/5.82 ![X0,X1]: (rd(ld(X0,X1),X0)=mult(ld(X0,X1),rd(ld(X0,X1),X1)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f660,f725])).
% 42.90/5.82 fof(f777,plain,(
% 42.90/5.82 ![X0,X1]: (rd(ld(X0,X1),X0)=mult(ld(X0,X1),ld(mult(X1,X0),X1)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f653,f769])).
% 42.90/5.82 fof(f779,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(mult(X0,X1),X0),rd(X1,mult(X0,X1)))=mult(X0,X1))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f10,f732])).
% 42.90/5.82 fof(f811,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(mult(X0,X1),X0),ld(X1,rd(X1,X0)))=mult(X0,X1))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f700,f779])).
% 42.90/5.82 fof(f853,plain,(
% 42.90/5.82 ![X0,X1,X2]: (ld(mult(mult(X0,rd(X1,X2)),rd(X2,X0)),mult(X0,X1))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f616])).
% 42.90/5.82 fof(f876,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,mult(X2,X0))),X2))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f616,f660])).
% 42.90/5.82 fof(f1189,plain,(
% 42.90/5.82 ![X0,X1,X2]: (ld(mult(mult(X0,X1),rd(ld(X1,X2),X0)),mult(X0,X2))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f7,f628])).
% 42.90/5.82 fof(f2326,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,rd(X1,X2)),rd(X2,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f853,f660])).
% 42.90/5.82 fof(f2781,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(mult(ld(X0,X1),X2),ld(X0,X1))=mult(mult(ld(X0,X1),rd(X2,X1)),X0))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f7,f876])).
% 42.90/5.82 fof(f2810,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(rd(mult(X0,X1),X0),X2)=mult(X0,rd(X1,mult(X2,X0))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f876,f10])).
% 42.90/5.82 fof(f2946,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(mult(X0,X1),X0)=mult(mult(X0,X2),rd(ld(X2,X1),X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f1189,f660])).
% 42.90/5.82 fof(f3193,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(rd(X0,X1),X2)=mult(X1,rd(ld(X1,X0),mult(X2,X1))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f7,f2810])).
% 42.90/5.82 fof(f3331,plain,(
% 42.90/5.82 ![X0,X1,X2]: (ld(mult(X0,X1),rd(mult(X0,X2),X0))=rd(ld(X1,X2),X0))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f2946,f8])).
% 42.90/5.82 fof(f3431,plain,(
% 42.90/5.82 ![X0,X1]: (rd(rd(mult(X0,X1),X1),X0)=mult(X1,ld(mult(mult(X0,X1),X1),mult(X0,X1))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f653,f3193])).
% 42.90/5.82 fof(f3443,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(rd(X0,X1),rd(X2,X1))=mult(X1,rd(ld(X1,X0),X2)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f9,f3193])).
% 42.90/5.82 fof(f3445,plain,(
% 42.90/5.82 ![X0,X1,X2]: (rd(rd(X0,X1),ld(mult(X1,X2),X1))=mult(X1,rd(ld(X1,X0),ld(X2,X1))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f262,f3193])).
% 42.90/5.82 fof(f3504,plain,(
% 42.90/5.82 ![X0,X1]: (rd(X0,X0)=mult(X1,ld(mult(mult(X0,X1),X1),mult(X0,X1))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f10,f3431])).
% 42.90/5.82 fof(f3745,plain,(
% 42.90/5.82 ![X0]: (rd(X0,X0)=mult(rd(X0,X0),ld(rd(mult(X0,X0),X0),mult(X0,rd(X0,X0)))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f2326,f3504])).
% 42.90/5.82 fof(f3828,plain,(
% 42.90/5.82 ![X0]: (rd(X0,X0)=mult(rd(X0,X0),ld(X0,mult(X0,rd(X0,X0)))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f10,f3745])).
% 42.90/5.82 fof(f3829,plain,(
% 42.90/5.82 ![X0]: (rd(X0,X0)=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f8,f3828])).
% 42.90/5.82 fof(f4042,plain,(
% 42.90/5.82 ![X0]: (mult(mult(rd(X0,X0),rd(X0,X0)),ld(rd(X0,X0),rd(rd(X0,X0),rd(X0,X0))))=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f3829,f811])).
% 42.90/5.82 fof(f4046,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),rd(rd(X0,X0),rd(X0,X0)))=ld(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f3829,f711])).
% 42.90/5.82 fof(f4102,plain,(
% 42.90/5.82 ![X0]: (mult(rd(X0,X0),ld(rd(X0,X0),rd(rd(X0,X0),rd(X0,X0))))=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3829,f4042])).
% 42.90/5.82 fof(f4103,plain,(
% 42.90/5.82 ![X0]: (rd(rd(X0,X0),rd(X0,X0))=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f7,f4102])).
% 42.90/5.82 fof(f4104,plain,(
% 42.90/5.82 ![X0]: (mult(X0,rd(ld(X0,X0),X0))=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3443,f4103])).
% 42.90/5.82 fof(f4105,plain,(
% 42.90/5.82 ![X0]: (mult(X0,ld(mult(X0,X0),X0))=mult(rd(X0,X0),rd(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f653,f4104])).
% 42.90/5.82 fof(f4108,plain,(
% 42.90/5.82 ![X0]: (mult(X0,ld(mult(X0,X0),X0))=rd(X0,X0))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3829,f4105])).
% 42.90/5.82 fof(f4120,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),mult(X0,rd(ld(X0,X0),X0)))=ld(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3443,f4046])).
% 42.90/5.82 fof(f4121,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),mult(X0,ld(mult(X0,X0),X0)))=ld(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f653,f4120])).
% 42.90/5.82 fof(f4122,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),rd(X0,X0))=ld(mult(rd(X0,X0),rd(X0,X0)),mult(rd(X0,X0),rd(X0,X0))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f4108,f4121])).
% 42.90/5.82 fof(f4123,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),rd(X0,X0))=ld(rd(X0,X0),mult(rd(X0,X0),rd(X0,X0))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3829,f4122])).
% 42.90/5.82 fof(f4126,plain,(
% 42.90/5.82 ![X0]: (ld(rd(X0,X0),rd(X0,X0))=rd(X0,X0))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f8,f4123])).
% 42.90/5.82 fof(f4194,plain,(
% 42.90/5.82 ![X0]: (rd(rd(X0,X0),ld(mult(X0,X0),X0))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4108,f10])).
% 42.90/5.82 fof(f4209,plain,(
% 42.90/5.82 ![X0]: (ld(X0,rd(X0,X0))=ld(mult(X0,X0),X0))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4108,f8])).
% 42.90/5.82 fof(f4245,plain,(
% 42.90/5.82 ![X0]: (mult(X0,rd(ld(X0,X0),ld(X0,X0)))=X0)),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f3445,f4194])).
% 42.90/5.82 fof(f5302,plain,(
% 42.90/5.82 ![X0]: (mult(mult(ld(X0,X0),X0),rd(ld(X0,X0),ld(X0,X0)))=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4245,f633])).
% 42.90/5.82 fof(f5314,plain,(
% 42.90/5.82 ![X0]: (rd(ld(rd(ld(X0,X0),ld(X0,X0)),X0),rd(ld(X0,X0),ld(X0,X0)))=mult(ld(rd(ld(X0,X0),ld(X0,X0)),X0),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4245,f777])).
% 42.90/5.82 fof(f5330,plain,(
% 42.90/5.82 ![X0]: (ld(rd(ld(X0,X0),ld(X0,X0)),X0)=mult(ld(X0,X0),X0))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4245,f262])).
% 42.90/5.82 fof(f5340,plain,(
% 42.90/5.82 ![X0]: (ld(X0,X0)=rd(ld(X0,X0),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4245,f8])).
% 42.90/5.82 fof(f5365,plain,(
% 42.90/5.82 ![X0]: (rd(mult(ld(X0,X0),X0),ld(X0,X0))=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f2946,f5302])).
% 42.90/5.82 fof(f5366,plain,(
% 42.90/5.82 ![X0]: (mult(mult(ld(X0,X0),rd(X0,X0)),X0)=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f2781,f5365])).
% 42.90/5.82 fof(f5367,plain,(
% 42.90/5.82 ![X0]: (mult(X0,mult(ld(X0,ld(X0,X0)),X0))=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f632,f5366])).
% 42.90/5.82 fof(f5407,plain,(
% 42.90/5.82 ![X0]: (rd(ld(rd(ld(X0,X0),ld(X0,X0)),X0),rd(ld(X0,X0),ld(X0,X0)))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(backward_demodulation,[status(thm)],[f5330,f5314])).
% 42.90/5.82 fof(f5445,plain,(
% 42.90/5.82 ![X0]: (mult(X0,mult(ld(X0,ld(X0,X0)),X0))=mult(ld(X0,X0),mult(ld(X0,X0),X0)))),
% 42.90/5.82 inference(backward_demodulation,[status(thm)],[f5340,f5367])).
% 42.90/5.82 fof(f5463,plain,(
% 42.90/5.82 ![X0]: (rd(mult(ld(X0,X0),X0),rd(ld(X0,X0),ld(X0,X0)))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5330,f5407])).
% 42.90/5.82 fof(f5464,plain,(
% 42.90/5.82 ![X0]: (rd(mult(ld(X0,X0),X0),ld(X0,X0))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5340,f5463])).
% 42.90/5.82 fof(f5465,plain,(
% 42.90/5.82 ![X0]: (mult(mult(ld(X0,X0),rd(X0,X0)),X0)=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f2781,f5464])).
% 42.90/5.82 fof(f5466,plain,(
% 42.90/5.82 ![X0]: (mult(X0,mult(ld(X0,ld(X0,X0)),X0))=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f632,f5465])).
% 42.90/5.82 fof(f5503,plain,(
% 42.90/5.82 ![X0]: (mult(X0,mult(ld(X0,ld(X0,X0)),X0))=ld(X0,mult(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f94,f5445])).
% 42.90/5.82 fof(f5504,plain,(
% 42.90/5.82 ![X0]: (X0=mult(mult(ld(X0,X0),X0),ld(X0,X0)))),
% 42.90/5.82 inference(backward_demodulation,[status(thm)],[f5505,f5466])).
% 42.90/5.82 fof(f5505,plain,(
% 42.90/5.82 ![X0]: (mult(X0,mult(ld(X0,ld(X0,X0)),X0))=X0)),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f8,f5503])).
% 42.90/5.82 fof(f5508,plain,(
% 42.90/5.82 ![X0]: (ld(ld(X0,rd(X0,X0)),ld(X0,X0))=X0)),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f4209,f289])).
% 42.90/5.82 fof(f5779,plain,(
% 42.90/5.82 ![X0]: (ld(ld(X0,X0),rd(ld(X0,X0),ld(X0,X0)))=rd(ld(X0,X0),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f5340,f4126])).
% 42.90/5.82 fof(f5782,plain,(
% 42.90/5.82 ![X0,X1]: (rd(mult(ld(X0,X0),X1),ld(X0,X0))=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f5340,f2326])).
% 42.90/5.82 fof(f5786,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(ld(X0,X0),X1),rd(ld(X0,X0),ld(X0,X0)))=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),mult(X1,ld(X0,X0)))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f5340,f633])).
% 42.90/5.82 fof(f5820,plain,(
% 42.90/5.82 ![X0]: (ld(ld(X0,X0),ld(X0,X0))=rd(ld(X0,X0),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5340,f5779])).
% 42.90/5.82 fof(f5821,plain,(
% 42.90/5.82 ![X0]: (ld(ld(X0,X0),ld(X0,X0))=ld(X0,X0))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5340,f5820])).
% 42.90/5.82 fof(f5825,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f2781,f5782])).
% 42.90/5.82 fof(f5826,plain,(
% 42.90/5.82 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(mult(ld(X0,X0),rd(X1,ld(X0,X0))),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f632,f5825])).
% 42.90/5.82 fof(f5827,plain,(
% 42.90/5.82 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(ld(ld(X0,X0),ld(X0,X0)),X1)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f632,f5826])).
% 42.90/5.82 fof(f5829,plain,(
% 42.90/5.82 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,X0),mult(ld(X0,X0),X1)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5821,f5827])).
% 42.90/5.82 fof(f5836,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(rd(ld(X0,X0),ld(X0,X0)),mult(ld(X0,X0),mult(X1,ld(X0,X0)))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5340,f5786])).
% 42.90/5.82 fof(f5837,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(ld(X0,X0),mult(ld(X0,X0),mult(X1,ld(X0,X0)))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5340,f5836])).
% 42.90/5.82 fof(f5838,plain,(
% 42.90/5.82 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=mult(X0,mult(ld(X0,ld(X0,X0)),mult(X1,ld(X0,X0)))))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f5829,f5837])).
% 42.90/5.82 fof(f6074,plain,(
% 42.90/5.82 ![X0]: (mult(X0,ld(X0,rd(X0,ld(X0,X0))))=mult(ld(X0,X0),X0))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f5504,f811])).
% 42.90/5.82 fof(f6127,plain,(
% 42.90/5.82 ![X0]: (rd(X0,ld(X0,X0))=mult(ld(X0,X0),X0))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f7,f6074])).
% 42.90/5.82 fof(f6132,plain,(
% 42.90/5.82 ![X0]: (X0=mult(ld(X0,X0),X0))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f660,f6127])).
% 42.90/5.82 fof(f6340,plain,(
% 42.90/5.82 ![X0,X1]: (ld(X0,rd(mult(ld(X0,X0),X1),ld(X0,X0)))=rd(ld(X0,X1),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f6132,f3331])).
% 42.90/5.82 fof(f6355,plain,(
% 42.90/5.82 ![X0]: (rd(X0,X0)=ld(X0,rd(X0,ld(X0,X0))))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f6132,f700])).
% 42.90/5.82 fof(f6361,plain,(
% 42.90/5.82 ![X0]: (ld(X0,ld(X0,X0))=mult(ld(X0,ld(X0,X0)),ld(X0,X0)))),
% 42.90/5.82 inference(paramodulation,[status(thm)],[f6132,f262])).
% 42.90/5.82 fof(f6393,plain,(
% 42.90/5.82 ![X0,X1]: (ld(X0,mult(mult(ld(X0,X0),rd(X1,X0)),X0))=rd(ld(X0,X1),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f2781,f6340])).
% 42.90/5.82 fof(f6394,plain,(
% 42.90/5.82 ![X0,X1]: (mult(ld(X0,ld(X0,X0)),mult(rd(X1,X0),X0))=rd(ld(X0,X1),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f29,f6393])).
% 42.90/5.82 fof(f6395,plain,(
% 42.90/5.82 ![X0,X1]: (mult(ld(X0,ld(X0,X0)),X1)=rd(ld(X0,X1),ld(X0,X0)))),
% 42.90/5.82 inference(forward_demodulation,[status(thm)],[f9,f6394])).
% 42.90/5.86 fof(f6494,plain,(
% 42.90/5.86 ![X0]: (ld(ld(X0,ld(X0,X0)),ld(X0,X0))=X0)),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f6527,f5508])).
% 42.90/5.86 fof(f6527,plain,(
% 42.90/5.86 ![X0]: (rd(X0,X0)=ld(X0,X0))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f660,f6355])).
% 42.90/5.86 fof(f11617,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,ld(X0,X0)),mult(X0,X1))=rd(X1,ld(X0,X0)))),
% 42.90/5.86 inference(paramodulation,[status(thm)],[f8,f6395])).
% 42.90/5.86 fof(f11619,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(ld(X0,X0),ld(ld(X0,X0),ld(X0,X0))),X1)=rd(ld(ld(X0,X0),X1),ld(X0,X0)))),
% 42.90/5.86 inference(paramodulation,[status(thm)],[f5821,f6395])).
% 42.90/5.86 fof(f11627,plain,(
% 42.90/5.86 ![X0,X1]: (mult(mult(mult(ld(X0,X0),ld(X0,X1)),ld(X0,X0)),ld(ld(X0,X1),mult(ld(X0,ld(X0,X0)),X1)))=mult(ld(X0,X0),ld(X0,X1)))),
% 42.90/5.86 inference(paramodulation,[status(thm)],[f6395,f811])).
% 42.90/5.86 fof(f11694,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(ld(X0,X0),ld(X0,X0)),X1)=rd(ld(ld(X0,X0),X1),ld(X0,X0)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f5821,f11619])).
% 42.90/5.86 fof(f11697,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X0),X1)=rd(ld(ld(X0,X0),X1),ld(X0,X0)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f5821,f11694])).
% 42.90/5.86 fof(f12000,plain,(
% 42.90/5.86 ![X0,X1]: (rd(mult(ld(X0,X0),X1),ld(X0,X0))=mult(mult(ld(X0,X0),rd(X1,ld(X0,ld(X0,X0)))),ld(X0,ld(X0,X0))))),
% 42.90/5.86 inference(paramodulation,[status(thm)],[f6361,f876])).
% 42.90/5.86 fof(f12145,plain,(
% 42.90/5.86 ![X0,X1]: (mult(mult(ld(X0,X0),rd(X1,X0)),X0)=mult(mult(ld(X0,X0),rd(X1,ld(X0,ld(X0,X0)))),ld(X0,ld(X0,X0))))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f2781,f12000])).
% 42.90/5.86 fof(f12146,plain,(
% 42.90/5.86 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(mult(ld(X0,X0),rd(X1,ld(X0,ld(X0,X0)))),ld(X0,ld(X0,X0))))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f632,f12145])).
% 42.90/5.86 fof(f12147,plain,(
% 42.90/5.86 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,ld(X0,X0)),mult(ld(ld(X0,ld(X0,X0)),ld(X0,X0)),X1)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f632,f12146])).
% 42.90/5.86 fof(f12148,plain,(
% 42.90/5.86 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=mult(ld(X0,ld(X0,X0)),mult(X0,X1)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f6494,f12147])).
% 42.90/5.86 fof(f12154,plain,(
% 42.90/5.86 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=rd(mult(X1,ld(X0,X0)),ld(X0,X0)))),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12171,f5838])).
% 42.90/5.86 fof(f12171,plain,(
% 42.90/5.86 ![X0,X1]: (mult(X0,mult(ld(X0,ld(X0,X0)),X1))=rd(X1,ld(X0,X0)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f11617,f12148])).
% 42.90/5.86 fof(f12288,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X1),ld(ld(X0,X1),mult(ld(X0,ld(X0,X0)),X1)))=mult(ld(X0,X0),ld(X0,X1)))),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12301,f11627])).
% 42.90/5.86 fof(f12301,plain,(
% 42.90/5.86 ![X0,X1]: (mult(mult(ld(X0,X0),X1),ld(X0,X0))=X1)),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f10,f12154])).
% 42.90/5.86 fof(f12359,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X0),ld(X0,mult(X0,X1)))=rd(X1,ld(X0,X0)))),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12381,f11617])).
% 42.90/5.86 fof(f12381,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,ld(X0,X0)),X1)=mult(ld(X0,X0),ld(X0,X1)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f7,f12288])).
% 42.90/5.86 fof(f12517,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X0),X1)=mult(ld(X0,X0),ld(ld(X0,X0),X1)))),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12554,f11697])).
% 42.90/5.86 fof(f12554,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X0),X1)=rd(X1,ld(X0,X0)))),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f8,f12359])).
% 42.90/5.86 fof(f12742,plain,(
% 42.90/5.86 ![X0,X1]: (mult(X0,ld(X1,X1))=X0)),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12752,f12301])).
% 42.90/5.86 fof(f12752,plain,(
% 42.90/5.86 ![X0,X1]: (mult(ld(X0,X0),X1)=X1)),
% 42.90/5.86 inference(forward_demodulation,[status(thm)],[f7,f12517])).
% 42.90/5.86 fof(f13339,plain,(
% 42.90/5.86 ~x0=x0),
% 42.90/5.86 inference(backward_demodulation,[status(thm)],[f12742,f12])).
% 42.90/5.86 fof(f13908,plain,(
% 42.90/5.86 $false),
% 42.90/5.86 inference(trivial_equality_resolution,[status(thm)],[f13339])).
% 42.90/5.86 % SZS output end CNFRefutation for theBenchmark.p
% 33.69/7.14 % Elapsed time: 6.561736 seconds
% 33.69/7.14 % CPU time: 20.940814 seconds
% 33.69/7.14 % Total memory used: 428.762 MB
% 33.69/7.14 % Net memory used: 426.924 MB
%------------------------------------------------------------------------------