%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP442-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:38 PM UTC 2026
% Result : Unsatisfiable 7.21s 6.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP442-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n010.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 20 20:14:02 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 7.21/6.40 % Refutation found
% 7.21/6.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.21/6.40 % SZS output start CNFRefutation for theBenchmark
% 7.21/6.40 fof(f1,axiom,(
% 7.21/6.40 (![A,B,C,D]: (inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = D ))),
% 7.21/6.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.21/6.40 fof(f2,negated_conjecture,(
% 7.21/6.40 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
% 7.21/6.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.21/6.40 fof(f3,plain,(
% 7.21/6.40 ![X0,X1,X2,X3]: (inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1)))))))=X3)),
% 7.21/6.40 inference(cnf_transformation,[status(thm)],[f1])).
% 7.21/6.40 fof(f4,plain,(
% 7.21/6.40 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)),
% 7.21/6.40 inference(cnf_transformation,[status(thm)],[f2])).
% 7.21/6.40 fof(f5,definition,(
% 7.21/6.40 sF1_fnc=inverse(a1)),
% 7.21/6.40 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 7.21/6.40 fof(f6,definition,(
% 7.21/6.40 sF0_fnc=multiply(sF1_fnc,a1)),
% 7.21/6.40 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 7.21/6.40 fof(f7,definition,(
% 7.21/6.40 sF3_fnc=inverse(b1)),
% 7.21/6.40 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 7.21/6.40 fof(f8,definition,(
% 7.21/6.40 sF2_fnc=multiply(sF3_fnc,b1)),
% 7.21/6.40 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 7.21/6.40 fof(f9,plain,(
% 7.21/6.40 ~sF0_fnc=sF2_fnc),
% 7.21/6.40 inference(definition_folding,[],[f4,f8,f7,f6,f5])).
% 7.21/6.40 fof(f11,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(X0,multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,multiply(X0,X1)))))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f7,f3])).
% 7.21/6.40 fof(f12,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,multiply(X0,X1)))))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f5,f3])).
% 7.21/6.40 fof(f15,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,sF0_fnc))))))=X1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f6,f3])).
% 7.21/6.40 fof(f16,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(b1,sF3_fnc),X1))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f11,f11])).
% 7.21/6.40 fof(f18,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f8,f11])).
% 7.21/6.40 fof(f22,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(b1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X0))))=sF3_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f18,f11])).
% 7.21/6.40 fof(f30,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(X0,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(a1,sF1_fnc),X1))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f12,f12])).
% 7.21/6.40 fof(f33,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f8,f12])).
% 7.21/6.40 fof(f34,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f6,f12])).
% 7.21/6.40 fof(f35,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(X0,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(b1,sF3_fnc),X1))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f12,f11])).
% 7.21/6.40 fof(f38,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(b1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))=sF3_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f33,f12])).
% 7.21/6.40 fof(f42,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0))))=sF1_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f34,f12])).
% 7.21/6.40 fof(f77,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(b1,sF3_fnc),sF3_fnc))))=b1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f22,f11])).
% 7.21/6.40 fof(f89,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))))=multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f16,f16])).
% 7.21/6.40 fof(f91,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(b1,sF3_fnc),X1))))=X2)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f11,f16])).
% 7.21/6.40 fof(f102,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))))=b1)),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f89,f77])).
% 7.21/6.40 fof(f104,plain,(
% 7.21/6.40 ![X0,X1,X2]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1))))=X2)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f89,f91])).
% 7.21/6.40 fof(f118,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))),multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,b1))),multiply(multiply(b1,sF3_fnc),X1))))=multiply(b1,sF3_fnc))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f102,f16])).
% 7.21/6.40 fof(f123,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(sF1_fnc,a1))))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f34,f104])).
% 7.21/6.40 fof(f125,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(sF1_fnc,a1))))=multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,sF0_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f15,f104])).
% 7.21/6.40 fof(f126,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(sF3_fnc,b1))))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f33,f104])).
% 7.21/6.40 fof(f130,plain,(
% 7.21/6.40 ![X0,X1,X2]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2))))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(X1,X2)))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f12,f104])).
% 7.21/6.40 fof(f136,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))))=b1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f8,f104])).
% 7.21/6.40 fof(f137,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,sF0_fnc)),multiply(X0,sF1_fnc))))=a1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f6,f104])).
% 7.21/6.40 fof(f141,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f8,f104])).
% 7.21/6.40 fof(f142,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc)))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f6,f104])).
% 7.21/6.40 fof(f158,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc)))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f6,f123])).
% 7.21/6.40 fof(f159,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc)))=multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,sF0_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f6,f125])).
% 7.21/6.40 fof(f168,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc)))=multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,sF0_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f158,f159])).
% 7.21/6.40 fof(f183,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc)))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f8,f126])).
% 7.21/6.40 fof(f194,plain,(
% 7.21/6.40 ![X0,X1,X2]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1))))=X2)),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f130,f104])).
% 7.21/6.40 fof(f224,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))))=b1)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f130,f136])).
% 7.21/6.40 fof(f225,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,sF0_fnc)),multiply(X0,sF1_fnc))))=a1)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f130,f137])).
% 7.21/6.40 fof(f226,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)))=X0)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f183,f141])).
% 7.21/6.40 fof(f227,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc)))=X0)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f158,f142])).
% 7.21/6.40 fof(f233,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(multiply(multiply(a1,sF1_fnc),X0),multiply(multiply(multiply(a1,sF1_fnc),X1),multiply(multiply(a1,sF1_fnc),X2))))=multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(X1,X2)))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f30,f30])).
% 7.21/6.40 fof(f258,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,b1))),multiply(multiply(b1,sF3_fnc),X1))))=multiply(a1,sF1_fnc))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f224,f35])).
% 7.21/6.40 fof(f283,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,X0))))))=X1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f227,f12])).
% 7.21/6.40 fof(f286,plain,(
% 7.21/6.40 ![X0,X1,X2]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(X1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,multiply(X0,X1))))))))=multiply(multiply(b1,sF3_fnc),X2))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f35,f194])).
% 7.21/6.40 fof(f289,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(a1,sF1_fnc)))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X1))),sF0_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f227,f194])).
% 7.21/6.40 fof(f290,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(a1,sF1_fnc)))))=inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X1))),sF2_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f226,f194])).
% 7.21/6.40 fof(f291,plain,(
% 7.21/6.40 ![X0,X1,X2,X3]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(a1,sF1_fnc)))))=inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,X3))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f194,f194])).
% 7.21/6.40 fof(f325,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,sF2_fnc)),multiply(X0,sF3_fnc))),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,b1))),multiply(multiply(b1,sF3_fnc),X1))))=multiply(b1,sF3_fnc))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f352,f118])).
% 7.21/6.40 fof(f352,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),X0)=multiply(multiply(b1,sF3_fnc),X0))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f12,f286])).
% 7.21/6.40 fof(f357,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc))=inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f289,f290])).
% 7.21/6.40 fof(f362,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc))=inverse(multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f289,f291])).
% 7.21/6.40 fof(f391,plain,(
% 7.21/6.40 multiply(a1,sF1_fnc)=multiply(b1,sF3_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f258,f325])).
% 7.21/6.40 fof(f408,plain,(
% 7.21/6.40 multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(b1,sF2_fnc)),multiply(a1,sF1_fnc))))=b1),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f391,f224])).
% 7.21/6.40 fof(f411,plain,(
% 7.21/6.40 inverse(multiply(sF1_fnc,multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF2_fnc))))))=a1),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f408,f30])).
% 7.21/6.40 fof(f453,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(X0,sF0_fnc)),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc)))))),multiply(multiply(a1,sF1_fnc),X1))))=multiply(X2,inverse(X2)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f168,f30])).
% 7.21/6.40 fof(f470,plain,(
% 7.21/6.40 ![X0]: (multiply(a1,sF1_fnc)=multiply(X0,inverse(X0)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f30,f453])).
% 7.21/6.40 fof(f479,plain,(
% 7.21/6.40 ![X0]: (multiply(a1,sF1_fnc)=multiply(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))))),X0))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f34,f470])).
% 7.21/6.40 fof(f488,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(X0),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(a1,sF1_fnc)))),multiply(multiply(a1,sF1_fnc),X1))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f470,f30])).
% 7.21/6.40 fof(f489,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(a1,sF1_fnc)))))))=X1)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f470,f12])).
% 7.21/6.40 fof(f609,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(X0,multiply(inverse(X0),b1)))=inverse(multiply(b1,sF2_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f408,f489])).
% 7.21/6.40 fof(f610,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(X0,multiply(inverse(X0),a1)))=inverse(multiply(a1,sF0_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f225,f489])).
% 7.21/6.40 fof(f611,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(a1,sF1_fnc)))),multiply(multiply(multiply(a1,sF1_fnc),X0),multiply(multiply(a1,sF1_fnc),X1))))=inverse(X1))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f489,f30])).
% 7.21/6.40 fof(f615,plain,(
% 7.21/6.40 ![X0,X1]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,multiply(a1,sF1_fnc))),multiply(X0,X1))))=inverse(X1))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f233,f611])).
% 7.21/6.40 fof(f631,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(X0),multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF2_fnc))))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f609,f12])).
% 7.21/6.40 fof(f652,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(X0),multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF0_fnc))))))=X0)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f610,f12])).
% 7.21/6.40 fof(f655,plain,(
% 7.21/6.40 ![X0]: (multiply(a1,sF1_fnc)=multiply(multiply(X0,multiply(inverse(X0),a1)),inverse(multiply(a1,sF0_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f610,f470])).
% 7.21/6.40 fof(f762,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(a1,sF0_fnc)),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,multiply(a1,sF1_fnc)))),multiply(multiply(a1,sF1_fnc),X0))))=multiply(X1,multiply(inverse(X1),a1)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f655,f30])).
% 7.21/6.40 fof(f773,plain,(
% 7.21/6.40 ![X0]: (multiply(a1,sF0_fnc)=multiply(X0,multiply(inverse(X0),a1)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f488,f762])).
% 7.21/6.40 fof(f835,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF2_fnc))))))=multiply(b1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f38,f631])).
% 7.21/6.40 fof(f837,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(sF1_fnc,multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF2_fnc))))))=multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f42,f631])).
% 7.21/6.40 fof(f859,plain,(
% 7.21/6.40 ![X0]: (b1=multiply(b1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f33,f835])).
% 7.21/6.40 fof(f870,plain,(
% 7.21/6.40 ![X0]: (a1=multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f411,f837])).
% 7.21/6.40 fof(f939,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(X0,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF0_fnc))))))=multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f34,f652])).
% 7.21/6.40 fof(f973,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X0,multiply(a1,sF1_fnc))),multiply(a1,sF1_fnc))))=inverse(inverse(X0)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f470,f615])).
% 7.21/6.40 fof(f1044,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),X0)))),sF0_fnc))=inverse(multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(multiply(a1,sF1_fnc),X1),multiply(multiply(a1,sF1_fnc),X2)))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f233,f362])).
% 7.21/6.40 fof(f1055,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),sF0_fnc))=inverse(multiply(inverse(multiply(X1,b1)),multiply(X1,b1))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f859,f362])).
% 7.21/6.40 fof(f1097,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),X0)))),sF0_fnc))=multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2)))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f233,f1044])).
% 7.21/6.40 fof(f1098,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),X0)))),sF0_fnc))=multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f362,f1097])).
% 7.21/6.40 fof(f1099,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),X0)))),sF0_fnc))=X0)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f227,f1098])).
% 7.21/6.40 fof(f1198,plain,(
% 7.21/6.40 ![X0]: (multiply(a1,sF1_fnc)=multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),X0)))),sF0_fnc),X0))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1099,f470])).
% 7.21/6.40 fof(f1239,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(sF1_fnc,a1)),sF0_fnc)))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f870,f227])).
% 7.21/6.40 fof(f1242,plain,(
% 7.21/6.40 ![X0,X1]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),sF0_fnc))=inverse(multiply(inverse(multiply(X1,a1)),multiply(X1,a1))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f870,f362])).
% 7.21/6.40 fof(f1257,plain,(
% 7.21/6.40 a1=multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1258,f870])).
% 7.21/6.40 fof(f1258,plain,(
% 7.21/6.40 ![X0]: (multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f6,f1239])).
% 7.21/6.40 fof(f1262,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,a1)),sF0_fnc))=inverse(multiply(inverse(multiply(X0,a1)),multiply(X0,a1))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f870,f1242])).
% 7.21/6.40 fof(f1263,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(sF0_fnc),sF0_fnc))=inverse(multiply(inverse(multiply(X0,a1)),multiply(X0,a1))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f6,f1262])).
% 7.21/6.40 fof(f1268,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(inverse(sF0_fnc),sF0_fnc))))),sF0_fnc))=inverse(multiply(inverse(a1),multiply(a1,multiply(a1,sF1_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1257,f362])).
% 7.21/6.40 fof(f1272,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(inverse(sF0_fnc),sF0_fnc))))),sF0_fnc))=inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f5,f1268])).
% 7.21/6.40 fof(f1274,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF0_fnc),sF0_fnc))=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF0_fnc))))),a1)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f479,f1263])).
% 7.21/6.40 fof(f1282,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF0_fnc),sF0_fnc))=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f479,f1274])).
% 7.21/6.40 fof(f1425,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),sF0_fnc))=inverse(multiply(inverse(multiply(sF3_fnc,b1)),sF2_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f859,f357])).
% 7.21/6.40 fof(f1436,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(sF2_fnc),sF2_fnc))=inverse(multiply(inverse(multiply(X0,b1)),multiply(X0,b1))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1437,f1055])).
% 7.21/6.40 fof(f1437,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(a1,sF1_fnc),X0))))),sF0_fnc))=inverse(multiply(inverse(sF2_fnc),sF2_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f8,f1425])).
% 7.21/6.40 fof(f1447,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF2_fnc),sF2_fnc))=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),b1)))),sF0_fnc),b1)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1198,f1436])).
% 7.21/6.40 fof(f1457,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF2_fnc),sF2_fnc))=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1198,f1447])).
% 7.21/6.40 fof(f1458,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(sF0_fnc),sF0_fnc))=inverse(multiply(inverse(multiply(X0,b1)),multiply(X0,b1))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1460,f1436])).
% 7.21/6.40 fof(f1460,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF2_fnc),sF2_fnc))=inverse(multiply(inverse(sF0_fnc),sF0_fnc))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1282,f1457])).
% 7.21/6.40 fof(f1593,plain,(
% 7.21/6.40 b1=multiply(b1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc))),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1460,f859])).
% 7.21/6.40 fof(f1595,plain,(
% 7.21/6.40 multiply(a1,sF0_fnc)=multiply(multiply(inverse(sF2_fnc),sF2_fnc),multiply(inverse(multiply(inverse(sF0_fnc),sF0_fnc)),a1))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1460,f773])).
% 7.21/6.40 fof(f1597,plain,(
% 7.21/6.40 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF2_fnc),sF2_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1460,f470])).
% 7.21/6.40 fof(f1698,plain,(
% 7.21/6.40 multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc))))=inverse(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))),sF0_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1198,f973])).
% 7.21/6.40 fof(f1711,plain,(
% 7.21/6.40 multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))=inverse(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),multiply(a1,sF1_fnc))))),sF0_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1282,f1698])).
% 7.21/6.40 fof(f1712,plain,(
% 7.21/6.40 a1=multiply(a1,inverse(multiply(a1,sF1_fnc)))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1716,f1257])).
% 7.21/6.40 fof(f1713,plain,(
% 7.21/6.40 b1=multiply(b1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1716,f1593])).
% 7.21/6.40 fof(f1715,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(a1,sF1_fnc))=multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(a1,sF1_fnc),X0)))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f1716,f1258])).
% 7.21/6.40 fof(f1716,plain,(
% 7.21/6.40 multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))=inverse(multiply(a1,sF1_fnc))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1099,f1711])).
% 7.21/6.40 fof(f1744,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))=inverse(multiply(inverse(multiply(sF3_fnc,b1)),sF2_fnc))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1713,f357])).
% 7.21/6.40 fof(f1748,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))=inverse(multiply(inverse(sF2_fnc),sF2_fnc))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f8,f1744])).
% 7.21/6.40 fof(f1749,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))=inverse(multiply(inverse(sF0_fnc),sF0_fnc))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1460,f1748])).
% 7.21/6.40 fof(f2016,plain,(
% 7.21/6.40 inverse(multiply(a1,sF1_fnc))=multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1716,f1715])).
% 7.21/6.40 fof(f2063,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))),sF0_fnc))=inverse(multiply(inverse(multiply(X0,inverse(multiply(a1,sF1_fnc)))),multiply(X0,inverse(multiply(a1,sF1_fnc))))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2016,f362])).
% 7.21/6.40 fof(f2066,plain,(
% 7.21/6.40 ![X0]: (inverse(sF0_fnc)=inverse(multiply(inverse(multiply(X0,inverse(multiply(a1,sF1_fnc)))),multiply(X0,inverse(multiply(a1,sF1_fnc))))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1099,f2063])).
% 7.21/6.40 fof(f2068,plain,(
% 7.21/6.40 inverse(sF0_fnc)=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))))),sF0_fnc),inverse(multiply(a1,sF1_fnc)))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f1198,f2066])).
% 7.21/6.40 fof(f2082,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF0_fnc),sF0_fnc))=inverse(sF0_fnc)),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2083,f1282])).
% 7.21/6.40 fof(f2083,plain,(
% 7.21/6.40 inverse(sF0_fnc)=inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(a1,sF1_fnc)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1198,f2068])).
% 7.21/6.40 fof(f2094,plain,(
% 7.21/6.40 multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))=inverse(multiply(a1,sF1_fnc))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1716])).
% 7.21/6.40 fof(f2097,plain,(
% 7.21/6.40 multiply(a1,sF0_fnc)=multiply(multiply(inverse(sF2_fnc),sF2_fnc),multiply(inverse(sF0_fnc),a1))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1595])).
% 7.21/6.40 fof(f2098,plain,(
% 7.21/6.40 ![X0]: (inverse(sF0_fnc)=inverse(multiply(inverse(multiply(X0,b1)),multiply(X0,b1))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1458])).
% 7.21/6.40 fof(f2099,plain,(
% 7.21/6.40 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF2_fnc),sF2_fnc),inverse(sF0_fnc))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1597])).
% 7.21/6.40 fof(f2114,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))=inverse(sF0_fnc)),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1749])).
% 7.21/6.40 fof(f2141,plain,(
% 7.21/6.40 inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(sF0_fnc)))),sF0_fnc))=inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc))))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2082,f1272])).
% 7.21/6.40 fof(f2224,plain,(
% 7.21/6.40 multiply(a1,sF1_fnc)=multiply(multiply(inverse(sF0_fnc),sF0_fnc),inverse(sF0_fnc))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2082,f470])).
% 7.21/6.40 fof(f2364,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(X0,b1)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc)))))=inverse(multiply(X0,b1)))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2098,f283])).
% 7.21/6.40 fof(f2366,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(X0,X1)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X2))),sF0_fnc))))))=inverse(multiply(X0,multiply(X1,X2))))),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f362,f283])).
% 7.21/6.40 fof(f2382,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(sF0_fnc)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=multiply(inverse(sF0_fnc),sF0_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2224,f283])).
% 7.21/6.40 fof(f2383,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(sF0_fnc),a1)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF0_fnc))))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2097,f283])).
% 7.21/6.40 fof(f2385,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(sF0_fnc)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(paramodulation,[status(thm)],[f2099,f283])).
% 7.21/6.40 fof(f2435,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(X0,b1)))),sF0_fnc)),inverse(multiply(a1,sF1_fnc)))))=inverse(multiply(X0,b1)))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2094,f2364])).
% 7.21/6.40 fof(f2448,plain,(
% 7.21/6.40 ![X0]: (inverse(multiply(X0,multiply(b1,inverse(multiply(a1,sF1_fnc)))))=inverse(multiply(X0,b1)))),
% 7.21/6.40 inference(backward_demodulation,[status(thm)],[f2451,f2435])).
% 7.21/6.40 fof(f2451,plain,(
% 7.21/6.40 ![X0,X1,X2]: (inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(X0,X1)))),sF0_fnc)),X2)))=inverse(multiply(X0,multiply(X1,X2))))),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f227,f2366])).
% 7.21/6.40 fof(f2483,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=multiply(inverse(sF0_fnc),sF0_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2141,f2382])).
% 7.21/6.40 fof(f2484,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(a1,sF1_fnc))))=multiply(inverse(sF0_fnc),sF0_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f470,f2483])).
% 7.21/6.40 fof(f2485,plain,(
% 7.21/6.40 inverse(multiply(inverse(sF0_fnc),multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF0_fnc))))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2451,f2383])).
% 7.21/6.40 fof(f2486,plain,(
% 7.21/6.40 multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f939,f2485])).
% 7.21/6.40 fof(f2487,plain,(
% 7.21/6.40 multiply(sF1_fnc,multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2082,f2486])).
% 7.21/6.40 fof(f2488,plain,(
% 7.21/6.40 multiply(sF1_fnc,multiply(a1,inverse(multiply(a1,sF1_fnc))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2094,f2487])).
% 7.21/6.40 fof(f2489,plain,(
% 7.21/6.40 multiply(sF1_fnc,a1)=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f1712,f2488])).
% 7.21/6.40 fof(f2502,plain,(
% 7.21/6.40 sF0_fnc=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f6,f2489])).
% 7.21/6.40 fof(f2509,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2141,f2385])).
% 7.21/6.40 fof(f2510,plain,(
% 7.21/6.40 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(a1,sF1_fnc))))=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f470,f2509])).
% 7.21/6.40 fof(f2511,plain,(
% 7.21/6.40 multiply(inverse(sF0_fnc),sF0_fnc)=multiply(inverse(sF2_fnc),sF2_fnc)),
% 7.21/6.40 inference(forward_demodulation,[status(thm)],[f2484,f2510])).
% 7.71/6.44 fof(f2514,plain,(
% 7.71/6.44 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(a1,sF1_fnc))))=sF0_fnc),
% 7.71/6.44 inference(backward_demodulation,[status(thm)],[f2519,f2484])).
% 7.71/6.44 fof(f2519,plain,(
% 7.71/6.44 multiply(inverse(sF0_fnc),sF0_fnc)=sF0_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2502,f2511])).
% 7.71/6.44 fof(f2659,plain,(
% 7.71/6.44 multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(b1),multiply(b1,multiply(a1,sF1_fnc)))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))),
% 7.71/6.44 inference(paramodulation,[status(thm)],[f1713,f289])).
% 7.71/6.44 fof(f2713,plain,(
% 7.71/6.44 multiply(multiply(a1,sF1_fnc),inverse(multiply(sF3_fnc,multiply(b1,multiply(a1,sF1_fnc)))))=inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(a1,sF1_fnc),inverse(sF2_fnc)))))),sF0_fnc))),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f7,f2659])).
% 7.71/6.44 fof(f2714,plain,(
% 7.71/6.44 multiply(multiply(a1,sF1_fnc),inverse(multiply(sF3_fnc,multiply(b1,multiply(a1,sF1_fnc)))))=inverse(sF0_fnc)),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2114,f2713])).
% 7.71/6.44 fof(f2991,plain,(
% 7.71/6.44 inverse(sF0_fnc)=inverse(multiply(inverse(multiply(b1,inverse(multiply(a1,sF1_fnc)))),b1))),
% 7.71/6.44 inference(paramodulation,[status(thm)],[f2066,f2448])).
% 7.71/6.44 fof(f3191,plain,(
% 7.71/6.44 multiply(a1,sF1_fnc)=multiply(multiply(inverse(multiply(b1,inverse(multiply(a1,sF1_fnc)))),b1),inverse(sF0_fnc))),
% 7.71/6.44 inference(paramodulation,[status(thm)],[f2991,f470])).
% 7.71/6.44 fof(f3644,plain,(
% 7.71/6.44 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,multiply(a1,sF1_fnc))))),sF0_fnc)),inverse(sF0_fnc))))=sF3_fnc),
% 7.71/6.44 inference(paramodulation,[status(thm)],[f2714,f283])).
% 7.71/6.44 fof(f3654,plain,(
% 7.71/6.44 inverse(multiply(b1,multiply(multiply(a1,sF1_fnc),inverse(sF0_fnc))))=sF3_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2451,f3644])).
% 7.71/6.44 fof(f3660,plain,(
% 7.71/6.44 multiply(a1,sF1_fnc)=multiply(multiply(sF3_fnc,b1),inverse(sF0_fnc))),
% 7.71/6.44 inference(backward_demodulation,[status(thm)],[f3664,f3191])).
% 7.71/6.44 fof(f3664,plain,(
% 7.71/6.44 inverse(multiply(b1,inverse(multiply(a1,sF1_fnc))))=sF3_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2094,f3654])).
% 7.71/6.44 fof(f3736,plain,(
% 7.71/6.44 multiply(a1,sF1_fnc)=multiply(sF2_fnc,inverse(sF0_fnc))),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f8,f3660])).
% 7.71/6.44 fof(f3802,plain,(
% 7.71/6.44 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(sF0_fnc)))),sF0_fnc)),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=sF2_fnc),
% 7.71/6.44 inference(paramodulation,[status(thm)],[f3736,f283])).
% 7.71/6.44 fof(f3806,plain,(
% 7.71/6.44 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc))))))=sF2_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2141,f3802])).
% 7.71/6.44 fof(f3807,plain,(
% 7.71/6.44 inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,sF1_fnc)))),multiply(a1,sF1_fnc))))=sF2_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f470,f3806])).
% 7.71/6.44 fof(f3808,plain,(
% 7.71/6.44 sF0_fnc=sF2_fnc),
% 7.71/6.44 inference(forward_demodulation,[status(thm)],[f2514,f3807])).
% 7.71/6.44 fof(f3809,plain,(
% 7.71/6.44 $false),
% 7.71/6.44 inference(forward_subsumption_resolution,[status(thm)],[f3808,f9])).
% 7.71/6.44 % SZS output end CNFRefutation for theBenchmark.p
% 7.71/6.45 % Elapsed time: 1.060212 seconds
% 7.71/6.45 % CPU time: 8.295098 seconds
% 7.71/6.45 % Total memory used: 210.090 MB
% 7.71/6.45 % Net memory used: 204.655 MB
%------------------------------------------------------------------------------