%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP435-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:36:37 PM UTC 2026
% Result : Unsatisfiable 34.51s 4.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP435-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.36 % Computer : n001.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Sun Sep 20 20:18:42 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.37 % Drodi V4.1.1
% 34.51/4.80 % Refutation found
% 34.51/4.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 34.51/4.80 % SZS output start CNFRefutation for theBenchmark
% 34.51/4.80 fof(f1,axiom,(
% 34.51/4.80 (![A,B,C,D]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(A,B),C)),A),B),multiply(D,inverse(D)))) = C ))),
% 34.51/4.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.51/4.80 fof(f2,negated_conjecture,(
% 34.51/4.80 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 34.51/4.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.51/4.80 fof(f3,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(X3,inverse(X3))))=X2)),
% 34.51/4.80 inference(cnf_transformation,[status(thm)],[f1])).
% 34.51/4.80 fof(f4,plain,(
% 34.51/4.80 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 34.51/4.80 inference(cnf_transformation,[status(thm)],[f2])).
% 34.51/4.80 fof(f10,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),multiply(X3,inverse(X3))))=multiply(X4,inverse(X4)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f3,f3])).
% 34.51/4.80 fof(f11,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(multiply(multiply(multiply(inverse(multiply(multiply(X3,X4),X5)),X3),X4),multiply(X6,inverse(X6))),X5)))=X2)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f3,f3])).
% 34.51/4.80 fof(f12,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f10,f10])).
% 34.51/4.80 fof(f25,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),multiply(X3,inverse(X3))))),X4),X5),multiply(X6,inverse(X6))))=inverse(multiply(X4,X5)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f10,f3])).
% 34.51/4.80 fof(f39,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(multiply(inverse(multiply(X0,inverse(X0))),X1),X2),multiply(X3,inverse(X3))))=inverse(multiply(X1,X2)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f12,f3])).
% 34.51/4.80 fof(f44,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,inverse(X0)),X1)),X2),inverse(X2)),multiply(X3,inverse(X3))))=X1)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f12,f3])).
% 34.51/4.80 fof(f82,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(X0,inverse(X0)))=inverse(multiply(X1,inverse(X1))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f39,f44])).
% 34.51/4.80 fof(f139,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),multiply(X6,inverse(X6))))),X7),X8),multiply(X9,inverse(X9))),inverse(multiply(X7,X8)))))=X2)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f10,f11])).
% 34.51/4.80 fof(f199,plain,(
% 34.51/4.80 ![X0,X1,X2]: (multiply(X0,inverse(X0))=multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f82,f12])).
% 34.51/4.80 fof(f241,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (multiply(X0,inverse(X0))=multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2)))),inverse(multiply(X3,inverse(X3)))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f199,f199])).
% 34.51/4.80 fof(f294,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(multiply(multiply(inverse(multiply(X0,inverse(X0))),multiply(inverse(multiply(X1,inverse(X1))),X2)),inverse(X2)),multiply(X3,inverse(X3))))=multiply(X4,inverse(X4)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f199,f10])).
% 34.51/4.80 fof(f314,plain,(
% 34.51/4.80 ![X0,X1,X2]: (inverse(multiply(multiply(inverse(multiply(X0,inverse(X0))),X1),inverse(X1)))=multiply(X2,inverse(X2)))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f39,f294])).
% 34.51/4.80 fof(f482,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,inverse(X1)))),X2),multiply(X3,inverse(X3))))=inverse(X2))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f314,f3])).
% 34.51/4.80 fof(f4296,plain,(
% 34.51/4.80 ![X0,X1,X2]: (inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(X2,inverse(X2))))=inverse(X1))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f241,f482])).
% 34.51/4.80 fof(f4538,plain,(
% 34.51/4.80 ![X0,X1]: (X0=inverse(inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),X0))))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f44,f4296])).
% 34.51/4.80 fof(f4745,plain,(
% 34.51/4.80 ![X0,X1,X2]: (multiply(X0,inverse(X0))=inverse(inverse(inverse(inverse(inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(X2))))))))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f482,f4538])).
% 34.51/4.80 fof(f4892,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(X0,inverse(X0))=inverse(inverse(multiply(X1,inverse(X1)))))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f4538,f4745])).
% 34.51/4.80 fof(f5122,plain,(
% 34.51/4.80 ![X0,X1,X2,X3]: (inverse(multiply(multiply(multiply(inverse(multiply(X0,inverse(X0))),multiply(X1,inverse(X1))),X2),multiply(X3,inverse(X3))))=inverse(X2))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f4892,f4296])).
% 34.51/4.80 fof(f5196,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(multiply(X0,inverse(X0)),X1))=inverse(X1))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f39,f5122])).
% 34.51/4.80 fof(f5200,plain,(
% 34.51/4.80 ![X0]: (X0=inverse(inverse(inverse(inverse(X0)))))),
% 34.51/4.80 inference(backward_demodulation,[status(thm)],[f5196,f4538])).
% 34.51/4.80 fof(f5848,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=inverse(inverse(inverse(inverse(X1)))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f5196,f5200])).
% 34.51/4.80 fof(f5920,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(multiply(X0,inverse(X0)),X1)=X1)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f5200,f5848])).
% 34.51/4.80 fof(f5931,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(X0,multiply(X1,inverse(X1))))=inverse(X0))),
% 34.51/4.80 inference(backward_demodulation,[status(thm)],[f5920,f4296])).
% 34.51/4.80 fof(f6769,plain,(
% 34.51/4.80 ![X0,X1,X2]: (inverse(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1))=X2)),
% 34.51/4.80 inference(backward_demodulation,[status(thm)],[f5931,f3])).
% 34.51/4.80 fof(f6811,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(X0,multiply(X1,inverse(X1)))=inverse(inverse(inverse(inverse(X0)))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f5931,f5200])).
% 34.51/4.80 fof(f6840,plain,(
% 34.51/4.80 ![X0,X1]: (multiply(X0,multiply(X1,inverse(X1)))=X0)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f5200,f6811])).
% 34.51/4.80 fof(f6914,plain,(
% 34.51/4.80 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(multiply(X0,multiply(X1,inverse(X1))),X2)),X0))=X2)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6840,f6769])).
% 34.51/4.80 fof(f6923,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(multiply(inverse(X0),X1),inverse(X1)))=X0)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f5920,f6769])).
% 34.51/4.80 fof(f6951,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),X0))=X1)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6840,f6914])).
% 34.51/4.80 fof(f6963,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(inverse(multiply(multiply(X0,inverse(X0)),X1)))=X1)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6840,f6951])).
% 34.51/4.80 fof(f6965,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(X0,inverse(multiply(X1,X0))))=X1)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6951,f6951])).
% 34.51/4.80 fof(f6991,plain,(
% 34.51/4.80 ![X0]: (inverse(inverse(X0))=X0)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f5920,f6963])).
% 34.51/4.80 fof(f6998,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(X0)=multiply(inverse(multiply(X1,X0)),X1))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6951,f6991])).
% 34.51/4.80 fof(f7397,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(X0)=multiply(X1,inverse(multiply(X0,X1))))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6965,f6991])).
% 34.51/4.80 fof(f8993,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(multiply(inverse(inverse(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),multiply(X3,inverse(X3))))),X4),X5))=inverse(multiply(X4,X5)))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6840,f25])).
% 34.51/4.80 fof(f8994,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5]: (inverse(multiply(multiply(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),multiply(X3,inverse(X3))),X4),X5))=inverse(multiply(X4,X5)))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6991,f8993])).
% 34.51/4.80 fof(f8995,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4]: (inverse(multiply(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),X3),X4))=inverse(multiply(X3,X4)))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6840,f8994])).
% 34.51/4.80 fof(f11195,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(inverse(X0),X1))=multiply(inverse(X1),X0))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6923,f7397])).
% 34.51/4.80 fof(f11196,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(inverse(X0))=multiply(X1,multiply(inverse(X1),X0)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6923,f6998])).
% 34.51/4.80 fof(f11280,plain,(
% 34.51/4.80 ![X0,X1]: (X0=multiply(X1,multiply(inverse(X1),X0)))),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6991,f11196])).
% 34.51/4.80 fof(f11289,plain,(
% 34.51/4.80 ![X0,X1]: (X0=multiply(multiply(X0,X1),inverse(X1)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6998,f11280])).
% 34.51/4.80 fof(f11298,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(X0,inverse(X1)))=multiply(X1,inverse(X0)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f7397,f11280])).
% 34.51/4.80 fof(f11305,plain,(
% 34.51/4.80 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6991,f11280])).
% 34.51/4.80 fof(f11393,plain,(
% 34.51/4.80 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f6998,f11289])).
% 34.51/4.80 fof(f14590,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(multiply(multiply(inverse(inverse(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),multiply(X6,inverse(X6))))),X7),X8),inverse(multiply(X7,X8)))))=X2)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6840,f139])).
% 34.51/4.80 fof(f14591,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(multiply(multiply(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),multiply(X6,inverse(X6))),X7),X8),inverse(multiply(X7,X8)))))=X2)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6991,f14590])).
% 34.51/4.80 fof(f14592,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(multiply(multiply(inverse(multiply(multiply(X0,X1),X2)),X0),X1),multiply(multiply(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),X6),X7),inverse(multiply(X6,X7)))))=X2)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f6840,f14591])).
% 34.51/4.80 fof(f25107,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(X1)),inverse(X0)),multiply(multiply(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),X6),X7),inverse(multiply(X6,X7)))))=X2)),
% 34.51/4.80 inference(paramodulation,[status(thm)],[f11393,f14592])).
% 34.51/4.80 fof(f25242,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(multiply(inverse(multiply(X0,multiply(inverse(multiply(X1,X0)),X2))),inverse(X1)),multiply(multiply(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),X6),X7),inverse(multiply(X6,X7)))))=X2)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f11393,f25107])).
% 34.51/4.80 fof(f25243,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(multiply(inverse(multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2)))),multiply(multiply(multiply(multiply(multiply(X3,multiply(inverse(multiply(multiply(X4,X5),X3)),X4)),X5),X6),X7),inverse(multiply(X6,X7)))))=X2)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f11393,f25242])).
% 34.51/4.80 fof(f25244,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(inverse(multiply(multiply(multiply(multiply(multiply(X0,multiply(inverse(multiply(multiply(X1,X2),X0)),X1)),X2),X3),X4),inverse(multiply(X3,X4)))),multiply(X5,multiply(X6,multiply(inverse(multiply(X5,X6)),X7))))=X7)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f11195,f25243])).
% 34.51/4.80 fof(f25245,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4,X5,X6,X7]: (multiply(multiply(multiply(X0,X1),inverse(multiply(multiply(multiply(multiply(X2,multiply(inverse(multiply(multiply(X3,X4),X2)),X3)),X4),X0),X1))),multiply(X5,multiply(X6,multiply(inverse(multiply(X5,X6)),X7))))=X7)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f11298,f25244])).
% 34.51/4.80 fof(f25246,plain,(
% 34.51/4.80 ![X0,X1,X2,X3,X4]: (multiply(multiply(multiply(X0,X1),inverse(multiply(X0,X1))),multiply(X2,multiply(X3,multiply(inverse(multiply(X2,X3)),X4))))=X4)),
% 34.51/4.80 inference(forward_demodulation,[status(thm)],[f8995,f25245])).
% 35.01/4.85 fof(f25247,plain,(
% 35.01/4.85 ![X0,X1,X2]: (multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2)))=X2)),
% 35.01/4.85 inference(forward_demodulation,[status(thm)],[f5920,f25246])).
% 35.01/4.85 fof(f31500,plain,(
% 35.01/4.85 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 35.01/4.85 inference(paramodulation,[status(thm)],[f11305,f25247])).
% 35.01/4.85 fof(f31852,plain,(
% 35.01/4.85 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 35.01/4.85 inference(backward_demodulation,[status(thm)],[f31500,f4])).
% 35.01/4.85 fof(f32097,plain,(
% 35.01/4.85 $false),
% 35.01/4.85 inference(trivial_equality_resolution,[status(thm)],[f31852])).
% 35.01/4.85 % SZS output end CNFRefutation for theBenchmark.p
% 29.16/6.05 % Elapsed time: 5.458155 seconds
% 29.16/6.05 % CPU time: 16.572506 seconds
% 29.16/6.05 % Total memory used: 94.287 MB
% 29.16/6.05 % Net memory used: 91.422 MB
%------------------------------------------------------------------------------