%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP442-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:13 PM UTC 2026
% Result : Unsatisfiable 5.60s 1.33s
% Output : CNFRefutation 4.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 6
% Syntax : Number of formulae : 113 ( 113 unt; 4 def)
% Number of atoms : 113 ( 112 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 13 ( 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 : 189 ( 189 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : inverse(multiply(A,multiply(B,multiply(multiply(C,inverse(C)),inverse(multiply(D,multiply(A,B))))))) = 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] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = 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,X6] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,multiply(X2,X3)))))),X5),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f13,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(X4,inverse(X4)),X2)))) = X3,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f30,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(b1,sF3_fnc),X1)))) = X2,
inference(paramodulation,[status(thm)],[f11,f11]) ).
fof(f33,plain,
! [X0] : inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc)))))) = X0,
inference(paramodulation,[status(thm)],[f8,f11]) ).
fof(f34,plain,
! [X0] : inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc)))))) = X0,
inference(paramodulation,[status(thm)],[f6,f11]) ).
fof(f83,plain,
! [X0] : inverse(multiply(b1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X0)))) = sF3_fnc,
inference(paramodulation,[status(thm)],[f33,f11]) ).
fof(f92,plain,
! [X0] : inverse(multiply(a1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(b1,sF3_fnc),X0)))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f34,f11]) ).
fof(f172,plain,
! [X0,X1,X2] : inverse(multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2)))) = multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),
inference(paramodulation,[status(thm)],[f30,f30]) ).
fof(f175,plain,
! [X0,X1,X2] : inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(b1,sF3_fnc),X1)))) = X2,
inference(paramodulation,[status(thm)],[f11,f30]) ).
fof(f184,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,multiply(X3,X4)))),multiply(multiply(multiply(b1,sF3_fnc),X2),multiply(multiply(X5,inverse(X5)),X3))),X4),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(paramodulation,[status(thm)],[f30,f10]) ).
fof(f194,plain,
! [X0,X1,X2] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1)))) = X2,
inference(forward_demodulation,[status(thm)],[f172,f175]) ).
fof(f206,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1)))))))) = multiply(multiply(X4,inverse(X4)),X3),
inference(paramodulation,[status(thm)],[f13,f194]) ).
fof(f211,plain,
! [X0,X1,X2,X3] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(b1,sF3_fnc))))) = inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,X3))),
inference(paramodulation,[status(thm)],[f194,f194]) ).
fof(f215,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc))) = X0,
inference(paramodulation,[status(thm)],[f8,f194]) ).
fof(f216,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF1_fnc,multiply(a1,X0))),sF0_fnc))) = X0,
inference(paramodulation,[status(thm)],[f6,f194]) ).
fof(f225,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X4))),multiply(X2,X3))),multiply(multiply(X5,inverse(X5)),inverse(multiply(X6,X4))))),X6),inverse(multiply(X7,multiply(X0,X1))))))) = X7,
inference(paramodulation,[status(thm)],[f194,f10]) ).
fof(f336,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,multiply(X3,X4)))),multiply(multiply(multiply(b1,sF3_fnc),X2),multiply(multiply(b1,sF3_fnc),X3))),X4),inverse(multiply(X5,multiply(X0,X1))))))) = X5,
inference(backward_demodulation,[status(thm)],[f351,f184]) ).
fof(f351,plain,
! [X0,X1] : multiply(multiply(b1,sF3_fnc),X0) = multiply(multiply(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f3,f206]) ).
fof(f366,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X4))),multiply(X2,X3))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X5,X4))))),X5),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(forward_demodulation,[status(thm)],[f351,f225]) ).
fof(f426,plain,
! [X0] : inverse(multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(b1,sF3_fnc),sF0_fnc)))))) = multiply(X0,inverse(X0)),
inference(paramodulation,[status(thm)],[f351,f34]) ).
fof(f474,plain,
! [X0] : multiply(b1,sF3_fnc) = multiply(X0,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f34,f426]) ).
fof(f492,plain,
! [X0] : multiply(b1,sF3_fnc) = multiply(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))),X0),
inference(paramodulation,[status(thm)],[f33,f474]) ).
fof(f498,plain,
! [X0,X1] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,multiply(inverse(X0),X1))),multiply(b1,sF3_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f474,f194]) ).
fof(f500,plain,
! [X0,X1] : inverse(multiply(inverse(X0),multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(b1,sF3_fnc)))),multiply(multiply(b1,sF3_fnc),X1)))) = X0,
inference(paramodulation,[status(thm)],[f474,f30]) ).
fof(f546,plain,
! [X0,X1] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(b1,sF3_fnc))))) = inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X1))),sF2_fnc)),
inference(paramodulation,[status(thm)],[f215,f194]) ).
fof(f552,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)) = inverse(multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2))),
inference(backward_demodulation,[status(thm)],[f546,f211]) ).
fof(f555,plain,
! [X0,X1,X2,X3,X4] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X2))),sF2_fnc)),multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X2))))),X3),inverse(multiply(X4,multiply(X0,X1))))))) = X4,
inference(backward_demodulation,[status(thm)],[f552,f366]) ).
fof(f626,plain,
! [X0,X1] : inverse(multiply(b1,multiply(sF3_fnc,X0))) = inverse(multiply(X1,multiply(inverse(X1),X0))),
inference(paramodulation,[status(thm)],[f498,f11]) ).
fof(f674,plain,
! [X0,X1,X2] : multiply(b1,sF3_fnc) = multiply(multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2))))),
inference(paramodulation,[status(thm)],[f172,f474]) ).
fof(f697,plain,
! [X0] : inverse(multiply(b1,multiply(sF3_fnc,X0))) = inverse(multiply(a1,multiply(sF1_fnc,X0))),
inference(paramodulation,[status(thm)],[f5,f626]) ).
fof(f700,plain,
! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X1))))))) = X0,
inference(paramodulation,[status(thm)],[f626,f11]) ).
fof(f701,plain,
! [X0,X1] : multiply(b1,sF3_fnc) = multiply(multiply(X0,multiply(inverse(X0),X1)),inverse(multiply(b1,multiply(sF3_fnc,X1)))),
inference(paramodulation,[status(thm)],[f626,f474]) ).
fof(f726,plain,
! [X0] : inverse(multiply(sF1_fnc,multiply(X0,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X0))))))) = a1,
inference(paramodulation,[status(thm)],[f697,f11]) ).
fof(f782,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(b1,multiply(sF3_fnc,X0))),multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(b1,sF3_fnc)))),multiply(multiply(b1,sF3_fnc),X1)))) = multiply(X2,multiply(inverse(X2),X0)),
inference(paramodulation,[status(thm)],[f701,f30]) ).
fof(f796,plain,
! [X0,X1] : multiply(b1,multiply(sF3_fnc,X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(forward_demodulation,[status(thm)],[f500,f782]) ).
fof(f865,plain,
! [X0,X1,X2,X3] : inverse(multiply(X0,multiply(X1,multiply(b1,sF3_fnc)))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X2,multiply(X3,multiply(X0,X1))))),multiply(multiply(multiply(b1,sF3_fnc),X2),multiply(multiply(b1,sF3_fnc),X3))),
inference(paramodulation,[status(thm)],[f474,f336]) ).
fof(f1161,plain,
! [X0,X1,X2,X3] : inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),multiply(X3,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X3))))))) = multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(paramodulation,[status(thm)],[f172,f700]) ).
fof(f1162,plain,
! [X0,X1] : inverse(multiply(sF1_fnc,multiply(X0,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X0))))))) = multiply(a1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,sF0_fnc))),multiply(multiply(b1,sF3_fnc),X1))),
inference(paramodulation,[status(thm)],[f92,f700]) ).
fof(f1163,plain,
! [X0,X1] : inverse(multiply(sF3_fnc,multiply(X0,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X0))))))) = multiply(b1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X1))),
inference(paramodulation,[status(thm)],[f83,f700]) ).
fof(f1164,plain,
! [X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X1))))))) = multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))))),
inference(paramodulation,[status(thm)],[f34,f700]) ).
fof(f1166,plain,
! [X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,multiply(sF3_fnc,X1))))))) = multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))),
inference(paramodulation,[status(thm)],[f33,f700]) ).
fof(f1197,plain,
! [X0] : a1 = multiply(a1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(b1,sF3_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f726,f1162]) ).
fof(f1203,plain,
! [X0] : b1 = multiply(b1,multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f11,f1163]) ).
fof(f1204,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X0),sF0_fnc))))) = X0,
inference(backward_demodulation,[status(thm)],[f1164,f700]) ).
fof(f1205,plain,
! [X0,X1,X2] : multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),sF0_fnc))))) = multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(backward_demodulation,[status(thm)],[f1164,f1161]) ).
fof(f1219,plain,
! [X0] : multiply(sF1_fnc,multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))))) = multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))),
inference(forward_demodulation,[status(thm)],[f1164,f1166]) ).
fof(f1244,plain,
! [X0] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(X0),sF2_fnc))))) = X0,
inference(forward_demodulation,[status(thm)],[f1219,f1204]) ).
fof(f1245,plain,
! [X0,X1,X2] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2)))),sF2_fnc))))) = multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(forward_demodulation,[status(thm)],[f1219,f1205]) ).
fof(f1380,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF1_fnc,a1)),sF0_fnc))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(b1,sF3_fnc),X0)),
inference(paramodulation,[status(thm)],[f1197,f216]) ).
fof(f1395,plain,
a1 = multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))),
inference(backward_demodulation,[status(thm)],[f1396,f1197]) ).
fof(f1396,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF0_fnc))),multiply(multiply(b1,sF3_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f6,f1380]) ).
fof(f1414,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF3_fnc,b1)),sF2_fnc))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X0)),
inference(paramodulation,[status(thm)],[f1203,f215]) ).
fof(f1433,plain,
b1 = multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF2_fnc),sF2_fnc)))),
inference(backward_demodulation,[status(thm)],[f1434,f1203]) ).
fof(f1434,plain,
! [X0] : multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF2_fnc),sF2_fnc))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))),multiply(multiply(b1,sF3_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f8,f1414]) ).
fof(f1847,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc)) = inverse(multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2)))),
inference(paramodulation,[status(thm)],[f172,f552]) ).
fof(f1878,plain,
! [X0] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF2_fnc),sF2_fnc)))))),sF2_fnc)) = inverse(multiply(inverse(multiply(X0,b1)),multiply(X0,b1))),
inference(paramodulation,[status(thm)],[f1433,f552]) ).
fof(f1884,plain,
! [X0] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF0_fnc),sF0_fnc)))))),sF2_fnc)) = inverse(multiply(inverse(multiply(X0,a1)),multiply(X0,a1))),
inference(paramodulation,[status(thm)],[f1395,f552]) ).
fof(f1945,plain,
! [X0,X1,X2] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)),sF2_fnc))))) = multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f552,f1244]) ).
fof(f1950,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc)) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f172,f1847]) ).
fof(f1951,plain,
! [X0] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc)) = multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f552,f1950]) ).
fof(f1952,plain,
! [X0] : inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f215,f1951]) ).
fof(f1964,plain,
! [X0] : inverse(multiply(inverse(sF2_fnc),sF2_fnc)) = inverse(multiply(inverse(multiply(X0,b1)),multiply(X0,b1))),
inference(forward_demodulation,[status(thm)],[f1952,f1878]) ).
fof(f1972,plain,
! [X0] : inverse(multiply(inverse(sF0_fnc),sF0_fnc)) = inverse(multiply(inverse(multiply(X0,a1)),multiply(X0,a1))),
inference(forward_demodulation,[status(thm)],[f1952,f1884]) ).
fof(f2032,plain,
! [X0,X1,X2] : multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc) = multiply(inverse(multiply(X1,multiply(X2,X0))),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f1244,f1945]) ).
fof(f2065,plain,
! [X0] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))) = multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc),
inference(paramodulation,[status(thm)],[f1952,f1244]) ).
fof(f2099,plain,
! [X0] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(inverse(sF2_fnc),sF2_fnc)),sF2_fnc))))) = multiply(inverse(multiply(X0,b1)),multiply(X0,b1)),
inference(paramodulation,[status(thm)],[f1964,f1244]) ).
fof(f2107,plain,
! [X0] : multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(multiply(X0,b1)),multiply(X0,b1)),
inference(forward_demodulation,[status(thm)],[f1244,f2099]) ).
fof(f2112,plain,
multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(multiply(b1,sF3_fnc)),multiply(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(b1,sF2_fnc))))),b1)),
inference(paramodulation,[status(thm)],[f492,f2107]) ).
fof(f2118,plain,
multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(multiply(b1,sF3_fnc)),multiply(b1,sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f492,f2112]) ).
fof(f2152,plain,
inverse(multiply(inverse(sF0_fnc),sF0_fnc)) = inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(a1,sF2_fnc))))),a1))),
inference(paramodulation,[status(thm)],[f492,f1972]) ).
fof(f2161,plain,
inverse(multiply(inverse(sF0_fnc),sF0_fnc)) = inverse(multiply(inverse(multiply(b1,sF3_fnc)),multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f492,f2152]) ).
fof(f2163,plain,
a1 = multiply(a1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF2_fnc),sF2_fnc)))),
inference(backward_demodulation,[status(thm)],[f2168,f1395]) ).
fof(f2168,plain,
inverse(multiply(inverse(sF0_fnc),sF0_fnc)) = inverse(multiply(inverse(sF2_fnc),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f2118,f2161]) ).
fof(f2253,plain,
! [X0,X1,X2] : multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),X0)))),sF2_fnc) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(paramodulation,[status(thm)],[f172,f2032]) ).
fof(f2266,plain,
multiply(inverse(multiply(sF3_fnc,multiply(b1,inverse(multiply(inverse(sF2_fnc),sF2_fnc))))),sF2_fnc) = multiply(inverse(b1),multiply(b1,multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f1433,f2032]) ).
fof(f2272,plain,
multiply(inverse(multiply(sF3_fnc,multiply(b1,inverse(multiply(inverse(sF2_fnc),sF2_fnc))))),sF2_fnc) = multiply(inverse(a1),multiply(a1,multiply(b1,sF3_fnc))),
inference(paramodulation,[status(thm)],[f2163,f2032]) ).
fof(f2300,plain,
! [X0] : multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(sF2_fnc),sF2_fnc)))))),sF2_fnc) = multiply(inverse(multiply(X0,a1)),multiply(X0,a1)),
inference(paramodulation,[status(thm)],[f2163,f2032]) ).
fof(f2360,plain,
! [X0,X1] : inverse(multiply(X0,multiply(X1,multiply(b1,sF3_fnc)))) = multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(multiply(X0,X1),sF2_fnc))))),
inference(backward_demodulation,[status(thm)],[f2397,f865]) ).
fof(f2397,plain,
! [X0,X1,X2] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,sF2_fnc))))) = multiply(multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(forward_demodulation,[status(thm)],[f2065,f2253]) ).
fof(f2404,plain,
multiply(inverse(multiply(sF3_fnc,multiply(b1,inverse(multiply(inverse(sF2_fnc),sF2_fnc))))),sF2_fnc) = multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f7,f2266]) ).
fof(f2409,plain,
multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc))) = multiply(inverse(a1),multiply(a1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f2404,f2272]) ).
fof(f2411,plain,
multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc))) = multiply(sF1_fnc,multiply(a1,multiply(b1,sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f2409]) ).
fof(f2442,plain,
! [X0] : multiply(sF3_fnc,multiply(b1,multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(inverse(sF2_fnc),sF2_fnc)),sF2_fnc))))) = multiply(inverse(multiply(X0,a1)),multiply(X0,a1)),
inference(forward_demodulation,[status(thm)],[f2065,f2300]) ).
fof(f2443,plain,
! [X0] : multiply(inverse(sF2_fnc),sF2_fnc) = multiply(inverse(multiply(X0,a1)),multiply(X0,a1)),
inference(forward_demodulation,[status(thm)],[f1244,f2442]) ).
fof(f2484,plain,
! [X0,X1,X2] : inverse(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(b1,sF3_fnc)))) = multiply(multiply(multiply(b1,sF3_fnc),X0),multiply(multiply(multiply(b1,sF3_fnc),X1),multiply(multiply(b1,sF3_fnc),X2))),
inference(backward_demodulation,[status(thm)],[f2360,f1245]) ).
fof(f2580,plain,
! [X0,X1,X2] : multiply(b1,sF3_fnc) = multiply(inverse(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(b1,sF3_fnc)))),multiply(multiply(b1,sF3_fnc),inverse(multiply(X0,multiply(X1,X2))))),
inference(backward_demodulation,[status(thm)],[f2484,f674]) ).
fof(f2636,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc)))),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f2032,f2580]) ).
fof(f2643,plain,
! [X0] : multiply(b1,multiply(sF3_fnc,multiply(X0,a1))) = multiply(multiply(X0,a1),multiply(inverse(sF2_fnc),sF2_fnc)),
inference(paramodulation,[status(thm)],[f2443,f796]) ).
fof(f2654,plain,
multiply(b1,multiply(sF3_fnc,sF2_fnc)) = multiply(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc))),multiply(b1,sF3_fnc)),
inference(paramodulation,[status(thm)],[f2636,f796]) ).
fof(f2676,plain,
multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc)))),sF2_fnc) = multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc)))),multiply(sF1_fnc,a1)),
inference(paramodulation,[status(thm)],[f2411,f2032]) ).
fof(f2679,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc)))),multiply(sF1_fnc,a1)),
inference(forward_demodulation,[status(thm)],[f2636,f2676]) ).
fof(f2680,plain,
multiply(b1,sF3_fnc) = multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc)))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f6,f2679]) ).
fof(f2681,plain,
multiply(b1,multiply(sF3_fnc,sF0_fnc)) = multiply(multiply(sF3_fnc,multiply(b1,multiply(b1,sF3_fnc))),multiply(b1,sF3_fnc)),
inference(paramodulation,[status(thm)],[f2680,f796]) ).
fof(f2693,plain,
multiply(b1,multiply(sF3_fnc,sF0_fnc)) = multiply(b1,multiply(sF3_fnc,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f2654,f2681]) ).
fof(f2705,plain,
multiply(multiply(b1,sF3_fnc),inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,multiply(sF3_fnc,sF2_fnc)))),sF2_fnc))) = multiply(sF3_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f2693,f215]) ).
fof(f2710,plain,
multiply(sF3_fnc,sF2_fnc) = multiply(sF3_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f215,f2705]) ).
fof(f2908,plain,
multiply(b1,multiply(sF3_fnc,multiply(sF1_fnc,a1))) = multiply(sF0_fnc,multiply(inverse(sF2_fnc),sF2_fnc)),
inference(paramodulation,[status(thm)],[f6,f2643]) ).
fof(f2913,plain,
multiply(b1,multiply(sF3_fnc,sF0_fnc)) = multiply(sF0_fnc,multiply(inverse(sF2_fnc),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f6,f2908]) ).
fof(f2914,plain,
multiply(b1,multiply(sF3_fnc,sF2_fnc)) = multiply(sF0_fnc,multiply(inverse(sF2_fnc),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f2710,f2913]) ).
fof(f3055,plain,
! [X0,X1] : inverse(multiply(inverse(sF2_fnc),multiply(sF2_fnc,multiply(multiply(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X0))),sF2_fnc)),multiply(multiply(b1,sF3_fnc),inverse(multiply(X1,X0))))),X1),inverse(multiply(b1,multiply(sF3_fnc,sF2_fnc))))))) = sF0_fnc,
inference(paramodulation,[status(thm)],[f2914,f555]) ).
fof(f3083,plain,
! [X0,X1,X2,X3] : inverse(multiply(inverse(X0),multiply(X1,multiply(multiply(multiply(multiply(b1,sF3_fnc),multiply(inverse(multiply(inverse(multiply(sF3_fnc,multiply(b1,X2))),sF2_fnc)),multiply(multiply(b1,sF3_fnc),inverse(multiply(X3,X2))))),X3),inverse(multiply(b1,multiply(sF3_fnc,X1))))))) = X0,
inference(paramodulation,[status(thm)],[f796,f555]) ).
fof(f3236,plain,
sF2_fnc = sF0_fnc,
inference(backward_demodulation,[status(thm)],[f3083,f3055]) ).
fof(f3253,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3236,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP442-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 20:11:37 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 5.60/1.33 % Refutation found
% 5.60/1.33 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.60/1.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.77/1.38 % Elapsed time: 0.995792 seconds
% 4.77/1.38 % CPU time: 7.700873 seconds
% 4.77/1.38 % Total memory used: 249.951 MB
% 4.77/1.38 % Net memory used: 245.639 MB
%------------------------------------------------------------------------------