%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP476-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:29 PM UTC 2026
% Result : Unsatisfiable 181.55s 23.34s
% Output : CNFRefutation 102.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 6
% Syntax : Number of formulae : 185 ( 185 unt; 3 def)
% Number of atoms : 185 ( 184 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 301 ( 301 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : divide(inverse(divide(divide(divide(A,B),C),divide(D,C))),divide(B,A)) = D,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(divide(divide(X0,X1),X2),divide(X3,X2))),divide(X1,X0)) = X3,
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(inverse(b2),b2),a2) != a2,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f7,definition,
sF2_fnc = inverse(b2),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f8,definition,
sF1_fnc = multiply(sF2_fnc,b2),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f9,definition,
sF0_fnc = multiply(sF1_fnc,a2),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f10,plain,
sF0_fnc != a2,
inference(definition_folding,[],[f6,f9,f8,f7]) ).
fof(f11,plain,
! [X0] : multiply(X0,b2) = divide(X0,sF2_fnc),
inference(paramodulation,[status(thm)],[f7,f5]) ).
fof(f12,plain,
sF1_fnc = divide(sF2_fnc,sF2_fnc),
inference(backward_demodulation,[status(thm)],[f11,f8]) ).
fof(f13,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(divide(X0,X1),X2),divide(X3,inverse(X2)))),divide(X1,X0)) = X3,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f14,plain,
! [X0,X1,X2,X3,X4,X5] : divide(inverse(divide(divide(X0,X1),divide(X2,X1))),divide(divide(X3,X4),inverse(divide(divide(divide(X4,X3),X5),divide(X0,X5))))) = X2,
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f15,plain,
! [X0,X1] : divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),divide(sF2_fnc,sF2_fnc)) = X1,
inference(paramodulation,[status(thm)],[f12,f4]) ).
fof(f16,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(divide(multiply(X0,X1),X2),divide(X3,X2))),divide(inverse(X1),X0)) = X3,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f17,plain,
! [X0,X1,X2,X3,X4,X5] : divide(inverse(divide(divide(divide(X0,X1),divide(X2,X3)),X4)),divide(X1,X0)) = inverse(divide(divide(divide(X3,X2),X5),divide(X4,X5))),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f22,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(divide(divide(inverse(X0),X1),X2),divide(X3,X2))),multiply(X1,X0)) = X3,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f23,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(divide(X0,X1),X2),multiply(X3,X2))),divide(X1,X0)) = X3,
inference(forward_demodulation,[status(thm)],[f5,f13]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4,X5] : divide(inverse(divide(divide(X0,X1),divide(X2,X1))),multiply(divide(X3,X4),divide(divide(divide(X4,X3),X5),divide(X0,X5)))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f14]) ).
fof(f25,plain,
! [X0,X1] : divide(inverse(divide(divide(sF1_fnc,X0),divide(X1,X0))),sF1_fnc) = X1,
inference(forward_demodulation,[status(thm)],[f12,f15]) ).
fof(f29,plain,
! [X0,X1] : divide(inverse(divide(multiply(sF1_fnc,X0),divide(X1,inverse(X0)))),sF1_fnc) = X1,
inference(paramodulation,[status(thm)],[f5,f25]) ).
fof(f30,plain,
! [X0,X1] : divide(inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),sF1_fnc) = inverse(divide(divide(sF1_fnc,X1),divide(X0,X1))),
inference(paramodulation,[status(thm)],[f25,f25]) ).
fof(f31,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(divide(sF1_fnc,divide(X0,X1)),X2)),sF1_fnc) = inverse(divide(divide(divide(X1,X0),X3),divide(X2,X3))),
inference(paramodulation,[status(thm)],[f4,f25]) ).
fof(f37,plain,
! [X0,X1] : divide(inverse(divide(multiply(sF1_fnc,X0),multiply(X1,X0))),sF1_fnc) = X1,
inference(forward_demodulation,[status(thm)],[f5,f29]) ).
fof(f41,plain,
! [X0] : divide(inverse(divide(sF0_fnc,multiply(X0,a2))),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f9,f37]) ).
fof(f43,plain,
divide(inverse(divide(multiply(sF1_fnc,a2),sF0_fnc)),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f9,f37]) ).
fof(f50,plain,
divide(inverse(divide(sF0_fnc,sF0_fnc)),sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f9,f43]) ).
fof(f79,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),divide(sF1_fnc,inverse(divide(divide(sF1_fnc,X3),divide(X0,X3))))) = X2,
inference(paramodulation,[status(thm)],[f25,f23]) ).
fof(f82,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(multiply(X0,X1),X2),multiply(X3,X2))),divide(inverse(X1),X0)) = X3,
inference(paramodulation,[status(thm)],[f5,f23]) ).
fof(f83,plain,
! [X0,X1] : divide(inverse(divide(multiply(divide(X0,X1),a2),sF0_fnc)),divide(X1,X0)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f9,f23]) ).
fof(f93,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(divide(inverse(X0),X1),X2),multiply(X3,X2))),multiply(X1,X0)) = X3,
inference(paramodulation,[status(thm)],[f5,f23]) ).
fof(f104,plain,
! [X0,X1,X2,X3] : divide(inverse(divide(multiply(X0,X1),multiply(X2,X1))),multiply(sF1_fnc,divide(divide(sF1_fnc,X3),divide(X0,X3)))) = X2,
inference(forward_demodulation,[status(thm)],[f5,f79]) ).
fof(f172,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : divide(inverse(divide(divide(divide(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),inverse(divide(divide(X3,X4),divide(X5,X4)))),X6),divide(X7,X6))),X5) = X7,
inference(paramodulation,[status(thm)],[f24,f4]) ).
fof(f199,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : divide(inverse(divide(divide(multiply(multiply(divide(X0,X1),divide(divide(divide(X1,X0),X2),divide(X3,X2))),divide(divide(X3,X4),divide(X5,X4))),X6),divide(X7,X6))),X5) = X7,
inference(forward_demodulation,[status(thm)],[f5,f172]) ).
fof(f208,plain,
! [X0,X1,X2,X3,X4,X5] : divide(inverse(divide(divide(multiply(X0,X1),divide(inverse(X2),X3)),X4)),divide(inverse(X1),X0)) = inverse(divide(divide(multiply(X3,X2),X5),divide(X4,X5))),
inference(paramodulation,[status(thm)],[f16,f16]) ).
fof(f339,plain,
! [X0,X1] : divide(inverse(divide(multiply(divide(inverse(X0),X1),a2),sF0_fnc)),multiply(X1,X0)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f5,f83]) ).
fof(f450,plain,
! [X0,X1] : divide(inverse(divide(divide(divide(inverse(a2),sF1_fnc),X0),divide(X1,X0))),sF0_fnc) = X1,
inference(paramodulation,[status(thm)],[f9,f22]) ).
fof(f874,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(divide(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),X3))),
inference(paramodulation,[status(thm)],[f4,f17]) ).
fof(f1383,plain,
! [X0,X1] : X0 = inverse(divide(divide(sF1_fnc,X1),divide(divide(X0,sF1_fnc),X1))),
inference(paramodulation,[status(thm)],[f25,f30]) ).
fof(f1505,plain,
! [X0,X1] : X0 = inverse(divide(multiply(sF1_fnc,X1),divide(divide(X0,sF1_fnc),inverse(X1)))),
inference(paramodulation,[status(thm)],[f5,f1383]) ).
fof(f1507,plain,
! [X0,X1] : inverse(divide(sF0_fnc,multiply(X0,a2))) = inverse(divide(divide(sF1_fnc,X1),divide(X0,X1))),
inference(paramodulation,[status(thm)],[f41,f1383]) ).
fof(f1527,plain,
! [X0,X1] : X0 = inverse(divide(multiply(sF1_fnc,X1),multiply(divide(X0,sF1_fnc),X1))),
inference(forward_demodulation,[status(thm)],[f5,f1505]) ).
fof(f1529,plain,
! [X0] : X0 = inverse(divide(sF0_fnc,multiply(divide(X0,sF1_fnc),a2))),
inference(paramodulation,[status(thm)],[f9,f1527]) ).
fof(f1532,plain,
! [X0,X1] : inverse(divide(sF0_fnc,multiply(X0,a2))) = inverse(divide(multiply(sF1_fnc,X1),multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f41,f1527]) ).
fof(f1548,plain,
! [X0,X1,X2] : multiply(X0,divide(multiply(sF1_fnc,X1),multiply(divide(X2,sF1_fnc),X1))) = divide(X0,X2),
inference(paramodulation,[status(thm)],[f1527,f5]) ).
fof(f1685,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(divide(sF1_fnc,divide(X0,X1)),X2)),sF1_fnc),divide(X0,X1)) = X2,
inference(paramodulation,[status(thm)],[f31,f4]) ).
fof(f1904,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(multiply(divide(X1,X2),X3),divide(divide(X0,divide(X2,X1)),inverse(X3)))),
inference(paramodulation,[status(thm)],[f5,f874]) ).
fof(f1986,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(multiply(divide(X1,X2),X3),multiply(divide(X0,divide(X2,X1)),X3))),
inference(forward_demodulation,[status(thm)],[f5,f1904]) ).
fof(f2841,plain,
! [X0,X1,X2,X3] : X0 = inverse(divide(multiply(divide(inverse(X1),X2),X3),multiply(divide(X0,multiply(X2,X1)),X3))),
inference(paramodulation,[status(thm)],[f5,f1986]) ).
fof(f3063,plain,
! [X0] : divide(divide(inverse(divide(divide(sF1_fnc,divide(sF1_fnc,inverse(a2))),X0)),sF1_fnc),sF0_fnc) = X0,
inference(paramodulation,[status(thm)],[f31,f450]) ).
fof(f3143,plain,
! [X0] : divide(divide(inverse(divide(divide(sF1_fnc,multiply(sF1_fnc,a2)),X0)),sF1_fnc),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f3063]) ).
fof(f3144,plain,
! [X0] : divide(divide(inverse(divide(divide(sF1_fnc,sF0_fnc),X0)),sF1_fnc),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f9,f3143]) ).
fof(f3184,plain,
! [X0] : divide(divide(inverse(multiply(divide(sF1_fnc,sF0_fnc),X0)),sF1_fnc),sF0_fnc) = inverse(X0),
inference(paramodulation,[status(thm)],[f5,f3144]) ).
fof(f5415,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(sF1_fnc,inverse(X0)),X1)),sF1_fnc),divide(divide(inverse(multiply(divide(sF1_fnc,sF0_fnc),X0)),sF1_fnc),sF0_fnc)) = X1,
inference(paramodulation,[status(thm)],[f3184,f1685]) ).
fof(f5417,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc),divide(divide(inverse(divide(divide(sF1_fnc,divide(X2,X3)),X0)),sF1_fnc),divide(X2,X3))) = X1,
inference(paramodulation,[status(thm)],[f1685,f1685]) ).
fof(f5562,plain,
! [X0,X1] : divide(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc),divide(divide(inverse(multiply(divide(sF1_fnc,sF0_fnc),X0)),sF1_fnc),sF0_fnc)) = X1,
inference(forward_demodulation,[status(thm)],[f5,f5415]) ).
fof(f5563,plain,
! [X0,X1] : divide(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc),inverse(X0)) = X1,
inference(forward_demodulation,[status(thm)],[f3184,f5562]) ).
fof(f5564,plain,
! [X0,X1] : multiply(divide(inverse(divide(multiply(sF1_fnc,X0),X1)),sF1_fnc),X0) = X1,
inference(forward_demodulation,[status(thm)],[f5,f5563]) ).
fof(f5568,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(sF1_fnc,X0),X1)),sF1_fnc),X0) = X1,
inference(forward_demodulation,[status(thm)],[f1685,f5417]) ).
fof(f5673,plain,
! [X0,X1] : multiply(divide(inverse(multiply(multiply(sF1_fnc,X0),X1)),sF1_fnc),X0) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f5564]) ).
fof(f5674,plain,
! [X0] : multiply(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),a2) = X0,
inference(paramodulation,[status(thm)],[f9,f5564]) ).
fof(f5680,plain,
! [X0,X1,X2] : divide(inverse(divide(X0,multiply(X1,X2))),multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X0))) = X1,
inference(paramodulation,[status(thm)],[f5564,f93]) ).
fof(f5687,plain,
! [X0,X1,X2] : X0 = inverse(divide(X1,multiply(divide(X0,divide(sF1_fnc,inverse(divide(multiply(sF1_fnc,X2),X1)))),X2))),
inference(paramodulation,[status(thm)],[f5564,f1986]) ).
fof(f5734,plain,
! [X0,X1,X2] : X0 = inverse(divide(X1,multiply(divide(X0,multiply(sF1_fnc,divide(multiply(sF1_fnc,X2),X1))),X2))),
inference(forward_demodulation,[status(thm)],[f5,f5687]) ).
fof(f5747,plain,
! [X0] : multiply(divide(inverse(multiply(sF0_fnc,X0)),sF1_fnc),a2) = inverse(X0),
inference(paramodulation,[status(thm)],[f5,f5674]) ).
fof(f5749,plain,
! [X0,X1] : divide(inverse(divide(X0,multiply(X1,a2))),multiply(sF1_fnc,divide(sF0_fnc,X0))) = X1,
inference(paramodulation,[status(thm)],[f5674,f93]) ).
fof(f5805,plain,
! [X0,X1] : divide(divide(inverse(multiply(divide(sF1_fnc,X0),X1)),sF1_fnc),X0) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f5568]) ).
fof(f15619,plain,
! [X0] : divide(X0,multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc))) = divide(X0,sF1_fnc),
inference(paramodulation,[status(thm)],[f1529,f5749]) ).
fof(f15879,plain,
multiply(divide(inverse(divide(sF0_fnc,sF1_fnc)),sF1_fnc),a2) = multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f15619,f5674]) ).
fof(f16096,plain,
sF1_fnc = multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f5674,f15879]) ).
fof(f16200,plain,
! [X0] : multiply(divide(inverse(multiply(sF1_fnc,X0)),sF1_fnc),divide(sF0_fnc,sF0_fnc)) = inverse(X0),
inference(paramodulation,[status(thm)],[f16096,f5673]) ).
fof(f16203,plain,
! [X0,X1] : multiply(X0,divide(sF1_fnc,multiply(divide(X1,sF1_fnc),divide(sF0_fnc,sF0_fnc)))) = divide(X0,X1),
inference(paramodulation,[status(thm)],[f16096,f1548]) ).
fof(f21106,plain,
! [X0,X1,X2,X3,X4] : inverse(divide(multiply(X0,X1),multiply(X2,X1))) = inverse(divide(multiply(divide(inverse(divide(divide(sF1_fnc,X3),divide(X0,X3))),sF1_fnc),X4),multiply(X2,X4))),
inference(paramodulation,[status(thm)],[f104,f2841]) ).
fof(f21203,plain,
! [X0,X1,X2,X3] : inverse(divide(multiply(X0,X1),multiply(X2,X1))) = inverse(divide(multiply(divide(inverse(divide(sF0_fnc,multiply(X0,a2))),sF1_fnc),X3),multiply(X2,X3))),
inference(forward_demodulation,[status(thm)],[f1507,f21106]) ).
fof(f21204,plain,
! [X0,X1,X2,X3] : inverse(divide(multiply(X0,X1),multiply(X2,X1))) = inverse(divide(multiply(X0,X3),multiply(X2,X3))),
inference(forward_demodulation,[status(thm)],[f41,f21203]) ).
fof(f24407,plain,
! [X0] : divide(inverse(divide(X0,sF1_fnc)),multiply(sF1_fnc,divide(multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),X0))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f16096,f5680]) ).
fof(f24652,plain,
! [X0] : divide(inverse(divide(X0,sF1_fnc)),multiply(sF1_fnc,divide(sF1_fnc,X0))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f16096,f24407]) ).
fof(f24770,plain,
! [X0] : divide(inverse(X0),multiply(sF1_fnc,divide(sF1_fnc,inverse(divide(sF0_fnc,multiply(X0,a2)))))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f41,f24652]) ).
fof(f24771,plain,
divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,inverse(divide(sF0_fnc,sF0_fnc))))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f50,f24652]) ).
fof(f24958,plain,
! [X0] : divide(inverse(X0),multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(X0,a2))))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f5,f24770]) ).
fof(f24959,plain,
divide(inverse(sF1_fnc),multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f5,f24771]) ).
fof(f24960,plain,
divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f16096,f24959]) ).
fof(f26839,plain,
! [X0,X1] : X0 = inverse(divide(multiply(sF1_fnc,X1),multiply(divide(X0,multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)),X1))),
inference(paramodulation,[status(thm)],[f24960,f2841]) ).
fof(f27021,plain,
! [X0] : X0 = inverse(divide(sF0_fnc,multiply(divide(X0,multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)),a2))),
inference(forward_demodulation,[status(thm)],[f1532,f26839]) ).
fof(f34276,plain,
! [X0] : multiply(divide(inverse(divide(sF0_fnc,X0)),sF1_fnc),a2) = inverse(divide(sF1_fnc,multiply(divide(X0,sF1_fnc),divide(sF0_fnc,sF0_fnc)))),
inference(paramodulation,[status(thm)],[f16203,f5747]) ).
fof(f34384,plain,
! [X0] : X0 = inverse(divide(sF1_fnc,multiply(divide(X0,sF1_fnc),divide(sF0_fnc,sF0_fnc)))),
inference(forward_demodulation,[status(thm)],[f5674,f34276]) ).
fof(f41314,plain,
! [X0,X1] : inverse(divide(multiply(X0,a2),sF0_fnc)) = inverse(divide(multiply(X0,X1),multiply(sF1_fnc,X1))),
inference(paramodulation,[status(thm)],[f9,f21204]) ).
fof(f46497,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : divide(divide(inverse(divide(divide(multiply(X0,X1),divide(inverse(divide(divide(X2,X3),divide(X4,X3))),multiply(divide(X5,X6),divide(divide(divide(X6,X5),X7),divide(X2,X7))))),X8)),divide(inverse(X1),X0)),X4) = X8,
inference(paramodulation,[status(thm)],[f208,f199]) ).
fof(f46982,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(divide(multiply(X0,X1),X2),X3)),divide(inverse(X1),X0)),X2) = X3,
inference(forward_demodulation,[status(thm)],[f24,f46497]) ).
fof(f47033,plain,
divide(sF2_fnc,multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2))))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f7,f24958]) ).
fof(f47485,plain,
! [X0] : divide(X0,sF1_fnc) = divide(X0,multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc)),
inference(paramodulation,[status(thm)],[f27021,f41]) ).
fof(f47541,plain,
multiply(divide(inverse(divide(sF0_fnc,sF1_fnc)),sF1_fnc),a2) = multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f47485,f5674]) ).
fof(f47949,plain,
sF1_fnc = multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5674,f47541]) ).
fof(f48173,plain,
multiply(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f47949,f5673]) ).
fof(f48175,plain,
! [X0] : divide(inverse(divide(sF1_fnc,multiply(X0,sF1_fnc))),divide(inverse(sF1_fnc),sF1_fnc)) = X0,
inference(paramodulation,[status(thm)],[f47949,f82]) ).
fof(f63430,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(inverse(divide(sF1_fnc,multiply(divide(X1,sF1_fnc),divide(sF0_fnc,sF0_fnc)))),X0)),X2) = X3,
inference(paramodulation,[status(thm)],[f16203,f46982]) ).
fof(f64001,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(divide(divide(X0,X1),X2),X3)),divide(X1,X0)),X2) = X3,
inference(forward_demodulation,[status(thm)],[f34384,f63430]) ).
fof(f64104,plain,
! [X0,X1,X2,X3] : multiply(divide(inverse(divide(divide(divide(X0,X1),inverse(X2)),X3)),divide(X1,X0)),X2) = X3,
inference(paramodulation,[status(thm)],[f5,f64001]) ).
fof(f64743,plain,
! [X0,X1,X2,X3] : multiply(divide(inverse(divide(multiply(divide(X0,X1),X2),X3)),divide(X1,X0)),X2) = X3,
inference(forward_demodulation,[status(thm)],[f5,f64104]) ).
fof(f65043,plain,
! [X0] : multiply(divide(inverse(divide(inverse(sF1_fnc),X0)),divide(sF1_fnc,inverse(sF1_fnc))),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f48173,f64743]) ).
fof(f65050,plain,
! [X0,X1] : multiply(divide(inverse(divide(X0,X1)),divide(sF1_fnc,inverse(divide(sF0_fnc,X0)))),a2) = X1,
inference(paramodulation,[status(thm)],[f5674,f64743]) ).
fof(f65384,plain,
! [X0] : multiply(divide(inverse(divide(inverse(sF1_fnc),X0)),multiply(sF1_fnc,sF1_fnc)),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f65043]) ).
fof(f65391,plain,
! [X0,X1] : multiply(divide(inverse(divide(X0,X1)),multiply(sF1_fnc,divide(sF0_fnc,X0))),a2) = X1,
inference(forward_demodulation,[status(thm)],[f5,f65050]) ).
fof(f67747,plain,
multiply(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF0_fnc,sF2_fnc))),a2) = sF2_fnc,
inference(paramodulation,[status(thm)],[f12,f65391]) ).
fof(f68919,plain,
multiply(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF0_fnc,sF2_fnc))),a2) = multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2)))),
inference(paramodulation,[status(thm)],[f47033,f65391]) ).
fof(f69187,plain,
sF2_fnc = multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2)))),
inference(forward_demodulation,[status(thm)],[f67747,f68919]) ).
fof(f69270,plain,
inverse(divide(multiply(sF1_fnc,a2),sF0_fnc)) = inverse(divide(sF2_fnc,multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2)))))),
inference(paramodulation,[status(thm)],[f69187,f41314]) ).
fof(f69299,plain,
! [X0] : divide(inverse(divide(X0,sF2_fnc)),multiply(sF1_fnc,divide(multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2)))),X0))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f69187,f5680]) ).
fof(f69344,plain,
inverse(divide(sF0_fnc,sF0_fnc)) = inverse(divide(sF2_fnc,multiply(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,multiply(b2,a2)))))),
inference(forward_demodulation,[status(thm)],[f9,f69270]) ).
fof(f69345,plain,
inverse(divide(sF0_fnc,sF0_fnc)) = inverse(divide(sF2_fnc,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f69187,f69344]) ).
fof(f69346,plain,
inverse(divide(sF0_fnc,sF0_fnc)) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f12,f69345]) ).
fof(f69360,plain,
! [X0] : divide(inverse(divide(X0,sF2_fnc)),multiply(sF1_fnc,divide(sF2_fnc,X0))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f69187,f69299]) ).
fof(f69378,plain,
divide(inverse(sF1_fnc),sF1_fnc) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f69346,f50]) ).
fof(f69426,plain,
! [X0] : divide(inverse(divide(sF1_fnc,multiply(X0,sF1_fnc))),sF1_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f69378,f48175]) ).
fof(f69429,plain,
multiply(divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f69378,f65384]) ).
fof(f69727,plain,
multiply(sF1_fnc,sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f24960,f69429]) ).
fof(f69925,plain,
! [X0,X1] : X0 = inverse(divide(X1,multiply(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,X1))),sF1_fnc))),
inference(paramodulation,[status(thm)],[f69727,f5734]) ).
fof(f69930,plain,
multiply(divide(inverse(sF1_fnc),sF1_fnc),divide(sF0_fnc,sF0_fnc)) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f69727,f16200]) ).
fof(f69932,plain,
! [X0] : multiply(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f69727,f5564]) ).
fof(f69933,plain,
! [X0] : inverse(divide(sF0_fnc,multiply(X0,a2))) = inverse(divide(sF1_fnc,multiply(X0,sF1_fnc))),
inference(paramodulation,[status(thm)],[f69727,f1532]) ).
fof(f69934,plain,
! [X0,X1] : multiply(X0,divide(sF1_fnc,multiply(divide(X1,sF1_fnc),sF1_fnc))) = divide(X0,X1),
inference(paramodulation,[status(thm)],[f69727,f1548]) ).
fof(f70010,plain,
multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f69378,f69930]) ).
fof(f70011,plain,
sF1_fnc = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f16096,f70010]) ).
fof(f70081,plain,
divide(sF1_fnc,sF1_fnc) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f70011,f69378]) ).
fof(f70082,plain,
inverse(divide(sF0_fnc,sF0_fnc)) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f70011,f69346]) ).
fof(f70122,plain,
! [X0] : multiply(X0,sF1_fnc) = divide(X0,sF1_fnc),
inference(paramodulation,[status(thm)],[f70011,f5]) ).
fof(f70157,plain,
multiply(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF0_fnc,sF1_fnc))),a2) = sF1_fnc,
inference(paramodulation,[status(thm)],[f70081,f65391]) ).
fof(f70432,plain,
multiply(divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,sF1_fnc))),a2) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f70011,f70157]) ).
fof(f77769,plain,
! [X0] : divide(inverse(divide(sF1_fnc,divide(X0,sF1_fnc))),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f70122,f69426]) ).
fof(f78364,plain,
! [X0] : divide(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f70122,f69932]) ).
fof(f78381,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,inverse(divide(sF1_fnc,X0)))),sF1_fnc) = X1,
inference(paramodulation,[status(thm)],[f78364,f64001]) ).
fof(f78699,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),multiply(sF1_fnc,divide(sF1_fnc,X0))),sF1_fnc) = X1,
inference(forward_demodulation,[status(thm)],[f5,f78381]) ).
fof(f84511,plain,
! [X0] : divide(inverse(divide(multiply(sF1_fnc,a2),sF0_fnc)),multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc))) = sF1_fnc,
inference(paramodulation,[status(thm)],[f69360,f339]) ).
fof(f84847,plain,
! [X0] : divide(inverse(divide(sF0_fnc,sF0_fnc)),multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f9,f84511]) ).
fof(f84848,plain,
! [X0] : divide(sF1_fnc,multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc))) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f70082,f84847]) ).
fof(f87411,plain,
! [X0,X1] : multiply(X0,divide(sF1_fnc,divide(divide(X1,sF1_fnc),sF1_fnc))) = divide(X0,X1),
inference(forward_demodulation,[status(thm)],[f70122,f69934]) ).
fof(f88307,plain,
divide(divide(inverse(sF1_fnc),sF1_fnc),multiply(sF1_fnc,divide(sF0_fnc,sF1_fnc))) = inverse(a2),
inference(paramodulation,[status(thm)],[f70432,f5805]) ).
fof(f88405,plain,
divide(divide(sF1_fnc,sF1_fnc),multiply(sF1_fnc,divide(sF0_fnc,sF1_fnc))) = inverse(a2),
inference(forward_demodulation,[status(thm)],[f70011,f88307]) ).
fof(f88406,plain,
divide(sF1_fnc,multiply(sF1_fnc,divide(sF0_fnc,sF1_fnc))) = inverse(a2),
inference(forward_demodulation,[status(thm)],[f70081,f88405]) ).
fof(f88427,plain,
multiply(inverse(a2),a2) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f88406,f70432]) ).
fof(f88936,plain,
divide(inverse(divide(sF0_fnc,sF1_fnc)),sF1_fnc) = inverse(a2),
inference(paramodulation,[status(thm)],[f88427,f41]) ).
fof(f93936,plain,
divide(inverse(divide(sF1_fnc,inverse(a2))),sF1_fnc) = inverse(divide(sF0_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f88936,f77769]) ).
fof(f94264,plain,
divide(inverse(multiply(sF1_fnc,a2)),sF1_fnc) = inverse(divide(sF0_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f93936]) ).
fof(f94265,plain,
divide(inverse(sF0_fnc),sF1_fnc) = inverse(divide(sF0_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f9,f94264]) ).
fof(f105452,plain,
! [X0,X1] : X0 = inverse(divide(X1,divide(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,X1))),sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f70122,f69925]) ).
fof(f106347,plain,
! [X0] : inverse(divide(sF0_fnc,multiply(X0,a2))) = inverse(divide(sF1_fnc,divide(X0,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f70122,f69933]) ).
fof(f123039,plain,
! [X0] : divide(divide(inverse(sF1_fnc),multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f84848,f78699]) ).
fof(f123425,plain,
! [X0] : divide(divide(sF1_fnc,multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70011,f123039]) ).
fof(f123426,plain,
! [X0] : divide(divide(sF1_fnc,multiply(sF1_fnc,sF1_fnc)),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70081,f123425]) ).
fof(f123427,plain,
! [X0] : divide(divide(sF1_fnc,divide(sF1_fnc,sF1_fnc)),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70122,f123426]) ).
fof(f123428,plain,
! [X0] : divide(divide(sF1_fnc,sF1_fnc),sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70081,f123427]) ).
fof(f123429,plain,
! [X0] : divide(sF1_fnc,sF1_fnc) = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70081,f123428]) ).
fof(f123430,plain,
! [X0] : sF1_fnc = multiply(multiply(sF1_fnc,divide(sF2_fnc,X0)),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70081,f123429]) ).
fof(f123575,plain,
! [X0] : multiply(divide(inverse(sF1_fnc),sF1_fnc),divide(sF2_fnc,X0)) = inverse(divide(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f123430,f5673]) ).
fof(f123690,plain,
! [X0] : multiply(divide(sF1_fnc,sF1_fnc),divide(sF2_fnc,X0)) = inverse(divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70011,f123575]) ).
fof(f123691,plain,
! [X0] : multiply(sF1_fnc,divide(sF2_fnc,X0)) = inverse(divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f70081,f123690]) ).
fof(f123753,plain,
! [X0] : sF1_fnc = multiply(inverse(divide(X0,sF2_fnc)),divide(X0,sF2_fnc)),
inference(backward_demodulation,[status(thm)],[f123691,f123430]) ).
fof(f123924,plain,
! [X0,X1,X2] : sF1_fnc = multiply(inverse(X0),divide(divide(inverse(divide(divide(multiply(X1,X2),sF2_fnc),X0)),divide(inverse(X2),X1)),sF2_fnc)),
inference(paramodulation,[status(thm)],[f46982,f123753]) ).
fof(f124058,plain,
! [X0] : sF1_fnc = multiply(inverse(X0),X0),
inference(forward_demodulation,[status(thm)],[f46982,f123924]) ).
fof(f124225,plain,
! [X0] : sF1_fnc = divide(inverse(divide(sF1_fnc,divide(divide(X0,sF1_fnc),sF1_fnc))),X0),
inference(paramodulation,[status(thm)],[f87411,f124058]) ).
fof(f124393,plain,
! [X0] : sF1_fnc = divide(inverse(divide(sF0_fnc,multiply(divide(X0,sF1_fnc),a2))),X0),
inference(forward_demodulation,[status(thm)],[f106347,f124225]) ).
fof(f124394,plain,
! [X0] : sF1_fnc = divide(X0,X0),
inference(forward_demodulation,[status(thm)],[f1529,f124393]) ).
fof(f124586,plain,
! [X0,X1] : divide(inverse(sF1_fnc),divide(X0,X1)) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f124394,f23]) ).
fof(f125362,plain,
! [X0,X1] : divide(sF1_fnc,divide(X0,X1)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f70011,f124586]) ).
fof(f145772,plain,
! [X0] : X0 = inverse(divide(sF1_fnc,divide(X0,multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))))),
inference(paramodulation,[status(thm)],[f125362,f105452]) ).
fof(f146318,plain,
! [X0] : X0 = inverse(divide(multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),X0)),
inference(forward_demodulation,[status(thm)],[f125362,f145772]) ).
fof(f146319,plain,
! [X0] : X0 = inverse(divide(multiply(sF1_fnc,sF1_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f124394,f146318]) ).
fof(f146320,plain,
! [X0] : X0 = inverse(divide(divide(sF1_fnc,sF1_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f70122,f146319]) ).
fof(f146321,plain,
! [X0] : X0 = inverse(divide(sF1_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f124394,f146320]) ).
fof(f146445,plain,
! [X0] : divide(divide(X0,multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc))),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f105452,f146321]) ).
fof(f146449,plain,
! [X0,X1] : divide(X0,X1) = inverse(divide(X1,X0)),
inference(paramodulation,[status(thm)],[f125362,f146321]) ).
fof(f146529,plain,
! [X0] : divide(divide(X0,multiply(sF1_fnc,sF1_fnc)),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f124394,f146445]) ).
fof(f146530,plain,
! [X0] : divide(divide(X0,divide(sF1_fnc,sF1_fnc)),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f70122,f146529]) ).
fof(f146531,plain,
! [X0] : divide(divide(X0,sF1_fnc),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f124394,f146530]) ).
fof(f146562,plain,
divide(inverse(divide(sF0_fnc,sF1_fnc)),sF1_fnc) = inverse(sF0_fnc),
inference(paramodulation,[status(thm)],[f94265,f146531]) ).
fof(f146989,plain,
inverse(a2) = inverse(sF0_fnc),
inference(forward_demodulation,[status(thm)],[f88936,f146562]) ).
fof(f147281,plain,
! [X0] : X0 = divide(X0,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f146449,f146321]) ).
fof(f147432,plain,
! [X0] : divide(sF1_fnc,divide(X0,sF1_fnc)) = inverse(X0),
inference(paramodulation,[status(thm)],[f146531,f146449]) ).
fof(f147526,plain,
! [X0] : divide(sF1_fnc,X0) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f125362,f147432]) ).
fof(f147561,plain,
! [X0] : divide(X0,sF1_fnc) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f147526,f146449]) ).
fof(f147564,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f147281,f147561]) ).
fof(f147566,plain,
sF0_fnc = inverse(inverse(a2)),
inference(paramodulation,[status(thm)],[f146989,f147564]) ).
fof(f147573,plain,
sF0_fnc = a2,
inference(forward_demodulation,[status(thm)],[f147564,f147566]) ).
fof(f147574,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f147573,f10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP476-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n004.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 20:14:05 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 181.55/23.34 % Refutation found
% 181.55/23.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 181.55/23.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 102.62/23.49 % Elapsed time: 23.099198 seconds
% 102.62/23.49 % CPU time: 182.697444 seconds
% 102.62/23.49 % Total memory used: 1.154 GB
% 102.62/23.49 % Net memory used: 1.132 GB
%------------------------------------------------------------------------------