%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP473-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 : n012.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 31.52s 9.34s
% Output : CNFRefutation 23.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 6
% Syntax : Number of formulae : 169 ( 169 unt; 3 def)
% Number of atoms : 169 ( 168 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 2 avg)
% Maximal term depth : 9 ( 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 : 246 ( 246 !; 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/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(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(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,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(f14,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),divide(divide(X0,X1),sF2_fnc)),divide(X1,X0)) = sF2_fnc,
inference(paramodulation,[status(thm)],[f12,f4]) ).
fof(f15,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(f19,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)),divide(sF2_fnc,sF2_fnc)) = X1,
inference(paramodulation,[status(thm)],[f12,f4]) ).
fof(f20,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f23,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(f25,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)),sF1_fnc) = X1,
inference(forward_demodulation,[status(thm)],[f12,f19]) ).
fof(f27,plain,
! [X0,X1] : divide(divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(X1,X0)),divide(sF1_fnc,X1)))),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f25,f25]) ).
fof(f30,plain,
! [X0,X1] : divide(divide(inverse(multiply(X0,X1)),divide(sF1_fnc,X0)),sF1_fnc) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f25]) ).
fof(f31,plain,
! [X0,X1] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(sF1_fnc,X0)),sF1_fnc) = X1,
inference(paramodulation,[status(thm)],[f5,f25]) ).
fof(f35,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF1_fnc,X3)))),divide(X2,X1)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f25,f4]) ).
fof(f57,plain,
! [X0] : divide(divide(inverse(divide(inverse(a2),X0)),sF0_fnc),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f9,f31]) ).
fof(f67,plain,
! [X0] : divide(divide(inverse(multiply(inverse(a2),X0)),sF0_fnc),sF1_fnc) = inverse(X0),
inference(paramodulation,[status(thm)],[f5,f57]) ).
fof(f69,plain,
! [X0] : divide(divide(inverse(X0),divide(sF1_fnc,divide(inverse(divide(inverse(a2),X0)),sF0_fnc))),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f57,f25]) ).
fof(f113,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,f13]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1)) = divide(divide(sF1_fnc,X4),inverse(divide(X4,X3))),
inference(paramodulation,[status(thm)],[f25,f13]) ).
fof(f124,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,f13]) ).
fof(f126,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(inverse(X3),X0)),multiply(divide(X4,X5),X3)))),divide(X2,X1)) = divide(X5,X4),
inference(paramodulation,[status(thm)],[f5,f13]) ).
fof(f133,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(X4,X3)))),divide(X2,X1)) = divide(sF1_fnc,divide(inverse(divide(X5,X4)),divide(sF1_fnc,X5))),
inference(paramodulation,[status(thm)],[f25,f13]) ).
fof(f135,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)],[f13,f13]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(multiply(X4,X5),X3)))),divide(X2,X1)) = divide(inverse(X5),X4),
inference(paramodulation,[status(thm)],[f5,f13]) ).
fof(f168,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(sF1_fnc,X0)),X3))),divide(X2,X1)) = multiply(divide(sF1_fnc,X4),divide(X4,X3)),
inference(forward_demodulation,[status(thm)],[f5,f123]) ).
fof(f169,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,f124]) ).
fof(f171,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)],[f13,f135]) ).
fof(f250,plain,
! [X0,X1] : divide(divide(inverse(sF0_fnc),divide(divide(X0,X1),sF1_fnc)),divide(X1,X0)) = inverse(a2),
inference(paramodulation,[status(thm)],[f9,f15]) ).
fof(f421,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF0_fnc,X0)),divide(inverse(a2),sF1_fnc)) = X1,
inference(paramodulation,[status(thm)],[f9,f20]) ).
fof(f808,plain,
! [X0,X1] : divide(divide(inverse(sF0_fnc),divide(divide(inverse(X0),X1),sF1_fnc)),multiply(X1,X0)) = inverse(a2),
inference(paramodulation,[status(thm)],[f5,f250]) ).
fof(f809,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(divide(X0,X1),X2)),inverse(a2)),multiply(divide(divide(X1,X0),sF1_fnc),sF0_fnc)) = X2,
inference(paramodulation,[status(thm)],[f250,f23]) ).
fof(f851,plain,
! [X0,X1,X2] : divide(multiply(inverse(divide(divide(X0,X1),X2)),a2),multiply(divide(divide(X1,X0),sF1_fnc),sF0_fnc)) = X2,
inference(forward_demodulation,[status(thm)],[f5,f809]) ).
fof(f1559,plain,
! [X0,X1] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(sF0_fnc,X0)),divide(inverse(a2),sF1_fnc)) = X1,
inference(paramodulation,[status(thm)],[f5,f421]) ).
fof(f15504,plain,
! [X0] : sF1_fnc = multiply(divide(sF1_fnc,X0),divide(X0,divide(sF1_fnc,sF1_fnc))),
inference(paramodulation,[status(thm)],[f35,f168]) ).
fof(f15505,plain,
! [X0,X1,X2] : divide(X0,X1) = multiply(divide(sF1_fnc,X2),divide(X2,divide(divide(X1,X0),sF1_fnc))),
inference(paramodulation,[status(thm)],[f13,f168]) ).
fof(f16106,plain,
! [X0] : sF1_fnc = multiply(multiply(sF1_fnc,X0),divide(inverse(X0),divide(sF1_fnc,sF1_fnc))),
inference(paramodulation,[status(thm)],[f5,f15504]) ).
fof(f16152,plain,
sF1_fnc = multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc))),
inference(paramodulation,[status(thm)],[f9,f16106]) ).
fof(f16480,plain,
! [X0,X1] : divide(sF0_fnc,inverse(multiply(inverse(a2),X0))) = multiply(divide(sF1_fnc,X1),divide(X1,inverse(X0))),
inference(paramodulation,[status(thm)],[f67,f15505]) ).
fof(f16484,plain,
! [X0,X1] : divide(sF0_fnc,inverse(divide(inverse(a2),X0))) = multiply(divide(sF1_fnc,X1),divide(X1,X0)),
inference(paramodulation,[status(thm)],[f57,f15505]) ).
fof(f16613,plain,
! [X0,X1] : multiply(sF0_fnc,multiply(inverse(a2),X0)) = multiply(divide(sF1_fnc,X1),divide(X1,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f5,f16480]) ).
fof(f16614,plain,
! [X0,X1] : multiply(sF0_fnc,multiply(inverse(a2),X0)) = multiply(divide(sF1_fnc,X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f5,f16613]) ).
fof(f16620,plain,
! [X0,X1] : multiply(sF0_fnc,divide(inverse(a2),X0)) = multiply(divide(sF1_fnc,X1),divide(X1,X0)),
inference(forward_demodulation,[status(thm)],[f5,f16484]) ).
fof(f16779,plain,
! [X0,X1,X2] : sF1_fnc = multiply(divide(divide(X0,X1),X2),divide(X2,divide(sF1_fnc,divide(X1,X0)))),
inference(paramodulation,[status(thm)],[f35,f169]) ).
fof(f19342,plain,
! [X0,X1] : divide(X0,X1) = multiply(sF0_fnc,divide(inverse(a2),divide(divide(X1,X0),sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f16620,f15505]) ).
fof(f20712,plain,
! [X0] : sF1_fnc = divide(sF1_fnc,divide(inverse(divide(X0,sF1_fnc)),divide(sF1_fnc,X0))),
inference(paramodulation,[status(thm)],[f35,f133]) ).
fof(f23475,plain,
! [X0] : sF1_fnc = divide(sF1_fnc,divide(inverse(divide(divide(inverse(divide(X0,sF1_fnc)),divide(sF1_fnc,X0)),sF1_fnc)),sF1_fnc)),
inference(paramodulation,[status(thm)],[f20712,f20712]) ).
fof(f23482,plain,
divide(divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f20712,f27]) ).
fof(f23633,plain,
sF1_fnc = divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f25,f23475]) ).
fof(f23738,plain,
! [X0] : sF1_fnc = multiply(divide(divide(sF1_fnc,inverse(sF1_fnc)),X0),divide(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f23633,f16779]) ).
fof(f23887,plain,
! [X0] : sF1_fnc = multiply(divide(multiply(sF1_fnc,sF1_fnc),X0),divide(X0,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f23738]) ).
fof(f23900,plain,
divide(divide(inverse(sF0_fnc),sF1_fnc),multiply(sF1_fnc,sF1_fnc)) = inverse(a2),
inference(paramodulation,[status(thm)],[f23482,f808]) ).
fof(f23902,plain,
! [X0] : divide(divide(inverse(divide(sF1_fnc,X0)),sF1_fnc),multiply(sF1_fnc,sF1_fnc)) = X0,
inference(paramodulation,[status(thm)],[f23482,f23]) ).
fof(f23903,plain,
divide(sF1_fnc,inverse(sF1_fnc)) = multiply(sF0_fnc,divide(inverse(a2),sF1_fnc)),
inference(paramodulation,[status(thm)],[f23482,f19342]) ).
fof(f24065,plain,
multiply(sF1_fnc,sF1_fnc) = multiply(sF0_fnc,divide(inverse(a2),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f23903]) ).
fof(f24205,plain,
! [X0] : sF1_fnc = multiply(multiply(multiply(sF1_fnc,sF1_fnc),X0),divide(inverse(X0),sF1_fnc)),
inference(paramodulation,[status(thm)],[f5,f23887]) ).
fof(f24211,plain,
sF1_fnc = multiply(divide(multiply(sF1_fnc,sF1_fnc),divide(inverse(sF1_fnc),sF1_fnc)),sF1_fnc),
inference(paramodulation,[status(thm)],[f23482,f23887]) ).
fof(f25229,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),divide(X2,X3)) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f171,f113]) ).
fof(f25896,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF1_fnc,X3)))),divide(X2,X1)) = divide(inverse(divide(inverse(a2),divide(sF1_fnc,sF1_fnc))),sF0_fnc),
inference(paramodulation,[status(thm)],[f16152,f137]) ).
fof(f25898,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF1_fnc,X3)))),divide(X2,X1)) = divide(inverse(divide(X4,sF1_fnc)),divide(multiply(sF1_fnc,sF1_fnc),X4)),
inference(paramodulation,[status(thm)],[f23887,f137]) ).
fof(f26268,plain,
sF1_fnc = divide(inverse(divide(inverse(a2),divide(sF1_fnc,sF1_fnc))),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f35,f25896]) ).
fof(f26270,plain,
! [X0] : sF1_fnc = divide(inverse(divide(X0,sF1_fnc)),divide(multiply(sF1_fnc,sF1_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f35,f25898]) ).
fof(f26449,plain,
divide(divide(inverse(sF1_fnc),multiply(sF0_fnc,divide(inverse(a2),divide(sF1_fnc,sF1_fnc)))),divide(inverse(a2),sF1_fnc)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f26268,f1559]) ).
fof(f26601,plain,
divide(divide(inverse(sF1_fnc),sF1_fnc),divide(inverse(a2),sF1_fnc)) = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f16152,f26449]) ).
fof(f27418,plain,
divide(divide(inverse(sF0_fnc),divide(sF1_fnc,divide(inverse(sF1_fnc),sF1_fnc))),sF1_fnc) = divide(inverse(a2),sF1_fnc),
inference(paramodulation,[status(thm)],[f26601,f25]) ).
fof(f27459,plain,
divide(divide(inverse(sF0_fnc),sF1_fnc),sF1_fnc) = divide(inverse(a2),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f23633,f27418]) ).
fof(f27514,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(inverse(X3),X0)),multiply(divide(inverse(a2),sF1_fnc),X3)))),divide(X2,X1)) = divide(sF1_fnc,divide(inverse(sF0_fnc),sF1_fnc)),
inference(paramodulation,[status(thm)],[f27459,f126]) ).
fof(f27656,plain,
divide(sF1_fnc,inverse(a2)) = divide(sF1_fnc,divide(inverse(sF0_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f126,f27514]) ).
fof(f27657,plain,
multiply(sF1_fnc,a2) = divide(sF1_fnc,divide(inverse(sF0_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f27656]) ).
fof(f27658,plain,
sF0_fnc = divide(sF1_fnc,divide(inverse(sF0_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f9,f27657]) ).
fof(f27702,plain,
! [X0] : sF1_fnc = multiply(divide(divide(sF1_fnc,inverse(sF0_fnc)),X0),divide(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f27658,f16779]) ).
fof(f27703,plain,
divide(divide(inverse(sF0_fnc),sF1_fnc),multiply(sF1_fnc,sF1_fnc)) = divide(inverse(sF0_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f27658,f23902]) ).
fof(f27704,plain,
sF1_fnc = divide(sF1_fnc,divide(inverse(divide(divide(inverse(sF0_fnc),sF1_fnc),sF1_fnc)),sF0_fnc)),
inference(paramodulation,[status(thm)],[f27658,f20712]) ).
fof(f27852,plain,
! [X0] : sF1_fnc = multiply(divide(multiply(sF1_fnc,sF0_fnc),X0),divide(X0,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f27702]) ).
fof(f27853,plain,
inverse(a2) = divide(inverse(sF0_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f23900,f27703]) ).
fof(f27854,plain,
sF1_fnc = divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f27459,f27704]) ).
fof(f27964,plain,
sF1_fnc = multiply(multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc),inverse(a2)),
inference(paramodulation,[status(thm)],[f27853,f24205]) ).
fof(f27987,plain,
sF1_fnc = divide(inverse(inverse(a2)),divide(multiply(sF1_fnc,sF1_fnc),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f27853,f26270]) ).
fof(f28129,plain,
sF1_fnc = divide(inverse(inverse(a2)),multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f27987]) ).
fof(f37643,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),divide(multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc),inverse(inverse(a2)))),divide(X0,X1)) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f28129,f25229]) ).
fof(f37875,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF1_fnc) = divide(multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc),inverse(inverse(a2))),
inference(paramodulation,[status(thm)],[f28129,f25229]) ).
fof(f38228,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),multiply(multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc),inverse(a2))),divide(X0,X1)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f5,f37643]) ).
fof(f38229,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),sF1_fnc),divide(X0,X1)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f27964,f38228]) ).
fof(f38302,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF1_fnc) = multiply(multiply(multiply(sF1_fnc,sF1_fnc),sF0_fnc),inverse(a2)),
inference(forward_demodulation,[status(thm)],[f5,f37875]) ).
fof(f38303,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f27964,f38302]) ).
fof(f38556,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),sF1_fnc),divide(X0,X1)) = divide(divide(X1,X0),divide(inverse(sF1_fnc),sF1_fnc)),
inference(paramodulation,[status(thm)],[f38229,f38229]) ).
fof(f38900,plain,
! [X0,X1] : divide(X0,X1) = divide(divide(X0,X1),divide(inverse(sF1_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f38229,f38556]) ).
fof(f42132,plain,
! [X0,X1] : divide(divide(X0,X1),inverse(divide(X1,X0))) = multiply(sF0_fnc,divide(inverse(a2),sF1_fnc)),
inference(paramodulation,[status(thm)],[f38303,f19342]) ).
fof(f42414,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = multiply(sF0_fnc,divide(inverse(a2),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f42132]) ).
fof(f42415,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = multiply(sF1_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f24065,f42414]) ).
fof(f45848,plain,
divide(inverse(sF1_fnc),sF1_fnc) = divide(sF1_fnc,inverse(sF1_fnc)),
inference(paramodulation,[status(thm)],[f38229,f38900]) ).
fof(f45893,plain,
! [X0,X1,X2] : divide(multiply(inverse(divide(divide(X0,X1),X2)),a2),multiply(divide(divide(X1,X0),sF1_fnc),sF0_fnc)) = divide(X2,divide(inverse(sF1_fnc),sF1_fnc)),
inference(paramodulation,[status(thm)],[f851,f38900]) ).
fof(f46264,plain,
divide(inverse(sF1_fnc),sF1_fnc) = multiply(sF1_fnc,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f5,f45848]) ).
fof(f46298,plain,
! [X0] : X0 = divide(X0,divide(inverse(sF1_fnc),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f851,f45893]) ).
fof(f46558,plain,
sF1_fnc = multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f46298,f24211]) ).
fof(f53547,plain,
! [X0] : X0 = divide(X0,multiply(sF1_fnc,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f46264,f46298]) ).
fof(f53551,plain,
divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f46264,f23482]) ).
fof(f53553,plain,
sF1_fnc = multiply(multiply(multiply(sF1_fnc,sF1_fnc),sF1_fnc),multiply(sF1_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f46264,f24205]) ).
fof(f53774,plain,
sF1_fnc = multiply(sF1_fnc,multiply(sF1_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f46558,f53553]) ).
fof(f53981,plain,
! [X0] : divide(inverse(divide(sF1_fnc,X0)),sF1_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f53547,f23902]) ).
fof(f54395,plain,
sF1_fnc = divide(inverse(sF1_fnc),divide(multiply(sF1_fnc,sF1_fnc),multiply(sF1_fnc,sF1_fnc))),
inference(paramodulation,[status(thm)],[f53551,f26270]) ).
fof(f54599,plain,
sF1_fnc = divide(inverse(sF1_fnc),multiply(sF1_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f53547,f54395]) ).
fof(f54600,plain,
sF1_fnc = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f53547,f54599]) ).
fof(f54851,plain,
! [X0,X1] : divide(divide(sF1_fnc,divide(divide(X0,X1),sF2_fnc)),divide(X1,X0)) = sF2_fnc,
inference(backward_demodulation,[status(thm)],[f54600,f14]) ).
fof(f54876,plain,
divide(divide(sF1_fnc,divide(sF1_fnc,divide(inverse(divide(inverse(a2),sF1_fnc)),sF0_fnc))),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f54600,f69]) ).
fof(f54910,plain,
! [X0] : multiply(X0,sF1_fnc) = divide(X0,sF1_fnc),
inference(paramodulation,[status(thm)],[f54600,f5]) ).
fof(f54916,plain,
divide(divide(sF1_fnc,sF1_fnc),sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f27854,f54876]) ).
fof(f54929,plain,
! [X0] : X0 = divide(X0,divide(sF1_fnc,sF1_fnc)),
inference(backward_demodulation,[status(thm)],[f54910,f53547]) ).
fof(f54930,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = divide(sF1_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f54910,f42415]) ).
fof(f55074,plain,
sF1_fnc = multiply(sF0_fnc,inverse(a2)),
inference(backward_demodulation,[status(thm)],[f54929,f16152]) ).
fof(f55472,plain,
sF1_fnc = multiply(sF1_fnc,divide(sF1_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f54910,f53774]) ).
fof(f55505,plain,
divide(divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc) = inverse(divide(sF1_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f55472,f30]) ).
fof(f55521,plain,
divide(inverse(sF1_fnc),sF1_fnc) = inverse(divide(sF1_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f54929,f55505]) ).
fof(f55522,plain,
divide(sF1_fnc,sF1_fnc) = inverse(divide(sF1_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f54600,f55521]) ).
fof(f55524,plain,
divide(sF1_fnc,divide(divide(sF1_fnc,sF1_fnc),sF2_fnc)) = sF2_fnc,
inference(paramodulation,[status(thm)],[f54929,f54851]) ).
fof(f56969,plain,
divide(multiply(inverse(sF1_fnc),a2),multiply(divide(divide(sF1_fnc,sF1_fnc),sF1_fnc),sF0_fnc)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f54916,f851]) ).
fof(f57155,plain,
divide(multiply(sF1_fnc,a2),multiply(divide(divide(sF1_fnc,sF1_fnc),sF1_fnc),sF0_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f54600,f56969]) ).
fof(f57156,plain,
divide(sF0_fnc,multiply(divide(divide(sF1_fnc,sF1_fnc),sF1_fnc),sF0_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f9,f57155]) ).
fof(f57157,plain,
divide(sF0_fnc,multiply(sF1_fnc,sF0_fnc)) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f54916,f57156]) ).
fof(f60504,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF1_fnc) = divide(multiply(sF1_fnc,sF0_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f57157,f25229]) ).
fof(f60650,plain,
sF1_fnc = divide(multiply(sF1_fnc,sF0_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f38303,f60504]) ).
fof(f61328,plain,
sF1_fnc = multiply(sF1_fnc,divide(sF0_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f60650,f27852]) ).
fof(f61720,plain,
divide(divide(inverse(sF1_fnc),divide(sF1_fnc,sF1_fnc)),sF1_fnc) = inverse(divide(sF0_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f61328,f30]) ).
fof(f61739,plain,
divide(inverse(sF1_fnc),sF1_fnc) = inverse(divide(sF0_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f54929,f61720]) ).
fof(f61740,plain,
divide(sF1_fnc,sF1_fnc) = inverse(divide(sF0_fnc,sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f54600,f61739]) ).
fof(f65946,plain,
! [X0] : multiply(X0,divide(sF1_fnc,sF1_fnc)) = divide(X0,divide(sF1_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f55522,f5]) ).
fof(f66024,plain,
! [X0] : multiply(X0,divide(sF1_fnc,sF1_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f54929,f65946]) ).
fof(f66097,plain,
! [X0] : multiply(sF0_fnc,multiply(inverse(a2),divide(sF1_fnc,sF1_fnc))) = multiply(divide(sF1_fnc,X0),X0),
inference(paramodulation,[status(thm)],[f66024,f16614]) ).
fof(f66200,plain,
! [X0] : multiply(sF0_fnc,inverse(a2)) = multiply(divide(sF1_fnc,X0),X0),
inference(forward_demodulation,[status(thm)],[f66024,f66097]) ).
fof(f66201,plain,
! [X0] : sF1_fnc = multiply(divide(sF1_fnc,X0),X0),
inference(forward_demodulation,[status(thm)],[f55074,f66200]) ).
fof(f73588,plain,
! [X0] : multiply(X0,divide(sF0_fnc,sF0_fnc)) = divide(X0,divide(sF1_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f61740,f5]) ).
fof(f73605,plain,
! [X0] : multiply(X0,divide(sF0_fnc,sF0_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f54929,f73588]) ).
fof(f74174,plain,
sF1_fnc = divide(sF1_fnc,divide(sF0_fnc,sF0_fnc)),
inference(paramodulation,[status(thm)],[f66201,f73605]) ).
fof(f74388,plain,
divide(inverse(sF1_fnc),sF1_fnc) = divide(sF0_fnc,sF0_fnc),
inference(paramodulation,[status(thm)],[f74174,f53981]) ).
fof(f74589,plain,
divide(sF1_fnc,sF1_fnc) = divide(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f54600,f74388]) ).
fof(f74705,plain,
! [X0] : X0 = divide(X0,divide(sF0_fnc,sF0_fnc)),
inference(backward_demodulation,[status(thm)],[f74589,f54929]) ).
fof(f94092,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = divide(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f74589,f54930]) ).
fof(f95103,plain,
divide(sF1_fnc,divide(divide(sF0_fnc,sF0_fnc),sF2_fnc)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f74589,f55524]) ).
fof(f95108,plain,
! [X0] : sF1_fnc = multiply(divide(divide(sF2_fnc,divide(sF0_fnc,sF0_fnc)),X0),divide(X0,sF2_fnc)),
inference(paramodulation,[status(thm)],[f95103,f16779]) ).
fof(f95355,plain,
! [X0] : sF1_fnc = multiply(divide(sF2_fnc,X0),divide(X0,sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f74705,f95108]) ).
fof(f95356,plain,
sF1_fnc = divide(sF0_fnc,sF0_fnc),
inference(forward_demodulation,[status(thm)],[f94092,f95355]) ).
fof(f95411,plain,
! [X0,X1] : multiply(divide(X0,X1),divide(X1,X0)) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f95356,f94092]) ).
fof(f95418,plain,
! [X0] : X0 = divide(X0,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f95356,f74705]) ).
fof(f95903,plain,
inverse(a2) = inverse(sF0_fnc),
inference(backward_demodulation,[status(thm)],[f95418,f27853]) ).
fof(f95913,plain,
! [X0] : inverse(divide(sF1_fnc,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f95418,f53981]) ).
fof(f95925,plain,
! [X0,X1] : divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)) = X1,
inference(backward_demodulation,[status(thm)],[f95418,f25]) ).
fof(f95935,plain,
! [X0] : multiply(X0,sF1_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f95418,f54910]) ).
fof(f105133,plain,
! [X0] : multiply(X0,divide(sF1_fnc,X0)) = sF1_fnc,
inference(paramodulation,[status(thm)],[f95418,f95411]) ).
fof(f105472,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(X0,X1)),divide(sF1_fnc,X0)),divide(inverse(divide(sF1_fnc,X2)),X2)) = X1,
inference(paramodulation,[status(thm)],[f105133,f20]) ).
fof(f105612,plain,
! [X0,X1] : divide(X0,divide(inverse(divide(sF1_fnc,X1)),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f95925,f105472]) ).
fof(f105613,plain,
! [X0,X1] : divide(X0,divide(X1,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f95913,f105612]) ).
fof(f105662,plain,
! [X0] : multiply(divide(X0,X0),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f105613,f105133]) ).
fof(f106094,plain,
! [X0] : divide(X0,X0) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f95935,f105662]) ).
fof(f106372,plain,
! [X0] : divide(inverse(sF1_fnc),divide(sF1_fnc,X0)) = X0,
inference(paramodulation,[status(thm)],[f106094,f95925]) ).
fof(f106768,plain,
! [X0] : divide(sF1_fnc,divide(sF1_fnc,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f54600,f106372]) ).
fof(f110589,plain,
! [X0] : inverse(X0) = divide(sF1_fnc,X0),
inference(paramodulation,[status(thm)],[f106768,f95913]) ).
fof(f111050,plain,
! [X0] : inverse(divide(sF1_fnc,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f110589,f106768]) ).
fof(f111264,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f110589,f111050]) ).
fof(f111501,plain,
inverse(inverse(a2)) = sF0_fnc,
inference(paramodulation,[status(thm)],[f95903,f111264]) ).
fof(f111564,plain,
a2 = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f111264,f111501]) ).
fof(f111565,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f111564,f10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP473-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/5.31 % Computer : n012.cluster.edu
% 0.05/5.31 % Model : x86_64 x86_64
% 0.05/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.31 % Memory : 8046.5625MB
% 0.05/5.31 % OS : Linux 6.8.0-71-generic
% 0.05/5.31 % CPULimit : 300
% 0.05/5.31 % WCLimit : 300
% 0.05/5.31 % DateTime : Sun Sep 20 20:14:13 UTC 2026
% 0.05/5.31 % CPUTime :
% 0.05/5.32 % Drodi V4.1.1
% 31.52/9.34 % Refutation found
% 31.52/9.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 31.52/9.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.25/9.44 % Elapsed time: 4.113134 seconds
% 23.25/9.44 % CPU time: 32.612143 seconds
% 23.25/9.44 % Total memory used: 893.008 MB
% 23.25/9.44 % Net memory used: 875.306 MB
%------------------------------------------------------------------------------