%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP430-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 : n007.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:11 PM UTC 2026
% Result : Unsatisfiable 6.59s 1.50s
% Output : CNFRefutation 6.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 6
% Syntax : Number of formulae : 210 ( 210 unt; 4 def)
% Number of atoms : 210 ( 209 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 396 ( 396 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : multiply(A,inverse(multiply(B,multiply(multiply(multiply(C,inverse(C)),inverse(multiply(D,B))),A)))) = D,
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(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),X0)))) = X3,
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(f10,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X5)))))),inverse(multiply(X5,X2))) = X4,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(X4,inverse(X4))),multiply(X2,X0)))) = X3,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f12,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),X0)))) = X2,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f13,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(X2,X1))),X0)))) = X2,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f36,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X3)))))),inverse(multiply(X3,X1))) = X2,
inference(paramodulation,[status(thm)],[f12,f12]) ).
fof(f38,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),multiply(b1,sF3_fnc)),multiply(X1,X0)))) = X2,
inference(paramodulation,[status(thm)],[f12,f12]) ).
fof(f41,plain,
! [X0] : multiply(X0,inverse(multiply(b1,multiply(multiply(multiply(b1,sF3_fnc),inverse(sF2_fnc)),X0)))) = sF3_fnc,
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f42,plain,
! [X0] : multiply(X0,inverse(multiply(a1,multiply(multiply(multiply(b1,sF3_fnc),inverse(sF0_fnc)),X0)))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f6,f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),X3))),multiply(multiply(multiply(b1,sF3_fnc),inverse(X2)),X0)))) = X3,
inference(paramodulation,[status(thm)],[f12,f12]) ).
fof(f46,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X4))),multiply(X5,inverse(X5))),X2))) = X4,
inference(paramodulation,[status(thm)],[f12,f10]) ).
fof(f131,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),sF3_fnc))),inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(sF2_fnc)),multiply(X3,inverse(X3))),X2))) = b1,
inference(paramodulation,[status(thm)],[f41,f10]) ).
fof(f155,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),sF1_fnc))),inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(sF0_fnc)),multiply(X3,inverse(X3))),X2))) = a1,
inference(paramodulation,[status(thm)],[f42,f10]) ).
fof(f174,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(X2)),multiply(X3,inverse(X3))),multiply(inverse(multiply(X4,multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X6,X4))),multiply(multiply(X7,inverse(X7)),inverse(multiply(X2,X8)))))),X0)))) = inverse(multiply(X8,X6)),
inference(paramodulation,[status(thm)],[f10,f11]) ).
fof(f364,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1))),multiply(b1,sF3_fnc)),X0)))) = multiply(X3,multiply(X4,inverse(X4))),
inference(paramodulation,[status(thm)],[f38,f11]) ).
fof(f365,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X0))),X3))),inverse(multiply(multiply(X4,multiply(X5,inverse(X5))),X2))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X4,X3))),multiply(b1,sF3_fnc)),
inference(paramodulation,[status(thm)],[f38,f10]) ).
fof(f367,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(X3,X0)))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X3))),multiply(b1,sF3_fnc)),
inference(paramodulation,[status(thm)],[f38,f3]) ).
fof(f377,plain,
multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(sF0_fnc)),sF1_fnc))),multiply(b1,sF3_fnc)) = a1,
inference(backward_demodulation,[status(thm)],[f365,f155]) ).
fof(f380,plain,
multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(sF2_fnc)),sF3_fnc))),multiply(b1,sF3_fnc)) = b1,
inference(backward_demodulation,[status(thm)],[f365,f131]) ).
fof(f383,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))),X0))),multiply(b1,sF3_fnc)) = X1,
inference(backward_demodulation,[status(thm)],[f365,f46]) ).
fof(f403,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X2))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X1,X6))))))))),multiply(b1,sF3_fnc)) = inverse(multiply(X6,X4)),
inference(backward_demodulation,[status(thm)],[f367,f174]) ).
fof(f408,plain,
! [X0,X1,X2] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),multiply(b1,sF3_fnc))))),multiply(b1,sF3_fnc)) = multiply(X1,multiply(X2,inverse(X2))),
inference(backward_demodulation,[status(thm)],[f367,f364]) ).
fof(f469,plain,
! [X0,X1] : multiply(X0,multiply(b1,sF3_fnc)) = multiply(X0,multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f12,f408]) ).
fof(f498,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(b1,sF3_fnc)))),multiply(b1,sF3_fnc)),multiply(X1,X0)))) = multiply(X2,inverse(X2)),
inference(paramodulation,[status(thm)],[f469,f38]) ).
fof(f538,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(X1)),inverse(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X2))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X5))))))))),multiply(b1,sF3_fnc)) = inverse(multiply(X5,X4)),
inference(backward_demodulation,[status(thm)],[f605,f403]) ).
fof(f605,plain,
! [X0] : multiply(b1,sF3_fnc) = multiply(X0,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f38,f498]) ).
fof(f623,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),inverse(multiply(X1,multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X4))))))))),multiply(b1,sF3_fnc)) = inverse(multiply(X4,X3)),
inference(forward_demodulation,[status(thm)],[f605,f538]) ).
fof(f624,plain,
! [X0,X1,X2,X3] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X3))))))))),multiply(b1,sF3_fnc)) = inverse(multiply(X3,X2)),
inference(forward_demodulation,[status(thm)],[f605,f623]) ).
fof(f676,plain,
multiply(b1,sF3_fnc) = multiply(a1,sF1_fnc),
inference(paramodulation,[status(thm)],[f5,f605]) ).
fof(f677,plain,
! [X0] : multiply(X0,inverse(multiply(sF1_fnc,multiply(multiply(b1,sF3_fnc),X0)))) = a1,
inference(paramodulation,[status(thm)],[f605,f13]) ).
fof(f678,plain,
! [X0] : multiply(X0,inverse(multiply(sF3_fnc,multiply(multiply(b1,sF3_fnc),X0)))) = b1,
inference(paramodulation,[status(thm)],[f605,f12]) ).
fof(f683,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(multiply(a1,sF1_fnc),inverse(multiply(b1,sF3_fnc))),X0)))) = X1,
inference(paramodulation,[status(thm)],[f605,f13]) ).
fof(f728,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,sF3_fnc))),X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f676,f683]) ).
fof(f729,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f605,f728]) ).
fof(f803,plain,
multiply(inverse(multiply(b1,sF3_fnc)),inverse(multiply(sF3_fnc,multiply(b1,sF3_fnc)))) = b1,
inference(paramodulation,[status(thm)],[f605,f678]) ).
fof(f829,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),inverse(multiply(inverse(X0),multiply(b1,sF3_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f605,f729]) ).
fof(f832,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)),multiply(X1,X0)))) = inverse(X1),
inference(paramodulation,[status(thm)],[f729,f12]) ).
fof(f870,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(multiply(multiply(b1,sF3_fnc),inverse(X3)),X0)))) = inverse(multiply(inverse(X2),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1)))))),
inference(paramodulation,[status(thm)],[f729,f43]) ).
fof(f878,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(multiply(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)),multiply(X1,X2))),multiply(multiply(multiply(b1,sF3_fnc),inverse(inverse(X1))),X0)))) = X2,
inference(paramodulation,[status(thm)],[f729,f43]) ).
fof(f915,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X1))),X2))),multiply(multiply(b1,sF3_fnc),X0)))) = X2,
inference(paramodulation,[status(thm)],[f605,f43]) ).
fof(f944,plain,
! [X0,X1] : multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f729,f915]) ).
fof(f949,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0)))))),
inference(paramodulation,[status(thm)],[f729,f944]) ).
fof(f955,plain,
! [X0] : multiply(X0,multiply(b1,sF3_fnc)) = inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0)))),
inference(paramodulation,[status(thm)],[f605,f944]) ).
fof(f965,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,sF3_fnc))),X0)) = X0,
inference(paramodulation,[status(thm)],[f605,f944]) ).
fof(f966,plain,
! [X0,X1] : multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),X0),inverse(multiply(inverse(X1),X0))) = X1,
inference(paramodulation,[status(thm)],[f944,f729]) ).
fof(f967,plain,
! [X0] : multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),X0),inverse(multiply(sF3_fnc,X0))) = b1,
inference(paramodulation,[status(thm)],[f944,f678]) ).
fof(f968,plain,
! [X0] : multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),X0),inverse(multiply(sF1_fnc,X0))) = a1,
inference(paramodulation,[status(thm)],[f944,f677]) ).
fof(f984,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),multiply(multiply(b1,sF3_fnc),X0)) = X0,
inference(forward_demodulation,[status(thm)],[f605,f965]) ).
fof(f986,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),X0) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),X0),
inference(paramodulation,[status(thm)],[f944,f984]) ).
fof(f988,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),X0) = inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),
inference(paramodulation,[status(thm)],[f729,f984]) ).
fof(f1001,plain,
! [X0] : multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),inverse(multiply(sF1_fnc,X0))) = a1,
inference(backward_demodulation,[status(thm)],[f986,f968]) ).
fof(f1002,plain,
! [X0] : multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),inverse(multiply(sF3_fnc,X0))) = b1,
inference(backward_demodulation,[status(thm)],[f986,f967]) ).
fof(f1003,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),inverse(multiply(inverse(X1),X0))) = X1,
inference(backward_demodulation,[status(thm)],[f986,f966]) ).
fof(f1153,plain,
! [X0] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),inverse(multiply(b1,sF3_fnc))))),multiply(b1,sF3_fnc)) = multiply(multiply(b1,sF3_fnc),X0),
inference(paramodulation,[status(thm)],[f984,f383]) ).
fof(f1154,plain,
! [X0] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),inverse(multiply(b1,sF3_fnc))))),multiply(b1,sF3_fnc)) = inverse(multiply(inverse(X0),multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f829,f383]) ).
fof(f1155,plain,
multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(b1)),inverse(multiply(b1,sF3_fnc))))),multiply(b1,sF3_fnc)) = inverse(multiply(sF3_fnc,multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f803,f383]) ).
fof(f1161,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),X1))),multiply(b1,sF3_fnc)) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X1))),X0),
inference(paramodulation,[status(thm)],[f944,f383]) ).
fof(f1163,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),X1))),multiply(b1,sF3_fnc)) = inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X1))),
inference(paramodulation,[status(thm)],[f729,f383]) ).
fof(f1168,plain,
! [X0,X1,X2] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(X0)),X1))),multiply(b1,sF3_fnc)) = inverse(multiply(X2,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X2))),X1))),
inference(paramodulation,[status(thm)],[f12,f383]) ).
fof(f1174,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X3))),X2))))))))),inverse(X3)) = X1,
inference(paramodulation,[status(thm)],[f383,f36]) ).
fof(f1195,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),X0) = inverse(multiply(inverse(X0),multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f1153,f1154]) ).
fof(f1202,plain,
multiply(multiply(b1,sF3_fnc),b1) = inverse(multiply(sF3_fnc,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f1153,f1155]) ).
fof(f1212,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))),multiply(X0,X1)) = X1,
inference(backward_demodulation,[status(thm)],[f1161,f383]) ).
fof(f1215,plain,
multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),sF3_fnc))),sF2_fnc) = b1,
inference(backward_demodulation,[status(thm)],[f1161,f380]) ).
fof(f1216,plain,
multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),sF1_fnc))),sF0_fnc) = a1,
inference(backward_demodulation,[status(thm)],[f1161,f377]) ).
fof(f1222,plain,
! [X0,X1,X2,X3] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X3))))))))),X2) = inverse(multiply(X3,X1)),
inference(backward_demodulation,[status(thm)],[f1161,f624]) ).
fof(f1264,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))),X1) = inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f1161,f1163]) ).
fof(f1269,plain,
! [X0,X1,X2] : multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))),X1) = inverse(multiply(X2,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X0))),
inference(forward_demodulation,[status(thm)],[f1161,f1168]) ).
fof(f1329,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X1))) = inverse(multiply(X2,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X2))),X1))),
inference(forward_demodulation,[status(thm)],[f1264,f1269]) ).
fof(f1333,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X1))))))))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f1329,f1174]) ).
fof(f1334,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X1))))))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f984,f1333]) ).
fof(f1338,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(b1,sF3_fnc),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f1264,f1212]) ).
fof(f1373,plain,
inverse(multiply(inverse(sF2_fnc),multiply(multiply(b1,sF3_fnc),sF3_fnc))) = b1,
inference(forward_demodulation,[status(thm)],[f1264,f1215]) ).
fof(f1374,plain,
inverse(multiply(inverse(sF0_fnc),multiply(multiply(b1,sF3_fnc),sF1_fnc))) = a1,
inference(forward_demodulation,[status(thm)],[f1264,f1216]) ).
fof(f1378,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X1))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X3))))))))) = inverse(multiply(X3,X2)),
inference(forward_demodulation,[status(thm)],[f1264,f1222]) ).
fof(f1379,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X2))))))))) = inverse(multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f1329,f1378]) ).
fof(f1462,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)))),X1)),X0)) = X1,
inference(paramodulation,[status(thm)],[f729,f1338]) ).
fof(f1465,plain,
! [X0] : inverse(multiply(inverse(multiply(inverse(multiply(b1,sF3_fnc)),X0)),multiply(b1,sF3_fnc))) = X0,
inference(paramodulation,[status(thm)],[f605,f1338]) ).
fof(f1477,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),X1)),X0)) = X1,
inference(forward_demodulation,[status(thm)],[f988,f1462]) ).
fof(f1482,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(b1,sF3_fnc)),X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1195,f1465]) ).
fof(f1486,plain,
multiply(b1,sF3_fnc) = multiply(multiply(inverse(sF2_fnc),multiply(multiply(b1,sF3_fnc),sF3_fnc)),b1),
inference(paramodulation,[status(thm)],[f1373,f605]) ).
fof(f1490,plain,
multiply(b1,sF3_fnc) = multiply(multiply(inverse(sF0_fnc),multiply(multiply(b1,sF3_fnc),sF1_fnc)),a1),
inference(paramodulation,[status(thm)],[f1374,f605]) ).
fof(f1495,plain,
multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)) = inverse(inverse(multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f605,f1482]) ).
fof(f1509,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X1,X2))),multiply(multiply(multiply(b1,sF3_fnc),inverse(inverse(X1))),X0)))) = X2,
inference(backward_demodulation,[status(thm)],[f1495,f878]) ).
fof(f1510,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X1,X0)))) = inverse(X1),
inference(backward_demodulation,[status(thm)],[f1495,f832]) ).
fof(f1569,plain,
! [X0,X1] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))))))) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f984,f1379]) ).
fof(f1577,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(X0)),multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0)))))) = inverse(multiply(multiply(multiply(b1,sF3_fnc),multiply(b1,sF3_fnc)),X1)),
inference(paramodulation,[status(thm)],[f729,f1379]) ).
fof(f1596,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(X2)))))))) = inverse(multiply(inverse(multiply(inverse(X2),multiply(multiply(b1,sF3_fnc),X0))),X1)),
inference(paramodulation,[status(thm)],[f729,f1379]) ).
fof(f1602,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(b1,sF3_fnc),inverse(X2)))) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X0))))))),
inference(paramodulation,[status(thm)],[f1379,f1338]) ).
fof(f1608,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(X0)),multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0)))))) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X1)),
inference(forward_demodulation,[status(thm)],[f1495,f1577]) ).
fof(f1656,plain,
inverse(multiply(multiply(multiply(b1,sF3_fnc),b1),multiply(multiply(b1,sF3_fnc),sF3_fnc))) = multiply(b1,sF3_fnc),
inference(paramodulation,[status(thm)],[f1202,f1338]) ).
fof(f1694,plain,
! [X0,X1] : multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),X1)),X0)) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f1477,f1195]) ).
fof(f1739,plain,
multiply(sF3_fnc,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,sF3_fnc)))) = inverse(b1),
inference(paramodulation,[status(thm)],[f1195,f1510]) ).
fof(f1756,plain,
! [X0] : multiply(inverse(X0),inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(b1,sF3_fnc)))) = inverse(X0),
inference(paramodulation,[status(thm)],[f605,f1510]) ).
fof(f1769,plain,
! [X0] : multiply(multiply(inverse(multiply(b1,sF3_fnc)),inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X0,sF3_fnc)))),inverse(inverse(X0))) = b1,
inference(paramodulation,[status(thm)],[f1510,f1002]) ).
fof(f1772,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(X0)),multiply(multiply(b1,sF3_fnc),X1))) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f1510,f1338]) ).
fof(f1773,plain,
multiply(sF3_fnc,multiply(b1,sF3_fnc)) = inverse(b1),
inference(forward_demodulation,[status(thm)],[f605,f1739]) ).
fof(f1774,plain,
multiply(multiply(b1,sF3_fnc),b1) = inverse(sF3_fnc),
inference(backward_demodulation,[status(thm)],[f1777,f1202]) ).
fof(f1777,plain,
multiply(sF3_fnc,multiply(b1,sF3_fnc)) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f7,f1773]) ).
fof(f1788,plain,
! [X0] : multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,sF3_fnc)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f1195,f1756]) ).
fof(f1790,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),X0) = inverse(inverse(X0)),
inference(backward_demodulation,[status(thm)],[f1796,f1195]) ).
fof(f1796,plain,
! [X0] : multiply(inverse(X0),multiply(b1,sF3_fnc)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f605,f1788]) ).
fof(f1812,plain,
inverse(multiply(inverse(sF3_fnc),multiply(multiply(b1,sF3_fnc),sF3_fnc))) = multiply(b1,sF3_fnc),
inference(backward_demodulation,[status(thm)],[f1774,f1656]) ).
fof(f1827,plain,
! [X0] : inverse(inverse(multiply(inverse(multiply(b1,sF3_fnc)),X0))) = X0,
inference(backward_demodulation,[status(thm)],[f1790,f1482]) ).
fof(f1841,plain,
multiply(b1,sF3_fnc) = multiply(multiply(inverse(sF2_fnc),inverse(inverse(sF3_fnc))),b1),
inference(backward_demodulation,[status(thm)],[f1790,f1486]) ).
fof(f1864,plain,
multiply(b1,sF3_fnc) = multiply(multiply(inverse(sF0_fnc),inverse(inverse(sF1_fnc))),a1),
inference(backward_demodulation,[status(thm)],[f1790,f1490]) ).
fof(f1883,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(multiply(multiply(inverse(multiply(b1,sF3_fnc)),X0),X1)),X0))) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(backward_demodulation,[status(thm)],[f1790,f1694]) ).
fof(f1899,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),X0))))))),
inference(backward_demodulation,[status(thm)],[f1790,f949]) ).
fof(f1909,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,X1)),multiply(multiply(b1,sF3_fnc),inverse(X2)))) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X0)))))))),
inference(backward_demodulation,[status(thm)],[f1790,f1602]) ).
fof(f1919,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(multiply(multiply(b1,sF3_fnc),inverse(X3)),X0)))) = inverse(multiply(inverse(X2),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1))))))),
inference(backward_demodulation,[status(thm)],[f1790,f870]) ).
fof(f1923,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(X2))))))))) = inverse(multiply(inverse(multiply(inverse(X2),multiply(multiply(b1,sF3_fnc),X0))),X1)),
inference(backward_demodulation,[status(thm)],[f1790,f1596]) ).
fof(f1933,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X1,X2))),multiply(inverse(inverse(inverse(inverse(X1)))),X0)))) = X2,
inference(backward_demodulation,[status(thm)],[f1790,f1509]) ).
fof(f1943,plain,
! [X0,X1] : inverse(multiply(inverse(X0),inverse(inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1)))))))) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(backward_demodulation,[status(thm)],[f1790,f1569]) ).
fof(f1945,plain,
! [X0] : multiply(X0,multiply(b1,sF3_fnc)) = inverse(inverse(inverse(inverse(multiply(multiply(b1,sF3_fnc),X0))))),
inference(backward_demodulation,[status(thm)],[f1790,f955]) ).
fof(f1946,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,inverse(inverse(inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X1)))))))),inverse(X2)) = X0,
inference(backward_demodulation,[status(thm)],[f1790,f1334]) ).
fof(f1951,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(X0)),inverse(inverse(inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X0))))))) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X1)),
inference(backward_demodulation,[status(thm)],[f1790,f1608]) ).
fof(f1976,plain,
! [X0,X1] : inverse(multiply(inverse(inverse(X0)),inverse(inverse(X1)))) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X0,X1))),
inference(backward_demodulation,[status(thm)],[f1790,f1772]) ).
fof(f2001,plain,
inverse(multiply(inverse(sF3_fnc),inverse(inverse(sF3_fnc)))) = multiply(b1,sF3_fnc),
inference(forward_demodulation,[status(thm)],[f1790,f1812]) ).
fof(f2004,plain,
! [X0,X1] : multiply(multiply(multiply(b1,sF3_fnc),X0),inverse(multiply(inverse(X1),X0))) = X1,
inference(backward_demodulation,[status(thm)],[f2033,f1003]) ).
fof(f2006,plain,
! [X0] : multiply(multiply(multiply(b1,sF3_fnc),X0),inverse(multiply(sF1_fnc,X0))) = a1,
inference(backward_demodulation,[status(thm)],[f2033,f1001]) ).
fof(f2013,plain,
! [X0] : multiply(multiply(inverse(multiply(b1,sF3_fnc)),inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X0,sF3_fnc)))),inverse(inverse(X0))) = b1,
inference(backward_demodulation,[status(thm)],[f2033,f1769]) ).
fof(f2033,plain,
inverse(multiply(b1,sF3_fnc)) = multiply(b1,sF3_fnc),
inference(forward_demodulation,[status(thm)],[f605,f2001]) ).
fof(f2078,plain,
! [X0] : inverse(inverse(multiply(multiply(b1,sF3_fnc),X0))) = X0,
inference(forward_demodulation,[status(thm)],[f2033,f1827]) ).
fof(f2081,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f1790,f2078]) ).
fof(f2198,plain,
! [X0] : inverse(X0) = inverse(multiply(X0,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f1477,f1883]) ).
fof(f2250,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(inverse(X1),inverse(multiply(X0,multiply(b1,sF3_fnc))))),
inference(forward_demodulation,[status(thm)],[f955,f1899]) ).
fof(f2270,plain,
! [X0,X1] : multiply(X0,X1) = inverse(multiply(inverse(X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f2198,f2250]) ).
fof(f2313,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,X1)),inverse(inverse(inverse(X2))))) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,X0)))))))),
inference(forward_demodulation,[status(thm)],[f1790,f1909]) ).
fof(f2314,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X2),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1)))))))),
inference(forward_demodulation,[status(thm)],[f2270,f2313]) ).
fof(f2315,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = inverse(inverse(inverse(multiply(inverse(X2),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))))))))),
inference(forward_demodulation,[status(thm)],[f1790,f2314]) ).
fof(f2316,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = inverse(inverse(multiply(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1)))),X2))),
inference(forward_demodulation,[status(thm)],[f2270,f2315]) ).
fof(f2317,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = inverse(inverse(multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),X2))),
inference(forward_demodulation,[status(thm)],[f1790,f2316]) ).
fof(f2318,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(X1,X2)) = inverse(inverse(multiply(multiply(X0,X1),X2))),
inference(forward_demodulation,[status(thm)],[f2081,f2317]) ).
fof(f2352,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(inverse(inverse(inverse(X3))),X0)))) = inverse(multiply(inverse(X2),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1))))))),
inference(forward_demodulation,[status(thm)],[f1790,f1919]) ).
fof(f2353,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(inverse(inverse(inverse(X3))),X0)))) = multiply(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X1)))),X2),
inference(forward_demodulation,[status(thm)],[f2270,f2352]) ).
fof(f2354,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(inverse(inverse(inverse(X3))),X0)))) = multiply(inverse(inverse(inverse(inverse(multiply(X3,X1))))),X2),
inference(forward_demodulation,[status(thm)],[f1790,f2353]) ).
fof(f2355,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(inverse(multiply(X1,X2)),multiply(inverse(inverse(inverse(X3))),X0)))) = multiply(multiply(X3,X1),X2),
inference(forward_demodulation,[status(thm)],[f2081,f2354]) ).
fof(f2365,plain,
! [X0,X1,X2] : inverse(multiply(inverse(X0),inverse(inverse(inverse(multiply(inverse(X1),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(X2)))))))))) = inverse(multiply(inverse(multiply(inverse(X2),multiply(multiply(b1,sF3_fnc),X0))),X1)),
inference(forward_demodulation,[status(thm)],[f1790,f1923]) ).
fof(f2366,plain,
! [X0,X1,X2] : multiply(inverse(inverse(multiply(inverse(X0),inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(X1))))))),X2) = inverse(multiply(inverse(multiply(inverse(X1),multiply(multiply(b1,sF3_fnc),X2))),X0)),
inference(forward_demodulation,[status(thm)],[f2270,f2365]) ).
fof(f2367,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(multiply(multiply(b1,sF3_fnc),inverse(X0))),X1)),X2) = inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X2))),X1)),
inference(forward_demodulation,[status(thm)],[f2270,f2366]) ).
fof(f2368,plain,
! [X0,X1,X2] : multiply(inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)),X2) = inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X2))),X1)),
inference(forward_demodulation,[status(thm)],[f1790,f2367]) ).
fof(f2369,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),X2) = inverse(multiply(inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X2))),X1)),
inference(forward_demodulation,[status(thm)],[f2081,f2368]) ).
fof(f2370,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),X2) = inverse(multiply(inverse(multiply(inverse(X0),inverse(inverse(X2)))),X1)),
inference(forward_demodulation,[status(thm)],[f1790,f2369]) ).
fof(f2371,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),X2) = inverse(multiply(multiply(inverse(X2),X0),X1)),
inference(forward_demodulation,[status(thm)],[f2270,f2370]) ).
fof(f2420,plain,
! [X0,X1] : multiply(multiply(inverse(X0),inverse(inverse(multiply(b1,sF3_fnc)))),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f2355,f1933]) ).
fof(f2421,plain,
! [X0,X1] : multiply(multiply(inverse(X0),inverse(multiply(b1,sF3_fnc))),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f2033,f2420]) ).
fof(f2422,plain,
! [X0,X1] : multiply(multiply(inverse(X0),multiply(b1,sF3_fnc)),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f2033,f2421]) ).
fof(f2425,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f1796,f2422]) ).
fof(f2448,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,X1))))),X0) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f2270,f1943]) ).
fof(f2449,plain,
! [X0,X1] : multiply(multiply(inverse(inverse(b1)),multiply(sF3_fnc,inverse(multiply(X0,X1)))),X0) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f2318,f2448]) ).
fof(f2450,plain,
! [X0,X1] : multiply(multiply(inverse(sF3_fnc),multiply(sF3_fnc,inverse(multiply(X0,X1)))),X0) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f7,f2449]) ).
fof(f2451,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),X0) = inverse(multiply(X1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f2425,f2450]) ).
fof(f2453,plain,
! [X0,X1] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(forward_demodulation,[status(thm)],[f2198,f2451]) ).
fof(f2458,plain,
! [X0] : multiply(X0,multiply(b1,sF3_fnc)) = multiply(multiply(b1,sF3_fnc),X0),
inference(forward_demodulation,[status(thm)],[f2081,f1945]) ).
fof(f2466,plain,
! [X0] : multiply(X0,multiply(b1,sF3_fnc)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1790,f2458]) ).
fof(f2467,plain,
! [X0,X1,X2] : multiply(inverse(inverse(inverse(inverse(multiply(X0,inverse(inverse(inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X1))))))))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f1790,f1946]) ).
fof(f2468,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(inverse(inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X2))),X1))))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f2081,f2467]) ).
fof(f2469,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(inverse(multiply(X1,X2)),X1)))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f2318,f2468]) ).
fof(f2470,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(inverse(multiply(X1,X2)),X1)))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f2033,f2469]) ).
fof(f2471,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(X1,X2)),X1)))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f2033,f2470]) ).
fof(f2472,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(inverse(inverse(multiply(inverse(multiply(X1,X2)),X1))))),inverse(X2)) = X0,
inference(forward_demodulation,[status(thm)],[f1790,f2471]) ).
fof(f2473,plain,
! [X0,X1] : multiply(multiply(X0,inverse(inverse(inverse(inverse(X1))))),inverse(X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2453,f2472]) ).
fof(f2474,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2081,f2473]) ).
fof(f2489,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(inverse(X0),multiply(multiply(b1,sF3_fnc),X1)))),inverse(X1)) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X0)),
inference(forward_demodulation,[status(thm)],[f2270,f1951]) ).
fof(f2490,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(inverse(X0),inverse(inverse(X1))))),inverse(X1)) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X0)),
inference(forward_demodulation,[status(thm)],[f1790,f2489]) ).
fof(f2491,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(X0),X1)),inverse(X0)) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X1)),
inference(forward_demodulation,[status(thm)],[f2270,f2490]) ).
fof(f2492,plain,
! [X0] : inverse(X0) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),X0)),
inference(forward_demodulation,[status(thm)],[f2453,f2491]) ).
fof(f2493,plain,
! [X0] : inverse(X0) = inverse(multiply(inverse(multiply(b1,sF3_fnc)),X0)),
inference(forward_demodulation,[status(thm)],[f2033,f2492]) ).
fof(f2494,plain,
! [X0] : inverse(X0) = inverse(multiply(multiply(b1,sF3_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f2033,f2493]) ).
fof(f2516,plain,
! [X0] : inverse(X0) = inverse(inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f1790,f2494]) ).
fof(f2613,plain,
! [X0,X1] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(inverse(inverse(multiply(b1,sF3_fnc))),multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2270,f1976]) ).
fof(f2614,plain,
! [X0,X1] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2033,f2613]) ).
fof(f2615,plain,
! [X0,X1] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(multiply(b1,sF3_fnc),multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2033,f2614]) ).
fof(f2616,plain,
! [X0,X1] : multiply(inverse(X0),inverse(X1)) = inverse(inverse(inverse(multiply(X1,X0)))),
inference(forward_demodulation,[status(thm)],[f1790,f2615]) ).
fof(f2620,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(inverse(sF1_fnc),sF0_fnc)),a1),
inference(backward_demodulation,[status(thm)],[f2630,f1864]) ).
fof(f2621,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1),
inference(backward_demodulation,[status(thm)],[f2630,f1841]) ).
fof(f2630,plain,
! [X0,X1] : multiply(inverse(X0),inverse(X1)) = inverse(multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f2516,f2616]) ).
fof(f2662,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))) = X1,
inference(forward_demodulation,[status(thm)],[f1790,f2004]) ).
fof(f2663,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(X0),X1),inverse(X1))) = X0,
inference(forward_demodulation,[status(thm)],[f2630,f2662]) ).
fof(f2664,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X0))),X1) = X1,
inference(forward_demodulation,[status(thm)],[f2371,f2663]) ).
fof(f2665,plain,
! [X0] : multiply(inverse(multiply(b1,sF3_fnc)),X0) = X0,
inference(forward_demodulation,[status(thm)],[f605,f2664]) ).
fof(f2666,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),X0) = X0,
inference(forward_demodulation,[status(thm)],[f2033,f2665]) ).
fof(f2688,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1790,f2666]) ).
fof(f2689,plain,
! [X0] : multiply(inverse(inverse(X0)),inverse(multiply(sF1_fnc,X0))) = a1,
inference(forward_demodulation,[status(thm)],[f1790,f2006]) ).
fof(f2690,plain,
! [X0] : inverse(multiply(multiply(sF1_fnc,X0),inverse(X0))) = a1,
inference(forward_demodulation,[status(thm)],[f2630,f2689]) ).
fof(f2692,plain,
inverse(sF1_fnc) = a1,
inference(forward_demodulation,[status(thm)],[f2474,f2690]) ).
fof(f2722,plain,
! [X0] : multiply(inverse(multiply(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X0,sF3_fnc)),multiply(b1,sF3_fnc))),inverse(inverse(X0))) = b1,
inference(forward_demodulation,[status(thm)],[f2630,f2013]) ).
fof(f2723,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X0,sF3_fnc)),multiply(b1,sF3_fnc)))) = b1,
inference(forward_demodulation,[status(thm)],[f2630,f2722]) ).
fof(f2724,plain,
! [X0] : inverse(multiply(inverse(X0),inverse(inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X0,sF3_fnc)))))) = b1,
inference(forward_demodulation,[status(thm)],[f2466,f2723]) ).
fof(f2725,plain,
! [X0] : multiply(inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(X0,sF3_fnc))),X0) = b1,
inference(forward_demodulation,[status(thm)],[f2270,f2724]) ).
fof(f2726,plain,
! [X0] : multiply(inverse(multiply(multiply(b1,sF3_fnc),multiply(X0,sF3_fnc))),X0) = b1,
inference(forward_demodulation,[status(thm)],[f2033,f2725]) ).
fof(f2727,plain,
! [X0] : multiply(inverse(inverse(inverse(multiply(X0,sF3_fnc)))),X0) = b1,
inference(forward_demodulation,[status(thm)],[f1790,f2726]) ).
fof(f2728,plain,
! [X0] : multiply(inverse(multiply(X0,sF3_fnc)),X0) = b1,
inference(forward_demodulation,[status(thm)],[f2516,f2727]) ).
fof(f2730,plain,
inverse(sF3_fnc) = b1,
inference(forward_demodulation,[status(thm)],[f2453,f2728]) ).
fof(f2962,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(a1,sF0_fnc)),a1),
inference(forward_demodulation,[status(thm)],[f2692,f2620]) ).
fof(f2967,plain,
multiply(b1,sF3_fnc) = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f2453,f2962]) ).
fof(f2968,plain,
inverse(sF0_fnc) = multiply(inverse(multiply(inverse(sF3_fnc),sF2_fnc)),b1),
inference(forward_demodulation,[status(thm)],[f2967,f2621]) ).
fof(f2969,plain,
inverse(sF0_fnc) = multiply(inverse(multiply(b1,sF2_fnc)),b1),
inference(forward_demodulation,[status(thm)],[f2730,f2968]) ).
fof(f2976,plain,
inverse(sF0_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f2453,f2969]) ).
fof(f3168,plain,
inverse(inverse(sF2_fnc)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f2976,f2688]) ).
fof(f3169,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f2688,f3168]) ).
fof(f3170,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3169,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP430-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.35 % Computer : n007.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:10:50 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 6.59/1.50 % Refutation found
% 6.59/1.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.59/1.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.61/1.55 % Elapsed time: 1.170929 seconds
% 4.61/1.55 % CPU time: 8.502378 seconds
% 4.61/1.55 % Total memory used: 198.859 MB
% 4.61/1.55 % Net memory used: 193.229 MB
%------------------------------------------------------------------------------