Drodi---4.1.1.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Drodi---4.1.1
% Problem  : GRP420-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n003.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:33:39 PM UTC 2026

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

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

fof(f2,negated_conjecture,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).

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

fof(f4,plain,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    inference(cnf_transformation,[status(thm)],[f2]) ).

fof(f5,definition,
    sF1_fnc = multiply(a3,b3),
    introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).

fof(f6,definition,
    sF0_fnc = multiply(sF1_fnc,c3),
    introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).

fof(f7,definition,
    sF3_fnc = multiply(b3,c3),
    introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).

fof(f8,definition,
    sF2_fnc = multiply(a3,sF3_fnc),
    introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).

fof(f9,plain,
    sF0_fnc != sF2_fnc,
    inference(definition_folding,[],[f4,f8,f7,f6,f5]) ).

fof(f11,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X2,X4)),inverse(multiply(X3,multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X2,X4)))))))))),multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X2,X4))))) = X1,
    inference(paramodulation,[status(thm)],[f3,f3]) ).

fof(f12,plain,
    ! [X0] : inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)) = X0,
    inference(paramodulation,[status(thm)],[f7,f3]) ).

fof(f15,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)) = X0,
    inference(paramodulation,[status(thm)],[f5,f3]) ).

fof(f16,plain,
    ! [X0] : inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)) = multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc),
    inference(paramodulation,[status(thm)],[f12,f12]) ).

fof(f17,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(paramodulation,[status(thm)],[f3,f12]) ).

fof(f44,plain,
    ! [X0] : inverse(inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc))) = X0,
    inference(backward_demodulation,[status(thm)],[f17,f3]) ).

fof(f53,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(multiply(b3,inverse(multiply(X2,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc))),
    inference(paramodulation,[status(thm)],[f17,f17]) ).

fof(f60,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc)) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(paramodulation,[status(thm)],[f44,f17]) ).

fof(f65,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f12,f60]) ).

fof(f75,plain,
    ! [X0] : multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),sF3_fnc)))))))),sF2_fnc),
    inference(paramodulation,[status(thm)],[f8,f65]) ).

fof(f76,plain,
    ! [X0] : multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f5,f65]) ).

fof(f81,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),sF3_fnc)))))))),sF2_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(backward_demodulation,[status(thm)],[f75,f65]) ).

fof(f94,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),sF3_fnc)))))))),sF2_fnc) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f5,f81]) ).

fof(f98,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)) = multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc),
    inference(forward_demodulation,[status(thm)],[f76,f16]) ).

fof(f99,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = X0,
    inference(backward_demodulation,[status(thm)],[f100,f15]) ).

fof(f100,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f76,f98]) ).

fof(f108,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),sF3_fnc)))))))),sF2_fnc) = multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),X1),
    inference(paramodulation,[status(thm)],[f99,f81]) ).

fof(f128,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(backward_demodulation,[status(thm)],[f94,f81]) ).

fof(f152,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X3,X4)))))))))),multiply(X0,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X3,X4))))) = X1,
    inference(forward_demodulation,[status(thm)],[f128,f11]) ).

fof(f153,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X3,X4))))) = X1,
    inference(forward_demodulation,[status(thm)],[f128,f152]) ).

fof(f154,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f128,f153]) ).

fof(f155,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = multiply(inverse(multiply(a3,inverse(multiply(X1,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f100,f154]) ).

fof(f156,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f154,f154]) ).

fof(f159,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(paramodulation,[status(thm)],[f154,f154]) ).

fof(f168,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f154,f99]) ).

fof(f175,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f154,f159]) ).

fof(f176,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X4,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X4),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f154,f175]) ).

fof(f244,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),X1),
    inference(forward_demodulation,[status(thm)],[f94,f108]) ).

fof(f254,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))),sF1_fnc)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc))))))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f244,f100]) ).

fof(f284,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),sF1_fnc)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc))))))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f100,f254]) ).

fof(f285,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),sF1_fnc)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc))))))),
    inference(forward_demodulation,[status(thm)],[f99,f284]) ).

fof(f368,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(paramodulation,[status(thm)],[f285,f244]) ).

fof(f376,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(paramodulation,[status(thm)],[f99,f368]) ).

fof(f414,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(equality_split,[status(thm)],[f156]) ).

fof(f702,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f414,f176]) ).

fof(f833,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(backward_demodulation,[status(thm)],[f376,f702]) ).

fof(f836,plain,
    ! [X0] : multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = X0,
    inference(backward_demodulation,[status(thm)],[f376,f99]) ).

fof(f839,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(backward_demodulation,[status(thm)],[f376,f154]) ).

fof(f840,plain,
    ! [X0] : inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(backward_demodulation,[status(thm)],[f376,f100]) ).

fof(f844,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(a3,multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f376,f833]) ).

fof(f845,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,a3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f376,f844]) ).

fof(f856,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(forward_demodulation,[status(thm)],[f376,f839]) ).

fof(f857,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(forward_demodulation,[status(thm)],[f376,f856]) ).

fof(f861,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,b3)),
    inference(paramodulation,[status(thm)],[f836,f128]) ).

fof(f863,plain,
    ! [X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc)))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,b3)),
    inference(forward_demodulation,[status(thm)],[f376,f861]) ).

fof(f864,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,b3)),
    inference(forward_demodulation,[status(thm)],[f836,f863]) ).

fof(f866,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),sF1_fnc) = multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f836,f864]) ).

fof(f876,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(paramodulation,[status(thm)],[f376,f840]) ).

fof(f890,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = X0,
    inference(forward_demodulation,[status(thm)],[f836,f876]) ).

fof(f901,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = sF3_fnc,
    inference(paramodulation,[status(thm)],[f8,f890]) ).

fof(f902,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = b3,
    inference(paramodulation,[status(thm)],[f5,f890]) ).

fof(f906,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,X0)),multiply(X1,b3)),
    inference(paramodulation,[status(thm)],[f890,f128]) ).

fof(f916,plain,
    ! [X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc)))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,X0)),multiply(X1,b3)),
    inference(forward_demodulation,[status(thm)],[f376,f906]) ).

fof(f917,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(X1,X0)),multiply(X1,b3)),
    inference(forward_demodulation,[status(thm)],[f836,f916]) ).

fof(f928,plain,
    ! [X0,X1,X2,X3,X4] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X4)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X4,multiply(inverse(inverse(multiply(inverse(multiply(a3,X4)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X3,multiply(inverse(inverse(multiply(inverse(multiply(a3,X4)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),
    inference(paramodulation,[status(thm)],[f857,f857]) ).

fof(f933,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(paramodulation,[status(thm)],[f5,f857]) ).

fof(f975,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f933]) ).

fof(f976,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = X1,
    inference(forward_demodulation,[status(thm)],[f5,f975]) ).

fof(f1029,plain,
    ! [X0] : multiply(inverse(multiply(a3,sF3_fnc)),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)),multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3)),
    inference(paramodulation,[status(thm)],[f76,f917]) ).

fof(f1031,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc)),multiply(inverse(multiply(X0,X1)),b3)),
    inference(paramodulation,[status(thm)],[f917,f917]) ).

fof(f1048,plain,
    ! [X0] : multiply(inverse(sF2_fnc),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)),multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f8,f1029]) ).

fof(f1049,plain,
    ! [X0] : multiply(inverse(sF2_fnc),sF1_fnc) = multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(b3,inverse(multiply(X0,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f840,f1048]) ).

fof(f1089,plain,
    multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),sF1_fnc) = multiply(sF3_fnc,multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f901,f917]) ).

fof(f1112,plain,
    multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),sF1_fnc) = multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f902,f917]) ).

fof(f1158,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc) = multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),multiply(inverse(multiply(X0,sF3_fnc)),b3)),
    inference(paramodulation,[status(thm)],[f8,f1031]) ).

fof(f1179,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(inverse(multiply(X0,X1)),b3))),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc)),multiply(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc)),b3)),
    inference(paramodulation,[status(thm)],[f917,f1031]) ).

