%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP752-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 : n007.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 24.18s 3.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP752-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.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 20:35:51 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 24.18/3.55 % Refutation found
% 24.18/3.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 24.18/3.55 % SZS output start CNFRefutation for theBenchmark
% 24.18/3.55 fof(f1,axiom,(
% 24.18/3.55 (![A,B]: (mult(A,ld(A,B)) = B ))),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f2,axiom,(
% 24.18/3.55 (![A,B]: (ld(A,mult(A,B)) = B ))),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f5,axiom,(
% 24.18/3.55 (![A,B,C]: (mult(mult(A,mult(A,A)),mult(B,C)) = mult(mult(A,B),mult(mult(A,A),C)) ))),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f6,axiom,(
% 24.18/3.55 (![A,B,C]: (mult(mult(A,A),mult(B,C)) = mult(mult(A,B),mult(A,C)) ))),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f7,axiom,(
% 24.18/3.55 (![A,B,C]: (mult(mult(A,B),mult(C,C)) = mult(mult(A,C),mult(B,C)) ))),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f8,negated_conjecture,(
% 24.18/3.55 mult(mult(a,b),c) != mult(mult(a,c),mult(b,ld(c,c))) ),
% 24.18/3.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 24.18/3.55 fof(f9,plain,(
% 24.18/3.55 ![X0,X1]: (mult(X0,ld(X0,X1))=X1)),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f1])).
% 24.18/3.55 fof(f10,plain,(
% 24.18/3.55 ![X0,X1]: (ld(X0,mult(X0,X1))=X1)),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f2])).
% 24.18/3.55 fof(f13,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,mult(X0,X0)),mult(X1,X2))=mult(mult(X0,X1),mult(mult(X0,X0),X2)))),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f5])).
% 24.18/3.55 fof(f14,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,X2))=mult(mult(X0,X1),mult(X0,X2)))),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f6])).
% 24.18/3.55 fof(f15,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X1),mult(X2,X2))=mult(mult(X0,X2),mult(X1,X2)))),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f7])).
% 24.18/3.55 fof(f16,plain,(
% 24.18/3.55 ~mult(mult(a,b),c)=mult(mult(a,c),mult(b,ld(c,c)))),
% 24.18/3.55 inference(cnf_transformation,[status(thm)],[f8])).
% 24.18/3.55 fof(f30,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),X1)=mult(mult(X0,X2),mult(X0,ld(X2,X1))))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f9,f14])).
% 24.18/3.55 fof(f34,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),mult(ld(X0,X1),X2))=mult(X1,mult(X0,X2)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f9,f14])).
% 24.18/3.55 fof(f37,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,ld(X0,X2)))=mult(mult(X0,X1),X2))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f9,f14])).
% 24.18/3.55 fof(f46,plain,(
% 24.18/3.55 ![X0,X1,X2]: (ld(mult(X0,X0),mult(X1,mult(X0,X2)))=mult(ld(X0,X1),X2))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f34,f10])).
% 24.18/3.55 fof(f56,plain,(
% 24.18/3.55 ![X0,X1,X2]: (ld(mult(X0,X0),mult(X1,X2))=mult(ld(X0,X1),ld(X0,X2)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f9,f46])).
% 24.18/3.55 fof(f72,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,mult(X0,X0)),X1)=mult(mult(X0,X2),mult(mult(X0,X0),ld(X2,X1))))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f9,f13])).
% 24.18/3.55 fof(f109,plain,(
% 24.18/3.55 ![X0,X1,X2]: (ld(mult(X0,X0),mult(mult(X0,X1),X2))=mult(X1,ld(X0,X2)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f10,f56])).
% 24.18/3.55 fof(f297,plain,(
% 24.18/3.55 ![X0,X1,X2]: (ld(mult(X0,X1),mult(mult(X0,X0),X2))=mult(X0,ld(X1,X2)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f30,f10])).
% 24.18/3.55 fof(f317,plain,(
% 24.18/3.55 ![X0,X1,X2,X3]: (ld(mult(mult(X0,X0),X1),mult(mult(mult(X0,X2),mult(X0,X2)),X3))=mult(mult(X0,X2),ld(mult(X0,ld(X2,X1)),X3)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f30,f297])).
% 24.18/3.55 fof(f324,plain,(
% 24.18/3.55 ![X0,X1,X2,X3]: (ld(mult(X0,X1),mult(mult(X0,X2),X3))=mult(X0,ld(X1,mult(X2,ld(X0,X3)))))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f37,f297])).
% 24.18/3.55 fof(f417,plain,(
% 24.18/3.55 ![X0,X1,X2]: (ld(mult(X0,X0),mult(mult(X0,mult(X0,X0)),X1))=mult(X2,ld(X0,mult(mult(X0,X0),ld(X2,X1)))))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f72,f109])).
% 24.18/3.55 fof(f439,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,X1))=mult(X2,ld(X0,mult(mult(X0,X0),ld(X2,X1)))))),
% 24.18/3.55 inference(forward_demodulation,[status(thm)],[f109,f417])).
% 24.18/3.55 fof(f440,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,X1))=ld(mult(X2,X0),mult(mult(X2,mult(X0,X0)),X1)))),
% 24.18/3.55 inference(forward_demodulation,[status(thm)],[f324,f439])).
% 24.18/3.55 fof(f617,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,X1))=ld(mult(mult(X2,X2),X0),mult(mult(mult(X2,X0),mult(X2,X0)),X1)))),
% 24.18/3.55 inference(paramodulation,[status(thm)],[f14,f440])).
% 24.18/3.55 fof(f661,plain,(
% 24.18/3.55 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,X1))=mult(mult(X2,X0),ld(mult(X2,ld(X0,X0)),X1)))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f317,f617])).
% 24.23/3.59 fof(f686,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(X0,mult(X1,X1))=mult(mult(X2,X1),mult(ld(X2,X0),X1)))),
% 24.23/3.59 inference(paramodulation,[status(thm)],[f9,f15])).
% 24.23/3.59 fof(f1761,plain,(
% 24.23/3.59 ![X0,X1,X2]: (ld(mult(X0,X1),mult(X2,mult(X1,X1)))=mult(ld(X0,X2),X1))),
% 24.23/3.59 inference(paramodulation,[status(thm)],[f686,f10])).
% 24.23/3.59 fof(f3964,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,mult(X1,mult(ld(X0,X0),ld(X0,X0)))))=mult(mult(X2,X0),mult(ld(X2,X1),ld(X0,X0))))),
% 24.23/3.59 inference(paramodulation,[status(thm)],[f1761,f661])).
% 24.23/3.59 fof(f4044,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(mult(X0,X0),ld(X0,mult(X1,ld(mult(X0,X0),mult(X0,X0)))))=mult(mult(X2,X0),mult(ld(X2,X1),ld(X0,X0))))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f56,f3964])).
% 24.23/3.59 fof(f4045,plain,(
% 24.23/3.59 ![X0,X1,X2]: (ld(mult(mult(X0,X0),X0),mult(mult(mult(X0,X0),X1),mult(X0,X0)))=mult(mult(X2,X0),mult(ld(X2,X1),ld(X0,X0))))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f324,f4044])).
% 24.23/3.59 fof(f4046,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(ld(mult(X0,X0),mult(mult(X0,X0),X1)),X0)=mult(mult(X2,X0),mult(ld(X2,X1),ld(X0,X0))))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f1761,f4045])).
% 24.23/3.59 fof(f4047,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(mult(X0,ld(X0,X1)),X0)=mult(mult(X2,X0),mult(ld(X2,X1),ld(X0,X0))))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f297,f4046])).
% 24.23/3.59 fof(f4048,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(X0,X1)=mult(mult(X2,X1),mult(ld(X2,X0),ld(X1,X1))))),
% 24.23/3.59 inference(forward_demodulation,[status(thm)],[f9,f4047])).
% 24.23/3.59 fof(f4149,plain,(
% 24.23/3.59 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X2),mult(X1,ld(X2,X2))))),
% 24.23/3.59 inference(paramodulation,[status(thm)],[f10,f4048])).
% 24.23/3.59 fof(f4228,plain,(
% 24.23/3.59 ~mult(mult(a,b),c)=mult(mult(a,b),c)),
% 24.23/3.59 inference(backward_demodulation,[status(thm)],[f4149,f16])).
% 24.23/3.59 fof(f4357,plain,(
% 24.23/3.59 $false),
% 24.23/3.59 inference(trivial_equality_resolution,[status(thm)],[f4228])).
% 24.23/3.59 % SZS output end CNFRefutation for theBenchmark.p
% 10.36/3.63 % Elapsed time: 3.245027 seconds
% 10.36/3.63 % CPU time: 25.475777 seconds
% 10.36/3.63 % Total memory used: 259.269 MB
% 10.36/3.63 % Net memory used: 256.759 MB
%------------------------------------------------------------------------------