%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP479-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:36:41 PM UTC 2026
% Result : Unsatisfiable 9.02s 1.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP479-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n009.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 20:14:13 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 9.02/1.58 % Refutation found
% 9.02/1.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.02/1.58 % SZS output start CNFRefutation for theBenchmark
% 9.02/1.58 fof(f1,axiom,(
% 9.02/1.58 (![A,B,C,D]: (divide(inverse(divide(divide(divide(A,A),B),divide(C,divide(B,D)))),D) = C ))),
% 9.02/1.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.02/1.58 fof(f2,axiom,(
% 9.02/1.58 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 9.02/1.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.02/1.58 fof(f3,negated_conjecture,(
% 9.02/1.58 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 9.02/1.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.02/1.58 fof(f4,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X0),X1),divide(X2,divide(X1,X3)))),X3)=X2)),
% 9.02/1.58 inference(cnf_transformation,[status(thm)],[f1])).
% 9.02/1.58 fof(f5,plain,(
% 9.02/1.58 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 9.02/1.58 inference(cnf_transformation,[status(thm)],[f2])).
% 9.02/1.58 fof(f6,plain,(
% 9.02/1.58 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 9.02/1.58 inference(cnf_transformation,[status(thm)],[f3])).
% 9.02/1.58 fof(f7,definition,(
% 9.02/1.58 sF2_fnc=inverse(b2)),
% 9.02/1.58 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 9.02/1.58 fof(f8,definition,(
% 9.02/1.58 sF1_fnc=multiply(sF2_fnc,b2)),
% 9.02/1.58 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 9.02/1.58 fof(f9,definition,(
% 9.02/1.58 sF0_fnc=multiply(sF1_fnc,a2)),
% 9.02/1.58 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 9.02/1.58 fof(f10,plain,(
% 9.02/1.58 ~sF0_fnc=a2),
% 9.02/1.58 inference(definition_folding,[],[f6,f9,f8,f7])).
% 9.02/1.58 fof(f11,plain,(
% 9.02/1.58 ![X0]: (multiply(X0,b2)=divide(X0,sF2_fnc))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f7,f5])).
% 9.02/1.58 fof(f12,plain,(
% 9.02/1.58 sF1_fnc=divide(sF2_fnc,sF2_fnc)),
% 9.02/1.58 inference(backward_demodulation,[status(thm)],[f11,f8])).
% 9.02/1.58 fof(f15,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),X2)=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f12,f4])).
% 9.02/1.58 fof(f26,plain,(
% 9.02/1.58 ![X0,X1,X2]: (multiply(inverse(divide(divide(sF1_fnc,X0),divide(X1,divide(X0,inverse(X2))))),X2)=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f15])).
% 9.02/1.58 fof(f27,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,X0),divide(X1,divide(inverse(X0),X2)))),X2)=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f15])).
% 9.02/1.58 fof(f28,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(sF1_fnc,X3),divide(X1,divide(X3,divide(X0,X2))))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f15,f15])).
% 9.02/1.58 fof(f29,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(divide(X3,X3),X4),divide(X1,divide(X4,divide(X0,X2))))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f4,f15])).
% 9.02/1.58 fof(f30,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,inverse(divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2))))),divide(X3,X1))),X2)=X3)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f15,f15])).
% 9.02/1.58 fof(f32,plain,(
% 9.02/1.58 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF2_fnc),divide(X0,sF1_fnc))),sF2_fnc)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f12,f15])).
% 9.02/1.58 fof(f37,plain,(
% 9.02/1.58 ![X0,X1,X2]: (multiply(inverse(divide(divide(sF1_fnc,X0),divide(X1,multiply(X0,X2)))),X2)=X1)),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f26])).
% 9.02/1.58 fof(f39,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1))),X2)=X3)),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f30])).
% 9.02/1.58 fof(f52,plain,(
% 9.02/1.58 ![X0,X1,X2]: (multiply(inverse(divide(multiply(sF1_fnc,X0),divide(X1,multiply(inverse(X0),X2)))),X2)=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f37])).
% 9.02/1.58 fof(f55,plain,(
% 9.02/1.58 ![X0]: (multiply(inverse(divide(divide(sF1_fnc,sF1_fnc),divide(X0,sF0_fnc))),a2)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f9,f37])).
% 9.02/1.58 fof(f66,plain,(
% 9.02/1.58 ![X0,X1]: (multiply(inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),X1)))),X1)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f9,f52])).
% 9.02/1.58 fof(f69,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (multiply(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X0),divide(X1,multiply(inverse(X0),X2)))),divide(X3,X1))),X2)=X3)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f52,f52])).
% 9.02/1.58 fof(f133,plain,(
% 9.02/1.58 ![X0,X1]: (divide(inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1)))),X1)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f9,f27])).
% 9.02/1.58 fof(f174,plain,(
% 9.02/1.58 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)=inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),sF1_fnc)))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f133,f32])).
% 9.02/1.58 fof(f176,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(sF0_fnc,divide(X1,divide(inverse(a2),divide(X0,X2))))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f133,f15])).
% 9.02/1.58 fof(f522,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),inverse(divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4)))))))),X4)=inverse(divide(divide(sF1_fnc,X3),X2)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f27,f28])).
% 9.02/1.58 fof(f526,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(sF1_fnc,inverse(divide(divide(sF1_fnc,X3),divide(X4,divide(X3,divide(X0,X2)))))),divide(X1,X4))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f15,f28])).
% 9.02/1.58 fof(f533,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2),divide(X0,X2))=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f28,f15])).
% 9.02/1.58 fof(f536,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,divide(X3,X4)))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,X3),X2)),X4)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f28,f5])).
% 9.02/1.58 fof(f538,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4))))))),X4)=inverse(divide(divide(sF1_fnc,X3),X2)))),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f522])).
% 9.02/1.58 fof(f542,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X3),divide(X4,divide(X3,divide(X0,X2))))),divide(X1,X4))))),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f526])).
% 9.02/1.58 fof(f550,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(sF1_fnc,divide(inverse(divide(divide(sF1_fnc,X0),X3)),X2)),divide(X1,X3))))),
% 9.02/1.58 inference(backward_demodulation,[status(thm)],[f536,f542])).
% 9.02/1.58 fof(f554,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(multiply(inverse(divide(divide(sF1_fnc,X0),X1)),X2),divide(X0,inverse(X2)))=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f533])).
% 9.02/1.58 fof(f555,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(divide(divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2),X3),divide(X4,X3))=divide(X1,divide(X4,divide(X0,X2))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f28,f533])).
% 9.02/1.58 fof(f557,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),X2),divide(inverse(X0),X2))=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f533])).
% 9.02/1.58 fof(f563,plain,(
% 9.02/1.58 ![X0]: (divide(divide(inverse(divide(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc),sF1_fnc)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f12,f533])).
% 9.02/1.58 fof(f574,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(multiply(inverse(divide(divide(sF1_fnc,X0),X1)),X2),multiply(X0,X2))=X1)),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f554])).
% 9.02/1.58 fof(f587,plain,(
% 9.02/1.58 ![X0]: (divide(divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc),sF1_fnc)=inverse(X0))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f563])).
% 9.02/1.58 fof(f598,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(multiply(inverse(divide(multiply(sF1_fnc,X0),X1)),X2),multiply(inverse(X0),X2))=X1)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f574])).
% 9.02/1.58 fof(f602,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,X0),divide(X1,multiply(inverse(X0),X2))))),X3)),X2),X1)=X3)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f52,f574])).
% 9.02/1.58 fof(f606,plain,(
% 9.02/1.58 ![X0]: (divide(multiply(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),a2),sF0_fnc)=X0)),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f9,f574])).
% 9.02/1.58 fof(f618,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X0),divide(X1,multiply(inverse(X0),X2)))),X3)),X2),X1)=X3)),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f602])).
% 9.02/1.58 fof(f635,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)),X1)),sF1_fnc)=inverse(divide(divide(sF1_fnc,X2),divide(X1,divide(X2,inverse(X0))))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f587,f28])).
% 9.02/1.58 fof(f639,plain,(
% 9.02/1.58 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)),X1)),sF1_fnc)=inverse(divide(divide(sF1_fnc,X2),divide(X1,multiply(X2,X0)))))),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f5,f635])).
% 9.02/1.58 fof(f654,plain,(
% 9.02/1.58 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(inverse(divide(divide(sF1_fnc,X1),X2)),divide(X0,X3)))),X3)=inverse(divide(divide(divide(X4,X4),X1),X2)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f533,f29])).
% 9.02/1.58 fof(f682,plain,(
% 9.02/1.58 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,X0),X1))=inverse(divide(divide(divide(X2,X2),X0),X1)))),
% 9.02/1.58 inference(forward_demodulation,[status(thm)],[f15,f654])).
% 9.02/1.58 fof(f719,plain,(
% 9.02/1.58 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,X0),inverse(X1)))=inverse(multiply(divide(divide(X2,X2),X0),X1)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f682])).
% 9.02/1.58 fof(f720,plain,(
% 9.02/1.58 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,divide(X0,inverse(divide(divide(sF1_fnc,X0),X1)))),X2))=inverse(divide(X1,X2)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f533,f682])).
% 9.02/1.58 fof(f721,plain,(
% 9.02/1.58 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,inverse(X0)),X1))=inverse(divide(multiply(divide(X2,X2),X0),X1)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f682])).
% 9.02/1.58 fof(f723,plain,(
% 9.02/1.58 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,X0),X1))=inverse(divide(divide(multiply(inverse(X2),X2),X0),X1)))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f5,f682])).
% 9.02/1.58 fof(f726,plain,(
% 9.02/1.58 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(divide(X1,X1),X2),X3))=divide(X0,inverse(divide(divide(sF1_fnc,X2),X3))))),
% 9.02/1.58 inference(paramodulation,[status(thm)],[f682,f5])).
% 9.02/1.59 fof(f729,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(multiply(divide(sF1_fnc,X0),X1))=inverse(multiply(divide(divide(X2,X2),X0),X1)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f719])).
% 9.02/1.59 fof(f731,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,multiply(X0,divide(divide(sF1_fnc,X0),X1))),X2))=inverse(divide(X1,X2)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f720])).
% 9.02/1.59 fof(f738,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,X0),X1))=inverse(divide(multiply(divide(X2,X2),X0),X1)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f721])).
% 9.02/1.59 fof(f751,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(divide(X1,X1),X2),X3))=multiply(X0,divide(divide(sF1_fnc,X2),X3)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f726])).
% 9.02/1.59 fof(f753,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(multiply(divide(sF1_fnc,divide(X0,inverse(divide(divide(sF1_fnc,X0),X1)))),X2))=inverse(multiply(X1,X2)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f533,f729])).
% 9.02/1.59 fof(f762,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(multiply(divide(sF1_fnc,multiply(X0,divide(divide(sF1_fnc,X0),X1))),X2))=inverse(multiply(X1,X2)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f753])).
% 9.02/1.59 fof(f834,plain,(
% 9.02/1.59 ![X0,X1]: (divide(multiply(inverse(divide(sF0_fnc,X0)),X1),multiply(inverse(a2),X1))=X0)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f9,f598])).
% 9.02/1.59 fof(f851,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,multiply(inverse(divide(multiply(sF1_fnc,X0),X1)),X2)),X3)),multiply(inverse(X0),X2))=inverse(divide(divide(sF1_fnc,X4),divide(X3,divide(X4,X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f598,f28])).
% 9.02/1.59 fof(f879,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,X0),divide(X1,divide(inverse(X0),X2))))),divide(X3,X1))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f27,f39])).
% 9.02/1.59 fof(f892,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),X3)),X2)=inverse(divide(sF0_fnc,divide(X3,divide(inverse(a2),X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f133,f39])).
% 9.02/1.59 fof(f894,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),X3)),X2)=inverse(divide(multiply(sF1_fnc,X4),divide(X3,divide(inverse(X4),X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f27,f39])).
% 9.02/1.59 fof(f895,plain,(
% 9.02/1.59 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(sF2_fnc,divide(X0,X1)))),X2)),X1)=inverse(divide(divide(sF1_fnc,sF2_fnc),divide(X2,sF1_fnc))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f32,f39])).
% 9.02/1.59 fof(f896,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),X3)),X2)=inverse(divide(divide(sF1_fnc,X4),divide(X3,divide(X4,X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f15,f39])).
% 9.02/1.59 fof(f898,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(inverse(X1),divide(X0,X2)))),multiply(X3,X1))),X2)=X3)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f5,f39])).
% 9.02/1.59 fof(f912,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1)))),X4)),X2)=inverse(divide(divide(sF1_fnc,X5),divide(X4,divide(X5,X3)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f39,f28])).
% 9.02/1.59 fof(f913,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1)))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f39,f15])).
% 9.02/1.59 fof(f926,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X0),divide(X1,divide(inverse(X0),X2)))),divide(X3,X1))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f879])).
% 9.02/1.59 fof(f947,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(multiply(sF1_fnc,X2),divide(X0,divide(inverse(X2),X1)))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f892,f894])).
% 9.02/1.59 fof(f948,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),sF2_fnc))))=inverse(divide(divide(sF1_fnc,sF2_fnc),divide(X0,sF1_fnc))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f892,f895])).
% 9.02/1.59 fof(f954,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,multiply(inverse(divide(multiply(sF1_fnc,X0),X1)),X2)),X3)),multiply(inverse(X0),X2))=inverse(divide(sF0_fnc,divide(X3,divide(inverse(a2),X1)))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f962,f851])).
% 9.02/1.59 fof(f962,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(divide(sF1_fnc,X2),divide(X0,divide(X2,X1)))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f892,f896])).
% 9.02/1.59 fof(f965,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(sF0_fnc,divide(multiply(X0,X1),divide(inverse(a2),inverse(X1)))))=X0)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f892,f898])).
% 9.02/1.59 fof(f966,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(sF0_fnc,divide(multiply(X0,X1),multiply(inverse(a2),X1))))=X0)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f965])).
% 9.02/1.59 fof(f990,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1))),X4)),X2)=inverse(divide(divide(sF1_fnc,X5),divide(X4,divide(X5,X3)))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f912])).
% 9.02/1.59 fof(f993,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1))),X4)),X2)=inverse(divide(sF0_fnc,divide(X4,divide(inverse(a2),X3)))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f962,f990])).
% 9.02/1.59 fof(f994,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(divide(sF1_fnc,X0),divide(X1,divide(X0,X2)))),divide(X3,X1))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f913])).
% 9.02/1.59 fof(f995,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(sF0_fnc,divide(divide(X0,X1),divide(inverse(a2),X1))))=X0)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f993,f994])).
% 9.02/1.59 fof(f1059,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),X1))))=inverse(divide(multiply(sF1_fnc,X2),divide(X0,multiply(inverse(X2),X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f52,f966])).
% 9.02/1.59 fof(f1060,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),a2))))=inverse(divide(divide(sF1_fnc,sF1_fnc),divide(X0,sF0_fnc))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f55,f966])).
% 9.02/1.59 fof(f1061,plain,(
% 9.02/1.59 ![X0,X1,X2]: (inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),X1))))=inverse(divide(divide(sF1_fnc,X2),divide(X0,multiply(X2,X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f37,f966])).
% 9.02/1.59 fof(f1062,plain,(
% 9.02/1.59 inverse(divide(sF0_fnc,divide(sF0_fnc,multiply(inverse(a2),a2))))=sF1_fnc),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f9,f966])).
% 9.02/1.59 fof(f1064,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(sF0_fnc,divide(multiply(X0,b2),divide(inverse(a2),sF2_fnc))))=X0)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f11,f966])).
% 9.02/1.59 fof(f1069,plain,(
% 9.02/1.59 ![X0,X1,X2]: (multiply(X0,divide(sF0_fnc,divide(multiply(X1,X2),multiply(inverse(a2),X2))))=divide(X0,X1))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f966,f5])).
% 9.02/1.59 fof(f1077,plain,(
% 9.02/1.59 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)),X1)),sF1_fnc)=inverse(divide(sF0_fnc,divide(X1,multiply(inverse(a2),X0)))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f1061,f639])).
% 9.02/1.59 fof(f1078,plain,(
% 9.02/1.59 inverse(divide(divide(sF1_fnc,sF1_fnc),divide(sF0_fnc,sF0_fnc)))=sF1_fnc),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f1060,f1062])).
% 9.02/1.59 fof(f1080,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(divide(sF1_fnc,sF2_fnc),divide(multiply(X0,b2),sF1_fnc)))=X0)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f948,f1064])).
% 9.02/1.59 fof(f1081,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(divide(sF1_fnc,sF2_fnc),divide(divide(X0,sF2_fnc),sF1_fnc)))=X0)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f11,f1080])).
% 9.02/1.59 fof(f1094,plain,(
% 9.02/1.59 ![X0]: (divide(divide(sF1_fnc,X0),divide(sF1_fnc,X0))=divide(sF0_fnc,sF0_fnc))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1078,f533])).
% 9.02/1.59 fof(f1226,plain,(
% 9.02/1.59 divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),a2),sF0_fnc)=divide(sF1_fnc,sF1_fnc)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f606])).
% 9.02/1.59 fof(f1228,plain,(
% 9.02/1.59 ![X0,X1]: (divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),X0),multiply(X1,X0))=divide(sF1_fnc,X1))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f574])).
% 9.02/1.59 fof(f1229,plain,(
% 9.02/1.59 ![X0,X1]: (divide(divide(inverse(divide(sF0_fnc,sF0_fnc)),X0),divide(X1,X0))=divide(sF1_fnc,X1))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f533])).
% 9.02/1.59 fof(f1231,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0))=inverse(divide(divide(sF0_fnc,sF0_fnc),X0)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f682])).
% 9.02/1.59 fof(f1250,plain,(
% 9.02/1.59 ![X0,X1]: (multiply(X0,divide(divide(sF1_fnc,sF2_fnc),divide(divide(X1,sF2_fnc),sF1_fnc)))=divide(X0,X1))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1081,f5])).
% 9.02/1.59 fof(f1701,plain,(
% 9.02/1.59 ![X0,X1]: (divide(divide(inverse(divide(sF0_fnc,X0)),X1),divide(inverse(a2),X1))=X0)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f9,f557])).
% 9.02/1.59 fof(f1757,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(divide(sF1_fnc,divide(inverse(a2),inverse(divide(sF0_fnc,X0)))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1701,f682])).
% 9.02/1.59 fof(f1766,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(inverse(a2),divide(sF0_fnc,X0))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f1757])).
% 9.02/1.59 fof(f2187,plain,(
% 9.02/1.59 ![X0]: (divide(divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc),inverse(X0))=divide(sF1_fnc,divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f587,f1229])).
% 9.02/1.59 fof(f2234,plain,(
% 9.02/1.59 ![X0,X1]: (divide(inverse(divide(multiply(divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc),X0),X1)),sF1_fnc)=inverse(divide(sF0_fnc,divide(X1,multiply(inverse(a2),X0)))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f2236,f1077])).
% 9.02/1.59 fof(f2236,plain,(
% 9.02/1.59 ![X0]: (multiply(divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc),X0)=divide(sF1_fnc,divide(inverse(multiply(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2187])).
% 9.02/1.59 fof(f2387,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(multiply(inverse(X1),X1),X2),X3))=divide(X0,inverse(divide(divide(sF1_fnc,X2),X3))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f723,f5])).
% 9.02/1.59 fof(f2446,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(multiply(inverse(X1),X1),X2),X3))=multiply(X0,divide(divide(sF1_fnc,X2),X3)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2387])).
% 9.02/1.59 fof(f2630,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),X3))))),X4)=inverse(divide(divide(sF1_fnc,divide(inverse(divide(divide(sF1_fnc,X0),X3)),X4)),X2)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f533,f538])).
% 9.02/1.59 fof(f2658,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(multiply(divide(sF1_fnc,inverse(multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4)))))))),divide(multiply(sF1_fnc,X5),divide(X6,divide(inverse(X5),divide(X7,inverse(divide(divide(sF1_fnc,X3),X2)))))))),X4)=inverse(divide(divide(sF1_fnc,X7),X6)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f538,f538])).
% 9.02/1.59 fof(f2672,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(sF0_fnc,sF0_fnc)),X0),inverse(divide(divide(sF1_fnc,X1),X2)))=divide(sF1_fnc,inverse(multiply(divide(sF1_fnc,X3),divide(multiply(sF1_fnc,X4),divide(X2,divide(inverse(X4),divide(X1,divide(X3,X0)))))))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f538,f1229])).
% 9.02/1.59 fof(f2819,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(divide(sF1_fnc,divide(inverse(divide(divide(sF1_fnc,inverse(multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4)))))))),divide(X5,inverse(divide(divide(sF1_fnc,X3),X2))))),X4)),X6))=inverse(divide(divide(sF1_fnc,X5),X6)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f2630,f2658])).
% 9.02/1.59 fof(f2820,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(divide(sF1_fnc,divide(inverse(divide(multiply(sF1_fnc,multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4))))))),divide(X5,inverse(divide(divide(sF1_fnc,X3),X2))))),X4)),X6))=inverse(divide(divide(sF1_fnc,X5),X6)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2819])).
% 9.02/1.59 fof(f2821,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(divide(sF1_fnc,divide(inverse(divide(multiply(sF1_fnc,multiply(divide(sF1_fnc,X0),divide(multiply(sF1_fnc,X1),divide(X2,divide(inverse(X1),divide(X3,divide(X0,X4))))))),multiply(X5,divide(divide(sF1_fnc,X3),X2)))),X4)),X6))=inverse(divide(divide(sF1_fnc,X5),X6)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2820])).
% 9.02/1.59 fof(f2846,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(divide(inverse(divide(sF0_fnc,sF0_fnc)),X0),divide(divide(sF1_fnc,X1),X2))=divide(sF1_fnc,inverse(multiply(divide(sF1_fnc,X3),divide(multiply(sF1_fnc,X4),divide(X2,divide(inverse(X4),divide(X1,divide(X3,X0)))))))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2672])).
% 9.02/1.59 fof(f2850,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(sF1_fnc,divide(inverse(divide(multiply(divide(inverse(divide(sF0_fnc,sF0_fnc)),X0),divide(divide(sF1_fnc,X1),X2)),multiply(X3,divide(divide(sF1_fnc,X1),X2)))),X0)),X4))=inverse(divide(divide(sF1_fnc,X3),X4)))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f2851,f2821])).
% 9.02/1.59 fof(f2851,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(divide(inverse(divide(sF0_fnc,sF0_fnc)),X0),divide(divide(sF1_fnc,X1),X2))=multiply(sF1_fnc,multiply(divide(sF1_fnc,X3),divide(multiply(sF1_fnc,X4),divide(X2,divide(inverse(X4),divide(X1,divide(X3,X0))))))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f2846])).
% 9.02/1.59 fof(f3398,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(X0,X1)),X2),multiply(multiply(X3,divide(divide(sF1_fnc,X3),X0)),X2))=X1)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f731,f574])).
% 9.02/1.59 fof(f3434,plain,(
% 9.02/1.59 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X2,divide(sF0_fnc,sF0_fnc))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,sF1_fnc),X2)),X1)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f536])).
% 9.02/1.59 fof(f3451,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,X3))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,multiply(inverse(divide(sF0_fnc,X3)),X4)),X2)),multiply(inverse(a2),X4))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f834,f536])).
% 9.02/1.59 fof(f3452,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,X3))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,multiply(inverse(divide(multiply(sF1_fnc,X4),X3)),X5)),X2)),multiply(inverse(X4),X5))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f598,f536])).
% 9.02/1.59 fof(f3602,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,X3))))=divide(X0,inverse(divide(sF0_fnc,divide(X2,divide(inverse(a2),X3))))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f954,f3452])).
% 9.02/1.59 fof(f3611,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(sF0_fnc,divide(X1,divide(inverse(a2),X2))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,multiply(inverse(divide(sF0_fnc,X2)),X3)),X1)),multiply(inverse(a2),X3))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f3612,f3451])).
% 9.02/1.59 fof(f3612,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,X3))))=multiply(X0,divide(sF0_fnc,divide(X2,divide(inverse(a2),X3)))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f3602])).
% 9.02/1.59 fof(f3942,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(sF1_fnc,multiply(X1,divide(divide(sF1_fnc,X1),X2))),X3))=divide(X0,inverse(multiply(X2,X3))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f762,f5])).
% 9.02/1.59 fof(f3960,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(sF1_fnc,multiply(X1,divide(divide(sF1_fnc,X1),X2))),X3))=multiply(X0,multiply(X2,X3)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f3942])).
% 9.02/1.59 fof(f3964,plain,(
% 9.02/1.59 ![X0,X1]: (multiply(X0,divide(divide(sF0_fnc,sF0_fnc),X1))=multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X1)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f751])).
% 9.02/1.59 fof(f4140,plain,(
% 9.02/1.59 inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(divide(sF0_fnc,sF0_fnc),divide(sF1_fnc,divide(sF1_fnc,sF1_fnc))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f1231])).
% 9.02/1.59 fof(f4143,plain,(
% 9.02/1.59 ![X0,X1]: (divide(multiply(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),X1),multiply(divide(sF1_fnc,sF1_fnc),X1))=X0)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1231,f574])).
% 9.02/1.59 fof(f4323,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,multiply(X0,divide(divide(sF1_fnc,X0),X1))),X2)),X3)=inverse(divide(divide(sF1_fnc,divide(inverse(divide(X1,X4)),X3)),divide(X2,X4))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f731,f550])).
% 9.02/1.59 fof(f4324,plain,(
% 9.02/1.59 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X0,divide(sF0_fnc,sF0_fnc)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1078,f550])).
% 9.02/1.59 fof(f4328,plain,(
% 9.02/1.59 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(sF1_fnc,divide(inverse(divide(sF0_fnc,sF0_fnc)),X2)),divide(X1,divide(sF1_fnc,X0)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f550])).
% 9.02/1.59 fof(f4378,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),X2)=inverse(divide(divide(sF1_fnc,divide(inverse(divide(X0,X3)),X2)),divide(X1,X3))))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f731,f4323])).
% 9.02/1.59 fof(f4842,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(X0,divide(sF1_fnc,multiply(inverse(a2),divide(sF0_fnc,X0))))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1094,f1766])).
% 9.02/1.59 fof(f4869,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X0),divide(X1,divide(inverse(X0),inverse(X2))))),divide(X3,X1))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f5,f926])).
% 9.02/1.59 fof(f4994,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(inverse(divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X0),divide(X1,multiply(inverse(X0),X2)))),divide(X3,X1))),divide(X4,X3))),X2)=X4)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f4869])).
% 9.02/1.59 fof(f6016,plain,(
% 9.02/1.59 ![X0]: (divide(sF1_fnc,multiply(X0,divide(divide(sF1_fnc,X0),sF0_fnc)))=sF0_fnc)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1228,f3398])).
% 9.02/1.59 fof(f6051,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(sF1_fnc,X0)),X1),multiply(multiply(X2,divide(divide(sF1_fnc,X2),multiply(inverse(divide(sF0_fnc,sF0_fnc)),X3))),X1))=multiply(X0,X3))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f1228,f3398])).
% 9.02/1.59 fof(f6100,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(X1,X2))=multiply(X0,divide(divide(sF1_fnc,multiply(multiply(X3,divide(divide(sF1_fnc,X3),X4)),divide(X4,X1))),X2)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f3398,f2446])).
% 9.02/1.59 fof(f6102,plain,(
% 9.02/1.59 ![X0,X1,X2,X3]: (inverse(divide(divide(sF1_fnc,multiply(multiply(X0,divide(divide(sF1_fnc,X0),X1)),divide(X1,X2))),X3))=inverse(divide(X2,X3)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f3398,f723])).
% 9.02/1.59 fof(f6170,plain,(
% 9.02/1.59 multiply(inverse(divide(sF0_fnc,sF0_fnc)),divide(divide(sF1_fnc,inverse(a2)),sF0_fnc))=sF1_fnc),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6016,f66])).
% 9.02/1.59 fof(f6171,plain,(
% 9.02/1.59 ![X0,X1,X2]: (divide(multiply(inverse(sF0_fnc),X0),multiply(multiply(X1,divide(divide(sF1_fnc,X1),sF1_fnc)),X0))=multiply(X2,divide(divide(sF1_fnc,X2),sF0_fnc)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6016,f3398])).
% 9.02/1.59 fof(f6180,plain,(
% 9.02/1.59 multiply(inverse(divide(sF0_fnc,sF0_fnc)),divide(multiply(sF1_fnc,a2),sF0_fnc))=sF1_fnc),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f6170])).
% 9.02/1.59 fof(f6181,plain,(
% 9.02/1.59 multiply(inverse(divide(sF0_fnc,sF0_fnc)),divide(sF0_fnc,sF0_fnc))=sF1_fnc),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f9,f6180])).
% 9.02/1.59 fof(f6237,plain,(
% 9.02/1.59 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1)))),X2),multiply(multiply(X3,divide(divide(sF1_fnc,X3),multiply(sF1_fnc,X4))),X2))=divide(X0,divide(inverse(X4),X1)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f947,f3398])).
% 9.02/1.59 fof(f6422,plain,(
% 9.02/1.59 ![X0]: (divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc)))=divide(sF1_fnc,X0))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6181,f1228])).
% 9.02/1.59 fof(f6436,plain,(
% 9.02/1.59 divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),divide(sF0_fnc,sF0_fnc)),sF1_fnc)=divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc)))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6181,f1228])).
% 9.02/1.59 fof(f6451,plain,(
% 9.02/1.59 divide(sF1_fnc,sF1_fnc)=divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc)))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f6181,f6436])).
% 9.02/1.59 fof(f6462,plain,(
% 9.02/1.59 divide(sF1_fnc,sF1_fnc)=multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc))),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f5,f6451])).
% 9.02/1.59 fof(f6469,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(divide(sF1_fnc,sF1_fnc),divide(X0,divide(inverse(divide(sF0_fnc,sF0_fnc)),X1)))))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6462,f947])).
% 9.02/1.59 fof(f6476,plain,(
% 9.02/1.59 ![X0]: (multiply(X0,divide(sF0_fnc,divide(divide(sF1_fnc,sF1_fnc),multiply(inverse(a2),divide(sF0_fnc,sF0_fnc)))))=divide(X0,sF1_fnc))),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6462,f1069])).
% 9.02/1.59 fof(f6478,plain,(
% 9.02/1.59 divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),divide(sF0_fnc,sF0_fnc)),divide(sF1_fnc,sF1_fnc))=divide(sF1_fnc,sF1_fnc)),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6462,f1228])).
% 9.02/1.59 fof(f6480,plain,(
% 9.02/1.59 inverse(divide(sF0_fnc,divide(divide(sF1_fnc,sF1_fnc),multiply(inverse(a2),divide(sF0_fnc,sF0_fnc)))))=sF1_fnc),
% 9.02/1.59 inference(paramodulation,[status(thm)],[f6462,f966])).
% 9.02/1.59 fof(f6485,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(divide(sF1_fnc,sF1_fnc),X0))=inverse(divide(divide(sF0_fnc,sF0_fnc),X0)))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6491,f1231])).
% 9.02/1.59 fof(f6488,plain,(
% 9.02/1.59 inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(divide(sF0_fnc,sF0_fnc),divide(sF1_fnc,sF1_fnc)))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6491,f4140])).
% 9.02/1.59 fof(f6490,plain,(
% 9.02/1.59 ![X0,X1]: (multiply(X0,divide(divide(sF0_fnc,sF0_fnc),X1))=multiply(X0,divide(divide(sF1_fnc,sF1_fnc),X1)))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6491,f3964])).
% 9.02/1.59 fof(f6491,plain,(
% 9.02/1.59 divide(sF1_fnc,divide(sF1_fnc,sF1_fnc))=divide(sF1_fnc,sF1_fnc)),
% 9.02/1.59 inference(forward_demodulation,[status(thm)],[f6181,f6478])).
% 9.02/1.59 fof(f6494,plain,(
% 9.02/1.59 ![X0]: (multiply(inverse(divide(divide(sF0_fnc,sF0_fnc),divide(X0,sF0_fnc))),a2)=X0)),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6485,f55])).
% 9.02/1.59 fof(f6496,plain,(
% 9.02/1.59 ![X0,X1]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(divide(sF0_fnc,sF0_fnc),divide(X0,divide(inverse(divide(sF0_fnc,sF0_fnc)),X1)))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6485,f6469])).
% 9.02/1.59 fof(f6498,plain,(
% 9.02/1.59 ![X0]: (inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),a2))))=inverse(divide(divide(sF0_fnc,sF0_fnc),divide(X0,sF0_fnc))))),
% 9.02/1.59 inference(backward_demodulation,[status(thm)],[f6485,f1060])).
% 9.02/1.59 fof(f6508,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X0,divide(sF0_fnc,sF0_fnc)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6485,f4324])).
% 9.02/1.60 fof(f6513,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X2,divide(sF0_fnc,sF0_fnc))))=divide(X0,divide(inverse(divide(divide(sF0_fnc,sF0_fnc),X2)),X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6485,f3434])).
% 9.02/1.60 fof(f6536,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(divide(sF1_fnc,sF1_fnc),divide(divide(sF1_fnc,sF1_fnc),X0))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.60 inference(paramodulation,[status(thm)],[f6491,f731])).
% 9.02/1.60 fof(f6543,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(inverse(divide(sF1_fnc,sF1_fnc)),X0),multiply(multiply(X1,divide(divide(sF1_fnc,X1),sF1_fnc)),X0))=divide(sF1_fnc,sF1_fnc))),
% 9.02/1.60 inference(paramodulation,[status(thm)],[f6491,f3398])).
% 9.02/1.60 fof(f6549,plain,(
% 9.02/1.60 inverse(divide(sF0_fnc,divide(divide(sF1_fnc,sF1_fnc),divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))))=sF1_fnc),
% 9.02/1.60 inference(paramodulation,[status(thm)],[f6491,f995])).
% 9.02/1.60 fof(f6550,plain,(
% 9.02/1.60 ![X0]: (divide(divide(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc))=X0)),
% 9.02/1.60 inference(paramodulation,[status(thm)],[f6491,f533])).
% 9.02/1.60 fof(f6554,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(divide(sF1_fnc,sF1_fnc),divide(divide(sF0_fnc,sF0_fnc),X0))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6490,f6536])).
% 9.02/1.60 fof(f6564,plain,(
% 9.02/1.60 divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),a2),sF0_fnc)=sF1_fnc),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f1226])).
% 9.02/1.60 fof(f6566,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(divide(sF0_fnc,sF0_fnc),X0))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6554])).
% 9.02/1.60 fof(f6572,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(X0,divide(divide(sF0_fnc,sF0_fnc),X1))=multiply(X0,divide(sF1_fnc,X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6490])).
% 9.02/1.60 fof(f6574,plain,(
% 9.02/1.60 inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(divide(sF0_fnc,sF0_fnc),sF1_fnc))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6488])).
% 9.02/1.60 fof(f6577,plain,(
% 9.02/1.60 ![X0]: (inverse(divide(sF1_fnc,X0))=inverse(divide(divide(sF0_fnc,sF0_fnc),X0)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6485])).
% 9.02/1.60 fof(f6578,plain,(
% 9.02/1.60 inverse(divide(sF0_fnc,divide(sF1_fnc,multiply(inverse(a2),divide(sF0_fnc,sF0_fnc)))))=sF1_fnc),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6480])).
% 9.02/1.60 fof(f6581,plain,(
% 9.02/1.60 ![X0]: (multiply(X0,divide(sF0_fnc,divide(sF1_fnc,multiply(inverse(a2),divide(sF0_fnc,sF0_fnc)))))=divide(X0,sF1_fnc))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f6476])).
% 9.02/1.60 fof(f6588,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),X1),multiply(sF1_fnc,X1))=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6599,f4143])).
% 9.02/1.60 fof(f6599,plain,(
% 9.02/1.60 sF1_fnc=divide(sF1_fnc,sF1_fnc)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f3398,f6543])).
% 9.02/1.60 fof(f6614,plain,(
% 9.02/1.60 divide(inverse(divide(divide(sF1_fnc,sF1_fnc),divide(sF1_fnc,sF1_fnc))),sF1_fnc)=sF1_fnc),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f176,f6549])).
% 9.02/1.60 fof(f6615,plain,(
% 9.02/1.60 divide(inverse(divide(divide(sF0_fnc,sF0_fnc),divide(sF1_fnc,sF1_fnc))),sF1_fnc)=sF1_fnc),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6485,f6614])).
% 9.02/1.60 fof(f6617,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(sF0_fnc,divide(X1,multiply(inverse(a2),X0)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6624,f2234])).
% 9.02/1.60 fof(f6624,plain,(
% 9.02/1.60 divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc)=sF1_fnc),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6488,f6615])).
% 9.02/1.60 fof(f6625,plain,(
% 9.02/1.60 ![X0]: (divide(divide(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc))=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6485,f6550])).
% 9.02/1.60 fof(f6626,plain,(
% 9.02/1.60 ![X0]: (divide(divide(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),sF1_fnc),divide(sF1_fnc,sF1_fnc))=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6599,f6625])).
% 9.02/1.60 fof(f6627,plain,(
% 9.02/1.60 ![X0]: (divide(divide(inverse(divide(divide(sF0_fnc,sF0_fnc),X0)),sF1_fnc),sF1_fnc)=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6599,f6626])).
% 9.02/1.60 fof(f6681,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,X0))),X1))=inverse(divide(X0,X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6572,f6566])).
% 9.02/1.60 fof(f6696,plain,(
% 9.02/1.60 inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(sF1_fnc,sF1_fnc))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6574])).
% 9.02/1.60 fof(f6698,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(sF1_fnc,divide(X0,divide(inverse(divide(sF0_fnc,sF0_fnc)),X1)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6496])).
% 9.02/1.60 fof(f6699,plain,(
% 9.02/1.60 ![X0]: (inverse(divide(sF0_fnc,divide(X0,multiply(inverse(a2),a2))))=inverse(divide(sF1_fnc,divide(X0,sF0_fnc))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6498])).
% 9.02/1.60 fof(f6701,plain,(
% 9.02/1.60 ![X0]: (multiply(inverse(divide(sF1_fnc,divide(X0,sF0_fnc))),a2)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6494])).
% 9.02/1.60 fof(f6703,plain,(
% 9.02/1.60 ![X0]: (divide(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6627])).
% 9.02/1.60 fof(f6706,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X2,divide(sF0_fnc,sF0_fnc))))=divide(X0,divide(inverse(divide(sF1_fnc,X2)),X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6513])).
% 9.02/1.60 fof(f6711,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(sF1_fnc,X0)),X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X0,divide(sF0_fnc,sF0_fnc)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6577,f6508])).
% 9.02/1.60 fof(f6721,plain,(
% 9.02/1.60 ![X0,X1]: (divide(divide(sF1_fnc,X0),divide(X1,X0))=divide(sF1_fnc,X1))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f1229])).
% 9.02/1.60 fof(f6722,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(sF1_fnc,X0),multiply(X1,X0))=divide(sF1_fnc,X1))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f1228])).
% 9.02/1.60 fof(f6724,plain,(
% 9.02/1.60 divide(multiply(sF1_fnc,a2),sF0_fnc)=sF1_fnc),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f6564])).
% 9.02/1.60 fof(f6760,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(sF1_fnc,X0)),X1),multiply(multiply(X2,divide(divide(sF1_fnc,X2),multiply(sF1_fnc,X3))),X1))=multiply(X0,X3))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f6051])).
% 9.02/1.60 fof(f6763,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X2)),divide(X1,divide(sF1_fnc,X0)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f4328])).
% 9.02/1.60 fof(f6775,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(sF1_fnc,divide(inverse(divide(multiply(divide(sF1_fnc,X0),divide(divide(sF1_fnc,X1),X2)),multiply(X3,divide(divide(sF1_fnc,X1),X2)))),X0)),X4))=inverse(divide(divide(sF1_fnc,X3),X4)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6796,f2850])).
% 9.02/1.60 fof(f6796,plain,(
% 9.02/1.60 inverse(divide(sF0_fnc,sF0_fnc))=sF1_fnc),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f4842,f6578])).
% 9.02/1.60 fof(f6807,plain,(
% 9.02/1.60 ![X0]: (multiply(X0,divide(sF0_fnc,divide(sF1_fnc,inverse(a2))))=divide(X0,sF1_fnc))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6422,f6581])).
% 9.02/1.60 fof(f6808,plain,(
% 9.02/1.60 ![X0]: (multiply(X0,divide(sF0_fnc,multiply(sF1_fnc,a2)))=divide(X0,sF1_fnc))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f5,f6807])).
% 9.02/1.60 fof(f6811,plain,(
% 9.02/1.60 ![X0]: (divide(sF1_fnc,divide(X0,sF1_fnc))=divide(sF1_fnc,X0))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6814,f6422])).
% 9.02/1.60 fof(f6814,plain,(
% 9.02/1.60 ![X0]: (multiply(X0,divide(sF0_fnc,sF0_fnc))=divide(X0,sF1_fnc))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f9,f6808])).
% 9.02/1.60 fof(f6821,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(inverse(divide(sF1_fnc,X0)),X1),multiply(sF1_fnc,X1))=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6577,f6588])).
% 9.02/1.60 fof(f6831,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(multiply(sF1_fnc,X0),multiply(X1,X0))),sF1_fnc)=X1)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6617,f966])).
% 9.02/1.60 fof(f6832,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc),X0)=X1)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6617,f66])).
% 9.02/1.60 fof(f6836,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(multiply(sF1_fnc,X2),divide(X1,multiply(inverse(X2),X0)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6617,f1059])).
% 9.02/1.60 fof(f6867,plain,(
% 9.02/1.60 sF1_fnc=inverse(divide(sF1_fnc,sF1_fnc))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6796,f6696])).
% 9.02/1.60 fof(f6869,plain,(
% 9.02/1.60 sF1_fnc=inverse(sF1_fnc)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6599,f6867])).
% 9.02/1.60 fof(f6874,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)=inverse(divide(sF1_fnc,divide(X0,divide(sF1_fnc,sF1_fnc)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6885,f174])).
% 9.02/1.60 fof(f6876,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=inverse(divide(sF1_fnc,divide(X1,divide(sF1_fnc,divide(X0,X2))))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6885,f176])).
% 9.02/1.60 fof(f6877,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(sF1_fnc,divide(X0,divide(sF1_fnc,X1)))),X2),multiply(multiply(X3,divide(divide(sF1_fnc,X3),multiply(sF1_fnc,X4))),X2))=divide(X0,divide(inverse(X4),X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6885,f6237])).
% 9.02/1.60 fof(f6885,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(sF0_fnc,divide(X0,divide(inverse(a2),X1))))=inverse(divide(sF1_fnc,divide(X0,divide(sF1_fnc,X1)))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6796,f6698])).
% 9.02/1.60 fof(f6886,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(multiply(sF1_fnc,a2),X0)),sF1_fnc)=inverse(divide(sF1_fnc,divide(X0,sF0_fnc))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6617,f6699])).
% 9.02/1.60 fof(f6888,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(sF0_fnc,X0)),sF1_fnc)=inverse(divide(sF1_fnc,divide(X0,sF0_fnc))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f9,f6886])).
% 9.02/1.60 fof(f6891,plain,(
% 9.02/1.60 ![X0]: (multiply(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),a2)=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6888,f6701])).
% 9.02/1.60 fof(f6912,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(sF1_fnc,X0)),X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X0,sF1_fnc))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6927,f6711])).
% 9.02/1.60 fof(f6913,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),divide(X2,sF1_fnc)))=divide(X0,divide(inverse(divide(sF1_fnc,X2)),X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6927,f6706])).
% 9.02/1.60 fof(f6927,plain,(
% 9.02/1.60 divide(sF0_fnc,sF0_fnc)=sF1_fnc),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f9,f6724])).
% 9.02/1.60 fof(f6981,plain,(
% 9.02/1.60 ![X0]: (divide(X0,sF1_fnc)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6982,f6703])).
% 9.02/1.60 fof(f6982,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6722,f6831])).
% 9.02/1.60 fof(f6992,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6599,f6874])).
% 9.02/1.60 fof(f6993,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6996,f563])).
% 9.02/1.60 fof(f6996,plain,(
% 9.02/1.60 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF2_fnc),X0)),sF2_fnc)=inverse(divide(sF1_fnc,X0)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6811,f6992])).
% 9.02/1.60 fof(f6998,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(divide(X0,divide(sF1_fnc,X1)),X2)=divide(X0,divide(inverse(X2),X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6760,f6877])).
% 9.02/1.60 fof(f7022,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(X0,divide(divide(sF1_fnc,sF2_fnc),divide(X1,sF2_fnc)))=divide(X0,X1))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f1250])).
% 9.02/1.60 fof(f7039,plain,(
% 9.02/1.60 ![X0]: (multiply(inverse(divide(sF0_fnc,X0)),a2)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6891])).
% 9.02/1.60 fof(f7040,plain,(
% 9.02/1.60 ![X0]: (inverse(divide(sF0_fnc,X0))=inverse(divide(sF1_fnc,divide(X0,sF0_fnc))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6888])).
% 9.02/1.60 fof(f7044,plain,(
% 9.02/1.60 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,X0),X1))=inverse(divide(multiply(sF1_fnc,X2),divide(X1,multiply(inverse(X2),X0)))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6836])).
% 9.02/1.60 fof(f7047,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(inverse(divide(multiply(sF1_fnc,X0),X1)),X0)=X1)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6832])).
% 9.02/1.60 fof(f7070,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(multiply(inverse(sF0_fnc),X0),multiply(multiply(X1,divide(sF1_fnc,X1)),X0))=multiply(X2,divide(divide(sF1_fnc,X2),sF0_fnc)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6171])).
% 9.02/1.60 fof(f7108,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),X2))=divide(X0,divide(inverse(divide(sF1_fnc,X2)),X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6913])).
% 9.02/1.60 fof(f7109,plain,(
% 9.02/1.60 ![X0,X1]: (divide(inverse(divide(sF1_fnc,X0)),X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),X0)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f6981,f6912])).
% 9.02/1.60 fof(f7125,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=divide(X1,divide(sF1_fnc,divide(X0,X2))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7155,f6876])).
% 9.02/1.60 fof(f7153,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(X0,X1),multiply(sF1_fnc,X1))=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7155,f6821])).
% 9.02/1.60 fof(f7155,plain,(
% 9.02/1.60 ![X0]: (inverse(divide(sF1_fnc,X0))=X0)),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6981,f6993])).
% 9.02/1.60 fof(f7167,plain,(
% 9.02/1.60 ![X0,X1]: (inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X0)),X1))=inverse(divide(X0,X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7174,f6681])).
% 9.02/1.60 fof(f7174,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(X0,divide(sF1_fnc,X1))=divide(X0,X1))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f6721,f7022])).
% 9.02/1.60 fof(f7195,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(divide(X0,sF0_fnc),X1),multiply(inverse(a2),X1))=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7210,f834])).
% 9.02/1.60 fof(f7196,plain,(
% 9.02/1.60 ![X0]: (multiply(divide(X0,sF0_fnc),a2)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7210,f7039])).
% 9.02/1.60 fof(f7201,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (multiply(X0,divide(sF0_fnc,divide(X1,divide(inverse(a2),X2))))=divide(X0,divide(inverse(divide(divide(sF1_fnc,multiply(divide(X2,sF0_fnc),X3)),X1)),multiply(inverse(a2),X3))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7210,f3611])).
% 9.02/1.60 fof(f7210,plain,(
% 9.02/1.60 ![X0]: (inverse(divide(sF0_fnc,X0))=divide(X0,sF0_fnc))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7155,f7040])).
% 9.02/1.60 fof(f7233,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(multiply(inverse(sF0_fnc),X0),multiply(divide(X1,X1),X0))=multiply(X2,divide(divide(sF1_fnc,X2),sF0_fnc)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7174,f7070])).
% 9.02/1.60 fof(f7259,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,divide(sF1_fnc,X1)),X2))=divide(X0,divide(X2,X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7155,f7108])).
% 9.02/1.60 fof(f7260,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),X2)=divide(divide(X1,divide(sF1_fnc,X0)),X2))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7263,f6763])).
% 9.02/1.60 fof(f7263,plain,(
% 9.02/1.60 ![X0,X1]: (divide(X0,X1)=inverse(divide(divide(sF1_fnc,divide(sF1_fnc,X1)),X0)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7155,f7109])).
% 9.02/1.60 fof(f7314,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(divide(divide(X0,divide(sF1_fnc,divide(X1,X2))),X3),divide(X4,X3))=divide(X0,divide(X4,divide(X1,X2))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7125,f555])).
% 9.02/1.60 fof(f7347,plain,(
% 9.02/1.60 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,X0),X1))=divide(X1,multiply(divide(X2,X2),X0)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f738])).
% 9.02/1.60 fof(f7369,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(sF1_fnc,divide(divide(multiply(X0,divide(divide(sF1_fnc,X1),X2)),multiply(divide(sF1_fnc,X3),divide(divide(sF1_fnc,X1),X2))),X3)),X4))=inverse(divide(divide(sF1_fnc,X0),X4)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f6775])).
% 9.02/1.60 fof(f7382,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (multiply(divide(divide(X0,X1),multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),divide(X3,multiply(inverse(X2),X4)))),divide(X1,X3)))),X4)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f4994])).
% 9.02/1.60 fof(f7383,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (multiply(divide(divide(X0,X1),multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),divide(X1,multiply(inverse(X2),X3))))),X3)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f69])).
% 9.02/1.60 fof(f7384,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X1),divide(X2,multiply(inverse(X1),X3))))),X3),X2)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f618])).
% 9.02/1.60 fof(f7412,plain,(
% 9.02/1.60 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,X0),X1))=divide(divide(X1,multiply(inverse(X2),X0)),multiply(sF1_fnc,X2)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f7044])).
% 9.02/1.60 fof(f7417,plain,(
% 9.02/1.60 ![X0,X1]: (multiply(divide(X0,multiply(sF1_fnc,X1)),X1)=X0)),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f7047])).
% 9.02/1.60 fof(f7437,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(X0,divide(sF1_fnc,multiply(multiply(X1,divide(divide(sF1_fnc,X1),X2)),divide(X2,X3))))=inverse(divide(X3,X0)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f6102])).
% 9.02/1.60 fof(f7443,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),X2)=divide(divide(X1,X3),divide(sF1_fnc,divide(inverse(divide(X0,X3)),X2))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7463,f4378])).
% 9.02/1.60 fof(f7463,plain,(
% 9.02/1.60 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7263,f7167])).
% 9.02/1.60 fof(f7540,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (multiply(X0,divide(sF0_fnc,divide(X1,divide(inverse(a2),X2))))=divide(X0,divide(X1,divide(sF1_fnc,divide(multiply(divide(X2,sF0_fnc),X3),multiply(inverse(a2),X3))))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7125,f7201])).
% 9.02/1.60 fof(f7548,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(sF1_fnc,X1),divide(X2,divide(X1,X3))))=divide(X0,divide(X2,divide(sF1_fnc,X3))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7549,f3612])).
% 9.02/1.60 fof(f7549,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(sF0_fnc,divide(X1,divide(inverse(a2),X2))))=divide(X0,divide(X1,divide(sF1_fnc,X2))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7195,f7540])).
% 9.02/1.60 fof(f7591,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(sF1_fnc,divide(sF1_fnc,divide(X1,X2))))=divide(X0,divide(X2,X1)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7596,f7259])).
% 9.02/1.60 fof(f7596,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(X0,divide(sF1_fnc,divide(X1,X2)))=divide(divide(X0,divide(sF1_fnc,X1)),X2))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7125,f7260])).
% 9.02/1.60 fof(f7678,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(divide(X0,divide(sF1_fnc,divide(divide(X1,X2),X3))),divide(X4,X3))=divide(X0,divide(X4,divide(X1,X2))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7596,f7314])).
% 9.02/1.60 fof(f7679,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(sF1_fnc,divide(divide(divide(X1,X2),X3),divide(X4,X3))))=divide(X0,divide(X4,divide(X1,X2))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7596,f7678])).
% 9.02/1.60 fof(f7689,plain,(
% 9.02/1.60 ![X0,X1]: (divide(multiply(inverse(sF0_fnc),X0),multiply(sF1_fnc,X0))=multiply(X1,divide(divide(sF1_fnc,X1),sF0_fnc)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7691,f7233])).
% 9.02/1.60 fof(f7691,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(X0,multiply(sF1_fnc,X1))=divide(X0,multiply(divide(X2,X2),X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7347])).
% 9.02/1.60 fof(f7712,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(sF1_fnc,divide(divide(multiply(X1,divide(divide(sF1_fnc,X2),X3)),multiply(divide(sF1_fnc,X4),divide(divide(sF1_fnc,X2),X3))),X4)))=inverse(divide(divide(sF1_fnc,X1),X0)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7369])).
% 9.02/1.60 fof(f7713,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(sF1_fnc,divide(divide(multiply(X1,divide(divide(sF1_fnc,X2),X3)),multiply(divide(sF1_fnc,X4),divide(divide(sF1_fnc,X2),X3))),X4)))=divide(X0,divide(sF1_fnc,X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7712])).
% 9.02/1.60 fof(f7732,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(X0,multiply(sF1_fnc,X1))=divide(divide(X0,multiply(inverse(X2),X1)),multiply(sF1_fnc,X2)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7412])).
% 9.02/1.60 fof(f7770,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(X0,divide(sF1_fnc,multiply(multiply(X1,divide(divide(sF1_fnc,X1),X2)),divide(X2,X3))))=divide(X0,X3))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7437])).
% 9.02/1.60 fof(f7780,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(divide(X0,X1),X2)=divide(divide(X0,X3),divide(sF1_fnc,divide(inverse(divide(X1,X3)),X2))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7443])).
% 9.02/1.60 fof(f7781,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(divide(X0,X1),X2)=divide(divide(X0,X3),divide(sF1_fnc,divide(divide(X3,X1),X2))))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7463,f7780])).
% 9.02/1.60 fof(f7921,plain,(
% 9.02/1.60 ![X0,X1,X2,X3]: (divide(divide(X0,X1),X2)=divide(divide(X0,X3),divide(X2,divide(X3,X1))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7938,f7781])).
% 9.02/1.60 fof(f7925,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(X1,divide(multiply(X2,divide(divide(sF1_fnc,X3),X4)),multiply(divide(sF1_fnc,X1),divide(divide(sF1_fnc,X3),X4)))))=divide(X0,divide(sF1_fnc,X2)))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7938,f7713])).
% 9.02/1.60 fof(f7926,plain,(
% 9.02/1.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(divide(X1,X2),divide(divide(X3,X4),X2)))=divide(X0,divide(X1,divide(X3,X4))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7938,f7679])).
% 9.02/1.60 fof(f7938,plain,(
% 9.02/1.60 ![X0,X1,X2]: (divide(X0,divide(sF1_fnc,divide(X1,X2)))=divide(X0,divide(X2,X1)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7174,f7591])).
% 9.02/1.60 fof(f7945,plain,(
% 9.02/1.60 divide(sF1_fnc,inverse(sF0_fnc))=sF0_fnc),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7950,f6016])).
% 9.02/1.60 fof(f7950,plain,(
% 9.02/1.60 ![X0]: (inverse(sF0_fnc)=multiply(X0,divide(divide(sF1_fnc,X0),sF0_fnc)))),
% 9.02/1.60 inference(forward_demodulation,[status(thm)],[f7153,f7689])).
% 9.02/1.60 fof(f7977,plain,(
% 9.02/1.60 ![X0,X1,X2]: (multiply(X0,divide(divide(sF1_fnc,X1),X2))=divide(X0,divide(X2,divide(sF1_fnc,X1))))),
% 9.02/1.60 inference(backward_demodulation,[status(thm)],[f7921,f7548])).
% 9.02/1.61 fof(f7982,plain,(
% 9.02/1.61 multiply(sF1_fnc,sF0_fnc)=sF0_fnc),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f5,f7945])).
% 9.02/1.61 fof(f7992,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (divide(X0,divide(X1,divide(multiply(X2,divide(divide(sF1_fnc,X3),X4)),divide(divide(sF1_fnc,X1),divide(X4,divide(sF1_fnc,X3))))))=divide(X0,divide(sF1_fnc,X2)))),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f7977,f7925])).
% 9.02/1.61 fof(f7994,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,divide(sF1_fnc,multiply(multiply(X3,divide(divide(sF1_fnc,X3),X4)),divide(X4,X1))))))),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f7977,f6100])).
% 9.02/1.61 fof(f8039,plain,(
% 9.02/1.61 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(sF1_fnc,divide(X1,divide(X2,divide(sF1_fnc,X1)))),X3))=multiply(X0,multiply(X2,X3)))),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f7977,f3960])).
% 9.02/1.61 fof(f8052,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (divide(X0,divide(X1,divide(divide(X2,divide(X3,divide(sF1_fnc,X4))),divide(divide(sF1_fnc,X1),divide(X3,divide(sF1_fnc,X4))))))=divide(X0,divide(sF1_fnc,X2)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7977,f7992])).
% 9.02/1.61 fof(f8054,plain,(
% 9.02/1.61 ![X0,X1,X2]: (divide(X0,divide(X1,divide(X2,divide(sF1_fnc,X1))))=divide(X0,divide(sF1_fnc,X2)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7926,f8052])).
% 9.02/1.61 fof(f8071,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (multiply(divide(divide(X0,X1),divide(sF1_fnc,divide(divide(X1,X2),multiply(sF1_fnc,divide(multiply(sF1_fnc,X3),divide(X2,multiply(inverse(X3),X4))))))),X4)=X0)),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f8115,f7382])).
% 9.02/1.61 fof(f8072,plain,(
% 9.02/1.61 ![X0,X1,X2,X3]: (divide(multiply(divide(X0,divide(sF1_fnc,divide(divide(X1,multiply(inverse(X2),X3)),multiply(sF1_fnc,X2)))),X3),X1)=X0)),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f8115,f7384])).
% 9.02/1.61 fof(f8115,plain,(
% 9.02/1.61 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7770,f7994])).
% 9.02/1.61 fof(f8151,plain,(
% 9.02/1.61 ![X0,X1,X2]: (multiply(X0,multiply(divide(sF1_fnc,divide(sF1_fnc,X1)),X2))=multiply(X0,multiply(X1,X2)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f8054,f8039])).
% 9.02/1.61 fof(f8152,plain,(
% 9.02/1.61 ![X0,X1,X2]: (multiply(X0,divide(sF1_fnc,divide(inverse(X1),X2)))=multiply(X0,multiply(X2,X1)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f6998,f8151])).
% 9.02/1.61 fof(f8180,plain,(
% 9.02/1.61 ![X0,X1,X2]: (divide(X0,divide(inverse(X1),X2))=multiply(X0,multiply(X2,X1)))),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7174,f8152])).
% 9.02/1.61 fof(f8201,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (divide(divide(X0,X1),divide(inverse(X2),divide(divide(X1,X3),multiply(sF1_fnc,divide(multiply(sF1_fnc,X4),divide(X3,multiply(inverse(X4),X2)))))))=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f6998,f8071])).
% 9.02/1.61 fof(f8202,plain,(
% 9.02/1.61 ![X0,X1,X2,X3,X4]: (multiply(divide(X0,X1),multiply(divide(divide(X1,X2),multiply(sF1_fnc,divide(multiply(sF1_fnc,X3),divide(X2,multiply(inverse(X3),X4))))),X4))=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f8180,f8201])).
% 9.02/1.61 fof(f8203,plain,(
% 9.02/1.61 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7383,f8202])).
% 9.02/1.61 fof(f8204,plain,(
% 9.02/1.61 ![X0,X1,X2,X3]: (divide(divide(X0,divide(inverse(X1),divide(divide(X2,multiply(inverse(X3),X1)),multiply(sF1_fnc,X3)))),X2)=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f6998,f8072])).
% 9.02/1.61 fof(f8205,plain,(
% 9.02/1.61 ![X0,X1,X2,X3]: (divide(multiply(X0,multiply(divide(divide(X1,multiply(inverse(X2),X3)),multiply(sF1_fnc,X2)),X3)),X1)=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f8180,f8204])).
% 9.02/1.61 fof(f8206,plain,(
% 9.02/1.61 ![X0,X1,X2]: (divide(multiply(X0,multiply(divide(X1,multiply(sF1_fnc,X2)),X2)),X1)=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7732,f8205])).
% 9.02/1.61 fof(f8208,plain,(
% 9.02/1.61 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f7417,f8206])).
% 9.02/1.61 fof(f8330,plain,(
% 9.02/1.61 ![X0]: (divide(X0,a2)=divide(X0,sF0_fnc))),
% 9.02/1.61 inference(paramodulation,[status(thm)],[f7196,f8208])).
% 9.02/1.61 fof(f8333,plain,(
% 9.02/1.61 divide(sF0_fnc,sF0_fnc)=sF1_fnc),
% 9.02/1.61 inference(paramodulation,[status(thm)],[f7982,f8208])).
% 9.02/1.61 fof(f8380,plain,(
% 9.02/1.61 divide(sF0_fnc,a2)=sF1_fnc),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f8330,f8333])).
% 9.02/1.61 fof(f8655,plain,(
% 9.02/1.61 divide(a2,sF0_fnc)=inverse(sF1_fnc)),
% 9.02/1.61 inference(paramodulation,[status(thm)],[f8380,f7463])).
% 9.02/1.61 fof(f8669,plain,(
% 9.02/1.61 divide(a2,a2)=inverse(sF1_fnc)),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f8330,f8655])).
% 9.02/1.61 fof(f8670,plain,(
% 9.02/1.61 divide(a2,a2)=sF1_fnc),
% 9.02/1.61 inference(forward_demodulation,[status(thm)],[f6869,f8669])).
% 9.02/1.61 fof(f9294,plain,(
% 9.02/1.61 multiply(sF1_fnc,a2)=a2),
% 9.02/1.61 inference(paramodulation,[status(thm)],[f8670,f8203])).
% 9.02/1.61 fof(f9297,plain,(
% 9.02/1.61 sF0_fnc=a2),
% 9.02/1.61 inference(backward_demodulation,[status(thm)],[f9294,f9])).
% 9.02/1.61 fof(f9298,plain,(
% 9.02/1.61 $false),
% 9.02/1.61 inference(forward_subsumption_resolution,[status(thm)],[f9297,f10])).
% 9.02/1.61 % SZS output end CNFRefutation for theBenchmark.p
% 7.50/1.66 % Elapsed time: 1.301352 seconds
% 7.50/1.66 % CPU time: 10.058505 seconds
% 7.50/1.66 % Total memory used: 164.617 MB
% 7.50/1.66 % Net memory used: 156.475 MB
%------------------------------------------------------------------------------