fof(f1469,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f376,f168]) ).

fof(f1470,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f376,f1469]) ).

fof(f1471,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f376,f1470]) ).

fof(f1474,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),
    inference(forward_demodulation,[status(thm)],[f376,f1471]) ).

fof(f1603,plain,
    ! [X0] : multiply(sF3_fnc,multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),b3)) = multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),b3)),
    inference(backward_demodulation,[status(thm)],[f1089,f866]) ).

fof(f1604,plain,
    multiply(inverse(inverse(multiply(sF3_fnc,multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),b3)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(b3,inverse(multiply(inverse(b3),b3))),
    inference(paramodulation,[status(thm)],[f1089,f836]) ).

fof(f1619,plain,
    multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)) = multiply(sF3_fnc,multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),b3)),
    inference(backward_demodulation,[status(thm)],[f1112,f1089]) ).

fof(f1640,plain,
    ! [X0] : multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)) = multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(X0))),sF1_fnc))),b3)),
    inference(forward_demodulation,[status(thm)],[f1619,f1603]) ).

fof(f1644,plain,
    ! [X0] : multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f890,f1640]) ).

fof(f1662,plain,
    ! [X0] : multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)) = multiply(X0,multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),b3)),
    inference(forward_demodulation,[status(thm)],[f840,f1644]) ).

fof(f1663,plain,
    ! [X0] : multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)) = multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),b3)),
    inference(forward_demodulation,[status(thm)],[f890,f1662]) ).

fof(f1692,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),b3))),sF1_fnc) = multiply(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))),multiply(X0,b3)),
    inference(paramodulation,[status(thm)],[f1663,f917]) ).

fof(f1711,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = X1,
    inference(forward_demodulation,[status(thm)],[f1474,f845]) ).

fof(f1939,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f1474,f928]) ).

fof(f1951,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(paramodulation,[status(thm)],[f5,f1939]) ).

fof(f2005,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,b3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f5,f1951]) ).

fof(f2006,plain,
    ! [X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f5,f2005]) ).

fof(f2150,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X3)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(a3,inverse(multiply(X3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(X3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(paramodulation,[status(thm)],[f1711,f976]) ).

fof(f2284,plain,
    multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(b3,inverse(multiply(inverse(b3),b3))),
    inference(forward_demodulation,[status(thm)],[f1619,f1604]) ).

fof(f2373,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))),multiply(X0,b3)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),b3),
    inference(paramodulation,[status(thm)],[f1692,f890]) ).

fof(f2719,plain,
    inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))))),sF1_fnc))))),sF1_fnc))),b3),
    inference(paramodulation,[status(thm)],[f1663,f2373]) ).

fof(f2753,plain,
    inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))))),sF1_fnc))))),sF1_fnc))),b3),
    inference(forward_demodulation,[status(thm)],[f2284,f2719]) ).

fof(f2797,plain,
    multiply(inverse(multiply(a3,b3)),sF1_fnc) = multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))))),sF1_fnc))))),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f2753,f917]) ).

fof(f2812,plain,
    multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3))))),sF1_fnc))))),sF1_fnc))),b3)),
    inference(forward_demodulation,[status(thm)],[f5,f2797]) ).

fof(f2813,plain,
    multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f2753,f2812]) ).

fof(f2817,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),sF1_fnc) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(paramodulation,[status(thm)],[f2813,f376]) ).

fof(f2828,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),sF1_fnc) = multiply(b3,inverse(multiply(inverse(b3),b3))),
    inference(forward_demodulation,[status(thm)],[f836,f2817]) ).

fof(f2919,plain,
    ! [X0,X1,X2,X3] : inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(multiply(b3,inverse(multiply(X2,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc))),
    inference(forward_demodulation,[status(thm)],[f76,f53]) ).

fof(f2920,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(multiply(b3,inverse(multiply(X2,inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),sF3_fnc))),
    inference(forward_demodulation,[status(thm)],[f840,f2919]) ).

fof(f2921,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),inverse(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f76,f2920]) ).

fof(f2922,plain,
    ! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X3),inverse(multiply(inverse(multiply(X1,X3)),multiply(X1,X3))))))))),multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),
    inference(forward_demodulation,[status(thm)],[f840,f2921]) ).

fof(f3765,plain,
    ! [X0] : multiply(inverse(sF2_fnc),sF1_fnc) = multiply(X0,multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3)),
    inference(paramodulation,[status(thm)],[f836,f1049]) ).

fof(f3824,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(sF2_fnc),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))))),sF1_fnc))),b3),
    inference(paramodulation,[status(thm)],[f3765,f2373]) ).

fof(f3849,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3))),sF1_fnc) = multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),multiply(X0,b3)),
    inference(paramodulation,[status(thm)],[f3765,f917]) ).

fof(f3853,plain,
    sF3_fnc = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))))),sF1_fnc))),b3),
    inference(forward_demodulation,[status(thm)],[f901,f3824]) ).

fof(f3887,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = multiply(inverse(multiply(a3,inverse(multiply(X1,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f376,f155]) ).

fof(f3888,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = multiply(inverse(multiply(a3,inverse(multiply(X1,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f376,f3887]) ).

fof(f3889,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)))) = multiply(inverse(multiply(a3,inverse(multiply(X1,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f376,f3888]) ).

fof(f3890,plain,
    ! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))))))))),multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))) = multiply(inverse(multiply(a3,inverse(multiply(X1,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f376,f3889]) ).

fof(f3891,plain,
    ! [X0] : multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f1939,f3890]) ).

fof(f4364,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),multiply(X0,b3)))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(multiply(b3,inverse(multiply(inverse(X0),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3),
    inference(paramodulation,[status(thm)],[f3849,f890]) ).

fof(f4416,plain,
    multiply(inverse(multiply(a3,b3)),sF1_fnc) = multiply(inverse(sF3_fnc),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))))),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f3853,f917]) ).

fof(f4440,plain,
    multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(sF3_fnc),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))))),sF1_fnc))),b3)),
    inference(forward_demodulation,[status(thm)],[f5,f4416]) ).

fof(f4441,plain,
    multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(sF3_fnc),sF3_fnc),
    inference(forward_demodulation,[status(thm)],[f3853,f4440]) ).

fof(f5620,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3),
    inference(paramodulation,[status(thm)],[f1158,f4364]) ).

fof(f5660,plain,
    ! [X0] : multiply(X0,b3) = multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),b3),
    inference(forward_demodulation,[status(thm)],[f890,f5620]) ).

fof(f5766,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),X1)),b3))),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc)),multiply(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc)),b3)),
    inference(paramodulation,[status(thm)],[f5660,f1179]) ).

fof(f5790,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),X1)),b3))),sF1_fnc) = multiply(inverse(multiply(a3,multiply(inverse(multiply(X0,X1)),b3))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f1179,f5766]) ).

fof(f8289,plain,
    ! [X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(inverse(multiply(X0,X1)),b3))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),X1)),b3),
    inference(paramodulation,[status(thm)],[f5790,f890]) ).

fof(f8342,plain,
    ! [X0,X1] : multiply(inverse(multiply(X0,X1)),b3) = multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X0,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),X1)),b3),
    inference(forward_demodulation,[status(thm)],[f890,f8289]) ).

fof(f8385,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(b3,inverse(multiply(inverse(inverse(multiply(X1,sF3_fnc))),inverse(multiply(c3,inverse(multiply(inverse(c3),c3)))))))),X2)),X0)),multiply(inverse(multiply(X1,X2)),b3)),
    inference(paramodulation,[status(thm)],[f8342,f917]) ).

fof(f8636,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,sF3_fnc)))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),sF1_fnc) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(b3,c3),inverse(multiply(inverse(multiply(b3,c3)),multiply(b3,c3))))))))),b3)),
    inference(paramodulation,[status(thm)],[f2922,f8385]) ).

fof(f8792,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X1)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(b3,c3),inverse(multiply(inverse(multiply(b3,c3)),multiply(b3,c3))))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f836,f8636]) ).

