%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP503-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:32 PM UTC 2026
% Result : Unsatisfiable 86.91s 16.30s
% Output : CNFRefutation 86.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 6
% Syntax : Number of formulae : 148 ( 148 unt; 3 def)
% Number of atoms : 148 ( 147 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 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 : 297 ( 297 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : double_divide(double_divide(A,inverse(double_divide(B,C))),double_divide(inverse(B),inverse(double_divide(D,double_divide(A,D))))) = C,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = inverse(double_divide(B,A)),
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] : double_divide(double_divide(X0,inverse(double_divide(X1,X2))),double_divide(inverse(X1),inverse(double_divide(X3,double_divide(X0,X3))))) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f6,plain,
multiply(multiply(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,X1,X2,X3] : double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(double_divide(X3,double_divide(X0,X3))))) = X1,
inference(forward_demodulation,[status(thm)],[f5,f4]) ).
fof(f12,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))) = X1,
inference(forward_demodulation,[status(thm)],[f5,f11]) ).
fof(f14,plain,
! [X0,X1] : double_divide(double_divide(X0,sF1_fnc),double_divide(inverse(b2),multiply(double_divide(X0,X1),X1))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f8,f12]) ).
fof(f15,plain,
! [X0,X1,X2,X3,X4] : double_divide(double_divide(X0,multiply(X1,double_divide(X2,X3))),double_divide(multiply(X3,X2),multiply(double_divide(X0,X4),X4))) = X1,
inference(paramodulation,[status(thm)],[f5,f12]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(X3,X0))) = inverse(X3),
inference(paramodulation,[status(thm)],[f12,f5]) ).
fof(f19,plain,
! [X0,X1] : double_divide(double_divide(X0,sF1_fnc),double_divide(sF2_fnc,multiply(double_divide(X0,X1),X1))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f7,f14]) ).
fof(f28,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(X1,X2)),double_divide(inverse(X2),multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,X3),X3))))) = X1,
inference(paramodulation,[status(thm)],[f19,f12]) ).
fof(f29,plain,
! [X0,X1] : multiply(double_divide(sF2_fnc,multiply(double_divide(X0,X1),X1)),double_divide(X0,sF1_fnc)) = inverse(sF2_fnc),
inference(paramodulation,[status(thm)],[f19,f5]) ).
fof(f43,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(sF2_fnc)),double_divide(inverse(double_divide(X1,sF1_fnc)),multiply(double_divide(X0,X2),X2))) = double_divide(sF2_fnc,multiply(double_divide(X1,X3),X3)),
inference(paramodulation,[status(thm)],[f29,f12]) ).
fof(f44,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(sF2_fnc)),double_divide(multiply(sF1_fnc,X1),multiply(double_divide(X0,X2),X2))) = double_divide(sF2_fnc,multiply(double_divide(X1,X3),X3)),
inference(forward_demodulation,[status(thm)],[f5,f43]) ).
fof(f45,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(X4,double_divide(X1,X0)))) = inverse(X4),
inference(paramodulation,[status(thm)],[f5,f18]) ).
fof(f51,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(inverse(double_divide(X0,multiply(X1,X2))),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X1))) = inverse(double_divide(inverse(X2),multiply(double_divide(X0,X5),X5))),
inference(paramodulation,[status(thm)],[f18,f18]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(double_divide(X0,inverse(X1)),double_divide(inverse(double_divide(X2,multiply(X1,X3))),multiply(double_divide(X0,X4),X4))) = double_divide(inverse(X3),multiply(double_divide(X2,X5),X5)),
inference(paramodulation,[status(thm)],[f18,f12]) ).
fof(f56,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X0))) = inverse(double_divide(inverse(X1),multiply(double_divide(X2,X5),X5))),
inference(forward_demodulation,[status(thm)],[f5,f51]) ).
fof(f57,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,X4),X4)),double_divide(X3,inverse(X0))) = multiply(multiply(double_divide(X2,X5),X5),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f5,f56]) ).
fof(f61,plain,
! [X0,X1,X2,X3,X4,X5] : double_divide(double_divide(X0,inverse(X1)),double_divide(multiply(multiply(X1,X2),X3),multiply(double_divide(X0,X4),X4))) = double_divide(inverse(X2),multiply(double_divide(X3,X5),X5)),
inference(forward_demodulation,[status(thm)],[f5,f55]) ).
fof(f95,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,double_divide(b2,sF2_fnc))),double_divide(sF1_fnc,multiply(double_divide(X0,X2),X2))) = X1,
inference(paramodulation,[status(thm)],[f8,f15]) ).
fof(f1341,plain,
! [X0,X1] : double_divide(sF2_fnc,multiply(double_divide(X0,X1),X1)) = double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2)),
inference(equality_split,[status(thm)],[f44]) ).
fof(f1486,plain,
! [X0,X1] : multiply(multiply(double_divide(X0,X1),X1),sF2_fnc) = inverse(double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2))),
inference(paramodulation,[status(thm)],[f1341,f5]) ).
fof(f1509,plain,
! [X0,X1] : multiply(multiply(double_divide(X0,X1),X1),sF2_fnc) = multiply(multiply(double_divide(X0,b2),b2),sF2_fnc),
inference(forward_demodulation,[status(thm)],[f5,f1486]) ).
fof(f1537,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(multiply(double_divide(X1,b2),b2),sF2_fnc)),double_divide(inverse(sF2_fnc),multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,X2),X2))))) = multiply(double_divide(X1,X3),X3),
inference(paramodulation,[status(thm)],[f1509,f28]) ).
fof(f1565,plain,
! [X0,X1] : multiply(double_divide(X0,b2),b2) = multiply(double_divide(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f28,f1537]) ).
fof(f1577,plain,
! [X0,X1,X2] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,X2),X2),
inference(paramodulation,[status(thm)],[f1565,f1565]) ).
fof(f1594,plain,
! [X0,X1] : multiply(double_divide(double_divide(X0,sF1_fnc),b2),b2) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,X1),X1))),
inference(paramodulation,[status(thm)],[f19,f1565]) ).
fof(f1601,plain,
! [X0,X1,X2,X3] : multiply(double_divide(double_divide(X0,multiply(X1,X2)),b2),b2) = multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))),
inference(paramodulation,[status(thm)],[f12,f1565]) ).
fof(f1692,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(double_divide(X4,b2),b2))) = inverse(double_divide(X4,double_divide(X1,X0))),
inference(paramodulation,[status(thm)],[f1565,f45]) ).
fof(f1702,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,b2),b2))) = inverse(double_divide(X3,X0)),
inference(paramodulation,[status(thm)],[f1565,f18]) ).
fof(f1703,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(X1,b2),b2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))) = double_divide(X1,X2),
inference(paramodulation,[status(thm)],[f1565,f12]) ).
fof(f1709,plain,
! [X0] : multiply(double_divide(double_divide(X0,sF1_fnc),b2),b2) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2))),
inference(forward_demodulation,[status(thm)],[f1341,f1594]) ).
fof(f1734,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,X3),X3)),double_divide(X2,multiply(double_divide(X4,b2),b2))) = multiply(double_divide(X1,X0),X4),
inference(forward_demodulation,[status(thm)],[f5,f1692]) ).
fof(f1736,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,b2),b2))) = multiply(X0,X3),
inference(forward_demodulation,[status(thm)],[f5,f1702]) ).
fof(f1738,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,b2),b2),
inference(equality_split,[status(thm)],[f1577]) ).
fof(f2290,plain,
! [X0,X1,X2] : multiply(double_divide(double_divide(X0,multiply(X1,X2)),b2),b2) = multiply(X1,double_divide(inverse(X2),multiply(double_divide(X0,b2),b2))),
inference(forward_demodulation,[status(thm)],[f1738,f1601]) ).
fof(f2474,plain,
! [X0,X1,X2] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,b2),b2)),double_divide(X1,multiply(double_divide(X2,b2),b2))) = multiply(X0,X2),
inference(forward_demodulation,[status(thm)],[f1738,f1736]) ).
fof(f2528,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(double_divide(X1,b2),b2)),double_divide(inverse(X2),multiply(double_divide(X0,b2),b2))) = double_divide(X1,X2),
inference(forward_demodulation,[status(thm)],[f1738,f1703]) ).
fof(f3153,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,b2),b2)),double_divide(X3,inverse(X0))) = multiply(multiply(double_divide(X2,X4),X4),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1738,f57]) ).
fof(f3154,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,b2),b2)),double_divide(X3,inverse(X0))) = multiply(multiply(double_divide(X2,b2),b2),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1738,f3153]) ).
fof(f3789,plain,
! [X0,X1,X2,X3,X4] : double_divide(double_divide(X0,inverse(X1)),double_divide(multiply(multiply(X1,X2),X3),multiply(double_divide(X0,b2),b2))) = double_divide(inverse(X2),multiply(double_divide(X3,X4),X4)),
inference(forward_demodulation,[status(thm)],[f1738,f61]) ).
fof(f3790,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(X1)),double_divide(multiply(multiply(X1,X2),X3),multiply(double_divide(X0,b2),b2))) = double_divide(inverse(X2),multiply(double_divide(X3,b2),b2)),
inference(forward_demodulation,[status(thm)],[f1738,f3789]) ).
fof(f3980,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,b2),b2)),double_divide(X2,multiply(double_divide(X3,b2),b2))) = multiply(double_divide(X1,X0),X3),
inference(forward_demodulation,[status(thm)],[f1738,f1734]) ).
fof(f4003,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(double_divide(X0,b2),b2),multiply(double_divide(X1,b2),b2)),double_divide(X1,multiply(double_divide(X2,b2),b2))) = multiply(double_divide(X3,double_divide(X0,X3)),X2),
inference(paramodulation,[status(thm)],[f1738,f3980]) ).
fof(f4060,plain,
! [X0,X1,X2] : multiply(double_divide(b2,double_divide(X0,b2)),X1) = multiply(double_divide(X2,double_divide(X0,X2)),X1),
inference(forward_demodulation,[status(thm)],[f3980,f4003]) ).
fof(f4102,plain,
! [X0,X1] : multiply(double_divide(b2,double_divide(X0,b2)),double_divide(X0,X1)) = multiply(double_divide(X1,b2),b2),
inference(paramodulation,[status(thm)],[f1738,f4060]) ).
fof(f4180,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),double_divide(b2,sF2_fnc))),double_divide(sF1_fnc,multiply(double_divide(X0,X3),X3))) = double_divide(b2,double_divide(X2,b2)),
inference(paramodulation,[status(thm)],[f4060,f95]) ).
fof(f4198,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(multiply(double_divide(X0,double_divide(X1,X0)),X2),X3),multiply(double_divide(X4,b2),b2)),double_divide(X4,inverse(double_divide(b2,double_divide(X1,b2))))) = multiply(multiply(double_divide(X3,b2),b2),inverse(X2)),
inference(paramodulation,[status(thm)],[f4060,f3154]) ).
fof(f4337,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = double_divide(b2,double_divide(X1,b2)),
inference(forward_demodulation,[status(thm)],[f95,f4180]) ).
fof(f4357,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(multiply(double_divide(X0,double_divide(X1,X0)),X2),X3),multiply(double_divide(X4,b2),b2)),double_divide(X4,multiply(double_divide(X1,b2),b2))) = multiply(multiply(double_divide(X3,b2),b2),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f5,f4198]) ).
fof(f4358,plain,
! [X0,X1,X2,X3] : multiply(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),X3)),X2) = multiply(multiply(double_divide(X0,b2),b2),inverse(X3)),
inference(forward_demodulation,[status(thm)],[f3980,f4357]) ).
fof(f4465,plain,
! [X0,X1,X2] : double_divide(X0,double_divide(X1,X0)) = double_divide(X2,double_divide(X1,X2)),
inference(paramodulation,[status(thm)],[f4337,f4337]) ).
fof(f4594,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = double_divide(b2,double_divide(X1,b2)),
inference(equality_split,[status(thm)],[f4465]) ).
fof(f5385,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(double_divide(X0,b2),b2),X1),multiply(double_divide(X2,b2),b2)),double_divide(X2,inverse(double_divide(b2,double_divide(X3,b2))))) = multiply(multiply(double_divide(X1,b2),b2),inverse(double_divide(X3,X0))),
inference(paramodulation,[status(thm)],[f4102,f3154]) ).
fof(f5475,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(double_divide(X0,b2),b2),X1),multiply(double_divide(X2,b2),b2)),double_divide(X2,multiply(double_divide(X3,b2),b2))) = multiply(multiply(double_divide(X1,b2),b2),inverse(double_divide(X3,X0))),
inference(forward_demodulation,[status(thm)],[f5,f5385]) ).
fof(f5476,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X1,b2),b2)),X2) = multiply(multiply(double_divide(X0,b2),b2),inverse(double_divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f3980,f5475]) ).
fof(f5477,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X1,b2),b2)),X2) = multiply(multiply(double_divide(X0,b2),b2),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f5,f5476]) ).
fof(f6872,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(b2,double_divide(X1,b2)),X2)),X1) = multiply(multiply(double_divide(X0,b2),b2),inverse(X2)),
inference(forward_demodulation,[status(thm)],[f4594,f4358]) ).
fof(f6881,plain,
inverse(sF2_fnc) = multiply(multiply(double_divide(sF2_fnc,b2),b2),inverse(double_divide(double_divide(b2,sF1_fnc),b2))),
inference(paramodulation,[status(thm)],[f29,f6872]) ).
fof(f6967,plain,
inverse(sF2_fnc) = multiply(multiply(double_divide(sF2_fnc,b2),b2),multiply(b2,double_divide(b2,sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f5,f6881]) ).
fof(f7304,plain,
! [X0,X1] : multiply(double_divide(inverse(sF2_fnc),multiply(double_divide(X0,b2),b2)),double_divide(X0,multiply(double_divide(X1,b2),b2))) = multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(double_divide(sF2_fnc,b2),b2)),X1),
inference(paramodulation,[status(thm)],[f6967,f3980]) ).
fof(f7331,plain,
! [X0] : multiply(sF2_fnc,X0) = multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(double_divide(sF2_fnc,b2),b2)),X0),
inference(forward_demodulation,[status(thm)],[f2474,f7304]) ).
fof(f9331,plain,
! [X0,X1,X2,X3] : inverse(X0) = multiply(multiply(double_divide(multiply(X1,X2),b2),b2),multiply(X3,double_divide(X3,multiply(X0,double_divide(X2,X1))))),
inference(paramodulation,[status(thm)],[f45,f5477]) ).
fof(f9336,plain,
! [X0] : inverse(sF2_fnc) = multiply(multiply(double_divide(sF2_fnc,b2),b2),multiply(X0,double_divide(X0,sF1_fnc))),
inference(paramodulation,[status(thm)],[f29,f5477]) ).
fof(f9553,plain,
! [X0,X1] : double_divide(double_divide(X0,inverse(double_divide(sF2_fnc,b2))),double_divide(inverse(sF2_fnc),multiply(double_divide(X0,b2),b2))) = double_divide(inverse(b2),multiply(double_divide(multiply(X1,double_divide(X1,sF1_fnc)),b2),b2)),
inference(paramodulation,[status(thm)],[f9336,f3790]) ).
fof(f9580,plain,
! [X0,X1] : double_divide(double_divide(X0,multiply(b2,sF2_fnc)),double_divide(inverse(sF2_fnc),multiply(double_divide(X0,b2),b2))) = double_divide(inverse(b2),multiply(double_divide(multiply(X1,double_divide(X1,sF1_fnc)),b2),b2)),
inference(forward_demodulation,[status(thm)],[f5,f9553]) ).
fof(f9581,plain,
! [X0] : b2 = double_divide(inverse(b2),multiply(double_divide(multiply(X0,double_divide(X0,sF1_fnc)),b2),b2)),
inference(forward_demodulation,[status(thm)],[f12,f9580]) ).
fof(f9582,plain,
! [X0] : b2 = double_divide(sF2_fnc,multiply(double_divide(multiply(X0,double_divide(X0,sF1_fnc)),b2),b2)),
inference(forward_demodulation,[status(thm)],[f7,f9581]) ).
fof(f9626,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(multiply(X0,double_divide(X0,sF1_fnc)),sF1_fnc),multiply(X1,X2)),double_divide(inverse(X2),multiply(sF2_fnc,b2))) = X1,
inference(paramodulation,[status(thm)],[f9582,f28]) ).
fof(f9708,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(multiply(X0,double_divide(X0,sF1_fnc)),sF1_fnc),multiply(X1,X2)),double_divide(inverse(X2),sF1_fnc)) = X1,
inference(forward_demodulation,[status(thm)],[f8,f9626]) ).
fof(f12157,plain,
! [X0] : multiply(sF2_fnc,X0) = multiply(multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),b2),b2),multiply(sF2_fnc,X0)),
inference(forward_demodulation,[status(thm)],[f5477,f7331]) ).
fof(f12468,plain,
! [X0] : inverse(X0) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(X0,double_divide(double_divide(b2,sF1_fnc),b2)))),
inference(paramodulation,[status(thm)],[f12157,f9331]) ).
fof(f12789,plain,
! [X0] : inverse(double_divide(X0,double_divide(double_divide(b2,sF1_fnc),b2))) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2))),
inference(paramodulation,[status(thm)],[f1341,f12468]) ).
fof(f12802,plain,
! [X0] : multiply(sF2_fnc,double_divide(sF2_fnc,multiply(X0,double_divide(double_divide(b2,sF1_fnc),b2)))) = multiply(multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),b2),b2),inverse(X0)),
inference(paramodulation,[status(thm)],[f12468,f12157]) ).
fof(f12818,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,inverse(X1)),double_divide(multiply(multiply(X1,double_divide(double_divide(b2,sF1_fnc),b2)),sF2_fnc),multiply(double_divide(X0,X2),X2))) = sF2_fnc,
inference(paramodulation,[status(thm)],[f12468,f15]) ).
fof(f12852,plain,
! [X0] : multiply(double_divide(double_divide(b2,sF1_fnc),b2),X0) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2))),
inference(forward_demodulation,[status(thm)],[f5,f12789]) ).
fof(f12853,plain,
! [X0] : multiply(double_divide(double_divide(b2,sF1_fnc),b2),X0) = multiply(double_divide(double_divide(X0,sF1_fnc),b2),b2),
inference(forward_demodulation,[status(thm)],[f1709,f12852]) ).
fof(f12872,plain,
! [X0] : inverse(X0) = multiply(multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),b2),b2),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f12468,f12802]) ).
fof(f12878,plain,
! [X0,X1] : double_divide(double_divide(X0,inverse(X1)),double_divide(multiply(multiply(X1,double_divide(double_divide(b2,sF1_fnc),b2)),sF2_fnc),multiply(double_divide(X0,b2),b2))) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f1738,f12818]) ).
fof(f12879,plain,
double_divide(inverse(double_divide(double_divide(b2,sF1_fnc),b2)),multiply(double_divide(sF2_fnc,b2),b2)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f3790,f12878]) ).
fof(f12880,plain,
double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(double_divide(sF2_fnc,b2),b2)) = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f5,f12879]) ).
fof(f12946,plain,
! [X0] : double_divide(double_divide(sF2_fnc,multiply(X0,double_divide(double_divide(b2,sF1_fnc),b2))),sF2_fnc) = X0,
inference(paramodulation,[status(thm)],[f12880,f15]) ).
fof(f13331,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(double_divide(X1,sF1_fnc),b2),b2)),double_divide(inverse(X1),multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,X2),X2))))) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(paramodulation,[status(thm)],[f12853,f28]) ).
fof(f13450,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(double_divide(X1,sF1_fnc),b2),b2)),double_divide(inverse(X1),multiply(sF2_fnc,double_divide(sF2_fnc,multiply(double_divide(X0,b2),b2))))) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(forward_demodulation,[status(thm)],[f1341,f13331]) ).
fof(f13451,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(double_divide(X1,sF1_fnc),b2),b2)),double_divide(inverse(X1),multiply(double_divide(double_divide(X0,sF1_fnc),b2),b2))) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(forward_demodulation,[status(thm)],[f1709,f13450]) ).
fof(f13452,plain,
! [X0] : double_divide(double_divide(X0,sF1_fnc),X0) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(forward_demodulation,[status(thm)],[f2528,f13451]) ).
fof(f13524,plain,
double_divide(double_divide(double_divide(b2,sF1_fnc),b2),double_divide(sF1_fnc,sF1_fnc)) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(paramodulation,[status(thm)],[f13452,f13452]) ).
fof(f13525,plain,
! [X0,X1] : double_divide(double_divide(X0,sF1_fnc),X0) = double_divide(double_divide(X1,sF1_fnc),X1),
inference(paramodulation,[status(thm)],[f13452,f13452]) ).
fof(f13526,plain,
! [X0] : double_divide(double_divide(double_divide(b2,sF1_fnc),b2),double_divide(inverse(double_divide(X0,sF1_fnc)),sF1_fnc)) = X0,
inference(paramodulation,[status(thm)],[f13452,f9708]) ).
fof(f13660,plain,
! [X0] : multiply(X0,double_divide(X0,sF1_fnc)) = inverse(double_divide(double_divide(b2,sF1_fnc),b2)),
inference(paramodulation,[status(thm)],[f13452,f5]) ).
fof(f13740,plain,
! [X0] : double_divide(double_divide(double_divide(b2,sF1_fnc),b2),double_divide(multiply(sF1_fnc,X0),sF1_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f5,f13526]) ).
fof(f13811,plain,
! [X0] : multiply(X0,double_divide(X0,sF1_fnc)) = multiply(b2,double_divide(b2,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f13660]) ).
fof(f13820,plain,
! [X0] : double_divide(double_divide(X0,sF1_fnc),X0) = double_divide(double_divide(b2,sF1_fnc),b2),
inference(equality_split,[status(thm)],[f13525]) ).
fof(f14276,plain,
! [X0,X1] : multiply(X0,double_divide(X0,sF1_fnc)) = multiply(X1,double_divide(X1,sF1_fnc)),
inference(paramodulation,[status(thm)],[f13811,f13811]) ).
fof(f14515,plain,
! [X0] : multiply(X0,double_divide(X0,sF1_fnc)) = multiply(b2,double_divide(b2,sF1_fnc)),
inference(equality_split,[status(thm)],[f14276]) ).
fof(f14864,plain,
double_divide(double_divide(double_divide(b2,sF1_fnc),b2),double_divide(sF0_fnc,sF1_fnc)) = a2,
inference(paramodulation,[status(thm)],[f9,f13740]) ).
fof(f14921,plain,
! [X0] : multiply(double_divide(multiply(sF1_fnc,X0),sF1_fnc),double_divide(double_divide(b2,sF1_fnc),b2)) = inverse(X0),
inference(paramodulation,[status(thm)],[f13740,f5]) ).
fof(f15260,plain,
! [X0] : double_divide(double_divide(sF2_fnc,inverse(X0)),sF2_fnc) = double_divide(multiply(sF1_fnc,X0),sF1_fnc),
inference(paramodulation,[status(thm)],[f14921,f12946]) ).
fof(f15261,plain,
! [X0] : inverse(double_divide(multiply(sF1_fnc,X0),sF1_fnc)) = multiply(sF2_fnc,double_divide(sF2_fnc,inverse(X0))),
inference(paramodulation,[status(thm)],[f14921,f12468]) ).
fof(f15309,plain,
! [X0] : multiply(sF1_fnc,multiply(sF1_fnc,X0)) = multiply(sF2_fnc,double_divide(sF2_fnc,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f5,f15261]) ).
fof(f15373,plain,
! [X0,X1] : double_divide(double_divide(sF2_fnc,multiply(X0,X1)),sF2_fnc) = double_divide(multiply(sF1_fnc,double_divide(X1,X0)),sF1_fnc),
inference(paramodulation,[status(thm)],[f5,f15260]) ).
fof(f15435,plain,
! [X0,X1] : multiply(sF1_fnc,multiply(sF1_fnc,double_divide(X0,X1))) = multiply(sF2_fnc,double_divide(sF2_fnc,multiply(X1,X0))),
inference(paramodulation,[status(thm)],[f5,f15309]) ).
fof(f16528,plain,
! [X0] : inverse(X0) = multiply(sF1_fnc,multiply(sF1_fnc,double_divide(double_divide(double_divide(b2,sF1_fnc),b2),X0))),
inference(backward_demodulation,[status(thm)],[f15435,f12468]) ).
fof(f18028,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(X1,double_divide(inverse(X2),multiply(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),b2),b2)))),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))) = X1,
inference(paramodulation,[status(thm)],[f12872,f15]) ).
fof(f18079,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(X1,X2)),b2),b2)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))) = X1,
inference(forward_demodulation,[status(thm)],[f2290,f18028]) ).
fof(f18080,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(double_divide(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(X1,X2)),b2),b2)),double_divide(inverse(X2),multiply(double_divide(X0,b2),b2))) = X1,
inference(forward_demodulation,[status(thm)],[f1738,f18079]) ).
fof(f18081,plain,
! [X0,X1] : double_divide(double_divide(multiply(b2,double_divide(b2,sF1_fnc)),multiply(X0,X1)),X1) = X0,
inference(forward_demodulation,[status(thm)],[f2528,f18080]) ).
fof(f20497,plain,
inverse(double_divide(sF1_fnc,sF1_fnc)) = multiply(sF1_fnc,multiply(sF1_fnc,double_divide(double_divide(b2,sF1_fnc),b2))),
inference(paramodulation,[status(thm)],[f13524,f16528]) ).
fof(f20548,plain,
multiply(sF1_fnc,sF1_fnc) = multiply(sF1_fnc,multiply(sF1_fnc,double_divide(double_divide(b2,sF1_fnc),b2))),
inference(forward_demodulation,[status(thm)],[f5,f20497]) ).
fof(f20557,plain,
double_divide(double_divide(double_divide(b2,sF1_fnc),b2),double_divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc)) = multiply(sF1_fnc,double_divide(double_divide(b2,sF1_fnc),b2)),
inference(paramodulation,[status(thm)],[f20548,f13740]) ).
fof(f20599,plain,
sF1_fnc = multiply(sF1_fnc,double_divide(double_divide(b2,sF1_fnc),b2)),
inference(forward_demodulation,[status(thm)],[f13740,f20557]) ).
fof(f20646,plain,
double_divide(double_divide(sF2_fnc,sF1_fnc),sF2_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f20599,f12946]) ).
fof(f20667,plain,
multiply(sF1_fnc,multiply(sF1_fnc,double_divide(double_divide(double_divide(b2,sF1_fnc),b2),sF1_fnc))) = multiply(sF2_fnc,double_divide(sF2_fnc,sF1_fnc)),
inference(paramodulation,[status(thm)],[f20599,f15435]) ).
fof(f20701,plain,
double_divide(double_divide(b2,sF1_fnc),b2) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f13820,f20646]) ).
fof(f20711,plain,
inverse(sF1_fnc) = multiply(sF2_fnc,double_divide(sF2_fnc,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f16528,f20667]) ).
fof(f20712,plain,
inverse(sF1_fnc) = multiply(b2,double_divide(b2,sF1_fnc)),
inference(forward_demodulation,[status(thm)],[f14515,f20711]) ).
fof(f20750,plain,
sF1_fnc = multiply(sF1_fnc,sF1_fnc),
inference(backward_demodulation,[status(thm)],[f20701,f20599]) ).
fof(f20758,plain,
double_divide(sF1_fnc,double_divide(sF0_fnc,sF1_fnc)) = a2,
inference(backward_demodulation,[status(thm)],[f20701,f14864]) ).
fof(f20762,plain,
! [X0] : double_divide(double_divide(X0,sF1_fnc),X0) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f20701,f13820]) ).
fof(f20765,plain,
! [X0] : double_divide(double_divide(sF2_fnc,multiply(X0,sF1_fnc)),sF2_fnc) = X0,
inference(backward_demodulation,[status(thm)],[f20701,f12946]) ).
fof(f20847,plain,
double_divide(b2,double_divide(sF0_fnc,b2)) = a2,
inference(forward_demodulation,[status(thm)],[f4594,f20758]) ).
fof(f21565,plain,
! [X0,X1] : double_divide(double_divide(inverse(sF1_fnc),multiply(X0,X1)),X1) = X0,
inference(backward_demodulation,[status(thm)],[f20712,f18081]) ).
fof(f21569,plain,
! [X0] : multiply(X0,double_divide(X0,sF1_fnc)) = inverse(sF1_fnc),
inference(backward_demodulation,[status(thm)],[f20712,f14515]) ).
fof(f21740,plain,
double_divide(double_divide(sF2_fnc,multiply(sF1_fnc,sF1_fnc)),sF2_fnc) = double_divide(inverse(sF1_fnc),sF1_fnc),
inference(paramodulation,[status(thm)],[f21569,f15373]) ).
fof(f21803,plain,
double_divide(double_divide(sF2_fnc,sF1_fnc),sF2_fnc) = double_divide(inverse(sF1_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f20750,f21740]) ).
fof(f21804,plain,
sF1_fnc = double_divide(inverse(sF1_fnc),sF1_fnc),
inference(forward_demodulation,[status(thm)],[f20762,f21803]) ).
fof(f21873,plain,
multiply(inverse(sF1_fnc),sF1_fnc) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f21804,f21569]) ).
fof(f22619,plain,
double_divide(double_divide(sF2_fnc,inverse(sF1_fnc)),sF2_fnc) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f21873,f20765]) ).
fof(f22680,plain,
double_divide(multiply(sF1_fnc,sF1_fnc),sF1_fnc) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f15260,f22619]) ).
fof(f22681,plain,
double_divide(sF1_fnc,sF1_fnc) = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f20750,f22680]) ).
fof(f23488,plain,
double_divide(double_divide(inverse(sF1_fnc),sF1_fnc),sF1_fnc) = sF1_fnc,
inference(paramodulation,[status(thm)],[f20750,f21565]) ).
fof(f23665,plain,
double_divide(sF1_fnc,sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f21804,f23488]) ).
fof(f23666,plain,
inverse(sF1_fnc) = sF1_fnc,
inference(forward_demodulation,[status(thm)],[f22681,f23665]) ).
fof(f23735,plain,
! [X0,X1] : double_divide(double_divide(sF1_fnc,multiply(X0,X1)),X1) = X0,
inference(backward_demodulation,[status(thm)],[f23666,f21565]) ).
fof(f23740,plain,
double_divide(sF1_fnc,sF1_fnc) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f23666,f22681]) ).
fof(f23746,plain,
! [X0] : multiply(X0,double_divide(X0,sF1_fnc)) = sF1_fnc,
inference(backward_demodulation,[status(thm)],[f23666,f21569]) ).
fof(f24667,plain,
! [X0] : double_divide(double_divide(sF1_fnc,sF1_fnc),double_divide(X0,sF1_fnc)) = X0,
inference(paramodulation,[status(thm)],[f23746,f23735]) ).
fof(f24826,plain,
! [X0] : double_divide(sF1_fnc,double_divide(X0,sF1_fnc)) = X0,
inference(forward_demodulation,[status(thm)],[f23740,f24667]) ).
fof(f24827,plain,
! [X0] : double_divide(b2,double_divide(X0,b2)) = X0,
inference(forward_demodulation,[status(thm)],[f4594,f24826]) ).
fof(f24899,plain,
sF0_fnc = a2,
inference(backward_demodulation,[status(thm)],[f24827,f20847]) ).
fof(f24959,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f24899,f10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP503-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/5.32 % Computer : n012.cluster.edu
% 0.04/5.32 % Model : x86_64 x86_64
% 0.04/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.32 % Memory : 8046.5625MB
% 0.04/5.32 % OS : Linux 6.8.0-71-generic
% 0.04/5.32 % CPULimit : 300
% 0.04/5.33 % WCLimit : 300
% 0.04/5.33 % DateTime : Sun Sep 20 20:15:02 UTC 2026
% 0.04/5.33 % CPUTime :
% 0.04/5.33 % Drodi V4.1.1
% 86.91/16.30 % Refutation found
% 86.91/16.30 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 86.91/16.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 27.46/16.40 % Elapsed time: 11.059299 seconds
% 27.46/16.40 % CPU time: 87.725786 seconds
% 27.46/16.40 % Total memory used: 926.053 MB
% 27.46/16.40 % Net memory used: 905.768 MB
%------------------------------------------------------------------------------