%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP472-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 : n010.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:27 PM UTC 2026
% Result : Unsatisfiable 137.52s 28.00s
% Output : CNFRefutation 137.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 3
% Syntax : Number of formulae : 78 ( 78 unt; 0 def)
% Number of atoms : 78 ( 77 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 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 : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 332 ( 332 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : divide(divide(inverse(divide(A,B)),divide(divide(C,D),A)),divide(D,C)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
multiply(inverse(a1),a1) != multiply(inverse(b1),b1),
file('/export/starexec/sandbox/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(inverse(a1),a1) != multiply(inverse(b1),b1),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f12,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(f13,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(f15,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(f19,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(X2),X3),X0)),multiply(X3,X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f26,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(multiply(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2)) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f13]) ).
fof(f29,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(multiply(X0,X1)),divide(divide(inverse(X2),X3),X0)),multiply(X3,X2)) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f13]) ).
fof(f30,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)],[f13,f4]) ).
fof(f38,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,f30]) ).
fof(f39,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,f38]) ).
fof(f46,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(divide(X2,X3),divide(inverse(multiply(X4,X5)),divide(divide(X3,X2),X4))),X0)),inverse(X5)) = X1,
inference(paramodulation,[status(thm)],[f13,f15]) ).
fof(f57,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(divide(inverse(divide(inverse(X0),X1)),multiply(divide(divide(X2,X3),divide(inverse(multiply(X4,X5)),divide(divide(X3,X2),X4))),X0)),X5) = X1,
inference(forward_demodulation,[status(thm)],[f5,f46]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),inverse(X1)),divide(divide(divide(divide(divide(X2,X3),X4),inverse(divide(X4,X0))),X5),inverse(multiply(X5,X1)))) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f13,f12]) ).
fof(f71,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,f12]) ).
fof(f74,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(divide(X3,X4),X0)),inverse(X5)))),divide(X2,X1)) = divide(divide(divide(X4,X3),X6),inverse(multiply(X6,X5))),
inference(paramodulation,[status(thm)],[f13,f12]) ).
fof(f82,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)],[f12,f12]) ).
fof(f98,plain,
! [X0,X1,X2,X3,X4,X5] : divide(multiply(inverse(X0),X1),divide(divide(divide(divide(divide(X2,X3),X4),inverse(divide(X4,X0))),X5),inverse(multiply(X5,X1)))) = divide(X3,X2),
inference(forward_demodulation,[status(thm)],[f5,f60]) ).
fof(f99,plain,
! [X0,X1,X2,X3,X4,X5] : divide(multiply(inverse(X0),X1),multiply(divide(divide(divide(divide(X2,X3),X4),inverse(divide(X4,X0))),X5),multiply(X5,X1))) = divide(X3,X2),
inference(forward_demodulation,[status(thm)],[f5,f98]) ).
fof(f100,plain,
! [X0,X1,X2,X3,X4,X5] : divide(multiply(inverse(X0),X1),multiply(divide(multiply(divide(divide(X2,X3),X4),divide(X4,X0)),X5),multiply(X5,X1))) = divide(X3,X2),
inference(forward_demodulation,[status(thm)],[f5,f99]) ).
fof(f107,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1)) = divide(divide(divide(X4,X3),X6),inverse(multiply(X6,X5))),
inference(forward_demodulation,[status(thm)],[f5,f74]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(divide(inverse(X0),divide(divide(X1,X2),multiply(inverse(divide(divide(X3,X4),X0)),X5))),divide(X2,X1)) = multiply(divide(divide(X4,X3),X6),multiply(X6,X5)),
inference(forward_demodulation,[status(thm)],[f5,f107]) ).
fof(f112,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)],[f12,f82]) ).
fof(f229,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(multiply(X0,X1)),divide(multiply(inverse(X2),X3),X0)),multiply(inverse(X3),X2)) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f26]) ).
fof(f707,plain,
! [X0,X1,X2,X3,X4,X5] : divide(multiply(inverse(divide(divide(divide(divide(X0,X1),X2),inverse(divide(X2,X3))),X4)),X5),multiply(X3,multiply(divide(X1,X0),X5))) = X4,
inference(paramodulation,[status(thm)],[f4,f39]) ).
fof(f779,plain,
! [X0,X1,X2,X3,X4,X5] : divide(multiply(inverse(divide(multiply(divide(divide(X0,X1),X2),divide(X2,X3)),X4)),X5),multiply(X3,multiply(divide(X1,X0),X5))) = X4,
inference(forward_demodulation,[status(thm)],[f5,f707]) ).
fof(f1193,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(multiply(multiply(inverse(X0),X1),X2)),inverse(X3)),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3))) = inverse(X2),
inference(paramodulation,[status(thm)],[f229,f29]) ).
fof(f1194,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(divide(multiply(inverse(X0),X1),X2)),inverse(X3)),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3))) = X2,
inference(paramodulation,[status(thm)],[f229,f19]) ).
fof(f1238,plain,
! [X0,X1,X2,X3,X4] : divide(multiply(inverse(multiply(multiply(inverse(X0),X1),X2)),X3),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f5,f1193]) ).
fof(f1239,plain,
! [X0,X1,X2,X3,X4] : divide(multiply(inverse(divide(multiply(inverse(X0),X1),X2)),X3),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f1194]) ).
fof(f9640,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : divide(multiply(inverse(X0),X1),multiply(divide(multiply(divide(divide(X2,X3),X4),divide(X4,X0)),X5),multiply(X5,X1))) = divide(multiply(divide(multiply(divide(divide(X3,X2),X6),divide(X6,X7)),X8),multiply(X8,X9)),multiply(inverse(X7),X9)),
inference(paramodulation,[status(thm)],[f100,f100]) ).
fof(f9906,plain,
! [X0,X1,X2,X3,X4,X5] : divide(X0,X1) = divide(multiply(divide(multiply(divide(divide(X0,X1),X2),divide(X2,X3)),X4),multiply(X4,X5)),multiply(inverse(X3),X5)),
inference(forward_demodulation,[status(thm)],[f100,f9640]) ).
fof(f22323,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] : divide(multiply(inverse(divide(multiply(divide(divide(X0,X1),X2),divide(X2,X3)),X4)),X5),multiply(X3,multiply(divide(X1,X0),X5))) = divide(multiply(divide(multiply(divide(X4,X6),divide(X6,X7)),X8),multiply(X8,X9)),multiply(inverse(X7),X9)),
inference(paramodulation,[status(thm)],[f779,f9906]) ).
fof(f22660,plain,
! [X0,X1,X2,X3,X4] : X0 = divide(multiply(divide(multiply(divide(X0,X1),divide(X1,X2)),X3),multiply(X3,X4)),multiply(inverse(X2),X4)),
inference(forward_demodulation,[status(thm)],[f779,f22323]) ).
fof(f23188,plain,
! [X0,X1,X2,X3,X4] : multiply(divide(divide(X0,X1),X2),multiply(X2,X3)) = multiply(divide(divide(X0,X1),X4),multiply(X4,X3)),
inference(paramodulation,[status(thm)],[f108,f108]) ).
fof(f24307,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(divide(X0,X1),multiply(X1,X2)) = multiply(divide(divide(multiply(divide(multiply(divide(X0,X3),divide(X3,X4)),X5),multiply(X5,X6)),multiply(inverse(X4),X6)),X7),multiply(X7,X2)),
inference(paramodulation,[status(thm)],[f22660,f23188]) ).
fof(f24722,plain,
! [X0,X1,X2,X3] : multiply(divide(X0,X1),multiply(X1,X2)) = multiply(divide(X0,X3),multiply(X3,X2)),
inference(forward_demodulation,[status(thm)],[f22660,f24307]) ).
fof(f24968,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,f24722]) ).
fof(f34451,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3)) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f112,f71]) ).
fof(f41659,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)],[f34451,f34451]) ).
fof(f42121,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)],[f34451,f41659]) ).
fof(f42364,plain,
! [X0,X1,X2,X3,X4,X5,X6] : divide(multiply(divide(multiply(divide(X0,X1),divide(X1,X2)),X3),multiply(X3,X4)),multiply(inverse(X2),X4)) = divide(X0,divide(inverse(divide(X5,X6)),divide(X6,X5))),
inference(paramodulation,[status(thm)],[f22660,f42121]) ).
fof(f43041,plain,
! [X0,X1,X2] : X0 = divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f22660,f42364]) ).
fof(f43406,plain,
! [X0,X1,X2] : X0 = divide(X0,inverse(divide(divide(X1,X2),inverse(divide(X2,X1))))),
inference(paramodulation,[status(thm)],[f43041,f43041]) ).
fof(f44118,plain,
! [X0,X1,X2] : X0 = multiply(X0,divide(divide(X1,X2),inverse(divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f5,f43406]) ).
fof(f44119,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(divide(X1,X2),divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f5,f44118]) ).
fof(f45725,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(multiply(X1,X2),divide(inverse(X2),X1))),
inference(paramodulation,[status(thm)],[f5,f44119]) ).
fof(f45824,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(divide(inverse(X1),X2),multiply(X2,X1))),
inference(paramodulation,[status(thm)],[f5,f44119]) ).
fof(f45918,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(X0,X1),inverse(X1)) = multiply(divide(X0,X2),multiply(X2,multiply(divide(X3,X4),divide(X4,X3)))),
inference(paramodulation,[status(thm)],[f44119,f24968]) ).
fof(f45960,plain,
! [X0,X1,X2,X3,X4] : multiply(divide(X0,X1),multiply(X1,multiply(divide(X2,X3),divide(X3,X2)))) = multiply(divide(X0,X4),X4),
inference(paramodulation,[status(thm)],[f44119,f24722]) ).
fof(f46060,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),inverse(X1)) = multiply(divide(X0,X2),X2),
inference(forward_demodulation,[status(thm)],[f44119,f45918]) ).
fof(f46078,plain,
! [X0,X1,X2] : multiply(divide(X0,X1),X1) = multiply(divide(X0,X2),X2),
inference(forward_demodulation,[status(thm)],[f44119,f45960]) ).
fof(f47613,plain,
! [X0,X1,X2] : X0 = multiply(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))),
inference(paramodulation,[status(thm)],[f44119,f45824]) ).
fof(f48859,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)],[f46060,f47613]) ).
fof(f48860,plain,
! [X0,X1,X2,X3] : divide(X0,divide(inverse(divide(X1,X2)),divide(X2,X1))) = multiply(divide(X0,X3),X3),
inference(paramodulation,[status(thm)],[f46078,f47613]) ).
fof(f49288,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f43041,f48859]) ).
fof(f49289,plain,
! [X0,X1] : X0 = multiply(divide(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f43041,f48860]) ).
fof(f49424,plain,
! [X0,X1,X2] : X0 = divide(X0,multiply(divide(X1,X2),divide(X2,X1))),
inference(paramodulation,[status(thm)],[f44119,f49289]) ).
fof(f50320,plain,
! [X0,X1] : divide(X0,X1) = multiply(X0,inverse(X1)),
inference(paramodulation,[status(thm)],[f49289,f49288]) ).
fof(f50416,plain,
! [X0,X1] : X0 = divide(multiply(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f50320,f49288]) ).
fof(f50426,plain,
! [X0,X1,X2,X3,X4] : divide(multiply(inverse(divide(multiply(inverse(X0),X1),X2)),X3),multiply(divide(multiply(inverse(X1),X0),X4),multiply(X4,X3))) = inverse(inverse(X2)),
inference(paramodulation,[status(thm)],[f50320,f1238]) ).
fof(f50617,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1239,f50426]) ).
fof(f60406,plain,
! [X0,X1,X2,X3,X4] : multiply(inverse(divide(inverse(divide(divide(inverse(multiply(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2))),X4)),X1) = X4,
inference(paramodulation,[status(thm)],[f49424,f57]) ).
fof(f60973,plain,
! [X0,X1] : multiply(inverse(divide(inverse(inverse(X0)),X1)),X0) = X1,
inference(forward_demodulation,[status(thm)],[f13,f60406]) ).
fof(f60974,plain,
! [X0,X1] : multiply(inverse(divide(X0,X1)),X0) = X1,
inference(forward_demodulation,[status(thm)],[f50617,f60973]) ).
fof(f61148,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(paramodulation,[status(thm)],[f50416,f60974]) ).
fof(f61554,plain,
! [X0,X1] : inverse(X0) = divide(X1,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f61148,f50416]) ).
fof(f63010,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(multiply(multiply(X1,inverse(X2)),X2),inverse(X1))),
inference(paramodulation,[status(thm)],[f61554,f45725]) ).
fof(f63127,plain,
! [X0,X1,X2] : X0 = multiply(X0,divide(multiply(multiply(X1,inverse(X2)),X2),X1)),
inference(forward_demodulation,[status(thm)],[f50320,f63010]) ).
fof(f63128,plain,
! [X0,X1,X2] : X0 = multiply(X0,divide(multiply(divide(X1,X2),X2),X1)),
inference(forward_demodulation,[status(thm)],[f50320,f63127]) ).
fof(f63129,plain,
! [X0,X1] : X0 = multiply(X0,divide(X1,X1)),
inference(forward_demodulation,[status(thm)],[f49289,f63128]) ).
fof(f63293,plain,
! [X0,X1] : multiply(inverse(X0),X0) = divide(X1,X1),
inference(paramodulation,[status(thm)],[f63129,f61148]) ).
fof(f66136,plain,
! [X0] : multiply(inverse(a1),a1) != divide(X0,X0),
inference(paramodulation,[status(thm)],[f63293,f6]) ).
fof(f66339,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f66136,f63293]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP472-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/10.42 % Computer : n010.cluster.edu
% 0.14/10.42 % Model : x86_64 x86_64
% 0.14/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/10.42 % Memory : 8046.5625MB
% 0.14/10.42 % OS : Linux 6.8.0-71-generic
% 0.14/10.42 % CPULimit : 300
% 0.14/10.42 % WCLimit : 300
% 0.14/10.42 % DateTime : Sun Sep 20 20:14:52 UTC 2026
% 0.14/10.43 % CPUTime :
% 0.14/10.43 % Drodi V4.1.1
% 137.52/28.00 % Refutation found
% 137.52/28.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 137.52/28.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 26.75/28.25 % Elapsed time: 17.786611 seconds
% 26.75/28.25 % CPU time: 140.144557 seconds
% 26.75/28.25 % Total memory used: 979.704 MB
% 26.75/28.25 % Net memory used: 965.301 MB
%------------------------------------------------------------------------------