%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP747+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:16 PM UTC 2026
% Result : Theorem 66.70s 9.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP747+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.46 % Computer : n026.cluster.edu
% 0.15/0.46 % Model : x86_64 x86_64
% 0.15/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.46 % Memory : 8046.5625MB
% 0.15/0.46 % OS : Linux 6.8.0-71-generic
% 0.15/0.47 % CPULimit : 300
% 0.15/0.47 % WCLimit : 300
% 0.15/0.47 % DateTime : Sun Sep 20 20:40:06 UTC 2026
% 0.15/0.47 % CPUTime :
% 0.15/0.49 % Drodi V4.1.1
% 66.70/9.31 % Refutation found
% 66.70/9.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.70/9.31 % SZS output start CNFRefutation for theBenchmark
% 66.70/9.31 fof(f6,axiom,(
% 66.70/9.31 (! [A] : mult(unit,A) = A )),
% 66.70/9.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.70/9.31 fof(f8,axiom,(
% 66.70/9.31 (! [X0,X1,X2] :( ( mult(mult(X0,X1),X2) = mult(X0,mult(X2,X1))& mult(mult(X0,X2),X1) = mult(X0,mult(X1,X2)) )| ( mult(mult(X0,X1),X2) = mult(mult(X0,X2),X1)& mult(X0,mult(X1,X2)) = mult(X0,mult(X2,X1)) ) ) )),
% 66.70/9.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.70/9.31 fof(f9,conjecture,(
% 66.70/9.31 mult(mult(a,b),c) = mult(a,mult(b,c)) ),
% 66.70/9.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.70/9.31 fof(f10,negated_conjecture,(
% 66.70/9.31 ~(mult(mult(a,b),c) = mult(a,mult(b,c)) )),
% 66.70/9.31 inference(negated_conjecture,[status(cth)],[f9])).
% 66.70/9.31 fof(f16,plain,(
% 66.70/9.31 ![X0]: (mult(unit,X0)=X0)),
% 66.70/9.31 inference(cnf_transformation,[status(thm)],[f6])).
% 66.70/9.31 fof(f18,definition,(
% 66.70/9.31 ![X0,X1,X2]: (sP0_prd(X2,X1,X0)<=>(mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))&mult(mult(X0,X2),X1)=mult(X0,mult(X1,X2))))),
% 66.70/9.31 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 66.70/9.31 fof(f19,plain,(
% 66.70/9.31 ![X0,X1,X2]: (sP0_prd(X2,X1,X0)|(mult(mult(X0,X1),X2)=mult(mult(X0,X2),X1)&mult(X0,mult(X1,X2))=mult(X0,mult(X2,X1))))),
% 66.70/9.31 inference(formula_renaming,[status(thm)],[f8,f18])).
% 66.70/9.31 fof(f20,plain,(
% 66.70/9.31 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|mult(mult(X2,X1),X0)=mult(mult(X2,X0),X1))),
% 66.70/9.31 inference(cnf_transformation,[status(thm)],[f19])).
% 66.70/9.31 fof(f21,plain,(
% 66.70/9.31 ![X0,X1,X2]: (sP0_prd(X0,X1,X2)|mult(X2,mult(X1,X0))=mult(X2,mult(X0,X1)))),
% 66.70/9.31 inference(cnf_transformation,[status(thm)],[f19])).
% 66.70/9.31 fof(f22,plain,(
% 66.70/9.31 ~mult(mult(a,b),c)=mult(a,mult(b,c))),
% 66.70/9.31 inference(cnf_transformation,[status(thm)],[f10])).
% 66.70/9.31 fof(f23,plain,(
% 66.70/9.31 ![X0,X1,X2]: ((~sP0_prd(X2,X1,X0)|(mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))&mult(mult(X0,X2),X1)=mult(X0,mult(X1,X2))))&(sP0_prd(X2,X1,X0)|(~mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))|~mult(mult(X0,X2),X1)=mult(X0,mult(X1,X2)))))),
% 66.70/9.31 inference(NNF_transformation,[status(thm)],[f18])).
% 66.70/9.31 fof(f24,plain,(
% 66.70/9.31 (![X0,X1,X2]: (~sP0_prd(X2,X1,X0)|(mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))&mult(mult(X0,X2),X1)=mult(X0,mult(X1,X2)))))&(![X0,X1,X2]: (sP0_prd(X2,X1,X0)|(~mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))|~mult(mult(X0,X2),X1)=mult(X0,mult(X1,X2)))))),
% 66.70/9.31 inference(miniscoping,[status(thm)],[f23])).
% 66.70/9.31 fof(f25,plain,(
% 66.70/9.31 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|mult(mult(X2,X1),X0)=mult(X2,mult(X0,X1)))),
% 66.70/9.31 inference(cnf_transformation,[status(thm)],[f24])).
% 66.70/9.31 fof(f976,plain,(
% 66.70/9.31 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))|mult(X0,mult(X1,X2))=mult(X0,mult(X2,X1)))),
% 66.70/9.31 inference(resolution,[status(thm)],[f25,f21])).
% 66.70/9.31 fof(f977,plain,(
% 66.70/9.31 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(X0,mult(X2,X1))|mult(mult(X0,X1),X2)=mult(mult(X0,X2),X1))),
% 66.70/9.31 inference(resolution,[status(thm)],[f25,f20])).
% 66.70/9.31 fof(f2736,plain,(
% 66.70/9.31 ![X0,X1]: (mult(X0,X1)=mult(unit,mult(X1,X0))|mult(unit,mult(X0,X1))=mult(unit,mult(X1,X0)))),
% 66.70/9.31 inference(paramodulation,[status(thm)],[f16,f976])).
% 66.70/9.31 fof(f2867,plain,(
% 66.70/9.31 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|mult(unit,mult(X0,X1))=mult(unit,mult(X1,X0)))),
% 66.70/9.31 inference(forward_demodulation,[status(thm)],[f16,f2736])).
% 66.70/9.31 fof(f2868,plain,(
% 66.70/9.31 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|mult(X0,X1)=mult(unit,mult(X1,X0)))),
% 66.70/9.31 inference(forward_demodulation,[status(thm)],[f16,f2867])).
% 66.70/9.31 fof(f2869,plain,(
% 66.70/9.31 ![X0,X1]: (mult(X0,X1)=mult(X1,X0)|mult(X0,X1)=mult(X1,X0))),
% 66.70/9.31 inference(forward_demodulation,[status(thm)],[f16,f2868])).
% 66.70/9.31 fof(f2870,plain,(
% 66.70/9.31 ![X0,X1]: (mult(X0,X1)=mult(X1,X0))),
% 66.70/9.31 inference(duplicate_literals_removal,[status(thm)],[f2869])).
% 66.70/9.31 fof(f3002,plain,(
% 66.70/9.31 ~mult(mult(a,c),b)=mult(a,mult(b,c))|mult(mult(a,b),c)=mult(a,mult(c,b))),
% 66.70/9.31 inference(paramodulation,[status(thm)],[f977,f22])).
% 66.70/9.31 fof(f5208,plain,(
% 66.70/9.31 ~mult(mult(b,a),c)=mult(a,mult(b,c))),
% 66.70/9.31 inference(paramodulation,[status(thm)],[f2870,f22])).
% 66.70/9.31 fof(f5219,plain,(
% 66.70/9.31 ~mult(c,mult(a,b))=mult(a,mult(b,c))),
% 66.70/9.31 inference(paramodulation,[status(thm)],[f2870,f22])).
% 66.70/9.31 fof(f6030,plain,(
% 66.70/9.31 ~mult(mult(b,c),a)=mult(a,mult(b,c))|mult(mult(b,c),a)=mult(b,mult(a,c))),
% 66.70/9.31 inference(paramodulation,[status(thm)],[f977,f5208])).
% 66.70/9.31 fof(f6035,plain,(
% 66.70/9.38 mult(mult(b,c),a)=mult(b,mult(a,c))),
% 66.70/9.38 inference(forward_subsumption_resolution,[status(thm)],[f6030,f2870])).
% 66.70/9.38 fof(f6037,plain,(
% 66.70/9.38 ~mult(c,mult(a,b))=mult(a,mult(c,b))),
% 66.70/9.38 inference(paramodulation,[status(thm)],[f2870,f5219])).
% 66.70/9.38 fof(f8198,plain,(
% 66.70/9.38 mult(a,mult(b,c))=mult(b,mult(a,c))),
% 66.70/9.38 inference(paramodulation,[status(thm)],[f2870,f6035])).
% 66.70/9.38 fof(f13342,plain,(
% 66.70/9.38 ~mult(mult(a,c),b)=mult(b,mult(a,c))|mult(mult(a,b),c)=mult(a,mult(c,b))),
% 66.70/9.38 inference(backward_demodulation,[status(thm)],[f8198,f3002])).
% 66.70/9.38 fof(f13366,plain,(
% 66.70/9.38 mult(mult(a,b),c)=mult(a,mult(c,b))),
% 66.70/9.38 inference(forward_subsumption_resolution,[status(thm)],[f13342,f2870])).
% 66.70/9.38 fof(f14820,plain,(
% 66.70/9.38 mult(c,mult(a,b))=mult(a,mult(c,b))),
% 66.70/9.38 inference(paramodulation,[status(thm)],[f2870,f13366])).
% 66.70/9.38 fof(f14858,plain,(
% 66.70/9.38 $false),
% 66.70/9.38 inference(forward_subsumption_resolution,[status(thm)],[f14820,f6037])).
% 66.70/9.38 % SZS output end CNFRefutation for theBenchmark.p
% 8.61/9.46 % Elapsed time: 8.966418 seconds
% 8.61/9.46 % CPU time: 70.140543 seconds
% 8.61/9.46 % Total memory used: 587.610 MB
% 8.61/9.46 % Net memory used: 580.805 MB
%------------------------------------------------------------------------------