%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP428-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 : n009.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:34:01 PM UTC 2026
% Result : Unsatisfiable 8.35s 6.65s
% Output : CNFRefutation 6.54s
% 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(multiply(inverse(b2),b2),a2) != a2,
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(multiply(inverse(b2),b2),a2) != a2,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF2_fnc = inverse(b2),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f6,definition,
sF1_fnc = multiply(sF2_fnc,b2),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f7,definition,
sF0_fnc = multiply(sF1_fnc,a2),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f8,plain,
sF0_fnc != a2,
inference(definition_folding,[],[f4,f7,f6,f5]) ).
fof(f10,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(inverse(X0),X1))),X2),inverse(multiply(b2,X2))))) = X1,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f13,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),a2),inverse(sF0_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f14,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),multiply(inverse(X0),X1))),b2),inverse(sF1_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f16,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f13]) ).
fof(f17,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f3,f13]) ).
fof(f18,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),a2),inverse(sF0_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f5,f13]) ).
fof(f19,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))),a2),inverse(sF0_fnc)))))))) = X3,
inference(paramodulation,[status(thm)],[f13,f3]) ).
fof(f24,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)),a2),inverse(sF0_fnc))))))))) = X3,
inference(forward_demodulation,[status(thm)],[f16,f19]) ).
fof(f32,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),X2),inverse(multiply(b2,X2))))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f10]) ).
fof(f41,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),X2),inverse(multiply(b2,X2))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f16,f32]) ).
fof(f47,plain,
multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),a2),inverse(sF0_fnc)))) = b2,
inference(paramodulation,[status(thm)],[f6,f18]) ).
fof(f48,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(sF2_fnc),X0))),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f18]) ).
fof(f50,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f13,f14]) ).
fof(f56,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f16,f50]) ).
fof(f60,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X1)),b2),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f56,f13]) ).
fof(f67,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(sF2_fnc),X0)),b2),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f13,f60]) ).
fof(f95,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),X1),inverse(multiply(b2,X1))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),b2)),a2),inverse(sF0_fnc)))),
inference(paramodulation,[status(thm)],[f6,f41]) ).
fof(f97,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(sF2_fnc),X1))),a2),inverse(sF0_fnc))))),a2),inverse(sF0_fnc)))),
inference(paramodulation,[status(thm)],[f13,f41]) ).
fof(f103,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(sF2_fnc,X1)),X2),inverse(multiply(b2,X2)))),
inference(paramodulation,[status(thm)],[f41,f13]) ).
fof(f108,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f48,f97]) ).
fof(f116,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))) = inverse(multiply(multiply(inverse(multiply(sF2_fnc,X0)),X1),inverse(multiply(b2,X1)))),
inference(forward_demodulation,[status(thm)],[f13,f103]) ).
fof(f119,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),b2)),a2),inverse(sF0_fnc))) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(paramodulation,[status(thm)],[f6,f116]) ).
fof(f134,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))) = inverse(multiply(multiply(inverse(sF1_fnc),X1),inverse(multiply(b2,X1)))),
inference(paramodulation,[status(thm)],[f119,f119]) ).
fof(f148,plain,
! [X0] : inverse(multiply(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),a2),inverse(sF0_fnc)))),inverse(b2))) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(paramodulation,[status(thm)],[f47,f134]) ).
fof(f163,plain,
! [X0] : inverse(multiply(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),a2),inverse(sF0_fnc)))),sF2_fnc)) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f148]) ).
fof(f330,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f16,f13]) ).
fof(f353,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),inverse(multiply(multiply(inverse(sF1_fnc),X3),inverse(multiply(b2,X3))))),inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),b2)),a2),inverse(sF0_fnc))))))),
inference(paramodulation,[status(thm)],[f95,f17]) ).
fof(f368,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(inverse(X0))),X1))),a2),inverse(sF0_fnc))))),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f13,f17]) ).
fof(f403,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(forward_demodulation,[status(thm)],[f16,f368]) ).
fof(f406,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f13,f403]) ).
fof(f430,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))))) = X0,
inference(paramodulation,[status(thm)],[f5,f330]) ).
fof(f467,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))))) = b2,
inference(paramodulation,[status(thm)],[f95,f430]) ).
fof(f469,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))))) = multiply(inverse(inverse(X0)),X1),
inference(paramodulation,[status(thm)],[f16,f430]) ).
fof(f610,plain,
multiply(sF2_fnc,multiply(b2,b2)) = multiply(inverse(inverse(b2)),sF1_fnc),
inference(paramodulation,[status(thm)],[f47,f469]) ).
fof(f611,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(inverse(b2)),multiply(sF2_fnc,X0)),
inference(paramodulation,[status(thm)],[f18,f469]) ).
fof(f612,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),X1),inverse(multiply(b2,X1))))))) = multiply(inverse(inverse(X0)),b2),
inference(paramodulation,[status(thm)],[f95,f469]) ).
fof(f613,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(inverse(X1)),multiply(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f13,f469]) ).
fof(f614,plain,
! [X0,X1,X2] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X2)),a2),inverse(sF0_fnc))))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(paramodulation,[status(thm)],[f16,f469]) ).
fof(f624,plain,
multiply(sF2_fnc,multiply(b2,b2)) = multiply(inverse(sF2_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5,f610]) ).
fof(f625,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(sF2_fnc),multiply(sF2_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f5,f611]) ).
fof(f648,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,X0))),a2),inverse(sF0_fnc))) = inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f625,f67]) ).
fof(f662,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc)))) = X0,
inference(backward_demodulation,[status(thm)],[f648,f18]) ).
fof(f696,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(X0),X1))),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(b2,X1)))),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f613,f16]) ).
fof(f716,plain,
! [X0] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(sF2_fnc,multiply(b2,X0)))),a2),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f13,f696]) ).
fof(f718,plain,
! [X0] : X0 = inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,X0)))),b2),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f648,f716]) ).
fof(f736,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,X1)))),b2),inverse(sF1_fnc)))),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f718,f613]) ).
fof(f754,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f718,f736]) ).
fof(f769,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,X1))) = multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,X1))),
inference(paramodulation,[status(thm)],[f754,f754]) ).
fof(f771,plain,
multiply(sF2_fnc,multiply(b2,a2)) = multiply(inverse(sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f7,f754]) ).
fof(f840,plain,
multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),b2),inverse(sF1_fnc)))) = a2,
inference(paramodulation,[status(thm)],[f771,f662]) ).
fof(f843,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(paramodulation,[status(thm)],[f467,f662]) ).
fof(f844,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X0)),a2),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f430,f662]) ).
fof(f845,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,X0)),b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),b2),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f662,f662]) ).
fof(f863,plain,
! [X0] : multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(forward_demodulation,[status(thm)],[f5,f843]) ).
fof(f876,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))) = multiply(inverse(inverse(X0)),b2),
inference(backward_demodulation,[status(thm)],[f905,f612]) ).
fof(f884,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),b2)),a2),inverse(sF0_fnc))))))),
inference(backward_demodulation,[status(thm)],[f905,f353]) ).
fof(f903,plain,
inverse(multiply(multiply(inverse(sF1_fnc),inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF1_fnc)),a2),inverse(sF0_fnc)))),sF2_fnc)) = multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f905,f163]) ).
fof(f905,plain,
! [X0] : multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(sF1_fnc),X0),inverse(multiply(b2,X0)))),
inference(forward_demodulation,[status(thm)],[f6,f863]) ).
fof(f906,plain,
multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),b2),inverse(sF1_fnc))))) = b2,
inference(backward_demodulation,[status(thm)],[f844,f47]) ).
fof(f908,plain,
! [X0,X1] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(X0),X1)),b2),inverse(sF1_fnc))))) = X1,
inference(backward_demodulation,[status(thm)],[f844,f13]) ).
fof(f909,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))))) = multiply(inverse(inverse(X0)),X1),
inference(backward_demodulation,[status(thm)],[f844,f469]) ).
fof(f910,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))))) = X0,
inference(backward_demodulation,[status(thm)],[f844,f430]) ).
fof(f927,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),X1)),a2),inverse(sF0_fnc))))),b2),inverse(sF1_fnc))))),
inference(backward_demodulation,[status(thm)],[f844,f108]) ).
fof(f942,plain,
! [X0,X1,X2] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,multiply(b2,inverse(multiply(multiply(inverse(X2),b2),inverse(sF1_fnc)))))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(backward_demodulation,[status(thm)],[f844,f614]) ).
fof(f948,plain,
! [X0,X1,X2] : multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(backward_demodulation,[status(thm)],[f844,f406]) ).
fof(f959,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(multiply(inverse(X2),multiply(inverse(X0),X3)),multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))))))) = X3,
inference(backward_demodulation,[status(thm)],[f844,f24]) ).
fof(f1010,plain,
! [X0,X1,X2] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),b2)),a2),inverse(sF0_fnc))))))),
inference(forward_demodulation,[status(thm)],[f844,f884]) ).
fof(f1011,plain,
! [X0,X1,X2] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(X2,multiply(b2,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc)))))))),
inference(forward_demodulation,[status(thm)],[f844,f1010]) ).
fof(f1012,plain,
! [X0,X1,X2] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(X2,multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc)))))))),
inference(forward_demodulation,[status(thm)],[f5,f1011]) ).
fof(f1013,plain,
! [X0,X1,X2] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(X2,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))),
inference(forward_demodulation,[status(thm)],[f6,f1012]) ).
fof(f1014,plain,
! [X0,X1] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),multiply(inverse(inverse(X0)),X1))),a2),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f406,f1013]) ).
fof(f1015,plain,
! [X0,X1] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = multiply(b2,inverse(multiply(multiply(inverse(multiply(inverse(inverse(X0)),X1)),b2),inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f844,f1014]) ).
fof(f1098,plain,
inverse(multiply(multiply(inverse(sF1_fnc),multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),b2),inverse(sF1_fnc))))),sF2_fnc)) = multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f844,f903]) ).
fof(f1127,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc)))))),b2),inverse(sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f844,f927]) ).
fof(f1168,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(X0,b2),inverse(sF1_fnc)))))) = multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,X0)))),b2),inverse(sF1_fnc)),
inference(paramodulation,[status(thm)],[f718,f910]) ).
fof(f1172,plain,
! [X0] : X0 = inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(X0,b2),inverse(sF1_fnc))))))),
inference(backward_demodulation,[status(thm)],[f1168,f718]) ).
fof(f1268,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(X1,multiply(multiply(inverse(X1),multiply(inverse(X0),X2)),a2)))))) = X2,
inference(paramodulation,[status(thm)],[f840,f959]) ).
fof(f1305,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,a2))) = multiply(inverse(inverse(X0)),multiply(inverse(sF1_fnc),sF0_fnc)),
inference(paramodulation,[status(thm)],[f771,f769]) ).
fof(f1404,plain,
! [X0] : multiply(sF1_fnc,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(X0),multiply(multiply(sF2_fnc,multiply(b2,multiply(X0,a2))),a2)))))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f1305,f1268]) ).
fof(f1407,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(X0),multiply(multiply(sF2_fnc,multiply(b2,X1)),a2)))))) = X1,
inference(paramodulation,[status(thm)],[f754,f1268]) ).
fof(f1509,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(sF2_fnc,multiply(b2,a2)))))) = X0,
inference(paramodulation,[status(thm)],[f754,f1407]) ).
fof(f1527,plain,
! [X0,X1] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(multiply(sF2_fnc,multiply(b2,X1)),a2))))),
inference(paramodulation,[status(thm)],[f1407,f908]) ).
fof(f1530,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc))))) = X0,
inference(forward_demodulation,[status(thm)],[f771,f1509]) ).
fof(f1573,plain,
! [X0] : multiply(X0,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc))))) = multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))),
inference(paramodulation,[status(thm)],[f910,f1530]) ).
fof(f1583,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(sF1_fnc),sF0_fnc)))))) = multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),
inference(paramodulation,[status(thm)],[f1530,f754]) ).
fof(f1606,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(inverse(b2),b2),inverse(sF1_fnc))))) = multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),
inference(forward_demodulation,[status(thm)],[f1573,f1583]) ).
fof(f1607,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(multiply(sF2_fnc,b2),inverse(sF1_fnc))))) = multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),
inference(forward_demodulation,[status(thm)],[f5,f1606]) ).
fof(f1608,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),
inference(forward_demodulation,[status(thm)],[f6,f1607]) ).
fof(f1612,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(X0,multiply(b2,inverse(multiply(multiply(X0,b2),inverse(sF1_fnc))))),
inference(paramodulation,[status(thm)],[f1172,f1608]) ).
fof(f1622,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))) = multiply(inverse(inverse(X0)),multiply(inverse(multiply(sF2_fnc,multiply(b2,X1))),X1)),
inference(paramodulation,[status(thm)],[f1608,f769]) ).
fof(f1624,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0))) = multiply(inverse(inverse(sF2_fnc)),b2),
inference(paramodulation,[status(thm)],[f1608,f876]) ).
fof(f1626,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),multiply(b2,inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),b2),inverse(sF1_fnc))))) = X0,
inference(paramodulation,[status(thm)],[f1608,f908]) ).
fof(f1629,plain,
inverse(multiply(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),sF2_fnc)) = multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f1612,f1098]) ).
fof(f1636,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),b2),inverse(sF1_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f845,f1626]) ).
fof(f1637,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(multiply(sF1_fnc,inverse(sF1_fnc))),b2),inverse(sF1_fnc)))))))) = X0,
inference(forward_demodulation,[status(thm)],[f1168,f1636]) ).
fof(f1638,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f1172,f1637]) ).
fof(f1642,plain,
! [X0] : multiply(multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = inverse(multiply(sF1_fnc,inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f1608,f1638]) ).
fof(f1643,plain,
! [X0] : multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = multiply(b2,inverse(multiply(multiply(inverse(X0),b2),inverse(sF1_fnc)))),
inference(paramodulation,[status(thm)],[f910,f1638]) ).
fof(f1646,plain,
multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = a2,
inference(paramodulation,[status(thm)],[f771,f1638]) ).
fof(f1647,plain,
multiply(multiply(inverse(sF2_fnc),sF1_fnc),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = b2,
inference(paramodulation,[status(thm)],[f624,f1638]) ).
fof(f1656,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = X1,
inference(backward_demodulation,[status(thm)],[f1643,f908]) ).
fof(f1657,plain,
multiply(b2,multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = b2,
inference(backward_demodulation,[status(thm)],[f1643,f906]) ).
fof(f1658,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))) = X0,
inference(backward_demodulation,[status(thm)],[f1643,f910]) ).
fof(f1664,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,multiply(multiply(b2,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
inference(backward_demodulation,[status(thm)],[f1643,f1127]) ).
fof(f1671,plain,
! [X0,X1] : multiply(X0,multiply(b2,inverse(multiply(multiply(inverse(X1),b2),inverse(sF1_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f1643,f1015]) ).
fof(f1677,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(multiply(sF2_fnc,multiply(b2,X1)),a2))))),
inference(backward_demodulation,[status(thm)],[f1643,f1527]) ).
fof(f1701,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(backward_demodulation,[status(thm)],[f1643,f948]) ).
fof(f1707,plain,
! [X0,X1,X2] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,multiply(X2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(backward_demodulation,[status(thm)],[f1643,f942]) ).
fof(f1714,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))) = multiply(inverse(inverse(X0)),X1),
inference(backward_demodulation,[status(thm)],[f1643,f909]) ).
fof(f1735,plain,
! [X0,X1] : X0 = multiply(inverse(inverse(X0)),multiply(inverse(multiply(sF2_fnc,multiply(b2,X1))),X1)),
inference(backward_demodulation,[status(thm)],[f1658,f1622]) ).
fof(f1737,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(X1),X2),inverse(multiply(b2,X2))))) = multiply(X0,multiply(multiply(b2,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f1643,f1664]) ).
fof(f1745,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f1643,f1671]) ).
fof(f1781,plain,
multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),
inference(paramodulation,[status(thm)],[f1646,f754]) ).
fof(f1782,plain,
! [X0] : multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2) = multiply(inverse(multiply(sF2_fnc,multiply(b2,X0))),X0),
inference(backward_demodulation,[status(thm)],[f1781,f1608]) ).
fof(f1784,plain,
inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),sF2_fnc)) = multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(backward_demodulation,[status(thm)],[f1781,f1629]) ).
fof(f1788,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),
inference(backward_demodulation,[status(thm)],[f1782,f1735]) ).
fof(f1789,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(sF1_fnc,inverse(sF1_fnc)))) = inverse(multiply(sF1_fnc,inverse(sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f1782,f1642]) ).
fof(f1791,plain,
multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))) = multiply(inverse(inverse(sF2_fnc)),b2),
inference(backward_demodulation,[status(thm)],[f1782,f1624]) ).
fof(f1794,plain,
multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),b2),
inference(paramodulation,[status(thm)],[f1647,f754]) ).
fof(f1795,plain,
multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2) = multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),b2),
inference(forward_demodulation,[status(thm)],[f1781,f1794]) ).
fof(f1799,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(b2,inverse(multiply(multiply(X0,b2),inverse(sF1_fnc)))))) = multiply(inverse(X0),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),
inference(paramodulation,[status(thm)],[f1172,f1788]) ).
fof(f1802,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))) = multiply(inverse(inverse(inverse(X0))),X0),
inference(paramodulation,[status(thm)],[f1788,f754]) ).
fof(f1803,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
inference(backward_demodulation,[status(thm)],[f1799,f1172]) ).
fof(f1811,plain,
! [X0] : multiply(inverse(inverse(sF2_fnc)),b2) = multiply(inverse(inverse(inverse(X0))),X0),
inference(forward_demodulation,[status(thm)],[f1791,f1802]) ).
fof(f1812,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),
inference(paramodulation,[status(thm)],[f1788,f1811]) ).
fof(f1822,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(inverse(inverse(inverse(inverse(X0)))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(paramodulation,[status(thm)],[f1811,f754]) ).
fof(f1877,plain,
multiply(sF2_fnc,multiply(b2,multiply(inverse(inverse(sF2_fnc)),b2))) = inverse(inverse(inverse(inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(paramodulation,[status(thm)],[f1811,f1658]) ).
fof(f1887,plain,
! [X0] : multiply(inverse(X0),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)) = inverse(multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
inference(paramodulation,[status(thm)],[f1803,f1803]) ).
fof(f1889,plain,
b2 = inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
inference(paramodulation,[status(thm)],[f5,f1803]) ).
fof(f1897,plain,
! [X0] : X0 = inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))),
inference(backward_demodulation,[status(thm)],[f1887,f1788]) ).
fof(f1915,plain,
! [X0] : X0 = inverse(inverse(multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)))),
inference(forward_demodulation,[status(thm)],[f1887,f1897]) ).
fof(f1921,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,X0)) = multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),X0)),
inference(paramodulation,[status(thm)],[f1889,f754]) ).
fof(f1936,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(paramodulation,[status(thm)],[f1915,f769]) ).
fof(f1990,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))))) = multiply(inverse(inverse(inverse(X0))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(paramodulation,[status(thm)],[f1915,f1822]) ).
fof(f2076,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(inverse(inverse(sF2_fnc)),b2)))) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))),
inference(paramodulation,[status(thm)],[f1811,f1714]) ).
fof(f2218,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(b2,X1),inverse(multiply(b2,X1))))) = multiply(X0,multiply(multiply(b2,multiply(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
inference(paramodulation,[status(thm)],[f1889,f1737]) ).
fof(f2287,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(b2,X1),inverse(multiply(b2,X1))))) = multiply(X0,multiply(multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f1921,f2218]) ).
fof(f2288,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(b2,X1),inverse(multiply(b2,X1))))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f1638,f2287]) ).
fof(f2451,plain,
! [X0] : multiply(X0,inverse(multiply(b2,inverse(multiply(b2,multiply(sF1_fnc,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(paramodulation,[status(thm)],[f1657,f2288]) ).
fof(f2455,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(multiply(b2,multiply(multiply(inverse(b2),X1),inverse(multiply(sF1_fnc,inverse(sF1_fnc))))))))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(paramodulation,[status(thm)],[f1656,f2288]) ).
fof(f2469,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(multiply(b2,X1),inverse(multiply(b2,X1))))))) = multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(paramodulation,[status(thm)],[f2288,f769]) ).
fof(f2487,plain,
! [X0] : multiply(X0,inverse(multiply(b2,inverse(b2)))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f1657,f2451]) ).
fof(f2488,plain,
inverse(multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),sF2_fnc)) = multiply(b2,inverse(multiply(b2,sF2_fnc))),
inference(backward_demodulation,[status(thm)],[f2649,f1784]) ).
fof(f2492,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,X0)),inverse(multiply(b2,sF2_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f2649,f1638]) ).
fof(f2496,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),inverse(multiply(b2,sF2_fnc)))) = X1,
inference(backward_demodulation,[status(thm)],[f2649,f1656]) ).
fof(f2587,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(sF1_fnc,inverse(sF1_fnc))))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(b2,sF2_fnc))),
inference(backward_demodulation,[status(thm)],[f2649,f1745]) ).
fof(f2590,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(b2,sF2_fnc))) = inverse(multiply(sF1_fnc,inverse(sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f2649,f1789]) ).
fof(f2623,plain,
! [X0,X1,X2] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(X1,multiply(X2,inverse(multiply(b2,sF2_fnc))))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(backward_demodulation,[status(thm)],[f2649,f1707]) ).
fof(f2629,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(b2,sF2_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(backward_demodulation,[status(thm)],[f2649,f1701]) ).
fof(f2648,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(b2,sF2_fnc)))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(multiply(sF2_fnc,multiply(b2,X1)),a2))))),
inference(backward_demodulation,[status(thm)],[f2649,f1677]) ).
fof(f2649,plain,
! [X0] : multiply(X0,inverse(multiply(b2,sF2_fnc))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f5,f2487]) ).
fof(f2659,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))),
inference(forward_demodulation,[status(thm)],[f1656,f2455]) ).
fof(f2661,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = multiply(X0,inverse(multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f2649,f2659]) ).
fof(f2690,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))) = multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(forward_demodulation,[status(thm)],[f2288,f2469]) ).
fof(f2691,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(forward_demodulation,[status(thm)],[f1658,f2690]) ).
fof(f2692,plain,
! [X0] : X0 = multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(forward_demodulation,[status(thm)],[f769,f2691]) ).
fof(f2693,plain,
! [X0] : X0 = multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(multiply(b2,sF2_fnc))))),
inference(forward_demodulation,[status(thm)],[f2649,f2692]) ).
fof(f2788,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(b2,sF2_fnc)))) = multiply(multiply(inverse(inverse(X0)),X1),inverse(multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f2649,f2587]) ).
fof(f2847,plain,
inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))) = multiply(sF2_fnc,multiply(b2,multiply(inverse(inverse(sF2_fnc)),b2))),
inference(paramodulation,[status(thm)],[f1811,f2693]) ).
fof(f2854,plain,
inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))) = inverse(inverse(inverse(inverse(multiply(sF1_fnc,inverse(sF1_fnc)))))),
inference(backward_demodulation,[status(thm)],[f2847,f1877]) ).
fof(f2863,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(inverse(inverse(sF2_fnc)),b2)))) = multiply(inverse(inverse(X0)),inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc)))))),
inference(backward_demodulation,[status(thm)],[f2854,f2076]) ).
fof(f2932,plain,
! [X0] : multiply(multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc))) = inverse(multiply(X0,inverse(X0))),
inference(paramodulation,[status(thm)],[f2661,f2492]) ).
fof(f2944,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),inverse(multiply(b2,sF2_fnc))) = inverse(multiply(b2,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f2948,f2590]) ).
fof(f2948,plain,
! [X0] : inverse(multiply(b2,sF2_fnc)) = inverse(multiply(X0,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f2492,f2932]) ).
fof(f2966,plain,
! [X0] : inverse(multiply(b2,sF2_fnc)) = inverse(multiply(multiply(X0,inverse(X0)),inverse(multiply(b2,sF2_fnc)))),
inference(paramodulation,[status(thm)],[f2948,f2948]) ).
fof(f2969,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(X0)))) = multiply(inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(paramodulation,[status(thm)],[f2948,f1822]) ).
fof(f2970,plain,
! [X0] : multiply(inverse(inverse(sF2_fnc)),b2) = multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),multiply(X0,inverse(X0))),
inference(paramodulation,[status(thm)],[f2948,f1811]) ).
fof(f2979,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,inverse(X0)))) = multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f1822,f2969]) ).
fof(f2993,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(multiply(X0,inverse(X0)),inverse(multiply(b2,sF2_fnc))))) = multiply(inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(paramodulation,[status(thm)],[f2966,f1822]) ).
fof(f2999,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(forward_demodulation,[status(thm)],[f2693,f2993]) ).
fof(f3000,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f1822,f2999]) ).
fof(f3008,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),
inference(paramodulation,[status(thm)],[f1812,f3000]) ).
fof(f3009,plain,
multiply(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),b2) = multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),
inference(paramodulation,[status(thm)],[f1889,f3000]) ).
fof(f3012,plain,
! [X0] : multiply(X0,multiply(multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),inverse(multiply(b2,sF2_fnc)))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f3000,f2496]) ).
fof(f3013,plain,
multiply(sF2_fnc,multiply(b2,inverse(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))))) = multiply(b2,multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc)))),
inference(paramodulation,[status(thm)],[f3000,f1921]) ).
fof(f3014,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))))),
inference(paramodulation,[status(thm)],[f3000,f2693]) ).
fof(f3017,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(X0))) = multiply(inverse(X0),multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc)))),
inference(paramodulation,[status(thm)],[f3000,f754]) ).
fof(f3019,plain,
! [X0] : multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2) = multiply(inverse(multiply(X0,inverse(X0))),multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f3000,f1782]) ).
fof(f3020,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(b2,sF2_fnc)))) = multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))),
inference(paramodulation,[status(thm)],[f3000,f769]) ).
fof(f3037,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(backward_demodulation,[status(thm)],[f3045,f3000]) ).
fof(f3039,plain,
multiply(multiply(sF2_fnc,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2)),b2) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(backward_demodulation,[status(thm)],[f3045,f3009]) ).
fof(f3040,plain,
multiply(multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(backward_demodulation,[status(thm)],[f3045,f3008]) ).
fof(f3045,plain,
! [X0] : multiply(X0,multiply(b2,sF2_fnc)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f2492,f3012]) ).
fof(f3046,plain,
multiply(inverse(inverse(inverse(sF2_fnc))),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(b2,multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f1990,f3013]) ).
fof(f3047,plain,
multiply(sF2_fnc,multiply(b2,b2)) = multiply(b2,multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f754,f3046]) ).
fof(f3048,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = multiply(b2,multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f624,f3047]) ).
fof(f3049,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = multiply(b2,multiply(sF2_fnc,inverse(inverse(b2)))),
inference(forward_demodulation,[status(thm)],[f3045,f3048]) ).
fof(f3050,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = multiply(b2,multiply(sF2_fnc,inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f3049]) ).
fof(f3051,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,inverse(inverse(b2))))),
inference(forward_demodulation,[status(thm)],[f3045,f3014]) ).
fof(f3052,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,multiply(b2,multiply(sF2_fnc,inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f5,f3051]) ).
fof(f3053,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,multiply(b2,multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f2979,f3052]) ).
fof(f3054,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(forward_demodulation,[status(thm)],[f3045,f3053]) ).
fof(f3055,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = multiply(b2,multiply(b2,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f3056,f3050]) ).
fof(f3056,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f3054]) ).
fof(f3059,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(X0))) = multiply(inverse(X0),multiply(sF2_fnc,inverse(inverse(b2)))),
inference(forward_demodulation,[status(thm)],[f3045,f3017]) ).
fof(f3060,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(X0))) = multiply(inverse(X0),multiply(sF2_fnc,inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f3059]) ).
fof(f3061,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(X0))) = multiply(inverse(X0),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3056,f3060]) ).
fof(f3067,plain,
! [X0] : inverse(inverse(inverse(multiply(X0,multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2))))) = multiply(inverse(inverse(inverse(X0))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(backward_demodulation,[status(thm)],[f3068,f1990]) ).
fof(f3068,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,inverse(X0))) = inverse(inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f3045,f3061]) ).
fof(f3069,plain,
! [X0] : multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2) = inverse(inverse(inverse(multiply(X0,inverse(X0))))),
inference(forward_demodulation,[status(thm)],[f3045,f3019]) ).
fof(f3073,plain,
inverse(inverse(inverse(multiply(b2,sF2_fnc)))) = multiply(inverse(multiply(inverse(sF2_fnc),sF1_fnc)),b2),
inference(backward_demodulation,[status(thm)],[f3121,f1795]) ).
fof(f3074,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc))))),
inference(backward_demodulation,[status(thm)],[f3121,f1812]) ).
fof(f3075,plain,
! [X0] : X0 = inverse(inverse(multiply(X0,inverse(inverse(inverse(multiply(b2,sF2_fnc))))))),
inference(backward_demodulation,[status(thm)],[f3121,f1915]) ).
fof(f3077,plain,
multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),inverse(multiply(b2,sF2_fnc))) = inverse(multiply(b2,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f3121,f2944]) ).
fof(f3104,plain,
inverse(multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),sF2_fnc)) = multiply(b2,inverse(multiply(b2,sF2_fnc))),
inference(backward_demodulation,[status(thm)],[f3121,f2488]) ).
fof(f3112,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(multiply(X0,inverse(inverse(inverse(multiply(b2,sF2_fnc))))),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(backward_demodulation,[status(thm)],[f3121,f1936]) ).
fof(f3121,plain,
multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a2) = inverse(inverse(inverse(multiply(b2,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f2948,f3069]) ).
fof(f3122,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,inverse(inverse(X0)))) = multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3045,f3020]) ).
fof(f3123,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(inverse(inverse(inverse(inverse(multiply(b2,sF2_fnc)))))),
inference(backward_demodulation,[status(thm)],[f3124,f2970]) ).
fof(f3124,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3068,f3122]) ).
fof(f3152,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(sF2_fnc,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f3037]) ).
fof(f3162,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3056,f3152]) ).
fof(f3165,plain,
multiply(multiply(sF2_fnc,inverse(inverse(inverse(multiply(b2,sF2_fnc))))),b2) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(forward_demodulation,[status(thm)],[f3121,f3039]) ).
fof(f3166,plain,
multiply(multiply(sF2_fnc,inverse(inverse(inverse(multiply(b2,sF2_fnc))))),b2) = multiply(sF2_fnc,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f3165]) ).
fof(f3167,plain,
multiply(multiply(sF2_fnc,inverse(inverse(inverse(multiply(b2,sF2_fnc))))),b2) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3056,f3166]) ).
fof(f3168,plain,
multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(sF2_fnc,inverse(inverse(b2))),
inference(forward_demodulation,[status(thm)],[f3121,f3040]) ).
fof(f3169,plain,
multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(sF2_fnc,inverse(sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f3168]) ).
fof(f3170,plain,
multiply(inverse(inverse(inverse(multiply(b2,sF2_fnc)))),multiply(inverse(inverse(sF2_fnc)),b2)) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3056,f3169]) ).
fof(f3175,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = inverse(inverse(b2)),
inference(forward_demodulation,[status(thm)],[f3045,f3055]) ).
fof(f3183,plain,
multiply(inverse(sF2_fnc),sF1_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5,f3175]) ).
fof(f3185,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,X0)) = inverse(inverse(X0)),
inference(backward_demodulation,[status(thm)],[f3188,f1822]) ).
fof(f3186,plain,
inverse(multiply(b2,sF2_fnc)) = multiply(b2,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f3188,f3170]) ).
fof(f3188,plain,
! [X0] : inverse(X0) = multiply(inverse(inverse(inverse(X0))),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(forward_demodulation,[status(thm)],[f1915,f3067]) ).
fof(f3193,plain,
multiply(multiply(sF2_fnc,multiply(inverse(inverse(sF2_fnc)),b2)),b2) = multiply(b2,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f3201,f3167]) ).
fof(f3196,plain,
! [X0] : multiply(sF2_fnc,multiply(b2,multiply(X0,multiply(inverse(inverse(sF2_fnc)),b2)))) = multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(sF2_fnc)),b2))),
inference(backward_demodulation,[status(thm)],[f3201,f2863]) ).
fof(f3201,plain,
inverse(inverse(inverse(multiply(b2,sF2_fnc)))) = multiply(inverse(inverse(sF2_fnc)),b2),
inference(forward_demodulation,[status(thm)],[f3183,f3073]) ).
fof(f3205,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(multiply(inverse(inverse(sF2_fnc)),b2)),
inference(forward_demodulation,[status(thm)],[f3201,f3074]) ).
fof(f3206,plain,
! [X0] : X0 = inverse(inverse(multiply(X0,multiply(inverse(inverse(sF2_fnc)),b2)))),
inference(forward_demodulation,[status(thm)],[f3201,f3075]) ).
fof(f3208,plain,
multiply(multiply(inverse(inverse(sF2_fnc)),b2),inverse(multiply(b2,sF2_fnc))) = inverse(multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3201,f3077]) ).
fof(f3209,plain,
multiply(sF2_fnc,multiply(b2,inverse(multiply(b2,sF2_fnc)))) = inverse(multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f2788,f3208]) ).
fof(f3211,plain,
inverse(inverse(inverse(multiply(b2,sF2_fnc)))) = inverse(multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3068,f3209]) ).
fof(f3245,plain,
inverse(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)) = multiply(b2,inverse(multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f3211,f3104]) ).
fof(f3265,plain,
! [X0,X1] : multiply(sF2_fnc,multiply(b2,multiply(multiply(X0,inverse(multiply(b2,sF2_fnc))),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(forward_demodulation,[status(thm)],[f3211,f3112]) ).
fof(f3279,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(inverse(inverse(multiply(b2,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f3211,f3123]) ).
fof(f3301,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = inverse(multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3211,f3279]) ).
fof(f3318,plain,
inverse(inverse(a2)) = multiply(inverse(sF1_fnc),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f3185,f771]) ).
fof(f3322,plain,
! [X0,X1] : inverse(inverse(multiply(X0,X1))) = multiply(inverse(inverse(X0)),multiply(sF2_fnc,multiply(b2,X1))),
inference(backward_demodulation,[status(thm)],[f3185,f769]) ).
fof(f3324,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(inverse(X1),multiply(X1,X0)),
inference(backward_demodulation,[status(thm)],[f3185,f754]) ).
fof(f3333,plain,
! [X0,X1] : inverse(inverse(multiply(multiply(X0,inverse(multiply(b2,sF2_fnc))),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(backward_demodulation,[status(thm)],[f3185,f3265]) ).
fof(f3338,plain,
! [X0] : multiply(sF1_fnc,inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(X0,a2))),a2)))))) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f3185,f1404]) ).
fof(f3342,plain,
! [X0,X1,X2] : inverse(inverse(multiply(X0,multiply(X1,multiply(X2,inverse(multiply(b2,sF2_fnc))))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(backward_demodulation,[status(thm)],[f3185,f2623]) ).
fof(f3355,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(multiply(b2,sF2_fnc)))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),a2))))),
inference(backward_demodulation,[status(thm)],[f3185,f2648]) ).
fof(f3375,plain,
! [X0,X1] : multiply(X0,multiply(multiply(inverse(X0),X1),multiply(b2,sF2_fnc))) = X1,
inference(backward_demodulation,[status(thm)],[f3186,f2496]) ).
fof(f3387,plain,
inverse(multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc)) = multiply(b2,multiply(b2,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f3186,f3245]) ).
fof(f3417,plain,
! [X0,X1,X2] : multiply(X0,multiply(b2,sF2_fnc)) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(backward_demodulation,[status(thm)],[f3186,f2629]) ).
fof(f3486,plain,
multiply(multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc))),b2) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3301,f3193]) ).
fof(f3487,plain,
multiply(multiply(sF2_fnc,multiply(b2,sF2_fnc)),b2) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3186,f3486]) ).
fof(f3488,plain,
multiply(inverse(inverse(sF2_fnc)),b2) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3185,f3487]) ).
fof(f3493,plain,
! [X0] : inverse(inverse(multiply(X0,multiply(inverse(inverse(sF2_fnc)),b2)))) = multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(sF2_fnc)),b2))),
inference(forward_demodulation,[status(thm)],[f3185,f3196]) ).
fof(f3494,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),inverse(multiply(inverse(inverse(sF2_fnc)),b2))),
inference(forward_demodulation,[status(thm)],[f3206,f3493]) ).
fof(f3495,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),multiply(inverse(inverse(sF2_fnc)),b2)),
inference(forward_demodulation,[status(thm)],[f3205,f3494]) ).
fof(f3496,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3488,f3495]) ).
fof(f3497,plain,
! [X0] : X0 = inverse(inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f3045,f3496]) ).
fof(f3715,plain,
! [X0,X1] : inverse(inverse(multiply(X0,X1))) = multiply(inverse(inverse(X0)),inverse(inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3185,f3322]) ).
fof(f3755,plain,
! [X0,X1] : inverse(inverse(multiply(multiply(X0,multiply(b2,sF2_fnc)),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(forward_demodulation,[status(thm)],[f3186,f3333]) ).
fof(f3756,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(inverse(X0)),X1))) = multiply(X0,multiply(sF2_fnc,multiply(b2,X1))),
inference(forward_demodulation,[status(thm)],[f3045,f3755]) ).
fof(f3758,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(inverse(X0)),X1))) = multiply(X0,inverse(inverse(X1))),
inference(forward_demodulation,[status(thm)],[f3185,f3756]) ).
fof(f3768,plain,
! [X0] : multiply(sF1_fnc,inverse(multiply(inverse(inverse(a2)),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(X0,a2))),a2)))))) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f3318,f3338]) ).
fof(f3776,plain,
! [X0,X1,X2] : inverse(inverse(multiply(X0,multiply(X1,multiply(X2,multiply(b2,sF2_fnc)))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(forward_demodulation,[status(thm)],[f3186,f3342]) ).
fof(f3777,plain,
! [X0,X1,X2] : inverse(inverse(multiply(X0,multiply(X1,inverse(inverse(X2)))))) = multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),X2)),
inference(forward_demodulation,[status(thm)],[f3045,f3776]) ).
fof(f3814,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(b2,sF2_fnc))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),a2))))),
inference(forward_demodulation,[status(thm)],[f3186,f3355]) ).
fof(f3815,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(multiply(inverse(sF1_fnc),sF0_fnc),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),a2))))),
inference(forward_demodulation,[status(thm)],[f3045,f3814]) ).
fof(f3816,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(inverse(inverse(a2)),inverse(multiply(inverse(inverse(X0)),multiply(inverse(inverse(X1)),a2))))),
inference(forward_demodulation,[status(thm)],[f3318,f3815]) ).
fof(f3817,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(inverse(inverse(a2)),inverse(inverse(inverse(multiply(X0,multiply(X1,inverse(inverse(a2))))))))),
inference(forward_demodulation,[status(thm)],[f3777,f3816]) ).
fof(f3818,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(inverse(inverse(multiply(a2,inverse(multiply(X0,multiply(X1,inverse(inverse(a2))))))))),
inference(forward_demodulation,[status(thm)],[f3715,f3817]) ).
fof(f3887,plain,
! [X0,X1] : multiply(X0,inverse(inverse(multiply(inverse(X0),X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f3045,f3375]) ).
fof(f3903,plain,
inverse(multiply(multiply(b2,sF2_fnc),sF2_fnc)) = multiply(b2,multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f3186,f3387]) ).
fof(f3904,plain,
inverse(multiply(multiply(b2,sF2_fnc),sF2_fnc)) = inverse(inverse(b2)),
inference(forward_demodulation,[status(thm)],[f3045,f3903]) ).
fof(f3905,plain,
inverse(multiply(multiply(b2,sF2_fnc),sF2_fnc)) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5,f3904]) ).
fof(f4017,plain,
! [X0,X1,X2] : inverse(inverse(X0)) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f3045,f3417]) ).
fof(f4415,plain,
multiply(multiply(b2,sF2_fnc),sF2_fnc) = inverse(inverse(inverse(inverse(sF2_fnc)))),
inference(paramodulation,[status(thm)],[f3905,f3497]) ).
fof(f4424,plain,
multiply(multiply(b2,sF2_fnc),sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f3497,f4415]) ).
fof(f4426,plain,
inverse(inverse(sF2_fnc)) = multiply(inverse(multiply(b2,sF2_fnc)),sF2_fnc),
inference(paramodulation,[status(thm)],[f4424,f3324]) ).
fof(f4427,plain,
inverse(inverse(sF2_fnc)) = multiply(multiply(b2,sF2_fnc),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f3186,f4426]) ).
fof(f4428,plain,
multiply(sF2_fnc,b2) = multiply(b2,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f4437,f3488]) ).
fof(f4437,plain,
inverse(inverse(sF2_fnc)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f4424,f4427]) ).
fof(f4439,plain,
inverse(multiply(b2,sF2_fnc)) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f4454,f3186]) ).
fof(f4441,plain,
! [X0] : multiply(X0,inverse(X0)) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f4454,f3162]) ).
fof(f4454,plain,
sF1_fnc = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f6,f4428]) ).
fof(f4512,plain,
inverse(sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f4454,f4439]) ).
fof(f5373,plain,
! [X0,X1] : inverse(inverse(X0)) = inverse(multiply(sF1_fnc,inverse(multiply(X1,inverse(inverse(multiply(inverse(X1),X0))))))),
inference(paramodulation,[status(thm)],[f4441,f4017]) ).
fof(f5416,plain,
! [X0] : inverse(inverse(X0)) = inverse(multiply(sF1_fnc,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f3887,f5373]) ).
fof(f5620,plain,
! [X0] : inverse(inverse(inverse(multiply(inverse(sF1_fnc),X0)))) = inverse(X0),
inference(paramodulation,[status(thm)],[f3887,f5416]) ).
fof(f5627,plain,
! [X0] : inverse(inverse(inverse(inverse(inverse(X0))))) = inverse(multiply(sF1_fnc,X0)),
inference(paramodulation,[status(thm)],[f3497,f5416]) ).
fof(f5633,plain,
! [X0,X1] : multiply(multiply(sF1_fnc,inverse(X0)),inverse(inverse(multiply(inverse(inverse(X0)),X1)))) = X1,
inference(paramodulation,[status(thm)],[f5416,f3887]) ).
fof(f5634,plain,
! [X0] : multiply(sF1_fnc,inverse(X0)) = inverse(inverse(inverse(inverse(inverse(X0))))),
inference(paramodulation,[status(thm)],[f5416,f3497]) ).
fof(f5635,plain,
! [X0] : inverse(inverse(inverse(multiply(sF1_fnc,X0)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f4512,f5620]) ).
fof(f5657,plain,
! [X0] : inverse(inverse(inverse(X0))) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f5668,f5635]) ).
fof(f5668,plain,
! [X0] : inverse(X0) = inverse(multiply(sF1_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f3497,f5627]) ).
fof(f5674,plain,
! [X0,X1] : multiply(multiply(sF1_fnc,inverse(X0)),multiply(X0,inverse(inverse(X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f3758,f5633]) ).
fof(f5676,plain,
! [X0] : inverse(multiply(inverse(inverse(a2)),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(X0,a2))),a2))))) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f5683,f3768]) ).
fof(f5678,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(inverse(X1)))) = X1,
inference(backward_demodulation,[status(thm)],[f5683,f5674]) ).
fof(f5683,plain,
! [X0] : multiply(sF1_fnc,inverse(X0)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f3497,f5634]) ).
fof(f5689,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = inverse(multiply(a2,inverse(multiply(X0,multiply(X1,inverse(inverse(a2))))))),
inference(backward_demodulation,[status(thm)],[f5657,f3818]) ).
fof(f5720,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f3324,f5678]) ).
fof(f5728,plain,
! [X0] : inverse(multiply(a2,inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(X0,a2))),a2))))) = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f5805,f5676]) ).
fof(f5805,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f5657,f5720]) ).
fof(f5814,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(a2,inverse(multiply(X0,multiply(X1,inverse(inverse(a2))))))),
inference(forward_demodulation,[status(thm)],[f5805,f5689]) ).
fof(f5815,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(a2,inverse(multiply(X0,multiply(X1,a2))))),
inference(forward_demodulation,[status(thm)],[f5805,f5814]) ).
fof(f5869,plain,
! [X0] : multiply(inverse(X0),inverse(inverse(multiply(X0,a2)))) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5815,f5728]) ).
fof(f5870,plain,
! [X0] : multiply(inverse(X0),multiply(X0,a2)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5805,f5869]) ).
fof(f5871,plain,
inverse(inverse(a2)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f3324,f5870]) ).
fof(f5872,plain,
a2 = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f5805,f5871]) ).
fof(f5873,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5872,f8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP428-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.41 % Computer : n009.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Sun Sep 20 20:13:02 UTC 2026
% 0.14/5.42 % CPUTime :
% 0.14/5.42 % Drodi V4.1.1
% 8.35/6.65 % Refutation found
% 8.35/6.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 8.35/6.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.54/6.73 % Elapsed time: 1.291472 seconds
% 6.54/6.73 % CPU time: 9.755989 seconds
% 6.54/6.73 % Total memory used: 172.794 MB
% 6.54/6.73 % Net memory used: 165.957 MB
%------------------------------------------------------------------------------