%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP082-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 : n002.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 23.00s 3.53s
% Output : CNFRefutation 21.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 3
% Syntax : Number of formulae : 154 ( 146 unt; 0 def)
% Number of atoms : 164 ( 163 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 28 ( 18 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 10 ( 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 : 639 ( 639 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z,U] : double_divide(inverse(X),inverse(double_divide(inverse(double_divide(X,double_divide(Y,Z))),double_divide(U,double_divide(Y,U))))) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = inverse(double_divide(Y,X)),
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] : double_divide(inverse(X0),inverse(double_divide(inverse(double_divide(X0,double_divide(X1,X2))),double_divide(X3,double_divide(X1,X3))))) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
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] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),inverse(double_divide(X0,double_divide(X2,X3))))) = X3,
inference(backward_demodulation,[status(thm)],[f5,f4]) ).
fof(f8,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X0))) = X3,
inference(forward_demodulation,[status(thm)],[f5,f7]) ).
fof(f9,plain,
! [X0,X1,X2,X3,X4] : double_divide(multiply(X0,X1),multiply(double_divide(X2,double_divide(X3,X2)),multiply(double_divide(X3,X4),double_divide(X1,X0)))) = X4,
inference(paramodulation,[status(thm)],[f5,f8]) ).
fof(f10,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X4)),X3),multiply(double_divide(inverse(X4),X5),X0))) = X5,
inference(paramodulation,[status(thm)],[f8,f8]) ).
fof(f11,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0))) = multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),X2)),
inference(paramodulation,[status(thm)],[f8,f8]) ).
fof(f12,plain,
! [X0,X1,X2,X3] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),X3)),inverse(X3)) = inverse(X2),
inference(paramodulation,[status(thm)],[f8,f5]) ).
fof(f14,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = inverse(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X2),X1))),
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f15,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,X4))),multiply(X4,X3)) = inverse(X2),
inference(paramodulation,[status(thm)],[f5,f12]) ).
fof(f69,plain,
! [X0,X1,X2,X3] : X0 = multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X0)),X3)),
inference(paramodulation,[status(thm)],[f8,f11]) ).
fof(f71,plain,
! [X0,X1,X2,X3,X4,X5,X6] : double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1)))) = multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,double_divide(inverse(X6),X3)),X6)),
inference(paramodulation,[status(thm)],[f11,f11]) ).
fof(f115,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),double_divide(inverse(X1),multiply(double_divide(X2,double_divide(inverse(X0),X2)),multiply(X3,X1)))) = X3,
inference(forward_demodulation,[status(thm)],[f69,f71]) ).
fof(f140,plain,
! [X0,X1,X2,X3,X4] : double_divide(inverse(multiply(double_divide(X0,double_divide(inverse(X1),X2)),X1)),multiply(double_divide(X3,double_divide(X4,X3)),X2)) = double_divide(X0,X4),
inference(paramodulation,[status(thm)],[f69,f8]) ).
fof(f158,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),double_divide(inverse(multiply(double_divide(X1,double_divide(inverse(X2),X3)),X2)),multiply(double_divide(X4,double_divide(inverse(X0),X4)),X3))) = double_divide(X5,double_divide(X1,X5)),
inference(paramodulation,[status(thm)],[f69,f115]) ).
fof(f184,plain,
! [X0,X1,X2] : double_divide(inverse(X0),double_divide(X1,inverse(X0))) = double_divide(X2,double_divide(X1,X2)),
inference(forward_demodulation,[status(thm)],[f140,f158]) ).
fof(f190,plain,
! [X0,X1,X2] : double_divide(X0,double_divide(X1,X0)) = double_divide(X2,double_divide(X1,X2)),
inference(paramodulation,[status(thm)],[f184,f184]) ).
fof(f278,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2))) = double_divide(X3,double_divide(X1,X3)),
inference(paramodulation,[status(thm)],[f190,f190]) ).
fof(f294,plain,
! [X0,X1,X2,X3] : X0 = multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(X2,double_divide(inverse(X3),X2)),X3)),
inference(paramodulation,[status(thm)],[f190,f69]) ).
fof(f318,plain,
! [X0,X1,X2] : multiply(double_divide(X0,X1),X1) = inverse(double_divide(X2,double_divide(X0,X2))),
inference(paramodulation,[status(thm)],[f190,f5]) ).
fof(f379,plain,
! [X0,X1,X2] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,X2),X2),
inference(forward_demodulation,[status(thm)],[f5,f318]) ).
fof(f390,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)) = multiply(double_divide(X2,X3),X3),
inference(paramodulation,[status(thm)],[f190,f379]) ).
fof(f408,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X3))) = X0,
inference(paramodulation,[status(thm)],[f379,f8]) ).
fof(f467,plain,
! [X0,X1,X2,X3,X4] : double_divide(X0,inverse(X1)) = multiply(double_divide(X2,double_divide(double_divide(X0,X3),X2)),multiply(double_divide(X4,double_divide(X3,X4)),X1)),
inference(paramodulation,[status(thm)],[f278,f69]) ).
fof(f519,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(X3,X4),X0))) = multiply(double_divide(X5,double_divide(X4,X5)),multiply(double_divide(double_divide(X6,X3),double_divide(X7,double_divide(X6,X7))),X2)),
inference(paramodulation,[status(thm)],[f278,f11]) ).
fof(f564,plain,
! [X0,X1,X2,X3,X4,X5,X6] : multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3) = multiply(double_divide(multiply(double_divide(X4,double_divide(X5,X4)),multiply(double_divide(X5,X3),double_divide(X2,X1))),X6),X6),
inference(paramodulation,[status(thm)],[f9,f390]) ).
fof(f568,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2) = multiply(double_divide(multiply(double_divide(X3,double_divide(X4,X3)),multiply(double_divide(X4,X2),X1)),X5),X5),
inference(paramodulation,[status(thm)],[f8,f390]) ).
fof(f697,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(double_divide(X2,X3),X1)),multiply(double_divide(X4,double_divide(X3,X4)),double_divide(X5,double_divide(X2,X5))))) = X0,
inference(paramodulation,[status(thm)],[f278,f408]) ).
fof(f742,plain,
! [X0,X1,X2] : double_divide(inverse(X0),double_divide(X1,inverse(double_divide(X2,double_divide(X1,X2))))) = X0,
inference(forward_demodulation,[status(thm)],[f467,f697]) ).
fof(f743,plain,
! [X0,X1,X2] : double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X1,X2),X2))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f742]) ).
fof(f747,plain,
! [X0,X1,X2,X3] : double_divide(multiply(X0,X1),double_divide(X2,multiply(double_divide(X2,X3),X3))) = double_divide(X1,X0),
inference(paramodulation,[status(thm)],[f5,f743]) ).
fof(f749,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),double_divide(X1,multiply(double_divide(X2,double_divide(X3,X2)),double_divide(X3,X1)))) = X0,
inference(paramodulation,[status(thm)],[f390,f743]) ).
fof(f768,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),X1),X1) = multiply(double_divide(X2,double_divide(inverse(X3),X2)),multiply(X3,X0)),
inference(paramodulation,[status(thm)],[f743,f69]) ).
fof(f772,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2))) = multiply(X2,double_divide(X3,multiply(double_divide(X3,X4),X4))),
inference(paramodulation,[status(thm)],[f743,f390]) ).
fof(f778,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),X1),X1) = multiply(X0,double_divide(X2,multiply(double_divide(X2,X3),X3))),
inference(paramodulation,[status(thm)],[f743,f379]) ).
fof(f780,plain,
! [X0,X1,X2,X3] : double_divide(X0,double_divide(inverse(X1),X0)) = double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X1),
inference(paramodulation,[status(thm)],[f743,f190]) ).
fof(f797,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),inverse(X2)) = inverse(X2),
inference(paramodulation,[status(thm)],[f743,f5]) ).
fof(f818,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),multiply(X2,X3)) = inverse(double_divide(X3,X2)),
inference(paramodulation,[status(thm)],[f5,f797]) ).
fof(f828,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),multiply(X2,X3)) = multiply(X2,X3),
inference(forward_demodulation,[status(thm)],[f5,f818]) ).
fof(f1085,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,multiply(X2,X3))) = multiply(double_divide(X3,X2),double_divide(X4,multiply(double_divide(X4,X5),X5))),
inference(paramodulation,[status(thm)],[f747,f390]) ).
fof(f1151,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2) = multiply(double_divide(X3,double_divide(X2,X3)),multiply(double_divide(X4,double_divide(inverse(X5),X4)),X5)),
inference(paramodulation,[status(thm)],[f294,f828]) ).
fof(f1191,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2) = X2,
inference(forward_demodulation,[status(thm)],[f294,f1151]) ).
fof(f1209,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),double_divide(X2,X0))),X3) = X3,
inference(paramodulation,[status(thm)],[f390,f1191]) ).
fof(f1239,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(X2,X1)),X0)) = multiply(double_divide(X2,X3),X3),
inference(paramodulation,[status(thm)],[f1191,f8]) ).
fof(f1310,plain,
! [X0,X1,X2,X3,X4,X5,X6] : double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X4)),X3),X0)) = multiply(double_divide(X5,double_divide(X6,X5)),double_divide(X6,inverse(X4))),
inference(paramodulation,[status(thm)],[f1209,f10]) ).
fof(f1379,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2))) = multiply(double_divide(X3,double_divide(inverse(X4),X3)),multiply(X4,X2)),
inference(paramodulation,[status(thm)],[f749,f69]) ).
fof(f1385,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = inverse(multiply(double_divide(double_divide(X4,multiply(double_divide(X5,double_divide(X6,X5)),double_divide(X6,X4))),X7),multiply(double_divide(inverse(X7),X2),X1))),
inference(paramodulation,[status(thm)],[f749,f14]) ).
fof(f1514,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(inverse(double_divide(X1,X2)),X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4)) = inverse(X2),
inference(paramodulation,[status(thm)],[f778,f15]) ).
fof(f1518,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(multiply(double_divide(X0,double_divide(inverse(double_divide(X1,multiply(double_divide(X1,X2),X2))),X0)),multiply(X3,X4)),inverse(X4)) = inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(inverse(double_divide(X6,X3)),X7),X7))),
inference(paramodulation,[status(thm)],[f778,f14]) ).
fof(f1565,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(multiply(X2,X1),X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4)) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f5,f1514]) ).
fof(f1571,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4)) = inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(inverse(double_divide(X6,X3)),X7),X7))),
inference(forward_demodulation,[status(thm)],[f5,f1518]) ).
fof(f1572,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4)) = inverse(multiply(double_divide(X5,double_divide(X6,X5)),multiply(double_divide(multiply(X3,X6),X7),X7))),
inference(forward_demodulation,[status(thm)],[f5,f1571]) ).
fof(f1759,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = inverse(multiply(double_divide(X4,double_divide(X5,double_divide(inverse(X4),X5))),multiply(double_divide(double_divide(X6,multiply(double_divide(X6,X7),X7)),X2),X1))),
inference(paramodulation,[status(thm)],[f780,f14]) ).
fof(f1768,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1))),double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X4)) = multiply(double_divide(X4,X5),X5),
inference(paramodulation,[status(thm)],[f780,f390]) ).
fof(f1778,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0))) = multiply(double_divide(X4,double_divide(X5,double_divide(inverse(X4),X5))),multiply(double_divide(double_divide(X6,multiply(double_divide(X6,X7),X7)),X3),X2)),
inference(paramodulation,[status(thm)],[f780,f11]) ).
fof(f1788,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1))),multiply(double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X4),X5)),inverse(X5)) = inverse(X4),
inference(paramodulation,[status(thm)],[f780,f12]) ).
fof(f1950,plain,
! [X0,X1,X2,X3] : double_divide(inverse(double_divide(X0,X1)),multiply(double_divide(X1,X2),X2)) = multiply(double_divide(X0,X3),X3),
inference(paramodulation,[status(thm)],[f390,f1239]) ).
fof(f1969,plain,
! [X0,X1,X2,X3,X4,X5,X6] : double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),double_divide(X4,X5))),X3),X0)) = multiply(double_divide(multiply(X5,X4),X6),X6),
inference(paramodulation,[status(thm)],[f9,f1239]) ).
fof(f2099,plain,
! [X0,X1,X2,X3] : double_divide(multiply(X0,X1),multiply(double_divide(X0,X2),X2)) = multiply(double_divide(X1,X3),X3),
inference(forward_demodulation,[status(thm)],[f5,f1950]) ).
fof(f2246,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(multiply(X1,X0),multiply(double_divide(X1,X2),X2))),X3) = X3,
inference(paramodulation,[status(thm)],[f2099,f1209]) ).
fof(f2288,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,X1),X1) = double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X0),
inference(paramodulation,[status(thm)],[f390,f2246]) ).
fof(f2298,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(inverse(double_divide(multiply(X1,double_divide(X2,multiply(double_divide(X2,X3),X3))),multiply(double_divide(X1,X4),X4))),X0)),X5) = X5,
inference(paramodulation,[status(thm)],[f780,f2246]) ).
fof(f2300,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(multiply(X1,multiply(double_divide(X1,X2),X2)),X0)),X3) = X3,
inference(paramodulation,[status(thm)],[f190,f2246]) ).
fof(f2400,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),multiply(X1,double_divide(X3,multiply(double_divide(X3,X4),X4)))),X0)),X5) = X5,
inference(forward_demodulation,[status(thm)],[f5,f2298]) ).
fof(f2442,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(multiply(double_divide(X3,X4),X4),X3))),X5),X5) = X2,
inference(paramodulation,[status(thm)],[f9,f2288]) ).
fof(f2444,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(double_divide(inverse(X0),multiply(X1,multiply(double_divide(X1,X2),X2))),X3),X3) = double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X0),
inference(paramodulation,[status(thm)],[f780,f2288]) ).
fof(f2569,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X1)),X0)) = multiply(multiply(double_divide(X4,X5),X5),X4),
inference(paramodulation,[status(thm)],[f2288,f1239]) ).
fof(f2573,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(inverse(X0),X1),X1) = multiply(X0,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),multiply(multiply(double_divide(X4,X5),X5),X4))),
inference(paramodulation,[status(thm)],[f2288,f778]) ).
fof(f2585,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(multiply(X2,multiply(double_divide(X2,X3),X3)),X1)),multiply(multiply(double_divide(X4,X5),X5),X4))) = X0,
inference(paramodulation,[status(thm)],[f2288,f408]) ).
fof(f2594,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(X0,multiply(double_divide(X0,X1),X1)),X2),X2) = multiply(multiply(double_divide(X3,X4),X4),X3),
inference(paramodulation,[status(thm)],[f2288,f379]) ).
fof(f2628,plain,
! [X0,X1,X2] : double_divide(inverse(X0),X0) = multiply(multiply(double_divide(X1,X2),X2),X1),
inference(forward_demodulation,[status(thm)],[f2300,f2569]) ).
fof(f2638,plain,
! [X0,X1,X2] : double_divide(inverse(X0),multiply(multiply(double_divide(X1,X2),X2),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2300,f2585]) ).
fof(f2771,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,multiply(double_divide(X1,double_divide(inverse(X0),X1)),multiply(multiply(double_divide(X2,X3),X3),X2))),X4) = X4,
inference(paramodulation,[status(thm)],[f2628,f1209]) ).
fof(f2783,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2))) = multiply(multiply(multiply(double_divide(X3,X4),X4),X3),X2),
inference(paramodulation,[status(thm)],[f2628,f390]) ).
fof(f2806,plain,
! [X0,X1,X2,X3,X4] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(multiply(double_divide(X3,X4),X4),X3),X0))) = X2,
inference(paramodulation,[status(thm)],[f2628,f8]) ).
fof(f2817,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(X1,X2),double_divide(X3,multiply(double_divide(X3,X4),X4)))),double_divide(inverse(X5),X5)) = inverse(X2),
inference(paramodulation,[status(thm)],[f2628,f15]) ).
fof(f3072,plain,
! [X0,X1,X2,X3] : double_divide(multiply(X0,X1),multiply(multiply(double_divide(X2,X3),X3),X2)) = double_divide(X1,X0),
inference(paramodulation,[status(thm)],[f5,f2638]) ).
fof(f3090,plain,
! [X0,X1,X2,X3,X4] : double_divide(inverse(X0),multiply(multiply(multiply(double_divide(X1,X2),X2),X1),multiply(X3,multiply(double_divide(X3,X4),X4)))) = X0,
inference(paramodulation,[status(thm)],[f2288,f2638]) ).
fof(f3119,plain,
! [X0,X1,X2,X3,X4] : X0 = multiply(double_divide(X1,double_divide(X0,X1)),multiply(double_divide(multiply(multiply(double_divide(X2,X3),X3),X2),X4),X4)),
inference(paramodulation,[status(thm)],[f2638,f294]) ).
fof(f3134,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(inverse(X0),X1),X1) = multiply(X0,double_divide(inverse(X2),multiply(X2,multiply(multiply(double_divide(X3,X4),X4),X3)))),
inference(paramodulation,[status(thm)],[f2638,f778]) ).
fof(f3149,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2))) = multiply(X2,multiply(multiply(double_divide(X3,X4),X4),X3)),
inference(paramodulation,[status(thm)],[f2638,f390]) ).
fof(f3160,plain,
! [X0,X1,X2,X3,X4,X5,X6] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(multiply(multiply(double_divide(X3,X4),X4),X3),X0))) = multiply(double_divide(X5,double_divide(inverse(X6),X5)),multiply(X6,X2)),
inference(paramodulation,[status(thm)],[f2638,f11]) ).
fof(f3181,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),X1),X1) = multiply(X0,double_divide(multiply(double_divide(X2,X3),X3),X2)),
inference(backward_demodulation,[status(thm)],[f3072,f2573]) ).
fof(f3217,plain,
! [X0,X1,X2] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,inverse(X2))) = X2,
inference(backward_demodulation,[status(thm)],[f3228,f1379]) ).
fof(f3222,plain,
! [X0,X1] : multiply(double_divide(inverse(X0),X1),X1) = X0,
inference(backward_demodulation,[status(thm)],[f3228,f768]) ).
fof(f3228,plain,
! [X0,X1,X2] : X0 = multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X2,X0)),
inference(forward_demodulation,[status(thm)],[f2806,f3160]) ).
fof(f3245,plain,
! [X0,X1,X2] : X0 = multiply(X0,multiply(multiply(double_divide(X1,X2),X2),X1)),
inference(backward_demodulation,[status(thm)],[f3217,f3149]) ).
fof(f3247,plain,
! [X0,X1,X2] : X0 = multiply(multiply(multiply(double_divide(X1,X2),X2),X1),X0),
inference(backward_demodulation,[status(thm)],[f3217,f2783]) ).
fof(f3250,plain,
! [X0,X1,X2,X3,X4] : double_divide(inverse(X0),multiply(double_divide(multiply(double_divide(X1,double_divide(X2,X1)),multiply(double_divide(X2,X3),X4)),X3),X0)) = X4,
inference(backward_demodulation,[status(thm)],[f3217,f1310]) ).
fof(f3253,plain,
! [X0,X1,X2] : X0 = multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2))),
inference(backward_demodulation,[status(thm)],[f3217,f772]) ).
fof(f3286,plain,
! [X0,X1,X2] : X0 = multiply(X0,double_divide(multiply(double_divide(X1,X2),X2),X1)),
inference(backward_demodulation,[status(thm)],[f3222,f3181]) ).
fof(f3289,plain,
! [X0,X1,X2,X3] : X0 = multiply(X0,double_divide(inverse(X1),multiply(X1,multiply(multiply(double_divide(X2,X3),X3),X2)))),
inference(backward_demodulation,[status(thm)],[f3222,f3134]) ).
fof(f3359,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(X1,X0)),multiply(double_divide(multiply(X2,X1),X3),X3)) = inverse(X2),
inference(backward_demodulation,[status(thm)],[f3245,f1565]) ).
fof(f3362,plain,
! [X0,X1,X2] : multiply(double_divide(X0,double_divide(X1,double_divide(inverse(X0),X1))),X2) = X2,
inference(backward_demodulation,[status(thm)],[f3245,f2771]) ).
fof(f3406,plain,
! [X0,X1,X2] : double_divide(inverse(X0),multiply(X1,multiply(double_divide(X1,X2),X2))) = X0,
inference(backward_demodulation,[status(thm)],[f3247,f3090]) ).
fof(f3459,plain,
! [X0,X1,X2] : double_divide(X0,X1) = multiply(double_divide(multiply(X1,X0),X2),X2),
inference(backward_demodulation,[status(thm)],[f3250,f1969]) ).
fof(f3470,plain,
! [X0,X1,X2,X3] : multiply(multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)),double_divide(inverse(X3),X3)) = inverse(X2),
inference(backward_demodulation,[status(thm)],[f3253,f2817]) ).
fof(f3482,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,multiply(X2,X3))) = double_divide(X3,X2),
inference(backward_demodulation,[status(thm)],[f3253,f1085]) ).
fof(f3497,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),X3) = X3,
inference(backward_demodulation,[status(thm)],[f3253,f2400]) ).
fof(f3622,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)),X3),X3) = X2,
inference(backward_demodulation,[status(thm)],[f3286,f2442]) ).
fof(f3632,plain,
! [X0,X1] : X0 = multiply(X0,double_divide(inverse(X1),X1)),
inference(forward_demodulation,[status(thm)],[f3245,f3289]) ).
fof(f3668,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(double_divide(X0,double_divide(multiply(multiply(double_divide(X1,X2),X2),X1),X0)),multiply(X3,X4)),inverse(X4)) = inverse(inverse(X3)),
inference(backward_demodulation,[status(thm)],[f3359,f1572]) ).
fof(f3674,plain,
! [X0,X1,X2,X3] : multiply(multiply(double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2),X3),inverse(X3)) = inverse(X2),
inference(backward_demodulation,[status(thm)],[f3362,f1788]) ).
fof(f3676,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0))) = multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X3),X2),
inference(backward_demodulation,[status(thm)],[f3362,f1778]) ).
fof(f3679,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = inverse(multiply(double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2),X1)),
inference(backward_demodulation,[status(thm)],[f3362,f1759]) ).
fof(f3681,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2) = multiply(double_divide(X2,X3),X3),
inference(backward_demodulation,[status(thm)],[f3362,f1768]) ).
fof(f3696,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,X1),X1) = double_divide(double_divide(X2,multiply(double_divide(X2,X3),X3)),X0),
inference(backward_demodulation,[status(thm)],[f3406,f2444]) ).
fof(f3703,plain,
! [X0,X1,X2,X3] : X0 = multiply(double_divide(X1,double_divide(X0,X1)),double_divide(X2,multiply(double_divide(X2,X3),X3))),
inference(backward_demodulation,[status(thm)],[f3459,f3119]) ).
fof(f3727,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(X0,double_divide(multiply(X1,X2),X0)),X3) = double_divide(multiply(double_divide(X4,X3),double_divide(X2,X1)),double_divide(X5,double_divide(X4,X5))),
inference(backward_demodulation,[status(thm)],[f3459,f564]) ).
fof(f3733,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(X0,double_divide(inverse(X1),X0)),X2) = double_divide(multiply(double_divide(X3,X2),X1),double_divide(X4,double_divide(X3,X4))),
inference(backward_demodulation,[status(thm)],[f3459,f568]) ).
fof(f3744,plain,
! [X0,X1,X2,X3] : double_divide(multiply(double_divide(X0,X1),X1),X0) = multiply(multiply(double_divide(X2,X3),X3),X2),
inference(backward_demodulation,[status(thm)],[f3459,f2594]) ).
fof(f3811,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = inverse(multiply(double_divide(double_divide(X4,inverse(X4)),X5),multiply(double_divide(inverse(X5),X2),X1))),
inference(backward_demodulation,[status(thm)],[f3848,f1385]) ).
fof(f3848,plain,
! [X0,X1,X2] : multiply(double_divide(X0,double_divide(X1,X0)),double_divide(X1,X2)) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f3632,f3470]) ).
fof(f3998,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f3848,f3482]) ).
fof(f4091,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(double_divide(X3,X4),X0))) = multiply(double_divide(X5,double_divide(X4,X5)),multiply(X3,X2)),
inference(backward_demodulation,[status(thm)],[f4110,f519]) ).
fof(f4110,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),double_divide(X2,double_divide(X0,X2))) = X1,
inference(forward_demodulation,[status(thm)],[f3459,f3622]) ).
fof(f4173,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f3497,f3668]) ).
fof(f4176,plain,
! [X0,X1,X2] : inverse(inverse(double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2))) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f4173,f3674]) ).
fof(f4177,plain,
! [X0,X1,X2] : inverse(multiply(X0,double_divide(X1,multiply(double_divide(X1,X2),X2)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f5,f4176]) ).
fof(f4298,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(double_divide(X0,X1),X1)),X2) = inverse(X2),
inference(forward_demodulation,[status(thm)],[f3998,f4177]) ).
fof(f4360,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),multiply(double_divide(X1,double_divide(inverse(X2),X1)),multiply(X3,X0))) = multiply(inverse(X3),X2),
inference(forward_demodulation,[status(thm)],[f4298,f3676]) ).
fof(f4363,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = double_divide(X1,double_divide(double_divide(X4,multiply(double_divide(X4,X5),X5)),X2)),
inference(forward_demodulation,[status(thm)],[f3998,f3679]) ).
fof(f4386,plain,
! [X0,X1,X2,X3] : multiply(multiply(double_divide(X0,double_divide(inverse(X1),X0)),multiply(X2,X3)),inverse(X3)) = double_divide(X1,inverse(X2)),
inference(forward_demodulation,[status(thm)],[f4298,f4363]) ).
fof(f4713,plain,
! [X0,X1] : inverse(X0) = multiply(double_divide(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f4298,f3681]) ).
fof(f4725,plain,
! [X0,X1,X2] : inverse(X0) = double_divide(double_divide(X1,multiply(double_divide(X1,X2),X2)),X0),
inference(forward_demodulation,[status(thm)],[f4713,f3696]) ).
fof(f4726,plain,
! [X0,X1] : inverse(X0) = double_divide(double_divide(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f4713,f4725]) ).
fof(f4916,plain,
! [X0,X1] : X0 = double_divide(X1,double_divide(X0,X1)),
inference(forward_demodulation,[status(thm)],[f3253,f3703]) ).
fof(f4972,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(X0,X1),X2) = double_divide(multiply(double_divide(X3,X2),double_divide(X1,X0)),double_divide(X4,double_divide(X3,X4))),
inference(forward_demodulation,[status(thm)],[f4916,f3727]) ).
fof(f4973,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,X1),X2) = double_divide(multiply(double_divide(X3,X2),double_divide(X1,X0)),X3),
inference(forward_demodulation,[status(thm)],[f4916,f4972]) ).
fof(f4986,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),X1) = double_divide(multiply(double_divide(X2,X1),X0),double_divide(X3,double_divide(X2,X3))),
inference(forward_demodulation,[status(thm)],[f4916,f3733]) ).
fof(f4988,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(inverse(double_divide(X1,X0)),X2),
inference(backward_demodulation,[status(thm)],[f4992,f4973]) ).
fof(f4992,plain,
! [X0,X1,X2] : multiply(inverse(X0),X1) = double_divide(multiply(double_divide(X2,X1),X0),X2),
inference(forward_demodulation,[status(thm)],[f4916,f4986]) ).
fof(f5020,plain,
! [X0,X1,X2] : multiply(inverse(X0),X0) = multiply(multiply(double_divide(X1,X2),X2),X1),
inference(forward_demodulation,[status(thm)],[f4992,f3744]) ).
fof(f5021,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(multiply(inverse(b2),b2),a2) != a2 ),
inference(backward_subsumption_resolution,[status(thm)],[f6,f5022]) ).
fof(f5022,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(forward_demodulation,[status(thm)],[f4713,f5020]) ).
fof(f5124,plain,
! [X0,X1,X2,X3] : double_divide(X0,inverse(X1)) = inverse(multiply(double_divide(double_divide(X2,inverse(X2)),X3),multiply(double_divide(inverse(X3),X1),X0))),
inference(forward_demodulation,[status(thm)],[f4386,f3811]) ).
fof(f5125,plain,
! [X0,X1,X2,X3] : double_divide(X0,inverse(X1)) = double_divide(multiply(double_divide(inverse(X2),X1),X0),double_divide(double_divide(X3,inverse(X3)),X2)),
inference(forward_demodulation,[status(thm)],[f3998,f5124]) ).
fof(f5126,plain,
! [X0,X1,X2] : double_divide(X0,inverse(X1)) = double_divide(multiply(double_divide(inverse(X2),X1),X0),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f4726,f5125]) ).
fof(f5145,plain,
! [X0,X1] : double_divide(X0,inverse(X1)) = multiply(inverse(X0),X1),
inference(forward_demodulation,[status(thm)],[f4992,f5126]) ).
fof(f6256,plain,
! [X0,X1,X2,X3] : multiply(inverse(double_divide(X0,X1)),X2) = multiply(double_divide(X3,double_divide(X1,X3)),multiply(X0,X2)),
inference(forward_demodulation,[status(thm)],[f4360,f4091]) ).
fof(f6257,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,X1),inverse(X2)) = multiply(double_divide(X3,double_divide(X1,X3)),multiply(X0,X2)),
inference(forward_demodulation,[status(thm)],[f5145,f6256]) ).
fof(f6260,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(X2)) = multiply(X1,multiply(X0,X2)),
inference(forward_demodulation,[status(thm)],[f4916,f6257]) ).
fof(f10121,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = double_divide(double_divide(X1,X0),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f5145,f4988]) ).
fof(f10134,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f6260,f10121]) ).
fof(f10147,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(inverse(b2),multiply(b2,a2)) != a2 ),
inference(forward_demodulation,[status(thm)],[f10134,f5021]) ).
fof(f10148,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| double_divide(b2,inverse(multiply(b2,a2))) != a2 ),
inference(forward_demodulation,[status(thm)],[f5145,f10147]) ).
fof(f10149,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| double_divide(b2,double_divide(a2,b2)) != a2 ),
inference(forward_demodulation,[status(thm)],[f3998,f10148]) ).
fof(f10150,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(forward_demodulation,[status(thm)],[f4916,f10149]) ).
fof(f10151,plain,
( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
| a2 != a2 ),
inference(forward_demodulation,[status(thm)],[f10134,f10150]) ).
fof(f10152,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f10151]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP082-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:00:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 23.00/3.53 % Refutation found
% 23.00/3.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 23.00/3.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.79/3.59 % Elapsed time: 3.223284 seconds
% 21.79/3.59 % CPU time: 25.193345 seconds
% 21.79/3.59 % Total memory used: 316.734 MB
% 21.79/3.59 % Net memory used: 311.617 MB
%------------------------------------------------------------------------------