Drodi---4.1.1.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : GRP470-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n011.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:34:17 PM UTC 2026

% Result   : Unsatisfiable 23.40s 8.44s
% Output   : CNFRefutation 23.40s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [A,B,C,D] : divide(inverse(divide(A,divide(B,divide(C,D)))),divide(divide(D,C),A)) = B,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f2,axiom,
    ! [A,B] : multiply(A,B) = divide(A,inverse(B)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f3,negated_conjecture,
    multiply(multiply(inverse(b2),b2),a2) != a2,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).

fof(f4,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0)) = X1,
    inference(cnf_transformation,[status(thm)],[f1]) ).

fof(f5,plain,
    ! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
    inference(cnf_transformation,[status(thm)],[f2]) ).

fof(f6,plain,
    multiply(multiply(inverse(b2),b2),a2) != a2,
    inference(cnf_transformation,[status(thm)],[f3]) ).

fof(f7,definition,
    sF2_fnc = inverse(b2),
    introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).

fof(f8,definition,
    sF1_fnc = multiply(sF2_fnc,b2),
    introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).

fof(f9,definition,
    sF0_fnc = multiply(sF1_fnc,a2),
    introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).

fof(f10,plain,
    sF0_fnc != a2,
    inference(definition_folding,[],[f6,f9,f8,f7]) ).

fof(f11,plain,
    ! [X0] : multiply(X0,b2) = divide(X0,sF2_fnc),
    inference(paramodulation,[status(thm)],[f7,f5]) ).

fof(f12,plain,
    sF1_fnc = divide(sF2_fnc,sF2_fnc),
    inference(backward_demodulation,[status(thm)],[f11,f8]) ).

fof(f13,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,divide(X3,X4)))))) = divide(X4,X3),
    inference(paramodulation,[status(thm)],[f4,f4]) ).

fof(f14,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(divide(X0,X1)),divide(divide(X2,divide(X3,X4)),X0)) = inverse(divide(X2,divide(X1,divide(X4,X3)))),
    inference(paramodulation,[status(thm)],[f4,f4]) ).

fof(f16,plain,
    ! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(divide(sF2_fnc,sF2_fnc),X0)) = X1,
    inference(paramodulation,[status(thm)],[f12,f4]) ).

fof(f17,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,divide(X1,multiply(X2,X3)))),divide(divide(inverse(X3),X2),X0)) = X1,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f18,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0)) = X1,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f21,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,divide(X1,divide(inverse(X2),X3)))),divide(multiply(X3,X2),X0)) = X1,
    inference(paramodulation,[status(thm)],[f5,f4]) ).

fof(f22,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4))))) = divide(X4,X3),
    inference(forward_demodulation,[status(thm)],[f5,f13]) ).

fof(f24,plain,
    ! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(sF1_fnc,X0)) = X1,
    inference(forward_demodulation,[status(thm)],[f12,f16]) ).

fof(f27,plain,
    ! [X0] : divide(inverse(X0),divide(sF1_fnc,inverse(divide(sF1_fnc,divide(X0,sF1_fnc))))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f24,f24]) ).

fof(f28,plain,
    ! [X0,X1,X2] : divide(inverse(X0),divide(sF1_fnc,inverse(divide(sF1_fnc,divide(X0,divide(X1,X2)))))) = divide(X2,X1),
    inference(paramodulation,[status(thm)],[f4,f24]) ).

fof(f29,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(sF1_fnc,X0)) = X1,
    inference(paramodulation,[status(thm)],[f5,f24]) ).

fof(f30,plain,
    ! [X0,X1,X2] : divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,sF1_fnc))))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f24,f4]) ).

fof(f31,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(divide(X2,sF1_fnc),X0)) = inverse(divide(X2,divide(X1,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f24,f4]) ).

fof(f34,plain,
    ! [X0] : divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,sF1_fnc)))) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f5,f27]) ).

fof(f35,plain,
    ! [X0,X1,X2] : divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,divide(X1,X2))))) = divide(X2,X1),
    inference(forward_demodulation,[status(thm)],[f5,f28]) ).

fof(f36,plain,
    ! [X0,X1,X2] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF1_fnc)))) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f5,f30]) ).

fof(f39,plain,
    divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc)))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f7,f34]) ).

fof(f49,plain,
    ! [X0] : divide(inverse(divide(inverse(a2),divide(X0,sF1_fnc))),sF0_fnc) = X0,
    inference(paramodulation,[status(thm)],[f9,f29]) ).

fof(f70,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X0,divide(X3,X4))))) = divide(X4,X3),
    inference(paramodulation,[status(thm)],[f5,f22]) ).

fof(f80,plain,
    ! [X0,X1,X2,X3] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(divide(X2,X3),divide(divide(X3,X2),X1))) = divide(X0,sF1_fnc),
    inference(paramodulation,[status(thm)],[f24,f22]) ).

fof(f81,plain,
    ! [X0,X1,X2,X3,X4,X5] : divide(inverse(inverse(divide(X0,divide(X1,divide(X2,X3))))),multiply(divide(X4,X5),divide(divide(X5,X4),X1))) = divide(X0,divide(X3,X2)),
    inference(paramodulation,[status(thm)],[f4,f22]) ).

fof(f82,plain,
    ! [X0,X1,X2,X3] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = divide(sF0_fnc,inverse(divide(inverse(a2),divide(X3,sF1_fnc)))),
    inference(paramodulation,[status(thm)],[f49,f22]) ).

fof(f84,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = divide(divide(sF1_fnc,X4),inverse(divide(X4,divide(X3,sF1_fnc)))),
    inference(paramodulation,[status(thm)],[f24,f22]) ).

fof(f88,plain,
    ! [X0,X1,X2] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,sF1_fnc)))) = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))),sF2_fnc),
    inference(paramodulation,[status(thm)],[f39,f22]) ).

fof(f90,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,multiply(X3,X4))))) = divide(inverse(X4),X3),
    inference(paramodulation,[status(thm)],[f5,f22]) ).

fof(f107,plain,
    ! [X0,X1] : multiply(sF0_fnc,divide(inverse(a2),divide(divide(X0,X1),sF1_fnc))) = divide(X1,X0),
    inference(backward_demodulation,[status(thm)],[f109,f22]) ).

fof(f108,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))) = sF1_fnc,
    inference(backward_demodulation,[status(thm)],[f109,f36]) ).

fof(f109,plain,
    ! [X0,X1,X2,X3] : divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,X3)))) = multiply(sF0_fnc,divide(inverse(a2),divide(X3,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f5,f82]) ).

fof(f116,plain,
    ! [X0,X1] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = divide(divide(sF1_fnc,X1),inverse(divide(X1,divide(X0,sF1_fnc)))),
    inference(forward_demodulation,[status(thm)],[f109,f84]) ).

fof(f121,plain,
    ! [X0,X1] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f5,f116]) ).

fof(f142,plain,
    sF1_fnc = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))),sF2_fnc),
    inference(forward_demodulation,[status(thm)],[f36,f88]) ).

fof(f144,plain,
    ! [X0,X1] : multiply(sF0_fnc,divide(inverse(a2),divide(multiply(X0,X1),sF1_fnc))) = divide(inverse(X1),X0),
    inference(forward_demodulation,[status(thm)],[f109,f90]) ).

fof(f178,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(sF0_fnc,sF1_fnc))) = divide(inverse(a2),sF1_fnc),
    inference(paramodulation,[status(thm)],[f9,f144]) ).

fof(f190,plain,
    ! [X0,X1,X2,X3] : X0 = inverse(divide(X1,divide(divide(X0,divide(divide(X2,X3),X1)),divide(X3,X2)))),
    inference(paramodulation,[status(thm)],[f4,f14]) ).

fof(f200,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(multiply(X0,X1)),divide(divide(X2,divide(X3,X4)),X0)) = inverse(divide(X2,divide(inverse(X1),divide(X4,X3)))),
    inference(paramodulation,[status(thm)],[f5,f14]) ).

fof(f201,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,divide(X3,X4)),X0)) = inverse(divide(X2,divide(X1,divide(X4,X3)))),
    inference(paramodulation,[status(thm)],[f5,f14]) ).

fof(f206,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,divide(sF0_fnc,inverse(divide(inverse(a2),divide(X3,sF1_fnc))))))),
    inference(paramodulation,[status(thm)],[f49,f14]) ).

fof(f214,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(divide(X0,X1)),divide(divide(X2,multiply(X3,X4)),X0)) = inverse(divide(X2,divide(X1,divide(inverse(X4),X3)))),
    inference(paramodulation,[status(thm)],[f5,f14]) ).

fof(f233,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,multiply(sF0_fnc,divide(inverse(a2),divide(X3,sF1_fnc)))))),
    inference(forward_demodulation,[status(thm)],[f5,f206]) ).

fof(f257,plain,
    ! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF1_fnc,X1)),divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))))))),
    inference(paramodulation,[status(thm)],[f142,f190]) ).

fof(f282,plain,
    ! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,divide(sF1_fnc,X1)),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f39,f257]) ).

fof(f310,plain,
    ! [X0,X1] : X0 = inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(sF1_fnc,X1)),sF1_fnc))))),
    inference(paramodulation,[status(thm)],[f14,f282]) ).

fof(f312,plain,
    ! [X0,X1] : X0 = inverse(divide(inverse(X1),divide(divide(X0,multiply(sF1_fnc,X1)),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f5,f282]) ).

fof(f329,plain,
    ! [X0] : X0 = inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f9,f312]) ).

fof(f353,plain,
    ! [X0] : divide(X0,multiply(sF1_fnc,divide(sF1_fnc,divide(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)),sF1_fnc)))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f329,f34]) ).

fof(f370,plain,
    ! [X0] : inverse(divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc))) = inverse(inverse(X0)),
    inference(paramodulation,[status(thm)],[f24,f310]) ).

fof(f375,plain,
    ! [X0,X1] : X0 = inverse(inverse(divide(X0,divide(inverse(X1),divide(inverse(multiply(sF1_fnc,X1)),sF1_fnc))))),
    inference(paramodulation,[status(thm)],[f5,f310]) ).