fof(f8793,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(X1,multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(b3,c3),inverse(multiply(inverse(multiply(b3,c3)),multiply(b3,c3))))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f890,f8792]) ).

fof(f8794,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(X1,multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(sF3_fnc,inverse(multiply(inverse(multiply(b3,c3)),multiply(b3,c3))))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f7,f8793]) ).

fof(f8795,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(X1,multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),multiply(b3,c3))))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f7,f8794]) ).

fof(f8796,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(X1,multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF3_fnc),sF3_fnc)))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f7,f8795]) ).

fof(f8797,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc) = multiply(X1,multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),b3)),
    inference(forward_demodulation,[status(thm)],[f4441,f8796]) ).

fof(f8939,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(X0,sF3_fnc))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))))),sF1_fnc))),b3),
    inference(paramodulation,[status(thm)],[f8797,f2373]) ).

fof(f9001,plain,
    ! [X0] : multiply(X0,sF3_fnc) = multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))))),sF1_fnc))),b3),
    inference(forward_demodulation,[status(thm)],[f890,f8939]) ).

fof(f19487,plain,
    ! [X0] : multiply(inverse(multiply(a3,b3)),sF1_fnc) = multiply(inverse(multiply(X0,sF3_fnc)),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))))),sF1_fnc))),b3)),
    inference(paramodulation,[status(thm)],[f9001,f917]) ).

fof(f19526,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(multiply(X0,sF3_fnc)),multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF1_fnc))),b3)))),inverse(multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))))),sF1_fnc))),b3)),
    inference(forward_demodulation,[status(thm)],[f5,f19487]) ).

fof(f19527,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(multiply(X0,sF3_fnc)),multiply(X0,sF3_fnc)),
    inference(forward_demodulation,[status(thm)],[f9001,f19526]) ).

fof(f19535,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)),multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(sF3_fnc)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),sF3_fnc)),
    inference(paramodulation,[status(thm)],[f244,f19527]) ).

fof(f19577,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(sF3_fnc)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),sF3_fnc)),
    inference(forward_demodulation,[status(thm)],[f840,f19535]) ).

fof(f19578,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)),
    inference(forward_demodulation,[status(thm)],[f244,f19577]) ).

fof(f26881,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(X0,multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f836,f19578]) ).

fof(f26924,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(X0,multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))),
    inference(forward_demodulation,[status(thm)],[f376,f26881]) ).

fof(f26985,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(multiply(inverse(inverse(multiply(inverse(multiply(a3,X2)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f2006,f2150]) ).

fof(f26986,plain,
    ! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f19578,f26985]) ).

fof(f27403,plain,
    ! [X0] : multiply(inverse(sF1_fnc),sF1_fnc) = multiply(inverse(X0),X0),
    inference(paramodulation,[status(thm)],[f836,f26924]) ).

fof(f27769,plain,
    ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
    inference(paramodulation,[status(thm)],[f27403,f27403]) ).

fof(f27858,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X0)))),sF1_fnc) = multiply(b3,inverse(multiply(inverse(b3),b3))),
    inference(paramodulation,[status(thm)],[f27403,f2828]) ).

fof(f27869,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = b3,
    inference(paramodulation,[status(thm)],[f27403,f902]) ).

fof(f28033,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(inverse(inverse(multiply(X0,inverse(multiply(inverse(X0),X0))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f27403,f128]) ).

fof(f28037,plain,
    ! [X0] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),multiply(inverse(X0),b3)),
    inference(paramodulation,[status(thm)],[f27403,f917]) ).

fof(f28170,plain,
    ! [X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))))),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f376,f28033]) ).

fof(f28171,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(X0),X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f836,f28170]) ).

fof(f28174,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(inverse(a3),a3),
    inference(equality_split,[status(thm)],[f27769]) ).

fof(f28175,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(inverse(a3),a3),
    inference(equality_split,[status(thm)],[f27769]) ).

fof(f28413,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))) = X0,
    inference(paramodulation,[status(thm)],[f28174,f890]) ).

fof(f28616,plain,
    ! [X0] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(inverse(b3),X0)),multiply(inverse(a3),a3)),
    inference(paramodulation,[status(thm)],[f28174,f917]) ).

fof(f31436,plain,
    ! [X0] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(X0),b3)),
    inference(forward_demodulation,[status(thm)],[f28175,f28037]) ).

fof(f31704,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),sF1_fnc) = multiply(b3,inverse(multiply(inverse(b3),b3))),
    inference(forward_demodulation,[status(thm)],[f28175,f27858]) ).

fof(f31705,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),sF1_fnc) = multiply(b3,inverse(multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f28175,f31704]) ).

fof(f31861,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(a3),a3))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = b3,
    inference(forward_demodulation,[status(thm)],[f28175,f27869]) ).

fof(f31862,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(a3),a3))),inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))) = b3,
    inference(forward_demodulation,[status(thm)],[f28175,f31861]) ).

fof(f31936,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(a3),a3))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f28175,f28171]) ).

fof(f31937,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(a3),a3))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(a3),a3)))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f28175,f31936]) ).

fof(f31939,plain,
    multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(inverse(a3),a3))) = multiply(inverse(a3),a3),
    inference(paramodulation,[status(thm)],[f28175,f31937]) ).

fof(f32593,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),sF1_fnc) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(multiply(inverse(a3),a3)),b3)),
    inference(paramodulation,[status(thm)],[f31939,f917]) ).

fof(f32599,plain,
    multiply(b3,inverse(multiply(inverse(a3),a3))) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(multiply(inverse(a3),a3)),b3)),
    inference(forward_demodulation,[status(thm)],[f31705,f32593]) ).

fof(f32600,plain,
    multiply(b3,inverse(multiply(inverse(a3),a3))) = multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f31436,f32599]) ).

fof(f32617,plain,
    inverse(multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))) = multiply(inverse(a3),a3),
    inference(paramodulation,[status(thm)],[f32600,f890]) ).

fof(f32654,plain,
    inverse(multiply(inverse(inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))),inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))) = multiply(inverse(a3),a3),
    inference(forward_demodulation,[status(thm)],[f28175,f32617]) ).

fof(f32655,plain,
    inverse(multiply(inverse(a3),a3)) = multiply(inverse(a3),a3),
    inference(forward_demodulation,[status(thm)],[f28175,f32654]) ).

fof(f32659,plain,
    multiply(b3,multiply(inverse(a3),a3)) = multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f32655,f32600]) ).

fof(f32661,plain,
    ! [X0,X1] : multiply(X0,inverse(multiply(inverse(a3),a3))) = multiply(inverse(multiply(X1,multiply(inverse(a3),a3))),multiply(X1,X0)),
    inference(backward_demodulation,[status(thm)],[f32655,f31937]) ).

fof(f32662,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(a3),a3))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = b3,
    inference(backward_demodulation,[status(thm)],[f32655,f31862]) ).

fof(f32665,plain,
    ! [X0] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(multiply(inverse(a3),a3),multiply(inverse(X0),b3)),
    inference(backward_demodulation,[status(thm)],[f32655,f31436]) ).

fof(f32690,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,multiply(inverse(a3),a3))),multiply(X1,X0)),
    inference(forward_demodulation,[status(thm)],[f32655,f32661]) ).

fof(f32691,plain,
    inverse(multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(b3,multiply(inverse(a3),a3))))) = b3,
    inference(forward_demodulation,[status(thm)],[f32655,f32662]) ).

fof(f32692,plain,
    inverse(multiply(multiply(inverse(a3),a3),inverse(multiply(b3,multiply(inverse(a3),a3))))) = b3,
    inference(forward_demodulation,[status(thm)],[f32655,f32691]) ).

fof(f34063,plain,
    ! [X0] : multiply(X0,multiply(inverse(a3),a3)) = multiply(inverse(multiply(inverse(X0),multiply(inverse(a3),a3))),multiply(inverse(a3),a3)),
    inference(paramodulation,[status(thm)],[f28175,f32690]) ).

