%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP122-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:35:40 PM UTC 2026
% Result : Unsatisfiable 17.62s 2.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP122-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 19:57:36 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 17.62/2.94 % Refutation found
% 17.62/2.94 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.62/2.94 % SZS output start CNFRefutation for theBenchmark
% 17.62/2.94 fof(f1,axiom,(
% 17.62/2.94 (![Y,X,Z]: (multiply(Y,multiply(multiply(Y,multiply(multiply(Y,Y),multiply(X,Z))),multiply(Z,multiply(Z,Z)))) = X ))),
% 17.62/2.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.62/2.94 fof(f2,axiom,(
% 17.62/2.94 multiply(identity,identity) = identity ),
% 17.62/2.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.62/2.94 fof(f3,negated_conjecture,(
% 17.62/2.94 multiply(multiply(a,b),c) != multiply(a,multiply(b,c)) ),
% 17.62/2.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.62/2.94 fof(f4,plain,(
% 17.62/2.94 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2))))=X1)),
% 17.62/2.94 inference(cnf_transformation,[status(thm)],[f1])).
% 17.62/2.94 fof(f5,plain,(
% 17.62/2.94 multiply(identity,identity)=identity),
% 17.62/2.94 inference(cnf_transformation,[status(thm)],[f2])).
% 17.62/2.94 fof(f6,plain,(
% 17.62/2.94 ~multiply(multiply(a,b),c)=multiply(a,multiply(b,c))),
% 17.62/2.94 inference(cnf_transformation,[status(thm)],[f3])).
% 17.62/2.95 fof(f12,plain,(
% 17.62/2.95 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2))))))=multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f4,f4])).
% 17.62/2.95 fof(f14,plain,(
% 17.62/2.95 ![X0]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(identity,identity))))=identity)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f5,f4])).
% 17.62/2.95 fof(f16,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),multiply(identity,identity)))=X1)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f5,f4])).
% 17.62/2.95 fof(f17,plain,(
% 17.62/2.95 ![X0]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,identity)))=identity)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 17.62/2.95 fof(f18,plain,(
% 17.62/2.95 ![X0]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))=identity)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f17])).
% 17.62/2.95 fof(f19,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f16])).
% 17.62/2.95 fof(f22,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))))=X1)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f18,f4])).
% 17.62/2.95 fof(f50,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))=multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f5,f12])).
% 17.62/2.95 fof(f77,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,multiply(identity,identity)),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity))=X1)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f12,f19])).
% 17.62/2.95 fof(f84,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))=multiply(identity,multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(identity,X0))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f50])).
% 17.62/2.95 fof(f85,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))=multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,X0))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f84])).
% 17.62/2.95 fof(f86,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))=multiply(identity,multiply(multiply(identity,identity),multiply(identity,X0))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f85])).
% 17.62/2.95 fof(f87,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))=multiply(identity,multiply(identity,multiply(identity,X0))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f86])).
% 17.62/2.95 fof(f133,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f77])).
% 17.62/2.95 fof(f134,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(identity,identity)))))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f133])).
% 17.62/2.95 fof(f135,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(multiply(identity,identity),multiply(identity,multiply(identity,identity)))))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f134])).
% 17.62/2.95 fof(f136,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f135])).
% 17.62/2.95 fof(f137,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,multiply(identity,identity))))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f136])).
% 17.62/2.95 fof(f138,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,multiply(identity,identity)))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f137])).
% 17.62/2.95 fof(f139,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),multiply(identity,identity))),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f138])).
% 17.62/2.95 fof(f140,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f139])).
% 17.62/2.95 fof(f141,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(multiply(identity,multiply(multiply(identity,X0),identity)),identity))=X0)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f5,f140])).
% 17.62/2.95 fof(f149,plain,(
% 17.62/2.95 ![X0]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity))=multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f18,f140])).
% 17.62/2.95 fof(f164,plain,(
% 17.62/2.95 ![X0]: (multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))=multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f149])).
% 17.62/2.95 fof(f173,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(X0,identity))=multiply(multiply(identity,X0),identity))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f141,f141])).
% 17.62/2.95 fof(f182,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))=multiply(multiply(identity,multiply(multiply(identity,identity),multiply(X0,X1))),multiply(X1,multiply(X1,X1))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f4,f141])).
% 17.62/2.95 fof(f205,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))=multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f182])).
% 17.62/2.95 fof(f217,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity)))=X0)),
% 17.62/2.95 inference(backward_demodulation,[status(thm)],[f173,f141])).
% 17.62/2.95 fof(f234,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)))=X0)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f217])).
% 17.62/2.95 fof(f235,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))=X0)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f234])).
% 17.62/2.95 fof(f713,plain,(
% 17.62/2.95 ![X0]: (multiply(multiply(X0,X0),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))=X0)),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f164,f140])).
% 17.62/2.95 fof(f1344,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f164,f22])).
% 17.62/2.95 fof(f1345,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f164,f1344])).
% 17.62/2.95 fof(f1346,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))=X1)),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f164,f1345])).
% 17.62/2.95 fof(f5124,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))=multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f205])).
% 17.62/2.95 fof(f5125,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity)))=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f235,f5124])).
% 17.62/2.95 fof(f5171,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity))))=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f5125])).
% 17.62/2.95 fof(f5172,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,multiply(identity,identity)))=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f5171])).
% 17.62/2.95 fof(f5173,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,identity))=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f5172])).
% 17.62/2.95 fof(f5174,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,identity)=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f5173])).
% 17.62/2.95 fof(f5175,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f5,f5174])).
% 17.62/2.95 fof(f5937,plain,(
% 17.62/2.95 ![X0]: (multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(identity,X0))),identity)),identity))=multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f87,f140])).
% 17.62/2.95 fof(f6015,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,multiply(identity,X0))=multiply(identity,multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f140,f5937])).
% 17.62/2.95 fof(f6151,plain,(
% 17.62/2.95 ![X0]: (multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,X0)),identity)),identity))=multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f6015,f140])).
% 17.62/2.95 fof(f6237,plain,(
% 17.62/2.95 ![X0]: (multiply(identity,X0)=multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f140,f6151])).
% 17.62/2.95 fof(f6245,plain,(
% 17.62/2.95 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2)))=multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))))),
% 17.62/2.95 inference(backward_demodulation,[status(thm)],[f6237,f12])).
% 17.62/2.95 fof(f6792,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))))))=multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f235,f6245])).
% 17.62/2.95 fof(f6855,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(X0,multiply(multiply(X0,identity),X1))=multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f235,f6792])).
% 17.62/2.95 fof(f7934,plain,(
% 17.62/2.95 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2)))=multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))))),
% 17.62/2.95 inference(backward_demodulation,[status(thm)],[f6855,f6245])).
% 17.62/2.95 fof(f8115,plain,(
% 17.62/2.95 ![X0,X1,X2]: (multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),identity)),identity))=multiply(multiply(X0,X1),multiply(identity,X2)))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f7934,f140])).
% 17.62/2.95 fof(f8264,plain,(
% 17.62/2.95 ![X0,X1,X2]: (multiply(multiply(X0,identity),multiply(X1,X2))=multiply(multiply(X0,X1),multiply(identity,X2)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f140,f8115])).
% 17.62/2.95 fof(f8385,plain,(
% 17.62/2.95 ![X0,X1]: (multiply(multiply(X0,identity),multiply(X1,identity))=multiply(multiply(X0,X1),identity))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f5,f8264])).
% 17.62/2.95 fof(f8857,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity))))),
% 17.62/2.95 inference(backward_demodulation,[status(thm)],[f8385,f5175])).
% 17.62/2.95 fof(f8937,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),identity)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f8385,f8857])).
% 17.62/2.95 fof(f8938,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,X0),identity)),identity)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f8385,f8937])).
% 17.62/2.95 fof(f8939,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f8385,f8938])).
% 17.62/2.95 fof(f9581,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(identity,X0),identity),identity)))),
% 17.62/2.95 inference(paramodulation,[status(thm)],[f6237,f8939])).
% 17.62/2.95 fof(f9623,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(identity,multiply(X0,identity)),identity)))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f9581])).
% 17.62/2.95 fof(f9624,plain,(
% 17.62/2.95 ![X0]: (identity=multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))))),
% 17.62/2.95 inference(forward_demodulation,[status(thm)],[f173,f9623])).
% 20.23/3.00 fof(f9996,plain,(
% 20.23/3.00 ![X0]: (identity=multiply(multiply(X0,identity),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))),
% 20.23/3.00 inference(paramodulation,[status(thm)],[f8264,f9624])).
% 20.23/3.00 fof(f10661,plain,(
% 20.23/3.00 ![X0,X1]: (multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))=multiply(X1,identity))),
% 20.23/3.00 inference(paramodulation,[status(thm)],[f9996,f4])).
% 20.23/3.00 fof(f10899,plain,(
% 20.23/3.00 ![X0]: (X0=multiply(X0,identity))),
% 20.23/3.00 inference(forward_demodulation,[status(thm)],[f1346,f10661])).
% 20.23/3.00 fof(f10909,plain,(
% 20.23/3.00 ![X0]: (multiply(multiply(X0,X0),multiply(multiply(X0,X0),multiply(X0,identity)))=X0)),
% 20.23/3.00 inference(backward_demodulation,[status(thm)],[f10899,f713])).
% 20.23/3.00 fof(f10911,plain,(
% 20.23/3.00 ![X0,X1]: (multiply(multiply(X0,X0),multiply(X0,multiply(multiply(X0,X1),identity)))=X1)),
% 20.23/3.00 inference(backward_demodulation,[status(thm)],[f10899,f140])).
% 20.23/3.00 fof(f10920,plain,(
% 20.23/3.00 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,X1),multiply(identity,X2)))=multiply(X0,multiply(X0,multiply(X1,X2))))),
% 20.23/3.00 inference(backward_demodulation,[status(thm)],[f10899,f7934])).
% 20.23/3.00 fof(f10961,plain,(
% 20.23/3.00 ![X0]: (multiply(multiply(X0,X0),multiply(multiply(X0,X0),X0))=X0)),
% 20.23/3.00 inference(forward_demodulation,[status(thm)],[f10899,f10909])).
% 20.23/3.00 fof(f10963,plain,(
% 20.23/3.00 ![X0,X1]: (multiply(multiply(X0,X0),multiply(X0,multiply(X0,X1)))=X1)),
% 20.23/3.00 inference(forward_demodulation,[status(thm)],[f10899,f10911])).
% 20.23/3.00 fof(f11466,plain,(
% 20.23/3.00 ![X0]: (multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X0)=X0)),
% 20.23/3.00 inference(paramodulation,[status(thm)],[f10961,f10963])).
% 20.23/3.00 fof(f11473,plain,(
% 20.23/3.00 ![X0]: (multiply(multiply(X0,X0),multiply(X0,X0))=identity)),
% 20.23/3.00 inference(paramodulation,[status(thm)],[f10899,f10963])).
% 20.23/3.00 fof(f12318,plain,(
% 20.23/3.00 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X0,X1),X2))=multiply(X0,multiply(X0,multiply(X1,X2))))),
% 20.23/3.00 inference(backward_demodulation,[status(thm)],[f12320,f10920])).
% 20.23/3.00 fof(f12320,plain,(
% 20.23/3.00 ![X0]: (multiply(identity,X0)=X0)),
% 20.23/3.00 inference(forward_demodulation,[status(thm)],[f11473,f11466])).
% 20.23/3.00 fof(f12635,plain,(
% 20.23/3.00 ![X0,X1,X2]: (multiply(multiply(X0,X0),multiply(X0,multiply(X0,multiply(X0,multiply(X1,X2)))))=multiply(multiply(X0,X1),X2))),
% 20.23/3.00 inference(paramodulation,[status(thm)],[f12318,f10963])).
% 20.23/3.00 fof(f12655,plain,(
% 20.23/3.00 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 20.23/3.00 inference(forward_demodulation,[status(thm)],[f10963,f12635])).
% 20.23/3.00 fof(f12896,plain,(
% 20.23/3.00 ~multiply(a,multiply(b,c))=multiply(a,multiply(b,c))),
% 20.23/3.00 inference(backward_demodulation,[status(thm)],[f12655,f6])).
% 20.23/3.00 fof(f12916,plain,(
% 20.23/3.00 $false),
% 20.23/3.00 inference(trivial_equality_resolution,[status(thm)],[f12896])).
% 20.23/3.00 % SZS output end CNFRefutation for theBenchmark.p
% 74.51/13.47 % Elapsed time: 12.894264 seconds
% 74.51/13.47 % CPU time: 33.227770 seconds
% 74.51/13.47 % Total memory used: 15.346 GB
% 74.51/13.47 % Net memory used: 15.341 GB
%------------------------------------------------------------------------------