%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP470-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 : n008.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 15.84s 7.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP470-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.12/5.59 % Computer : n008.cluster.edu
% 0.12/5.59 % Model : x86_64 x86_64
% 0.12/5.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.59 % Memory : 8046.5625MB
% 0.12/5.59 % OS : Linux 6.8.0-71-generic
% 0.12/5.59 % CPULimit : 300
% 0.12/5.59 % WCLimit : 300
% 0.12/5.59 % DateTime : Sun Sep 20 20:15:17 UTC 2026
% 0.12/5.59 % CPUTime :
% 0.15/5.60 % Drodi V4.1.1
% 15.84/7.66 % Refutation found
% 15.84/7.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 15.84/7.66 % SZS output start CNFRefutation for theBenchmark
% 15.84/7.66 fof(f1,axiom,(
% 15.84/7.66 (![A,B,C,D]: (divide(inverse(divide(A,divide(B,divide(C,D)))),divide(divide(D,C),A)) = B ))),
% 15.84/7.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.84/7.66 fof(f2,axiom,(
% 15.84/7.66 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 15.84/7.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.84/7.66 fof(f3,negated_conjecture,(
% 15.84/7.66 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 15.84/7.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.84/7.66 fof(f4,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0))=X1)),
% 15.84/7.66 inference(cnf_transformation,[status(thm)],[f1])).
% 15.84/7.66 fof(f5,plain,(
% 15.84/7.66 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 15.84/7.66 inference(cnf_transformation,[status(thm)],[f2])).
% 15.84/7.66 fof(f6,plain,(
% 15.84/7.66 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 15.84/7.66 inference(cnf_transformation,[status(thm)],[f3])).
% 15.84/7.66 fof(f7,definition,(
% 15.84/7.66 sF2_fnc=inverse(b2)),
% 15.84/7.66 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 15.84/7.66 fof(f8,definition,(
% 15.84/7.66 sF1_fnc=multiply(sF2_fnc,b2)),
% 15.84/7.66 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 15.84/7.66 fof(f9,definition,(
% 15.84/7.66 sF0_fnc=multiply(sF1_fnc,a2)),
% 15.84/7.66 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 15.84/7.66 fof(f10,plain,(
% 15.84/7.66 ~sF0_fnc=a2),
% 15.84/7.66 inference(definition_folding,[],[f6,f9,f8,f7])).
% 15.84/7.66 fof(f11,plain,(
% 15.84/7.66 ![X0]: (multiply(X0,b2)=divide(X0,sF2_fnc))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f7,f5])).
% 15.84/7.66 fof(f12,plain,(
% 15.84/7.66 sF1_fnc=divide(sF2_fnc,sF2_fnc)),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f11,f8])).
% 15.84/7.66 fof(f13,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,divide(X3,X4))))))=divide(X4,X3))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f4,f4])).
% 15.84/7.66 fof(f14,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(X4,X3)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f4,f4])).
% 15.84/7.66 fof(f16,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(divide(sF2_fnc,sF2_fnc),X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f12,f4])).
% 15.84/7.66 fof(f17,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(X2,X3)))),divide(divide(inverse(X3),X2),X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f4])).
% 15.84/7.66 fof(f18,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f4])).
% 15.84/7.66 fof(f21,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(inverse(X2),X3)))),divide(multiply(X3,X2),X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f4])).
% 15.84/7.66 fof(f22,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f13])).
% 15.84/7.66 fof(f24,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(sF1_fnc,X0))=X1)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f12,f16])).
% 15.84/7.66 fof(f27,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),divide(sF1_fnc,inverse(divide(sF1_fnc,divide(X0,sF1_fnc)))))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f24])).
% 15.84/7.66 fof(f28,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(X0),divide(sF1_fnc,inverse(divide(sF1_fnc,divide(X0,divide(X1,X2))))))=divide(X2,X1))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f4,f24])).
% 15.84/7.66 fof(f29,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(sF1_fnc,X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f24])).
% 15.84/7.66 fof(f30,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF1_fnc)))))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f4])).
% 15.84/7.66 fof(f31,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(divide(X2,sF1_fnc),X0))=inverse(divide(X2,divide(X1,sF1_fnc))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f4])).
% 15.84/7.66 fof(f34,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,sF1_fnc))))=sF1_fnc)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f27])).
% 15.84/7.66 fof(f35,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,divide(X1,X2)))))=divide(X2,X1))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f28])).
% 15.84/7.66 fof(f36,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF1_fnc))))=sF1_fnc)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f30])).
% 15.84/7.66 fof(f39,plain,(
% 15.84/7.66 divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))))=sF1_fnc),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f7,f34])).
% 15.84/7.66 fof(f49,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(divide(inverse(a2),divide(X0,sF1_fnc))),sF0_fnc)=X0)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f9,f29])).
% 15.84/7.66 fof(f70,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f22])).
% 15.84/7.66 fof(f80,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(divide(X2,X3),divide(divide(X3,X2),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f22])).
% 15.84/7.66 fof(f81,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(inverse(divide(X0,divide(X1,divide(X2,X3))))),multiply(divide(X4,X5),divide(divide(X5,X4),X1)))=divide(X0,divide(X3,X2)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f4,f22])).
% 15.84/7.66 fof(f82,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3))))=divide(sF0_fnc,inverse(divide(inverse(a2),divide(X3,sF1_fnc)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f49,f22])).
% 15.84/7.66 fof(f84,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3))))=divide(divide(sF1_fnc,X4),inverse(divide(X4,divide(X3,sF1_fnc)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f22])).
% 15.84/7.66 fof(f88,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF1_fnc))))=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))),sF2_fnc))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f39,f22])).
% 15.84/7.66 fof(f90,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,multiply(X3,X4)))))=divide(inverse(X4),X3))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f22])).
% 15.84/7.66 fof(f107,plain,(
% 15.84/7.66 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(divide(X0,X1),sF1_fnc)))=divide(X1,X0))),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f109,f22])).
% 15.84/7.66 fof(f108,plain,(
% 15.84/7.66 multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=sF1_fnc),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f109,f36])).
% 15.84/7.66 fof(f109,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3))))=multiply(sF0_fnc,divide(inverse(a2),divide(X3,sF1_fnc))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f82])).
% 15.84/7.66 fof(f116,plain,(
% 15.84/7.66 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=divide(divide(sF1_fnc,X1),inverse(divide(X1,divide(X0,sF1_fnc)))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f109,f84])).
% 15.84/7.66 fof(f121,plain,(
% 15.84/7.66 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f116])).
% 15.84/7.66 fof(f142,plain,(
% 15.84/7.66 sF1_fnc=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))),sF2_fnc)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f36,f88])).
% 15.84/7.66 fof(f144,plain,(
% 15.84/7.66 ![X0,X1]: (multiply(sF0_fnc,divide(inverse(a2),divide(multiply(X0,X1),sF1_fnc)))=divide(inverse(X1),X0))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f109,f90])).
% 15.84/7.66 fof(f178,plain,(
% 15.84/7.66 multiply(sF0_fnc,divide(inverse(a2),divide(sF0_fnc,sF1_fnc)))=divide(inverse(a2),sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f9,f144])).
% 15.84/7.66 fof(f190,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (X0=inverse(divide(X1,divide(divide(X0,divide(divide(X2,X3),X1)),divide(X3,X2)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f4,f14])).
% 15.84/7.66 fof(f200,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(multiply(X0,X1)),divide(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(inverse(X1),divide(X4,X3)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f14])).
% 15.84/7.66 fof(f201,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(X4,X3)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f14])).
% 15.84/7.66 fof(f206,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,divide(sF0_fnc,inverse(divide(inverse(a2),divide(X3,sF1_fnc))))))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f49,f14])).
% 15.84/7.66 fof(f214,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,multiply(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(inverse(X4),X3)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f14])).
% 15.84/7.66 fof(f233,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,multiply(sF0_fnc,divide(inverse(a2),divide(X3,sF1_fnc)))))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f206])).
% 15.84/7.66 fof(f257,plain,(
% 15.84/7.66 ![X0,X1]: (X0=inverse(divide(X1,divide(divide(X0,divide(sF1_fnc,X1)),divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))))))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f142,f190])).
% 15.84/7.66 fof(f282,plain,(
% 15.84/7.66 ![X0,X1]: (X0=inverse(divide(X1,divide(divide(X0,divide(sF1_fnc,X1)),sF1_fnc))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f39,f257])).
% 15.84/7.66 fof(f310,plain,(
% 15.84/7.66 ![X0,X1]: (X0=inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(sF1_fnc,X1)),sF1_fnc))))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f14,f282])).
% 15.84/7.66 fof(f312,plain,(
% 15.84/7.66 ![X0,X1]: (X0=inverse(divide(inverse(X1),divide(divide(X0,multiply(sF1_fnc,X1)),sF1_fnc))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f282])).
% 15.84/7.66 fof(f329,plain,(
% 15.84/7.66 ![X0]: (X0=inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f9,f312])).
% 15.84/7.66 fof(f353,plain,(
% 15.84/7.66 ![X0]: (divide(X0,multiply(sF1_fnc,divide(sF1_fnc,divide(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)),sF1_fnc))))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f329,f34])).
% 15.84/7.66 fof(f370,plain,(
% 15.84/7.66 ![X0]: (inverse(divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc)))=inverse(inverse(X0)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f310])).
% 15.84/7.66 fof(f375,plain,(
% 15.84/7.66 ![X0,X1]: (X0=inverse(inverse(divide(X0,divide(inverse(X1),divide(inverse(multiply(sF1_fnc,X1)),sF1_fnc))))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f310])).
% 15.84/7.66 fof(f509,plain,(
% 15.84/7.66 ![X0,X1,X2,X3]: (divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,divide(X1,X2)))))=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X3,divide(X2,X1)))),inverse(X3)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f35,f35])).
% 15.84/7.66 fof(f540,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(X0,X1)=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X2,divide(X0,X1)))),inverse(X2)))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f35,f509])).
% 15.84/7.66 fof(f541,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X2,divide(X0,X1)))),X2))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f540])).
% 15.84/7.66 fof(f570,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(inverse(a2),divide(X0,sF1_fnc))),sF0_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),X1))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f49,f541])).
% 15.84/7.66 fof(f588,plain,(
% 15.84/7.66 ![X0,X1]: (X0=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),X1))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f49,f570])).
% 15.84/7.66 fof(f602,plain,(
% 15.84/7.66 ![X0]: (X0=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X0))),sF2_fnc))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f11,f588])).
% 15.84/7.66 fof(f611,plain,(
% 15.84/7.66 multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc)))=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f39,f588])).
% 15.84/7.66 fof(f612,plain,(
% 15.84/7.66 sF2_fnc=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f12,f588])).
% 15.84/7.66 fof(f613,plain,(
% 15.84/7.66 ![X0,X1]: (inverse(X0)=multiply(multiply(sF1_fnc,divide(sF1_fnc,multiply(X1,X0))),X1))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f588])).
% 15.84/7.66 fof(f630,plain,(
% 15.84/7.66 multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc)))=sF2_fnc),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f612,f611])).
% 15.84/7.66 fof(f660,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,sF1_fnc),X0))=inverse(divide(X2,divide(X1,sF1_fnc))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f24,f18])).
% 15.84/7.66 fof(f751,plain,(
% 15.84/7.66 ![X0]: (inverse(X0)=divide(multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0))),sF2_fnc))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f5,f602])).
% 15.84/7.66 fof(f759,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X0)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f602,f107])).
% 15.84/7.66 fof(f773,plain,(
% 15.84/7.66 ![X0,X1]: (inverse(X0)=multiply(multiply(sF1_fnc,divide(sF1_fnc,inverse(X1))),multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f613,f613])).
% 15.84/7.66 fof(f774,plain,(
% 15.84/7.66 inverse(sF2_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc)),multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f612,f613])).
% 15.84/7.66 fof(f781,plain,(
% 15.84/7.66 inverse(a2)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)),sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f9,f613])).
% 15.84/7.66 fof(f790,plain,(
% 15.84/7.66 ![X0,X1]: (inverse(X0)=multiply(multiply(sF1_fnc,multiply(sF1_fnc,X1)),multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f773])).
% 15.84/7.66 fof(f800,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,inverse(a2)))),divide(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),X0))=X1)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f781,f17])).
% 15.84/7.66 fof(f801,plain,(
% 15.84/7.66 multiply(sF0_fnc,divide(inverse(a2),divide(inverse(a2),sF1_fnc)))=divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f781,f144])).
% 15.84/7.66 fof(f804,plain,(
% 15.84/7.66 ![X0]: (inverse(divide(inverse(sF1_fnc),divide(divide(X0,inverse(a2)),divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc))))=X0)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f214,f800])).
% 15.84/7.66 fof(f805,plain,(
% 15.84/7.66 ![X0]: (inverse(divide(inverse(sF1_fnc),divide(multiply(X0,a2),divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc))))=X0)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f804])).
% 15.84/7.66 fof(f816,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(inverse(X0),sF1_fnc)))=divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f751,f107])).
% 15.84/7.66 fof(f827,plain,(
% 15.84/7.66 divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,a2))))=divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f816,f801])).
% 15.84/7.66 fof(f1014,plain,(
% 15.84/7.66 ![X0]: (X0=inverse(inverse(divide(X0,divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f9,f375])).
% 15.84/7.66 fof(f1481,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(inverse(X0)),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)))=X0)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f370,f24])).
% 15.84/7.66 fof(f1504,plain,(
% 15.84/7.66 ![X0]: (divide(X0,divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)))=divide(X0,divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1014,f1481])).
% 15.84/7.66 fof(f1510,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(inverse(inverse(X0))),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)))=divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f370,f1481])).
% 15.84/7.66 fof(f1511,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)))=divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f329,f1481])).
% 15.84/7.66 fof(f1519,plain,(
% 15.84/7.66 divide(inverse(sF2_fnc),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)))=b2),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f7,f1481])).
% 15.84/7.66 fof(f1520,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),multiply(divide(sF1_fnc,inverse(divide(sF1_fnc,sF1_fnc))),inverse(X0)))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1481,f18])).
% 15.84/7.66 fof(f1531,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(inverse(X2)),divide(X1,divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),sF1_fnc)))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1481,f14])).
% 15.84/7.66 fof(f1536,plain,(
% 15.84/7.66 ![X0]: (divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))=multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),inverse(inverse(X0))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1481,f588])).
% 15.84/7.66 fof(f1541,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=divide(divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)),inverse(inverse(X0))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1481,f107])).
% 15.84/7.66 fof(f1544,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(inverse(X0)),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc)))=X0)),
% 15.84/7.66 inference(backward_demodulation,[status(thm)],[f1504,f1481])).
% 15.84/7.66 fof(f1563,plain,(
% 15.84/7.66 ![X0]: (inverse(X0)=divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc)))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1481,f1510])).
% 15.84/7.66 fof(f1565,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc)))=divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1504,f1511])).
% 15.84/7.66 fof(f1604,plain,(
% 15.84/7.66 divide(inverse(sF2_fnc),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc)))=b2),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1504,f1519])).
% 15.84/7.66 fof(f1605,plain,(
% 15.84/7.66 divide(inverse(a2),divide(divide(sF2_fnc,sF0_fnc),sF1_fnc))=b2),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1565,f1604])).
% 15.84/7.66 fof(f1606,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(X0),multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)))=sF1_fnc)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f1520])).
% 15.84/7.66 fof(f1627,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=multiply(divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)),inverse(X0)))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f1541])).
% 15.84/7.66 fof(f1632,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(a2),divide(divide(inverse(X0),sF0_fnc),sF1_fnc))=X0)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1565,f1544])).
% 15.84/7.66 fof(f1696,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(sF1_fnc,divide(inverse(X1),sF0_fnc)),X0))=inverse(a2))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1632,f18])).
% 15.84/7.66 fof(f1709,plain,(
% 15.84/7.66 ![X0]: (inverse(divide(sF1_fnc,divide(X0,divide(sF0_fnc,inverse(X0)))))=inverse(a2))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f201,f1696])).
% 15.84/7.66 fof(f1710,plain,(
% 15.84/7.66 ![X0]: (inverse(divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0))))=inverse(a2))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f1709])).
% 15.84/7.66 fof(f1738,plain,(
% 15.84/7.66 ![X0]: (divide(inverse(a2),divide(divide(inverse(a2),sF0_fnc),sF1_fnc))=divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0))))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1710,f1632])).
% 15.84/7.66 fof(f1750,plain,(
% 15.84/7.66 ![X0]: (a2=divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0))))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f1632,f1738])).
% 15.84/7.66 fof(f1916,plain,(
% 15.84/7.66 a2=divide(sF1_fnc,divide(b2,divide(sF0_fnc,sF2_fnc)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f11,f1750])).
% 15.84/7.66 fof(f1920,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(divide(X0,a2)),divide(multiply(multiply(sF0_fnc,inverse(X1)),X1),X0))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1750,f21])).
% 15.84/7.66 fof(f1987,plain,(
% 15.84/7.66 ![X0]: (divide(X0,multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)))))=sF1_fnc)),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f329,f1606])).
% 15.84/7.66 fof(f2000,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),inverse(X0)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1606,f107])).
% 15.84/7.66 fof(f2004,plain,(
% 15.84/7.66 ![X0]: (divide(X0,multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0))=sF1_fnc)),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f329,f1987])).
% 15.84/7.66 fof(f2019,plain,(
% 15.84/7.66 ![X0]: (sF1_fnc=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),inverse(X0)))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f108,f2000])).
% 15.84/7.66 fof(f2023,plain,(
% 15.84/7.66 ![X0]: (sF1_fnc=multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),X0))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f5,f2019])).
% 15.84/7.66 fof(f2049,plain,(
% 15.84/7.66 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0),X0))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f2004,f107])).
% 15.84/7.66 fof(f2064,plain,(
% 15.84/7.66 ![X0]: (sF1_fnc=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0),X0))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f108,f2049])).
% 15.84/7.66 fof(f2119,plain,(
% 15.84/7.66 ![X0,X1]: (divide(inverse(sF1_fnc),multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),a2)))=divide(divide(sF0_fnc,sF2_fnc),b2))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1916,f70])).
% 15.84/7.66 fof(f2120,plain,(
% 15.84/7.66 ![X0,X1,X2]: (divide(inverse(sF1_fnc),multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),a2)))=divide(multiply(sF0_fnc,X2),X2))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f1750,f70])).
% 15.84/7.66 fof(f2156,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),divide(X2,divide(X3,X4))))=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X4,X3))),inverse(X2)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f70,f588])).
% 15.84/7.66 fof(f2159,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (multiply(sF0_fnc,divide(inverse(a2),divide(divide(X0,X1),sF1_fnc)))=divide(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X1,X0)))),inverse(X4)))),
% 15.84/7.66 inference(paramodulation,[status(thm)],[f70,f107])).
% 15.84/7.66 fof(f2197,plain,(
% 15.84/7.66 ![X0]: (divide(divide(sF0_fnc,sF2_fnc),b2)=divide(multiply(sF0_fnc,X0),X0))),
% 15.84/7.66 inference(forward_demodulation,[status(thm)],[f2119,f2120])).
% 15.84/7.66 fof(f2258,plain,(
% 15.84/7.66 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=divide(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X0,X1)))),inverse(X4)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f107,f2159])).
% 15.84/7.67 fof(f2259,plain,(
% 15.84/7.67 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X0,X1)))),X4))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f2258])).
% 15.84/7.67 fof(f2260,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),inverse(X2)),X2))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2156,f2259])).
% 15.84/7.67 fof(f2271,plain,(
% 15.84/7.67 sF1_fnc=divide(divide(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc),b2)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f11,f2064])).
% 15.84/7.67 fof(f2278,plain,(
% 15.84/7.67 divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2064,f49])).
% 15.84/7.67 fof(f2295,plain,(
% 15.84/7.67 ![X0]: (X0=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2064,f588])).
% 15.84/7.67 fof(f2319,plain,(
% 15.84/7.67 b2=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2271,f588])).
% 15.84/7.67 fof(f2352,plain,(
% 15.84/7.67 ![X0]: (divide(divide(sF0_fnc,sF2_fnc),b2)=multiply(multiply(sF0_fnc,inverse(X0)),X0))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f5,f2197])).
% 15.84/7.67 fof(f2364,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(divide(X0,X1)),divide(divide(divide(sF0_fnc,sF2_fnc),b2),X0))=inverse(divide(multiply(sF0_fnc,sF1_fnc),divide(X1,sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2197,f31])).
% 15.84/7.67 fof(f2385,plain,(
% 15.84/7.67 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(divide(divide(sF0_fnc,sF2_fnc),b2),sF1_fnc)))=divide(X0,multiply(sF0_fnc,X0)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2197,f107])).
% 15.84/7.67 fof(f2388,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(X0,a2)),divide(divide(divide(sF0_fnc,sF2_fnc),b2),X0))=sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f2352,f1920])).
% 15.84/7.67 fof(f2394,plain,(
% 15.84/7.67 ![X0]: (divide(b2,divide(sF0_fnc,sF2_fnc))=divide(X0,multiply(sF0_fnc,X0)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f107,f2385])).
% 15.84/7.67 fof(f2397,plain,(
% 15.84/7.67 inverse(divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)))=sF1_fnc),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2364,f2388])).
% 15.84/7.67 fof(f2401,plain,(
% 15.84/7.67 sF1_fnc=multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2397,f2023])).
% 15.84/7.67 fof(f2402,plain,(
% 15.84/7.67 divide(inverse(a2),divide(divide(sF1_fnc,sF0_fnc),sF1_fnc))=divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2397,f1632])).
% 15.84/7.67 fof(f2407,plain,(
% 15.84/7.67 ![X0]: (multiply(X0,divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)))=divide(X0,sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2397,f5])).
% 15.84/7.67 fof(f2408,plain,(
% 15.84/7.67 sF1_fnc=multiply(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2278,f2401])).
% 15.84/7.67 fof(f2410,plain,(
% 15.84/7.67 sF1_fnc=divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f2407,f2408])).
% 15.84/7.67 fof(f2647,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)))=inverse(divide(X0,divide(sF1_fnc,sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2410,f31])).
% 15.84/7.67 fof(f2653,plain,(
% 15.84/7.67 multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2410,f107])).
% 15.84/7.67 fof(f2662,plain,(
% 15.84/7.67 sF1_fnc=divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f108,f2653])).
% 15.84/7.67 fof(f2672,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc))=inverse(divide(X0,divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2662,f31])).
% 15.84/7.67 fof(f2684,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc))=inverse(divide(X0,sF1_fnc)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2410,f2672])).
% 15.84/7.67 fof(f2698,plain,(
% 15.84/7.67 ![X0,X1]: (divide(X0,multiply(sF0_fnc,X0))=divide(X1,multiply(sF0_fnc,X1)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2394,f2394])).
% 15.84/7.67 fof(f2936,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),a2)))=divide(multiply(sF0_fnc,sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2397,f80])).
% 15.84/7.67 fof(f2939,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(sF1_fnc)),multiply(divide(X0,X1),divide(divide(X1,X0),X2)))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(X2,sF1_fnc)),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2064,f80])).
% 15.84/7.67 fof(f2943,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(X0)),multiply(divide(X1,X2),divide(divide(X2,X1),sF1_fnc)))=divide(inverse(divide(sF1_fnc,divide(X0,sF1_fnc))),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f24,f80])).
% 15.84/7.67 fof(f2962,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X2)))),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f602,f80])).
% 15.84/7.67 fof(f3031,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),a2)))=divide(divide(sF0_fnc,sF2_fnc),b2))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2197,f2936])).
% 15.84/7.67 fof(f3049,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(sF0_fnc,divide(inverse(a2),divide(X2,sF1_fnc))),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f759,f2962])).
% 15.84/7.67 fof(f3163,plain,(
% 15.84/7.67 ![X0]: (divide(X0,multiply(sF0_fnc,X0))=divide(divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)),divide(sF0_fnc,sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2407,f2698])).
% 15.84/7.67 fof(f3166,plain,(
% 15.84/7.67 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,sF1_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2407,f2197])).
% 15.84/7.67 fof(f3188,plain,(
% 15.84/7.67 divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc))=inverse(divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2410,f2684])).
% 15.84/7.67 fof(f3204,plain,(
% 15.84/7.67 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,inverse(divide(X0,sF1_fnc)))),inverse(sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f2684,f588])).
% 15.84/7.67 fof(f3210,plain,(
% 15.84/7.67 divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc))=inverse(sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2410,f3188])).
% 15.84/7.67 fof(f3228,plain,(
% 15.84/7.67 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,multiply(sF1_fnc,divide(X0,sF1_fnc))),inverse(sF1_fnc)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3204])).
% 15.84/7.67 fof(f3237,plain,(
% 15.84/7.67 divide(inverse(inverse(sF1_fnc)),multiply(sF1_fnc,sF1_fnc))=sF1_fnc),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3210,f29])).
% 15.84/7.67 fof(f3242,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(inverse(X0),inverse(sF1_fnc))),multiply(divide(sF1_fnc,sF1_fnc),X0))=inverse(sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3210,f18])).
% 15.84/7.67 fof(f3253,plain,(
% 15.84/7.67 multiply(sF0_fnc,divide(inverse(a2),divide(inverse(sF1_fnc),sF1_fnc)))=divide(divide(sF1_fnc,sF1_fnc),inverse(sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3210,f107])).
% 15.84/7.67 fof(f3260,plain,(
% 15.84/7.67 inverse(divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)))=inverse(sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f660,f3242])).
% 15.84/7.67 fof(f3272,plain,(
% 15.84/7.67 divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,sF1_fnc))))=divide(divide(sF1_fnc,sF1_fnc),inverse(sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f816,f3253])).
% 15.84/7.67 fof(f3276,plain,(
% 15.84/7.67 divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,sF1_fnc))))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3272])).
% 15.84/7.67 fof(f3288,plain,(
% 15.84/7.67 multiply(sF1_fnc,sF1_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(inverse(sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3237,f588])).
% 15.84/7.67 fof(f3291,plain,(
% 15.84/7.67 multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))=divide(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3237,f107])).
% 15.84/7.67 fof(f3300,plain,(
% 15.84/7.67 ![X0]: (multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc)))=multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0)))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3304,f1627])).
% 15.84/7.67 fof(f3304,plain,(
% 15.84/7.67 multiply(sF1_fnc,sF1_fnc)=divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f1536,f3288])).
% 15.84/7.67 fof(f3310,plain,(
% 15.84/7.67 sF1_fnc=divide(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f108,f3291])).
% 15.84/7.67 fof(f3316,plain,(
% 15.84/7.67 sF1_fnc=multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3310])).
% 15.84/7.67 fof(f3321,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF0_fnc))=divide(inverse(a2),sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f178])).
% 15.84/7.67 fof(f3322,plain,(
% 15.84/7.67 ![X0,X1]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(multiply(X0,X1)))=divide(inverse(X1),X0))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f144])).
% 15.84/7.67 fof(f3323,plain,(
% 15.84/7.67 ![X0,X1]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(divide(X0,X1)))=divide(X1,X0))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f107])).
% 15.84/7.67 fof(f3329,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(X0)))=divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0)))))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f816])).
% 15.84/7.67 fof(f3331,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(multiply(sF1_fnc,sF1_fnc),inverse(X2)),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f3049])).
% 15.84/7.67 fof(f3348,plain,(
% 15.84/7.67 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,multiply(multiply(sF1_fnc,sF1_fnc),inverse(X3))))))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f233])).
% 15.84/7.67 fof(f3350,plain,(
% 15.84/7.67 ![X0,X1]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0))=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3300,f121])).
% 15.84/7.67 fof(f3388,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc)))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3329,f3276])).
% 15.84/7.67 fof(f3392,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(a2)))=divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3329,f827])).
% 15.84/7.67 fof(f3455,plain,(
% 15.84/7.67 ![X0,X1]: (inverse(inverse(divide(X0,X1)))=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),multiply(sF1_fnc,sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3323,f613])).
% 15.84/7.67 fof(f3496,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc))=divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3260,f3323])).
% 15.84/7.67 fof(f3501,plain,(
% 15.84/7.67 divide(inverse(a2),divide(divide(inverse(sF1_fnc),sF0_fnc),sF1_fnc))=divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3260,f1632])).
% 15.84/7.67 fof(f3508,plain,(
% 15.84/7.67 sF1_fnc=divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3316,f3496])).
% 15.84/7.67 fof(f3513,plain,(
% 15.84/7.67 sF1_fnc=divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f1632,f3501])).
% 15.84/7.67 fof(f3532,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc),X0))=X1)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3513,f18])).
% 15.84/7.67 fof(f3533,plain,(
% 15.84/7.67 divide(inverse(sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3513,f588])).
% 15.84/7.67 fof(f3549,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc)))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f660,f3532])).
% 15.84/7.67 fof(f3550,plain,(
% 15.84/7.67 divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)=divide(inverse(sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3533,f2278])).
% 15.84/7.67 fof(f3560,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)))=inverse(divide(X0,divide(sF1_fnc,sF1_fnc))))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3550,f2647])).
% 15.84/7.67 fof(f3566,plain,(
% 15.84/7.67 divide(inverse(sF1_fnc),sF1_fnc)=inverse(divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3508,f2684])).
% 15.84/7.67 fof(f3567,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=inverse(divide(inverse(sF1_fnc),divide(X0,sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3508,f31])).
% 15.84/7.67 fof(f3581,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),X0))=X1)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3508,f18])).
% 15.84/7.67 fof(f3597,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,inverse(sF1_fnc)))))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f201,f3581])).
% 15.84/7.67 fof(f3599,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),multiply(sF1_fnc,sF1_fnc))))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3597])).
% 15.84/7.67 fof(f3604,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))=divide(sF1_fnc,inverse(sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3566,f3323])).
% 15.84/7.67 fof(f3607,plain,(
% 15.84/7.67 divide(divide(sF0_fnc,sF2_fnc),b2)=multiply(multiply(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3566,f2352])).
% 15.84/7.67 fof(f3614,plain,(
% 15.84/7.67 ![X0]: (multiply(X0,divide(inverse(sF1_fnc),sF1_fnc))=divide(X0,divide(inverse(sF1_fnc),sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3566,f5])).
% 15.84/7.67 fof(f3615,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))=multiply(sF1_fnc,sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3604])).
% 15.84/7.67 fof(f3620,plain,(
% 15.84/7.67 divide(divide(sF0_fnc,sF2_fnc),b2)=multiply(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3614,f3607])).
% 15.84/7.67 fof(f3621,plain,(
% 15.84/7.67 divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))=multiply(sF1_fnc,sF1_fnc)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f3614,f3615])).
% 15.84/7.67 fof(f3627,plain,(
% 15.84/7.67 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3614,f3620])).
% 15.84/7.67 fof(f3639,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),X0)=divide(divide(divide(X0,sF1_fnc),multiply(sF1_fnc,sF1_fnc)),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3599,f3323])).
% 15.84/7.67 fof(f3679,plain,(
% 15.84/7.67 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,sF1_fnc))),multiply(divide(X1,X2),divide(divide(X2,X1),sF1_fnc)))=divide(X0,divide(sF1_fnc,inverse(sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3513,f81])).
% 15.84/7.67 fof(f3836,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),sF1_fnc))),sF1_fnc)=divide(X0,divide(sF1_fnc,inverse(sF1_fnc))))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f2943,f3679])).
% 15.84/7.67 fof(f3837,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),sF1_fnc))),sF1_fnc)=divide(X0,multiply(sF1_fnc,sF1_fnc)))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f3836])).
% 15.84/7.67 fof(f4054,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),inverse(divide(inverse(a2),sF1_fnc)))=divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f3321,f3322])).
% 15.84/7.67 fof(f4076,plain,(
% 15.84/7.67 divide(sF1_fnc,inverse(a2))=divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3323,f4054])).
% 15.84/7.67 fof(f4077,plain,(
% 15.84/7.67 multiply(sF1_fnc,a2)=divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f4076])).
% 15.84/7.67 fof(f4079,plain,(
% 15.84/7.67 sF0_fnc=divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f9,f4077])).
% 15.84/7.67 fof(f4095,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(divide(X0,sF0_fnc)),divide(divide(inverse(sF1_fnc),sF1_fnc),X0))=inverse(inverse(sF0_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4079,f17])).
% 15.84/7.67 fof(f4105,plain,(
% 15.84/7.67 inverse(divide(inverse(sF1_fnc),divide(sF0_fnc,sF1_fnc)))=inverse(inverse(sF0_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f31,f4095])).
% 15.84/7.67 fof(f4107,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(inverse(sF1_fnc),divide(multiply(X0,a2),inverse(inverse(sF0_fnc)))))=X0)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f4108,f805])).
% 15.84/7.67 fof(f4108,plain,(
% 15.84/7.67 divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc)=inverse(inverse(sF0_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3567,f4105])).
% 15.84/7.67 fof(f4119,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(inverse(sF1_fnc),multiply(multiply(X0,a2),inverse(sF0_fnc))))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f4107])).
% 15.84/7.67 fof(f4163,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(inverse(sF1_fnc),multiply(X0,inverse(sF0_fnc))))=multiply(sF1_fnc,divide(sF1_fnc,divide(a2,X0))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f588,f4119])).
% 15.84/7.67 fof(f4164,plain,(
% 15.84/7.67 inverse(divide(inverse(sF1_fnc),multiply(sF0_fnc,inverse(sF0_fnc))))=sF1_fnc),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f9,f4119])).
% 15.84/7.67 fof(f4165,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),X0)=divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),inverse(sF1_fnc)))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4119,f3323])).
% 15.84/7.67 fof(f4177,plain,(
% 15.84/7.67 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,divide(a2,multiply(X0,a2))))=X0)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f4163,f4119])).
% 15.84/7.67 fof(f4181,plain,(
% 15.84/7.67 multiply(sF1_fnc,divide(sF1_fnc,divide(a2,sF0_fnc)))=sF1_fnc),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f4163,f4164])).
% 15.84/7.67 fof(f4182,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),X0)=multiply(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc))),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f5,f4165])).
% 15.84/7.67 fof(f4202,plain,(
% 15.84/7.67 inverse(divide(sF1_fnc,divide(a2,sF0_fnc)))=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4181,f613])).
% 15.84/7.67 fof(f4203,plain,(
% 15.84/7.67 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(divide(inverse(divide(sF1_fnc,divide(a2,sF0_fnc))),sF1_fnc),X0))=X1)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4181,f17])).
% 15.84/7.67 fof(f4208,plain,(
% 15.84/7.67 inverse(divide(sF1_fnc,divide(a2,sF0_fnc)))=divide(inverse(sF1_fnc),sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3533,f4202])).
% 15.84/7.67 fof(f4209,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(inverse(divide(sF1_fnc,divide(a2,sF0_fnc))),divide(divide(X0,sF1_fnc),sF1_fnc)))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f31,f4203])).
% 15.84/7.67 fof(f4210,plain,(
% 15.84/7.67 ![X0]: (inverse(inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc))))=X0)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f31,f4209])).
% 15.84/7.67 fof(f4217,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))=inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4210,f1632])).
% 15.84/7.67 fof(f4522,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0))=divide(inverse(divide(sF1_fnc,divide(a2,multiply(X0,a2)))),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4177,f3322])).
% 15.84/7.67 fof(f4524,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(sF1_fnc,divide(a2,multiply(X0,a2))))=multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4177,f613])).
% 15.84/7.67 fof(f4531,plain,(
% 15.84/7.67 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f4524,f4522])).
% 15.84/7.67 fof(f4535,plain,(
% 15.84/7.67 multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))=divide(divide(a2,sF0_fnc),sF1_fnc)),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4208,f3323])).
% 15.84/7.67 fof(f4536,plain,(
% 15.84/7.67 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc))=inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc))))),
% 15.84/7.67 inference(paramodulation,[status(thm)],[f4208,f31])).
% 15.84/7.67 fof(f4546,plain,(
% 15.84/7.67 divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))=divide(divide(a2,sF0_fnc),sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3614,f4535])).
% 15.84/7.67 fof(f4547,plain,(
% 15.84/7.67 ![X0]: (divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))=inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))))),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f4550,f4217])).
% 15.84/7.67 fof(f4550,plain,(
% 15.84/7.67 multiply(sF1_fnc,sF1_fnc)=divide(divide(a2,sF0_fnc),sF1_fnc)),
% 15.84/7.67 inference(forward_demodulation,[status(thm)],[f3621,f4546])).
% 15.84/7.67 fof(f4551,plain,(
% 15.84/7.67 ![X0]: (inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)))=X0)),
% 15.84/7.67 inference(backward_demodulation,[status(thm)],[f4552,f3549])).
% 15.84/7.68 fof(f4552,plain,(
% 15.84/7.68 ![X0]: (divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc))=divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4217,f4536])).
% 15.84/7.68 fof(f4568,plain,(
% 15.84/7.68 ![X0]: (inverse(divide(inverse(X0),multiply(sF1_fnc,sF1_fnc)))=X0)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4547,f1632])).
% 15.84/7.68 fof(f4569,plain,(
% 15.84/7.68 inverse(divide(sF2_fnc,multiply(sF1_fnc,sF1_fnc)))=b2),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4547,f1605])).
% 15.84/7.68 fof(f4572,plain,(
% 15.84/7.68 inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))=divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4547,f2402])).
% 15.84/7.68 fof(f4593,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF1_fnc,divide(sF1_fnc,divide(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))),sF1_fnc))))=sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4547,f353])).
% 15.84/7.68 fof(f4595,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4547,f4551])).
% 15.84/7.68 fof(f4601,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,sF1_fnc),inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4572,f3166])).
% 15.84/7.68 fof(f4603,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF0_fnc,X0))=divide(inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),divide(sF0_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4572,f3163])).
% 15.84/7.68 fof(f4609,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=multiply(divide(sF0_fnc,sF1_fnc),divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f4601])).
% 15.84/7.68 fof(f4620,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,divide(sF2_fnc,multiply(sF1_fnc,sF1_fnc)))=divide(X0,b2))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4569,f5])).
% 15.84/7.68 fof(f4635,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(X0))=inverse(divide(inverse(sF1_fnc),divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f29,f4595])).
% 15.84/7.68 fof(f4643,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=inverse(inverse(X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4635,f3567])).
% 15.84/7.68 fof(f4658,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))=divide(X0,multiply(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4643,f3837])).
% 15.84/7.68 fof(f4673,plain,(
% 15.84/7.68 multiply(sF1_fnc,sF1_fnc)=divide(sF1_fnc,inverse(inverse(sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4643,f3304])).
% 15.84/7.68 fof(f4674,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(inverse(X2)),divide(X1,divide(inverse(inverse(sF1_fnc)),sF1_fnc)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4643,f1531])).
% 15.84/7.68 fof(f4675,plain,(
% 15.84/7.68 ![X0]: (inverse(X0)=divide(inverse(inverse(sF1_fnc)),divide(X0,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4643,f1563])).
% 15.84/7.68 fof(f4688,plain,(
% 15.84/7.68 multiply(sF1_fnc,sF1_fnc)=multiply(sF1_fnc,inverse(sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f4673])).
% 15.84/7.68 fof(f4694,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),inverse(multiply(sF1_fnc,sF1_fnc)))=divide(inverse(inverse(sF1_fnc)),sF1_fnc)),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4688,f3322])).
% 15.84/7.68 fof(f4696,plain,(
% 15.84/7.68 inverse(inverse(sF1_fnc))=multiply(multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),sF1_fnc)),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4688,f613])).
% 15.84/7.68 fof(f4703,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(inverse(X2)),divide(X1,divide(inverse(sF1_fnc),sF1_fnc)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4704,f4674])).
% 15.84/7.68 fof(f4704,plain,(
% 15.84/7.68 divide(inverse(sF1_fnc),sF1_fnc)=divide(inverse(inverse(sF1_fnc)),sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f3322,f4694])).
% 15.84/7.68 fof(f4707,plain,(
% 15.84/7.68 ![X0]: (inverse(X0)=divide(inverse(sF1_fnc),divide(X0,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4714,f4675])).
% 15.84/7.68 fof(f4710,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc))=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4714,f3388])).
% 15.84/7.68 fof(f4713,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),X2)))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(X2,sF1_fnc)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4714,f2939])).
% 15.84/7.68 fof(f4714,plain,(
% 15.84/7.68 inverse(inverse(sF1_fnc))=inverse(sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f613,f4696])).
% 15.84/7.68 fof(f4740,plain,(
% 15.84/7.68 sF1_fnc=multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f3316,f4710])).
% 15.84/7.68 fof(f4741,plain,(
% 15.84/7.68 divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(a2,sF1_fnc)),sF1_fnc)=divide(divide(sF0_fnc,sF2_fnc),b2)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4713,f3031])).
% 15.84/7.68 fof(f4751,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,inverse(sF1_fnc))=divide(X0,inverse(sF1_fnc)))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4714,f5])).
% 15.84/7.68 fof(f4754,plain,(
% 15.84/7.68 sF1_fnc=multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4768,f3316])).
% 15.84/7.68 fof(f4761,plain,(
% 15.84/7.68 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=multiply(multiply(sF1_fnc,multiply(sF1_fnc,divide(X0,sF1_fnc))),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4768,f3228])).
% 15.84/7.68 fof(f4768,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(X0,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f4751])).
% 15.84/7.68 fof(f4922,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc))=divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4754,f3322])).
% 15.84/7.68 fof(f4926,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)=divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4768,f4922])).
% 15.84/7.68 fof(f4927,plain,(
% 15.84/7.68 sF1_fnc=divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4754,f4926])).
% 15.84/7.68 fof(f4932,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc))=divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4740,f3322])).
% 15.84/7.68 fof(f4936,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)=divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4768,f4932])).
% 15.84/7.68 fof(f4937,plain,(
% 15.84/7.68 sF1_fnc=divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4754,f4936])).
% 15.84/7.68 fof(f4941,plain,(
% 15.84/7.68 sF1_fnc=divide(sF1_fnc,divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3513])).
% 15.84/7.68 fof(f4946,plain,(
% 15.84/7.68 sF1_fnc=divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f4927])).
% 15.84/7.68 fof(f4963,plain,(
% 15.84/7.68 ![X0]: (inverse(X0)=divide(sF1_fnc,divide(X0,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f4707])).
% 15.84/7.68 fof(f4964,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(inverse(X2)),divide(X1,divide(sF1_fnc,sF1_fnc)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f4703])).
% 15.84/7.68 fof(f4978,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3627])).
% 15.84/7.68 fof(f4979,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,divide(inverse(sF1_fnc),sF1_fnc))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3614])).
% 15.84/7.68 fof(f4985,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)))=inverse(divide(X0,divide(sF1_fnc,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3560])).
% 15.84/7.68 fof(f4988,plain,(
% 15.84/7.68 divide(sF1_fnc,sF1_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3533])).
% 15.84/7.68 fof(f4991,plain,(
% 15.84/7.68 multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(a2)))=divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5017,f3392])).
% 15.84/7.68 fof(f5017,plain,(
% 15.84/7.68 sF1_fnc=inverse(sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4707,f4937])).
% 15.84/7.68 fof(f5027,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF0_fnc,X0))=divide(inverse(sF1_fnc),divide(sF0_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4946,f4603])).
% 15.84/7.68 fof(f5029,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=multiply(divide(sF0_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4946,f4609])).
% 15.84/7.68 fof(f5033,plain,(
% 15.84/7.68 multiply(sF1_fnc,inverse(b2))=sF2_fnc),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4963,f630])).
% 15.84/7.68 fof(f5035,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF1_fnc,inverse(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))))))=sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f4963,f4593])).
% 15.84/7.68 fof(f5048,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5017,f4978])).
% 15.84/7.68 fof(f5052,plain,(
% 15.84/7.68 ![X0]: (sF1_fnc=multiply(multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),X0))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5098,f2023])).
% 15.84/7.68 fof(f5063,plain,(
% 15.84/7.68 divide(multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(a2,sF1_fnc)),sF1_fnc)=divide(divide(sF0_fnc,sF2_fnc),b2)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5098,f4741])).
% 15.84/7.68 fof(f5080,plain,(
% 15.84/7.68 b2=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5098,f2319])).
% 15.84/7.68 fof(f5083,plain,(
% 15.84/7.68 ![X0]: (X0=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5098,f2295])).
% 15.84/7.68 fof(f5097,plain,(
% 15.84/7.68 inverse(sF2_fnc)=multiply(multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc)),divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5098,f774])).
% 15.84/7.68 fof(f5098,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,divide(sF1_fnc,sF1_fnc))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5017,f4979])).
% 15.84/7.68 fof(f5100,plain,(
% 15.84/7.68 ![X0]: (divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)))=inverse(divide(X0,divide(sF1_fnc,sF1_fnc))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5017,f4985])).
% 15.84/7.68 fof(f5102,plain,(
% 15.84/7.68 divide(sF1_fnc,sF1_fnc)=multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5098,f4988])).
% 15.84/7.68 fof(f5108,plain,(
% 15.84/7.68 ![X0,X1]: (multiply(divide(sF1_fnc,sF1_fnc),inverse(divide(X0,X1)))=divide(X1,X0))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3323])).
% 15.84/7.68 fof(f5123,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f4658])).
% 15.84/7.68 fof(f5124,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,divide(sF2_fnc,divide(sF1_fnc,sF1_fnc)))=divide(X0,b2))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f4620])).
% 15.84/7.68 fof(f5144,plain,(
% 15.84/7.68 ![X0]: (inverse(divide(inverse(X0),divide(sF1_fnc,sF1_fnc)))=X0)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f4568])).
% 15.84/7.68 fof(f5148,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),inverse(X0))=divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f4531])).
% 15.84/7.68 fof(f5153,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),X0)=multiply(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f4182])).
% 15.84/7.68 fof(f5165,plain,(
% 15.84/7.68 ![X0]: (multiply(multiply(sF1_fnc,sF1_fnc),X0)=divide(divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3639])).
% 15.84/7.68 fof(f5168,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(divide(X0,X1)))=multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3455])).
% 15.84/7.68 fof(f5196,plain,(
% 15.84/7.68 ![X0,X1]: (multiply(divide(sF1_fnc,sF1_fnc),inverse(X0))=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3350])).
% 15.84/7.68 fof(f5198,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,multiply(divide(sF1_fnc,sF1_fnc),inverse(X3))))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3348])).
% 15.84/7.68 fof(f5214,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(divide(sF1_fnc,sF1_fnc),inverse(X2)),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5224,f3331])).
% 15.84/7.68 fof(f5224,plain,(
% 15.84/7.68 divide(sF1_fnc,sF1_fnc)=multiply(sF1_fnc,sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5102])).
% 15.84/7.68 fof(f5225,plain,(
% 15.84/7.68 multiply(divide(sF1_fnc,sF1_fnc),inverse(inverse(a2)))=divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5224,f4991])).
% 15.84/7.68 fof(f5275,plain,(
% 15.84/7.68 a2=divide(sF1_fnc,inverse(sF0_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5312,f1750])).
% 15.84/7.68 fof(f5312,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF0_fnc,X0))=inverse(sF0_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4707,f5027])).
% 15.84/7.68 fof(f5336,plain,(
% 15.84/7.68 multiply(sF1_fnc,sF2_fnc)=sF2_fnc),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7,f5033])).
% 15.84/7.68 fof(f5337,plain,(
% 15.84/7.68 ![X0]: (divide(X0,multiply(sF1_fnc,X0))=sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4595,f5035])).
% 15.84/7.68 fof(f5349,plain,(
% 15.84/7.68 ![X0]: (sF1_fnc=multiply(multiply(sF1_fnc,inverse(X0)),X0))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5052])).
% 15.84/7.68 fof(f5366,plain,(
% 15.84/7.68 divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc)=divide(divide(sF0_fnc,sF2_fnc),b2)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5063])).
% 15.84/7.68 fof(f5397,plain,(
% 15.84/7.68 b2=multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5098,f5080])).
% 15.84/7.68 fof(f5398,plain,(
% 15.84/7.68 b2=multiply(sF1_fnc,divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5397])).
% 15.84/7.68 fof(f5400,plain,(
% 15.84/7.68 b2=multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5398])).
% 15.84/7.68 fof(f5403,plain,(
% 15.84/7.68 ![X0]: (X0=multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5098,f5083])).
% 15.84/7.68 fof(f5404,plain,(
% 15.84/7.68 ![X0]: (X0=multiply(sF1_fnc,multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5403])).
% 15.84/7.68 fof(f5406,plain,(
% 15.84/7.68 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=multiply(divide(X0,sF1_fnc),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5412,f4761])).
% 15.84/7.68 fof(f5411,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(X0)=multiply(X1,multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5412,f790])).
% 15.84/7.68 fof(f5412,plain,(
% 15.84/7.68 ![X0]: (X0=multiply(sF1_fnc,multiply(sF1_fnc,X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5404])).
% 15.84/7.68 fof(f5427,plain,(
% 15.84/7.68 inverse(sF2_fnc)=multiply(b2,divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5400,f5097])).
% 15.84/7.68 fof(f5428,plain,(
% 15.84/7.68 inverse(sF2_fnc)=multiply(b2,sF1_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4941,f5427])).
% 15.84/7.68 fof(f5444,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),X0)=divide(divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5224,f5165])).
% 15.84/7.68 fof(f5445,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(divide(X0,X1)))=divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5098,f5168])).
% 15.84/7.68 fof(f5461,plain,(
% 15.84/7.68 a2=multiply(sF1_fnc,sF0_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f5275])).
% 15.84/7.68 fof(f5484,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF2_fnc),b2)=divide(divide(sF0_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5406,f5029])).
% 15.84/7.68 fof(f5518,plain,(
% 15.84/7.68 divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc)=divide(divide(sF0_fnc,sF1_fnc),sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5484,f5366])).
% 15.84/7.68 fof(f5523,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF1_fnc),sF1_fnc)=divide(divide(sF0_fnc,divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5484,f5048])).
% 15.84/7.68 fof(f5591,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,sF1_fnc)=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5017,f5])).
% 15.84/7.68 fof(f5597,plain,(
% 15.84/7.68 inverse(sF2_fnc)=divide(b2,sF1_fnc)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5591,f5428])).
% 15.84/7.68 fof(f5599,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),X0)=divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5591,f5153])).
% 15.84/7.68 fof(f5605,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),inverse(X0))=divide(divide(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5591,f5148])).
% 15.84/7.68 fof(f5662,plain,(
% 15.84/7.68 ![X0]: (inverse(multiply(sF1_fnc,X0))=multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5412,f613])).
% 15.84/7.68 fof(f5669,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),inverse(X0))=divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5670,f5605])).
% 15.84/7.68 fof(f5670,plain,(
% 15.84/7.68 ![X0]: (inverse(multiply(sF1_fnc,X0))=divide(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5591,f5662])).
% 15.84/7.68 fof(f5674,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(multiply(sF1_fnc,divide(X0,X1))),sF1_fnc)=divide(X1,X0))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5669,f5108])).
% 15.84/7.68 fof(f5684,plain,(
% 15.84/7.68 divide(inverse(multiply(sF1_fnc,inverse(a2))),sF1_fnc)=divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5669,f5225])).
% 15.84/7.68 fof(f5696,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(divide(inverse(multiply(sF1_fnc,X2)),sF1_fnc),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5669,f5214])).
% 15.84/7.68 fof(f5712,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,divide(inverse(multiply(sF1_fnc,X3)),sF1_fnc)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5669,f5198])).
% 15.84/7.68 fof(f5714,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5669,f5196])).
% 15.84/7.68 fof(f5752,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(divide(inverse(a2),divide(X0,X1))),sF0_fnc)=inverse(multiply(sF1_fnc,divide(X1,X0))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5674,f49])).
% 15.84/7.68 fof(f5783,plain,(
% 15.84/7.68 ![X0]: (inverse(multiply(sF1_fnc,divide(sF1_fnc,X0)))=X0)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f5752,f49])).
% 15.84/7.68 fof(f5827,plain,(
% 15.84/7.68 divide(inverse(multiply(sF1_fnc,inverse(sF2_fnc))),sF1_fnc)=divide(sF1_fnc,b2)),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5597,f5674])).
% 15.84/7.68 fof(f5854,plain,(
% 15.84/7.68 divide(a2,sF0_fnc)=sF1_fnc),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f9,f5337])).
% 15.84/7.68 fof(f6277,plain,(
% 15.84/7.68 ![X0,X1]: (multiply(X0,multiply(sF1_fnc,divide(sF1_fnc,X1)))=divide(X0,X1))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5783,f5])).
% 15.84/7.68 fof(f6286,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(X0)=divide(X1,multiply(X0,X1)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f6277,f5411])).
% 15.84/7.68 fof(f6295,plain,(
% 15.84/7.68 ![X0]: (inverse(multiply(sF1_fnc,inverse(X0)))=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5349,f6286])).
% 15.84/7.68 fof(f6320,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(multiply(sF1_fnc,inverse(X0))),sF1_fnc)=divide(multiply(X0,X1),X1))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6286,f5674])).
% 15.84/7.68 fof(f6322,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(inverse(X0)),divide(divide(X1,sF1_fnc),X2))=inverse(divide(X1,divide(multiply(X0,X2),sF1_fnc))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6286,f31])).
% 15.84/7.68 fof(f6326,plain,(
% 15.84/7.68 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,inverse(X3)),X0))=inverse(divide(X2,divide(X1,divide(multiply(X3,X4),X4)))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6286,f14])).
% 15.84/7.68 fof(f6330,plain,(
% 15.84/7.68 divide(divide(sF2_fnc,sF1_fnc),sF1_fnc)=divide(sF1_fnc,b2)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f6295,f5827])).
% 15.84/7.68 fof(f6331,plain,(
% 15.84/7.68 divide(divide(a2,sF1_fnc),sF1_fnc)=divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f6295,f5684])).
% 15.84/7.68 fof(f6387,plain,(
% 15.84/7.68 ![X0,X1]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(multiply(X0,X1),X1))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f6295,f6320])).
% 15.84/7.68 fof(f6402,plain,(
% 15.84/7.68 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0))=inverse(divide(X2,divide(X1,divide(multiply(X3,X4),X4)))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f6326])).
% 15.84/7.68 fof(f6403,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0))=inverse(divide(X2,divide(X1,divide(divide(X3,sF1_fnc),sF1_fnc)))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f6387,f6402])).
% 15.84/7.68 fof(f7076,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(divide(X0,sF1_fnc),divide(divide(X1,divide(X2,X3)),sF1_fnc))=inverse(divide(X1,divide(inverse(inverse(X0)),divide(X3,X2)))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6295,f200])).
% 15.84/7.68 fof(f7275,plain,(
% 15.84/7.68 ![X0]: (inverse(divide(X0,divide(sF1_fnc,sF1_fnc)))=divide(inverse(X0),divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5144,f5144])).
% 15.84/7.68 fof(f7280,plain,(
% 15.84/7.68 ![X0]: (inverse(divide(X0,divide(sF1_fnc,sF1_fnc)))=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5783,f5144])).
% 15.84/7.68 fof(f7318,plain,(
% 15.84/7.68 ![X0]: (divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)))=divide(inverse(X0),divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7275,f5100])).
% 15.84/7.68 fof(f7323,plain,(
% 15.84/7.68 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,X0))=divide(inverse(X0),divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7280,f7275])).
% 15.84/7.68 fof(f7349,plain,(
% 15.84/7.68 ![X0]: (divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)))=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7323,f7318])).
% 15.84/7.68 fof(f7440,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(divide(X0,X1)),divide(divide(sF1_fnc,b2),X0))=inverse(divide(divide(sF2_fnc,sF1_fnc),divide(X1,sF1_fnc))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6330,f31])).
% 15.84/7.68 fof(f7455,plain,(
% 15.84/7.68 ![X0,X1]: (divide(inverse(divide(X0,divide(X1,divide(sF1_fnc,divide(sF2_fnc,sF1_fnc))))),divide(divide(sF1_fnc,b2),X0))=X1)),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f6330,f4])).
% 15.84/7.68 fof(f7499,plain,(
% 15.84/7.68 ![X0]: (inverse(divide(divide(sF2_fnc,sF1_fnc),divide(divide(X0,divide(sF1_fnc,divide(sF2_fnc,sF1_fnc))),sF1_fnc)))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7440,f7455])).
% 15.84/7.68 fof(f7500,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(divide(X0,divide(inverse(inverse(sF2_fnc)),divide(divide(sF2_fnc,sF1_fnc),sF1_fnc)))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7076,f7499])).
% 15.84/7.68 fof(f7501,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(divide(X0,inverse(divide(sF2_fnc,divide(multiply(sF2_fnc,sF1_fnc),sF1_fnc))))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f6322,f7500])).
% 15.84/7.68 fof(f7502,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(multiply(X0,divide(sF2_fnc,divide(multiply(sF2_fnc,sF1_fnc),sF1_fnc)))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7501])).
% 15.84/7.68 fof(f7503,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(multiply(X0,divide(sF2_fnc,divide(divide(sF2_fnc,sF1_fnc),sF1_fnc)))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f6387,f7502])).
% 15.84/7.68 fof(f7504,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(multiply(X0,divide(sF2_fnc,divide(sF1_fnc,b2)))))=X0)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f6330,f7503])).
% 15.84/7.68 fof(f7510,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(inverse(X0)),sF1_fnc)=inverse(inverse(divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4963,f4643])).
% 15.84/7.68 fof(f7512,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc)=inverse(inverse(inverse(X0))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f5,f4643])).
% 15.84/7.68 fof(f7524,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(multiply(sF1_fnc,inverse(inverse(X0)))),sF1_fnc)=divide(sF1_fnc,inverse(divide(sF1_fnc,X0))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4643,f5674])).
% 15.84/7.68 fof(f7530,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,inverse(inverse(X3))),X0))=inverse(divide(X2,divide(X1,divide(sF1_fnc,inverse(divide(sF1_fnc,X3)))))))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4643,f14])).
% 15.84/7.68 fof(f7537,plain,(
% 15.84/7.68 ![X0]: (divide(inverse(inverse(divide(X0,sF1_fnc))),sF1_fnc)=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7510,f5123])).
% 15.84/7.68 fof(f7546,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(inverse(divide(X0,X1))))=divide(X1,X0))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7512,f5674])).
% 15.84/7.68 fof(f7561,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(inverse(X0)))=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7512,f5714])).
% 15.84/7.68 fof(f7563,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,divide(X1,inverse(inverse(inverse(X3)))))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7512,f5712])).
% 15.84/7.68 fof(f7578,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(inverse(inverse(inverse(X2))),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7512,f5696])).
% 15.84/7.68 fof(f7608,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(inverse(inverse(inverse(X0)))))=divide(sF1_fnc,inverse(divide(sF1_fnc,X0))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7512,f7524])).
% 15.84/7.68 fof(f7609,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(inverse(inverse(inverse(X0)))))=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7608])).
% 15.84/7.68 fof(f7623,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0))=inverse(divide(X2,divide(X1,divide(sF1_fnc,inverse(divide(sF1_fnc,X3)))))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7530])).
% 15.84/7.68 fof(f7626,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0))=inverse(divide(X2,divide(X1,multiply(sF1_fnc,divide(sF1_fnc,X3))))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7623])).
% 15.84/7.68 fof(f7633,plain,(
% 15.84/7.68 ![X0]: (divide(divide(inverse(inverse(X0)),sF1_fnc),sF1_fnc)=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7510,f7537])).
% 15.84/7.68 fof(f7662,plain,(
% 15.84/7.68 ![X0,X1,X2]: (inverse(divide(inverse(X0),multiply(divide(X1,multiply(X2,X0)),inverse(inverse(X2)))))=X1)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7674,f17])).
% 15.84/7.68 fof(f7674,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0))=inverse(divide(X2,multiply(X1,inverse(inverse(X3))))))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7563])).
% 15.84/7.68 fof(f7724,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(inverse(inverse(X0))))=divide(divide(X0,sF1_fnc),sF1_fnc))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f4963,f7546])).
% 15.84/7.68 fof(f7743,plain,(
% 15.84/7.68 ![X0,X1,X2]: (multiply(X0,inverse(inverse(divide(X1,X2))))=divide(X0,divide(X2,X1)))),
% 15.84/7.68 inference(paramodulation,[status(thm)],[f7546,f5])).
% 15.84/7.68 fof(f7746,plain,(
% 15.84/7.68 ![X0]: (divide(divide(inverse(X0),sF1_fnc),sF1_fnc)=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7724,f7609])).
% 15.84/7.68 fof(f7780,plain,(
% 15.84/7.68 ![X0]: (multiply(sF1_fnc,divide(sF1_fnc,inverse(X0)))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7746,f7633])).
% 15.84/7.68 fof(f7795,plain,(
% 15.84/7.68 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7780])).
% 15.84/7.68 fof(f7796,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF1_fnc),sF1_fnc)=divide(sF0_fnc,divide(sF1_fnc,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f5523])).
% 15.84/7.68 fof(f7801,plain,(
% 15.84/7.68 ![X0]: (multiply(X0,sF2_fnc)=divide(X0,b2))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f5124])).
% 15.84/7.68 fof(f7803,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(divide(X0,X1)))=multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f5445])).
% 15.84/7.68 fof(f7806,plain,(
% 15.84/7.68 ![X0]: (divide(sF1_fnc,divide(X0,sF1_fnc))=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f7349])).
% 15.84/7.68 fof(f7807,plain,(
% 15.84/7.68 ![X0]: (multiply(divide(sF1_fnc,sF1_fnc),X0)=divide(divide(X0,sF1_fnc),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f5444])).
% 15.84/7.68 fof(f7817,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(X2,X0))=inverse(divide(inverse(inverse(X2)),X1)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7818,f4964])).
% 15.84/7.68 fof(f7818,plain,(
% 15.84/7.68 ![X0]: (X0=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5412,f7795])).
% 15.84/7.68 fof(f7848,plain,(
% 15.84/7.68 divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc)=sF0_fnc),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7853,f5518])).
% 15.84/7.68 fof(f7853,plain,(
% 15.84/7.68 divide(divide(sF0_fnc,sF1_fnc),sF1_fnc)=sF0_fnc),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7818,f7796])).
% 15.84/7.68 fof(f7854,plain,(
% 15.84/7.68 divide(sF1_fnc,b2)=sF2_fnc),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7801,f5336])).
% 15.84/7.68 fof(f7893,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(X0,X1)=multiply(multiply(inverse(inverse(divide(X0,X1))),inverse(X2)),X2))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7803,f2260])).
% 15.84/7.68 fof(f7900,plain,(
% 15.84/7.68 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7948,f6277])).
% 15.84/7.68 fof(f7901,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(X0))=X0)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7948,f5783])).
% 15.84/7.68 fof(f7903,plain,(
% 15.84/7.68 divide(divide(a2,sF1_fnc),sF1_fnc)=divide(sF1_fnc,inverse(sF0_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7948,f6331])).
% 15.84/7.68 fof(f7910,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(inverse(divide(X0,X1)))=inverse(divide(X1,X0)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7948,f7803])).
% 15.84/7.68 fof(f7912,plain,(
% 15.84/7.68 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0))=inverse(divide(X2,divide(X1,inverse(X3)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7948,f7626])).
% 15.84/7.68 fof(f7948,plain,(
% 15.84/7.68 ![X0]: (inverse(X0)=multiply(sF1_fnc,divide(sF1_fnc,X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f4963,f7806])).
% 15.84/7.68 fof(f7950,plain,(
% 15.84/7.68 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7807,f5599])).
% 15.84/7.68 fof(f8018,plain,(
% 15.84/7.68 ![X0,X1,X2]: (inverse(divide(inverse(inverse(multiply(X0,X1))),X2))=inverse(divide(X0,divide(X2,divide(divide(X1,sF1_fnc),sF1_fnc)))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7817,f6403])).
% 15.84/7.68 fof(f8034,plain,(
% 15.84/7.68 ![X0]: (inverse(inverse(multiply(X0,divide(sF2_fnc,sF2_fnc))))=X0)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7854,f7504])).
% 15.84/7.68 fof(f8113,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(inverse(inverse(divide(X0,X1))),X2),X2))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7900,f7893])).
% 15.84/7.68 fof(f8147,plain,(
% 15.84/7.68 ![X0,X1,X2]: (inverse(divide(inverse(X0),divide(divide(X1,multiply(X2,X0)),inverse(X2))))=X1)),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7900,f7662])).
% 15.84/7.68 fof(f8175,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(X0,inverse(divide(X1,X2)))=divide(X0,divide(X2,X1)))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7900,f7743])).
% 15.84/7.68 fof(f8214,plain,(
% 15.84/7.68 ![X0,X1,X2]: (divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(inverse(X2),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7901,f7578])).
% 15.84/7.68 fof(f8226,plain,(
% 15.84/7.68 ![X0,X1]: (inverse(X0)=multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))))),
% 15.84/7.68 inference(backward_demodulation,[status(thm)],[f7901,f7561])).
% 15.84/7.68 fof(f8327,plain,(
% 15.84/7.68 divide(divide(a2,sF1_fnc),sF1_fnc)=multiply(sF1_fnc,sF0_fnc)),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5,f7903])).
% 15.84/7.68 fof(f8329,plain,(
% 15.84/7.68 divide(divide(a2,sF1_fnc),sF1_fnc)=a2),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f5461,f8327])).
% 15.84/7.68 fof(f8470,plain,(
% 15.84/7.68 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 15.84/7.68 inference(forward_demodulation,[status(thm)],[f7901,f7910])).
% 15.84/7.68 fof(f8471,plain,(
% 15.84/7.68 ![X0,X1,X2]: (inverse(divide(inverse(inverse(multiply(X0,inverse(X1)))),X2))=inverse(divide(X0,divide(X2,inverse(X1)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7817,f7912])).
% 15.84/7.70 fof(f8472,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,inverse(inverse(multiply(X1,inverse(X2)))))=inverse(divide(X1,divide(X0,inverse(X2)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8470,f8471])).
% 15.84/7.70 fof(f8473,plain,(
% 15.84/7.70 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,inverse(X2))))=inverse(divide(X1,divide(X0,inverse(X2)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f8472])).
% 15.84/7.70 fof(f8474,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,multiply(X1,inverse(X2)))=inverse(divide(X1,divide(X0,inverse(X2)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7900,f8473])).
% 15.84/7.70 fof(f8475,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=inverse(divide(X1,divide(X0,inverse(X2)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7900,f8474])).
% 15.84/7.70 fof(f8476,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=divide(divide(X0,inverse(X2)),X1))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8470,f8475])).
% 15.84/7.70 fof(f8483,plain,(
% 15.84/7.70 divide(sF1_fnc,divide(sF1_fnc,divide(a2,sF1_fnc)))=sF0_fnc),
% 15.84/7.70 inference(backward_demodulation,[status(thm)],[f8498,f7848])).
% 15.84/7.70 fof(f8498,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=divide(multiply(X0,X2),X1))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f8476])).
% 15.84/7.70 fof(f8563,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(multiply(X0,a2),divide(sF1_fnc,inverse(sF0_fnc))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8498,f7950])).
% 15.84/7.70 fof(f8564,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(X0,divide(divide(sF1_fnc,inverse(sF0_fnc)),a2)))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8498,f8563])).
% 15.84/7.70 fof(f8565,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(X0,divide(multiply(sF1_fnc,sF0_fnc),a2)))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f8564])).
% 15.84/7.70 fof(f8566,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(X0,divide(sF1_fnc,divide(a2,sF0_fnc))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8498,f8565])).
% 15.84/7.70 fof(f8567,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=divide(X0,divide(sF1_fnc,sF1_fnc)))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5854,f8566])).
% 15.84/7.70 fof(f8584,plain,(
% 15.84/7.70 ![X0]: (divide(divide(X0,sF1_fnc),sF1_fnc)=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7818,f8567])).
% 15.84/7.70 fof(f8754,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,inverse(inverse(multiply(X1,X2))))=inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8470,f8018])).
% 15.84/7.70 fof(f8755,plain,(
% 15.84/7.70 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,X2)))=inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f8754])).
% 15.84/7.70 fof(f8756,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,multiply(X1,X2))=inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7900,f8755])).
% 15.84/7.70 fof(f8757,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,multiply(X1,X2))=divide(divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)),X1))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8470,f8756])).
% 15.84/7.70 fof(f8828,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,multiply(X1,X2))=divide(divide(X0,X2),X1))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8584,f8757])).
% 15.84/7.70 fof(f8879,plain,(
% 15.84/7.70 ![X0]: (multiply(X0,divide(sF2_fnc,sF2_fnc))=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7901,f8034])).
% 15.84/7.70 fof(f8881,plain,(
% 15.84/7.70 ![X0]: (multiply(X0,sF1_fnc)=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f12,f8879])).
% 15.84/7.70 fof(f9032,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(divide(X0,X1),X2),X2))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7901,f8113])).
% 15.84/7.70 fof(f9034,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,multiply(X2,X1)),X2))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8828,f9032])).
% 15.84/7.70 fof(f9184,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(divide(divide(X0,multiply(X1,X2)),inverse(X1)),inverse(X2))=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8470,f8147])).
% 15.84/7.70 fof(f9185,plain,(
% 15.84/7.70 ![X0,X1,X2]: (multiply(divide(divide(X0,multiply(X1,X2)),inverse(X1)),X2)=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f9184])).
% 15.84/7.70 fof(f9186,plain,(
% 15.84/7.70 ![X0,X1,X2]: (multiply(multiply(divide(X0,multiply(X1,X2)),X1),X2)=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f9185])).
% 15.84/7.70 fof(f9190,plain,(
% 15.84/7.70 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f9034,f9186])).
% 15.84/7.70 fof(f9441,plain,(
% 15.84/7.70 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f5,f8175])).
% 15.84/7.70 fof(f9797,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(divide(X0,divide(X1,sF1_fnc)),multiply(X2,divide(inverse(X2),X1)))=divide(X0,sF1_fnc))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f7901,f8214])).
% 15.84/7.70 fof(f9798,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,multiply(multiply(X1,divide(inverse(X1),X2)),divide(X2,sF1_fnc)))=divide(X0,sF1_fnc))),
% 15.84/7.70 inference(forward_demodulation,[status(thm)],[f8828,f9797])).
% 15.84/7.70 fof(f9799,plain,(
% 15.84/7.70 ![X0,X1,X2]: (divide(X0,divide(multiply(X1,divide(inverse(X1),X2)),divide(sF1_fnc,X2)))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9441,f9798])).
% 13.52/7.73 fof(f9800,plain,(
% 13.52/7.73 ![X0,X1,X2]: (divide(X0,divide(X1,divide(divide(sF1_fnc,X2),divide(inverse(X1),X2))))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8498,f9799])).
% 13.52/7.73 fof(f9801,plain,(
% 13.52/7.73 ![X0,X1,X2]: (divide(X0,divide(X1,divide(sF1_fnc,multiply(divide(inverse(X1),X2),X2))))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8828,f9800])).
% 13.52/7.73 fof(f9802,plain,(
% 13.52/7.73 ![X0,X1]: (divide(X0,divide(X1,divide(sF1_fnc,inverse(X1))))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9190,f9801])).
% 13.52/7.73 fof(f9803,plain,(
% 13.52/7.73 ![X0,X1]: (divide(X0,divide(X1,multiply(sF1_fnc,X1)))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f5,f9802])).
% 13.52/7.73 fof(f9804,plain,(
% 13.52/7.73 ![X0]: (divide(X0,inverse(sF1_fnc))=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f6286,f9803])).
% 13.52/7.73 fof(f9805,plain,(
% 13.52/7.73 ![X0]: (multiply(X0,sF1_fnc)=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f5,f9804])).
% 13.52/7.73 fof(f9816,plain,(
% 13.52/7.73 ![X0]: (X0=divide(X0,sF1_fnc))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8881,f9805])).
% 13.52/7.73 fof(f9897,plain,(
% 13.52/7.73 ![X0,X1]: (inverse(X0)=divide(divide(sF1_fnc,X1),divide(divide(X0,sF1_fnc),X1)))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9441,f8226])).
% 13.52/7.73 fof(f9898,plain,(
% 13.52/7.73 ![X0,X1]: (inverse(X0)=divide(sF1_fnc,multiply(divide(divide(X0,sF1_fnc),X1),X1)))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8828,f9897])).
% 13.52/7.73 fof(f9899,plain,(
% 13.52/7.73 ![X0]: (inverse(X0)=divide(sF1_fnc,divide(X0,sF1_fnc)))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9190,f9898])).
% 13.52/7.73 fof(f9907,plain,(
% 13.52/7.73 ![X0]: (inverse(X0)=divide(sF1_fnc,X0))),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9816,f9899])).
% 13.52/7.73 fof(f12208,plain,(
% 13.52/7.73 inverse(divide(sF1_fnc,divide(a2,sF1_fnc)))=sF0_fnc),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f9907,f8483])).
% 13.52/7.73 fof(f12209,plain,(
% 13.52/7.73 divide(divide(a2,sF1_fnc),sF1_fnc)=sF0_fnc),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8470,f12208])).
% 13.52/7.73 fof(f12210,plain,(
% 13.52/7.73 a2=sF0_fnc),
% 13.52/7.73 inference(forward_demodulation,[status(thm)],[f8329,f12209])).
% 13.52/7.73 fof(f12211,plain,(
% 13.52/7.73 $false),
% 13.52/7.73 inference(forward_subsumption_resolution,[status(thm)],[f12210,f10])).
% 13.52/7.73 % SZS output end CNFRefutation for theBenchmark.p
% 13.52/7.74 % Elapsed time: 2.136393 seconds
% 13.52/7.74 % CPU time: 16.798090 seconds
% 13.52/7.74 % Total memory used: 341.215 MB
% 13.52/7.74 % Net memory used: 337.252 MB
%------------------------------------------------------------------------------