%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:36 PM UTC 2026
% Result : Unsatisfiable 7.45s 1.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:11:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 7.45/1.37 % Refutation found
% 7.45/1.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.45/1.37 % SZS output start CNFRefutation for theBenchmark
% 7.45/1.37 fof(f1,axiom,(
% 7.45/1.37 (![A,B,C]: (inverse(multiply(inverse(multiply(A,inverse(multiply(inverse(B),inverse(multiply(C,inverse(multiply(inverse(C),C)))))))),multiply(A,C))) = B ))),
% 7.45/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.45/1.37 fof(f2,negated_conjecture,(
% 7.45/1.37 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 7.45/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.45/1.37 fof(f3,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))=X1)),
% 7.45/1.37 inference(cnf_transformation,[status(thm)],[f1])).
% 7.45/1.37 fof(f4,plain,(
% 7.45/1.37 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 7.45/1.37 inference(cnf_transformation,[status(thm)],[f2])).
% 7.45/1.37 fof(f5,definition,(
% 7.45/1.37 sF2_fnc=inverse(b2)),
% 7.45/1.37 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 7.45/1.37 fof(f6,definition,(
% 7.45/1.37 sF1_fnc=multiply(sF2_fnc,b2)),
% 7.45/1.37 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 7.45/1.37 fof(f7,definition,(
% 7.45/1.37 sF0_fnc=multiply(sF1_fnc,a2)),
% 7.45/1.37 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 7.45/1.37 fof(f8,plain,(
% 7.45/1.37 ~sF0_fnc=a2),
% 7.45/1.37 inference(definition_folding,[],[f4,f7,f6,f5])).
% 7.45/1.37 fof(f12,plain,(
% 7.45/1.37 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(multiply(sF2_fnc,b2)))))))),multiply(X0,b2)))=X1)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f5,f3])).
% 7.45/1.37 fof(f14,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(inverse(b2),b2)))))))),sF1_fnc))=X0)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f6,f3])).
% 7.45/1.37 fof(f15,plain,(
% 7.45/1.37 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X0,b2)))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f6,f12])).
% 7.45/1.37 fof(f16,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(multiply(sF2_fnc,b2)))))))),sF1_fnc))=X0)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f5,f14])).
% 7.45/1.37 fof(f17,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))=X0)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f6,f16])).
% 7.45/1.37 fof(f18,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f17,f17])).
% 7.45/1.37 fof(f20,plain,(
% 7.45/1.37 inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(sF2_fnc,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))=b2),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f5,f17])).
% 7.45/1.37 fof(f21,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(X2,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f17,f3])).
% 7.45/1.37 fof(f22,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f17,f3])).
% 7.45/1.37 fof(f23,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=X0)),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f18,f17])).
% 7.45/1.37 fof(f28,plain,(
% 7.45/1.37 multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=b2),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f20])).
% 7.45/1.37 fof(f33,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X0,b2)))=multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X2,b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f15,f15])).
% 7.45/1.37 fof(f37,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X1,b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f15,f23])).
% 7.45/1.37 fof(f40,plain,(
% 7.45/1.37 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X0,b2)))=multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X1),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f37,f33])).
% 7.45/1.37 fof(f66,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X1,b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f40,f23])).
% 7.45/1.37 fof(f68,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f66])).
% 7.45/1.37 fof(f73,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f23,f68])).
% 7.45/1.37 fof(f116,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f22,f23])).
% 7.45/1.37 fof(f122,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f116])).
% 7.45/1.37 fof(f130,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f23,f122])).
% 7.45/1.37 fof(f139,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X1)),inverse(multiply(b2,inverse(sF1_fnc))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),X1))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f23,f130])).
% 7.45/1.37 fof(f140,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),b2))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f28,f130])).
% 7.45/1.37 fof(f143,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(multiply(inverse(a2),a2)))))))),sF0_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f7,f130])).
% 7.45/1.37 fof(f173,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f18,f21])).
% 7.45/1.37 fof(f198,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f173])).
% 7.45/1.37 fof(f199,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f198])).
% 7.45/1.37 fof(f255,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f18,f199])).
% 7.45/1.37 fof(f279,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f255])).
% 7.45/1.37 fof(f280,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f279])).
% 7.45/1.37 fof(f333,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(inverse(multiply(b2,inverse(sF1_fnc))))),inverse(multiply(b2,inverse(sF1_fnc))))))),inverse(multiply(X0,inverse(multiply(sF1_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc)))))))),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),multiply(X1,b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f139,f73])).
% 7.45/1.37 fof(f344,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f139,f333])).
% 7.45/1.37 fof(f345,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f344])).
% 7.45/1.37 fof(f346,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),sF1_fnc)=multiply(inverse(multiply(X1,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f345])).
% 7.45/1.37 fof(f354,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),sF1_fnc)=multiply(inverse(multiply(X1,X0)),multiply(X1,b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f23,f346])).
% 7.45/1.37 fof(f371,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF2_fnc,X0)),sF1_fnc)=multiply(inverse(multiply(X1,X0)),multiply(X1,b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f23,f354])).
% 7.45/1.37 fof(f390,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(X0,X1))),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)),multiply(inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f130,f371])).
% 7.45/1.37 fof(f406,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(X0,X1))),sF1_fnc)=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(X0,inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),b2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f18,f390])).
% 7.45/1.37 fof(f902,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,multiply(X0,X1))),sF1_fnc)=multiply(X2,multiply(inverse(multiply(X0,inverse(multiply(inverse(X2),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))))),b2)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f23,f406])).
% 7.45/1.37 fof(f941,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(sF2_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))),sF1_fnc)=multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f140,f902])).
% 7.45/1.37 fof(f959,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,b2)),sF1_fnc)=multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f28,f941])).
% 7.45/1.37 fof(f962,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(sF1_fnc),sF1_fnc)=multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f6,f959])).
% 7.45/1.37 fof(f1399,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(sF1_fnc),sF1_fnc)=multiply(inverse(X0),X0))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f23,f962])).
% 7.45/1.37 fof(f1400,plain,(
% 7.45/1.37 multiply(inverse(sF1_fnc),sF1_fnc)=multiply(sF2_fnc,b2)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f28,f962])).
% 7.45/1.37 fof(f1402,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(sF1_fnc),sF1_fnc)=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f18,f962])).
% 7.45/1.37 fof(f1441,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(X0,multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1504,f962])).
% 7.45/1.37 fof(f1447,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(inverse(X0),X0))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1504,f1399])).
% 7.45/1.37 fof(f1504,plain,(
% 7.45/1.37 multiply(inverse(sF1_fnc),sF1_fnc)=sF1_fnc),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f6,f1400])).
% 7.45/1.37 fof(f1511,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1504,f1402])).
% 7.45/1.37 fof(f1606,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1447,f143])).
% 7.45/1.37 fof(f1609,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(sF1_fnc))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1447,f130])).
% 7.45/1.37 fof(f1668,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)=X0)),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1606,f23])).
% 7.45/1.37 fof(f1671,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1606,f18])).
% 7.45/1.37 fof(f1674,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1606,f280])).
% 7.45/1.37 fof(f1676,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1606,f1511])).
% 7.45/1.37 fof(f1701,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f1606,f1441])).
% 7.45/1.37 fof(f1754,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(sF1_fnc))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1609])).
% 7.45/1.37 fof(f1796,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1671])).
% 7.45/1.37 fof(f1807,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1674])).
% 7.45/1.37 fof(f1808,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1807])).
% 7.45/1.37 fof(f1809,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1808])).
% 7.45/1.37 fof(f1810,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(X2,inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1809])).
% 7.45/1.37 fof(f1811,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1810])).
% 7.45/1.37 fof(f1812,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1811])).
% 7.45/1.37 fof(f1813,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1812])).
% 7.45/1.37 fof(f1814,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1813])).
% 7.45/1.37 fof(f1815,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X2),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1814])).
% 7.45/1.37 fof(f1816,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1815])).
% 7.45/1.37 fof(f1820,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,inverse(sF1_fnc))))))),sF1_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1676])).
% 7.45/1.37 fof(f1821,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1606,f1820])).
% 7.45/1.37 fof(f1911,plain,(
% 7.45/1.37 multiply(inverse(multiply(sF1_fnc,inverse(sF1_fnc))),sF0_fnc)=multiply(a2,inverse(sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1447,f1668])).
% 7.45/1.37 fof(f2006,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(X0,inverse(sF1_fnc)))),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)=multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,X0)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1447,f1754])).
% 7.45/1.37 fof(f2033,plain,(
% 7.45/1.37 ![X0,X1]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(multiply(X1,inverse(sF1_fnc))),multiply(X1,X0)))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f1668,f2006])).
% 7.45/1.37 fof(f2040,plain,(
% 7.45/1.37 multiply(inverse(sF1_fnc),inverse(sF1_fnc))=sF1_fnc),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1447,f2033])).
% 7.45/1.37 fof(f2041,plain,(
% 7.45/1.37 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),X0)))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1447,f2033])).
% 7.45/1.37 fof(f2059,plain,(
% 7.45/1.37 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(multiply(inverse(X0),inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1447,f2033])).
% 7.45/1.37 fof(f2062,plain,(
% 7.45/1.37 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(X0,inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f1701,f2033])).
% 7.45/1.37 fof(f2090,plain,(
% 7.45/1.37 multiply(inverse(sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),sF1_fnc)),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f2040,f2033])).
% 7.45/1.37 fof(f2091,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))))))),sF1_fnc))),
% 7.45/1.37 inference(paramodulation,[status(thm)],[f2040,f1754])).
% 7.45/1.37 fof(f2095,plain,(
% 7.45/1.37 sF1_fnc=multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),sF1_fnc)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2040,f2090])).
% 7.45/1.37 fof(f2096,plain,(
% 7.45/1.37 multiply(inverse(sF1_fnc),sF0_fnc)=multiply(a2,inverse(sF1_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2131,f1911])).
% 7.45/1.37 fof(f2131,plain,(
% 7.45/1.37 sF1_fnc=multiply(sF1_fnc,inverse(sF1_fnc))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2059,f2095])).
% 7.45/1.37 fof(f2134,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(X0)),inverse(sF1_fnc))))),sF1_fnc)=X0)),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f1668])).
% 7.45/1.37 fof(f2135,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f1796])).
% 7.45/1.37 fof(f2137,plain,(
% 7.45/1.37 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,inverse(sF1_fnc))))))),multiply(X1,X2)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f1754])).
% 7.45/1.37 fof(f2140,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f1816])).
% 7.45/1.37 fof(f2142,plain,(
% 7.45/1.37 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc)))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f1821])).
% 7.45/1.37 fof(f2150,plain,(
% 7.45/1.37 ![X0]: (multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(X0,inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.37 inference(backward_demodulation,[status(thm)],[f2199,f2062])).
% 7.45/1.37 fof(f2199,plain,(
% 7.45/1.37 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2040,f2091])).
% 7.45/1.37 fof(f2264,plain,(
% 7.45/1.37 ![X0]: (inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc))),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2199,f2135])).
% 7.45/1.37 fof(f2275,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2199,f2140])).
% 7.45/1.37 fof(f2276,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2199,f2275])).
% 7.45/1.37 fof(f2277,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.37 inference(forward_demodulation,[status(thm)],[f2062,f2276])).
% 7.45/1.37 fof(f2278,plain,(
% 7.45/1.37 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2277])).
% 7.45/1.38 fof(f2279,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2278])).
% 7.45/1.38 fof(f2280,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2279])).
% 7.45/1.38 fof(f2281,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2280])).
% 7.45/1.38 fof(f2282,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2062,f2281])).
% 7.45/1.38 fof(f2283,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X2),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2282])).
% 7.45/1.38 fof(f2284,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2062,f2283])).
% 7.45/1.38 fof(f2293,plain,(
% 7.45/1.38 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(a2,inverse(sF1_fnc))))))),sF0_fnc),inverse(sF1_fnc))))),sF1_fnc)))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2199,f2142])).
% 7.45/1.38 fof(f2295,plain,(
% 7.45/1.38 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2062,f2293])).
% 7.45/1.38 fof(f2333,plain,(
% 7.45/1.38 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(sF1_fnc,X0)))),
% 7.45/1.38 inference(paramodulation,[status(thm)],[f2131,f2033])).
% 7.45/1.38 fof(f2362,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(sF1_fnc,X0),inverse(sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),multiply(X0,inverse(sF1_fnc))))),
% 7.45/1.38 inference(paramodulation,[status(thm)],[f2333,f2033])).
% 7.45/1.38 fof(f2368,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(sF1_fnc,X0),inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(X0,inverse(sF1_fnc))))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2040,f2362])).
% 7.45/1.38 fof(f2646,plain,(
% 7.45/1.38 inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(sF1_fnc))),sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))),sF1_fnc)),
% 7.45/1.38 inference(paramodulation,[status(thm)],[f2040,f2264])).
% 7.45/1.38 fof(f2652,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.38 inference(paramodulation,[status(thm)],[f2264,f2059])).
% 7.45/1.38 fof(f2662,plain,(
% 7.45/1.38 inverse(multiply(sF1_fnc,inverse(sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))),sF1_fnc)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2059,f2646])).
% 7.45/1.38 fof(f2663,plain,(
% 7.45/1.38 inverse(sF1_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(sF1_fnc)),inverse(sF1_fnc))))),sF1_fnc)),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2131,f2662])).
% 7.45/1.38 fof(f2664,plain,(
% 7.45/1.38 ![X0]: (inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2264])).
% 7.45/1.38 fof(f2665,plain,(
% 7.45/1.38 ![X0]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(inverse(X0)),sF1_fnc)))),sF1_fnc)=X0)),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2134])).
% 7.45/1.38 fof(f2672,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(sF1_fnc,X0),inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(X0,sF1_fnc)))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2368])).
% 7.45/1.38 fof(f2673,plain,(
% 7.45/1.38 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2059])).
% 7.45/1.38 fof(f2674,plain,(
% 7.45/1.38 ![X0]: (multiply(X0,inverse(sF1_fnc))=multiply(inverse(sF1_fnc),multiply(inverse(sF1_fnc),X0)))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2041])).
% 7.45/1.38 fof(f2679,plain,(
% 7.45/1.38 multiply(inverse(sF1_fnc),sF0_fnc)=multiply(a2,sF1_fnc)),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2096])).
% 7.45/1.38 fof(f2778,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2150])).
% 7.45/1.38 fof(f2785,plain,(
% 7.45/1.38 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2295])).
% 7.45/1.38 fof(f2787,plain,(
% 7.45/1.38 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2284])).
% 7.45/1.38 fof(f2789,plain,(
% 7.45/1.38 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,sF1_fnc)))))),multiply(X1,X2)))),
% 7.45/1.38 inference(backward_demodulation,[status(thm)],[f2850,f2137])).
% 7.45/1.38 fof(f2850,plain,(
% 7.45/1.38 inverse(sF1_fnc)=sF1_fnc),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2134,f2663])).
% 7.45/1.38 fof(f2879,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2850,f2652])).
% 7.45/1.38 fof(f2880,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2850,f2879])).
% 7.45/1.38 fof(f2881,plain,(
% 7.45/1.38 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))),sF1_fnc))),
% 7.45/1.38 inference(forward_demodulation,[status(thm)],[f2850,f2880])).
% 7.45/1.39 fof(f2882,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2150,f2881])).
% 7.45/1.39 fof(f2883,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(inverse(multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2882])).
% 7.45/1.39 fof(f2898,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2664])).
% 7.45/1.39 fof(f2899,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc))=multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2898])).
% 7.45/1.39 fof(f2900,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2899])).
% 7.45/1.39 fof(f2901,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),sF1_fnc)))),sF1_fnc)=X0)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2665])).
% 7.45/1.39 fof(f2915,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(sF1_fnc,X0),sF1_fnc)=multiply(inverse(sF1_fnc),multiply(X0,sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2672])).
% 7.45/1.39 fof(f2916,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(sF1_fnc,X0),sF1_fnc)=multiply(sF1_fnc,multiply(X0,sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2915])).
% 7.45/1.39 fof(f2917,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(multiply(X0,sF1_fnc),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f2918,f2883])).
% 7.45/1.39 fof(f2918,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2673])).
% 7.45/1.39 fof(f2919,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(inverse(sF1_fnc),multiply(inverse(sF1_fnc),X0)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2674])).
% 7.45/1.39 fof(f2920,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(inverse(sF1_fnc),X0)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2919])).
% 7.45/1.39 fof(f2922,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(sF1_fnc,X0)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2920])).
% 7.45/1.39 fof(f2927,plain,(
% 7.45/1.39 multiply(sF1_fnc,sF0_fnc)=multiply(a2,sF1_fnc)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2679])).
% 7.45/1.39 fof(f3309,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2778])).
% 7.45/1.39 fof(f3310,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3309])).
% 7.45/1.39 fof(f3311,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3310])).
% 7.45/1.39 fof(f3312,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)),sF1_fnc)=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2883,f3311])).
% 7.45/1.39 fof(f3313,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(multiply(inverse(inverse(X0)),sF1_fnc),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3315,f2918])).
% 7.45/1.39 fof(f3315,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(X0),sF1_fnc),sF1_fnc)=multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2918,f3312])).
% 7.45/1.39 fof(f3343,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2785])).
% 7.45/1.39 fof(f3344,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3343])).
% 7.45/1.39 fof(f3345,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X0,sF1_fnc)),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3344])).
% 7.45/1.39 fof(f3346,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X0),sF1_fnc),sF1_fnc)))),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3345])).
% 7.45/1.39 fof(f3369,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2787])).
% 7.45/1.39 fof(f3370,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3369])).
% 7.45/1.39 fof(f3371,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X2,sF1_fnc)),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3370])).
% 7.45/1.39 fof(f3372,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3371])).
% 7.45/1.39 fof(f3373,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3372])).
% 7.45/1.39 fof(f3374,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)),sF1_fnc)),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2883,f3373])).
% 7.45/1.39 fof(f3375,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2918,f3374])).
% 7.45/1.39 fof(f3376,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3375])).
% 7.45/1.39 fof(f3377,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,inverse(sF1_fnc))))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3376])).
% 7.45/1.39 fof(f3378,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3377])).
% 7.45/1.39 fof(f3379,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X2,sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3378])).
% 7.45/1.39 fof(f3380,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(X2,sF1_fnc)),sF1_fnc)),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2883,f3379])).
% 7.45/1.39 fof(f3381,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2918,f3380])).
% 7.45/1.39 fof(f3382,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3381])).
% 7.45/1.39 fof(f3383,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3382])).
% 7.45/1.39 fof(f3384,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X2,sF1_fnc)),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3383])).
% 7.45/1.39 fof(f3385,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3384])).
% 7.45/1.39 fof(f3386,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3385])).
% 7.45/1.39 fof(f3387,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)),sF1_fnc)),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2883,f3386])).
% 7.45/1.39 fof(f3388,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2918,f3387])).
% 7.45/1.39 fof(f3389,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3388])).
% 7.45/1.39 fof(f3390,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3389])).
% 7.45/1.39 fof(f3391,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc)),sF1_fnc)),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2883,f3390])).
% 7.45/1.39 fof(f3392,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1_fnc))),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2918,f3391])).
% 7.45/1.39 fof(f3393,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(X2,sF1_fnc)),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3392])).
% 7.45/1.39 fof(f3394,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3393])).
% 7.45/1.39 fof(f3404,plain,(
% 7.45/1.39 ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,inverse(sF1_fnc))))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,sF1_fnc)))))),multiply(X1,X2)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f2789])).
% 7.45/1.39 fof(f3406,plain,(
% 7.45/1.39 ![X0,X1,X2]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc)=multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X2,sF1_fnc)))))),multiply(X1,X2)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2850,f3404])).
% 7.45/1.39 fof(f3694,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),sF1_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f2900,f2900])).
% 7.45/1.39 fof(f3695,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(X0))),sF1_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),sF1_fnc))))),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f2901,f2900])).
% 7.45/1.39 fof(f3699,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2901,f3694])).
% 7.45/1.39 fof(f3700,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(X0,sF1_fnc))),sF1_fnc)))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3703,f2900])).
% 7.45/1.39 fof(f3703,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(X0))),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(inverse(inverse(X0)),sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2901,f3695])).
% 7.45/1.39 fof(f3714,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc)))=X0)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3700,f2901])).
% 7.45/1.39 fof(f3719,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(X0,sF1_fnc))),sF1_fnc))))),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3700,f3699])).
% 7.45/1.39 fof(f3744,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(X0,sF1_fnc))),sF1_fnc)),sF1_fnc)),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3719])).
% 7.45/1.39 fof(f3745,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(X0,sF1_fnc))),sF1_fnc))),sF1_fnc),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3744])).
% 7.45/1.39 fof(f3746,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(multiply(inverse(inverse(multiply(X0,sF1_fnc))),sF1_fnc),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3745])).
% 7.45/1.39 fof(f3748,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3759,f3394])).
% 7.45/1.39 fof(f3753,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc))))),sF1_fnc)))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3759,f3346])).
% 7.45/1.39 fof(f3759,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(multiply(X0,sF1_fnc),sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3746])).
% 7.45/1.39 fof(f3777,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3759,f3748])).
% 7.45/1.39 fof(f3778,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)),sF1_fnc)),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3777])).
% 7.45/1.39 fof(f3779,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))),sF1_fnc),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3778])).
% 7.45/1.39 fof(f3780,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(X2,sF1_fnc),sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3779])).
% 7.45/1.39 fof(f3781,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(X2,sF1_fnc))))),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3759,f3780])).
% 7.45/1.39 fof(f3782,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(multiply(X2,sF1_fnc)),sF1_fnc)),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3781])).
% 7.45/1.39 fof(f3783,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(inverse(inverse(multiply(X2,sF1_fnc))),sF1_fnc),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3782])).
% 7.45/1.39 fof(f3784,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(inverse(multiply(sF1_fnc,inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc)))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3783])).
% 7.45/1.39 fof(f3785,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3759,f3784])).
% 7.45/1.39 fof(f3786,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)),sF1_fnc)),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3785])).
% 7.45/1.39 fof(f3787,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3786])).
% 7.45/1.39 fof(f3788,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(sF1_fnc,multiply(sF1_fnc,inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3787])).
% 7.45/1.39 fof(f3789,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(inverse(multiply(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)),sF1_fnc)),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3788])).
% 7.45/1.39 fof(f3790,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3789])).
% 7.45/1.39 fof(f3791,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3790])).
% 7.45/1.39 fof(f3808,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f2922,f3753])).
% 7.45/1.39 fof(f3809,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3808])).
% 7.45/1.39 fof(f3810,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(multiply(inverse(X0),sF1_fnc),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3809])).
% 7.45/1.39 fof(f3817,plain,(
% 7.45/1.39 multiply(sF0_fnc,sF1_fnc)=multiply(sF1_fnc,multiply(a2,sF1_fnc))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f2927,f2922])).
% 7.45/1.39 fof(f3833,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc)),sF1_fnc)))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f3714,f2916])).
% 7.45/1.39 fof(f3834,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc)),sF1_fnc)=multiply(sF1_fnc,X0))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f3714,f2922])).
% 7.45/1.39 fof(f3842,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(multiply(inverse(inverse(inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3833])).
% 7.45/1.39 fof(f3843,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3842])).
% 7.45/1.39 fof(f3844,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(multiply(inverse(inverse(X0)),sF1_fnc),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3843])).
% 7.45/1.39 fof(f3845,plain,(
% 7.45/1.39 multiply(sF0_fnc,sF1_fnc)=multiply(a2,sF1_fnc)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3862,f3817])).
% 7.45/1.39 fof(f3862,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(sF1_fnc,multiply(X0,sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3844])).
% 7.45/1.39 fof(f3863,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(inverse(inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc),sF1_fnc)=multiply(sF1_fnc,X0))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3834])).
% 7.45/1.39 fof(f3864,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(inverse(X0),sF1_fnc)),sF1_fnc)=multiply(sF1_fnc,X0))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3313,f3863])).
% 7.45/1.39 fof(f3865,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(inverse(inverse(X0)),sF1_fnc),sF1_fnc)=multiply(sF1_fnc,X0))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3315,f3864])).
% 7.45/1.39 fof(f3879,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(X0,sF1_fnc),sF1_fnc)=multiply(sF1_fnc,multiply(X0,sF1_fnc)))),
% 7.45/1.39 inference(paramodulation,[status(thm)],[f3862,f2922])).
% 7.45/1.39 fof(f3884,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f3791])).
% 7.45/1.39 fof(f3885,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(inverse(X0)),sF1_fnc)=multiply(sF1_fnc,X0))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f3865])).
% 7.45/1.39 fof(f3886,plain,(
% 7.45/1.39 ![X0]: (multiply(X0,sF1_fnc)=multiply(inverse(inverse(X0)),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f3313])).
% 7.45/1.39 fof(f3887,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc)=multiply(multiply(X0,sF1_fnc),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f2917])).
% 7.45/1.39 fof(f3889,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc),multiply(inverse(X0),sF1_fnc)))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f3810])).
% 7.45/1.39 fof(f3894,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(X0,sF1_fnc))=multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc))))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3895,f3759])).
% 7.45/1.39 fof(f3895,plain,(
% 7.45/1.39 ![X0]: (multiply(multiply(X0,sF1_fnc),sF1_fnc)=multiply(X0,sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3862,f3879])).
% 7.45/1.39 fof(f3896,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3884])).
% 7.45/1.39 fof(f3897,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(multiply(multiply(multiply(X2,sF1_fnc),sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3896])).
% 7.45/1.39 fof(f3898,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(multiply(multiply(X2,sF1_fnc),multiply(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3897])).
% 7.45/1.39 fof(f3899,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(multiply(multiply(X2,sF1_fnc),multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3898])).
% 7.45/1.39 fof(f3900,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(multiply(multiply(X2,sF1_fnc),multiply(inverse(X2),sF1_fnc))))))))),multiply(X0,multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3899])).
% 7.45/1.39 fof(f3901,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(multiply(multiply(X2,sF1_fnc),multiply(inverse(X2),sF1_fnc))))))))),multiply(X0,multiply(inverse(X2),sF1_fnc))))=X1)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3900])).
% 7.45/1.39 fof(f3902,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))=X0)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3885,f3714])).
% 7.45/1.39 fof(f3927,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(X0,sF1_fnc))))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3885,f3700])).
% 7.45/1.39 fof(f3984,plain,(
% 7.45/1.39 ![X0]: (multiply(inverse(multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))),sF1_fnc)=multiply(X0,sF1_fnc))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3895,f3887])).
% 7.45/1.39 fof(f3986,plain,(
% 7.45/1.39 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),inverse(sF1_fnc))))))),multiply(X0,multiply(inverse(X2),sF1_fnc))))=X1)),
% 7.45/1.39 inference(backward_demodulation,[status(thm)],[f3987,f3901])).
% 7.45/1.39 fof(f3987,plain,(
% 7.45/1.39 ![X0]: (sF1_fnc=multiply(multiply(X0,sF1_fnc),multiply(inverse(X0),sF1_fnc)))),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3984,f3889])).
% 7.45/1.39 fof(f4005,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=X0)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3862,f3902])).
% 7.45/1.39 fof(f4010,plain,(
% 7.45/1.39 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=X0)),
% 7.45/1.39 inference(forward_demodulation,[status(thm)],[f3894,f4005])).
% 7.45/1.39 fof(f4089,plain,(
% 7.45/1.39 ![X0]: (multiply(sF1_fnc,inverse(multiply(X0,sF1_fnc)))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3862,f3927])).
% 7.45/1.41 fof(f4090,plain,(
% 7.45/1.41 ![X0]: (inverse(multiply(X0,sF1_fnc))=multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3894,f4089])).
% 7.45/1.41 fof(f4142,plain,(
% 7.45/1.41 ![X0]: (inverse(multiply(X0,sF1_fnc))=multiply(inverse(X0),sF1_fnc))),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3984,f4090])).
% 7.45/1.41 fof(f4308,plain,(
% 7.45/1.41 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),sF1_fnc),sF1_fnc)))))),multiply(X0,multiply(inverse(X2),sF1_fnc))))=X1)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f2850,f3986])).
% 7.45/1.41 fof(f4309,plain,(
% 7.45/1.41 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))),sF1_fnc))=X0)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3406,f4308])).
% 7.45/1.41 fof(f4310,plain,(
% 7.45/1.41 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc)))=X0)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3703,f4309])).
% 7.45/1.41 fof(f4311,plain,(
% 7.45/1.41 ![X0]: (inverse(multiply(inverse(inverse(multiply(inverse(X0),sF1_fnc))),sF1_fnc))=X0)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f3894,f4310])).
% 7.45/1.41 fof(f4312,plain,(
% 7.45/1.41 ![X0]: (inverse(multiply(inverse(X0),sF1_fnc))=X0)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f4010,f4311])).
% 7.45/1.41 fof(f4313,plain,(
% 7.45/1.41 ![X0]: (multiply(X0,sF1_fnc)=X0)),
% 7.45/1.41 inference(backward_demodulation,[status(thm)],[f4315,f3886])).
% 7.45/1.41 fof(f4315,plain,(
% 7.45/1.41 ![X0]: (multiply(inverse(inverse(X0)),sF1_fnc)=X0)),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f4142,f4312])).
% 7.45/1.41 fof(f4440,plain,(
% 7.45/1.41 sF0_fnc=multiply(a2,sF1_fnc)),
% 7.45/1.41 inference(backward_demodulation,[status(thm)],[f4313,f3845])).
% 7.45/1.41 fof(f4568,plain,(
% 7.45/1.41 sF0_fnc=a2),
% 7.45/1.41 inference(forward_demodulation,[status(thm)],[f4313,f4440])).
% 7.45/1.41 fof(f4569,plain,(
% 7.45/1.41 $false),
% 7.45/1.41 inference(forward_subsumption_resolution,[status(thm)],[f4568,f8])).
% 7.45/1.41 % SZS output end CNFRefutation for theBenchmark.p
% 7.45/1.43 % Elapsed time: 1.054372 seconds
% 7.45/1.43 % CPU time: 8.092716 seconds
% 7.45/1.43 % Total memory used: 295.815 MB
% 7.45/1.43 % Net memory used: 285.254 MB
%------------------------------------------------------------------------------