%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP427-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:33:51 PM UTC 2026
% Result : Unsatisfiable 53.93s 7.26s
% Output : CNFRefutation 53.93s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : multiply(A,inverse(multiply(multiply(inverse(multiply(inverse(B),multiply(inverse(A),C))),D),inverse(multiply(B,D))))) = C,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF1_fnc = inverse(a1),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f6,definition,
sF0_fnc = multiply(sF1_fnc,a1),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f7,definition,
sF3_fnc = inverse(b1),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f8,definition,
sF2_fnc = multiply(sF3_fnc,b1),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f9,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f4,f8,f7,f6,f5]) ).
fof(f15,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(sF1_fnc,X1))),X2),inverse(multiply(X0,X2))))) = X1,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f17,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),a1),inverse(sF0_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f18,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))) = X2,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f19,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f17,f17]) ).
fof(f21,plain,
! [X0] : multiply(b1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF3_fnc,X0))),a1),inverse(sF0_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f7,f17]) ).
fof(f23,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(multiply(inverse(X2),multiply(inverse(X0),X3)))),X1))),a1),inverse(sF0_fnc)))))))) = X3,
inference(paramodulation,[status(thm)],[f17,f3]) ).
fof(f24,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X2))),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f17,f3]) ).
fof(f28,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),X3))),a1),inverse(sF0_fnc)))),inverse(X3)))) = X2,
inference(backward_demodulation,[status(thm)],[f32,f18]) ).
fof(f29,plain,
! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF1_fnc,X0))),a1),inverse(sF0_fnc)))) = X0,
inference(backward_demodulation,[status(thm)],[f32,f15]) ).
fof(f32,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a1),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f19,f24]) ).
fof(f33,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc))))))))) = X3,
inference(forward_demodulation,[status(thm)],[f19,f23]) ).
fof(f35,plain,
multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(sF0_fnc)))) = a1,
inference(paramodulation,[status(thm)],[f6,f29]) ).
fof(f37,plain,
multiply(b1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF2_fnc)),a1),inverse(sF0_fnc)))) = b1,
inference(paramodulation,[status(thm)],[f8,f21]) ).
fof(f126,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(sF1_fnc),X0))),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X1),X2))),a1),inverse(sF0_fnc)))),inverse(X2))),
inference(paramodulation,[status(thm)],[f28,f29]) ).
fof(f171,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc))))),X2))),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f19,f19]) ).
fof(f175,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f19,f17]) ).
fof(f176,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc)))),X2))),a1),inverse(sF0_fnc)))) = X2,
inference(paramodulation,[status(thm)],[f19,f17]) ).
fof(f183,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a1),inverse(sF0_fnc))))) = X0,
inference(paramodulation,[status(thm)],[f5,f175]) ).
fof(f189,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a1),inverse(sF0_fnc)))))) = multiply(inverse(inverse(X1)),X2),
inference(paramodulation,[status(thm)],[f19,f175]) ).
fof(f194,plain,
! [X0] : multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f175,f29]) ).
fof(f196,plain,
multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(sF2_fnc),a1),inverse(sF0_fnc))))) = b1,
inference(backward_demodulation,[status(thm)],[f194,f37]) ).
fof(f197,plain,
multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(sF0_fnc),a1),inverse(sF0_fnc))))) = a1,
inference(backward_demodulation,[status(thm)],[f194,f35]) ).
fof(f198,plain,
! [X0] : multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(multiply(sF3_fnc,X0)),a1),inverse(sF0_fnc))))) = X0,
inference(backward_demodulation,[status(thm)],[f194,f21]) ).
fof(f199,plain,
! [X0] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,X0)),a1),inverse(sF0_fnc))))) = X0,
inference(backward_demodulation,[status(thm)],[f194,f29]) ).
fof(f200,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),a1),inverse(sF0_fnc)))),
inference(backward_demodulation,[status(thm)],[f194,f19]) ).
fof(f201,plain,
! [X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),a1),inverse(sF0_fnc))))) = X1,
inference(backward_demodulation,[status(thm)],[f194,f17]) ).
fof(f212,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc)))),X2)),a1),inverse(sF0_fnc))))) = X2,
inference(backward_demodulation,[status(thm)],[f194,f176]) ).
fof(f216,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a1),inverse(sF0_fnc)))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc))))),X2)),a1),inverse(sF0_fnc)))),
inference(backward_demodulation,[status(thm)],[f194,f171]) ).
fof(f223,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(sF1_fnc),X0))),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),a1),inverse(sF0_fnc))))),inverse(X2))),
inference(backward_demodulation,[status(thm)],[f194,f126]) ).
fof(f237,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc)))))))))) = X3,
inference(backward_demodulation,[status(thm)],[f194,f33]) ).
fof(f242,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF0_fnc))))))) = multiply(inverse(inverse(X1)),X2),
inference(forward_demodulation,[status(thm)],[f194,f189]) ).
fof(f247,plain,
! [X0,X1,X2] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(sF1_fnc),X0))),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),a1),inverse(sF0_fnc))))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f194,f223]) ).
fof(f256,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f194,f183]) ).
fof(f276,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),multiply(a1,inverse(multiply(multiply(inverse(multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))),X2)),a1),inverse(sF0_fnc))))) = X2,
inference(forward_demodulation,[status(thm)],[f194,f212]) ).
fof(f279,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF0_fnc))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a1),inverse(sF0_fnc))))),X2)),a1),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f194,f216]) ).
fof(f280,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc)))))),multiply(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))),X2))),a1),inverse(sF0_fnc)))) = X2,
inference(backward_demodulation,[status(thm)],[f282,f276]) ).
fof(f282,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a1),inverse(sF0_fnc)),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF0_fnc))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc)))))),X2)),a1),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f194,f279]) ).
fof(f283,plain,
! [X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))) = multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),a1),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f194,f200]) ).
fof(f295,plain,
multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(sF1_fnc,a1),inverse(sF0_fnc)))))) = a1,
inference(paramodulation,[status(thm)],[f5,f256]) ).
fof(f297,plain,
multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))) = a1,
inference(forward_demodulation,[status(thm)],[f6,f295]) ).
fof(f303,plain,
! [X0,X1,X2] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),X0)),a1),inverse(sF0_fnc))))),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),a1),inverse(sF0_fnc))))),inverse(X2))),
inference(paramodulation,[status(thm)],[f201,f247]) ).
fof(f314,plain,
! [X0,X1,X2] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))))),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),a1),inverse(sF0_fnc))))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f283,f303]) ).
fof(f319,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),a1),inverse(sF0_fnc))))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f199,f314]) ).
fof(f360,plain,
! [X0,X1] : multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))))) = multiply(inverse(inverse(X0)),X1),
inference(paramodulation,[status(thm)],[f5,f242]) ).
fof(f364,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(inverse(b1)),multiply(sF3_fnc,X1)),
inference(paramodulation,[status(thm)],[f198,f242]) ).
fof(f365,plain,
! [X0] : multiply(inverse(X0),multiply(X0,b1)) = multiply(inverse(inverse(b1)),sF2_fnc),
inference(paramodulation,[status(thm)],[f196,f242]) ).
fof(f367,plain,
! [X0] : multiply(inverse(X0),multiply(X0,a1)) = multiply(inverse(inverse(a1)),sF0_fnc),
inference(paramodulation,[status(thm)],[f197,f242]) ).
fof(f370,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,multiply(X1,multiply(a1,inverse(multiply(multiply(sF1_fnc,a1),inverse(sF0_fnc))))))) = multiply(inverse(inverse(X1)),a1),
inference(paramodulation,[status(thm)],[f5,f242]) ).
fof(f372,plain,
! [X0] : multiply(inverse(X0),multiply(X0,b1)) = multiply(inverse(sF3_fnc),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f7,f365]) ).
fof(f373,plain,
! [X0] : multiply(inverse(X0),multiply(X0,a1)) = multiply(inverse(sF1_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f5,f367]) ).
fof(f374,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(sF3_fnc),multiply(sF3_fnc,X1)),
inference(forward_demodulation,[status(thm)],[f7,f364]) ).
fof(f375,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,multiply(X1,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))) = multiply(inverse(inverse(X1)),a1),
inference(forward_demodulation,[status(thm)],[f6,f370]) ).
fof(f377,plain,
multiply(sF3_fnc,multiply(b1,b1)) = multiply(inverse(sF3_fnc),sF2_fnc),
inference(paramodulation,[status(thm)],[f7,f372]) ).
fof(f378,plain,
multiply(sF1_fnc,multiply(a1,b1)) = multiply(inverse(sF3_fnc),sF2_fnc),
inference(paramodulation,[status(thm)],[f5,f372]) ).
fof(f413,plain,
multiply(sF3_fnc,multiply(b1,a1)) = multiply(inverse(sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f7,f373]) ).
fof(f414,plain,
multiply(sF1_fnc,multiply(a1,a1)) = multiply(inverse(sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f5,f373]) ).
fof(f501,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(X2),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f374,f374]) ).
fof(f508,plain,
! [X0] : multiply(inverse(X0),multiply(X0,multiply(b1,a1))) = multiply(inverse(sF3_fnc),multiply(inverse(sF1_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f413,f374]) ).
fof(f509,plain,
! [X0] : multiply(inverse(X0),multiply(X0,multiply(b1,b1))) = multiply(inverse(sF3_fnc),multiply(inverse(sF3_fnc),sF2_fnc)),
inference(paramodulation,[status(thm)],[f377,f374]) ).
fof(f595,plain,
! [X0,X1] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f5,f501]) ).
fof(f602,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(X3),multiply(X3,multiply(X0,X2))),
inference(paramodulation,[status(thm)],[f501,f501]) ).
fof(f725,plain,
! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),a1),inverse(sF0_fnc)))) = X0,
inference(backward_demodulation,[status(thm)],[f595,f280]) ).
fof(f726,plain,
multiply(sF1_fnc,multiply(a1,multiply(b1,a1))) = multiply(inverse(sF3_fnc),multiply(inverse(sF1_fnc),sF0_fnc)),
inference(backward_demodulation,[status(thm)],[f595,f508]) ).
fof(f727,plain,
multiply(sF1_fnc,multiply(a1,multiply(b1,b1))) = multiply(inverse(sF3_fnc),multiply(inverse(sF3_fnc),sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f595,f509]) ).
fof(f730,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))) = multiply(inverse(inverse(X0)),a1),
inference(backward_demodulation,[status(thm)],[f595,f375]) ).
fof(f733,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(sF1_fnc,multiply(a1,multiply(X0,X2))),
inference(backward_demodulation,[status(thm)],[f595,f602]) ).
fof(f768,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),multiply(sF1_fnc,multiply(a1,X1))) = multiply(sF1_fnc,multiply(a1,multiply(X0,X1))),
inference(forward_demodulation,[status(thm)],[f595,f733]) ).
fof(f936,plain,
! [X0] : multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,X0)),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f725,f725]) ).
fof(f953,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(sF1_fnc),sF0_fnc)) = multiply(sF1_fnc,multiply(a1,multiply(X0,a1))),
inference(paramodulation,[status(thm)],[f414,f768]) ).
fof(f981,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
inference(paramodulation,[status(thm)],[f201,f237]) ).
fof(f1003,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),multiply(a1,inverse(multiply(multiply(sF1_fnc,a1),inverse(sF0_fnc)))))))))) = X2,
inference(paramodulation,[status(thm)],[f5,f237]) ).
fof(f1005,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(a1,inverse(multiply(multiply(inverse(X2),a1),inverse(sF0_fnc))))))))),
inference(paramodulation,[status(thm)],[f237,f201]) ).
fof(f1037,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))))))) = X2,
inference(forward_demodulation,[status(thm)],[f6,f1003]) ).
fof(f1202,plain,
! [X0] : multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),X0),inverse(multiply(sF3_fnc,X0))))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f726,f981]) ).
fof(f1204,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,X1))),X2),inverse(multiply(inverse(X0),X2))))) = X1,
inference(paramodulation,[status(thm)],[f595,f981]) ).
fof(f1234,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X0),X1))),b1),inverse(sF2_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f8,f981]) ).
fof(f1296,plain,
multiply(sF1_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),b1),inverse(sF2_fnc)))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f726,f1234]) ).
fof(f1297,plain,
multiply(sF3_fnc,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,b1)))),b1),inverse(sF2_fnc)))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f727,f1234]) ).
fof(f1359,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(sF1_fnc,multiply(a1,X1)),inverse(multiply(inverse(X0),multiply(multiply(sF1_fnc,multiply(a1,X2)),X1)))))) = X2,
inference(paramodulation,[status(thm)],[f595,f1204]) ).
fof(f1542,plain,
multiply(b1,multiply(a1,inverse(multiply(multiply(inverse(sF2_fnc),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,b1)))),b1),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f1297,f198]) ).
fof(f1545,plain,
b1 = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,b1)))),b1),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f196,f1542]) ).
fof(f1553,plain,
multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(b1,a1),inverse(sF0_fnc)))))) = multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,b1)))),b1),inverse(sF2_fnc)),
inference(paramodulation,[status(thm)],[f1545,f256]) ).
fof(f1555,plain,
b1 = inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(b1,a1),inverse(sF0_fnc))))))),
inference(backward_demodulation,[status(thm)],[f1553,f1545]) ).
fof(f1588,plain,
multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(sF0_fnc),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),b1),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f1296,f199]) ).
fof(f1591,plain,
a1 = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),b1),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f197,f1588]) ).
fof(f1598,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),b1),inverse(sF2_fnc)),X0)),
inference(paramodulation,[status(thm)],[f1591,f595]) ).
fof(f1599,plain,
multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(a1,a1),inverse(sF0_fnc)))))) = multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),b1),inverse(sF2_fnc)),
inference(paramodulation,[status(thm)],[f1591,f256]) ).
fof(f1610,plain,
a1 = inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(a1,a1),inverse(sF0_fnc))))))),
inference(backward_demodulation,[status(thm)],[f1599,f1591]) ).
fof(f1612,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(a1,a1),inverse(sF0_fnc)))))),X0)),
inference(backward_demodulation,[status(thm)],[f1599,f1598]) ).
fof(f1719,plain,
! [X0] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(sF0_fnc),a1),inverse(sF0_fnc))))) = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),X0),inverse(multiply(sF3_fnc,X0)))),
inference(paramodulation,[status(thm)],[f1202,f199]) ).
fof(f1723,plain,
! [X0] : a1 = inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1)))),X0),inverse(multiply(sF3_fnc,X0)))),
inference(forward_demodulation,[status(thm)],[f197,f1719]) ).
fof(f1731,plain,
! [X0] : a1 = inverse(multiply(X0,inverse(multiply(sF3_fnc,multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(multiply(sF1_fnc,multiply(a1,multiply(b1,a1))))),X0)),a1),inverse(sF0_fnc)))))))),
inference(paramodulation,[status(thm)],[f201,f1723]) ).
fof(f1754,plain,
! [X0] : a1 = inverse(multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(sF1_fnc,multiply(a1,multiply(b1,a1))),multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc))))))))),
inference(forward_demodulation,[status(thm)],[f283,f1731]) ).
fof(f2978,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(X0),multiply(multiply(sF1_fnc,multiply(a1,X1)),a1)))))) = X1,
inference(paramodulation,[status(thm)],[f414,f1359]) ).
fof(f2979,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(sF3_fnc),sF2_fnc),inverse(multiply(inverse(X0),multiply(multiply(sF1_fnc,multiply(a1,X1)),b1)))))) = X1,
inference(paramodulation,[status(thm)],[f378,f1359]) ).
fof(f2995,plain,
! [X0,X1] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(multiply(sF1_fnc,multiply(a1,X1)),inverse(multiply(sF1_fnc,multiply(a1,X1)))))) = X0,
inference(paramodulation,[status(thm)],[f595,f1359]) ).
fof(f3087,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(multiply(inverse(sF3_fnc),sF2_fnc),inverse(multiply(sF1_fnc,multiply(a1,b1)))))) = X0,
inference(paramodulation,[status(thm)],[f595,f2979]) ).
fof(f3125,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(multiply(inverse(sF3_fnc),sF2_fnc),inverse(multiply(inverse(sF3_fnc),sF2_fnc))))) = X0,
inference(forward_demodulation,[status(thm)],[f378,f3087]) ).
fof(f3172,plain,
multiply(a1,inverse(multiply(multiply(inverse(sF3_fnc),sF2_fnc),inverse(multiply(inverse(sF3_fnc),sF2_fnc))))) = multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))),
inference(paramodulation,[status(thm)],[f297,f3125]) ).
fof(f3184,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,inverse(multiply(multiply(inverse(sF3_fnc),sF2_fnc),inverse(multiply(inverse(sF3_fnc),sF2_fnc)))))) = multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),
inference(paramodulation,[status(thm)],[f3125,f595]) ).
fof(f3185,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),
inference(backward_demodulation,[status(thm)],[f3172,f3184]) ).
fof(f3216,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(a1,multiply(a1,inverse(multiply(multiply(a1,a1),inverse(sF0_fnc))))),
inference(paramodulation,[status(thm)],[f1610,f3185]) ).
fof(f3239,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))) = multiply(inverse(sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0)),
inference(paramodulation,[status(thm)],[f3185,f595]) ).
fof(f3240,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))),a1),inverse(sF0_fnc))))) = X0,
inference(paramodulation,[status(thm)],[f3185,f201]) ).
fof(f3243,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))) = multiply(inverse(inverse(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc))))))))),X0),
inference(paramodulation,[status(thm)],[f3185,f360]) ).
fof(f3258,plain,
a1 = inverse(multiply(sF1_fnc,multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))),
inference(backward_demodulation,[status(thm)],[f3216,f1610]) ).
fof(f3264,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))),X0)),
inference(backward_demodulation,[status(thm)],[f3216,f1612]) ).
fof(f3266,plain,
! [X0] : multiply(inverse(inverse(sF1_fnc)),a1) = multiply(inverse(inverse(inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc))))))))),X0),
inference(forward_demodulation,[status(thm)],[f730,f3243]) ).
fof(f3267,plain,
! [X0] : multiply(inverse(inverse(sF1_fnc)),a1) = multiply(inverse(inverse(inverse(X0))),X0),
inference(forward_demodulation,[status(thm)],[f256,f3266]) ).
fof(f3280,plain,
! [X0] : a1 = multiply(inverse(sF1_fnc),multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0)),
inference(forward_demodulation,[status(thm)],[f297,f3239]) ).
fof(f3283,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))),a1),inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f936,f3240]) ).
fof(f3285,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f199,f3283]) ).
fof(f3308,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = multiply(sF1_fnc,multiply(a1,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1))),
inference(paramodulation,[status(thm)],[f953,f3267]) ).
fof(f3320,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(a1,inverse(multiply(multiply(inverse(multiply(inverse(inverse(sF1_fnc)),a1)),a1),inverse(sF0_fnc))))) = X0,
inference(paramodulation,[status(thm)],[f3267,f201]) ).
fof(f3324,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(inverse(inverse(inverse(inverse(X0)))),multiply(inverse(inverse(sF1_fnc)),a1)),
inference(paramodulation,[status(thm)],[f3267,f595]) ).
fof(f3328,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(sF1_fnc,multiply(a1,inverse(multiply(multiply(inverse(a1),a1),inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f283,f3320]) ).
fof(f3329,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(multiply(inverse(a1),a1),inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f768,f3328]) ).
fof(f3330,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(multiply(sF1_fnc,a1),inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f3329]) ).
fof(f3334,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))) = X0,
inference(forward_demodulation,[status(thm)],[f6,f3330]) ).
fof(f3341,plain,
multiply(sF1_fnc,multiply(a1,multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))) = inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))),
inference(paramodulation,[status(thm)],[f3185,f3334]) ).
fof(f3344,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(X1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))),
inference(paramodulation,[status(thm)],[f3334,f768]) ).
fof(f3347,plain,
! [X0] : multiply(a1,multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc))))) = multiply(a1,multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))),
inference(paramodulation,[status(thm)],[f3334,f199]) ).
fof(f3357,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = inverse(multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))),
inference(forward_demodulation,[status(thm)],[f730,f3341]) ).
fof(f3358,plain,
! [X0] : multiply(a1,multiply(multiply(sF1_fnc,X0),inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = X0,
inference(backward_demodulation,[status(thm)],[f3347,f199]) ).
fof(f3461,plain,
! [X0] : multiply(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(sF0_fnc,inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f3185,f3285]) ).
fof(f3466,plain,
! [X0] : multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a1),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f201,f3285]) ).
fof(f3492,plain,
! [X0,X1] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))),
inference(backward_demodulation,[status(thm)],[f3618,f283]) ).
fof(f3493,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = X1,
inference(backward_demodulation,[status(thm)],[f3618,f201]) ).
fof(f3494,plain,
! [X0] : multiply(b1,multiply(multiply(sF3_fnc,X0),inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = X0,
inference(backward_demodulation,[status(thm)],[f3618,f198]) ).
fof(f3522,plain,
! [X0,X1,X2] : multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(multiply(inverse(X1),X2),inverse(multiply(sF0_fnc,inverse(sF0_fnc))))),inverse(X2))),
inference(backward_demodulation,[status(thm)],[f3618,f319]) ).
fof(f3583,plain,
! [X0] : a1 = inverse(multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(sF1_fnc,multiply(a1,multiply(b1,a1))),multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))))),
inference(backward_demodulation,[status(thm)],[f3618,f1754]) ).
fof(f3611,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(a1,inverse(multiply(multiply(inverse(X1),a1),inverse(sF0_fnc))))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(X2,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))))),
inference(backward_demodulation,[status(thm)],[f3618,f1005]) ).
fof(f3618,plain,
! [X0] : multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = multiply(a1,inverse(multiply(multiply(inverse(X0),a1),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f194,f3466]) ).
fof(f3635,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f3618,f3492]) ).
fof(f3675,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(multiply(inverse(X1),X2),inverse(multiply(sF0_fnc,inverse(sF0_fnc))))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f3618,f3522]) ).
fof(f3742,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(X2,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))))))),
inference(forward_demodulation,[status(thm)],[f3618,f3611]) ).
fof(f3794,plain,
! [X0] : multiply(a1,multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))),
inference(paramodulation,[status(thm)],[f3493,f3358]) ).
fof(f3836,plain,
a1 = multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)),
inference(paramodulation,[status(thm)],[f414,f3280]) ).
fof(f3837,plain,
a1 = multiply(inverse(sF1_fnc),multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1)),
inference(paramodulation,[status(thm)],[f378,f3280]) ).
fof(f3863,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1),
inference(paramodulation,[status(thm)],[f3837,f3493]) ).
fof(f3865,plain,
! [X0] : multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1) = multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),
inference(backward_demodulation,[status(thm)],[f3863,f3185]) ).
fof(f3871,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = inverse(multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1)),
inference(backward_demodulation,[status(thm)],[f3863,f3357]) ).
fof(f3872,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1)),X0)),
inference(backward_demodulation,[status(thm)],[f3863,f3264]) ).
fof(f3875,plain,
a1 = inverse(multiply(sF1_fnc,multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1))),
inference(backward_demodulation,[status(thm)],[f3863,f3258]) ).
fof(f3880,plain,
multiply(multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(sF0_fnc,inverse(sF0_fnc))),
inference(backward_demodulation,[status(thm)],[f3865,f3461]) ).
fof(f3891,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(paramodulation,[status(thm)],[f3836,f3493]) ).
fof(f3895,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)),X0)),
inference(backward_demodulation,[status(thm)],[f3903,f3872]) ).
fof(f3896,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(sF0_fnc,inverse(sF0_fnc))),
inference(backward_demodulation,[status(thm)],[f3903,f3880]) ).
fof(f3897,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)),
inference(backward_demodulation,[status(thm)],[f3903,f3871]) ).
fof(f3898,plain,
a1 = inverse(multiply(sF1_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1))),
inference(backward_demodulation,[status(thm)],[f3903,f3875]) ).
fof(f3903,plain,
multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(forward_demodulation,[status(thm)],[f3863,f3891]) ).
fof(f3997,plain,
multiply(multiply(inverse(inverse(sF1_fnc)),a1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(paramodulation,[status(thm)],[f3308,f3285]) ).
fof(f3998,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF1_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)))),
inference(paramodulation,[status(thm)],[f3308,f768]) ).
fof(f4006,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(forward_demodulation,[status(thm)],[f3635,f3997]) ).
fof(f4012,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))),
inference(paramodulation,[status(thm)],[f4006,f768]) ).
fof(f4019,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = X0,
inference(forward_demodulation,[status(thm)],[f3334,f4012]) ).
fof(f4046,plain,
multiply(inverse(b1),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(b1,a1),inverse(sF0_fnc)))))),
inference(paramodulation,[status(thm)],[f1555,f4019]) ).
fof(f4054,plain,
b1 = inverse(multiply(sF3_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1))),
inference(backward_demodulation,[status(thm)],[f4066,f1555]) ).
fof(f4066,plain,
multiply(sF3_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(multiply(b1,a1),inverse(sF0_fnc)))))),
inference(forward_demodulation,[status(thm)],[f7,f4046]) ).
fof(f4405,plain,
! [X0] : multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(a1,inverse(multiply(inverse(X0),multiply(X0,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))))))) = a1,
inference(paramodulation,[status(thm)],[f4019,f1037]) ).
fof(f4470,plain,
multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(a1,inverse(multiply(sF1_fnc,multiply(a1,multiply(a1,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))))))))) = a1,
inference(forward_demodulation,[status(thm)],[f595,f4405]) ).
fof(f4471,plain,
multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(a1,inverse(a1)))) = a1,
inference(forward_demodulation,[status(thm)],[f3334,f4470]) ).
fof(f4472,plain,
multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(a1,sF1_fnc))) = a1,
inference(forward_demodulation,[status(thm)],[f5,f4471]) ).
fof(f4539,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(a1,sF1_fnc)))) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(paramodulation,[status(thm)],[f4472,f595]) ).
fof(f4540,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(a1,sF1_fnc)),
inference(paramodulation,[status(thm)],[f4539,f3285]) ).
fof(f4541,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(a1,sF1_fnc))))),
inference(paramodulation,[status(thm)],[f4539,f768]) ).
fof(f4546,plain,
! [X0] : X0 = multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(a1,sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f4019,f4541]) ).
fof(f4548,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(X1,inverse(multiply(a1,sF1_fnc)))))),
inference(backward_demodulation,[status(thm)],[f4687,f3344]) ).
fof(f4550,plain,
! [X0] : multiply(a1,multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(a1,sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f4687,f3794]) ).
fof(f4552,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(a1,sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f4687,f3635]) ).
fof(f4553,plain,
! [X0] : multiply(b1,multiply(multiply(sF3_fnc,X0),inverse(multiply(a1,sF1_fnc)))) = X0,
inference(backward_demodulation,[status(thm)],[f4687,f3494]) ).
fof(f4555,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(a1,sF1_fnc)))) = X1,
inference(backward_demodulation,[status(thm)],[f4687,f3493]) ).
fof(f4556,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(a1,sF1_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f4687,f3285]) ).
fof(f4557,plain,
! [X0] : multiply(a1,multiply(multiply(sF1_fnc,X0),inverse(multiply(a1,sF1_fnc)))) = X0,
inference(backward_demodulation,[status(thm)],[f4687,f3358]) ).
fof(f4599,plain,
! [X0] : a1 = inverse(multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(sF1_fnc,multiply(a1,multiply(b1,a1))),multiply(X0,inverse(multiply(a1,sF1_fnc)))))))),
inference(backward_demodulation,[status(thm)],[f4687,f3583]) ).
fof(f4618,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,inverse(multiply(sF0_fnc,inverse(sF0_fnc))))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(X2,inverse(multiply(a1,sF1_fnc)))))))),
inference(backward_demodulation,[status(thm)],[f4687,f3742]) ).
fof(f4659,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(sF0_fnc,inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(multiply(inverse(X1),X2),inverse(multiply(a1,sF1_fnc)))),inverse(X2))),
inference(backward_demodulation,[status(thm)],[f4687,f3675]) ).
fof(f4687,plain,
inverse(multiply(sF0_fnc,inverse(sF0_fnc))) = inverse(multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f3896,f4540]) ).
fof(f4688,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,inverse(multiply(a1,sF1_fnc)))) = inverse(multiply(X2,inverse(multiply(X3,multiply(multiply(inverse(X3),multiply(inverse(inverse(X0)),X1)),multiply(X2,inverse(multiply(a1,sF1_fnc)))))))),
inference(forward_demodulation,[status(thm)],[f4687,f4618]) ).
fof(f4690,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),multiply(multiply(inverse(X1),X2),inverse(multiply(a1,sF1_fnc)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f4687,f4659]) ).
fof(f4713,plain,
! [X0] : multiply(a1,multiply(X0,inverse(multiply(a1,sF1_fnc)))) = multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f4687,f4550]) ).
fof(f4715,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(a1,sF1_fnc)))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f4687,f4552]) ).
fof(f4865,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(a1,sF1_fnc))) = inverse(multiply(a1,sF1_fnc)),
inference(paramodulation,[status(thm)],[f4539,f4556]) ).
fof(f4873,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,inverse(multiply(a1,sF1_fnc)))) = multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),
inference(paramodulation,[status(thm)],[f4556,f595]) ).
fof(f4878,plain,
! [X0] : multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1) = multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),X0),
inference(forward_demodulation,[status(thm)],[f4539,f4873]) ).
fof(f5094,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,multiply(multiply(sF1_fnc,multiply(a1,X0)),a1))),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1))))) = X0,
inference(paramodulation,[status(thm)],[f4878,f2978]) ).
fof(f5098,plain,
! [X0] : multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(multiply(inverse(inverse(sF1_fnc)),a1),multiply(multiply(sF1_fnc,multiply(a1,X0)),a1)))))) = X0,
inference(paramodulation,[status(thm)],[f3897,f2978]) ).
fof(f5130,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,multiply(multiply(sF1_fnc,multiply(a1,X0)),a1))),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),multiply(inverse(inverse(sF1_fnc)),a1)))) = X0,
inference(forward_demodulation,[status(thm)],[f3897,f5094]) ).
fof(f5302,plain,
! [X0,X1,X2] : multiply(X0,multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(a1,sF1_fnc)))) = inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X0),multiply(X1,inverse(multiply(a1,sF1_fnc)))))))),
inference(paramodulation,[status(thm)],[f4019,f4688]) ).
fof(f5352,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,sF1_fnc))) = inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),X0),multiply(X1,inverse(multiply(a1,sF1_fnc)))))))),
inference(forward_demodulation,[status(thm)],[f4865,f5302]) ).
fof(f5411,plain,
! [X0,X1] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(X1,inverse(multiply(sF1_fnc,multiply(a1,multiply(X1,inverse(multiply(a1,sF1_fnc))))))))) = X0,
inference(paramodulation,[status(thm)],[f4546,f2995]) ).
fof(f5444,plain,
! [X0,X1] : multiply(multiply(sF1_fnc,multiply(a1,X0)),inverse(multiply(X1,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f4546,f5411]) ).
fof(f5478,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = multiply(X0,inverse(multiply(a1,sF1_fnc))),
inference(paramodulation,[status(thm)],[f4546,f5444]) ).
fof(f5638,plain,
! [X0] : multiply(b1,multiply(multiply(sF3_fnc,inverse(multiply(a1,sF1_fnc))),inverse(multiply(a1,sF1_fnc)))) = inverse(multiply(X0,inverse(X0))),
inference(paramodulation,[status(thm)],[f5478,f4553]) ).
fof(f5647,plain,
! [X0] : inverse(multiply(a1,sF1_fnc)) = inverse(multiply(X0,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f4553,f5638]) ).
fof(f5687,plain,
! [X0] : multiply(inverse(inverse(multiply(a1,sF1_fnc))),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1)) = multiply(X0,inverse(X0)),
inference(paramodulation,[status(thm)],[f5647,f4019]) ).
fof(f5711,plain,
! [X0] : multiply(a1,sF1_fnc) = multiply(X0,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f4019,f5687]) ).
fof(f5724,plain,
! [X0] : multiply(X0,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f5711,f4555]) ).
fof(f5725,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(sF1_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1))))) = multiply(a1,multiply(a1,sF1_fnc)),
inference(paramodulation,[status(thm)],[f5711,f3895]) ).
fof(f5732,plain,
multiply(a1,multiply(multiply(a1,sF1_fnc),inverse(multiply(a1,sF1_fnc)))) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f5711,f4557]) ).
fof(f5746,plain,
multiply(a1,multiply(a1,sF1_fnc)) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5711,f5732]) ).
fof(f5753,plain,
multiply(sF1_fnc,multiply(a1,a1)) = multiply(a1,multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f3898,f5725]) ).
fof(f5754,plain,
multiply(inverse(sF1_fnc),sF0_fnc) = multiply(a1,multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f414,f5753]) ).
fof(f5755,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),a1)),X0)),
inference(backward_demodulation,[status(thm)],[f5842,f3895]) ).
fof(f5757,plain,
multiply(multiply(inverse(inverse(sF1_fnc)),a1),inverse(multiply(a1,sF1_fnc))) = inverse(multiply(a1,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f5842,f4865]) ).
fof(f5760,plain,
b1 = inverse(multiply(sF3_fnc,multiply(inverse(inverse(sF1_fnc)),a1))),
inference(backward_demodulation,[status(thm)],[f5842,f4054]) ).
fof(f5765,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = inverse(multiply(inverse(inverse(sF1_fnc)),a1)),
inference(backward_demodulation,[status(thm)],[f5842,f3897]) ).
fof(f5766,plain,
a1 = inverse(multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),a1))),
inference(backward_demodulation,[status(thm)],[f5842,f3898]) ).
fof(f5768,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(sF1_fnc)) = multiply(sF1_fnc,multiply(a1,multiply(X0,a1))),
inference(backward_demodulation,[status(thm)],[f5842,f953]) ).
fof(f5769,plain,
multiply(sF1_fnc,multiply(a1,multiply(b1,a1))) = multiply(inverse(sF3_fnc),inverse(sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f5842,f726]) ).
fof(f5790,plain,
! [X0] : multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(inverse(sF1_fnc)),a1),multiply(multiply(sF1_fnc,multiply(a1,X0)),a1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f5842,f5098]) ).
fof(f5798,plain,
! [X0] : multiply(multiply(sF1_fnc,multiply(a1,multiply(multiply(sF1_fnc,multiply(a1,X0)),a1))),inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),a1)))) = X0,
inference(backward_demodulation,[status(thm)],[f5842,f5130]) ).
fof(f5823,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF1_fnc)),a1)) = multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(inverse(inverse(sF1_fnc)),a1)))),
inference(backward_demodulation,[status(thm)],[f5842,f3998]) ).
fof(f5842,plain,
multiply(inverse(sF1_fnc),sF0_fnc) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5746,f5754]) ).
fof(f5849,plain,
! [X0] : multiply(multiply(inverse(inverse(sF1_fnc)),a1),inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(inverse(sF1_fnc)),a1),multiply(multiply(sF1_fnc,multiply(a1,X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f5842,f5790]) ).
fof(f5855,plain,
! [X0] : a1 = inverse(multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(inverse(sF3_fnc),inverse(sF1_fnc)),multiply(X0,inverse(multiply(a1,sF1_fnc)))))))),
inference(backward_demodulation,[status(thm)],[f5769,f4599]) ).
fof(f5863,plain,
multiply(sF1_fnc,multiply(a1,inverse(multiply(a1,sF1_fnc)))) = inverse(multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f4715,f5757]) ).
fof(f5864,plain,
multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1) = inverse(multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f4539,f5863]) ).
fof(f5866,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = multiply(inverse(inverse(inverse(inverse(X0)))),inverse(multiply(a1,sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f5896,f3324]) ).
fof(f5881,plain,
! [X0] : multiply(multiply(inverse(inverse(sF1_fnc)),a1),inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(sF1_fnc,multiply(a1,X0)),a1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f5896,f5849]) ).
fof(f5896,plain,
multiply(inverse(inverse(sF1_fnc)),a1) = inverse(multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5842,f5864]) ).
fof(f5916,plain,
a1 = multiply(inverse(sF1_fnc),inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f5352,f5855]) ).
fof(f5918,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(multiply(a1,sF1_fnc))) = multiply(sF1_fnc,multiply(a1,multiply(X0,multiply(inverse(inverse(sF1_fnc)),a1)))),
inference(forward_demodulation,[status(thm)],[f5896,f5823]) ).
fof(f5919,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(multiply(a1,sF1_fnc))) = multiply(sF1_fnc,multiply(a1,multiply(X0,inverse(multiply(a1,sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f5896,f5918]) ).
fof(f5923,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(multiply(a1,sF1_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f4546,f5919]) ).
fof(f5978,plain,
! [X0] : multiply(X0,multiply(a1,sF1_fnc)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f5711,f5724]) ).
fof(f5980,plain,
b1 = inverse(multiply(sF3_fnc,inverse(multiply(a1,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f5896,f5760]) ).
fof(f6019,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(multiply(X0,multiply(X1,inverse(multiply(a1,sF1_fnc)))))),
inference(backward_demodulation,[status(thm)],[f6087,f4548]) ).
fof(f6051,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(sF1_fnc)) = inverse(inverse(multiply(X0,a1))),
inference(backward_demodulation,[status(thm)],[f6087,f5768]) ).
fof(f6087,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,X0)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f5923,f5866]) ).
fof(f6181,plain,
! [X0] : multiply(multiply(inverse(inverse(multiply(sF1_fnc,multiply(a1,X0)))),inverse(sF1_fnc)),inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),a1)))) = X0,
inference(forward_demodulation,[status(thm)],[f5768,f5798]) ).
fof(f6182,plain,
! [X0] : multiply(inverse(inverse(multiply(multiply(sF1_fnc,multiply(a1,X0)),a1))),inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),a1)))) = X0,
inference(forward_demodulation,[status(thm)],[f6051,f6181]) ).
fof(f6183,plain,
! [X0] : multiply(inverse(inverse(multiply(inverse(inverse(X0)),a1))),inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(sF1_fnc)),a1)))) = X0,
inference(forward_demodulation,[status(thm)],[f6087,f6182]) ).
fof(f6184,plain,
! [X0] : multiply(inverse(inverse(multiply(inverse(inverse(X0)),a1))),inverse(multiply(inverse(sF1_fnc),inverse(multiply(a1,sF1_fnc))))) = X0,
inference(forward_demodulation,[status(thm)],[f5896,f6183]) ).
fof(f6185,plain,
! [X0] : multiply(inverse(inverse(multiply(inverse(inverse(X0)),a1))),inverse(a1)) = X0,
inference(forward_demodulation,[status(thm)],[f5916,f6184]) ).
fof(f6186,plain,
! [X0] : multiply(inverse(inverse(multiply(inverse(inverse(X0)),a1))),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f6185]) ).
fof(f6197,plain,
a1 = inverse(multiply(sF1_fnc,inverse(multiply(a1,sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f5896,f5766]) ).
fof(f6213,plain,
inverse(multiply(a1,sF1_fnc)) = inverse(multiply(inverse(inverse(sF1_fnc)),a1)),
inference(forward_demodulation,[status(thm)],[f5896,f5765]) ).
fof(f6215,plain,
inverse(multiply(a1,sF1_fnc)) = inverse(inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f5896,f6213]) ).
fof(f6286,plain,
! [X0] : multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(multiply(sF1_fnc,multiply(a1,X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f5896,f5881]) ).
fof(f6287,plain,
! [X0] : multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(sF1_fnc),inverse(multiply(inverse(multiply(a1,sF1_fnc)),multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f6087,f6286]) ).
fof(f6295,plain,
! [X0] : inverse(inverse(X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(inverse(inverse(sF1_fnc)),a1)),X0)),
inference(forward_demodulation,[status(thm)],[f6087,f5755]) ).
fof(f6296,plain,
! [X0] : inverse(inverse(X0)) = multiply(a1,multiply(multiply(sF1_fnc,inverse(multiply(a1,sF1_fnc))),X0)),
inference(forward_demodulation,[status(thm)],[f5896,f6295]) ).
fof(f6307,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(a1,sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),multiply(multiply(inverse(X1),X3),inverse(multiply(a1,sF1_fnc)))),inverse(X3))),X0)),multiply(multiply(multiply(X2,inverse(multiply(a1,sF1_fnc))),X4),inverse(multiply(a1,sF1_fnc)))),inverse(X4))),
inference(paramodulation,[status(thm)],[f4690,f4690]) ).
fof(f6333,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),inverse(multiply(a1,sF1_fnc)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f4690,f6307]) ).
fof(f6363,plain,
multiply(sF1_fnc,inverse(inverse(a1))) = inverse(inverse(multiply(a1,sF1_fnc))),
inference(paramodulation,[status(thm)],[f5978,f6087]) ).
fof(f6377,plain,
multiply(sF1_fnc,inverse(sF1_fnc)) = inverse(inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f6363]) ).
fof(f6378,plain,
multiply(a1,sF1_fnc) = inverse(inverse(multiply(a1,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f5711,f6377]) ).
fof(f6379,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(a1,sF1_fnc)))) = multiply(multiply(inverse(inverse(X0)),X1),multiply(a1,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f6517,f4715]) ).
fof(f6381,plain,
! [X0] : multiply(a1,multiply(X0,inverse(multiply(a1,sF1_fnc)))) = multiply(multiply(inverse(sF1_fnc),X0),multiply(a1,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f6517,f4713]) ).
fof(f6382,plain,
! [X0] : multiply(a1,multiply(multiply(sF1_fnc,X0),multiply(a1,sF1_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f6517,f4557]) ).
fof(f6386,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),multiply(a1,sF1_fnc))) = X1,
inference(backward_demodulation,[status(thm)],[f6517,f4555]) ).
fof(f6395,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(a1,sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),multiply(a1,sF1_fnc))),inverse(X2))),
inference(backward_demodulation,[status(thm)],[f6517,f6333]) ).
fof(f6402,plain,
! [X0] : inverse(inverse(X0)) = multiply(a1,multiply(multiply(sF1_fnc,multiply(a1,sF1_fnc)),X0)),
inference(backward_demodulation,[status(thm)],[f6517,f6296]) ).
fof(f6408,plain,
! [X0] : multiply(inverse(multiply(a1,sF1_fnc)),inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f6517,f6287]) ).
fof(f6416,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(multiply(X0,multiply(X1,multiply(a1,sF1_fnc))))),
inference(backward_demodulation,[status(thm)],[f6517,f6019]) ).
fof(f6433,plain,
a1 = inverse(multiply(sF1_fnc,multiply(a1,sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f6517,f6197]) ).
fof(f6467,plain,
b1 = inverse(multiply(sF3_fnc,multiply(a1,sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f6517,f5980]) ).
fof(f6478,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(a1,sF1_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f6517,f5923]) ).
fof(f6517,plain,
multiply(a1,sF1_fnc) = inverse(multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f6215,f6378]) ).
fof(f6523,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f5978,f6478]) ).
fof(f6533,plain,
! [X0,X1] : multiply(X0,inverse(inverse(multiply(inverse(X0),X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f5978,f6386]) ).
fof(f6565,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(a1,sF1_fnc))) = multiply(multiply(inverse(inverse(X0)),X1),multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f6517,f6379]) ).
fof(f6566,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(multiply(inverse(inverse(X0)),X1),multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5978,f6565]) ).
fof(f6567,plain,
! [X0] : multiply(multiply(X0,inverse(inverse(a1))),sF1_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f6570,f6186]) ).
fof(f6570,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(multiply(inverse(inverse(X0)),X1))),
inference(forward_demodulation,[status(thm)],[f5978,f6566]) ).
fof(f6573,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = inverse(inverse(multiply(X0,inverse(inverse(X1))))),
inference(forward_demodulation,[status(thm)],[f5978,f6416]) ).
fof(f6579,plain,
a1 = inverse(inverse(inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f6087,f6433]) ).
fof(f6596,plain,
b1 = inverse(inverse(inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f5978,f6467]) ).
fof(f6606,plain,
! [X0] : multiply(multiply(X0,inverse(sF1_fnc)),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f6567]) ).
fof(f6625,plain,
! [X0,X1,X2] : multiply(X0,multiply(a1,sF1_fnc)) = inverse(multiply(multiply(inverse(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),multiply(a1,sF1_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f6517,f6395]) ).
fof(f6626,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),multiply(a1,sF1_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f5978,f6625]) ).
fof(f6627,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),multiply(a1,sF1_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f6517,f6626]) ).
fof(f6628,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),multiply(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2),multiply(a1,sF1_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f5978,f6627]) ).
fof(f6629,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),inverse(inverse(multiply(multiply(X1,inverse(multiply(a1,sF1_fnc))),X2)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f5978,f6628]) ).
fof(f6630,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),inverse(inverse(multiply(multiply(X1,multiply(a1,sF1_fnc)),X2)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f6517,f6629]) ).
fof(f6631,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),inverse(inverse(multiply(inverse(inverse(X1)),X2)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f5978,f6630]) ).
fof(f6632,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),multiply(X1,inverse(inverse(X2)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f6570,f6631]) ).
fof(f6729,plain,
! [X0] : multiply(a1,multiply(X0,multiply(a1,sF1_fnc))) = multiply(multiply(inverse(sF1_fnc),X0),multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f6517,f6381]) ).
fof(f6730,plain,
! [X0] : multiply(a1,inverse(inverse(X0))) = multiply(multiply(inverse(sF1_fnc),X0),multiply(a1,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5978,f6729]) ).
fof(f6735,plain,
! [X0] : multiply(a1,inverse(inverse(X0))) = inverse(inverse(multiply(inverse(sF1_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f5978,f6730]) ).
fof(f6755,plain,
! [X0] : inverse(inverse(X0)) = multiply(a1,multiply(inverse(inverse(sF1_fnc)),X0)),
inference(forward_demodulation,[status(thm)],[f6087,f6402]) ).
fof(f6776,plain,
! [X0] : multiply(a1,inverse(inverse(multiply(sF1_fnc,X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f5978,f6382]) ).
fof(f6806,plain,
! [X0] : multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(a1,sF1_fnc),multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f6517,f6408]) ).
fof(f6902,plain,
multiply(a1,sF1_fnc) = multiply(inverse(inverse(sF1_fnc)),a1),
inference(paramodulation,[status(thm)],[f6579,f5711]) ).
fof(f6918,plain,
multiply(multiply(a1,sF1_fnc),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f5711,f6606]) ).
fof(f6937,plain,
! [X0,X1] : multiply(X0,inverse(inverse(inverse(inverse(multiply(inverse(inverse(inverse(X0))),X1)))))) = inverse(inverse(X1)),
inference(paramodulation,[status(thm)],[f6533,f6570]) ).
fof(f6940,plain,
! [X0,X1,X2] : multiply(multiply(inverse(inverse(X0)),X1),inverse(inverse(X2))) = inverse(inverse(multiply(multiply(X0,inverse(inverse(X1))),X2))),
inference(paramodulation,[status(thm)],[f6570,f6570]) ).
fof(f6944,plain,
! [X0] : multiply(multiply(a1,sF1_fnc),inverse(inverse(X0))) = inverse(inverse(multiply(inverse(multiply(a1,sF1_fnc)),X0))),
inference(paramodulation,[status(thm)],[f6517,f6570]) ).
fof(f6945,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(inverse(X0)),X1)),inverse(inverse(X2))) = inverse(inverse(multiply(inverse(multiply(X0,inverse(inverse(X1)))),X2))),
inference(paramodulation,[status(thm)],[f6570,f6570]) ).
fof(f6951,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(inverse(X1)))) = X1,
inference(paramodulation,[status(thm)],[f6570,f6533]) ).
fof(f6965,plain,
! [X0,X1] : multiply(X0,multiply(inverse(inverse(inverse(X0))),X1)) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f6523,f6937]) ).
fof(f6995,plain,
! [X0] : multiply(multiply(a1,sF1_fnc),inverse(inverse(X0))) = inverse(inverse(multiply(multiply(a1,sF1_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f6517,f6944]) ).
fof(f7096,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(X1)),
inference(paramodulation,[status(thm)],[f6523,f6951]) ).
fof(f7146,plain,
multiply(inverse(multiply(a1,sF1_fnc)),sF1_fnc) = inverse(inverse(sF1_fnc)),
inference(paramodulation,[status(thm)],[f6918,f7096]) ).
fof(f7147,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1_fnc))),X0) = inverse(inverse(sF1_fnc)),
inference(paramodulation,[status(thm)],[f6606,f7096]) ).
fof(f7178,plain,
multiply(multiply(a1,sF1_fnc),sF1_fnc) = inverse(inverse(sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f6517,f7146]) ).
fof(f7179,plain,
multiply(a1,sF1_fnc) = multiply(sF1_fnc,a1),
inference(backward_demodulation,[status(thm)],[f7201,f6902]) ).
fof(f7180,plain,
a1 = inverse(sF1_fnc),
inference(backward_demodulation,[status(thm)],[f7201,f6579]) ).
fof(f7189,plain,
! [X0] : inverse(inverse(X0)) = multiply(a1,multiply(sF1_fnc,X0)),
inference(backward_demodulation,[status(thm)],[f7201,f6755]) ).
fof(f7201,plain,
sF1_fnc = inverse(inverse(sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f6918,f7178]) ).
fof(f7205,plain,
multiply(a1,sF1_fnc) = inverse(sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7221,f6517]) ).
fof(f7207,plain,
! [X0] : multiply(X0,sF0_fnc) = inverse(inverse(X0)),
inference(backward_demodulation,[status(thm)],[f7221,f5978]) ).
fof(f7212,plain,
! [X0] : multiply(multiply(a1,sF1_fnc),inverse(inverse(X0))) = inverse(inverse(multiply(sF0_fnc,X0))),
inference(backward_demodulation,[status(thm)],[f7221,f6995]) ).
fof(f7215,plain,
! [X0] : multiply(multiply(a1,sF1_fnc),inverse(multiply(inverse(sF1_fnc),inverse(multiply(sF0_fnc,multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f7221,f6806]) ).
fof(f7221,plain,
multiply(a1,sF1_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f6,f7179]) ).
fof(f7240,plain,
sF0_fnc = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7221,f7205]) ).
fof(f7242,plain,
b1 = inverse(multiply(sF3_fnc,sF0_fnc)),
inference(backward_demodulation,[status(thm)],[f7207,f6596]) ).
fof(f7243,plain,
! [X0] : multiply(inverse(inverse(X0)),sF0_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f7207,f6523]) ).
fof(f7245,plain,
! [X0] : multiply(a1,multiply(multiply(sF1_fnc,X0),sF0_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f7207,f6776]) ).
fof(f7246,plain,
! [X0] : multiply(a1,inverse(inverse(X0))) = multiply(multiply(inverse(sF1_fnc),X0),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f6735]) ).
fof(f7247,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(multiply(inverse(inverse(X0)),X1),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f6570]) ).
fof(f7248,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),sF0_fnc)) = X1,
inference(backward_demodulation,[status(thm)],[f7207,f6533]) ).
fof(f7275,plain,
! [X0,X1,X2] : multiply(multiply(inverse(inverse(X0)),X1),inverse(inverse(X2))) = multiply(multiply(multiply(X0,inverse(inverse(X1))),X2),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f6940]) ).
fof(f7280,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(inverse(X0)),X1)),inverse(inverse(X2))) = multiply(multiply(inverse(multiply(X0,inverse(inverse(X1)))),X2),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f6945]) ).
fof(f7303,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(multiply(X0,inverse(inverse(X1))),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f6573]) ).
fof(f7322,plain,
sF1_fnc = multiply(sF1_fnc,sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7207,f7201]) ).
fof(f7323,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),sF0_fnc),X1)) = inverse(inverse(X1)),
inference(backward_demodulation,[status(thm)],[f7207,f6965]) ).
fof(f7350,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),multiply(X1,multiply(X2,sF0_fnc))),inverse(X2))),
inference(backward_demodulation,[status(thm)],[f7207,f6632]) ).
fof(f7369,plain,
! [X0,X1,X2] : multiply(X0,sF0_fnc) = inverse(multiply(multiply(inverse(multiply(inverse(inverse(X1)),X0)),multiply(X1,multiply(X2,sF0_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f7207,f7350]) ).
fof(f7370,plain,
! [X0,X1,X2] : multiply(X0,sF0_fnc) = inverse(multiply(multiply(inverse(multiply(multiply(X1,sF0_fnc),X0)),multiply(X1,multiply(X2,sF0_fnc))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f7207,f7369]) ).
fof(f7376,plain,
! [X0,X1] : multiply(multiply(X0,sF0_fnc),X1) = multiply(multiply(X0,inverse(inverse(X1))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7303]) ).
fof(f7377,plain,
! [X0,X1] : multiply(multiply(X0,sF0_fnc),X1) = multiply(multiply(X0,multiply(X1,sF0_fnc)),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7376]) ).
fof(f7380,plain,
! [X0] : multiply(a1,multiply(X0,sF0_fnc)) = multiply(multiply(inverse(sF1_fnc),X0),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7246]) ).
fof(f7385,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1_fnc))),X0) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f7201,f7147]) ).
fof(f7404,plain,
! [X0] : multiply(inverse(multiply(X0,a1)),X0) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f7180,f7385]) ).
fof(f7406,plain,
! [X0] : multiply(a1,multiply(X0,sF0_fnc)) = multiply(multiply(a1,X0),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7180,f7380]) ).
fof(f7453,plain,
! [X0,X1] : multiply(X0,multiply(X1,sF0_fnc)) = multiply(multiply(inverse(inverse(X0)),X1),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7247]) ).
fof(f7454,plain,
! [X0,X1] : multiply(X0,multiply(X1,sF0_fnc)) = multiply(multiply(multiply(X0,sF0_fnc),X1),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7453]) ).
fof(f7459,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),sF0_fnc),X1)) = multiply(X1,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7323]) ).
fof(f7481,plain,
! [X0] : multiply(multiply(X0,sF0_fnc),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f7207,f7243]) ).
fof(f7494,plain,
! [X0] : multiply(sF0_fnc,inverse(multiply(inverse(sF1_fnc),inverse(multiply(sF0_fnc,multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f7221,f7215]) ).
fof(f7495,plain,
! [X0] : multiply(sF0_fnc,inverse(multiply(a1,inverse(multiply(sF0_fnc,multiply(inverse(inverse(X0)),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f7180,f7494]) ).
fof(f7496,plain,
! [X0] : multiply(sF0_fnc,inverse(multiply(a1,inverse(multiply(sF0_fnc,multiply(multiply(X0,sF0_fnc),a1)))))) = X0,
inference(forward_demodulation,[status(thm)],[f7207,f7495]) ).
fof(f7523,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),inverse(inverse(X2))) = multiply(multiply(inverse(multiply(X0,inverse(inverse(X1)))),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7280]) ).
fof(f7524,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),multiply(X2,sF0_fnc)) = multiply(multiply(inverse(multiply(X0,inverse(inverse(X1)))),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7523]) ).
fof(f7525,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),multiply(X2,sF0_fnc)) = multiply(multiply(inverse(multiply(X0,multiply(X1,sF0_fnc))),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7524]) ).
fof(f7532,plain,
! [X0,X1,X2] : multiply(multiply(multiply(X0,sF0_fnc),X1),inverse(inverse(X2))) = multiply(multiply(multiply(X0,inverse(inverse(X1))),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7275]) ).
fof(f7533,plain,
! [X0,X1,X2] : multiply(multiply(multiply(X0,sF0_fnc),X1),multiply(X2,sF0_fnc)) = multiply(multiply(multiply(X0,inverse(inverse(X1))),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7532]) ).
fof(f7534,plain,
! [X0,X1,X2] : multiply(multiply(multiply(X0,sF0_fnc),X1),multiply(X2,sF0_fnc)) = multiply(multiply(multiply(X0,multiply(X1,sF0_fnc)),X2),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7533]) ).
fof(f7611,plain,
! [X0] : multiply(sF0_fnc,inverse(inverse(X0))) = inverse(inverse(multiply(sF0_fnc,X0))),
inference(forward_demodulation,[status(thm)],[f7221,f7212]) ).
fof(f7612,plain,
! [X0] : multiply(sF0_fnc,multiply(X0,sF0_fnc)) = inverse(inverse(multiply(sF0_fnc,X0))),
inference(forward_demodulation,[status(thm)],[f7207,f7611]) ).
fof(f7615,plain,
! [X0] : multiply(sF0_fnc,multiply(X0,sF0_fnc)) = multiply(multiply(sF0_fnc,X0),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f7612]) ).
fof(f7621,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(a1,multiply(sF1_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f7207,f7189]) ).
fof(f7634,plain,
multiply(a1,multiply(sF1_fnc,sF0_fnc)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7322,f7245]) ).
fof(f7635,plain,
multiply(a1,multiply(sF0_fnc,sF0_fnc)) = a1,
inference(paramodulation,[status(thm)],[f6,f7245]) ).
fof(f7636,plain,
multiply(a1,sF0_fnc) = a1,
inference(backward_demodulation,[status(thm)],[f7637,f7635]) ).
fof(f7637,plain,
multiply(sF0_fnc,sF0_fnc) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f7621,f7634]) ).
fof(f7639,plain,
! [X0] : multiply(inverse(X0),sF0_fnc) = inverse(multiply(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f7207,f7207]) ).
fof(f7645,plain,
b1 = multiply(inverse(sF3_fnc),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f7639,f7242]) ).
fof(f7714,plain,
! [X0] : multiply(X0,inverse(X0)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7481,f7248]) ).
fof(f7740,plain,
! [X0,X1] : multiply(multiply(X0,sF0_fnc),multiply(X1,sF0_fnc)) = multiply(multiply(X0,X1),sF0_fnc),
inference(paramodulation,[status(thm)],[f7481,f7454]) ).
fof(f7766,plain,
! [X0] : multiply(inverse(X0),multiply(X0,sF0_fnc)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7207,f7714]) ).
fof(f7789,plain,
multiply(inverse(inverse(sF3_fnc)),b1) = sF0_fnc,
inference(paramodulation,[status(thm)],[f7645,f7766]) ).
fof(f7806,plain,
multiply(multiply(sF3_fnc,sF0_fnc),b1) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f7207,f7789]) ).
fof(f7924,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),sF0_fnc) = inverse(multiply(X0,multiply(X1,sF0_fnc))),
inference(paramodulation,[status(thm)],[f7454,f7639]) ).
fof(f7973,plain,
! [X0] : multiply(inverse(multiply(a1,X0)),sF0_fnc) = inverse(multiply(a1,multiply(X0,sF0_fnc))),
inference(paramodulation,[status(thm)],[f7406,f7639]) ).
fof(f8410,plain,
! [X0] : multiply(inverse(multiply(sF0_fnc,X0)),sF0_fnc) = inverse(multiply(sF0_fnc,multiply(X0,sF0_fnc))),
inference(paramodulation,[status(thm)],[f7615,f7639]) ).
fof(f8912,plain,
! [X0,X1] : multiply(inverse(multiply(X0,multiply(X1,sF0_fnc))),multiply(sF0_fnc,sF0_fnc)) = multiply(multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),multiply(sF0_fnc,sF0_fnc)),sF0_fnc),
inference(paramodulation,[status(thm)],[f7525,f7454]) ).
fof(f8940,plain,
! [X0,X1] : multiply(inverse(multiply(X0,multiply(X1,sF0_fnc))),sF0_fnc) = multiply(multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),multiply(sF0_fnc,sF0_fnc)),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7637,f8912]) ).
fof(f8941,plain,
! [X0,X1] : multiply(inverse(multiply(X0,multiply(X1,sF0_fnc))),sF0_fnc) = multiply(multiply(inverse(multiply(multiply(X0,sF0_fnc),X1)),sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7377,f8940]) ).
fof(f8942,plain,
! [X0,X1] : multiply(inverse(multiply(X0,multiply(X1,sF0_fnc))),sF0_fnc) = inverse(multiply(multiply(X0,sF0_fnc),X1)),
inference(forward_demodulation,[status(thm)],[f7481,f8941]) ).
fof(f10652,plain,
! [X0] : multiply(multiply(X0,sF0_fnc),a1) = multiply(multiply(X0,a1),sF0_fnc),
inference(paramodulation,[status(thm)],[f7636,f7740]) ).
fof(f10704,plain,
! [X0] : multiply(sF0_fnc,inverse(multiply(a1,inverse(multiply(sF0_fnc,multiply(multiply(X0,a1),sF0_fnc)))))) = X0,
inference(backward_demodulation,[status(thm)],[f10652,f7496]) ).
fof(f10716,plain,
! [X0] : multiply(sF0_fnc,inverse(multiply(a1,multiply(inverse(multiply(sF0_fnc,multiply(X0,a1))),sF0_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f8410,f10704]) ).
fof(f10717,plain,
! [X0] : multiply(sF0_fnc,multiply(inverse(multiply(a1,inverse(multiply(sF0_fnc,multiply(X0,a1))))),sF0_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f7973,f10716]) ).
fof(f11165,plain,
! [X0,X1] : multiply(X0,sF0_fnc) = inverse(multiply(multiply(inverse(multiply(multiply(X1,sF0_fnc),X0)),multiply(X1,multiply(sF0_fnc,sF0_fnc))),sF0_fnc)),
inference(paramodulation,[status(thm)],[f7240,f7370]) ).
fof(f11177,plain,
! [X0,X1] : multiply(X0,sF0_fnc) = multiply(inverse(multiply(inverse(multiply(multiply(X1,sF0_fnc),X0)),multiply(X1,multiply(sF0_fnc,sF0_fnc)))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7639,f11165]) ).
fof(f11178,plain,
! [X0,X1] : multiply(X0,sF0_fnc) = multiply(inverse(multiply(inverse(multiply(multiply(X1,sF0_fnc),X0)),multiply(X1,sF0_fnc))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7637,f11177]) ).
fof(f11179,plain,
! [X0,X1] : multiply(X0,sF0_fnc) = inverse(multiply(multiply(inverse(multiply(multiply(X1,sF0_fnc),X0)),sF0_fnc),X1)),
inference(forward_demodulation,[status(thm)],[f8942,f11178]) ).
fof(f11180,plain,
! [X0,X1] : multiply(X0,sF0_fnc) = inverse(multiply(inverse(multiply(X1,multiply(X0,sF0_fnc))),X1)),
inference(forward_demodulation,[status(thm)],[f7924,f11179]) ).
fof(f11632,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(inverse(inverse(multiply(sF0_fnc,multiply(X0,sF0_fnc)))),sF0_fnc),
inference(paramodulation,[status(thm)],[f7639,f11180]) ).
fof(f11645,plain,
! [X0] : multiply(X0,sF0_fnc) = inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(X0,sF0_fnc),a1)))),
inference(paramodulation,[status(thm)],[f7404,f11180]) ).
fof(f11650,plain,
! [X0] : multiply(multiply(inverse(X0),sF0_fnc),sF0_fnc) = inverse(multiply(inverse(multiply(sF0_fnc,sF0_fnc)),X0)),
inference(paramodulation,[status(thm)],[f7459,f11180]) ).
fof(f11736,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(multiply(multiply(sF0_fnc,multiply(X0,sF0_fnc)),sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7207,f11632]) ).
fof(f11737,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(multiply(multiply(sF0_fnc,sF0_fnc),X0),multiply(sF0_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f7534,f11736]) ).
fof(f11738,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(multiply(sF0_fnc,X0),multiply(sF0_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f7637,f11737]) ).
fof(f11739,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(multiply(sF0_fnc,X0),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7637,f11738]) ).
fof(f11742,plain,
! [X0] : multiply(inverse(multiply(a1,inverse(multiply(sF0_fnc,multiply(X0,a1))))),sF0_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f11763,f10717]) ).
fof(f11763,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(sF0_fnc,multiply(X0,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f7615,f11739]) ).
fof(f11841,plain,
! [X0] : inverse(X0) = inverse(multiply(inverse(multiply(sF0_fnc,sF0_fnc)),X0)),
inference(forward_demodulation,[status(thm)],[f7481,f11650]) ).
fof(f11842,plain,
! [X0] : inverse(X0) = inverse(multiply(multiply(inverse(sF0_fnc),sF0_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f7639,f11841]) ).
fof(f11843,plain,
! [X0] : inverse(X0) = inverse(multiply(multiply(sF0_fnc,sF0_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f7240,f11842]) ).
fof(f11866,plain,
! [X0] : inverse(X0) = inverse(multiply(sF0_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f7637,f11843]) ).
fof(f11873,plain,
! [X0] : multiply(inverse(multiply(a1,inverse(multiply(X0,a1)))),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f11866,f11742]) ).
fof(f11908,plain,
! [X0] : multiply(X0,sF0_fnc) = inverse(multiply(a1,inverse(multiply(multiply(X0,sF0_fnc),a1)))),
inference(forward_demodulation,[status(thm)],[f7180,f11645]) ).
fof(f11909,plain,
! [X0] : multiply(X0,sF0_fnc) = inverse(multiply(a1,inverse(multiply(multiply(X0,a1),sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f10652,f11908]) ).
fof(f11910,plain,
! [X0] : multiply(X0,sF0_fnc) = inverse(multiply(a1,multiply(inverse(multiply(X0,a1)),sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f7639,f11909]) ).
fof(f11911,plain,
! [X0] : multiply(X0,sF0_fnc) = multiply(inverse(multiply(a1,inverse(multiply(X0,a1)))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f7973,f11910]) ).
fof(f11939,plain,
multiply(sF3_fnc,b1) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f12339,f7806]) ).
fof(f12339,plain,
! [X0] : multiply(X0,sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f11873,f11911]) ).
fof(f12558,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f8,f11939]) ).
fof(f12559,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f12558,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP427-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:12:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 53.93/7.26 % Refutation found
% 53.93/7.26 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 53.93/7.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 29.50/8.51 % Elapsed time: 7.931765 seconds
% 29.50/8.51 % CPU time: 45.050170 seconds
% 29.50/8.51 % Total memory used: 680.112 MB
% 29.50/8.51 % Net memory used: 660.275 MB
%------------------------------------------------------------------------------