%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP504-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:33 PM UTC 2026
% Result : Unsatisfiable 112.58s 14.84s
% Output : CNFRefutation 112.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 7
% Syntax : Number of formulae : 163 ( 163 unt; 4 def)
% Number of atoms : 163 ( 162 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 : 11 ( 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 : 331 ( 331 !; 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : multiply(A,B) = inverse(double_divide(B,A)),
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] : 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(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] : 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(f13,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,f12]) ).
fof(f16,plain,
! [X0,X1] : double_divide(double_divide(X0,sF2_fnc),double_divide(inverse(sF3_fnc),multiply(double_divide(X0,X1),X1))) = a3,
inference(paramodulation,[status(thm)],[f10,f13]) ).
fof(f17,plain,
! [X0,X1] : double_divide(double_divide(X0,sF1_fnc),double_divide(inverse(b3),multiply(double_divide(X0,X1),X1))) = a3,
inference(paramodulation,[status(thm)],[f7,f13]) ).
fof(f18,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,f13]) ).
fof(f20,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)],[f13,f5]) ).
fof(f38,plain,
! [X0,X1] : multiply(double_divide(inverse(sF3_fnc),multiply(double_divide(X0,X1),X1)),double_divide(X0,sF2_fnc)) = inverse(a3),
inference(paramodulation,[status(thm)],[f16,f5]) ).
fof(f47,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(X1,X2)),double_divide(inverse(X2),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,X3),X3))))) = X1,
inference(paramodulation,[status(thm)],[f17,f13]) ).
fof(f76,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,double_divide(b3,a3))),double_divide(sF1_fnc,multiply(double_divide(X0,X2),X2))) = X1,
inference(paramodulation,[status(thm)],[f7,f18]) ).
fof(f90,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)],[f18,f5]) ).
fof(f101,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,inverse(a3)),double_divide(multiply(sF2_fnc,X1),multiply(double_divide(X0,X2),X2))) = double_divide(inverse(sF3_fnc),multiply(double_divide(X1,X3),X3)),
inference(paramodulation,[status(thm)],[f38,f18]) ).
fof(f128,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)],[f20,f20]) ).
fof(f144,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,f128]) ).
fof(f145,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,f144]) ).
fof(f2835,plain,
! [X0,X1] : double_divide(inverse(sF3_fnc),multiply(double_divide(X0,X1),X1)) = double_divide(inverse(sF3_fnc),multiply(double_divide(X0,a3),a3)),
inference(equality_split,[status(thm)],[f101]) ).
fof(f3059,plain,
! [X0,X1] : multiply(multiply(double_divide(X0,X1),X1),inverse(sF3_fnc)) = inverse(double_divide(inverse(sF3_fnc),multiply(double_divide(X0,a3),a3))),
inference(paramodulation,[status(thm)],[f2835,f5]) ).
fof(f3079,plain,
! [X0,X1] : multiply(multiply(double_divide(X0,X1),X1),inverse(sF3_fnc)) = multiply(multiply(double_divide(X0,a3),a3),inverse(sF3_fnc)),
inference(forward_demodulation,[status(thm)],[f5,f3059]) ).
fof(f3124,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(multiply(double_divide(X1,a3),a3),inverse(sF3_fnc))),double_divide(inverse(inverse(sF3_fnc)),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,X2),X2))))) = multiply(double_divide(X1,X3),X3),
inference(paramodulation,[status(thm)],[f3079,f47]) ).
fof(f3157,plain,
! [X0,X1] : multiply(double_divide(X0,a3),a3) = multiply(double_divide(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f47,f3124]) ).
fof(f3174,plain,
! [X0,X1,X2] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,X2),X2),
inference(paramodulation,[status(thm)],[f3157,f3157]) ).
fof(f3350,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,a3),a3))) = inverse(double_divide(X4,double_divide(X1,X0))),
inference(paramodulation,[status(thm)],[f3157,f90]) ).
fof(f3363,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,a3),a3))) = inverse(double_divide(X3,X0)),
inference(paramodulation,[status(thm)],[f3157,f20]) ).
fof(f3365,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(X1,a3),a3)),double_divide(inverse(X2),multiply(double_divide(X0,X3),X3))) = double_divide(X1,X2),
inference(paramodulation,[status(thm)],[f3157,f13]) ).
fof(f3385,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,a3),a3))) = multiply(double_divide(X1,X0),X4),
inference(forward_demodulation,[status(thm)],[f5,f3350]) ).
fof(f3387,plain,
! [X0,X1,X2,X3] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,X2),X2)),double_divide(X1,multiply(double_divide(X3,a3),a3))) = multiply(X0,X3),
inference(forward_demodulation,[status(thm)],[f5,f3363]) ).
fof(f4121,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,a3),a3),
inference(equality_split,[status(thm)],[f3174]) ).
fof(f4122,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = multiply(double_divide(X0,a3),a3),
inference(equality_split,[status(thm)],[f3174]) ).
fof(f4164,plain,
! [X0,X1,X2,X3] : multiply(X0,double_divide(inverse(X1),multiply(double_divide(X2,X3),X3))) = multiply(double_divide(double_divide(X2,multiply(X0,X1)),a3),a3),
inference(paramodulation,[status(thm)],[f13,f4121]) ).
fof(f4418,plain,
! [X0,X1,X2] : multiply(X0,double_divide(inverse(X1),multiply(double_divide(X2,a3),a3))) = multiply(double_divide(double_divide(X2,multiply(X0,X1)),a3),a3),
inference(forward_demodulation,[status(thm)],[f4122,f4164]) ).
fof(f5160,plain,
! [X0,X1,X2] : multiply(double_divide(inverse(X0),multiply(double_divide(X1,a3),a3)),double_divide(X1,multiply(double_divide(X2,a3),a3))) = multiply(X0,X2),
inference(forward_demodulation,[status(thm)],[f4122,f3387]) ).
fof(f5226,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(double_divide(X1,a3),a3)),double_divide(inverse(X2),multiply(double_divide(X0,a3),a3))) = double_divide(X1,X2),
inference(forward_demodulation,[status(thm)],[f4122,f3365]) ).
fof(f7757,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(X0,X1),multiply(double_divide(X2,a3),a3)),double_divide(X2,multiply(double_divide(X3,a3),a3))) = multiply(double_divide(X1,X0),X3),
inference(forward_demodulation,[status(thm)],[f4122,f3385]) ).
fof(f7783,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(double_divide(X0,a3),a3),multiply(double_divide(X1,a3),a3)),double_divide(X1,multiply(double_divide(X2,a3),a3))) = multiply(double_divide(X3,double_divide(X0,X3)),X2),
inference(paramodulation,[status(thm)],[f4122,f7757]) ).
fof(f7849,plain,
! [X0,X1,X2] : multiply(double_divide(a3,double_divide(X0,a3)),X1) = multiply(double_divide(X2,double_divide(X0,X2)),X1),
inference(forward_demodulation,[status(thm)],[f7757,f7783]) ).
fof(f7896,plain,
! [X0,X1] : multiply(double_divide(a3,double_divide(X0,a3)),double_divide(X0,X1)) = multiply(double_divide(X1,a3),a3),
inference(paramodulation,[status(thm)],[f4122,f7849]) ).
fof(f8015,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(double_divide(X1,double_divide(X2,X1)),double_divide(b3,a3))),double_divide(sF1_fnc,multiply(double_divide(X0,X3),X3))) = double_divide(a3,double_divide(X2,a3)),
inference(paramodulation,[status(thm)],[f7849,f76]) ).
fof(f8250,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = double_divide(a3,double_divide(X1,a3)),
inference(forward_demodulation,[status(thm)],[f76,f8015]) ).
fof(f8394,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),double_divide(a3,double_divide(X0,a3))) = double_divide(a3,double_divide(X1,a3)),
inference(paramodulation,[status(thm)],[f8250,f8250]) ).
fof(f8395,plain,
! [X0,X1,X2] : double_divide(X0,double_divide(X1,X0)) = double_divide(X2,double_divide(X1,X2)),
inference(paramodulation,[status(thm)],[f8250,f8250]) ).
fof(f10045,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = double_divide(a3,double_divide(X1,a3)),
inference(equality_split,[status(thm)],[f8395]) ).
fof(f11596,plain,
! [X0,X1,X2,X3,X4] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,a3),a3)),double_divide(X3,inverse(X0))) = multiply(multiply(double_divide(X2,X4),X4),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f4122,f145]) ).
fof(f11597,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(X0,X1),X2),multiply(double_divide(X3,a3),a3)),double_divide(X3,inverse(X0))) = multiply(multiply(double_divide(X2,a3),a3),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f4122,f11596]) ).
fof(f11609,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(double_divide(X0,a3),a3),X1),multiply(double_divide(X2,a3),a3)),double_divide(X2,inverse(double_divide(a3,double_divide(X3,a3))))) = multiply(multiply(double_divide(X1,a3),a3),inverse(double_divide(X3,X0))),
inference(paramodulation,[status(thm)],[f7896,f11597]) ).
fof(f11690,plain,
! [X0,X1,X2,X3] : multiply(double_divide(multiply(multiply(double_divide(X0,a3),a3),X1),multiply(double_divide(X2,a3),a3)),double_divide(X2,multiply(double_divide(X3,a3),a3))) = multiply(multiply(double_divide(X1,a3),a3),inverse(double_divide(X3,X0))),
inference(forward_demodulation,[status(thm)],[f5,f11609]) ).
fof(f11691,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X1,a3),a3)),X2) = multiply(multiply(double_divide(X0,a3),a3),inverse(double_divide(X2,X1))),
inference(forward_demodulation,[status(thm)],[f7757,f11690]) ).
fof(f11692,plain,
! [X0,X1,X2] : multiply(double_divide(X0,multiply(double_divide(X1,a3),a3)),X2) = multiply(multiply(double_divide(X0,a3),a3),multiply(X1,X2)),
inference(forward_demodulation,[status(thm)],[f5,f11691]) ).
fof(f12365,plain,
! [X0,X1,X2] : multiply(multiply(double_divide(inverse(X0),a3),a3),multiply(X1,double_divide(X1,multiply(double_divide(X2,a3),a3)))) = multiply(X0,X2),
inference(backward_demodulation,[status(thm)],[f11692,f5160]) ).
fof(f12377,plain,
! [X0,X1,X2] : inverse(X0) = multiply(multiply(double_divide(inverse(X1),a3),a3),multiply(X2,double_divide(X2,multiply(X0,X1)))),
inference(paramodulation,[status(thm)],[f20,f11692]) ).
fof(f12378,plain,
! [X0,X1] : multiply(double_divide(X0,a3),a3) = multiply(multiply(double_divide(X0,a3),a3),multiply(X1,multiply(double_divide(X1,a3),a3))),
inference(paramodulation,[status(thm)],[f4122,f11692]) ).
fof(f16629,plain,
! [X0,X1,X2] : inverse(multiply(double_divide(X0,a3),a3)) = multiply(multiply(double_divide(inverse(multiply(X1,multiply(double_divide(X1,a3),a3))),a3),a3),multiply(X2,double_divide(X2,multiply(double_divide(X0,a3),a3)))),
inference(paramodulation,[status(thm)],[f12378,f12377]) ).
fof(f16642,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(X1,a3),a3)),double_divide(inverse(multiply(X2,multiply(double_divide(X2,a3),a3))),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,X3),X3))))) = multiply(double_divide(X1,a3),a3),
inference(paramodulation,[status(thm)],[f12378,f47]) ).
fof(f16661,plain,
! [X0,X1] : inverse(multiply(double_divide(X0,a3),a3)) = multiply(multiply(X1,multiply(double_divide(X1,a3),a3)),X0),
inference(forward_demodulation,[status(thm)],[f12365,f16629]) ).
fof(f16665,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(X1,a3),a3)),double_divide(inverse(multiply(X2,multiply(double_divide(X2,a3),a3))),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,a3),a3))))) = multiply(double_divide(X1,a3),a3),
inference(forward_demodulation,[status(thm)],[f4122,f16642]) ).
fof(f16666,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(X1,a3),a3)),double_divide(inverse(multiply(X2,multiply(double_divide(X2,a3),a3))),multiply(double_divide(double_divide(X0,multiply(a3,b3)),a3),a3))) = multiply(double_divide(X1,a3),a3),
inference(forward_demodulation,[status(thm)],[f4418,f16665]) ).
fof(f16667,plain,
! [X0,X1,X2] : double_divide(double_divide(double_divide(X0,sF1_fnc),multiply(double_divide(X1,a3),a3)),double_divide(inverse(multiply(X2,multiply(double_divide(X2,a3),a3))),multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3))) = multiply(double_divide(X1,a3),a3),
inference(forward_demodulation,[status(thm)],[f7,f16666]) ).
fof(f16668,plain,
! [X0,X1] : double_divide(X0,multiply(X1,multiply(double_divide(X1,a3),a3))) = multiply(double_divide(X0,a3),a3),
inference(forward_demodulation,[status(thm)],[f5226,f16667]) ).
fof(f16714,plain,
! [X0,X1,X2] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(multiply(double_divide(X1,a3),a3)),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,X2),X2))))) = X1,
inference(paramodulation,[status(thm)],[f16668,f47]) ).
fof(f16724,plain,
! [X0,X1] : inverse(X0) = multiply(multiply(double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3),a3),multiply(X1,multiply(double_divide(X1,a3),a3))),
inference(paramodulation,[status(thm)],[f16668,f12377]) ).
fof(f16814,plain,
! [X0,X1] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(multiply(double_divide(X1,a3),a3)),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,a3),a3))))) = X1,
inference(forward_demodulation,[status(thm)],[f4122,f16714]) ).
fof(f16815,plain,
! [X0,X1] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(multiply(double_divide(X1,a3),a3)),multiply(double_divide(double_divide(X0,multiply(a3,b3)),a3),a3))) = X1,
inference(forward_demodulation,[status(thm)],[f4418,f16814]) ).
fof(f16816,plain,
! [X0,X1] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(multiply(double_divide(X1,a3),a3)),multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3))) = X1,
inference(forward_demodulation,[status(thm)],[f7,f16815]) ).
fof(f16817,plain,
! [X0] : double_divide(a3,double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f10045,f16816]) ).
fof(f16833,plain,
! [X0] : inverse(X0) = multiply(double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3),a3),
inference(forward_demodulation,[status(thm)],[f12378,f16724]) ).
fof(f16917,plain,
! [X0,X1] : multiply(X0,double_divide(inverse(multiply(double_divide(X0,a3),a3)),X1)) = multiply(double_divide(X1,a3),a3),
inference(paramodulation,[status(thm)],[f16817,f7896]) ).
fof(f17010,plain,
! [X0] : double_divide(a3,double_divide(inverse(inverse(X0)),a3)) = inverse(multiply(double_divide(X0,a3),a3)),
inference(paramodulation,[status(thm)],[f16833,f16817]) ).
fof(f17013,plain,
! [X0,X1] : multiply(double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3),a3) = multiply(inverse(X0),multiply(X1,multiply(double_divide(X1,a3),a3))),
inference(paramodulation,[status(thm)],[f16833,f12378]) ).
fof(f17122,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X0),multiply(X1,multiply(double_divide(X1,a3),a3))),
inference(forward_demodulation,[status(thm)],[f16833,f17013]) ).
fof(f17189,plain,
! [X0,X1,X2] : inverse(double_divide(X0,X1)) = multiply(multiply(X1,X0),multiply(X2,multiply(double_divide(X2,a3),a3))),
inference(paramodulation,[status(thm)],[f5,f17122]) ).
fof(f17194,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X0),multiply(inverse(multiply(double_divide(X1,a3),a3)),inverse(X1))),
inference(paramodulation,[status(thm)],[f16833,f17122]) ).
fof(f17231,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(X2,multiply(double_divide(X2,a3),a3))),
inference(forward_demodulation,[status(thm)],[f5,f17189]) ).
fof(f17336,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(inverse(multiply(double_divide(X2,a3),a3)),inverse(X2))),
inference(paramodulation,[status(thm)],[f16833,f17231]) ).
fof(f18502,plain,
! [X0,X1] : multiply(X0,multiply(double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3),a3)) = multiply(double_divide(multiply(X1,multiply(double_divide(X1,a3),a3)),a3),a3),
inference(paramodulation,[status(thm)],[f16668,f16917]) ).
fof(f18569,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(double_divide(multiply(X1,multiply(double_divide(X1,a3),a3)),a3),a3),
inference(forward_demodulation,[status(thm)],[f16833,f18502]) ).
fof(f22993,plain,
! [X0] : multiply(double_divide(multiply(X0,multiply(double_divide(X0,a3),a3)),a3),a3) = multiply(a3,inverse(a3)),
inference(equality_split,[status(thm)],[f18569]) ).
fof(f22994,plain,
! [X0] : multiply(X0,inverse(X0)) = multiply(a3,inverse(a3)),
inference(equality_split,[status(thm)],[f18569]) ).
fof(f22995,plain,
! [X0] : multiply(double_divide(inverse(multiply(double_divide(multiply(double_divide(multiply(X0,multiply(double_divide(X0,a3),a3)),a3),a3),a3),a3)),a3),a3) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f16661,f22993]) ).
fof(f23025,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X0),multiply(multiply(X1,multiply(double_divide(X1,a3),a3)),multiply(a3,inverse(a3)))),
inference(paramodulation,[status(thm)],[f22993,f17122]) ).
fof(f23150,plain,
! [X0,X1] : multiply(double_divide(X0,X1),multiply(X1,X0)) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f5,f22994]) ).
fof(f23201,plain,
! [X0] : inverse(multiply(double_divide(multiply(X0,multiply(double_divide(X0,a3),a3)),a3),a3)) = multiply(a3,inverse(a3)),
inference(forward_demodulation,[status(thm)],[f16833,f22995]) ).
fof(f23202,plain,
inverse(multiply(a3,inverse(a3))) = multiply(a3,inverse(a3)),
inference(forward_demodulation,[status(thm)],[f22993,f23201]) ).
fof(f23215,plain,
! [X0] : inverse(X0) = multiply(inverse(X0),inverse(multiply(double_divide(multiply(a3,inverse(a3)),a3),a3))),
inference(forward_demodulation,[status(thm)],[f16661,f23025]) ).
fof(f23315,plain,
multiply(multiply(a3,inverse(a3)),multiply(a3,inverse(a3))) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f23202,f22994]) ).
fof(f24031,plain,
multiply(double_divide(multiply(a3,inverse(a3)),multiply(a3,inverse(a3))),multiply(a3,inverse(a3))) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f23315,f23150]) ).
fof(f24092,plain,
! [X0] : multiply(double_divide(inverse(X0),X0),multiply(a3,inverse(a3))) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f22994,f23150]) ).
fof(f24316,plain,
multiply(double_divide(multiply(a3,inverse(a3)),a3),a3) = multiply(a3,inverse(a3)),
inference(forward_demodulation,[status(thm)],[f4122,f24031]) ).
fof(f24799,plain,
! [X0] : multiply(multiply(double_divide(inverse(multiply(double_divide(X0,a3),a3)),a3),a3),multiply(X0,multiply(a3,inverse(a3)))) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f11692,f24092]) ).
fof(f24911,plain,
! [X0] : multiply(inverse(X0),multiply(X0,multiply(a3,inverse(a3)))) = multiply(a3,inverse(a3)),
inference(forward_demodulation,[status(thm)],[f16833,f24799]) ).
fof(f25048,plain,
! [X0] : multiply(inverse(multiply(X0,multiply(double_divide(X0,a3),a3))),inverse(multiply(double_divide(multiply(a3,inverse(a3)),a3),a3))) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f16661,f24911]) ).
fof(f25103,plain,
! [X0] : inverse(multiply(X0,multiply(double_divide(X0,a3),a3))) = multiply(a3,inverse(a3)),
inference(forward_demodulation,[status(thm)],[f23215,f25048]) ).
fof(f25179,plain,
! [X0,X1,X2] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(inverse(multiply(double_divide(multiply(X2,multiply(double_divide(X2,a3),a3)),a3),a3)),multiply(a3,inverse(a3)))),
inference(paramodulation,[status(thm)],[f25103,f17336]) ).
fof(f25181,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X0),multiply(inverse(multiply(double_divide(multiply(X1,multiply(double_divide(X1,a3),a3)),a3),a3)),multiply(a3,inverse(a3)))),
inference(paramodulation,[status(thm)],[f25103,f17194]) ).
fof(f25247,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(inverse(multiply(a3,inverse(a3))),multiply(a3,inverse(a3)))),
inference(forward_demodulation,[status(thm)],[f22993,f25179]) ).
fof(f25248,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(multiply(a3,inverse(a3)),multiply(a3,inverse(a3)))),
inference(forward_demodulation,[status(thm)],[f23202,f25247]) ).
fof(f25249,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),multiply(a3,inverse(a3))),
inference(forward_demodulation,[status(thm)],[f23315,f25248]) ).
fof(f25251,plain,
! [X0] : inverse(X0) = multiply(inverse(X0),multiply(inverse(multiply(a3,inverse(a3))),multiply(a3,inverse(a3)))),
inference(forward_demodulation,[status(thm)],[f22993,f25181]) ).
fof(f25252,plain,
! [X0] : inverse(X0) = multiply(inverse(X0),multiply(multiply(a3,inverse(a3)),multiply(a3,inverse(a3)))),
inference(forward_demodulation,[status(thm)],[f23202,f25251]) ).
fof(f25253,plain,
! [X0] : inverse(X0) = multiply(inverse(X0),multiply(a3,inverse(a3))),
inference(forward_demodulation,[status(thm)],[f23315,f25252]) ).
fof(f27371,plain,
! [X0] : double_divide(X0,multiply(multiply(a3,inverse(a3)),multiply(a3,inverse(a3)))) = multiply(double_divide(X0,a3),a3),
inference(paramodulation,[status(thm)],[f24316,f16668]) ).
fof(f27530,plain,
! [X0] : double_divide(X0,multiply(a3,inverse(a3))) = multiply(double_divide(X0,a3),a3),
inference(forward_demodulation,[status(thm)],[f25249,f27371]) ).
fof(f27595,plain,
! [X0,X1] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(inverse(a3)),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,X1),X1))))) = a3,
inference(paramodulation,[status(thm)],[f27530,f47]) ).
fof(f27700,plain,
! [X0] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(inverse(a3)),multiply(a3,double_divide(inverse(b3),multiply(double_divide(X0,a3),a3))))) = a3,
inference(forward_demodulation,[status(thm)],[f4122,f27595]) ).
fof(f27701,plain,
! [X0] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(inverse(a3)),multiply(double_divide(double_divide(X0,multiply(a3,b3)),a3),a3))) = a3,
inference(forward_demodulation,[status(thm)],[f4418,f27700]) ).
fof(f27702,plain,
! [X0] : double_divide(multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3),double_divide(inverse(inverse(a3)),multiply(double_divide(double_divide(X0,sF1_fnc),a3),a3))) = a3,
inference(forward_demodulation,[status(thm)],[f7,f27701]) ).
fof(f27703,plain,
double_divide(a3,double_divide(inverse(inverse(a3)),a3)) = a3,
inference(forward_demodulation,[status(thm)],[f10045,f27702]) ).
fof(f27704,plain,
inverse(multiply(double_divide(a3,a3),a3)) = a3,
inference(forward_demodulation,[status(thm)],[f17010,f27703]) ).
fof(f27811,plain,
! [X0] : multiply(a3,double_divide(a3,X0)) = multiply(double_divide(X0,a3),a3),
inference(paramodulation,[status(thm)],[f27704,f16917]) ).
fof(f27818,plain,
double_divide(a3,double_divide(a3,a3)) = a3,
inference(paramodulation,[status(thm)],[f27704,f16817]) ).
fof(f27822,plain,
inverse(multiply(double_divide(a3,a3),a3)) = multiply(a3,multiply(a3,inverse(a3))),
inference(paramodulation,[status(thm)],[f27704,f25253]) ).
fof(f27878,plain,
a3 = multiply(a3,multiply(a3,inverse(a3))),
inference(forward_demodulation,[status(thm)],[f27704,f27822]) ).
fof(f30339,plain,
! [X0] : double_divide(a3,double_divide(inverse(multiply(a3,double_divide(a3,X0))),a3)) = X0,
inference(backward_demodulation,[status(thm)],[f27811,f16817]) ).
fof(f30360,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = multiply(a3,double_divide(a3,X0)),
inference(backward_demodulation,[status(thm)],[f27811,f4122]) ).
fof(f31391,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(X1,double_divide(X2,X3))),double_divide(multiply(X3,X2),multiply(a3,double_divide(a3,X0)))) = X1,
inference(backward_demodulation,[status(thm)],[f30360,f18]) ).
fof(f31398,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),multiply(a3,double_divide(a3,X0)))) = X1,
inference(backward_demodulation,[status(thm)],[f30360,f13]) ).
fof(f32234,plain,
! [X0] : double_divide(double_divide(inverse(multiply(a3,double_divide(a3,X0))),a3),X0) = double_divide(a3,double_divide(a3,a3)),
inference(paramodulation,[status(thm)],[f30339,f10045]) ).
fof(f32247,plain,
! [X0] : double_divide(double_divide(inverse(multiply(a3,double_divide(a3,X0))),a3),X0) = a3,
inference(forward_demodulation,[status(thm)],[f27818,f32234]) ).
fof(f32290,plain,
! [X0,X1] : double_divide(a3,double_divide(inverse(X0),multiply(a3,double_divide(a3,double_divide(inverse(multiply(a3,double_divide(a3,multiply(X1,X0)))),a3))))) = X1,
inference(paramodulation,[status(thm)],[f32247,f31398]) ).
fof(f32324,plain,
! [X0,X1] : double_divide(a3,double_divide(inverse(X0),multiply(a3,multiply(X1,X0)))) = X1,
inference(forward_demodulation,[status(thm)],[f30339,f32290]) ).
fof(f32460,plain,
double_divide(a3,double_divide(inverse(c3),multiply(a3,sF3_fnc))) = b3,
inference(paramodulation,[status(thm)],[f9,f32324]) ).
fof(f32472,plain,
! [X0] : double_divide(a3,double_divide(inverse(inverse(X0)),multiply(a3,multiply(a3,inverse(a3))))) = X0,
inference(paramodulation,[status(thm)],[f22994,f32324]) ).
fof(f32531,plain,
double_divide(a3,double_divide(inverse(c3),sF2_fnc)) = b3,
inference(forward_demodulation,[status(thm)],[f10,f32460]) ).
fof(f32539,plain,
! [X0] : double_divide(a3,double_divide(inverse(inverse(X0)),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f27878,f32472]) ).
fof(f32565,plain,
double_divide(double_divide(inverse(c3),sF2_fnc),b3) = double_divide(a3,double_divide(a3,a3)),
inference(paramodulation,[status(thm)],[f32531,f10045]) ).
fof(f32586,plain,
double_divide(double_divide(inverse(c3),sF2_fnc),b3) = a3,
inference(forward_demodulation,[status(thm)],[f27818,f32565]) ).
fof(f32655,plain,
! [X0] : multiply(double_divide(inverse(inverse(X0)),a3),a3) = inverse(X0),
inference(paramodulation,[status(thm)],[f32539,f5]) ).
fof(f32665,plain,
! [X0] : multiply(a3,double_divide(a3,inverse(inverse(X0)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f30360,f32655]) ).
fof(f33105,plain,
! [X0] : double_divide(a3,double_divide(inverse(inverse(X0)),a3)) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f32665,f30339]) ).
fof(f33141,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f32539,f33105]) ).
fof(f33168,plain,
! [X0] : multiply(a3,double_divide(a3,X0)) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f33141,f32665]) ).
fof(f33171,plain,
! [X0] : double_divide(a3,double_divide(X0,a3)) = X0,
inference(backward_demodulation,[status(thm)],[f33141,f32539]) ).
fof(f33175,plain,
! [X0,X1] : double_divide(X0,X1) = inverse(multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f5,f33141]) ).
fof(f33194,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(a3,inverse(a3)),
inference(paramodulation,[status(thm)],[f33141,f22994]) ).
fof(f33253,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),double_divide(a3,double_divide(X0,a3))) = X1,
inference(backward_demodulation,[status(thm)],[f33171,f8394]) ).
fof(f33255,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = X1,
inference(backward_demodulation,[status(thm)],[f33171,f10045]) ).
fof(f33283,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
inference(forward_demodulation,[status(thm)],[f33171,f33253]) ).
fof(f33406,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = inverse(X0),
inference(paramodulation,[status(thm)],[f33255,f5]) ).
fof(f33485,plain,
multiply(a3,b3) = inverse(double_divide(inverse(c3),sF2_fnc)),
inference(paramodulation,[status(thm)],[f32586,f33406]) ).
fof(f33533,plain,
sF1_fnc = inverse(double_divide(inverse(c3),sF2_fnc)),
inference(forward_demodulation,[status(thm)],[f7,f33485]) ).
fof(f33534,plain,
sF1_fnc = multiply(sF2_fnc,inverse(c3)),
inference(forward_demodulation,[status(thm)],[f5,f33533]) ).
fof(f33676,plain,
! [X0] : double_divide(multiply(a3,inverse(a3)),inverse(X0)) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f25253,f33175]) ).
fof(f33729,plain,
! [X0] : double_divide(multiply(a3,inverse(a3)),inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f33141,f33676]) ).
fof(f34404,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(X0,multiply(X1,double_divide(X2,X3))),double_divide(multiply(X3,X2),inverse(X0))) = X1,
inference(backward_demodulation,[status(thm)],[f33168,f31391]) ).
fof(f34407,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,X2)),double_divide(inverse(X2),inverse(X0))) = X1,
inference(backward_demodulation,[status(thm)],[f33168,f31398]) ).
fof(f34967,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,double_divide(X2,inverse(X2)))),double_divide(multiply(a3,inverse(a3)),inverse(X0))) = X1,
inference(paramodulation,[status(thm)],[f33194,f34404]) ).
fof(f34977,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,multiply(X1,double_divide(X2,inverse(X2)))),X0) = X1,
inference(forward_demodulation,[status(thm)],[f33729,f34967]) ).
fof(f34978,plain,
! [X0,X1] : multiply(X0,double_divide(X1,inverse(X1))) = X0,
inference(forward_demodulation,[status(thm)],[f33283,f34977]) ).
fof(f34987,plain,
! [X0,X1] : multiply(X0,double_divide(inverse(X1),X1)) = X0,
inference(paramodulation,[status(thm)],[f33141,f34978]) ).
fof(f35022,plain,
! [X0,X1] : inverse(X0) = double_divide(X0,double_divide(inverse(X1),X1)),
inference(paramodulation,[status(thm)],[f33406,f34987]) ).
fof(f35059,plain,
! [X0,X1] : inverse(double_divide(X0,multiply(X1,inverse(X0)))) = X1,
inference(paramodulation,[status(thm)],[f34407,f35022]) ).
fof(f35079,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X1)),X1) = X0,
inference(forward_demodulation,[status(thm)],[f5,f35059]) ).
fof(f35098,plain,
multiply(sF1_fnc,c3) = sF2_fnc,
inference(paramodulation,[status(thm)],[f33534,f35079]) ).
fof(f35123,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f8,f35098]) ).
fof(f35124,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f35123,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP504-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.58 % Computer : n007.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Sun Sep 20 20:13:05 UTC 2026
% 0.11/0.58 % CPUTime :
% 0.11/0.58 % Drodi V4.1.1
% 112.58/14.84 % Refutation found
% 112.58/14.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 112.58/14.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 59.93/14.99 % Elapsed time: 14.391432 seconds
% 59.93/14.99 % CPU time: 113.701852 seconds
% 59.93/14.99 % Total memory used: 892.137 MB
% 59.93/14.99 % Net memory used: 882.471 MB
%------------------------------------------------------------------------------