%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP102-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 0.13s 10.50s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 9
% Syntax : Number of formulae : 124 ( 105 unt; 4 def)
% Number of atoms : 149 ( 120 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 45 ( 20 ~; 21 |; 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 : 181 ( 181 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : double_divide(double_divide(X,double_divide(double_divide(double_divide(Y,X),Z),double_divide(Y,identity))),double_divide(identity,identity)) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] : multiply(X,Y) = double_divide(double_divide(Y,X),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : inverse(X) = double_divide(X,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : identity = double_divide(X,inverse(X)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),double_divide(X1,identity))),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(double_divide(X1,X0),X2),double_divide(X1,identity))),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,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),inverse(identity)) = X2,
inference(forward_demodulation,[status(thm)],[f8,f24]) ).
fof(f27,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(identity),
inference(paramodulation,[status(thm)],[f9,f25]) ).
fof(f28,plain,
! [X0] : multiply(identity,X0) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f8,f25]) ).
fof(f29,plain,
! [X0,X1] : identity = double_divide(double_divide(X0,X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f25,f9]) ).
fof(f31,plain,
! [X0] : multiply(identity,inverse(X0)) = inverse(multiply(identity,X0)),
inference(paramodulation,[status(thm)],[f28,f28]) ).
fof(f32,plain,
! [X0,X1] : multiply(identity,double_divide(X0,X1)) = inverse(multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f25,f28]) ).
fof(f43,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(identity)) = double_divide(double_divide(double_divide(X2,double_divide(identity,X0)),X1),inverse(X2)),
inference(paramodulation,[status(thm)],[f26,f26]) ).
fof(f45,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,inverse(X1))),inverse(identity)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f29,f26]) ).
fof(f48,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),inverse(double_divide(X2,double_divide(double_divide(double_divide(X3,X2),X0),inverse(X3)))))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f26,f26]) ).
fof(f50,plain,
! [X0,X1] : double_divide(double_divide(inverse(X0),double_divide(double_divide(identity,X1),inverse(X0))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f9,f26]) ).
fof(f51,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(inverse(X0),X1),inverse(X0))),inverse(identity)) = X1,
inference(paramodulation,[status(thm)],[f8,f26]) ).
fof(f58,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(inverse(identity),double_divide(double_divide(X0,X1),multiply(double_divide(double_divide(double_divide(X2,X3),X0),inverse(X2)),X3))),inverse(identity)) = X1,
inference(forward_demodulation,[status(thm)],[f25,f48]) ).
fof(f68,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),inverse(identity)) = double_divide(double_divide(double_divide(inverse(X2),double_divide(identity,X0)),X1),multiply(identity,X2)),
inference(paramodulation,[status(thm)],[f28,f43]) ).
fof(f277,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),identity),inverse(identity)) = double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)),
inference(paramodulation,[status(thm)],[f29,f58]) ).
fof(f286,plain,
! [X0,X1,X2] : double_divide(double_divide(inverse(identity),double_divide(identity,multiply(double_divide(double_divide(double_divide(X0,X1),X2),inverse(X0)),X1))),inverse(identity)) = inverse(X2),
inference(paramodulation,[status(thm)],[f9,f58]) ).
fof(f321,plain,
! [X0,X1] : double_divide(inverse(inverse(identity)),inverse(identity)) = double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f8,f277]) ).
fof(f322,plain,
! [X0,X1] : double_divide(multiply(identity,identity),inverse(identity)) = double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)),
inference(forward_demodulation,[status(thm)],[f28,f321]) ).
fof(f391,plain,
! [X0] : double_divide(double_divide(inverse(double_divide(identity,X0)),identity),inverse(identity)) = X0,
inference(paramodulation,[status(thm)],[f9,f50]) ).
fof(f415,plain,
! [X0] : double_divide(inverse(inverse(double_divide(identity,X0))),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f391]) ).
fof(f416,plain,
! [X0] : double_divide(multiply(identity,double_divide(identity,X0)),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f28,f415]) ).
fof(f417,plain,
! [X0] : double_divide(inverse(multiply(X0,identity)),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f32,f416]) ).
fof(f434,plain,
double_divide(multiply(identity,inverse(identity)),inverse(identity)) = identity,
inference(paramodulation,[status(thm)],[f31,f417]) ).
fof(f436,plain,
double_divide(inverse(inverse(identity)),inverse(identity)) = inverse(identity),
inference(paramodulation,[status(thm)],[f27,f417]) ).
fof(f445,plain,
! [X0] : multiply(inverse(identity),inverse(multiply(X0,identity))) = inverse(X0),
inference(paramodulation,[status(thm)],[f417,f25]) ).
fof(f448,plain,
! [X0,X1] : inverse(identity) = double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)),
inference(backward_demodulation,[status(thm)],[f449,f322]) ).
fof(f449,plain,
double_divide(multiply(identity,identity),inverse(identity)) = inverse(identity),
inference(forward_demodulation,[status(thm)],[f28,f436]) ).
fof(f490,plain,
! [X0,X1] : double_divide(double_divide(inverse(identity),double_divide(identity,multiply(double_divide(double_divide(double_divide(X0,X1),multiply(identity,inverse(identity))),inverse(X0)),X1))),inverse(identity)) = inverse(identity),
inference(paramodulation,[status(thm)],[f434,f58]) ).
fof(f502,plain,
inverse(multiply(identity,inverse(identity))) = inverse(identity),
inference(forward_demodulation,[status(thm)],[f286,f490]) ).
fof(f503,plain,
multiply(identity,inverse(inverse(identity))) = inverse(identity),
inference(forward_demodulation,[status(thm)],[f31,f502]) ).
fof(f504,plain,
multiply(identity,multiply(identity,identity)) = inverse(identity),
inference(forward_demodulation,[status(thm)],[f28,f503]) ).
fof(f538,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(identity,X0),inverse(identity)) = double_divide(double_divide(X1,X0),multiply(double_divide(double_divide(double_divide(X2,X3),X1),inverse(X2)),X3)),
inference(paramodulation,[status(thm)],[f58,f51]) ).
fof(f715,plain,
inverse(identity) = double_divide(double_divide(identity,inverse(identity)),inverse(multiply(identity,inverse(identity)))),
inference(paramodulation,[status(thm)],[f434,f448]) ).
fof(f736,plain,
! [X0] : double_divide(double_divide(X0,inverse(identity)),inverse(identity)) = X0,
inference(paramodulation,[status(thm)],[f448,f26]) ).
fof(f738,plain,
! [X0,X1] : double_divide(double_divide(X0,inverse(X1)),inverse(identity)) = double_divide(inverse(identity),inverse(double_divide(X1,double_divide(identity,X0)))),
inference(paramodulation,[status(thm)],[f448,f43]) ).
fof(f756,plain,
inverse(identity) = double_divide(identity,inverse(multiply(identity,inverse(identity)))),
inference(forward_demodulation,[status(thm)],[f9,f715]) ).
fof(f757,plain,
inverse(identity) = double_divide(identity,multiply(identity,inverse(inverse(identity)))),
inference(forward_demodulation,[status(thm)],[f31,f756]) ).
fof(f758,plain,
inverse(identity) = double_divide(identity,multiply(identity,multiply(identity,identity))),
inference(forward_demodulation,[status(thm)],[f28,f757]) ).
fof(f759,plain,
inverse(identity) = double_divide(identity,inverse(identity)),
inference(forward_demodulation,[status(thm)],[f504,f758]) ).
fof(f760,plain,
! [X0,X1] : identity = double_divide(double_divide(double_divide(X0,X1),X1),inverse(X0)),
inference(backward_demodulation,[status(thm)],[f902,f448]) ).
fof(f761,plain,
! [X0] : multiply(identity,inverse(multiply(X0,identity))) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f902,f445]) ).
fof(f767,plain,
! [X0] : double_divide(inverse(multiply(X0,identity)),identity) = X0,
inference(backward_demodulation,[status(thm)],[f902,f417]) ).
fof(f776,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1))),identity) = X2,
inference(backward_demodulation,[status(thm)],[f902,f26]) ).
fof(f801,plain,
! [X0,X1,X2,X3] : double_divide(double_divide(identity,X0),identity) = double_divide(double_divide(X1,X0),multiply(double_divide(double_divide(double_divide(X2,X3),X1),inverse(X2)),X3)),
inference(backward_demodulation,[status(thm)],[f902,f538]) ).
fof(f892,plain,
! [X0,X1,X2] : double_divide(double_divide(X0,X1),identity) = double_divide(double_divide(double_divide(inverse(X2),double_divide(identity,X0)),X1),multiply(identity,X2)),
inference(backward_demodulation,[status(thm)],[f902,f68]) ).
fof(f901,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(identity,inverse(X1))),identity) = multiply(X0,X1),
inference(backward_demodulation,[status(thm)],[f902,f45]) ).
fof(f902,plain,
inverse(identity) = identity,
inference(forward_demodulation,[status(thm)],[f9,f759]) ).
fof(f966,plain,
! [X0] : double_divide(double_divide(X0,identity),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f902,f736]) ).
fof(f967,plain,
! [X0] : double_divide(inverse(X0),inverse(identity)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f966]) ).
fof(f968,plain,
! [X0] : double_divide(inverse(X0),identity) = X0,
inference(forward_demodulation,[status(thm)],[f902,f967]) ).
fof(f969,plain,
! [X0] : multiply(identity,X0) = X0,
inference(backward_demodulation,[status(thm)],[f970,f28]) ).
fof(f970,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f8,f968]) ).
fof(f974,plain,
! [X0,X1] : double_divide(double_divide(X0,inverse(X1)),identity) = double_divide(inverse(identity),inverse(double_divide(X1,double_divide(identity,X0)))),
inference(forward_demodulation,[status(thm)],[f902,f738]) ).
fof(f975,plain,
! [X0,X1] : inverse(double_divide(X0,inverse(X1))) = double_divide(inverse(identity),inverse(double_divide(X1,double_divide(identity,X0)))),
inference(forward_demodulation,[status(thm)],[f8,f974]) ).
fof(f976,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(inverse(identity),inverse(double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f25,f975]) ).
fof(f977,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(identity,inverse(double_divide(X0,double_divide(identity,X1)))),
inference(forward_demodulation,[status(thm)],[f902,f976]) ).
fof(f978,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(identity,multiply(double_divide(identity,X1),X0)),
inference(forward_demodulation,[status(thm)],[f25,f977]) ).
fof(f1038,plain,
! [X0] : inverse(inverse(multiply(X0,identity))) = X0,
inference(forward_demodulation,[status(thm)],[f8,f767]) ).
fof(f1041,plain,
! [X0] : multiply(identity,multiply(X0,identity)) = X0,
inference(forward_demodulation,[status(thm)],[f28,f1038]) ).
fof(f1052,plain,
! [X0,X1,X2] : inverse(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),X2),inverse(X1)))) = X2,
inference(forward_demodulation,[status(thm)],[f8,f776]) ).
fof(f1054,plain,
! [X0,X1,X2] : multiply(double_divide(double_divide(double_divide(X0,X1),X2),inverse(X0)),X1) = X2,
inference(forward_demodulation,[status(thm)],[f25,f1052]) ).
fof(f1142,plain,
! [X0,X1,X2,X3] : inverse(double_divide(identity,X0)) = double_divide(double_divide(X1,X0),multiply(double_divide(double_divide(double_divide(X2,X3),X1),inverse(X2)),X3)),
inference(forward_demodulation,[status(thm)],[f8,f801]) ).
fof(f1143,plain,
! [X0,X1,X2,X3] : multiply(X0,identity) = double_divide(double_divide(X1,X0),multiply(double_divide(double_divide(double_divide(X2,X3),X1),inverse(X2)),X3)),
inference(forward_demodulation,[status(thm)],[f25,f1142]) ).
fof(f1151,plain,
! [X0,X1] : multiply(X0,identity) = double_divide(double_divide(X1,X0),X1),
inference(forward_demodulation,[status(thm)],[f1054,f1143]) ).
fof(f1496,plain,
! [X0,X1,X2] : inverse(double_divide(X0,X1)) = double_divide(double_divide(double_divide(inverse(X2),double_divide(identity,X0)),X1),multiply(identity,X2)),
inference(forward_demodulation,[status(thm)],[f8,f892]) ).
fof(f1497,plain,
! [X0,X1,X2] : multiply(X0,X1) = double_divide(double_divide(double_divide(inverse(X2),double_divide(identity,X1)),X0),multiply(identity,X2)),
inference(forward_demodulation,[status(thm)],[f25,f1496]) ).
fof(f1521,plain,
! [X0,X1] : inverse(double_divide(X0,double_divide(identity,inverse(X1)))) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f8,f901]) ).
fof(f1524,plain,
! [X0,X1] : multiply(double_divide(identity,inverse(X0)),X1) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f25,f1521]) ).
fof(f1525,plain,
! [X0,X1] : double_divide(X0,X1) = inverse(multiply(X1,X0)),
inference(backward_demodulation,[status(thm)],[f969,f32]) ).
fof(f1535,plain,
! [X0] : multiply(X0,identity) = X0,
inference(backward_demodulation,[status(thm)],[f969,f1041]) ).
fof(f1536,plain,
! [X0] : inverse(multiply(X0,identity)) = inverse(X0),
inference(backward_demodulation,[status(thm)],[f969,f761]) ).
fof(f1552,plain,
! [X0,X1,X2] : multiply(X0,X1) = double_divide(double_divide(double_divide(inverse(X2),double_divide(identity,X1)),X0),X2),
inference(backward_demodulation,[status(thm)],[f969,f1497]) ).
fof(f1618,plain,
! [X0,X1] : X0 = double_divide(double_divide(X1,X0),X1),
inference(backward_demodulation,[status(thm)],[f1535,f1151]) ).
fof(f1619,plain,
! [X0,X1] : multiply(inverse(X0),X1) = inverse(multiply(double_divide(identity,X1),X0)),
inference(backward_demodulation,[status(thm)],[f1642,f978]) ).
fof(f1623,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),X1) = multiply(X1,X0),
inference(backward_demodulation,[status(thm)],[f1642,f1524]) ).
fof(f1642,plain,
! [X0] : double_divide(identity,X0) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f1525,f1536]) ).
fof(f1665,plain,
! [X0,X1,X2] : multiply(X0,X1) = double_divide(double_divide(double_divide(inverse(X2),inverse(X1)),X0),X2),
inference(forward_demodulation,[status(thm)],[f1642,f1552]) ).
fof(f1686,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(X0,double_divide(identity,X1)),
inference(forward_demodulation,[status(thm)],[f1525,f1619]) ).
fof(f1690,plain,
! [X0,X1] : multiply(inverse(X0),X1) = double_divide(X0,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1642,f1686]) ).
fof(f1697,plain,
! [X0,X1,X2] : multiply(X0,X1) = double_divide(double_divide(multiply(X1,X2),X0),X2),
inference(backward_demodulation,[status(thm)],[f1700,f1665]) ).
fof(f1700,plain,
! [X0,X1] : double_divide(inverse(X0),inverse(X1)) = multiply(X1,X0),
inference(forward_demodulation,[status(thm)],[f1690,f1623]) ).
fof(f2009,plain,
! [X0,X1] : X0 = double_divide(X1,double_divide(X0,X1)),
inference(paramodulation,[status(thm)],[f1618,f1618]) ).
fof(f2040,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X1) = double_divide(inverse(X0),identity),
inference(paramodulation,[status(thm)],[f760,f2009]) ).
fof(f2057,plain,
! [X0,X1] : multiply(double_divide(X0,X1),X1) = inverse(X0),
inference(paramodulation,[status(thm)],[f2009,f25]) ).
fof(f2059,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X1) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f8,f2040]) ).
fof(f2067,plain,
! [X0,X1] : double_divide(double_divide(X0,X1),X1) = X0,
inference(forward_demodulation,[status(thm)],[f970,f2059]) ).
fof(f2110,plain,
! [X0,X1] : double_divide(X0,X1) = double_divide(X1,X0),
inference(paramodulation,[status(thm)],[f1618,f2067]) ).
fof(f2329,plain,
! [X0,X1] : multiply(X0,X1) = inverse(double_divide(X0,X1)),
inference(paramodulation,[status(thm)],[f2110,f25]) ).
fof(f2924,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(paramodulation,[status(thm)],[f25,f2329]) ).
fof(f2942,plain,
( sQ3_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f22,f2924]) ).
fof(f2950,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2942]) ).
fof(f3087,plain,
( sQ2_spl
| multiply(multiply(a3,b3),c3) != multiply(multiply(b3,c3),a3) ),
inference(paramodulation,[status(thm)],[f2924,f19]) ).
fof(f4590,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = inverse(double_divide(multiply(X1,X2),X0)),
inference(paramodulation,[status(thm)],[f1697,f2057]) ).
fof(f4645,plain,
( sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f3087,f4646]) ).
fof(f4646,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(multiply(X1,X2),X0),
inference(forward_demodulation,[status(thm)],[f2329,f4590]) ).
fof(f4663,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f4645]) ).
fof(f4666,plain,
( sQ0_spl
| double_divide(a1,inverse(a1)) != identity ),
inference(forward_demodulation,[status(thm)],[f1690,f13]) ).
fof(f4667,plain,
( sQ0_spl
| identity != identity ),
inference(forward_demodulation,[status(thm)],[f9,f4666]) ).
fof(f4668,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4667]) ).
fof(f4669,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f4668]) ).
fof(f4670,plain,
( sQ1_spl
| a2 != a2 ),
inference(forward_demodulation,[status(thm)],[f969,f16]) ).
fof(f4671,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4670]) ).
fof(f4672,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f4671]) ).
fof(f4673,plain,
$false,
inference(sat_refutation,[status(thm)],[f23,f2950,f4663,f4669,f4672]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP102-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/10.37 % Computer : n004.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.37 % CPULimit : 300
% 0.08/10.37 % WCLimit : 300
% 0.08/10.37 % DateTime : Sun Sep 20 19:57:31 UTC 2026
% 0.08/10.37 % CPUTime :
% 0.08/10.38 % Drodi V4.1.1
% 0.13/10.50 % Refutation found
% 0.13/10.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/10.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/10.52 % Elapsed time: 0.140916 seconds
% 0.13/10.52 % CPU time: 0.877327 seconds
% 0.13/10.52 % Total memory used: 88.956 MB
% 0.13/10.52 % Net memory used: 86.580 MB
%------------------------------------------------------------------------------