fof(f509,plain,
    ! [X0,X1,X2,X3] : divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,divide(X0,divide(X1,X2))))) = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X3,divide(X2,X1)))),inverse(X3)),
    inference(paramodulation,[status(thm)],[f35,f35]) ).

fof(f540,plain,
    ! [X0,X1,X2] : divide(X0,X1) = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X2,divide(X0,X1)))),inverse(X2)),
    inference(forward_demodulation,[status(thm)],[f35,f509]) ).

fof(f541,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X2,divide(X0,X1)))),X2),
    inference(forward_demodulation,[status(thm)],[f5,f540]) ).

fof(f570,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(a2),divide(X0,sF1_fnc))),sF0_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),X1),
    inference(paramodulation,[status(thm)],[f49,f541]) ).

fof(f588,plain,
    ! [X0,X1] : X0 = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),X1),
    inference(forward_demodulation,[status(thm)],[f49,f570]) ).

fof(f602,plain,
    ! [X0] : X0 = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X0))),sF2_fnc),
    inference(paramodulation,[status(thm)],[f11,f588]) ).

fof(f611,plain,
    multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc),
    inference(paramodulation,[status(thm)],[f39,f588]) ).

fof(f612,plain,
    sF2_fnc = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc),
    inference(paramodulation,[status(thm)],[f12,f588]) ).

fof(f613,plain,
    ! [X0,X1] : inverse(X0) = multiply(multiply(sF1_fnc,divide(sF1_fnc,multiply(X1,X0))),X1),
    inference(paramodulation,[status(thm)],[f5,f588]) ).

fof(f630,plain,
    multiply(sF1_fnc,divide(sF1_fnc,divide(b2,sF1_fnc))) = sF2_fnc,
    inference(backward_demodulation,[status(thm)],[f612,f611]) ).

fof(f660,plain,
    ! [X0,X1,X2] : divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,sF1_fnc),X0)) = inverse(divide(X2,divide(X1,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f24,f18]) ).

fof(f751,plain,
    ! [X0] : inverse(X0) = divide(multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0))),sF2_fnc),
    inference(paramodulation,[status(thm)],[f5,f602]) ).

fof(f759,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X0)))),
    inference(paramodulation,[status(thm)],[f602,f107]) ).

fof(f773,plain,
    ! [X0,X1] : inverse(X0) = multiply(multiply(sF1_fnc,divide(sF1_fnc,inverse(X1))),multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))),
    inference(paramodulation,[status(thm)],[f613,f613]) ).

fof(f774,plain,
    inverse(sF2_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc)),multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f612,f613]) ).

fof(f781,plain,
    inverse(a2) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f9,f613]) ).

fof(f790,plain,
    ! [X0,X1] : inverse(X0) = multiply(multiply(sF1_fnc,multiply(sF1_fnc,X1)),multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))),
    inference(forward_demodulation,[status(thm)],[f5,f773]) ).

fof(f800,plain,
    ! [X0,X1] : divide(inverse(divide(X0,divide(X1,inverse(a2)))),divide(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),X0)) = X1,
    inference(paramodulation,[status(thm)],[f781,f17]) ).

fof(f801,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(inverse(a2),sF1_fnc))) = divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(paramodulation,[status(thm)],[f781,f144]) ).

fof(f804,plain,
    ! [X0] : inverse(divide(inverse(sF1_fnc),divide(divide(X0,inverse(a2)),divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f214,f800]) ).

fof(f805,plain,
    ! [X0] : inverse(divide(inverse(sF1_fnc),divide(multiply(X0,a2),divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f804]) ).

fof(f816,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(inverse(X0),sF1_fnc))) = divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0)))),
    inference(paramodulation,[status(thm)],[f751,f107]) ).

fof(f827,plain,
    divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,a2)))) = divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(backward_demodulation,[status(thm)],[f816,f801]) ).

fof(f1014,plain,
    ! [X0] : X0 = inverse(inverse(divide(X0,divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))))),
    inference(paramodulation,[status(thm)],[f9,f375]) ).

fof(f1481,plain,
    ! [X0] : divide(inverse(inverse(X0)),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))) = X0,
    inference(paramodulation,[status(thm)],[f370,f24]) ).

fof(f1504,plain,
    ! [X0] : divide(X0,divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))) = divide(X0,divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f1014,f1481]) ).

fof(f1510,plain,
    ! [X0] : divide(inverse(inverse(inverse(X0))),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))) = divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f370,f1481]) ).

fof(f1511,plain,
    ! [X0] : divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))) = divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f329,f1481]) ).

fof(f1519,plain,
    divide(inverse(sF2_fnc),divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc))) = b2,
    inference(paramodulation,[status(thm)],[f7,f1481]) ).

fof(f1520,plain,
    ! [X0] : divide(inverse(X0),multiply(divide(sF1_fnc,inverse(divide(sF1_fnc,sF1_fnc))),inverse(X0))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f1481,f18]) ).

fof(f1531,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(inverse(X2)),divide(X1,divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),sF1_fnc)))),
    inference(paramodulation,[status(thm)],[f1481,f14]) ).

fof(f1536,plain,
    ! [X0] : divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)) = multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f1481,f588]) ).

fof(f1541,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = divide(divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)),inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f1481,f107]) ).

fof(f1544,plain,
    ! [X0] : divide(inverse(inverse(X0)),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))) = X0,
    inference(backward_demodulation,[status(thm)],[f1504,f1481]) ).

fof(f1563,plain,
    ! [X0] : inverse(X0) = divide(divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(X0,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f1481,f1510]) ).

fof(f1565,plain,
    ! [X0] : divide(inverse(X0),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))) = divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f1504,f1511]) ).

fof(f1604,plain,
    divide(inverse(sF2_fnc),divide(inverse(a2),divide(inverse(sF0_fnc),sF1_fnc))) = b2,
    inference(forward_demodulation,[status(thm)],[f1504,f1519]) ).

fof(f1605,plain,
    divide(inverse(a2),divide(divide(sF2_fnc,sF0_fnc),sF1_fnc)) = b2,
    inference(forward_demodulation,[status(thm)],[f1565,f1604]) ).

fof(f1606,plain,
    ! [X0] : divide(inverse(X0),multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0))) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f5,f1520]) ).

fof(f1627,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = multiply(divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)),inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f5,f1541]) ).

fof(f1632,plain,
    ! [X0] : divide(inverse(a2),divide(divide(inverse(X0),sF0_fnc),sF1_fnc)) = X0,
    inference(forward_demodulation,[status(thm)],[f1565,f1544]) ).

fof(f1696,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(X0),X1)),multiply(divide(sF1_fnc,divide(inverse(X1),sF0_fnc)),X0)) = inverse(a2),
    inference(paramodulation,[status(thm)],[f1632,f18]) ).

fof(f1709,plain,
    ! [X0] : inverse(divide(sF1_fnc,divide(X0,divide(sF0_fnc,inverse(X0))))) = inverse(a2),
    inference(forward_demodulation,[status(thm)],[f201,f1696]) ).

fof(f1710,plain,
    ! [X0] : inverse(divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0)))) = inverse(a2),
    inference(forward_demodulation,[status(thm)],[f5,f1709]) ).

fof(f1738,plain,
    ! [X0] : divide(inverse(a2),divide(divide(inverse(a2),sF0_fnc),sF1_fnc)) = divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0))),
    inference(paramodulation,[status(thm)],[f1710,f1632]) ).

fof(f1750,plain,
    ! [X0] : a2 = divide(sF1_fnc,divide(X0,multiply(sF0_fnc,X0))),
    inference(forward_demodulation,[status(thm)],[f1632,f1738]) ).

fof(f1916,plain,
    a2 = divide(sF1_fnc,divide(b2,divide(sF0_fnc,sF2_fnc))),
    inference(paramodulation,[status(thm)],[f11,f1750]) ).

fof(f1920,plain,
    ! [X0,X1] : divide(inverse(divide(X0,a2)),divide(multiply(multiply(sF0_fnc,inverse(X1)),X1),X0)) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f1750,f21]) ).

fof(f1987,plain,
    ! [X0] : divide(X0,multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f329,f1606]) ).

fof(f2000,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),inverse(X0)),
    inference(paramodulation,[status(thm)],[f1606,f107]) ).

fof(f2004,plain,
    ! [X0] : divide(X0,multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f329,f1987]) ).

fof(f2019,plain,
    ! [X0] : sF1_fnc = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f108,f2000]) ).

fof(f2023,plain,
    ! [X0] : sF1_fnc = multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),X0),
    inference(forward_demodulation,[status(thm)],[f5,f2019]) ).

fof(f2049,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0),X0),
    inference(paramodulation,[status(thm)],[f2004,f107]) ).

fof(f2064,plain,
    ! [X0] : sF1_fnc = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0),X0),
    inference(forward_demodulation,[status(thm)],[f108,f2049]) ).

fof(f2119,plain,
    ! [X0,X1] : divide(inverse(sF1_fnc),multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),a2))) = divide(divide(sF0_fnc,sF2_fnc),b2),
    inference(paramodulation,[status(thm)],[f1916,f70]) ).

fof(f2120,plain,
    ! [X0,X1,X2] : divide(inverse(sF1_fnc),multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),a2))) = divide(multiply(sF0_fnc,X2),X2),
    inference(paramodulation,[status(thm)],[f1750,f70]) ).

fof(f2156,plain,
    ! [X0,X1,X2,X3,X4] : multiply(multiply(X0,X1),divide(divide(inverse(X1),X0),divide(X2,divide(X3,X4)))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X4,X3))),inverse(X2)),
    inference(paramodulation,[status(thm)],[f70,f588]) ).

fof(f2159,plain,
    ! [X0,X1,X2,X3,X4] : multiply(sF0_fnc,divide(inverse(a2),divide(divide(X0,X1),sF1_fnc))) = divide(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X1,X0)))),inverse(X4)),
    inference(paramodulation,[status(thm)],[f70,f107]) ).

