%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP431-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:12 PM UTC 2026
% Result : Unsatisfiable 0.20s 1.00s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 5
% Syntax : Number of formulae : 74 ( 74 unt; 3 def)
% Number of atoms : 74 ( 73 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 114 ( 114 !; 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/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(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,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(f11,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),X0)))) = X2,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f17,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X2))),multiply(b2,sF2_fnc)),multiply(X1,X0)))) = X2,
inference(paramodulation,[status(thm)],[f11,f11]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,X3))),multiply(b2,sF2_fnc)),multiply(X2,X0)))) = X3,
inference(paramodulation,[status(thm)],[f3,f11]) ).
fof(f20,plain,
! [X0] : multiply(X0,inverse(multiply(b2,multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),X0)))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f6,f11]) ).
fof(f24,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,X2))),multiply(X3,inverse(X3))),multiply(X1,X0)))) = X2,
inference(paramodulation,[status(thm)],[f11,f3]) ).
fof(f76,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X2))),multiply(multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,X1))),multiply(X5,inverse(X5))),X0)))) = multiply(X4,multiply(X6,inverse(X6))),
inference(paramodulation,[status(thm)],[f10,f10]) ).
fof(f77,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(sF2_fnc,multiply(X1,inverse(X1))),multiply(b2,X0)))) = multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f20,f10]) ).
fof(f3191,plain,
! [X0,X1] : multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),multiply(X0,inverse(X0))) = multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),multiply(X1,inverse(X1))),
inference(paramodulation,[status(thm)],[f77,f77]) ).
fof(f5268,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),multiply(X1,inverse(X1))))),multiply(X2,inverse(X2))),multiply(multiply(multiply(b2,sF2_fnc),inverse(sF1_fnc)),X0)))) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f3191,f24]) ).
fof(f5322,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f24,f5268]) ).
fof(f5334,plain,
! [X0] : multiply(b2,sF2_fnc) = multiply(X0,inverse(X0)),
inference(paramodulation,[status(thm)],[f5,f5322]) ).
fof(f5370,plain,
! [X0,X1,X2] : multiply(inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))),inverse(multiply(X1,multiply(X2,inverse(X2))))) = X0,
inference(paramodulation,[status(thm)],[f5322,f11]) ).
fof(f5393,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(multiply(X1,inverse(X1)),multiply(b2,sF2_fnc)),multiply(X2,X0)))) = inverse(X2),
inference(paramodulation,[status(thm)],[f5322,f18]) ).
fof(f5395,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X2)),X0)))) = X1,
inference(paramodulation,[status(thm)],[f5322,f3]) ).
fof(f6211,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),multiply(multiply(b2,sF2_fnc),X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f5334,f5395]) ).
fof(f6435,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(X1,X0)))) = inverse(X1),
inference(forward_demodulation,[status(thm)],[f5334,f5393]) ).
fof(f6436,plain,
! [X0] : X0 = inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)))))),
inference(paramodulation,[status(thm)],[f11,f6435]) ).
fof(f6748,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,X1)))),inverse(multiply(X1,multiply(b2,sF2_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f5334,f5370]) ).
fof(f6939,plain,
multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)) = inverse(inverse(multiply(b2,sF2_fnc))),
inference(paramodulation,[status(thm)],[f6435,f6436]) ).
fof(f6960,plain,
! [X0] : X0 = inverse(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,inverse(inverse(multiply(b2,sF2_fnc))))))),
inference(backward_demodulation,[status(thm)],[f6939,f6436]) ).
fof(f6962,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(X1,X0)))) = inverse(X1),
inference(backward_demodulation,[status(thm)],[f6939,f6435]) ).
fof(f7116,plain,
! [X0] : multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f6960,f6748]) ).
fof(f7137,plain,
multiply(b2,sF2_fnc) = multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f5334,f7116]) ).
fof(f7151,plain,
! [X0] : multiply(X0,inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(inverse(inverse(multiply(b2,sF2_fnc))),X0)))) = multiply(b2,sF2_fnc),
inference(paramodulation,[status(thm)],[f7116,f17]) ).
fof(f7186,plain,
! [X0] : multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(inverse(inverse(multiply(b2,sF2_fnc))),X0)))) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f6939,f7151]) ).
fof(f7187,plain,
inverse(inverse(inverse(multiply(b2,sF2_fnc)))) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f6962,f7186]) ).
fof(f7197,plain,
! [X0] : multiply(X0,inverse(multiply(b2,sF2_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f7137,f7116]) ).
fof(f7285,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(X1,multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,X1))),multiply(X4,inverse(X4))),X0)))) = multiply(X3,multiply(X5,inverse(X5))),
inference(forward_demodulation,[status(thm)],[f5334,f76]) ).
fof(f7286,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(X1,multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),multiply(X3,inverse(X3))),X0)))) = multiply(X2,multiply(X4,inverse(X4))),
inference(forward_demodulation,[status(thm)],[f5334,f7285]) ).
fof(f7287,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(X1,multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),multiply(b2,sF2_fnc)),X0)))) = multiply(X2,multiply(X3,inverse(X3))),
inference(forward_demodulation,[status(thm)],[f5334,f7286]) ).
fof(f7288,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(X1,multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,X1))),multiply(b2,sF2_fnc)),X0)))) = multiply(X2,multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f5334,f7287]) ).
fof(f7329,plain,
! [X0] : multiply(X0,inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(b2,sF2_fnc)),X0)))) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f6939,f7288]) ).
fof(f7423,plain,
! [X0] : multiply(X0,inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(multiply(multiply(multiply(b2,sF2_fnc),inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(b2,sF2_fnc)),X0)))) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f6939,f7329]) ).
fof(f7424,plain,
inverse(multiply(multiply(multiply(b2,sF2_fnc),inverse(inverse(inverse(multiply(b2,sF2_fnc))))),multiply(b2,sF2_fnc))) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f6962,f7423]) ).
fof(f7425,plain,
inverse(multiply(multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc))) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f7187,f7424]) ).
fof(f7426,plain,
inverse(multiply(inverse(inverse(multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc))) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f6939,f7425]) ).
fof(f7427,plain,
inverse(multiply(b2,sF2_fnc)) = multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f7137,f7426]) ).
fof(f7428,plain,
inverse(multiply(b2,sF2_fnc)) = inverse(inverse(multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f6939,f7427]) ).
fof(f7515,plain,
inverse(inverse(multiply(b2,sF2_fnc))) = multiply(b2,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f7428,f7187]) ).
fof(f7527,plain,
inverse(multiply(b2,sF2_fnc)) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f7428,f7515]) ).
fof(f7558,plain,
! [X0] : multiply(X0,multiply(b2,sF2_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f7527,f7197]) ).
fof(f7593,plain,
! [X0] : multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(X0),multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f7558,f6211]) ).
fof(f7617,plain,
! [X0] : multiply(multiply(b2,sF2_fnc),inverse(inverse(X0))) = X0,
inference(forward_demodulation,[status(thm)],[f7558,f7593]) ).
fof(f7666,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(multiply(inverse(X1),X0))) = X1,
inference(paramodulation,[status(thm)],[f7617,f6211]) ).
fof(f7749,plain,
! [X0] : multiply(inverse(inverse(inverse(inverse(X0)))),inverse(multiply(b2,sF2_fnc))) = X0,
inference(paramodulation,[status(thm)],[f5334,f7666]) ).
fof(f7770,plain,
! [X0] : multiply(inverse(inverse(inverse(inverse(X0)))),multiply(b2,sF2_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f7527,f7749]) ).
fof(f7771,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f7558,f7770]) ).
fof(f7782,plain,
! [X0] : multiply(multiply(b2,sF2_fnc),X0) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f7771,f7617]) ).
fof(f8119,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,multiply(inverse(inverse(inverse(multiply(X2,X1)))),X0)))) = X2,
inference(backward_demodulation,[status(thm)],[f7782,f11]) ).
fof(f8181,plain,
! [X0,X1] : multiply(inverse(inverse(inverse(inverse(multiply(X0,X1))))),inverse(multiply(X1,multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f5334,f8119]) ).
fof(f8200,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(multiply(X1,multiply(b2,sF2_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f7771,f8181]) ).
fof(f8201,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(forward_demodulation,[status(thm)],[f7558,f8200]) ).
fof(f8217,plain,
! [X0,X1] : multiply(X0,inverse(inverse(X1))) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f8201,f8201]) ).
fof(f8224,plain,
multiply(sF1_fnc,inverse(b2)) = sF2_fnc,
inference(paramodulation,[status(thm)],[f6,f8201]) ).
fof(f8235,plain,
multiply(sF1_fnc,sF2_fnc) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f8224]) ).
fof(f8239,plain,
multiply(sF2_fnc,inverse(sF2_fnc)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f8235,f8201]) ).
fof(f8241,plain,
multiply(b2,sF2_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f5334,f8239]) ).
fof(f8243,plain,
! [X0] : multiply(sF1_fnc,X0) = inverse(inverse(X0)),
inference(backward_demodulation,[status(thm)],[f8241,f7782]) ).
fof(f8315,plain,
sF0_fnc = inverse(inverse(a2)),
inference(backward_demodulation,[status(thm)],[f8243,f7]) ).
fof(f8340,plain,
inverse(inverse(sF0_fnc)) = a2,
inference(paramodulation,[status(thm)],[f8315,f7771]) ).
fof(f8616,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = multiply(sF1_fnc,X0),
inference(paramodulation,[status(thm)],[f8243,f8217]) ).
fof(f8639,plain,
! [X0] : X0 = multiply(sF1_fnc,X0),
inference(forward_demodulation,[status(thm)],[f7771,f8616]) ).
fof(f8640,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f8243,f8639]) ).
fof(f8647,plain,
sF0_fnc = a2,
inference(backward_demodulation,[status(thm)],[f8640,f8340]) ).
fof(f8662,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8647,f8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP431-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.45 % Computer : n006.cluster.edu
% 0.15/0.45 % Model : x86_64 x86_64
% 0.15/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.45 % Memory : 8046.5625MB
% 0.15/0.45 % OS : Linux 6.8.0-71-generic
% 0.15/0.45 % CPULimit : 300
% 0.15/0.45 % WCLimit : 300
% 0.15/0.45 % DateTime : Sun Sep 20 20:12:27 UTC 2026
% 0.15/0.46 % CPUTime :
% 0.15/0.48 % Drodi V4.1.1
% 0.20/1.00 % Refutation found
% 0.20/1.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.20/1.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.20/1.06 % Elapsed time: 0.573018 seconds
% 0.20/1.06 % CPU time: 3.569325 seconds
% 0.20/1.06 % Total memory used: 95.287 MB
% 0.20/1.06 % Net memory used: 93.967 MB
%------------------------------------------------------------------------------