%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP485-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 : n015.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:30 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.40s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 6
% Syntax : Number of formulae : 89 ( 89 unt; 1 def)
% Number of atoms : 89 ( 88 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 126 ( 126 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : double_divide(double_divide(A,double_divide(double_divide(double_divide(A,B),C),double_divide(B,identity))),double_divide(identity,identity)) = C,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = double_divide(double_divide(B,A),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : inverse(A) = double_divide(A,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : identity = double_divide(A,inverse(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
multiply(identity,a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),double_divide(X1,identity))),double_divide(identity,identity)) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f7,plain,
! [X0,X1] : multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f8,plain,
! [X0] : inverse(X0) = double_divide(X0,identity),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f9,plain,
! [X0] : identity = double_divide(X0,inverse(X0)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
multiply(identity,a2) != a2,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f11,definition,
sF0_fnc = multiply(identity,a2),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f12,plain,
sF0_fnc != a2,
inference(definition_folding,[],[f10,f11]) ).
fof(f20,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),double_divide(identity,identity)) = double_divide(double_divide(double_divide(double_divide(X0,identity),X2),X1),double_divide(X2,identity)),
inference(paramodulation,[status(thm)],[f6,f6]) ).
fof(f22,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(multiply(X1,X0),double_divide(X1,identity))),double_divide(identity,identity)) = identity,
inference(paramodulation,[status(thm)],[f7,f6]) ).
fof(f25,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(multiply(X1,X0),X2),double_divide(identity,identity))),double_divide(identity,identity)) = X2,
inference(paramodulation,[status(thm)],[f7,f6]) ).
fof(f28,plain,
! [X0,X1,X2] : multiply(double_divide(identity,identity),double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),double_divide(X1,identity)))) = double_divide(X2,identity),
inference(paramodulation,[status(thm)],[f6,f7]) ).
fof(f35,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),double_divide(identity,identity)) = double_divide(multiply(X1,double_divide(X0,identity)),double_divide(X1,identity)),
inference(paramodulation,[status(thm)],[f22,f6]) ).
fof(f103,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,X1),identity),double_divide(identity,identity)) = double_divide(multiply(X2,multiply(X1,X0)),double_divide(X2,identity)),
inference(paramodulation,[status(thm)],[f7,f35]) ).
fof(f113,plain,
! [X0,X1,X2] : double_divide(multiply(X0,X1),double_divide(identity,identity)) = double_divide(multiply(X2,multiply(X0,X1)),double_divide(X2,identity)),
inference(forward_demodulation,[status(thm)],[f7,f103]) ).
fof(f117,plain,
! [X0] : double_divide(multiply(identity,a2),double_divide(identity,identity)) = double_divide(multiply(X0,sF0_fnc),double_divide(X0,identity)),
inference(paramodulation,[status(thm)],[f11,f113]) ).
fof(f128,plain,
! [X0] : double_divide(sF0_fnc,double_divide(identity,identity)) = double_divide(multiply(X0,sF0_fnc),double_divide(X0,identity)),
inference(forward_demodulation,[status(thm)],[f11,f117]) ).
fof(f238,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(identity)) = double_divide(double_divide(double_divide(double_divide(X0,identity),X2),X1),double_divide(X2,identity)),
inference(backward_demodulation,[status(thm)],[f8,f20]) ).
fof(f246,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),double_divide(X1,identity))),inverse(identity)) = X2,
inference(backward_demodulation,[status(thm)],[f8,f6]) ).
fof(f249,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
inference(backward_demodulation,[status(thm)],[f8,f7]) ).
fof(f252,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(identity)) = double_divide(double_divide(double_divide(inverse(X0),X2),X1),double_divide(X2,identity)),
inference(forward_demodulation,[status(thm)],[f8,f238]) ).
fof(f253,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(identity)) = double_divide(double_divide(double_divide(inverse(X0),X2),X1),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f8,f252]) ).
fof(f261,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1))),inverse(identity)) = X2,
inference(forward_demodulation,[status(thm)],[f8,f246]) ).
fof(f263,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(identity),
inference(paramodulation,[status(thm)],[f9,f249]) ).
fof(f264,plain,
! [X0] : multiply(identity,X0) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f8,f249]) ).
fof(f267,plain,
sF0_fnc = inverse(inverse(a2)),
inference(backward_demodulation,[status(thm)],[f264,f11]) ).
fof(f289,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,inverse(X1))),inverse(identity)) = inverse(double_divide(X0,X1)),
inference(paramodulation,[status(thm)],[f9,f261]) ).
fof(f302,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,inverse(X1))),inverse(identity)) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f249,f289]) ).
fof(f337,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(multiply(X1,X0),X2),inverse(identity))),double_divide(identity,identity)) = X2,
inference(forward_demodulation,[status(thm)],[f8,f25]) ).
fof(f338,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,X1),double_divide(double_divide(multiply(X1,X0),X2),inverse(identity))),inverse(identity)) = X2,
inference(forward_demodulation,[status(thm)],[f8,f337]) ).
fof(f347,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,X1),double_divide(identity,inverse(identity))),inverse(identity)) = inverse(multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f9,f338]) ).
fof(f364,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,X1),identity),inverse(identity)) = inverse(multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f9,f347]) ).
fof(f365,plain,
! [X0,X1] : double_divide(inverse(double_divide(X0,X1)),inverse(identity)) = inverse(multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f8,f364]) ).
fof(f366,plain,
! [X0,X1] : double_divide(multiply(X0,X1),inverse(identity)) = inverse(multiply(X0,X1)),
inference(forward_demodulation,[status(thm)],[f249,f365]) ).
fof(f385,plain,
! [X0] : double_divide(sF0_fnc,inverse(identity)) = double_divide(multiply(X0,sF0_fnc),double_divide(X0,identity)),
inference(forward_demodulation,[status(thm)],[f8,f128]) ).
fof(f386,plain,
! [X0] : double_divide(sF0_fnc,inverse(identity)) = double_divide(multiply(X0,sF0_fnc),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f8,f385]) ).
fof(f459,plain,
double_divide(sF0_fnc,inverse(identity)) = inverse(multiply(identity,sF0_fnc)),
inference(paramodulation,[status(thm)],[f386,f366]) ).
fof(f474,plain,
double_divide(sF0_fnc,inverse(identity)) = inverse(inverse(inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f264,f459]) ).
fof(f481,plain,
! [X0] : inverse(inverse(inverse(sF0_fnc))) = double_divide(multiply(X0,sF0_fnc),inverse(X0)),
inference(backward_demodulation,[status(thm)],[f474,f386]) ).
fof(f497,plain,
! [X0,X1,X2] : multiply(inverse(identity),double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),double_divide(X1,identity)))) = double_divide(X2,identity),
inference(forward_demodulation,[status(thm)],[f8,f28]) ).
fof(f498,plain,
! [X0,X1,X2] : multiply(inverse(identity),double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1)))) = double_divide(X2,identity),
inference(forward_demodulation,[status(thm)],[f8,f497]) ).
fof(f499,plain,
! [X0,X1,X2] : multiply(inverse(identity),double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1)))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f8,f498]) ).
fof(f523,plain,
! [X0,X1,X2] : double_divide(inverse(X0),inverse(identity)) = inverse(multiply(inverse(identity),double_divide(X1,double_divide(double_divide(double_divide(X1,X2),X0),inverse(X2))))),
inference(paramodulation,[status(thm)],[f499,f366]) ).
fof(f539,plain,
! [X0] : double_divide(inverse(X0),inverse(identity)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f499,f523]) ).
fof(f601,plain,
double_divide(sF0_fnc,inverse(identity)) = inverse(inverse(inverse(a2))),
inference(paramodulation,[status(thm)],[f267,f539]) ).
fof(f611,plain,
! [X0] : multiply(inverse(identity),inverse(X0)) = inverse(inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f539,f249]) ).
fof(f612,plain,
inverse(inverse(inverse(sF0_fnc))) = inverse(inverse(inverse(a2))),
inference(forward_demodulation,[status(thm)],[f474,f601]) ).
fof(f613,plain,
inverse(inverse(inverse(sF0_fnc))) = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f267,f612]) ).
fof(f703,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),inverse(identity)) = double_divide(inverse(double_divide(inverse(X0),X1)),inverse(X1)),
inference(paramodulation,[status(thm)],[f8,f253]) ).
fof(f747,plain,
! [X0,X1] : double_divide(inverse(X0),inverse(identity)) = double_divide(inverse(double_divide(inverse(X0),X1)),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f8,f703]) ).
fof(f748,plain,
! [X0,X1] : inverse(inverse(X0)) = double_divide(inverse(double_divide(inverse(X0),X1)),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f539,f747]) ).
fof(f749,plain,
! [X0,X1] : inverse(inverse(X0)) = double_divide(multiply(X1,inverse(X0)),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f249,f748]) ).
fof(f902,plain,
! [X0] : inverse(sF0_fnc) = double_divide(multiply(X0,sF0_fnc),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f613,f481]) ).
fof(f905,plain,
inverse(sF0_fnc) = double_divide(inverse(identity),inverse(inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f263,f902]) ).
fof(f964,plain,
! [X0] : inverse(inverse(X0)) = inverse(multiply(identity,inverse(X0))),
inference(paramodulation,[status(thm)],[f366,f749]) ).
fof(f990,plain,
! [X0] : inverse(inverse(X0)) = inverse(inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f264,f964]) ).
fof(f1015,plain,
inverse(inverse(a2)) = inverse(inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f267,f990]) ).
fof(f1035,plain,
sF0_fnc = inverse(inverse(sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f267,f1015]) ).
fof(f1044,plain,
inverse(sF0_fnc) = double_divide(inverse(identity),sF0_fnc),
inference(backward_demodulation,[status(thm)],[f1035,f905]) ).
fof(f1105,plain,
multiply(sF0_fnc,inverse(identity)) = inverse(inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f1044,f249]) ).
fof(f1106,plain,
multiply(sF0_fnc,inverse(identity)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1035,f1105]) ).
fof(f1107,plain,
inverse(inverse(identity)) = double_divide(sF0_fnc,inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f1106,f749]) ).
fof(f1114,plain,
inverse(inverse(identity)) = identity,
inference(forward_demodulation,[status(thm)],[f9,f1107]) ).
fof(f1132,plain,
multiply(inverse(identity),identity) = inverse(inverse(inverse(inverse(identity)))),
inference(paramodulation,[status(thm)],[f1114,f611]) ).
fof(f1149,plain,
inverse(identity) = inverse(inverse(inverse(inverse(identity)))),
inference(forward_demodulation,[status(thm)],[f263,f1132]) ).
fof(f1150,plain,
inverse(identity) = inverse(inverse(identity)),
inference(forward_demodulation,[status(thm)],[f990,f1149]) ).
fof(f1151,plain,
inverse(identity) = identity,
inference(forward_demodulation,[status(thm)],[f1114,f1150]) ).
fof(f1164,plain,
inverse(sF0_fnc) = double_divide(identity,sF0_fnc),
inference(backward_demodulation,[status(thm)],[f1151,f1044]) ).
fof(f1179,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1))),identity) = X2,
inference(backward_demodulation,[status(thm)],[f1151,f261]) ).
fof(f1206,plain,
! [X0,X1,X2] : inverse(double_divide(X0,double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1)))) = X2,
inference(forward_demodulation,[status(thm)],[f8,f1179]) ).
fof(f1207,plain,
! [X0,X1,X2] : multiply(double_divide(double_divide(double_divide(X0,X1),X2),inverse(X1)),X0) = X2,
inference(forward_demodulation,[status(thm)],[f249,f1206]) ).
fof(f1263,plain,
! [X0,X1] : multiply(double_divide(double_divide(inverse(X0),X1),inverse(identity)),X0) = X1,
inference(paramodulation,[status(thm)],[f8,f1207]) ).
fof(f1275,plain,
! [X0,X1] : multiply(double_divide(double_divide(inverse(X0),X1),identity),X0) = X1,
inference(forward_demodulation,[status(thm)],[f1151,f1263]) ).
fof(f1276,plain,
! [X0,X1] : multiply(inverse(double_divide(inverse(X0),X1)),X0) = X1,
inference(forward_demodulation,[status(thm)],[f8,f1275]) ).
fof(f1277,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X1)),X1) = X0,
inference(forward_demodulation,[status(thm)],[f249,f1276]) ).
fof(f1283,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,inverse(X1))),identity) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f1151,f302]) ).
fof(f1284,plain,
! [X0,X1] : inverse(double_divide(X0,double_divide(identity,inverse(X1)))) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f8,f1283]) ).
fof(f1285,plain,
! [X0,X1] : multiply(double_divide(identity,inverse(X0)),X1) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f249,f1284]) ).
fof(f1341,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X1)),X1) = double_divide(identity,inverse(X0)),
inference(paramodulation,[status(thm)],[f1285,f1277]) ).
fof(f1357,plain,
! [X0] : X0 = double_divide(identity,inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1277,f1341]) ).
fof(f1366,plain,
inverse(a2) = double_divide(identity,sF0_fnc),
inference(paramodulation,[status(thm)],[f267,f1357]) ).
fof(f1374,plain,
inverse(a2) = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f1164,f1366]) ).
fof(f1435,plain,
a2 = double_divide(identity,inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f1374,f1357]) ).
fof(f1446,plain,
a2 = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f1357,f1435]) ).
fof(f1447,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1446,f12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP485-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/5.37 % Computer : n015.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 20:17:57 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.38 % Drodi V4.1.1
% 0.15/5.40 % Refutation found
% 0.15/5.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.42 % Elapsed time: 0.040257 seconds
% 0.15/5.42 % CPU time: 0.174268 seconds
% 0.15/5.42 % Total memory used: 8.634 MB
% 0.15/5.42 % Net memory used: 8.022 MB
%------------------------------------------------------------------------------