fof(f2197,plain,
    ! [X0] : divide(divide(sF0_fnc,sF2_fnc),b2) = divide(multiply(sF0_fnc,X0),X0),
    inference(forward_demodulation,[status(thm)],[f2119,f2120]) ).

fof(f2258,plain,
    ! [X0,X1,X2,X3,X4] : divide(X0,X1) = divide(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X0,X1)))),inverse(X4)),
    inference(forward_demodulation,[status(thm)],[f107,f2159]) ).

fof(f2259,plain,
    ! [X0,X1,X2,X3,X4] : divide(X0,X1) = multiply(multiply(multiply(X2,X3),divide(divide(inverse(X3),X2),divide(X4,divide(X0,X1)))),X4),
    inference(forward_demodulation,[status(thm)],[f5,f2258]) ).

fof(f2260,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),inverse(X2)),X2),
    inference(forward_demodulation,[status(thm)],[f2156,f2259]) ).

fof(f2271,plain,
    sF1_fnc = divide(divide(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc),b2),
    inference(paramodulation,[status(thm)],[f11,f2064]) ).

fof(f2278,plain,
    divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f2064,f49]) ).

fof(f2295,plain,
    ! [X0] : X0 = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)),
    inference(paramodulation,[status(thm)],[f2064,f588]) ).

fof(f2319,plain,
    b2 = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
    inference(paramodulation,[status(thm)],[f2271,f588]) ).

fof(f2352,plain,
    ! [X0] : divide(divide(sF0_fnc,sF2_fnc),b2) = multiply(multiply(sF0_fnc,inverse(X0)),X0),
    inference(paramodulation,[status(thm)],[f5,f2197]) ).

fof(f2364,plain,
    ! [X0,X1] : divide(inverse(divide(X0,X1)),divide(divide(divide(sF0_fnc,sF2_fnc),b2),X0)) = inverse(divide(multiply(sF0_fnc,sF1_fnc),divide(X1,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f2197,f31]) ).

fof(f2385,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(divide(divide(sF0_fnc,sF2_fnc),b2),sF1_fnc))) = divide(X0,multiply(sF0_fnc,X0)),
    inference(paramodulation,[status(thm)],[f2197,f107]) ).

fof(f2388,plain,
    ! [X0] : divide(inverse(divide(X0,a2)),divide(divide(divide(sF0_fnc,sF2_fnc),b2),X0)) = sF1_fnc,
    inference(backward_demodulation,[status(thm)],[f2352,f1920]) ).

fof(f2394,plain,
    ! [X0] : divide(b2,divide(sF0_fnc,sF2_fnc)) = divide(X0,multiply(sF0_fnc,X0)),
    inference(forward_demodulation,[status(thm)],[f107,f2385]) ).

fof(f2397,plain,
    inverse(divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f2364,f2388]) ).

fof(f2401,plain,
    sF1_fnc = multiply(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f2397,f2023]) ).

fof(f2402,plain,
    divide(inverse(a2),divide(divide(sF1_fnc,sF0_fnc),sF1_fnc)) = divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f2397,f1632]) ).

fof(f2407,plain,
    ! [X0] : multiply(X0,divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))) = divide(X0,sF1_fnc),
    inference(paramodulation,[status(thm)],[f2397,f5]) ).

fof(f2408,plain,
    sF1_fnc = multiply(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f2278,f2401]) ).

fof(f2410,plain,
    sF1_fnc = divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f2407,f2408]) ).

fof(f2647,plain,
    ! [X0] : divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc))) = inverse(divide(X0,divide(sF1_fnc,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f2410,f31]) ).

fof(f2653,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))) = divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)),
    inference(paramodulation,[status(thm)],[f2410,f107]) ).

fof(f2662,plain,
    sF1_fnc = divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)),
    inference(forward_demodulation,[status(thm)],[f108,f2653]) ).

fof(f2672,plain,
    ! [X0] : divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc)) = inverse(divide(X0,divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f2662,f31]) ).

fof(f2684,plain,
    ! [X0] : divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc)) = inverse(divide(X0,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f2410,f2672]) ).

fof(f2698,plain,
    ! [X0,X1] : divide(X0,multiply(sF0_fnc,X0)) = divide(X1,multiply(sF0_fnc,X1)),
    inference(paramodulation,[status(thm)],[f2394,f2394]) ).

fof(f2936,plain,
    ! [X0,X1] : divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),a2))) = divide(multiply(sF0_fnc,sF1_fnc),sF1_fnc),
    inference(paramodulation,[status(thm)],[f2397,f80]) ).

fof(f2939,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(sF1_fnc)),multiply(divide(X0,X1),divide(divide(X1,X0),X2))) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(X2,sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f2064,f80]) ).

fof(f2943,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(X0)),multiply(divide(X1,X2),divide(divide(X2,X1),sF1_fnc))) = divide(inverse(divide(sF1_fnc,divide(X0,sF1_fnc))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f24,f80]) ).

fof(f2962,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,divide(b2,X2)))),X1))) = divide(X0,sF1_fnc),
    inference(paramodulation,[status(thm)],[f602,f80]) ).

fof(f3031,plain,
    ! [X0,X1] : divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),a2))) = divide(divide(sF0_fnc,sF2_fnc),b2),
    inference(forward_demodulation,[status(thm)],[f2197,f2936]) ).

fof(f3049,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(sF0_fnc,divide(inverse(a2),divide(X2,sF1_fnc))),X1))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f759,f2962]) ).

fof(f3163,plain,
    ! [X0] : divide(X0,multiply(sF0_fnc,X0)) = divide(divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)),divide(sF0_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f2407,f2698]) ).

fof(f3166,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,sF1_fnc),divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f2407,f2197]) ).

fof(f3188,plain,
    divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)) = inverse(divide(divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f2410,f2684]) ).

fof(f3204,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,inverse(divide(X0,sF1_fnc)))),inverse(sF1_fnc)),
    inference(paramodulation,[status(thm)],[f2684,f588]) ).

fof(f3210,plain,
    divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)) = inverse(sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f2410,f3188]) ).

fof(f3228,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = multiply(multiply(sF1_fnc,multiply(sF1_fnc,divide(X0,sF1_fnc))),inverse(sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f3204]) ).

fof(f3237,plain,
    divide(inverse(inverse(sF1_fnc)),multiply(sF1_fnc,sF1_fnc)) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f3210,f29]) ).

fof(f3242,plain,
    ! [X0] : divide(inverse(divide(inverse(X0),inverse(sF1_fnc))),multiply(divide(sF1_fnc,sF1_fnc),X0)) = inverse(sF1_fnc),
    inference(paramodulation,[status(thm)],[f3210,f18]) ).

fof(f3253,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(inverse(sF1_fnc),sF1_fnc))) = divide(divide(sF1_fnc,sF1_fnc),inverse(sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3210,f107]) ).

fof(f3260,plain,
    inverse(divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))) = inverse(sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f660,f3242]) ).

fof(f3272,plain,
    divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,sF1_fnc)))) = divide(divide(sF1_fnc,sF1_fnc),inverse(sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f816,f3253]) ).

fof(f3276,plain,
    divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,sF1_fnc)))) = multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f3272]) ).

fof(f3288,plain,
    multiply(sF1_fnc,sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(inverse(sF1_fnc))),
    inference(paramodulation,[status(thm)],[f3237,f588]) ).

fof(f3291,plain,
    multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))) = divide(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc))),
    inference(paramodulation,[status(thm)],[f3237,f107]) ).

fof(f3300,plain,
    ! [X0] : multiply(sF0_fnc,divide(inverse(a2),divide(X0,sF1_fnc))) = multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0)),
    inference(backward_demodulation,[status(thm)],[f3304,f1627]) ).

fof(f3304,plain,
    multiply(sF1_fnc,sF1_fnc) = divide(sF1_fnc,divide(inverse(divide(sF1_fnc,sF1_fnc)),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f1536,f3288]) ).

fof(f3310,plain,
    sF1_fnc = divide(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f108,f3291]) ).

fof(f3316,plain,
    sF1_fnc = multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f3310]) ).

fof(f3321,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF0_fnc)) = divide(inverse(a2),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f3300,f178]) ).

fof(f3322,plain,
    ! [X0,X1] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(multiply(X0,X1))) = divide(inverse(X1),X0),
    inference(backward_demodulation,[status(thm)],[f3300,f144]) ).

fof(f3323,plain,
    ! [X0,X1] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(divide(X0,X1))) = divide(X1,X0),
    inference(backward_demodulation,[status(thm)],[f3300,f107]) ).

fof(f3329,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(X0))) = divide(sF2_fnc,multiply(sF1_fnc,divide(sF1_fnc,multiply(b2,X0)))),
    inference(backward_demodulation,[status(thm)],[f3300,f816]) ).

fof(f3331,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(multiply(sF1_fnc,sF1_fnc),inverse(X2)),X1))) = divide(X0,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f3300,f3049]) ).

fof(f3348,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,multiply(multiply(sF1_fnc,sF1_fnc),inverse(X3))))),
    inference(backward_demodulation,[status(thm)],[f3300,f233]) ).

fof(f3350,plain,
    ! [X0,X1] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0)) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f3300,f121]) ).

fof(f3388,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(sF1_fnc))) = multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f3329,f3276]) ).

fof(f3392,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(a2))) = divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(backward_demodulation,[status(thm)],[f3329,f827]) ).

fof(f3455,plain,
    ! [X0,X1] : inverse(inverse(divide(X0,X1))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),multiply(sF1_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3323,f613]) ).

fof(f3496,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc)) = divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc),
    inference(paramodulation,[status(thm)],[f3260,f3323]) ).

fof(f3501,plain,
    divide(inverse(a2),divide(divide(inverse(sF1_fnc),sF0_fnc),sF1_fnc)) = divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3260,f1632]) ).

fof(f3508,plain,
    sF1_fnc = divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3316,f3496]) ).

fof(f3513,plain,
    sF1_fnc = divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f1632,f3501]) ).

fof(f3532,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc),X0)) = X1,
    inference(paramodulation,[status(thm)],[f3513,f18]) ).

fof(f3533,plain,
    divide(inverse(sF1_fnc),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f3513,f588]) ).

