%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP072-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 : n018.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:27 PM UTC 2026
% Result : Unsatisfiable 80.89s 10.66s
% Output : CNFRefutation 71.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 3
% Syntax : Number of formulae : 80 ( 75 unt; 0 def)
% Number of atoms : 89 ( 88 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 25 ( 16 ~; 9 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 287 ( 287 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z,U] : divide(divide(inverse(divide(X,Y)),divide(divide(Z,U),X)),divide(U,Z)) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = divide(X,inverse(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f7,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1)) = divide(X5,X4),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f8,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2)) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f10,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),divide(inverse(X4),divide(divide(X5,X6),divide(inverse(divide(X7,X4)),divide(divide(X1,X0),X7)))))),divide(X3,X2)) = divide(X6,X5),
inference(paramodulation,[status(thm)],[f4,f7]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1)) = divide(divide(divide(X4,X3),X6),inverse(divide(X6,X5))),
inference(paramodulation,[status(thm)],[f4,f7]) ).
fof(f28,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1)) = divide(divide(X6,X7),divide(inverse(X8),divide(divide(X7,X6),divide(inverse(divide(X9,X8)),divide(divide(X5,X4),X9))))),
inference(paramodulation,[status(thm)],[f7,f7]) ).
fof(f41,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1)) = multiply(divide(divide(X4,X3),X6),divide(X6,X5)),
inference(forward_demodulation,[status(thm)],[f5,f24]) ).
fof(f43,plain,
! [X0,X1,X2,X3,X4,X5] : divide(X0,X1) = divide(divide(X2,X3),divide(inverse(X4),divide(divide(X3,X2),divide(inverse(divide(X5,X4)),divide(divide(X0,X1),X5))))),
inference(forward_demodulation,[status(thm)],[f7,f28]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(divide(divide(X0,X1),X2)),inverse(X3)),divide(divide(divide(X1,X0),X4),inverse(multiply(X4,X3)))) = X2,
inference(paramodulation,[status(thm)],[f8,f4]) ).
fof(f77,plain,
! [X0,X1,X2,X3,X4] : divide(multiply(inverse(divide(divide(X0,X1),X2)),X3),divide(divide(divide(X1,X0),X4),inverse(multiply(X4,X3)))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f59]) ).
fof(f78,plain,
! [X0,X1,X2,X3,X4] : divide(multiply(inverse(divide(divide(X0,X1),X2)),X3),multiply(divide(divide(X1,X0),X4),multiply(X4,X3))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f77]) ).
fof(f95,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(divide(divide(X0,X1),X2)),X3),divide(multiply(divide(X1,X0),X4),inverse(divide(inverse(X4),X3)))) = X2,
inference(paramodulation,[status(thm)],[f10,f4]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(divide(divide(X0,X1),X2)),X3),multiply(multiply(divide(X1,X0),X4),divide(inverse(X4),X3))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f95]) ).
fof(f4598,plain,
! [X0,X1,X2,X3,X4] : multiply(divide(divide(X0,X1),X2),divide(X2,X3)) = multiply(divide(divide(X0,X1),X4),divide(X4,X3)),
inference(paramodulation,[status(thm)],[f41,f41]) ).
fof(f5159,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(divide(X0,X1),divide(X1,X2)) = multiply(divide(divide(multiply(inverse(divide(divide(X3,X4),X0)),X5),multiply(divide(divide(X4,X3),X6),multiply(X6,X5))),X7),divide(X7,X2)),
inference(paramodulation,[status(thm)],[f78,f4598]) ).
fof(f5377,plain,
! [X0,X1,X2,X3] : multiply(divide(X0,X1),divide(X1,X2)) = multiply(divide(X0,X3),divide(X3,X2)),
inference(forward_demodulation,[status(thm)],[f78,f5159]) ).
fof(f5477,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,X1),divide(inverse(X1),X2)) = multiply(divide(X0,X3),divide(X3,X2)),
inference(paramodulation,[status(thm)],[f5,f5377]) ).
fof(f5510,plain,
! [X0,X1,X2,X3] : multiply(divide(X0,X1),multiply(X1,X2)) = multiply(divide(X0,X3),divide(X3,inverse(X2))),
inference(paramodulation,[status(thm)],[f5,f5377]) ).
fof(f5638,plain,
! [X0,X1,X2,X3] : multiply(divide(X0,X1),multiply(X1,X2)) = multiply(divide(X0,X3),multiply(X3,X2)),
inference(forward_demodulation,[status(thm)],[f5,f5510]) ).
fof(f5674,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,X1),multiply(inverse(X1),X2)) = multiply(divide(X0,X3),multiply(X3,X2)),
inference(paramodulation,[status(thm)],[f5,f5638]) ).
fof(f7918,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3)) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f43,f21]) ).
fof(f10628,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3)) = divide(divide(X3,X2),divide(inverse(divide(X4,X5)),divide(X5,X4))),
inference(paramodulation,[status(thm)],[f7918,f7918]) ).
fof(f10855,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = divide(divide(X0,X1),divide(inverse(divide(X2,X3)),divide(X3,X2))),
inference(forward_demodulation,[status(thm)],[f7918,f10628]) ).
fof(f10982,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(multiply(inverse(divide(divide(X0,X1),X2)),X3),multiply(divide(divide(X1,X0),X4),multiply(X4,X3))) = divide(X2,divide(inverse(divide(X5,X6)),divide(X6,X5))),
inference(paramodulation,[status(thm)],[f78,f10855]) ).
fof(f11321,plain,
! [X0,X1,X2] : X0 = divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f78,f10982]) ).
fof(f11504,plain,
! [X0,X1,X2] : X0 = divide(X0,inverse(divide(divide(X1,X2),inverse(divide(X2,X1))))),
inference(paramodulation,[status(thm)],[f11321,f11321]) ).
fof(f11610,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(X0,X1),inverse(X1)) = multiply(divide(X0,X2),divide(X2,divide(inverse(divide(X3,X4)),divide(X4,X3)))),
inference(paramodulation,[status(thm)],[f11321,f5477]) ).
fof(f11840,plain,
! [X0,X1,X2] : X0 = multiply(X0,divide(divide(X1,X2),inverse(divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f5,f11504]) ).
fof(f11841,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(divide(X1,X2),divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f5,f11840]) ).
fof(f11874,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),inverse(X1)) = multiply(divide(X0,X2),X2),
inference(forward_demodulation,[status(thm)],[f11321,f11610]) ).
fof(f12162,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(divide(inverse(X1),X2),multiply(X2,X1))),
inference(paramodulation,[status(thm)],[f5,f11841]) ).
fof(f15479,plain,
! [X0,X1,X2,X3] : divide(X0,divide(inverse(X1),X2)) = multiply(multiply(X0,X3),multiply(inverse(X3),multiply(X2,X1))),
inference(paramodulation,[status(thm)],[f5674,f12162]) ).
fof(f15620,plain,
! [X0,X1,X2,X3] : divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))) = multiply(multiply(X0,X3),inverse(X3)),
inference(paramodulation,[status(thm)],[f11841,f15479]) ).
fof(f15677,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f11321,f15620]) ).
fof(f15693,plain,
! [X0,X1] : X0 = multiply(divide(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f15677,f11874]) ).
fof(f15711,plain,
! [X0,X1,X2] : X0 = multiply(X0,inverse(multiply(divide(X1,X2),divide(X2,X1)))),
inference(paramodulation,[status(thm)],[f11841,f15677]) ).
fof(f15814,plain,
! [X0,X1] : divide(X0,X1) = multiply(X0,inverse(X1)),
inference(paramodulation,[status(thm)],[f15693,f15677]) ).
fof(f15851,plain,
! [X0,X1] : X0 = divide(multiply(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f15814,f15677]) ).
fof(f15965,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = divide(multiply(divide(X0,X2),divide(X2,X3)),divide(X1,X3)),
inference(paramodulation,[status(thm)],[f5377,f15851]) ).
fof(f16049,plain,
! [X0,X1,X2,X3] : multiply(divide(multiply(X0,X1),X2),multiply(X2,X3)) = multiply(X0,multiply(X1,X3)),
inference(paramodulation,[status(thm)],[f15851,f5638]) ).
fof(f18677,plain,
! [X0,X1,X2] : X0 = divide(X0,multiply(divide(X1,X2),divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f15814,f15711]) ).
fof(f20163,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = divide(multiply(divide(X0,multiply(X2,X3)),X2),divide(X1,X3)),
inference(paramodulation,[status(thm)],[f15851,f15965]) ).
fof(f20506,plain,
! [X0,X1,X2,X3] : divide(multiply(X0,X1),divide(X2,X3)) = multiply(X0,multiply(X1,divide(X3,X2))),
inference(paramodulation,[status(thm)],[f11841,f16049]) ).
fof(f20549,plain,
! [X0,X1,X2,X3] : multiply(divide(multiply(X0,X1),divide(X2,X3)),X2) = multiply(X0,multiply(X1,X3)),
inference(paramodulation,[status(thm)],[f15693,f16049]) ).
fof(f21010,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = divide(multiply(X0,divide(X2,X3)),divide(X1,divide(X3,X2))),
inference(paramodulation,[status(thm)],[f18677,f20163]) ).
fof(f23541,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,multiply(X1,divide(X2,X3))),X3) = multiply(X0,multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f20506,f20549]) ).
fof(f23557,plain,
! [X0,X1,X2,X3] : multiply(X0,X1) = multiply(divide(X0,multiply(X2,divide(X3,X1))),multiply(X2,X3)),
inference(paramodulation,[status(thm)],[f15693,f23541]) ).
fof(f23715,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = multiply(X0,multiply(divide(X2,X3),divide(divide(X3,X2),X1))),
inference(forward_demodulation,[status(thm)],[f20506,f21010]) ).
fof(f24603,plain,
! [X0,X1,X2,X3,X4] : multiply(divide(inverse(divide(divide(X0,X1),X2)),X3),X3) = multiply(X2,multiply(multiply(divide(X1,X0),X4),inverse(X4))),
inference(paramodulation,[status(thm)],[f110,f23557]) ).
fof(f24766,plain,
! [X0,X1,X2,X3] : inverse(divide(divide(X0,X1),X2)) = multiply(X2,multiply(multiply(divide(X1,X0),X3),inverse(X3))),
inference(forward_demodulation,[status(thm)],[f15693,f24603]) ).
fof(f24767,plain,
! [X0,X1,X2,X3] : inverse(divide(divide(X0,X1),X2)) = multiply(X2,divide(multiply(divide(X1,X0),X3),X3)),
inference(forward_demodulation,[status(thm)],[f15814,f24766]) ).
fof(f24768,plain,
! [X0,X1,X2] : inverse(divide(divide(X0,X1),X2)) = multiply(X2,divide(X1,X0)),
inference(forward_demodulation,[status(thm)],[f15851,f24767]) ).
fof(f26440,plain,
! [X0,X1,X2,X3] : inverse(divide(X0,X1)) = multiply(divide(X1,X0),divide(divide(X2,X3),inverse(divide(X3,X2)))),
inference(paramodulation,[status(thm)],[f7918,f24768]) ).
fof(f26514,plain,
! [X0,X1,X2,X3] : X0 = divide(X0,divide(multiply(X1,divide(X2,X3)),divide(X1,divide(X3,X2)))),
inference(paramodulation,[status(thm)],[f24768,f11321]) ).
fof(f26550,plain,
! [X0,X1,X2,X3,X4] : X0 = multiply(X0,multiply(divide(multiply(X1,divide(X2,X3)),X4),multiply(X4,divide(divide(X3,X2),X1)))),
inference(paramodulation,[status(thm)],[f24768,f12162]) ).
fof(f26625,plain,
! [X0,X1,X2,X3] : inverse(divide(X0,X1)) = multiply(divide(X1,X0),multiply(divide(X2,X3),divide(X3,X2))),
inference(forward_demodulation,[status(thm)],[f5,f26440]) ).
fof(f26626,plain,
! [X0,X1] : inverse(divide(X0,X1)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f11841,f26625]) ).
fof(f26713,plain,
! [X0,X1,X2,X3] : X0 = divide(X0,multiply(X1,multiply(divide(X2,X3),divide(divide(X3,X2),X1)))),
inference(forward_demodulation,[status(thm)],[f20506,f26514]) ).
fof(f26714,plain,
! [X0,X1] : X0 = divide(X0,divide(X1,X1)),
inference(forward_demodulation,[status(thm)],[f23715,f26713]) ).
fof(f26775,plain,
! [X0,X1,X2,X3] : X0 = multiply(X0,multiply(X1,multiply(divide(X2,X3),divide(divide(X3,X2),X1)))),
inference(forward_demodulation,[status(thm)],[f16049,f26550]) ).
fof(f26776,plain,
! [X0,X1] : X0 = multiply(X0,divide(X1,X1)),
inference(forward_demodulation,[status(thm)],[f23715,f26775]) ).
fof(f27370,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(paramodulation,[status(thm)],[f26776,f23541]) ).
fof(f29740,plain,
! [X0,X1] : inverse(X0) = divide(divide(X1,X1),X0),
inference(paramodulation,[status(thm)],[f26714,f26626]) ).
fof(f30004,plain,
! [X0,X1] : inverse(divide(X0,X0)) = divide(X1,X1),
inference(paramodulation,[status(thm)],[f26714,f29740]) ).
fof(f30044,plain,
! [X0,X1] : divide(X0,X0) = multiply(inverse(X1),X1),
inference(paramodulation,[status(thm)],[f29740,f15693]) ).
fof(f30080,plain,
! [X0,X1] : divide(X0,X0) = divide(X1,X1),
inference(forward_demodulation,[status(thm)],[f26626,f30004]) ).
fof(f30226,plain,
! [X0,X1] : X0 = multiply(divide(X1,X1),X0),
inference(paramodulation,[status(thm)],[f30080,f15693]) ).
fof(f31589,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(paramodulation,[status(thm)],[f5,f30044]) ).
fof(f31698,plain,
! [X0] :
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(divide(X0,X0),a2) != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(paramodulation,[status(thm)],[f30044,f6]) ).
fof(f31825,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(forward_demodulation,[status(thm)],[f30226,f31698]) ).
fof(f31826,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ),
inference(trivial_equality_resolution,[status(thm)],[f31825]) ).
fof(f34133,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(backward_subsumption_resolution,[status(thm)],[f31826,f31589]) ).
fof(f35293,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(backward_demodulation,[status(thm)],[f27370,f34133]) ).
fof(f35327,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f35293]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP072-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.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 19:58:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 80.89/10.66 % Refutation found
% 80.89/10.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 80.89/10.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 74.90/10.80 % Elapsed time: 10.406972 seconds
% 74.90/10.80 % CPU time: 82.212026 seconds
% 74.90/10.80 % Total memory used: 876.141 MB
% 74.90/10.80 % Net memory used: 870.279 MB
%------------------------------------------------------------------------------