%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP431-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 : n016.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 0.24s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP431-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n016.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 20 20:17:22 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 0.24/0.62 % Refutation found
% 0.24/0.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/0.62 % SZS output start CNFRefutation for theBenchmark
% 0.24/0.62 fof(f1,axiom,(
% 0.24/0.62 (![A,B,C,D]: (multiply(A,inverse(multiply(B,multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,B))),A)))) = D ))),
% 0.24/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.62 fof(f2,negated_conjecture,(
% 0.24/0.62 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 0.24/0.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.24/0.62 fof(f3,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X0))))=X3)),
% 0.24/0.62 inference(cnf_transformation,[status(thm)],[f1])).
% 0.24/0.62 fof(f4,plain,(
% 0.24/0.62 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 0.24/0.62 inference(cnf_transformation,[status(thm)],[f2])).
% 0.24/0.62 fof(f5,definition,(
% 0.24/0.62 sF2_fnc=inverse(b2)),
% 0.24/0.62 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.24/0.62 fof(f6,definition,(
% 0.24/0.62 sF1_fnc=multiply(sF2_fnc,b2)),
% 0.24/0.62 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.24/0.62 fof(f7,definition,(
% 0.24/0.62 sF0_fnc=multiply(sF1_fnc,a2)),
% 0.24/0.62 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.24/0.62 fof(f8,plain,(
% 0.24/0.62 ~sF0_fnc=a2),
% 0.24/0.62 inference(definition_folding,[],[f4,f7,f6,f5])).
% 0.24/0.62 fof(f10,plain,(
% 0.24/0.62 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))),multiply(X2,X0))))=X3)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f3,f3])).
% 0.24/0.62 fof(f11,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),X0))))=X2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f5,f3])).
% 0.24/0.62 fof(f13,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(b2,multiply(multiply(multiply(X1,inverse(X1)),inverse(sF1_fnc)),X0))))=sF2_fnc)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f6,f3])).
% 0.24/0.62 fof(f15,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X0))),multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X3)))))),inverse(multiply(X3,X1)))=X2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f11,f11])).
% 0.24/0.62 fof(f17,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X2))),multiply(b2,sF2_fnc)),multiply(X1,X0))))=X2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f11,f11])).
% 0.24/0.62 fof(f19,plain,(
% 0.24/0.62 ![X0]: (multiply(X0,inverse(multiply(a2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),X0))))=sF1_fnc)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f7,f11])).
% 0.24/0.62 fof(f21,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),X3))),multiply(multiply(multiply(b2,sF2_fnc),inverse(X2)),X0))))=X3)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f11,f11])).
% 0.24/0.62 fof(f45,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(sF1_fnc)),multiply(X2,inverse(X2))),multiply(sF2_fnc,X0))))=b2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f13,f3])).
% 0.24/0.62 fof(f89,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(sF1_fnc)),multiply(X2,inverse(X2))),multiply(X3,X0))))=inverse(multiply(a2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),X3))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f19,f10])).
% 0.24/0.62 fof(f91,plain,(
% 0.24/0.62 ![X0,X1,X2,X3,X4,X5]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(X2)),multiply(X3,inverse(X3))),multiply(X4,X0))))=inverse(multiply(X5,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X5))),X4))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f11,f10])).
% 0.24/0.62 fof(f123,plain,(
% 0.24/0.62 inverse(multiply(a2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc)))=b2),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f89,f45])).
% 0.24/0.62 fof(f137,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),b2),multiply(X2,inverse(X2))),multiply(a2,X0))))=multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f123,f10])).
% 0.24/0.62 fof(f143,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(X1,multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),multiply(b2,sF2_fnc)),X0))))=multiply(X2,multiply(b2,sF2_fnc)))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f17,f17])).
% 0.24/0.62 fof(f155,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),multiply(b2,sF2_fnc)),multiply(X1,X0))))=inverse(multiply(a2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),X1))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f19,f17])).
% 0.24/0.62 fof(f156,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(X1)),multiply(b2,sF2_fnc)),multiply(X2,X0))))=inverse(multiply(X3,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X3))),X2))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f11,f17])).
% 0.24/0.62 fof(f171,plain,(
% 0.24/0.62 ![X0,X1,X2,X3,X4]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X3,X1))),multiply(b2,sF2_fnc)),X0))))=multiply(X3,multiply(X4,inverse(X4))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f17,f10])).
% 0.24/0.62 fof(f172,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0))))=multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X3))),multiply(b2,sF2_fnc)))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f17,f3])).
% 0.24/0.62 fof(f187,plain,(
% 0.24/0.62 ![X0]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(X0,inverse(X0)),b2),a2))),multiply(b2,sF2_fnc))=multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc))),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f172,f137])).
% 0.24/0.62 fof(f192,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),X2))),multiply(b2,sF2_fnc))=inverse(multiply(X3,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X3))),X2))))),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f172,f91])).
% 0.24/0.62 fof(f194,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X0))),multiply(b2,sF2_fnc))))),multiply(b2,sF2_fnc))=multiply(X1,multiply(X2,inverse(X2))))),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f172,f171])).
% 0.24/0.62 fof(f229,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,multiply(b2,sF2_fnc))=multiply(X0,multiply(X1,inverse(X1))))),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f11,f194])).
% 0.24/0.62 fof(f261,plain,(
% 0.24/0.62 multiply(inverse(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc))),inverse(multiply(a2,multiply(b2,sF2_fnc))))=sF1_fnc),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f229,f19])).
% 0.24/0.62 fof(f271,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,multiply(b2,sF2_fnc)))),multiply(b2,sF2_fnc)),multiply(X1,X0))))=multiply(X2,inverse(X2)))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f229,f17])).
% 0.24/0.62 fof(f288,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),inverse(X0)),X1))),multiply(b2,sF2_fnc))=inverse(multiply(X2,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X2))),X1))))),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f324,f192])).
% 0.24/0.62 fof(f293,plain,(
% 0.24/0.62 multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),b2),a2))),multiply(b2,sF2_fnc))=multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc)),
% 0.24/0.62 inference(backward_demodulation,[status(thm)],[f324,f187])).
% 0.24/0.62 fof(f324,plain,(
% 0.24/0.62 ![X0]: (multiply(b2,sF2_fnc)=multiply(X0,inverse(X0)))),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f17,f271])).
% 0.24/0.62 fof(f337,plain,(
% 0.24/0.62 ![X0]: (multiply(X0,inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),X0))))=b2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f11])).
% 0.24/0.62 fof(f342,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc)),multiply(X1,X0))))=inverse(X1))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f17])).
% 0.24/0.62 fof(f343,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc))),X0))))=X1)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f11])).
% 0.24/0.62 fof(f348,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(X1,X0))))=inverse(X1))),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f324,f342])).
% 0.24/0.62 fof(f349,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(b2,sF2_fnc),X0))))=X1)),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f324,f343])).
% 0.24/0.62 fof(f350,plain,(
% 0.24/0.62 multiply(inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)))),inverse(multiply(sF2_fnc,b2)))=b2),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f337,f337])).
% 0.24/0.62 fof(f355,plain,(
% 0.24/0.62 multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(sF2_fnc,multiply(b2,sF2_fnc))))=b2),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f337])).
% 0.24/0.62 fof(f363,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),X1))),multiply(multiply(multiply(b2,sF2_fnc),inverse(b2)),X0))))=X1)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f337,f11])).
% 0.24/0.62 fof(f364,plain,(
% 0.24/0.62 multiply(inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)))),inverse(sF1_fnc))=b2),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f6,f350])).
% 0.24/0.62 fof(f367,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),X1))),multiply(multiply(multiply(b2,sF2_fnc),sF2_fnc),X0))))=X1)),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f5,f363])).
% 0.24/0.62 fof(f374,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc),multiply(multiply(multiply(b2,sF2_fnc),b2),multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))))),inverse(multiply(X1,a2)))=X0)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f123,f15])).
% 0.24/0.62 fof(f462,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(b2,sF2_fnc),X1))),X2))),multiply(multiply(b2,sF2_fnc),X0))))=X2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f21])).
% 0.24/0.62 fof(f483,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(X0,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(b2,sF2_fnc),X0))),X1))=X1)),
% 0.24/0.62 inference(forward_demodulation,[status(thm)],[f349,f462])).
% 0.24/0.62 fof(f488,plain,(
% 0.24/0.62 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)))),inverse(multiply(inverse(X1),X0)))=X1)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f349,f349])).
% 0.24/0.62 fof(f494,plain,(
% 0.24/0.62 ![X0]: (multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(inverse(X0),multiply(b2,sF2_fnc))))=X0)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f324,f349])).
% 0.24/0.62 fof(f495,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(X1,X2))),multiply(multiply(multiply(b2,sF2_fnc),inverse(inverse(X1))),X0))))=X2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f349,f21])).
% 0.24/0.62 fof(f501,plain,(
% 0.24/0.62 ![X0]: (multiply(inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)))),inverse(multiply(sF2_fnc,X0)))=b2)),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f349,f337])).
% 0.24/0.62 fof(f504,plain,(
% 0.24/0.62 ![X0,X1,X2,X3]: (multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(multiply(multiply(b2,sF2_fnc),inverse(X3)),X0))))=inverse(multiply(inverse(X2),multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),inverse(multiply(X3,X1)))))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f349,f21])).
% 0.24/0.62 fof(f512,plain,(
% 0.24/0.62 ![X0,X1,X2]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(X1)),multiply(b2,sF2_fnc)),multiply(X2,X0))))=inverse(multiply(inverse(X1),multiply(multiply(b2,sF2_fnc),X2))))),
% 0.24/0.62 inference(paramodulation,[status(thm)],[f349,f17])).
% 0.24/0.62 fof(f526,plain,(
% 0.24/0.62 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc))))))))=X1)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f504,f495])).
% 0.24/0.63 fof(f545,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(multiply(b2,sF2_fnc),X0)))=inverse(multiply(a2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),X0))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f512,f155])).
% 0.24/0.63 fof(f549,plain,(
% 0.24/0.63 ![X0,X1,X2]: (inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),X1)))=inverse(multiply(X2,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X2))),X1))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f512,f156])).
% 0.24/0.63 fof(f569,plain,(
% 0.24/0.63 ![X0,X1]: (inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(b2,sF2_fnc),X0)))=X1)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f349,f526])).
% 0.24/0.63 fof(f608,plain,(
% 0.24/0.63 inverse(multiply(inverse(sF1_fnc),multiply(multiply(b2,sF2_fnc),sF2_fnc)))=b2),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f545,f123])).
% 0.24/0.63 fof(f658,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),inverse(X0)),X1))),multiply(b2,sF2_fnc))=inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),X1))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f549,f288])).
% 0.24/0.63 fof(f712,plain,(
% 0.24/0.63 ![X0,X1]: (inverse(multiply(X0,multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X0)))))=multiply(multiply(b2,sF2_fnc),X1))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f569,f569])).
% 0.24/0.63 fof(f717,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),X0)))=inverse(X0))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f324,f569])).
% 0.24/0.63 fof(f720,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(multiply(inverse(multiply(b2,sF2_fnc)),X0)),multiply(b2,sF2_fnc)))=X0)),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f324,f569])).
% 0.24/0.63 fof(f735,plain,(
% 0.24/0.63 inverse(multiply(inverse(b2),multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc)))))=inverse(multiply(sF2_fnc,multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f355,f569])).
% 0.24/0.63 fof(f736,plain,(
% 0.24/0.63 inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc)))))=inverse(multiply(sF2_fnc,multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f5,f735])).
% 0.24/0.63 fof(f738,plain,(
% 0.24/0.63 multiply(multiply(b2,sF2_fnc),b2)=inverse(multiply(sF2_fnc,multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f712,f736])).
% 0.24/0.63 fof(f739,plain,(
% 0.24/0.63 inverse(multiply(multiply(multiply(b2,sF2_fnc),b2),multiply(multiply(b2,sF2_fnc),sF2_fnc)))=multiply(b2,sF2_fnc)),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f738,f569])).
% 0.24/0.63 fof(f749,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(X0,multiply(b2,sF2_fnc))))=multiply(inverse(multiply(X1,X0)),multiply(multiply(b2,sF2_fnc),X1)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f569,f494])).
% 0.24/0.63 fof(f757,plain,(
% 0.24/0.63 inverse(multiply(inverse(multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc)))=inverse(inverse(multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f324,f717])).
% 0.24/0.63 fof(f760,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc)))))=multiply(multiply(b2,sF2_fnc),X0))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f717,f569])).
% 0.24/0.63 fof(f761,plain,(
% 0.24/0.63 ![X0]: (multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(inverse(X0),multiply(b2,sF2_fnc))))=multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),X0)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f717,f494])).
% 0.24/0.63 fof(f765,plain,(
% 0.24/0.63 ![X0]: (multiply(multiply(b2,sF2_fnc),multiply(inverse(multiply(b2,sF2_fnc)),X0))=X0)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f768,f720])).
% 0.24/0.63 fof(f767,plain,(
% 0.24/0.63 multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc))=inverse(inverse(multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f768,f757])).
% 0.24/0.63 fof(f768,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(X0),multiply(b2,sF2_fnc)))=multiply(multiply(b2,sF2_fnc),X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f324,f760])).
% 0.24/0.63 fof(f771,plain,(
% 0.24/0.63 ![X0]: (X0=multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),X0)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f494,f761])).
% 0.24/0.63 fof(f780,plain,(
% 0.24/0.63 ![X0]: (multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(b2,sF2_fnc))))),inverse(multiply(sF2_fnc,X0)))=b2)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f767,f501])).
% 0.24/0.63 fof(f784,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(X0),inverse(inverse(multiply(b2,sF2_fnc))))),inverse(multiply(inverse(X1),X0)))=X1)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f767,f488])).
% 0.24/0.63 fof(f787,plain,(
% 0.24/0.63 multiply(inverse(multiply(sF2_fnc,inverse(inverse(multiply(b2,sF2_fnc))))),inverse(sF1_fnc))=b2),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f767,f364])).
% 0.24/0.63 fof(f788,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(X1,X0))))=inverse(X1))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f767,f348])).
% 0.24/0.63 fof(f789,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc))))=multiply(inverse(multiply(b2,sF2_fnc)),X0))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f349,f771])).
% 0.24/0.63 fof(f790,plain,(
% 0.24/0.63 inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc))))=multiply(inverse(multiply(b2,sF2_fnc)),b2)),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f337,f771])).
% 0.24/0.63 fof(f795,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(inverse(X1),X0)))=X1)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f800,f784])).
% 0.24/0.63 fof(f796,plain,(
% 0.24/0.63 ![X0]: (multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(sF2_fnc,X0)))=b2)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f800,f780])).
% 0.24/0.63 fof(f800,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(inverse(X0),inverse(inverse(multiply(b2,sF2_fnc)))))=multiply(inverse(multiply(b2,sF2_fnc)),X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f767,f789])).
% 0.24/0.63 fof(f801,plain,(
% 0.24/0.63 multiply(multiply(inverse(multiply(b2,sF2_fnc)),b2),inverse(sF1_fnc))=b2),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f806,f787])).
% 0.24/0.63 fof(f806,plain,(
% 0.24/0.63 inverse(multiply(sF2_fnc,inverse(inverse(multiply(b2,sF2_fnc)))))=multiply(inverse(multiply(b2,sF2_fnc)),b2)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f767,f790])).
% 0.24/0.63 fof(f849,plain,(
% 0.24/0.63 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),multiply(multiply(b2,sF2_fnc),X2)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f569,f795])).
% 0.24/0.63 fof(f889,plain,(
% 0.24/0.63 ![X0]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),b2),X0))),multiply(b2,sF2_fnc))=inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(multiply(b2,sF2_fnc),sF2_fnc))),multiply(multiply(b2,sF2_fnc),X0))))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f608,f658])).
% 0.24/0.63 fof(f908,plain,(
% 0.24/0.63 inverse(multiply(b2,multiply(multiply(b2,sF2_fnc),a2)))=multiply(multiply(multiply(b2,sF2_fnc),inverse(sF0_fnc)),sF2_fnc)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f909,f293])).
% 0.24/0.63 fof(f909,plain,(
% 0.24/0.63 ![X0]: (multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),b2),X0))),multiply(b2,sF2_fnc))=inverse(multiply(b2,multiply(multiply(b2,sF2_fnc),X0))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f608,f889])).
% 0.24/0.63 fof(f922,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(b2,multiply(multiply(b2,sF2_fnc),a2))),multiply(multiply(multiply(b2,sF2_fnc),b2),multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))))),inverse(multiply(X1,a2)))=X0)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f908,f374])).
% 0.24/0.63 fof(f930,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc)),multiply(multiply(X1,multiply(b2,sF2_fnc)),X0))))=multiply(inverse(X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f349,f143])).
% 0.24/0.63 fof(f937,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X1)),multiply(b2,sF2_fnc)),X0))))=multiply(inverse(X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f768,f143])).
% 0.24/0.63 fof(f939,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(b2)),multiply(b2,sF2_fnc)),X0))))=multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f796,f143])).
% 0.24/0.63 fof(f961,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc)),multiply(multiply(X1,multiply(b2,sF2_fnc)),X0))))=multiply(inverse(X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f767,f930])).
% 0.24/0.63 fof(f969,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(multiply(multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X1)),multiply(b2,sF2_fnc)),X0))))=multiply(inverse(X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f767,f937])).
% 0.24/0.63 fof(f971,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X0)),multiply(b2,sF2_fnc)))=multiply(inverse(X0),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f788,f969])).
% 0.24/0.63 fof(f973,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),sF2_fnc),multiply(b2,sF2_fnc)),X0))))=multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f5,f939])).
% 0.24/0.63 fof(f1055,plain,(
% 0.24/0.63 multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc))))=inverse(b2)),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f768,f788])).
% 0.24/0.63 fof(f1065,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(X0,X1))),inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f788,f788])).
% 0.24/0.63 fof(f1068,plain,(
% 0.24/0.63 ![X0]: (multiply(inverse(X0),inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc))))=inverse(X0))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f324,f788])).
% 0.24/0.63 fof(f1083,plain,(
% 0.24/0.63 multiply(sF2_fnc,multiply(b2,sF2_fnc))=inverse(b2)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f324,f1055])).
% 0.24/0.63 fof(f1085,plain,(
% 0.24/0.63 multiply(multiply(b2,sF2_fnc),b2)=inverse(sF2_fnc)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1104,f738])).
% 0.24/0.63 fof(f1104,plain,(
% 0.24/0.63 multiply(sF2_fnc,multiply(b2,sF2_fnc))=sF2_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f5,f1083])).
% 0.24/0.63 fof(f1109,plain,(
% 0.24/0.63 ![X0]: (multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc))))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f768,f1068])).
% 0.24/0.63 fof(f1110,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(X0))=multiply(multiply(b2,sF2_fnc),X0))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1124,f768])).
% 0.24/0.63 fof(f1111,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(multiply(X1,multiply(b2,sF2_fnc)),X0))))=multiply(inverse(X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1124,f961])).
% 0.24/0.63 fof(f1115,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,X1)),multiply(multiply(multiply(multiply(b2,sF2_fnc),sF2_fnc),multiply(b2,sF2_fnc)),X0))))=multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1124,f973])).
% 0.24/0.63 fof(f1119,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X0)),multiply(b2,sF2_fnc)))=inverse(X0))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1124,f971])).
% 0.24/0.63 fof(f1124,plain,(
% 0.24/0.63 ![X0]: (multiply(inverse(X0),multiply(b2,sF2_fnc))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f324,f1109])).
% 0.24/0.63 fof(f1139,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(b2,multiply(multiply(b2,sF2_fnc),a2))),multiply(inverse(sF2_fnc),multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))))),inverse(multiply(X1,a2)))=X0)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1085,f922])).
% 0.24/0.63 fof(f1141,plain,(
% 0.24/0.63 inverse(multiply(inverse(sF2_fnc),multiply(multiply(b2,sF2_fnc),sF2_fnc)))=multiply(b2,sF2_fnc)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1085,f739])).
% 0.24/0.63 fof(f1171,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(multiply(inverse(multiply(b2,sF2_fnc)),X0)))=X0)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f765])).
% 0.24/0.63 fof(f1196,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),X1))),multiply(inverse(inverse(sF2_fnc)),X0))))=X1)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f367])).
% 0.24/0.63 fof(f1224,plain,(
% 0.24/0.63 multiply(inverse(inverse(inverse(inverse(sF0_fnc)))),inverse(multiply(a2,multiply(b2,sF2_fnc))))=sF1_fnc),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f261])).
% 0.24/0.63 fof(f1230,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,multiply(inverse(inverse(inverse(multiply(multiply(b2,sF2_fnc),X0)))),X1))=X1)),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f483])).
% 0.24/0.63 fof(f1260,plain,(
% 0.24/0.63 ![X0,X1,X2]: (multiply(multiply(inverse(multiply(b2,sF2_fnc)),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f849])).
% 0.24/0.63 fof(f1261,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(b2,sF2_fnc)),inverse(multiply(X0,multiply(b2,sF2_fnc))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1110,f749])).
% 0.24/0.63 fof(f1264,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(X0,multiply(b2,sF2_fnc)))=multiply(inverse(X0),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f788,f1111])).
% 0.24/0.63 fof(f1265,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(X0,multiply(b2,sF2_fnc)))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1124,f1264])).
% 0.24/0.63 fof(f1275,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,X1)),multiply(multiply(inverse(inverse(sF2_fnc)),multiply(b2,sF2_fnc)),X0))))=multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1115])).
% 0.24/0.63 fof(f1276,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(sF2_fnc,X1)),multiply(inverse(inverse(sF2_fnc)),X0))))=multiply(multiply(inverse(multiply(b2,sF2_fnc)),X1),multiply(b2,sF2_fnc)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1124,f1275])).
% 0.24/0.63 fof(f1281,plain,(
% 0.24/0.63 ![X0]: (inverse(multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X0)))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1265,f1119])).
% 0.24/0.63 fof(f1282,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(inverse(multiply(multiply(b2,sF2_fnc),X0))))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1281])).
% 0.24/0.63 fof(f1283,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(inverse(inverse(inverse(X0)))))=inverse(X0))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1282])).
% 0.24/0.63 fof(f1302,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(b2,inverse(inverse(a2)))),multiply(inverse(sF2_fnc),multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))))),inverse(multiply(X1,a2)))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1139])).
% 0.24/0.63 fof(f1303,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(b2,inverse(inverse(a2)))),multiply(inverse(sF2_fnc),inverse(inverse(inverse(multiply(X0,X1))))))),inverse(multiply(X1,a2)))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1302])).
% 0.24/0.63 fof(f1306,plain,(
% 0.24/0.63 inverse(multiply(inverse(sF2_fnc),inverse(inverse(sF2_fnc))))=multiply(b2,sF2_fnc)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1141])).
% 0.24/0.63 fof(f1311,plain,(
% 0.24/0.63 multiply(multiply(multiply(b2,sF2_fnc),b2),inverse(sF1_fnc))=b2),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1342,f801])).
% 0.24/0.63 fof(f1328,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(X0,X1))),inverse(multiply(inverse(multiply(b2,sF2_fnc)),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1342,f1065])).
% 0.24/0.63 fof(f1342,plain,(
% 0.24/0.63 inverse(multiply(b2,sF2_fnc))=multiply(b2,sF2_fnc)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f324,f1306])).
% 0.24/0.63 fof(f1389,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(multiply(multiply(b2,sF2_fnc),X0)))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1171])).
% 0.24/0.63 fof(f1394,plain,(
% 0.24/0.63 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1389])).
% 0.24/0.63 fof(f1441,plain,(
% 0.24/0.63 ![X0]: (multiply(multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),X0)),multiply(b2,sF2_fnc))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1276,f1196])).
% 0.24/0.63 fof(f1446,plain,(
% 0.24/0.63 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=X0)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f771,f1441])).
% 0.24/0.63 fof(f1525,plain,(
% 0.24/0.63 multiply(sF0_fnc,inverse(multiply(a2,multiply(b2,sF2_fnc))))=sF1_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1394,f1224])).
% 0.24/0.63 fof(f1526,plain,(
% 0.24/0.63 multiply(sF0_fnc,inverse(a2))=sF1_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1265,f1525])).
% 0.24/0.63 fof(f1537,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,multiply(inverse(inverse(inverse(inverse(inverse(X0))))),X1))=X1)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1230])).
% 0.24/0.63 fof(f1538,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1283,f1537])).
% 0.24/0.63 fof(f1640,plain,(
% 0.24/0.63 ![X0,X1,X2]: (multiply(multiply(multiply(b2,sF2_fnc),X0),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1260])).
% 0.24/0.63 fof(f1641,plain,(
% 0.24/0.63 ![X0,X1,X2]: (multiply(inverse(inverse(X0)),inverse(multiply(X1,X0)))=multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1640])).
% 0.24/0.63 fof(f1642,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,multiply(b2,sF2_fnc))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1261])).
% 0.24/0.63 fof(f1643,plain,(
% 0.24/0.63 ![X0,X1]: (inverse(inverse(inverse(multiply(X0,multiply(b2,sF2_fnc)))))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1642])).
% 0.24/0.63 fof(f1644,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(inverse(X0)),inverse(multiply(X1,X0)))=inverse(inverse(inverse(X1))))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1646,f1641])).
% 0.24/0.63 fof(f1646,plain,(
% 0.24/0.63 ![X0,X1]: (inverse(inverse(inverse(X0)))=multiply(inverse(multiply(X1,X0)),inverse(inverse(X1))))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1265,f1643])).
% 0.24/0.63 fof(f1658,plain,(
% 0.24/0.63 multiply(inverse(sF2_fnc),inverse(sF1_fnc))=b2),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1085,f1311])).
% 0.24/0.63 fof(f1733,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(b2,sF2_fnc)),multiply(X0,X1))),inverse(multiply(inverse(multiply(b2,sF2_fnc)),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1328])).
% 0.24/0.63 fof(f1734,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(multiply(b2,sF2_fnc),multiply(X0,X1))),inverse(multiply(inverse(multiply(b2,sF2_fnc)),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1733])).
% 0.24/0.63 fof(f1735,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(inverse(inverse(multiply(X0,X1)))),inverse(multiply(inverse(multiply(b2,sF2_fnc)),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1734])).
% 0.24/0.63 fof(f1736,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(inverse(inverse(multiply(X0,X1)))),inverse(multiply(multiply(b2,sF2_fnc),inverse(X0))))=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1342,f1735])).
% 0.24/0.63 fof(f1737,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(inverse(inverse(multiply(X0,X1)))),inverse(inverse(inverse(inverse(X0)))))=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1110,f1736])).
% 0.24/0.63 fof(f1738,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(inverse(inverse(multiply(X0,X1)))),X0)=inverse(X1))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1394,f1737])).
% 0.24/0.63 fof(f1829,plain,(
% 0.24/0.63 multiply(inverse(multiply(inverse(multiply(b2,inverse(inverse(a2)))),multiply(inverse(sF2_fnc),inverse(inverse(inverse(sF1_fnc)))))),inverse(multiply(inverse(a2),a2)))=sF0_fnc),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f1526,f1303])).
% 0.24/0.63 fof(f1831,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f1538,f1538])).
% 0.24/0.63 fof(f1833,plain,(
% 0.24/0.63 ![X0]: (multiply(X0,multiply(b2,sF2_fnc))=inverse(inverse(X0)))),
% 0.24/0.63 inference(paramodulation,[status(thm)],[f324,f1538])).
% 0.24/0.63 fof(f1848,plain,(
% 0.24/0.63 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),X0)=inverse(X1))),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1831,f1738])).
% 0.24/0.63 fof(f1874,plain,(
% 0.24/0.63 multiply(inverse(multiply(inverse(multiply(b2,a2)),multiply(inverse(sF2_fnc),inverse(inverse(inverse(sF1_fnc)))))),inverse(multiply(inverse(a2),a2)))=sF0_fnc),
% 0.24/0.63 inference(backward_demodulation,[status(thm)],[f1903,f1829])).
% 0.24/0.63 fof(f1903,plain,(
% 0.24/0.63 ![X0]: (X0=inverse(inverse(X0)))),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1446,f1833])).
% 0.24/0.63 fof(f1943,plain,(
% 0.24/0.63 multiply(inverse(multiply(inverse(multiply(b2,a2)),multiply(inverse(sF2_fnc),inverse(sF1_fnc)))),inverse(multiply(inverse(a2),a2)))=sF0_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1903,f1874])).
% 0.24/0.63 fof(f1944,plain,(
% 0.24/0.63 multiply(inverse(multiply(inverse(multiply(b2,a2)),b2)),inverse(multiply(inverse(a2),a2)))=sF0_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1658,f1943])).
% 0.24/0.63 fof(f1945,plain,(
% 0.24/0.63 multiply(inverse(inverse(a2)),inverse(multiply(inverse(a2),a2)))=sF0_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1848,f1944])).
% 0.24/0.63 fof(f1946,plain,(
% 0.24/0.63 inverse(inverse(inverse(inverse(a2))))=sF0_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1644,f1945])).
% 0.24/0.63 fof(f1947,plain,(
% 0.24/0.63 a2=sF0_fnc),
% 0.24/0.63 inference(forward_demodulation,[status(thm)],[f1394,f1946])).
% 0.24/0.63 fof(f1948,plain,(
% 0.24/0.63 $false),
% 0.24/0.63 inference(forward_subsumption_resolution,[status(thm)],[f1947,f8])).
% 0.24/0.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.67 % Elapsed time: 0.196713 seconds
% 0.24/0.67 % CPU time: 1.153587 seconds
% 0.24/0.67 % Total memory used: 42.382 MB
% 0.24/0.67 % Net memory used: 41.124 MB
%------------------------------------------------------------------------------