fof(f3549,plain,
    ! [X0] : inverse(divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc))) = X0,
    inference(forward_demodulation,[status(thm)],[f660,f3532]) ).

fof(f3550,plain,
    divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc) = divide(inverse(sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f3533,f2278]) ).

fof(f3560,plain,
    ! [X0] : divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc))) = inverse(divide(X0,divide(sF1_fnc,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f3550,f2647]) ).

fof(f3566,plain,
    divide(inverse(sF1_fnc),sF1_fnc) = inverse(divide(inverse(sF1_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3508,f2684]) ).

fof(f3567,plain,
    ! [X0] : divide(inverse(divide(sF1_fnc,X0)),sF1_fnc) = inverse(divide(inverse(sF1_fnc),divide(X0,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f3508,f31]) ).

fof(f3581,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(X0),divide(X1,sF1_fnc))),multiply(divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),X0)) = X1,
    inference(paramodulation,[status(thm)],[f3508,f18]) ).

fof(f3597,plain,
    ! [X0] : inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,inverse(sF1_fnc))))) = X0,
    inference(forward_demodulation,[status(thm)],[f201,f3581]) ).

fof(f3599,plain,
    ! [X0] : inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),multiply(sF1_fnc,sF1_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f3597]) ).

fof(f3604,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)) = divide(sF1_fnc,inverse(sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3566,f3323]) ).

fof(f3607,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = multiply(multiply(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3566,f2352]) ).

fof(f3614,plain,
    ! [X0] : multiply(X0,divide(inverse(sF1_fnc),sF1_fnc)) = divide(X0,divide(inverse(sF1_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3566,f5]) ).

fof(f3615,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)) = multiply(sF1_fnc,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f3604]) ).

fof(f3620,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = multiply(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f3614,f3607]) ).

fof(f3621,plain,
    divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)) = multiply(sF1_fnc,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f3614,f3615]) ).

fof(f3627,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(inverse(sF1_fnc),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f3614,f3620]) ).

fof(f3639,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),X0) = divide(divide(divide(X0,sF1_fnc),multiply(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f3599,f3323]) ).

fof(f3679,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,sF1_fnc))),multiply(divide(X1,X2),divide(divide(X2,X1),sF1_fnc))) = divide(X0,divide(sF1_fnc,inverse(sF1_fnc))),
    inference(paramodulation,[status(thm)],[f3513,f81]) ).

fof(f3836,plain,
    ! [X0] : divide(inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),sF1_fnc))),sF1_fnc) = divide(X0,divide(sF1_fnc,inverse(sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f2943,f3679]) ).

fof(f3837,plain,
    ! [X0] : divide(inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),sF1_fnc))),sF1_fnc) = divide(X0,multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f3836]) ).

fof(f4054,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(divide(inverse(a2),sF1_fnc))) = divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f3321,f3322]) ).

fof(f4076,plain,
    divide(sF1_fnc,inverse(a2)) = divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f3323,f4054]) ).

fof(f4077,plain,
    multiply(sF1_fnc,a2) = divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f4076]) ).

fof(f4079,plain,
    sF0_fnc = divide(inverse(inverse(sF0_fnc)),multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f9,f4077]) ).

fof(f4095,plain,
    ! [X0] : divide(inverse(divide(X0,sF0_fnc)),divide(divide(inverse(sF1_fnc),sF1_fnc),X0)) = inverse(inverse(sF0_fnc)),
    inference(paramodulation,[status(thm)],[f4079,f17]) ).

fof(f4105,plain,
    inverse(divide(inverse(sF1_fnc),divide(sF0_fnc,sF1_fnc))) = inverse(inverse(sF0_fnc)),
    inference(forward_demodulation,[status(thm)],[f31,f4095]) ).

fof(f4107,plain,
    ! [X0] : inverse(divide(inverse(sF1_fnc),divide(multiply(X0,a2),inverse(inverse(sF0_fnc))))) = X0,
    inference(backward_demodulation,[status(thm)],[f4108,f805]) ).

fof(f4108,plain,
    divide(inverse(divide(sF1_fnc,sF0_fnc)),sF1_fnc) = inverse(inverse(sF0_fnc)),
    inference(forward_demodulation,[status(thm)],[f3567,f4105]) ).

fof(f4119,plain,
    ! [X0] : inverse(divide(inverse(sF1_fnc),multiply(multiply(X0,a2),inverse(sF0_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f4107]) ).

fof(f4163,plain,
    ! [X0] : inverse(divide(inverse(sF1_fnc),multiply(X0,inverse(sF0_fnc)))) = multiply(sF1_fnc,divide(sF1_fnc,divide(a2,X0))),
    inference(paramodulation,[status(thm)],[f588,f4119]) ).

fof(f4164,plain,
    inverse(divide(inverse(sF1_fnc),multiply(sF0_fnc,inverse(sF0_fnc)))) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f9,f4119]) ).

fof(f4165,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),X0) = divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),inverse(sF1_fnc)),
    inference(paramodulation,[status(thm)],[f4119,f3323]) ).

fof(f4177,plain,
    ! [X0] : multiply(sF1_fnc,divide(sF1_fnc,divide(a2,multiply(X0,a2)))) = X0,
    inference(backward_demodulation,[status(thm)],[f4163,f4119]) ).

fof(f4181,plain,
    multiply(sF1_fnc,divide(sF1_fnc,divide(a2,sF0_fnc))) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f4163,f4164]) ).

fof(f4182,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),X0) = multiply(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f4165]) ).

fof(f4202,plain,
    inverse(divide(sF1_fnc,divide(a2,sF0_fnc))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4181,f613]) ).

fof(f4203,plain,
    ! [X0,X1] : divide(inverse(divide(X0,divide(X1,sF1_fnc))),divide(divide(inverse(divide(sF1_fnc,divide(a2,sF0_fnc))),sF1_fnc),X0)) = X1,
    inference(paramodulation,[status(thm)],[f4181,f17]) ).

fof(f4208,plain,
    inverse(divide(sF1_fnc,divide(a2,sF0_fnc))) = divide(inverse(sF1_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3533,f4202]) ).

fof(f4209,plain,
    ! [X0] : inverse(divide(inverse(divide(sF1_fnc,divide(a2,sF0_fnc))),divide(divide(X0,sF1_fnc),sF1_fnc))) = X0,
    inference(forward_demodulation,[status(thm)],[f31,f4203]) ).

fof(f4210,plain,
    ! [X0] : inverse(inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f31,f4209]) ).

fof(f4217,plain,
    ! [X0] : divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)) = inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f4210,f1632]) ).

fof(f4522,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0)) = divide(inverse(divide(sF1_fnc,divide(a2,multiply(X0,a2)))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4177,f3322]) ).

fof(f4524,plain,
    ! [X0] : inverse(divide(sF1_fnc,divide(a2,multiply(X0,a2)))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4177,f613]) ).

fof(f4531,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),inverse(X0)) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4524,f4522]) ).

fof(f4535,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)) = divide(divide(a2,sF0_fnc),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4208,f3323]) ).

fof(f4536,plain,
    ! [X0] : divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc)) = inverse(divide(X0,divide(divide(a2,sF0_fnc),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f4208,f31]) ).

fof(f4546,plain,
    divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)) = divide(divide(a2,sF0_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3614,f4535]) ).

fof(f4547,plain,
    ! [X0] : divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)) = inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f4550,f4217]) ).

fof(f4550,plain,
    multiply(sF1_fnc,sF1_fnc) = divide(divide(a2,sF0_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3621,f4546]) ).

fof(f4551,plain,
    ! [X0] : inverse(divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc))) = X0,
    inference(backward_demodulation,[status(thm)],[f4552,f3549]) ).

fof(f4552,plain,
    ! [X0] : divide(divide(inverse(sF1_fnc),sF1_fnc),divide(divide(X0,sF1_fnc),sF1_fnc)) = divide(inverse(a2),divide(divide(X0,sF0_fnc),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f4217,f4536]) ).

fof(f4568,plain,
    ! [X0] : inverse(divide(inverse(X0),multiply(sF1_fnc,sF1_fnc))) = X0,
    inference(backward_demodulation,[status(thm)],[f4547,f1632]) ).

fof(f4569,plain,
    inverse(divide(sF2_fnc,multiply(sF1_fnc,sF1_fnc))) = b2,
    inference(backward_demodulation,[status(thm)],[f4547,f1605]) ).

fof(f4572,plain,
    inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))) = divide(multiply(sF0_fnc,sF1_fnc),divide(a2,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4547,f2402]) ).

fof(f4593,plain,
    ! [X0] : divide(X0,multiply(sF1_fnc,divide(sF1_fnc,divide(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc))),sF1_fnc)))) = sF1_fnc,
    inference(backward_demodulation,[status(thm)],[f4547,f353]) ).

fof(f4595,plain,
    ! [X0] : inverse(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc)))) = X0,
    inference(forward_demodulation,[status(thm)],[f4547,f4551]) ).

fof(f4601,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,sF1_fnc),inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f4572,f3166]) ).

fof(f4603,plain,
    ! [X0] : divide(X0,multiply(sF0_fnc,X0)) = divide(inverse(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),divide(sF0_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4572,f3163]) ).

fof(f4609,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = multiply(divide(sF0_fnc,sF1_fnc),divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f5,f4601]) ).

fof(f4620,plain,
    ! [X0] : multiply(X0,divide(sF2_fnc,multiply(sF1_fnc,sF1_fnc))) = divide(X0,b2),
    inference(paramodulation,[status(thm)],[f4569,f5]) ).