fof(f37313,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = X0,
    inference(forward_demodulation,[status(thm)],[f32655,f28413]) ).

fof(f38753,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(multiply(inverse(X0),multiply(inverse(a3),a3))),b3))),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),sF1_fnc)),multiply(inverse(multiply(X0,multiply(inverse(a3),a3))),b3)),
    inference(paramodulation,[status(thm)],[f34063,f1031]) ).

fof(f38931,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(multiply(inverse(X0),multiply(inverse(a3),a3))),b3))),sF1_fnc) = multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f1031,f38753]) ).

fof(f49278,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,multiply(X0,b3))),sF1_fnc))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = multiply(inverse(multiply(inverse(X0),multiply(inverse(a3),a3))),b3),
    inference(paramodulation,[status(thm)],[f38931,f37313]) ).

fof(f49463,plain,
    ! [X0] : multiply(X0,b3) = multiply(inverse(multiply(inverse(X0),multiply(inverse(a3),a3))),b3),
    inference(forward_demodulation,[status(thm)],[f37313,f49278]) ).

fof(f49618,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(inverse(a3),a3))),X0)),multiply(X1,b3)),
    inference(paramodulation,[status(thm)],[f49463,f917]) ).

fof(f51968,plain,
    ! [X0,X1] : multiply(inverse(multiply(a3,multiply(inverse(X0),X1))),sF1_fnc) = multiply(inverse(multiply(X1,multiply(inverse(a3),a3))),multiply(X0,b3)),
    inference(paramodulation,[status(thm)],[f32690,f49618]) ).

fof(f52623,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(a3),a3)))))),sF1_fnc) = multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),sF1_fnc),
    inference(paramodulation,[status(thm)],[f49618,f51968]) ).

fof(f52845,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(a3),a3)))))),sF1_fnc) = multiply(b3,multiply(inverse(a3),a3)),
    inference(forward_demodulation,[status(thm)],[f32659,f52623]) ).

fof(f56072,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(b3,multiply(inverse(a3),a3)))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(a3),a3)))),
    inference(paramodulation,[status(thm)],[f52845,f37313]) ).

fof(f56215,plain,
    ! [X0] : inverse(multiply(inverse(a3),a3)) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(a3),a3)))),
    inference(forward_demodulation,[status(thm)],[f28175,f56072]) ).

fof(f56216,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(inverse(X0),inverse(multiply(inverse(X0),multiply(inverse(a3),a3)))),
    inference(forward_demodulation,[status(thm)],[f32655,f56215]) ).

fof(f56290,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,multiply(inverse(a3),a3))))),multiply(inverse(a3),a3)))),
    inference(paramodulation,[status(thm)],[f37313,f56216]) ).

fof(f56335,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(b3),multiply(inverse(a3),a3))))),sF1_fnc) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(a3),a3)),
    inference(paramodulation,[status(thm)],[f56216,f28616]) ).

fof(f56412,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(a3),a3))))),sF1_fnc) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(X0),b3)),
    inference(paramodulation,[status(thm)],[f56216,f917]) ).

fof(f56434,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(X0,inverse(multiply(X0,multiply(inverse(a3),a3)))),
    inference(forward_demodulation,[status(thm)],[f37313,f56290]) ).

fof(f56535,plain,
    multiply(inverse(multiply(a3,inverse(multiply(inverse(b3),multiply(inverse(a3),a3))))),sF1_fnc) = multiply(inverse(a3),a3),
    inference(forward_demodulation,[status(thm)],[f28175,f56335]) ).

fof(f56925,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(a3),a3))))),sF1_fnc) = multiply(multiply(inverse(a3),a3),multiply(inverse(X0),b3)),
    inference(forward_demodulation,[status(thm)],[f32655,f56412]) ).

fof(f56926,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),multiply(inverse(a3),a3))))),sF1_fnc) = multiply(inverse(multiply(a3,X0)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f32665,f56925]) ).

fof(f59032,plain,
    inverse(multiply(inverse(inverse(multiply(inverse(a3),a3))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = inverse(multiply(inverse(b3),multiply(inverse(a3),a3))),
    inference(paramodulation,[status(thm)],[f56535,f37313]) ).

fof(f59096,plain,
    inverse(multiply(inverse(multiply(inverse(a3),a3)),inverse(multiply(b3,multiply(inverse(a3),a3))))) = inverse(multiply(inverse(b3),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f32655,f59032]) ).

fof(f59097,plain,
    inverse(multiply(multiply(inverse(a3),a3),inverse(multiply(b3,multiply(inverse(a3),a3))))) = inverse(multiply(inverse(b3),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f32655,f59096]) ).

fof(f59098,plain,
    b3 = inverse(multiply(inverse(b3),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f32692,f59097]) ).

fof(f59197,plain,
    ! [X0] : multiply(inverse(multiply(a3,multiply(inverse(X0),inverse(b3)))),sF1_fnc) = multiply(b3,multiply(X0,b3)),
    inference(paramodulation,[status(thm)],[f59098,f51968]) ).

fof(f59203,plain,
    ! [X0] : multiply(X0,multiply(inverse(a3),a3)) = multiply(b3,multiply(inverse(b3),X0)),
    inference(paramodulation,[status(thm)],[f59098,f32690]) ).

fof(f59425,plain,
    ! [X0] : multiply(inverse(multiply(a3,X0)),sF1_fnc) = multiply(b3,multiply(inverse(b3),inverse(multiply(inverse(b3),X0)))),
    inference(backward_demodulation,[status(thm)],[f59203,f28616]) ).

fof(f59517,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(X0,inverse(multiply(b3,multiply(inverse(b3),X0)))),
    inference(paramodulation,[status(thm)],[f59203,f56434]) ).

fof(f59521,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(a3),a3)) = multiply(inverse(multiply(b3,multiply(inverse(b3),X1))),multiply(X1,X0)),
    inference(paramodulation,[status(thm)],[f59203,f32690]) ).

fof(f66401,plain,
    ! [X0] : multiply(inverse(multiply(a3,inverse(multiply(b3,multiply(inverse(b3),inverse(X0)))))),sF1_fnc) = multiply(inverse(multiply(a3,X0)),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f59203,f56926]) ).

fof(f66442,plain,
    ! [X0] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,multiply(inverse(a3),a3))))) = inverse(multiply(b3,multiply(inverse(b3),inverse(X0)))),
    inference(paramodulation,[status(thm)],[f66401,f37313]) ).

fof(f66578,plain,
    ! [X0] : X0 = inverse(multiply(b3,multiply(inverse(b3),inverse(X0)))),
    inference(forward_demodulation,[status(thm)],[f37313,f66442]) ).

fof(f66633,plain,
    ! [X0] : multiply(inverse(b3),X0) = inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f59425,f66578]) ).

fof(f66636,plain,
    ! [X0] : multiply(b3,multiply(inverse(b3),inverse(X0))) = inverse(multiply(b3,multiply(inverse(b3),X0))),
    inference(paramodulation,[status(thm)],[f66578,f66578]) ).

fof(f66659,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(a3),a3)) = multiply(X1,multiply(inverse(X1),X0)),
    inference(paramodulation,[status(thm)],[f66578,f59521]) ).

fof(f66677,plain,
    ! [X0] : multiply(X0,multiply(b3,multiply(inverse(b3),inverse(X0)))) = multiply(inverse(a3),a3),
    inference(paramodulation,[status(thm)],[f66578,f28175]) ).

fof(f66951,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f66633,f3891]) ).

fof(f66990,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(backward_demodulation,[status(thm)],[f66633,f840]) ).

fof(f66992,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),inverse(X0))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = X0,
    inference(backward_demodulation,[status(thm)],[f66633,f836]) ).

fof(f67007,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f66633,f26986]) ).

fof(f67026,plain,
    ! [X0] : multiply(inverse(b3),multiply(inverse(X0),inverse(b3))) = inverse(multiply(b3,multiply(X0,b3))),
    inference(paramodulation,[status(thm)],[f59197,f66633]) ).

