Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : GRP425-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 : n019.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:36 PM UTC 2026

% Result   : Unsatisfiable 87.92s 19.03s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP425-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37  % Computer : n019.cluster.edu
% 0.10/0.37  % Model    : x86_64 x86_64
% 0.10/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37  % Memory   : 8046.5625MB
% 0.10/0.37  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Sun Sep 20 20:13:05 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.37  % Drodi V4.1.1
% 87.92/19.03  % Refutation found
% 87.92/19.03  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 87.92/19.03  % SZS output start CNFRefutation for theBenchmark
% 87.92/19.03  fof(f1,axiom,(
% 87.92/19.03    (![A,B,C]: (multiply(inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),C)))),multiply(A,inverse(C)))),inverse(multiply(inverse(C),C))) = B ))),
% 87.92/19.03    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 87.92/19.03  fof(f2,negated_conjecture,(
% 87.92/19.03    multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 87.92/19.03    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 87.92/19.03  fof(f3,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X1)),
% 87.92/19.03    inference(cnf_transformation,[status(thm)],[f1])).
% 87.92/19.03  fof(f4,plain,(
% 87.92/19.03    ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 87.92/19.03    inference(cnf_transformation,[status(thm)],[f2])).
% 87.92/19.03  fof(f5,definition,(
% 87.92/19.03    sF2_fnc=inverse(b2)),
% 87.92/19.03    introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 87.92/19.03  fof(f6,definition,(
% 87.92/19.03    sF1_fnc=multiply(sF2_fnc,b2)),
% 87.92/19.03    introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 87.92/19.03  fof(f7,definition,(
% 87.92/19.03    sF0_fnc=multiply(sF1_fnc,a2)),
% 87.92/19.03    introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 87.92/19.03  fof(f8,plain,(
% 87.92/19.03    ~sF0_fnc=a2),
% 87.92/19.03    inference(definition_folding,[],[f4,f7,f6,f5])).
% 87.92/19.03  fof(f9,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f3,f3])).
% 87.92/19.03  fof(f10,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f3,f3])).
% 87.92/19.03  fof(f11,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(sF2_fnc,X1)))),multiply(X0,inverse(X1)))),inverse(multiply(inverse(X1),X1)))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f5,f3])).
% 87.92/19.03  fof(f12,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=X3)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f3,f3])).
% 87.92/19.03  fof(f13,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),inverse(multiply(inverse(b2),b2)))=X1)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f5,f3])).
% 87.92/19.03  fof(f15,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),inverse(multiply(sF2_fnc,b2)))=X1)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f13])).
% 87.92/19.03  fof(f16,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),inverse(sF1_fnc))=X1)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f15])).
% 87.92/19.03  fof(f20,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(sF2_fnc,b2)))),multiply(X0,sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f5,f16])).
% 87.92/19.03  fof(f21,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f16,f3])).
% 87.92/19.03  fof(f24,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f20])).
% 87.92/19.03  fof(f25,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f24,f24])).
% 87.92/19.03  fof(f28,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),b2)),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))=X1)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f24,f3])).
% 87.92/19.03  fof(f29,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f25])).
% 87.92/19.03  fof(f35,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f3,f11])).
% 87.92/19.03  fof(f40,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(sF2_fnc,X1)))),multiply(X0,inverse(X1)))),inverse(X1)))),inverse(multiply(inverse(X1),X1)))=X1)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f11,f3])).
% 87.92/19.03  fof(f55,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(sF2_fnc,X1)))),multiply(X0,inverse(X1)))),inverse(X1)))),inverse(multiply(inverse(X1),X1)))=X1)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f40])).
% 87.92/19.03  fof(f57,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f24,f29])).
% 87.92/19.03  fof(f64,plain,(
% 87.92/19.03    ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f57])).
% 87.92/19.03  fof(f74,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=inverse(sF1_fnc))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f16,f9])).
% 87.92/19.03  fof(f87,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))=multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f9,f3])).
% 87.92/19.03  fof(f153,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))=multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f55,f3])).
% 87.92/19.03  fof(f156,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(multiply(inverse(X0),X0)))=X0)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f55,f9])).
% 87.92/19.03  fof(f225,plain,(
% 87.92/19.03    ![X0,X1]: (b2=multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X1),X1)))),X1)))),multiply(X0,inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f11,f10])).
% 87.92/19.03  fof(f226,plain,(
% 87.92/19.03    ![X0,X1,X2]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X1,inverse(X2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f3,f10])).
% 87.92/19.03  fof(f227,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f10])).
% 87.92/19.03  fof(f232,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f28,f10])).
% 87.92/19.03  fof(f245,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))=multiply(inverse(X1),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f55,f10])).
% 87.92/19.03  fof(f262,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3)))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3))))),inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3)))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(multiply(X1,inverse(X3))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f10])).
% 87.92/19.03  fof(f272,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f10])).
% 87.92/19.03  fof(f283,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f9])).
% 87.92/19.03  fof(f286,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f9])).
% 87.92/19.03  fof(f376,plain,(
% 87.92/19.03    ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(sF2_fnc,b2)))),b2)))),multiply(X1,inverse(b2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f5,f226])).
% 87.92/19.03  fof(f385,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f226])).
% 87.92/19.03  fof(f398,plain,(
% 87.92/19.03    ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(sF1_fnc))),b2)))),multiply(X1,inverse(b2))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f376])).
% 87.92/19.03  fof(f399,plain,(
% 87.92/19.03    ![X0,X1]: (X0=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),inverse(sF1_fnc))),b2)))),multiply(X1,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f398])).
% 87.92/19.03  fof(f413,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,sF2_fnc))))),inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))))=multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(sF1_fnc))),b2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f399,f3])).
% 87.92/19.03  fof(f433,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(sF2_fnc,X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=X2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f55,f12])).
% 87.92/19.03  fof(f471,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),X1)))),multiply(X0,inverse(X1)))),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))=multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f12,f226])).
% 87.92/19.03  fof(f673,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X2,inverse(X3)))))),multiply(X4,inverse(multiply(X2,inverse(X3))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f226,f227])).
% 87.92/19.03  fof(f675,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(b2))),multiply(X0,inverse(multiply(X1,inverse(X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X1,inverse(X2)))))),multiply(X3,inverse(multiply(X1,inverse(X2))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f225,f227])).
% 87.92/19.03  fof(f789,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3)))))=multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X2,inverse(X3))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f226,f673])).
% 87.92/19.03  fof(f793,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,inverse(multiply(X1,inverse(X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),X2)))),X2)))),multiply(X1,inverse(X2)))))),multiply(X3,inverse(multiply(X1,inverse(X2))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f675])).
% 87.92/19.03  fof(f794,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,inverse(multiply(X1,inverse(X2)))))=multiply(inverse(multiply(X3,inverse(b2))),multiply(X3,inverse(multiply(X1,inverse(X2))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f225,f793])).
% 87.92/19.03  fof(f795,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,inverse(multiply(X1,inverse(X2)))))=multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,inverse(multiply(X1,inverse(X2))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f794])).
% 87.92/19.03  fof(f873,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),b2)))),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f28,f21])).
% 87.92/19.03  fof(f914,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f21,f10])).
% 87.92/19.03  fof(f915,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),inverse(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))),multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f21,f55])).
% 87.92/19.03  fof(f917,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))),multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))=b2)),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f21,f11])).
% 87.92/19.03  fof(f1282,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,inverse(b2)))=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f64,f795])).
% 87.92/19.03  fof(f1332,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f1282])).
% 87.92/19.03  fof(f1333,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,inverse(b2))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f64,f1332])).
% 87.92/19.03  fof(f1334,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f1333])).
% 87.92/19.03  fof(f1467,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc))))),multiply(X0,inverse(multiply(X2,sF2_fnc))))),inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))))=multiply(X2,sF2_fnc))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f1334,f3])).
% 87.92/19.03  fof(f1490,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc))),inverse(sF1_fnc))),b2)))=multiply(X0,sF2_fnc))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f413,f1467])).
% 87.92/19.03  fof(f1589,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF2_fnc))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc))),inverse(sF1_fnc)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f1490,f16])).
% 87.92/19.03  fof(f2034,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f10,f789])).
% 87.92/19.03  fof(f2036,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(b2)))=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(sF1_fnc))),multiply(X3,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f64,f789])).
% 87.92/19.03  fof(f2037,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X4,inverse(multiply(sF2_fnc,X2)))),multiply(X4,inverse(X2)))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f55,f789])).
% 87.92/19.03  fof(f2188,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(sF1_fnc))),multiply(X3,sF2_fnc))),sF2_fnc))),sF2_fnc))),inverse(sF1_fnc))))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f2036])).
% 87.92/19.03  fof(f2189,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(b2))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f64,f2188])).
% 87.92/19.03  fof(f2190,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF2_fnc))=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f2189])).
% 87.92/19.03  fof(f2191,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f55,f2037])).
% 87.92/19.03  fof(f2322,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF2_fnc))))),multiply(X0,inverse(multiply(X3,sF2_fnc))))),inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))))=multiply(X3,inverse(X2)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f2190,f3])).
% 87.92/19.03  fof(f2364,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF2_fnc))),inverse(sF1_fnc))),b2)))=multiply(X0,inverse(X2)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f413,f2322])).
% 87.92/19.03  fof(f2379,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),inverse(X1)))=multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f24,f2191])).
% 87.92/19.03  fof(f2386,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X3)))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X0),X0)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f9,f2191])).
% 87.92/19.03  fof(f2518,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),inverse(X1)))=multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,inverse(X1))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f2379])).
% 87.92/19.03  fof(f2700,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),inverse(X3)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f2364,f9])).
% 87.92/19.03  fof(f2747,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f2364,f10])).
% 87.92/19.03  fof(f2748,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,sF2_fnc))),inverse(sF1_fnc))),b2)),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f2364,f10])).
% 87.92/19.03  fof(f2778,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X1,inverse(X3)))),inverse(X3)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f2364,f2700])).
% 87.92/19.03  fof(f3121,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(X1))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f1589,f2191])).
% 87.92/19.03  fof(f3122,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(X1)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(X1))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f1589,f2191])).
% 87.92/19.03  fof(f3134,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f1589,f10])).
% 87.92/19.03  fof(f3318,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),b2)))),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f35,f21])).
% 87.92/19.03  fof(f3323,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(b2),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f35,f10])).
% 87.92/19.03  fof(f3433,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),b2)))),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f3318])).
% 87.92/19.03  fof(f3434,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5,f3323])).
% 87.92/19.03  fof(f3436,plain,(
% 87.92/19.03    ![X0]: (multiply(sF2_fnc,b2)=multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(sF1_fnc))))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f24,f2518])).
% 87.92/19.03  fof(f3474,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,sF2_fnc))),inverse(sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),b2)))),multiply(X1,sF2_fnc))),inverse(sF1_fnc))),X2))),
% 87.92/19.03    inference(paramodulation,[status(thm)],[f16,f2518])).
% 87.92/19.03  fof(f3526,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f3543,f917])).
% 87.92/19.03  fof(f3528,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),inverse(sF1_fnc))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f3543,f915])).
% 87.92/19.03  fof(f3543,plain,(
% 87.92/19.03    ![X0]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f3436])).
% 87.92/19.03  fof(f3572,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(sF2_fnc,b2)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),inverse(sF1_fnc))),X1))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f24,f3474])).
% 87.92/19.03  fof(f3573,plain,(
% 87.92/19.03    ![X0,X1]: (sF1_fnc=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),inverse(sF1_fnc))),X1))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f3572])).
% 87.92/19.03  fof(f3583,plain,(
% 87.92/19.03    ![X0]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),b2)))=multiply(X0,sF2_fnc))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f1490])).
% 87.92/19.03  fof(f3614,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(sF1_fnc))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f3134])).
% 87.92/19.03  fof(f3702,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(X2,inverse(multiply(inverse(sF1_fnc),b2)))),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f873])).
% 87.92/19.03  fof(f3729,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(sF1_fnc),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f232])).
% 87.92/19.03  fof(f3756,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),b2)))),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f3433])).
% 87.92/19.03  fof(f3780,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(sF1_fnc),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f914])).
% 87.92/19.03  fof(f3809,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=inverse(sF1_fnc))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f74])).
% 87.92/19.03  fof(f3814,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))))),inverse(sF1_fnc))=multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f2747])).
% 87.92/19.03  fof(f3820,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X4),X2)))),multiply(X5,inverse(X2)))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f272])).
% 87.92/19.03  fof(f3838,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(sF1_fnc)),X1)))),multiply(X0,inverse(X1)))),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))=multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f471])).
% 87.92/19.03  fof(f3855,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))))),multiply(X0,inverse(inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3)))))))),inverse(sF1_fnc))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(multiply(X1,inverse(X3))))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f262])).
% 87.92/19.03  fof(f3868,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,multiply(inverse(X2),X2))))),X1)),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(sF1_fnc))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f3434])).
% 87.92/19.03  fof(f3879,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,sF2_fnc))),inverse(sF1_fnc))),b2)),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f2748])).
% 87.92/19.03  fof(f3884,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(X3))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X1),X2)))),multiply(X4,inverse(X2))))=multiply(inverse(multiply(X5,inverse(X3))),multiply(X5,inverse(sF1_fnc))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f2034])).
% 87.92/19.03  fof(f3897,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(sF2_fnc,X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),sF1_fnc)))=X2)),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f433])).
% 87.92/19.03  fof(f3900,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),sF1_fnc)))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f385])).
% 87.92/19.03  fof(f3904,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(sF1_fnc))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f286])).
% 87.92/19.03  fof(f3907,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=sF1_fnc)),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f283])).
% 87.92/19.03  fof(f3911,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(sF1_fnc))=multiply(inverse(X1),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f245])).
% 87.92/19.03  fof(f3923,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(sF1_fnc))=multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f153])).
% 87.92/19.03  fof(f3925,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))))),inverse(sF1_fnc))=multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f87])).
% 87.92/19.03  fof(f3980,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X1,inverse(X3)))),inverse(X3)))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f2778])).
% 87.92/19.03  fof(f4120,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(sF1_fnc))),multiply(X0,inverse(X1)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),multiply(inverse(sF1_fnc),inverse(X1))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f3122])).
% 87.92/19.03  fof(f4121,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(X1))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f3121])).
% 87.92/19.03  fof(f4201,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0)))),inverse(X3)))=multiply(inverse(multiply(X4,inverse(sF1_fnc))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f2386])).
% 87.92/19.03  fof(f4213,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(X0)))),inverse(sF1_fnc))=X0)),
% 87.92/19.03    inference(backward_demodulation,[status(thm)],[f4217,f156])).
% 87.92/19.03  fof(f4217,plain,(
% 87.92/19.03    ![X0]: (sF1_fnc=multiply(inverse(X0),X0))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f16,f3573])).
% 87.92/19.03  fof(f4344,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,sF1_fnc)))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(sF1_fnc))=b2)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3526])).
% 87.92/19.03  fof(f4348,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,sF1_fnc)))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))))),inverse(sF1_fnc))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3528])).
% 87.92/19.03  fof(f4349,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(sF2_fnc,sF1_fnc)))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sF2_fnc)))),inverse(sF1_fnc)))),inverse(sF1_fnc))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4348])).
% 87.92/19.03  fof(f4350,plain,(
% 87.92/19.03    multiply(inverse(multiply(sF2_fnc,b2)),inverse(sF1_fnc))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4344,f4349])).
% 87.92/19.03  fof(f4351,plain,(
% 87.92/19.03    multiply(inverse(sF1_fnc),inverse(sF1_fnc))=multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f6,f4350])).
% 87.92/19.03  fof(f4354,plain,(
% 87.92/19.03    multiply(inverse(sF1_fnc),inverse(sF1_fnc))=sF1_fnc),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4351])).
% 87.92/19.03  fof(f4389,plain,(
% 87.92/19.03    ![X0]: (multiply(X0,inverse(multiply(inverse(sF1_fnc),b2)))=multiply(X0,sF2_fnc))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4354,f3583])).
% 87.92/19.03  fof(f4483,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(sF1_fnc))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3614])).
% 87.92/19.03  fof(f4484,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4483])).
% 87.92/19.03  fof(f4485,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4484])).
% 87.92/19.03  fof(f4486,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4485])).
% 87.92/19.03  fof(f4487,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4486])).
% 87.92/19.03  fof(f4495,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X1),sF1_fnc)))),sF1_fnc))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4354,f4487])).
% 87.92/19.03  fof(f4699,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(inverse(sF1_fnc),b2)))),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3702])).
% 87.92/19.03  fof(f4700,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4389,f4699])).
% 87.92/19.03  fof(f4701,plain,(
% 87.92/19.03    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=sF1_fnc)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4700])).
% 87.92/19.03  fof(f4797,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(sF1_fnc),X2)))),multiply(X3,inverse(X2))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3729])).
% 87.92/19.03  fof(f4798,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,sF2_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),b2)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(inverse(sF1_fnc),X3)))),multiply(X2,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4797])).
% 87.92/19.03  fof(f4800,plain,(
% 87.92/19.03    ![X0,X1]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(multiply(inverse(sF1_fnc),X1)))),multiply(X0,inverse(X1))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4701,f4798])).
% 87.92/19.03  fof(f4870,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),b2)))),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3756])).
% 87.92/19.03  fof(f4871,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(sF1_fnc),b2)))),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4870])).
% 87.92/19.03  fof(f4872,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,sF2_fnc)),multiply(X3,sF2_fnc)))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4389,f4871])).
% 87.92/19.03  fof(f4873,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=sF1_fnc)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4872])).
% 87.92/19.03  fof(f4927,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))=multiply(inverse(multiply(X4,inverse(multiply(inverse(sF1_fnc),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3780])).
% 87.92/19.03  fof(f4928,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(sF1_fnc),X4)))),multiply(X3,inverse(X4))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f4927])).
% 87.92/19.03  fof(f4929,plain,(
% 87.92/19.03    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),b2)))),multiply(X0,sF2_fnc))),multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(sF1_fnc))))),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=sF1_fnc)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4800,f4928])).
% 87.92/19.03  fof(f5220,plain,(
% 87.92/19.03    sF1_fnc=inverse(sF1_fnc)),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4929,f3809])).
% 87.92/19.03  fof(f5243,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X2,inverse(X4))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3814])).
% 87.92/19.03  fof(f5244,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X1,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4495,f5243])).
% 87.92/19.03  fof(f5245,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))))),multiply(X1,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5220,f5244])).
% 87.92/19.03  fof(f5246,plain,(
% 87.92/19.03    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),sF1_fnc)),b2))))),multiply(X1,inverse(X3))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5220,f5245])).
% 87.92/19.03  fof(f5273,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(inverse(multiply(inverse(X4),X4)))))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X4),X4))),inverse(multiply(inverse(X4),X4))))))),multiply(inverse(multiply(X5,inverse(multiply(inverse(X3),X4)))),multiply(X5,inverse(X4)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f3820])).
% 87.92/19.03  fof(f5274,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4495,f5273])).
% 87.92/19.03  fof(f5275,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5220,f5274])).
% 87.92/19.03  fof(f5276,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f4217,f5275])).
% 87.92/19.03  fof(f5277,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(sF1_fnc)))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5220,f5276])).
% 87.92/19.03  fof(f5278,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF1_fnc))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.03    inference(forward_demodulation,[status(thm)],[f5220,f5277])).
% 87.92/19.03  fof(f5279,plain,(
% 87.92/19.03    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF1_fnc))),inverse(multiply(inverse(X0),sF1_fnc)))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X4)))),multiply(X3,inverse(X4)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5278])).
% 87.92/19.04  fof(f5446,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(sF1_fnc),X1)))),multiply(X0,inverse(X1)))),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))=multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f3838])).
% 87.92/19.04  fof(f5447,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),multiply(inverse(X1),X1))))=multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4800,f5446])).
% 87.92/19.04  fof(f5448,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(inverse(X1),X1))))=multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5447])).
% 87.92/19.04  fof(f5449,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5448])).
% 87.92/19.04  fof(f5450,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(sF1_fnc)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5449])).
% 87.92/19.04  fof(f5451,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5450])).
% 87.92/19.04  fof(f5458,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5451])).
% 87.92/19.04  fof(f5534,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),multiply(X4,inverse(multiply(X1,inverse(X3))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3855])).
% 87.92/19.04  fof(f5535,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f5534])).
% 87.92/19.04  fof(f5536,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5535])).
% 87.92/19.04  fof(f5537,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5536])).
% 87.92/19.04  fof(f5538,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(sF1_fnc)))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5537])).
% 87.92/19.04  fof(f5539,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,sF1_fnc))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5538])).
% 87.92/19.04  fof(f5540,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f5539])).
% 87.92/19.04  fof(f5541,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),inverse(sF1_fnc))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5540])).
% 87.92/19.04  fof(f5542,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),sF1_fnc)))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5541])).
% 87.92/19.04  fof(f5655,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(multiply(inverse(X3),X3)))))),inverse(sF1_fnc))=multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X3)))),multiply(X4,inverse(X3))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3868])).
% 87.92/19.04  fof(f5656,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(sF2_fnc,sF1_fnc)))),X1)),inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),X4)))),multiply(X3,inverse(X4))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5655])).
% 87.92/19.04  fof(f5657,plain,(
% 87.92/19.04    ![X0,X1,X2]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),X2)))),multiply(X0,inverse(X2))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4873,f5656])).
% 87.92/19.04  fof(f5658,plain,(
% 87.92/19.04    ![X0,X1]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(multiply(inverse(sF1_fnc),X1)))),multiply(X0,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5657])).
% 87.92/19.04  fof(f5659,plain,(
% 87.92/19.04    ![X0,X1]: (sF1_fnc=multiply(inverse(multiply(X0,inverse(multiply(sF1_fnc,X1)))),multiply(X0,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5658])).
% 87.92/19.04  fof(f5747,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,sF2_fnc))),inverse(sF1_fnc))),b2)),X4)))),multiply(X2,inverse(X4))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3879])).
% 87.92/19.04  fof(f5748,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),X3)))),multiply(X1,inverse(X3))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f5747])).
% 87.92/19.04  fof(f5749,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2)),X3)))),multiply(X1,inverse(X3))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5748])).
% 87.92/19.04  fof(f5750,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,sF2_fnc))),sF1_fnc)),b2)),X3)))),multiply(X1,inverse(X3))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5749])).
% 87.92/19.04  fof(f5770,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(X2))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X4)))),multiply(X3,inverse(X4))))=multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3884])).
% 87.92/19.04  fof(f5771,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(sF1_fnc)))),inverse(X2))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X4)))),multiply(X3,inverse(X4))))=multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5770])).
% 87.92/19.04  fof(f5772,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc))),inverse(X2))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X4)))),multiply(X3,inverse(X4))))=multiply(inverse(multiply(X5,inverse(X2))),multiply(X5,inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5771])).
% 87.92/19.04  fof(f5773,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(X1))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X3)))),multiply(X2,inverse(X3))))=multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f5772])).
% 87.92/19.04  fof(f5774,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(X1))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X3)))),multiply(X2,inverse(X3))))=multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5773])).
% 87.92/19.04  fof(f5776,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(X1))),multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X3)))),multiply(X2,inverse(X3))))=multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f5774])).
% 87.92/19.04  fof(f5879,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(sF2_fnc,X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),sF1_fnc)))=X2)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3897])).
% 87.92/19.04  fof(f5880,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(sF1_fnc)))),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(sF2_fnc,X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),sF1_fnc)))=X2)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5879])).
% 87.92/19.04  fof(f5881,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc))),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(sF2_fnc,X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),sF1_fnc)))=X2)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5880])).
% 87.92/19.04  fof(f5882,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),sF1_fnc)))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f5881])).
% 87.92/19.04  fof(f5883,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),sF1_fnc)))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5882])).
% 87.92/19.04  fof(f5884,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5883])).
% 87.92/19.04  fof(f5885,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),inverse(sF1_fnc))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5884])).
% 87.92/19.04  fof(f5886,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),sF1_fnc)=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5885])).
% 87.92/19.04  fof(f5911,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),sF1_fnc)))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3900])).
% 87.92/19.04  fof(f5912,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(sF1_fnc)))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),sF1_fnc)))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5911])).
% 87.92/19.04  fof(f5913,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF1_fnc))),inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),sF1_fnc)))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5912])).
% 87.92/19.04  fof(f5914,plain,(
% 87.92/19.04    ![X0,X1]: (X0=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),sF1_fnc)))),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5279,f5913])).
% 87.92/19.04  fof(f5915,plain,(
% 87.92/19.04    ![X0]: (X0=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5914])).
% 87.92/19.04  fof(f5916,plain,(
% 87.92/19.04    ![X0]: (X0=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5915])).
% 87.92/19.04  fof(f5934,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))),inverse(X2)))),inverse(multiply(inverse(X2),X2)))=X2)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3904])).
% 87.92/19.04  fof(f5935,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),inverse(multiply(inverse(X1),X1)))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f5934])).
% 87.92/19.04  fof(f5936,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),inverse(multiply(inverse(X1),X1)))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5935])).
% 87.92/19.04  fof(f5937,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),inverse(sF1_fnc))=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5936])).
% 87.92/19.04  fof(f5939,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),sF1_fnc)=X1)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5937])).
% 87.92/19.04  fof(f5958,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(inverse(sF1_fnc))))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3907])).
% 87.92/19.04  fof(f5959,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(sF1_fnc)))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5958])).
% 87.92/19.04  fof(f5960,plain,(
% 87.92/19.04    ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sF1_fnc))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),multiply(inverse(multiply(X4,inverse(multiply(inverse(X2),X3)))),multiply(X4,inverse(X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5959])).
% 87.92/19.04  fof(f5961,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f5960])).
% 87.92/19.04  fof(f5962,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),sF1_fnc)))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5776,f5961])).
% 87.92/19.04  fof(f5963,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5962])).
% 87.92/19.04  fof(f5964,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(sF1_fnc)))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5963])).
% 87.92/19.04  fof(f5965,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),sF1_fnc))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5964])).
% 87.92/19.04  fof(f5966,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5916,f5965])).
% 87.92/19.04  fof(f5967,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5966])).
% 87.92/19.04  fof(f5968,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))))=sF1_fnc)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5967])).
% 87.92/19.04  fof(f5969,plain,(
% 87.92/19.04    multiply(sF1_fnc,inverse(sF1_fnc))=sF1_fnc),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f5968])).
% 87.92/19.04  fof(f5973,plain,(
% 87.92/19.04    multiply(sF1_fnc,sF1_fnc)=sF1_fnc),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f5969])).
% 87.92/19.04  fof(f6009,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(X1),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1)))),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3911])).
% 87.92/19.04  fof(f6010,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(X0),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f6009])).
% 87.92/19.04  fof(f6011,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(X0),multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f6010])).
% 87.92/19.04  fof(f6075,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sF2_fnc,X1)))),multiply(X2,inverse(X1)))),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3923])).
% 87.92/19.04  fof(f6076,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f6075])).
% 87.92/19.04  fof(f6077,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X0))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f6082,f6011])).
% 87.92/19.04  fof(f6078,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),inverse(multiply(inverse(X1),sF1_fnc)))),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),sF1_fnc)=X1)),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f6082,f5886])).
% 87.92/19.04  fof(f6082,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(sF2_fnc,multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sF2_fnc,X0)))),multiply(X1,inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f6076])).
% 87.92/19.04  fof(f6094,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1_fnc))))),inverse(sF1_fnc))=multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),X1)))),multiply(X3,inverse(X1)))),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f3925])).
% 87.92/19.04  fof(f6095,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4495,f6094])).
% 87.92/19.04  fof(f6101,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(X1),multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),X0)))),multiply(X2,inverse(X0)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f6095])).
% 87.92/19.04  fof(f6393,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),sF1_fnc)),b2))))),multiply(X1,inverse(X3)))),inverse(X3)))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f3980])).
% 87.92/19.04  fof(f6394,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5246,f6393])).
% 87.92/19.04  fof(f6395,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f6394])).
% 87.92/19.04  fof(f6396,plain,(
% 87.92/19.04    ![X0,X1]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,sF2_fnc))),inverse(sF1_fnc))),b2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5939,f6395])).
% 87.92/19.04  fof(f6405,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f6408,f5750])).
% 87.92/19.04  fof(f6408,plain,(
% 87.92/19.04    ![X0,X1]: (X0=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,sF2_fnc))),sF1_fnc)),b2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f6396])).
% 87.92/19.04  fof(f7088,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(sF1_fnc))),multiply(inverse(sF1_fnc),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f4120])).
% 87.92/19.04  fof(f7089,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1)))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),multiply(inverse(sF1_fnc),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f7088])).
% 87.92/19.04  fof(f7090,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1)))=multiply(inverse(sF1_fnc),multiply(inverse(sF1_fnc),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4354,f7089])).
% 87.92/19.04  fof(f7091,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1)))=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f7090])).
% 87.92/19.04  fof(f7100,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,inverse(X1)))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f7091])).
% 87.92/19.04  fof(f7101,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,sF1_fnc))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,sF2_fnc)),multiply(X2,sF2_fnc))),inverse(X1))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f4121])).
% 87.92/19.04  fof(f7102,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,sF2_fnc)),multiply(X1,sF2_fnc))),inverse(X0))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f7101])).
% 87.92/19.04  fof(f7103,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(X0))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f7102])).
% 87.92/19.04  fof(f7104,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(sF1_fnc,inverse(X0))),multiply(inverse(sF1_fnc),inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f7103])).
% 87.92/19.04  fof(f7126,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),sF1_fnc)),sF1_fnc)))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),sF1_fnc)))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f7142,f5542])).
% 87.92/19.04  fof(f7142,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(multiply(sF1_fnc,inverse(X0))),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4354,f7104])).
% 87.92/19.04  fof(f7455,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X1)))=multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f6101,f4201])).
% 87.92/19.04  fof(f7456,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(X1)))=multiply(inverse(multiply(X2,inverse(sF1_fnc))),multiply(X2,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f7455])).
% 87.92/19.04  fof(f7457,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(X1)))=multiply(inverse(multiply(X2,sF1_fnc)),multiply(X2,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f7456])).
% 87.92/19.04  fof(f7461,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(X1)))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7100,f7457])).
% 87.92/19.04  fof(f7500,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X0)))),inverse(sF1_fnc))=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f6011,f4213])).
% 87.92/19.04  fof(f7501,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(X0)))),inverse(sF1_fnc))=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f7500])).
% 87.92/19.04  fof(f7502,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))),inverse(sF1_fnc))=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7461,f7501])).
% 87.92/19.04  fof(f7503,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))),sF1_fnc)=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f7502])).
% 87.92/19.04  fof(f8871,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))=multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc)),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f6077])).
% 87.92/19.04  fof(f8872,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))=multiply(inverse(X0),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f8871])).
% 87.92/19.04  fof(f8893,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7461,f8872])).
% 87.92/19.04  fof(f8894,plain,(
% 87.92/19.04    ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),sF1_fnc)=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5458,f6078])).
% 87.92/19.04  fof(f8895,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)),sF1_fnc)))=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f8894])).
% 87.92/19.04  fof(f8896,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc))))=X0)),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f8893,f8895])).
% 87.92/19.04  fof(f8976,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f6405])).
% 87.92/19.04  fof(f8977,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X2)))),multiply(X1,inverse(X2))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f8893,f8976])).
% 87.92/19.04  fof(f9098,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X1),sF1_fnc)))),sF1_fnc)))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f8893,f7126])).
% 87.92/19.04  fof(f9099,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(inverse(multiply(X3,inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(X1),sF1_fnc)),sF1_fnc)))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7142,f9098])).
% 87.92/19.04  fof(f9100,plain,(
% 87.92/19.04    ![X0,X1,X2,X3]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(inverse(multiply(X3,inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))),multiply(X3,inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f8893,f9099])).
% 87.92/19.04  fof(f9357,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(multiply(inverse(inverse(X2)),inverse(X1))),sF1_fnc))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f4217,f2191])).
% 87.92/19.04  fof(f9358,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(X1)),inverse(X2))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f4217,f2191])).
% 87.92/19.04  fof(f9359,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(X1))),sF1_fnc)=multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X0))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f4217,f2191])).
% 87.92/19.04  fof(f9396,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(inverse(multiply(inverse(inverse(multiply(X0,inverse(X2)))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9357,f9100])).
% 87.92/19.04  fof(f9398,plain,(
% 87.92/19.04    ![X0]: (sF1_fnc=multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(sF1_fnc,X0)))),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9357,f5659])).
% 87.92/19.04  fof(f9401,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))=multiply(inverse(multiply(inverse(inverse(X1)),inverse(multiply(inverse(X0),X1)))),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9357,f8977])).
% 87.92/19.04  fof(f9414,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))=multiply(sF1_fnc,multiply(inverse(inverse(X1)),inverse(X2))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9358])).
% 87.92/19.04  fof(f9415,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(X1))),sF1_fnc)=multiply(sF1_fnc,multiply(inverse(inverse(X1)),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9414,f9359])).
% 87.92/19.04  fof(f9457,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9415,f9396])).
% 87.92/19.04  fof(f9459,plain,(
% 87.92/19.04    ![X0]: (sF1_fnc=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,X0))),inverse(X0))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9415,f9398])).
% 87.92/19.04  fof(f9463,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9415,f9401])).
% 87.92/19.04  fof(f9476,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(inverse(sF1_fnc),X1))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))),inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f5220,f9457])).
% 87.92/19.04  fof(f9478,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),inverse(sF1_fnc))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f4217,f9457])).
% 87.92/19.04  fof(f9481,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,sF1_fnc)))),inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9476])).
% 87.92/19.04  fof(f9482,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,sF1_fnc))),inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5973,f9481])).
% 87.92/19.04  fof(f9483,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5973,f9482])).
% 87.92/19.04  fof(f9484,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9483])).
% 87.92/19.04  fof(f9485,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9484])).
% 87.92/19.04  fof(f9487,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9478])).
% 87.92/19.04  fof(f9522,plain,(
% 87.92/19.04    sF1_fnc=multiply(sF1_fnc,multiply(inverse(inverse(sF0_fnc)),inverse(a2)))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f7,f9459])).
% 87.92/19.04  fof(f9554,plain,(
% 87.92/19.04    sF1_fnc=multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),inverse(multiply(inverse(inverse(sF0_fnc)),inverse(a2)))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9522,f9459])).
% 87.92/19.04  fof(f9555,plain,(
% 87.92/19.04    sF1_fnc=multiply(sF1_fnc,multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(sF0_fnc)),inverse(a2)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9554])).
% 87.92/19.04  fof(f9556,plain,(
% 87.92/19.04    sF1_fnc=multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(sF0_fnc)),inverse(a2)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9555])).
% 87.92/19.04  fof(f9574,plain,(
% 87.92/19.04    multiply(inverse(sF1_fnc),sF1_fnc)=multiply(inverse(inverse(sF0_fnc)),inverse(a2))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9556,f7503])).
% 87.92/19.04  fof(f9579,plain,(
% 87.92/19.04    sF1_fnc=multiply(inverse(inverse(sF0_fnc)),inverse(a2))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f4217,f9574])).
% 87.92/19.04  fof(f9593,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),inverse(sF1_fnc))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9579,f9457])).
% 87.92/19.04  fof(f9594,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9593])).
% 87.92/19.04  fof(f9601,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),sF1_fnc)))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f4217,f5458])).
% 87.92/19.04  fof(f9612,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))),sF1_fnc))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9614,f9594])).
% 87.92/19.04  fof(f9613,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))),sF1_fnc))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9614,f9487])).
% 87.92/19.04  fof(f9614,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=multiply(sF1_fnc,multiply(inverse(inverse(X0)),sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f9601])).
% 87.92/19.04  fof(f9620,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,inverse(X0)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7503,f9612])).
% 87.92/19.04  fof(f9621,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,inverse(X1)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f7503,f9613])).
% 87.92/19.04  fof(f9932,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f8893,f8896])).
% 87.92/19.04  fof(f9937,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(X1),sF1_fnc)),sF1_fnc)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f8893,f9457])).
% 87.92/19.04  fof(f9963,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,X0)=multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f8896,f9932])).
% 87.92/19.04  fof(f9969,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0)))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9963,f8893])).
% 87.92/19.04  fof(f9970,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9963,f9937])).
% 87.92/19.04  fof(f9982,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))=X0)),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f8896])).
% 87.92/19.04  fof(f9983,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1))))),inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9457])).
% 87.92/19.04  fof(f9984,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9932])).
% 87.92/19.04  fof(f9989,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,inverse(X0)))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9620])).
% 87.92/19.04  fof(f9992,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,inverse(X1)))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9621])).
% 87.92/19.04  fof(f9994,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9485])).
% 87.92/19.04  fof(f10013,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0)))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f9969,f9463])).
% 87.92/19.04  fof(f10022,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f9970])).
% 87.92/19.04  fof(f10023,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0))))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f10022])).
% 87.92/19.04  fof(f10024,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f10023])).
% 87.92/19.04  fof(f10025,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X1)))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f10024])).
% 87.92/19.04  fof(f10027,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(sF1_fnc,X1))))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10028,f10025])).
% 87.92/19.04  fof(f10028,plain,(
% 87.92/19.04    ![X0,X1,X2]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X1))))),inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f9983])).
% 87.92/19.04  fof(f10029,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0))))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f9984])).
% 87.92/19.04  fof(f10042,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(X1))))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9969,f9994])).
% 87.92/19.04  fof(f10047,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))),sF1_fnc))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f10029,f10027])).
% 87.92/19.04  fof(f10049,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))=multiply(inverse(multiply(sF1_fnc,X0)),sF1_fnc))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9963,f9963])).
% 87.92/19.04  fof(f10129,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(inverse(sF0_fnc)),inverse(multiply(inverse(X0),a2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(sF1_fnc))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9579,f10028])).
% 87.92/19.04  fof(f10131,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(X0),multiply(sF1_fnc,multiply(inverse(X1),sF1_fnc))))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(X1))))),
% 87.92/19.04    inference(paramodulation,[status(thm)],[f9982,f10028])).
% 87.92/19.04  fof(f10166,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(X0))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9989,f10129])).
% 87.92/19.04  fof(f10167,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(X0))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),sF1_fnc)))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f5220,f10166])).
% 87.92/19.04  fof(f10168,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(X0))=multiply(sF1_fnc,inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0)))),sF1_fnc))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f9614,f10167])).
% 87.92/19.04  fof(f10169,plain,(
% 87.92/19.04    ![X0]: (multiply(sF1_fnc,inverse(X0))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,X0))),sF1_fnc)))))),
% 87.92/19.04    inference(forward_demodulation,[status(thm)],[f10049,f10168])).
% 87.92/19.04  fof(f10171,plain,(
% 87.92/19.04    ![X0]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))=X0)),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10224,f9982])).
% 87.92/19.04  fof(f10172,plain,(
% 87.92/19.04    ![X0,X1,X2]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X1))))),inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10224,f10028])).
% 87.92/19.04  fof(f10177,plain,(
% 87.92/19.04    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=multiply(sF1_fnc,inverse(X1)))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10224,f9992])).
% 87.92/19.04  fof(f10178,plain,(
% 87.92/19.04    ![X0,X1]: (multiply(sF1_fnc,inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10224,f10047])).
% 87.92/19.04  fof(f10179,plain,(
% 87.92/19.04    ![X0]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(sF1_fnc,X0))))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.04    inference(backward_demodulation,[status(thm)],[f10224,f10029])).
% 87.92/19.04  fof(f10183,plain,(
% 87.92/19.04    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,X1))))))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,inverse(X1))))))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10224,f10042])).
% 87.92/19.05  fof(f10207,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0)))=multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10224,f10013])).
% 87.92/19.05  fof(f10222,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc)))=multiply(sF1_fnc,multiply(inverse(inverse(X0)),sF1_fnc)))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10224,f9614])).
% 87.92/19.05  fof(f10224,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,inverse(X0))=inverse(multiply(sF1_fnc,X0)))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f9982,f10169])).
% 87.92/19.05  fof(f10235,plain,(
% 87.92/19.05    ![X0,X1]: (multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,multiply(inverse(X1),sF1_fnc))))),sF1_fnc)=multiply(sF1_fnc,multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))),inverse(X1))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10029,f10131])).
% 87.92/19.05  fof(f10236,plain,(
% 87.92/19.05    ![X0,X1]: (multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,multiply(inverse(X1),sF1_fnc))))),sF1_fnc)=multiply(sF1_fnc,multiply(inverse(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0))))),inverse(X1))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10235])).
% 87.92/19.05  fof(f10269,plain,(
% 87.92/19.05    ![X0,X1,X2]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(X1),X2))))))=multiply(sF1_fnc,multiply(inverse(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,X1))))),inverse(multiply(X0,inverse(X2))))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10172])).
% 87.92/19.05  fof(f10274,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))))))=inverse(multiply(sF1_fnc,X1)))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10177])).
% 87.92/19.05  fof(f10275,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(X0),multiply(sF1_fnc,X1)))))))=multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))),sF1_fnc))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10178])).
% 87.92/19.05  fof(f10276,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(X0),multiply(sF1_fnc,multiply(inverse(X1),sF1_fnc)))),sF1_fnc))=multiply(sF1_fnc,multiply(inverse(inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0))))),inverse(X1))))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10278,f10236])).
% 87.92/19.05  fof(f10278,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1))),sF1_fnc))=multiply(inverse(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1)))),sF1_fnc))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10029,f10275])).
% 87.92/19.05  fof(f10284,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,X1))))))=inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(X1))))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10183])).
% 87.92/19.05  fof(f10336,plain,(
% 87.92/19.05    ![X0,X1,X2]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(X1),X2))))))=inverse(multiply(inverse(multiply(inverse(X1),multiply(sF1_fnc,multiply(inverse(multiply(X0,inverse(X2))),sF1_fnc)))),sF1_fnc)))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10276,f10269])).
% 87.92/19.05  fof(f10367,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(inverse(sF1_fnc),X1))))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc)))),sF1_fnc)))),
% 87.92/19.05    inference(paramodulation,[status(thm)],[f5220,f10336])).
% 87.92/19.05  fof(f10387,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,X1))))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc)))),sF1_fnc)))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f5220,f10367])).
% 87.92/19.05  fof(f10388,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(X1)))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc)))),sF1_fnc)))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10284,f10387])).
% 87.92/19.05  fof(f10389,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(X1)))))=inverse(multiply(sF1_fnc,multiply(inverse(multiply(sF1_fnc,multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc))),sF1_fnc))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10049,f10388])).
% 87.92/19.05  fof(f10390,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(X1)))))=inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc)),sF1_fnc)))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10049,f10389])).
% 87.92/19.05  fof(f10394,plain,(
% 87.92/19.05    ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0)))),sF1_fnc)=inverse(multiply(sF1_fnc,X1)))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10411,f10274])).
% 87.92/19.05  fof(f10411,plain,(
% 87.92/19.05    ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(X0,inverse(X1)))))=multiply(inverse(multiply(X0,inverse(X1))),sF1_fnc))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10171,f10390])).
% 87.92/19.05  fof(f10435,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0)))=inverse(multiply(sF1_fnc,X0)))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10436,f10207])).
% 87.92/19.05  fof(f10436,plain,(
% 87.92/19.05    ![X0,X1]: (multiply(sF1_fnc,multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1)))=inverse(multiply(sF1_fnc,X0)))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f9415,f10394])).
% 87.92/19.05  fof(f10446,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0)))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10435,f10179])).
% 87.92/19.05  fof(f10448,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc)))=X0)),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10435,f10171])).
% 87.92/19.05  fof(f10477,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc)))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(X0)))))),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10531,f10222])).
% 87.92/19.05  fof(f10531,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,X0))=multiply(inverse(X0),sF1_fnc))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10435,f10446])).
% 87.92/19.05  fof(f10532,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))=X0)),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10531,f10448])).
% 87.92/19.05  fof(f10533,plain,(
% 87.92/19.05    ![X0]: (inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0))))=X0)),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10532])).
% 87.92/19.05  fof(f10535,plain,(
% 87.92/19.05    ![X0]: (inverse(inverse(multiply(sF1_fnc,X0)))=X0)),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10435,f10533])).
% 87.92/19.05  fof(f10604,plain,(
% 87.92/19.05    ![X0]: (inverse(multiply(sF1_fnc,inverse(multiply(sF1_fnc,X0))))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(X0)))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10531,f10477])).
% 87.92/19.05  fof(f10605,plain,(
% 87.92/19.05    ![X0]: (inverse(inverse(multiply(sF1_fnc,multiply(sF1_fnc,X0))))=multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(X0)))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10604])).
% 87.92/19.05  fof(f10606,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,X0)=multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(X0)))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10535,f10605])).
% 87.92/19.05  fof(f10607,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,X0)=inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(X0)))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10606])).
% 87.92/19.05  fof(f10608,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,X0)=inverse(multiply(sF1_fnc,inverse(X0))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10435,f10607])).
% 87.92/19.05  fof(f10609,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,X0)=inverse(inverse(multiply(sF1_fnc,X0))))),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10224,f10608])).
% 87.92/19.05  fof(f10614,plain,(
% 87.92/19.05    sF0_fnc=a2),
% 87.92/19.05    inference(backward_demodulation,[status(thm)],[f10644,f7])).
% 87.92/19.05  fof(f10644,plain,(
% 87.92/19.05    ![X0]: (multiply(sF1_fnc,X0)=X0)),
% 87.92/19.05    inference(forward_demodulation,[status(thm)],[f10535,f10609])).
% 87.92/19.05  fof(f10959,plain,(
% 87.92/19.05    $false),
% 87.92/19.05    inference(forward_subsumption_resolution,[status(thm)],[f10614,f8])).
% 87.92/19.05  % SZS output end CNFRefutation for theBenchmark.p
% 74.86/19.31  % Elapsed time: 18.709445 seconds
% 74.86/19.31  % CPU time: 71.464890 seconds
% 74.86/19.31  % Total memory used: 3.484 GB
% 74.86/19.31  % Net memory used: 3.454 GB
%------------------------------------------------------------------------------