fof(f4635,plain,
    ! [X0] : inverse(inverse(X0)) = inverse(divide(inverse(sF1_fnc),divide(X0,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f29,f4595]) ).

fof(f4643,plain,
    ! [X0] : divide(inverse(divide(sF1_fnc,X0)),sF1_fnc) = inverse(inverse(X0)),
    inference(backward_demodulation,[status(thm)],[f4635,f3567]) ).

fof(f4658,plain,
    ! [X0] : inverse(inverse(divide(divide(X0,sF1_fnc),sF1_fnc))) = divide(X0,multiply(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4643,f3837]) ).

fof(f4673,plain,
    multiply(sF1_fnc,sF1_fnc) = divide(sF1_fnc,inverse(inverse(sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f4643,f3304]) ).

fof(f4674,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(inverse(X2)),divide(X1,divide(inverse(inverse(sF1_fnc)),sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f4643,f1531]) ).

fof(f4675,plain,
    ! [X0] : inverse(X0) = divide(inverse(inverse(sF1_fnc)),divide(X0,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4643,f1563]) ).

fof(f4688,plain,
    multiply(sF1_fnc,sF1_fnc) = multiply(sF1_fnc,inverse(sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f4673]) ).

fof(f4694,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(multiply(sF1_fnc,sF1_fnc))) = divide(inverse(inverse(sF1_fnc)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4688,f3322]) ).

fof(f4696,plain,
    inverse(inverse(sF1_fnc)) = multiply(multiply(sF1_fnc,divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4688,f613]) ).

fof(f4703,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(inverse(X2)),divide(X1,divide(inverse(sF1_fnc),sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f4704,f4674]) ).

fof(f4704,plain,
    divide(inverse(sF1_fnc),sF1_fnc) = divide(inverse(inverse(sF1_fnc)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3322,f4694]) ).

fof(f4707,plain,
    ! [X0] : inverse(X0) = divide(inverse(sF1_fnc),divide(X0,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4714,f4675]) ).

fof(f4710,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc)) = multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4714,f3388]) ).

fof(f4713,plain,
    ! [X0,X1,X2] : divide(inverse(sF1_fnc),multiply(divide(X0,X1),divide(divide(X1,X0),X2))) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(X2,sF1_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4714,f2939]) ).

fof(f4714,plain,
    inverse(inverse(sF1_fnc)) = inverse(sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f613,f4696]) ).

fof(f4740,plain,
    sF1_fnc = multiply(divide(sF1_fnc,sF1_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f3316,f4710]) ).

fof(f4741,plain,
    divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(a2,sF1_fnc)),sF1_fnc) = divide(divide(sF0_fnc,sF2_fnc),b2),
    inference(backward_demodulation,[status(thm)],[f4713,f3031]) ).

fof(f4751,plain,
    ! [X0] : multiply(X0,inverse(sF1_fnc)) = divide(X0,inverse(sF1_fnc)),
    inference(paramodulation,[status(thm)],[f4714,f5]) ).

fof(f4754,plain,
    sF1_fnc = multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4768,f3316]) ).

fof(f4761,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = multiply(multiply(sF1_fnc,multiply(sF1_fnc,divide(X0,sF1_fnc))),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4768,f3228]) ).

fof(f4768,plain,
    ! [X0] : multiply(X0,inverse(sF1_fnc)) = multiply(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f4751]) ).

fof(f4922,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc)) = divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f4754,f3322]) ).

fof(f4926,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc) = divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f4768,f4922]) ).

fof(f4927,plain,
    sF1_fnc = divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f4754,f4926]) ).

fof(f4932,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(sF1_fnc)) = divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f4740,f3322]) ).

fof(f4936,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc) = divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f4768,f4932]) ).

fof(f4937,plain,
    sF1_fnc = divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f4754,f4936]) ).

fof(f4941,plain,
    sF1_fnc = divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5017,f3513]) ).

fof(f4946,plain,
    sF1_fnc = divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5017,f4927]) ).

fof(f4963,plain,
    ! [X0] : inverse(X0) = divide(sF1_fnc,divide(X0,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5017,f4707]) ).

fof(f4964,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(inverse(X2)),divide(X1,divide(sF1_fnc,sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f5017,f4703]) ).

fof(f4978,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,divide(inverse(sF1_fnc),sF1_fnc)),divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5017,f3627]) ).

fof(f4979,plain,
    ! [X0] : multiply(X0,divide(inverse(sF1_fnc),sF1_fnc)) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5017,f3614]) ).

fof(f4985,plain,
    ! [X0] : divide(inverse(sF1_fnc),divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc))) = inverse(divide(X0,divide(sF1_fnc,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f5017,f3560]) ).

fof(f4988,plain,
    divide(sF1_fnc,sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5017,f3533]) ).

fof(f4991,plain,
    multiply(multiply(sF1_fnc,sF1_fnc),inverse(inverse(a2))) = divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(backward_demodulation,[status(thm)],[f5017,f3392]) ).

fof(f5017,plain,
    sF1_fnc = inverse(sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f4707,f4937]) ).

fof(f5027,plain,
    ! [X0] : divide(X0,multiply(sF0_fnc,X0)) = divide(inverse(sF1_fnc),divide(sF0_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f4946,f4603]) ).

fof(f5029,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = multiply(divide(sF0_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f4946,f4609]) ).

fof(f5033,plain,
    multiply(sF1_fnc,inverse(b2)) = sF2_fnc,
    inference(backward_demodulation,[status(thm)],[f4963,f630]) ).

fof(f5035,plain,
    ! [X0] : divide(X0,multiply(sF1_fnc,inverse(inverse(divide(X0,multiply(sF1_fnc,sF1_fnc)))))) = sF1_fnc,
    inference(backward_demodulation,[status(thm)],[f4963,f4593]) ).

fof(f5048,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5017,f4978]) ).

fof(f5052,plain,
    ! [X0] : sF1_fnc = multiply(multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),inverse(X0)),X0),
    inference(backward_demodulation,[status(thm)],[f5098,f2023]) ).

fof(f5063,plain,
    divide(multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(a2,sF1_fnc)),sF1_fnc) = divide(divide(sF0_fnc,sF2_fnc),b2),
    inference(backward_demodulation,[status(thm)],[f5098,f4741]) ).

fof(f5080,plain,
    b2 = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
    inference(backward_demodulation,[status(thm)],[f5098,f2319]) ).

fof(f5083,plain,
    ! [X0] : X0 = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)),
    inference(backward_demodulation,[status(thm)],[f5098,f2295]) ).

fof(f5097,plain,
    inverse(sF2_fnc) = multiply(multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc)),divide(sF1_fnc,divide(sF1_fnc,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f5098,f774]) ).

fof(f5098,plain,
    ! [X0] : multiply(X0,divide(sF1_fnc,sF1_fnc)) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5017,f4979]) ).

fof(f5100,plain,
    ! [X0] : divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc))) = inverse(divide(X0,divide(sF1_fnc,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f5017,f4985]) ).

fof(f5102,plain,
    divide(sF1_fnc,sF1_fnc) = multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5098,f4988]) ).

fof(f5108,plain,
    ! [X0,X1] : multiply(divide(sF1_fnc,sF1_fnc),inverse(divide(X0,X1))) = divide(X1,X0),
    inference(backward_demodulation,[status(thm)],[f5224,f3323]) ).

fof(f5123,plain,
    ! [X0] : inverse(inverse(divide(divide(X0,sF1_fnc),sF1_fnc))) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5224,f4658]) ).

fof(f5124,plain,
    ! [X0] : multiply(X0,divide(sF2_fnc,divide(sF1_fnc,sF1_fnc))) = divide(X0,b2),
    inference(backward_demodulation,[status(thm)],[f5224,f4620]) ).

fof(f5144,plain,
    ! [X0] : inverse(divide(inverse(X0),divide(sF1_fnc,sF1_fnc))) = X0,
    inference(backward_demodulation,[status(thm)],[f5224,f4568]) ).

fof(f5148,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),inverse(X0)) = divide(multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5224,f4531]) ).

fof(f5153,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),X0) = multiply(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5224,f4182]) ).

fof(f5165,plain,
    ! [X0] : multiply(multiply(sF1_fnc,sF1_fnc),X0) = divide(divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5224,f3639]) ).

fof(f5168,plain,
    ! [X0,X1] : inverse(inverse(divide(X0,X1))) = multiply(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5224,f3455]) ).

fof(f5196,plain,
    ! [X0,X1] : multiply(divide(sF1_fnc,sF1_fnc),inverse(X0)) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f5224,f3350]) ).

fof(f5198,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,multiply(divide(sF1_fnc,sF1_fnc),inverse(X3))))),
    inference(backward_demodulation,[status(thm)],[f5224,f3348]) ).

fof(f5214,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(multiply(divide(sF1_fnc,sF1_fnc),inverse(X2)),X1))) = divide(X0,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5224,f3331]) ).

fof(f5224,plain,
    divide(sF1_fnc,sF1_fnc) = multiply(sF1_fnc,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f4941,f5102]) ).

fof(f5225,plain,
    multiply(divide(sF1_fnc,sF1_fnc),inverse(inverse(a2))) = divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(forward_demodulation,[status(thm)],[f5224,f4991]) ).

fof(f5275,plain,
    a2 = divide(sF1_fnc,inverse(sF0_fnc)),
    inference(backward_demodulation,[status(thm)],[f5312,f1750]) ).

fof(f5312,plain,
    ! [X0] : divide(X0,multiply(sF0_fnc,X0)) = inverse(sF0_fnc),
    inference(forward_demodulation,[status(thm)],[f4707,f5027]) ).

fof(f5336,plain,
    multiply(sF1_fnc,sF2_fnc) = sF2_fnc,
    inference(forward_demodulation,[status(thm)],[f7,f5033]) ).

fof(f5337,plain,
    ! [X0] : divide(X0,multiply(sF1_fnc,X0)) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f4595,f5035]) ).

fof(f5349,plain,
    ! [X0] : sF1_fnc = multiply(multiply(sF1_fnc,inverse(X0)),X0),
    inference(forward_demodulation,[status(thm)],[f4941,f5052]) ).

fof(f5366,plain,
    divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc) = divide(divide(sF0_fnc,sF2_fnc),b2),
    inference(forward_demodulation,[status(thm)],[f4941,f5063]) ).

fof(f5397,plain,
    b2 = multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
    inference(forward_demodulation,[status(thm)],[f5098,f5080]) ).

fof(f5398,plain,
    b2 = multiply(sF1_fnc,divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF2_fnc)),
    inference(forward_demodulation,[status(thm)],[f4941,f5397]) ).

