%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP404-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 : n013.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:35 PM UTC 2026
% Result : Unsatisfiable 130.76s 17.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP404-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n013.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 20 20:11:35 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 130.76/17.15 % Refutation found
% 130.76/17.15 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 130.76/17.15 % SZS output start CNFRefutation for theBenchmark
% 130.76/17.15 fof(f1,axiom,(
% 130.76/17.15 (![A,B,C]: (multiply(A,inverse(multiply(inverse(multiply(inverse(multiply(A,B)),C)),inverse(multiply(B,multiply(inverse(B),B)))))) = C ))),
% 130.76/17.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 130.76/17.15 fof(f2,negated_conjecture,(
% 130.76/17.15 multiply(multiply(inverse(b2),b2),a2) != a2 ),
% 130.76/17.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 130.76/17.15 fof(f3,plain,(
% 130.76/17.15 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1))))))=X2)),
% 130.76/17.15 inference(cnf_transformation,[status(thm)],[f1])).
% 130.76/17.15 fof(f4,plain,(
% 130.76/17.15 ~multiply(multiply(inverse(b2),b2),a2)=a2),
% 130.76/17.15 inference(cnf_transformation,[status(thm)],[f2])).
% 130.76/17.15 fof(f5,definition,(
% 130.76/17.15 sF2_fnc=inverse(b2)),
% 130.76/17.15 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 130.76/17.15 fof(f6,definition,(
% 130.76/17.15 sF1_fnc=multiply(sF2_fnc,b2)),
% 130.76/17.15 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 130.76/17.15 fof(f7,definition,(
% 130.76/17.15 sF0_fnc=multiply(sF1_fnc,a2)),
% 130.76/17.15 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 130.76/17.15 fof(f8,plain,(
% 130.76/17.15 ~sF0_fnc=a2),
% 130.76/17.15 inference(definition_folding,[],[f4,f7,f6,f5])).
% 130.76/17.15 fof(f11,plain,(
% 130.76/17.15 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(sF1_fnc),X0)),inverse(multiply(b2,multiply(inverse(b2),b2))))))=X0)),
% 130.76/17.15 inference(paramodulation,[status(thm)],[f6,f3])).
% 130.76/17.15 fof(f13,plain,(
% 130.76/17.15 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,multiply(sF2_fnc,b2))))))=X1)),
% 130.76/17.15 inference(paramodulation,[status(thm)],[f5,f3])).
% 130.76/17.15 fof(f14,plain,(
% 130.76/17.15 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(sF1_fnc),X0)),inverse(multiply(b2,multiply(sF2_fnc,b2))))))=X0)),
% 130.76/17.15 inference(forward_demodulation,[status(thm)],[f5,f11])).
% 130.76/17.15 fof(f15,plain,(
% 130.76/17.15 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(sF1_fnc),X0)),inverse(multiply(b2,sF1_fnc)))))=X0)),
% 130.76/17.15 inference(forward_demodulation,[status(thm)],[f6,f14])).
% 130.76/17.15 fof(f16,plain,(
% 130.76/17.15 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))))=X1)),
% 130.76/17.15 inference(forward_demodulation,[status(thm)],[f6,f13])).
% 130.76/17.15 fof(f25,plain,(
% 130.76/17.15 ![X0]: (multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,sF1_fnc)))))=inverse(multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),b2)),X0)),inverse(multiply(b2,sF1_fnc)))))),
% 130.76/17.15 inference(paramodulation,[status(thm)],[f16,f15])).
% 130.76/17.15 fof(f26,plain,(
% 130.76/17.15 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))=inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),X1)),inverse(multiply(b2,sF1_fnc)))))),
% 130.76/17.15 inference(paramodulation,[status(thm)],[f16,f3])).
% 130.76/17.15 fof(f27,plain,(
% 130.76/17.15 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))),multiply(inverse(inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc))))),inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc))))))))))=X2)),
% 130.76/17.15 inference(paramodulation,[status(thm)],[f16,f3])).
% 130.76/17.15 fof(f34,plain,(
% 130.76/17.15 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))))),b2)),multiply(inverse(X1),X2))),inverse(multiply(b2,sF1_fnc))))=X2)),
% 130.76/17.15 inference(forward_demodulation,[status(thm)],[f26,f27])).
% 130.76/17.15 fof(f35,plain,(
% 130.76/17.15 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),b2)),multiply(inverse(X0),X1))),inverse(multiply(b2,sF1_fnc))))=X1)),
% 130.76/17.15 inference(forward_demodulation,[status(thm)],[f16,f34])).
% 130.76/17.15 fof(f40,plain,(
% 130.76/17.15 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),b2)),multiply(inverse(X1),X0))),inverse(multiply(b2,sF1_fnc)))),X2))),inverse(multiply(b2,sF1_fnc))))=X2)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f35,f35])).
% 130.76/17.16 fof(f41,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(multiply(inverse(multiply(sF2_fnc,b2)),multiply(inverse(b2),X0))),inverse(multiply(b2,sF1_fnc))))=X0)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5,f35])).
% 130.76/17.16 fof(f51,plain,(
% 130.76/17.16 ![X0,X1]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),multiply(X0,X1))),inverse(multiply(b2,sF1_fnc))))=X1)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f35,f40])).
% 130.76/17.16 fof(f52,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(b2),X0))),inverse(multiply(b2,sF1_fnc))))=X0)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6,f41])).
% 130.76/17.16 fof(f53,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),inverse(multiply(b2,sF1_fnc))))=X0)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f5,f52])).
% 130.76/17.16 fof(f62,plain,(
% 130.76/17.16 inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),inverse(multiply(b2,sF1_fnc))))=b2),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f6,f53])).
% 130.76/17.16 fof(f72,plain,(
% 130.76/17.16 multiply(inverse(sF1_fnc),inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))))=inverse(multiply(b2,sF1_fnc))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f62,f3])).
% 130.76/17.16 fof(f83,plain,(
% 130.76/17.16 ![X0,X1,X2]: (inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc))))=inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),X1)),inverse(multiply(X2,multiply(inverse(X2),X2))))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f3,f51])).
% 130.76/17.16 fof(f85,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,b2)),inverse(multiply(X1,inverse(multiply(multiply(X0,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))=inverse(multiply(b2,sF1_fnc)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f51,f3])).
% 130.76/17.16 fof(f98,plain,(
% 130.76/17.16 multiply(sF2_fnc,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc)))))=inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f72,f15])).
% 130.76/17.16 fof(f146,plain,(
% 130.76/17.16 multiply(inverse(multiply(sF1_fnc,b2)),inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(multiply(sF1_fnc,a2)),multiply(sF1_fnc,a2)))))))=inverse(multiply(b2,sF1_fnc))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f7,f85])).
% 130.76/17.16 fof(f175,plain,(
% 130.76/17.16 multiply(inverse(multiply(sF1_fnc,b2)),inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(sF0_fnc),multiply(sF1_fnc,a2)))))))=inverse(multiply(b2,sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7,f146])).
% 130.76/17.16 fof(f176,plain,(
% 130.76/17.16 multiply(inverse(multiply(sF1_fnc,b2)),inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(sF0_fnc),sF0_fnc))))))=inverse(multiply(b2,sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7,f175])).
% 130.76/17.16 fof(f228,plain,(
% 130.76/17.16 multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc)))))=inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(sF0_fnc),sF0_fnc)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f176,f16])).
% 130.76/17.16 fof(f244,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,sF1_fnc))))))=X0)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f25,f16])).
% 130.76/17.16 fof(f333,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),X1))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f26,f244])).
% 130.76/17.16 fof(f337,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))=multiply(inverse(multiply(X1,b2)),multiply(X1,X0)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f51,f244])).
% 130.76/17.16 fof(f344,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(multiply(inverse(multiply(X1,b2)),multiply(X1,X0))),inverse(multiply(b2,sF1_fnc))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f51,f244])).
% 130.76/17.16 fof(f347,plain,(
% 130.76/17.16 multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(sF2_fnc,inverse(multiply(b2,sF1_fnc))))))=b2),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5,f244])).
% 130.76/17.16 fof(f357,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),inverse(multiply(b2,sF1_fnc))))=X0)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f337,f51])).
% 130.76/17.16 fof(f369,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),inverse(multiply(b2,sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f337,f344])).
% 130.76/17.16 fof(f377,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc)))))))=X0)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f369,f357])).
% 130.76/17.16 fof(f394,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,X1))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f337,f337])).
% 130.76/17.16 fof(f549,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(b2,sF1_fnc)))))))=multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),X1))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f244,f394])).
% 130.76/17.16 fof(f627,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(b2,sF1_fnc))))))))=multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(multiply(inverse(multiply(X1,b2)),b2)),X2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f549,f394])).
% 130.76/17.16 fof(f654,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(sF2_fnc,inverse(multiply(X1,multiply(inverse(X1),X1))))))))=multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),b2))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5,f333])).
% 130.76/17.16 fof(f1230,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),inverse(multiply(b2,sF1_fnc)))),inverse(multiply(b2,sF1_fnc)))))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f83,f16])).
% 130.76/17.16 fof(f1233,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X1,b2)),X2)),inverse(multiply(b2,sF1_fnc)))))))=multiply(inverse(multiply(inverse(multiply(X0,X3)),b2)),multiply(inverse(multiply(X1,X3)),X2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f83,f333])).
% 130.76/17.16 fof(f1246,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))),inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(multiply(inverse(multiply(X0,X2)),X1)),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f83,f244])).
% 130.76/17.16 fof(f1383,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,multiply(inverse(b2),b2)))))))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f26,f1230])).
% 130.76/17.16 fof(f1384,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,multiply(sF2_fnc,b2)))))))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f5,f1383])).
% 130.76/17.16 fof(f1385,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc))))))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6,f1384])).
% 130.76/17.16 fof(f1386,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(multiply(X1,b2)),X2))=multiply(inverse(multiply(inverse(multiply(X0,X3)),b2)),multiply(inverse(multiply(X1,X3)),X2)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f549,f1233])).
% 130.76/17.16 fof(f1401,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(X0,X2)),X1)),inverse(multiply(X2,multiply(inverse(X2),X2)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f244,f1246])).
% 130.76/17.16 fof(f1442,plain,(
% 130.76/17.16 multiply(inverse(sF0_fnc),multiply(sF1_fnc,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc))))))=inverse(multiply(a2,multiply(inverse(a2),a2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f7,f1385])).
% 130.76/17.16 fof(f1449,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(sF2_fnc,X0)),inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))))=inverse(multiply(X0,multiply(inverse(X0),X0))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f98,f1385])).
% 130.76/17.16 fof(f1517,plain,(
% 130.76/17.16 multiply(inverse(sF0_fnc),inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(sF0_fnc),sF0_fnc))))))=inverse(multiply(a2,multiply(inverse(a2),a2)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f228,f1442])).
% 130.76/17.16 fof(f2075,plain,(
% 130.76/17.16 multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),b2)),inverse(multiply(b2,sF1_fnc)))),inverse(multiply(b2,sF1_fnc)))=multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f62,f1401])).
% 130.76/17.16 fof(f2079,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(inverse(multiply(sF2_fnc,b2)),inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f1449,f1401])).
% 130.76/17.16 fof(f2080,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),b2)),inverse(multiply(b2,sF1_fnc)))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))),inverse(multiply(multiply(sF2_fnc,X0),multiply(inverse(multiply(sF2_fnc,X0)),multiply(sF2_fnc,X0))))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f369,f1401])).
% 130.76/17.16 fof(f2185,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(inverse(multiply(b2,multiply(inverse(b2),b2)))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f1449,f2079])).
% 130.76/17.16 fof(f2186,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(inverse(multiply(b2,multiply(sF2_fnc,b2)))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f5,f2185])).
% 130.76/17.16 fof(f2188,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(inverse(multiply(X0,multiply(inverse(X0),X0)))),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6,f2186])).
% 130.76/17.16 fof(f2189,plain,(
% 130.76/17.16 ![X0]: (multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))=multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))),inverse(multiply(multiply(sF2_fnc,X0),multiply(inverse(multiply(sF2_fnc,X0)),multiply(sF2_fnc,X0))))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f2075,f2080])).
% 130.76/17.16 fof(f2190,plain,(
% 130.76/17.16 ![X0]: (multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))=multiply(X0,inverse(multiply(multiply(sF2_fnc,X0),multiply(inverse(multiply(sF2_fnc,X0)),multiply(sF2_fnc,X0))))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f377,f2189])).
% 130.76/17.16 fof(f2387,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))))))=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X1))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2190,f333])).
% 130.76/17.16 fof(f2389,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,inverse(multiply(b2,inverse(multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))))))))=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2190,f654])).
% 130.76/17.16 fof(f2464,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2)=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X1))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f2389,f2387])).
% 130.76/17.16 fof(f3190,plain,(
% 130.76/17.16 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(multiply(inverse(multiply(X1,b2)),b2)),multiply(inverse(multiply(X2,b2)),X3)))=multiply(inverse(multiply(inverse(multiply(X0,X4)),b2)),multiply(inverse(multiply(inverse(multiply(X1,X5)),X4)),multiply(inverse(multiply(X2,X5)),X3))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f1386,f1386])).
% 130.76/17.16 fof(f3194,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),multiply(inverse(multiply(X3,X2)),multiply(X3,X1))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f337,f1386])).
% 130.76/17.16 fof(f3282,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,multiply(sF2_fnc,inverse(X2)))),b2)),b2)),X3))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,multiply(sF2_fnc,sF2_fnc))),b2)),b2)),X3)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2464,f1386])).
% 130.76/17.16 fof(f3374,plain,(
% 130.76/17.16 ![X0,X1,X2,X3,X4,X5]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,b2)),X3)),inverse(multiply(b2,sF1_fnc))))))))=multiply(inverse(multiply(inverse(multiply(X0,X4)),b2)),multiply(inverse(multiply(inverse(multiply(X1,X5)),X4)),multiply(inverse(multiply(X2,X5)),X3))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f627,f3190])).
% 130.76/17.16 fof(f3380,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),multiply(inverse(multiply(X3,X2)),multiply(X3,X1))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f394,f3194])).
% 130.76/17.16 fof(f3423,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(inverse(multiply(X1,multiply(sF2_fnc,inverse(X2)))),inverse(multiply(inverse(X3),inverse(multiply(b2,sF1_fnc))))))))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,multiply(sF2_fnc,sF2_fnc))),b2)),b2)),X3)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f627,f3282])).
% 130.76/17.16 fof(f4546,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,multiply(sF2_fnc,inverse(X1)))),b2)),X2)),multiply(inverse(multiply(inverse(multiply(X3,multiply(sF2_fnc,sF2_fnc))),b2)),b2))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2464,f3380])).
% 130.76/17.16 fof(f4583,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X2)))),inverse(multiply(b2,sF1_fnc)))))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f3380,f16])).
% 130.76/17.16 fof(f4707,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(inverse(multiply(X2,multiply(sF2_fnc,inverse(X1)))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(sF2_fnc,sF2_fnc))),b2)),b2)),inverse(multiply(b2,sF1_fnc)))))))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f3374,f4546])).
% 130.76/17.16 fof(f4708,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(sF2_fnc,sF2_fnc))),b2)),b2)),multiply(inverse(multiply(inverse(multiply(X2,multiply(sF2_fnc,sF2_fnc))),b2)),b2))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f3423,f4707])).
% 130.76/17.16 fof(f4709,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,b2))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f337,f4708])).
% 130.76/17.16 fof(f4712,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))=multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),multiply(inverse(sF1_fnc),sF1_fnc)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6,f4709])).
% 130.76/17.16 fof(f4761,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(multiply(X0,X2),inverse(multiply(b2,sF1_fnc))))))))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f369,f4583])).
% 130.76/17.16 fof(f4762,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X2))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f377,f4761])).
% 130.76/17.16 fof(f4806,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2)),multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X2))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2464,f4762])).
% 130.76/17.16 fof(f4815,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),multiply(inverse(multiply(X1,b2)),X2))=multiply(inverse(multiply(X3,multiply(X1,X0))),multiply(X3,X2)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f337,f4762])).
% 130.76/17.16 fof(f4829,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF0_fnc),multiply(sF1_fnc,X0))=multiply(inverse(multiply(X1,a2)),multiply(X1,X0)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f7,f4762])).
% 130.76/17.16 fof(f4847,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X2)),multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2))=multiply(inverse(multiply(X3,X2)),multiply(X3,X1)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2464,f4762])).
% 130.76/17.16 fof(f4856,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,X2)))=multiply(inverse(multiply(X3,X1)),multiply(X3,multiply(X0,X2))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f337,f4762])).
% 130.76/17.16 fof(f4858,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1))))=multiply(inverse(multiply(X3,X2)),multiply(X3,multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc))))))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f1385,f4762])).
% 130.76/17.16 fof(f5113,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc))))))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f1401,f4858])).
% 130.76/17.16 fof(f5683,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(sF2_fnc,inverse(multiply(inverse(sF1_fnc),sF1_fnc))))))=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f2464,f4712])).
% 130.76/17.16 fof(f5746,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,X1)))),inverse(multiply(b2,sF1_fnc)))))=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f4712,f16])).
% 130.76/17.16 fof(f5840,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(multiply(X0,X1),inverse(multiply(b2,sF1_fnc))))))))=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f369,f5746])).
% 130.76/17.16 fof(f5900,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X1))=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f377,f5840])).
% 130.76/17.16 fof(f6021,plain,(
% 130.76/17.16 multiply(inverse(sF0_fnc),multiply(sF1_fnc,a2))=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f4829,f5900])).
% 130.76/17.16 fof(f6030,plain,(
% 130.76/17.16 ![X0]: (multiply(X0,multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc)))))))=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f377,f5900])).
% 130.76/17.16 fof(f6043,plain,(
% 130.76/17.16 multiply(inverse(inverse(multiply(a2,multiply(inverse(a2),a2)))),multiply(inverse(sF0_fnc),inverse(multiply(a2,inverse(multiply(sF0_fnc,multiply(inverse(sF0_fnc),sF0_fnc)))))))=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f1517,f5900])).
% 130.76/17.16 fof(f6114,plain,(
% 130.76/17.16 multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(sF2_fnc,inverse(multiply(b2,sF1_fnc))))))),b2)=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f347,f5900])).
% 130.76/17.16 fof(f6115,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(inverse(X0),inverse(multiply(b2,sF1_fnc))))))),X0)=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f244,f5900])).
% 130.76/17.16 fof(f6143,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),multiply(X0,X1))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),inverse(multiply(X1,multiply(inverse(X1),X1)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5900,f1401])).
% 130.76/17.16 fof(f6162,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X2,X3)))=multiply(inverse(multiply(inverse(multiply(X2,X3)),X1)),multiply(inverse(sF1_fnc),sF1_fnc)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5900,f4762])).
% 130.76/17.16 fof(f6163,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X3))=multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),multiply(inverse(multiply(X1,X2)),X3)))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5900,f4762])).
% 130.76/17.16 fof(f6171,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),X2)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),X2)),inverse(multiply(multiply(X0,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f5900,f1401])).
% 130.76/17.16 fof(f6297,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(sF2_fnc,inverse(multiply(inverse(sF0_fnc),sF0_fnc))))))=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f6418,f5683])).
% 130.76/17.16 fof(f6418,plain,(
% 130.76/17.16 multiply(inverse(sF0_fnc),sF0_fnc)=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7,f6021])).
% 130.76/17.16 fof(f6432,plain,(
% 130.76/17.16 ![X0]: (multiply(X0,multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc)))))))=multiply(inverse(sF0_fnc),sF0_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6418,f6030])).
% 130.76/17.16 fof(f6462,plain,(
% 130.76/17.16 multiply(inverse(inverse(multiply(a2,multiply(inverse(a2),a2)))),inverse(multiply(a2,multiply(inverse(a2),a2))))=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f1517,f6043])).
% 130.76/17.16 fof(f6463,plain,(
% 130.76/17.16 multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f2188,f6462])).
% 130.76/17.16 fof(f6467,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(sF0_fnc),sF0_fnc))))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f6556,f1385])).
% 130.76/17.16 fof(f6473,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X0,inverse(multiply(inverse(sF0_fnc),sF0_fnc))))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f6556,f5113])).
% 130.76/17.16 fof(f6556,plain,(
% 130.76/17.16 multiply(inverse(inverse(multiply(b2,sF1_fnc))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(sF0_fnc),sF0_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6418,f6463])).
% 130.76/17.16 fof(f6700,plain,(
% 130.76/17.16 multiply(sF2_fnc,b2)=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f377,f6114])).
% 130.76/17.16 fof(f6702,plain,(
% 130.76/17.16 sF1_fnc=multiply(inverse(sF1_fnc),sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6,f6700])).
% 130.76/17.16 fof(f6703,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(X0),X0)=multiply(inverse(sF1_fnc),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f377,f6115])).
% 130.76/17.16 fof(f6715,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,sF1_fnc)))))=inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X2)),b2)),X1)),inverse(multiply(b2,sF1_fnc)))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7037,f26])).
% 130.76/17.16 fof(f6725,plain,(
% 130.76/17.16 ![X0]: (multiply(X0,multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc)))))))=sF1_fnc)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7037,f6432])).
% 130.76/17.16 fof(f7037,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(X0),X0)=sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f6703])).
% 130.76/17.16 fof(f7096,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f337,f6143])).
% 130.76/17.16 fof(f7097,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f369,f7096])).
% 130.76/17.16 fof(f7098,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(sF1_fnc),inverse(multiply(X0,multiply(inverse(X0),X0)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f7097])).
% 130.76/17.16 fof(f7100,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))=X0)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7109,f244])).
% 130.76/17.16 fof(f7102,plain,(
% 130.76/17.16 ![X0]: (inverse(multiply(inverse(sF1_fnc),inverse(multiply(X0,sF1_fnc))))=X0)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7109,f377])).
% 130.76/17.16 fof(f7109,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,inverse(multiply(X0,inverse(multiply(b2,sF1_fnc))))))=multiply(inverse(sF1_fnc),inverse(multiply(X0,sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f7098])).
% 130.76/17.16 fof(f7164,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,X2)))=multiply(inverse(multiply(inverse(multiply(X0,X2)),X1)),sF1_fnc))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7165,f4856])).
% 130.76/17.16 fof(f7165,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X2,X3)))=multiply(inverse(multiply(inverse(multiply(X2,X3)),X1)),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f6162])).
% 130.76/17.16 fof(f7182,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),multiply(inverse(multiply(X1,b2)),X2))=multiply(inverse(sF1_fnc),multiply(inverse(multiply(X1,X0)),X2)))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7183,f4815])).
% 130.76/17.16 fof(f7183,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X3))=multiply(inverse(sF1_fnc),multiply(inverse(multiply(X1,X2)),X3)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f6163])).
% 130.76/17.16 fof(f7192,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),X2)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),X2)),inverse(multiply(multiply(X0,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f6171])).
% 130.76/17.16 fof(f7193,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),X2)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),X2)),inverse(multiply(multiply(X0,X1),multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f5900,f7192])).
% 130.76/17.16 fof(f7207,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),b2)),X2)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(sF1_fnc),X2)),inverse(multiply(multiply(X0,X1),sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f6702,f7193])).
% 130.76/17.16 fof(f7631,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X2)),multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))))=multiply(inverse(multiply(X3,X2)),multiply(X3,X1)))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7649,f4847])).
% 130.76/17.16 fof(f7632,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc)))))),multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),b2)),X2))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f7649,f4806])).
% 130.76/17.16 fof(f7649,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc)))))=multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,sF2_fnc))),b2)),b2))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f6297])).
% 130.76/17.16 fof(f8021,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(sF1_fnc)))=inverse(multiply(X1,multiply(inverse(X1),X1))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f6467])).
% 130.76/17.16 fof(f8022,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(sF1_fnc)))=inverse(multiply(X1,sF1_fnc)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f8021])).
% 130.76/17.16 fof(f8038,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(sF0_fnc),sF0_fnc)))),X1)),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7165,f6473])).
% 130.76/17.16 fof(f8040,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),X1)),sF1_fnc)))=X1)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f8069,f16])).
% 130.76/17.16 fof(f8054,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),inverse(sF1_fnc))),X2)),sF1_fnc)=multiply(inverse(multiply(inverse(sF1_fnc),X2)),inverse(multiply(multiply(X0,X1),sF1_fnc))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f8069,f7207])).
% 130.76/17.16 fof(f8069,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(multiply(inverse(multiply(X0,b2)),X1)),inverse(multiply(b2,sF1_fnc)))=multiply(inverse(multiply(inverse(multiply(X0,inverse(sF1_fnc))),X1)),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f8038])).
% 130.76/17.16 fof(f8575,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,sF1_fnc)))))=inverse(multiply(inverse(multiply(inverse(sF1_fnc),X1)),inverse(multiply(multiply(X0,X2),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7207,f6715])).
% 130.76/17.16 fof(f8610,plain,(
% 130.76/17.16 ![X0]: (multiply(X0,multiply(inverse(sF1_fnc),inverse(multiply(X0,sF1_fnc))))=sF1_fnc)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7109,f6725])).
% 130.76/17.16 fof(f9870,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))),X2)),sF1_fnc)=multiply(inverse(multiply(X3,X2)),multiply(X3,X1)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7164,f7631])).
% 130.76/17.16 fof(f9871,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(X0))),multiply(sF2_fnc,inverse(sF1_fnc))))),X1)),sF1_fnc)=multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7183,f9870])).
% 130.76/17.16 fof(f9872,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),X1)),sF1_fnc)=multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f8022,f9871])).
% 130.76/17.16 fof(f9877,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(X0,X1)),multiply(X0,X2))=multiply(inverse(multiply(inverse(X2),X1)),sF1_fnc))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f9910,f4762])).
% 130.76/17.16 fof(f9891,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(multiply(inverse(inverse(sF1_fnc)),X0)),sF1_fnc)=inverse(multiply(X0,sF1_fnc)))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f9910,f8022])).
% 130.76/17.16 fof(f9910,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(multiply(inverse(X0),X1)),sF1_fnc)=multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7102,f9872])).
% 130.76/17.16 fof(f9911,plain,(
% 130.76/17.16 ![X0,X1,X2,X3]: (multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(multiply(X0,multiply(sF2_fnc,inverse(X1)))),multiply(X0,multiply(sF2_fnc,inverse(sF1_fnc))))),X2))=multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7182,f7632])).
% 130.76/17.16 fof(f9912,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(multiply(sF2_fnc,inverse(X0))),multiply(sF2_fnc,inverse(sF1_fnc))))),X1))=multiply(inverse(multiply(X2,X0)),multiply(X2,X1)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7183,f9911])).
% 130.76/17.16 fof(f9913,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(X0),sF1_fnc)))),X1))=multiply(inverse(multiply(X2,X0)),multiply(X2,X1)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f8022,f9912])).
% 130.76/17.16 fof(f9915,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))=multiply(inverse(multiply(X2,X0)),multiply(X2,X1)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7102,f9913])).
% 130.76/17.16 fof(f10064,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),inverse(sF1_fnc))))=multiply(inverse(multiply(inverse(sF1_fnc),X0)),inverse(multiply(multiply(X1,X2),sF1_fnc))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10089,f8054])).
% 130.76/17.16 fof(f10078,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),multiply(X0,inverse(sF1_fnc))))))=X1)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10089,f8040])).
% 130.76/17.16 fof(f10089,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))=multiply(inverse(multiply(inverse(X1),X0)),sF1_fnc))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f9915,f9877])).
% 130.76/17.16 fof(f10115,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(sF1_fnc)))=inverse(multiply(X0,sF1_fnc)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10089,f9891])).
% 130.76/17.16 fof(f10264,plain,(
% 130.76/17.16 multiply(inverse(sF1_fnc),multiply(inverse(sF1_fnc),inverse(sF1_fnc)))=sF1_fnc),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f7037,f8610])).
% 130.76/17.16 fof(f10296,plain,(
% 130.76/17.16 inverse(multiply(sF1_fnc,sF1_fnc))=sF1_fnc),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10115,f10264])).
% 130.76/17.16 fof(f10411,plain,(
% 130.76/17.16 multiply(sF1_fnc,multiply(inverse(sF1_fnc),sF1_fnc))=sF1_fnc),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f10296,f8610])).
% 130.76/17.16 fof(f10412,plain,(
% 130.76/17.16 inverse(multiply(inverse(sF1_fnc),sF1_fnc))=sF1_fnc),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f10296,f7102])).
% 130.76/17.16 fof(f10416,plain,(
% 130.76/17.16 multiply(sF1_fnc,sF1_fnc)=sF1_fnc),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f10411])).
% 130.76/17.16 fof(f10420,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=X0)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10704,f7100])).
% 130.76/17.16 fof(f10555,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(X0,inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),multiply(X0,sF1_fnc)))))=X1)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10704,f10078])).
% 130.76/17.16 fof(f10566,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),inverse(sF1_fnc))))=multiply(inverse(multiply(sF1_fnc,X0)),inverse(multiply(multiply(X1,X2),sF1_fnc))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10704,f10064])).
% 130.76/17.16 fof(f10589,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),multiply(inverse(X0),sF1_fnc))=inverse(multiply(X0,sF1_fnc)))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10704,f10115])).
% 130.76/17.16 fof(f10650,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,sF1_fnc)))))=inverse(multiply(inverse(multiply(sF1_fnc,X1)),inverse(multiply(multiply(X0,X2),sF1_fnc)))))),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f10704,f8575])).
% 130.76/17.16 fof(f10704,plain,(
% 130.76/17.16 inverse(sF1_fnc)=sF1_fnc),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f10412])).
% 130.76/17.16 fof(f11004,plain,(
% 130.76/17.16 ![X0,X1]: (multiply(X0,inverse(multiply(sF1_fnc,multiply(inverse(X1),multiply(X0,sF1_fnc)))))=X1)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f10555])).
% 130.76/17.16 fof(f11020,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),inverse(sF1_fnc))))=multiply(inverse(multiply(sF1_fnc,X0)),inverse(multiply(multiply(X1,X2),sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f10566])).
% 130.76/17.16 fof(f11031,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(multiply(X1,X2)),sF1_fnc)))=multiply(inverse(multiply(sF1_fnc,X0)),inverse(multiply(multiply(X1,X2),sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f11020])).
% 130.76/17.16 fof(f11093,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))=inverse(multiply(X0,sF1_fnc)))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f10589])).
% 130.76/17.16 fof(f11199,plain,(
% 130.76/17.16 ![X0,X1,X2]: (multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,sF1_fnc)))))=inverse(multiply(sF1_fnc,multiply(inverse(X1),multiply(inverse(multiply(X0,X2)),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f11031,f10650])).
% 130.76/17.16 fof(f11321,plain,(
% 130.76/17.16 ![X0]: (multiply(inverse(sF1_fnc),inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))=X0)),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f7037,f11004])).
% 130.76/17.16 fof(f11324,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))=X0)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f11321])).
% 130.76/17.16 fof(f11325,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(inverse(multiply(X0,sF1_fnc))))=X0)),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f11093,f11324])).
% 130.76/17.16 fof(f11353,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(multiply(sF1_fnc,sF1_fnc)))))=inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(paramodulation,[status(thm)],[f10416,f11199])).
% 130.76/17.16 fof(f11375,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),inverse(sF1_fnc))))=inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10416,f11353])).
% 130.76/17.16 fof(f11376,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,inverse(multiply(inverse(X0),sF1_fnc)))=inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10704,f11375])).
% 130.76/17.16 fof(f11377,plain,(
% 130.76/17.16 ![X0]: (X0=inverse(multiply(sF1_fnc,multiply(inverse(X0),multiply(inverse(sF1_fnc),sF1_fnc)))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f10420,f11376])).
% 130.76/17.16 fof(f11378,plain,(
% 130.76/17.16 ![X0]: (X0=inverse(multiply(sF1_fnc,multiply(inverse(X0),sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f7037,f11377])).
% 130.76/17.16 fof(f11386,plain,(
% 130.76/17.16 ![X0]: (multiply(sF1_fnc,X0)=X0)),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f11407,f11325])).
% 130.76/17.16 fof(f11407,plain,(
% 130.76/17.16 ![X0]: (X0=inverse(inverse(multiply(X0,sF1_fnc))))),
% 130.76/17.16 inference(forward_demodulation,[status(thm)],[f11093,f11378])).
% 130.76/17.16 fof(f11424,plain,(
% 130.76/17.16 sF0_fnc=a2),
% 130.76/17.16 inference(backward_demodulation,[status(thm)],[f11386,f7])).
% 130.76/17.26 fof(f11668,plain,(
% 130.76/17.26 $false),
% 130.76/17.26 inference(forward_subsumption_resolution,[status(thm)],[f11424,f8])).
% 130.76/17.26 % SZS output end CNFRefutation for theBenchmark.p
% 13.53/17.49 % Elapsed time: 16.994665 seconds
% 13.53/17.49 % CPU time: 133.350531 seconds
% 13.53/17.49 % Total memory used: 1.089 GB
% 13.53/17.49 % Net memory used: 1.053 GB
%------------------------------------------------------------------------------