%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP476-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:36:41 PM UTC 2026
% Result : Unsatisfiable 109.72s 14.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP476-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n004.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Sun Sep 20 20:14:05 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.08/0.34 % Drodi V4.1.1
% 109.72/14.47 % Refutation found
% 109.72/14.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 109.72/14.47 % SZS output start CNFRefutation for theBenchmark
% 109.72/14.47 fof(f1,axiom,(
% 109.72/14.47 (![A,B,C,D]: (divide(inverse(divide(divide(divide(A,B),C),divide(D,C))),divide(B,A)) = D ))),
% 109.72/14.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.72/14.47 fof(f2,axiom,(
% 109.72/14.47 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 109.72/14.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.72/14.47 fof(f3,negated_conjecture,(
% 109.72/14.47 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 109.72/14.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 109.72/14.47 fof(f4,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),X2),divide(X3,X2))),divide(X1,X0))=X3)),
% 109.72/14.47 inference(cnf_transformation,[status(thm)],[f1])).
% 109.72/14.47 fof(f5,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 109.72/14.47 inference(cnf_transformation,[status(thm)],[f2])).
% 109.72/14.47 fof(f6,plain,(
% 109.72/14.47 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 109.72/14.47 inference(cnf_transformation,[status(thm)],[f3])).
% 109.72/14.47 fof(f7,definition,(
% 109.72/14.47 sF2_fnc=inverse(b2)),
% 109.72/14.47 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 109.72/14.47 fof(f8,definition,(
% 109.72/14.47 sF1_fnc=multiply(sF2_fnc,b2)),
% 109.72/14.47 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 109.72/14.47 fof(f9,definition,(
% 109.72/14.47 sF0_fnc=multiply(sF1_fnc,a2)),
% 109.72/14.47 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 109.72/14.47 fof(f10,plain,(
% 109.72/14.47 ~sF0_fnc=a2),
% 109.72/14.47 inference(definition_folding,[],[f6,f9,f8,f7])).
% 109.72/14.47 fof(f11,plain,(
% 109.72/14.47 ![X0]: (multiply(X0,b2)=divide(X0,sF2_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f7,f5])).
% 109.72/14.47 fof(f13,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),divide(X3,inverse(X2)))),divide(X1,X0))=X3)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f4])).
% 109.72/14.47 fof(f14,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(X0,X1),divide(X2,X1))),divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X5),divide(X0,X5)))))=X2)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f4,f4])).
% 109.72/14.47 fof(f16,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(multiply(X0,X1),X2),divide(X3,X2))),divide(inverse(X1),X0))=X3)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f4])).
% 109.72/14.47 fof(f17,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0))=inverse(divide(divide(divide(X3,X2),X5),divide(X4,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f4,f4])).
% 109.72/14.47 fof(f20,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(divide(X0,X1),inverse(divide(divide(divide(X1,X0),X2),divide(X3,X2)))),X4),divide(X5,X4))),X3)=X5)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f4,f4])).
% 109.72/14.47 fof(f25,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),multiply(X3,X2))),divide(X1,X0))=X3)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f13])).
% 109.72/14.47 fof(f26,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(X0,X1),divide(X2,X1))),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X0,X5))))=X2)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 109.72/14.47 fof(f29,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),X4),divide(X5,X4))),X3)=X5)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f20])).
% 109.72/14.47 fof(f32,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(multiply(X0,b2),X1),multiply(X2,X1))),divide(sF2_fnc,X0))=X2)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f11,f25])).
% 109.72/14.47 fof(f34,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(divide(X0,X1),a2),sF0_fnc)),divide(X1,X0))=sF1_fnc)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f9,f25])).
% 109.72/14.47 fof(f35,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(divide(X0,X1),b2),sF1_fnc)),divide(X1,X0))=sF2_fnc)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f8,f25])).
% 109.72/14.47 fof(f39,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(inverse(X0),X1),X2),multiply(X3,X2))),multiply(X1,X0))=X3)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f25])).
% 109.72/14.47 fof(f76,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),inverse(divide(divide(X3,X4),divide(X5,X4)))),X6),multiply(X7,X6))),X5)=X7)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f26,f25])).
% 109.72/14.47 fof(f77,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),divide(multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X6,X5))),inverse(divide(divide(X6,X7),divide(X0,X7)))))=X2)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f26,f25])).
% 109.72/14.47 fof(f95,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(multiply(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),divide(divide(X3,X4),divide(X5,X4))),X6),multiply(X7,X6))),X5)=X7)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f76])).
% 109.72/14.47 fof(f96,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),multiply(multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X6,X5))),divide(divide(X6,X7),divide(X0,X7))))=X2)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f77])).
% 109.72/14.47 fof(f105,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(divide(divide(X0,X1),inverse(divide(multiply(divide(X1,X0),a2),sF0_fnc))),a2),sF0_fnc)),sF1_fnc)=sF1_fnc)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f34,f34])).
% 109.72/14.47 fof(f126,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),sF0_fnc)),a2),sF0_fnc)),sF1_fnc)=sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f105])).
% 109.72/14.47 fof(f188,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(sF1_fnc,X0),multiply(X1,X0))),divide(sF2_fnc,sF2_fnc))=X1)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f8,f32])).
% 109.72/14.47 fof(f207,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(sF1_fnc,X0),multiply(X1,X0))),multiply(sF2_fnc,b2))=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f11,f188])).
% 109.72/14.47 fof(f208,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(multiply(sF1_fnc,X0),multiply(X1,X0))),sF1_fnc)=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8,f207])).
% 109.72/14.47 fof(f221,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(sF0_fnc,multiply(X0,a2))),sF1_fnc)=X0)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f9,f208])).
% 109.72/14.47 fof(f222,plain,(
% 109.72/14.47 divide(inverse(divide(multiply(sF1_fnc,a2),sF0_fnc)),sF1_fnc)=sF1_fnc),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f9,f208])).
% 109.72/14.47 fof(f231,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(X0,sF1_fnc),X1)),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X0,X4))))=inverse(divide(multiply(sF1_fnc,X5),multiply(X1,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f208,f26])).
% 109.72/14.47 fof(f238,plain,(
% 109.72/14.47 divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc)=sF1_fnc),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9,f222])).
% 109.72/14.47 fof(f282,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(X0,sF1_fnc),X1)),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X0,X4))))=inverse(divide(sF0_fnc,multiply(X1,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f221,f26])).
% 109.72/14.47 fof(f287,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(divide(divide(X0,X1),sF1_fnc),X2)),divide(X1,X0))=inverse(divide(sF0_fnc,multiply(X2,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f221,f4])).
% 109.72/14.47 fof(f296,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,multiply(X0,a2)))=inverse(divide(multiply(sF1_fnc,X1),multiply(X0,X1))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f282,f231])).
% 109.72/14.47 fof(f311,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),divide(inverse(b2),sF2_fnc))=X1)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f8,f16])).
% 109.72/14.47 fof(f344,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(divide(divide(inverse(X0),X1),inverse(divide(divide(multiply(X1,X0),X2),divide(X3,X2)))),X4),multiply(X5,X4))),X3)=X5)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f16,f25])).
% 109.72/14.47 fof(f351,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),multiply(inverse(b2),b2))=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f11,f311])).
% 109.72/14.47 fof(f352,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),multiply(sF2_fnc,b2))=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f7,f351])).
% 109.72/14.47 fof(f353,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),sF1_fnc)=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8,f352])).
% 109.72/14.47 fof(f365,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(multiply(divide(inverse(X0),X1),divide(divide(multiply(X1,X0),X2),divide(X3,X2))),X4),multiply(X5,X4))),X3)=X5)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f344])).
% 109.72/14.47 fof(f370,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (X0=inverse(divide(divide(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f4,f17])).
% 109.72/14.47 fof(f373,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(multiply(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0))=inverse(divide(divide(divide(X3,X2),X5),divide(inverse(X4),X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f17])).
% 109.72/14.47 fof(f377,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),divide(divide(X3,X4),inverse(divide(multiply(divide(X4,X3),b2),sF1_fnc))))=inverse(divide(divide(divide(X1,X0),X5),divide(X2,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f35,f17])).
% 109.72/14.47 fof(f387,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),sF1_fnc),X2)),divide(X1,X0))=inverse(divide(divide(divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc))),X3),divide(X2,X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f238,f17])).
% 109.72/14.47 fof(f389,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X1),sF2_fnc),X2)),divide(X1,X0))=inverse(divide(divide(divide(divide(X3,X4),inverse(divide(multiply(divide(X4,X3),b2),sF1_fnc))),X5),divide(X2,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f35,f17])).
% 109.72/14.47 fof(f394,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0))=inverse(divide(divide(divide(divide(X4,X5),inverse(divide(divide(divide(X5,X4),X6),divide(X2,X6)))),X7),divide(X3,X7))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f4,f17])).
% 109.72/14.47 fof(f395,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0))=inverse(divide(divide(divide(multiply(divide(X4,X5),divide(divide(divide(X5,X4),X6),divide(X7,X6))),inverse(divide(divide(X7,X8),divide(X2,X8)))),X9),divide(X3,X9))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f26,f17])).
% 109.72/14.47 fof(f397,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X1),multiply(X2,X3)),X4)),divide(X1,X0))=inverse(divide(divide(divide(inverse(X3),X2),X5),divide(X4,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f17])).
% 109.72/14.47 fof(f412,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(divide(X0,X1),divide(sF1_fnc,inverse(divide(sF0_fnc,multiply(X2,a2))))),X3)),divide(X1,X0))=inverse(divide(divide(X2,X4),divide(X3,X4))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f221,f17])).
% 109.72/14.47 fof(f419,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(divide(X0,X1),divide(divide(X2,X3),inverse(divide(divide(divide(X3,X2),divide(X4,X5)),X6)))),X7)),divide(X1,X0))=inverse(divide(divide(inverse(divide(divide(divide(X5,X4),X8),divide(X6,X8))),X9),divide(X7,X9))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f17,f17])).
% 109.72/14.47 fof(f426,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),inverse(divide(multiply(divide(X4,X5),a2),sF0_fnc)))),divide(X1,X0))=inverse(divide(divide(divide(X3,X2),divide(X5,X4)),sF1_fnc)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f34,f17])).
% 109.72/14.47 fof(f453,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(X0,divide(divide(divide(X1,X2),X3),divide(X4,X3)))=divide(X0,divide(inverse(divide(divide(divide(X5,X6),divide(X2,X1)),X4)),divide(X6,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f17,f5])).
% 109.72/14.47 fof(f459,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),multiply(divide(X3,X4),divide(multiply(divide(X4,X3),b2),sF1_fnc)))=inverse(divide(divide(divide(X1,X0),X5),divide(X2,X5))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f377])).
% 109.72/14.47 fof(f467,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,multiply(X0,a2)))=inverse(divide(divide(divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc))),X1),divide(X0,X1))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f287,f387])).
% 109.72/14.47 fof(f469,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,multiply(X0,a2)))=inverse(divide(divide(multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),X1),divide(X0,X1))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f467])).
% 109.72/14.47 fof(f471,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(divide(X0,X1),b2),X2)),divide(X1,X0))=inverse(divide(divide(divide(divide(X3,X4),inverse(divide(multiply(divide(X4,X3),b2),sF1_fnc))),X5),divide(X2,X5))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f11,f389])).
% 109.72/14.47 fof(f472,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(divide(X0,X1),b2),X2)),divide(X1,X0))=inverse(divide(divide(multiply(divide(X3,X4),divide(multiply(divide(X4,X3),b2),sF1_fnc)),X5),divide(X2,X5))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f471])).
% 109.72/14.47 fof(f480,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0))=inverse(divide(divide(multiply(divide(X4,X5),divide(divide(divide(X5,X4),X6),divide(X2,X6))),X7),divide(X3,X7))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f394])).
% 109.72/14.47 fof(f481,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0))=inverse(divide(divide(multiply(multiply(divide(X4,X5),divide(divide(divide(X5,X4),X6),divide(X7,X6))),divide(divide(X7,X8),divide(X2,X8))),X9),divide(X3,X9))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f395])).
% 109.72/14.47 fof(f495,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(divide(X0,X1),multiply(sF1_fnc,divide(sF0_fnc,multiply(X2,a2)))),X3)),divide(X1,X0))=inverse(divide(divide(X2,X4),divide(X3,X4))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f412])).
% 109.72/14.47 fof(f502,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(divide(X0,X1),multiply(divide(X2,X3),divide(divide(divide(X3,X2),divide(X4,X5)),X6))),X7)),divide(X1,X0))=inverse(divide(divide(inverse(divide(divide(divide(X5,X4),X8),divide(X6,X8))),X9),divide(X7,X9))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f419])).
% 109.72/14.47 fof(f508,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(multiply(divide(divide(X0,X1),divide(X2,X3)),divide(multiply(divide(X4,X5),a2),sF0_fnc))),divide(X1,X0))=inverse(divide(divide(divide(X3,X2),divide(X5,X4)),sF1_fnc)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f426])).
% 109.72/14.47 fof(f536,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(inverse(X3),X2))),X4),divide(X5,X4))),X3)=X5)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f29])).
% 109.72/14.47 fof(f586,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),X4),X5)),X3)=inverse(divide(divide(multiply(divide(X6,X7),divide(divide(divide(X7,X6),X8),divide(X4,X8))),X9),divide(X5,X9))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f29,f29])).
% 109.72/14.47 fof(f610,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(X0,divide(X1,X2))),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(inverse(divide(divide(multiply(divide(X6,X7),divide(divide(divide(X7,X6),X8),divide(X2,X8))),X9),divide(X0,X9))),X5))))=X1)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f29,f26])).
% 109.72/14.47 fof(f739,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),sF1_fnc)=inverse(divide(sF0_fnc,multiply(X0,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f221,f353])).
% 109.72/14.47 fof(f744,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,divide(X0,X1)),X2)),sF1_fnc)=inverse(divide(multiply(divide(X1,X0),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f25,f353])).
% 109.72/14.47 fof(f746,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(divide(multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X0,X4))),X5),divide(X1,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f29,f353])).
% 109.72/14.47 fof(f750,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2)))),X4)),sF1_fnc)=inverse(divide(divide(X3,X5),divide(X4,X5))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f26,f353])).
% 109.72/14.47 fof(f789,plain,(
% 109.72/14.47 ![X0,X1]: (divide(divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc),X0)=X1)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f746,f29])).
% 109.72/14.47 fof(f790,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(divide(divide(sF1_fnc,inverse(X0)),X1)),sF1_fnc),X0)=X1)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f746,f536])).
% 109.72/14.47 fof(f792,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(X0,divide(X1,X2))),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(divide(inverse(divide(divide(sF1_fnc,X2),X0)),sF1_fnc),X5))))=X1)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f746,f610])).
% 109.72/14.47 fof(f796,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),X4),X5)),X3)=divide(inverse(divide(divide(sF1_fnc,X4),X5)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f746,f586])).
% 109.72/14.47 fof(f797,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0))=divide(inverse(divide(divide(sF1_fnc,X2),X3)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f746,f480])).
% 109.72/14.47 fof(f826,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc),X0)=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f790])).
% 109.72/14.47 fof(f858,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(X0,a2)))),X1)),sF1_fnc)=inverse(divide(divide(X0,X2),divide(X1,X2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f797,f495])).
% 109.72/14.47 fof(f864,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),divide(X2,X3)),X4))),X5)),sF1_fnc)=inverse(divide(divide(inverse(divide(divide(divide(X3,X2),X6),divide(X4,X6))),X7),divide(X5,X7))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f797,f502])).
% 109.72/14.47 fof(f868,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2)),sF1_fnc)=inverse(divide(divide(divide(inverse(X1),X0),X3),divide(X2,X3))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f797,f397])).
% 109.72/14.47 fof(f873,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(divide(divide(X1,X2),X3),divide(X4,X3)))=divide(X0,divide(inverse(divide(divide(sF1_fnc,divide(X2,X1)),X4)),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f797,f453])).
% 109.72/14.47 fof(f881,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(divide(multiply(multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X5,X4))),divide(divide(X5,X6),divide(X0,X6))),X7),divide(X1,X7))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f797,f481])).
% 109.72/14.47 fof(f901,plain,(
% 109.72/14.47 ![X0,X1]: (divide(divide(inverse(multiply(divide(sF1_fnc,X0),X1)),sF1_fnc),X0)=inverse(X1))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f789])).
% 109.72/14.47 fof(f920,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(multiply(multiply(sF1_fnc,X0),X1)),sF1_fnc),X0)=inverse(X1))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f826])).
% 109.72/14.47 fof(f921,plain,(
% 109.72/14.47 ![X0]: (multiply(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),a2)=X0)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f9,f826])).
% 109.72/14.47 fof(f922,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(X0,sF1_fnc)),divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,b2),X0))))=sF2_fnc)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f35])).
% 109.72/14.47 fof(f924,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(X0,multiply(X1,X2))),divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,X2),X0))))=X1)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f25])).
% 109.72/14.47 fof(f928,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X1),X2),X3)),divide(X1,X0))=divide(inverse(divide(multiply(sF1_fnc,X2),X3)),sF1_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f25])).
% 109.72/14.47 fof(f931,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(X0,sF1_fnc)),multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)))=sF2_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f922])).
% 109.72/14.47 fof(f936,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(X0,multiply(X1,X2))),multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X0)))=X1)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f924])).
% 109.72/14.47 fof(f945,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(sF1_fnc,b2),X0)),sF1_fnc)=inverse(divide(divide(multiply(divide(X1,X2),divide(multiply(divide(X2,X1),b2),sF1_fnc)),X3),divide(X0,X3))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f928,f472])).
% 109.72/14.47 fof(f1057,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),inverse(X3)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f370])).
% 109.72/14.47 fof(f1069,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(multiply(divide(sF1_fnc,divide(X0,X1)),X2)),sF1_fnc)=inverse(divide(divide(divide(X1,X0),X3),divide(inverse(X2),X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f901,f370])).
% 109.72/14.47 fof(f1076,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(divide(divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc))),X1),divide(divide(X0,sF1_fnc),X1))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f238,f370])).
% 109.72/14.47 fof(f1086,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X0,divide(X2,X1)),X3))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f1057])).
% 109.72/14.47 fof(f1098,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(multiply(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0))=divide(inverse(multiply(divide(sF1_fnc,divide(X2,X3)),X4)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1069,f373])).
% 109.72/14.47 fof(f1105,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(divide(multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),X1),divide(divide(X0,sF1_fnc),X1))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f1076])).
% 109.72/14.47 fof(f1106,plain,(
% 109.72/14.47 ![X0]: (X0=inverse(divide(sF0_fnc,multiply(divide(X0,sF1_fnc),a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f469,f1105])).
% 109.72/14.47 fof(f1115,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(multiply(divide(sF1_fnc,divide(X0,X1)),divide(multiply(divide(X2,X3),a2),sF0_fnc))),sF1_fnc)=inverse(divide(divide(divide(X1,X0),divide(X3,X2)),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1098,f508])).
% 109.72/14.47 fof(f1131,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(divide(X1,sF1_fnc),a2)))=divide(X0,X1))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1106,f5])).
% 109.72/14.47 fof(f1452,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(X1,multiply(divide(X0,divide(sF1_fnc,inverse(divide(sF0_fnc,X1)))),a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f921,f1086])).
% 109.72/14.47 fof(f1453,plain,(
% 109.72/14.47 ![X0,X1,X2]: (X0=inverse(divide(X1,multiply(divide(X0,divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,X2),X1)))),X2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f1086])).
% 109.72/14.47 fof(f1463,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(X1,X2),X3),multiply(divide(X0,divide(inverse(X2),X1)),X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f1086])).
% 109.72/14.47 fof(f1475,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X0,multiply(X2,X1)),X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f5,f1086])).
% 109.72/14.47 fof(f1481,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(X1,multiply(divide(X0,multiply(sF1_fnc,divide(sF0_fnc,X1))),a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f1452])).
% 109.72/14.47 fof(f1482,plain,(
% 109.72/14.47 ![X0,X1,X2]: (X0=inverse(divide(X1,multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X1))),X2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f1453])).
% 109.72/14.47 fof(f1502,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,X0))),X1)),sF1_fnc)=inverse(divide(X0,multiply(X1,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f789,f1481])).
% 109.72/14.47 fof(f1508,plain,(
% 109.72/14.47 ![X0]: (divide(X0,sF1_fnc)=divide(X0,multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1481,f221])).
% 109.72/14.47 fof(f1513,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(multiply(X0,a2),multiply(X1,a2)))=inverse(divide(divide(X0,X2),divide(X1,X2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1502,f858])).
% 109.72/14.47 fof(f1529,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),divide(X2,X3)),X4))),X5)),sF1_fnc)=inverse(divide(multiply(inverse(divide(divide(divide(X3,X2),X6),divide(X4,X6))),a2),multiply(X5,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f864])).
% 109.72/14.47 fof(f1538,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2)),sF1_fnc)=inverse(divide(multiply(divide(inverse(X1),X0),a2),multiply(X2,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f868])).
% 109.72/14.47 fof(f1577,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),multiply(divide(X3,X4),divide(multiply(divide(X4,X3),b2),sF1_fnc)))=inverse(divide(multiply(divide(X1,X0),a2),multiply(X2,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f459])).
% 109.72/14.47 fof(f1609,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(multiply(multiply(multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X5,X4))),divide(divide(X5,X6),divide(X0,X6))),a2),multiply(X1,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f881])).
% 109.72/14.47 fof(f1622,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,b2),X0)),sF1_fnc)=inverse(divide(multiply(multiply(divide(X1,X2),divide(multiply(divide(X2,X1),b2),sF1_fnc)),a2),multiply(X0,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f945])).
% 109.72/14.47 fof(f1668,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2)))),X4)),sF1_fnc)=inverse(divide(multiply(X3,a2),multiply(X4,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f1513,f750])).
% 109.72/14.47 fof(f1704,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),divide(X2,X3)),X4))),X5)),sF1_fnc)=inverse(divide(multiply(inverse(divide(multiply(divide(X3,X2),a2),multiply(X4,a2))),a2),multiply(X5,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1513,f1529])).
% 109.72/14.47 fof(f1718,plain,(
% 109.72/14.47 ![X0]: (divide(divide(inverse(divide(divide(sF1_fnc,X0),sF1_fnc)),sF1_fnc),X0)=multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1508,f789])).
% 109.72/14.47 fof(f1746,plain,(
% 109.72/14.47 sF1_fnc=multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f789,f1718])).
% 109.72/14.47 fof(f1761,plain,(
% 109.72/14.47 ![X0]: (multiply(divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc),divide(sF0_fnc,sF0_fnc))=inverse(X0))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1746,f920])).
% 109.72/14.47 fof(f1762,plain,(
% 109.72/14.47 ![X0]: (multiply(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),divide(sF0_fnc,sF0_fnc))=X0)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1746,f826])).
% 109.72/14.47 fof(f2037,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(X1,multiply(divide(X0,divide(sF1_fnc,inverse(divide(sF1_fnc,X1)))),divide(sF0_fnc,sF0_fnc)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1762,f1086])).
% 109.72/14.47 fof(f2040,plain,(
% 109.72/14.47 ![X0,X1]: (X0=inverse(divide(X1,multiply(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,X1))),divide(sF0_fnc,sF0_fnc)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f2037])).
% 109.72/14.47 fof(f2041,plain,(
% 109.72/14.47 multiply(divide(inverse(sF1_fnc),sF1_fnc),divide(sF0_fnc,sF0_fnc))=inverse(divide(sF0_fnc,sF0_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1746,f1761])).
% 109.72/14.47 fof(f2058,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(X0,multiply(X1,a2))),multiply(sF1_fnc,divide(sF0_fnc,X0)))=X1)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f921,f39])).
% 109.72/14.47 fof(f2408,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(divide(multiply(multiply(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),divide(divide(X3,X4),divide(multiply(sF1_fnc,divide(sF0_fnc,X5)),X4))),X6),multiply(X7,X6)))=inverse(divide(X5,multiply(X7,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f95,f1481])).
% 109.72/14.47 fof(f2487,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(X0,multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(X1,X2),a2))))=divide(X0,divide(X2,X1)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1086,f2058])).
% 109.72/14.47 fof(f2541,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(X0,X1)),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(divide(inverse(divide(divide(sF1_fnc,X5),X0)),sF1_fnc),X4))))=divide(inverse(divide(divide(sF1_fnc,X5),X1)),sF1_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f789,f792])).
% 109.72/14.47 fof(f2546,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (divide(inverse(divide(X0,X1)),multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(divide(inverse(divide(divide(sF1_fnc,multiply(divide(X5,X6),divide(divide(divide(X6,X5),X7),divide(divide(inverse(divide(divide(sF1_fnc,X8),X9)),sF1_fnc),X7)))),X0)),sF1_fnc),X4))))=inverse(divide(X9,divide(X1,X8))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f792,f792])).
% 109.72/14.47 fof(f2589,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(divide(inverse(divide(divide(sF1_fnc,X3),X4)),sF1_fnc),X2)))),X5)),sF1_fnc)=inverse(divide(X4,divide(X5,X3))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f2541,f2546])).
% 109.72/14.47 fof(f2590,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(multiply(divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc),a2),multiply(X2,a2)))=inverse(divide(X1,divide(X2,X0))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1668,f2589])).
% 109.72/14.47 fof(f2593,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(divide(sF1_fnc,X0),X1))),X2)),sF1_fnc)=inverse(divide(X1,divide(X2,X0))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1538,f2590])).
% 109.72/14.47 fof(f2730,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (divide(X0,multiply(multiply(divide(X1,X2),divide(divide(divide(X2,X1),X3),divide(X4,X3))),divide(divide(X4,X5),divide(X6,X5))))=divide(X0,multiply(sF1_fnc,divide(sF0_fnc,multiply(X6,a2)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1481,f96])).
% 109.72/14.47 fof(f2738,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc)))),multiply(multiply(divide(X1,X2),divide(divide(divide(X2,X1),X3),divide(X4,X3))),divide(divide(X4,X5),divide(sF1_fnc,X5))))=X0)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1746,f96])).
% 109.72/14.47 fof(f2749,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(divide(multiply(X0,X1),X2)),multiply(multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X6,X5))),divide(divide(X6,X7),divide(X0,X7))))=divide(inverse(divide(multiply(sF1_fnc,X1),X2)),sF1_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f96])).
% 109.72/14.47 fof(f2835,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc)))),multiply(sF1_fnc,divide(sF0_fnc,multiply(sF1_fnc,a2))))=X0)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f2730,f2738])).
% 109.72/14.47 fof(f2836,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc)))),multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)))=X0)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9,f2835])).
% 109.72/14.47 fof(f2837,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc)))),sF1_fnc)=X0)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1746,f2836])).
% 109.72/14.47 fof(f2862,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(X0,X1),X2)),multiply(sF1_fnc,divide(sF0_fnc,multiply(X0,a2))))=divide(inverse(divide(multiply(sF1_fnc,X1),X2)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f2730,f2749])).
% 109.72/14.47 fof(f2937,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(multiply(sF2_fnc,divide(divide(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)),divide(X0,sF1_fnc)),X1),divide(X2,X1))),X3),multiply(X4,X3))),X2)=X4)),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f931,f365])).
% 109.72/14.47 fof(f3082,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc))))=inverse(divide(sF0_fnc,multiply(X0,a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f2837,f1106])).
% 109.72/14.47 fof(f3187,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),divide(sF1_fnc,X1)))),X2))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1482,f789])).
% 109.72/14.47 fof(f3190,plain,(
% 109.72/14.47 ![X0,X1,X2]: (multiply(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),multiply(sF1_fnc,X1)))),X2))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1482,f826])).
% 109.72/14.47 fof(f4223,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(inverse(divide(sF0_fnc,multiply(X1,a2))),a2)))=divide(X0,inverse(divide(divide(sF1_fnc,sF1_fnc),X1))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f739,f1131])).
% 109.72/14.47 fof(f4236,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(inverse(divide(sF0_fnc,multiply(X1,a2))),a2)))=multiply(X0,divide(divide(sF1_fnc,sF1_fnc),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f4223])).
% 109.72/14.47 fof(f4636,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X0)))=divide(inverse(divide(multiply(sF1_fnc,X2),X1)),sF1_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f826,f936])).
% 109.72/14.47 fof(f4751,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,divide(inverse(X0),X1)),X2)),sF1_fnc)=inverse(divide(multiply(multiply(X1,X0),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f789,f1463])).
% 109.72/14.47 fof(f4908,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2)),sF1_fnc)=inverse(divide(multiply(divide(inverse(X1),X0),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f789,f1475])).
% 109.72/14.47 fof(f5743,plain,(
% 109.72/14.47 ![X0,X1]: (divide(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,divide(sF1_fnc,X1)))),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f2040,f789])).
% 109.72/14.47 fof(f5747,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,X1)))),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f2040,f826])).
% 109.72/14.47 fof(f5823,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(multiply(sF1_fnc,divide(sF1_fnc,X3)),X2))),X4),X5))=inverse(divide(X3,multiply(divide(inverse(divide(divide(sF1_fnc,X4),X5)),sF1_fnc),divide(sF0_fnc,sF0_fnc)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f796,f2040])).
% 109.72/14.47 fof(f5833,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6,X7]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(divide(X3,X4),X2))),X5),X6))=inverse(divide(multiply(divide(X4,X3),X7),multiply(divide(inverse(divide(divide(sF1_fnc,X5),X6)),sF1_fnc),X7))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f796,f1086])).
% 109.72/14.47 fof(f6188,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),a2),multiply(X1,a2)))=inverse(divide(inverse(divide(sF0_fnc,multiply(X0,a2))),divide(X1,sF1_fnc))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f739,f1513])).
% 109.72/14.47 fof(f6191,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(inverse(divide(sF0_fnc,sF0_fnc)),a2),multiply(X0,a2)))=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f238,f1513])).
% 109.72/14.47 fof(f6201,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(X0,a2),multiply(inverse(divide(sF0_fnc,multiply(X1,a2))),a2)))=inverse(divide(divide(X0,sF1_fnc),X1)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f221,f1513])).
% 109.72/14.47 fof(f6202,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),multiply(inverse(divide(sF0_fnc,sF0_fnc)),a2)))=inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f238,f1513])).
% 109.72/14.47 fof(f6217,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(X1,X2),divide(X3,X2)))=divide(X0,inverse(divide(multiply(X1,a2),multiply(X3,a2)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f1513,f5])).
% 109.72/14.47 fof(f6251,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(multiply(sF2_fnc,divide(multiply(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)),divide(X0,sF1_fnc)),a2),multiply(X1,a2))),X2),multiply(X3,X2))),X1)=X3)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f2937])).
% 109.72/14.47 fof(f6489,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(multiply(multiply(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),divide(multiply(X3,a2),multiply(multiply(sF1_fnc,divide(sF0_fnc,X4)),a2))),X5),multiply(X6,X5)))=inverse(divide(X4,multiply(X6,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f2408])).
% 109.72/14.47 fof(f6507,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(multiply(multiply(multiply(divide(X2,X3),divide(divide(divide(X3,X2),X4),divide(X5,X4))),divide(multiply(X5,a2),multiply(X0,a2))),a2),multiply(X1,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f1609])).
% 109.72/14.47 fof(f6712,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(multiply(sF1_fnc,divide(sF1_fnc,X2)),a2))),X3),X4))=inverse(divide(X2,multiply(divide(inverse(divide(divide(sF1_fnc,X3),X4)),sF1_fnc),divide(sF0_fnc,sF0_fnc)))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f5823])).
% 109.72/14.47 fof(f6747,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(divide(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(divide(X2,X3),a2))),X4),X5))=inverse(divide(multiply(divide(X3,X2),X6),multiply(divide(inverse(divide(divide(sF1_fnc,X4),X5)),sF1_fnc),X6))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f5833])).
% 109.72/14.47 fof(f6893,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (multiply(X0,divide(multiply(divide(X1,X2),a2),multiply(X3,a2)))=divide(X0,divide(inverse(divide(divide(sF1_fnc,divide(X2,X1)),X3)),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f6917,f873])).
% 109.72/14.47 fof(f6917,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(X1,X2),divide(X3,X2)))=multiply(X0,divide(multiply(X1,a2),multiply(X3,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f6217])).
% 109.72/14.47 fof(f7093,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(multiply(multiply(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(X2,a2))),divide(multiply(X2,a2),multiply(multiply(sF1_fnc,divide(sF0_fnc,X3)),a2))),X4),multiply(X5,X4)))=inverse(divide(X3,multiply(X5,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f6917,f6489])).
% 109.72/14.47 fof(f7118,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=inverse(divide(multiply(multiply(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),a2),multiply(X4,a2))),divide(multiply(X4,a2),multiply(X0,a2))),a2),multiply(X1,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f6917,f6507])).
% 109.72/14.47 fof(f7318,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(divide(X0,X1),X2),X3))=inverse(divide(multiply(divide(X0,X1),X4),multiply(divide(inverse(divide(divide(sF1_fnc,X2),X3)),sF1_fnc),X4))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f797,f1086])).
% 109.72/14.47 fof(f7358,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(divide(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(divide(X2,X3),a2))),X4),X5))=inverse(divide(divide(divide(X3,X2),X4),X5)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f7318,f6747])).
% 109.72/14.47 fof(f7564,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(X0,multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(inverse(divide(divide(sF1_fnc,X1),X2)),sF1_fnc),a2))))=divide(X0,divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X1),X2)))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f797,f2487])).
% 109.72/14.47 fof(f7577,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(divide(sF1_fnc,divide(X0,X1))),sF1_fnc),divide(sF0_fnc,sF0_fnc))=multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(X1,X0),a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f2487,f1762])).
% 109.72/14.47 fof(f7593,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,multiply(sF1_fnc,a2)))=inverse(divide(multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(X0,X1),a2))),divide(X1,X0))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f2487,f296])).
% 109.72/14.47 fof(f7631,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(X0,divide(sF1_fnc,inverse(divide(divide(sF1_fnc,X1),X2))))=divide(X0,divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X1),X2)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f2487,f7564])).
% 109.72/14.47 fof(f7632,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(X0,multiply(sF1_fnc,divide(divide(sF1_fnc,X1),X2)))=divide(X0,divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X1),X2)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f7631])).
% 109.72/14.47 fof(f7633,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(divide(sF1_fnc,divide(X0,X1)),X2))),X3)),sF1_fnc)=inverse(divide(multiply(inverse(divide(multiply(divide(X1,X0),a2),multiply(X2,a2))),a2),multiply(X3,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f7666,f1704])).
% 109.72/14.47 fof(f7666,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(X0,multiply(sF1_fnc,divide(divide(sF1_fnc,X1),X2)))=divide(X0,multiply(divide(X3,X4),divide(divide(divide(X4,X3),X1),X2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f7632])).
% 109.72/14.47 fof(f7692,plain,(
% 109.72/14.47 ![X0,X1]: (divide(X0,X1)=multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(X1,X0),a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1762,f7577])).
% 109.72/14.47 fof(f7713,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(multiply(sF1_fnc,divide(sF0_fnc,multiply(divide(X0,X1),a2))),divide(X1,X0))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9,f7593])).
% 109.72/14.47 fof(f7714,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(divide(X0,X1),divide(X0,X1))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f7692,f7713])).
% 109.72/14.47 fof(f7715,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(multiply(X0,a2),multiply(X0,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1513,f7714])).
% 109.72/14.47 fof(f7734,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=inverse(divide(multiply(inverse(divide(multiply(divide(X3,X2),a2),multiply(X0,a2))),a2),multiply(X1,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f2593,f7633])).
% 109.72/14.47 fof(f7762,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(divide(X0,X1)),sF1_fnc),divide(sF0_fnc,sF0_fnc))=inverse(divide(sF0_fnc,multiply(divide(X1,X0),a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f7692,f1761])).
% 109.72/14.47 fof(f7966,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(multiply(sF1_fnc,divide(sF1_fnc,X2)),a2))),X3),X4))=inverse(divide(X2,inverse(divide(sF0_fnc,multiply(divide(X4,divide(sF1_fnc,X3)),a2))))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f7762,f6712])).
% 109.72/14.47 fof(f8026,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(multiply(sF1_fnc,divide(sF1_fnc,X2)),a2))),X3),X4))=inverse(multiply(X2,divide(sF0_fnc,multiply(divide(X4,divide(sF1_fnc,X3)),a2)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f7966])).
% 109.72/14.47 fof(f8034,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(X0,multiply(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),a2))))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f921,f7715])).
% 109.72/14.47 fof(f8055,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF0_fnc,sF0_fnc))=inverse(divide(X0,X0)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f921,f8034])).
% 109.72/14.47 fof(f8071,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(X0,X0))=inverse(divide(X1,X1)))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f8055,f8055])).
% 109.72/14.47 fof(f8074,plain,(
% 109.72/14.47 inverse(divide(sF0_fnc,sF0_fnc))=inverse(multiply(sF2_fnc,b2))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f11,f8055])).
% 109.72/14.47 fof(f8085,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(sF0_fnc,sF0_fnc)),divide(X0,X1))=divide(inverse(divide(divide(sF1_fnc,X2),divide(divide(X1,X0),X2))),sF1_fnc))),
% 109.72/14.47 inference(paramodulation,[status(thm)],[f8055,f797])).
% 109.72/14.47 fof(f8099,plain,(
% 109.72/14.47 multiply(divide(inverse(sF1_fnc),sF1_fnc),divide(sF0_fnc,sF0_fnc))=inverse(sF1_fnc)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8140,f2041])).
% 109.72/14.47 fof(f8100,plain,(
% 109.72/14.47 divide(inverse(sF1_fnc),sF1_fnc)=sF1_fnc),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8140,f238])).
% 109.72/14.47 fof(f8125,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),multiply(inverse(sF1_fnc),a2)))=inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8140,f6202])).
% 109.72/14.47 fof(f8126,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(inverse(sF1_fnc),a2),multiply(X0,a2)))=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8140,f6191])).
% 109.72/14.47 fof(f8140,plain,(
% 109.72/14.47 inverse(divide(sF0_fnc,sF0_fnc))=inverse(sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8,f8074])).
% 109.72/14.47 fof(f8144,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(sF1_fnc),divide(X0,X1))=divide(inverse(divide(divide(sF1_fnc,X2),divide(divide(X1,X0),X2))),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8140,f8085])).
% 109.72/14.47 fof(f8145,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(sF1_fnc),divide(X0,X1))=divide(inverse(divide(multiply(sF1_fnc,a2),multiply(divide(X1,X0),a2))),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1513,f8144])).
% 109.72/14.47 fof(f8146,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(sF1_fnc),divide(X0,X1))=divide(inverse(divide(sF0_fnc,multiply(divide(X1,X0),a2))),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f296,f8145])).
% 109.72/14.47 fof(f8147,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(sF1_fnc),divide(X0,X1))=divide(X1,X0))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f221,f8146])).
% 109.72/14.47 fof(f8163,plain,(
% 109.72/14.47 multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc))=inverse(sF1_fnc)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8100,f8099])).
% 109.72/14.47 fof(f8215,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(sF1_fnc,a2),multiply(X0,a2)))=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8240,f8126])).
% 109.72/14.47 fof(f8216,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),multiply(sF1_fnc,a2)))=inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8240,f8125])).
% 109.72/14.47 fof(f8229,plain,(
% 109.72/14.47 divide(sF1_fnc,sF1_fnc)=sF1_fnc),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8240,f8100])).
% 109.72/14.47 fof(f8236,plain,(
% 109.72/14.47 ![X0,X1]: (divide(sF1_fnc,divide(X0,X1))=divide(X1,X0))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8240,f8147])).
% 109.72/14.47 fof(f8240,plain,(
% 109.72/14.47 sF1_fnc=inverse(sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1746,f8163])).
% 109.72/14.47 fof(f8246,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF0_fnc,multiply(X0,a2)))=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f296,f8215])).
% 109.72/14.47 fof(f8247,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),sF0_fnc))=inverse(divide(divide(X0,sF1_fnc),sF1_fnc)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9,f8216])).
% 109.72/14.47 fof(f8299,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(inverse(divide(sF1_fnc,X0)),a2),multiply(X1,a2)))=inverse(divide(inverse(divide(sF0_fnc,multiply(X0,a2))),divide(X1,sF1_fnc))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8229,f6188])).
% 109.72/14.47 fof(f8308,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(inverse(divide(sF0_fnc,multiply(X1,a2))),a2)))=multiply(X0,divide(sF1_fnc,X1)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8229,f4236])).
% 109.72/14.47 fof(f8312,plain,(
% 109.72/14.47 ![X0,X1]: (divide(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,divide(X1,sF1_fnc))),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f5743])).
% 109.72/14.47 fof(f8319,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(X0,inverse(X1)),X2)),sF1_fnc)=inverse(divide(multiply(multiply(X0,X1),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f4751])).
% 109.72/14.47 fof(f8332,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF0_fnc,multiply(X0,a2)))=inverse(divide(sF1_fnc,X0)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f8246])).
% 109.72/14.47 fof(f8357,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (multiply(X0,divide(multiply(divide(X1,X2),a2),multiply(X3,a2)))=divide(X0,divide(inverse(divide(divide(X1,X2),X3)),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f6893])).
% 109.72/14.47 fof(f8380,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(multiply(divide(X0,X1),divide(multiply(divide(X2,X3),a2),sF0_fnc))),sF1_fnc)=inverse(divide(divide(divide(X0,X1),divide(X3,X2)),sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f1115])).
% 109.72/14.47 fof(f8381,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(X0,X1),X2)),sF1_fnc)=inverse(divide(multiply(divide(X0,X1),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8236,f744])).
% 109.72/14.47 fof(f8433,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(divide(inverse(divide(multiply(sF2_fnc,divide(multiply(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)),divide(X0,sF1_fnc)),a2),multiply(X1,a2))),X2)),sF1_fnc),X1)=X2)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8666,f6251])).
% 109.72/14.47 fof(f8551,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),multiply(X2,a2))),divide(multiply(X2,a2),multiply(multiply(sF1_fnc,divide(sF0_fnc,X3)),a2))),X4)),sF1_fnc)=inverse(divide(X3,multiply(X4,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8666,f7093])).
% 109.72/14.47 fof(f8553,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=divide(inverse(divide(multiply(multiply(divide(X2,X3),divide(multiply(divide(X3,X2),a2),multiply(X4,a2))),divide(multiply(X4,a2),multiply(X0,a2))),X1)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8666,f7118])).
% 109.72/14.47 fof(f8609,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,b2),X0)),sF1_fnc)=divide(inverse(divide(multiply(divide(X1,X2),divide(multiply(divide(X2,X1),b2),sF1_fnc)),X0)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8666,f1622])).
% 109.72/14.47 fof(f8666,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(X0,X1),X2)),sF1_fnc)=inverse(divide(multiply(multiply(X0,X1),X3),multiply(X2,X3))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f8319])).
% 109.72/14.47 fof(f8680,plain,(
% 109.72/14.47 ![X0]: (X0=inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f1106])).
% 109.72/14.47 fof(f8682,plain,(
% 109.72/14.47 ![X0]: (divide(inverse(divide(sF1_fnc,X0)),sF1_fnc)=X0)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f221])).
% 109.72/14.47 fof(f8689,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(divide(inverse(divide(X0,X1)),sF1_fnc),divide(sF0_fnc,sF0_fnc))=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f7762])).
% 109.72/14.47 fof(f8691,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(inverse(divide(sF1_fnc,X1)),a2)))=multiply(X0,divide(sF1_fnc,X1)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f8308])).
% 109.72/14.47 fof(f8693,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(inverse(divide(sF1_fnc,X0)),a2),multiply(X1,a2)))=inverse(divide(inverse(divide(sF1_fnc,X0)),divide(X1,sF1_fnc))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f8299])).
% 109.72/14.47 fof(f8720,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(X0,a2),multiply(inverse(divide(sF1_fnc,X1)),a2)))=inverse(divide(divide(X0,sF1_fnc),X1)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f6201])).
% 109.72/14.47 fof(f8722,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(sF1_fnc,multiply(X0,divide(sF0_fnc,sF0_fnc))))=inverse(divide(sF1_fnc,X0)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8332,f3082])).
% 109.72/14.47 fof(f8846,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(divide(divide(X0,X1),divide(inverse(divide(divide(X1,X0),multiply(sF1_fnc,divide(sF1_fnc,X2)))),sF1_fnc)),X3),X4))=inverse(multiply(X2,divide(sF0_fnc,multiply(divide(X4,divide(sF1_fnc,X3)),a2)))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8357,f8026])).
% 109.72/14.47 fof(f8893,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(divide(divide(divide(X0,X1),divide(inverse(divide(divide(X1,X0),divide(X2,X3))),sF1_fnc)),X4),X5))=inverse(divide(divide(divide(X3,X2),X4),X5)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8357,f7358])).
% 109.72/14.47 fof(f8984,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2)),sF1_fnc)=divide(inverse(divide(divide(inverse(X1),X0),X2)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8381,f4908])).
% 109.72/14.47 fof(f9000,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=inverse(divide(multiply(divide(inverse(divide(divide(X3,X2),X0)),sF1_fnc),a2),multiply(X1,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8381,f7734])).
% 109.72/14.47 fof(f9003,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),multiply(divide(X3,X4),divide(multiply(divide(X4,X3),b2),sF1_fnc)))=divide(inverse(divide(divide(X1,X0),X2)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f8381,f1577])).
% 109.72/14.47 fof(f9108,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(multiply(divide(divide(X0,X1),divide(inverse(divide(divide(X1,X0),X2)),sF1_fnc)),divide(multiply(X2,a2),multiply(multiply(sF1_fnc,divide(sF0_fnc,X3)),a2))),X4)),sF1_fnc)=inverse(divide(X3,multiply(X4,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8357,f8551])).
% 109.72/14.47 fof(f9112,plain,(
% 109.72/14.47 ![X0,X1]: (divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,X0))),X1)),sF1_fnc)=inverse(divide(X0,multiply(X1,a2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9116,f9108])).
% 109.72/14.47 fof(f9116,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc)=divide(inverse(divide(multiply(divide(divide(X2,X3),divide(inverse(divide(divide(X3,X2),X4)),sF1_fnc)),divide(multiply(X4,a2),multiply(X0,a2))),X1)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8357,f8553])).
% 109.72/14.47 fof(f9229,plain,(
% 109.72/14.47 ![X0]: (X0=inverse(divide(sF1_fnc,X0)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f8236,f8680])).
% 109.72/14.47 fof(f9241,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(X1,a2)))=divide(X0,X1))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f1131])).
% 109.72/14.47 fof(f9271,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (divide(inverse(multiply(divide(X0,X1),divide(multiply(divide(X2,X3),a2),sF0_fnc))),sF1_fnc)=inverse(divide(divide(X0,X1),divide(X3,X2))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f8380])).
% 109.72/14.47 fof(f9273,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),sF0_fnc))=inverse(divide(X0,sF1_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f8247])).
% 109.72/14.47 fof(f9296,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF1_fnc,b2),X0)),sF1_fnc)=divide(inverse(divide(multiply(divide(X1,X2),multiply(divide(X2,X1),b2)),X0)),sF1_fnc))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f8609])).
% 109.72/14.47 fof(f9444,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X0)))=inverse(divide(multiply(sF1_fnc,X2),X1)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f4636])).
% 109.72/14.47 fof(f9445,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(X0,X1),X2)),multiply(sF1_fnc,divide(sF0_fnc,multiply(X0,a2))))=inverse(divide(multiply(sF1_fnc,X1),X2)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f2862])).
% 109.72/14.47 fof(f9460,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF2_fnc,divide(multiply(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)),divide(X0,sF1_fnc)),a2),multiply(X1,a2))),X2)),X1)=X2)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f8433])).
% 109.72/14.47 fof(f9536,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),sF0_fnc)),a2),sF0_fnc))=sF1_fnc)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f126])).
% 109.72/14.47 fof(f9678,plain,(
% 109.72/14.47 ![X0,X1]: (divide(divide(X0,sF1_fnc),X1)=multiply(divide(X0,multiply(sF1_fnc,X1)),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f8312])).
% 109.72/14.47 fof(f9683,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,X1)=multiply(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,X1)))),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f5747])).
% 109.72/14.47 fof(f9688,plain,(
% 109.72/14.47 ![X0,X1,X2]: (multiply(X0,X1)=multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),multiply(sF1_fnc,X1)))),X2))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f3190])).
% 109.72/14.47 fof(f9690,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),divide(sF1_fnc,X1)))),X2))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9697,f3187])).
% 109.72/14.47 fof(f9697,plain,(
% 109.72/14.47 ![X0]: (divide(X0,sF1_fnc)=X0)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f8682])).
% 109.72/14.47 fof(f9705,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(inverse(divide(X0,X1)),divide(sF0_fnc,sF0_fnc))=inverse(divide(sF1_fnc,divide(X1,X0))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f8689])).
% 109.72/14.47 fof(f9706,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(inverse(divide(X0,X1)),divide(sF0_fnc,sF0_fnc))=divide(X1,X0))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f9705])).
% 109.72/14.47 fof(f9739,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,divide(sF0_fnc,multiply(X1,a2)))=multiply(X0,divide(sF1_fnc,X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f8691])).
% 109.72/14.47 fof(f9741,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(X0,a2),multiply(X1,a2)))=inverse(divide(inverse(divide(sF1_fnc,X0)),divide(X1,sF1_fnc))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f8693])).
% 109.72/14.47 fof(f9742,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(X0,a2),multiply(X1,a2)))=inverse(divide(X0,divide(X1,sF1_fnc))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f9741])).
% 109.72/14.47 fof(f9757,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(multiply(X0,a2),multiply(X1,a2)))=inverse(divide(X0,X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9742])).
% 109.72/14.47 fof(f9845,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(X0,inverse(divide(sF1_fnc,X1))))=inverse(divide(divide(X0,sF1_fnc),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9757,f8720])).
% 109.72/14.47 fof(f9846,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(multiply(X0,divide(sF1_fnc,X1)))=inverse(divide(divide(X0,sF1_fnc),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f9845])).
% 109.72/14.47 fof(f9847,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(multiply(X0,divide(sF1_fnc,X1)))=inverse(divide(X0,X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9846])).
% 109.72/14.47 fof(f9850,plain,(
% 109.72/14.47 ![X0]: (multiply(X0,divide(sF0_fnc,sF0_fnc))=inverse(divide(sF1_fnc,X0)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f8722])).
% 109.72/14.47 fof(f9856,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(X0,X1))=divide(X1,X0))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f9867,f9706])).
% 109.72/14.47 fof(f9867,plain,(
% 109.72/14.47 ![X0]: (multiply(X0,divide(sF0_fnc,sF0_fnc))=X0)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9229,f9850])).
% 109.72/14.47 fof(f10460,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),multiply(sF1_fnc,divide(sF1_fnc,X2))))),X3),X4))=inverse(multiply(X2,divide(sF0_fnc,multiply(divide(X4,divide(sF1_fnc,X3)),a2)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f8846])).
% 109.72/14.47 fof(f10461,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(X1,X0),multiply(sF1_fnc,divide(sF1_fnc,X2)))),X3),X4))=inverse(multiply(X2,divide(sF0_fnc,multiply(divide(X4,divide(sF1_fnc,X3)),a2)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f10460])).
% 109.72/14.47 fof(f10462,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(X1,X0),multiply(sF1_fnc,divide(sF1_fnc,X2)))),X3),X4))=inverse(multiply(X2,divide(sF1_fnc,divide(X4,divide(sF1_fnc,X3))))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9739,f10461])).
% 109.72/14.47 fof(f10463,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(X1,X0),multiply(sF1_fnc,divide(sF1_fnc,X2)))),X3),X4))=inverse(divide(X2,divide(X4,divide(sF1_fnc,X3)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9847,f10462])).
% 109.72/14.47 fof(f10655,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(divide(divide(divide(X0,X1),inverse(divide(divide(X1,X0),divide(X2,X3)))),X4),X5))=inverse(divide(divide(divide(X3,X2),X4),X5)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f8893])).
% 109.72/14.47 fof(f10656,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4,X5]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(X2,X3))),X4),X5))=inverse(divide(divide(divide(X3,X2),X4),X5)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f5,f10655])).
% 109.72/14.47 fof(f10949,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2))=divide(inverse(divide(divide(inverse(X1),X0),X2)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f8984])).
% 109.72/14.47 fof(f10951,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(divide(sF1_fnc,multiply(X0,X1)),X2))=inverse(divide(divide(inverse(X1),X0),X2)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f10949])).
% 109.72/14.47 fof(f10983,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(divide(X3,X2),X0))),X1)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f4908,f9000])).
% 109.72/14.47 fof(f10984,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(divide(X3,X2),X0))),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f10983])).
% 109.72/14.47 fof(f10985,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=inverse(divide(divide(inverse(divide(divide(X3,X2),X0)),sF1_fnc),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f10951,f10984])).
% 109.72/14.47 fof(f10988,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=inverse(divide(inverse(divide(divide(X3,X2),X0)),X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f10985])).
% 109.72/14.47 fof(f10994,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),multiply(divide(X3,X4),multiply(divide(X4,X3),b2)))=divide(inverse(divide(divide(X1,X0),X2)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9003])).
% 109.72/14.47 fof(f10995,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(divide(sF2_fnc,divide(X0,X1)),X2)),multiply(divide(X3,X4),multiply(divide(X4,X3),b2)))=inverse(divide(divide(X1,X0),X2)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f10994])).
% 109.72/14.47 fof(f11044,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,X0))),X1))=inverse(divide(X0,multiply(X1,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9112])).
% 109.72/14.47 fof(f11045,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),X1))=inverse(divide(X0,multiply(X1,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f10951,f11044])).
% 109.72/14.47 fof(f11047,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(inverse(divide(sF0_fnc,X0)),X1))=inverse(divide(X0,multiply(X1,a2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f11045])).
% 109.72/14.47 fof(f11165,plain,(
% 109.72/14.47 ![X0,X1,X2,X3]: (inverse(multiply(divide(X0,X1),divide(multiply(divide(X2,X3),a2),sF0_fnc)))=inverse(divide(divide(X0,X1),divide(X3,X2))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9271])).
% 109.72/14.47 fof(f11177,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),sF0_fnc))=inverse(X0))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9273])).
% 109.72/14.47 fof(f11219,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,b2),X0))=divide(inverse(divide(multiply(divide(X1,X2),multiply(divide(X2,X1),b2)),X0)),sF1_fnc))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9296])).
% 109.72/14.47 fof(f11221,plain,(
% 109.72/14.47 ![X0,X1,X2]: (inverse(divide(multiply(sF1_fnc,b2),X0))=inverse(divide(multiply(divide(X1,X2),multiply(divide(X2,X1),b2)),X0)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f11219])).
% 109.72/14.47 fof(f11404,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(X0,X1),X2)),divide(sF1_fnc,X0))=inverse(divide(multiply(sF1_fnc,X1),X2)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9241,f9445])).
% 109.72/14.47 fof(f11415,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(multiply(sF2_fnc,divide(multiply(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X0)),X0),a2),multiply(X1,a2))),X2)),X1)=X2)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9460])).
% 109.72/14.47 fof(f11519,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(multiply(divide(X0,X1),divide(multiply(divide(X1,X0),a2),sF0_fnc)))=sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f11177,f9536])).
% 109.72/14.47 fof(f11520,plain,(
% 109.72/14.47 ![X0,X1]: (inverse(divide(divide(X0,X1),divide(X0,X1)))=sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f11165,f11519])).
% 109.72/14.47 fof(f11521,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(multiply(X0,a2),multiply(X0,a2)))=sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f1513,f11520])).
% 109.72/14.47 fof(f11523,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(X0,X0))=sF1_fnc)),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f11524,f8071])).
% 109.72/14.47 fof(f11524,plain,(
% 109.72/14.47 ![X0]: (inverse(divide(X0,X0))=sF1_fnc)),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9757,f11521])).
% 109.72/14.47 fof(f11985,plain,(
% 109.72/14.47 ![X0,X1]: (divide(X0,X1)=multiply(divide(X0,multiply(sF1_fnc,X1)),divide(sF0_fnc,sF0_fnc)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9697,f9678])).
% 109.72/14.47 fof(f12015,plain,(
% 109.72/14.47 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(multiply(divide(X0,X1),divide(divide(X1,X0),divide(sF1_fnc,X2))),X3),X4))=inverse(divide(X2,divide(X4,divide(sF1_fnc,X3)))))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f12090,f10463])).
% 109.72/14.47 fof(f12055,plain,(
% 109.72/14.47 ![X0,X1,X2]: (divide(inverse(divide(X0,X1)),divide(multiply(sF1_fnc,X2),X0))=inverse(divide(multiply(sF1_fnc,X2),X1)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f12090,f9444])).
% 109.72/14.47 fof(f12090,plain,(
% 109.72/14.47 ![X0,X1]: (divide(X0,X1)=divide(X0,multiply(sF1_fnc,X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9867,f11985])).
% 109.72/14.47 fof(f12096,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,X1)=divide(X0,multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,X1)))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f9867,f9683])).
% 109.72/14.47 fof(f12097,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,X1)=divide(X0,divide(sF1_fnc,multiply(sF1_fnc,X1))))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f12090,f12096])).
% 109.72/14.47 fof(f12099,plain,(
% 109.72/14.47 ![X0,X1,X2]: (multiply(inverse(divide(multiply(X0,X1),X2)),X0)=inverse(divide(multiply(sF1_fnc,X1),X2)))),
% 109.72/14.47 inference(backward_demodulation,[status(thm)],[f12146,f11404])).
% 109.72/14.47 fof(f12146,plain,(
% 109.72/14.47 ![X0,X1]: (multiply(X0,X1)=divide(X0,divide(sF1_fnc,X1)))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f12090,f12097])).
% 109.72/14.47 fof(f12157,plain,(
% 109.72/14.47 ![X0,X1,X2]: (multiply(X0,X1)=multiply(divide(X0,divide(multiply(sF1_fnc,X2),multiply(sF1_fnc,X1))),X2))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f12090,f9688])).
% 109.72/14.47 fof(f12160,plain,(
% 109.72/14.47 ![X0,X1,X2]: (multiply(X0,X1)=multiply(divide(X0,divide(multiply(sF1_fnc,X2),X1)),X2))),
% 109.72/14.47 inference(forward_demodulation,[status(thm)],[f12090,f12157])).
% 109.72/14.49 fof(f12163,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,X1)=multiply(divide(X0,divide(multiply(sF1_fnc,X2),divide(sF1_fnc,X1))),X2))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12090,f9690])).
% 109.72/14.49 fof(f12184,plain,(
% 109.72/14.49 ![X0,X1]: (divide(X0,X1)=multiply(X0,divide(sF1_fnc,X1)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12160,f12163])).
% 109.72/14.49 fof(f12302,plain,(
% 109.72/14.49 ![X0,X1,X2,X3]: (inverse(divide(X0,divide(X1,divide(X2,X3))))=divide(X1,inverse(divide(divide(X3,X2),X0))))),
% 109.72/14.49 inference(backward_demodulation,[status(thm)],[f9856,f10988])).
% 109.72/14.49 fof(f12303,plain,(
% 109.72/14.49 ![X0,X1]: (divide(X0,inverse(divide(sF0_fnc,X1)))=inverse(divide(X1,multiply(X0,a2))))),
% 109.72/14.49 inference(backward_demodulation,[status(thm)],[f9856,f11047])).
% 109.72/14.49 fof(f12336,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,multiply(sF2_fnc,divide(multiply(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X1)),X1),a2),multiply(X2,a2)))),X2)=X0)),
% 109.72/14.49 inference(backward_demodulation,[status(thm)],[f9856,f11415])).
% 109.72/14.49 fof(f12354,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,multiply(sF1_fnc,b2))=inverse(divide(multiply(divide(X1,X2),multiply(divide(X2,X1),b2)),X0)))),
% 109.72/14.49 inference(backward_demodulation,[status(thm)],[f9856,f11221])).
% 109.72/14.49 fof(f12495,plain,(
% 109.72/14.49 ![X0,X1,X2,X3,X4]: (divide(divide(X0,divide(sF2_fnc,divide(X1,X2))),multiply(divide(X3,X4),multiply(divide(X4,X3),b2)))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.49 inference(backward_demodulation,[status(thm)],[f9856,f10995])).
% 109.72/14.49 fof(f12671,plain,(
% 109.72/14.49 ![X0]: (divide(X0,X0)=sF1_fnc)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f11523])).
% 109.72/14.49 fof(f13295,plain,(
% 109.72/14.49 ![X0,X1,X2]: (inverse(divide(divide(divide(X0,sF1_fnc),X1),X2))=inverse(divide(X0,divide(X2,divide(sF1_fnc,X1)))))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f10656,f12015])).
% 109.72/14.49 fof(f13296,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,divide(divide(X1,sF1_fnc),X2))=inverse(divide(X1,divide(X0,divide(sF1_fnc,X2)))))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f13295])).
% 109.72/14.49 fof(f13297,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=inverse(divide(X1,divide(X0,divide(sF1_fnc,X2)))))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9697,f13296])).
% 109.72/14.49 fof(f13298,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=divide(divide(X0,divide(sF1_fnc,X2)),X1))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f13297])).
% 109.72/14.49 fof(f13461,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=divide(multiply(X0,X2),X1))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12146,f13298])).
% 109.72/14.49 fof(f13638,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,X1),divide(multiply(sF1_fnc,X2),X1))=inverse(divide(multiply(sF1_fnc,X2),X0)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f12055])).
% 109.72/14.49 fof(f13639,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,X1),divide(sF1_fnc,divide(X1,X2)))=inverse(divide(multiply(sF1_fnc,X2),X0)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f13638])).
% 109.72/14.49 fof(f13640,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,X1),divide(X1,X2))=inverse(divide(multiply(sF1_fnc,X2),X0)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12146,f13639])).
% 109.72/14.49 fof(f13641,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,X1),divide(X1,X2))=divide(X0,multiply(sF1_fnc,X2)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f13640])).
% 109.72/14.49 fof(f13645,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,X1),divide(X1,X2))=divide(X0,X2))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12090,f13641])).
% 109.72/14.49 fof(f13728,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,multiply(X1,X2)),X1)=inverse(divide(multiply(sF1_fnc,X2),X0)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f12099])).
% 109.72/14.49 fof(f13729,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,multiply(X1,X2)),X1)=divide(X0,multiply(sF1_fnc,X2)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f13728])).
% 109.72/14.49 fof(f13730,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(divide(X0,multiply(X1,X2)),X1)=divide(X0,X2))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12090,f13729])).
% 109.72/14.49 fof(f14167,plain,(
% 109.72/14.49 ![X0,X1,X2,X3]: (divide(divide(X0,divide(X1,X2)),X3)=divide(X0,inverse(divide(divide(X2,X1),X3))))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f12302])).
% 109.72/14.49 fof(f14205,plain,(
% 109.72/14.49 ![X0,X1,X2,X3]: (divide(divide(X0,divide(X1,X2)),X3)=multiply(X0,divide(divide(X2,X1),X3)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f5,f14167])).
% 109.72/14.49 fof(f14206,plain,(
% 109.72/14.49 ![X0,X1]: (multiply(X0,divide(sF0_fnc,X1))=inverse(divide(X1,multiply(X0,a2))))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f5,f12303])).
% 109.72/14.49 fof(f14207,plain,(
% 109.72/14.49 ![X0,X1]: (multiply(X0,divide(sF0_fnc,X1))=divide(multiply(X0,a2),X1))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f9856,f14206])).
% 109.72/14.49 fof(f14209,plain,(
% 109.72/14.49 ![X0,X1]: (multiply(X0,divide(sF0_fnc,X1))=divide(X0,divide(X1,a2)))),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f14207])).
% 109.72/14.49 fof(f14327,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,multiply(sF2_fnc,divide(multiply(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X1)),X1),divide(multiply(X2,a2),a2)))),X2)=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f12336])).
% 109.72/14.49 fof(f14328,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,multiply(sF2_fnc,divide(multiply(sF1_fnc,divide(multiply(sF1_fnc,b2),X1)),divide(divide(multiply(X2,a2),a2),X1)))),X2)=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f14327])).
% 109.72/14.49 fof(f14329,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,multiply(sF2_fnc,divide(sF1_fnc,divide(divide(divide(multiply(X1,a2),a2),X2),divide(multiply(sF1_fnc,b2),X2))))),X1)=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f14328])).
% 109.72/14.49 fof(f14330,plain,(
% 109.72/14.49 ![X0,X1,X2]: (divide(divide(X0,divide(sF2_fnc,divide(divide(divide(multiply(X1,a2),a2),X2),divide(multiply(sF1_fnc,b2),X2)))),X1)=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12184,f14329])).
% 109.72/14.49 fof(f14331,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,divide(divide(divide(divide(divide(multiply(X1,a2),a2),X2),divide(multiply(sF1_fnc,b2),X2)),sF2_fnc),X1))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f14205,f14330])).
% 109.72/14.49 fof(f14332,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,divide(multiply(divide(divide(divide(multiply(X1,a2),a2),X2),divide(multiply(sF1_fnc,b2),X2)),b2),X1))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f11,f14331])).
% 109.72/14.49 fof(f14333,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,divide(divide(divide(divide(multiply(X1,a2),a2),X2),divide(multiply(sF1_fnc,b2),X2)),divide(X1,b2)))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f14332])).
% 109.72/14.49 fof(f14334,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,multiply(divide(divide(multiply(X1,a2),a2),X2),divide(divide(X2,multiply(sF1_fnc,b2)),divide(X1,b2))))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f14205,f14333])).
% 109.72/14.49 fof(f14335,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,multiply(divide(divide(X1,divide(a2,a2)),X2),divide(divide(X2,multiply(sF1_fnc,b2)),divide(X1,b2))))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f13461,f14334])).
% 109.72/14.49 fof(f14336,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X1,divide(divide(a2,a2),X2)),divide(divide(X2,multiply(sF1_fnc,b2)),divide(X1,b2))))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f14205,f14335])).
% 109.72/14.49 fof(f14337,plain,(
% 109.72/14.49 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X1,divide(sF1_fnc,X2)),divide(divide(X2,multiply(sF1_fnc,b2)),divide(X1,b2))))=X0)),
% 109.72/14.49 inference(forward_demodulation,[status(thm)],[f12671,f14336])).
% 109.72/14.51 fof(f14338,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,multiply(divide(X1,X2),divide(divide(X2,multiply(sF1_fnc,b2)),divide(X1,b2))))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12184,f14337])).
% 109.72/14.51 fof(f14339,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,multiply(divide(X1,X2),divide(divide(X2,b2),divide(X1,b2))))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12090,f14338])).
% 109.72/14.51 fof(f14340,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,multiply(divide(X1,X2),divide(multiply(X2,a2),multiply(X1,a2))))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f6917,f14339])).
% 109.72/14.51 fof(f14341,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,multiply(divide(X1,X2),divide(X2,divide(multiply(X1,a2),a2))))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f13461,f14340])).
% 109.72/14.51 fof(f14342,plain,(
% 109.72/14.51 ![X0,X1]: (multiply(X0,divide(X1,divide(multiply(X1,a2),a2)))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f13645,f14341])).
% 109.72/14.51 fof(f14343,plain,(
% 109.72/14.51 ![X0,X1]: (multiply(X0,multiply(X1,divide(sF0_fnc,multiply(X1,a2))))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f14209,f14342])).
% 109.72/14.51 fof(f14344,plain,(
% 109.72/14.51 ![X0,X1]: (multiply(X0,divide(X1,X1))=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f9241,f14343])).
% 109.72/14.51 fof(f14345,plain,(
% 109.72/14.51 ![X0]: (multiply(X0,sF1_fnc)=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12671,f14344])).
% 109.72/14.51 fof(f14470,plain,(
% 109.72/14.51 ![X0,X1,X2]: (divide(X0,b2)=inverse(divide(multiply(divide(X1,X2),multiply(divide(X2,X1),b2)),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12090,f12354])).
% 109.72/14.51 fof(f14472,plain,(
% 109.72/14.51 ![X0,X1,X2]: (divide(X0,b2)=divide(X0,multiply(divide(X1,X2),multiply(divide(X2,X1),b2))))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f9856,f14470])).
% 109.72/14.51 fof(f15186,plain,(
% 109.72/14.51 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(divide(divide(X1,X2),sF2_fnc),multiply(divide(X3,X4),multiply(divide(X4,X3),b2))))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f14205,f12495])).
% 109.72/14.51 fof(f15187,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(divide(divide(X1,X2),sF2_fnc),b2))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f14472,f15186])).
% 109.72/14.51 fof(f15188,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(multiply(divide(X1,X2),b2),b2))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f11,f15187])).
% 109.72/14.51 fof(f15189,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(divide(X1,X2),divide(b2,b2)))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f13461,f15188])).
% 109.72/14.51 fof(f15190,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(divide(X1,X2),sF1_fnc))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12671,f15189])).
% 109.72/14.51 fof(f15191,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=inverse(divide(divide(X2,X1),X0)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f9697,f15190])).
% 109.72/14.51 fof(f15268,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(multiply(X0,X1),X2))),
% 109.72/14.51 inference(backward_demodulation,[status(thm)],[f15278,f13461])).
% 109.72/14.51 fof(f15278,plain,(
% 109.72/14.51 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f9856,f15191])).
% 109.72/14.51 fof(f19271,plain,(
% 109.72/14.51 ![X0,X1]: (multiply(sF1_fnc,X0)=divide(multiply(X0,X1),X1))),
% 109.72/14.51 inference(paramodulation,[status(thm)],[f12671,f13730])).
% 109.72/14.51 fof(f19277,plain,(
% 109.72/14.51 ![X0,X1]: (multiply(sF1_fnc,X0)=multiply(X0,divide(X1,X1)))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f15268,f19271])).
% 109.72/14.51 fof(f19278,plain,(
% 109.72/14.51 ![X0]: (multiply(sF1_fnc,X0)=multiply(X0,sF1_fnc))),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f12671,f19277])).
% 109.72/14.51 fof(f19279,plain,(
% 109.72/14.51 sF0_fnc=a2),
% 109.72/14.51 inference(backward_demodulation,[status(thm)],[f19302,f9])).
% 109.72/14.51 fof(f19302,plain,(
% 109.72/14.51 ![X0]: (multiply(sF1_fnc,X0)=X0)),
% 109.72/14.51 inference(forward_demodulation,[status(thm)],[f14345,f19278])).
% 109.72/14.51 fof(f19309,plain,(
% 109.72/14.51 $false),
% 109.72/14.51 inference(forward_subsumption_resolution,[status(thm)],[f19279,f10])).
% 109.72/14.51 % SZS output end CNFRefutation for theBenchmark.p
% 47.02/14.68 % Elapsed time: 14.331891 seconds
% 47.02/14.68 % CPU time: 112.409073 seconds
% 47.02/14.68 % Total memory used: 628.090 MB
% 47.02/14.68 % Net memory used: 604.722 MB
%------------------------------------------------------------------------------