%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO007-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:43 PM UTC 2026
% Result : Unsatisfiable 0.21s 1.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO007-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n004.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 13:47:04 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 0.21/1.15 % Refutation found
% 0.21/1.15 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/1.15 % SZS output start CNFRefutation for theBenchmark
% 0.21/1.15 fof(f1,axiom,(
% 0.21/1.15 (![X,Y]: (add(X,Y) = add(Y,X) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f2,axiom,(
% 0.21/1.15 (![X,Y]: (multiply(X,Y) = multiply(Y,X) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f3,axiom,(
% 0.21/1.15 (![X,Y,Z]: (add(multiply(X,Y),Z) = multiply(add(X,Z),add(Y,Z)) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f4,axiom,(
% 0.21/1.15 (![X,Y,Z]: (add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f5,axiom,(
% 0.21/1.15 (![X,Y,Z]: (multiply(add(X,Y),Z) = add(multiply(X,Z),multiply(Y,Z)) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f6,axiom,(
% 0.21/1.15 (![X,Y,Z]: (multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f7,axiom,(
% 0.21/1.15 (![X]: (add(X,inverse(X)) = multiplicative_identity ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f11,axiom,(
% 0.21/1.15 (![X]: (multiply(X,multiplicative_identity) = X ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f12,axiom,(
% 0.21/1.15 (![X]: (multiply(multiplicative_identity,X) = X ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f13,axiom,(
% 0.21/1.15 (![X]: (add(X,additive_identity) = X ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f14,axiom,(
% 0.21/1.15 (![X]: (add(additive_identity,X) = X ))),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f15,negated_conjecture,(
% 0.21/1.15 multiply(a,multiply(b,c)) != multiply(multiply(a,b),c) ),
% 0.21/1.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/1.15 fof(f16,plain,(
% 0.21/1.15 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 0.21/1.15 inference(cnf_transformation,[status(thm)],[f1])).
% 0.21/1.15 fof(f17,plain,(
% 0.21/1.15 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.21/1.15 inference(cnf_transformation,[status(thm)],[f2])).
% 0.21/1.15 fof(f18,plain,(
% 0.21/1.15 ![X0,X1,X2]: (add(multiply(X0,X1),X2)=multiply(add(X0,X2),add(X1,X2)))),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f3])).
% 0.21/1.16 fof(f19,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X1),add(X0,X2)))),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f4])).
% 0.21/1.16 fof(f20,plain,(
% 0.21/1.16 ![X0,X1,X2]: (multiply(add(X0,X1),X2)=add(multiply(X0,X2),multiply(X1,X2)))),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f5])).
% 0.21/1.16 fof(f21,plain,(
% 0.21/1.16 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X0,X1),multiply(X0,X2)))),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f6])).
% 0.21/1.16 fof(f22,plain,(
% 0.21/1.16 ![X0]: (add(X0,inverse(X0))=multiplicative_identity)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f7])).
% 0.21/1.16 fof(f26,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,multiplicative_identity)=X0)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f11])).
% 0.21/1.16 fof(f27,plain,(
% 0.21/1.16 ![X0]: (multiply(multiplicative_identity,X0)=X0)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f12])).
% 0.21/1.16 fof(f28,plain,(
% 0.21/1.16 ![X0]: (add(X0,additive_identity)=X0)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f13])).
% 0.21/1.16 fof(f29,plain,(
% 0.21/1.16 ![X0]: (add(additive_identity,X0)=X0)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f14])).
% 0.21/1.16 fof(f30,plain,(
% 0.21/1.16 ~multiply(a,multiply(b,c))=multiply(multiply(a,b),c)),
% 0.21/1.16 inference(cnf_transformation,[status(thm)],[f15])).
% 0.21/1.16 fof(f31,definition,(
% 0.21/1.16 sF1_fnc=multiply(b,c)),
% 0.21/1.16 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.21/1.16 fof(f32,definition,(
% 0.21/1.16 sF0_fnc=multiply(a,sF1_fnc)),
% 0.21/1.16 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.21/1.16 fof(f33,definition,(
% 0.21/1.16 sF3_fnc=multiply(a,b)),
% 0.21/1.16 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.21/1.16 fof(f34,definition,(
% 0.21/1.16 sF2_fnc=multiply(sF3_fnc,c)),
% 0.21/1.16 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.21/1.16 fof(f35,plain,(
% 0.21/1.16 ~sF0_fnc=sF2_fnc),
% 0.21/1.16 inference(definition_folding,[],[f30,f34,f33,f32,f31])).
% 0.21/1.16 fof(f38,plain,(
% 0.21/1.16 sF2_fnc=multiply(c,sF3_fnc)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f34])).
% 0.21/1.16 fof(f75,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(multiply(X0,X1),X2)=multiply(add(X1,X2),add(X0,X2)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f17,f18])).
% 0.21/1.16 fof(f77,plain,(
% 0.21/1.16 ![X0,X1]: (add(multiply(additive_identity,X0),X1)=multiply(X1,add(X0,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f29,f18])).
% 0.21/1.16 fof(f82,plain,(
% 0.21/1.16 ![X0,X1]: (add(multiply(X0,additive_identity),X1)=multiply(add(X0,X1),X1))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f29,f18])).
% 0.21/1.16 fof(f92,plain,(
% 0.21/1.16 ![X0,X1]: (add(multiply(X0,additive_identity),X1)=multiply(X1,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f82])).
% 0.21/1.16 fof(f96,plain,(
% 0.21/1.16 ![X0]: (add(multiply(X0,additive_identity),multiplicative_identity)=add(X0,multiplicative_identity))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f27,f92])).
% 0.21/1.16 fof(f97,plain,(
% 0.21/1.16 ![X0]: (add(multiply(additive_identity,additive_identity),X0)=multiply(X0,X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f29,f92])).
% 0.21/1.16 fof(f100,plain,(
% 0.21/1.16 ![X0,X1]: (add(multiply(X0,additive_identity),X1)=multiply(X1,add(X1,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f16,f92])).
% 0.21/1.16 fof(f103,plain,(
% 0.21/1.16 ![X0]: (add(multiplicative_identity,multiply(X0,additive_identity))=add(X0,multiplicative_identity))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f96])).
% 0.21/1.16 fof(f110,plain,(
% 0.21/1.16 ![X0]: (add(multiplicative_identity,multiply(additive_identity,X0))=add(X0,multiplicative_identity))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f17,f103])).
% 0.21/1.16 fof(f134,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(multiply(X0,X1),X2)=add(multiply(X1,X0),X2))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f18,f75])).
% 0.21/1.16 fof(f174,plain,(
% 0.21/1.16 ![X0]: (add(X0,multiply(additive_identity,additive_identity))=multiply(X0,X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f16,f97])).
% 0.21/1.16 fof(f199,plain,(
% 0.21/1.16 ![X0]: (add(multiply(multiplicative_identity,additive_identity),multiply(additive_identity,X0))=multiply(multiply(additive_identity,X0),add(X0,multiplicative_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f110,f92])).
% 0.21/1.16 fof(f213,plain,(
% 0.21/1.16 ![X0]: (add(additive_identity,multiply(additive_identity,X0))=multiply(multiply(additive_identity,X0),add(X0,multiplicative_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f27,f199])).
% 0.21/1.16 fof(f214,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(multiply(additive_identity,X0),add(X0,multiplicative_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f213])).
% 0.21/1.16 fof(f215,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(add(X0,multiplicative_identity),multiply(additive_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f214])).
% 0.21/1.16 fof(f254,plain,(
% 0.21/1.16 ![X0]: (add(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,X0))=multiply(multiply(additive_identity,X0),add(X0,multiplicative_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f110,f77])).
% 0.21/1.16 fof(f269,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(multiplicative_identity,X0))=multiply(multiply(additive_identity,X0),add(X0,multiplicative_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f21,f254])).
% 0.21/1.16 fof(f270,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(multiplicative_identity,X0))=multiply(add(X0,multiplicative_identity),multiply(additive_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f269])).
% 0.21/1.16 fof(f272,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(multiplicative_identity,X0))=multiply(additive_identity,X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f215,f270])).
% 0.21/1.16 fof(f289,plain,(
% 0.21/1.16 add(multiply(additive_identity,multiplicative_identity),additive_identity)=multiply(additive_identity,additive_identity)),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f77,f272])).
% 0.21/1.16 fof(f292,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(X0,multiplicative_identity))=multiply(additive_identity,multiply(additive_identity,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f110,f272])).
% 0.21/1.16 fof(f293,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(X0,multiplicative_identity))=multiply(additive_identity,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f103,f272])).
% 0.21/1.16 fof(f297,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(X0,multiplicative_identity))=multiply(additive_identity,X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f16,f272])).
% 0.21/1.16 fof(f302,plain,(
% 0.21/1.16 multiply(additive_identity,multiplicative_identity)=multiply(additive_identity,additive_identity)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f289])).
% 0.21/1.16 fof(f303,plain,(
% 0.21/1.16 ![X0]: (add(X0,additive_identity)=multiply(X0,X0))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f318,f174])).
% 0.21/1.16 fof(f318,plain,(
% 0.21/1.16 additive_identity=multiply(additive_identity,additive_identity)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f26,f302])).
% 0.21/1.16 fof(f329,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(additive_identity,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f297,f293])).
% 0.21/1.16 fof(f330,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(additive_identity,multiply(additive_identity,X0)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f297,f292])).
% 0.21/1.16 fof(f338,plain,(
% 0.21/1.16 ![X0]: (X0=multiply(X0,X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f303])).
% 0.21/1.16 fof(f502,plain,(
% 0.21/1.16 ![X0]: (add(multiply(X0,additive_identity),multiplicative_identity)=add(multiplicative_identity,X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f27,f100])).
% 0.21/1.16 fof(f516,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(additive_identity,X0))=multiply(additive_identity,add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f330])).
% 0.21/1.16 fof(f530,plain,(
% 0.21/1.16 ![X0]: (add(multiplicative_identity,multiply(X0,additive_identity))=add(multiplicative_identity,X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f502])).
% 0.21/1.16 fof(f560,plain,(
% 0.21/1.16 ![X0]: (add(multiply(X0,additive_identity),additive_identity)=multiply(additive_identity,add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f100,f516])).
% 0.21/1.16 fof(f561,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=multiply(additive_identity,add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f560])).
% 0.21/1.16 fof(f562,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=add(multiply(additive_identity,multiply(X0,additive_identity)),additive_identity))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f77,f561])).
% 0.21/1.16 fof(f563,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=multiply(additive_identity,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f562])).
% 0.21/1.16 fof(f659,plain,(
% 0.21/1.16 ![X0]: (add(multiply(additive_identity,multiplicative_identity),multiply(X0,additive_identity))=multiply(multiply(X0,additive_identity),add(multiplicative_identity,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f530,f77])).
% 0.21/1.16 fof(f674,plain,(
% 0.21/1.16 ![X0]: (add(multiply(multiplicative_identity,additive_identity),multiply(X0,additive_identity))=multiply(multiply(X0,additive_identity),add(multiplicative_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f134,f659])).
% 0.21/1.16 fof(f675,plain,(
% 0.21/1.16 ![X0]: (multiply(add(multiplicative_identity,X0),additive_identity)=multiply(multiply(X0,additive_identity),add(multiplicative_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f20,f674])).
% 0.21/1.16 fof(f676,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(multiplicative_identity,X0))=multiply(multiply(X0,additive_identity),add(multiplicative_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f675])).
% 0.21/1.16 fof(f677,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(multiply(X0,additive_identity),add(multiplicative_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f272,f676])).
% 0.21/1.16 fof(f678,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(add(multiplicative_identity,X0),multiply(X0,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f677])).
% 0.21/1.16 fof(f851,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X2),add(X0,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f17,f19])).
% 0.21/1.16 fof(f877,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X1,inverse(X0)))=multiply(add(X0,X1),multiplicative_identity))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f22,f19])).
% 0.21/1.16 fof(f878,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X1,additive_identity))=multiply(add(X0,X1),X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f28,f19])).
% 0.21/1.16 fof(f879,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=multiply(add(X0,X1),add(X2,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f16,f19])).
% 0.21/1.16 fof(f929,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X1,inverse(X0)))=add(X0,X1))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f26,f877])).
% 0.21/1.16 fof(f930,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X1,additive_identity))=multiply(X0,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f878])).
% 0.21/1.16 fof(f940,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(additive_identity,X0),multiply(X1,additive_identity))=add(multiply(additive_identity,X1),multiply(X0,multiply(X1,additive_identity))))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f329,f20])).
% 0.21/1.16 fof(f946,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(multiplicative_identity,X0),X1)=add(X1,multiply(X0,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f27,f20])).
% 0.21/1.16 fof(f947,plain,(
% 0.21/1.16 ![X0]: (multiply(add(c,X0),sF3_fnc)=add(sF2_fnc,multiply(X0,sF3_fnc)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f38,f20])).
% 0.21/1.16 fof(f948,plain,(
% 0.21/1.16 ![X0]: (multiply(add(a,X0),b)=add(sF3_fnc,multiply(X0,b)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f33,f20])).
% 0.21/1.16 fof(f949,plain,(
% 0.21/1.16 ![X0]: (multiply(add(a,X0),sF1_fnc)=add(sF0_fnc,multiply(X0,sF1_fnc)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f32,f20])).
% 0.21/1.16 fof(f950,plain,(
% 0.21/1.16 ![X0]: (multiply(add(b,X0),c)=add(sF1_fnc,multiply(X0,c)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f31,f20])).
% 0.21/1.16 fof(f957,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),X0)=add(X0,multiply(X1,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f338,f20])).
% 0.21/1.16 fof(f962,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,additive_identity),multiply(X1,additive_identity))=add(multiply(X0,multiply(X1,additive_identity)),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f563,f20])).
% 0.21/1.16 fof(f969,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,multiplicative_identity),X1)=add(multiply(X0,X1),X1))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f27,f20])).
% 0.21/1.16 fof(f970,plain,(
% 0.21/1.16 ![X0]: (multiply(add(X0,c),sF3_fnc)=add(multiply(X0,sF3_fnc),sF2_fnc))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f38,f20])).
% 0.21/1.16 fof(f971,plain,(
% 0.21/1.16 ![X0]: (multiply(add(X0,a),b)=add(multiply(X0,b),sF3_fnc))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f33,f20])).
% 0.21/1.16 fof(f980,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),X1)=add(multiply(X0,X1),X1))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f338,f20])).
% 0.21/1.16 fof(f997,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=add(multiply(additive_identity,X1),multiply(X0,multiply(X1,additive_identity))))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f940])).
% 0.21/1.16 fof(f1002,plain,(
% 0.21/1.16 ![X0]: (multiply(sF3_fnc,add(c,X0))=add(sF2_fnc,multiply(X0,sF3_fnc)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f947])).
% 0.21/1.16 fof(f1003,plain,(
% 0.21/1.16 ![X0]: (multiply(b,add(a,X0))=add(sF3_fnc,multiply(X0,b)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f948])).
% 0.21/1.16 fof(f1004,plain,(
% 0.21/1.16 ![X0]: (multiply(sF1_fnc,add(a,X0))=add(sF0_fnc,multiply(X0,sF1_fnc)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f949])).
% 0.21/1.16 fof(f1005,plain,(
% 0.21/1.16 ![X0]: (multiply(c,add(b,X0))=add(sF1_fnc,multiply(X0,c)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f950])).
% 0.21/1.16 fof(f1017,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X1,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f957])).
% 0.21/1.16 fof(f1023,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=add(multiply(X0,multiply(X1,additive_identity)),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f962])).
% 0.21/1.16 fof(f1024,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=add(multiply(X1,additive_identity),multiply(X0,multiply(X1,additive_identity))))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1023])).
% 0.21/1.16 fof(f1025,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(X0,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f1026,f678])).
% 0.21/1.16 fof(f1026,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=multiply(add(multiplicative_identity,X0),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f946,f1024])).
% 0.21/1.16 fof(f1033,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,multiplicative_identity),X1)=add(X1,multiply(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f969])).
% 0.21/1.16 fof(f1034,plain,(
% 0.21/1.16 ![X0]: (multiply(sF3_fnc,add(X0,c))=add(multiply(X0,sF3_fnc),sF2_fnc))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f970])).
% 0.21/1.16 fof(f1035,plain,(
% 0.21/1.16 ![X0]: (multiply(sF3_fnc,add(X0,c))=add(sF2_fnc,multiply(X0,sF3_fnc)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1034])).
% 0.21/1.16 fof(f1036,plain,(
% 0.21/1.16 ![X0]: (multiply(b,add(X0,a))=add(multiply(X0,b),sF3_fnc))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f971])).
% 0.21/1.16 fof(f1037,plain,(
% 0.21/1.16 ![X0]: (multiply(b,add(X0,a))=add(sF3_fnc,multiply(X0,b)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1036])).
% 0.21/1.16 fof(f1056,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X1,X0))=add(multiply(X1,X0),X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f980])).
% 0.21/1.16 fof(f1057,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X1,X0))=add(X0,multiply(X1,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1056])).
% 0.21/1.16 fof(f1071,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(add(X0,multiplicative_identity),X1))=add(multiply(additive_identity,X0),multiply(additive_identity,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f297,f21])).
% 0.21/1.16 fof(f1086,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X0,X1))=add(X0,multiply(X0,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f338,f21])).
% 0.21/1.16 fof(f1087,plain,(
% 0.21/1.16 ![X0,X1,X2]: (multiply(X0,add(X1,X2))=add(multiply(X1,X0),multiply(X0,X2)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f17,f21])).
% 0.21/1.16 fof(f1094,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(X0,add(X1,multiplicative_identity)))=add(multiply(additive_identity,X0),multiply(additive_identity,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f297,f21])).
% 0.21/1.16 fof(f1108,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X1,multiplicative_identity))=add(multiply(X0,X1),X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f26,f21])).
% 0.21/1.16 fof(f1131,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(add(X0,multiplicative_identity),X1))=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f21,f1071])).
% 0.21/1.16 fof(f1143,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(X0,add(X1,multiplicative_identity)))=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f21,f1094])).
% 0.21/1.16 fof(f1154,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X1,multiplicative_identity))=add(X0,multiply(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1108])).
% 0.21/1.16 fof(f1159,plain,(
% 0.21/1.16 add(multiply(c,additive_identity),sF3_fnc)=add(sF2_fnc,multiply(sF3_fnc,sF3_fnc))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f1035])).
% 0.21/1.16 fof(f1168,plain,(
% 0.21/1.16 add(sF3_fnc,multiply(c,additive_identity))=add(sF2_fnc,multiply(sF3_fnc,sF3_fnc))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1159])).
% 0.21/1.16 fof(f1169,plain,(
% 0.21/1.16 add(sF3_fnc,multiply(c,additive_identity))=add(sF2_fnc,sF3_fnc)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f338,f1168])).
% 0.21/1.16 fof(f1206,plain,(
% 0.21/1.16 add(multiply(additive_identity,sF3_fnc),multiply(c,additive_identity))=multiply(multiply(c,additive_identity),add(sF2_fnc,sF3_fnc))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1169,f77])).
% 0.21/1.16 fof(f1219,plain,(
% 0.21/1.16 add(multiply(c,additive_identity),multiply(additive_identity,sF3_fnc))=multiply(multiply(c,additive_identity),add(sF2_fnc,sF3_fnc))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1206])).
% 0.21/1.16 fof(f1220,plain,(
% 0.21/1.16 multiply(additive_identity,add(c,sF3_fnc))=multiply(multiply(c,additive_identity),add(sF2_fnc,sF3_fnc))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f1087,f1219])).
% 0.21/1.16 fof(f1221,plain,(
% 0.21/1.16 multiply(additive_identity,add(c,sF3_fnc))=multiply(add(sF2_fnc,sF3_fnc),multiply(c,additive_identity))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f1220])).
% 0.21/1.16 fof(f1230,plain,(
% 0.21/1.16 add(multiply(a,additive_identity),b)=add(sF3_fnc,multiply(b,b))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f1037])).
% 0.21/1.16 fof(f1239,plain,(
% 0.21/1.16 add(b,multiply(a,additive_identity))=add(sF3_fnc,multiply(b,b))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1230])).
% 0.21/1.16 fof(f1240,plain,(
% 0.21/1.16 add(b,multiply(a,additive_identity))=add(sF3_fnc,b)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f338,f1239])).
% 0.21/1.16 fof(f1241,plain,(
% 0.21/1.16 add(b,multiply(a,additive_identity))=add(b,sF3_fnc)),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1240])).
% 0.21/1.16 fof(f1278,plain,(
% 0.21/1.16 ![X0]: (add(b,multiply(X0,multiply(a,additive_identity)))=multiply(add(b,X0),add(b,sF3_fnc)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1241,f19])).
% 0.21/1.16 fof(f1287,plain,(
% 0.21/1.16 ![X0]: (add(b,multiply(X0,multiply(a,additive_identity)))=add(b,multiply(X0,sF3_fnc)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f19,f1278])).
% 0.21/1.16 fof(f1341,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,X0)=multiply(X0,multiply(additive_identity,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f17,f1025])).
% 0.21/1.16 fof(f1353,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),multiply(X1,additive_identity))=add(multiply(X0,multiply(X1,additive_identity)),multiply(additive_identity,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1025,f20])).
% 0.21/1.16 fof(f1366,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),multiply(X1,additive_identity))=add(multiply(additive_identity,X1),multiply(X0,multiply(X1,additive_identity))))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1353])).
% 0.21/1.16 fof(f1367,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),multiply(X1,additive_identity))=multiply(X0,multiply(X1,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f997,f1366])).
% 0.21/1.16 fof(f1384,plain,(
% 0.21/1.16 ![X0]: (multiply(additive_identity,add(additive_identity,X0))=multiply(add(additive_identity,X0),add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f1341])).
% 0.21/1.16 fof(f1422,plain,(
% 0.21/1.16 ![X0]: (add(multiply(X0,additive_identity),additive_identity)=multiply(add(additive_identity,X0),add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f100,f1384])).
% 0.21/1.16 fof(f1423,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=multiply(add(additive_identity,X0),add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f1422])).
% 0.21/1.16 fof(f1424,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=add(additive_identity,multiply(X0,multiply(X0,additive_identity))))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f879,f1423])).
% 0.21/1.16 fof(f1425,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,additive_identity)=multiply(X0,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f1424])).
% 0.21/1.16 fof(f1474,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(add(X0,X1),multiply(X1,additive_identity))=add(multiply(X0,multiply(X1,additive_identity)),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1425,f20])).
% 0.21/1.16 fof(f1487,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=add(multiply(X0,multiply(X1,additive_identity)),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f1367,f1474])).
% 0.21/1.16 fof(f1488,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=add(multiply(X1,additive_identity),multiply(X0,multiply(X1,additive_identity))))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1487])).
% 0.21/1.16 fof(f1489,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=multiply(add(X0,multiplicative_identity),multiply(X1,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f1033,f1488])).
% 0.21/1.16 fof(f1673,plain,(
% 0.21/1.16 ![X0]: (add(multiply(X0,additive_identity),X0)=add(X0,multiply(X0,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f1057])).
% 0.21/1.16 fof(f1691,plain,(
% 0.21/1.16 ![X0]: (multiply(X0,X0)=add(X0,multiply(additive_identity,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f29,f1057])).
% 0.21/1.16 fof(f1719,plain,(
% 0.21/1.16 ![X0]: (add(X0,multiply(X0,additive_identity))=add(X0,multiply(X0,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f1673])).
% 0.21/1.16 fof(f1720,plain,(
% 0.21/1.16 ![X0]: (add(X0,multiply(X0,additive_identity))=add(X0,X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f338,f1719])).
% 0.21/1.16 fof(f1801,plain,(
% 0.21/1.16 ![X0]: (X0=add(X0,multiply(additive_identity,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f338,f1691])).
% 0.21/1.16 fof(f1911,plain,(
% 0.21/1.16 ![X0]: (add(additive_identity,X0)=add(add(additive_identity,X0),add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f100,f1801])).
% 0.21/1.16 fof(f1962,plain,(
% 0.21/1.16 ![X0]: (X0=add(add(additive_identity,X0),add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f1911])).
% 0.21/1.16 fof(f1963,plain,(
% 0.21/1.16 ![X0]: (X0=add(X0,add(multiply(X0,additive_identity),additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f1962])).
% 0.21/1.16 fof(f1964,plain,(
% 0.21/1.16 ![X0]: (X0=add(X0,X0))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f1965,f1720])).
% 0.21/1.16 fof(f1965,plain,(
% 0.21/1.16 ![X0]: (X0=add(X0,multiply(X0,additive_identity)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f28,f1963])).
% 0.21/1.16 fof(f2030,plain,(
% 0.21/1.16 ![X0,X1]: (add(multiply(X0,X1),X0)=multiply(add(X1,X0),X0))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1964,f75])).
% 0.21/1.16 fof(f2051,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(add(X1,X0),X0))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f16,f2030])).
% 0.21/1.16 fof(f2052,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X0,X1))=multiply(X0,add(X1,X0)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f17,f2051])).
% 0.21/1.16 fof(f2311,plain,(
% 0.21/1.16 ![X0,X1,X2]: (add(X0,multiply(X1,X2))=add(X0,multiply(X2,X1)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f19,f851])).
% 0.21/1.16 fof(f2467,plain,(
% 0.21/1.16 ![X0,X1]: (add(X0,multiply(X1,additive_identity))=add(X0,multiply(X1,X0)))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f1017,f930])).
% 0.21/1.16 fof(f2641,plain,(
% 0.21/1.16 ![X0]: (add(X0,inverse(X0))=add(X0,multiplicative_identity))),
% 0.21/1.16 inference(paramodulation,[status(thm)],[f27,f929])).
% 0.21/1.16 fof(f2681,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=multiply(multiplicative_identity,multiply(X1,additive_identity)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2694,f1489])).
% 0.21/1.16 fof(f2682,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiplicative_identity)=add(X0,multiply(X0,X1)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2694,f1154])).
% 0.21/1.16 fof(f2683,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(X0,multiplicative_identity))=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2694,f1143])).
% 0.21/1.16 fof(f2684,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,add(multiplicative_identity,X0))=multiply(additive_identity,add(X1,X0)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2694,f1131])).
% 0.21/1.16 fof(f2685,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(multiplicative_identity,X0)=add(X0,multiply(X1,X0)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2694,f1033])).
% 0.21/1.16 fof(f2694,plain,(
% 0.21/1.16 ![X0]: (multiplicative_identity=add(X0,multiplicative_identity))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f22,f2641])).
% 0.21/1.16 fof(f2774,plain,(
% 0.21/1.16 multiply(additive_identity,add(c,sF3_fnc))=multiply(c,additive_identity)),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2782,f1221])).
% 0.21/1.16 fof(f2777,plain,(
% 0.21/1.16 ![X0]: (add(b,multiply(a,additive_identity))=add(b,multiply(X0,sF3_fnc)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2782,f1287])).
% 0.21/1.16 fof(f2782,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,multiply(X1,additive_identity))=multiply(X1,additive_identity))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f27,f2681])).
% 0.21/1.16 fof(f2785,plain,(
% 0.21/1.16 ![X0,X1]: (X0=multiply(X0,add(X1,X0)))),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2787,f2052])).
% 0.21/1.16 fof(f2786,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(X0,add(X0,X1))=X0)),
% 0.21/1.16 inference(backward_demodulation,[status(thm)],[f2787,f1086])).
% 0.21/1.16 fof(f2787,plain,(
% 0.21/1.16 ![X0,X1]: (X0=add(X0,multiply(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f26,f2682])).
% 0.21/1.16 fof(f2788,plain,(
% 0.21/1.16 ![X0,X1]: (add(additive_identity,multiply(additive_identity,X0))=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f1154,f2683])).
% 0.21/1.16 fof(f2793,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,X0)=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.16 inference(forward_demodulation,[status(thm)],[f29,f2788])).
% 0.21/1.16 fof(f2794,plain,(
% 0.21/1.16 ![X0,X1]: (multiply(additive_identity,multiplicative_identity)=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2793,f2684])).
% 0.21/1.17 fof(f2796,plain,(
% 0.21/1.17 ![X0,X1]: (additive_identity=multiply(additive_identity,add(X0,X1)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f26,f2794])).
% 0.21/1.17 fof(f2810,plain,(
% 0.21/1.17 ![X0,X1]: (X0=add(X0,multiply(X1,X0)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f27,f2685])).
% 0.21/1.17 fof(f2893,plain,(
% 0.21/1.17 add(sF3_fnc,additive_identity)=add(sF2_fnc,sF3_fnc)),
% 0.21/1.17 inference(backward_demodulation,[status(thm)],[f2896,f1169])).
% 0.21/1.17 fof(f2896,plain,(
% 0.21/1.17 additive_identity=multiply(c,additive_identity)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2796,f2774])).
% 0.21/1.17 fof(f2897,plain,(
% 0.21/1.17 ![X0]: (add(b,multiply(a,b))=add(b,multiply(X0,sF3_fnc)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2467,f2777])).
% 0.21/1.17 fof(f2898,plain,(
% 0.21/1.17 ![X0]: (b=add(b,multiply(X0,sF3_fnc)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2810,f2897])).
% 0.21/1.17 fof(f2983,plain,(
% 0.21/1.17 sF3_fnc=add(sF2_fnc,sF3_fnc)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f28,f2893])).
% 0.21/1.17 fof(f3228,plain,(
% 0.21/1.17 multiply(sF2_fnc,sF3_fnc)=sF2_fnc),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f2983,f2786])).
% 0.21/1.17 fof(f3277,plain,(
% 0.21/1.17 ![X0]: (multiply(sF2_fnc,add(X0,sF3_fnc))=add(multiply(sF2_fnc,X0),sF2_fnc))),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3228,f21])).
% 0.21/1.17 fof(f3281,plain,(
% 0.21/1.17 ![X0]: (multiply(sF2_fnc,add(X0,sF3_fnc))=add(sF2_fnc,multiply(sF2_fnc,X0)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f16,f3277])).
% 0.21/1.17 fof(f3282,plain,(
% 0.21/1.17 ![X0]: (multiply(sF2_fnc,add(X0,sF3_fnc))=sF2_fnc)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2787,f3281])).
% 0.21/1.17 fof(f3301,plain,(
% 0.21/1.17 sF1_fnc=add(sF1_fnc,sF0_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f32,f2810])).
% 0.21/1.17 fof(f3304,plain,(
% 0.21/1.17 c=add(c,sF1_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f31,f2810])).
% 0.21/1.17 fof(f3329,plain,(
% 0.21/1.17 sF1_fnc=add(sF0_fnc,sF1_fnc)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f16,f3301])).
% 0.21/1.17 fof(f3348,plain,(
% 0.21/1.17 multiply(sF0_fnc,sF1_fnc)=sF0_fnc),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3329,f2786])).
% 0.21/1.17 fof(f3371,plain,(
% 0.21/1.17 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=add(multiply(sF0_fnc,X0),sF0_fnc))),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3348,f21])).
% 0.21/1.17 fof(f3376,plain,(
% 0.21/1.17 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=add(sF0_fnc,multiply(sF0_fnc,X0)))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f16,f3371])).
% 0.21/1.17 fof(f3377,plain,(
% 0.21/1.17 ![X0]: (multiply(sF0_fnc,add(X0,sF1_fnc))=sF0_fnc)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2787,f3376])).
% 0.21/1.17 fof(f3436,plain,(
% 0.21/1.17 c=add(c,sF2_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f38,f2787])).
% 0.21/1.17 fof(f3437,plain,(
% 0.21/1.17 a=add(a,sF3_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f33,f2787])).
% 0.21/1.17 fof(f3438,plain,(
% 0.21/1.17 a=add(a,sF0_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f32,f2787])).
% 0.21/1.17 fof(f3441,plain,(
% 0.21/1.17 b=add(b,sF1_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f31,f2787])).
% 0.21/1.17 fof(f3939,plain,(
% 0.21/1.17 sF2_fnc=multiply(sF2_fnc,c)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3436,f2785])).
% 0.21/1.17 fof(f3954,plain,(
% 0.21/1.17 sF2_fnc=multiply(c,sF2_fnc)),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f17,f3939])).
% 0.21/1.17 fof(f3969,plain,(
% 0.21/1.17 multiply(b,a)=add(sF3_fnc,multiply(sF0_fnc,b))),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3438,f1003])).
% 0.21/1.17 fof(f3992,plain,(
% 0.21/1.17 multiply(a,b)=add(sF3_fnc,multiply(sF0_fnc,b))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f17,f3969])).
% 0.21/1.17 fof(f3993,plain,(
% 0.21/1.17 sF3_fnc=add(sF3_fnc,multiply(sF0_fnc,b))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f33,f3992])).
% 0.21/1.17 fof(f3994,plain,(
% 0.21/1.17 sF3_fnc=add(sF3_fnc,multiply(b,sF0_fnc))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f2311,f3993])).
% 0.21/1.17 fof(f4310,plain,(
% 0.21/1.17 b=add(b,sF2_fnc)),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f3228,f2898])).
% 0.21/1.17 fof(f4445,plain,(
% 0.21/1.17 multiply(c,b)=add(sF1_fnc,multiply(sF2_fnc,c))),
% 0.21/1.17 inference(paramodulation,[status(thm)],[f4310,f1005])).
% 0.21/1.17 fof(f4471,plain,(
% 0.21/1.17 multiply(b,c)=add(sF1_fnc,multiply(sF2_fnc,c))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f17,f4445])).
% 0.21/1.17 fof(f4472,plain,(
% 0.21/1.17 sF1_fnc=add(sF1_fnc,multiply(sF2_fnc,c))),
% 0.21/1.17 inference(forward_demodulation,[status(thm)],[f31,f4471])).
% 0.21/1.19 fof(f4473,plain,(
% 0.21/1.19 sF1_fnc=add(sF1_fnc,multiply(c,sF2_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f2311,f4472])).
% 0.21/1.19 fof(f4474,plain,(
% 0.21/1.19 sF1_fnc=add(sF1_fnc,sF2_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f3954,f4473])).
% 0.21/1.19 fof(f4517,plain,(
% 0.21/1.19 sF2_fnc=multiply(sF2_fnc,sF1_fnc)),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f4474,f2785])).
% 0.21/1.19 fof(f4530,plain,(
% 0.21/1.19 sF2_fnc=multiply(sF1_fnc,sF2_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f4517])).
% 0.21/1.19 fof(f4838,plain,(
% 0.21/1.19 multiply(sF2_fnc,a)=sF2_fnc),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f3437,f3282])).
% 0.21/1.19 fof(f4856,plain,(
% 0.21/1.19 multiply(a,sF2_fnc)=sF2_fnc),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f4838])).
% 0.21/1.19 fof(f4870,plain,(
% 0.21/1.19 a=add(a,sF2_fnc)),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f4856,f2787])).
% 0.21/1.19 fof(f4885,plain,(
% 0.21/1.19 multiply(sF1_fnc,a)=add(sF0_fnc,multiply(sF2_fnc,sF1_fnc))),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f4870,f1004])).
% 0.21/1.19 fof(f4899,plain,(
% 0.21/1.19 multiply(a,sF1_fnc)=add(sF0_fnc,multiply(sF2_fnc,sF1_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f4885])).
% 0.21/1.19 fof(f4900,plain,(
% 0.21/1.19 sF0_fnc=add(sF0_fnc,multiply(sF2_fnc,sF1_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f32,f4899])).
% 0.21/1.19 fof(f4901,plain,(
% 0.21/1.19 sF0_fnc=add(sF0_fnc,multiply(sF1_fnc,sF2_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f2311,f4900])).
% 0.21/1.19 fof(f4902,plain,(
% 0.21/1.19 sF0_fnc=add(sF0_fnc,sF2_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f4530,f4901])).
% 0.21/1.19 fof(f5880,plain,(
% 0.21/1.19 multiply(sF0_fnc,c)=sF0_fnc),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f3304,f3377])).
% 0.21/1.19 fof(f5882,plain,(
% 0.21/1.19 multiply(sF0_fnc,b)=sF0_fnc),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f3441,f3377])).
% 0.21/1.19 fof(f5897,plain,(
% 0.21/1.19 multiply(c,sF0_fnc)=sF0_fnc),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f5880])).
% 0.21/1.19 fof(f5898,plain,(
% 0.21/1.19 sF3_fnc=add(sF3_fnc,sF0_fnc)),
% 0.21/1.19 inference(backward_demodulation,[status(thm)],[f5899,f3994])).
% 0.21/1.19 fof(f5899,plain,(
% 0.21/1.19 multiply(b,sF0_fnc)=sF0_fnc),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f5882])).
% 0.21/1.19 fof(f5908,plain,(
% 0.21/1.19 sF3_fnc=add(sF0_fnc,sF3_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f16,f5898])).
% 0.21/1.19 fof(f5911,plain,(
% 0.21/1.19 c=add(c,sF0_fnc)),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f5897,f2787])).
% 0.21/1.19 fof(f5949,plain,(
% 0.21/1.19 multiply(sF0_fnc,sF3_fnc)=sF0_fnc),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f5908,f2786])).
% 0.21/1.19 fof(f6000,plain,(
% 0.21/1.19 multiply(sF3_fnc,c)=add(sF2_fnc,multiply(sF0_fnc,sF3_fnc))),
% 0.21/1.19 inference(paramodulation,[status(thm)],[f5911,f1002])).
% 0.21/1.19 fof(f6018,plain,(
% 0.21/1.19 multiply(c,sF3_fnc)=add(sF2_fnc,multiply(sF0_fnc,sF3_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f17,f6000])).
% 0.21/1.19 fof(f6019,plain,(
% 0.21/1.19 sF2_fnc=add(sF2_fnc,multiply(sF0_fnc,sF3_fnc))),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f38,f6018])).
% 0.21/1.19 fof(f6020,plain,(
% 0.21/1.19 sF2_fnc=add(sF2_fnc,sF0_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f5949,f6019])).
% 0.21/1.19 fof(f6021,plain,(
% 0.21/1.19 sF2_fnc=add(sF0_fnc,sF2_fnc)),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f16,f6020])).
% 0.21/1.19 fof(f6022,plain,(
% 0.21/1.19 sF2_fnc=sF0_fnc),
% 0.21/1.19 inference(forward_demodulation,[status(thm)],[f4902,f6021])).
% 0.21/1.19 fof(f6023,plain,(
% 0.21/1.19 $false),
% 0.21/1.19 inference(forward_subsumption_resolution,[status(thm)],[f6022,f35])).
% 0.21/1.19 % SZS output end CNFRefutation for theBenchmark.p
% 0.95/1.20 % Elapsed time: 0.726073 seconds
% 0.95/1.20 % CPU time: 4.794262 seconds
% 0.95/1.20 % Total memory used: 57.498 MB
% 0.95/1.20 % Net memory used: 56.122 MB
%------------------------------------------------------------------------------