%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP748-3 : 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 : n012.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:16 PM UTC 2026
% Result : Unsatisfiable 151.23s 24.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP748-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/5.32 % Computer : n012.cluster.edu
% 0.04/5.32 % Model : x86_64 x86_64
% 0.04/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.32 % Memory : 8046.5625MB
% 0.04/5.32 % OS : Linux 6.8.0-71-generic
% 0.04/5.32 % CPULimit : 300
% 0.04/5.32 % WCLimit : 300
% 0.04/5.32 % DateTime : Sun Sep 20 20:36:58 UTC 2026
% 0.04/5.32 % CPUTime :
% 0.04/5.33 % Drodi V4.1.1
% 151.23/24.41 % Refutation found
% 151.23/24.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 151.23/24.41 % SZS output start CNFRefutation for theBenchmark
% 151.23/24.41 fof(f1,axiom,(
% 151.23/24.41 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f2,axiom,(
% 151.23/24.41 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f3,axiom,(
% 151.23/24.41 (![A,B]: (mult(rd(A,B),B) = A ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f4,axiom,(
% 151.23/24.41 (![A,B]: (rd(mult(A,B),B) = A ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f5,axiom,(
% 151.23/24.41 (![A]: (mult(A,unit) = A ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f6,axiom,(
% 151.23/24.41 (![A]: (mult(unit,A) = A ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f7,axiom,(
% 151.23/24.41 (![A,B,C]: (mult(mult(mult(A,B),C),B) = mult(A,mult(mult(B,C),B)) ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f8,axiom,(
% 151.23/24.41 (![A,B]: (mult(mult(A,B),i(B)) = A ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f9,axiom,(
% 151.23/24.41 (![A]: (mult(A,i(A)) = unit ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f10,axiom,(
% 151.23/24.41 (![A]: (mult(i(A),A) = unit ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f11,axiom,(
% 151.23/24.41 (![A,B]: (( mult(A,B) = mult(B,A)| mult(i(A),mult(A,B)) = B ) ))),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f12,negated_conjecture,(
% 151.23/24.41 mult(a,mult(b,mult(c,b))) != mult(mult(mult(a,b),c),b) ),
% 151.23/24.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 151.23/24.41 fof(f13,plain,(
% 151.23/24.41 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f1])).
% 151.23/24.41 fof(f14,plain,(
% 151.23/24.41 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f2])).
% 151.23/24.41 fof(f15,plain,(
% 151.23/24.41 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f3])).
% 151.23/24.41 fof(f16,plain,(
% 151.23/24.41 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f4])).
% 151.23/24.41 fof(f17,plain,(
% 151.23/24.41 ![X0]: (mult(X0,unit)=X0)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f5])).
% 151.23/24.41 fof(f18,plain,(
% 151.23/24.41 ![X0]: (mult(unit,X0)=X0)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f6])).
% 151.23/24.41 fof(f19,plain,(
% 151.23/24.41 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(X0,mult(mult(X1,X2),X1)))),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f7])).
% 151.23/24.41 fof(f20,plain,(
% 151.23/24.41 ![X0,X1]: (mult(mult(X0,X1),i(X1))=X0)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f8])).
% 151.23/24.41 fof(f21,plain,(
% 151.23/24.41 ![X0]: (mult(X0,i(X0))=unit)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f9])).
% 151.23/24.41 fof(f22,plain,(
% 151.23/24.41 ![X0]: (mult(i(X0),X0)=unit)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f10])).
% 151.23/24.41 fof(f23,plain,(
% 151.23/24.41 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|mult(i(X0),mult(X0,X1))=X1)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f11])).
% 151.23/24.41 fof(f24,plain,(
% 151.23/24.41 ~mult(a,mult(b,mult(c,b)))=mult(mult(mult(a,b),c),b)),
% 151.23/24.41 inference(cnf_transformation,[status(thm)],[f12])).
% 151.23/24.41 fof(f25,plain,(
% 151.23/24.41 ~mult(a,mult(b,mult(c,b)))=mult(a,mult(mult(b,c),b))),
% 151.23/24.41 inference(backward_demodulation,[status(thm)],[f19,f24])).
% 151.23/24.41 fof(f1619,plain,(
% 151.23/24.41 ![X0,X1]: (mult(mult(X0,X1),X1)=mult(X0,mult(mult(X1,unit),X1)))),
% 151.23/24.41 inference(paramodulation,[status(thm)],[f17,f19])).
% 151.23/24.41 fof(f1747,plain,(
% 151.23/24.41 ![X0,X1]: (mult(mult(X0,X1),X1)=mult(X0,mult(X1,X1)))),
% 151.23/24.41 inference(forward_demodulation,[status(thm)],[f17,f1619])).
% 151.23/24.41 fof(f2300,plain,(
% 151.23/24.41 ![X0,X1]: (mult(mult(unit,X0),X1)=mult(i(X1),mult(mult(X1,X0),X1)))),
% 151.23/24.41 inference(paramodulation,[status(thm)],[f22,f19])).
% 151.23/24.41 fof(f2436,plain,(
% 151.23/24.41 ![X0,X1]: (mult(X0,X1)=mult(i(X1),mult(mult(X1,X0),X1)))),
% 151.23/24.41 inference(forward_demodulation,[status(thm)],[f18,f2300])).
% 151.23/24.41 fof(f2451,plain,(
% 151.23/24.41 ![X0,X1]: (mult(X0,i(X1))=rd(X0,X1))),
% 151.23/24.41 inference(paramodulation,[status(thm)],[f15,f20])).
% 151.23/24.41 fof(f2654,plain,(
% 151.23/24.41 ![X0,X1]: (mult(X0,ld(X0,X1))=mult(ld(X0,X1),X0)|mult(i(X0),X1)=ld(X0,X1))),
% 151.23/24.41 inference(paramodulation,[status(thm)],[f13,f23])).
% 151.23/24.41 fof(f2668,plain,(
% 151.23/24.41 ![X0,X1]: (ld(i(X0),X1)=mult(X0,X1)|mult(X0,X1)=mult(X1,X0))),
% 151.23/24.41 inference(paramodulation,[status(thm)],[f23,f14])).
% 151.23/24.41 fof(f2709,plain,(
% 151.23/24.41 ![X0,X1]: (X0=mult(ld(X1,X0),X1)|mult(i(X1),X0)=ld(X1,X0))),
% 119.16/24.60 inference(forward_demodulation,[status(thm)],[f13,f2654])).
% 119.16/24.60 fof(f2721,plain,(
% 119.16/24.60 ![X0]: (mult(unit,X0)=mult(i(X0),mult(X0,X0)))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f22,f1747])).
% 119.16/24.60 fof(f2738,plain,(
% 119.16/24.60 ![X0]: (mult(unit,i(X0))=mult(X0,mult(i(X0),i(X0))))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f21,f1747])).
% 119.16/24.60 fof(f2814,plain,(
% 119.16/24.60 ![X0]: (X0=mult(i(X0),mult(X0,X0)))),
% 119.16/24.60 inference(forward_demodulation,[status(thm)],[f18,f2721])).
% 119.16/24.60 fof(f2815,plain,(
% 119.16/24.60 ![X0]: (i(X0)=mult(X0,mult(i(X0),i(X0))))),
% 119.16/24.60 inference(forward_demodulation,[status(thm)],[f18,f2738])).
% 119.16/24.60 fof(f2891,plain,(
% 119.16/24.60 ![X0]: (mult(X0,i(mult(X0,X0)))=i(X0))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f2814,f20])).
% 119.16/24.60 fof(f3383,plain,(
% 119.16/24.60 ![X0]: (mult(i(X0),i(mult(i(X0),i(X0))))=X0)),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f2815,f20])).
% 119.16/24.60 fof(f3421,plain,(
% 119.16/24.60 ![X0]: (i(i(X0))=X0)),
% 119.16/24.60 inference(forward_demodulation,[status(thm)],[f2891,f3383])).
% 119.16/24.60 fof(f5856,plain,(
% 119.16/24.60 ![X0,X1]: (ld(i(X0),mult(X1,X0))=mult(mult(X0,X1),X0))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f2436,f14])).
% 119.16/24.60 fof(f10767,plain,(
% 119.16/24.60 ![X0,X1]: (rd(X0,X1)=ld(X1,X0)|mult(i(X1),X0)=ld(X1,X0))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f2709,f16])).
% 119.16/24.60 fof(f15307,plain,(
% 119.16/24.60 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|mult(i(X0),X1)=mult(X1,i(X0)))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f3421,f2668])).
% 119.16/24.60 fof(f15338,plain,(
% 119.16/24.60 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|mult(i(X0),X1)=rd(X1,X0))),
% 119.16/24.60 inference(forward_demodulation,[status(thm)],[f2451,f15307])).
% 119.16/24.60 fof(f160232,plain,(
% 119.16/24.60 ![X0,X1]: (~rd(X0,X1)=ld(X1,X0)|mult(i(X1),X0)=ld(X1,X0))),
% 119.16/24.60 inference(equality_factoring,[status(thm)],[f15338])).
% 119.16/24.60 fof(f161550,plain,(
% 119.16/24.60 ![X0,X1]: (mult(i(X0),X1)=ld(X0,X1))),
% 119.16/24.60 inference(forward_subsumption_resolution,[status(thm)],[f160232,f10767])).
% 119.16/24.60 fof(f161629,plain,(
% 119.16/24.60 ![X0,X1]: (mult(X0,X1)=ld(i(X0),X1))),
% 119.16/24.60 inference(paramodulation,[status(thm)],[f3421,f161550])).
% 119.16/24.60 fof(f163394,plain,(
% 119.16/24.60 ![X0,X1]: (mult(X0,mult(X1,X0))=mult(mult(X0,X1),X0))),
% 119.16/24.60 inference(backward_demodulation,[status(thm)],[f161629,f5856])).
% 119.16/24.60 fof(f175906,plain,(
% 119.16/24.60 ~mult(a,mult(b,mult(c,b)))=mult(a,mult(b,mult(c,b)))),
% 119.16/24.60 inference(backward_demodulation,[status(thm)],[f163394,f25])).
% 119.16/24.60 fof(f176032,plain,(
% 119.16/24.60 $false),
% 119.16/24.60 inference(trivial_equality_resolution,[status(thm)],[f175906])).
% 119.16/24.60 % SZS output end CNFRefutation for theBenchmark.p
% 5.15/24.76 % Elapsed time: 19.429060 seconds
% 5.15/24.76 % CPU time: 153.083753 seconds
% 5.15/24.76 % Total memory used: 2.458 GB
% 5.15/24.76 % Net memory used: 2.420 GB
%------------------------------------------------------------------------------