fof(f5400,plain,
    b2 = multiply(sF1_fnc,divide(sF1_fnc,sF2_fnc)),
    inference(forward_demodulation,[status(thm)],[f4941,f5398]) ).

fof(f5403,plain,
    ! [X0] : X0 = multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)),
    inference(forward_demodulation,[status(thm)],[f5098,f5083]) ).

fof(f5404,plain,
    ! [X0] : X0 = multiply(sF1_fnc,multiply(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)),
    inference(forward_demodulation,[status(thm)],[f4941,f5403]) ).

fof(f5406,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = multiply(divide(X0,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5412,f4761]) ).

fof(f5411,plain,
    ! [X0,X1] : inverse(X0) = multiply(X1,multiply(sF1_fnc,divide(sF1_fnc,multiply(X0,X1)))),
    inference(backward_demodulation,[status(thm)],[f5412,f790]) ).

fof(f5412,plain,
    ! [X0] : X0 = multiply(sF1_fnc,multiply(sF1_fnc,X0)),
    inference(forward_demodulation,[status(thm)],[f4941,f5404]) ).

fof(f5427,plain,
    inverse(sF2_fnc) = multiply(b2,divide(sF1_fnc,divide(sF1_fnc,sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f5400,f5097]) ).

fof(f5428,plain,
    inverse(sF2_fnc) = multiply(b2,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f4941,f5427]) ).

fof(f5444,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),X0) = divide(divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5224,f5165]) ).

fof(f5445,plain,
    ! [X0,X1] : inverse(inverse(divide(X0,X1))) = divide(multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5098,f5168]) ).

fof(f5461,plain,
    a2 = multiply(sF1_fnc,sF0_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f5275]) ).

fof(f5484,plain,
    divide(divide(sF0_fnc,sF2_fnc),b2) = divide(divide(sF0_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5406,f5029]) ).

fof(f5518,plain,
    divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc) = divide(divide(sF0_fnc,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5484,f5366]) ).

fof(f5523,plain,
    divide(divide(sF0_fnc,sF1_fnc),sF1_fnc) = divide(divide(sF0_fnc,divide(sF1_fnc,sF1_fnc)),divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f5484,f5048]) ).

fof(f5591,plain,
    ! [X0] : multiply(X0,sF1_fnc) = divide(X0,sF1_fnc),
    inference(paramodulation,[status(thm)],[f5017,f5]) ).

fof(f5597,plain,
    inverse(sF2_fnc) = divide(b2,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5591,f5428]) ).

fof(f5599,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),X0) = divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5591,f5153]) ).

fof(f5605,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),inverse(X0)) = divide(divide(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5591,f5148]) ).

fof(f5662,plain,
    ! [X0] : inverse(multiply(sF1_fnc,X0)) = multiply(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),
    inference(paramodulation,[status(thm)],[f5412,f613]) ).

fof(f5669,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),inverse(X0)) = divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5670,f5605]) ).

fof(f5670,plain,
    ! [X0] : inverse(multiply(sF1_fnc,X0)) = divide(multiply(sF1_fnc,divide(sF1_fnc,X0)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5591,f5662]) ).

fof(f5674,plain,
    ! [X0,X1] : divide(inverse(multiply(sF1_fnc,divide(X0,X1))),sF1_fnc) = divide(X1,X0),
    inference(backward_demodulation,[status(thm)],[f5669,f5108]) ).

fof(f5684,plain,
    divide(inverse(multiply(sF1_fnc,inverse(a2))),sF1_fnc) = divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(backward_demodulation,[status(thm)],[f5669,f5225]) ).

fof(f5696,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(divide(inverse(multiply(sF1_fnc,X2)),sF1_fnc),X1))) = divide(X0,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f5669,f5214]) ).

fof(f5712,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,divide(inverse(multiply(sF1_fnc,X3)),sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f5669,f5198]) ).

fof(f5714,plain,
    ! [X0,X1] : divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f5669,f5196]) ).

fof(f5752,plain,
    ! [X0,X1] : divide(inverse(divide(inverse(a2),divide(X0,X1))),sF0_fnc) = inverse(multiply(sF1_fnc,divide(X1,X0))),
    inference(paramodulation,[status(thm)],[f5674,f49]) ).

fof(f5783,plain,
    ! [X0] : inverse(multiply(sF1_fnc,divide(sF1_fnc,X0))) = X0,
    inference(backward_demodulation,[status(thm)],[f5752,f49]) ).

fof(f5827,plain,
    divide(inverse(multiply(sF1_fnc,inverse(sF2_fnc))),sF1_fnc) = divide(sF1_fnc,b2),
    inference(paramodulation,[status(thm)],[f5597,f5674]) ).

fof(f5854,plain,
    divide(a2,sF0_fnc) = sF1_fnc,
    inference(paramodulation,[status(thm)],[f9,f5337]) ).

fof(f6277,plain,
    ! [X0,X1] : multiply(X0,multiply(sF1_fnc,divide(sF1_fnc,X1))) = divide(X0,X1),
    inference(paramodulation,[status(thm)],[f5783,f5]) ).

fof(f6286,plain,
    ! [X0,X1] : inverse(X0) = divide(X1,multiply(X0,X1)),
    inference(backward_demodulation,[status(thm)],[f6277,f5411]) ).

fof(f6295,plain,
    ! [X0] : inverse(multiply(sF1_fnc,inverse(X0))) = divide(X0,sF1_fnc),
    inference(paramodulation,[status(thm)],[f5349,f6286]) ).

fof(f6320,plain,
    ! [X0,X1] : divide(inverse(multiply(sF1_fnc,inverse(X0))),sF1_fnc) = divide(multiply(X0,X1),X1),
    inference(paramodulation,[status(thm)],[f6286,f5674]) ).

fof(f6322,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(X0)),divide(divide(X1,sF1_fnc),X2)) = inverse(divide(X1,divide(multiply(X0,X2),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f6286,f31]) ).

fof(f6326,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(divide(X0,X1)),divide(divide(X2,inverse(X3)),X0)) = inverse(divide(X2,divide(X1,divide(multiply(X3,X4),X4)))),
    inference(paramodulation,[status(thm)],[f6286,f14]) ).

fof(f6330,plain,
    divide(divide(sF2_fnc,sF1_fnc),sF1_fnc) = divide(sF1_fnc,b2),
    inference(backward_demodulation,[status(thm)],[f6295,f5827]) ).

fof(f6331,plain,
    divide(divide(a2,sF1_fnc),sF1_fnc) = divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF0_fnc))),
    inference(backward_demodulation,[status(thm)],[f6295,f5684]) ).

fof(f6387,plain,
    ! [X0,X1] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(multiply(X0,X1),X1),
    inference(forward_demodulation,[status(thm)],[f6295,f6320]) ).

fof(f6402,plain,
    ! [X0,X1,X2,X3,X4] : divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0)) = inverse(divide(X2,divide(X1,divide(multiply(X3,X4),X4)))),
    inference(forward_demodulation,[status(thm)],[f5,f6326]) ).

fof(f6403,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0)) = inverse(divide(X2,divide(X1,divide(divide(X3,sF1_fnc),sF1_fnc)))),
    inference(forward_demodulation,[status(thm)],[f6387,f6402]) ).

fof(f7076,plain,
    ! [X0,X1,X2,X3] : divide(divide(X0,sF1_fnc),divide(divide(X1,divide(X2,X3)),sF1_fnc)) = inverse(divide(X1,divide(inverse(inverse(X0)),divide(X3,X2)))),
    inference(paramodulation,[status(thm)],[f6295,f200]) ).

fof(f7275,plain,
    ! [X0] : inverse(divide(X0,divide(sF1_fnc,sF1_fnc))) = divide(inverse(X0),divide(sF1_fnc,sF1_fnc)),
    inference(paramodulation,[status(thm)],[f5144,f5144]) ).

fof(f7280,plain,
    ! [X0] : inverse(divide(X0,divide(sF1_fnc,sF1_fnc))) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(paramodulation,[status(thm)],[f5783,f5144]) ).

fof(f7318,plain,
    ! [X0] : divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc))) = divide(inverse(X0),divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f7275,f5100]) ).

fof(f7323,plain,
    ! [X0] : multiply(sF1_fnc,divide(sF1_fnc,X0)) = divide(inverse(X0),divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f7280,f7275]) ).

fof(f7349,plain,
    ! [X0] : divide(sF1_fnc,divide(divide(X0,sF1_fnc),divide(sF1_fnc,sF1_fnc))) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(backward_demodulation,[status(thm)],[f7323,f7318]) ).

fof(f7440,plain,
    ! [X0,X1] : divide(inverse(divide(X0,X1)),divide(divide(sF1_fnc,b2),X0)) = inverse(divide(divide(sF2_fnc,sF1_fnc),divide(X1,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f6330,f31]) ).

fof(f7455,plain,
    ! [X0,X1] : divide(inverse(divide(X0,divide(X1,divide(sF1_fnc,divide(sF2_fnc,sF1_fnc))))),divide(divide(sF1_fnc,b2),X0)) = X1,
    inference(paramodulation,[status(thm)],[f6330,f4]) ).

fof(f7499,plain,
    ! [X0] : inverse(divide(divide(sF2_fnc,sF1_fnc),divide(divide(X0,divide(sF1_fnc,divide(sF2_fnc,sF1_fnc))),sF1_fnc))) = X0,
    inference(forward_demodulation,[status(thm)],[f7440,f7455]) ).

fof(f7500,plain,
    ! [X0] : inverse(inverse(divide(X0,divide(inverse(inverse(sF2_fnc)),divide(divide(sF2_fnc,sF1_fnc),sF1_fnc))))) = X0,
    inference(forward_demodulation,[status(thm)],[f7076,f7499]) ).

fof(f7501,plain,
    ! [X0] : inverse(inverse(divide(X0,inverse(divide(sF2_fnc,divide(multiply(sF2_fnc,sF1_fnc),sF1_fnc)))))) = X0,
    inference(forward_demodulation,[status(thm)],[f6322,f7500]) ).

fof(f7502,plain,
    ! [X0] : inverse(inverse(multiply(X0,divide(sF2_fnc,divide(multiply(sF2_fnc,sF1_fnc),sF1_fnc))))) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f7501]) ).

