%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP080-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:32:28 PM UTC 2026
% Result : Unsatisfiable 0.19s 0.52s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 5
% Syntax : Number of formulae : 84 ( 77 unt; 0 def)
% Number of atoms : 96 ( 95 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 21 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 163 ( 163 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : double_divide(double_divide(identity,double_divide(X,double_divide(Y,identity))),double_divide(double_divide(Y,double_divide(Z,X)),identity)) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : inverse(X) = double_divide(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : identity = double_divide(X,inverse(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(X0,double_divide(X1,identity))),double_divide(double_divide(X1,double_divide(X2,X0)),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(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f11,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(X0,double_divide(X1,identity))),multiply(double_divide(X2,X0),X1)) = X2,
inference(backward_demodulation,[status(thm)],[f7,f6]) ).
fof(f12,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
inference(backward_demodulation,[status(thm)],[f8,f7]) ).
fof(f13,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(X0,inverse(X1))),multiply(double_divide(X2,X0),X1)) = X2,
inference(forward_demodulation,[status(thm)],[f8,f11]) ).
fof(f14,plain,
! [X0,X1] : double_divide(double_divide(identity,identity),multiply(double_divide(X0,X1),X1)) = X0,
inference(paramodulation,[status(thm)],[f9,f13]) ).
fof(f15,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(identity,double_divide(multiply(double_divide(X0,X1),X2),inverse(X3))),multiply(X0,X3)) = double_divide(identity,double_divide(X1,inverse(X2))),
inference(paramodulation,[status(thm)],[f13,f13]) ).
fof(f17,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,inverse(X0))),multiply(inverse(X1),X0)) = X1,
inference(paramodulation,[status(thm)],[f8,f13]) ).
fof(f18,plain,
! [X0,X1] : double_divide(inverse(identity),multiply(double_divide(X0,X1),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f14]) ).
fof(f20,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(identity),
inference(paramodulation,[status(thm)],[f9,f12]) ).
fof(f21,plain,
! [X0] : multiply(identity,X0) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f23,plain,
! [X0,X1] : identity = double_divide(double_divide(X0,X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f12,f9]) ).
fof(f24,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| inverse(identity) != identity ),
inference(backward_demodulation,[status(thm)],[f20,f10]) ).
fof(f26,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| inverse(inverse(a2)) != a2
| inverse(identity) != identity ),
inference(forward_demodulation,[status(thm)],[f21,f24]) ).
fof(f28,plain,
identity = inverse(identity),
inference(paramodulation,[status(thm)],[f13,f23]) ).
fof(f37,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(multiply(X0,X1),inverse(X2))),multiply(identity,X2)) = double_divide(X1,X0),
inference(paramodulation,[status(thm)],[f23,f13]) ).
fof(f40,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| inverse(inverse(a2)) != a2
| identity != identity ),
inference(backward_demodulation,[status(thm)],[f28,f26]) ).
fof(f41,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,X1),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f28,f18]) ).
fof(f48,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(multiply(X0,X1),inverse(X2))),inverse(inverse(X2))) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f21,f37]) ).
fof(f51,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| inverse(inverse(a2)) != a2 ),
inference(trivial_equality_resolution,[status(thm)],[f40]) ).
fof(f59,plain,
! [X0] : double_divide(identity,multiply(identity,inverse(X0))) = X0,
inference(paramodulation,[status(thm)],[f9,f41]) ).
fof(f62,plain,
! [X0,X1] : multiply(multiply(double_divide(X0,X1),X1),identity) = inverse(X0),
inference(paramodulation,[status(thm)],[f41,f12]) ).
fof(f66,plain,
! [X0] : double_divide(identity,inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f21,f59]) ).
fof(f78,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(multiply(identity,X0),inverse(X1))),multiply(X2,X1)) = double_divide(identity,double_divide(inverse(X2),inverse(X0))),
inference(paramodulation,[status(thm)],[f9,f15]) ).
fof(f82,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(multiply(double_divide(identity,X0),X1),inverse(X2))),inverse(inverse(X2))) = double_divide(identity,double_divide(X0,inverse(X1))),
inference(paramodulation,[status(thm)],[f21,f15]) ).
fof(f94,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(inverse(inverse(X0)),inverse(X1))),multiply(X2,X1)) = double_divide(identity,double_divide(inverse(X2),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f21,f78]) ).
fof(f96,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,double_divide(identity,multiply(double_divide(X1,X2),X3))),multiply(X1,X0)) = double_divide(identity,double_divide(X2,inverse(X3))),
inference(backward_demodulation,[status(thm)],[f109,f15]) ).
fof(f99,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,identity)),multiply(inverse(X1),X0)) = X1,
inference(backward_demodulation,[status(thm)],[f109,f17]) ).
fof(f100,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(identity,inverse(inverse(X1)))),multiply(X2,X0)) = double_divide(identity,double_divide(inverse(X2),inverse(X1))),
inference(backward_demodulation,[status(thm)],[f109,f94]) ).
fof(f109,plain,
! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = double_divide(identity,double_divide(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f48,f82]) ).
fof(f121,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,double_divide(identity,multiply(double_divide(X1,X2),X3))),multiply(X1,X0)) = double_divide(X3,double_divide(identity,X2)),
inference(forward_demodulation,[status(thm)],[f109,f96]) ).
fof(f123,plain,
! [X0,X1] : double_divide(double_divide(X0,inverse(identity)),multiply(inverse(X1),X0)) = X1,
inference(forward_demodulation,[status(thm)],[f8,f99]) ).
fof(f124,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),multiply(inverse(X1),X0)) = X1,
inference(forward_demodulation,[status(thm)],[f28,f123]) ).
fof(f125,plain,
! [X0,X1] : double_divide(inverse(X0),multiply(inverse(X1),X0)) = X1,
inference(forward_demodulation,[status(thm)],[f8,f124]) ).
fof(f126,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(identity,inverse(inverse(X1)))),multiply(X2,X0)) = double_divide(X1,double_divide(identity,inverse(X2))),
inference(forward_demodulation,[status(thm)],[f109,f100]) ).
fof(f135,plain,
! [X0] : multiply(inverse(inverse(inverse(X0))),identity) = inverse(X0),
inference(paramodulation,[status(thm)],[f66,f12]) ).
fof(f142,plain,
! [X0] : multiply(multiply(inverse(X0),identity),identity) = inverse(X0),
inference(paramodulation,[status(thm)],[f8,f62]) ).
fof(f158,plain,
! [X0] : multiply(inverse(X0),identity) = inverse(inverse(inverse(X0))),
inference(paramodulation,[status(thm)],[f135,f142]) ).
fof(f162,plain,
! [X0] : inverse(inverse(inverse(inverse(inverse(X0))))) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f158,f135]) ).
fof(f192,plain,
! [X0] : double_divide(identity,inverse(X0)) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f162,f66]) ).
fof(f195,plain,
! [X0] : double_divide(identity,inverse(inverse(inverse(X0)))) = inverse(inverse(inverse(inverse(X0)))),
inference(paramodulation,[status(thm)],[f162,f66]) ).
fof(f202,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,inverse(inverse(inverse(X1)))),multiply(X2,X0)) = double_divide(X1,double_divide(identity,inverse(X2))),
inference(backward_demodulation,[status(thm)],[f192,f126]) ).
fof(f209,plain,
! [X0] : X0 = inverse(inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[status(thm)],[f66,f195]) ).
fof(f211,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,inverse(inverse(inverse(X1)))),multiply(X2,X0)) = double_divide(X1,inverse(inverse(X2))),
inference(forward_demodulation,[status(thm)],[f192,f202]) ).
fof(f238,plain,
! [X0] : double_divide(identity,X0) = inverse(inverse(inverse(inverse(inverse(X0))))),
inference(paramodulation,[status(thm)],[f209,f192]) ).
fof(f247,plain,
! [X0,X1] : inverse(multiply(double_divide(X0,X1),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f258,f41]) ).
fof(f249,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(multiply(double_divide(X1,X2),X3))),multiply(X1,X0)) = double_divide(X3,double_divide(identity,X2)),
inference(backward_demodulation,[status(thm)],[f258,f121]) ).
fof(f253,plain,
! [X0,X1] : double_divide(X0,double_divide(identity,X1)) = inverse(double_divide(X1,inverse(X0))),
inference(backward_demodulation,[status(thm)],[f258,f109]) ).
fof(f258,plain,
! [X0] : double_divide(identity,X0) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f209,f238]) ).
fof(f269,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(multiply(double_divide(X1,X2),X3))),multiply(X1,X0)) = double_divide(X3,inverse(X2)),
inference(forward_demodulation,[status(thm)],[f258,f249]) ).
fof(f272,plain,
! [X0,X1] : double_divide(X0,inverse(X1)) = inverse(double_divide(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f258,f253]) ).
fof(f273,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(backward_demodulation,[status(thm)],[f280,f9]) ).
fof(f277,plain,
! [X0,X1,X2,X3] : double_divide(multiply(inverse(X0),multiply(double_divide(X1,X2),X3)),multiply(X1,X0)) = double_divide(X3,inverse(X2)),
inference(backward_demodulation,[status(thm)],[f280,f269]) ).
fof(f279,plain,
! [X0,X1,X2] : double_divide(multiply(inverse(X0),inverse(inverse(X1))),multiply(X2,X0)) = double_divide(X1,inverse(inverse(X2))),
inference(backward_demodulation,[status(thm)],[f280,f211]) ).
fof(f280,plain,
! [X0,X1] : double_divide(X0,inverse(X1)) = multiply(inverse(X0),X1),
inference(forward_demodulation,[status(thm)],[f12,f272]) ).
fof(f288,plain,
! [X0,X1,X2,X3] : double_divide(multiply(inverse(X0),multiply(double_divide(X1,X2),X3)),multiply(X1,X0)) = multiply(inverse(X3),X2),
inference(forward_demodulation,[status(thm)],[f280,f277]) ).
fof(f290,plain,
! [X0,X1,X2] : double_divide(multiply(inverse(X0),inverse(inverse(X1))),multiply(X2,X0)) = multiply(inverse(X1),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f280,f279]) ).
fof(f335,plain,
! [X0] : double_divide(inverse(X0),identity) = X0,
inference(paramodulation,[status(thm)],[f273,f125]) ).
fof(f337,plain,
! [X0,X1] : double_divide(inverse(X0),multiply(X1,X0)) = inverse(inverse(inverse(X1))),
inference(paramodulation,[status(thm)],[f209,f125]) ).
fof(f339,plain,
! [X0,X1,X2] : double_divide(inverse(X0),multiply(multiply(X1,X2),X0)) = double_divide(X2,X1),
inference(paramodulation,[status(thm)],[f12,f125]) ).
fof(f346,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(backward_demodulation,[status(thm)],[f359,f51]) ).
fof(f357,plain,
! [X0,X1,X2] : double_divide(multiply(inverse(X0),X1),multiply(X2,X0)) = multiply(inverse(X1),inverse(X2)),
inference(backward_demodulation,[status(thm)],[f359,f290]) ).
fof(f359,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f335]) ).
fof(f364,plain,
! [X0,X1] : double_divide(inverse(X0),multiply(X1,X0)) = inverse(X1),
inference(forward_demodulation,[status(thm)],[f359,f337]) ).
fof(f367,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = X1,
inference(backward_demodulation,[status(thm)],[f369,f247]) ).
fof(f369,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f364,f339]) ).
fof(f371,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(trivial_equality_resolution,[status(thm)],[f346]) ).
fof(f376,plain,
! [X0,X1,X2] : multiply(inverse(multiply(double_divide(X0,X1),X2)),inverse(X0)) = multiply(inverse(X2),X1),
inference(backward_demodulation,[status(thm)],[f357,f288]) ).
fof(f383,plain,
! [X0,X1,X2] : multiply(double_divide(X0,double_divide(X1,X2)),inverse(X1)) = multiply(inverse(X0),X2),
inference(forward_demodulation,[status(thm)],[f369,f376]) ).
fof(f460,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
inference(paramodulation,[status(thm)],[f367,f367]) ).
fof(f844,plain,
! [X0,X1,X2] : multiply(X0,inverse(X1)) = multiply(inverse(double_divide(double_divide(X1,X2),X0)),X2),
inference(paramodulation,[status(thm)],[f460,f383]) ).
fof(f870,plain,
! [X0,X1,X2] : multiply(X0,inverse(X1)) = multiply(multiply(X0,double_divide(X1,X2)),X2),
inference(forward_demodulation,[status(thm)],[f12,f844]) ).
fof(f1716,plain,
! [X0,X1,X2] : multiply(X0,inverse(double_divide(X1,X2))) = multiply(multiply(X0,X2),X1),
inference(paramodulation,[status(thm)],[f460,f870]) ).
fof(f1751,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(backward_demodulation,[status(thm)],[f1774,f371]) ).
fof(f1774,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(multiply(X0,X1),X2),
inference(forward_demodulation,[status(thm)],[f12,f1716]) ).
fof(f1806,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f1751]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP080-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n019.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 20 19:56:50 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 0.19/0.52 % Refutation found
% 0.19/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.19/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/0.56 % Elapsed time: 0.106348 seconds
% 0.19/0.56 % CPU time: 0.358015 seconds
% 0.19/0.56 % Total memory used: 36.853 MB
% 0.19/0.56 % Net memory used: 36.027 MB
%------------------------------------------------------------------------------