%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP755-1 : TPTP v9.3.1. Released v4.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 12:37:17 PM UTC 2026
% Result : Unsatisfiable 140.95s 18.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP755-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 20:40:36 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 140.95/18.38 % Refutation found
% 140.95/18.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 140.95/18.38 % SZS output start CNFRefutation for theBenchmark
% 140.95/18.38 fof(f1,axiom,(
% 140.95/18.38 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f2,axiom,(
% 140.95/18.38 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f3,axiom,(
% 140.95/18.38 (![A,B]: (mult(rd(A,B),B) = A ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f4,axiom,(
% 140.95/18.38 (![A,B]: (rd(mult(A,B),B) = A ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f5,axiom,(
% 140.95/18.38 (![A]: (mult(A,unit) = A ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f6,axiom,(
% 140.95/18.38 (![A]: (mult(unit,A) = A ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f7,axiom,(
% 140.95/18.38 (![A,B,C]: (( mult(A,mult(B,C)) = mult(mult(A,B),C)| mult(A,mult(B,C)) = mult(mult(A,C),B) ) ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f8,axiom,(
% 140.95/18.38 (![A,B,C]: (( mult(A,mult(B,C)) = mult(mult(A,B),C)| mult(A,mult(C,B)) = mult(mult(A,B),C) ) ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f9,axiom,(
% 140.95/18.38 (![A]: (i(A) = ld(A,unit) ))),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f10,negated_conjecture,(
% 140.95/18.38 i(mult(a,b)) != mult(i(b),i(a)) ),
% 140.95/18.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.95/18.38 fof(f11,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f1])).
% 140.95/18.38 fof(f12,plain,(
% 140.95/18.38 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f2])).
% 140.95/18.38 fof(f13,plain,(
% 140.95/18.38 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f3])).
% 140.95/18.38 fof(f14,plain,(
% 140.95/18.38 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f4])).
% 140.95/18.38 fof(f15,plain,(
% 140.95/18.38 ![X0]: (mult(X0,unit)=X0)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f5])).
% 140.95/18.38 fof(f16,plain,(
% 140.95/18.38 ![X0]: (mult(unit,X0)=X0)),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f6])).
% 140.95/18.38 fof(f17,plain,(
% 140.95/18.38 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(mult(X0,X1),X2)|mult(X0,mult(X1,X2))=mult(mult(X0,X2),X1))),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f7])).
% 140.95/18.38 fof(f18,plain,(
% 140.95/18.38 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(mult(X0,X1),X2)|mult(X0,mult(X2,X1))=mult(mult(X0,X1),X2))),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f8])).
% 140.95/18.38 fof(f19,plain,(
% 140.95/18.38 ![X0]: (i(X0)=ld(X0,unit))),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f9])).
% 140.95/18.38 fof(f20,plain,(
% 140.95/18.38 ~i(mult(a,b))=mult(i(b),i(a))),
% 140.95/18.38 inference(cnf_transformation,[status(thm)],[f10])).
% 140.95/18.38 fof(f23,plain,(
% 140.95/18.38 ![X0]: (ld(unit,X0)=X0)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f16,f11])).
% 140.95/18.38 fof(f27,plain,(
% 140.95/18.38 ![X0]: (ld(X0,X0)=unit)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f15,f12])).
% 140.95/18.38 fof(f50,plain,(
% 140.95/18.38 ![X0]: (mult(X0,i(X0))=unit)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f19,f11])).
% 140.95/18.38 fof(f82,plain,(
% 140.95/18.38 ![X0,X1,X2]: (mult(X0,mult(X1,ld(mult(X0,X1),X2)))=X2|mult(X0,mult(X1,ld(mult(X0,X1),X2)))=mult(mult(X0,ld(mult(X0,X1),X2)),X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f11,f17])).
% 140.95/18.38 fof(f170,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=mult(unit,X1)|mult(X0,mult(X1,i(X0)))=mult(mult(X0,i(X0)),X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f50,f18])).
% 140.95/18.38 fof(f185,plain,(
% 140.95/18.38 ![X0,X1,X2]: (~mult(X0,mult(X1,X2))=mult(X0,mult(X2,X1))|mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1)))),
% 140.95/18.38 inference(equality_factoring,[status(thm)],[f18])).
% 140.95/18.38 fof(f195,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|mult(X0,mult(X1,i(X0)))=mult(mult(X0,i(X0)),X1))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f16,f170])).
% 140.95/18.38 fof(f196,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|mult(X0,mult(X1,i(X0)))=mult(unit,X1))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f195])).
% 140.95/18.38 fof(f197,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|mult(X0,mult(X1,i(X0)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f16,f196])).
% 140.95/18.38 fof(f222,plain,(
% 140.95/18.38 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|mult(X0,mult(X1,i(X0)))=X1)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f197,f12])).
% 140.95/18.38 fof(f269,plain,(
% 140.95/18.38 ![X0,X1]: (ld(X0,X1)=mult(X1,i(X0))|ld(X0,X1)=mult(i(X0),X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f222,f12])).
% 140.95/18.38 fof(f320,plain,(
% 140.95/18.38 ![X0,X1]: (rd(ld(X0,X1),i(X0))=X1|ld(X0,X1)=mult(i(X0),X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f269,f14])).
% 140.95/18.38 fof(f321,plain,(
% 140.95/18.38 ![X0,X1]: (ld(X0,ld(X1,X0))=i(X1)|ld(X1,X0)=mult(i(X1),X0))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f269,f12])).
% 140.95/18.38 fof(f330,plain,(
% 140.95/18.38 ![X0,X1]: (rd(X0,i(X1))=mult(X1,X0)|ld(X1,mult(X1,X0))=mult(i(X1),mult(X1,X0)))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f12,f320])).
% 140.95/18.38 fof(f338,plain,(
% 140.95/18.38 ![X0,X1]: (rd(X0,i(X1))=mult(X1,X0)|X0=mult(i(X1),mult(X1,X0)))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f12,f330])).
% 140.95/18.38 fof(f346,plain,(
% 140.95/18.38 ![X0,X1]: (ld(mult(X0,X1),X1)=i(X0)|ld(X0,mult(X0,X1))=mult(i(X0),mult(X0,X1)))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f12,f321])).
% 140.95/18.38 fof(f354,plain,(
% 140.95/18.38 ![X0,X1]: (ld(mult(X0,X1),X1)=i(X0)|X1=mult(i(X0),mult(X0,X1)))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f12,f346])).
% 140.95/18.38 fof(f397,plain,(
% 140.95/18.38 ![X0,X1]: (ld(i(X0),X1)=mult(X0,X1)|rd(X1,i(X0))=mult(X0,X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f338,f12])).
% 140.95/18.38 fof(f463,plain,(
% 140.95/18.38 ![X0,X1]: (mult(mult(X0,X1),i(X0))=X1|X1=mult(i(X0),mult(X0,X1)))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f354,f11])).
% 140.95/18.38 fof(f858,plain,(
% 140.95/18.38 ![X0,X1]: (mult(mult(X0,X1),i(X0))=X1|ld(i(X0),X1)=mult(X0,X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f397,f13])).
% 140.95/18.38 fof(f930,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=ld(mult(X0,i(X0)),X1)|ld(mult(X0,i(X0)),X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f82,f463])).
% 140.95/18.38 fof(f980,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),ld(unit,X1)))=ld(mult(X0,i(X0)),X1)|ld(mult(X0,i(X0)),X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f930])).
% 140.95/18.38 fof(f981,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=ld(mult(X0,i(X0)),X1)|ld(mult(X0,i(X0)),X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f980])).
% 140.95/18.38 fof(f982,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=ld(unit,X1)|ld(mult(X0,i(X0)),X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f981])).
% 140.95/18.38 fof(f983,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(mult(X0,i(X0)),X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f982])).
% 140.95/18.38 fof(f984,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(unit,X1)=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f983])).
% 140.95/18.38 fof(f985,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,ld(mult(X0,i(X0)),X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f984])).
% 140.95/18.38 fof(f986,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,ld(unit,X1)))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f985])).
% 140.95/18.38 fof(f987,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f986])).
% 140.95/18.38 fof(f988,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,X1))|mult(X0,mult(i(X0),ld(unit,X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f987])).
% 140.95/18.38 fof(f989,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,X1))|mult(X0,mult(i(X0),X1))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f988])).
% 140.95/18.38 fof(f990,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|X1=mult(i(X0),mult(X0,X1)))),
% 140.95/18.38 inference(duplicate_literals_removal,[status(thm)],[f989])).
% 140.95/18.38 fof(f1220,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=ld(mult(X0,i(X0)),X1)|ld(i(X0),ld(mult(X0,i(X0)),X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f82,f858])).
% 140.95/18.38 fof(f1276,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),ld(unit,X1)))=ld(mult(X0,i(X0)),X1)|ld(i(X0),ld(mult(X0,i(X0)),X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1220])).
% 140.95/18.38 fof(f1277,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=ld(mult(X0,i(X0)),X1)|ld(i(X0),ld(mult(X0,i(X0)),X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f1276])).
% 140.95/18.38 fof(f1278,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=ld(unit,X1)|ld(i(X0),ld(mult(X0,i(X0)),X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1277])).
% 140.95/18.38 fof(f1279,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),ld(mult(X0,i(X0)),X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f1278])).
% 140.95/18.38 fof(f1280,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),ld(unit,X1))=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1279])).
% 140.95/18.38 fof(f1281,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,ld(mult(X0,i(X0)),X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f1280])).
% 140.95/18.38 fof(f1282,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,ld(unit,X1))|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1281])).
% 140.95/18.38 fof(f1283,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,X1)|mult(X0,mult(i(X0),ld(mult(X0,i(X0)),X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f1282])).
% 140.95/18.38 fof(f1284,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,X1)|mult(X0,mult(i(X0),ld(unit,X1)))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1283])).
% 140.95/18.38 fof(f1285,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,X1)|mult(X0,mult(i(X0),X1))=X1)),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f23,f1284])).
% 140.95/18.38 fof(f1286,plain,(
% 140.95/18.38 ![X0,X1]: (mult(X0,mult(i(X0),X1))=X1|ld(i(X0),X1)=mult(X0,X1))),
% 140.95/18.38 inference(duplicate_literals_removal,[status(thm)],[f1285])).
% 140.95/18.38 fof(f1440,plain,(
% 140.95/18.38 ![X0]: (mult(X0,mult(i(X0),i(i(X0))))=i(i(X0))|i(i(X0))=X0|ld(i(X0),X0)=mult(i(i(X0)),X0))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f222,f990])).
% 140.95/18.38 fof(f1488,plain,(
% 140.95/18.38 ![X0]: (mult(X0,unit)=i(i(X0))|i(i(X0))=X0|ld(i(X0),X0)=mult(i(i(X0)),X0))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f50,f1440])).
% 140.95/18.38 fof(f1489,plain,(
% 140.95/18.38 ![X0]: (X0=i(i(X0))|i(i(X0))=X0|ld(i(X0),X0)=mult(i(i(X0)),X0))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f15,f1488])).
% 140.95/18.38 fof(f1490,plain,(
% 140.95/18.38 ![X0]: (X0=i(i(X0))|ld(i(X0),X0)=mult(i(i(X0)),X0))),
% 140.95/18.38 inference(duplicate_literals_removal,[status(thm)],[f1489])).
% 140.95/18.38 fof(f2569,plain,(
% 140.95/18.38 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|ld(i(X0),X1)=mult(X0,X1))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f1286,f12])).
% 140.95/18.38 fof(f2737,plain,(
% 140.95/18.38 ![X0]: (rd(ld(i(X0),X0),X0)=i(i(X0))|X0=i(i(X0)))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f1490,f14])).
% 140.95/18.38 fof(f3349,plain,(
% 140.95/18.38 ![X0]: (rd(mult(X0,X0),X0)=i(i(X0))|X0=i(i(X0))|ld(X0,X0)=mult(i(X0),X0))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f2569,f2737])).
% 140.95/18.38 fof(f3374,plain,(
% 140.95/18.38 ![X0]: (X0=i(i(X0))|X0=i(i(X0))|ld(X0,X0)=mult(i(X0),X0))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f14,f3349])).
% 140.95/18.38 fof(f3375,plain,(
% 140.95/18.38 ![X0]: (X0=i(i(X0))|X0=i(i(X0))|unit=mult(i(X0),X0))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f27,f3374])).
% 140.95/18.38 fof(f3376,plain,(
% 140.95/18.38 ![X0]: (X0=i(i(X0))|unit=mult(i(X0),X0))),
% 140.95/18.38 inference(duplicate_literals_removal,[status(thm)],[f3375])).
% 140.95/18.38 fof(f3436,plain,(
% 140.95/18.38 ![X0]: (ld(i(X0),unit)=X0|X0=i(i(X0)))),
% 140.95/18.38 inference(paramodulation,[status(thm)],[f3376,f12])).
% 140.95/18.38 fof(f3494,plain,(
% 140.95/18.38 ![X0]: (i(i(X0))=X0|X0=i(i(X0)))),
% 140.95/18.38 inference(forward_demodulation,[status(thm)],[f19,f3436])).
% 140.95/18.55 fof(f3495,plain,(
% 140.95/18.55 ![X0]: (i(i(X0))=X0)),
% 140.95/18.55 inference(duplicate_literals_removal,[status(thm)],[f3494])).
% 140.95/18.55 fof(f5693,plain,(
% 140.95/18.55 ![X0,X1]: (ld(i(i(X0)),X1)=mult(i(X0),X1)|rd(X1,X0)=mult(i(X0),X1))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f3495,f397])).
% 140.95/18.55 fof(f5696,plain,(
% 140.95/18.55 ![X0,X1]: (ld(i(X0),X1)=mult(X1,X0)|ld(i(X0),X1)=mult(i(i(X0)),X1))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f3495,f269])).
% 140.95/18.55 fof(f5702,plain,(
% 140.95/18.55 ![X0]: (mult(i(X0),X0)=unit)),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f3495,f50])).
% 140.95/18.55 fof(f5719,plain,(
% 140.95/18.55 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|rd(X1,X0)=mult(i(X0),X1))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f3495,f5693])).
% 140.95/18.55 fof(f5722,plain,(
% 140.95/18.55 ![X0,X1]: (ld(i(X0),X1)=mult(X1,X0)|ld(i(X0),X1)=mult(X0,X1))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f3495,f5696])).
% 140.95/18.55 fof(f5982,plain,(
% 140.95/18.55 ![X0,X1]: (~mult(X0,mult(X1,i(X1)))=mult(X0,unit)|mult(mult(X0,X1),i(X1))=mult(X0,mult(i(X1),X1)))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f5702,f185])).
% 140.95/18.55 fof(f6047,plain,(
% 140.95/18.55 ![X0,X1]: (~mult(X0,unit)=mult(X0,unit)|mult(mult(X0,X1),i(X1))=mult(X0,mult(i(X1),X1)))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f50,f5982])).
% 140.95/18.55 fof(f6048,plain,(
% 140.95/18.55 ![X0,X1]: (~X0=mult(X0,unit)|mult(mult(X0,X1),i(X1))=mult(X0,mult(i(X1),X1)))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f15,f6047])).
% 140.95/18.55 fof(f6049,plain,(
% 140.95/18.55 ![X0,X1]: (~X0=X0|mult(mult(X0,X1),i(X1))=mult(X0,mult(i(X1),X1)))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f15,f6048])).
% 140.95/18.55 fof(f6050,plain,(
% 140.95/18.55 ![X0,X1]: (~X0=X0|mult(mult(X0,X1),i(X1))=mult(X0,unit))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f5702,f6049])).
% 140.95/18.55 fof(f6051,plain,(
% 140.95/18.55 ![X0,X1]: (~X0=X0|mult(mult(X0,X1),i(X1))=X0)),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f15,f6050])).
% 140.95/18.55 fof(f6052,plain,(
% 140.95/18.55 ![X0,X1]: (mult(mult(X0,X1),i(X1))=X0)),
% 140.95/18.55 inference(trivial_equality_resolution,[status(thm)],[f6051])).
% 140.95/18.55 fof(f6174,plain,(
% 140.95/18.55 ![X0,X1]: (mult(X0,i(i(X1)))=mult(X1,X0)|ld(i(X1),X0)=mult(X1,X0))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f858,f6052])).
% 140.95/18.55 fof(f6181,plain,(
% 140.95/18.55 ![X0,X1]: (mult(X0,i(X1))=rd(X0,X1))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f13,f6052])).
% 140.95/18.55 fof(f6255,plain,(
% 140.95/18.55 ![X0,X1]: (ld(mult(X0,X1),X0)=i(X1))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f6052,f12])).
% 140.95/18.55 fof(f6264,plain,(
% 140.95/18.55 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|ld(i(X1),X0)=mult(X1,X0))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f3495,f6174])).
% 140.95/18.55 fof(f6992,plain,(
% 140.95/18.55 ~i(mult(a,b))=rd(i(b),a)),
% 140.95/18.55 inference(backward_demodulation,[status(thm)],[f6181,f20])).
% 140.95/18.55 fof(f7007,plain,(
% 140.95/18.55 ![X0,X1]: (ld(X0,X1)=rd(X1,X0)|ld(X0,X1)=mult(i(X0),X1))),
% 140.95/18.55 inference(backward_demodulation,[status(thm)],[f6181,f269])).
% 140.95/18.55 fof(f7278,plain,(
% 140.95/18.55 ![X0,X1]: (ld(X0,X1)=i(ld(X1,X0)))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f11,f6255])).
% 140.95/18.55 fof(f39125,plain,(
% 140.95/18.55 ![X0,X1]: (~rd(X0,X1)=ld(X1,X0)|mult(i(X1),X0)=ld(X1,X0))),
% 140.95/18.55 inference(equality_factoring,[status(thm)],[f5719])).
% 140.95/18.55 fof(f39568,plain,(
% 140.95/18.55 ![X0,X1]: (mult(i(X0),X1)=ld(X0,X1))),
% 140.95/18.55 inference(forward_subsumption_resolution,[status(thm)],[f39125,f7007])).
% 140.95/18.55 fof(f40526,plain,(
% 140.95/18.55 ![X0,X1]: (~mult(X0,X1)=mult(X1,X0)|ld(i(X1),X0)=mult(X1,X0))),
% 140.95/18.55 inference(equality_factoring,[status(thm)],[f5722])).
% 140.95/18.55 fof(f40620,plain,(
% 140.95/18.55 ![X0,X1]: (ld(i(X0),X1)=mult(X0,X1))),
% 140.95/18.55 inference(forward_subsumption_resolution,[status(thm)],[f40526,f6264])).
% 140.95/18.55 fof(f49718,plain,(
% 140.95/18.55 ![X0,X1]: (rd(i(X0),X1)=ld(X0,i(X1)))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f6181,f39568])).
% 140.95/18.55 fof(f50940,plain,(
% 140.95/18.55 ![X0,X1]: (ld(X0,i(X1))=i(mult(X1,X0)))),
% 140.95/18.55 inference(paramodulation,[status(thm)],[f40620,f7278])).
% 140.95/18.55 fof(f52320,plain,(
% 140.95/18.55 ~i(mult(a,b))=ld(b,i(a))),
% 140.95/18.55 inference(backward_demodulation,[status(thm)],[f49718,f6992])).
% 140.95/18.55 fof(f52784,plain,(
% 140.95/18.55 ~i(mult(a,b))=i(mult(a,b))),
% 140.95/18.55 inference(forward_demodulation,[status(thm)],[f50940,f52320])).
% 140.95/18.55 fof(f52785,plain,(
% 140.95/18.55 $false),
% 140.95/18.55 inference(trivial_equality_resolution,[status(thm)],[f52784])).
% 140.95/18.55 % SZS output end CNFRefutation for theBenchmark.p
% 140.95/18.55 % Elapsed time: 18.172783 seconds
% 140.95/18.55 % CPU time: 143.077658 seconds
% 140.95/18.55 % Total memory used: 1.016 GB
% 140.95/18.55 % Net memory used: 997.447 MB
%------------------------------------------------------------------------------