%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP474-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:28 PM UTC 2026
% Result : Unsatisfiable 20.01s 3.01s
% Output : CNFRefutation 20.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 7
% Syntax : Number of formulae : 149 ( 149 unt; 4 def)
% Number of atoms : 149 ( 148 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 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 : 283 ( 283 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : divide(divide(inverse(divide(A,B)),divide(divide(C,D),A)),divide(D,C)) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(divide(X2,X3),X0)),divide(X3,X2)) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1] : multiply(X0,X1) = divide(X0,inverse(X1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f7,definition,
sF1_fnc = multiply(a3,b3),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f8,definition,
sF0_fnc = multiply(sF1_fnc,c3),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f9,definition,
sF3_fnc = multiply(b3,c3),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f10,definition,
sF2_fnc = multiply(a3,sF3_fnc),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f11,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X4,X5),X3)))),divide(X2,X1)) = divide(X5,X4),
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f14,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(divide(X0,X1)),divide(X2,X0)),divide(divide(X3,X4),divide(inverse(divide(X5,X2)),divide(divide(X4,X3),X5)))) = X1,
inference(paramodulation,[status(thm)],[f4,f4]) ).
fof(f17,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,X3),X0)),divide(X3,X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f19,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f4]) ).
fof(f24,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(multiply(X2,X3),X0)),divide(inverse(X3),X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f17]) ).
fof(f27,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(inverse(X0),X1)),multiply(divide(inverse(X2),X3),X0)),multiply(X3,X2)) = X1,
inference(paramodulation,[status(thm)],[f5,f17]) ).
fof(f36,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(multiply(X0,X1)),divide(multiply(X2,X3),X0)),divide(inverse(X3),X2)) = inverse(X1),
inference(paramodulation,[status(thm)],[f5,f19]) ).
fof(f38,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF3_fnc,X0)),divide(inverse(c3),b3)) = X1,
inference(paramodulation,[status(thm)],[f9,f19]) ).
fof(f39,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(sF0_fnc,X0)),divide(inverse(c3),sF1_fnc)) = X1,
inference(paramodulation,[status(thm)],[f8,f19]) ).
fof(f50,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(inverse(X1),X0)),multiply(divide(X2,X3),X1)))),divide(inverse(c3),b3)) = divide(X3,X2),
inference(paramodulation,[status(thm)],[f17,f38]) ).
fof(f51,plain,
! [X0,X1] : divide(divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(X1,X0)),divide(sF3_fnc,X1)))),divide(inverse(c3),b3)) = divide(inverse(c3),b3),
inference(paramodulation,[status(thm)],[f38,f38]) ).
fof(f78,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(sF0_fnc,X3)))),divide(X2,X1)) = divide(inverse(c3),sF1_fnc),
inference(paramodulation,[status(thm)],[f39,f4]) ).
fof(f168,plain,
! [X0,X1,X2,X3,X4,X5] : divide(divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(inverse(X1),X0)),multiply(divide(X2,X3),X1)))),divide(inverse(c3),b3)) = divide(divide(inverse(c3),b3),divide(inverse(X4),divide(sF3_fnc,divide(inverse(divide(inverse(X5),X4)),multiply(divide(X3,X2),X5))))),
inference(paramodulation,[status(thm)],[f50,f50]) ).
fof(f181,plain,
! [X0,X1,X2,X3] : divide(X0,X1) = divide(divide(inverse(c3),b3),divide(inverse(X2),divide(sF3_fnc,divide(inverse(divide(inverse(X3),X2)),multiply(divide(X0,X1),X3))))),
inference(forward_demodulation,[status(thm)],[f50,f168]) ).
fof(f202,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(inverse(X1),X0)),multiply(divide(inverse(c3),b3),X1)))),divide(inverse(c3),b3)) = divide(divide(inverse(c3),b3),divide(inverse(X2),divide(sF3_fnc,divide(inverse(divide(X3,X2)),divide(sF3_fnc,X3))))),
inference(paramodulation,[status(thm)],[f51,f50]) ).
fof(f211,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(c3),b3),X0)),divide(divide(inverse(c3),b3),divide(inverse(X2),divide(sF3_fnc,divide(inverse(divide(X3,X2)),divide(sF3_fnc,X3)))))) = X1,
inference(paramodulation,[status(thm)],[f51,f4]) ).
fof(f214,plain,
! [X0,X1] : divide(b3,inverse(c3)) = divide(divide(inverse(c3),b3),divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(X1,X0)),divide(sF3_fnc,X1))))),
inference(forward_demodulation,[status(thm)],[f50,f202]) ).
fof(f215,plain,
! [X0,X1] : multiply(b3,c3) = divide(divide(inverse(c3),b3),divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(X1,X0)),divide(sF3_fnc,X1))))),
inference(forward_demodulation,[status(thm)],[f5,f214]) ).
fof(f216,plain,
! [X0,X1] : sF3_fnc = divide(divide(inverse(c3),b3),divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(X1,X0)),divide(sF3_fnc,X1))))),
inference(forward_demodulation,[status(thm)],[f9,f215]) ).
fof(f220,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(c3),b3),X0)),sF3_fnc) = X1,
inference(forward_demodulation,[status(thm)],[f216,f211]) ).
fof(f232,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(divide(inverse(c3),b3),divide(inverse(X2),divide(sF3_fnc,divide(inverse(divide(inverse(X3),X2)),multiply(divide(X1,X0),X3)))))),sF3_fnc) = divide(inverse(c3),b3),
inference(paramodulation,[status(thm)],[f50,f220]) ).
fof(f250,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),divide(X1,X0)),sF3_fnc) = divide(inverse(c3),b3),
inference(forward_demodulation,[status(thm)],[f181,f232]) ).
fof(f315,plain,
! [X0,X1] : divide(divide(inverse(sF3_fnc),divide(multiply(X0,X1),b3)),divide(inverse(X1),X0)) = inverse(c3),
inference(paramodulation,[status(thm)],[f9,f36]) ).
fof(f317,plain,
! [X0,X1] : divide(divide(inverse(sF2_fnc),divide(multiply(X0,X1),a3)),divide(inverse(X1),X0)) = inverse(sF3_fnc),
inference(paramodulation,[status(thm)],[f10,f36]) ).
fof(f384,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(X0),divide(sF3_fnc,divide(inverse(divide(inverse(X1),X0)),multiply(divide(inverse(c3),b3),X1)))),divide(inverse(c3),b3)) = divide(sF3_fnc,divide(inverse(divide(X2,X3)),divide(X3,X2))),
inference(paramodulation,[status(thm)],[f250,f50]) ).
fof(f401,plain,
! [X0,X1] : divide(b3,inverse(c3)) = divide(sF3_fnc,divide(inverse(divide(X0,X1)),divide(X1,X0))),
inference(forward_demodulation,[status(thm)],[f50,f384]) ).
fof(f402,plain,
! [X0,X1] : multiply(b3,c3) = divide(sF3_fnc,divide(inverse(divide(X0,X1)),divide(X1,X0))),
inference(forward_demodulation,[status(thm)],[f5,f401]) ).
fof(f406,plain,
! [X0,X1] : sF3_fnc = divide(sF3_fnc,divide(inverse(divide(X0,X1)),divide(X1,X0))),
inference(forward_demodulation,[status(thm)],[f9,f402]) ).
fof(f430,plain,
! [X0,X1] : sF3_fnc = divide(sF3_fnc,divide(inverse(multiply(X0,X1)),divide(inverse(X1),X0))),
inference(paramodulation,[status(thm)],[f5,f406]) ).
fof(f449,plain,
! [X0,X1] : sF3_fnc = divide(sF3_fnc,divide(inverse(divide(inverse(X0),X1)),multiply(X1,X0))),
inference(paramodulation,[status(thm)],[f5,f406]) ).
fof(f566,plain,
sF3_fnc = divide(sF3_fnc,divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc))),
inference(paramodulation,[status(thm)],[f8,f430]) ).
fof(f568,plain,
sF3_fnc = divide(sF3_fnc,divide(inverse(sF1_fnc),divide(inverse(b3),a3))),
inference(paramodulation,[status(thm)],[f7,f430]) ).
fof(f603,plain,
! [X0] : divide(divide(inverse(divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X0)),sF3_fnc),divide(inverse(c3),b3)) = X0,
inference(paramodulation,[status(thm)],[f566,f38]) ).
fof(f682,plain,
! [X0] : divide(divide(inverse(divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X0)),sF3_fnc),divide(inverse(c3),b3)) = X0,
inference(paramodulation,[status(thm)],[f568,f38]) ).
fof(f732,plain,
! [X0,X1] : divide(divide(inverse(divide(X0,X1)),sF3_fnc),divide(inverse(c3),b3)) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f449,f50]) ).
fof(f748,plain,
! [X0] : divide(X0,divide(inverse(sF1_fnc),divide(inverse(b3),a3))) = X0,
inference(backward_demodulation,[status(thm)],[f732,f682]) ).
fof(f749,plain,
! [X0] : divide(X0,divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f732,f603]) ).
fof(f908,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(X4,X3)))),divide(X2,X1)) = divide(divide(X5,X6),divide(inverse(divide(X7,X4)),divide(divide(X6,X5),X7))),
inference(paramodulation,[status(thm)],[f4,f12]) ).
fof(f1486,plain,
! [X0,X1,X2] : divide(divide(inverse(inverse(X0)),multiply(divide(inverse(X1),X2),X0)),multiply(X2,X1)) = divide(inverse(sF1_fnc),divide(inverse(b3),a3)),
inference(paramodulation,[status(thm)],[f748,f27]) ).
fof(f1510,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X0)),X1),divide(divide(X2,X3),divide(inverse(divide(X4,X1)),divide(divide(X3,X2),X4)))) = X0,
inference(paramodulation,[status(thm)],[f748,f14]) ).
fof(f1516,plain,
! [X0,X1,X2,X3,X4] : divide(divide(inverse(X0),divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(X4,X3)))),divide(X2,X1)) = divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X4),
inference(paramodulation,[status(thm)],[f748,f12]) ).
fof(f1547,plain,
! [X0,X1] : divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),divide(X0,X1)) = divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f1516,f12]) ).
fof(f1551,plain,
divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f1516,f78]) ).
fof(f1556,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X0) = divide(divide(X1,X2),divide(inverse(divide(X3,X0)),divide(divide(X2,X1),X3))),
inference(backward_demodulation,[status(thm)],[f1516,f908]) ).
fof(f1656,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X0)),X1),divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f1556,f1510]) ).
fof(f1972,plain,
! [X0,X1,X2] : divide(divide(inverse(inverse(X0)),multiply(divide(inverse(X1),X2),X0)),multiply(X2,X1)) = divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),
inference(paramodulation,[status(thm)],[f749,f27]) ).
fof(f2000,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(X0,X1)),divide(divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X2),X0)),X2) = X1,
inference(paramodulation,[status(thm)],[f749,f4]) ).
fof(f2039,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(sF1_fnc),divide(inverse(b3),a3)),X0)),X1),divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f2119,f1656]) ).
fof(f2068,plain,
divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f2119,f1551]) ).
fof(f2072,plain,
! [X0,X1] : divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),divide(X0,X1)) = divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f2119,f1547]) ).
fof(f2119,plain,
divide(inverse(sF1_fnc),divide(inverse(b3),a3)) = divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f1486,f1972]) ).
fof(f2146,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X0)),X1),divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2119,f2039]) ).
fof(f2203,plain,
divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)) = divide(divide(inverse(c3),sF1_fnc),inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f749,f2072]) ).
fof(f2224,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0)),divide(divide(inverse(c3),sF1_fnc),inverse(sF0_fnc))) = X2,
inference(paramodulation,[status(thm)],[f2072,f4]) ).
fof(f2234,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),divide(multiply(X2,X3),divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)))),divide(inverse(X3),X2)) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f2072,f19]) ).
fof(f2240,plain,
! [X0,X1] : divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),divide(X0,X1)) = divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f2311,f2072]) ).
fof(f2241,plain,
! [X0] : divide(X0,multiply(divide(inverse(c3),sF1_fnc),sF0_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f2311,f749]) ).
fof(f2252,plain,
divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f2311,f2068]) ).
fof(f2266,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)),X0)),X1),divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f2311,f2146]) ).
fof(f2290,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(X0,X1)),divide(divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),X2),X0)),X2) = X1,
inference(backward_demodulation,[status(thm)],[f2311,f2000]) ).
fof(f2311,plain,
divide(inverse(sF0_fnc),divide(inverse(c3),sF1_fnc)) = multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),
inference(forward_demodulation,[status(thm)],[f5,f2203]) ).
fof(f2331,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0)),multiply(divide(inverse(c3),sF1_fnc),sF0_fnc)) = X2,
inference(forward_demodulation,[status(thm)],[f5,f2224]) ).
fof(f2346,plain,
! [X0,X1,X2,X3] : divide(divide(inverse(divide(X0,X1)),multiply(X2,X3)),divide(inverse(X3),X2)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f749,f2234]) ).
fof(f2353,plain,
! [X0,X1,X2] : divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0)) = X2,
inference(backward_demodulation,[status(thm)],[f2241,f2331]) ).
fof(f2356,plain,
! [X0,X1] : divide(divide(inverse(divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),X0)),X1),divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2311,f2266]) ).
fof(f2379,plain,
! [X0] : divide(inverse(divide(inverse(sF0_fnc),X0)),multiply(sF1_fnc,c3)) = X0,
inference(paramodulation,[status(thm)],[f2241,f27]) ).
fof(f2417,plain,
! [X0] : divide(inverse(divide(inverse(sF0_fnc),X0)),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f8,f2379]) ).
fof(f2441,plain,
divide(inverse(inverse(sF0_fnc)),sF0_fnc) = multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),
inference(paramodulation,[status(thm)],[f2241,f2417]) ).
fof(f2442,plain,
! [X0] : divide(inverse(multiply(inverse(sF0_fnc),X0)),sF0_fnc) = inverse(X0),
inference(paramodulation,[status(thm)],[f5,f2417]) ).
fof(f2467,plain,
! [X0] : divide(X0,divide(inverse(inverse(sF0_fnc)),sF0_fnc)) = X0,
inference(backward_demodulation,[status(thm)],[f2441,f2241]) ).
fof(f2495,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(X0,X1)),divide(divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X2),X0)),X2) = X1,
inference(backward_demodulation,[status(thm)],[f2441,f2290]) ).
fof(f2519,plain,
! [X0,X1] : divide(divide(inverse(divide(multiply(divide(inverse(c3),sF1_fnc),sF0_fnc),X0)),X1),divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f2441,f2356]) ).
fof(f2533,plain,
divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f2441,f2252]) ).
fof(f2543,plain,
! [X0,X1] : divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),divide(X0,X1)) = divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f2441,f2240]) ).
fof(f2594,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X0)),X1),divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2441,f2519]) ).
fof(f2656,plain,
! [X0,X1] : X0 = divide(inverse(divide(inverse(X1),X0)),multiply(multiply(sF0_fnc,inverse(sF0_fnc)),X1)),
inference(paramodulation,[status(thm)],[f24,f2467]) ).
fof(f2717,plain,
divide(inverse(inverse(sF0_fnc)),sF0_fnc) = divide(sF0_fnc,inverse(inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f2467,f2543]) ).
fof(f2718,plain,
! [X0] : divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),inverse(X0)) = divide(sF0_fnc,inverse(multiply(inverse(sF0_fnc),X0))),
inference(paramodulation,[status(thm)],[f2442,f2543]) ).
fof(f2740,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(divide(X0,X1),X2)),divide(X1,X0)),divide(sF0_fnc,inverse(inverse(sF0_fnc)))) = X2,
inference(paramodulation,[status(thm)],[f2543,f4]) ).
fof(f2756,plain,
! [X0,X1] : divide(multiply(sF0_fnc,inverse(sF0_fnc)),divide(X0,X1)) = divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f2838,f2543]) ).
fof(f2786,plain,
divide(multiply(sF0_fnc,inverse(sF0_fnc)),sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f2838,f2533]) ).
fof(f2800,plain,
! [X0,X1] : divide(divide(inverse(divide(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X0)),X1),divide(multiply(sF0_fnc,inverse(sF0_fnc)),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f2838,f2594]) ).
fof(f2824,plain,
! [X0,X1,X2] : divide(divide(inverse(divide(X0,X1)),divide(divide(multiply(sF0_fnc,inverse(sF0_fnc)),X2),X0)),X2) = X1,
inference(backward_demodulation,[status(thm)],[f2838,f2495]) ).
fof(f2838,plain,
divide(inverse(inverse(sF0_fnc)),sF0_fnc) = multiply(sF0_fnc,inverse(sF0_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f2717]) ).
fof(f2839,plain,
! [X0] : multiply(divide(inverse(inverse(sF0_fnc)),sF0_fnc),X0) = divide(sF0_fnc,inverse(multiply(inverse(sF0_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f5,f2718]) ).
fof(f2840,plain,
! [X0] : multiply(multiply(sF0_fnc,inverse(sF0_fnc)),X0) = divide(sF0_fnc,inverse(multiply(inverse(sF0_fnc),X0))),
inference(forward_demodulation,[status(thm)],[f2838,f2839]) ).
fof(f2841,plain,
! [X0,X1] : X0 = divide(inverse(divide(inverse(X1),X0)),multiply(sF0_fnc,multiply(inverse(sF0_fnc),X1))),
inference(backward_demodulation,[status(thm)],[f2842,f2656]) ).
fof(f2842,plain,
! [X0] : multiply(multiply(sF0_fnc,inverse(sF0_fnc)),X0) = multiply(sF0_fnc,multiply(inverse(sF0_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f5,f2840]) ).
fof(f2873,plain,
! [X0] : divide(X0,divide(sF0_fnc,inverse(inverse(sF0_fnc)))) = X0,
inference(forward_demodulation,[status(thm)],[f2353,f2740]) ).
fof(f2874,plain,
! [X0] : divide(X0,multiply(sF0_fnc,inverse(sF0_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f5,f2873]) ).
fof(f2916,plain,
! [X0,X1] : divide(divide(inverse(divide(multiply(sF0_fnc,inverse(sF0_fnc)),X0)),X1),divide(multiply(sF0_fnc,inverse(sF0_fnc)),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2838,f2800]) ).
fof(f3485,plain,
! [X0,X1] : divide(inverse(divide(X0,X1)),divide(inverse(inverse(sF0_fnc)),sF0_fnc)) = divide(X1,X0),
inference(paramodulation,[status(thm)],[f2874,f2346]) ).
fof(f3544,plain,
! [X0,X1] : divide(inverse(divide(X0,X1)),multiply(sF0_fnc,inverse(sF0_fnc))) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f2838,f3485]) ).
fof(f3548,plain,
! [X0] : divide(divide(X0,inverse(sF0_fnc)),sF0_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f3878,f2417]) ).
fof(f3561,plain,
! [X0,X1,X2,X3] : divide(divide(divide(X0,X1),divide(multiply(X2,X3),X1)),divide(inverse(X3),X2)) = X0,
inference(backward_demodulation,[status(thm)],[f3878,f19]) ).
fof(f3573,plain,
! [X0,X1] : divide(divide(divide(X0,multiply(sF0_fnc,inverse(sF0_fnc))),X1),divide(multiply(sF0_fnc,inverse(sF0_fnc)),X1)) = X0,
inference(backward_demodulation,[status(thm)],[f3878,f2916]) ).
fof(f3637,plain,
! [X0,X1] : X0 = divide(divide(X0,inverse(X1)),multiply(sF0_fnc,multiply(inverse(sF0_fnc),X1))),
inference(backward_demodulation,[status(thm)],[f3878,f2841]) ).
fof(f3822,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),divide(divide(multiply(sF0_fnc,inverse(sF0_fnc)),X2),X1)),X2) = X0,
inference(backward_demodulation,[status(thm)],[f3878,f2824]) ).
fof(f3878,plain,
! [X0,X1] : inverse(divide(X0,X1)) = divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f2874,f3544]) ).
fof(f3981,plain,
! [X0] : divide(multiply(X0,sF0_fnc),sF0_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f3548]) ).
fof(f3996,plain,
! [X0,X1] : divide(divide(X0,X1),divide(multiply(sF0_fnc,inverse(sF0_fnc)),X1)) = X0,
inference(forward_demodulation,[status(thm)],[f2874,f3573]) ).
fof(f4101,plain,
! [X0,X1] : X0 = divide(multiply(X0,X1),multiply(sF0_fnc,multiply(inverse(sF0_fnc),X1))),
inference(forward_demodulation,[status(thm)],[f5,f3637]) ).
fof(f4267,plain,
! [X0] : divide(multiply(sF0_fnc,inverse(sF0_fnc)),X0) = divide(sF0_fnc,multiply(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f3981,f2756]) ).
fof(f4272,plain,
divide(sF0_fnc,multiply(sF0_fnc,sF0_fnc)) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f4267,f2786]) ).
fof(f4288,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),divide(divide(sF0_fnc,multiply(X2,sF0_fnc)),X1)),X2) = X0,
inference(backward_demodulation,[status(thm)],[f4267,f3822]) ).
fof(f4317,plain,
! [X0,X1] : divide(divide(X0,X1),divide(sF0_fnc,multiply(X1,sF0_fnc))) = X0,
inference(backward_demodulation,[status(thm)],[f4267,f3996]) ).
fof(f4351,plain,
! [X0] : inverse(X0) = divide(sF0_fnc,multiply(X0,sF0_fnc)),
inference(paramodulation,[status(thm)],[f3981,f3878]) ).
fof(f4353,plain,
! [X0] : inverse(inverse(X0)) = divide(sF0_fnc,inverse(multiply(inverse(sF0_fnc),X0))),
inference(paramodulation,[status(thm)],[f2442,f3878]) ).
fof(f4356,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = divide(inverse(X1),X0),
inference(paramodulation,[status(thm)],[f5,f3878]) ).
fof(f4472,plain,
inverse(sF0_fnc) = divide(inverse(c3),sF1_fnc),
inference(backward_demodulation,[status(thm)],[f4351,f4272]) ).
fof(f4483,plain,
! [X0,X1] : divide(divide(X0,X1),inverse(X1)) = X0,
inference(backward_demodulation,[status(thm)],[f4351,f4317]) ).
fof(f4501,plain,
! [X0,X1,X2] : divide(divide(divide(X0,X1),divide(inverse(X2),X1)),X2) = X0,
inference(backward_demodulation,[status(thm)],[f4351,f4288]) ).
fof(f4530,plain,
! [X0,X1] : X0 = divide(multiply(X0,X1),inverse(inverse(X1))),
inference(backward_demodulation,[status(thm)],[f4541,f4101]) ).
fof(f4541,plain,
! [X0] : inverse(inverse(X0)) = multiply(sF0_fnc,multiply(inverse(sF0_fnc),X0)),
inference(forward_demodulation,[status(thm)],[f5,f4353]) ).
fof(f4909,plain,
! [X0,X1] : multiply(divide(X0,X1),X1) = X0,
inference(forward_demodulation,[status(thm)],[f5,f4483]) ).
fof(f4972,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f5,f4530]) ).
fof(f5280,plain,
! [X0,X1] : divide(X0,X1) = multiply(X0,inverse(X1)),
inference(paramodulation,[status(thm)],[f4909,f4972]) ).
fof(f5284,plain,
a3 = multiply(sF1_fnc,inverse(b3)),
inference(paramodulation,[status(thm)],[f7,f4972]) ).
fof(f5288,plain,
! [X0,X1] : X0 = divide(multiply(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f5280,f4972]) ).
fof(f5299,plain,
a3 = divide(sF1_fnc,b3),
inference(forward_demodulation,[status(thm)],[f5280,f5284]) ).
fof(f5315,plain,
inverse(a3) = divide(b3,sF1_fnc),
inference(paramodulation,[status(thm)],[f5299,f3878]) ).
fof(f5326,plain,
! [X0,X1] : inverse(X0) = divide(X1,multiply(X0,X1)),
inference(paramodulation,[status(thm)],[f5288,f3878]) ).
fof(f5342,plain,
! [X0,X1,X2,X3] : divide(divide(X0,divide(multiply(X1,X2),X3)),divide(inverse(X2),X1)) = multiply(X0,X3),
inference(paramodulation,[status(thm)],[f5288,f3561]) ).
fof(f5371,plain,
multiply(inverse(sF2_fnc),a3) = inverse(sF3_fnc),
inference(backward_demodulation,[status(thm)],[f5342,f317]) ).
fof(f5374,plain,
multiply(inverse(sF3_fnc),b3) = inverse(c3),
inference(backward_demodulation,[status(thm)],[f5342,f315]) ).
fof(f5614,plain,
multiply(inverse(a3),sF1_fnc) = b3,
inference(paramodulation,[status(thm)],[f5315,f4909]) ).
fof(f5640,plain,
! [X0,X1] : inverse(inverse(X0)) = divide(multiply(X0,X1),X1),
inference(paramodulation,[status(thm)],[f5326,f3878]) ).
fof(f5672,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f5288,f5640]) ).
fof(f6274,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = divide(X0,divide(inverse(X2),X1)),
inference(paramodulation,[status(thm)],[f4356,f5]) ).
fof(f6365,plain,
! [X0,X1,X2] : divide(multiply(divide(X0,X1),multiply(X1,X2)),X2) = X0,
inference(backward_demodulation,[status(thm)],[f6274,f4501]) ).
fof(f7919,plain,
! [X0] : divide(multiply(divide(X0,inverse(a3)),b3),sF1_fnc) = X0,
inference(paramodulation,[status(thm)],[f5614,f6365]) ).
fof(f7990,plain,
! [X0] : divide(multiply(multiply(X0,a3),b3),sF1_fnc) = X0,
inference(forward_demodulation,[status(thm)],[f5,f7919]) ).
fof(f8507,plain,
divide(multiply(inverse(sF3_fnc),b3),sF1_fnc) = inverse(sF2_fnc),
inference(paramodulation,[status(thm)],[f5371,f7990]) ).
fof(f8516,plain,
divide(inverse(c3),sF1_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5374,f8507]) ).
fof(f8519,plain,
inverse(sF0_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f4472,f8516]) ).
fof(f8546,plain,
inverse(inverse(sF0_fnc)) = sF2_fnc,
inference(paramodulation,[status(thm)],[f8519,f5672]) ).
fof(f8549,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5672,f8546]) ).
fof(f8550,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8549,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP474-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n007.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 20:12:22 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 20.01/3.01 % Refutation found
% 20.01/3.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 20.01/3.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.59/4.29 % Elapsed time: 3.719475 seconds
% 15.59/4.29 % CPU time: 17.440404 seconds
% 15.59/4.29 % Total memory used: 477.407 MB
% 15.59/4.29 % Net memory used: 471.331 MB
%------------------------------------------------------------------------------