%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP103-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:32:31 PM UTC 2026
% Result : Unsatisfiable 3.55s 0.92s
% Output : CNFRefutation 3.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 9
% Syntax : Number of formulae : 287 ( 265 unt; 4 def)
% Number of atoms : 315 ( 283 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 51 ( 23 ~; 24 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 471 ( 471 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : double_divide(double_divide(X,double_divide(double_divide(identity,Y),double_divide(Z,double_divide(Y,X)))),double_divide(identity,identity)) = Z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : inverse(X) = double_divide(X,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : identity = double_divide(X,inverse(X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),double_divide(identity,identity)) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f7,plain,
! [X0,X1] : multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f8,plain,
! [X0] : inverse(X0) = double_divide(X0,identity),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f9,plain,
! [X0] : identity = double_divide(X0,inverse(X0)),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
( multiply(a4,b4) != multiply(b4,a4)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(identity,a2) != a2
| multiply(inverse(a1),a1) != identity ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f11,definition,
( sQ0_spl
<=> multiply(inverse(a1),a1) = identity ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f13,plain,
( sQ0_spl
| multiply(inverse(a1),a1) != identity ),
inference(component_clause,[status(thm)],[f11]) ).
fof(f14,definition,
( sQ1_spl
<=> multiply(identity,a2) = a2 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f16,plain,
( sQ1_spl
| multiply(identity,a2) != a2 ),
inference(component_clause,[status(thm)],[f14]) ).
fof(f17,definition,
( sQ2_spl
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f19,plain,
( sQ2_spl
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(component_clause,[status(thm)],[f17]) ).
fof(f20,definition,
( sQ3_spl
<=> multiply(a4,b4) = multiply(b4,a4) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f22,plain,
( sQ3_spl
| multiply(a4,b4) != multiply(b4,a4) ),
inference(component_clause,[status(thm)],[f20]) ).
fof(f23,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f10,f11,f14,f17,f20]) ).
fof(f24,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0)))),inverse(identity)) = X2,
inference(backward_demodulation,[status(thm)],[f8,f6]) ).
fof(f25,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X1,X0)),
inference(backward_demodulation,[status(thm)],[f8,f7]) ).
fof(f26,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(identity),
inference(paramodulation,[status(thm)],[f9,f25]) ).
fof(f27,plain,
! [X0] : multiply(identity,X0) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f8,f25]) ).
fof(f28,plain,
! [X0,X1] : identity = double_divide(double_divide(X0,X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f25,f9]) ).
fof(f30,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,double_divide(X1,double_divide(inverse(identity),X0)))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f9,f24]) ).
fof(f32,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(X2,double_divide(X1,X0))))),double_divide(X3,X2))),inverse(identity)) = X3,
inference(paramodulation,[status(thm)],[f24,f24]) ).
fof(f33,plain,
! [X0,X1] : double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),double_divide(X1,identity))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f9,f24]) ).
fof(f34,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0)))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f8,f24]) ).
fof(f36,plain,
! [X0,X1] : double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),inverse(identity)) = X1,
inference(forward_demodulation,[status(thm)],[f8,f33]) ).
fof(f37,plain,
! [X0] : multiply(identity,inverse(X0)) = inverse(multiply(identity,X0)),
inference(paramodulation,[status(thm)],[f27,f27]) ).
fof(f38,plain,
! [X0,X1] : multiply(identity,double_divide(X0,X1)) = inverse(multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f40,plain,
! [X0] : identity = double_divide(inverse(X0),multiply(identity,X0)),
inference(paramodulation,[status(thm)],[f27,f9]) ).
fof(f56,plain,
! [X0,X1] : double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),double_divide(X1,identity))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f40,f24]) ).
fof(f60,plain,
! [X0,X1] : double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),inverse(identity)) = X1,
inference(forward_demodulation,[status(thm)],[f8,f56]) ).
fof(f118,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))),identity)),inverse(identity)) = double_divide(X3,X2),
inference(paramodulation,[status(thm)],[f28,f32]) ).
fof(f130,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),inverse(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0))))))),inverse(identity)) = double_divide(X3,X2),
inference(forward_demodulation,[status(thm)],[f8,f118]) ).
fof(f132,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),multiply(double_divide(X0,double_divide(double_divide(identity,X1),double_divide(multiply(X2,X3),double_divide(X1,X0)))),identity)),inverse(identity)) = double_divide(X3,X2),
inference(forward_demodulation,[status(thm)],[f25,f130]) ).
fof(f168,plain,
! [X0] : double_divide(double_divide(inverse(X0),identity),inverse(identity)) = double_divide(identity,X0),
inference(paramodulation,[status(thm)],[f9,f36]) ).
fof(f175,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X0,double_divide(double_divide(identity,X1),double_divide(inverse(identity),double_divide(X1,X0))))),X2)),inverse(identity)) = double_divide(inverse(X3),double_divide(double_divide(identity,X3),inverse(X2))),
inference(paramodulation,[status(thm)],[f36,f32]) ).
fof(f188,plain,
! [X0] : double_divide(inverse(inverse(X0)),inverse(identity)) = double_divide(identity,X0),
inference(forward_demodulation,[status(thm)],[f8,f168]) ).
fof(f189,plain,
! [X0] : double_divide(multiply(identity,X0),inverse(identity)) = double_divide(identity,X0),
inference(forward_demodulation,[status(thm)],[f27,f188]) ).
fof(f208,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity)) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(paramodulation,[status(thm)],[f34,f34]) ).
fof(f209,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity)) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))),
inference(paramodulation,[status(thm)],[f32,f34]) ).
fof(f212,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))),
inference(paramodulation,[status(thm)],[f30,f34]) ).
fof(f213,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(double_divide(identity,identity),X0)),inverse(identity)) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(paramodulation,[status(thm)],[f24,f34]) ).
fof(f214,plain,
! [X0] : double_divide(double_divide(identity,double_divide(double_divide(identity,X0),identity)),inverse(identity)) = X0,
inference(paramodulation,[status(thm)],[f9,f34]) ).
fof(f216,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f27,f34]) ).
fof(f225,plain,
! [X0,X1] : multiply(inverse(identity),double_divide(identity,double_divide(double_divide(identity,X0),double_divide(X1,inverse(X0))))) = inverse(X1),
inference(paramodulation,[status(thm)],[f34,f25]) ).
fof(f227,plain,
! [X0] : double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),inverse(identity)) = X0,
inference(backward_demodulation,[status(thm)],[f229,f34]) ).
fof(f229,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f8,f208]) ).
fof(f235,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X3,double_divide(X2,X1))))),double_divide(X0,X3))),
inference(forward_demodulation,[status(thm)],[f8,f209]) ).
fof(f248,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(inverse(identity),X1)))),
inference(forward_demodulation,[status(thm)],[f8,f212]) ).
fof(f251,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(backward_demodulation,[status(thm)],[f257,f175]) ).
fof(f254,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),inverse(identity)) = double_divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f257,f132]) ).
fof(f255,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),inverse(identity))),double_divide(X0,X1))),
inference(backward_demodulation,[status(thm)],[f257,f235]) ).
fof(f257,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f8,f213]) ).
fof(f258,plain,
! [X0] : double_divide(double_divide(identity,inverse(double_divide(identity,X0))),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f214]) ).
fof(f259,plain,
! [X0] : double_divide(double_divide(identity,multiply(X0,identity)),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f25,f258]) ).
fof(f271,plain,
! [X0] : multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f229,f225]) ).
fof(f310,plain,
! [X0,X1] : double_divide(inverse(multiply(X0,X1)),inverse(identity)) = double_divide(identity,double_divide(X1,X0)),
inference(paramodulation,[status(thm)],[f38,f189]) ).
fof(f314,plain,
! [X0] : multiply(inverse(identity),multiply(identity,X0)) = inverse(double_divide(identity,X0)),
inference(paramodulation,[status(thm)],[f189,f25]) ).
fof(f319,plain,
! [X0] : multiply(inverse(identity),multiply(identity,X0)) = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f25,f314]) ).
fof(f360,plain,
double_divide(double_divide(identity,inverse(identity)),inverse(identity)) = inverse(identity),
inference(paramodulation,[status(thm)],[f26,f259]) ).
fof(f361,plain,
! [X0] : double_divide(double_divide(inverse(multiply(X0,identity)),X0),inverse(identity)) = identity,
inference(paramodulation,[status(thm)],[f259,f36]) ).
fof(f367,plain,
double_divide(identity,inverse(identity)) = inverse(identity),
inference(forward_demodulation,[status(thm)],[f9,f360]) ).
fof(f368,plain,
! [X0] : double_divide(double_divide(identity,multiply(X0,identity)),identity) = X0,
inference(backward_demodulation,[status(thm)],[f412,f259]) ).
fof(f370,plain,
! [X0] : double_divide(multiply(identity,X0),identity) = double_divide(identity,X0),
inference(backward_demodulation,[status(thm)],[f412,f189]) ).
fof(f371,plain,
! [X0] : double_divide(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)),identity) = X0,
inference(backward_demodulation,[status(thm)],[f412,f227]) ).
fof(f373,plain,
! [X0,X1] : double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1))),identity) = X1,
inference(backward_demodulation,[status(thm)],[f412,f36]) ).
fof(f375,plain,
! [X0] : multiply(inverse(X0),X0) = identity,
inference(backward_demodulation,[status(thm)],[f412,f26]) ).
fof(f378,plain,
! [X0] : multiply(identity,multiply(identity,X0)) = multiply(X0,identity),
inference(backward_demodulation,[status(thm)],[f412,f319]) ).
fof(f379,plain,
! [X0,X1] : double_divide(inverse(multiply(X0,X1)),identity) = double_divide(identity,double_divide(X1,X0)),
inference(backward_demodulation,[status(thm)],[f412,f310]) ).
fof(f381,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(backward_demodulation,[status(thm)],[f412,f255]) ).
fof(f382,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity)),identity) = double_divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f412,f254]) ).
fof(f384,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0)),identity) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(backward_demodulation,[status(thm)],[f412,f251]) ).
fof(f385,plain,
! [X0] : multiply(inverse(identity),double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity)) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f412,f271]) ).
fof(f388,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0)))),identity) = X1,
inference(backward_demodulation,[status(thm)],[f412,f216]) ).
fof(f390,plain,
! [X0,X1,X2] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(backward_demodulation,[status(thm)],[f412,f257]) ).
fof(f391,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(backward_demodulation,[status(thm)],[f412,f248]) ).
fof(f394,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(backward_demodulation,[status(thm)],[f412,f229]) ).
fof(f411,plain,
! [X0,X1] : double_divide(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1))),identity) = X1,
inference(backward_demodulation,[status(thm)],[f412,f60]) ).
fof(f412,plain,
identity = inverse(identity),
inference(forward_demodulation,[status(thm)],[f9,f367]) ).
fof(f413,plain,
! [X0] : double_divide(double_divide(inverse(multiply(X0,identity)),X0),identity) = identity,
inference(forward_demodulation,[status(thm)],[f412,f361]) ).
fof(f414,plain,
! [X0] : inverse(double_divide(inverse(multiply(X0,identity)),X0)) = identity,
inference(forward_demodulation,[status(thm)],[f8,f413]) ).
fof(f415,plain,
! [X0] : multiply(X0,inverse(multiply(X0,identity))) = identity,
inference(forward_demodulation,[status(thm)],[f25,f414]) ).
fof(f434,plain,
! [X0] : inverse(double_divide(identity,multiply(X0,identity))) = X0,
inference(forward_demodulation,[status(thm)],[f8,f368]) ).
fof(f437,plain,
! [X0] : multiply(multiply(X0,identity),identity) = X0,
inference(forward_demodulation,[status(thm)],[f25,f434]) ).
fof(f440,plain,
! [X0] : multiply(identity,inverse(X0)) = double_divide(identity,X0),
inference(backward_demodulation,[status(thm)],[f441,f37]) ).
fof(f441,plain,
! [X0] : inverse(multiply(identity,X0)) = double_divide(identity,X0),
inference(forward_demodulation,[status(thm)],[f8,f370]) ).
fof(f442,plain,
! [X0] : inverse(double_divide(double_divide(identity,double_divide(inverse(identity),X0)),inverse(identity))) = X0,
inference(forward_demodulation,[status(thm)],[f8,f371]) ).
fof(f443,plain,
! [X0] : multiply(inverse(identity),double_divide(identity,double_divide(inverse(identity),X0))) = X0,
inference(forward_demodulation,[status(thm)],[f25,f442]) ).
fof(f444,plain,
! [X0] : multiply(identity,double_divide(identity,double_divide(inverse(identity),X0))) = X0,
inference(forward_demodulation,[status(thm)],[f412,f443]) ).
fof(f445,plain,
! [X0] : inverse(multiply(double_divide(inverse(identity),X0),identity)) = X0,
inference(forward_demodulation,[status(thm)],[f38,f444]) ).
fof(f446,plain,
! [X0] : inverse(multiply(double_divide(identity,X0),identity)) = X0,
inference(forward_demodulation,[status(thm)],[f412,f445]) ).
fof(f447,plain,
! [X0,X1] : inverse(double_divide(inverse(X0),double_divide(double_divide(identity,X0),inverse(X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f8,f373]) ).
fof(f448,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,X0),inverse(X1)),inverse(X0)) = X1,
inference(forward_demodulation,[status(thm)],[f25,f447]) ).
fof(f454,plain,
! [X0,X1] : inverse(inverse(multiply(X0,X1))) = double_divide(identity,double_divide(X1,X0)),
inference(forward_demodulation,[status(thm)],[f8,f379]) ).
fof(f455,plain,
! [X0] : double_divide(identity,double_divide(X0,identity)) = multiply(X0,identity),
inference(backward_demodulation,[status(thm)],[f456,f378]) ).
fof(f456,plain,
! [X0,X1] : multiply(identity,multiply(X0,X1)) = double_divide(identity,double_divide(X1,X0)),
inference(forward_demodulation,[status(thm)],[f27,f454]) ).
fof(f460,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity)) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f412,f381]) ).
fof(f461,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,X0)),identity) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f412,f460]) ).
fof(f462,plain,
! [X0,X1] : inverse(double_divide(identity,double_divide(identity,X0))) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f8,f461]) ).
fof(f463,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f25,f462]) ).
fof(f464,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X1)),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f412,f463]) ).
fof(f465,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,inverse(double_divide(identity,double_divide(inverse(identity),X1)))),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f8,f464]) ).
fof(f466,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(inverse(identity),X1),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f25,f465]) ).
fof(f467,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,X1),identity)),double_divide(X0,X1))),
inference(forward_demodulation,[status(thm)],[f412,f466]) ).
fof(f468,plain,
! [X0,X1] : inverse(double_divide(inverse(identity),multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity))) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f8,f382]) ).
fof(f469,plain,
! [X0,X1] : multiply(multiply(double_divide(double_divide(identity,double_divide(inverse(identity),multiply(X0,X1))),inverse(identity)),identity),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f25,f468]) ).
fof(f470,plain,
! [X0,X1] : multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),inverse(identity)),identity),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f412,f469]) ).
fof(f471,plain,
! [X0,X1] : multiply(multiply(double_divide(double_divide(identity,double_divide(identity,multiply(X0,X1))),identity),identity),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f412,f470]) ).
fof(f472,plain,
! [X0,X1] : multiply(multiply(inverse(double_divide(identity,double_divide(identity,multiply(X0,X1)))),identity),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f8,f471]) ).
fof(f473,plain,
! [X0,X1] : multiply(multiply(multiply(double_divide(identity,multiply(X0,X1)),identity),identity),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f25,f472]) ).
fof(f474,plain,
! [X0,X1] : multiply(double_divide(identity,multiply(X0,X1)),inverse(identity)) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f437,f473]) ).
fof(f475,plain,
! [X0,X1] : multiply(double_divide(identity,multiply(X0,X1)),identity) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f412,f474]) ).
fof(f484,plain,
! [X0,X1] : inverse(double_divide(inverse(identity),double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0))) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f8,f384]) ).
fof(f485,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),inverse(identity))),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f25,f484]) ).
fof(f486,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,double_divide(identity,inverse(identity))),inverse(identity))),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f412,f485]) ).
fof(f487,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,double_divide(double_divide(identity,identity),inverse(identity))),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f9,f486]) ).
fof(f488,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,double_divide(inverse(identity),inverse(identity))),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f8,f487]) ).
fof(f489,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,double_divide(identity,inverse(identity))),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f412,f488]) ).
fof(f490,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,identity),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f9,f489]) ).
fof(f491,plain,
! [X0,X1] : multiply(double_divide(inverse(identity),X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f8,f490]) ).
fof(f492,plain,
! [X0,X1] : multiply(double_divide(identity,X0),inverse(identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f412,f491]) ).
fof(f493,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(forward_demodulation,[status(thm)],[f412,f492]) ).
fof(f494,plain,
! [X0] : multiply(identity,double_divide(double_divide(identity,double_divide(inverse(identity),X0)),identity)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f412,f385]) ).
fof(f495,plain,
! [X0] : inverse(multiply(identity,double_divide(identity,double_divide(inverse(identity),X0)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f38,f494]) ).
fof(f496,plain,
! [X0] : multiply(identity,inverse(double_divide(identity,double_divide(inverse(identity),X0)))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f37,f495]) ).
fof(f497,plain,
! [X0] : multiply(identity,multiply(double_divide(inverse(identity),X0),identity)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f25,f496]) ).
fof(f498,plain,
! [X0] : double_divide(identity,double_divide(identity,double_divide(inverse(identity),X0))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f456,f497]) ).
fof(f499,plain,
! [X0] : double_divide(identity,double_divide(identity,double_divide(identity,X0))) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f412,f498]) ).
fof(f515,plain,
! [X0,X1] : inverse(double_divide(identity,double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0))))) = X1,
inference(forward_demodulation,[status(thm)],[f8,f388]) ).
fof(f516,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,inverse(X0)),double_divide(X1,multiply(identity,X0))),identity) = X1,
inference(forward_demodulation,[status(thm)],[f25,f515]) ).
fof(f519,plain,
! [X0,X1,X2] : inverse(double_divide(identity,double_divide(inverse(identity),X0))) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f8,f390]) ).
fof(f520,plain,
! [X0,X1,X2] : multiply(double_divide(inverse(identity),X0),identity) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f25,f519]) ).
fof(f521,plain,
! [X0,X1,X2] : multiply(double_divide(identity,X0),identity) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f412,f520]) ).
fof(f522,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,X0)),inverse(identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f412,f391]) ).
fof(f523,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(identity,X0)),identity) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f412,f522]) ).
fof(f524,plain,
! [X0,X1] : inverse(double_divide(identity,double_divide(identity,X0))) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f8,f523]) ).
fof(f525,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f25,f524]) ).
fof(f533,plain,
! [X0,X1] : inverse(double_divide(identity,double_divide(inverse(identity),X0))) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f8,f394]) ).
fof(f534,plain,
! [X0,X1] : multiply(double_divide(inverse(identity),X0),identity) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f25,f533]) ).
fof(f535,plain,
! [X0,X1] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f412,f534]) ).
fof(f580,plain,
! [X0,X1] : inverse(double_divide(multiply(identity,X0),double_divide(double_divide(identity,inverse(X0)),inverse(X1)))) = X1,
inference(forward_demodulation,[status(thm)],[f8,f411]) ).
fof(f581,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,inverse(X0)),inverse(X1)),multiply(identity,X0)) = X1,
inference(forward_demodulation,[status(thm)],[f25,f580]) ).
fof(f589,plain,
! [X0,X1] : multiply(double_divide(multiply(X0,identity),inverse(X1)),multiply(identity,X0)) = X1,
inference(backward_demodulation,[status(thm)],[f594,f581]) ).
fof(f592,plain,
! [X0,X1] : multiply(double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0))),identity) = X1,
inference(backward_demodulation,[status(thm)],[f594,f516]) ).
fof(f594,plain,
! [X0] : double_divide(identity,inverse(X0)) = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f8,f455]) ).
fof(f624,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,X0),X1),inverse(X0)) = multiply(double_divide(identity,X1),identity),
inference(paramodulation,[status(thm)],[f446,f448]) ).
fof(f659,plain,
! [X0] : identity = double_divide(double_divide(identity,multiply(X0,identity)),X0),
inference(paramodulation,[status(thm)],[f437,f28]) ).
fof(f712,plain,
! [X0] : multiply(double_divide(identity,X0),X0) = identity,
inference(paramodulation,[status(thm)],[f446,f415]) ).
fof(f821,plain,
! [X0] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(double_divide(identity,identity),double_divide(X0,identity))),
inference(paramodulation,[status(thm)],[f712,f467]) ).
fof(f826,plain,
! [X0] : multiply(double_divide(identity,inverse(X0)),identity) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)),
inference(paramodulation,[status(thm)],[f40,f467]) ).
fof(f827,plain,
! [X0,X1] : multiply(double_divide(identity,double_divide(X0,X1)),identity) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)),
inference(paramodulation,[status(thm)],[f28,f467]) ).
fof(f836,plain,
! [X0] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(inverse(identity),double_divide(X0,identity))),
inference(forward_demodulation,[status(thm)],[f8,f821]) ).
fof(f837,plain,
! [X0] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(identity,double_divide(X0,identity))),
inference(forward_demodulation,[status(thm)],[f412,f836]) ).
fof(f838,plain,
! [X0] : multiply(double_divide(identity,X0),identity) = double_divide(identity,double_divide(identity,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f8,f837]) ).
fof(f841,plain,
! [X0,X1] : double_divide(identity,multiply(multiply(X0,X1),identity)) = double_divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f852,f475]) ).
fof(f845,plain,
! [X0,X1] : multiply(double_divide(double_divide(identity,X0),X1),inverse(X0)) = double_divide(identity,multiply(X1,identity)),
inference(backward_demodulation,[status(thm)],[f852,f624]) ).
fof(f848,plain,
! [X0,X1] : double_divide(identity,multiply(X0,identity)) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(backward_demodulation,[status(thm)],[f852,f535]) ).
fof(f849,plain,
! [X0,X1] : double_divide(identity,multiply(X0,identity)) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(backward_demodulation,[status(thm)],[f852,f525]) ).
fof(f850,plain,
! [X0,X1,X2] : double_divide(identity,multiply(X0,identity)) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(backward_demodulation,[status(thm)],[f852,f521]) ).
fof(f851,plain,
! [X0,X1] : double_divide(identity,multiply(X0,identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),inverse(X0))),
inference(backward_demodulation,[status(thm)],[f852,f493]) ).
fof(f852,plain,
! [X0] : multiply(double_divide(identity,X0),identity) = double_divide(identity,multiply(X0,identity)),
inference(forward_demodulation,[status(thm)],[f594,f838]) ).
fof(f869,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity)),
inference(forward_demodulation,[status(thm)],[f852,f826]) ).
fof(f870,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)))),
inference(forward_demodulation,[status(thm)],[f8,f869]) ).
fof(f871,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = multiply(double_divide(identity,multiply(double_divide(identity,multiply(identity,X0)),identity)),identity),
inference(forward_demodulation,[status(thm)],[f594,f870]) ).
fof(f872,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = double_divide(identity,double_divide(identity,multiply(identity,X0))),
inference(forward_demodulation,[status(thm)],[f475,f871]) ).
fof(f873,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,X1),identity)) = double_divide(identity,double_divide(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity)),
inference(forward_demodulation,[status(thm)],[f852,f827]) ).
fof(f874,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,X1),identity)) = double_divide(identity,inverse(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)))),
inference(forward_demodulation,[status(thm)],[f8,f873]) ).
fof(f875,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,X1),identity)) = multiply(double_divide(identity,multiply(double_divide(identity,multiply(X1,X0)),identity)),identity),
inference(forward_demodulation,[status(thm)],[f594,f874]) ).
fof(f876,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,X1),identity)) = double_divide(identity,double_divide(identity,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f475,f875]) ).
fof(f939,plain,
! [X0] : multiply(double_divide(identity,double_divide(identity,X0)),identity) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f499,f25]) ).
fof(f954,plain,
! [X0] : double_divide(identity,multiply(double_divide(identity,X0),identity)) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f852,f939]) ).
fof(f955,plain,
! [X0] : double_divide(identity,double_divide(identity,multiply(X0,identity))) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f876,f954]) ).
fof(f960,plain,
! [X0] : double_divide(identity,double_divide(identity,multiply(X0,identity))) = multiply(identity,X0),
inference(forward_demodulation,[status(thm)],[f27,f955]) ).
fof(f964,plain,
! [X0] : multiply(identity,double_divide(identity,X0)) = double_divide(identity,multiply(identity,X0)),
inference(paramodulation,[status(thm)],[f441,f440]) ).
fof(f977,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = double_divide(identity,inverse(multiply(X0,identity))),
inference(backward_demodulation,[status(thm)],[f980,f872]) ).
fof(f980,plain,
! [X0] : inverse(multiply(X0,identity)) = double_divide(identity,multiply(identity,X0)),
inference(forward_demodulation,[status(thm)],[f38,f964]) ).
fof(f994,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = multiply(multiply(X0,identity),identity),
inference(forward_demodulation,[status(thm)],[f594,f977]) ).
fof(f995,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = X0,
inference(forward_demodulation,[status(thm)],[f437,f994]) ).
fof(f1098,plain,
! [X0] : double_divide(identity,multiply(identity,X0)) = multiply(inverse(X0),identity),
inference(paramodulation,[status(thm)],[f27,f594]) ).
fof(f1099,plain,
! [X0,X1] : double_divide(identity,multiply(X0,X1)) = multiply(double_divide(X1,X0),identity),
inference(paramodulation,[status(thm)],[f25,f594]) ).
fof(f1106,plain,
! [X0] : multiply(inverse(X0),identity) = inverse(multiply(X0,identity)),
inference(paramodulation,[status(thm)],[f594,f25]) ).
fof(f1115,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(X0,multiply(identity,X1)),multiply(X1,identity))) = X0,
inference(backward_demodulation,[status(thm)],[f1099,f592]) ).
fof(f1211,plain,
! [X0] : double_divide(identity,multiply(identity,identity)) = double_divide(X0,double_divide(identity,X0)),
inference(paramodulation,[status(thm)],[f712,f841]) ).
fof(f1223,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,X1))) = inverse(multiply(multiply(X1,X0),identity)),
inference(paramodulation,[status(thm)],[f841,f499]) ).
fof(f1229,plain,
! [X0] : multiply(inverse(identity),identity) = double_divide(X0,double_divide(identity,X0)),
inference(forward_demodulation,[status(thm)],[f1098,f1211]) ).
fof(f1231,plain,
! [X0] : identity = double_divide(X0,double_divide(identity,X0)),
inference(forward_demodulation,[status(thm)],[f375,f1229]) ).
fof(f1255,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,X1))) = multiply(inverse(multiply(X1,X0)),identity),
inference(forward_demodulation,[status(thm)],[f1106,f1223]) ).
fof(f1297,plain,
! [X0] : multiply(identity,inverse(X0)) = double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)),
inference(paramodulation,[status(thm)],[f1231,f845]) ).
fof(f1301,plain,
! [X0,X1] : multiply(double_divide(multiply(X0,identity),X1),inverse(inverse(X0))) = double_divide(identity,multiply(X1,identity)),
inference(paramodulation,[status(thm)],[f594,f845]) ).
fof(f1309,plain,
! [X0,X1] : double_divide(identity,multiply(double_divide(identity,multiply(X0,identity)),identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)),
inference(paramodulation,[status(thm)],[f845,f841]) ).
fof(f1313,plain,
! [X0] : double_divide(identity,X0) = double_divide(identity,multiply(double_divide(identity,double_divide(identity,X0)),identity)),
inference(forward_demodulation,[status(thm)],[f440,f1297]) ).
fof(f1314,plain,
! [X0] : double_divide(identity,X0) = double_divide(identity,double_divide(identity,multiply(double_divide(identity,X0),identity))),
inference(forward_demodulation,[status(thm)],[f1099,f1313]) ).
fof(f1315,plain,
! [X0] : double_divide(identity,X0) = multiply(identity,double_divide(identity,X0)),
inference(forward_demodulation,[status(thm)],[f960,f1314]) ).
fof(f1316,plain,
! [X0] : multiply(inverse(X0),identity) = double_divide(identity,X0),
inference(backward_demodulation,[status(thm)],[f1317,f1106]) ).
fof(f1317,plain,
! [X0] : double_divide(identity,X0) = inverse(multiply(X0,identity)),
inference(forward_demodulation,[status(thm)],[f38,f1315]) ).
fof(f1323,plain,
! [X0] : double_divide(identity,multiply(inverse(X0),identity)) = X0,
inference(backward_demodulation,[status(thm)],[f1324,f589]) ).
fof(f1324,plain,
! [X0,X1] : multiply(double_divide(multiply(X0,identity),X1),multiply(identity,X0)) = double_divide(identity,multiply(X1,identity)),
inference(forward_demodulation,[status(thm)],[f27,f1301]) ).
fof(f1336,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,multiply(multiply(X0,identity),identity))) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)),
inference(forward_demodulation,[status(thm)],[f1099,f1309]) ).
fof(f1337,plain,
! [X0,X1] : multiply(identity,multiply(X0,identity)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)),
inference(forward_demodulation,[status(thm)],[f960,f1336]) ).
fof(f1338,plain,
! [X0] : double_divide(identity,multiply(X0,identity)) = double_divide(identity,double_divide(identity,inverse(X0))),
inference(backward_demodulation,[status(thm)],[f1339,f851]) ).
fof(f1339,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,X0)) = double_divide(inverse(X1),double_divide(double_divide(identity,X1),X0)),
inference(forward_demodulation,[status(thm)],[f456,f1337]) ).
fof(f1344,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(X0,X1))) = double_divide(identity,multiply(X1,X0)),
inference(backward_demodulation,[status(thm)],[f1316,f1255]) ).
fof(f1352,plain,
! [X0] : double_divide(identity,multiply(identity,X0)) = double_divide(identity,X0),
inference(backward_demodulation,[status(thm)],[f1316,f1098]) ).
fof(f1353,plain,
! [X0] : double_divide(identity,double_divide(identity,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f1316,f995]) ).
fof(f1355,plain,
! [X0] : multiply(X0,identity) = multiply(identity,X0),
inference(backward_demodulation,[status(thm)],[f1360,f960]) ).
fof(f1360,plain,
! [X0] : double_divide(identity,double_divide(identity,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1316,f1323]) ).
fof(f1362,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = double_divide(X1,X0),
inference(backward_demodulation,[status(thm)],[f1375,f841]) ).
fof(f1369,plain,
! [X0,X1,X2] : inverse(X0) = double_divide(X1,double_divide(double_divide(identity,X2),double_divide(X0,double_divide(X2,X1)))),
inference(backward_demodulation,[status(thm)],[f1375,f850]) ).
fof(f1370,plain,
! [X0,X1] : inverse(X0) = double_divide(X1,double_divide(identity,double_divide(X0,double_divide(identity,X1)))),
inference(backward_demodulation,[status(thm)],[f1375,f849]) ).
fof(f1371,plain,
! [X0,X1] : inverse(X0) = double_divide(identity,double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(backward_demodulation,[status(thm)],[f1375,f848]) ).
fof(f1374,plain,
! [X0] : identity = double_divide(inverse(X0),X0),
inference(backward_demodulation,[status(thm)],[f1375,f659]) ).
fof(f1375,plain,
! [X0] : double_divide(identity,multiply(X0,identity)) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f1360,f1338]) ).
fof(f1376,plain,
! [X0,X1] : double_divide(multiply(X0,identity),double_divide(X1,multiply(identity,X0))) = X1,
inference(backward_demodulation,[status(thm)],[f1382,f1115]) ).
fof(f1382,plain,
! [X0,X1] : double_divide(X0,X1) = double_divide(identity,multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1360,f1344]) ).
fof(f1386,plain,
! [X0] : double_divide(X0,identity) = double_divide(identity,X0),
inference(forward_demodulation,[status(thm)],[f1382,f1352]) ).
fof(f1387,plain,
! [X0] : inverse(inverse(X0)) = multiply(X0,identity),
inference(backward_demodulation,[status(thm)],[f1409,f594]) ).
fof(f1409,plain,
! [X0] : inverse(X0) = double_divide(identity,X0),
inference(forward_demodulation,[status(thm)],[f8,f1386]) ).
fof(f1410,plain,
! [X0] : inverse(double_divide(identity,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1409,f1353]) ).
fof(f1419,plain,
! [X0] : multiply(X0,identity) = X0,
inference(forward_demodulation,[status(thm)],[f25,f1410]) ).
fof(f1427,plain,
! [X0] : X0 = multiply(identity,X0),
inference(forward_demodulation,[status(thm)],[f1419,f1355]) ).
fof(f1438,plain,
! [X0,X1,X2] : inverse(X0) = double_divide(X1,double_divide(inverse(X2),double_divide(X0,double_divide(X2,X1)))),
inference(forward_demodulation,[status(thm)],[f1409,f1369]) ).
fof(f1439,plain,
! [X0,X1] : inverse(X0) = double_divide(X1,inverse(double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f1409,f1370]) ).
fof(f1440,plain,
! [X0,X1] : inverse(X0) = double_divide(X1,multiply(double_divide(identity,X1),X0)),
inference(forward_demodulation,[status(thm)],[f25,f1439]) ).
fof(f1441,plain,
! [X0,X1] : inverse(X0) = double_divide(X1,multiply(inverse(X1),X0)),
inference(forward_demodulation,[status(thm)],[f1409,f1440]) ).
fof(f1442,plain,
! [X0,X1] : inverse(X0) = inverse(double_divide(double_divide(identity,X1),double_divide(X0,inverse(X1)))),
inference(forward_demodulation,[status(thm)],[f1409,f1371]) ).
fof(f1443,plain,
! [X0,X1] : inverse(X0) = multiply(double_divide(X0,inverse(X1)),double_divide(identity,X1)),
inference(forward_demodulation,[status(thm)],[f25,f1442]) ).
fof(f1445,plain,
! [X0,X1] : inverse(X0) = multiply(double_divide(X0,inverse(X1)),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1409,f1443]) ).
fof(f1448,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,multiply(identity,X0))) = X1,
inference(forward_demodulation,[status(thm)],[f1419,f1376]) ).
fof(f1450,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = X1,
inference(forward_demodulation,[status(thm)],[f1427,f1448]) ).
fof(f1460,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f1419,f1387]) ).
fof(f1505,plain,
! [X0,X1,X2,X3] : inverse(X0) = double_divide(X1,double_divide(double_divide(X2,X3),double_divide(X0,double_divide(multiply(X3,X2),X1)))),
inference(paramodulation,[status(thm)],[f1362,f1438]) ).
fof(f1539,plain,
! [X0,X1] : inverse(X0) = double_divide(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f1460,f1441]) ).
fof(f1542,plain,
! [X0,X1,X2] : inverse(X0) = double_divide(double_divide(X1,X2),multiply(multiply(X2,X1),X0)),
inference(paramodulation,[status(thm)],[f25,f1441]) ).
fof(f1584,plain,
! [X0,X1] : inverse(X0) = multiply(double_divide(X0,X1),inverse(inverse(X1))),
inference(paramodulation,[status(thm)],[f1460,f1445]) ).
fof(f1598,plain,
! [X0,X1] : inverse(X0) = multiply(double_divide(X0,X1),X1),
inference(forward_demodulation,[status(thm)],[f1460,f1584]) ).
fof(f1631,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X0) = X1,
inference(paramodulation,[status(thm)],[f1450,f1450]) ).
fof(f1636,plain,
! [X0,X1,X2] : inverse(X0) = double_divide(double_divide(X1,X2),double_divide(inverse(X2),double_divide(X0,X1))),
inference(paramodulation,[status(thm)],[f1450,f1438]) ).
fof(f1653,plain,
! [X0,X1] : inverse(inverse(double_divide(X0,X1))) = double_divide(X1,double_divide(inverse(X0),identity)),
inference(paramodulation,[status(thm)],[f1374,f1438]) ).
fof(f1661,plain,
! [X0,X1] : double_divide(X0,X1) = double_divide(X1,double_divide(inverse(X0),identity)),
inference(forward_demodulation,[status(thm)],[f1460,f1653]) ).
fof(f1662,plain,
! [X0,X1] : double_divide(X0,X1) = double_divide(X1,inverse(inverse(X0))),
inference(forward_demodulation,[status(thm)],[f8,f1661]) ).
fof(f1669,plain,
! [X0,X1] : double_divide(X0,double_divide(X0,X1)) = X1,
inference(backward_demodulation,[status(thm)],[f1670,f1631]) ).
fof(f1670,plain,
! [X0,X1] : double_divide(X0,X1) = double_divide(X1,X0),
inference(forward_demodulation,[status(thm)],[f1460,f1662]) ).
fof(f1734,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X0,X1)),
inference(paramodulation,[status(thm)],[f1670,f25]) ).
fof(f1764,plain,
! [X0,X1,X2,X3] : inverse(X0) = double_divide(double_divide(X1,multiply(X2,X3)),double_divide(double_divide(X3,X2),double_divide(X0,X1))),
inference(paramodulation,[status(thm)],[f1450,f1505]) ).
fof(f1855,plain,
! [X0,X1] : double_divide(X0,inverse(X1)) = multiply(inverse(X0),X1),
inference(paramodulation,[status(thm)],[f1441,f1669]) ).
fof(f2140,plain,
! [X0,X1] : inverse(X0) = multiply(X1,double_divide(X0,X1)),
inference(paramodulation,[status(thm)],[f1669,f1598]) ).
fof(f2141,plain,
! [X0,X1] : inverse(X0) = multiply(X1,double_divide(X1,X0)),
inference(paramodulation,[status(thm)],[f1450,f1598]) ).
fof(f2194,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(X2)) = multiply(multiply(X1,X0),X2),
inference(paramodulation,[status(thm)],[f1542,f1669]) ).
fof(f2253,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(paramodulation,[status(thm)],[f25,f1734]) ).
fof(f2266,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = double_divide(X0,X1),
inference(paramodulation,[status(thm)],[f1734,f1460]) ).
fof(f2271,plain,
( sQ3_spl
| multiply(a4,b4) != multiply(a4,b4) ),
inference(backward_demodulation,[status(thm)],[f2253,f22]) ).
fof(f2281,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2271]) ).
fof(f2282,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2281]) ).
fof(f2283,plain,
( sQ2_spl
| multiply(c3,multiply(a3,b3)) != multiply(a3,multiply(b3,c3)) ),
inference(forward_demodulation,[status(thm)],[f2253,f19]) ).
fof(f2348,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(X2)) = double_divide(inverse(X1),double_divide(X2,X0)),
inference(paramodulation,[status(thm)],[f1636,f1669]) ).
fof(f2416,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = double_divide(inverse(X0),double_divide(X2,X1)),
inference(forward_demodulation,[status(thm)],[f2194,f2348]) ).
fof(f2801,plain,
! [X0,X1] : inverse(double_divide(X0,X1)) = double_divide(inverse(X0),inverse(X1)),
inference(paramodulation,[status(thm)],[f2141,f1539]) ).
fof(f2802,plain,
! [X0,X1] : inverse(double_divide(X0,X1)) = double_divide(inverse(X1),inverse(X0)),
inference(paramodulation,[status(thm)],[f2140,f1539]) ).
fof(f2826,plain,
! [X0,X1] : multiply(X0,X1) = double_divide(inverse(X0),inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1734,f2801]) ).
fof(f2827,plain,
! [X0,X1] : multiply(X0,X1) = double_divide(inverse(X1),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1734,f2802]) ).
fof(f3002,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(double_divide(X0,X1),double_divide(X2,X3)),inverse(X2)) = double_divide(X3,multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f1764,f1450]) ).
fof(f3159,plain,
! [X0,X1,X2,X3] : double_divide(inverse(X0),double_divide(double_divide(X1,X2),double_divide(X0,X3))) = double_divide(X3,multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f1670,f3002]) ).
fof(f3160,plain,
! [X0,X1,X2,X3] : multiply(multiply(X0,double_divide(X0,X1)),double_divide(X2,X3)) = double_divide(X1,multiply(X3,X2)),
inference(forward_demodulation,[status(thm)],[f2416,f3159]) ).
fof(f3161,plain,
! [X0,X1,X2] : multiply(inverse(X0),double_divide(X1,X2)) = double_divide(X0,multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f2141,f3160]) ).
fof(f3162,plain,
! [X0,X1,X2] : double_divide(X0,inverse(double_divide(X1,X2))) = double_divide(X0,multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f1855,f3161]) ).
fof(f3163,plain,
! [X0,X1,X2] : double_divide(X0,multiply(X1,X2)) = double_divide(X0,multiply(X2,X1)),
inference(forward_demodulation,[status(thm)],[f1734,f3162]) ).
fof(f3749,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = double_divide(inverse(X0),double_divide(X1,X2)),
inference(paramodulation,[status(thm)],[f2266,f2826]) ).
fof(f3776,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X2,X1)),
inference(backward_demodulation,[status(thm)],[f3749,f2416]) ).
fof(f4156,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(inverse(X1),X0),
inference(paramodulation,[status(thm)],[f1460,f2827]) ).
fof(f5778,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = inverse(double_divide(X2,multiply(X1,X0))),
inference(paramodulation,[status(thm)],[f3163,f25]) ).
fof(f5828,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = inverse(double_divide(X1,multiply(X2,X0))),
inference(forward_demodulation,[status(thm)],[f3776,f5778]) ).
fof(f5829,plain,
( sQ2_spl
| multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)) ),
inference(backward_demodulation,[status(thm)],[f5835,f2283]) ).
fof(f5835,plain,
! [X0,X1,X2] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X2,X0)),
inference(forward_demodulation,[status(thm)],[f1734,f5828]) ).
fof(f5858,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5829]) ).
fof(f5859,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f5858]) ).
fof(f5875,plain,
( sQ0_spl
| double_divide(inverse(a1),a1) != identity ),
inference(forward_demodulation,[status(thm)],[f4156,f13]) ).
fof(f5876,plain,
( sQ0_spl
| double_divide(a1,inverse(a1)) != identity ),
inference(forward_demodulation,[status(thm)],[f1670,f5875]) ).
fof(f5877,plain,
( sQ0_spl
| identity != identity ),
inference(forward_demodulation,[status(thm)],[f9,f5876]) ).
fof(f5878,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5877]) ).
fof(f5879,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f5878]) ).
fof(f5882,plain,
( sQ1_spl
| a2 != a2 ),
inference(forward_demodulation,[status(thm)],[f1427,f16]) ).
fof(f5883,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5882]) ).
fof(f5884,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f5883]) ).
fof(f5885,plain,
$false,
inference(sat_refutation,[status(thm)],[f23,f2282,f5859,f5879,f5884]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP103-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 19:57:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 3.55/0.92 % Refutation found
% 3.55/0.92 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.55/0.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.55/0.95 % Elapsed time: 0.561968 seconds
% 3.55/0.95 % CPU time: 4.124871 seconds
% 3.55/0.95 % Total memory used: 118.565 MB
% 3.55/0.95 % Net memory used: 114.219 MB
%------------------------------------------------------------------------------