%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG240-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 11:49:55 AM UTC 2026
% Result : Unsatisfiable 5.06s 1.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG240-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.18/0.45 % Computer : n007.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 13:07:50 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 5.06/1.16 % Refutation found
% 5.06/1.16 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.06/1.16 % SZS output start CNFRefutation for theBenchmark
% 5.06/1.16 fof(f1,axiom,(
% 5.06/1.16 (![A,B,C]: (mult(A,mult(B,C)) = mult(mult(A,B),mult(A,C)) ))),
% 5.06/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.06/1.16 fof(f2,axiom,(
% 5.06/1.16 (![A,B,C]: (mult(mult(A,B),C) = mult(mult(A,C),mult(B,C)) ))),
% 5.06/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.06/1.16 fof(f3,axiom,(
% 5.06/1.16 (![A,B,C,D]: (mult(mult(mult(A,B),mult(C,D)),mult(mult(mult(A,B),mult(C,D)),mult(mult(A,C),mult(B,D)))) = mult(mult(A,C),mult(B,D)) ))),
% 5.06/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.06/1.16 fof(f4,axiom,(
% 5.06/1.16 (![A,B,C,D]: (mult(mult(mult(mult(A,B),mult(C,D)),mult(mult(A,C),mult(B,D))),mult(mult(A,C),mult(B,D))) = mult(mult(A,B),mult(C,D)) ))),
% 5.06/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.06/1.16 fof(f5,negated_conjecture,(
% 5.06/1.16 mult(mult(mult(a,b),mult(c,d)),mult(mult(a,c),mult(b,d))) != mult(mult(mult(a,c),mult(b,d)),mult(mult(a,b),mult(c,d))) ),
% 5.06/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.06/1.16 fof(f6,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(cnf_transformation,[status(thm)],[f1])).
% 5.06/1.16 fof(f7,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(cnf_transformation,[status(thm)],[f2])).
% 5.06/1.16 fof(f8,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))))=mult(mult(X0,X2),mult(X1,X3)))),
% 5.06/1.16 inference(cnf_transformation,[status(thm)],[f3])).
% 5.06/1.16 fof(f9,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(X0,X1),mult(X2,X3)))),
% 5.06/1.16 inference(cnf_transformation,[status(thm)],[f4])).
% 5.06/1.16 fof(f10,plain,(
% 5.06/1.16 ~mult(mult(mult(a,b),mult(c,d)),mult(mult(a,c),mult(b,d)))=mult(mult(mult(a,c),mult(b,d)),mult(mult(a,b),mult(c,d)))),
% 5.06/1.16 inference(cnf_transformation,[status(thm)],[f5])).
% 5.06/1.16 fof(f23,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(X0,X1),mult(X2,mult(X0,X3)))=mult(mult(mult(X0,X1),X2),mult(X0,mult(X1,X3))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f6,f6])).
% 5.06/1.16 fof(f24,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(X0,X0),X1)=mult(X0,mult(X1,X1)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f6,f7])).
% 5.06/1.16 fof(f25,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),X2),mult(X3,X1))=mult(mult(mult(X0,X3),X1),mult(X2,mult(X3,X1))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f7])).
% 5.06/1.16 fof(f26,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),X2),mult(X0,X3))=mult(mult(X0,mult(X1,X3)),mult(X2,mult(X0,X3))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f6,f7])).
% 5.06/1.16 fof(f33,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X0,X0)),X1)=mult(X0,mult(mult(X1,X1),mult(X1,X1))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f24,f24])).
% 5.06/1.16 fof(f34,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),X1),X2)=mult(mult(X0,X1),mult(X2,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f24])).
% 5.06/1.16 fof(f48,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X0),X1)=mult(X0,mult(mult(X1,X1),mult(X1,X1))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f33])).
% 5.06/1.16 fof(f49,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X0),X1)=mult(X0,mult(mult(X1,X1),X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f48])).
% 5.06/1.16 fof(f56,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X0),X1),mult(X0,X1)),X2)=mult(mult(X0,X1),mult(mult(X2,X2),X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f49])).
% 5.06/1.16 fof(f63,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),X0),mult(X1,X2))=mult(X0,mult(mult(X1,mult(X2,X2)),mult(X1,X2))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f6,f49])).
% 5.06/1.16 fof(f71,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X2,X2),X2))=mult(mult(mult(mult(X0,X0),X0),X2),mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f49,f7])).
% 5.06/1.16 fof(f86,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X0),X0),X1),X2)=mult(mult(X0,X1),mult(mult(X2,X2),X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f56])).
% 5.06/1.16 fof(f101,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),X0),mult(X1,X2))=mult(X0,mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f63])).
% 5.06/1.16 fof(f129,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X1),X1)=mult(mult(X0,X1),X1))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f34])).
% 5.06/1.16 fof(f150,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X0),X1),mult(X2,X3))=mult(mult(mult(X0,X1),mult(X2,X2)),mult(mult(mult(X0,X0),X1),X3)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f34,f6])).
% 5.06/1.16 fof(f230,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(X0,mult(X1,X1)),X1)=mult(mult(X0,X1),X1))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f24,f129])).
% 5.06/1.16 fof(f243,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(mult(X0,X0),X1),mult(mult(X0,X0),X1)),X1),X2)=mult(mult(mult(X0,X1),X1),mult(X2,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f129,f34])).
% 5.06/1.16 fof(f293,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(mult(X0,X0),mult(X0,X0)),X1),X1),X2)=mult(mult(mult(X0,X1),X1),mult(X2,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f243])).
% 5.06/1.16 fof(f294,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X0),X1),X1),X2)=mult(mult(mult(X0,X1),X1),mult(X2,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f129,f293])).
% 5.06/1.16 fof(f297,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X1),X2)=mult(mult(mult(X0,X1),X1),mult(X2,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f129,f294])).
% 5.06/1.16 fof(f312,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X2),mult(X1,X2))),mult(mult(mult(X0,X0),mult(X1,X2)),mult(mult(X0,X1),mult(X0,X2))))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f24,f8])).
% 5.06/1.16 fof(f335,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X1,X1)),mult(mult(mult(mult(X0,X0),mult(X0,X0)),mult(X1,X1)),mult(X0,X1)))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f34,f8])).
% 5.06/1.16 fof(f373,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X1),mult(X2,X2)),mult(mult(mult(X0,X1),mult(X2,X2)),mult(mult(X0,X1),X2)))=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f8])).
% 5.06/1.16 fof(f374,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),mult(X1,X2)),mult(mult(mult(X0,X0),mult(X1,X2)),mult(X0,mult(X1,X2))))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f6,f8])).
% 5.06/1.16 fof(f402,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(mult(X1,X2),mult(X3,X4))),mult(mult(mult(X1,X2),mult(X3,X4)),mult(mult(X1,X3),mult(X2,X4))))=mult(mult(X0,mult(mult(mult(X1,X2),mult(X3,X4)),mult(mult(X1,X3),mult(X2,X4)))),mult(mult(X1,X3),mult(X2,X4))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f8,f7])).
% 5.06/1.16 fof(f405,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),X4))=mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),X4)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f8,f6])).
% 5.06/1.16 fof(f423,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(mult(mult(X0,X0),mult(X1,X2)),mult(mult(X0,X1),mult(X0,X2))))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f312])).
% 5.06/1.16 fof(f424,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(mult(mult(X0,X0),mult(X1,X2)),mult(X0,mult(X1,X2))))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f423])).
% 5.06/1.16 fof(f425,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(mult(mult(X0,X0),X0),mult(X1,X2)))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f424])).
% 5.06/1.16 fof(f426,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(mult(mult(X0,X0),X0),mult(X1,X2)))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f425])).
% 5.06/1.16 fof(f441,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X1,X1)),mult(mult(mult(mult(X0,X0),X0),mult(X1,X1)),mult(X0,X1)))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f335])).
% 5.06/1.16 fof(f442,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X1,X1)),mult(mult(mult(mult(X0,X0),X0),X1),mult(X0,X1)))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f297,f441])).
% 5.06/1.16 fof(f443,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X1,X1)),mult(mult(mult(mult(X0,X0),X0),X0),X1))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f442])).
% 5.06/1.16 fof(f444,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),mult(X1,X1)),mult(mult(mult(X0,X0),X0),X1))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f129,f443])).
% 5.06/1.16 fof(f445,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X0),mult(X1,X1))=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f150,f444])).
% 5.06/1.16 fof(f446,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X0),X1)=mult(mult(X0,X1),mult(X0,X1)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f297,f445])).
% 5.06/1.16 fof(f447,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(mult(X0,X0),mult(X1,X2)))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(backward_demodulation,[status(thm)],[f470,f426])).
% 5.06/1.16 fof(f451,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,X2))=mult(X0,mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(backward_demodulation,[status(thm)],[f470,f101])).
% 5.06/1.16 fof(f466,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X2,X2),X2))=mult(mult(mult(X0,X0),X2),mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(backward_demodulation,[status(thm)],[f470,f71])).
% 5.06/1.16 fof(f469,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),X1),X2)=mult(mult(X0,X1),mult(mult(X2,X2),X2)))),
% 5.06/1.16 inference(backward_demodulation,[status(thm)],[f470,f86])).
% 5.06/1.16 fof(f470,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(mult(X0,X0),X0),X1)=mult(mult(X0,X0),X1))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f446])).
% 5.06/1.16 fof(f543,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(mult(X0,X1),X2),mult(mult(X0,X1),mult(X2,X2))),mult(mult(X0,X1),X2))=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f26,f373])).
% 5.06/1.16 fof(f544,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X1),mult(X2,mult(X2,X2))),mult(mult(X0,X1),X2))=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f543])).
% 5.06/1.16 fof(f545,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X2,mult(X2,X2)),X2))=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f544])).
% 5.06/1.16 fof(f546,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X2,X2),X2))=mult(mult(X0,X2),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f230,f545])).
% 5.06/1.16 fof(f551,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X2,X2),X2))=mult(mult(X0,X1),X2))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f546])).
% 5.06/1.16 fof(f552,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,mult(X1,X2)),mult(mult(X0,X0),mult(X1,X2))),mult(X0,mult(X1,X2)))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f25,f374])).
% 5.06/1.16 fof(f553,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,mult(X0,X0)),mult(X1,X2)),mult(X0,mult(X1,X2)))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f552])).
% 5.06/1.16 fof(f554,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,mult(X0,X0)),X0),mult(X1,X2))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f553])).
% 5.06/1.16 fof(f555,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X0),X0),mult(X1,X2))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f230,f554])).
% 5.06/1.16 fof(f556,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,X2))=mult(mult(X0,X1),mult(X0,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f470,f555])).
% 5.06/1.16 fof(f566,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X0),mult(X1,X2))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f556])).
% 5.06/1.16 fof(f643,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,mult(mult(X1,X1),X2)),mult(X0,mult(X1,X2)))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f566,f447])).
% 5.06/1.16 fof(f644,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(mult(mult(X1,X1),X2),mult(X1,X2)))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f643])).
% 5.06/1.16 fof(f645,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(mult(mult(X1,X1),X1),X2))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f644])).
% 5.06/1.16 fof(f682,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(mult(X1,X1),X2))=mult(X0,mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f470,f645])).
% 5.06/1.16 fof(f698,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(X0,mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f566,f451])).
% 5.06/1.16 fof(f712,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(X0,mult(X1,X2))=mult(X0,mult(X1,mult(X2,X2))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f682,f698])).
% 5.06/1.16 fof(f786,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(mult(X0,X0),X2),mult(X1,mult(mult(X2,X2),X2))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f551,f466])).
% 5.06/1.16 fof(f787,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(mult(X0,X0),X2),mult(X1,mult(X2,X2))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f682,f786])).
% 5.06/1.16 fof(f788,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(mult(X0,X0),X2),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f712,f787])).
% 5.06/1.16 fof(f797,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(mult(X0,X0),X1),X2))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f788])).
% 5.06/1.16 fof(f804,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X1),mult(mult(X2,X2),X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f797,f469])).
% 5.06/1.16 fof(f809,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),X2)=mult(mult(X0,X1),mult(X2,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f682,f804])).
% 5.06/1.16 fof(f1006,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(X0,X1),X0)=mult(X0,mult(X1,X0)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f566])).
% 5.06/1.16 fof(f1138,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X2),X0)=mult(mult(X0,mult(X1,X0)),mult(X2,X0)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f1006,f7])).
% 5.06/1.16 fof(f1976,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(mult(mult(X1,X2),mult(X3,X4)),mult(mult(X1,X3),mult(X2,X4)))),mult(mult(X1,X3),mult(X2,X4)))=mult(mult(X0,mult(mult(X1,X3),mult(X2,X4))),mult(mult(X1,X2),mult(X3,X4))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f9,f7])).
% 5.06/1.16 fof(f1977,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),X4),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(X0,X1),mult(X2,X3)),mult(X4,mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f9,f7])).
% 5.06/1.16 fof(f1979,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(mult(X0,X2),mult(X1,X3)),X4))=mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),X4)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f9,f6])).
% 5.06/1.16 fof(f2378,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(X0,mult(mult(X1,X2),mult(X3,X4))),mult(mult(mult(X1,X2),mult(X3,X4)),mult(mult(X1,X3),mult(X2,X4))))=mult(mult(X0,mult(mult(X1,X3),mult(X2,X4))),mult(mult(X1,X2),mult(X3,X4))))),
% 5.06/1.16 inference(backward_demodulation,[status(thm)],[f1976,f402])).
% 5.06/1.16 fof(f2380,plain,(
% 5.06/1.16 ![X0,X1,X2,X3,X4]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(mult(X0,X2),mult(X1,X3)),X4))=mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),X4)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f405,f1979])).
% 5.06/1.16 fof(f3779,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X1,X2),mult(X0,X2)))=mult(mult(mult(X0,X1),X0),mult(X1,X2)))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f7,f23])).
% 5.06/1.16 fof(f3923,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X1,X0),X2))=mult(mult(mult(X0,X1),X0),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f7,f3779])).
% 5.06/1.16 fof(f3924,plain,(
% 5.06/1.16 ![X0,X1,X2]: (mult(mult(X0,X1),mult(mult(X1,X0),X2))=mult(mult(X0,mult(X1,X0)),mult(X1,X2)))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f1006,f3923])).
% 5.06/1.16 fof(f4118,plain,(
% 5.06/1.16 ![X0,X1]: (mult(mult(X0,X1),mult(mult(X1,X0),X0))=mult(mult(mult(X0,X1),X1),X0))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f1138,f3924])).
% 5.06/1.16 fof(f4489,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(paramodulation,[status(thm)],[f8,f4118])).
% 5.06/1.16 fof(f4738,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X1),mult(X2,X3)))),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f1006,f4489])).
% 5.06/1.16 fof(f4739,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f3924,f4738])).
% 5.06/1.16 fof(f4740,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X2),mult(X1,X3)))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f2380,f4739])).
% 5.06/1.16 fof(f4741,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X2),mult(X1,X3)))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f6,f4740])).
% 5.06/1.16 fof(f4742,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X2),mult(X1,X3))))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f712,f4741])).
% 5.06/1.16 fof(f4743,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f809,f4742])).
% 5.06/1.16 fof(f4744,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f2378,f4743])).
% 5.06/1.16 fof(f4745,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))),mult(mult(X0,X1),mult(X2,X3))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f1977,f4744])).
% 5.06/1.16 fof(f4746,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3))),mult(mult(X0,X1),mult(X2,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f1006,f4745])).
% 5.06/1.16 fof(f4747,plain,(
% 5.06/1.16 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X1),mult(X2,X3)))))),
% 5.06/1.16 inference(forward_demodulation,[status(thm)],[f405,f4746])).
% 5.06/1.17 fof(f4749,plain,(
% 5.06/1.17 ![X0,X1,X2,X3]: (mult(mult(mult(X0,X1),mult(X2,X3)),mult(mult(X0,X2),mult(X1,X3)))=mult(mult(mult(X0,X2),mult(X1,X3)),mult(mult(X0,X1),mult(X2,X3))))),
% 5.06/1.17 inference(forward_demodulation,[status(thm)],[f809,f4747])).
% 5.06/1.17 fof(f4750,plain,(
% 5.06/1.17 $false),
% 5.06/1.17 inference(backward_subsumption_resolution,[status(thm)],[f10,f4749])).
% 5.06/1.17 % SZS output end CNFRefutation for theBenchmark.p
% 5.06/1.20 % Elapsed time: 0.730571 seconds
% 5.06/1.20 % CPU time: 5.577196 seconds
% 5.06/1.20 % Total memory used: 84.422 MB
% 5.06/1.20 % Net memory used: 81.830 MB
%------------------------------------------------------------------------------