%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP473-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 : n018.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 18.44s 2.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP473-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n018.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:16:30 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 18.44/2.79 % Refutation found
% 18.44/2.79 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.44/2.79 % SZS output start CNFRefutation for theBenchmark
% 18.44/2.79 fof(f1,axiom,(
% 18.44/2.79 (![A,B,C,D]: (divide(divide(inverse(divide(A,B)),divide(divide(C,D),A)),divide(D,C)) = B ))),
% 18.44/2.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.44/2.79 fof(f2,axiom,(
% 18.44/2.79 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 18.44/2.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.44/2.79 fof(f3,negated_conjecture,(
% 18.44/2.79 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 18.44/2.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 18.44/2.79 fof(f4,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 18.44/2.79 inference(cnf_transformation,[status(thm)],[f1])).
% 18.44/2.79 fof(f5,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 18.44/2.79 inference(cnf_transformation,[status(thm)],[f2])).
% 18.44/2.79 fof(f6,plain,(
% 18.44/2.79 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 18.44/2.79 inference(cnf_transformation,[status(thm)],[f3])).
% 18.44/2.79 fof(f7,definition,(
% 18.44/2.79 sF2_fnc=inverse(b2)),
% 18.44/2.79 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 18.44/2.79 fof(f8,definition,(
% 18.44/2.79 sF1_fnc=multiply(sF2_fnc,b2)),
% 18.44/2.79 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 18.44/2.79 fof(f9,definition,(
% 18.44/2.79 sF0_fnc=multiply(sF1_fnc,a2)),
% 18.44/2.79 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 18.44/2.79 fof(f10,plain,(
% 18.44/2.79 ~sF0_fnc=a2),
% 18.44/2.79 inference(definition_folding,[],[f6,f9,f8,f7])).
% 18.44/2.79 fof(f11,plain,(
% 18.44/2.79 ![X0]: (multiply(X0,b2)=divide(X0,sF2_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f7,f5])).
% 18.44/2.79 fof(f12,plain,(
% 18.44/2.79 sF1_fnc=divide(sF2_fnc,sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f11,f8])).
% 18.44/2.79 fof(f13,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(X5,X4))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4,f4])).
% 18.44/2.79 fof(f14,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),divide(divide(X0,X1),sF2_fnc)),divide(X1,X0))=sF2_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f12,f4])).
% 18.44/2.79 fof(f15,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))=inverse(X1))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f4])).
% 18.44/2.79 fof(f16,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(divide(X0,X1),X2)),X3),divide(divide(divide(X1,X0),X4),inverse(divide(X4,X3))))=X2)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4,f4])).
% 18.44/2.79 fof(f17,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2))=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f4])).
% 18.44/2.79 fof(f19,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)),divide(sF2_fnc,sF2_fnc))=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f12,f4])).
% 18.44/2.79 fof(f20,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2))=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f4])).
% 18.44/2.79 fof(f23,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(X2),X3),X0)),multiply(X3,X2))=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f4])).
% 18.44/2.79 fof(f24,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(divide(divide(X0,X1),X2)),X3),multiply(divide(divide(X1,X0),X4),divide(X4,X3)))=X2)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f16])).
% 18.44/2.79 fof(f25,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)),sF1_fnc)=X1)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f12,f19])).
% 18.44/2.79 fof(f28,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(X1,X0)),divide(divide(X2,X3),X1)))),sF1_fnc)=divide(X3,X2))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4,f25])).
% 18.44/2.79 fof(f30,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(multiply(X0,X1)),divide(sF1_fnc,X0)),sF1_fnc)=inverse(X1))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f25])).
% 18.44/2.79 fof(f31,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(sF1_fnc,X0)),sF1_fnc)=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f25])).
% 18.44/2.79 fof(f35,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF1_fnc,X3)))),divide(X2,X1))=sF1_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f25,f4])).
% 18.44/2.79 fof(f65,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(a2),X0)),sF0_fnc),sF1_fnc)=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f9,f31])).
% 18.44/2.79 fof(f75,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(multiply(inverse(a2),X0)),sF0_fnc),sF1_fnc)=inverse(X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f65])).
% 18.44/2.79 fof(f83,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(sF1_fnc,X0)),inverse(X1)),divide(sF0_fnc,inverse(multiply(inverse(a2),X1))))=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f4])).
% 18.44/2.79 fof(f89,plain,(
% 18.44/2.79 ![X0,X1]: (divide(multiply(inverse(divide(sF1_fnc,X0)),X1),divide(sF0_fnc,inverse(multiply(inverse(a2),X1))))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f83])).
% 18.44/2.79 fof(f90,plain,(
% 18.44/2.79 ![X0,X1]: (divide(multiply(inverse(divide(sF1_fnc,X0)),X1),multiply(sF0_fnc,multiply(inverse(a2),X1)))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f89])).
% 18.44/2.79 fof(f107,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(X2,b2)),divide(divide(X3,X4),X2)))),divide(X1,X0))=divide(X4,X3))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f7,f13])).
% 18.44/2.79 fof(f132,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(sF2_fnc),divide(divide(X0,X1),divide(inverse(sF1_fnc),divide(divide(X2,X3),sF2_fnc)))),divide(X1,X0))=divide(X3,X2))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f12,f13])).
% 18.44/2.79 fof(f135,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),inverse(X3)))),divide(X2,X1))=divide(sF0_fnc,inverse(multiply(inverse(a2),X3))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f13])).
% 18.44/2.79 fof(f137,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),inverse(X3)))),divide(X2,X1))=divide(divide(sF1_fnc,X4),inverse(multiply(X4,X3))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f30,f13])).
% 18.44/2.79 fof(f139,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=divide(sF0_fnc,inverse(divide(inverse(a2),X3))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f65,f13])).
% 18.44/2.79 fof(f140,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=divide(multiply(sF1_fnc,X4),inverse(divide(inverse(X4),X3))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f31,f13])).
% 18.44/2.79 fof(f141,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=divide(divide(sF1_fnc,X4),inverse(divide(X4,X3))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f25,f13])).
% 18.44/2.79 fof(f150,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(X4,X3)))),divide(X2,X1))=divide(sF1_fnc,divide(inverse(divide(inverse(a2),X4)),sF0_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f65,f13])).
% 18.44/2.79 fof(f154,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(divide(X6,X7),divide(inverse(X8),divide(divide(X7,X6),divide(inverse(divide(X9,X8)),divide(divide(X5,X4),X9))))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f13,f13])).
% 18.44/2.79 fof(f156,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(multiply(X4,X5),X3)))),divide(X2,X1))=divide(inverse(X5),X4))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f13])).
% 18.44/2.79 fof(f166,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(divide(inverse(X0),divide(divide(divide(X1,X2),divide(inverse(X3),divide(divide(X2,X1),divide(inverse(divide(X4,X3)),divide(divide(X5,X6),X4))))),divide(inverse(divide(X7,X0)),divide(divide(X8,X9),X7)))),divide(X6,X5))=divide(X9,X8))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f13,f13])).
% 18.44/2.79 fof(f181,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=divide(sF0_fnc,inverse(multiply(inverse(a2),X3))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f135])).
% 18.44/2.79 fof(f183,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=multiply(sF0_fnc,multiply(inverse(a2),X3)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f181])).
% 18.44/2.79 fof(f188,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4]: (divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=divide(divide(sF1_fnc,X4),inverse(multiply(X4,X3))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f137])).
% 18.44/2.79 fof(f189,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,multiply(inverse(a2),X0))=divide(divide(sF1_fnc,X1),inverse(multiply(X1,X0))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f183,f188])).
% 18.44/2.79 fof(f191,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,multiply(inverse(a2),X0))=multiply(divide(sF1_fnc,X1),multiply(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f189])).
% 18.44/2.79 fof(f194,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1))=multiply(sF0_fnc,divide(inverse(a2),X3)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f139])).
% 18.44/2.79 fof(f195,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),X0))=divide(multiply(sF1_fnc,X1),inverse(divide(inverse(X1),X0))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f194,f140])).
% 18.44/2.79 fof(f197,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),X0))=multiply(multiply(sF1_fnc,X1),divide(inverse(X1),X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f195])).
% 18.44/2.79 fof(f198,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),X0))=divide(divide(sF1_fnc,X1),inverse(divide(X1,X0))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f194,f141])).
% 18.44/2.79 fof(f200,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),X0))=multiply(divide(sF1_fnc,X1),divide(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f198])).
% 18.44/2.79 fof(f217,plain,(
% 18.44/2.79 divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc))=sF1_fnc),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f150,f35])).
% 18.44/2.79 fof(f233,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5]: (divide(X0,X1)=divide(divide(X2,X3),divide(inverse(X4),divide(divide(X3,X2),divide(inverse(divide(X5,X4)),divide(divide(X0,X1),X5))))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f13,f154])).
% 18.44/2.79 fof(f235,plain,(
% 18.44/2.79 ![X0,X1]: (divide(sF1_fnc,divide(inverse(divide(inverse(a2),multiply(X0,X1))),sF0_fnc))=divide(inverse(X1),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f150,f156])).
% 18.44/2.79 fof(f245,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1))=divide(X5,X4))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f233,f166])).
% 18.44/2.79 fof(f246,plain,(
% 18.44/2.79 ![X0,X1]: (divide(sF1_fnc,divide(inverse(divide(inverse(a2),divide(X0,X1))),sF0_fnc))=divide(X1,X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f150,f245])).
% 18.44/2.79 fof(f263,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),divide(multiply(X0,X1),sF2_fnc)),divide(inverse(X1),X0))=sF2_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f14])).
% 18.44/2.79 fof(f327,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f217,f200])).
% 18.44/2.79 fof(f439,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(multiply(inverse(divide(X0,X1)),X2),multiply(sF0_fnc,multiply(inverse(a2),X2)))=divide(inverse(divide(inverse(a2),divide(X1,X0))),sF0_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f246,f90])).
% 18.44/2.79 fof(f481,plain,(
% 18.44/2.79 ![X0]: (divide(inverse(divide(inverse(a2),divide(X0,sF1_fnc))),sF0_fnc)=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f439,f90])).
% 18.44/2.79 fof(f495,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(divide(inverse(a2),X0)),sF0_fnc)=divide(inverse(divide(inverse(X1),X0)),multiply(sF1_fnc,X1)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f31,f481])).
% 18.44/2.79 fof(f501,plain,(
% 18.44/2.79 ![X0]: (divide(sF1_fnc,divide(inverse(divide(inverse(a2),X0)),sF0_fnc))=divide(sF0_fnc,inverse(divide(inverse(a2),divide(X0,sF1_fnc)))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f481,f246])).
% 18.44/2.79 fof(f529,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(divide(X0,X1),sF1_fnc)))=divide(X1,X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f546,f246])).
% 18.44/2.79 fof(f530,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=sF1_fnc),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f546,f217])).
% 18.44/2.79 fof(f531,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(multiply(X0,X1),sF1_fnc)))=divide(inverse(X1),X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f546,f235])).
% 18.44/2.79 fof(f546,plain,(
% 18.44/2.79 ![X0]: (divide(sF1_fnc,divide(inverse(divide(inverse(a2),X0)),sF0_fnc))=multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f501])).
% 18.44/2.79 fof(f561,plain,(
% 18.44/2.79 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(inverse(X0),sF1_fnc)))=divide(sF1_fnc,divide(inverse(multiply(inverse(a2),X0)),sF0_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f529])).
% 18.44/2.79 fof(f581,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),divide(divide(X0,X1),sF0_fnc)),divide(X1,X0))=inverse(divide(inverse(a2),divide(sF1_fnc,sF1_fnc))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f530,f15])).
% 18.44/2.79 fof(f891,plain,(
% 18.44/2.79 divide(divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc)),divide(inverse(a2),sF1_fnc))=sF2_fnc),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f9,f263])).
% 18.44/2.79 fof(f1062,plain,(
% 18.44/2.79 ![X0,X1,X2,X3,X4,X5]: (divide(divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(X1,X0)),divide(divide(X2,X3),X1)))),sF1_fnc)=divide(sF1_fnc,divide(inverse(X4),divide(sF1_fnc,divide(inverse(divide(X5,X4)),divide(divide(X3,X2),X5))))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f28,f28])).
% 18.44/2.79 fof(f1079,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(divide(sF1_fnc,divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(X1,X0)),divide(divide(X2,X3),X1))))),divide(X3,X2)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f28,f200])).
% 18.44/2.79 fof(f1127,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(X0,X1)=divide(sF1_fnc,divide(inverse(X2),divide(sF1_fnc,divide(inverse(divide(X3,X2)),divide(divide(X0,X1),X3))))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f28,f1062])).
% 18.44/2.79 fof(f1153,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(divide(X0,X1),divide(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1127,f1079])).
% 18.44/2.79 fof(f1174,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(sF1_fnc,divide(sF2_fnc,sF2_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f12,f1153])).
% 18.44/2.79 fof(f1175,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(multiply(X0,X1),divide(inverse(X1),X0)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f1153])).
% 18.44/2.79 fof(f1176,plain,(
% 18.44/2.79 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(divide(sF0_fnc,inverse(divide(inverse(a2),divide(X0,sF1_fnc)))),X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f481,f1153])).
% 18.44/2.79 fof(f1190,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(divide(inverse(X0),X1),multiply(X1,X0)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f1153])).
% 18.44/2.79 fof(f1217,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),sF1_fnc))=multiply(sF1_fnc,sF1_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f12,f1174])).
% 18.44/2.79 fof(f1218,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF1_fnc,sF1_fnc)=multiply(multiply(X0,X1),divide(inverse(X1),X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1217,f1175])).
% 18.44/2.79 fof(f1219,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,sF1_fnc)=multiply(divide(sF0_fnc,inverse(divide(inverse(a2),divide(X0,sF1_fnc)))),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1217,f1176])).
% 18.44/2.79 fof(f1220,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,sF1_fnc)=multiply(multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f1219])).
% 18.44/2.79 fof(f1243,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF1_fnc,sF1_fnc)=multiply(divide(inverse(X0),X1),multiply(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1217,f1190])).
% 18.44/2.79 fof(f1252,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)))=divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1217,f531])).
% 18.44/2.79 fof(f1261,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(inverse(sF1_fnc),sF1_fnc)))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f1268,f327])).
% 18.44/2.79 fof(f1268,plain,(
% 18.44/2.79 divide(inverse(sF1_fnc),sF1_fnc)=divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f531,f1252])).
% 18.44/2.79 fof(f1269,plain,(
% 18.44/2.79 divide(sF1_fnc,divide(inverse(multiply(inverse(a2),sF1_fnc)),sF0_fnc))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f561,f1261])).
% 18.44/2.79 fof(f1346,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=multiply(divide(inverse(a2),sF1_fnc),sF0_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f9,f1243])).
% 18.44/2.79 fof(f1372,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(sF0_fnc),X0)),multiply(sF1_fnc,sF1_fnc)),divide(sF1_fnc,inverse(a2)))=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1346,f17])).
% 18.44/2.79 fof(f1375,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)))=divide(inverse(sF0_fnc),divide(inverse(a2),sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1346,f531])).
% 18.44/2.79 fof(f1378,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(sF0_fnc),X0)),multiply(sF1_fnc,sF1_fnc)),multiply(sF1_fnc,a2))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f1372])).
% 18.44/2.79 fof(f1379,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(sF0_fnc),X0)),multiply(sF1_fnc,sF1_fnc)),sF0_fnc)=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f9,f1378])).
% 18.44/2.79 fof(f1382,plain,(
% 18.44/2.79 divide(inverse(sF1_fnc),sF1_fnc)=divide(inverse(sF0_fnc),divide(inverse(a2),sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f531,f1375])).
% 18.44/2.79 fof(f1411,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)))=divide(inverse(divide(inverse(X0),X1)),multiply(X1,X0)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1218,f531])).
% 18.44/2.79 fof(f1412,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(multiply(sF1_fnc,sF1_fnc)),divide(divide(X0,X1),multiply(X2,X3))),divide(X1,X0))=inverse(divide(inverse(X3),X2)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1218,f15])).
% 18.44/2.79 fof(f1436,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(sF1_fnc),sF1_fnc)=divide(inverse(divide(inverse(X0),X1)),multiply(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f531,f1411])).
% 18.44/2.79 fof(f1496,plain,(
% 18.44/2.79 divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc)=sF1_fnc),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1268,f65])).
% 18.44/2.79 fof(f1556,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc),divide(sF1_fnc,inverse(sF1_fnc)))=inverse(X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1496,f15])).
% 18.44/2.79 fof(f1557,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),divide(sF1_fnc,inverse(sF1_fnc)))=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1496,f4])).
% 18.44/2.79 fof(f1568,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1496,f529])).
% 18.44/2.79 fof(f1578,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc),multiply(sF1_fnc,sF1_fnc))=inverse(X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f1556])).
% 18.44/2.79 fof(f1579,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),multiply(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f1557])).
% 18.44/2.79 fof(f1592,plain,(
% 18.44/2.79 sF1_fnc=divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f530,f1568])).
% 18.44/2.79 fof(f1848,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(divide(divide(X0,X1),X2)),divide(inverse(sF1_fnc),sF1_fnc)),multiply(divide(divide(X1,X0),sF1_fnc),sF1_fnc))=X2)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1592,f24])).
% 18.44/2.79 fof(f1891,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(X0),divide(multiply(X1,X2),divide(inverse(divide(sF1_fnc,X0)),sF1_fnc))),divide(inverse(X2),X1))=multiply(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1579,f20])).
% 18.44/2.79 fof(f1925,plain,(
% 18.44/2.79 divide(divide(inverse(divide(inverse(sF1_fnc),sF1_fnc)),multiply(sF1_fnc,sF1_fnc)),sF0_fnc)=divide(inverse(a2),sF1_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1382,f1379])).
% 18.44/2.79 fof(f1951,plain,(
% 18.44/2.79 divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF0_fnc)=divide(inverse(a2),sF1_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f495,f1925])).
% 18.44/2.79 fof(f1952,plain,(
% 18.44/2.79 divide(divide(inverse(sF1_fnc),sF1_fnc),sF0_fnc)=divide(inverse(a2),sF1_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1268,f1951])).
% 18.44/2.79 fof(f2012,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(divide(inverse(a2),sF1_fnc),sF1_fnc)))=divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1952,f529])).
% 18.44/2.79 fof(f2023,plain,(
% 18.44/2.79 divide(sF1_fnc,inverse(a2))=divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f529,f2012])).
% 18.44/2.79 fof(f2024,plain,(
% 18.44/2.79 multiply(sF1_fnc,a2)=divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2023])).
% 18.44/2.79 fof(f2033,plain,(
% 18.44/2.79 sF0_fnc=divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f9,f2024])).
% 18.44/2.79 fof(f2041,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF0_fnc),divide(multiply(X0,X1),sF0_fnc)),divide(inverse(X1),X0))=divide(inverse(sF1_fnc),sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2033,f20])).
% 18.44/2.79 fof(f2052,plain,(
% 18.44/2.79 multiply(sF0_fnc,divide(inverse(a2),divide(inverse(sF1_fnc),sF1_fnc)))=multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2033,f200])).
% 18.44/2.79 fof(f2067,plain,(
% 18.44/2.79 multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2068,f1269])).
% 18.44/2.79 fof(f2068,plain,(
% 18.44/2.79 divide(sF1_fnc,divide(inverse(multiply(inverse(a2),sF1_fnc)),sF0_fnc))=multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f561,f2052])).
% 18.44/2.79 fof(f2073,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(sF1_fnc),X0)),multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),divide(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2067,f17])).
% 18.44/2.79 fof(f2442,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=divide(multiply(sF0_fnc,divide(inverse(a2),divide(b2,sF1_fnc))),sF2_fnc)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f11,f1220])).
% 18.44/2.79 fof(f2506,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),sF1_fnc),divide(X0,X1))=divide(X1,X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1436,f17])).
% 18.44/2.79 fof(f2605,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),X0)=divide(sF0_fnc,inverse(divide(inverse(a2),divide(X0,sF1_fnc)))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f481,f2506])).
% 18.44/2.79 fof(f2609,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),inverse(X0))=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1578,f2506])).
% 18.44/2.79 fof(f2610,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),inverse(X0))=divide(sF1_fnc,divide(inverse(multiply(inverse(a2),X0)),sF0_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f2506])).
% 18.44/2.79 fof(f2612,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),sF1_fnc),divide(X0,X1))=divide(divide(X1,X0),divide(inverse(sF1_fnc),sF1_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2506,f2506])).
% 18.44/2.79 fof(f2615,plain,(
% 18.44/2.79 divide(divide(inverse(sF1_fnc),sF1_fnc),sF2_fnc)=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f891,f2506])).
% 18.44/2.79 fof(f2620,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),X0)=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1579,f2506])).
% 18.44/2.79 fof(f2629,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),sF1_fnc),multiply(X0,X1))=divide(inverse(X1),X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f5,f2506])).
% 18.44/2.79 fof(f2632,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),X2),multiply(divide(divide(sF1_fnc,inverse(sF1_fnc)),X3),divide(X3,X2)))=divide(X1,X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2506,f24])).
% 18.44/2.79 fof(f2647,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,X1)))=multiply(divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(X1,X0)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2506,f200])).
% 18.44/2.79 fof(f2667,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=divide(divide(divide(inverse(sF1_fnc),sF1_fnc),b2),sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2699,f2442])).
% 18.44/2.79 fof(f2699,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),X0)=multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2605])).
% 18.44/2.79 fof(f2724,plain,(
% 18.44/2.79 ![X0]: (multiply(divide(inverse(sF1_fnc),sF1_fnc),X0)=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2609])).
% 18.44/2.79 fof(f2725,plain,(
% 18.44/2.79 multiply(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc)=multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2742,f2068])).
% 18.44/2.79 fof(f2742,plain,(
% 18.44/2.79 ![X0]: (multiply(divide(inverse(sF1_fnc),sF1_fnc),X0)=divide(sF1_fnc,divide(inverse(multiply(inverse(a2),X0)),sF0_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2610])).
% 18.44/2.79 fof(f2750,plain,(
% 18.44/2.79 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),divide(inverse(sF1_fnc),sF1_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2506,f2612])).
% 18.44/2.79 fof(f2777,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),X2),multiply(divide(multiply(sF1_fnc,sF1_fnc),X3),divide(X3,X2)))=divide(X1,X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2632])).
% 18.44/2.79 fof(f2796,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),X0)=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2801,f2699])).
% 18.44/2.79 fof(f2801,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,X1)))=multiply(sF1_fnc,divide(X1,X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f1592,f2647])).
% 18.44/2.79 fof(f2835,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF1_fnc,divide(sF1_fnc,divide(X0,X1)))=divide(X1,X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f2506])).
% 18.44/2.79 fof(f2837,plain,(
% 18.44/2.79 multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))=sF1_fnc),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f1496])).
% 18.44/2.79 fof(f2838,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=divide(multiply(sF1_fnc,divide(sF1_fnc,b2)),sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f2667])).
% 18.44/2.79 fof(f2843,plain,(
% 18.44/2.79 multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc))=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f2615])).
% 18.44/2.79 fof(f2844,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))=divide(inverse(X1),X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f2629])).
% 18.44/2.79 fof(f2874,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,X0))=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2796,f2620])).
% 18.44/2.79 fof(f2877,plain,(
% 18.44/2.79 divide(divide(inverse(sF1_fnc),sF1_fnc),multiply(sF1_fnc,sF1_fnc))=inverse(divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2837,f1578])).
% 18.44/2.79 fof(f2889,plain,(
% 18.44/2.79 multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))=inverse(divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2796,f2877])).
% 18.44/2.79 fof(f2898,plain,(
% 18.44/2.79 ![X0]: (divide(inverse(divide(sF1_fnc,sF1_fnc)),X0)=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f2796])).
% 18.44/2.79 fof(f2915,plain,(
% 18.44/2.79 multiply(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)=multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f2725])).
% 18.44/2.79 fof(f2919,plain,(
% 18.44/2.79 ![X0,X1]: (divide(X0,X1)=divide(divide(X0,X1),inverse(divide(sF1_fnc,sF1_fnc))))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f2750])).
% 18.44/2.79 fof(f2922,plain,(
% 18.44/2.79 ![X0]: (multiply(inverse(divide(sF1_fnc,sF1_fnc)),X0)=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f2724])).
% 18.44/2.79 fof(f2937,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF0_fnc),divide(multiply(X0,X1),sF0_fnc)),divide(inverse(X1),X0))=inverse(divide(sF1_fnc,sF1_fnc)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f2041])).
% 18.44/2.79 fof(f2944,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(divide(divide(X0,X1),X2)),inverse(divide(sF1_fnc,sF1_fnc))),multiply(divide(divide(X1,X0),sF1_fnc),sF1_fnc))=X2)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f2958,f1848])).
% 18.44/2.79 fof(f2958,plain,(
% 18.44/2.79 divide(inverse(sF1_fnc),sF1_fnc)=inverse(divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2844,f2889])).
% 18.44/2.79 fof(f2975,plain,(
% 18.44/2.79 ![X0,X1]: (divide(X0,X1)=multiply(divide(X0,X1),divide(sF1_fnc,sF1_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2919])).
% 18.44/2.79 fof(f2977,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(multiply(inverse(divide(divide(X0,X1),X2)),divide(sF1_fnc,sF1_fnc)),multiply(divide(divide(X1,X0),sF1_fnc),sF1_fnc))=X2)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f2944])).
% 18.44/2.79 fof(f3013,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(multiply(sF1_fnc,sF1_fnc),b2)),inverse(X2)))),divide(X1,X0))=divide(sF1_fnc,inverse(multiply(sF1_fnc,X2))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1578,f107])).
% 18.44/2.79 fof(f3014,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(sF1_fnc,b2)),inverse(X2)))),divide(X1,X0))=divide(sF0_fnc,inverse(multiply(inverse(a2),X2))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f107])).
% 18.44/2.79 fof(f3030,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(X2,b2)),divide(X3,X2)))),divide(X1,X0))=divide(sF0_fnc,inverse(divide(inverse(a2),divide(X3,sF1_fnc)))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f481,f107])).
% 18.44/2.79 fof(f3034,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(X2,b2)),divide(inverse(X3),X2)))),divide(X1,X0))=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X3)),sF1_fnc)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f1578,f107])).
% 18.44/2.79 fof(f3135,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(divide(multiply(sF1_fnc,sF1_fnc),b2)),X2))),divide(X1,X0))=divide(sF1_fnc,inverse(multiply(sF1_fnc,X2))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3013])).
% 18.44/2.79 fof(f3137,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(divide(multiply(sF1_fnc,sF1_fnc),b2)),X2))),divide(X1,X0))=multiply(sF1_fnc,multiply(sF1_fnc,X2)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3135])).
% 18.44/2.79 fof(f3138,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(divide(sF1_fnc,b2)),X2))),divide(X1,X0))=divide(sF0_fnc,inverse(multiply(inverse(a2),X2))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3014])).
% 18.44/2.79 fof(f3140,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(divide(sF1_fnc,b2)),X2))),divide(X1,X0))=multiply(sF0_fnc,multiply(inverse(a2),X2)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3138])).
% 18.44/2.79 fof(f3160,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(X2,b2)),divide(X3,X2)))),divide(X1,X0))=multiply(sF0_fnc,divide(inverse(a2),divide(X3,sF1_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3030])).
% 18.44/2.79 fof(f3162,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(sF2_fnc,divide(divide(X0,X1),divide(inverse(divide(X2,b2)),divide(X3,X2)))),divide(X1,X0))=multiply(sF1_fnc,divide(sF1_fnc,X3)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2801,f3160])).
% 18.44/2.79 fof(f3173,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,inverse(X0)))=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f3162,f3034])).
% 18.44/2.79 fof(f3174,plain,(
% 18.44/2.79 ![X0]: (multiply(inverse(divide(sF1_fnc,sF1_fnc)),X0)=multiply(sF1_fnc,multiply(sF1_fnc,X0)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3175,f2922])).
% 18.44/2.79 fof(f3175,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3173])).
% 18.44/2.79 fof(f3247,plain,(
% 18.44/2.79 multiply(sF1_fnc,multiply(sF1_fnc,sF1_fnc))=multiply(divide(sF1_fnc,sF0_fnc),sF0_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3174,f2915])).
% 18.44/2.79 fof(f3270,plain,(
% 18.44/2.79 ![X0]: (divide(divide(inverse(divide(inverse(sF1_fnc),X0)),multiply(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),divide(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3247,f2073])).
% 18.44/2.79 fof(f3824,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(sF1_fnc,inverse(sF1_fnc)),X0)),inverse(divide(sF1_fnc,sF1_fnc)))=X1)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2958,f17])).
% 18.44/2.79 fof(f3828,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(divide(inverse(divide(sF1_fnc,sF1_fnc)),X0)),X1),multiply(divide(divide(sF1_fnc,inverse(sF1_fnc)),X2),divide(X2,X1)))=X0)),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2958,f24])).
% 18.44/2.79 fof(f3853,plain,(
% 18.44/2.79 ![X0,X1]: (multiply(divide(inverse(divide(inverse(X0),X1)),multiply(divide(sF1_fnc,inverse(sF1_fnc)),X0)),divide(sF1_fnc,sF1_fnc))=X1)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3824])).
% 18.44/2.79 fof(f3854,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(sF1_fnc,inverse(sF1_fnc)),X0))=X1)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2975,f3853])).
% 18.44/2.79 fof(f3855,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(divide(inverse(X0),X1)),multiply(multiply(sF1_fnc,sF1_fnc),X0))=X1)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3854])).
% 18.44/2.79 fof(f3861,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(multiply(sF1_fnc,divide(sF1_fnc,X0))),X1),multiply(divide(divide(sF1_fnc,inverse(sF1_fnc)),X2),divide(X2,X1)))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2898,f3828])).
% 18.44/2.79 fof(f3862,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(multiply(sF1_fnc,divide(sF1_fnc,X0))),X1),multiply(divide(multiply(sF1_fnc,sF1_fnc),X2),divide(X2,X1)))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3861])).
% 18.44/2.79 fof(f3922,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),sF1_fnc),multiply(sF1_fnc,sF1_fnc))=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2835,f1578])).
% 18.44/2.79 fof(f3930,plain,(
% 18.44/2.79 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),sF1_fnc)),divide(X3,X2))=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f2835,f15])).
% 18.44/2.79 fof(f3944,plain,(
% 18.44/2.79 ![X0]: (inverse(divide(sF1_fnc,divide(X0,sF1_fnc)))=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3922,f1579])).
% 18.44/2.79 fof(f3961,plain,(
% 18.44/2.79 ![X0]: (inverse(divide(sF1_fnc,inverse(X0)))=divide(inverse(multiply(inverse(a2),X0)),sF0_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f75,f3944])).
% 18.44/2.79 fof(f3963,plain,(
% 18.44/2.79 ![X0]: (inverse(divide(sF1_fnc,X0))=divide(inverse(divide(inverse(a2),X0)),sF0_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f65,f3944])).
% 18.44/2.79 fof(f3966,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(X0,divide(divide(X1,X2),sF1_fnc)),divide(X2,X1))=divide(X0,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f3944,f4])).
% 18.44/2.79 fof(f3994,plain,(
% 18.44/2.79 ![X0]: (divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)=inverse(X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4009,f75])).
% 18.44/2.79 fof(f4009,plain,(
% 18.44/2.79 ![X0]: (inverse(multiply(sF1_fnc,X0))=divide(inverse(multiply(inverse(a2),X0)),sF0_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f3961])).
% 18.44/2.79 fof(f4023,plain,(
% 18.44/2.79 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3963,f65])).
% 18.44/2.79 fof(f4044,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(divide(X0,X1)),sF1_fnc)=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3966,f3930])).
% 18.44/2.79 fof(f4084,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=divide(multiply(sF1_fnc,sF1_fnc),inverse(X0)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f3994,f3175])).
% 18.44/2.79 fof(f4123,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,X0))=divide(multiply(sF1_fnc,sF1_fnc),X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4023,f2874])).
% 18.44/2.79 fof(f4126,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(X0),divide(multiply(X1,X2),X0)),divide(inverse(X2),X1))=multiply(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4023,f1891])).
% 18.44/2.79 fof(f4206,plain,(
% 18.44/2.79 ![X0,X1]: (divide(inverse(divide(inverse(X0),X1)),multiply(sF1_fnc,multiply(sF1_fnc,X0)))=X1)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4210,f3855])).
% 18.44/2.79 fof(f4210,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=multiply(multiply(sF1_fnc,sF1_fnc),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f5,f4084])).
% 18.44/2.79 fof(f4222,plain,(
% 18.44/2.79 ![X0,X1]: (divide(multiply(sF1_fnc,sF1_fnc),divide(X0,X1))=divide(X1,X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f2835])).
% 18.44/2.79 fof(f4224,plain,(
% 18.44/2.79 divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)=sF1_fnc),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f2837])).
% 18.44/2.79 fof(f4225,plain,(
% 18.44/2.79 ![X0,X1]: (divide(multiply(sF1_fnc,sF1_fnc),multiply(X0,X1))=divide(inverse(X1),X0))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f2844])).
% 18.44/2.79 fof(f4227,plain,(
% 18.44/2.79 divide(multiply(sF1_fnc,sF1_fnc),sF2_fnc)=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f2843])).
% 18.44/2.79 fof(f4231,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=divide(divide(multiply(sF1_fnc,sF1_fnc),b2),sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f2838])).
% 18.44/2.79 fof(f4233,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(divide(multiply(sF1_fnc,sF1_fnc),X0)),X1),multiply(divide(multiply(sF1_fnc,sF1_fnc),X2),divide(X2,X1)))=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4123,f3862])).
% 18.44/2.79 fof(f4282,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=inverse(divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4126,f2937])).
% 18.44/2.79 fof(f4296,plain,(
% 18.44/2.79 ![X0]: (divide(X0,divide(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4206,f3270])).
% 18.44/2.79 fof(f4309,plain,(
% 18.44/2.79 ![X0]: (divide(X0,multiply(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2777,f4233])).
% 18.44/2.79 fof(f4315,plain,(
% 18.44/2.79 divide(inverse(sF1_fnc),sF1_fnc)=multiply(sF1_fnc,sF1_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4282,f2958])).
% 18.44/2.79 fof(f4353,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF1_fnc),divide(divide(X0,X1),sF0_fnc)),divide(X1,X0))=inverse(inverse(a2)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4296,f581])).
% 18.44/2.79 fof(f4385,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(divide(X0,X1),divide(inverse(sF1_fnc),divide(sF2_fnc,sF2_fnc)))),divide(X1,X0))=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc))))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f891,f132])).
% 18.44/2.79 fof(f4459,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(divide(X0,X1),divide(inverse(sF1_fnc),sF1_fnc))),divide(X1,X0))=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f12,f4385])).
% 18.44/2.79 fof(f4460,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(divide(X0,X1),multiply(sF1_fnc,sF1_fnc))),divide(X1,X0))=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4315,f4459])).
% 18.44/2.79 fof(f4461,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,X1)),divide(X1,X0))=divide(divide(inverse(a2),sF1_fnc),divide(inverse(sF1_fnc),divide(sF0_fnc,sF2_fnc))))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4309,f4460])).
% 18.44/2.79 fof(f4462,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,X1)),divide(X1,X0))=divide(multiply(sF1_fnc,sF1_fnc),sF2_fnc))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4227,f4461])).
% 18.44/2.79 fof(f4634,plain,(
% 18.44/2.79 ![X0,X1]: (X0=divide(inverse(divide(X1,X0)),divide(divide(sF1_fnc,sF1_fnc),X1)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4,f4296])).
% 18.44/2.79 fof(f4636,plain,(
% 18.44/2.79 inverse(sF1_fnc)=sF1_fnc),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f3944])).
% 18.44/2.79 fof(f4645,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(inverse(X0)),multiply(divide(X1,X2),X0)),divide(X2,X1))=divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f17])).
% 18.44/2.79 fof(f4646,plain,(
% 18.44/2.79 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=multiply(multiply(sF1_fnc,X0),inverse(X0)))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f197])).
% 18.44/2.79 fof(f4656,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(X0),divide(divide(inverse(X1),X2),X0)),multiply(X2,X1))=divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f23])).
% 18.44/2.79 fof(f4667,plain,(
% 18.44/2.79 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=multiply(divide(sF1_fnc,X0),X0))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f200])).
% 18.44/2.79 fof(f4672,plain,(
% 18.44/2.79 ![X0,X1,X2]: (divide(divide(inverse(X0),divide(divide(X1,X2),X0)),divide(X2,X1))=divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(paramodulation,[status(thm)],[f4296,f4])).
% 18.44/2.79 fof(f4676,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(sF1_fnc,divide(divide(X0,X1),sF2_fnc)),divide(X1,X0))=sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4636,f14])).
% 18.44/2.79 fof(f4694,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(sF1_fnc,divide(divide(X0,X1),sF0_fnc)),divide(X1,X0))=inverse(inverse(a2)))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4636,f4353])).
% 18.44/2.79 fof(f4699,plain,(
% 18.44/2.79 divide(sF1_fnc,sF1_fnc)=multiply(sF1_fnc,sF1_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4636,f4315])).
% 18.44/2.79 fof(f4767,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))=multiply(multiply(sF1_fnc,X0),inverse(X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2801,f4646])).
% 18.44/2.79 fof(f4768,plain,(
% 18.44/2.79 ![X0]: (divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,X0),inverse(X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4123,f4767])).
% 18.44/2.79 fof(f4770,plain,(
% 18.44/2.79 ![X0]: (sF1_fnc=multiply(multiply(sF1_fnc,X0),inverse(X0)))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4224,f4768])).
% 18.44/2.79 fof(f4778,plain,(
% 18.44/2.79 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))=multiply(divide(sF1_fnc,X0),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f2801,f4667])).
% 18.44/2.79 fof(f4779,plain,(
% 18.44/2.79 ![X0]: (divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)=multiply(divide(sF1_fnc,X0),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4123,f4778])).
% 18.44/2.79 fof(f4781,plain,(
% 18.44/2.79 ![X0]: (sF1_fnc=multiply(divide(sF1_fnc,X0),X0))),
% 18.44/2.79 inference(forward_demodulation,[status(thm)],[f4224,f4779])).
% 18.44/2.79 fof(f4807,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,X1)),divide(X1,X0))=divide(divide(sF1_fnc,sF1_fnc),sF2_fnc))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4699,f4462])).
% 18.44/2.79 fof(f4837,plain,(
% 18.44/2.79 divide(sF1_fnc,sF1_fnc)=inverse(divide(sF1_fnc,sF1_fnc))),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4699,f4282])).
% 18.44/2.79 fof(f4876,plain,(
% 18.44/2.79 multiply(sF1_fnc,sF1_fnc)=divide(divide(divide(sF1_fnc,sF1_fnc),b2),sF2_fnc)),
% 18.44/2.79 inference(backward_demodulation,[status(thm)],[f4699,f4231])).
% 18.44/2.79 fof(f4877,plain,(
% 18.44/2.79 ![X0,X1]: (divide(divide(sF1_fnc,sF1_fnc),multiply(X0,X1))=divide(inverse(X1),X0))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f4699,f4225])).
% 18.44/2.80 fof(f4879,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(sF1_fnc,sF1_fnc),divide(X0,X1))=divide(X1,X0))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f4699,f4222])).
% 18.44/2.80 fof(f4888,plain,(
% 18.44/2.80 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=multiply(divide(sF1_fnc,sF1_fnc),X0))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f4699,f4210])).
% 18.44/2.80 fof(f4899,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(divide(divide(sF1_fnc,sF1_fnc),b2)),X2))),divide(X1,X0))=multiply(sF1_fnc,multiply(sF1_fnc,X2)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f4699,f3137])).
% 18.44/2.80 fof(f4910,plain,(
% 18.44/2.80 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),divide(divide(X0,X1),multiply(X2,X3))),divide(X1,X0))=inverse(divide(inverse(X3),X2)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f4699,f1412])).
% 18.44/2.80 fof(f4969,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=divide(divide(divide(sF1_fnc,sF1_fnc),b2),sF2_fnc)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4699,f4876])).
% 18.44/2.80 fof(f5004,plain,(
% 18.44/2.80 ![X0,X1,X2,X3]: (divide(divide(divide(sF1_fnc,sF1_fnc),divide(divide(X0,X1),multiply(X2,X3))),divide(X1,X0))=inverse(divide(inverse(X3),X2)))),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4837,f4910])).
% 18.44/2.80 fof(f5005,plain,(
% 18.44/2.80 ![X0,X1,X2,X3]: (divide(divide(multiply(X0,X1),divide(X2,X3)),divide(X3,X2))=inverse(divide(inverse(X1),X0)))),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4879,f5004])).
% 18.44/2.80 fof(f5043,plain,(
% 18.44/2.80 ![X0]: (multiply(X0,sF1_fnc)=divide(X0,sF1_fnc))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f4636,f5])).
% 18.44/2.80 fof(f5078,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(multiply(inverse(divide(divide(X0,X1),X2)),divide(sF1_fnc,sF1_fnc)),divide(divide(divide(X1,X0),sF1_fnc),sF1_fnc))=X2)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5043,f2977])).
% 18.44/2.80 fof(f5141,plain,(
% 18.44/2.80 sF1_fnc=divide(divide(sF1_fnc,b2),sF2_fnc)),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f11,f4781])).
% 18.44/2.80 fof(f5150,plain,(
% 18.44/2.80 ![X0]: (multiply(sF0_fnc,multiply(inverse(a2),X0))=multiply(divide(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f4781,f191])).
% 18.44/2.80 fof(f5159,plain,(
% 18.44/2.80 ![X0]: (multiply(sF0_fnc,multiply(inverse(a2),X0))=divide(divide(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f5043,f5150])).
% 18.44/2.80 fof(f5174,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(inverse(sF1_fnc),divide(divide(X0,X1),multiply(sF1_fnc,X2))),divide(X1,X0))=inverse(inverse(X2)))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f4770,f15])).
% 18.44/2.80 fof(f5187,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(sF1_fnc,divide(divide(X0,X1),multiply(sF1_fnc,X2))),divide(X1,X0))=inverse(inverse(X2)))),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4636,f5174])).
% 18.44/2.80 fof(f5263,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,sF1_fnc),divide(b2,sF1_fnc))=sF2_fnc),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5141,f4676])).
% 18.44/2.80 fof(f5278,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,divide(divide(sF2_fnc,divide(sF1_fnc,b2)),sF2_fnc)),sF1_fnc)=sF2_fnc),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5141,f4676])).
% 18.44/2.80 fof(f5318,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(sF2_fnc),X2))),divide(X1,X0))=multiply(sF0_fnc,multiply(inverse(a2),X2)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5319,f3140])).
% 18.44/2.80 fof(f5319,plain,(
% 18.44/2.80 divide(sF1_fnc,b2)=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4879,f5263])).
% 18.44/2.80 fof(f5336,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,divide(divide(sF2_fnc,sF2_fnc),sF2_fnc)),sF1_fnc)=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f5319,f5278])).
% 18.44/2.80 fof(f5337,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,divide(sF1_fnc,sF2_fnc)),sF1_fnc)=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f12,f5336])).
% 18.44/2.80 fof(f5338,plain,(
% 18.44/2.80 multiply(sF0_fnc,multiply(inverse(a2),sF2_fnc))=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f5159,f5337])).
% 18.44/2.80 fof(f5522,plain,(
% 18.44/2.80 ![X0]: (multiply(sF0_fnc,multiply(inverse(a2),X0))=multiply(sF2_fnc,multiply(b2,X0)))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5319,f191])).
% 18.44/2.80 fof(f5582,plain,(
% 18.44/2.80 multiply(sF2_fnc,multiply(b2,sF2_fnc))=sF2_fnc),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5522,f5338])).
% 18.44/2.80 fof(f5590,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(sF2_fnc),X2))),divide(X1,X0))=multiply(sF2_fnc,multiply(b2,X2)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5522,f5318])).
% 18.44/2.80 fof(f5591,plain,(
% 18.44/2.80 ![X0]: (multiply(sF2_fnc,multiply(b2,X0))=divide(divide(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5522,f5159])).
% 18.44/2.80 fof(f5666,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(divide(X0,X1),sF2_fnc)),divide(X1,X0))=inverse(multiply(b2,sF2_fnc)))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5582,f15])).
% 18.44/2.80 fof(f5669,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=inverse(multiply(b2,sF2_fnc))),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4672,f5666])).
% 18.44/2.80 fof(f5735,plain,(
% 18.44/2.80 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5669,f5])).
% 18.44/2.80 fof(f5743,plain,(
% 18.44/2.80 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=X0)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4296,f5735])).
% 18.44/2.80 fof(f5745,plain,(
% 18.44/2.80 sF1_fnc=divide(sF1_fnc,multiply(b2,sF2_fnc))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f4781,f5743])).
% 18.44/2.80 fof(f5762,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(inverse(sF1_fnc),divide(divide(inverse(X0),X1),sF1_fnc)),multiply(X1,X0))=multiply(b2,sF2_fnc))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5745,f23])).
% 18.44/2.80 fof(f5776,plain,(
% 18.44/2.80 ![X0]: (multiply(X0,divide(sF1_fnc,sF1_fnc))=X0)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5780,f5743])).
% 18.44/2.80 fof(f5780,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=multiply(b2,sF2_fnc)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4656,f5762])).
% 18.44/2.80 fof(f5806,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(inverse(divide(divide(X0,X1),X2)),divide(divide(divide(X1,X0),sF1_fnc),sF1_fnc))=X2)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f5776,f5078])).
% 18.44/2.80 fof(f5832,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(inverse(divide(X0,X1)),divide(divide(sF1_fnc,sF1_fnc),X0)),divide(inverse(sF2_fnc),b2))=X1)),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5780,f20])).
% 18.44/2.80 fof(f5835,plain,(
% 18.44/2.80 ![X0]: (divide(X0,divide(inverse(sF2_fnc),b2))=X0)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4634,f5832])).
% 18.44/2.80 fof(f5865,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(inverse(inverse(X0)),multiply(divide(X1,X2),X0)),divide(X2,X1))=divide(inverse(sF2_fnc),b2))),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5835,f17])).
% 18.44/2.80 fof(f5908,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=divide(inverse(sF2_fnc),b2)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4645,f5865])).
% 18.44/2.80 fof(f6014,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),multiply(divide(X0,X1),sF2_fnc)),divide(X1,X0))=b2)),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f5908,f17])).
% 18.44/2.80 fof(f6033,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(divide(sF1_fnc,sF1_fnc),multiply(divide(X0,X1),sF2_fnc)),divide(X1,X0))=b2)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4837,f6014])).
% 18.44/2.80 fof(f6034,plain,(
% 18.44/2.80 b2=divide(divide(sF1_fnc,sF1_fnc),sF2_fnc)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6035,f4807])).
% 18.44/2.80 fof(f6035,plain,(
% 18.44/2.80 ![X0,X1]: (divide(divide(inverse(sF2_fnc),divide(X0,X1)),divide(X1,X0))=b2)),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4877,f6033])).
% 18.44/2.80 fof(f6085,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,divide(divide(sF2_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),b2)=sF2_fnc),
% 18.44/2.80 inference(paramodulation,[status(thm)],[f6034,f4676])).
% 18.44/2.80 fof(f6103,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,divide(sF2_fnc,sF2_fnc)),b2)=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f4296,f6085])).
% 18.44/2.80 fof(f6104,plain,(
% 18.44/2.80 ![X0,X1,X2]: (divide(divide(sF2_fnc,divide(divide(X0,X1),multiply(inverse(sF2_fnc),X2))),divide(X1,X0))=multiply(sF1_fnc,multiply(sF1_fnc,X2)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6107,f4899])).
% 18.44/2.80 fof(f6105,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=divide(sF2_fnc,sF2_fnc)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6107,f4969])).
% 18.44/2.80 fof(f6107,plain,(
% 18.44/2.80 divide(divide(sF1_fnc,sF1_fnc),b2)=sF2_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f12,f6103])).
% 18.44/2.80 fof(f6125,plain,(
% 18.44/2.80 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=multiply(sF2_fnc,multiply(b2,X0)))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6104,f5590])).
% 18.44/2.80 fof(f6132,plain,(
% 18.44/2.80 ![X0]: (divide(X0,sF1_fnc)=X0)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6230,f4296])).
% 18.44/2.80 fof(f6163,plain,(
% 18.44/2.80 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=multiply(sF1_fnc,X0))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6230,f4888])).
% 18.44/2.80 fof(f6170,plain,(
% 18.44/2.80 ![X0,X1]: (divide(sF1_fnc,divide(X0,X1))=divide(X1,X0))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6230,f4879])).
% 18.44/2.80 fof(f6230,plain,(
% 18.44/2.80 divide(sF1_fnc,sF1_fnc)=sF1_fnc),
% 18.44/2.80 inference(forward_demodulation,[status(thm)],[f12,f6105])).
% 18.44/2.80 fof(f6254,plain,(
% 18.44/2.80 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=divide(divide(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6125,f5591])).
% 18.44/2.80 fof(f6272,plain,(
% 18.44/2.80 ![X0]: (inverse(divide(sF1_fnc,X0))=X0)),
% 18.44/2.80 inference(backward_demodulation,[status(thm)],[f6132,f3944])).
% 18.44/2.80 fof(f6344,plain,(
% 18.44/2.80 ![X0,X1]: (inverse(divide(X0,X1))=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 19.25/2.85 inference(backward_demodulation,[status(thm)],[f6132,f4044])).
% 19.25/2.85 fof(f6349,plain,(
% 19.25/2.85 ![X0,X1,X2]: (divide(inverse(divide(divide(X0,X1),X2)),divide(divide(X1,X0),sF1_fnc))=X2)),
% 19.25/2.85 inference(backward_demodulation,[status(thm)],[f6132,f5806])).
% 19.25/2.85 fof(f6507,plain,(
% 19.25/2.85 ![X0,X1,X2]: (divide(divide(multiply(sF1_fnc,X0),divide(X1,X2)),divide(X2,X1))=inverse(inverse(X0)))),
% 19.25/2.85 inference(backward_demodulation,[status(thm)],[f6170,f5187])).
% 19.25/2.85 fof(f6512,plain,(
% 19.25/2.85 ![X0,X1]: (divide(divide(sF0_fnc,divide(X0,X1)),divide(X1,X0))=inverse(inverse(a2)))),
% 19.25/2.85 inference(backward_demodulation,[status(thm)],[f6170,f4694])).
% 19.25/2.85 fof(f6684,plain,(
% 19.25/2.85 ![X0]: (multiply(sF1_fnc,X0)=divide(divide(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6163,f6254])).
% 19.25/2.85 fof(f6685,plain,(
% 19.25/2.85 ![X0]: (multiply(sF1_fnc,X0)=divide(sF1_fnc,divide(sF1_fnc,X0)))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6132,f6684])).
% 19.25/2.85 fof(f6686,plain,(
% 19.25/2.85 ![X0]: (multiply(sF1_fnc,X0)=divide(X0,sF1_fnc))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6170,f6685])).
% 19.25/2.85 fof(f6719,plain,(
% 19.25/2.85 ![X0]: (multiply(sF1_fnc,X0)=X0)),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6132,f6686])).
% 19.25/2.85 fof(f7104,plain,(
% 19.25/2.85 ![X0,X1]: (inverse(divide(X0,X1))=divide(X1,X0))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6272,f6344])).
% 19.25/2.85 fof(f7109,plain,(
% 19.25/2.85 ![X0,X1,X2]: (divide(divide(X0,divide(X1,X2)),divide(divide(X2,X1),sF1_fnc))=X0)),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f7104,f6349])).
% 19.25/2.85 fof(f7113,plain,(
% 19.25/2.85 ![X0,X1,X2]: (divide(divide(X0,divide(X1,X2)),divide(X2,X1))=X0)),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6132,f7109])).
% 19.25/2.85 fof(f7392,plain,(
% 19.25/2.85 ![X0]: (inverse(divide(inverse(X0),sF1_fnc))=inverse(inverse(X0)))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f5005,f6507])).
% 19.25/2.85 fof(f7393,plain,(
% 19.25/2.85 ![X0]: (divide(sF1_fnc,inverse(X0))=inverse(inverse(X0)))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f7104,f7392])).
% 19.25/2.85 fof(f7394,plain,(
% 19.25/2.85 ![X0]: (multiply(sF1_fnc,X0)=inverse(inverse(X0)))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f5,f7393])).
% 19.25/2.85 fof(f7414,plain,(
% 19.25/2.85 ![X0]: (X0=inverse(inverse(X0)))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f6719,f7394])).
% 19.25/2.85 fof(f7466,plain,(
% 19.25/2.85 sF0_fnc=inverse(inverse(a2))),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f7113,f6512])).
% 19.25/2.85 fof(f7467,plain,(
% 19.25/2.85 sF0_fnc=a2),
% 19.25/2.85 inference(forward_demodulation,[status(thm)],[f7414,f7466])).
% 19.25/2.85 fof(f7468,plain,(
% 19.25/2.85 $false),
% 19.25/2.85 inference(forward_subsumption_resolution,[status(thm)],[f7467,f10])).
% 19.25/2.85 % SZS output end CNFRefutation for theBenchmark.p
% 19.25/2.88 % Elapsed time: 2.514627 seconds
% 19.25/2.88 % CPU time: 19.759533 seconds
% 19.25/2.88 % Total memory used: 388.646 MB
% 19.25/2.88 % Net memory used: 383.679 MB
%------------------------------------------------------------------------------