fof(f7503,plain,
    ! [X0] : inverse(inverse(multiply(X0,divide(sF2_fnc,divide(divide(sF2_fnc,sF1_fnc),sF1_fnc))))) = X0,
    inference(forward_demodulation,[status(thm)],[f6387,f7502]) ).

fof(f7504,plain,
    ! [X0] : inverse(inverse(multiply(X0,divide(sF2_fnc,divide(sF1_fnc,b2))))) = X0,
    inference(forward_demodulation,[status(thm)],[f6330,f7503]) ).

fof(f7510,plain,
    ! [X0] : divide(inverse(inverse(X0)),sF1_fnc) = inverse(inverse(divide(X0,sF1_fnc))),
    inference(paramodulation,[status(thm)],[f4963,f4643]) ).

fof(f7512,plain,
    ! [X0] : divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc) = inverse(inverse(inverse(X0))),
    inference(paramodulation,[status(thm)],[f5,f4643]) ).

fof(f7524,plain,
    ! [X0] : divide(inverse(multiply(sF1_fnc,inverse(inverse(X0)))),sF1_fnc) = divide(sF1_fnc,inverse(divide(sF1_fnc,X0))),
    inference(paramodulation,[status(thm)],[f4643,f5674]) ).

fof(f7530,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,inverse(inverse(X3))),X0)) = inverse(divide(X2,divide(X1,divide(sF1_fnc,inverse(divide(sF1_fnc,X3)))))),
    inference(paramodulation,[status(thm)],[f4643,f14]) ).

fof(f7537,plain,
    ! [X0] : divide(inverse(inverse(divide(X0,sF1_fnc))),sF1_fnc) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f7510,f5123]) ).

fof(f7546,plain,
    ! [X0,X1] : inverse(inverse(inverse(divide(X0,X1)))) = divide(X1,X0),
    inference(backward_demodulation,[status(thm)],[f7512,f5674]) ).

fof(f7561,plain,
    ! [X0,X1] : inverse(inverse(inverse(X0))) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f7512,f5714]) ).

fof(f7563,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,divide(X1,inverse(inverse(inverse(X3)))))),
    inference(backward_demodulation,[status(thm)],[f7512,f5712]) ).

fof(f7578,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(inverse(inverse(inverse(X2))),X1))) = divide(X0,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f7512,f5696]) ).

fof(f7608,plain,
    ! [X0] : inverse(inverse(inverse(inverse(inverse(X0))))) = divide(sF1_fnc,inverse(divide(sF1_fnc,X0))),
    inference(forward_demodulation,[status(thm)],[f7512,f7524]) ).

fof(f7609,plain,
    ! [X0] : inverse(inverse(inverse(inverse(inverse(X0))))) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(forward_demodulation,[status(thm)],[f5,f7608]) ).

fof(f7623,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0)) = inverse(divide(X2,divide(X1,divide(sF1_fnc,inverse(divide(sF1_fnc,X3)))))),
    inference(forward_demodulation,[status(thm)],[f5,f7530]) ).

fof(f7626,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0)) = inverse(divide(X2,divide(X1,multiply(sF1_fnc,divide(sF1_fnc,X3))))),
    inference(forward_demodulation,[status(thm)],[f5,f7623]) ).

fof(f7633,plain,
    ! [X0] : divide(divide(inverse(inverse(X0)),sF1_fnc),sF1_fnc) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f7510,f7537]) ).

fof(f7662,plain,
    ! [X0,X1,X2] : inverse(divide(inverse(X0),multiply(divide(X1,multiply(X2,X0)),inverse(inverse(X2))))) = X1,
    inference(backward_demodulation,[status(thm)],[f7674,f17]) ).

fof(f7674,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)) = inverse(divide(X2,multiply(X1,inverse(inverse(X3))))),
    inference(forward_demodulation,[status(thm)],[f5,f7563]) ).

fof(f7724,plain,
    ! [X0] : inverse(inverse(inverse(inverse(X0)))) = divide(divide(X0,sF1_fnc),sF1_fnc),
    inference(paramodulation,[status(thm)],[f4963,f7546]) ).

fof(f7743,plain,
    ! [X0,X1,X2] : multiply(X0,inverse(inverse(divide(X1,X2)))) = divide(X0,divide(X2,X1)),
    inference(paramodulation,[status(thm)],[f7546,f5]) ).

fof(f7746,plain,
    ! [X0] : divide(divide(inverse(X0),sF1_fnc),sF1_fnc) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(backward_demodulation,[status(thm)],[f7724,f7609]) ).

fof(f7780,plain,
    ! [X0] : multiply(sF1_fnc,divide(sF1_fnc,inverse(X0))) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f7746,f7633]) ).

fof(f7795,plain,
    ! [X0] : multiply(sF1_fnc,multiply(sF1_fnc,X0)) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5,f7780]) ).

fof(f7796,plain,
    divide(divide(sF0_fnc,sF1_fnc),sF1_fnc) = divide(sF0_fnc,divide(sF1_fnc,sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f7818,f5523]) ).

fof(f7801,plain,
    ! [X0] : multiply(X0,sF2_fnc) = divide(X0,b2),
    inference(backward_demodulation,[status(thm)],[f7818,f5124]) ).

fof(f7803,plain,
    ! [X0,X1] : inverse(inverse(divide(X0,X1))) = multiply(sF1_fnc,divide(sF1_fnc,divide(X1,X0))),
    inference(backward_demodulation,[status(thm)],[f7818,f5445]) ).

fof(f7806,plain,
    ! [X0] : divide(sF1_fnc,divide(X0,sF1_fnc)) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(backward_demodulation,[status(thm)],[f7818,f7349]) ).

fof(f7807,plain,
    ! [X0] : multiply(divide(sF1_fnc,sF1_fnc),X0) = divide(divide(X0,sF1_fnc),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f7818,f5444]) ).

fof(f7817,plain,
    ! [X0,X1,X2] : divide(inverse(divide(X0,X1)),divide(X2,X0)) = inverse(divide(inverse(inverse(X2)),X1)),
    inference(backward_demodulation,[status(thm)],[f7818,f4964]) ).

fof(f7818,plain,
    ! [X0] : X0 = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5412,f7795]) ).

fof(f7848,plain,
    divide(multiply(sF1_fnc,divide(a2,sF1_fnc)),sF1_fnc) = sF0_fnc,
    inference(backward_demodulation,[status(thm)],[f7853,f5518]) ).

fof(f7853,plain,
    divide(divide(sF0_fnc,sF1_fnc),sF1_fnc) = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f7818,f7796]) ).

fof(f7854,plain,
    divide(sF1_fnc,b2) = sF2_fnc,
    inference(backward_demodulation,[status(thm)],[f7801,f5336]) ).

fof(f7893,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(multiply(inverse(inverse(divide(X0,X1))),inverse(X2)),X2),
    inference(backward_demodulation,[status(thm)],[f7803,f2260]) ).

fof(f7900,plain,
    ! [X0,X1] : multiply(X0,inverse(X1)) = divide(X0,X1),
    inference(backward_demodulation,[status(thm)],[f7948,f6277]) ).

fof(f7901,plain,
    ! [X0] : inverse(inverse(X0)) = X0,
    inference(backward_demodulation,[status(thm)],[f7948,f5783]) ).

fof(f7903,plain,
    divide(divide(a2,sF1_fnc),sF1_fnc) = divide(sF1_fnc,inverse(sF0_fnc)),
    inference(backward_demodulation,[status(thm)],[f7948,f6331]) ).

fof(f7910,plain,
    ! [X0,X1] : inverse(inverse(divide(X0,X1))) = inverse(divide(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f7948,f7803]) ).

fof(f7912,plain,
    ! [X0,X1,X2,X3] : divide(inverse(divide(X0,X1)),divide(multiply(X2,inverse(X3)),X0)) = inverse(divide(X2,divide(X1,inverse(X3)))),
    inference(backward_demodulation,[status(thm)],[f7948,f7626]) ).

fof(f7948,plain,
    ! [X0] : inverse(X0) = multiply(sF1_fnc,divide(sF1_fnc,X0)),
    inference(forward_demodulation,[status(thm)],[f4963,f7806]) ).

fof(f7950,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(multiply(multiply(X0,a2),inverse(sF0_fnc)),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f7807,f5599]) ).

fof(f8018,plain,
    ! [X0,X1,X2] : inverse(divide(inverse(inverse(multiply(X0,X1))),X2)) = inverse(divide(X0,divide(X2,divide(divide(X1,sF1_fnc),sF1_fnc)))),
    inference(backward_demodulation,[status(thm)],[f7817,f6403]) ).

fof(f8034,plain,
    ! [X0] : inverse(inverse(multiply(X0,divide(sF2_fnc,sF2_fnc)))) = X0,
    inference(backward_demodulation,[status(thm)],[f7854,f7504]) ).

fof(f8113,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(divide(inverse(inverse(divide(X0,X1))),X2),X2),
    inference(backward_demodulation,[status(thm)],[f7900,f7893]) ).

fof(f8147,plain,
    ! [X0,X1,X2] : inverse(divide(inverse(X0),divide(divide(X1,multiply(X2,X0)),inverse(X2)))) = X1,
    inference(backward_demodulation,[status(thm)],[f7900,f7662]) ).

fof(f8175,plain,
    ! [X0,X1,X2] : divide(X0,inverse(divide(X1,X2))) = divide(X0,divide(X2,X1)),
    inference(backward_demodulation,[status(thm)],[f7900,f7743]) ).

fof(f8214,plain,
    ! [X0,X1,X2] : divide(inverse(inverse(divide(X0,divide(X1,sF1_fnc)))),multiply(X2,divide(inverse(X2),X1))) = divide(X0,sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f7901,f7578]) ).

fof(f8226,plain,
    ! [X0,X1] : inverse(X0) = multiply(divide(sF1_fnc,X1),divide(X1,divide(X0,sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f7901,f7561]) ).

fof(f8327,plain,
    divide(divide(a2,sF1_fnc),sF1_fnc) = multiply(sF1_fnc,sF0_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f7903]) ).