fof(f67031,plain,
    multiply(inverse(b3),sF3_fnc) = inverse(multiply(inverse(sF2_fnc),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f8,f66633]) ).

fof(f67150,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f66633,f66951]) ).

fof(f67151,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f28175,f67150]) ).

fof(f67152,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f32655,f67151]) ).

fof(f67153,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f28175,f67152]) ).

fof(f67154,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f32655,f67153]) ).

fof(f67155,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f28175,f67154]) ).

fof(f67156,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f32655,f67155]) ).

fof(f67310,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f28175,f66990]) ).

fof(f67311,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(inverse(multiply(inverse(multiply(a3,X0)),sF1_fnc))),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f32655,f67310]) ).

fof(f67312,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(b3),b3))))),
    inference(forward_demodulation,[status(thm)],[f66633,f67311]) ).

fof(f67313,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))),
    inference(forward_demodulation,[status(thm)],[f28175,f67312]) ).

fof(f67314,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))),
    inference(forward_demodulation,[status(thm)],[f32655,f67313]) ).

fof(f67315,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),inverse(X0))),inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))) = X0,
    inference(forward_demodulation,[status(thm)],[f28175,f66992]) ).

fof(f67316,plain,
    ! [X0] : multiply(inverse(multiply(inverse(b3),inverse(X0))),inverse(multiply(b3,multiply(inverse(a3),a3)))) = X0,
    inference(forward_demodulation,[status(thm)],[f32655,f67315]) ).

fof(f67322,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,inverse(multiply(inverse(a3),a3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f28175,f67007]) ).

fof(f67323,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f32655,f67322]) ).

fof(f67324,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f28175,f67323]) ).

fof(f67325,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f32655,f67324]) ).

fof(f67326,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),inverse(multiply(inverse(a3),a3)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f28175,f67325]) ).

fof(f67327,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),multiply(inverse(a3),a3))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f32655,f67326]) ).

fof(f67328,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(b3),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(b3),b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f59203,f67327]) ).

fof(f67329,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(b3),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,inverse(multiply(inverse(a3),a3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f28175,f67328]) ).

fof(f67330,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(b3),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f32655,f67329]) ).

fof(f67642,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(X0,multiply(inverse(X0),inverse(multiply(inverse(a3),a3)))),
    inference(paramodulation,[status(thm)],[f28175,f66659]) ).

fof(f67644,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(inverse(X0),X1)) = multiply(X2,multiply(inverse(X2),X1)),
    inference(paramodulation,[status(thm)],[f66659,f66659]) ).

fof(f67917,plain,
    ! [X0] : multiply(inverse(a3),a3) = multiply(X0,multiply(inverse(X0),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f32655,f67642]) ).

fof(f68640,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = multiply(a3,multiply(inverse(a3),X1)),
    inference(equality_split,[status(thm)],[f67644]) ).

fof(f68641,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = multiply(a3,multiply(inverse(a3),X1)),
    inference(equality_split,[status(thm)],[f67644]) ).

fof(f68816,plain,
    ! [X0] : X0 = inverse(multiply(a3,multiply(inverse(a3),inverse(X0)))),
    inference(paramodulation,[status(thm)],[f68640,f66578]) ).

fof(f70616,plain,
    ! [X0] : multiply(X0,multiply(a3,multiply(inverse(a3),inverse(X0)))) = multiply(inverse(a3),a3),
    inference(forward_demodulation,[status(thm)],[f68641,f66677]) ).

fof(f71024,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(a3),a3)))))) = X0,
    inference(backward_demodulation,[status(thm)],[f67314,f67316]) ).

fof(f71114,plain,
    multiply(inverse(a3),a3) = multiply(a3,multiply(inverse(a3),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f68641,f67917]) ).

fof(f71377,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),inverse(X0))) = inverse(multiply(b3,multiply(inverse(b3),X0))),
    inference(forward_demodulation,[status(thm)],[f68641,f66636]) ).

fof(f71378,plain,
    ! [X0] : X0 = multiply(a3,multiply(inverse(a3),inverse(inverse(X0)))),
    inference(backward_demodulation,[status(thm)],[f71384,f68816]) ).

fof(f71384,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),inverse(X0))) = inverse(multiply(a3,multiply(inverse(a3),X0))),
    inference(forward_demodulation,[status(thm)],[f68641,f71377]) ).

fof(f71388,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),inverse(X0))) = inverse(multiply(X0,multiply(inverse(a3),a3))),
    inference(paramodulation,[status(thm)],[f66659,f71384]) ).

fof(f71743,plain,
    ! [X0] : multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(a3),a3)))) = inverse(multiply(b3,X0)),
    inference(paramodulation,[status(thm)],[f71024,f66578]) ).

fof(f71814,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(inverse(a3),a3)))),inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f67314,f67156]) ).

fof(f71815,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f67314,f71814]) ).

fof(f72166,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(backward_demodulation,[status(thm)],[f71388,f71815]) ).

fof(f72167,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),inverse(b3)))))) = X0,
    inference(backward_demodulation,[status(thm)],[f71388,f71024]) ).

fof(f72169,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(inverse(b3),X0)),multiply(a3,multiply(inverse(a3),inverse(b3)))),
    inference(backward_demodulation,[status(thm)],[f71388,f67314]) ).

fof(f72254,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))),inverse(multiply(b3,multiply(inverse(a3),a3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f71388,f72166]) ).

fof(f72255,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))),multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f71388,f72254]) ).

fof(f72257,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(inverse(multiply(inverse(b3),X0)),multiply(a3,multiply(inverse(a3),inverse(b3)))),
    inference(forward_demodulation,[status(thm)],[f71388,f72169]) ).

fof(f72608,plain,
    ! [X0] : multiply(inverse(X0),multiply(a3,multiply(inverse(a3),inverse(b3)))) = inverse(multiply(b3,X0)),
    inference(forward_demodulation,[status(thm)],[f71388,f71743]) ).

fof(f72668,plain,
    ! [X0] : multiply(X0,inverse(multiply(b3,X0))) = multiply(a3,multiply(inverse(a3),multiply(a3,multiply(inverse(a3),inverse(b3))))),
    inference(paramodulation,[status(thm)],[f72608,f68641]) ).

fof(f72999,plain,
    ! [X0] : multiply(X0,inverse(multiply(b3,X0))) = multiply(a3,inverse(multiply(b3,a3))),
    inference(forward_demodulation,[status(thm)],[f72608,f72668]) ).

fof(f73031,plain,
    multiply(c3,inverse(sF3_fnc)) = multiply(a3,inverse(multiply(b3,a3))),
    inference(paramodulation,[status(thm)],[f7,f72999]) ).

fof(f73413,plain,
    ! [X0] : multiply(X0,inverse(multiply(b3,X0))) = multiply(c3,inverse(sF3_fnc)),
    inference(backward_demodulation,[status(thm)],[f73031,f72999]) ).

fof(f73439,plain,
    ! [X0] : multiply(multiply(inverse(b3),inverse(X0)),X0) = multiply(c3,inverse(sF3_fnc)),
    inference(paramodulation,[status(thm)],[f66578,f73413]) ).

fof(f73459,plain,
    multiply(b3,inverse(b3)) = inverse(multiply(b3,multiply(c3,inverse(sF3_fnc)))),
    inference(paramodulation,[status(thm)],[f73413,f66578]) ).

fof(f73806,plain,
    ! [X0] : multiply(inverse(b3),inverse(inverse(multiply(b3,X0)))) = X0,
    inference(forward_demodulation,[status(thm)],[f72608,f72167]) ).

fof(f73880,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))) = inverse(multiply(b3,multiply(inverse(b3),X0))),
    inference(forward_demodulation,[status(thm)],[f72608,f72257]) ).

fof(f73881,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))) = inverse(multiply(a3,multiply(inverse(a3),X0))),
    inference(forward_demodulation,[status(thm)],[f68641,f73880]) ).

fof(f73882,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(a3,multiply(inverse(a3),inverse(X0))),
    inference(forward_demodulation,[status(thm)],[f71384,f73881]) ).

