%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:13 PM UTC 2026
% Result : Unsatisfiable 10.18s 2.06s
% Output : CNFRefutation 6.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 19
% Syntax : Number of formulae : 198 ( 198 unt; 2 def)
% Number of atoms : 198 ( 197 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-4 aty)
% Number of variables : 278 ( 278 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : ifeq2(A,A,B,C) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : ifeq(A,A,B,C) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : product(identity,X,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : product(X,identity,X) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : product(inverse(X),X,identity) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] : product(X,inverse(X),identity) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y] : product(X,Y,multiply(X,Y)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y,W,Z] : ifeq2(product(X,Y,W),true,ifeq2(product(X,Y,Z),true,Z,W),W) = W,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [U,Z,W,Y,V,X] : ifeq(product(U,Z,W),true,ifeq(product(Y,Z,V),true,ifeq(product(X,Y,U),true,product(X,V,W),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,Z,V,X,W,U] : ifeq(product(Y,Z,V),true,ifeq(product(X,V,W),true,ifeq(product(X,Y,U),true,product(U,Z,W),true),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
! [X,Y] : ifeq(product(X,X,Y),true,product(X,Y,identity),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
product(a,b,c) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
product(c,inverse(a),d) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
product(d,inverse(b),h) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
product(h,b,j) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
product(j,inverse(h),k) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
product(k,inverse(b),identity) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,plain,
! [X0,X1,X2] : ifeq2(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1,X2] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f21,plain,
! [X0] : product(identity,X0,X0) = true,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f22,plain,
! [X0] : product(X0,identity,X0) = true,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
! [X0] : product(inverse(X0),X0,identity) = true,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f24,plain,
! [X0] : product(X0,inverse(X0),identity) = true,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0,X1] : product(X0,X1,multiply(X0,X1)) = true,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0,X1,X2,X3] : ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2) = X2,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
! [X0,X1,X2,X3,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X3,X0),true,product(X5,X4,X2),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0,X1,X2,X3,X4,X5] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X2,X4),true,ifeq(product(X3,X0,X5),true,product(X5,X1,X4),true),true),true) = true,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f29,plain,
! [X0,X1] : ifeq(product(X0,X0,X1),true,product(X0,X1,identity),true) = true,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f31,plain,
product(a,b,c) = true,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f32,plain,
product(c,inverse(a),d) = true,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f33,plain,
product(d,inverse(b),h) = true,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
product(h,b,j) = true,
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f35,plain,
product(j,inverse(h),k) = true,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f36,plain,
product(k,inverse(b),identity) != true,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f37,definition,
sF1_fnc = inverse(b),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f38,definition,
sF0_fnc = product(k,sF1_fnc,identity),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f39,plain,
sF0_fnc != true,
inference(definition_folding,[],[f36,f38,f37]) ).
fof(f40,plain,
product(d,sF1_fnc,h) = true,
inference(forward_demodulation,[status(thm)],[f37,f33]) ).
fof(f44,plain,
product(b,sF1_fnc,identity) = true,
inference(paramodulation,[status(thm)],[f37,f24]) ).
fof(f79,plain,
! [X0] : ifeq(true,true,product(X0,multiply(X0,X0),identity),true) = true,
inference(paramodulation,[status(thm)],[f25,f29]) ).
fof(f81,plain,
! [X0] : product(X0,multiply(X0,X0),identity) = true,
inference(forward_demodulation,[status(thm)],[f20,f79]) ).
fof(f102,plain,
! [X0,X1] : ifeq2(true,true,ifeq2(product(X0,identity,X1),true,X1,X0),X0) = X0,
inference(paramodulation,[status(thm)],[f22,f26]) ).
fof(f103,plain,
! [X0,X1,X2] : ifeq2(true,true,ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)),multiply(X0,X1)) = multiply(X0,X1),
inference(paramodulation,[status(thm)],[f25,f26]) ).
fof(f110,plain,
! [X0] : ifeq2(product(d,sF1_fnc,X0),true,ifeq2(true,true,h,X0),X0) = X0,
inference(paramodulation,[status(thm)],[f40,f26]) ).
fof(f113,plain,
! [X0] : ifeq2(product(h,b,X0),true,ifeq2(true,true,j,X0),X0) = X0,
inference(paramodulation,[status(thm)],[f34,f26]) ).
fof(f117,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,ifeq2(true,true,X0,X1),X1) = X1,
inference(paramodulation,[status(thm)],[f22,f26]) ).
fof(f118,plain,
! [X0,X1,X2] : ifeq2(product(X0,X1,X2),true,ifeq2(true,true,multiply(X0,X1),X2),X2) = X2,
inference(paramodulation,[status(thm)],[f25,f26]) ).
fof(f131,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,X1,X0) = X0,
inference(forward_demodulation,[status(thm)],[f19,f102]) ).
fof(f132,plain,
! [X0,X1,X2] : ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)) = multiply(X0,X1),
inference(forward_demodulation,[status(thm)],[f19,f103]) ).
fof(f139,plain,
! [X0] : ifeq2(product(d,sF1_fnc,X0),true,h,X0) = X0,
inference(forward_demodulation,[status(thm)],[f19,f110]) ).
fof(f141,plain,
! [X0] : ifeq2(product(h,b,X0),true,j,X0) = X0,
inference(forward_demodulation,[status(thm)],[f19,f113]) ).
fof(f145,plain,
! [X0,X1] : ifeq2(product(X0,identity,X1),true,X0,X1) = X1,
inference(forward_demodulation,[status(thm)],[f19,f117]) ).
fof(f146,plain,
! [X0,X1,X2] : ifeq2(product(X0,X1,X2),true,multiply(X0,X1),X2) = X2,
inference(forward_demodulation,[status(thm)],[f19,f118]) ).
fof(f148,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(product(X0,inverse(h),X1),true,ifeq(product(X2,X0,j),true,product(X2,X1,k),true),true),true) = true,
inference(paramodulation,[status(thm)],[f35,f27]) ).
fof(f152,plain,
! [X0,X1,X2,X3] : ifeq(true,true,ifeq(product(X0,X1,X2),true,ifeq(product(X3,X0,identity),true,product(X3,X2,X1),true),true),true) = true,
inference(paramodulation,[status(thm)],[f21,f27]) ).
fof(f153,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(product(X0,sF1_fnc,X1),true,ifeq(product(X2,X0,d),true,product(X2,X1,h),true),true),true) = true,
inference(paramodulation,[status(thm)],[f40,f27]) ).
fof(f154,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(product(X0,inverse(a),X1),true,ifeq(product(X2,X0,c),true,product(X2,X1,d),true),true),true) = true,
inference(paramodulation,[status(thm)],[f32,f27]) ).
fof(f161,plain,
! [X0,X1,X2,X3,X4] : ifeq(true,true,ifeq(product(X0,X1,X2),true,ifeq(product(X3,X0,X4),true,product(X3,X2,multiply(X4,X1)),true),true),true) = true,
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f210,plain,
! [X0,X1,X2] : ifeq(product(X0,inverse(h),X1),true,ifeq(product(X2,X0,j),true,product(X2,X1,k),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f148]) ).
fof(f214,plain,
! [X0,X1,X2,X3] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X0,identity),true,product(X3,X2,X1),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f152]) ).
fof(f215,plain,
! [X0,X1,X2] : ifeq(product(X0,sF1_fnc,X1),true,ifeq(product(X2,X0,d),true,product(X2,X1,h),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f153]) ).
fof(f216,plain,
! [X0,X1,X2] : ifeq(product(X0,inverse(a),X1),true,ifeq(product(X2,X0,c),true,product(X2,X1,d),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f154]) ).
fof(f222,plain,
! [X0,X1,X2,X3,X4] : ifeq(product(X0,X1,X2),true,ifeq(product(X3,X0,X4),true,product(X3,X2,multiply(X4,X1)),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f161]) ).
fof(f256,plain,
! [X0,X1,X2,X3] : ifeq(true,true,ifeq(product(X0,identity,X1),true,ifeq(product(X0,inverse(X2),X3),true,product(X3,X2,X1),true),true),true) = true,
inference(paramodulation,[status(thm)],[f23,f28]) ).
fof(f319,plain,
! [X0,X1,X2,X3] : ifeq(product(X0,identity,X1),true,ifeq(product(X0,inverse(X2),X3),true,product(X3,X2,X1),true),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f256]) ).
fof(f368,plain,
ifeq2(true,true,h,multiply(d,sF1_fnc)) = multiply(d,sF1_fnc),
inference(paramodulation,[status(thm)],[f25,f139]) ).
fof(f370,plain,
h = multiply(d,sF1_fnc),
inference(forward_demodulation,[status(thm)],[f19,f368]) ).
fof(f406,plain,
! [X0] : ifeq2(true,true,multiply(X0,identity),X0) = X0,
inference(paramodulation,[status(thm)],[f25,f131]) ).
fof(f411,plain,
! [X0] : multiply(X0,identity) = X0,
inference(forward_demodulation,[status(thm)],[f19,f406]) ).
fof(f463,plain,
ifeq2(true,true,j,multiply(h,b)) = multiply(h,b),
inference(paramodulation,[status(thm)],[f25,f141]) ).
fof(f465,plain,
j = multiply(h,b),
inference(forward_demodulation,[status(thm)],[f19,f463]) ).
fof(f512,plain,
! [X0] : ifeq2(true,true,multiply(X0,multiply(X0,X0)),identity) = identity,
inference(paramodulation,[status(thm)],[f81,f146]) ).
fof(f537,plain,
! [X0] : multiply(X0,multiply(X0,X0)) = identity,
inference(forward_demodulation,[status(thm)],[f19,f512]) ).
fof(f754,plain,
! [X0,X1] : ifeq(true,true,ifeq(product(X0,X1,j),true,product(X0,multiply(X1,inverse(h)),k),true),true) = true,
inference(paramodulation,[status(thm)],[f25,f210]) ).
fof(f768,plain,
! [X0,X1] : ifeq(product(X0,X1,j),true,product(X0,multiply(X1,inverse(h)),k),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f754]) ).
fof(f963,plain,
! [X0,X1] : ifeq(product(sF1_fnc,X0,X1),true,ifeq(true,true,product(b,X1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f44,f214]) ).
fof(f965,plain,
! [X0,X1,X2] : ifeq(product(X0,X1,X2),true,ifeq(true,true,product(inverse(X0),X2,X1),true),true) = true,
inference(paramodulation,[status(thm)],[f23,f214]) ).
fof(f1004,plain,
! [X0,X1] : ifeq(product(sF1_fnc,X0,X1),true,product(b,X1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f963]) ).
fof(f1006,plain,
! [X0,X1,X2] : ifeq(product(X0,X1,X2),true,product(inverse(X0),X2,X1),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f965]) ).
fof(f1019,plain,
! [X0,X1] : ifeq(true,true,ifeq(product(X0,X1,d),true,product(X0,multiply(X1,sF1_fnc),h),true),true) = true,
inference(paramodulation,[status(thm)],[f25,f215]) ).
fof(f1033,plain,
! [X0,X1] : ifeq(product(X0,X1,d),true,product(X0,multiply(X1,sF1_fnc),h),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f1019]) ).
fof(f1043,plain,
! [X0,X1] : ifeq(true,true,ifeq(product(X0,X1,c),true,product(X0,multiply(X1,inverse(a)),d),true),true) = true,
inference(paramodulation,[status(thm)],[f25,f216]) ).
fof(f1057,plain,
! [X0,X1] : ifeq(product(X0,X1,c),true,product(X0,multiply(X1,inverse(a)),d),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f1043]) ).
fof(f1064,plain,
ifeq(true,true,product(b,identity,inverse(sF1_fnc)),true) = true,
inference(paramodulation,[status(thm)],[f24,f1004]) ).
fof(f1075,plain,
product(b,identity,inverse(sF1_fnc)) = true,
inference(forward_demodulation,[status(thm)],[f20,f1064]) ).
fof(f1085,plain,
ifeq2(true,true,b,inverse(sF1_fnc)) = inverse(sF1_fnc),
inference(paramodulation,[status(thm)],[f1075,f145]) ).
fof(f1105,plain,
b = inverse(sF1_fnc),
inference(forward_demodulation,[status(thm)],[f19,f1085]) ).
fof(f1658,plain,
! [X0,X1] : ifeq(true,true,ifeq(product(X0,a,X1),true,product(X0,c,multiply(X1,b)),true),true) = true,
inference(paramodulation,[status(thm)],[f31,f222]) ).
fof(f1662,plain,
! [X0,X1,X2,X3] : ifeq(true,true,ifeq(product(X0,X1,X2),true,product(X0,multiply(X1,X3),multiply(X2,X3)),true),true) = true,
inference(paramodulation,[status(thm)],[f25,f222]) ).
fof(f1715,plain,
! [X0,X1] : ifeq(product(X0,a,X1),true,product(X0,c,multiply(X1,b)),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f1658]) ).
fof(f1720,plain,
! [X0,X1,X2,X3] : ifeq(product(X0,X1,X2),true,product(X0,multiply(X1,X3),multiply(X2,X3)),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f1662]) ).
fof(f2106,plain,
! [X0] : ifeq(true,true,product(inverse(inverse(X0)),identity,X0),true) = true,
inference(paramodulation,[status(thm)],[f23,f1006]) ).
fof(f2116,plain,
! [X0,X1] : ifeq(true,true,product(inverse(X0),multiply(X0,X1),X1),true) = true,
inference(paramodulation,[status(thm)],[f25,f1006]) ).
fof(f2140,plain,
! [X0] : product(inverse(inverse(X0)),identity,X0) = true,
inference(forward_demodulation,[status(thm)],[f20,f2106]) ).
fof(f2150,plain,
! [X0,X1] : product(inverse(X0),multiply(X0,X1),X1) = true,
inference(forward_demodulation,[status(thm)],[f20,f2116]) ).
fof(f2327,plain,
! [X0] : ifeq2(true,true,inverse(inverse(X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f2140,f145]) ).
fof(f2390,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f19,f2327]) ).
fof(f2690,plain,
! [X0,X1] : ifeq2(true,true,X0,multiply(inverse(X1),multiply(X1,X0))) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f2150,f132]) ).
fof(f2748,plain,
! [X0,X1] : X0 = multiply(inverse(X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f19,f2690]) ).
fof(f2758,plain,
! [X0,X1] : X0 = multiply(X1,multiply(inverse(X1),X0)),
inference(paramodulation,[status(thm)],[f2390,f2748]) ).
fof(f2780,plain,
! [X0] : multiply(X0,X0) = multiply(inverse(X0),identity),
inference(paramodulation,[status(thm)],[f537,f2748]) ).
fof(f2799,plain,
! [X0] : multiply(X0,X0) = inverse(X0),
inference(forward_demodulation,[status(thm)],[f411,f2780]) ).
fof(f2857,plain,
! [X0] : product(X0,X0,inverse(X0)) = true,
inference(paramodulation,[status(thm)],[f2799,f25]) ).
fof(f6121,plain,
! [X0,X1,X2] : ifeq(true,true,ifeq(product(X0,inverse(X1),X2),true,product(X2,X1,X0),true),true) = true,
inference(paramodulation,[status(thm)],[f22,f319]) ).
fof(f6176,plain,
! [X0,X1,X2] : ifeq(product(X0,inverse(X1),X2),true,product(X2,X1,X0),true) = true,
inference(forward_demodulation,[status(thm)],[f20,f6121]) ).
fof(f6448,plain,
! [X0,X1] : ifeq(true,true,product(multiply(X0,inverse(X1)),X1,X0),true) = true,
inference(paramodulation,[status(thm)],[f25,f6176]) ).
fof(f6471,plain,
ifeq(product(identity,inverse(sF1_fnc),k),true,sF0_fnc,true) = true,
inference(paramodulation,[status(thm)],[f38,f6176]) ).
fof(f6507,plain,
! [X0,X1] : product(multiply(X0,inverse(X1)),X1,X0) = true,
inference(forward_demodulation,[status(thm)],[f20,f6448]) ).
fof(f6508,plain,
ifeq(product(identity,b,k),true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f1105,f6471]) ).
fof(f6970,plain,
! [X0,X1] : product(multiply(X0,X1),inverse(X1),X0) = true,
inference(paramodulation,[status(thm)],[f2390,f6507]) ).
fof(f7101,plain,
! [X0,X1] : ifeq2(true,true,X0,multiply(multiply(X0,inverse(X1)),X1)) = multiply(multiply(X0,inverse(X1)),X1),
inference(paramodulation,[status(thm)],[f6507,f132]) ).
fof(f7278,plain,
! [X0,X1] : X0 = multiply(multiply(X0,inverse(X1)),X1),
inference(forward_demodulation,[status(thm)],[f19,f7101]) ).
fof(f7300,plain,
! [X0,X1] : X0 = multiply(multiply(X0,X1),inverse(X1)),
inference(paramodulation,[status(thm)],[f2390,f7278]) ).
fof(f7301,plain,
! [X0] : X0 = multiply(multiply(X0,b),sF1_fnc),
inference(paramodulation,[status(thm)],[f1105,f7278]) ).
fof(f7303,plain,
! [X0] : X0 = multiply(multiply(X0,sF1_fnc),b),
inference(paramodulation,[status(thm)],[f37,f7278]) ).
fof(f7310,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(X1,inverse(X0))),X1),
inference(paramodulation,[status(thm)],[f7278,f2748]) ).
fof(f7336,plain,
! [X0,X1] : inverse(X0) = multiply(X1,inverse(multiply(X0,X1))),
inference(paramodulation,[status(thm)],[f2748,f7300]) ).
fof(f7341,plain,
d = multiply(h,inverse(sF1_fnc)),
inference(paramodulation,[status(thm)],[f370,f7300]) ).
fof(f7360,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(multiply(X1,X0)),X1),
inference(paramodulation,[status(thm)],[f7300,f2748]) ).
fof(f7370,plain,
d = multiply(h,b),
inference(forward_demodulation,[status(thm)],[f1105,f7341]) ).
fof(f7371,plain,
d = j,
inference(forward_demodulation,[status(thm)],[f465,f7370]) ).
fof(f9322,plain,
! [X0] : inverse(multiply(sF1_fnc,inverse(X0))) = multiply(X0,b),
inference(paramodulation,[status(thm)],[f7310,f7303]) ).
fof(f9489,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
inference(paramodulation,[status(thm)],[f7300,f7336]) ).
fof(f9961,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(paramodulation,[status(thm)],[f2758,f7360]) ).
fof(f14207,plain,
! [X0,X1] : product(multiply(X0,multiply(sF1_fnc,inverse(X1))),multiply(X1,b),X0) = true,
inference(paramodulation,[status(thm)],[f9322,f6970]) ).
fof(f14209,plain,
! [X0,X1] : X0 = multiply(multiply(X0,multiply(sF1_fnc,inverse(X1))),multiply(X1,b)),
inference(paramodulation,[status(thm)],[f9322,f7300]) ).
fof(f16680,plain,
! [X0,X1,X2] : X0 = multiply(multiply(X0,multiply(inverse(X1),X2)),multiply(inverse(X2),X1)),
inference(paramodulation,[status(thm)],[f9961,f7300]) ).
fof(f31462,plain,
! [X0,X1] : ifeq(product(X0,X1,d),true,product(X0,multiply(X1,inverse(h)),k),true) = true,
inference(forward_demodulation,[status(thm)],[f7371,f768]) ).
fof(f31475,plain,
! [X0] : ifeq(true,true,product(multiply(d,X0),multiply(inverse(X0),inverse(h)),k),true) = true,
inference(paramodulation,[status(thm)],[f6970,f31462]) ).
fof(f31520,plain,
! [X0] : product(multiply(d,X0),multiply(inverse(X0),inverse(h)),k) = true,
inference(forward_demodulation,[status(thm)],[f20,f31475]) ).
fof(f31521,plain,
! [X0] : product(multiply(d,X0),inverse(multiply(h,X0)),k) = true,
inference(forward_demodulation,[status(thm)],[f9489,f31520]) ).
fof(f34115,plain,
! [X0] : ifeq(true,true,product(k,multiply(h,X0),multiply(d,X0)),true) = true,
inference(paramodulation,[status(thm)],[f31521,f6176]) ).
fof(f34212,plain,
! [X0] : product(k,multiply(h,X0),multiply(d,X0)) = true,
inference(forward_demodulation,[status(thm)],[f20,f34115]) ).
fof(f34691,plain,
! [X0] : ifeq2(true,true,multiply(d,X0),multiply(k,multiply(h,X0))) = multiply(k,multiply(h,X0)),
inference(paramodulation,[status(thm)],[f34212,f132]) ).
fof(f34771,plain,
! [X0] : multiply(d,X0) = multiply(k,multiply(h,X0)),
inference(forward_demodulation,[status(thm)],[f19,f34691]) ).
fof(f34790,plain,
! [X0] : multiply(d,multiply(inverse(h),X0)) = multiply(k,X0),
inference(paramodulation,[status(thm)],[f2758,f34771]) ).
fof(f37627,plain,
! [X0] : d = multiply(multiply(k,X0),multiply(inverse(X0),h)),
inference(paramodulation,[status(thm)],[f34790,f16680]) ).
fof(f39805,plain,
! [X0] : d = multiply(X0,multiply(inverse(multiply(inverse(k),X0)),h)),
inference(paramodulation,[status(thm)],[f2758,f37627]) ).
fof(f39867,plain,
! [X0] : d = multiply(X0,multiply(multiply(inverse(X0),k),h)),
inference(forward_demodulation,[status(thm)],[f9961,f39805]) ).
fof(f40476,plain,
! [X0] : multiply(multiply(inverse(inverse(X0)),k),h) = multiply(X0,d),
inference(paramodulation,[status(thm)],[f39867,f2758]) ).
fof(f40588,plain,
! [X0] : multiply(multiply(X0,k),h) = multiply(X0,d),
inference(forward_demodulation,[status(thm)],[f2390,f40476]) ).
fof(f40661,plain,
! [X0] : multiply(X0,k) = multiply(multiply(X0,d),inverse(h)),
inference(paramodulation,[status(thm)],[f40588,f7300]) ).
fof(f47659,plain,
! [X0] : ifeq(true,true,product(multiply(d,multiply(sF1_fnc,inverse(X0))),multiply(multiply(X0,b),sF1_fnc),h),true) = true,
inference(paramodulation,[status(thm)],[f14207,f1033]) ).
fof(f47704,plain,
! [X0] : product(multiply(d,multiply(sF1_fnc,inverse(X0))),multiply(multiply(X0,b),sF1_fnc),h) = true,
inference(forward_demodulation,[status(thm)],[f20,f47659]) ).
fof(f47705,plain,
! [X0] : product(multiply(d,multiply(sF1_fnc,inverse(X0))),X0,h) = true,
inference(forward_demodulation,[status(thm)],[f7301,f47704]) ).
fof(f50195,plain,
! [X0] : ifeq(true,true,product(multiply(c,X0),multiply(inverse(X0),inverse(a)),d),true) = true,
inference(paramodulation,[status(thm)],[f6970,f1057]) ).
fof(f50242,plain,
! [X0] : product(multiply(c,X0),multiply(inverse(X0),inverse(a)),d) = true,
inference(forward_demodulation,[status(thm)],[f20,f50195]) ).
fof(f50243,plain,
! [X0] : product(multiply(c,X0),inverse(multiply(a,X0)),d) = true,
inference(forward_demodulation,[status(thm)],[f9489,f50242]) ).
fof(f54097,plain,
! [X0] : ifeq(true,true,product(h,X0,multiply(d,multiply(sF1_fnc,inverse(inverse(X0))))),true) = true,
inference(paramodulation,[status(thm)],[f47705,f6176]) ).
fof(f54351,plain,
! [X0] : product(h,X0,multiply(d,multiply(sF1_fnc,inverse(inverse(X0))))) = true,
inference(forward_demodulation,[status(thm)],[f20,f54097]) ).
fof(f54352,plain,
! [X0] : product(h,X0,multiply(d,multiply(sF1_fnc,X0))) = true,
inference(forward_demodulation,[status(thm)],[f2390,f54351]) ).
fof(f54940,plain,
! [X0] : ifeq2(true,true,multiply(d,multiply(sF1_fnc,X0)),multiply(h,X0)) = multiply(h,X0),
inference(paramodulation,[status(thm)],[f54352,f132]) ).
fof(f55222,plain,
! [X0] : multiply(d,multiply(sF1_fnc,X0)) = multiply(h,X0),
inference(forward_demodulation,[status(thm)],[f19,f54940]) ).
fof(f55507,plain,
! [X0] : d = multiply(multiply(h,inverse(X0)),multiply(X0,b)),
inference(paramodulation,[status(thm)],[f55222,f14209]) ).
fof(f59075,plain,
! [X0] : d = multiply(inverse(X0),multiply(multiply(X0,h),b)),
inference(paramodulation,[status(thm)],[f7336,f55507]) ).
fof(f63298,plain,
! [X0] : multiply(multiply(X0,h),b) = multiply(X0,d),
inference(paramodulation,[status(thm)],[f59075,f2758]) ).
fof(f63441,plain,
! [X0] : inverse(b) = multiply(inverse(multiply(X0,d)),multiply(X0,h)),
inference(paramodulation,[status(thm)],[f63298,f7360]) ).
fof(f63469,plain,
! [X0] : sF1_fnc = multiply(inverse(multiply(X0,d)),multiply(X0,h)),
inference(forward_demodulation,[status(thm)],[f37,f63441]) ).
fof(f69079,plain,
! [X0] : ifeq(true,true,product(d,multiply(a,X0),multiply(c,X0)),true) = true,
inference(paramodulation,[status(thm)],[f50243,f6176]) ).
fof(f69148,plain,
! [X0] : ifeq2(true,true,d,multiply(multiply(c,X0),inverse(multiply(a,X0)))) = multiply(multiply(c,X0),inverse(multiply(a,X0))),
inference(paramodulation,[status(thm)],[f50243,f132]) ).
fof(f69197,plain,
! [X0] : product(d,multiply(a,X0),multiply(c,X0)) = true,
inference(forward_demodulation,[status(thm)],[f20,f69079]) ).
fof(f69269,plain,
! [X0] : d = multiply(multiply(c,X0),inverse(multiply(a,X0))),
inference(forward_demodulation,[status(thm)],[f19,f69148]) ).
fof(f69711,plain,
! [X0] : ifeq2(true,true,multiply(c,X0),multiply(d,multiply(a,X0))) = multiply(d,multiply(a,X0)),
inference(paramodulation,[status(thm)],[f69197,f132]) ).
fof(f69806,plain,
! [X0] : multiply(c,X0) = multiply(d,multiply(a,X0)),
inference(forward_demodulation,[status(thm)],[f19,f69711]) ).
fof(f69827,plain,
! [X0] : multiply(c,multiply(inverse(a),X0)) = multiply(d,X0),
inference(paramodulation,[status(thm)],[f2758,f69806]) ).
fof(f69905,plain,
d = multiply(inverse(c),inverse(multiply(a,c))),
inference(paramodulation,[status(thm)],[f2799,f69269]) ).
fof(f69985,plain,
d = inverse(multiply(multiply(a,c),c)),
inference(forward_demodulation,[status(thm)],[f9489,f69905]) ).
fof(f70040,plain,
inverse(multiply(a,c)) = multiply(c,d),
inference(paramodulation,[status(thm)],[f69985,f7336]) ).
fof(f70346,plain,
inverse(multiply(c,d)) = multiply(a,c),
inference(paramodulation,[status(thm)],[f70040,f2390]) ).
fof(f70515,plain,
sF1_fnc = multiply(multiply(a,c),multiply(c,h)),
inference(paramodulation,[status(thm)],[f70346,f63469]) ).
fof(f71628,plain,
! [X0] : c = multiply(multiply(d,X0),multiply(inverse(X0),a)),
inference(paramodulation,[status(thm)],[f69827,f16680]) ).
fof(f74057,plain,
! [X0] : c = multiply(X0,multiply(inverse(multiply(inverse(d),X0)),a)),
inference(paramodulation,[status(thm)],[f2758,f71628]) ).
fof(f74143,plain,
! [X0] : c = multiply(X0,multiply(multiply(inverse(X0),d),a)),
inference(forward_demodulation,[status(thm)],[f9961,f74057]) ).
fof(f74780,plain,
! [X0] : multiply(multiply(inverse(inverse(X0)),d),a) = multiply(X0,c),
inference(paramodulation,[status(thm)],[f74143,f2758]) ).
fof(f74962,plain,
! [X0] : multiply(multiply(X0,d),a) = multiply(X0,c),
inference(forward_demodulation,[status(thm)],[f2390,f74780]) ).
fof(f75080,plain,
! [X0] : multiply(X0,d) = multiply(multiply(X0,c),inverse(a)),
inference(paramodulation,[status(thm)],[f74962,f7300]) ).
fof(f75196,plain,
ifeq(true,true,product(a,c,multiply(inverse(a),b)),true) = true,
inference(paramodulation,[status(thm)],[f2857,f1715]) ).
fof(f75241,plain,
product(a,c,multiply(inverse(a),b)) = true,
inference(forward_demodulation,[status(thm)],[f20,f75196]) ).
fof(f76634,plain,
ifeq2(true,true,multiply(inverse(a),b),multiply(a,c)) = multiply(a,c),
inference(paramodulation,[status(thm)],[f75241,f132]) ).
fof(f76715,plain,
multiply(inverse(a),b) = multiply(a,c),
inference(forward_demodulation,[status(thm)],[f19,f76634]) ).
fof(f76752,plain,
b = multiply(a,multiply(a,c)),
inference(paramodulation,[status(thm)],[f76715,f2758]) ).
fof(f76775,plain,
inverse(a) = multiply(multiply(a,c),sF1_fnc),
inference(paramodulation,[status(thm)],[f76715,f7301]) ).
fof(f77217,plain,
! [X0,X1] : ifeq(true,true,product(X0,multiply(X0,X1),multiply(inverse(X0),X1)),true) = true,
inference(paramodulation,[status(thm)],[f2857,f1720]) ).
fof(f77861,plain,
! [X0,X1] : product(X0,multiply(X0,X1),multiply(inverse(X0),X1)) = true,
inference(forward_demodulation,[status(thm)],[f20,f77217]) ).
fof(f79846,plain,
! [X0,X1] : product(X0,multiply(X0,multiply(X0,X1)),X1) = true,
inference(paramodulation,[status(thm)],[f2748,f77861]) ).
fof(f81111,plain,
! [X0,X1] : ifeq2(true,true,X0,multiply(X1,multiply(X1,multiply(X1,X0)))) = multiply(X1,multiply(X1,multiply(X1,X0))),
inference(paramodulation,[status(thm)],[f79846,f132]) ).
fof(f81499,plain,
! [X0,X1] : X0 = multiply(X1,multiply(X1,multiply(X1,X0))),
inference(forward_demodulation,[status(thm)],[f19,f81111]) ).
fof(f81553,plain,
multiply(c,h) = multiply(multiply(a,c),multiply(multiply(a,c),sF1_fnc)),
inference(paramodulation,[status(thm)],[f70515,f81499]) ).
fof(f81918,plain,
multiply(c,h) = multiply(multiply(a,c),inverse(a)),
inference(forward_demodulation,[status(thm)],[f76775,f81553]) ).
fof(f81919,plain,
multiply(c,h) = multiply(a,d),
inference(forward_demodulation,[status(thm)],[f75080,f81918]) ).
fof(f82128,plain,
c = multiply(multiply(a,d),inverse(h)),
inference(paramodulation,[status(thm)],[f81919,f7300]) ).
fof(f82144,plain,
c = multiply(a,k),
inference(forward_demodulation,[status(thm)],[f40661,f82128]) ).
fof(f82156,plain,
k = multiply(a,multiply(a,c)),
inference(paramodulation,[status(thm)],[f82144,f81499]) ).
fof(f82193,plain,
k = b,
inference(forward_demodulation,[status(thm)],[f76752,f82156]) ).
fof(f82381,plain,
ifeq(product(identity,k,k),true,sF0_fnc,true) = true,
inference(backward_demodulation,[status(thm)],[f82193,f6508]) ).
fof(f82500,plain,
ifeq(true,true,sF0_fnc,true) = true,
inference(forward_demodulation,[status(thm)],[f21,f82381]) ).
fof(f82501,plain,
sF0_fnc = true,
inference(forward_demodulation,[status(thm)],[f20,f82500]) ).
fof(f82502,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f82501,f39]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n008.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 20 19:53:39 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.40 % Drodi V4.1.1
% 10.18/2.06 % Refutation found
% 10.18/2.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.18/2.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.40/2.29 % Elapsed time: 1.875223 seconds
% 1.40/2.29 % CPU time: 13.516436 seconds
% 1.40/2.29 % Total memory used: 223.796 MB
% 1.40/2.29 % Net memory used: 211.423 MB
%------------------------------------------------------------------------------