%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP443-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 : n011.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 0.15s 15.64s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 5
% Syntax : Number of formulae : 71 ( 71 unt; 3 def)
% Number of atoms : 71 ( 70 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 : 12 ( 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 : 138 ( 138 !; 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/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] : 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(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] : inverse(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f11,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(f13,plain,
! [X0,X1] : inverse(multiply(sF2_fnc,multiply(b2,multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,sF1_fnc)))))) = X1,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f14,plain,
! [X0,X1,X2] : inverse(multiply(X0,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(b2,sF2_fnc),X1)))) = X2,
inference(paramodulation,[status(thm)],[f10,f10]) ).
fof(f29,plain,
! [X0,X1,X2,X3] : inverse(multiply(sF2_fnc,multiply(b2,multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,multiply(X0,X1)))))),X2),inverse(multiply(X3,sF1_fnc)))))) = X3,
inference(paramodulation,[status(thm)],[f10,f13]) ).
fof(f55,plain,
! [X0,X1,X2,X3] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,sF1_fnc))),multiply(multiply(multiply(X2,inverse(X2)),X1),multiply(multiply(X3,inverse(X3)),sF2_fnc)))) = b2,
inference(paramodulation,[status(thm)],[f13,f11]) ).
fof(f58,plain,
! [X0,X1,X2,X3,X4,X5,X6] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,multiply(X3,X5)))),
inference(paramodulation,[status(thm)],[f11,f11]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X1),multiply(multiply(X5,inverse(X5)),X2)))) = X3,
inference(paramodulation,[status(thm)],[f3,f11]) ).
fof(f120,plain,
! [X0,X1,X2] : inverse(multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X0,multiply(X1,X2)))),multiply(multiply(multiply(b2,sF2_fnc),X0),multiply(multiply(b2,sF2_fnc),X1)))) = X2,
inference(paramodulation,[status(thm)],[f10,f14]) ).
fof(f6447,plain,
! [X0,X1,X2,X3] : X0 = multiply(multiply(X1,inverse(X1)),inverse(multiply(inverse(multiply(X2,multiply(X3,X0))),multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f60,f58]) ).
fof(f6449,plain,
! [X0,X1] : b2 = multiply(multiply(X0,inverse(X0)),inverse(multiply(inverse(multiply(X1,sF1_fnc)),multiply(X1,sF2_fnc)))),
inference(paramodulation,[status(thm)],[f55,f58]) ).
fof(f6451,plain,
! [X0,X1,X2,X3,X4] : X0 = multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(inverse(multiply(X3,multiply(X0,multiply(multiply(X4,inverse(X4)),X2)))),X3)))),
inference(paramodulation,[status(thm)],[f11,f58]) ).
fof(f6768,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,inverse(X0)),inverse(multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X2)))) = X3,
inference(paramodulation,[status(thm)],[f58,f60]) ).
fof(f7015,plain,
! [X0,X1,X2,X3] : multiply(multiply(b2,sF2_fnc),X0) = multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(multiply(multiply(b2,sF2_fnc),inverse(multiply(X3,multiply(X0,X2)))),multiply(multiply(b2,sF2_fnc),X3))))),
inference(paramodulation,[status(thm)],[f120,f6447]) ).
fof(f7163,plain,
! [X0,X1] : multiply(multiply(b2,sF2_fnc),X0) = multiply(multiply(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f14,f7015]) ).
fof(f7285,plain,
! [X0,X1,X2,X3] : inverse(multiply(sF2_fnc,multiply(b2,multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,multiply(X0,X1)))))),X2),inverse(multiply(multiply(b2,sF2_fnc),sF1_fnc)))))) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f7163,f29]) ).
fof(f7345,plain,
! [X0] : multiply(b2,sF2_fnc) = multiply(X0,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f29,f7285]) ).
fof(f7374,plain,
! [X0,X1,X2] : multiply(b2,sF2_fnc) = multiply(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),inverse(multiply(X2,multiply(X0,X1)))))),X2),
inference(paramodulation,[status(thm)],[f10,f7345]) ).
fof(f7392,plain,
! [X0,X1] : inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,multiply(b2,sF2_fnc))))))) = X1,
inference(paramodulation,[status(thm)],[f7345,f10]) ).
fof(f8215,plain,
! [X0] : b2 = multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(multiply(X0,sF1_fnc)),multiply(X0,sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f7345,f6449]) ).
fof(f8287,plain,
! [X0,X1,X2] : multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X1)))) = X2,
inference(forward_demodulation,[status(thm)],[f7345,f6768]) ).
fof(f8316,plain,
! [X0,X1] : multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(multiply(X0,multiply(b2,sF2_fnc))),multiply(X0,X1)))) = inverse(X1),
inference(paramodulation,[status(thm)],[f7345,f8287]) ).
fof(f8727,plain,
! [X0,X1] : inverse(multiply(X0,multiply(inverse(X0),X1))) = inverse(multiply(b2,multiply(sF2_fnc,X1))),
inference(paramodulation,[status(thm)],[f8287,f7392]) ).
fof(f8728,plain,
! [X0] : inverse(multiply(X0,multiply(inverse(X0),b2))) = inverse(multiply(b2,sF1_fnc)),
inference(paramodulation,[status(thm)],[f8215,f7392]) ).
fof(f8823,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(b2,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF1_fnc)))))) = X0,
inference(paramodulation,[status(thm)],[f8728,f10]) ).
fof(f8910,plain,
! [X0,X1] : inverse(multiply(inverse(X0),multiply(X1,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,multiply(sF2_fnc,X1))))))) = X0,
inference(paramodulation,[status(thm)],[f8727,f10]) ).
fof(f9396,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(b2,multiply(sF2_fnc,X0))),multiply(b2,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF1_fnc)))))) = multiply(X1,multiply(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f8727,f8823]) ).
fof(f9459,plain,
! [X0,X1] : multiply(b2,multiply(sF2_fnc,X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(forward_demodulation,[status(thm)],[f8823,f9396]) ).
fof(f10884,plain,
! [X0,X1,X2,X3] : X0 = multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,multiply(inverse(multiply(X2,multiply(X0,multiply(multiply(X3,inverse(X3)),X1)))),X2)))),
inference(forward_demodulation,[status(thm)],[f7345,f6451]) ).
fof(f10885,plain,
! [X0,X1,X2] : X0 = multiply(multiply(b2,sF2_fnc),inverse(multiply(X1,multiply(inverse(multiply(X2,multiply(X0,multiply(multiply(b2,sF2_fnc),X1)))),X2)))),
inference(forward_demodulation,[status(thm)],[f7345,f10884]) ).
fof(f10917,plain,
! [X0,X1,X2] : multiply(b2,sF2_fnc) = multiply(multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),X2)))),multiply(X0,X1)),X2),
inference(paramodulation,[status(thm)],[f10885,f7374]) ).
fof(f10927,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(b2,sF2_fnc),X2)))),multiply(X0,X1))) = X2,
inference(paramodulation,[status(thm)],[f10885,f10]) ).
fof(f11006,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(X0,multiply(X1,multiply(b2,sF2_fnc)))),multiply(X0,X1))) = inverse(multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f7345,f10927]) ).
fof(f11183,plain,
! [X0,X1,X2] : inverse(multiply(inverse(multiply(b2,sF2_fnc)),multiply(X0,multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,multiply(sF2_fnc,X0))))))) = multiply(inverse(multiply(X1,multiply(X2,multiply(b2,sF2_fnc)))),multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f11006,f8910]) ).
fof(f11207,plain,
! [X0,X1] : multiply(b2,sF2_fnc) = multiply(inverse(multiply(X0,multiply(X1,multiply(b2,sF2_fnc)))),multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f8910,f11183]) ).
fof(f11246,plain,
! [X0,X1] : multiply(b2,multiply(sF2_fnc,multiply(X0,X1))) = multiply(multiply(X0,multiply(X1,multiply(b2,sF2_fnc))),multiply(b2,sF2_fnc)),
inference(paramodulation,[status(thm)],[f11207,f9459]) ).
fof(f11276,plain,
! [X0,X1,X2] : multiply(multiply(b2,sF2_fnc),inverse(multiply(inverse(multiply(X0,multiply(b2,sF2_fnc))),multiply(X0,inverse(multiply(X1,multiply(X2,multiply(b2,sF2_fnc)))))))) = multiply(X1,X2),
inference(paramodulation,[status(thm)],[f11207,f8287]) ).
fof(f11307,plain,
! [X0,X1] : inverse(inverse(multiply(X0,multiply(X1,multiply(b2,sF2_fnc))))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f8316,f11276]) ).
fof(f11308,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),X0)))),X1),
inference(paramodulation,[status(thm)],[f10927,f11307]) ).
fof(f11949,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,multiply(inverse(multiply(X0,multiply(multiply(b2,sF2_fnc),multiply(multiply(b2,sF2_fnc),multiply(b2,sF2_fnc))))),X0))) = multiply(b2,sF2_fnc),
inference(paramodulation,[status(thm)],[f10917,f11246]) ).
fof(f12012,plain,
multiply(b2,multiply(sF2_fnc,inverse(multiply(b2,sF2_fnc)))) = multiply(b2,sF2_fnc),
inference(forward_demodulation,[status(thm)],[f11308,f11949]) ).
fof(f12016,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),inverse(multiply(b2,sF2_fnc)))))) = X0,
inference(paramodulation,[status(thm)],[f12012,f8910]) ).
fof(f12058,plain,
! [X0] : inverse(multiply(inverse(X0),multiply(inverse(multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f7345,f12016]) ).
fof(f12134,plain,
! [X0] : multiply(multiply(b2,sF2_fnc),multiply(inverse(multiply(b2,sF2_fnc)),multiply(multiply(b2,sF2_fnc),X0))) = X0,
inference(paramodulation,[status(thm)],[f12058,f8287]) ).
fof(f12161,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,multiply(multiply(b2,sF2_fnc),X0))) = X0,
inference(forward_demodulation,[status(thm)],[f9459,f12134]) ).
fof(f12382,plain,
! [X0] : inverse(inverse(multiply(X0,multiply(b2,sF2_fnc)))) = X0,
inference(paramodulation,[status(thm)],[f12161,f10]) ).
fof(f12383,plain,
! [X0] : multiply(b2,sF2_fnc) = multiply(multiply(inverse(X0),multiply(b2,sF2_fnc)),X0),
inference(paramodulation,[status(thm)],[f12161,f10917]) ).
fof(f12975,plain,
! [X0] : inverse(inverse(multiply(X0,multiply(b2,sF2_fnc)))) = multiply(X0,multiply(inverse(multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc))),
inference(paramodulation,[status(thm)],[f12383,f11307]) ).
fof(f13040,plain,
! [X0] : X0 = multiply(X0,multiply(inverse(multiply(b2,sF2_fnc)),multiply(b2,sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f12382,f12975]) ).
fof(f13219,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(backward_demodulation,[status(thm)],[f13040,f12058]) ).
fof(f13371,plain,
! [X0] : multiply(X0,multiply(b2,sF2_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f13219,f12382]) ).
fof(f13397,plain,
inverse(sF2_fnc) = b2,
inference(paramodulation,[status(thm)],[f5,f13219]) ).
fof(f13410,plain,
multiply(b2,sF2_fnc) = multiply(sF2_fnc,b2),
inference(paramodulation,[status(thm)],[f13397,f7345]) ).
fof(f13411,plain,
multiply(b2,sF2_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f6,f13410]) ).
fof(f13422,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,multiply(sF1_fnc,X0))) = X0,
inference(backward_demodulation,[status(thm)],[f13411,f12161]) ).
fof(f13456,plain,
! [X0] : sF1_fnc = multiply(X0,inverse(X0)),
inference(backward_demodulation,[status(thm)],[f13411,f7345]) ).
fof(f13509,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,inverse(inverse(X0)))) = multiply(X0,sF1_fnc),
inference(paramodulation,[status(thm)],[f13456,f9459]) ).
fof(f13511,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,X0)) = multiply(X0,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f13219,f13509]) ).
fof(f13519,plain,
! [X0] : multiply(X0,sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f13411,f13371]) ).
fof(f13800,plain,
multiply(b2,multiply(sF2_fnc,sF0_fnc)) = a2,
inference(paramodulation,[status(thm)],[f7,f13422]) ).
fof(f13828,plain,
sF0_fnc = a2,
inference(backward_demodulation,[status(thm)],[f13833,f13800]) ).
fof(f13833,plain,
! [X0] : multiply(b2,multiply(sF2_fnc,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f13519,f13511]) ).
fof(f13845,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13828,f8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP443-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.03/15.23 % CPULimit : 300
% 0.03/15.23 % WCLimit : 300
% 0.03/15.23 % DateTime : Sun Sep 20 20:13:40 UTC 2026
% 0.03/15.23 % CPUTime :
% 0.03/15.23 % Drodi V4.1.1
% 0.15/15.64 % Refutation found
% 0.15/15.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/15.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/15.68 % Elapsed time: 0.431607 seconds
% 0.15/15.68 % CPU time: 3.362828 seconds
% 0.15/15.68 % Total memory used: 196.324 MB
% 0.15/15.68 % Net memory used: 187.541 MB
%------------------------------------------------------------------------------