%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP430-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:36:37 PM UTC 2026
% Result : Unsatisfiable 3.37s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP430-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 20 20:10:50 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 3.37/0.87 % Refutation found
% 3.37/0.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.37/0.87 % SZS output start CNFRefutation for theBenchmark
% 3.37/0.87 fof(f1,axiom,(
% 3.37/0.87 (![A,B,C,D]: (multiply(A,inverse(multiply(B,multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,B))),A)))) = D ))),
% 3.37/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.37/0.87 fof(f2,negated_conjecture,(
% 3.37/0.87 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 3.37/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.37/0.87 fof(f3,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X0))))=X3)),
% 3.37/0.87 inference(cnf_transformation,[status(thm)],[f1])).
% 3.37/0.87 fof(f4,plain,(
% 3.37/0.87 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 3.37/0.87 inference(cnf_transformation,[status(thm)],[f2])).
% 3.37/0.87 fof(f5,definition,(
% 3.37/0.87 sF1_fnc=inverse(a1)),
% 3.37/0.87 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.37/0.87 fof(f6,definition,(
% 3.37/0.87 sF0_fnc=multiply(sF1_fnc,a1)),
% 3.37/0.87 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.37/0.87 fof(f7,definition,(
% 3.37/0.87 sF3_fnc=inverse(b1)),
% 3.37/0.87 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 3.37/0.87 fof(f8,definition,(
% 3.37/0.87 sF2_fnc=multiply(sF3_fnc,b1)),
% 3.37/0.87 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.37/0.87 fof(f9,plain,(
% 3.37/0.87 ~sF0_fnc=sF2_fnc),
% 3.37/0.87 inference(definition_folding,[],[f4,f8,f7,f6,f5])).
% 3.37/0.87 fof(f11,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))),multiply(X2,X0))))=X3)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f3,f3])).
% 3.37/0.87 fof(f12,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),X0))))=X2)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f7,f3])).
% 3.37/0.87 fof(f13,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),X0))))=X2)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f5,f3])).
% 3.37/0.87 fof(f16,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X4))),multiply(multiply(multiply(X5,inverse(X5)),inverse(X3)),X0))))=X4)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f3,f3])).
% 3.37/0.87 fof(f19,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),multiply(b1,sF3_fnc)),multiply(X1,X0))))=X2)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f12,f12])).
% 3.37/0.87 fof(f31,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X2))),multiply(a1,sF1_fnc)),multiply(X1,X0))))=X2)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f13,f13])).
% 3.37/0.87 fof(f34,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(b1,multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),X0))))=sF3_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f8,f13])).
% 3.37/0.87 fof(f35,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc)),X0))))=sF1_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f6,f13])).
% 3.37/0.87 fof(f121,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),multiply(a1,sF1_fnc)),multiply(sF3_fnc,X0))))=b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f34,f13])).
% 3.37/0.87 fof(f143,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc)),multiply(a1,sF1_fnc)),multiply(sF1_fnc,X0))))=a1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f35,f13])).
% 3.37/0.87 fof(f164,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X3))),multiply(X4,inverse(X4))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f13,f11])).
% 3.37/0.87 fof(f166,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,X3))),multiply(X5,inverse(X5))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f3,f11])).
% 3.37/0.87 fof(f184,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(sF1_fnc,X1))),multiply(X2,inverse(X2))),sF0_fnc)))=X1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f6,f11])).
% 3.37/0.87 fof(f271,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(X4,inverse(X4))),X0))))=multiply(X3,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f11,f19])).
% 3.37/0.87 fof(f273,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(sF3_fnc,multiply(b1,sF3_fnc)),multiply(b1,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f34,f19])).
% 3.37/0.87 fof(f274,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(X2,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X2))),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f13,f19])).
% 3.37/0.87 fof(f302,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1))),multiply(b1,sF3_fnc)),X0))))=multiply(X3,multiply(X4,inverse(X4))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f19,f11])).
% 3.37/0.87 fof(f303,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X3))),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f19,f3])).
% 3.37/0.87 fof(f330,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),multiply(b1,sF3_fnc))))),multiply(b1,sF3_fnc))=multiply(X1,multiply(X2,inverse(X2))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f303,f302])).
% 3.37/0.87 fof(f332,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc))=multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))),multiply(X3,inverse(X3))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f303,f166])).
% 3.37/0.87 fof(f334,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,X1))),multiply(X2,inverse(X2))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f303,f164])).
% 3.37/0.87 fof(f348,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(sF1_fnc,X1))),multiply(b1,sF3_fnc)),sF0_fnc)))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f376,f184])).
% 3.37/0.87 fof(f354,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(b1,sF3_fnc)),X0))))=multiply(X3,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f376,f271])).
% 3.37/0.87 fof(f376,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,multiply(b1,sF3_fnc))=multiply(X0,multiply(X1,inverse(X1))))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f12,f330])).
% 3.37/0.87 fof(f380,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc))=multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f376,f332])).
% 3.37/0.87 fof(f416,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,X1))),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f376,f334])).
% 3.37/0.87 fof(f423,plain,(
% 3.37/0.87 ![X0]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(sF1_fnc,X0))),multiply(b1,sF3_fnc)),sF0_fnc)))=X0)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f380,f348])).
% 3.37/0.87 fof(f424,plain,(
% 3.37/0.87 ![X0]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(sF1_fnc,X0))),multiply(b1,sF3_fnc)),sF0_fnc)))=X0)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f416,f423])).
% 3.37/0.87 fof(f438,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),multiply(b1,sF3_fnc)),X0))))=multiply(X2,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f380,f354])).
% 3.37/0.87 fof(f439,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),multiply(b1,sF3_fnc)),X0))))=multiply(X2,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f416,f438])).
% 3.37/0.87 fof(f580,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X2)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X3)))=sF1_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f16,f35])).
% 3.37/0.87 fof(f581,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X2)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X3)))=sF3_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f16,f34])).
% 3.37/0.87 fof(f618,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,multiply(b1,sF3_fnc))=multiply(X0,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f5,f376])).
% 3.37/0.87 fof(f627,plain,(
% 3.37/0.87 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(b1,sF3_fnc)))),multiply(multiply(multiply(X4,inverse(X4)),inverse(X3)),X0))))=multiply(X5,inverse(X5)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f376,f16])).
% 3.37/0.87 fof(f643,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(sF3_fnc,multiply(a1,sF1_fnc)),multiply(b1,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f618,f273])).
% 3.37/0.87 fof(f674,plain,(
% 3.37/0.87 ![X0]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(sF1_fnc,X0))),multiply(a1,sF1_fnc)),sF0_fnc)))=X0)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f618,f424])).
% 3.37/0.87 fof(f694,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),multiply(a1,sF1_fnc)),X0))))=multiply(X2,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f618,f439])).
% 3.37/0.87 fof(f698,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b1,sF3_fnc)),multiply(X2,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X2))),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f618,f274])).
% 3.37/0.87 fof(f738,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),multiply(multiply(multiply(b1,sF3_fnc),inverse(X2)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X3)))=sF3_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f814,f581])).
% 3.37/0.87 fof(f739,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),multiply(multiply(multiply(b1,sF3_fnc),inverse(X2)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X3)))=sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f814,f580])).
% 3.37/0.87 fof(f814,plain,(
% 3.37/0.87 ![X0]: (multiply(b1,sF3_fnc)=multiply(X0,inverse(X0)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f16,f627])).
% 3.37/0.87 fof(f837,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(sF3_fnc,multiply(a1,sF1_fnc)),multiply(b1,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f618,f643])).
% 3.37/0.87 fof(f874,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),multiply(a1,sF1_fnc)),X0))))=multiply(X2,multiply(b1,sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f618,f694])).
% 3.37/0.87 fof(f875,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),multiply(a1,sF1_fnc)),X0))))=multiply(X2,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f618,f874])).
% 3.37/0.87 fof(f879,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(X2,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X2))),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f618,f698])).
% 3.37/0.87 fof(f915,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(b1,sF3_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X2)))=sF3_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f814,f738])).
% 3.37/0.87 fof(f916,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(b1,sF3_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X2)))=sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f814,f739])).
% 3.37/0.87 fof(f985,plain,(
% 3.37/0.87 multiply(b1,sF3_fnc)=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f5,f814])).
% 3.37/0.87 fof(f986,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF1_fnc,multiply(multiply(b1,sF3_fnc),X0))))=a1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f814,f13])).
% 3.37/0.87 fof(f987,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(b1,sF3_fnc),X0))))=b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f814,f12])).
% 3.37/0.87 fof(f992,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF3_fnc))),X0))))=X1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f814,f13])).
% 3.37/0.87 fof(f994,plain,(
% 3.37/0.87 ![X0]: (multiply(a1,sF1_fnc)=multiply(X0,inverse(X0)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f985,f814])).
% 3.37/0.87 fof(f1029,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X2)))=sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f985,f916])).
% 3.37/0.87 fof(f1030,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X2)))=sF3_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f985,f915])).
% 3.37/0.87 fof(f1104,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),X0))))=a1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f986])).
% 3.37/0.87 fof(f1105,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),X0))))=b1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f987])).
% 3.37/0.87 fof(f1111,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))),X0))))=X1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f992])).
% 3.37/0.87 fof(f1112,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0))))=X1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f814,f1111])).
% 3.37/0.87 fof(f1113,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(a1,sF1_fnc),X0))))=X1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f1112])).
% 3.37/0.87 fof(f1166,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X2)))=sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f1029])).
% 3.37/0.87 fof(f1167,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X0))),X2))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X2)))=sF3_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f985,f1030])).
% 3.37/0.87 fof(f1210,plain,(
% 3.37/0.87 multiply(inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(multiply(sF1_fnc,a1)))=a1),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1104,f1104])).
% 3.37/0.87 fof(f1214,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc))))=a1),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1104])).
% 3.37/0.87 fof(f1220,plain,(
% 3.37/0.87 multiply(inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(sF0_fnc))=a1),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f6,f1210])).
% 3.37/0.87 fof(f1222,plain,(
% 3.37/0.87 multiply(inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(multiply(sF3_fnc,b1)))=b1),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1105,f1105])).
% 3.37/0.87 fof(f1227,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(sF3_fnc,multiply(a1,sF1_fnc))))=b1),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1105])).
% 3.37/0.87 fof(f1234,plain,(
% 3.37/0.87 multiply(inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(sF2_fnc))=b1),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f8,f1222])).
% 3.37/0.87 fof(f1238,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(multiply(inverse(X1),X0)))=X1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f1113])).
% 3.37/0.87 fof(f1244,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(X0),multiply(a1,sF1_fnc))))=X0)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1113])).
% 3.37/0.87 fof(f1245,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(X1,X0))))=inverse(X1))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f13])).
% 3.37/0.87 fof(f1246,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),inverse(multiply(sF3_fnc,X0)))=b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f1105])).
% 3.37/0.87 fof(f1268,plain,(
% 3.37/0.87 ![X0]: (X0=inverse(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f13,f1245])).
% 3.37/0.87 fof(f1274,plain,(
% 3.37/0.87 multiply(sF3_fnc,inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=inverse(b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f985,f1245])).
% 3.37/0.87 fof(f1284,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(X0),inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=inverse(X0))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1245])).
% 3.37/0.87 fof(f1294,plain,(
% 3.37/0.87 multiply(sF3_fnc,inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=sF3_fnc),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f7,f1274])).
% 3.37/0.87 fof(f1411,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(b1)),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1234,f31])).
% 3.37/0.87 fof(f1412,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(a1)),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1220,f31])).
% 3.37/0.87 fof(f1422,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(inverse(X1))),multiply(a1,sF1_fnc)),multiply(X2,X0))))=inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(X1,X2))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1245,f31])).
% 3.37/0.87 fof(f1423,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(a1,sF1_fnc)),multiply(X2,X0))))=inverse(multiply(inverse(X1),multiply(multiply(a1,sF1_fnc),X2))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f31])).
% 3.37/0.87 fof(f1428,plain,(
% 3.37/0.87 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(X1)),multiply(a1,sF1_fnc)),multiply(X2,X0))))=inverse(multiply(X3,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X3))),X2))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f13,f31])).
% 3.37/0.87 fof(f1429,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))),multiply(a1,sF1_fnc)),multiply(X1,X0))))=inverse(X1))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f31])).
% 3.37/0.87 fof(f1438,plain,(
% 3.37/0.87 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,X0))),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=X0)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f985,f31])).
% 3.37/0.87 fof(f1449,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(X0),inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,X1))),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=X1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f31])).
% 3.37/0.87 fof(f1465,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF3_fnc),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f7,f1411])).
% 3.37/0.87 fof(f1466,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF1_fnc),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f1412])).
% 3.37/0.87 fof(f1473,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(a1,sF1_fnc),X0)))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1423,f31])).
% 3.37/0.87 fof(f1474,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(inverse(X0)),multiply(multiply(a1,sF1_fnc),X1)))=inverse(multiply(multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)),multiply(X0,X1))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1423,f1422])).
% 3.37/0.87 fof(f1477,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF0_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))=a1),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1423,f143])).
% 3.37/0.87 fof(f1478,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF2_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc)))=b1),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1423,f121])).
% 3.37/0.87 fof(f1579,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1588,f1167])).
% 3.37/0.87 fof(f1580,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1588,f1166])).
% 3.37/0.87 fof(f1588,plain,(
% 3.37/0.87 ![X0,X1,X2]: (inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1)))=inverse(multiply(X2,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,X2))),X1))))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1423,f1428])).
% 3.37/0.87 fof(f1589,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),X0)))=inverse(X0))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1423,f1429])).
% 3.37/0.87 fof(f1602,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(X0),inverse(multiply(inverse(inverse(a1)),multiply(multiply(a1,sF1_fnc),sF1_fnc))))=inverse(X0))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1474,f1284])).
% 3.37/0.87 fof(f1603,plain,(
% 3.37/0.87 multiply(sF3_fnc,inverse(multiply(inverse(inverse(a1)),multiply(multiply(a1,sF1_fnc),sF1_fnc))))=sF3_fnc),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1474,f1294])).
% 3.37/0.87 fof(f1699,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(X0),inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc))))=inverse(X0))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f1602])).
% 3.37/0.87 fof(f1700,plain,(
% 3.37/0.87 multiply(sF3_fnc,inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc))))=sF3_fnc),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f1603])).
% 3.37/0.87 fof(f1736,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(X0,multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X0)))))=multiply(multiply(a1,sF1_fnc),X1))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1473,f1473])).
% 3.37/0.87 fof(f1742,plain,(
% 3.37/0.87 inverse(multiply(inverse(a1),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))))=inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1214,f1473])).
% 3.37/0.87 fof(f1751,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc)))),X1)),X0))=X1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f1473])).
% 3.37/0.87 fof(f1754,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(multiply(inverse(multiply(a1,sF1_fnc)),X0)),multiply(a1,sF1_fnc)))=X0)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1473])).
% 3.37/0.87 fof(f1756,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(X0,multiply(a1,sF1_fnc))))=multiply(inverse(multiply(X1,X0)),multiply(multiply(a1,sF1_fnc),X1)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1473,f1244])).
% 3.37/0.87 fof(f1769,plain,(
% 3.37/0.87 inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))))=inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f1742])).
% 3.37/0.87 fof(f1776,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),a1)=inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1736,f1769])).
% 3.37/0.87 fof(f1795,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(a1,multiply(a1,sF1_fnc))))=multiply(inverse(sF0_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1477,f1244])).
% 3.37/0.87 fof(f1797,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF0_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)),a1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1477,f994])).
% 3.37/0.87 fof(f1800,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(b1,multiply(a1,sF1_fnc))))=multiply(inverse(sF2_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1478,f1244])).
% 3.37/0.87 fof(f1802,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF2_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc)),b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1478,f994])).
% 3.37/0.87 fof(f1812,plain,(
% 3.37/0.87 multiply(a1,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),multiply(multiply(a1,sF1_fnc),a1)),multiply(a1,sF1_fnc)),sF0_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1776,f674])).
% 3.37/0.87 fof(f1814,plain,(
% 3.37/0.87 ![X0]: (multiply(a1,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),multiply(a1,sF1_fnc)),sF0_fnc)))=inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),sF1_fnc))))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f674])).
% 3.37/0.87 fof(f1829,plain,(
% 3.37/0.87 inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc)))=inverse(inverse(multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f994,f1589])).
% 3.37/0.87 fof(f1832,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))))=multiply(multiply(a1,sF1_fnc),X0))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1589,f1473])).
% 3.37/0.87 fof(f1833,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(X0),multiply(a1,sF1_fnc))))=multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),X0)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1589,f1244])).
% 3.37/0.87 fof(f1839,plain,(
% 3.37/0.87 ![X0]: (multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(a1,sF1_fnc)),X0))=X0)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1846,f1754])).
% 3.37/0.87 fof(f1841,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))=inverse(inverse(multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1846,f1829])).
% 3.37/0.87 fof(f1846,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(X0),multiply(a1,sF1_fnc)))=multiply(multiply(a1,sF1_fnc),X0))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f994,f1832])).
% 3.37/0.87 fof(f1849,plain,(
% 3.37/0.87 ![X0]: (X0=multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),X0)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1244,f1833])).
% 3.37/0.87 fof(f1863,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(a1,sF1_fnc))))),X1)),X0))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1751])).
% 3.37/0.87 fof(f1876,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF1_fnc),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF1_fnc,inverse(inverse(multiply(a1,sF1_fnc))))),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1466])).
% 3.37/0.87 fof(f1877,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF3_fnc),multiply(a1,sF1_fnc)),multiply(inverse(multiply(sF3_fnc,inverse(inverse(multiply(a1,sF1_fnc))))),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1465])).
% 3.37/0.87 fof(f1889,plain,(
% 3.37/0.87 ![X0]: (X0=inverse(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,inverse(inverse(multiply(a1,sF1_fnc))))))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1268])).
% 3.37/0.87 fof(f1893,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(a1,sF1_fnc))))),inverse(multiply(sF3_fnc,X0)))=b1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1246])).
% 3.37/0.87 fof(f1896,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(a1,sF1_fnc))))),inverse(multiply(inverse(X1),X0)))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1841,f1238])).
% 3.37/0.87 fof(f1906,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))=multiply(inverse(multiply(a1,sF1_fnc)),X0))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1113,f1849])).
% 3.37/0.87 fof(f1907,plain,(
% 3.37/0.87 inverse(multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))=multiply(inverse(multiply(a1,sF1_fnc)),b1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1105,f1849])).
% 3.37/0.87 fof(f1908,plain,(
% 3.37/0.87 inverse(multiply(sF1_fnc,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))=multiply(inverse(multiply(a1,sF1_fnc)),a1)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1104,f1849])).
% 3.37/0.87 fof(f1913,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(multiply(inverse(multiply(a1,sF1_fnc)),X0),inverse(multiply(inverse(X1),X0)))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1919,f1896])).
% 3.37/0.87 fof(f1914,plain,(
% 3.37/0.87 ![X0]: (multiply(multiply(inverse(multiply(a1,sF1_fnc)),X0),inverse(multiply(sF3_fnc,X0)))=b1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1919,f1893])).
% 3.37/0.87 fof(f1917,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(multiply(multiply(inverse(multiply(a1,sF1_fnc)),X0),X1)),X0))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1919,f1863])).
% 3.37/0.87 fof(f1919,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(inverse(X0),inverse(inverse(multiply(a1,sF1_fnc)))))=multiply(inverse(multiply(a1,sF1_fnc)),X0))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1841,f1906])).
% 3.37/0.87 fof(f1924,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF3_fnc),multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),b1),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1931,f1877])).
% 3.37/0.87 fof(f1931,plain,(
% 3.37/0.87 inverse(multiply(sF3_fnc,inverse(inverse(multiply(a1,sF1_fnc)))))=multiply(inverse(multiply(a1,sF1_fnc)),b1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1841,f1907])).
% 3.37/0.87 fof(f1936,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),sF1_fnc),multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),a1),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f1943,f1876])).
% 3.37/0.87 fof(f1943,plain,(
% 3.37/0.87 inverse(multiply(sF1_fnc,inverse(inverse(multiply(a1,sF1_fnc)))))=multiply(inverse(multiply(a1,sF1_fnc)),a1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1841,f1908])).
% 3.37/0.87 fof(f1946,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),b1)=inverse(multiply(sF3_fnc,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1227,f1839])).
% 3.37/0.87 fof(f1972,plain,(
% 3.37/0.87 inverse(multiply(b1,multiply(a1,sF1_fnc)))=multiply(multiply(a1,sF1_fnc),multiply(inverse(sF2_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1478,f1846])).
% 3.37/0.87 fof(f1973,plain,(
% 3.37/0.87 inverse(multiply(a1,multiply(a1,sF1_fnc)))=multiply(multiply(a1,sF1_fnc),multiply(inverse(sF0_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1477,f1846])).
% 3.37/0.87 fof(f2001,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(a1,sF1_fnc)),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),multiply(multiply(a1,sF1_fnc),X2)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1473,f1913])).
% 3.37/0.87 fof(f2082,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(X0,multiply(a1,sF1_fnc)))=multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(multiply(inverse(multiply(a1,sF1_fnc)),X1),X0)),X1)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1917,f1846])).
% 3.37/0.87 fof(f2278,plain,(
% 3.37/0.87 inverse(multiply(multiply(multiply(a1,sF1_fnc),b1),multiply(multiply(a1,sF1_fnc),sF3_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1946,f1473])).
% 3.37/0.87 fof(f2286,plain,(
% 3.37/0.87 multiply(multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))),inverse(sF3_fnc))=b1),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1700,f1914])).
% 3.37/0.87 fof(f2287,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF3_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc)))=inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f1700,f1473])).
% 3.37/0.87 fof(f2289,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(sF3_fnc))=b1),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1699,f2286])).
% 3.37/0.87 fof(f2296,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),b1)=inverse(sF3_fnc)),
% 3.37/0.87 inference(paramodulation,[status(thm)],[f2289,f1839])).
% 3.37/0.87 fof(f2304,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF3_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2296,f2278])).
% 3.37/0.87 fof(f2313,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2304,f2287])).
% 3.37/0.87 fof(f2314,plain,(
% 3.37/0.87 multiply(sF3_fnc,multiply(a1,sF1_fnc))=sF3_fnc),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2313,f1700])).
% 3.37/0.87 fof(f2315,plain,(
% 3.37/0.87 ![X0]: (multiply(inverse(X0),multiply(a1,sF1_fnc))=inverse(X0))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2313,f1699])).
% 3.37/0.87 fof(f2320,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF3_fnc,multiply(b1,X0))))=multiply(multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2314,f837])).
% 3.37/0.87 fof(f2321,plain,(
% 3.37/0.87 ![X0]: (inverse(inverse(X0))=multiply(multiply(a1,sF1_fnc),X0))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2315,f1846])).
% 3.37/0.87 fof(f2329,plain,(
% 3.37/0.87 ![X0]: (inverse(inverse(multiply(inverse(multiply(a1,sF1_fnc)),X0)))=X0)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1839])).
% 3.37/0.87 fof(f2334,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),inverse(inverse(X0))))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1473])).
% 3.37/0.87 fof(f2343,plain,(
% 3.37/0.87 multiply(a1,inverse(multiply(multiply(multiply(multiply(a1,sF1_fnc),inverse(inverse(a1))),multiply(a1,sF1_fnc)),sF0_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1812])).
% 3.37/0.87 fof(f2349,plain,(
% 3.37/0.87 inverse(multiply(a1,multiply(a1,sF1_fnc)))=inverse(inverse(multiply(inverse(sF0_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1973])).
% 3.37/0.87 fof(f2350,plain,(
% 3.37/0.87 inverse(multiply(b1,multiply(a1,sF1_fnc)))=inverse(inverse(multiply(inverse(sF2_fnc),multiply(multiply(a1,sF1_fnc),sF3_fnc))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1972])).
% 3.37/0.87 fof(f2353,plain,(
% 3.37/0.87 ![X0,X1]: (inverse(multiply(X0,multiply(a1,sF1_fnc)))=inverse(inverse(multiply(inverse(multiply(multiply(inverse(multiply(a1,sF1_fnc)),X1),X0)),X1))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f2082])).
% 3.37/0.87 fof(f2396,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(sF1_fnc)),multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),a1),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1936])).
% 3.37/0.87 fof(f2400,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc))),a1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1797])).
% 3.37/0.87 fof(f2402,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(a1,multiply(a1,sF1_fnc))))=multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1795])).
% 3.37/0.87 fof(f2414,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(sF3_fnc)),multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),b1),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1924])).
% 3.37/0.87 fof(f2417,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc))),b1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1802])).
% 3.37/0.87 fof(f2419,plain,(
% 3.37/0.87 multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(b1,multiply(a1,sF1_fnc))))=multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1800])).
% 3.37/0.87 fof(f2425,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),inverse(inverse(inverse(sF0_fnc)))))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1580])).
% 3.37/0.87 fof(f2430,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF3_fnc,multiply(b1,X0))))=multiply(inverse(inverse(inverse(sF2_fnc))),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f2320])).
% 3.37/0.87 fof(f2431,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),inverse(inverse(inverse(sF2_fnc)))))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1579])).
% 3.37/0.87 fof(f2435,plain,(
% 3.37/0.87 ![X0]: (multiply(sF3_fnc,inverse(multiply(multiply(inverse(inverse(inverse(multiply(b1,X0)))),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=X0)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1438])).
% 3.37/0.87 fof(f2441,plain,(
% 3.37/0.87 ![X0]: (X0=inverse(inverse(inverse(inverse(multiply(X0,inverse(inverse(multiply(a1,sF1_fnc)))))))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1889])).
% 3.37/0.87 fof(f2454,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(X0),inverse(multiply(multiply(inverse(inverse(inverse(multiply(X0,X1)))),multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=X1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1449])).
% 3.37/0.87 fof(f2457,plain,(
% 3.37/0.87 ![X0,X1,X2]: (inverse(multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),X1)))=inverse(multiply(X2,multiply(inverse(inverse(inverse(multiply(X0,X2)))),X1))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1588])).
% 3.37/0.87 fof(f2458,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(X2,X0))))=multiply(inverse(inverse(inverse(multiply(X1,X2)))),multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f879])).
% 3.37/0.87 fof(f2459,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(multiply(inverse(inverse(inverse(multiply(X2,X1)))),multiply(a1,sF1_fnc)),X0))))=multiply(X2,multiply(a1,sF1_fnc)))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f875])).
% 3.37/0.87 fof(f2481,plain,(
% 3.37/0.87 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(a1,sF1_fnc)),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f2001])).
% 3.37/0.87 fof(f2489,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(X0,multiply(a1,sF1_fnc))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2321,f1756])).
% 3.37/0.87 fof(f2512,plain,(
% 3.37/0.87 inverse(multiply(inverse(inverse(a1)),multiply(multiply(a1,sF1_fnc),sF1_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1814,f2343])).
% 3.37/0.87 fof(f2513,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF1_fnc),multiply(multiply(a1,sF1_fnc),sF1_fnc)))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f2512])).
% 3.37/0.87 fof(f2514,plain,(
% 3.37/0.87 inverse(multiply(inverse(sF1_fnc),inverse(inverse(sF1_fnc))))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2513])).
% 3.37/0.87 fof(f2542,plain,(
% 3.37/0.87 inverse(multiply(a1,sF1_fnc))=multiply(a1,sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f994,f2514])).
% 3.37/0.87 fof(f2559,plain,(
% 3.37/0.87 inverse(multiply(a1,multiply(a1,sF1_fnc)))=inverse(a1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1477,f2349])).
% 3.37/0.87 fof(f2560,plain,(
% 3.37/0.87 inverse(multiply(a1,multiply(a1,sF1_fnc)))=sF1_fnc),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f2559])).
% 3.37/0.87 fof(f2561,plain,(
% 3.37/0.87 inverse(multiply(b1,multiply(a1,sF1_fnc)))=inverse(b1)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1478,f2350])).
% 3.37/0.87 fof(f2562,plain,(
% 3.37/0.87 inverse(multiply(b1,multiply(a1,sF1_fnc)))=sF3_fnc),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f7,f2561])).
% 3.37/0.87 fof(f2577,plain,(
% 3.37/0.87 ![X0]: (inverse(multiply(X0,multiply(a1,sF1_fnc)))=inverse(X0))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f1917,f2353])).
% 3.37/0.87 fof(f2675,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF1_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),a1),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2315,f2396])).
% 3.37/0.87 fof(f2676,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF1_fnc)),multiply(multiply(multiply(a1,sF1_fnc),a1),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2542,f2675])).
% 3.37/0.87 fof(f2677,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF1_fnc)),multiply(inverse(inverse(a1)),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2676])).
% 3.37/0.87 fof(f2678,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF1_fnc)),multiply(inverse(sF1_fnc),X0))))=inverse(sF0_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f5,f2677])).
% 3.37/0.87 fof(f2689,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,multiply(a1,sF1_fnc))))=multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2542,f2402])).
% 3.37/0.87 fof(f2690,plain,(
% 3.37/0.87 inverse(inverse(inverse(multiply(a1,multiply(a1,sF1_fnc)))))=multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2689])).
% 3.37/0.87 fof(f2692,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(inverse(inverse(sF1_fnc)),a1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2695,f2400])).
% 3.37/0.87 fof(f2695,plain,(
% 3.37/0.87 inverse(inverse(sF1_fnc))=multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2560,f2690])).
% 3.37/0.87 fof(f2718,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF3_fnc)),multiply(multiply(inverse(multiply(a1,sF1_fnc)),b1),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2315,f2414])).
% 3.37/0.87 fof(f2719,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF3_fnc)),multiply(multiply(multiply(a1,sF1_fnc),b1),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2542,f2718])).
% 3.37/0.87 fof(f2720,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(inverse(inverse(sF3_fnc)),multiply(inverse(sF3_fnc),X0))))=inverse(sF2_fnc))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2296,f2719])).
% 3.37/0.87 fof(f2727,plain,(
% 3.37/0.87 multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,multiply(a1,sF1_fnc))))=multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2542,f2419])).
% 3.37/0.87 fof(f2728,plain,(
% 3.37/0.87 inverse(inverse(inverse(multiply(b1,multiply(a1,sF1_fnc)))))=multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2727])).
% 3.37/0.87 fof(f2730,plain,(
% 3.37/0.87 multiply(a1,sF1_fnc)=multiply(inverse(inverse(sF3_fnc)),b1)),
% 3.37/0.87 inference(backward_demodulation,[status(thm)],[f2733,f2417])).
% 3.37/0.87 fof(f2733,plain,(
% 3.37/0.87 inverse(inverse(sF3_fnc))=multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc)))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2562,f2728])).
% 3.37/0.87 fof(f2742,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),inverse(inverse(inverse(sF0_fnc)))))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2425])).
% 3.37/0.87 fof(f2743,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(sF0_fnc)))))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2742])).
% 3.37/0.87 fof(f2749,plain,(
% 3.37/0.87 ![X0]: (multiply(X0,inverse(multiply(sF3_fnc,multiply(b1,X0))))=inverse(inverse(inverse(sF2_fnc))))),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2315,f2430])).
% 3.37/0.87 fof(f2750,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(multiply(multiply(a1,sF1_fnc),inverse(X0)),inverse(inverse(inverse(sF2_fnc)))))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2431])).
% 3.37/0.87 fof(f2751,plain,(
% 3.37/0.87 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X0))),inverse(inverse(inverse(sF2_fnc)))))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.87 inference(forward_demodulation,[status(thm)],[f2321,f2750])).
% 3.37/0.88 fof(f2756,plain,(
% 3.37/0.88 ![X0]: (multiply(sF3_fnc,inverse(multiply(inverse(inverse(inverse(multiply(b1,X0)))),multiply(a1,sF1_fnc))))=X0)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2577,f2435])).
% 3.37/0.88 fof(f2757,plain,(
% 3.37/0.88 ![X0]: (multiply(sF3_fnc,multiply(multiply(a1,sF1_fnc),inverse(inverse(multiply(b1,X0)))))=X0)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f1846,f2756])).
% 3.37/0.88 fof(f2758,plain,(
% 3.37/0.88 ![X0]: (multiply(sF3_fnc,inverse(inverse(inverse(inverse(multiply(b1,X0))))))=X0)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2321,f2757])).
% 3.37/0.88 fof(f2799,plain,(
% 3.37/0.88 ![X0]: (X0=inverse(inverse(inverse(inverse(multiply(X0,inverse(multiply(a1,sF1_fnc))))))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2542,f2441])).
% 3.37/0.88 fof(f2800,plain,(
% 3.37/0.88 ![X0]: (X0=inverse(inverse(inverse(inverse(multiply(X0,multiply(a1,sF1_fnc)))))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2542,f2799])).
% 3.37/0.88 fof(f2809,plain,(
% 3.37/0.88 ![X0]: (multiply(sF3_fnc,multiply(b1,X0))=X0)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2813,f2758])).
% 3.37/0.88 fof(f2813,plain,(
% 3.37/0.88 ![X0]: (X0=inverse(inverse(inverse(inverse(X0)))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2577,f2800])).
% 3.37/0.88 fof(f2851,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(X0),inverse(multiply(inverse(inverse(inverse(multiply(X0,X1)))),multiply(a1,sF1_fnc))))=X1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2577,f2454])).
% 3.37/0.88 fof(f2852,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),inverse(inverse(multiply(X0,X1)))))=X1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f1846,f2851])).
% 3.37/0.88 fof(f2853,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(X0),inverse(inverse(inverse(inverse(multiply(X0,X1))))))=X1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2321,f2852])).
% 3.37/0.88 fof(f2854,plain,(
% 3.37/0.88 ![X0]: (multiply(X0,inverse(X0))=inverse(sF2_fnc))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2856,f2720])).
% 3.37/0.88 fof(f2855,plain,(
% 3.37/0.88 ![X0]: (multiply(X0,inverse(X0))=inverse(sF0_fnc))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2856,f2678])).
% 3.37/0.88 fof(f2856,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2813,f2853])).
% 3.37/0.88 fof(f2861,plain,(
% 3.37/0.88 ![X0,X1,X2]: (inverse(multiply(inverse(X0),inverse(inverse(X1))))=inverse(multiply(X2,multiply(inverse(inverse(inverse(multiply(X0,X2)))),X1))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2321,f2457])).
% 3.37/0.88 fof(f2863,plain,(
% 3.37/0.88 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),multiply(X2,X0))))=inverse(inverse(inverse(multiply(X1,X2)))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2315,f2458])).
% 3.37/0.88 fof(f2864,plain,(
% 3.37/0.88 ![X0,X1]: (inverse(inverse(inverse(multiply(X0,multiply(inverse(inverse(inverse(multiply(X1,X0)))),multiply(a1,sF1_fnc))))))=multiply(X1,multiply(a1,sF1_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2863,f2459])).
% 3.37/0.88 fof(f2865,plain,(
% 3.37/0.88 ![X0]: (inverse(inverse(inverse(multiply(inverse(X0),inverse(inverse(multiply(a1,sF1_fnc)))))))=multiply(X0,multiply(a1,sF1_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2861,f2864])).
% 3.37/0.88 fof(f2866,plain,(
% 3.37/0.88 ![X0]: (inverse(inverse(multiply(inverse(multiply(a1,sF1_fnc)),X0)))=multiply(X0,multiply(a1,sF1_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f1919,f2865])).
% 3.37/0.88 fof(f2875,plain,(
% 3.37/0.88 ![X0]: (X0=multiply(X0,multiply(a1,sF1_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2329,f2866])).
% 3.37/0.88 fof(f2952,plain,(
% 3.37/0.88 ![X0,X1,X2]: (multiply(multiply(multiply(a1,sF1_fnc),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2542,f2481])).
% 3.37/0.88 fof(f2953,plain,(
% 3.37/0.88 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2321,f2952])).
% 3.37/0.88 fof(f2975,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(a1,sF1_fnc))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2542,f2489])).
% 3.37/0.88 fof(f2976,plain,(
% 3.37/0.88 ![X0,X1]: (inverse(inverse(inverse(multiply(X0,multiply(a1,sF1_fnc)))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2321,f2975])).
% 3.37/0.88 fof(f2981,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(inverse(X0)),inverse(multiply(X1,X0)))=inverse(inverse(inverse(X1))))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2983,f2953])).
% 3.37/0.88 fof(f2983,plain,(
% 3.37/0.88 ![X0,X1]: (inverse(inverse(inverse(X0)))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2577,f2976])).
% 3.37/0.88 fof(f3048,plain,(
% 3.37/0.88 ![X0]: (multiply(X0,inverse(X0))=inverse(inverse(inverse(sF2_fnc))))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2809,f2749])).
% 3.37/0.88 fof(f3051,plain,(
% 3.37/0.88 multiply(a1,sF1_fnc)=inverse(sF2_fnc)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2854,f994])).
% 3.37/0.88 fof(f3052,plain,(
% 3.37/0.88 inverse(sF0_fnc)=inverse(sF2_fnc)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f2855,f2854])).
% 3.37/0.88 fof(f3084,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X0))),multiply(a1,sF1_fnc)))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3086,f2751])).
% 3.37/0.88 fof(f3086,plain,(
% 3.37/0.88 multiply(a1,sF1_fnc)=inverse(inverse(inverse(sF2_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f994,f3048])).
% 3.37/0.88 fof(f3088,plain,(
% 3.37/0.88 inverse(sF2_fnc)=inverse(inverse(inverse(sF2_fnc)))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3051,f3086])).
% 3.37/0.88 fof(f3092,plain,(
% 3.37/0.88 inverse(sF2_fnc)=multiply(inverse(inverse(sF3_fnc)),b1)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3051,f2730])).
% 3.37/0.88 fof(f3093,plain,(
% 3.37/0.88 inverse(sF2_fnc)=multiply(inverse(inverse(sF1_fnc)),a1)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3051,f2692])).
% 3.37/0.88 fof(f3097,plain,(
% 3.37/0.88 ![X0]: (X0=multiply(X0,inverse(sF2_fnc)))),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3051,f2875])).
% 3.37/0.88 fof(f3127,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),inverse(inverse(inverse(X0))))),inverse(multiply(b1,X1)))=sF3_fnc)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2315,f3084])).
% 3.37/0.88 fof(f3128,plain,(
% 3.37/0.88 ![X0]: (multiply(inverse(inverse(X0)),inverse(multiply(b1,X0)))=sF3_fnc)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2334,f3127])).
% 3.37/0.88 fof(f3129,plain,(
% 3.37/0.88 inverse(inverse(inverse(b1)))=sF3_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2981,f3128])).
% 3.37/0.88 fof(f3137,plain,(
% 3.37/0.88 inverse(inverse(sF3_fnc))=sF3_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f7,f3129])).
% 3.37/0.88 fof(f3140,plain,(
% 3.37/0.88 inverse(sF0_fnc)=inverse(inverse(inverse(sF2_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3052,f3088])).
% 3.37/0.88 fof(f3146,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X0))),inverse(sF0_fnc)))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3148,f2743])).
% 3.37/0.88 fof(f3148,plain,(
% 3.37/0.88 inverse(sF0_fnc)=inverse(inverse(inverse(sF0_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3052,f3140])).
% 3.37/0.88 fof(f3152,plain,(
% 3.37/0.88 inverse(sF0_fnc)=multiply(inverse(inverse(sF3_fnc)),b1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3052,f3092])).
% 3.37/0.88 fof(f3153,plain,(
% 3.37/0.88 inverse(sF0_fnc)=multiply(sF3_fnc,b1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3137,f3152])).
% 3.37/0.88 fof(f3172,plain,(
% 3.37/0.88 inverse(sF0_fnc)=sF2_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f8,f3153])).
% 3.37/0.88 fof(f3173,plain,(
% 3.37/0.88 inverse(sF0_fnc)=multiply(inverse(inverse(sF1_fnc)),a1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3052,f3093])).
% 3.37/0.88 fof(f3174,plain,(
% 3.37/0.88 sF2_fnc=multiply(inverse(inverse(sF1_fnc)),a1)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3172,f3173])).
% 3.37/0.88 fof(f3182,plain,(
% 3.37/0.88 ![X0]: (X0=multiply(X0,inverse(sF0_fnc)))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3052,f3097])).
% 3.37/0.88 fof(f3184,plain,(
% 3.37/0.88 ![X0]: (X0=multiply(X0,sF2_fnc))),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3172,f3182])).
% 3.37/0.88 fof(f3257,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),multiply(inverse(inverse(inverse(X0))),sF2_fnc))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3172,f3146])).
% 3.37/0.88 fof(f3258,plain,(
% 3.37/0.88 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X1)))),inverse(inverse(inverse(X0))))),inverse(multiply(a1,X1)))=sF1_fnc)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f3184,f3257])).
% 3.37/0.88 fof(f3259,plain,(
% 3.37/0.88 ![X0]: (multiply(inverse(inverse(X0)),inverse(multiply(a1,X0)))=sF1_fnc)),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2334,f3258])).
% 3.37/0.88 fof(f3260,plain,(
% 3.37/0.88 inverse(inverse(inverse(a1)))=sF1_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f2981,f3259])).
% 3.37/0.88 fof(f3262,plain,(
% 3.37/0.88 sF2_fnc=multiply(sF1_fnc,a1)),
% 3.37/0.88 inference(backward_demodulation,[status(thm)],[f3269,f3174])).
% 3.37/0.88 fof(f3269,plain,(
% 3.37/0.88 inverse(inverse(sF1_fnc))=sF1_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f5,f3260])).
% 3.37/0.88 fof(f3324,plain,(
% 3.37/0.88 sF2_fnc=sF0_fnc),
% 3.37/0.88 inference(forward_demodulation,[status(thm)],[f6,f3262])).
% 3.37/0.88 fof(f3325,plain,(
% 3.37/0.88 $false),
% 3.37/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3324,f9])).
% 3.37/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.48/0.93 % Elapsed time: 0.535900 seconds
% 0.48/0.93 % CPU time: 3.889958 seconds
% 0.48/0.93 % Total memory used: 91.825 MB
% 0.48/0.93 % Net memory used: 90.644 MB
%------------------------------------------------------------------------------