%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP438-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 : n004.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 75.91s 10.06s
% Output : CNFRefutation 75.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 2
% Syntax : Number of formulae : 72 ( 72 unt; 0 def)
% Number of atoms : 72 ( 71 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 260 ( 260 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : multiply(A,inverse(multiply(B,multiply(C,multiply(multiply(inverse(C),inverse(multiply(D,B))),A))))) = D,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0))))) = X3,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f11,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))),multiply(X4,multiply(X2,X0))))) = X3,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f16,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X4,X0))))) = multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X2,X4))),inverse(X1))),
inference(paramodulation,[status(thm)],[f3,f11]) ).
fof(f17,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(X4,X0))))) = inverse(multiply(multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X6,X2))),inverse(X7))),multiply(X7,multiply(X6,X4)))),
inference(paramodulation,[status(thm)],[f11,f11]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),X3)))),inverse(multiply(multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X3,X5))),inverse(X6))),multiply(X6,X2)))) = X5,
inference(paramodulation,[status(thm)],[f3,f11]) ).
fof(f24,plain,
! [X0,X1,X2,X3] : X0 = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),inverse(multiply(X3,X0))),X3))),inverse(X2))),
inference(paramodulation,[status(thm)],[f11,f16]) ).
fof(f58,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(X0),inverse(multiply(X1,multiply(X2,inverse(multiply(multiply(X0,multiply(X3,inverse(X4))),multiply(X4,multiply(X1,X2)))))))) = X3,
inference(paramodulation,[status(thm)],[f16,f3]) ).
fof(f127,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(multiply(inverse(X1),inverse(multiply(X2,multiply(X0,multiply(X3,inverse(X1)))))),X2))) = X3,
inference(paramodulation,[status(thm)],[f3,f58]) ).
fof(f178,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(X3,X0))))) = multiply(inverse(X4),inverse(multiply(X1,multiply(X2,multiply(X3,inverse(X4)))))),
inference(paramodulation,[status(thm)],[f127,f3]) ).
fof(f256,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(X0,multiply(X3,X1))))),X2))) = X3,
inference(paramodulation,[status(thm)],[f178,f127]) ).
fof(f262,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(multiply(X4,inverse(multiply(X5,multiply(X1,multiply(X2,X4))))),X0))))) = X5,
inference(paramodulation,[status(thm)],[f178,f3]) ).
fof(f305,plain,
! [X0,X1,X2,X3,X4] : X0 = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,multiply(X3,inverse(multiply(X0,multiply(X4,multiply(X2,X3)))))))),inverse(X4))),
inference(paramodulation,[status(thm)],[f256,f24]) ).
fof(f1350,plain,
! [X0,X1,X2,X3,X4] : X0 = inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,multiply(X3,X0)))),inverse(X4))),multiply(X4,multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f11,f17]) ).
fof(f1570,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,multiply(X1,inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(X3)),inverse(X4))),multiply(X4,multiply(X0,X1)))))) = X3,
inference(paramodulation,[status(thm)],[f17,f11]) ).
fof(f1632,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(multiply(X3,X0),X1))),X3)))),
inference(paramodulation,[status(thm)],[f24,f1350]) ).
fof(f1776,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : X0 = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,multiply(X4,X5)))),inverse(X6))),multiply(X6,multiply(X3,X4)))),inverse(multiply(X7,X0))),X7))),X5)),
inference(paramodulation,[status(thm)],[f1350,f24]) ).
fof(f1789,plain,
! [X0,X1,X2,X3] : X0 = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(X2,inverse(multiply(X3,X0))),X3))),X2)),
inference(forward_demodulation,[status(thm)],[f1350,f1776]) ).
fof(f1792,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(X1,inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),X0),X1))))),X2)),
inference(paramodulation,[status(thm)],[f305,f1632]) ).
fof(f2075,plain,
! [X0,X1,X2,X3] : inverse(multiply(multiply(X0,inverse(multiply(X1,X2))),X1)) = inverse(multiply(multiply(X0,inverse(multiply(X3,X2))),X3)),
inference(paramodulation,[status(thm)],[f1789,f1792]) ).
fof(f2123,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(multiply(inverse(X0),X1),X2)) = multiply(X3,multiply(multiply(inverse(X3),X1),X2)),
inference(paramodulation,[status(thm)],[f1792,f1789]) ).
fof(f3605,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(X3)),X0))))),X1) = X3,
inference(paramodulation,[status(thm)],[f262,f1570]) ).
fof(f3659,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(X0,multiply(X1,inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(multiply(X3,inverse(multiply(X4,X5))),X4))),inverse(X6))),multiply(X6,multiply(X0,X1)))))) = multiply(multiply(X3,inverse(multiply(X7,X5))),X7),
inference(paramodulation,[status(thm)],[f2075,f1570]) ).
fof(f3813,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,inverse(multiply(X1,X2))),X1) = multiply(multiply(X0,inverse(multiply(X3,X2))),X3),
inference(forward_demodulation,[status(thm)],[f1570,f3659]) ).
fof(f3940,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X3))))) = X0,
inference(paramodulation,[status(thm)],[f3813,f3]) ).
fof(f4782,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X3))))),X4)) = multiply(X5,multiply(inverse(X5),X4)),
inference(paramodulation,[status(thm)],[f3940,f2123]) ).
fof(f4849,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(X4,X2))),X4))))))),X1) = multiply(multiply(X0,inverse(X5)),X5),
inference(paramodulation,[status(thm)],[f3940,f3813]) ).
fof(f4901,plain,
! [X0,X1,X2] : multiply(X0,multiply(inverse(X0),X1)) = multiply(X2,multiply(inverse(X2),X1)),
inference(forward_demodulation,[status(thm)],[f3940,f4782]) ).
fof(f4907,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X1)),X1) = multiply(multiply(X0,inverse(X2)),X2),
inference(forward_demodulation,[status(thm)],[f3940,f4849]) ).
fof(f5277,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(X0)) = multiply(X1,multiply(inverse(X1),inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(X4,X2))),X4)))))),
inference(paramodulation,[status(thm)],[f3940,f4901]) ).
fof(f5567,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f3940,f5277]) ).
fof(f5569,plain,
! [X0,X1,X2,X3] : multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),X2))) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f3940,f5567]) ).
fof(f5595,plain,
! [X0,X1,X2] : multiply(X0,multiply(inverse(X0),inverse(inverse(X1)))) = multiply(X1,multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f5567,f4901]) ).
fof(f6248,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(multiply(X1,inverse(X2)),X2),
inference(paramodulation,[status(thm)],[f5567,f4907]) ).
fof(f35094,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(multiply(inverse(X2),inverse(multiply(X3,multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X6))),inverse(X2)))))),X3),X0))),X5)))),inverse(multiply(X7,inverse(X7)))) = X6,
inference(paramodulation,[status(thm)],[f5569,f20]) ).
fof(f35434,plain,
! [X0,X1,X2,X3,X4,X5] : X0 = inverse(multiply(inverse(multiply(X1,X0)),multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X3))),X5))))),X1)))),
inference(paramodulation,[status(thm)],[f5569,f1632]) ).
fof(f35570,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),X1) = multiply(multiply(X0,inverse(multiply(X3,multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X3))),X5))))),X2),
inference(paramodulation,[status(thm)],[f5569,f3813]) ).
fof(f35584,plain,
! [X0,X1,X2,X3,X4,X5] : inverse(X0) = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(X2,inverse(multiply(X3,multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X5,X3))),X5))))),X0))),X2)),
inference(paramodulation,[status(thm)],[f5569,f1789]) ).
fof(f35627,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(X2,X3),X0))),X2)))),inverse(multiply(X4,inverse(X4)))) = X3,
inference(forward_demodulation,[status(thm)],[f3605,f35094]) ).
fof(f35628,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = X0,
inference(forward_demodulation,[status(thm)],[f1632,f35627]) ).
fof(f35639,plain,
! [X0,X1,X2] : X0 = inverse(multiply(inverse(multiply(X1,X0)),multiply(X2,multiply(inverse(X2),X1)))),
inference(forward_demodulation,[status(thm)],[f3940,f35434]) ).
fof(f35695,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(multiply(X1,inverse(X2)))),X1) = multiply(X0,X2),
inference(forward_demodulation,[status(thm)],[f3940,f35570]) ).
fof(f35704,plain,
! [X0,X1,X2] : inverse(X0) = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X0))),X2)),
inference(forward_demodulation,[status(thm)],[f3940,f35584]) ).
fof(f37106,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(X1,multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f35628,f6248]) ).
fof(f48071,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f35695,f35704]) ).
fof(f48655,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = multiply(X0,multiply(X1,inverse(X1))),
inference(backward_demodulation,[status(thm)],[f48071,f5595]) ).
fof(f48657,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(multiply(X1,X0)),inverse(inverse(X1)))),
inference(backward_demodulation,[status(thm)],[f48071,f35639]) ).
fof(f48674,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = multiply(multiply(X1,inverse(X1)),X0),
inference(paramodulation,[status(thm)],[f37106,f48071]) ).
fof(f48739,plain,
! [X0,X1] : inverse(inverse(inverse(multiply(X0,inverse(X0))))) = multiply(X1,inverse(X1)),
inference(paramodulation,[status(thm)],[f35628,f48071]) ).
fof(f50584,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),inverse(multiply(X2,X1))) = multiply(X0,inverse(X2)),
inference(paramodulation,[status(thm)],[f48657,f35695]) ).
fof(f56954,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(X0,inverse(X1))),inverse(multiply(X2,multiply(X3,multiply(inverse(X3),inverse(X0)))))),X2) = X1,
inference(paramodulation,[status(thm)],[f50584,f3605]) ).
fof(f57204,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(X1))),inverse(multiply(X2,inverse(inverse(inverse(X0)))))),X2) = X1,
inference(forward_demodulation,[status(thm)],[f48071,f56954]) ).
fof(f57205,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),inverse(inverse(X0))) = X1,
inference(forward_demodulation,[status(thm)],[f35695,f57204]) ).
fof(f58317,plain,
! [X0,X1] : multiply(X0,inverse(inverse(inverse(multiply(X1,X0))))) = inverse(X1),
inference(paramodulation,[status(thm)],[f48657,f57205]) ).
fof(f58637,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X1,inverse(X1))) = inverse(X0),
inference(paramodulation,[status(thm)],[f48739,f58317]) ).
fof(f59006,plain,
! [X0] : inverse(inverse(inverse(inverse(inverse(X0))))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f48655,f58637]) ).
fof(f59021,plain,
! [X0,X1] : inverse(inverse(inverse(inverse(X0)))) = inverse(multiply(inverse(multiply(X1,X0)),inverse(inverse(X1)))),
inference(paramodulation,[status(thm)],[f48657,f59006]) ).
fof(f59253,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f48657,f59021]) ).
fof(f59271,plain,
! [X0,X1] : X0 = multiply(multiply(X1,inverse(X1)),X0),
inference(backward_demodulation,[status(thm)],[f59253,f48674]) ).
fof(f59273,plain,
! [X0,X1] : X0 = multiply(X0,multiply(X1,inverse(X1))),
inference(backward_demodulation,[status(thm)],[f59253,f48655]) ).
fof(f61836,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(X1,X0))) = multiply(multiply(X2,inverse(X2)),inverse(X1)),
inference(paramodulation,[status(thm)],[f59271,f50584]) ).
fof(f62094,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(forward_demodulation,[status(thm)],[f59271,f61836]) ).
fof(f62663,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(X1,multiply(X2,multiply(inverse(X2),inverse(multiply(multiply(multiply(X3,inverse(X3)),X0),X1)))))),
inference(paramodulation,[status(thm)],[f59273,f1632]) ).
fof(f63054,plain,
! [X0,X1,X2] : X0 = inverse(multiply(X1,inverse(inverse(inverse(multiply(multiply(multiply(X2,inverse(X2)),X0),X1)))))),
inference(forward_demodulation,[status(thm)],[f48071,f62663]) ).
fof(f63055,plain,
! [X0,X1] : X0 = inverse(inverse(multiply(multiply(X1,inverse(X1)),X0))),
inference(forward_demodulation,[status(thm)],[f58317,f63054]) ).
fof(f63056,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f59271,f63055]) ).
fof(f74652,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(inverse(X1))),X2) = multiply(X0,multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f62094,f35695]) ).
fof(f74947,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f63056,f74652]) ).
fof(f142202,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(backward_demodulation,[status(thm)],[f74947,f4]) ).
fof(f142280,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f142202]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP438-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:13:04 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 75.91/10.06 % Refutation found
% 75.91/10.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 75.91/10.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 38.48/12.94 % Elapsed time: 12.352406 seconds
% 38.48/12.94 % CPU time: 73.352976 seconds
% 38.48/12.94 % Total memory used: 4.989 GB
% 38.48/12.94 % Net memory used: 4.958 GB
%------------------------------------------------------------------------------