%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:35:24 PM UTC 2026
% Result : Unsatisfiable 22.98s 3.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP002-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 20 19:55:31 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 22.98/3.54 % Refutation found
% 22.98/3.54 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.98/3.54 % SZS output start CNFRefutation for theBenchmark
% 22.98/3.54 fof(f1,axiom,(
% 22.98/3.54 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f2,axiom,(
% 22.98/3.54 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f3,axiom,(
% 22.98/3.54 (![X]: (product(identity,X,X) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f4,axiom,(
% 22.98/3.54 (![X]: (product(X,identity,X) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f5,axiom,(
% 22.98/3.54 (![X]: (product(inverse(X),X,identity) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f6,axiom,(
% 22.98/3.54 (![X]: (product(X,inverse(X),identity) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f7,axiom,(
% 22.98/3.54 (![X,Y]: (product(X,Y,multiply(X,Y)) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f8,axiom,(
% 22.98/3.54 (![X,Y,W,Z]: (ifeq2(product(X,Y,W),true,ifeq2(product(X,Y,Z),true,Z,W),W) = W ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f9,axiom,(
% 22.98/3.54 (![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 ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f10,axiom,(
% 22.98/3.54 (![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 ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f11,hypothesis,(
% 22.98/3.54 (![X,Y]: (ifeq(product(X,X,Y),true,product(X,Y,identity),true) = true ))),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f13,negated_conjecture,(
% 22.98/3.54 product(a,b,c) = true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f14,negated_conjecture,(
% 22.98/3.54 product(c,inverse(a),d) = true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f15,negated_conjecture,(
% 22.98/3.54 product(d,inverse(b),h) = true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f16,negated_conjecture,(
% 22.98/3.54 product(h,b,j) = true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f17,negated_conjecture,(
% 22.98/3.54 product(j,inverse(h),k) = true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f18,negated_conjecture,(
% 22.98/3.54 product(k,inverse(b),identity) != true ),
% 22.98/3.54 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.54 fof(f19,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f1])).
% 22.98/3.54 fof(f20,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f2])).
% 22.98/3.54 fof(f21,plain,(
% 22.98/3.54 ![X0]: (product(identity,X0,X0)=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f3])).
% 22.98/3.54 fof(f22,plain,(
% 22.98/3.54 ![X0]: (product(X0,identity,X0)=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f4])).
% 22.98/3.54 fof(f23,plain,(
% 22.98/3.54 ![X0]: (product(inverse(X0),X0,identity)=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f5])).
% 22.98/3.54 fof(f24,plain,(
% 22.98/3.54 ![X0]: (product(X0,inverse(X0),identity)=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f6])).
% 22.98/3.54 fof(f25,plain,(
% 22.98/3.54 ![X0,X1]: (product(X0,X1,multiply(X0,X1))=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f7])).
% 22.98/3.54 fof(f26,plain,(
% 22.98/3.54 ![X0,X1,X2,X3]: (ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2)=X2)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f8])).
% 22.98/3.54 fof(f27,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f9])).
% 22.98/3.54 fof(f28,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f10])).
% 22.98/3.54 fof(f29,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(product(X0,X0,X1),true,product(X0,X1,identity),true)=true)),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f11])).
% 22.98/3.54 fof(f31,plain,(
% 22.98/3.54 product(a,b,c)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f13])).
% 22.98/3.54 fof(f32,plain,(
% 22.98/3.54 product(c,inverse(a),d)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f14])).
% 22.98/3.54 fof(f33,plain,(
% 22.98/3.54 product(d,inverse(b),h)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f15])).
% 22.98/3.54 fof(f34,plain,(
% 22.98/3.54 product(h,b,j)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f16])).
% 22.98/3.54 fof(f35,plain,(
% 22.98/3.54 product(j,inverse(h),k)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f17])).
% 22.98/3.54 fof(f36,plain,(
% 22.98/3.54 ~product(k,inverse(b),identity)=true),
% 22.98/3.54 inference(cnf_transformation,[status(thm)],[f18])).
% 22.98/3.54 fof(f45,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,ifeq2(product(h,b,X0),true,X0,j),j)=j)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f34,f26])).
% 22.98/3.54 fof(f50,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(true,true,ifeq2(product(X0,identity,X1),true,X1,X0),X0)=X0)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f22,f26])).
% 22.98/3.54 fof(f51,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq2(true,true,ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)),multiply(X0,X1))=multiply(X0,X1))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f26])).
% 22.98/3.54 fof(f56,plain,(
% 22.98/3.54 ![X0]: (ifeq2(product(a,b,X0),true,ifeq2(true,true,c,X0),X0)=X0)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f31,f26])).
% 22.98/3.54 fof(f60,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(product(X0,identity,X1),true,ifeq2(true,true,X0,X1),X1)=X1)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f22,f26])).
% 22.98/3.54 fof(f61,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,ifeq2(true,true,multiply(X0,X1),X2),X2)=X2)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f26])).
% 22.98/3.54 fof(f65,plain,(
% 22.98/3.54 ![X0]: (ifeq2(product(h,b,X0),true,X0,j)=j)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f45])).
% 22.98/3.54 fof(f70,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(product(X0,identity,X1),true,X1,X0)=X0)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f50])).
% 22.98/3.54 fof(f71,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1))=multiply(X0,X1))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f51])).
% 22.98/3.54 fof(f76,plain,(
% 22.98/3.54 ![X0]: (ifeq2(product(a,b,X0),true,c,X0)=X0)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f56])).
% 22.98/3.54 fof(f80,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(product(X0,identity,X1),true,X0,X1)=X1)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f60])).
% 22.98/3.54 fof(f81,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,multiply(X0,X1),X2)=X2)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f61])).
% 22.98/3.54 fof(f96,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,multiply(X0,identity),X0)=X0)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f70])).
% 22.98/3.54 fof(f100,plain,(
% 22.98/3.54 ![X0]: (multiply(X0,identity)=X0)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f96])).
% 22.98/3.54 fof(f115,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f35,f27])).
% 22.98/3.54 fof(f117,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f32,f27])).
% 22.98/3.54 fof(f121,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f21,f27])).
% 22.98/3.54 fof(f124,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f27])).
% 22.98/3.54 fof(f155,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(product(X0,inverse(h),X1),true,ifeq(product(X2,X0,j),true,product(X2,X1,k),true),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f115])).
% 22.98/3.54 fof(f157,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(product(X0,inverse(a),X1),true,ifeq(product(X2,X0,c),true,product(X2,X1,d),true),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f117])).
% 22.98/3.54 fof(f161,plain,(
% 22.98/3.54 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X0,identity),true,product(X3,X2,X1),true),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f121])).
% 22.98/3.54 fof(f164,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f124])).
% 22.98/3.54 fof(f204,plain,(
% 22.98/3.54 ifeq2(true,true,c,multiply(a,b))=multiply(a,b)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f76])).
% 22.98/3.54 fof(f206,plain,(
% 22.98/3.54 c=multiply(a,b)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f204])).
% 22.98/3.54 fof(f221,plain,(
% 22.98/3.54 ![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)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f23,f28])).
% 22.98/3.54 fof(f262,plain,(
% 22.98/3.54 ![X0,X1,X2,X3]: (ifeq(product(X0,identity,X1),true,ifeq(product(X0,inverse(X2),X3),true,product(X3,X2,X1),true),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f221])).
% 22.98/3.54 fof(f334,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(X0,multiply(X0,X0),identity),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f29])).
% 22.98/3.54 fof(f343,plain,(
% 22.98/3.54 ![X0]: (product(X0,multiply(X0,X0),identity)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f334])).
% 22.98/3.54 fof(f353,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,multiply(X0,multiply(X0,X0)),identity)=identity)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f343,f81])).
% 22.98/3.54 fof(f367,plain,(
% 22.98/3.54 ![X0]: (multiply(X0,multiply(X0,X0))=identity)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f353])).
% 22.98/3.54 fof(f671,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(true,true,ifeq(product(X0,X1,j),true,product(X0,multiply(X1,inverse(h)),k),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f155])).
% 22.98/3.54 fof(f685,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(product(X0,X1,j),true,product(X0,multiply(X1,inverse(h)),k),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f671])).
% 22.98/3.54 fof(f788,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(true,true,ifeq(product(X0,X1,c),true,product(X0,multiply(X1,inverse(a)),d),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f157])).
% 22.98/3.54 fof(f802,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(product(X0,X1,c),true,product(X0,multiply(X1,inverse(a)),d),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f788])).
% 22.98/3.54 fof(f984,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,product(inverse(X0),X2,X1),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f23,f161])).
% 22.98/3.54 fof(f1016,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,product(inverse(X0),X2,X1),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f984])).
% 22.98/3.54 fof(f1331,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(true,true,ifeq(product(X0,a,X1),true,product(X0,c,multiply(X1,b)),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f31,f164])).
% 22.98/3.54 fof(f1337,plain,(
% 22.98/3.54 ![X0,X1,X2,X3]: (ifeq(true,true,ifeq(product(X0,X1,X2),true,product(X0,multiply(X1,X3),multiply(X2,X3)),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f164])).
% 22.98/3.54 fof(f1371,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(product(X0,a,X1),true,product(X0,c,multiply(X1,b)),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f1331])).
% 22.98/3.54 fof(f1378,plain,(
% 22.98/3.54 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,product(X0,multiply(X1,X3),multiply(X2,X3)),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f1337])).
% 22.98/3.54 fof(f1446,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(inverse(inverse(X0)),identity,X0),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f23,f1016])).
% 22.98/3.54 fof(f1451,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(true,true,product(inverse(X0),multiply(X0,X1),X1),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f1016])).
% 22.98/3.54 fof(f1465,plain,(
% 22.98/3.54 ![X0]: (product(inverse(inverse(X0)),identity,X0)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f1446])).
% 22.98/3.54 fof(f1471,plain,(
% 22.98/3.54 ![X0,X1]: (product(inverse(X0),multiply(X0,X1),X1)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f1451])).
% 22.98/3.54 fof(f1615,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,inverse(inverse(X0)),X0)=X0)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1465,f80])).
% 22.98/3.54 fof(f1668,plain,(
% 22.98/3.54 ![X0]: (inverse(inverse(X0))=X0)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f1615])).
% 22.98/3.54 fof(f1802,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(true,true,X0,multiply(inverse(X1),multiply(X1,X0)))=multiply(inverse(X1),multiply(X1,X0)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1471,f71])).
% 22.98/3.54 fof(f1844,plain,(
% 22.98/3.54 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f1802])).
% 22.98/3.54 fof(f1854,plain,(
% 22.98/3.54 ![X0,X1]: (X0=multiply(X1,multiply(inverse(X1),X0)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1668,f1844])).
% 22.98/3.54 fof(f1867,plain,(
% 22.98/3.54 ![X0]: (multiply(X0,X0)=multiply(inverse(X0),identity))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f367,f1844])).
% 22.98/3.54 fof(f1882,plain,(
% 22.98/3.54 ![X0]: (multiply(X0,X0)=inverse(X0))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f100,f1867])).
% 22.98/3.54 fof(f1957,plain,(
% 22.98/3.54 ![X0]: (product(X0,X0,inverse(X0))=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1882,f25])).
% 22.98/3.54 fof(f5111,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(true,true,ifeq(product(X0,inverse(X1),X2),true,product(X2,X1,X0),true),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f22,f262])).
% 22.98/3.54 fof(f5161,plain,(
% 22.98/3.54 ![X0,X1,X2]: (ifeq(product(X0,inverse(X1),X2),true,product(X2,X1,X0),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f5111])).
% 22.98/3.54 fof(f5200,plain,(
% 22.98/3.54 ifeq(true,true,product(h,b,d),true)=true),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f33,f5161])).
% 22.98/3.54 fof(f5207,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(true,true,product(multiply(X0,inverse(X1)),X1,X0),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f5161])).
% 22.98/3.54 fof(f5251,plain,(
% 22.98/3.54 product(h,b,d)=true),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f5200])).
% 22.98/3.54 fof(f5260,plain,(
% 22.98/3.54 ![X0,X1]: (product(multiply(X0,inverse(X1)),X1,X0)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f5207])).
% 22.98/3.54 fof(f5374,plain,(
% 22.98/3.54 ifeq2(true,true,d,j)=j),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f5251,f65])).
% 22.98/3.54 fof(f5418,plain,(
% 22.98/3.54 ifeq2(true,true,d,multiply(h,b))=multiply(h,b)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f5251,f71])).
% 22.98/3.54 fof(f5430,plain,(
% 22.98/3.54 d=j),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f5374])).
% 22.98/3.54 fof(f5470,plain,(
% 22.98/3.54 d=multiply(h,b)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f5418])).
% 22.98/3.54 fof(f6256,plain,(
% 22.98/3.54 ![X0,X1]: (product(multiply(X0,X1),inverse(X1),X0)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1668,f5260])).
% 22.98/3.54 fof(f6371,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq2(true,true,X0,multiply(multiply(X0,inverse(X1)),X1))=multiply(multiply(X0,inverse(X1)),X1))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f5260,f71])).
% 22.98/3.54 fof(f6528,plain,(
% 22.98/3.54 ![X0,X1]: (X0=multiply(multiply(X0,inverse(X1)),X1))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f6371])).
% 22.98/3.54 fof(f6551,plain,(
% 22.98/3.54 ![X0,X1]: (X0=multiply(multiply(X0,X1),inverse(X1)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1668,f6528])).
% 22.98/3.54 fof(f6733,plain,(
% 22.98/3.54 ![X0,X1]: (inverse(X0)=multiply(X1,inverse(multiply(X0,X1))))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1844,f6551])).
% 22.98/3.54 fof(f6735,plain,(
% 22.98/3.54 a=multiply(c,inverse(b))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f206,f6551])).
% 22.98/3.54 fof(f6750,plain,(
% 22.98/3.54 ![X0,X1]: (inverse(X0)=multiply(inverse(multiply(X1,X0)),X1))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6551,f1844])).
% 22.98/3.54 fof(f6772,plain,(
% 22.98/3.54 inverse(b)=multiply(inverse(c),a)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6735,f1844])).
% 22.98/3.54 fof(f7661,plain,(
% 22.98/3.54 ![X0,X1]: (inverse(multiply(X0,X1))=multiply(inverse(X1),inverse(X0)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6551,f6733])).
% 22.98/3.54 fof(f7814,plain,(
% 22.98/3.54 ![X0,X1]: (inverse(multiply(inverse(X0),X1))=multiply(inverse(X1),X0))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1854,f6750])).
% 22.98/3.54 fof(f11662,plain,(
% 22.98/3.54 ![X0,X1,X2]: (X0=multiply(multiply(X0,multiply(inverse(X1),X2)),multiply(inverse(X2),X1)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f7814,f6551])).
% 22.98/3.54 fof(f19121,plain,(
% 22.98/3.54 ![X0,X1]: (ifeq(product(X0,X1,d),true,product(X0,multiply(X1,inverse(h)),k),true)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f5430,f685])).
% 22.98/3.54 fof(f19127,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(multiply(d,X0),multiply(inverse(X0),inverse(h)),k),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6256,f19121])).
% 22.98/3.54 fof(f19161,plain,(
% 22.98/3.54 ![X0]: (product(multiply(d,X0),multiply(inverse(X0),inverse(h)),k)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f19127])).
% 22.98/3.54 fof(f19162,plain,(
% 22.98/3.54 ![X0]: (product(multiply(d,X0),inverse(multiply(h,X0)),k)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f7661,f19161])).
% 22.98/3.54 fof(f20550,plain,(
% 22.98/3.54 product(multiply(d,b),inverse(d),k)=true),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f5470,f19162])).
% 22.98/3.54 fof(f21026,plain,(
% 22.98/3.54 ifeq(true,true,product(k,d,multiply(d,b)),true)=true),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f20550,f5161])).
% 22.98/3.54 fof(f21103,plain,(
% 22.98/3.54 product(k,d,multiply(d,b))=true),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f21026])).
% 22.98/3.54 fof(f21247,plain,(
% 22.98/3.54 ifeq2(true,true,multiply(d,b),multiply(k,d))=multiply(k,d)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f21103,f71])).
% 22.98/3.54 fof(f21322,plain,(
% 22.98/3.54 multiply(d,b)=multiply(k,d)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f21247])).
% 22.98/3.54 fof(f24402,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(multiply(c,X0),multiply(inverse(X0),inverse(a)),d),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6256,f802])).
% 22.98/3.54 fof(f24437,plain,(
% 22.98/3.54 ![X0]: (product(multiply(c,X0),multiply(inverse(X0),inverse(a)),d)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f24402])).
% 22.98/3.54 fof(f24438,plain,(
% 22.98/3.54 ![X0]: (product(multiply(c,X0),inverse(multiply(a,X0)),d)=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f7661,f24437])).
% 22.98/3.54 fof(f44471,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(d,multiply(a,X0),multiply(c,X0)),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f24438,f5161])).
% 22.98/3.54 fof(f44540,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,d,multiply(multiply(c,X0),inverse(multiply(a,X0))))=multiply(multiply(c,X0),inverse(multiply(a,X0))))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f24438,f71])).
% 22.98/3.54 fof(f44575,plain,(
% 22.98/3.54 ![X0]: (product(d,multiply(a,X0),multiply(c,X0))=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f44471])).
% 22.98/3.54 fof(f44648,plain,(
% 22.98/3.54 ![X0]: (d=multiply(multiply(c,X0),inverse(multiply(a,X0))))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f44540])).
% 22.98/3.54 fof(f45102,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,multiply(c,X0),multiply(d,multiply(a,X0)))=multiply(d,multiply(a,X0)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f44575,f71])).
% 22.98/3.54 fof(f45188,plain,(
% 22.98/3.54 ![X0]: (multiply(c,X0)=multiply(d,multiply(a,X0)))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f45102])).
% 22.98/3.54 fof(f45207,plain,(
% 22.98/3.54 ![X0]: (multiply(c,multiply(inverse(a),X0))=multiply(d,X0))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1854,f45188])).
% 22.98/3.54 fof(f45277,plain,(
% 22.98/3.54 ![X0]: (d=multiply(multiply(c,inverse(multiply(X0,a))),inverse(inverse(X0))))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f6733,f44648])).
% 22.98/3.54 fof(f45347,plain,(
% 22.98/3.54 ![X0]: (d=multiply(multiply(c,inverse(multiply(X0,a))),X0))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f1668,f45277])).
% 22.98/3.54 fof(f47779,plain,(
% 22.98/3.54 ![X0]: (c=multiply(multiply(d,X0),multiply(inverse(X0),a)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f45207,f11662])).
% 22.98/3.54 fof(f50039,plain,(
% 22.98/3.54 ![X0]: (c=multiply(X0,multiply(inverse(multiply(inverse(d),X0)),a)))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f1854,f47779])).
% 22.98/3.54 fof(f50113,plain,(
% 22.98/3.54 ![X0]: (c=multiply(X0,multiply(multiply(inverse(X0),d),a)))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f7814,f50039])).
% 22.98/3.54 fof(f50660,plain,(
% 22.98/3.54 ![X0]: (multiply(multiply(inverse(inverse(X0)),d),a)=multiply(X0,c))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f50113,f1854])).
% 22.98/3.54 fof(f50803,plain,(
% 22.98/3.54 ![X0]: (multiply(multiply(X0,d),a)=multiply(X0,c))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f1668,f50660])).
% 22.98/3.54 fof(f50827,plain,(
% 22.98/3.54 multiply(multiply(d,b),a)=multiply(k,c)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f21322,f50803])).
% 22.98/3.54 fof(f53353,plain,(
% 22.98/3.54 ![X0]: (ifeq(true,true,product(X0,c,multiply(multiply(X0,a),b)),true)=true)),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f25,f1371])).
% 22.98/3.54 fof(f53397,plain,(
% 22.98/3.54 ![X0]: (product(X0,c,multiply(multiply(X0,a),b))=true)),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f20,f53353])).
% 22.98/3.54 fof(f55099,plain,(
% 22.98/3.54 ![X0]: (ifeq2(true,true,multiply(multiply(X0,a),b),multiply(X0,c))=multiply(X0,c))),
% 22.98/3.54 inference(paramodulation,[status(thm)],[f53397,f71])).
% 22.98/3.54 fof(f55320,plain,(
% 22.98/3.54 ![X0]: (multiply(multiply(X0,a),b)=multiply(X0,c))),
% 22.98/3.54 inference(forward_demodulation,[status(thm)],[f19,f55099])).
% 22.98/3.54 fof(f55397,plain,(
% 22.98/3.54 multiply(d,b)=multiply(multiply(c,inverse(multiply(a,a))),c)),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f45347,f55320])).
% 24.86/3.63 fof(f55454,plain,(
% 24.86/3.63 multiply(d,b)=multiply(multiply(c,inverse(inverse(a))),c)),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f1882,f55397])).
% 24.86/3.63 fof(f55455,plain,(
% 24.86/3.63 multiply(d,b)=multiply(multiply(c,a),c)),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f1668,f55454])).
% 24.86/3.63 fof(f56002,plain,(
% 24.86/3.63 ![X0,X1]: (ifeq(true,true,product(X0,multiply(X0,X1),multiply(inverse(X0),X1)),true)=true)),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f1957,f1378])).
% 24.86/3.63 fof(f56506,plain,(
% 24.86/3.63 ![X0,X1]: (product(X0,multiply(X0,X1),multiply(inverse(X0),X1))=true)),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f20,f56002])).
% 24.86/3.63 fof(f57510,plain,(
% 24.86/3.63 ![X0,X1]: (ifeq2(true,true,multiply(inverse(X0),X1),multiply(X0,multiply(X0,X1)))=multiply(X0,multiply(X0,X1)))),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f56506,f71])).
% 24.86/3.63 fof(f57906,plain,(
% 24.86/3.63 ![X0,X1]: (multiply(inverse(X0),X1)=multiply(X0,multiply(X0,X1)))),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f19,f57510])).
% 24.86/3.63 fof(f59498,plain,(
% 24.86/3.63 ![X0,X1]: (X0=multiply(multiply(inverse(X0),X1),inverse(multiply(X0,X1))))),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f57906,f6551])).
% 24.86/3.63 fof(f68593,plain,(
% 24.86/3.63 multiply(c,a)=multiply(multiply(inverse(multiply(c,a)),c),inverse(multiply(d,b)))),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f55455,f59498])).
% 24.86/3.63 fof(f68638,plain,(
% 24.86/3.63 multiply(c,a)=multiply(inverse(a),inverse(multiply(d,b)))),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f6750,f68593])).
% 24.86/3.63 fof(f68639,plain,(
% 24.86/3.63 multiply(c,a)=inverse(multiply(multiply(d,b),a))),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f7661,f68638])).
% 24.86/3.63 fof(f68640,plain,(
% 24.86/3.63 multiply(c,a)=inverse(multiply(k,c))),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f50827,f68639])).
% 24.86/3.63 fof(f68670,plain,(
% 24.86/3.63 inverse(k)=multiply(c,multiply(c,a))),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f68640,f6733])).
% 24.86/3.63 fof(f68805,plain,(
% 24.86/3.63 inverse(k)=multiply(inverse(c),a)),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f57906,f68670])).
% 24.86/3.63 fof(f68806,plain,(
% 24.86/3.63 inverse(k)=inverse(b)),
% 24.86/3.63 inference(forward_demodulation,[status(thm)],[f6772,f68805])).
% 24.86/3.63 fof(f69037,plain,(
% 24.86/3.63 product(k,inverse(b),identity)=true),
% 24.86/3.63 inference(paramodulation,[status(thm)],[f68806,f24])).
% 24.86/3.63 fof(f69072,plain,(
% 24.86/3.63 $false),
% 24.86/3.63 inference(forward_subsumption_resolution,[status(thm)],[f69037,f36])).
% 24.86/3.63 % SZS output end CNFRefutation for theBenchmark.p
% 24.86/3.66 % Elapsed time: 3.260181 seconds
% 24.86/3.66 % CPU time: 25.660980 seconds
% 24.86/3.66 % Total memory used: 434.882 MB
% 24.86/3.66 % Net memory used: 425.707 MB
%------------------------------------------------------------------------------