%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:06:47 PM UTC 2026
% Result : Unsatisfiable 13.91s 2.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n003.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 13:51:02 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 13.91/2.33 % Refutation found
% 13.91/2.33 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 13.91/2.33 % SZS output start CNFRefutation for theBenchmark
% 13.91/2.33 fof(f1,axiom,(
% 13.91/2.33 (![X,Y,Z]: (add(multiply(X,Y),add(multiply(Y,Z),multiply(Z,X))) = multiply(add(X,Y),multiply(add(Y,Z),add(Z,X))) ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f2,axiom,(
% 13.91/2.33 (![X,Y,Z]: (add(X,multiply(Y,multiply(X,Z))) = X ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f3,axiom,(
% 13.91/2.33 (![X,Y,Z]: (add(add(multiply(X,Y),multiply(Y,Z)),Y) = Y ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f4,axiom,(
% 13.91/2.33 (![X,Y]: (multiply(add(X,inverse(X)),Y) = Y ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f5,axiom,(
% 13.91/2.33 (![X,Y,Z]: (multiply(X,add(Y,add(X,Z))) = X ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f6,axiom,(
% 13.91/2.33 (![X,Y,Z]: (multiply(multiply(add(X,Y),add(Y,Z)),Y) = Y ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f7,axiom,(
% 13.91/2.33 (![X,Y]: (add(multiply(X,inverse(X)),Y) = Y ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f8,axiom,(
% 13.91/2.33 (![X]: (add(X,inverse(X)) = n1 ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f9,axiom,(
% 13.91/2.33 (![X]: (multiply(X,inverse(X)) = n0 ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f10,axiom,(
% 13.91/2.33 (![X,Y,Z]: (add(add(X,Y),Z) = add(X,add(Y,Z)) ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f11,axiom,(
% 13.91/2.33 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f12,negated_conjecture,(
% 13.91/2.33 multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)) ),
% 13.91/2.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.91/2.33 fof(f13,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0)))=multiply(add(X0,X1),multiply(add(X1,X2),add(X2,X0))))),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f1])).
% 13.91/2.33 fof(f14,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,multiply(X1,multiply(X0,X2)))=X0)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f2])).
% 13.91/2.33 fof(f15,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(add(multiply(X0,X1),multiply(X1,X2)),X1)=X1)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f3])).
% 13.91/2.33 fof(f16,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(add(X0,inverse(X0)),X1)=X1)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f4])).
% 13.91/2.33 fof(f17,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(X0,add(X1,add(X0,X2)))=X0)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f5])).
% 13.91/2.33 fof(f18,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(multiply(add(X0,X1),add(X1,X2)),X1)=X1)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f6])).
% 13.91/2.33 fof(f19,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,inverse(X0)),X1)=X1)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f7])).
% 13.91/2.33 fof(f20,plain,(
% 13.91/2.33 ![X0]: (add(X0,inverse(X0))=n1)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f8])).
% 13.91/2.33 fof(f21,plain,(
% 13.91/2.33 ![X0]: (multiply(X0,inverse(X0))=n0)),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f9])).
% 13.91/2.33 fof(f22,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(add(X0,X1),X2)=add(X0,add(X1,X2)))),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f10])).
% 13.91/2.33 fof(f23,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f11])).
% 13.91/2.33 fof(f24,plain,(
% 13.91/2.33 ~multiply(a,add(b,c))=add(multiply(b,a),multiply(c,a))),
% 13.91/2.33 inference(cnf_transformation,[status(thm)],[f12])).
% 13.91/2.33 fof(f31,plain,(
% 13.91/2.33 ![X0]: (multiply(n1,X0)=X0)),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f20,f16])).
% 13.91/2.33 fof(f32,plain,(
% 13.91/2.33 ![X0]: (add(n0,X0)=X0)),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f21,f19])).
% 13.91/2.33 fof(f33,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),X1))=X1)),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f22,f15])).
% 13.91/2.33 fof(f34,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(add(X0,X1),multiply(add(X1,X2),X1))=X1)),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f23,f18])).
% 13.91/2.33 fof(f35,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(X0,add(X1,X0))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f14,f17])).
% 13.91/2.33 fof(f36,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,multiply(X1,X0))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f17,f14])).
% 13.91/2.33 fof(f42,plain,(
% 13.91/2.33 ![X0,X1]: (add(add(X0,X1),X1)=add(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f35,f36])).
% 13.91/2.33 fof(f43,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(multiply(X0,X1),X1)=multiply(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f36,f35])).
% 13.91/2.33 fof(f47,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,add(X1,X1))=add(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f22,f42])).
% 13.91/2.33 fof(f48,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(X0,multiply(X1,X1))=multiply(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f43])).
% 13.91/2.33 fof(f51,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(add(X0,X0),add(X1,X0))=add(X0,X0))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f47,f35])).
% 13.91/2.33 fof(f56,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X0)),add(multiply(multiply(X1,X0),X2),multiply(X2,X0)))=multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f36,f13])).
% 13.91/2.33 fof(f64,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(multiply(X0,X1),X2),add(multiply(X2,X1),multiply(X1,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),multiply(add(X2,X1),X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f36,f13])).
% 13.91/2.33 fof(f71,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X0)),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0)))=multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f56])).
% 13.91/2.33 fof(f86,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),multiply(add(X2,X1),X1)))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f64])).
% 13.91/2.33 fof(f89,plain,(
% 13.91/2.33 ![X0]: (add(multiply(X0,X0),add(multiply(X0,X0),multiply(X0,X0)))=multiply(add(X0,X0),add(X0,X0)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f13,f48])).
% 13.91/2.33 fof(f93,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X0),multiply(X1,X0))=multiply(X0,X0))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f48,f36])).
% 13.91/2.33 fof(f95,plain,(
% 13.91/2.33 ![X0]: (add(multiply(X0,X0),multiply(X0,X0))=multiply(add(X0,X0),add(X0,X0)))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f47,f89])).
% 13.91/2.33 fof(f96,plain,(
% 13.91/2.33 ![X0]: (add(multiply(X0,X0),multiply(X0,X0))=add(X0,X0))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f51,f95])).
% 13.91/2.33 fof(f100,plain,(
% 13.91/2.33 ![X0]: (multiply(X0,X0)=add(X0,X0))),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f93,f96])).
% 13.91/2.33 fof(f109,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,add(multiply(X0,X1),multiply(X0,X1)))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f100,f14])).
% 13.91/2.33 fof(f110,plain,(
% 13.91/2.33 ![X0]: (add(X0,add(X0,X0))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f100,f36])).
% 13.91/2.33 fof(f116,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,multiply(X0,X1))=X0)),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f47,f109])).
% 13.91/2.33 fof(f117,plain,(
% 13.91/2.33 ![X0]: (multiply(X0,X0)=X0)),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f124,f100])).
% 13.91/2.33 fof(f124,plain,(
% 13.91/2.33 ![X0]: (add(X0,X0)=X0)),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f47,f110])).
% 13.91/2.33 fof(f135,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(X0,add(X0,X1))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f124,f17])).
% 13.91/2.33 fof(f137,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X1),add(multiply(X1,X1),multiply(X1,X0)))=multiply(add(X0,X1),multiply(X1,add(X1,X0))))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f124,f13])).
% 13.91/2.33 fof(f142,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X1),add(X1,multiply(X1,X0)))=multiply(add(X0,X1),multiply(X1,add(X1,X0))))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f117,f137])).
% 13.91/2.33 fof(f143,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X1),X1)=multiply(add(X0,X1),multiply(X1,add(X1,X0))))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f116,f142])).
% 13.91/2.33 fof(f145,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),add(multiply(X2,X1),X1)))),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f147,f86])).
% 13.91/2.33 fof(f147,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X1),X1)=multiply(add(X0,X1),X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f135,f143])).
% 13.91/2.33 fof(f156,plain,(
% 13.91/2.33 ![X0,X1]: (add(add(X0,X1),X0)=add(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f135,f36])).
% 13.91/2.33 fof(f160,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,add(X1,X0))=add(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f22,f156])).
% 13.91/2.33 fof(f164,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(add(X0,X1),add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))))=add(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f13,f116])).
% 13.91/2.33 fof(f172,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(multiply(X0,X1),X2),add(multiply(X2,X0),multiply(X0,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),multiply(add(X2,X0),X0)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f116,f13])).
% 13.91/2.33 fof(f173,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X1,X2)),multiply(multiply(X1,X2),X0)))=multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f116,f13])).
% 13.91/2.33 fof(f175,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f116,f35])).
% 13.91/2.33 fof(f177,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,add(X1,add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0)))))=add(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f22,f164])).
% 13.91/2.33 fof(f178,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),multiply(add(X2,X0),X0)))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f172])).
% 13.91/2.33 fof(f179,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),add(multiply(X2,X0),X0)))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f147,f178])).
% 13.91/2.33 fof(f180,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X1,X2)),multiply(X1,multiply(X2,X0))))=multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f173])).
% 13.91/2.33 fof(f182,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0)))=multiply(add(multiply(X0,X1),X2),add(multiply(X2,X1),X1)))),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f186,f145])).
% 13.91/2.33 fof(f184,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0)))=multiply(X0,multiply(add(multiply(X1,X0),X2),add(X2,X0))))),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f186,f71])).
% 13.91/2.33 fof(f186,plain,(
% 13.91/2.33 ![X0,X1]: (multiply(X0,multiply(X1,X0))=multiply(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f23,f175])).
% 13.91/2.33 fof(f220,plain,(
% 13.91/2.33 ![X0,X1]: (add(multiply(X0,X1),multiply(X1,X0))=multiply(X0,X1))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f186,f36])).
% 13.91/2.33 fof(f408,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,X1)=add(X0,add(multiply(X0,X2),X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f116,f22])).
% 13.91/2.33 fof(f409,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,X1)=add(X0,add(multiply(X2,X0),X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f36,f22])).
% 13.91/2.33 fof(f410,plain,(
% 13.91/2.33 ![X0,X1]: (add(X0,X1)=add(X0,add(X0,X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f124,f22])).
% 13.91/2.33 fof(f421,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(multiply(add(X0,X1),X2),X2)=multiply(add(X0,add(X1,X2)),X2))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f22,f147])).
% 13.91/2.33 fof(f428,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(X0,add(X1,add(X2,X0)))=X0)),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f22,f35])).
% 13.91/2.33 fof(f442,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,add(X1,add(multiply(X1,X2),multiply(X2,X0))))=add(X0,X1))),
% 13.91/2.33 inference(backward_demodulation,[status(thm)],[f409,f177])).
% 13.91/2.33 fof(f469,plain,(
% 13.91/2.33 ![X0,X1,X2]: (add(X0,add(X1,multiply(X2,X0)))=add(X0,X1))),
% 13.91/2.33 inference(forward_demodulation,[status(thm)],[f408,f442])).
% 13.91/2.33 fof(f484,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(X0,X1)=multiply(X0,multiply(X1,add(X2,multiply(X0,X1)))))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f35,f23])).
% 13.91/2.33 fof(f489,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(add(multiply(X0,X1),X1),X2)=multiply(add(X0,X1),multiply(X1,X2)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f147,f23])).
% 13.91/2.33 fof(f492,plain,(
% 13.91/2.33 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(X0,multiply(add(X2,add(X0,X3)),X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f17,f23])).
% 13.91/2.33 fof(f493,plain,(
% 13.91/2.33 ![X0,X1,X2]: (multiply(X0,X1)=multiply(X0,multiply(add(X0,X2),X1)))),
% 13.91/2.33 inference(paramodulation,[status(thm)],[f135,f23])).
% 13.91/2.33 fof(f494,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(X0,multiply(add(X2,X0),X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f35,f23])).
% 14.68/2.35 fof(f495,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,X1)=multiply(X0,multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f117,f23])).
% 14.68/2.35 fof(f505,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X0,multiply(X1,X2)))=multiply(X0,X1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f23,f116])).
% 14.68/2.35 fof(f507,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(X1,multiply(X2,X0)))=X0)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f23,f36])).
% 14.68/2.35 fof(f532,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),multiply(X1,multiply(X2,X0))))=multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f495,f180])).
% 14.68/2.35 fof(f533,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,X1)))=multiply(add(multiply(X0,X1),X2),add(multiply(X2,X0),X0)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f495,f179])).
% 14.68/2.35 fof(f549,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(add(X0,X1),multiply(X1,add(multiply(X1,X2),X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f505,f532])).
% 14.68/2.35 fof(f553,plain,(
% 14.68/2.35 ![X0]: (multiply(inverse(X0),n0)=multiply(inverse(X0),X0))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f21,f186])).
% 14.68/2.35 fof(f554,plain,(
% 14.68/2.35 ![X0]: (add(X0,n0)=X0)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f21,f116])).
% 14.68/2.35 fof(f570,plain,(
% 14.68/2.35 ![X0]: (multiply(n0,X0)=n0)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f554,f35])).
% 14.68/2.35 fof(f589,plain,(
% 14.68/2.35 ![X0]: (multiply(n1,X0)=multiply(X0,n1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f186,f31])).
% 14.68/2.35 fof(f591,plain,(
% 14.68/2.35 ![X0]: (n1=add(n1,X0))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f135,f31])).
% 14.68/2.35 fof(f592,plain,(
% 14.68/2.35 ![X0]: (n1=add(X0,n1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f35,f31])).
% 14.68/2.35 fof(f606,plain,(
% 14.68/2.35 ![X0]: (X0=multiply(X0,n1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f31,f589])).
% 14.68/2.35 fof(f745,plain,(
% 14.68/2.35 ![X0,X1]: (n0=multiply(X0,multiply(n0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f14,f32])).
% 14.68/2.35 fof(f770,plain,(
% 14.68/2.35 ![X0]: (n0=multiply(inverse(X0),X0))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f773,f553])).
% 14.68/2.35 fof(f773,plain,(
% 14.68/2.35 ![X0]: (n0=multiply(X0,n0))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f570,f745])).
% 14.68/2.35 fof(f989,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,add(X1,X2)),multiply(add(X1,X2),X0)))=multiply(add(X0,X1),multiply(add(X1,X2),add(add(X1,X2),X0))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f410,f13])).
% 14.68/2.35 fof(f1025,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(X1,multiply(add(X1,X2),X0)))=multiply(add(X0,X1),multiply(add(X1,X2),add(add(X1,X2),X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f135,f989])).
% 14.68/2.35 fof(f1026,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(X1,multiply(add(X1,X2),X0)))=multiply(add(X0,X1),add(X1,X2)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f135,f1025])).
% 14.68/2.35 fof(f1137,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X2,X0))=multiply(X0,X1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f116,f428])).
% 14.68/2.35 fof(f1163,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0)))=multiply(X0,add(multiply(X1,X0),X2)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1165,f184])).
% 14.68/2.35 fof(f1165,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,multiply(X1,add(X2,X0)))=multiply(X0,X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f1137])).
% 14.68/2.35 fof(f1263,plain,(
% 14.68/2.35 ![X0,X1]: (add(n0,add(multiply(X0,X1),X0))=X0)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f770,f33])).
% 14.68/2.35 fof(f1266,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X3),X2))=X2)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f23,f33])).
% 14.68/2.35 fof(f1268,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(add(multiply(X0,X1),X1),add(multiply(X1,X2),X1))=X1)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f147,f33])).
% 14.68/2.35 fof(f1311,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(multiply(X0,X1),add(multiply(X1,X2),X1)),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1))))=multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f33,f13])).
% 14.68/2.35 fof(f1318,plain,(
% 14.68/2.35 ![X0,X1]: (add(multiply(X0,X1),X0)=X0)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f32,f1263])).
% 14.68/2.35 fof(f1321,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),X2)=X2)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1318,f1266])).
% 14.68/2.35 fof(f1325,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(X1,add(multiply(X1,X2),X1)))=X1)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f22,f1268])).
% 14.68/2.35 fof(f1326,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(X1,multiply(X1,X2)))=X1)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f160,f1325])).
% 14.68/2.35 fof(f1327,plain,(
% 14.68/2.35 ![X0,X1]: (X0=multiply(add(X1,X0),X0))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1344,f147])).
% 14.68/2.35 fof(f1329,plain,(
% 14.68/2.35 ![X0,X1,X2]: (X0=multiply(add(X1,add(X2,X0)),X0))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1344,f421])).
% 14.68/2.35 fof(f1337,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X0),multiply(X0,X1)))=multiply(add(multiply(X0,X1),X2),X0))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1344,f533])).
% 14.68/2.35 fof(f1339,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(add(X2,X0),multiply(X0,X1)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1344,f489])).
% 14.68/2.35 fof(f1342,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0)))=multiply(add(multiply(X0,X1),X2),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1344,f182])).
% 14.68/2.35 fof(f1344,plain,(
% 14.68/2.35 ![X0,X1]: (add(multiply(X0,X1),X1)=X1)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f116,f1326])).
% 14.68/2.35 fof(f1405,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,multiply(X1,add(multiply(X1,X2),X1))),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1))))=multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f1311])).
% 14.68/2.35 fof(f1406,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,X1),add(multiply(add(multiply(X1,X2),X1),X3),multiply(X3,multiply(X0,X1))))=multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f35,f1405])).
% 14.68/2.35 fof(f1407,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,X1),multiply(add(multiply(X1,X2),X1),X3))=multiply(X1,multiply(add(add(multiply(X1,X2),X1),X3),add(X3,multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f469,f1406])).
% 14.68/2.35 fof(f1408,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(X1,multiply(add(add(multiply(X1,X3),X1),X2),add(X2,multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1318,f1407])).
% 14.68/2.35 fof(f1409,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(X1,multiply(add(multiply(X1,X3),add(X1,X2)),add(X2,multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f22,f1408])).
% 14.68/2.35 fof(f1410,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(X0,add(multiply(X0,X1),multiply(X1,X2))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1411,f484])).
% 14.68/2.35 fof(f1411,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(X1,add(X2,multiply(X0,X1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f492,f1409])).
% 14.68/2.35 fof(f1419,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(X1,add(multiply(X1,X2),X0)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1339,f549])).
% 14.68/2.35 fof(f1422,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=add(multiply(multiply(X1,X2),X0),multiply(X0,X1)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1419,f1410])).
% 14.68/2.35 fof(f1424,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=add(multiply(X1,multiply(X2,X0)),multiply(X0,X1)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f1422])).
% 14.68/2.35 fof(f1428,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(n1,multiply(add(X0,X1),X0))=X0)),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f591,f34])).
% 14.68/2.35 fof(f1438,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (multiply(X0,multiply(add(multiply(X1,multiply(X2,X0)),X3),multiply(X1,multiply(X2,X0))))=multiply(X1,multiply(X2,X0)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f507,f34])).
% 14.68/2.35 fof(f1479,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(add(X0,X1),X0)=X0)),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f31,f1428])).
% 14.68/2.35 fof(f1492,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,multiply(X1,multiply(X2,X0)))=multiply(X1,multiply(X2,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1479,f1438])).
% 14.68/2.35 fof(f1830,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,X1)=add(multiply(X2,X0),add(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1344,f22])).
% 14.68/2.35 fof(f1842,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X0,X1),X2))=multiply(add(X2,X0),add(X0,X1)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1830,f1026])).
% 14.68/2.35 fof(f1862,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0)))=multiply(add(X0,X1),add(X2,multiply(add(X2,X0),X1))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f1842,f13])).
% 14.68/2.35 fof(f1946,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,X1)=multiply(X1,multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f36,f1327])).
% 14.68/2.35 fof(f2015,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(add(X0,X2),multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1479,f23])).
% 14.68/2.35 fof(f2135,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,multiply(X1,X0))=multiply(multiply(X1,X0),multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f186,f1946])).
% 14.68/2.35 fof(f2181,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,X1)=multiply(multiply(X0,X1),multiply(X1,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1946,f2135])).
% 14.68/2.35 fof(f2182,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,X1)=multiply(X0,multiply(X1,multiply(X1,X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f2181])).
% 14.68/2.35 fof(f2183,plain,(
% 14.68/2.35 ![X0,X1]: (multiply(X0,X1)=multiply(X1,multiply(X1,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1492,f2182])).
% 14.68/2.35 fof(f2216,plain,(
% 14.68/2.35 ![X0,X1]: (add(multiply(X0,n1),add(multiply(n1,X1),multiply(X1,X0)))=multiply(n1,add(X1,multiply(add(X1,X0),n1))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f592,f1862])).
% 14.68/2.35 fof(f2225,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X0)),add(multiply(multiply(X1,X0),X2),multiply(X2,X0)))=multiply(X0,add(X2,multiply(add(X2,X0),multiply(X1,X0)))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f36,f1862])).
% 14.68/2.35 fof(f2231,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(multiply(X1,X2),X1),multiply(X1,X0)))=multiply(add(X0,multiply(X1,X2)),X1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f14,f1862])).
% 14.68/2.35 fof(f2247,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(multiply(X0,X2),X0)))=multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1318,f1862])).
% 14.68/2.35 fof(f2264,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(multiply(X0,X1),X2),add(multiply(X2,X1),multiply(X1,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f36,f1862])).
% 14.68/2.35 fof(f2268,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))),add(X0,X1))=add(X0,X1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1862,f1318])).
% 14.68/2.35 fof(f2316,plain,(
% 14.68/2.35 ![X0,X1]: (add(X0,add(multiply(n1,X1),multiply(X1,X0)))=multiply(n1,add(X1,multiply(add(X1,X0),n1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f606,f2216])).
% 14.68/2.35 fof(f2317,plain,(
% 14.68/2.35 ![X0,X1]: (add(X0,multiply(n1,X1))=multiply(n1,add(X1,multiply(add(X1,X0),n1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f469,f2316])).
% 14.68/2.35 fof(f2318,plain,(
% 14.68/2.35 ![X0,X1]: (add(X0,X1)=multiply(n1,add(X1,multiply(add(X1,X0),n1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f31,f2317])).
% 14.68/2.35 fof(f2319,plain,(
% 14.68/2.35 ![X0,X1]: (add(X0,X1)=add(X1,multiply(add(X1,X0),n1)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f31,f2318])).
% 14.68/2.35 fof(f2320,plain,(
% 14.68/2.35 ![X0,X1]: (add(X0,X1)=add(X1,add(X1,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f606,f2319])).
% 14.68/2.35 fof(f2349,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(multiply(X0,X1),X2),multiply(X2,X1)))=multiply(X1,add(X2,multiply(add(X2,X1),multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1946,f2225])).
% 14.68/2.35 fof(f2350,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=multiply(X1,add(X2,multiply(add(X2,X1),multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f408,f2349])).
% 14.68/2.35 fof(f2369,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X1,multiply(X2,X1)),multiply(X1,X0)))=multiply(add(X0,multiply(X1,X2)),X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f2231])).
% 14.68/2.35 fof(f2370,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,multiply(X1,X2)),X1)=multiply(add(multiply(X0,X1),X2),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f2371,f1342])).
% 14.68/2.35 fof(f2371,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0)))=multiply(add(X0,multiply(X1,X2)),X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1946,f2369])).
% 14.68/2.35 fof(f2452,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X0,multiply(X2,X0))))=multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f2247])).
% 14.68/2.35 fof(f2453,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X0)))=multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1946,f2452])).
% 14.68/2.35 fof(f2454,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,add(multiply(X1,X0),X2))=multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1163,f2453])).
% 14.68/2.35 fof(f2518,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,multiply(X0,X1))))=multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f2264])).
% 14.68/2.35 fof(f2519,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1)))=multiply(add(multiply(X0,X1),X2),add(X1,multiply(X1,X2))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1946,f2518])).
% 14.68/2.35 fof(f2520,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1)))=multiply(add(multiply(X0,X1),X2),X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f116,f2519])).
% 14.68/2.35 fof(f2529,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(add(multiply(X1,X2),multiply(X2,X0)),add(X0,X1)))=add(X0,X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f22,f2268])).
% 14.68/2.35 fof(f2530,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),add(multiply(X2,X0),add(X0,X1))))=add(X0,X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f22,f2529])).
% 14.68/2.35 fof(f2533,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,X2),add(X0,X1)))=add(X0,X1))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1830,f2530])).
% 14.68/2.35 fof(f2558,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X0,X1)))=multiply(add(X0,multiply(X1,X2)),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f2370,f2520])).
% 14.68/2.35 fof(f2586,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),multiply(X2,X1))=multiply(X2,X1))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f186,f1321])).
% 14.68/2.35 fof(f2587,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,X1),add(X2,add(X3,X1)))=add(X2,add(X3,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f428,f1321])).
% 14.68/2.35 fof(f2615,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X0))=multiply(X0,add(multiply(X1,X0),X2)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f2586,f1163])).
% 14.68/2.35 fof(f2617,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(X2,X0))=add(X2,X0))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f2587,f2533])).
% 14.68/2.35 fof(f2634,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X0))=multiply(add(X0,X1),add(multiply(X0,X2),multiply(X0,X1))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f2615,f2454])).
% 14.68/2.35 fof(f3006,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,add(X0,X1)),add(multiply(add(X0,X1),X2),multiply(X2,X0)))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f2320,f1862])).
% 14.68/2.35 fof(f3081,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,add(multiply(add(X0,X1),X2),multiply(X2,X0)))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f135,f3006])).
% 14.68/2.35 fof(f3082,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X0,X1),X2))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f469,f3081])).
% 14.68/2.35 fof(f3083,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X0,X1),X2))=multiply(add(X1,X0),add(X2,add(X0,multiply(add(X0,X1),X2)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1842,f3082])).
% 14.68/2.35 fof(f3084,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X0,X1),X2))=multiply(add(X1,X0),add(X2,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f469,f3083])).
% 14.68/2.35 fof(f3139,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(add(X2,X1),multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f36,f1329])).
% 14.68/2.35 fof(f3176,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=multiply(X1,add(X2,multiply(X0,X1))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f3139,f2350])).
% 14.68/2.35 fof(f3899,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(multiply(add(X0,X1),X2),X0),multiply(X0,X2))=multiply(multiply(add(X0,X1),X2),X0))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f493,f220])).
% 14.68/2.35 fof(f3914,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(add(X0,X1),X2),multiply(X0,X2))=multiply(add(X0,X1),X2))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f493,f36])).
% 14.68/2.35 fof(f3973,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(add(X0,X1),multiply(X2,X0)),multiply(X0,X2))=multiply(multiply(add(X0,X1),X2),X0))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f3899])).
% 14.68/2.35 fof(f3974,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(multiply(add(X0,X2),X1),X0))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f2586,f3973])).
% 14.68/2.35 fof(f3975,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,X1)=multiply(add(X0,X2),multiply(X1,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f3974])).
% 14.68/2.35 fof(f5499,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X0,X1)),add(multiply(multiply(X0,X1),X2),multiply(X2,X0)))=multiply(add(X0,multiply(X0,X1)),add(X2,multiply(X0,X1))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1339,f1862])).
% 14.68/2.35 fof(f5596,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(multiply(X1,X0),X2),multiply(X2,X1)))=multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f2183,f5499])).
% 14.68/2.35 fof(f5597,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),add(multiply(X1,multiply(X0,X2)),multiply(X2,X1)))=multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f5596])).
% 14.68/2.35 fof(f5598,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=multiply(add(X1,multiply(X1,X0)),add(X2,multiply(X1,X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1424,f5597])).
% 14.68/2.35 fof(f5599,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=add(multiply(X1,X0),multiply(add(multiply(X1,X0),X1),X2)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f3084,f5598])).
% 14.68/2.35 fof(f5600,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=add(multiply(X1,X0),multiply(X1,X2)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1318,f5599])).
% 14.68/2.35 fof(f6085,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(X0,add(X1,multiply(add(X1,X2),X0)))=multiply(X0,add(multiply(X2,X0),add(multiply(X0,X1),multiply(X1,X2)))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f1862,f494])).
% 14.68/2.35 fof(f6184,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(add(X0,X1),X2),multiply(X0,X2))=multiply(X2,add(multiply(X1,X2),add(multiply(X2,X0),multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f3176,f6085])).
% 14.68/2.35 fof(f6185,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(X2,add(multiply(X1,X2),add(multiply(X2,X0),multiply(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f3914,f6184])).
% 14.68/2.35 fof(f6187,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X2,X1),multiply(add(multiply(X2,X0),multiply(X0,X1)),X2)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f2615,f6185])).
% 14.68/2.35 fof(f6726,plain,(
% 14.68/2.35 ![X0,X1,X2,X3]: (add(multiply(X0,multiply(X1,X2)),add(X3,multiply(X0,X1)))=add(X3,multiply(X0,X1)))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f23,f2617])).
% 14.68/2.35 fof(f6831,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=multiply(add(X2,multiply(X1,X0)),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6726,f2558])).
% 14.68/2.35 fof(f6832,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(add(multiply(X1,X2),X0),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6726,f1337])).
% 14.68/2.35 fof(f6928,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0)))=add(multiply(X2,X1),multiply(X0,X1)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6831,f2371])).
% 14.68/2.35 fof(f6929,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X2,X1),add(multiply(multiply(X0,X1),X2),multiply(X2,X0))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6832,f6187])).
% 14.68/2.35 fof(f6935,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X2,X1),add(multiply(X0,multiply(X1,X2)),multiply(X2,X0))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f23,f6929])).
% 14.68/2.35 fof(f6938,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X1))=multiply(add(X2,X0),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6940,f5600])).
% 14.68/2.35 fof(f6939,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X0))=multiply(add(X0,X1),multiply(add(X1,X2),X0)))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6940,f2634])).
% 14.68/2.35 fof(f6940,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X2,X1),multiply(X2,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1424,f6935])).
% 14.68/2.35 fof(f6943,plain,(
% 14.68/2.35 ~multiply(a,add(b,c))=multiply(add(c,b),a)),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6938,f24])).
% 14.68/2.35 fof(f6948,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X1),multiply(X1,X0)))=multiply(add(X0,X2),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6938,f6928])).
% 14.68/2.35 fof(f6951,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(add(X0,multiply(X2,X1)),X2))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6938,f6831])).
% 14.68/2.35 fof(f6956,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(X2,add(X0,multiply(X1,X2))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6938,f3176])).
% 14.68/2.35 fof(f6970,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X2,X0))=multiply(X0,add(X1,X2)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f3975,f6939])).
% 14.68/2.35 fof(f6979,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(X1,X2))=multiply(add(X2,X0),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6956,f1411])).
% 14.68/2.35 fof(f6994,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,X1),multiply(add(X0,X1),X2))=multiply(add(X0,X1),add(X2,multiply(add(X2,X0),X1))))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6979,f1862])).
% 14.68/2.35 fof(f7037,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),multiply(add(X0,X2),X1))=multiply(add(X0,X2),X1))),
% 14.68/2.35 inference(backward_demodulation,[status(thm)],[f6979,f6948])).
% 14.68/2.35 fof(f7634,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,add(X0,X1)),multiply(add(X0,add(X0,X1)),X2))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f2320,f6994])).
% 14.68/2.35 fof(f7655,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),multiply(add(X0,multiply(X1,X2)),X1))=multiply(add(X0,multiply(X1,X2)),add(X1,multiply(X1,X2))))),
% 14.68/2.35 inference(paramodulation,[status(thm)],[f2015,f6994])).
% 14.68/2.35 fof(f7833,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X0,add(X0,X1)),X2))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f135,f7634])).
% 14.68/2.35 fof(f7834,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X1,X0),X2))=multiply(add(X1,X0),add(X2,multiply(add(X2,X0),add(X0,X1)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f2320,f7833])).
% 14.68/2.35 fof(f7835,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X1,X0),X2))=multiply(add(X1,X0),add(X2,add(X0,multiply(add(X0,X1),X2)))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f1842,f7834])).
% 14.68/2.35 fof(f7836,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(X0,multiply(add(X1,X0),X2))=multiply(add(X1,X0),add(X2,X0)))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f469,f7835])).
% 14.68/2.35 fof(f7909,plain,(
% 14.68/2.35 ![X0,X1,X2]: (add(multiply(X0,multiply(X1,X2)),multiply(add(X0,X2),X1))=multiply(add(X0,multiply(X1,X2)),add(X1,multiply(X1,X2))))),
% 14.68/2.35 inference(forward_demodulation,[status(thm)],[f6951,f7655])).
% 14.68/2.35 fof(f7910,plain,(
% 14.68/2.35 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(add(X0,multiply(X2,X1)),add(X2,multiply(X2,X1))))),
% 14.68/2.38 inference(forward_demodulation,[status(thm)],[f7037,f7909])).
% 14.68/2.38 fof(f7911,plain,(
% 14.68/2.38 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X2,X1),multiply(add(X0,multiply(X2,X1)),X2)))),
% 14.68/2.38 inference(forward_demodulation,[status(thm)],[f7836,f7910])).
% 14.68/2.38 fof(f7912,plain,(
% 14.68/2.38 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(X2,add(X1,add(X0,multiply(X2,X1)))))),
% 14.68/2.38 inference(forward_demodulation,[status(thm)],[f6970,f7911])).
% 14.68/2.38 fof(f7914,plain,(
% 14.68/2.38 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=multiply(X2,add(X1,X0)))),
% 14.68/2.38 inference(forward_demodulation,[status(thm)],[f469,f7912])).
% 14.68/2.38 fof(f7915,plain,(
% 14.68/2.38 $false),
% 14.68/2.38 inference(backward_subsumption_resolution,[status(thm)],[f6943,f7914])).
% 14.68/2.38 % SZS output end CNFRefutation for theBenchmark.p
% 14.68/2.40 % Elapsed time: 1.950737 seconds
% 14.68/2.40 % CPU time: 15.168173 seconds
% 14.68/2.40 % Total memory used: 139.312 MB
% 14.68/2.40 % Net memory used: 135.019 MB
%------------------------------------------------------------------------------