fof(f74055,plain,
    multiply(inverse(b3),inverse(multiply(c3,inverse(sF3_fnc)))) = multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(b3),inverse(multiply(a3,multiply(inverse(a3),inverse(b3)))))))),
    inference(paramodulation,[status(thm)],[f73439,f73882]) ).

fof(f74056,plain,
    multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(b3),inverse(multiply(inverse(a3),a3)))))) = inverse(multiply(c3,inverse(sF3_fnc))),
    inference(paramodulation,[status(thm)],[f73439,f71388]) ).

fof(f74185,plain,
    multiply(inverse(b3),inverse(multiply(c3,inverse(sF3_fnc)))) = multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(b3),multiply(a3,multiply(inverse(a3),inverse(inverse(b3)))))))),
    inference(forward_demodulation,[status(thm)],[f71384,f74055]) ).

fof(f74186,plain,
    multiply(inverse(b3),inverse(multiply(c3,inverse(sF3_fnc)))) = multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(a3),a3)))),
    inference(forward_demodulation,[status(thm)],[f70616,f74185]) ).

fof(f74187,plain,
    multiply(inverse(b3),inverse(multiply(c3,inverse(sF3_fnc)))) = multiply(a3,multiply(inverse(a3),multiply(inverse(a3),a3))),
    inference(forward_demodulation,[status(thm)],[f32655,f74186]) ).

fof(f74188,plain,
    multiply(inverse(b3),inverse(multiply(c3,inverse(sF3_fnc)))) = multiply(inverse(a3),a3),
    inference(forward_demodulation,[status(thm)],[f71114,f74187]) ).

fof(f74189,plain,
    multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(b3),multiply(inverse(a3),a3))))) = inverse(multiply(c3,inverse(sF3_fnc))),
    inference(forward_demodulation,[status(thm)],[f32655,f74056]) ).

fof(f74190,plain,
    multiply(a3,multiply(inverse(a3),multiply(a3,multiply(inverse(a3),inverse(inverse(b3)))))) = inverse(multiply(c3,inverse(sF3_fnc))),
    inference(forward_demodulation,[status(thm)],[f71388,f74189]) ).

fof(f74191,plain,
    multiply(a3,multiply(inverse(a3),b3)) = inverse(multiply(c3,inverse(sF3_fnc))),
    inference(forward_demodulation,[status(thm)],[f71378,f74190]) ).

fof(f74724,plain,
    multiply(inverse(a3),a3) = multiply(inverse(multiply(c3,inverse(sF3_fnc))),inverse(multiply(b3,multiply(inverse(a3),a3)))),
    inference(paramodulation,[status(thm)],[f74188,f59517]) ).

fof(f74738,plain,
    multiply(inverse(a3),a3) = multiply(inverse(multiply(c3,inverse(sF3_fnc))),multiply(a3,multiply(inverse(a3),inverse(b3)))),
    inference(forward_demodulation,[status(thm)],[f71388,f74724]) ).

fof(f74739,plain,
    multiply(inverse(a3),a3) = inverse(multiply(b3,multiply(c3,inverse(sF3_fnc)))),
    inference(forward_demodulation,[status(thm)],[f72608,f74738]) ).

fof(f74740,plain,
    multiply(inverse(a3),a3) = multiply(b3,inverse(b3)),
    inference(forward_demodulation,[status(thm)],[f73459,f74739]) ).

fof(f74767,plain,
    ! [X0,X1] : multiply(X0,multiply(b3,inverse(b3))) = multiply(X1,multiply(inverse(X1),X0)),
    inference(backward_demodulation,[status(thm)],[f74740,f66659]) ).

fof(f74777,plain,
    inverse(multiply(inverse(a3),a3)) = multiply(b3,inverse(b3)),
    inference(backward_demodulation,[status(thm)],[f74740,f32655]) ).

fof(f74779,plain,
    ! [X0] : multiply(inverse(X0),X0) = multiply(b3,inverse(b3)),
    inference(backward_demodulation,[status(thm)],[f74740,f28175]) ).

fof(f74798,plain,
    inverse(multiply(b3,inverse(b3))) = multiply(b3,inverse(b3)),
    inference(forward_demodulation,[status(thm)],[f74740,f74777]) ).

fof(f74861,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(b3,inverse(b3))))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)),
    inference(backward_demodulation,[status(thm)],[f74779,f128]) ).

fof(f74970,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,inverse(multiply(b3,inverse(b3))))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(b3,inverse(b3))))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f74779,f74861]) ).

fof(f74992,plain,
    multiply(inverse(b3),inverse(multiply(b3,inverse(b3)))) = inverse(b3),
    inference(paramodulation,[status(thm)],[f74798,f73806]) ).

fof(f75006,plain,
    multiply(c3,inverse(sF3_fnc)) = inverse(b3),
    inference(forward_demodulation,[status(thm)],[f73413,f74992]) ).

fof(f75013,plain,
    multiply(a3,multiply(inverse(a3),b3)) = inverse(inverse(b3)),
    inference(backward_demodulation,[status(thm)],[f75006,f74191]) ).

fof(f75016,plain,
    ! [X0] : multiply(multiply(inverse(b3),inverse(X0)),X0) = inverse(b3),
    inference(backward_demodulation,[status(thm)],[f75006,f73439]) ).

fof(f75017,plain,
    ! [X0] : multiply(X0,inverse(multiply(b3,X0))) = inverse(b3),
    inference(backward_demodulation,[status(thm)],[f75006,f73413]) ).

fof(f75019,plain,
    multiply(inverse(b3),multiply(b3,inverse(b3))) = inverse(b3),
    inference(paramodulation,[status(thm)],[f74798,f75017]) ).

fof(f75361,plain,
    ! [X0] : inverse(b3) = multiply(X0,multiply(inverse(X0),multiply(inverse(b3),inverse(multiply(b3,inverse(b3)))))),
    inference(paramodulation,[status(thm)],[f75016,f74767]) ).

fof(f75365,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(inverse(X0),X1)) = multiply(X2,multiply(inverse(X2),X1)),
    inference(paramodulation,[status(thm)],[f74767,f74767]) ).

fof(f75366,plain,
    multiply(inverse(b3),multiply(b3,inverse(b3))) = inverse(multiply(b3,multiply(inverse(b3),b3))),
    inference(paramodulation,[status(thm)],[f67026,f74767]) ).

fof(f75437,plain,
    inverse(b3) = multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(b3,inverse(b3)))))),
    inference(forward_demodulation,[status(thm)],[f68641,f75361]) ).

fof(f75438,plain,
    inverse(b3) = multiply(a3,multiply(inverse(a3),inverse(b3))),
    inference(forward_demodulation,[status(thm)],[f75017,f75437]) ).

fof(f75443,plain,
    inverse(b3) = inverse(multiply(b3,multiply(inverse(b3),b3))),
    inference(forward_demodulation,[status(thm)],[f75019,f75366]) ).

fof(f75444,plain,
    inverse(b3) = inverse(multiply(b3,multiply(b3,inverse(b3)))),
    inference(forward_demodulation,[status(thm)],[f74767,f75443]) ).

fof(f75530,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(X0,inverse(b3)))) = multiply(a3,multiply(inverse(a3),inverse(X0))),
    inference(backward_demodulation,[status(thm)],[f75438,f73882]) ).

fof(f75531,plain,
    ! [X0] : multiply(inverse(X0),inverse(b3)) = inverse(multiply(b3,X0)),
    inference(backward_demodulation,[status(thm)],[f75438,f72608]) ).

fof(f75532,plain,
    multiply(a3,multiply(inverse(a3),inverse(inverse(b3)))) = inverse(inverse(b3)),
    inference(paramodulation,[status(thm)],[f75438,f71384]) ).

fof(f75537,plain,
    b3 = inverse(inverse(b3)),
    inference(forward_demodulation,[status(thm)],[f71378,f75532]) ).

fof(f75544,plain,
    multiply(a3,multiply(inverse(a3),b3)) = b3,
    inference(backward_demodulation,[status(thm)],[f75537,f75013]) ).

