%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP428-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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:36:37 PM UTC 2026
% Result : Unsatisfiable 3.90s 0.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP428-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.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 20:16:05 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 3.90/0.96 % Refutation found
% 3.90/0.96 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.90/0.96 % SZS output start CNFRefutation for theBenchmark
% 3.90/0.96 fof(f1,axiom,(
% 3.90/0.96 (![A,B,C,D]: (multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),D),inverse(multiply(B,D))))) = C ))),
% 3.90/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.90/0.96 fof(f2,negated_conjecture,(
% 3.90/0.96 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 3.90/0.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.90/0.96 fof(f3,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3)))))=X2)),
% 3.90/0.96 inference(cnf_transformation,[status(thm)],[f1])).
% 3.90/0.96 fof(f4,plain,(
% 3.90/0.96 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 3.90/0.96 inference(cnf_transformation,[status(thm)],[f2])).
% 3.90/0.96 fof(f5,definition,(
% 3.90/0.96 sF2_fnc=inverse(b2)),
% 3.90/0.96 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.90/0.96 fof(f6,definition,(
% 3.90/0.96 sF1_fnc=multiply(sF2_fnc,b2)),
% 3.90/0.96 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.90/0.96 fof(f7,definition,(
% 3.90/0.96 sF0_fnc=multiply(sF1_fnc,a2)),
% 3.90/0.96 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.90/0.96 fof(f8,plain,(
% 3.90/0.96 ~sF0_fnc=a2),
% 3.90/0.96 inference(definition_folding,[],[f4,f7,f6,f5])).
% 3.90/0.96 fof(f10,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(inverse(X0),X1))),X2),inverse(multiply(b2,X2)))))=X1)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f3])).
% 3.90/0.96 fof(f13,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),a2),inverse(sF0_fnc))))=X1)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f7,f3])).
% 3.90/0.96 fof(f14,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),multiply(inverse(X0),X1))),b2),inverse(sF1_fnc))))=X1)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f6,f3])).
% 3.90/0.96 fof(f16,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f13])).
% 3.90/0.96 fof(f17,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),X3),inverse(multiply(X2,X3)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f3,f13])).
% 3.90/0.96 fof(f18,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),a2),inverse(sF0_fnc))))=X0)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f13])).
% 3.90/0.96 fof(f19,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X3)))),X1))),a2),inverse(sF0_fnc))))))))=X3)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f3])).
% 3.90/0.96 fof(f24,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))))))=X3)),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f19])).
% 3.90/0.96 fof(f30,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,inverse(multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(sF2_fnc,multiply(inverse(X0),X2)))),X1))),a2),inverse(sF0_fnc))))))))=X2)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f10])).
% 3.90/0.96 fof(f36,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(inverse(inverse(X0)),X1))),X2),inverse(multiply(b2,X2)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f10,f13])).
% 3.90/0.96 fof(f37,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f30])).
% 3.90/0.96 fof(f47,plain,(
% 3.90/0.96 multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),a2),inverse(sF0_fnc))))=b2),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f6,f18])).
% 3.90/0.96 fof(f50,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f14])).
% 3.90/0.96 fof(f56,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc))))=multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f50])).
% 3.90/0.96 fof(f60,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f56,f13])).
% 3.90/0.96 fof(f67,plain,(
% 3.90/0.96 ![X0]: (inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))=inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f13,f60])).
% 3.90/0.96 fof(f78,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),X1))),a2),inverse(sF0_fnc))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f37])).
% 3.90/0.96 fof(f89,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f78])).
% 3.90/0.96 fof(f97,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))=X1)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f16,f13])).
% 3.90/0.96 fof(f104,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))))=X0)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f97])).
% 3.90/0.96 fof(f108,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a2),inverse(sF0_fnc))))))=multiply(inverse(inverse(X1)),X2))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f16,f97])).
% 3.90/0.96 fof(f121,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))))=multiply(inverse(inverse(X0)),X1))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f16,f104])).
% 3.90/0.96 fof(f122,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc)))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),X0))),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f104])).
% 3.90/0.96 fof(f125,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc))))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f126,f89])).
% 3.90/0.96 fof(f126,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc)))))=multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f122])).
% 3.90/0.96 fof(f128,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,X0))=multiply(inverse(inverse(b2)),multiply(sF2_fnc,X0)))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f18,f121])).
% 3.90/0.96 fof(f129,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(sF2_fnc,multiply(b2,X0))=multiply(inverse(inverse(X1)),multiply(inverse(X1),X0)))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f121])).
% 3.90/0.96 fof(f134,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,X0))=multiply(inverse(sF2_fnc),multiply(sF2_fnc,X0)))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f5,f128])).
% 3.90/0.96 fof(f144,plain,(
% 3.90/0.96 ![X0]: (inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),a2),inverse(sF0_fnc)))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f134,f67])).
% 3.90/0.96 fof(f148,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc))))=X0)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f144,f18])).
% 3.90/0.96 fof(f173,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)))),X2))),a2),inverse(sF0_fnc))))))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f17])).
% 3.90/0.96 fof(f180,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(inverse(X0))),X1))),a2),inverse(sF0_fnc))))),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f13,f17])).
% 3.90/0.96 fof(f201,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a2),inverse(sF0_fnc)))))))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f173])).
% 3.90/0.96 fof(f203,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f16,f180])).
% 3.90/0.96 fof(f207,plain,(
% 3.90/0.96 ![X0,X1,X2]: (inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))=inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f13,f203])).
% 3.90/0.96 fof(f231,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f104,f148])).
% 3.90/0.96 fof(f232,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X0)),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f148,f148])).
% 3.90/0.96 fof(f236,plain,(
% 3.90/0.96 multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),b2),inverse(sF1_fnc)))))=b2),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f47])).
% 3.90/0.96 fof(f237,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),b2),inverse(sF1_fnc)))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f16])).
% 3.90/0.96 fof(f238,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),b2),inverse(sF1_fnc)))))=X1)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f13])).
% 3.90/0.96 fof(f239,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))))=multiply(inverse(inverse(X0)),X1))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f121])).
% 3.90/0.96 fof(f240,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))))=X0)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f104])).
% 3.90/0.96 fof(f241,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f67])).
% 3.90/0.96 fof(f259,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f207])).
% 3.90/0.96 fof(f264,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))=inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(b2,inverse(multiply(multiply(inverse(X2),b2),inverse(sF1_fnc))))))))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f201])).
% 3.90/0.96 fof(f267,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc)))))=multiply(sF1_fnc,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f126])).
% 3.90/0.96 fof(f268,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,multiply(X1,multiply(b2,inverse(multiply(multiply(inverse(X2),b2),inverse(sF1_fnc)))))))=multiply(inverse(inverse(X1)),X2))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f108])).
% 3.90/0.96 fof(f274,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(inverse(inverse(X0)),X1))),X2),inverse(multiply(b2,X2)))))),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f36])).
% 3.90/0.96 fof(f276,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))))))=X3)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f231,f24])).
% 3.90/0.96 fof(f277,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X0)),b2),inverse(sF1_fnc)))))=X0)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f232,f148])).
% 3.90/0.96 fof(f282,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))=multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),b2),inverse(sF1_fnc)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f231,f237])).
% 3.90/0.96 fof(f301,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))=inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(b2,inverse(multiply(multiply(inverse(X2),b2),inverse(sF1_fnc))))))))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f231,f264])).
% 3.90/0.96 fof(f304,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.96 inference(backward_demodulation,[status(thm)],[f267,f125])).
% 3.90/0.96 fof(f320,plain,(
% 3.90/0.96 multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))))=b2),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f240])).
% 3.90/0.96 fof(f323,plain,(
% 3.90/0.96 multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))=b2),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f6,f320])).
% 3.90/0.96 fof(f413,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(X0),multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))=X1)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f282,f238])).
% 3.90/0.96 fof(f436,plain,(
% 3.90/0.96 ![X0]: (multiply(inverse(X0),multiply(X0,multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))))=b2)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f413])).
% 3.90/0.96 fof(f443,plain,(
% 3.90/0.96 ![X0]: (multiply(inverse(X0),multiply(X0,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))=b2)),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f6,f436])).
% 3.90/0.96 fof(f451,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))=multiply(inverse(inverse(X0)),b2))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f443,f129])).
% 3.90/0.96 fof(f494,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(inverse(b2)),multiply(sF2_fnc,X1)))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f277,f268])).
% 3.90/0.96 fof(f510,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(inverse(sF2_fnc),multiply(sF2_fnc,X1)))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f5,f494])).
% 3.90/0.96 fof(f518,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=multiply(sF2_fnc,multiply(b2,X1)))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f134,f510])).
% 3.90/0.96 fof(f535,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,X1)))=multiply(sF2_fnc,multiply(b2,multiply(X0,X1))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f518,f518])).
% 3.90/0.96 fof(f536,plain,(
% 3.90/0.96 multiply(inverse(sF1_fnc),sF0_fnc)=multiply(sF2_fnc,multiply(b2,a2))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f7,f518])).
% 3.90/0.96 fof(f627,plain,(
% 3.90/0.96 ![X0]: (multiply(inverse(inverse(X0)),multiply(inverse(sF1_fnc),sF0_fnc))=multiply(sF2_fnc,multiply(b2,multiply(X0,a2))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f536,f535])).
% 3.90/0.96 fof(f658,plain,(
% 3.90/0.96 ![X0]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc)))))=multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,multiply(X0,a2)))),b2),inverse(sF1_fnc)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f627,f282])).
% 3.90/0.96 fof(f662,plain,(
% 3.90/0.96 ![X0]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc)))))=multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(X0,a2))),b2),inverse(sF1_fnc))))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f232,f658])).
% 3.90/0.96 fof(f664,plain,(
% 3.90/0.96 ![X0]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc)))))=multiply(X0,a2))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f277,f662])).
% 3.90/0.96 fof(f690,plain,(
% 3.90/0.96 ![X0]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(X0),a2)),b2),inverse(sF1_fnc)))))=multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f664,f238])).
% 3.90/0.96 fof(f703,plain,(
% 3.90/0.96 a2=multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f238,f690])).
% 3.90/0.96 fof(f713,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(inverse(X0))),X1)),b2),inverse(sF1_fnc))))),b2),inverse(sF1_fnc)))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),X2),inverse(multiply(b2,X2)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f238,f274])).
% 3.90/0.96 fof(f738,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))),b2),inverse(sF1_fnc)))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),X2),inverse(multiply(b2,X2)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f282,f713])).
% 3.90/0.96 fof(f742,plain,(
% 3.90/0.96 ![X0,X1]: (multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(sF2_fnc,X0)),X1),inverse(multiply(b2,X1)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f238,f738])).
% 3.90/0.96 fof(f760,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),X0)),b2),inverse(sF1_fnc))))),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f238,f231])).
% 3.90/0.96 fof(f768,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))),b2),inverse(sF1_fnc))))))=multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f231,f240])).
% 3.90/0.96 fof(f769,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))))),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f282,f760])).
% 3.90/0.96 fof(f784,plain,(
% 3.90/0.96 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))),b2),inverse(sF1_fnc))))))=multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc)))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f241,f240])).
% 3.90/0.96 fof(f810,plain,(
% 3.90/0.96 ![X0]: (multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))=multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc)))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f768,f784])).
% 3.90/0.96 fof(f879,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f6,f742])).
% 3.90/0.96 fof(f900,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f5,f879])).
% 3.90/0.96 fof(f901,plain,(
% 3.90/0.96 ![X0]: (multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f6,f900])).
% 3.90/0.96 fof(f944,plain,(
% 3.90/0.96 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))))))=inverse(multiply(X4,inverse(multiply(X5,multiply(multiply(inverse(X5),multiply(inverse(inverse(X0)),X3)),multiply(b2,inverse(multiply(multiply(inverse(X4),b2),inverse(sF1_fnc))))))))))),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f276,f276])).
% 3.90/0.96 fof(f948,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),a2))))))=X2)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f703,f276])).
% 3.90/0.96 fof(f952,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(b2,inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))))))))=X2)),
% 3.90/0.96 inference(paramodulation,[status(thm)],[f5,f276])).
% 3.90/0.96 fof(f969,plain,(
% 3.90/0.96 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))))))=multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X3),b2),inverse(sF1_fnc))))))),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f301,f944])).
% 3.90/0.96 fof(f974,plain,(
% 3.90/0.96 ![X0,X1,X2]: (multiply(X0,inverse(multiply(b2,inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))))=X2)),
% 3.90/0.96 inference(forward_demodulation,[status(thm)],[f6,f952])).
% 3.90/0.97 fof(f989,plain,(
% 3.90/0.97 multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(sF1_fnc),multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),b2),inverse(sF1_fnc))))),inverse(b2)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f236,f901])).
% 3.90/0.97 fof(f1000,plain,(
% 3.90/0.97 multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(sF1_fnc),multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),b2),inverse(sF1_fnc))))),sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f5,f989])).
% 3.90/0.97 fof(f1011,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(X0),multiply(multiply(sF2_fnc,multiply(b2,X1)),a2))))))=X1)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f518,f948])).
% 3.90/0.97 fof(f1118,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(sF2_fnc,multiply(b2,a2))))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f518,f1011])).
% 3.90/0.97 fof(f1144,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc)))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f536,f1118])).
% 3.90/0.97 fof(f1182,plain,(
% 3.90/0.97 multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc)))))=multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f323,f1144])).
% 3.90/0.97 fof(f1193,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0)=multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc)))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1144,f518])).
% 3.90/0.97 fof(f1210,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0)=multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1182,f1193])).
% 3.90/0.97 fof(f1215,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(X0),multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))))=multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f240,f1210])).
% 3.90/0.97 fof(f1225,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),b2),inverse(sF1_fnc)))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f238])).
% 3.90/0.97 fof(f1227,plain,(
% 3.90/0.97 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))=multiply(inverse(inverse(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))))))),X0))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f239])).
% 3.90/0.97 fof(f1229,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),multiply(inverse(multiply(sF2_fnc,multiply(b2,X1))),X1))=multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f535])).
% 3.90/0.97 fof(f1232,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(sF2_fnc),multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0))=multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f518])).
% 3.90/0.97 fof(f1233,plain,(
% 3.90/0.97 multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),sF2_fnc))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1215,f1000])).
% 3.90/0.97 fof(f1238,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),b2),inverse(sF1_fnc))))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f232,f1225])).
% 3.90/0.97 fof(f1239,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f277,f1238])).
% 3.90/0.97 fof(f1242,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(sF2_fnc)),b2)=multiply(inverse(inverse(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))))))),X0))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f451,f1227])).
% 3.90/0.97 fof(f1243,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(sF2_fnc)),b2)=multiply(inverse(inverse(inverse(X0))),X0))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f240,f1242])).
% 3.90/0.97 fof(f1245,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(sF2_fnc),multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0))=b2)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f323,f1232])).
% 3.90/0.97 fof(f1295,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f627,f1243])).
% 3.90/0.97 fof(f1307,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(sF2_fnc)),b2)),b2),inverse(sF1_fnc)))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1243,f238])).
% 3.90/0.97 fof(f1310,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(inverse(inverse(X0)))),multiply(inverse(inverse(sF2_fnc)),b2))=multiply(sF2_fnc,multiply(b2,X0)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1243,f518])).
% 3.90/0.97 fof(f1316,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc))))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f282,f1307])).
% 3.90/0.97 fof(f1317,plain,(
% 3.90/0.97 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc))))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f535,f1316])).
% 3.90/0.97 fof(f1318,plain,(
% 3.90/0.97 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f5,f1317])).
% 3.90/0.97 fof(f1320,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),multiply(inverse(multiply(sF2_fnc,multiply(b2,X1))),X1))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1321,f1229])).
% 3.90/0.97 fof(f1321,plain,(
% 3.90/0.97 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f6,f1318])).
% 3.90/0.97 fof(f1322,plain,(
% 3.90/0.97 multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))=inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f1321])).
% 3.90/0.97 fof(f1326,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1321,f535])).
% 3.90/0.97 fof(f1327,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))))=multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1321,f277])).
% 3.90/0.97 fof(f1329,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f451,f1322])).
% 3.90/0.97 fof(f1333,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,multiply(multiply(sF2_fnc,X0),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1327,f277])).
% 3.90/0.97 fof(f1360,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1210,f1239])).
% 3.90/0.97 fof(f1361,plain,(
% 3.90/0.97 multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=a2),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f536,f1239])).
% 3.90/0.97 fof(f1363,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f239,f1239])).
% 3.90/0.97 fof(f1365,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f238,f1239])).
% 3.90/0.97 fof(f1377,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(multiply(multiply(inverse(inverse(sF1_fnc)),X0),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),b2),inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1363,f769])).
% 3.90/0.97 fof(f1378,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(inverse(inverse(sF1_fnc)),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1363,f304])).
% 3.90/0.97 fof(f1407,plain,(
% 3.90/0.97 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))))=multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X3),b2),inverse(sF1_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1363,f969])).
% 3.90/0.97 fof(f1439,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc))))=multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1440,f231])).
% 3.90/0.97 fof(f1440,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f810,f1365])).
% 3.90/0.97 fof(f1479,plain,(
% 3.90/0.97 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(inverse(multiply(inverse(X2),X3))),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))))=multiply(multiply(inverse(inverse(X0)),X3),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1363,f1407])).
% 3.90/0.97 fof(f1491,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(multiply(inverse(inverse(sF1_fnc)),X0),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1439,f1377])).
% 3.90/0.97 fof(f1504,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1439,f1363])).
% 3.90/0.97 fof(f1520,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1439,f259])).
% 3.90/0.97 fof(f1527,plain,(
% 3.90/0.97 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))))=multiply(multiply(inverse(inverse(X0)),X3),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1504,f1479])).
% 3.90/0.97 fof(f1544,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1504,f1491])).
% 3.90/0.97 fof(f1547,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1504,f1378])).
% 3.90/0.97 fof(f1581,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))=X1)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1582,f974])).
% 3.90/0.97 fof(f1582,plain,(
% 3.90/0.97 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X3),multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))))=multiply(X0,multiply(X3,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1504,f1527])).
% 3.90/0.97 fof(f1592,plain,(
% 3.90/0.97 multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)=multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1361,f518])).
% 3.90/0.97 fof(f1593,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0)=multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1592,f1210])).
% 3.90/0.97 fof(f1595,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1592,f1329])).
% 3.90/0.97 fof(f1596,plain,(
% 3.90/0.97 multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),sF2_fnc))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1592,f1233])).
% 3.90/0.97 fof(f1600,plain,(
% 3.90/0.97 multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1593,f1360])).
% 3.90/0.97 fof(f1601,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1593,f1320])).
% 3.90/0.97 fof(f1602,plain,(
% 3.90/0.97 multiply(inverse(sF2_fnc),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=b2),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f1593,f1245])).
% 3.90/0.97 fof(f1674,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(inverse(inverse(sF2_fnc)),b2)),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),X0))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1595,f535])).
% 3.90/0.97 fof(f1736,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF2_fnc)),b2))=multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1295,f535])).
% 3.90/0.97 fof(f1818,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),sF2_fnc)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1596,f1601])).
% 3.90/0.97 fof(f1831,plain,(
% 3.90/0.97 ![X0]: (multiply(a2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(multiply(inverse(inverse(sF2_fnc)),b2),X0),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),X0)))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1595,f1520])).
% 3.90/0.97 fof(f1840,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(b2),X0),inverse(multiply(sF2_fnc,X0)))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1602,f1520])).
% 3.90/0.97 fof(f1912,plain,(
% 3.90/0.97 ![X0]: (inverse(multiply(sF1_fnc,inverse(sF1_fnc)))=inverse(multiply(multiply(inverse(b2),X0),inverse(multiply(sF2_fnc,X0)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1600,f1840])).
% 3.90/0.97 fof(f1913,plain,(
% 3.90/0.97 ![X0]: (inverse(multiply(sF1_fnc,inverse(sF1_fnc)))=inverse(multiply(multiply(sF2_fnc,X0),inverse(multiply(sF2_fnc,X0)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f5,f1912])).
% 3.90/0.97 fof(f1952,plain,(
% 3.90/0.97 ![X0]: (inverse(multiply(sF1_fnc,inverse(sF1_fnc)))=inverse(multiply(X0,inverse(multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1321,f1913])).
% 3.90/0.97 fof(f1981,plain,(
% 3.90/0.97 ![X0]: (inverse(multiply(sF1_fnc,inverse(sF1_fnc)))=inverse(multiply(X0,inverse(X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1321,f1952])).
% 3.90/0.97 fof(f2012,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),X1)=multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2))))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1326])).
% 3.90/0.97 fof(f2013,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)=multiply(sF2_fnc,multiply(b2,inverse(multiply(X0,inverse(X0))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1592])).
% 3.90/0.97 fof(f2014,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(X2,inverse(X2)))))=X1)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1581])).
% 3.90/0.97 fof(f2015,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(b2,multiply(multiply(sF2_fnc,X0),inverse(multiply(X1,inverse(X1)))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1333])).
% 3.90/0.97 fof(f2017,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(X1,inverse(X1))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1239])).
% 3.90/0.97 fof(f2019,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(X1,inverse(X1))))))=X0)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1321])).
% 3.90/0.97 fof(f2025,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=multiply(sF1_fnc,inverse(sF1_fnc)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1601])).
% 3.90/0.97 fof(f2026,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(sF2_fnc)),b2)=multiply(inverse(inverse(inverse(multiply(X0,inverse(X0))))),multiply(sF1_fnc,inverse(sF1_fnc))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1981,f1243])).
% 3.90/0.97 fof(f2054,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,inverse(X0))=multiply(sF1_fnc,inverse(sF1_fnc)))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1601,f2025])).
% 3.90/0.97 fof(f2070,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(X1,inverse(X1)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2054,f2054])).
% 3.90/0.97 fof(f2076,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(X0),multiply(sF1_fnc,inverse(sF1_fnc)))=multiply(sF2_fnc,multiply(b2,inverse(X0))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2054,f518])).
% 3.90/0.97 fof(f2084,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(sF2_fnc)),b2)=multiply(sF2_fnc,multiply(b2,inverse(inverse(inverse(multiply(X0,inverse(X0))))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2076,f2026])).
% 3.90/0.97 fof(f2092,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,sF2_fnc)=multiply(X0,inverse(X0)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f5,f2070])).
% 3.90/0.97 fof(f2095,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,inverse(X0))=multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),multiply(inverse(inverse(sF2_fnc)),b2)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f1595,f2070])).
% 3.90/0.97 fof(f2105,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(inverse(multiply(inverse(X2),X0))))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2070,f1520])).
% 3.90/0.97 fof(f2108,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),X2),inverse(multiply(X0,X2)))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2070,f1520])).
% 3.90/0.97 fof(f2110,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(X0),multiply(X1,inverse(X1)))=multiply(sF2_fnc,multiply(b2,inverse(X0))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2070,f518])).
% 3.90/0.97 fof(f2197,plain,(
% 3.90/0.97 ![X0]: (multiply(a2,inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(multiply(inverse(inverse(sF2_fnc)),b2),X0),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),X0)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f1831])).
% 3.90/0.97 fof(f2203,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f1818])).
% 3.90/0.97 fof(f2230,plain,(
% 3.90/0.97 multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f1600])).
% 3.90/0.97 fof(f2250,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,multiply(X1,inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f1547])).
% 3.90/0.97 fof(f2253,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF1_fnc,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f1544])).
% 3.90/0.97 fof(f2302,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=multiply(sF2_fnc,multiply(b2,inverse(inverse(inverse(multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2084])).
% 3.90/0.97 fof(f2304,plain,(
% 3.90/0.97 ![X0]: (multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(b2,sF2_fnc)))))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2019])).
% 3.90/0.97 fof(f2306,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(b2,sF2_fnc)))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2017])).
% 3.90/0.97 fof(f2308,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,multiply(multiply(sF2_fnc,X0),inverse(multiply(b2,sF2_fnc))))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2015])).
% 3.90/0.97 fof(f2309,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(b2,sF2_fnc))))=X1)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2014])).
% 3.90/0.97 fof(f2310,plain,(
% 3.90/0.97 multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)=multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2013])).
% 3.90/0.97 fof(f2311,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,inverse(multiply(b2,sF2_fnc)))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2092,f2012])).
% 3.90/0.97 fof(f2315,plain,(
% 3.90/0.97 multiply(b2,sF2_fnc)=multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),multiply(inverse(inverse(sF2_fnc)),b2))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2095])).
% 3.90/0.97 fof(f2336,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,inverse(inverse(multiply(inverse(X2),X0))))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2105])).
% 3.90/0.97 fof(f2337,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,inverse(inverse(multiply(inverse(X1),X0))))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2336])).
% 3.90/0.97 fof(f2341,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(inverse(multiply(X1,inverse(X1))),X2),inverse(multiply(X0,X2)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2108])).
% 3.90/0.97 fof(f2342,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),inverse(multiply(X0,X1)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2341])).
% 3.90/0.97 fof(f2345,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(X0),multiply(b2,sF2_fnc))=multiply(sF2_fnc,multiply(b2,inverse(X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2110])).
% 3.90/0.97 fof(f2429,plain,(
% 3.90/0.97 multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2230])).
% 3.90/0.97 fof(f2440,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF1_fnc,multiply(X0,inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2253])).
% 3.90/0.97 fof(f2671,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc))))=inverse(inverse(X0)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2092,f2309])).
% 3.90/0.97 fof(f2704,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(inverse(X0)))=multiply(sF2_fnc,multiply(b2,inverse(X0))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2706,f2345])).
% 3.90/0.97 fof(f2706,plain,(
% 3.90/0.97 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=inverse(inverse(X0)))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2092,f2671])).
% 3.90/0.97 fof(f2715,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2704,f2302])).
% 3.90/0.97 fof(f2718,plain,(
% 3.90/0.97 multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)=inverse(inverse(inverse(multiply(b2,sF2_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2704,f2310])).
% 3.90/0.97 fof(f2726,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f1595])).
% 3.90/0.97 fof(f2728,plain,(
% 3.90/0.97 multiply(inverse(sF2_fnc),inverse(inverse(inverse(multiply(b2,sF2_fnc)))))=b2),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f1602])).
% 3.90/0.97 fof(f2730,plain,(
% 3.90/0.97 multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f2429])).
% 3.90/0.97 fof(f2741,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))=multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f2203])).
% 3.90/0.97 fof(f2753,plain,(
% 3.90/0.97 multiply(b2,sF2_fnc)=multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),multiply(inverse(inverse(sF2_fnc)),b2))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f2315])).
% 3.90/0.97 fof(f2754,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF2_fnc)),b2))=multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(inverse(inverse(multiply(b2,sF2_fnc))))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f1736])).
% 3.90/0.97 fof(f2757,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(inverse(inverse(sF2_fnc)),b2)),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),X0))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2718,f1674])).
% 3.90/0.97 fof(f2761,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(multiply(inverse(inverse(sF2_fnc)),b2))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2726,f2715])).
% 3.90/0.97 fof(f2769,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),inverse(inverse(inverse(multiply(b2,sF2_fnc)))))=multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2718,f2741])).
% 3.90/0.97 fof(f2772,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(inverse(inverse(sF2_fnc)),b2),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),X0))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2761,f2757])).
% 3.90/0.97 fof(f2808,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),inverse(multiply(b2,sF2_fnc)))=sF2_fnc),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2706,f2306])).
% 3.90/0.97 fof(f2834,plain,(
% 3.90/0.97 multiply(inverse(sF2_fnc),multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2808,f2309])).
% 3.90/0.97 fof(f2838,plain,(
% 3.90/0.97 multiply(inverse(inverse(inverse(sF2_fnc))),sF2_fnc)=multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f2808,f518])).
% 3.90/0.97 fof(f2839,plain,(
% 3.90/0.97 multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc))))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f518,f2834])).
% 3.90/0.97 fof(f2845,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(inverse(inverse(sF2_fnc)),b2),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(b2,sF2_fnc)),X0))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2772])).
% 3.90/0.97 fof(f2850,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF2_fnc)),b2))=multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2754])).
% 3.90/0.97 fof(f2851,plain,(
% 3.90/0.97 multiply(b2,sF2_fnc)=multiply(inverse(multiply(b2,sF2_fnc)),multiply(inverse(inverse(sF2_fnc)),b2))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2753])).
% 3.90/0.97 fof(f2862,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),inverse(inverse(inverse(multiply(b2,sF2_fnc)))))=multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2769])).
% 3.90/0.97 fof(f2870,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(b2,sF2_fnc)))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2730])).
% 3.90/0.97 fof(f2872,plain,(
% 3.90/0.97 multiply(inverse(sF2_fnc),inverse(multiply(b2,sF2_fnc)))=b2),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2878,f2728])).
% 3.90/0.97 fof(f2878,plain,(
% 3.90/0.97 inverse(inverse(inverse(multiply(b2,sF2_fnc))))=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2704,f2839])).
% 3.90/0.97 fof(f2880,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f1243,f2838])).
% 3.90/0.97 fof(f2881,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(inverse(inverse(multiply(b2,sF2_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2704,f2880])).
% 3.90/0.97 fof(f2882,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(inverse(inverse(X0)))),inverse(multiply(b2,sF2_fnc)))=multiply(sF2_fnc,multiply(b2,X0)))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2908,f1310])).
% 3.90/0.97 fof(f2897,plain,(
% 3.90/0.97 ![X0]: (multiply(a2,inverse(multiply(b2,sF2_fnc)))=inverse(multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),X0)))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f2908,f2197])).
% 3.90/0.97 fof(f2908,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2878,f2881])).
% 3.90/0.97 fof(f2910,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(b2,sF2_fnc)),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(b2,sF2_fnc)),X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2908,f2845])).
% 3.90/0.97 fof(f2914,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),inverse(multiply(b2,sF2_fnc)))=multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2908,f2850])).
% 3.90/0.97 fof(f2918,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(X0)),inverse(multiply(b2,sF2_fnc)))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2304,f2914])).
% 3.90/0.97 fof(f2920,plain,(
% 3.90/0.97 multiply(b2,sF2_fnc)=multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(b2,sF2_fnc)))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2908,f2851])).
% 3.90/0.97 fof(f2924,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc)))=multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2878,f2862])).
% 3.90/0.97 fof(f2926,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,multiply(multiply(inverse(X0),X1),multiply(b2,sF2_fnc)))=X1)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2309])).
% 3.90/0.97 fof(f2928,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,multiply(multiply(sF2_fnc,X0),multiply(b2,sF2_fnc)))=X0)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2308])).
% 3.90/0.97 fof(f2941,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc)))=multiply(multiply(b2,sF2_fnc),sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2924])).
% 3.90/0.97 fof(f2957,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(multiply(b2,sF2_fnc)),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(multiply(b2,sF2_fnc),X0))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2910])).
% 3.90/0.97 fof(f2962,plain,(
% 3.90/0.97 multiply(inverse(inverse(sF2_fnc)),b2)=multiply(b2,sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2908])).
% 3.90/0.97 fof(f2970,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2311])).
% 3.90/0.97 fof(f3010,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(sF1_fnc,multiply(X0,inverse(multiply(b2,sF2_fnc)))),multiply(b2,sF2_fnc))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2440])).
% 3.90/0.97 fof(f3012,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,multiply(X1,multiply(b2,sF2_fnc))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2250])).
% 3.90/0.97 fof(f3070,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,multiply(b2,sF2_fnc))=inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,inverse(inverse(multiply(inverse(X1),X0))))))))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3073,f2337])).
% 3.90/0.97 fof(f3073,plain,(
% 3.90/0.97 multiply(b2,sF2_fnc)=inverse(multiply(b2,sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2920,f2870])).
% 3.90/0.97 fof(f3077,plain,(
% 3.90/0.97 multiply(inverse(sF2_fnc),multiply(b2,sF2_fnc))=b2),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f2872])).
% 3.90/0.97 fof(f3079,plain,(
% 3.90/0.97 inverse(inverse(inverse(sF2_fnc)))=b2),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3077])).
% 3.90/0.97 fof(f3096,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=inverse(inverse(X1)))),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3107,f518])).
% 3.90/0.97 fof(f3107,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(X0))=multiply(sF2_fnc,multiply(b2,X0)))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2918,f2882])).
% 3.90/0.97 fof(f3164,plain,(
% 3.90/0.97 ![X0]: (multiply(a2,multiply(b2,sF2_fnc))=inverse(multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),X0)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f2897])).
% 3.90/0.97 fof(f3165,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(a2))=inverse(multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),X0)))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3164])).
% 3.90/0.97 fof(f3166,plain,(
% 3.90/0.97 inverse(inverse(a2))=multiply(inverse(inverse(multiply(inverse(sF1_fnc),sF0_fnc))),inverse(multiply(b2,sF2_fnc)))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2342,f3165])).
% 3.90/0.97 fof(f3168,plain,(
% 3.90/0.97 inverse(inverse(a2))=multiply(inverse(sF1_fnc),sF0_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2918,f3166])).
% 3.90/0.97 fof(f3228,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(X0,inverse(inverse(multiply(inverse(X0),X1))))=X1)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f2926])).
% 3.90/0.97 fof(f3231,plain,(
% 3.90/0.97 ![X0]: (multiply(b2,inverse(inverse(multiply(sF2_fnc,X0))))=X0)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f2928])).
% 3.90/0.97 fof(f3263,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,multiply(b2,sF2_fnc))),inverse(multiply(b2,sF2_fnc)))=multiply(multiply(b2,sF2_fnc),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f2941])).
% 3.90/0.97 fof(f3264,plain,(
% 3.90/0.97 multiply(inverse(inverse(inverse(b2))),inverse(multiply(b2,sF2_fnc)))=multiply(multiply(b2,sF2_fnc),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3263])).
% 3.90/0.97 fof(f3265,plain,(
% 3.90/0.97 inverse(b2)=multiply(multiply(b2,sF2_fnc),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2918,f3264])).
% 3.90/0.97 fof(f3267,plain,(
% 3.90/0.97 sF2_fnc=multiply(multiply(b2,sF2_fnc),sF2_fnc)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f5,f3265])).
% 3.90/0.97 fof(f3318,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(b2,sF2_fnc),multiply(sF2_fnc,multiply(b2,X0)))=multiply(sF2_fnc,multiply(b2,multiply(multiply(b2,sF2_fnc),X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f2957])).
% 3.90/0.97 fof(f3319,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(b2,sF2_fnc),inverse(inverse(X0)))=multiply(sF2_fnc,multiply(b2,multiply(multiply(b2,sF2_fnc),X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3107,f3318])).
% 3.90/0.97 fof(f3320,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(b2,sF2_fnc),inverse(inverse(X0)))=inverse(inverse(multiply(multiply(b2,sF2_fnc),X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3107,f3319])).
% 3.90/0.97 fof(f3357,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=inverse(inverse(multiply(X0,multiply(X1,multiply(b2,sF2_fnc))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3107,f2970])).
% 3.90/0.97 fof(f3358,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(X0)),X1)=inverse(inverse(multiply(X0,inverse(inverse(X1))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3357])).
% 3.90/0.97 fof(f3483,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(multiply(sF1_fnc,multiply(X0,inverse(multiply(b2,sF2_fnc))))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3010])).
% 3.90/0.97 fof(f3484,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(multiply(sF1_fnc,multiply(X0,multiply(b2,sF2_fnc)))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f3483])).
% 3.90/0.97 fof(f3485,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(multiply(sF1_fnc,inverse(inverse(X0)))))=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3484])).
% 3.90/0.97 fof(f3488,plain,(
% 3.90/0.97 ![X0]: (multiply(inverse(inverse(sF1_fnc)),X0)=inverse(multiply(multiply(inverse(X0),a2),inverse(sF0_fnc))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3358,f3485])).
% 3.90/0.97 fof(f3492,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,inverse(inverse(X1))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),inverse(multiply(multiply(inverse(X1),a2),inverse(sF0_fnc)))))))))=X2)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3012])).
% 3.90/0.97 fof(f3493,plain,(
% 3.90/0.97 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(sF1_fnc,inverse(inverse(X1))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(X0),X2)),multiply(inverse(inverse(sF1_fnc)),X1)))))))=X2)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3488,f3492])).
% 3.90/0.97 fof(f3710,plain,(
% 3.90/0.97 ![X0,X1]: (inverse(inverse(X0))=inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,inverse(inverse(multiply(inverse(X1),X0))))))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f2706,f3070])).
% 3.90/0.97 fof(f3712,plain,(
% 3.90/0.97 ![X0]: (inverse(inverse(X0))=inverse(multiply(multiply(b2,sF2_fnc),inverse(X0))))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3228,f3710])).
% 3.90/0.97 fof(f3847,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(sF2_fnc)),inverse(multiply(multiply(sF1_fnc,inverse(inverse(X0))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(b2,X1)),multiply(inverse(inverse(sF1_fnc)),X0)))))))=X1)),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f3079,f3493])).
% 3.90/0.97 fof(f3853,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(b2,inverse(inverse(X0)))=inverse(multiply(multiply(sF1_fnc,inverse(inverse(X1))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(sF2_fnc),X0)),multiply(inverse(inverse(sF1_fnc)),X1)))))))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f3493,f3231])).
% 3.90/0.97 fof(f3873,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(inverse(inverse(sF2_fnc)),inverse(multiply(multiply(sF1_fnc,inverse(inverse(X0))),inverse(multiply(b2,multiply(inverse(inverse(X1)),multiply(inverse(inverse(sF1_fnc)),X0)))))))=X1)),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3107,f3847])).
% 3.90/0.97 fof(f3932,plain,(
% 3.90/0.97 ![X0]: (multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X0))=inverse(inverse(X0)))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f3073,f3096])).
% 3.90/0.97 fof(f3936,plain,(
% 3.90/0.97 multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)=inverse(inverse(sF2_fnc))),
% 3.90/0.97 inference(paramodulation,[status(thm)],[f3267,f3096])).
% 3.90/0.97 fof(f3952,plain,(
% 3.90/0.97 multiply(multiply(b2,sF2_fnc),sF2_fnc)=inverse(inverse(sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3073,f3936])).
% 3.90/0.97 fof(f3953,plain,(
% 3.90/0.97 inverse(sF2_fnc)=b2),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3971,f3079])).
% 3.90/0.97 fof(f3954,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(sF2_fnc,inverse(multiply(multiply(sF1_fnc,inverse(inverse(X0))),inverse(multiply(b2,multiply(inverse(inverse(X1)),multiply(inverse(inverse(sF1_fnc)),X0)))))))=X1)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3971,f3873])).
% 3.90/0.97 fof(f3969,plain,(
% 3.90/0.97 multiply(sF2_fnc,b2)=multiply(b2,sF2_fnc)),
% 3.90/0.97 inference(backward_demodulation,[status(thm)],[f3971,f2962])).
% 3.90/0.97 fof(f3971,plain,(
% 3.90/0.97 sF2_fnc=inverse(inverse(sF2_fnc))),
% 3.90/0.97 inference(forward_demodulation,[status(thm)],[f3267,f3952])).
% 3.90/0.97 fof(f3987,plain,(
% 3.90/0.97 ![X0,X1]: (multiply(b2,inverse(inverse(X0)))=inverse(multiply(multiply(sF1_fnc,inverse(inverse(X1))),inverse(multiply(b2,multiply(multiply(sF2_fnc,multiply(b2,X0)),multiply(inverse(inverse(sF1_fnc)),X1)))))))),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f3953,f3853])).
% 3.90/0.98 fof(f4013,plain,(
% 3.90/0.98 multiply(b2,sF2_fnc)=inverse(sF1_fnc)),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4029,f3073])).
% 3.90/0.98 fof(f4015,plain,(
% 3.90/0.98 ![X0]: (multiply(X0,sF1_fnc)=inverse(inverse(X0)))),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4029,f2706])).
% 3.90/0.98 fof(f4019,plain,(
% 3.90/0.98 ![X0]: (multiply(multiply(b2,sF2_fnc),multiply(sF1_fnc,X0))=inverse(inverse(X0)))),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4029,f3932])).
% 3.90/0.98 fof(f4023,plain,(
% 3.90/0.98 ![X0]: (inverse(inverse(X0))=inverse(multiply(sF1_fnc,inverse(X0))))),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4029,f3712])).
% 3.90/0.98 fof(f4025,plain,(
% 3.90/0.98 ![X0]: (multiply(multiply(b2,sF2_fnc),inverse(inverse(X0)))=inverse(inverse(multiply(sF1_fnc,X0))))),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4029,f3320])).
% 3.90/0.98 fof(f4029,plain,(
% 3.90/0.98 sF1_fnc=multiply(b2,sF2_fnc)),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f6,f3969])).
% 3.90/0.98 fof(f4036,plain,(
% 3.90/0.98 ![X0]: (multiply(sF2_fnc,multiply(b2,inverse(inverse(X0))))=X0)),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4037,f3954])).
% 3.90/0.98 fof(f4037,plain,(
% 3.90/0.98 ![X0,X1]: (multiply(b2,inverse(inverse(X0)))=inverse(multiply(multiply(sF1_fnc,inverse(inverse(X1))),inverse(multiply(b2,multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF1_fnc)),X1)))))))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f3107,f3987])).
% 3.90/0.98 fof(f4059,plain,(
% 3.90/0.98 inverse(inverse(a2))=multiply(sF1_fnc,sF0_fnc)),
% 3.90/0.98 inference(backward_demodulation,[status(thm)],[f4083,f3168])).
% 3.90/0.98 fof(f4083,plain,(
% 3.90/0.98 sF1_fnc=inverse(sF1_fnc)),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4029,f4013])).
% 3.90/0.98 fof(f4140,plain,(
% 3.90/0.98 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=inverse(inverse(X0)))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4029,f4019])).
% 3.90/0.98 fof(f4141,plain,(
% 3.90/0.98 ![X0]: (multiply(sF1_fnc,multiply(sF1_fnc,X0))=multiply(X0,sF1_fnc))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4015,f4140])).
% 3.90/0.98 fof(f4147,plain,(
% 3.90/0.98 ![X0]: (multiply(X0,sF1_fnc)=inverse(multiply(sF1_fnc,inverse(X0))))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4015,f4023])).
% 3.90/0.98 fof(f4149,plain,(
% 3.90/0.98 ![X0]: (multiply(sF1_fnc,inverse(inverse(X0)))=inverse(inverse(multiply(sF1_fnc,X0))))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4029,f4025])).
% 3.90/0.98 fof(f4150,plain,(
% 3.90/0.98 ![X0]: (multiply(sF1_fnc,multiply(X0,sF1_fnc))=inverse(inverse(multiply(sF1_fnc,X0))))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4015,f4149])).
% 3.90/0.98 fof(f4152,plain,(
% 3.90/0.98 ![X0]: (multiply(sF1_fnc,multiply(X0,sF1_fnc))=multiply(multiply(sF1_fnc,X0),sF1_fnc))),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4015,f4150])).
% 3.90/0.98 fof(f4165,plain,(
% 3.90/0.98 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f3107,f4036])).
% 3.90/0.98 fof(f4166,plain,(
% 3.90/0.98 ![X0]: (multiply(inverse(inverse(X0)),sF1_fnc)=X0)),
% 3.90/0.98 inference(forward_demodulation,[status(thm)],[f4015,f4165])).
% 3.90/0.98 fof(f4167,plain,(
% 3.90/0.98 ![X0]: (multiply(multiply(X0,sF1_fnc),sF1_fnc)=X0)),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4015,f4166])).
% 3.90/0.99 fof(f4184,plain,(
% 3.90/0.99 multiply(a2,sF1_fnc)=multiply(sF1_fnc,sF0_fnc)),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4015,f4059])).
% 3.90/0.99 fof(f4331,plain,(
% 3.90/0.99 ![X0]: (multiply(inverse(X0),sF1_fnc)=inverse(multiply(X0,sF1_fnc)))),
% 3.90/0.99 inference(paramodulation,[status(thm)],[f4015,f4015])).
% 3.90/0.99 fof(f4656,plain,(
% 3.90/0.99 ![X0]: (multiply(multiply(sF1_fnc,inverse(X0)),sF1_fnc)=inverse(multiply(sF1_fnc,multiply(X0,sF1_fnc))))),
% 3.90/0.99 inference(paramodulation,[status(thm)],[f4147,f4147])).
% 3.90/0.99 fof(f4657,plain,(
% 3.90/0.99 ![X0]: (multiply(multiply(X0,sF1_fnc),sF1_fnc)=inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))),
% 3.90/0.99 inference(paramodulation,[status(thm)],[f4331,f4147])).
% 3.90/0.99 fof(f4673,plain,(
% 3.90/0.99 ![X0]: (multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))=inverse(multiply(sF1_fnc,multiply(X0,sF1_fnc))))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4152,f4656])).
% 3.90/0.99 fof(f4674,plain,(
% 3.90/0.99 ![X0]: (X0=inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4167,f4657])).
% 3.90/0.99 fof(f4675,plain,(
% 3.90/0.99 ![X0]: (X0=multiply(sF1_fnc,multiply(inverse(inverse(X0)),sF1_fnc)))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4673,f4674])).
% 3.90/0.99 fof(f4676,plain,(
% 3.90/0.99 ![X0]: (X0=multiply(sF1_fnc,multiply(multiply(X0,sF1_fnc),sF1_fnc)))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4015,f4675])).
% 3.90/0.99 fof(f4678,plain,(
% 3.90/0.99 ![X0]: (multiply(sF1_fnc,X0)=multiply(X0,sF1_fnc))),
% 3.90/0.99 inference(backward_demodulation,[status(thm)],[f4726,f4141])).
% 3.90/0.99 fof(f4679,plain,(
% 3.90/0.99 multiply(a2,sF1_fnc)=sF0_fnc),
% 3.90/0.99 inference(backward_demodulation,[status(thm)],[f4726,f4184])).
% 3.90/0.99 fof(f4726,plain,(
% 3.90/0.99 ![X0]: (X0=multiply(sF1_fnc,X0))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4167,f4676])).
% 3.90/0.99 fof(f4843,plain,(
% 3.90/0.99 ![X0]: (X0=multiply(X0,sF1_fnc))),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4726,f4678])).
% 3.90/0.99 fof(f4844,plain,(
% 3.90/0.99 a2=sF0_fnc),
% 3.90/0.99 inference(forward_demodulation,[status(thm)],[f4843,f4679])).
% 3.90/0.99 fof(f4845,plain,(
% 3.90/0.99 $false),
% 3.90/0.99 inference(forward_subsumption_resolution,[status(thm)],[f4844,f8])).
% 3.90/0.99 % SZS output end CNFRefutation for theBenchmark.p
% 0.29/1.01 % Elapsed time: 0.625539 seconds
% 0.29/1.01 % CPU time: 4.700899 seconds
% 0.29/1.01 % Total memory used: 142.148 MB
% 0.29/1.01 % Net memory used: 138.336 MB
%------------------------------------------------------------------------------