fof(f8329,plain,
    divide(divide(a2,sF1_fnc),sF1_fnc) = a2,
    inference(forward_demodulation,[status(thm)],[f5461,f8327]) ).

fof(f8470,plain,
    ! [X0,X1] : divide(X0,X1) = inverse(divide(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f7901,f7910]) ).

fof(f8471,plain,
    ! [X0,X1,X2] : inverse(divide(inverse(inverse(multiply(X0,inverse(X1)))),X2)) = inverse(divide(X0,divide(X2,inverse(X1)))),
    inference(forward_demodulation,[status(thm)],[f7817,f7912]) ).

fof(f8472,plain,
    ! [X0,X1,X2] : divide(X0,inverse(inverse(multiply(X1,inverse(X2))))) = inverse(divide(X1,divide(X0,inverse(X2)))),
    inference(forward_demodulation,[status(thm)],[f8470,f8471]) ).

fof(f8473,plain,
    ! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,inverse(X2)))) = inverse(divide(X1,divide(X0,inverse(X2)))),
    inference(forward_demodulation,[status(thm)],[f5,f8472]) ).

fof(f8474,plain,
    ! [X0,X1,X2] : divide(X0,multiply(X1,inverse(X2))) = inverse(divide(X1,divide(X0,inverse(X2)))),
    inference(forward_demodulation,[status(thm)],[f7900,f8473]) ).

fof(f8475,plain,
    ! [X0,X1,X2] : divide(X0,divide(X1,X2)) = inverse(divide(X1,divide(X0,inverse(X2)))),
    inference(forward_demodulation,[status(thm)],[f7900,f8474]) ).

fof(f8476,plain,
    ! [X0,X1,X2] : divide(X0,divide(X1,X2)) = divide(divide(X0,inverse(X2)),X1),
    inference(forward_demodulation,[status(thm)],[f8470,f8475]) ).

fof(f8483,plain,
    divide(sF1_fnc,divide(sF1_fnc,divide(a2,sF1_fnc))) = sF0_fnc,
    inference(backward_demodulation,[status(thm)],[f8498,f7848]) ).

fof(f8498,plain,
    ! [X0,X1,X2] : divide(X0,divide(X1,X2)) = divide(multiply(X0,X2),X1),
    inference(forward_demodulation,[status(thm)],[f5,f8476]) ).

fof(f8563,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(multiply(X0,a2),divide(sF1_fnc,inverse(sF0_fnc))),
    inference(forward_demodulation,[status(thm)],[f8498,f7950]) ).

fof(f8564,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(X0,divide(divide(sF1_fnc,inverse(sF0_fnc)),a2)),
    inference(forward_demodulation,[status(thm)],[f8498,f8563]) ).

fof(f8565,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(X0,divide(multiply(sF1_fnc,sF0_fnc),a2)),
    inference(forward_demodulation,[status(thm)],[f5,f8564]) ).

fof(f8566,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(X0,divide(sF1_fnc,divide(a2,sF0_fnc))),
    inference(forward_demodulation,[status(thm)],[f8498,f8565]) ).

fof(f8567,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = divide(X0,divide(sF1_fnc,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f5854,f8566]) ).

fof(f8584,plain,
    ! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = X0,
    inference(forward_demodulation,[status(thm)],[f7818,f8567]) ).

fof(f8754,plain,
    ! [X0,X1,X2] : divide(X0,inverse(inverse(multiply(X1,X2)))) = inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))),
    inference(forward_demodulation,[status(thm)],[f8470,f8018]) ).

fof(f8755,plain,
    ! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,X2))) = inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))),
    inference(forward_demodulation,[status(thm)],[f5,f8754]) ).

fof(f8756,plain,
    ! [X0,X1,X2] : divide(X0,multiply(X1,X2)) = inverse(divide(X1,divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)))),
    inference(forward_demodulation,[status(thm)],[f7900,f8755]) ).

fof(f8757,plain,
    ! [X0,X1,X2] : divide(X0,multiply(X1,X2)) = divide(divide(X0,divide(divide(X2,sF1_fnc),sF1_fnc)),X1),
    inference(forward_demodulation,[status(thm)],[f8470,f8756]) ).

fof(f8828,plain,
    ! [X0,X1,X2] : divide(X0,multiply(X1,X2)) = divide(divide(X0,X2),X1),
    inference(forward_demodulation,[status(thm)],[f8584,f8757]) ).

fof(f8879,plain,
    ! [X0] : multiply(X0,divide(sF2_fnc,sF2_fnc)) = X0,
    inference(forward_demodulation,[status(thm)],[f7901,f8034]) ).

fof(f8881,plain,
    ! [X0] : multiply(X0,sF1_fnc) = X0,
    inference(forward_demodulation,[status(thm)],[f12,f8879]) ).

fof(f9032,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(divide(divide(X0,X1),X2),X2),
    inference(forward_demodulation,[status(thm)],[f7901,f8113]) ).

fof(f9034,plain,
    ! [X0,X1,X2] : divide(X0,X1) = multiply(divide(X0,multiply(X2,X1)),X2),
    inference(forward_demodulation,[status(thm)],[f8828,f9032]) ).

fof(f9184,plain,
    ! [X0,X1,X2] : divide(divide(divide(X0,multiply(X1,X2)),inverse(X1)),inverse(X2)) = X0,
    inference(forward_demodulation,[status(thm)],[f8470,f8147]) ).

fof(f9185,plain,
    ! [X0,X1,X2] : multiply(divide(divide(X0,multiply(X1,X2)),inverse(X1)),X2) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f9184]) ).

fof(f9186,plain,
    ! [X0,X1,X2] : multiply(multiply(divide(X0,multiply(X1,X2)),X1),X2) = X0,
    inference(forward_demodulation,[status(thm)],[f5,f9185]) ).

fof(f9190,plain,
    ! [X0,X1] : multiply(divide(X0,X1),X1) = X0,
    inference(forward_demodulation,[status(thm)],[f9034,f9186]) ).

fof(f9441,plain,
    ! [X0,X1,X2] : multiply(X0,divide(X1,X2)) = divide(X0,divide(X2,X1)),
    inference(forward_demodulation,[status(thm)],[f5,f8175]) ).

fof(f9797,plain,
    ! [X0,X1,X2] : divide(divide(X0,divide(X1,sF1_fnc)),multiply(X2,divide(inverse(X2),X1))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f7901,f8214]) ).

fof(f9798,plain,
    ! [X0,X1,X2] : divide(X0,multiply(multiply(X1,divide(inverse(X1),X2)),divide(X2,sF1_fnc))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f8828,f9797]) ).

fof(f9799,plain,
    ! [X0,X1,X2] : divide(X0,divide(multiply(X1,divide(inverse(X1),X2)),divide(sF1_fnc,X2))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f9441,f9798]) ).

fof(f9800,plain,
    ! [X0,X1,X2] : divide(X0,divide(X1,divide(divide(sF1_fnc,X2),divide(inverse(X1),X2)))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f8498,f9799]) ).

fof(f9801,plain,
    ! [X0,X1,X2] : divide(X0,divide(X1,divide(sF1_fnc,multiply(divide(inverse(X1),X2),X2)))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f8828,f9800]) ).

fof(f9802,plain,
    ! [X0,X1] : divide(X0,divide(X1,divide(sF1_fnc,inverse(X1)))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f9190,f9801]) ).

fof(f9803,plain,
    ! [X0,X1] : divide(X0,divide(X1,multiply(sF1_fnc,X1))) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f9802]) ).

fof(f9804,plain,
    ! [X0] : divide(X0,inverse(sF1_fnc)) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f6286,f9803]) ).

fof(f9805,plain,
    ! [X0] : multiply(X0,sF1_fnc) = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f5,f9804]) ).

fof(f9816,plain,
    ! [X0] : X0 = divide(X0,sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f8881,f9805]) ).

fof(f9897,plain,
    ! [X0,X1] : inverse(X0) = divide(divide(sF1_fnc,X1),divide(divide(X0,sF1_fnc),X1)),
    inference(forward_demodulation,[status(thm)],[f9441,f8226]) ).

fof(f9898,plain,
    ! [X0,X1] : inverse(X0) = divide(sF1_fnc,multiply(divide(divide(X0,sF1_fnc),X1),X1)),
    inference(forward_demodulation,[status(thm)],[f8828,f9897]) ).

fof(f9899,plain,
    ! [X0] : inverse(X0) = divide(sF1_fnc,divide(X0,sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f9190,f9898]) ).

fof(f9907,plain,
    ! [X0] : inverse(X0) = divide(sF1_fnc,X0),
    inference(forward_demodulation,[status(thm)],[f9816,f9899]) ).

fof(f12208,plain,
    inverse(divide(sF1_fnc,divide(a2,sF1_fnc))) = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f9907,f8483]) ).

fof(f12209,plain,
    divide(divide(a2,sF1_fnc),sF1_fnc) = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f8470,f12208]) ).

fof(f12210,plain,
    a2 = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f8329,f12209]) ).

fof(f12211,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[f12210,f10]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP470-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05  % Command  : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.42  % Computer : n011.cluster.edu
% 0.16/5.42  % Model    : x86_64 x86_64
% 0.16/5.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.42  % Memory   : 8046.5625MB
% 0.16/5.42  % OS       : Linux 6.8.0-71-generic
% 0.16/5.42  % CPULimit : 300
% 0.16/5.42  % WCLimit  : 300
% 0.16/5.42  % DateTime : Sun Sep 20 20:14:31 UTC 2026
% 0.16/5.43  % CPUTime  : 
% 0.16/5.44  % Drodi V4.1.1
% 23.40/8.44  % Refutation found
% 23.40/8.44  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 23.40/8.44  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.40/8.52  % Elapsed time: 3.078929 seconds
% 23.40/8.52  % CPU time: 24.178627 seconds
% 23.40/8.52  % Total memory used: 394.032 MB
% 23.40/8.52  % Net memory used: 382.862 MB
%------------------------------------------------------------------------------