fof(f75547,plain,
    ! [X0] : multiply(X0,multiply(b3,inverse(b3))) = multiply(inverse(b3),multiply(b3,X0)),
    inference(paramodulation,[status(thm)],[f75537,f74767]) ).

fof(f75556,plain,
    ! [X0] : multiply(inverse(b3),multiply(b3,X0)) = multiply(a3,multiply(inverse(a3),X0)),
    inference(paramodulation,[status(thm)],[f75537,f68641]) ).

fof(f75703,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b3,multiply(inverse(b3),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f74779,f67330]) ).

fof(f75704,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(a3,multiply(inverse(a3),multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f68641,f75703]) ).

fof(f75705,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),inverse(multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc)))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f71384,f75704]) ).

fof(f75706,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3)))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f66633,f75705]) ).

fof(f75707,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(inverse(a3),a3))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f74779,f75706]) ).

fof(f75708,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3)))))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f74779,f75707]) ).

fof(f75806,plain,
    ! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = multiply(a3,multiply(inverse(a3),X1)),
    inference(equality_split,[status(thm)],[f75365]) ).

fof(f75990,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(multiply(b3,multiply(b3,inverse(b3))))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(backward_demodulation,[status(thm)],[f75444,f75708]) ).

fof(f76005,plain,
    multiply(b3,multiply(b3,inverse(b3))) = multiply(a3,multiply(inverse(a3),inverse(inverse(b3)))),
    inference(paramodulation,[status(thm)],[f75444,f71378]) ).

fof(f76009,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(inverse(b3),X0)),inverse(b3)) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f75444,f75990]) ).

fof(f76010,plain,
    ! [X0,X1,X2] : inverse(multiply(b3,multiply(inverse(b3),X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f75531,f76009]) ).

fof(f76011,plain,
    ! [X0,X1,X2] : inverse(multiply(a3,multiply(inverse(a3),X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f75806,f76010]) ).

fof(f76012,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),inverse(X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(multiply(b3,multiply(b3,inverse(b3))))))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f71384,f76011]) ).

fof(f76013,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),inverse(X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(inverse(b3),inverse(multiply(X2,inverse(b3)))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f75444,f76012]) ).

fof(f76014,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),inverse(X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(a3,multiply(inverse(a3),inverse(X2))))))))),multiply(X1,multiply(inverse(multiply(a3,inverse(multiply(X2,inverse(b3))))),sF1_fnc))),
    inference(forward_demodulation,[status(thm)],[f75530,f76013]) ).

fof(f76049,plain,
    multiply(b3,multiply(b3,inverse(b3))) = b3,
    inference(forward_demodulation,[status(thm)],[f71378,f76005]) ).

fof(f76353,plain,
    multiply(c3,multiply(b3,inverse(b3))) = multiply(inverse(b3),sF3_fnc),
    inference(paramodulation,[status(thm)],[f7,f75547]) ).

fof(f76690,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,multiply(a3,inverse(multiply(b3,a3)))))),multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75531,f72255]) ).

fof(f76691,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(inverse(b3),inverse(multiply(X0,inverse(b3)))),multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75017,f76690]) ).

fof(f76692,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(a3,multiply(inverse(a3),inverse(X0))),multiply(a3,multiply(inverse(a3),inverse(b3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75530,f76691]) ).

fof(f76693,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(a3,multiply(inverse(a3),inverse(X0))),multiply(a3,inverse(multiply(b3,a3)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75531,f76692]) ).

fof(f76694,plain,
    ! [X0] : multiply(inverse(b3),inverse(multiply(multiply(a3,multiply(inverse(a3),inverse(X0))),inverse(b3)))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75017,f76693]) ).

fof(f76695,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),inverse(multiply(a3,multiply(inverse(a3),inverse(X0)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75530,f76694]) ).

fof(f76696,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),multiply(a3,multiply(inverse(a3),inverse(inverse(X0)))))) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f71384,f76695]) ).

fof(f76697,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),X0)) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,multiply(inverse(a3),inverse(b3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f71378,f76696]) ).

fof(f76698,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),X0)) = multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,inverse(multiply(b3,a3))))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75531,f76697]) ).

fof(f76700,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),X0)) = multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(b3))))),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f75017,f76698]) ).

fof(f76977,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(multiply(b3,multiply(b3,inverse(b3)))))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(b3,inverse(b3))))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f74798,f74970]) ).

fof(f76978,plain,
    ! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(b3))))),sF1_fnc) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(b3,inverse(b3))))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f76049,f76977]) ).

fof(f76979,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),X0)) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(b3,inverse(b3))))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f76700,f76978]) ).

fof(f76980,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),X0)) = multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,multiply(b3,inverse(b3)))))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f74798,f76979]) ).

fof(f76987,plain,
    ! [X0] : multiply(a3,multiply(inverse(a3),b3)) = multiply(inverse(inverse(b3)),multiply(inverse(multiply(X0,multiply(b3,inverse(b3)))),X0)),
    inference(paramodulation,[status(thm)],[f75017,f76980]) ).

fof(f77076,plain,
    ! [X0] : b3 = multiply(inverse(inverse(b3)),multiply(inverse(multiply(X0,multiply(b3,inverse(b3)))),X0)),
    inference(forward_demodulation,[status(thm)],[f75544,f76987]) ).

fof(f77077,plain,
    ! [X0] : b3 = multiply(b3,multiply(inverse(multiply(X0,multiply(b3,inverse(b3)))),X0)),
    inference(forward_demodulation,[status(thm)],[f75537,f77076]) ).

fof(f77368,plain,
    ! [X0] : b3 = multiply(b3,multiply(inverse(multiply(inverse(b3),multiply(b3,X0))),X0)),
    inference(paramodulation,[status(thm)],[f75547,f77077]) ).

fof(f77414,plain,
    ! [X0] : b3 = multiply(b3,multiply(inverse(multiply(a3,multiply(inverse(a3),X0))),X0)),
    inference(forward_demodulation,[status(thm)],[f75556,f77368]) ).

fof(f77415,plain,
    ! [X0] : b3 = multiply(b3,multiply(multiply(a3,multiply(inverse(a3),inverse(X0))),X0)),
    inference(forward_demodulation,[status(thm)],[f71384,f77414]) ).

fof(f77449,plain,
    ! [X0] : b3 = multiply(b3,multiply(X0,inverse(X0))),
    inference(paramodulation,[status(thm)],[f71378,f77415]) ).

fof(f77522,plain,
    ! [X0] : multiply(inverse(b3),inverse(inverse(b3))) = multiply(X0,inverse(X0)),
    inference(paramodulation,[status(thm)],[f77449,f73806]) ).

fof(f77538,plain,
    ! [X0] : multiply(inverse(b3),b3) = multiply(X0,inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f75537,f77522]) ).

fof(f77539,plain,
    ! [X0] : multiply(b3,inverse(b3)) = multiply(X0,inverse(X0)),
    inference(forward_demodulation,[status(thm)],[f74779,f77538]) ).

fof(f77548,plain,
    ! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
    inference(paramodulation,[status(thm)],[f77539,f77539]) ).

fof(f77564,plain,
    ! [X0] : multiply(c3,multiply(X0,inverse(X0))) = multiply(inverse(b3),sF3_fnc),
    inference(paramodulation,[status(thm)],[f77539,f76353]) ).

fof(f77568,plain,
    ! [X0,X1,X2] : multiply(X0,multiply(X1,inverse(X1))) = multiply(X2,multiply(inverse(X2),X0)),
    inference(paramodulation,[status(thm)],[f77539,f74767]) ).

fof(f77569,plain,
    ! [X0] : inverse(multiply(X0,inverse(X0))) = multiply(b3,inverse(b3)),
    inference(paramodulation,[status(thm)],[f77539,f74798]) ).

fof(f77593,plain,
    ! [X0] : multiply(X0,multiply(b3,inverse(b3))) = multiply(a3,multiply(inverse(a3),inverse(inverse(X0)))),
    inference(paramodulation,[status(thm)],[f77539,f75806]) ).

