%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP748+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 : n016.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 : Theorem 112.07s 14.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP748+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.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 20 20:42:06 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 112.07/14.78 % Refutation found
% 112.07/14.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 112.07/14.78 % SZS output start CNFRefutation for theBenchmark
% 112.07/14.78 fof(f1,axiom,(
% 112.07/14.78 (! [B,A] : mult(A,ld(A,B)) = B )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f2,axiom,(
% 112.07/14.78 (! [B,A] : ld(A,mult(A,B)) = B )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f3,axiom,(
% 112.07/14.78 (! [B,A] : mult(rd(A,B),B) = A )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f4,axiom,(
% 112.07/14.78 (! [B,A] : rd(mult(A,B),B) = A )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f5,axiom,(
% 112.07/14.78 (! [A] : mult(A,unit) = A )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f6,axiom,(
% 112.07/14.78 (! [A] : mult(unit,A) = A )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f7,axiom,(
% 112.07/14.78 (! [C,B,A] : mult(mult(mult(A,B),C),B) = mult(A,mult(mult(B,C),B)) )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f8,axiom,(
% 112.07/14.78 (! [B,A] : mult(mult(A,B),i(B)) = A )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f9,axiom,(
% 112.07/14.78 (! [A] : mult(A,i(A)) = unit )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f10,axiom,(
% 112.07/14.78 (! [A] : mult(i(A),A) = unit )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f11,axiom,(
% 112.07/14.78 (! [B,A] :( mult(A,B) = mult(B,A)| mult(i(A),mult(A,B)) = B ) )),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f12,conjecture,(
% 112.07/14.78 ( (! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1))| (! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5))| (! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8))| (! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11)) )) ),
% 112.07/14.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 112.07/14.78 fof(f13,negated_conjecture,(
% 112.07/14.78 ~(( (! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1))| (! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5))| (! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8))| (! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11)) )) )),
% 112.07/14.78 inference(negated_conjecture,[status(cth)],[f12])).
% 112.07/14.78 fof(f14,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f1])).
% 112.07/14.78 fof(f15,plain,(
% 112.07/14.78 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f2])).
% 112.07/14.78 fof(f16,plain,(
% 112.07/14.78 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f3])).
% 112.07/14.78 fof(f17,plain,(
% 112.07/14.78 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f4])).
% 112.07/14.78 fof(f18,plain,(
% 112.07/14.78 ![X0]: (mult(X0,unit)=X0)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f5])).
% 112.07/14.78 fof(f19,plain,(
% 112.07/14.78 ![X0]: (mult(unit,X0)=X0)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f6])).
% 112.07/14.78 fof(f20,plain,(
% 112.07/14.78 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X1)=mult(X0,mult(mult(X1,X2),X1)))),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f7])).
% 112.07/14.78 fof(f21,plain,(
% 112.07/14.78 ![X0,X1]: (mult(mult(X0,X1),i(X1))=X0)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f8])).
% 112.07/14.78 fof(f22,plain,(
% 112.07/14.78 ![X0]: (mult(X0,i(X0))=unit)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f9])).
% 112.07/14.78 fof(f23,plain,(
% 112.07/14.78 ![X0]: (mult(i(X0),X0)=unit)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f10])).
% 112.07/14.78 fof(f24,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|mult(i(X0),mult(X0,X1))=X1)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f11])).
% 112.07/14.78 fof(f25,plain,(
% 112.07/14.78 ((((?[X0,X1,X2]: ~mult(X2,mult(X0,mult(X2,X1)))=mult(mult(mult(X2,X0),X2),X1))&(?[X3,X4,X5]: ~mult(X3,mult(X5,mult(X4,X5)))=mult(mult(mult(X3,X5),X4),X5)))&(?[X6,X7,X8]: ~mult(mult(X8,X6),mult(X7,X8))=mult(mult(X8,mult(X6,X7)),X8)))&(?[X9,X10,X11]: ~mult(mult(X11,X9),mult(X10,X11))=mult(X11,mult(mult(X9,X10),X11))))),
% 112.07/14.78 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 112.07/14.78 fof(f26,plain,(
% 112.07/14.78 ((~mult(sK2_skl,mult(sK0_skl,mult(sK2_skl,sK1_skl)))=mult(mult(mult(sK2_skl,sK0_skl),sK2_skl),sK1_skl)&~mult(sK3_skl,mult(sK5_skl,mult(sK4_skl,sK5_skl)))=mult(mult(mult(sK3_skl,sK5_skl),sK4_skl),sK5_skl))&~mult(mult(sK8_skl,sK6_skl),mult(sK7_skl,sK8_skl))=mult(mult(sK8_skl,mult(sK6_skl,sK7_skl)),sK8_skl))&~mult(mult(sK11_skl,sK9_skl),mult(sK10_skl,sK11_skl))=mult(sK11_skl,mult(mult(sK9_skl,sK10_skl),sK11_skl))),
% 112.07/14.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl),skolemize(X3,sK3_skl),skolemize(X4,sK4_skl),skolemize(X5,sK5_skl),skolemize(X6,sK6_skl),skolemize(X7,sK7_skl),skolemize(X8,sK8_skl),skolemize(X9,sK9_skl),skolemize(X10,sK10_skl),skolemize(X11,sK11_skl)],[f25])).
% 112.07/14.78 fof(f28,plain,(
% 112.07/14.78 ~mult(sK3_skl,mult(sK5_skl,mult(sK4_skl,sK5_skl)))=mult(mult(mult(sK3_skl,sK5_skl),sK4_skl),sK5_skl)),
% 112.07/14.78 inference(cnf_transformation,[status(thm)],[f26])).
% 112.07/14.78 fof(f31,plain,(
% 112.07/14.78 ~mult(sK3_skl,mult(sK5_skl,mult(sK4_skl,sK5_skl)))=mult(sK3_skl,mult(mult(sK5_skl,sK4_skl),sK5_skl))),
% 112.07/14.78 inference(backward_demodulation,[status(thm)],[f20,f28])).
% 112.07/14.78 fof(f1065,plain,(
% 112.07/14.78 ![X0,X1]: (mult(mult(X0,X1),X1)=mult(X0,mult(mult(X1,unit),X1)))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f18,f20])).
% 112.07/14.78 fof(f1167,plain,(
% 112.07/14.78 ![X0,X1]: (mult(mult(X0,X1),X1)=mult(X0,mult(X1,X1)))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f18,f1065])).
% 112.07/14.78 fof(f1594,plain,(
% 112.07/14.78 ![X0,X1]: (mult(mult(unit,X0),X1)=mult(i(X1),mult(mult(X1,X0),X1)))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f23,f20])).
% 112.07/14.78 fof(f1688,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,X1)=mult(i(X1),mult(mult(X1,X0),X1)))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f19,f1594])).
% 112.07/14.78 fof(f1702,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,i(X1))=rd(X0,X1))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f16,f21])).
% 112.07/14.78 fof(f1858,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,ld(X0,X1))=mult(ld(X0,X1),X0)|mult(i(X0),X1)=ld(X0,X1))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f14,f24])).
% 112.07/14.78 fof(f1870,plain,(
% 112.07/14.78 ![X0,X1]: (ld(i(X0),X1)=mult(X0,X1)|mult(X0,X1)=mult(X1,X0))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f24,f15])).
% 112.07/14.78 fof(f1904,plain,(
% 112.07/14.78 ![X0,X1]: (X0=mult(ld(X1,X0),X1)|mult(i(X1),X0)=ld(X1,X0))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f14,f1858])).
% 112.07/14.78 fof(f1913,plain,(
% 112.07/14.78 ![X0]: (mult(unit,X0)=mult(i(X0),mult(X0,X0)))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f23,f1167])).
% 112.07/14.78 fof(f1928,plain,(
% 112.07/14.78 ![X0]: (mult(unit,i(X0))=mult(X0,mult(i(X0),i(X0))))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f22,f1167])).
% 112.07/14.78 fof(f1991,plain,(
% 112.07/14.78 ![X0]: (X0=mult(i(X0),mult(X0,X0)))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f19,f1913])).
% 112.07/14.78 fof(f1992,plain,(
% 112.07/14.78 ![X0]: (i(X0)=mult(X0,mult(i(X0),i(X0))))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f19,f1928])).
% 112.07/14.78 fof(f2055,plain,(
% 112.07/14.78 ![X0]: (mult(X0,i(mult(X0,X0)))=i(X0))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f1991,f21])).
% 112.07/14.78 fof(f2457,plain,(
% 112.07/14.78 ![X0]: (mult(i(X0),i(mult(i(X0),i(X0))))=X0)),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f1992,f21])).
% 112.07/14.78 fof(f2490,plain,(
% 112.07/14.78 ![X0]: (i(i(X0))=X0)),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f2055,f2457])).
% 112.07/14.78 fof(f4585,plain,(
% 112.07/14.78 ![X0,X1]: (ld(i(X0),mult(X1,X0))=mult(mult(X0,X1),X0))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f1688,f15])).
% 112.07/14.78 fof(f9231,plain,(
% 112.07/14.78 ![X0,X1]: (rd(X0,X1)=ld(X1,X0)|mult(i(X1),X0)=ld(X1,X0))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f1904,f17])).
% 112.07/14.78 fof(f12512,plain,(
% 112.07/14.78 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|mult(i(X0),X1)=mult(X1,i(X0)))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f2490,f1870])).
% 112.07/14.78 fof(f12543,plain,(
% 112.07/14.78 ![X0,X1]: (ld(X0,X1)=mult(i(X0),X1)|mult(i(X0),X1)=rd(X1,X0))),
% 112.07/14.78 inference(forward_demodulation,[status(thm)],[f1702,f12512])).
% 112.07/14.78 fof(f157420,plain,(
% 112.07/14.78 ![X0,X1]: (~rd(X0,X1)=ld(X1,X0)|mult(i(X1),X0)=ld(X1,X0))),
% 112.07/14.78 inference(equality_factoring,[status(thm)],[f12543])).
% 112.07/14.78 fof(f158833,plain,(
% 112.07/14.78 ![X0,X1]: (mult(i(X0),X1)=ld(X0,X1))),
% 112.07/14.78 inference(forward_subsumption_resolution,[status(thm)],[f157420,f9231])).
% 112.07/14.78 fof(f158921,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,X1)=ld(i(X0),X1))),
% 112.07/14.78 inference(paramodulation,[status(thm)],[f2490,f158833])).
% 112.07/14.78 fof(f163475,plain,(
% 112.07/14.78 ![X0,X1]: (mult(X0,mult(X1,X0))=mult(mult(X0,X1),X0))),
% 112.07/14.78 inference(backward_demodulation,[status(thm)],[f158921,f4585])).
% 112.07/14.90 fof(f179174,plain,(
% 112.07/14.90 ~mult(sK3_skl,mult(sK5_skl,mult(sK4_skl,sK5_skl)))=mult(sK3_skl,mult(sK5_skl,mult(sK4_skl,sK5_skl)))),
% 112.07/14.90 inference(backward_demodulation,[status(thm)],[f163475,f31])).
% 112.07/14.90 fof(f179333,plain,(
% 112.07/14.90 $false),
% 112.07/14.90 inference(trivial_equality_resolution,[status(thm)],[f179174])).
% 112.07/14.90 % SZS output end CNFRefutation for theBenchmark.p
% 21.25/15.01 % Elapsed time: 14.613034 seconds
% 21.25/15.01 % CPU time: 115.517278 seconds
% 21.25/15.01 % Total memory used: 1.465 GB
% 21.25/15.01 % Net memory used: 1.442 GB
%------------------------------------------------------------------------------