%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO023-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 : n026.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 247.78s 31.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 13:51:23 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 247.78/31.67 % Refutation found
% 247.78/31.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 247.78/31.67 % SZS output start CNFRefutation for theBenchmark
% 247.78/31.67 fof(f1,axiom,(
% 247.78/31.67 (![X,Y]: (multiply(add(X,Y),Y) = Y ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f2,axiom,(
% 247.78/31.67 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f3,axiom,(
% 247.78/31.67 (![X]: (add(X,inverse(X)) = n1 ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f4,axiom,(
% 247.78/31.67 (![X,Y,Z]: (pixley(X,Y,Z) = add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z))) ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f5,axiom,(
% 247.78/31.67 (![X,Y]: (pixley(X,X,Y) = Y ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f6,axiom,(
% 247.78/31.67 (![X,Y]: (pixley(X,Y,Y) = X ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f7,axiom,(
% 247.78/31.67 (![X,Y]: (pixley(X,Y,X) = X ))),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f8,negated_conjecture,(
% 247.78/31.67 add(a,multiply(b,c)) != multiply(add(a,b),add(a,c)) ),
% 247.78/31.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 247.78/31.67 fof(f9,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X1),X1)=X1)),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f1])).
% 247.78/31.67 fof(f10,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X1,X0),multiply(X2,X0)))),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f2])).
% 247.78/31.67 fof(f11,plain,(
% 247.78/31.67 ![X0]: (add(X0,inverse(X0))=n1)),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f3])).
% 247.78/31.67 fof(f12,plain,(
% 247.78/31.67 ![X0,X1,X2]: (pixley(X0,X1,X2)=add(multiply(X0,inverse(X1)),add(multiply(X0,X2),multiply(inverse(X1),X2))))),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f4])).
% 247.78/31.67 fof(f13,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,X0,X1)=X1)),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f5])).
% 247.78/31.67 fof(f14,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,X1,X1)=X0)),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f6])).
% 247.78/31.67 fof(f15,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,X1,X0)=X0)),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f7])).
% 247.78/31.67 fof(f16,plain,(
% 247.78/31.67 ~add(a,multiply(b,c))=multiply(add(a,b),add(a,c))),
% 247.78/31.67 inference(cnf_transformation,[status(thm)],[f8])).
% 247.78/31.67 fof(f23,plain,(
% 247.78/31.67 ![X0,X1,X2]: (pixley(X0,X1,X2)=add(multiply(X0,inverse(X1)),multiply(X2,add(X0,inverse(X1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f12])).
% 247.78/31.67 fof(f30,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,inverse(X0))=inverse(X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f9])).
% 247.78/31.67 fof(f31,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(X0,add(add(X1,X0),X2))=add(X0,multiply(X2,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f9,f10])).
% 247.78/31.67 fof(f32,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(X0,add(X1,add(X2,X0)))=add(multiply(X1,X0),X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f9,f10])).
% 247.78/31.67 fof(f33,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(multiply(X0,add(X1,X2)),multiply(X2,X0))=multiply(X2,X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f10,f9])).
% 247.78/31.67 fof(f34,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(inverse(X0),add(X1,n1))=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f30,f10])).
% 247.78/31.67 fof(f36,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,n1)=add(X0,multiply(inverse(add(X1,X0)),X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f31])).
% 247.78/31.67 fof(f37,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),add(multiply(X1,add(X2,X0)),X3))=add(multiply(X0,X1),multiply(X3,multiply(X0,X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f10,f31])).
% 247.78/31.67 fof(f39,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(add(X0,X1),X2),add(X3,X1))=add(multiply(X3,add(add(X0,X1),X2)),add(X1,multiply(X2,X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f31,f10])).
% 247.78/31.67 fof(f40,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(add(X0,X1),X2),add(X1,X3))=add(add(X1,multiply(X2,X1)),multiply(X3,add(add(X0,X1),X2))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f31,f10])).
% 247.78/31.67 fof(f45,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(X0,add(X1,X2)),add(X3,X2))=add(multiply(X3,add(X0,add(X1,X2))),add(multiply(X0,X2),X2)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f32,f10])).
% 247.78/31.67 fof(f46,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(X0,add(X1,X2)),add(X2,X3))=add(add(multiply(X0,X2),X2),multiply(X3,add(X0,add(X1,X2)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f32,f10])).
% 247.78/31.67 fof(f49,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,X1),multiply(X1,add(X2,add(X0,X1))))=multiply(X1,add(X2,add(X0,X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f9,f33])).
% 247.78/31.67 fof(f53,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,n1),multiply(inverse(X1),X0))=multiply(inverse(X1),X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f33])).
% 247.78/31.67 fof(f57,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(add(add(X0,X1),X2),add(X3,X1)),add(X1,multiply(X2,X1)))=multiply(X1,add(add(X0,X1),X2)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f31,f33])).
% 247.78/31.67 fof(f61,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,X1),add(multiply(X2,X1),X1))=multiply(X1,add(X2,add(X0,X1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f32,f49])).
% 247.78/31.67 fof(f62,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,X1),add(multiply(X2,X1),X1))=add(multiply(X2,X1),X1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f32,f61])).
% 247.78/31.67 fof(f70,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(add(add(X0,X1),X2),add(X3,X1)),add(X1,multiply(X2,X1)))=add(X1,multiply(X2,X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f31,f57])).
% 247.78/31.67 fof(f82,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(n1,X0,X1)=add(inverse(X0),multiply(X1,add(n1,inverse(X0)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f30,f23])).
% 247.78/31.67 fof(f86,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,X0,X1)=add(multiply(X0,inverse(X0)),multiply(X1,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f23])).
% 247.78/31.67 fof(f89,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X2))),add(X3,pixley(X1,X2,X0)))=add(multiply(X3,multiply(X0,add(X1,inverse(X2)))),multiply(X0,add(X1,inverse(X2)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f23,f32])).
% 247.78/31.67 fof(f90,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X2))),add(pixley(X1,X2,X0),X3))=add(multiply(X0,add(X1,inverse(X2))),multiply(X3,multiply(X0,add(X1,inverse(X2))))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f23,f31])).
% 247.78/31.67 fof(f91,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(pixley(X0,X1,X2),multiply(X2,add(X0,inverse(X1))))=multiply(X2,add(X0,inverse(X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f23,f9])).
% 247.78/31.67 fof(f92,plain,(
% 247.78/31.67 ![X0,X1]: (X0=add(multiply(X1,inverse(X1)),multiply(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f13,f86])).
% 247.78/31.67 fof(f94,plain,(
% 247.78/31.67 ![X0]: (X0=add(inverse(n1),multiply(X0,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f30,f92])).
% 247.78/31.67 fof(f98,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,n1),add(X1,X0))=add(multiply(X1,multiply(X0,n1)),multiply(X0,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f92,f32])).
% 247.78/31.67 fof(f99,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,n1),add(X0,X1))=add(multiply(X0,n1),multiply(X1,multiply(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f92,f31])).
% 247.78/31.67 fof(f100,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(X0,n1))=multiply(X0,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f92,f9])).
% 247.78/31.67 fof(f102,plain,(
% 247.78/31.67 ![X0]: (add(X0,n1)=add(inverse(n1),n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f9,f94])).
% 247.78/31.67 fof(f114,plain,(
% 247.78/31.67 ![X0,X1]: (add(X0,n1)=add(X1,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f102,f102])).
% 247.78/31.67 fof(f130,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(X1,n1))=add(X0,multiply(n1,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f114,f31])).
% 247.78/31.67 fof(f146,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(X0,add(X1,n1))=multiply(X0,add(X2,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f130,f130])).
% 247.78/31.67 fof(f147,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(inverse(X0),add(X1,n1))=add(inverse(X0),inverse(X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f30,f130])).
% 247.78/31.67 fof(f179,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,n1),add(X1,n1))=add(add(X0,n1),multiply(n1,add(X2,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f146,f130])).
% 247.78/31.67 fof(f256,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(multiply(inverse(X0),X1),add(X2,multiply(X1,n1)))=add(multiply(X2,multiply(inverse(X0),X1)),multiply(inverse(X0),X1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f53,f10])).
% 247.78/31.67 fof(f306,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(inverse(X1),X2)),add(multiply(inverse(X1),X2),multiply(inverse(X1),X2)))=add(multiply(multiply(X2,n1),multiply(inverse(X1),X2)),multiply(inverse(X1),X2)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f53,f62])).
% 247.78/31.67 fof(f307,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(X0,multiply(X1,X2)),add(multiply(X1,X2),multiply(X1,X2)))=add(multiply(multiply(X2,add(X3,X1)),multiply(X1,X2)),multiply(X1,X2)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f33,f62])).
% 247.78/31.67 fof(f310,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,X1),add(X1,X1))=add(multiply(add(X2,X1),X1),X1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f9,f62])).
% 247.78/31.67 fof(f311,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,multiply(X1,n1)),add(multiply(X1,n1),multiply(X1,n1)))=add(multiply(X1,multiply(X1,n1)),multiply(X1,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f100,f62])).
% 247.78/31.67 fof(f342,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(inverse(X1),X2)),multiply(X2,add(inverse(X1),inverse(X1))))=add(multiply(multiply(X2,n1),multiply(inverse(X1),X2)),multiply(inverse(X1),X2)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f306])).
% 247.78/31.67 fof(f343,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(inverse(X1),X2)),multiply(X2,add(inverse(X1),inverse(X1))))=multiply(multiply(inverse(X1),X2),add(multiply(X2,n1),multiply(X2,n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f256,f342])).
% 247.78/31.67 fof(f344,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(inverse(X1),X2)),multiply(X2,add(inverse(X1),inverse(X1))))=multiply(multiply(inverse(X1),X2),multiply(n1,add(X2,X2))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f343])).
% 247.78/31.67 fof(f345,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(add(X0,multiply(X1,X2)),multiply(X2,add(X1,X1)))=add(multiply(multiply(X2,add(X3,X1)),multiply(X1,X2)),multiply(X1,X2)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f307])).
% 247.78/31.67 fof(f346,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(X1,X2)),multiply(X2,add(X1,X1)))=add(multiply(X1,X2),multiply(X1,X2)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f33,f345])).
% 247.78/31.67 fof(f347,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(inverse(X1),inverse(X1)))=multiply(multiply(inverse(X1),X0),multiply(n1,add(X0,X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f348,f344])).
% 247.78/31.67 fof(f348,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(X1,X2)),multiply(X2,add(X1,X1)))=multiply(X2,add(X1,X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f346])).
% 247.78/31.67 fof(f353,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X1),add(X1,X1))=add(X1,X1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f9,f310])).
% 247.78/31.67 fof(f354,plain,(
% 247.78/31.67 ![X0]: (add(multiply(X0,n1),multiply(X0,n1))=add(multiply(X0,multiply(X0,n1)),multiply(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f353,f311])).
% 247.78/31.67 fof(f355,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,add(X0,X0))=add(multiply(X0,multiply(X0,n1)),multiply(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f354])).
% 247.78/31.67 fof(f356,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,add(X0,X0))=multiply(multiply(X0,n1),add(X0,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f98,f355])).
% 247.78/31.67 fof(f361,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,n1),add(X1,n1))=add(n1,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f146,f353])).
% 247.78/31.67 fof(f363,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,add(multiply(X0,n1),multiply(X0,n1)))=add(multiply(X0,n1),multiply(X0,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f94,f353])).
% 247.78/31.67 fof(f373,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,add(inverse(X0),inverse(X0)))=add(inverse(X0),inverse(X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f353])).
% 247.78/31.67 fof(f381,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),multiply(X0,add(X1,X0)))=multiply(X0,add(X1,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f353,f33])).
% 247.78/31.67 fof(f387,plain,(
% 247.78/31.67 ![X0,X1]: (add(n1,n1)=add(add(X0,n1),multiply(n1,add(X1,n1))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f361,f179])).
% 247.78/31.67 fof(f389,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(n1,add(X0,X0)))=add(multiply(X0,n1),multiply(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f363])).
% 247.78/31.67 fof(f390,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(n1,add(X0,X0)))=multiply(n1,add(X0,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f389])).
% 247.78/31.67 fof(f428,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,n1),add(add(X1,n1),X2))=add(add(n1,n1),multiply(X2,add(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f361,f10])).
% 247.78/31.67 fof(f445,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=add(multiply(X1,add(X0,X0)),multiply(n1,add(X0,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f356,f10])).
% 247.78/31.67 fof(f455,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=multiply(add(X0,X0),add(X1,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f445])).
% 247.78/31.67 fof(f470,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,add(X0,X0)),add(X1,X0))=add(multiply(X1,multiply(n1,add(X0,X0))),multiply(n1,add(X0,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f390,f10])).
% 247.78/31.67 fof(f471,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,add(X0,X0)),add(X0,X1))=add(multiply(n1,add(X0,X0)),multiply(X1,multiply(n1,add(X0,X0)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f390,f10])).
% 247.78/31.67 fof(f533,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(inverse(X0),inverse(X0)),add(X1,n1))=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f373,f130])).
% 247.78/31.67 fof(f552,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,n1),add(n1,multiply(n1,n1)))=multiply(n1,add(X0,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f130,f381])).
% 247.78/31.67 fof(f571,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,n1),add(n1,n1))=multiply(n1,add(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f455,f552])).
% 247.78/31.67 fof(f577,plain,(
% 247.78/31.67 ![X0]: (add(n1,n1)=add(add(X0,n1),add(n1,n1)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f578,f387])).
% 247.78/31.67 fof(f578,plain,(
% 247.78/31.67 ![X0]: (add(n1,n1)=multiply(n1,add(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f361,f571])).
% 247.78/31.67 fof(f621,plain,(
% 247.78/31.67 multiply(add(n1,n1),multiply(n1,n1))=multiply(n1,n1)),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f578,f33])).
% 247.78/31.67 fof(f625,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,n1),add(n1,X1))=add(add(n1,n1),multiply(X1,add(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f578,f10])).
% 247.78/31.67 fof(f635,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,n1),add(add(X1,n1),X2))=multiply(add(X0,n1),add(n1,X2)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f625,f428])).
% 247.78/31.67 fof(f639,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,multiply(X1,add(X0,inverse(X1))))=multiply(X1,add(X0,inverse(X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f14,f91])).
% 247.78/31.67 fof(f736,plain,(
% 247.78/31.67 ![X0,X1]: (add(n1,n1)=add(add(X0,n1),add(X1,n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f114,f577])).
% 247.78/31.67 fof(f790,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,n1),n1)=add(add(X0,n1),multiply(inverse(add(n1,n1)),add(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f736,f36])).
% 247.78/31.67 fof(f793,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,n1),add(add(n1,n1),X1))=add(add(X0,n1),multiply(X1,add(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f736,f31])).
% 247.78/31.67 fof(f816,plain,(
% 247.78/31.67 ![X0]: (n1=add(add(X0,n1),multiply(inverse(add(n1,n1)),add(X0,n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f9,f790])).
% 247.78/31.67 fof(f819,plain,(
% 247.78/31.67 ![X0]: (n1=multiply(add(X0,n1),add(n1,inverse(add(n1,n1)))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f820,f816])).
% 247.78/31.67 fof(f820,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,n1),add(n1,X1))=add(add(X0,n1),multiply(X1,add(X0,n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f635,f793])).
% 247.78/31.67 fof(f995,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,n1),multiply(n1,n1))=multiply(n1,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f114,f621])).
% 247.78/31.67 fof(f1015,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,n1),add(add(X0,n1),X1))=add(multiply(n1,n1),multiply(X1,multiply(n1,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f995,f10])).
% 247.78/31.67 fof(f1026,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,n1),add(add(X0,n1),X1))=multiply(multiply(n1,n1),add(n1,X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f99,f1015])).
% 247.78/31.67 fof(f1412,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=add(multiply(X1,multiply(X0,add(X1,inverse(X0)))),multiply(X3,multiply(X1,multiply(X0,add(X1,inverse(X0)))))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f639,f37])).
% 247.78/31.67 fof(f1413,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,multiply(X1,add(X2,inverse(X1)))),add(multiply(X1,add(X2,inverse(X1))),multiply(X1,add(X2,inverse(X1)))))=add(multiply(X2,multiply(X1,add(X2,inverse(X1)))),multiply(X1,add(X2,inverse(X1)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f639,f62])).
% 247.78/31.67 fof(f1425,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=add(multiply(X0,add(X1,inverse(X0))),multiply(X3,multiply(X1,multiply(X0,add(X1,inverse(X0)))))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f639,f1412])).
% 247.78/31.67 fof(f1426,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=add(multiply(X0,add(X1,inverse(X0))),multiply(X3,multiply(X0,add(X1,inverse(X0))))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f639,f1425])).
% 247.78/31.67 fof(f1427,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=multiply(multiply(X0,add(X1,inverse(X0))),add(pixley(X1,X0,X0),X3)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f90,f1426])).
% 247.78/31.67 fof(f1428,plain,(
% 247.78/31.67 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=multiply(multiply(X0,add(X1,inverse(X0))),add(X1,X3)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f14,f1427])).
% 247.78/31.67 fof(f1429,plain,(
% 247.78/31.67 ![X0,X1]: (add(multiply(X0,add(X1,inverse(X0))),multiply(X0,add(X1,inverse(X0))))=add(multiply(X1,multiply(X0,add(X1,inverse(X0)))),multiply(X0,add(X1,inverse(X0)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f353,f1413])).
% 247.78/31.67 fof(f1430,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X1,X1))=add(multiply(X0,multiply(X1,add(X0,inverse(X1)))),multiply(X1,add(X0,inverse(X1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f1429])).
% 247.78/31.67 fof(f1431,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X1,X1))=multiply(multiply(X1,add(X0,inverse(X1))),add(X0,pixley(X0,X1,X1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f89,f1430])).
% 247.78/31.67 fof(f1432,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X1,X1))=multiply(multiply(X1,add(X0,inverse(X1))),add(X0,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f14,f1431])).
% 247.78/31.67 fof(f1502,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(add(X0,multiply(n1,add(X1,X1))),X1),add(X2,multiply(n1,add(X1,X1))))=add(multiply(X2,add(add(X0,multiply(n1,add(X1,X1))),X1)),add(multiply(n1,add(X1,X1)),multiply(n1,add(X1,X1)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f390,f39])).
% 247.78/31.67 fof(f1577,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(add(X0,multiply(n1,add(X1,X1))),X1),add(X2,multiply(n1,add(X1,X1))))=add(multiply(X2,add(add(X0,multiply(n1,add(X1,X1))),X1)),multiply(add(X1,X1),add(n1,n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f1502])).
% 247.78/31.67 fof(f1647,plain,(
% 247.78/31.67 multiply(n1,n1)=multiply(add(n1,n1),add(n1,inverse(add(n1,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f819,f639])).
% 247.78/31.67 fof(f1667,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,n1),add(add(X0,n1),X1))=multiply(n1,add(n1,X1)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1676,f1026])).
% 247.78/31.67 fof(f1676,plain,(
% 247.78/31.67 multiply(n1,n1)=n1),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f819,f1647])).
% 247.78/31.67 fof(f1700,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(n1,add(add(X0,n1),X1))=multiply(n1,add(n1,X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1676,f1667])).
% 247.78/31.67 fof(f1703,plain,(
% 247.78/31.67 ![X0]: (add(n1,multiply(X0,n1))=multiply(n1,add(n1,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f31,f1700])).
% 247.78/31.67 fof(f1712,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,multiply(inverse(X0),n1))=multiply(inverse(X0),n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1676,f53])).
% 247.78/31.67 fof(f1714,plain,(
% 247.78/31.67 n1=add(inverse(n1),n1)),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1676,f94])).
% 247.78/31.67 fof(f1733,plain,(
% 247.78/31.67 ![X0]: (n1=add(X0,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f114,f1714])).
% 247.78/31.67 fof(f1745,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(X0),n1)=add(inverse(X0),inverse(X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1714,f147])).
% 247.78/31.67 fof(f1749,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,n1)=add(X0,multiply(n1,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1714,f130])).
% 247.78/31.67 fof(f1758,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(X0,n1),multiply(n1,X0))=multiply(n1,X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1714,f33])).
% 247.78/31.67 fof(f1768,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(inverse(X0),n1)=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1733,f34])).
% 247.78/31.67 fof(f1796,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(add(X0,multiply(n1,add(X1,X1))),X1),add(X2,multiply(n1,add(X1,X1))))=add(multiply(X2,add(add(X0,multiply(n1,add(X1,X1))),X1)),multiply(add(X1,X1),n1)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1733,f1577])).
% 247.78/31.67 fof(f1867,plain,(
% 247.78/31.67 ![X0]: (multiply(add(inverse(X0),inverse(X0)),n1)=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1733,f533])).
% 247.78/31.67 fof(f1871,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=multiply(add(X0,X0),n1))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1733,f455])).
% 247.78/31.67 fof(f1937,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,multiply(inverse(X1),n1))=multiply(multiply(inverse(X1),X0),multiply(n1,add(X0,X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f1745,f347])).
% 247.78/31.67 fof(f2219,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(add(inverse(X0),inverse(X0)),add(inverse(X0),inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1745,f1867])).
% 247.78/31.67 fof(f2220,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(multiply(inverse(X0),n1),add(inverse(X0),inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1745,f2219])).
% 247.78/31.67 fof(f2221,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=add(multiply(inverse(X0),n1),multiply(inverse(X0),n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1745,f2220])).
% 247.78/31.67 fof(f2222,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(n1,add(inverse(X0),inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f2221])).
% 247.78/31.67 fof(f2223,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(n1,multiply(inverse(X0),n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1745,f2222])).
% 247.78/31.67 fof(f2227,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(inverse(X0),n1),n1)=multiply(inverse(X0),n1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1712,f2223])).
% 247.78/31.67 fof(f2468,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(add(X0,multiply(n1,X0)),X1),add(multiply(n1,X0),X2))=add(add(multiply(n1,X0),multiply(X1,multiply(n1,X0))),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1749,f40])).
% 247.78/31.67 fof(f2474,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(n1,X0),n1)=add(multiply(n1,X0),multiply(inverse(multiply(X0,n1)),multiply(n1,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1749,f36])).
% 247.78/31.67 fof(f2514,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(multiply(X0,n1),X1),add(multiply(n1,X0),X2))=add(add(multiply(n1,X0),multiply(X1,multiply(n1,X0))),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1749,f2468])).
% 247.78/31.67 fof(f2946,plain,(
% 247.78/31.67 ![X0]: (pixley(n1,X0,n1)=add(inverse(X0),add(n1,multiply(inverse(X0),n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f1703,f82])).
% 247.78/31.67 fof(f2984,plain,(
% 247.78/31.67 ![X0]: (n1=add(inverse(X0),add(n1,multiply(inverse(X0),n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f15,f2946])).
% 247.78/31.67 fof(f3131,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(X0),n1)=add(inverse(n1),multiply(inverse(X0),n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f2227,f94])).
% 247.78/31.67 fof(f3155,plain,(
% 247.78/31.67 ![X0,X1]: (inverse(X0)=add(multiply(X1,inverse(X0)),inverse(X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f3205,f1768])).
% 247.78/31.67 fof(f3168,plain,(
% 247.78/31.67 ![X0]: (n1=add(inverse(X0),add(n1,inverse(X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f3205,f2984])).
% 247.78/31.67 fof(f3175,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,inverse(X1))=multiply(multiply(inverse(X1),X0),multiply(n1,add(X0,X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f3205,f1937])).
% 247.78/31.67 fof(f3205,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(X0),n1)=inverse(X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f94,f3131])).
% 247.78/31.67 fof(f3314,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,add(X1,inverse(X1))),add(X2,inverse(X1)))=add(multiply(X2,add(X0,n1)),add(multiply(X0,inverse(X1)),inverse(X1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f45])).
% 247.78/31.67 fof(f3383,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,n1),add(X1,inverse(X2)))=add(multiply(X1,add(X0,n1)),add(multiply(X0,inverse(X2)),inverse(X2))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f11,f3314])).
% 247.78/31.67 fof(f3384,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(n1,add(X0,inverse(X1)))=add(multiply(X0,add(X2,n1)),add(multiply(X2,inverse(X1)),inverse(X1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f3383])).
% 247.78/31.67 fof(f3385,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(n1,add(X0,inverse(X1)))=add(multiply(X0,n1),add(multiply(X2,inverse(X1)),inverse(X1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f3384])).
% 247.78/31.67 fof(f3388,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(n1,add(X0,inverse(X1)))=add(multiply(X0,n1),inverse(X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3155,f3385])).
% 247.78/31.67 fof(f3430,plain,(
% 247.78/31.67 ![X0]: (inverse(X0)=add(inverse(n1),inverse(X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3205,f94])).
% 247.78/31.67 fof(f3597,plain,(
% 247.78/31.67 inverse(inverse(n1))=n1),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f11,f3430])).
% 247.78/31.67 fof(f3599,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(n1),multiply(X0,inverse(X0)))=multiply(X0,add(inverse(n1),inverse(X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3430,f639])).
% 247.78/31.67 fof(f3625,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(n1),multiply(X0,inverse(X0)))=multiply(X0,inverse(X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3430,f3599])).
% 247.78/31.67 fof(f3703,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,add(inverse(n1),inverse(X1))),add(inverse(X1),X2))=add(add(multiply(X0,inverse(X1)),inverse(X1)),multiply(X2,add(X0,inverse(X1)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3430,f46])).
% 247.78/31.67 fof(f3775,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,inverse(X1)),add(inverse(X1),X2))=add(add(multiply(X0,inverse(X1)),inverse(X1)),multiply(X2,add(X0,inverse(X1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3430,f3703])).
% 247.78/31.67 fof(f3777,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(X0,inverse(X1)),add(inverse(X1),X2))=add(inverse(X1),multiply(X2,add(X0,inverse(X1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3155,f3775])).
% 247.78/31.67 fof(f3821,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(inverse(n1),add(X0,n1)))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3597,f639])).
% 247.78/31.67 fof(f3837,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,inverse(n1),X1)=add(multiply(X0,inverse(inverse(n1))),multiply(X1,add(X0,n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3597,f23])).
% 247.78/31.67 fof(f3847,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(inverse(n1),n1))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f3821])).
% 247.78/31.67 fof(f3848,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),add(X0,inverse(inverse(n1)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3205,f3847])).
% 247.78/31.67 fof(f3849,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),add(X0,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3597,f3848])).
% 247.78/31.67 fof(f3850,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,inverse(n1))=multiply(inverse(n1),n1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f3849])).
% 247.78/31.67 fof(f3851,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,inverse(n1))=inverse(n1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3205,f3850])).
% 247.78/31.67 fof(f3898,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,inverse(n1),X1)=add(multiply(X0,n1),multiply(X1,add(X0,n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3597,f3837])).
% 247.78/31.67 fof(f3899,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,inverse(n1),X1)=add(multiply(X0,n1),multiply(X1,n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f3898])).
% 247.78/31.67 fof(f3903,plain,(
% 247.78/31.67 ![X0,X1]: (pixley(X0,inverse(n1),X1)=multiply(n1,add(X0,X1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f3899])).
% 247.78/31.67 fof(f3931,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(inverse(n1),add(X0,X1))=add(multiply(X0,inverse(n1)),inverse(n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3851,f10])).
% 247.78/31.67 fof(f3957,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(inverse(n1),add(X0,X1))=inverse(n1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3155,f3931])).
% 247.78/31.67 fof(f4055,plain,(
% 247.78/31.67 ![X0]: (multiply(add(add(n1,inverse(X0)),add(n1,inverse(X0))),multiply(add(n1,inverse(X0)),n1))=multiply(add(n1,inverse(X0)),add(inverse(X0),add(n1,inverse(X0)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3168,f381])).
% 247.78/31.67 fof(f4056,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,add(add(n1,inverse(X0)),add(n1,inverse(X0))))=add(add(n1,inverse(X0)),add(n1,inverse(X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f3168,f353])).
% 247.78/31.67 fof(f4086,plain,(
% 247.78/31.67 ![X0]: (multiply(add(add(n1,inverse(X0)),add(n1,inverse(X0))),multiply(add(n1,inverse(X0)),n1))=add(inverse(X0),multiply(add(n1,inverse(X0)),add(n1,inverse(X0)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3777,f4055])).
% 247.78/31.67 fof(f4087,plain,(
% 247.78/31.67 ![X0]: (multiply(add(add(n1,inverse(X0)),add(n1,inverse(X0))),multiply(add(n1,inverse(X0)),n1))=pixley(n1,X0,add(n1,inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f82,f4086])).
% 247.78/31.67 fof(f4561,plain,(
% 247.78/31.67 ![X0]: (multiply(inverse(n1),X0)=inverse(n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f94,f3957])).
% 247.78/31.67 fof(f4614,plain,(
% 247.78/31.67 ![X0]: (inverse(n1)=multiply(X0,inverse(X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f4561,f3625])).
% 247.78/31.67 fof(f4751,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(multiply(add(add(X0,multiply(n1,add(X1,X1))),X1),add(X2,multiply(n1,add(X1,X1)))),add(multiply(n1,add(X1,X1)),multiply(n1,add(X1,X1))))=add(multiply(n1,add(X1,X1)),multiply(X1,multiply(n1,add(X1,X1)))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f390,f70])).
% 247.78/31.67 fof(f4902,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(multiply(X0,add(add(X1,multiply(n1,add(X2,X2))),X2)),multiply(add(X2,X2),n1)),add(multiply(n1,add(X2,X2)),multiply(n1,add(X2,X2))))=add(multiply(n1,add(X2,X2)),multiply(X2,multiply(n1,add(X2,X2)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1796,f4751])).
% 247.78/31.67 fof(f4903,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(multiply(X0,add(add(X1,multiply(n1,add(X2,X2))),X2)),multiply(add(X2,X2),n1)),multiply(add(X2,X2),add(n1,n1)))=add(multiply(n1,add(X2,X2)),multiply(X2,multiply(n1,add(X2,X2)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f10,f4902])).
% 247.78/31.67 fof(f4904,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(multiply(X0,add(add(X1,multiply(n1,add(X2,X2))),X2)),multiply(add(X2,X2),n1)),multiply(add(X2,X2),n1))=add(multiply(n1,add(X2,X2)),multiply(X2,multiply(n1,add(X2,X2)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f4903])).
% 247.78/31.67 fof(f4905,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=add(multiply(n1,add(X0,X0)),multiply(X0,multiply(n1,add(X0,X0)))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f9,f4904])).
% 247.78/31.67 fof(f4906,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=multiply(multiply(n1,add(X0,X0)),add(X0,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f471,f4905])).
% 247.78/31.67 fof(f5596,plain,(
% 247.78/31.67 ![X0]: (X0=multiply(n1,add(X0,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f15,f3903])).
% 247.78/31.67 fof(f5597,plain,(
% 247.78/31.67 ![X0]: (X0=multiply(n1,add(X0,inverse(n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f14,f3903])).
% 247.78/31.67 fof(f5643,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(n1,add(X0,X0)))=X0)),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f390])).
% 247.78/31.67 fof(f5645,plain,(
% 247.78/31.67 ![X0]: (add(n1,inverse(X0))=add(add(n1,inverse(X0)),add(n1,inverse(X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f4056])).
% 247.78/31.67 fof(f5650,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=multiply(X0,add(X0,X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f4906])).
% 247.78/31.67 fof(f5662,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,inverse(X1))=multiply(multiply(inverse(X1),X0),X0))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f3175])).
% 247.78/31.67 fof(f5672,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,add(X0,X0)),add(X0,X1))=add(multiply(n1,add(X0,X0)),multiply(X1,X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f471])).
% 247.78/31.67 fof(f5673,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(n1,add(X0,X0)),add(X1,X0))=add(multiply(X1,multiply(n1,add(X0,X0))),X0))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5596,f470])).
% 247.78/31.67 fof(f5675,plain,(
% 247.78/31.67 ![X0]: (X0=add(multiply(X0,n1),inverse(n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3388,f5597])).
% 247.78/31.67 fof(f5740,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,X0)=X0)),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f5643])).
% 247.78/31.67 fof(f5741,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,inverse(X0)),multiply(add(n1,inverse(X0)),n1))=pixley(n1,X0,add(n1,inverse(X0))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5645,f4087])).
% 247.78/31.67 fof(f5767,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(X0,X1))=add(multiply(n1,add(X0,X0)),multiply(X1,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f5672])).
% 247.78/31.67 fof(f5786,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=add(X0,multiply(X0,X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5787,f5650])).
% 247.78/31.67 fof(f5787,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X1,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f5767])).
% 247.78/31.67 fof(f5788,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(X1,X0))=add(multiply(X1,multiply(n1,add(X0,X0))),X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f5673])).
% 247.78/31.67 fof(f5813,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,add(X1,X0))=add(multiply(X1,X0),X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f5788])).
% 247.78/31.67 fof(f5895,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,inverse(X0)),n1)=pixley(n1,X0,add(n1,inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f100,f5741])).
% 247.78/31.67 fof(f5929,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=add(X0,X0))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f5930,f1871])).
% 247.78/31.67 fof(f5930,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=add(X0,X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5740,f5786])).
% 247.78/31.67 fof(f5986,plain,(
% 247.78/31.67 ![X0]: (pixley(n1,X0,add(n1,inverse(X0)))=add(inverse(X0),add(n1,inverse(X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5740,f82])).
% 247.78/31.67 fof(f6021,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,inverse(X0)),n1)=add(inverse(X0),add(n1,inverse(X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5895,f5986])).
% 247.78/31.67 fof(f6027,plain,(
% 247.78/31.67 ![X0]: (multiply(add(n1,inverse(X0)),n1)=n1)),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3168,f6021])).
% 247.78/31.67 fof(f6119,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,X1)=multiply(n1,multiply(X1,add(X0,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f10,f5596])).
% 247.78/31.67 fof(f6122,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),n1)=add(add(X0,X0),X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5596,f1749])).
% 247.78/31.67 fof(f6147,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,n1))=add(multiply(X1,add(X0,X0)),X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5596,f10])).
% 247.78/31.67 fof(f6148,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(n1,X1))=add(X0,multiply(X1,add(X0,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5596,f10])).
% 247.78/31.67 fof(f6157,plain,(
% 247.78/31.67 ![X0]: (add(X0,X0)=add(add(X0,X0),X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5930,f6122])).
% 247.78/31.67 fof(f6200,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),n1)=add(multiply(X1,add(X0,X0)),X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f6147])).
% 247.78/31.67 fof(f6201,plain,(
% 247.78/31.67 ![X0,X1]: (add(X0,X0)=add(multiply(X1,add(X0,X0)),X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5930,f6200])).
% 247.78/31.67 fof(f6214,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(add(X0,X0),X0),add(X1,X0))=add(multiply(X1,add(X0,X0)),add(X0,multiply(X0,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f6157,f39])).
% 247.78/31.67 fof(f6257,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,X0))=add(multiply(X1,add(X0,X0)),add(X0,multiply(X0,X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f6157,f6214])).
% 247.78/31.67 fof(f6259,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,X0))=add(multiply(X1,add(X0,X0)),add(X0,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5740,f6257])).
% 247.78/31.67 fof(f6313,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(X0,n1),multiply(n1,X0))=multiply(n1,add(multiply(X0,n1),inverse(n1))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5675,f639])).
% 247.78/31.67 fof(f6339,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,X0)=multiply(n1,add(multiply(X0,n1),inverse(n1))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1758,f6313])).
% 247.78/31.67 fof(f6340,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,X0)=add(multiply(multiply(X0,n1),n1),inverse(n1)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f3388,f6339])).
% 247.78/31.67 fof(f6341,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,X0)=multiply(X0,n1))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5675,f6340])).
% 247.78/31.67 fof(f6418,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(multiply(X0,n1),add(multiply(X0,add(X1,n1)),X2))=add(multiply(n1,X0),multiply(X2,multiply(n1,X0))))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f6341,f37])).
% 247.78/31.67 fof(f6432,plain,(
% 247.78/31.67 ![X0]: (multiply(X0,multiply(n1,X0))=multiply(X0,n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f6341,f100])).
% 247.78/31.67 fof(f6468,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,n1),add(multiply(X0,n1),X1))=add(multiply(n1,X0),multiply(X1,multiply(n1,X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f1733,f6418])).
% 247.78/31.67 fof(f6469,plain,(
% 247.78/31.67 ![X0,X1]: (add(multiply(X0,n1),multiply(X1,multiply(X0,n1)))=add(multiply(n1,X0),multiply(X1,multiply(n1,X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5787,f6468])).
% 247.78/31.67 fof(f6470,plain,(
% 247.78/31.67 ![X0]: (multiply(multiply(n1,X0),n1)=multiply(multiply(X0,n1),add(X0,inverse(multiply(X0,n1)))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6477,f2474])).
% 247.78/31.67 fof(f6475,plain,(
% 247.78/31.67 ![X0,X1,X2]: (multiply(add(multiply(X0,n1),X1),add(multiply(n1,X0),X2))=add(multiply(multiply(X0,n1),add(X0,X1)),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6477,f2514])).
% 247.78/31.67 fof(f6477,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,n1),add(X0,X1))=add(multiply(n1,X0),multiply(X1,multiply(n1,X0))))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f99,f6469])).
% 247.78/31.67 fof(f6769,plain,(
% 247.78/31.67 ![X0]: (multiply(n1,add(X0,X0))=add(X0,X0))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f6341,f5930])).
% 247.78/31.67 fof(f6773,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,add(X1,X1)),n1)=add(multiply(X1,X0),multiply(X1,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f10,f5930])).
% 247.78/31.67 fof(f6778,plain,(
% 247.78/31.67 ![X0]: (add(X0,X0)=add(add(X0,X0),inverse(n1)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5930,f5675])).
% 247.78/31.67 fof(f6779,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),multiply(n1,add(X0,X0)))=multiply(n1,add(X0,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5930,f1758])).
% 247.78/31.67 fof(f6781,plain,(
% 247.78/31.67 ![X0]: (multiply(add(X0,X0),add(X0,X0))=multiply(add(X0,X0),n1))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5930,f100])).
% 247.78/31.67 fof(f6782,plain,(
% 247.78/31.67 ![X0]: (add(X0,X0)=add(inverse(n1),add(X0,X0)))),
% 247.78/31.67 inference(paramodulation,[status(thm)],[f5930,f94])).
% 247.78/31.67 fof(f6851,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,X0))=add(multiply(X1,add(X0,X0)),X0))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6927,f6259])).
% 247.78/31.67 fof(f6856,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(n1,X1))=add(X0,multiply(X1,X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6927,f6148])).
% 247.78/31.67 fof(f6864,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(X0,X1)=multiply(n1,multiply(X1,X0)))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6927,f6119])).
% 247.78/31.67 fof(f6867,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,X0),add(X1,multiply(X0,n1)))=X0)),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6927,f5929])).
% 247.78/31.67 fof(f6920,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(add(X0,inverse(X1)),add(X1,X1))=multiply(multiply(X1,add(X0,inverse(X1))),X0))),
% 247.78/31.67 inference(backward_demodulation,[status(thm)],[f6927,f1432])).
% 247.78/31.67 fof(f6927,plain,(
% 247.78/31.67 ![X0]: (X0=add(X0,X0))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f5596,f6769])).
% 247.78/31.67 fof(f6931,plain,(
% 247.78/31.67 ![X0,X1]: (multiply(multiply(X0,X1),n1)=add(multiply(X1,X0),multiply(X1,X0)))),
% 247.78/31.67 inference(forward_demodulation,[status(thm)],[f6927,f6773])).
% 247.78/31.67 fof(f6932,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(multiply(X0,X1),n1)=multiply(X0,add(X1,X1)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f10,f6931])).
% 247.78/31.69 fof(f6933,plain,(
% 247.78/31.69 ![X0]: (multiply(n1,X0)=multiply(multiply(X0,n1),add(X0,inverse(multiply(X0,n1)))))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f6942,f6470])).
% 247.78/31.69 fof(f6942,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(multiply(X0,X1),n1)=multiply(X0,X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6932])).
% 247.78/31.69 fof(f6949,plain,(
% 247.78/31.69 ![X0]: (X0=add(add(X0,X0),inverse(n1)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6778])).
% 247.78/31.69 fof(f6962,plain,(
% 247.78/31.69 ![X0]: (X0=add(X0,inverse(n1)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6949])).
% 247.78/31.69 fof(f6963,plain,(
% 247.78/31.69 ![X0]: (multiply(add(X0,X0),n1)=multiply(n1,add(X0,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6432,f6779])).
% 247.78/31.69 fof(f6964,plain,(
% 247.78/31.69 ![X0]: (add(X0,X0)=multiply(n1,add(X0,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f5930,f6963])).
% 247.78/31.69 fof(f6965,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(n1,add(X0,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6964])).
% 247.78/31.69 fof(f6985,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(multiply(X0,n1),X1),add(X0,X2))=add(multiply(multiply(X0,n1),add(X0,X1)),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f7017,f6475])).
% 247.78/31.69 fof(f7017,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(n1,X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6965])).
% 247.78/31.69 fof(f7022,plain,(
% 247.78/31.69 ![X0]: (add(X0,X0)=multiply(add(X0,X0),n1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f353,f6781])).
% 247.78/31.69 fof(f7023,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(add(X0,X0),n1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f7022])).
% 247.78/31.69 fof(f7031,plain,(
% 247.78/31.69 ![X0]: (add(n1,inverse(X0))=n1)),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f7118,f6027])).
% 247.78/31.69 fof(f7118,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(X0,n1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f7023])).
% 247.78/31.69 fof(f7119,plain,(
% 247.78/31.69 ![X0]: (X0=add(inverse(n1),add(X0,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6782])).
% 247.78/31.69 fof(f7127,plain,(
% 247.78/31.69 ![X0]: (X0=add(inverse(n1),X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f7119])).
% 247.78/31.69 fof(f7305,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(X1,X0))=add(multiply(X1,add(X0,X0)),X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6851])).
% 247.78/31.69 fof(f7306,plain,(
% 247.78/31.69 ![X0,X1]: (add(multiply(X0,X1),X1)=add(multiply(X0,add(X1,X1)),X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f5813,f7305])).
% 247.78/31.69 fof(f7307,plain,(
% 247.78/31.69 ![X0,X1]: (add(multiply(X0,X1),X1)=add(X1,X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6201,f7306])).
% 247.78/31.69 fof(f7311,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(add(X0,add(X1,X2)),add(X2,X3))=add(X2,multiply(X3,add(X0,add(X1,X2)))))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f7411,f46])).
% 247.78/31.69 fof(f7411,plain,(
% 247.78/31.69 ![X0,X1]: (add(multiply(X0,X1),X1)=X1)),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f7307])).
% 247.78/31.69 fof(f7420,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(n1,X1))=add(X0,multiply(X1,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6856])).
% 247.78/31.69 fof(f7440,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7017,f6864])).
% 247.78/31.69 fof(f7445,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(X1,multiply(X0,n1)))=X0)),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6867])).
% 247.78/31.69 fof(f7446,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(X1,X0))=X0)),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7445])).
% 247.78/31.69 fof(f7553,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(add(X0,inverse(X1)),X1)=multiply(multiply(X1,add(X0,inverse(X1))),X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6927,f6920])).
% 247.78/31.69 fof(f7562,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(multiply(X0,n1),add(X0,inverse(multiply(X0,n1)))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7017,f6933])).
% 247.78/31.69 fof(f7563,plain,(
% 247.78/31.69 ![X0]: (X0=multiply(X0,add(X0,inverse(multiply(X0,n1)))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7562])).
% 247.78/31.69 fof(f7564,plain,(
% 247.78/31.69 ![X0]: (X0=add(X0,multiply(inverse(multiply(X0,n1)),X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f5787,f7563])).
% 247.78/31.69 fof(f7566,plain,(
% 247.78/31.69 ![X0]: (X0=add(X0,multiply(inverse(X0),X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7564])).
% 247.78/31.69 fof(f7636,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,X1),add(X0,X2))=add(multiply(multiply(X0,n1),add(X0,X1)),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f6985])).
% 247.78/31.69 fof(f7637,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,X1),add(X0,X2))=add(multiply(X0,add(X0,X1)),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7636])).
% 247.78/31.69 fof(f7638,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,X1),add(X0,X2))=add(add(X0,multiply(X1,X0)),multiply(X2,add(multiply(X0,n1),X1))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f5787,f7637])).
% 247.78/31.69 fof(f7639,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,X1),add(X0,X2))=add(add(X0,multiply(X1,X0)),multiply(X2,add(X0,X1))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7638])).
% 247.78/31.69 fof(f7743,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(n1,X0,X1)=add(inverse(X0),multiply(X1,n1)))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f7031,f82])).
% 247.78/31.69 fof(f8178,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(n1,X0,X1)=add(inverse(X0),X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f7743])).
% 247.78/31.69 fof(f8725,plain,(
% 247.78/31.69 ![X0,X1]: (add(multiply(X0,X1),X0)=X0)),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f7440,f7411])).
% 247.78/31.69 fof(f8860,plain,(
% 247.78/31.69 ![X0,X1]: (add(add(X0,multiply(X1,X0)),X0)=X0)),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f31,f8725])).
% 247.78/31.69 fof(f9018,plain,(
% 247.78/31.69 ![X0]: (multiply(multiply(inverse(X0),X0),X0)=multiply(inverse(X0),X0))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f7566,f7446])).
% 247.78/31.69 fof(f9047,plain,(
% 247.78/31.69 ![X0]: (multiply(X0,inverse(X0))=multiply(inverse(X0),X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f5662,f9018])).
% 247.78/31.69 fof(f9052,plain,(
% 247.78/31.69 ![X0]: (inverse(n1)=multiply(inverse(X0),X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f4614,f9047])).
% 247.78/31.69 fof(f9147,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(inverse(inverse(X0)),X0,X1)=add(inverse(n1),multiply(X1,add(inverse(inverse(X0)),inverse(X0)))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f9052,f23])).
% 247.78/31.69 fof(f9166,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(X1,inverse(X0)))=add(multiply(X1,X0),inverse(n1)))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f9052,f10])).
% 247.78/31.69 fof(f9171,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(inverse(inverse(X0)),X0,X1)=multiply(X1,add(inverse(inverse(X0)),inverse(X0))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7127,f9147])).
% 247.78/31.69 fof(f9199,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,multiply(X1,add(X0,inverse(X1))))=multiply(X0,X1))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f9213,f639])).
% 247.78/31.69 fof(f9206,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(add(X0,inverse(X1)),X1)=multiply(multiply(X0,X1),X0))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f9213,f7553])).
% 247.78/31.69 fof(f9212,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(multiply(X0,add(X1,inverse(X0))),add(multiply(multiply(X0,add(X1,inverse(X0))),add(X2,X1)),X3))=multiply(multiply(X1,X0),add(X1,X3)))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f9213,f1428])).
% 247.78/31.69 fof(f9213,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,add(X1,inverse(X0)))=multiply(X1,X0))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f6962,f9166])).
% 247.78/31.69 fof(f9220,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,multiply(X0,X1))=multiply(X0,X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9213,f9199])).
% 247.78/31.69 fof(f9239,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),add(multiply(multiply(X1,add(X0,inverse(X1))),add(X2,X0)),X3))=multiply(multiply(X0,X1),add(X0,X3)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9213,f9212])).
% 247.78/31.69 fof(f9240,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),add(multiply(multiply(X0,X1),add(X2,X0)),X3))=multiply(multiply(X0,X1),add(X0,X3)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9213,f9239])).
% 247.78/31.69 fof(f9606,plain,(
% 247.78/31.69 ![X0,X1]: (add(add(X0,multiply(X0,X1)),X0)=X0)),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f7440,f8860])).
% 247.78/31.69 fof(f9734,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(multiply(X0,X1),add(multiply(multiply(X0,X1),add(X2,X0)),X3))=add(multiply(X0,multiply(X0,X1)),multiply(X3,multiply(X0,multiply(X0,X1)))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f9220,f37])).
% 247.78/31.69 fof(f9736,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X2,X0))=add(multiply(X2,multiply(X0,X1)),multiply(X0,X1)))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f9220,f10])).
% 247.78/31.69 fof(f9775,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X0,X2))=add(multiply(X0,multiply(X0,X1)),multiply(X2,multiply(X0,multiply(X0,X1)))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9240,f9734])).
% 247.78/31.69 fof(f9776,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X0,X2))=add(multiply(X0,X1),multiply(X2,multiply(X0,multiply(X0,X1)))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9220,f9775])).
% 247.78/31.69 fof(f9811,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X0,X2))=add(multiply(X0,X1),multiply(X2,multiply(X0,X1))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9220,f9776])).
% 247.78/31.69 fof(f9819,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X2,X0))=multiply(X0,X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7411,f9736])).
% 247.78/31.69 fof(f9874,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(multiply(X0,X1),X0)=add(multiply(X0,X1),multiply(X0,multiply(X0,X1))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f9606,f31])).
% 247.78/31.69 fof(f9934,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(multiply(X0,X1),add(X0,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9811,f9874])).
% 247.78/31.69 fof(f9943,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(add(X0,inverse(X1)),X1)=multiply(X0,X1))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f9944,f9206])).
% 247.78/31.69 fof(f9944,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(multiply(X0,X1),X0)=multiply(X0,X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f9819,f9934])).
% 247.78/31.69 fof(f11141,plain,(
% 247.78/31.69 ![X0]: (n1=add(inverse(X0),X0))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f14,f8178])).
% 247.78/31.69 fof(f11157,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(inverse(inverse(X0)),X0,X1)=multiply(X1,n1))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11141,f9171])).
% 247.78/31.69 fof(f11171,plain,(
% 247.78/31.69 ![X0,X1]: (pixley(inverse(inverse(X0)),X0,X1)=X1)),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f11157])).
% 247.78/31.69 fof(f11198,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(add(inverse(X0),X0),X1),add(X0,X2))=add(add(X0,multiply(X1,X0)),multiply(X2,add(n1,X1))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11141,f40])).
% 247.78/31.69 fof(f11233,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(n1,X0),add(X1,X2))=add(add(X1,multiply(X0,X1)),multiply(X2,add(n1,X0))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f11141,f11198])).
% 247.78/31.69 fof(f11241,plain,(
% 247.78/31.69 ![X0]: (inverse(inverse(X0))=X0)),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f14,f11171])).
% 247.78/31.69 fof(f11486,plain,(
% 247.78/31.69 ![X0]: (add(n1,X0)=n1)),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11241,f7031])).
% 247.78/31.69 fof(f11506,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(n1,X0),add(X1,X2))=add(add(X1,multiply(X0,X1)),multiply(X2,n1)))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11486,f11233])).
% 247.78/31.69 fof(f11518,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(X0,n1)=add(X0,multiply(X1,X0)))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11486,f7420])).
% 247.78/31.69 fof(f11577,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(n1,add(X0,X1))=add(add(X0,multiply(X2,X0)),multiply(X1,n1)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f11486,f11506])).
% 247.78/31.69 fof(f11578,plain,(
% 247.78/31.69 ![X0,X1,X2]: (add(X0,X1)=add(add(X0,multiply(X2,X0)),multiply(X1,n1)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7017,f11577])).
% 247.78/31.69 fof(f11579,plain,(
% 247.78/31.69 ![X0,X1,X2,X3]: (multiply(add(add(X0,X1),X2),add(X1,X3))=add(X1,multiply(X3,add(add(X0,X1),X2))))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11597,f40])).
% 247.78/31.69 fof(f11595,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,X1),add(X0,X2))=add(X0,multiply(X2,add(X0,X1))))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11597,f7639])).
% 247.78/31.69 fof(f11597,plain,(
% 247.78/31.69 ![X0,X1,X2]: (add(X0,X1)=add(add(X0,multiply(X2,X0)),X1))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f11578])).
% 247.78/31.69 fof(f11631,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(multiply(X0,X1),add(X0,X2))=multiply(X0,X1))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11672,f9811])).
% 247.78/31.69 fof(f11672,plain,(
% 247.78/31.69 ![X0,X1]: (X0=add(X0,multiply(X1,X0)))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f11518])).
% 247.78/31.69 fof(f11823,plain,(
% 247.78/31.69 ~add(a,multiply(b,c))=add(a,multiply(c,add(a,b)))),
% 247.78/31.69 inference(backward_demodulation,[status(thm)],[f11595,f16])).
% 247.78/31.69 fof(f12885,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(X0,add(X1,X2)),n1)=add(X2,multiply(inverse(X2),add(X0,add(X1,X2)))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11,f7311])).
% 247.78/31.69 fof(f12987,plain,(
% 247.78/31.69 ![X0,X1,X2]: (add(X0,add(X1,X2))=add(X2,multiply(inverse(X2),add(X0,add(X1,X2)))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f12885])).
% 247.78/31.69 fof(f14253,plain,(
% 247.78/31.69 ![X0,X1]: (multiply(add(X0,X1),inverse(X1))=multiply(X0,inverse(X1)))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11241,f9943])).
% 247.78/31.69 fof(f15394,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(add(add(X0,X1),X2),n1)=add(X1,multiply(inverse(X1),add(add(X0,X1),X2))))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11,f11579])).
% 247.78/31.69 fof(f15513,plain,(
% 247.78/31.69 ![X0,X1,X2]: (add(add(X0,X1),X2)=add(X1,multiply(inverse(X1),add(add(X0,X1),X2))))),
% 247.78/31.69 inference(forward_demodulation,[status(thm)],[f7118,f15394])).
% 247.78/31.69 fof(f19644,plain,(
% 247.78/31.69 ![X0,X1,X2]: (add(X0,X1)=add(add(X0,X1),multiply(X0,X2)))),
% 247.78/31.69 inference(paramodulation,[status(thm)],[f11631,f11672])).
% 247.78/31.69 fof(f56447,plain,(
% 247.78/31.69 ![X0,X1,X2]: (multiply(inverse(X0),add(X1,add(X2,X0)))=add(multiply(X1,inverse(X0)),multiply(X2,inverse(X0))))),
% 149.48/33.17 inference(paramodulation,[status(thm)],[f14253,f10])).
% 149.48/33.17 fof(f56448,plain,(
% 149.48/33.17 ![X0,X1,X2]: (multiply(inverse(X0),add(add(X1,X0),X2))=add(multiply(X1,inverse(X0)),multiply(X2,inverse(X0))))),
% 149.48/33.17 inference(paramodulation,[status(thm)],[f14253,f10])).
% 149.48/33.17 fof(f56544,plain,(
% 149.48/33.17 ![X0,X1,X2]: (add(X0,add(X1,X2))=add(X2,multiply(inverse(X2),add(X0,X1))))),
% 149.48/33.17 inference(backward_demodulation,[status(thm)],[f56545,f12987])).
% 149.48/33.17 fof(f56545,plain,(
% 149.48/33.17 ![X0,X1,X2]: (multiply(inverse(X0),add(X1,add(X2,X0)))=multiply(inverse(X0),add(X1,X2)))),
% 149.48/33.17 inference(forward_demodulation,[status(thm)],[f10,f56447])).
% 149.48/33.17 fof(f56546,plain,(
% 149.48/33.17 ![X0,X1,X2]: (add(add(X0,X1),X2)=add(X1,multiply(inverse(X1),add(X0,X2))))),
% 149.48/33.17 inference(backward_demodulation,[status(thm)],[f56548,f15513])).
% 149.48/33.17 fof(f56548,plain,(
% 149.48/33.17 ![X0,X1,X2]: (multiply(inverse(X0),add(add(X1,X0),X2))=multiply(inverse(X0),add(X1,X2)))),
% 149.48/33.17 inference(forward_demodulation,[status(thm)],[f10,f56448])).
% 149.48/33.17 fof(f56562,plain,(
% 149.48/33.17 ![X0,X1,X2]: (add(X0,X1)=add(X0,add(multiply(X0,X2),X1)))),
% 149.48/33.17 inference(backward_demodulation,[status(thm)],[f57642,f19644])).
% 149.48/33.17 fof(f57642,plain,(
% 149.48/33.17 ![X0,X1,X2]: (add(add(X0,X1),X2)=add(X0,add(X2,X1)))),
% 149.48/33.17 inference(forward_demodulation,[status(thm)],[f56544,f56546])).
% 149.48/33.17 fof(f78879,plain,(
% 149.48/33.17 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=add(X0,multiply(X2,add(X0,X1))))),
% 149.48/33.17 inference(paramodulation,[status(thm)],[f10,f56562])).
% 149.48/33.17 fof(f79151,plain,(
% 149.48/33.17 ~add(a,multiply(b,c))=add(a,multiply(b,c))),
% 149.48/33.17 inference(backward_demodulation,[status(thm)],[f78879,f11823])).
% 149.48/33.17 fof(f79383,plain,(
% 149.48/33.17 $false),
% 149.48/33.17 inference(trivial_equality_resolution,[status(thm)],[f79151])).
% 149.48/33.17 % SZS output end CNFRefutation for theBenchmark.p
% 149.48/33.17 % Elapsed time: 32.577075 seconds
% 149.48/33.17 % CPU time: 117.778220 seconds
% 149.48/33.17 % Total memory used: 720.000 MB
% 149.48/33.17 % Net memory used: 685.779 MB
%------------------------------------------------------------------------------