fof(f77638,plain,
    ! [X0] : multiply(X0,multiply(b3,inverse(b3))) = X0,
    inference(forward_demodulation,[status(thm)],[f71378,f77593]) ).

fof(f77653,plain,
    ! [X0] : multiply(X0,inverse(X0)) = multiply(a3,inverse(a3)),
    inference(equality_split,[status(thm)],[f77548]) ).

fof(f77843,plain,
    ! [X0] : multiply(X0,multiply(a3,inverse(a3))) = X0,
    inference(forward_demodulation,[status(thm)],[f77653,f77638]) ).

fof(f77852,plain,
    multiply(inverse(multiply(a3,multiply(a3,inverse(a3)))),sF1_fnc) = multiply(b3,multiply(inverse(b3),inverse(inverse(b3)))),
    inference(paramodulation,[status(thm)],[f77843,f59425]) ).

fof(f77874,plain,
    multiply(inverse(a3),sF1_fnc) = multiply(b3,multiply(inverse(b3),inverse(inverse(b3)))),
    inference(forward_demodulation,[status(thm)],[f77843,f77852]) ).

fof(f77875,plain,
    multiply(inverse(a3),sF1_fnc) = b3,
    inference(forward_demodulation,[status(thm)],[f77449,f77874]) ).

fof(f77902,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),inverse(X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),multiply(a3,multiply(inverse(a3),inverse(X2))))))))),multiply(X1,multiply(a3,multiply(inverse(a3),X2)))),
    inference(forward_demodulation,[status(thm)],[f76700,f76014]) ).

fof(f78198,plain,
    inverse(multiply(a3,inverse(a3))) = multiply(b3,inverse(b3)),
    inference(forward_demodulation,[status(thm)],[f77653,f77569]) ).

fof(f78199,plain,
    inverse(multiply(a3,inverse(a3))) = multiply(a3,inverse(a3)),
    inference(forward_demodulation,[status(thm)],[f77653,f78198]) ).

fof(f78966,plain,
    multiply(c3,multiply(a3,inverse(a3))) = multiply(inverse(b3),sF3_fnc),
    inference(forward_demodulation,[status(thm)],[f77653,f77564]) ).

fof(f78971,plain,
    c3 = inverse(multiply(inverse(sF2_fnc),sF1_fnc)),
    inference(backward_demodulation,[status(thm)],[f78972,f67031]) ).

fof(f78972,plain,
    c3 = multiply(inverse(b3),sF3_fnc),
    inference(forward_demodulation,[status(thm)],[f77843,f78966]) ).

fof(f79014,plain,
    ! [X0] : multiply(X0,multiply(b3,inverse(b3))) = multiply(multiply(inverse(sF2_fnc),sF1_fnc),multiply(c3,X0)),
    inference(paramodulation,[status(thm)],[f78971,f74767]) ).

fof(f79028,plain,
    ! [X0] : multiply(X0,multiply(a3,inverse(a3))) = multiply(multiply(inverse(sF2_fnc),sF1_fnc),multiply(c3,X0)),
    inference(forward_demodulation,[status(thm)],[f77653,f79014]) ).

fof(f79029,plain,
    ! [X0] : X0 = multiply(multiply(inverse(sF2_fnc),sF1_fnc),multiply(c3,X0)),
    inference(forward_demodulation,[status(thm)],[f77843,f79028]) ).

fof(f79154,plain,
    inverse(c3) = multiply(multiply(inverse(sF2_fnc),sF1_fnc),multiply(a3,inverse(a3))),
    inference(paramodulation,[status(thm)],[f77653,f79029]) ).

fof(f79166,plain,
    inverse(c3) = multiply(inverse(sF2_fnc),sF1_fnc),
    inference(forward_demodulation,[status(thm)],[f77843,f79154]) ).

fof(f79180,plain,
    multiply(sF2_fnc,inverse(c3)) = multiply(a3,multiply(inverse(a3),sF1_fnc)),
    inference(paramodulation,[status(thm)],[f79166,f75806]) ).

fof(f79186,plain,
    multiply(sF2_fnc,inverse(c3)) = multiply(a3,b3),
    inference(forward_demodulation,[status(thm)],[f77875,f79180]) ).

fof(f79187,plain,
    multiply(sF2_fnc,inverse(c3)) = sF1_fnc,
    inference(forward_demodulation,[status(thm)],[f5,f79186]) ).

fof(f79287,plain,
    ! [X0,X1] : multiply(X0,multiply(a3,inverse(a3))) = multiply(X1,multiply(inverse(X1),X0)),
    inference(forward_demodulation,[status(thm)],[f77653,f77568]) ).

fof(f79291,plain,
    ! [X0] : X0 = inverse(inverse(X0)),
    inference(backward_demodulation,[status(thm)],[f79319,f66578]) ).

fof(f79296,plain,
    ! [X0,X1,X2] : multiply(a3,multiply(inverse(a3),inverse(X0))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),inverse(X2))))))),multiply(X1,multiply(a3,multiply(inverse(a3),X2)))),
    inference(backward_demodulation,[status(thm)],[f79319,f77902]) ).

fof(f79319,plain,
    ! [X0,X1] : X0 = multiply(X1,multiply(inverse(X1),X0)),
    inference(forward_demodulation,[status(thm)],[f77843,f79287]) ).

fof(f79370,plain,
    ! [X0,X1,X2] : inverse(X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,multiply(inverse(a3),inverse(X2))))))),multiply(X1,multiply(a3,multiply(inverse(a3),X2)))),
    inference(forward_demodulation,[status(thm)],[f79319,f79296]) ).

fof(f79371,plain,
    ! [X0,X1,X2] : inverse(X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(X2))))),multiply(X1,multiply(a3,multiply(inverse(a3),X2)))),
    inference(forward_demodulation,[status(thm)],[f79319,f79370]) ).

fof(f79372,plain,
    ! [X0,X1,X2] : inverse(X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(X2))))),multiply(X1,X2)),
    inference(forward_demodulation,[status(thm)],[f79319,f79371]) ).

fof(f79683,plain,
    ! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(a3,inverse(a3)))))),multiply(X1,multiply(a3,inverse(a3)))),
    inference(paramodulation,[status(thm)],[f78199,f79372]) ).

fof(f79773,plain,
    ! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,inverse(inverse(X0)))),multiply(X1,multiply(a3,inverse(a3)))),
    inference(forward_demodulation,[status(thm)],[f77843,f79683]) ).

fof(f79774,plain,
    ! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),multiply(X1,multiply(a3,inverse(a3)))),
    inference(forward_demodulation,[status(thm)],[f79291,f79773]) ).

fof(f79775,plain,
    ! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),X1),
    inference(forward_demodulation,[status(thm)],[f77843,f79774]) ).

fof(f80138,plain,
    inverse(inverse(c3)) = multiply(inverse(sF1_fnc),sF2_fnc),
    inference(paramodulation,[status(thm)],[f79187,f79775]) ).

fof(f80203,plain,
    c3 = multiply(inverse(sF1_fnc),sF2_fnc),
    inference(forward_demodulation,[status(thm)],[f79291,f80138]) ).

fof(f80252,plain,
    sF2_fnc = multiply(sF1_fnc,c3),
    inference(paramodulation,[status(thm)],[f80203,f79319]) ).

fof(f80258,plain,
    sF2_fnc = sF0_fnc,
    inference(forward_demodulation,[status(thm)],[f6,f80252]) ).

fof(f80259,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[f80258,f9]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP420-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36  % Computer : n003.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Sun Sep 20 20:14:45 UTC 2026
% 0.10/0.36  % CPUTime  : 
% 0.10/0.37  % Drodi V4.1.1
% 158.61/20.44  % Refutation found
% 158.61/20.44  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 158.61/20.44  % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.16/20.73  % Elapsed time: 20.351070 seconds
% 10.16/20.73  % CPU time: 160.167637 seconds
% 10.16/20.73  % Total memory used: 1.985 GB
% 10.16/20.73  % Net memory used: 1.952 GB
%------------------------------------------------------------------------------