%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP767-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:37:18 PM UTC 2026
% Result : Unsatisfiable 10.70s 2.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP767-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n003.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Sun Sep 20 20:41:01 UTC 2026
% 0.19/0.43 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 10.70/2.14 % Refutation found
% 10.70/2.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.70/2.14 % SZS output start CNFRefutation for theBenchmark
% 10.70/2.14 fof(f1,axiom,(
% 10.70/2.14 (![A]: (product(A,one) = A ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f3,axiom,(
% 10.70/2.14 (![A,B]: (product(A,difference(A,B)) = B ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f4,axiom,(
% 10.70/2.14 (![A,B]: (difference(A,product(A,B)) = B ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f5,axiom,(
% 10.70/2.14 (![A,B]: (quotient(product(A,B),B) = A ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f6,axiom,(
% 10.70/2.14 (![A,B]: (product(quotient(A,B),B) = A ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f7,axiom,(
% 10.70/2.14 (![A,B,C]: (difference(A,product(product(A,B),C)) = quotient(product(B,product(C,A)),A) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f9,axiom,(
% 10.70/2.14 (![A]: (i(A) = difference(A,one) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f10,axiom,(
% 10.70/2.14 (![A]: (j(A) = quotient(one,A) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f11,axiom,(
% 10.70/2.14 (![A]: (product(i(A),A) = product(A,j(A)) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f12,axiom,(
% 10.70/2.14 (![A]: (eta(A) = product(i(A),A) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f13,axiom,(
% 10.70/2.14 (![A,B]: (product(i(i(A)),B) = product(eta(A),product(A,B)) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f14,axiom,(
% 10.70/2.14 (![A,B]: (product(A,product(eta(A),B)) = product(j(j(A)),B) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f15,axiom,(
% 10.70/2.14 (![A,B]: (product(A,product(B,eta(A))) = product(product(A,B),eta(A)) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f16,axiom,(
% 10.70/2.14 (![A,B,C]: (product(eta(A),product(B,C)) = product(product(eta(A),B),C) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f17,axiom,(
% 10.70/2.14 (![A,B,C]: (l(A,B,C) = difference(product(A,B),product(A,product(B,C))) ))),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f21,negated_conjecture,(
% 10.70/2.14 product(j(j(x0)),j(product(x1,x0))) != j(x1) ),
% 10.70/2.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.70/2.14 fof(f22,plain,(
% 10.70/2.14 ![X0]: (product(X0,one)=X0)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f1])).
% 10.70/2.14 fof(f24,plain,(
% 10.70/2.14 ![X0,X1]: (product(X0,difference(X0,X1))=X1)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f3])).
% 10.70/2.14 fof(f25,plain,(
% 10.70/2.14 ![X0,X1]: (difference(X0,product(X0,X1))=X1)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f4])).
% 10.70/2.14 fof(f26,plain,(
% 10.70/2.14 ![X0,X1]: (quotient(product(X0,X1),X1)=X0)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f5])).
% 10.70/2.14 fof(f27,plain,(
% 10.70/2.14 ![X0,X1]: (product(quotient(X0,X1),X1)=X0)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f6])).
% 10.70/2.14 fof(f28,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(X0,product(product(X0,X1),X2))=quotient(product(X1,product(X2,X0)),X0))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f7])).
% 10.70/2.14 fof(f30,plain,(
% 10.70/2.14 ![X0]: (i(X0)=difference(X0,one))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f9])).
% 10.70/2.14 fof(f31,plain,(
% 10.70/2.14 ![X0]: (j(X0)=quotient(one,X0))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f10])).
% 10.70/2.14 fof(f32,plain,(
% 10.70/2.14 ![X0]: (product(i(X0),X0)=product(X0,j(X0)))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f11])).
% 10.70/2.14 fof(f33,plain,(
% 10.70/2.14 ![X0]: (eta(X0)=product(i(X0),X0))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f12])).
% 10.70/2.14 fof(f34,plain,(
% 10.70/2.14 ![X0,X1]: (product(i(i(X0)),X1)=product(eta(X0),product(X0,X1)))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f13])).
% 10.70/2.14 fof(f35,plain,(
% 10.70/2.14 ![X0,X1]: (product(X0,product(eta(X0),X1))=product(j(j(X0)),X1))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f14])).
% 10.70/2.14 fof(f36,plain,(
% 10.70/2.14 ![X0,X1]: (product(X0,product(X1,eta(X0)))=product(product(X0,X1),eta(X0)))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f15])).
% 10.70/2.14 fof(f37,plain,(
% 10.70/2.14 ![X0,X1,X2]: (product(eta(X0),product(X1,X2))=product(product(eta(X0),X1),X2))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f16])).
% 10.70/2.14 fof(f38,plain,(
% 10.70/2.14 ![X0,X1,X2]: (l(X0,X1,X2)=difference(product(X0,X1),product(X0,product(X1,X2))))),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f17])).
% 10.70/2.14 fof(f42,plain,(
% 10.70/2.14 ~product(j(j(x0)),j(product(x1,x0)))=j(x1)),
% 10.70/2.14 inference(cnf_transformation,[status(thm)],[f21])).
% 10.70/2.14 fof(f50,plain,(
% 10.70/2.14 ![X0]: (eta(X0)=product(X0,j(X0)))),
% 10.70/2.14 inference(backward_demodulation,[status(thm)],[f33,f32])).
% 10.70/2.14 fof(f67,plain,(
% 10.70/2.14 ![X0,X1]: (quotient(X0,difference(X1,X0))=X1)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f24,f26])).
% 10.70/2.14 fof(f79,plain,(
% 10.70/2.14 ![X0,X1]: (difference(quotient(X0,X1),X0)=X1)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f27,f25])).
% 10.70/2.14 fof(f84,plain,(
% 10.70/2.14 ![X0]: (product(X0,i(X0))=one)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f30,f24])).
% 10.70/2.14 fof(f88,plain,(
% 10.70/2.14 ![X0]: (product(j(X0),X0)=one)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f31,f27])).
% 10.70/2.14 fof(f98,plain,(
% 10.70/2.14 ![X0,X1,X2]: (product(X0,quotient(product(X1,product(X2,X0)),X0))=product(product(X0,X1),X2))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f28,f24])).
% 10.70/2.14 fof(f109,plain,(
% 10.70/2.14 ![X0]: (j(difference(X0,one))=X0)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f31,f67])).
% 10.70/2.14 fof(f117,plain,(
% 10.70/2.14 ![X0]: (j(i(X0))=X0)),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f30,f109])).
% 10.70/2.14 fof(f121,plain,(
% 10.70/2.14 ![X0]: (i(quotient(one,X0))=X0)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f30,f79])).
% 10.70/2.14 fof(f130,plain,(
% 10.70/2.14 ![X0]: (i(j(X0))=X0)),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f31,f121])).
% 10.70/2.14 fof(f148,plain,(
% 10.70/2.14 ![X0]: (eta(j(X0))=product(X0,j(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f130,f33])).
% 10.70/2.14 fof(f155,plain,(
% 10.70/2.14 ![X0]: (eta(j(X0))=eta(X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f50,f148])).
% 10.70/2.14 fof(f206,plain,(
% 10.70/2.14 ![X0]: (product(i(i(X0)),one)=product(eta(X0),X0))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f22,f34])).
% 10.70/2.14 fof(f225,plain,(
% 10.70/2.14 ![X0]: (i(i(X0))=product(eta(X0),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f22,f206])).
% 10.70/2.14 fof(f290,plain,(
% 10.70/2.14 ![X0]: (product(X0,one)=product(j(j(X0)),i(eta(X0))))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f84,f35])).
% 10.70/2.14 fof(f292,plain,(
% 10.70/2.14 ![X0]: (product(X0,eta(X0))=product(j(j(X0)),one))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f22,f35])).
% 10.70/2.14 fof(f307,plain,(
% 10.70/2.14 ![X0]: (X0=product(j(j(X0)),i(eta(X0))))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f22,f290])).
% 10.70/2.14 fof(f308,plain,(
% 10.70/2.14 ![X0]: (product(X0,eta(X0))=j(j(X0)))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f22,f292])).
% 10.70/2.14 fof(f340,plain,(
% 10.70/2.14 ![X0]: (i(i(j(X0)))=product(eta(X0),j(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f155,f225])).
% 10.70/2.14 fof(f351,plain,(
% 10.70/2.14 ![X0]: (i(X0)=product(eta(X0),j(X0)))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f130,f340])).
% 10.70/2.14 fof(f517,plain,(
% 10.70/2.14 ![X0]: (product(i(i(X0)),eta(X0))=product(eta(X0),j(j(X0))))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f308,f34])).
% 10.70/2.14 fof(f542,plain,(
% 10.70/2.14 ![X0,X1]: (product(eta(X0),product(j(eta(X0)),X1))=product(eta(eta(X0)),X1))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f50,f37])).
% 10.70/2.14 fof(f550,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(eta(X0),product(eta(X0),product(X1,X2)))=quotient(product(X1,product(X2,eta(X0))),eta(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f37,f28])).
% 10.70/2.14 fof(f562,plain,(
% 10.70/2.14 ![X0,X1,X2]: (quotient(product(eta(X0),product(X1,X2)),X2)=product(eta(X0),X1))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f37,f26])).
% 10.70/2.14 fof(f563,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(product(eta(X0),X1),product(eta(X0),product(X1,X2)))=X2)),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f37,f25])).
% 10.70/2.14 fof(f574,plain,(
% 10.70/2.14 ![X0,X1,X2]: (product(X0,X1)=quotient(product(X0,product(X1,eta(X2))),eta(X2)))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f25,f550])).
% 10.70/2.14 fof(f580,plain,(
% 10.70/2.14 ![X0,X1,X2]: (l(eta(X0),X1,X2)=X2)),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f38,f563])).
% 10.70/2.14 fof(f590,plain,(
% 10.70/2.14 ![X0]: (i(j(X0))=product(eta(X0),j(j(X0))))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f155,f351])).
% 10.70/2.14 fof(f604,plain,(
% 10.70/2.14 ![X0]: (product(i(i(X0)),eta(X0))=X0)),
% 10.70/2.14 inference(backward_demodulation,[status(thm)],[f605,f517])).
% 10.70/2.14 fof(f605,plain,(
% 10.70/2.14 ![X0]: (X0=product(eta(X0),j(j(X0))))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f130,f590])).
% 10.70/2.14 fof(f704,plain,(
% 10.70/2.14 ![X0,X1]: (l(X0,X1,i(X1))=difference(product(X0,X1),product(X0,one)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f84,f38])).
% 10.70/2.14 fof(f745,plain,(
% 10.70/2.14 ![X0,X1]: (l(X0,X1,i(X1))=difference(product(X0,X1),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f22,f704])).
% 10.70/2.14 fof(f862,plain,(
% 10.70/2.14 ![X0]: (difference(eta(X0),X0)=j(j(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f605,f25])).
% 10.70/2.14 fof(f1284,plain,(
% 10.70/2.14 ![X0]: (product(i(i(j(j(X0)))),i(eta(X0)))=product(eta(j(j(X0))),X0))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f307,f34])).
% 10.70/2.14 fof(f1307,plain,(
% 10.70/2.14 ![X0]: (product(i(j(X0)),i(eta(X0)))=product(eta(j(j(X0))),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f130,f1284])).
% 10.70/2.14 fof(f1308,plain,(
% 10.70/2.14 ![X0]: (product(X0,i(eta(X0)))=product(eta(j(j(X0))),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f130,f1307])).
% 10.70/2.14 fof(f1309,plain,(
% 10.70/2.14 ![X0]: (product(X0,i(eta(X0)))=product(eta(j(X0)),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f155,f1308])).
% 10.70/2.14 fof(f1310,plain,(
% 10.70/2.14 ![X0]: (product(X0,i(eta(X0)))=product(eta(X0),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f155,f1309])).
% 10.70/2.14 fof(f1311,plain,(
% 10.70/2.14 ![X0]: (product(X0,i(eta(X0)))=i(i(X0)))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f225,f1310])).
% 10.70/2.14 fof(f1487,plain,(
% 10.70/2.14 ![X0]: (product(X0,product(i(eta(X0)),eta(X0)))=product(i(i(X0)),eta(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f1311,f36])).
% 10.70/2.14 fof(f1507,plain,(
% 10.70/2.14 ![X0]: (product(X0,eta(eta(X0)))=product(i(i(X0)),eta(X0)))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f33,f1487])).
% 10.70/2.14 fof(f1509,plain,(
% 10.70/2.14 ![X0]: (product(X0,eta(eta(X0)))=X0)),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f604,f1507])).
% 10.70/2.14 fof(f1529,plain,(
% 10.70/2.14 ![X0,X1]: (difference(X0,product(X0,X1))=quotient(product(eta(eta(X0)),product(X1,X0)),X0))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f1509,f28])).
% 10.70/2.14 fof(f1546,plain,(
% 10.70/2.14 ![X0,X1]: (X0=quotient(product(eta(eta(X1)),product(X0,X1)),X1))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f25,f1529])).
% 10.70/2.14 fof(f1554,plain,(
% 10.70/2.14 ![X0,X1]: (product(eta(X0),product(j(eta(X0)),X1))=X1)),
% 10.70/2.14 inference(backward_demodulation,[status(thm)],[f1556,f542])).
% 10.70/2.14 fof(f1556,plain,(
% 10.70/2.14 ![X0,X1]: (X0=product(eta(eta(X1)),X0))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f562,f1546])).
% 10.70/2.14 fof(f2476,plain,(
% 10.70/2.14 ![X0,X1]: (product(X0,quotient(one,X0))=product(product(X0,j(product(X1,X0))),X1))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f88,f98])).
% 10.70/2.14 fof(f2532,plain,(
% 10.70/2.14 ![X0,X1]: (product(X0,j(X0))=product(product(X0,j(product(X1,X0))),X1))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f31,f2476])).
% 10.70/2.14 fof(f2533,plain,(
% 10.70/2.14 ![X0,X1]: (eta(X0)=product(product(X0,j(product(X1,X0))),X1))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f50,f2532])).
% 10.70/2.14 fof(f2960,plain,(
% 10.70/2.14 ![X0,X1]: (i(X0)=difference(product(eta(X1),X0),eta(X1)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f580,f745])).
% 10.70/2.14 fof(f3422,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(eta(X0),product(X1,X2))=quotient(product(product(j(eta(X0)),X1),product(X2,eta(X0))),eta(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f1554,f28])).
% 10.70/2.14 fof(f3424,plain,(
% 10.70/2.14 ![X0,X1]: (difference(eta(X0),X1)=product(j(eta(X0)),X1))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f1554,f25])).
% 10.70/2.14 fof(f3489,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(eta(X0),product(X1,X2))=product(product(j(eta(X0)),X1),X2))),
% 10.70/2.14 inference(forward_demodulation,[status(thm)],[f574,f3422])).
% 10.70/2.14 fof(f3497,plain,(
% 10.70/2.14 ![X0,X1,X2]: (difference(eta(X0),product(X1,X2))=product(difference(eta(X0),X1),X2))),
% 10.70/2.14 inference(backward_demodulation,[status(thm)],[f3424,f3489])).
% 10.70/2.14 fof(f3830,plain,(
% 10.70/2.14 ![X0,X1]: (i(difference(eta(X0),X1))=difference(X1,eta(X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f24,f2960])).
% 10.70/2.14 fof(f5285,plain,(
% 10.70/2.14 ![X0,X1]: (j(difference(X0,eta(X1)))=difference(eta(X1),X0))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f3830,f117])).
% 10.70/2.14 fof(f6032,plain,(
% 10.70/2.14 ![X0,X1]: (j(X0)=difference(eta(X1),quotient(eta(X1),X0)))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f79,f5285])).
% 10.70/2.14 fof(f7827,plain,(
% 10.70/2.14 ![X0,X1]: (quotient(eta(X0),X1)=product(X0,j(product(X1,X0))))),
% 10.70/2.14 inference(paramodulation,[status(thm)],[f2533,f26])).
% 10.70/2.14 fof(f9869,plain,(
% 10.70/2.14 ![X0,X1]: (quotient(eta(X0),quotient(X1,X0))=product(X0,j(X1)))),
% 10.70/2.23 inference(paramodulation,[status(thm)],[f27,f7827])).
% 10.70/2.23 fof(f16263,plain,(
% 10.70/2.23 ![X0,X1]: (j(quotient(X0,X1))=difference(eta(X1),product(X1,j(X0))))),
% 10.70/2.23 inference(paramodulation,[status(thm)],[f9869,f6032])).
% 10.70/2.23 fof(f16366,plain,(
% 10.70/2.23 ![X0,X1]: (j(quotient(X0,X1))=product(difference(eta(X1),X1),j(X0)))),
% 10.70/2.23 inference(forward_demodulation,[status(thm)],[f3497,f16263])).
% 10.70/2.23 fof(f16367,plain,(
% 10.70/2.23 ~j(quotient(product(x1,x0),x0))=j(x1)),
% 10.70/2.23 inference(backward_demodulation,[status(thm)],[f16381,f42])).
% 10.70/2.23 fof(f16381,plain,(
% 10.70/2.23 ![X0,X1]: (j(quotient(X0,X1))=product(j(j(X1)),j(X0)))),
% 10.70/2.23 inference(forward_demodulation,[status(thm)],[f862,f16366])).
% 10.70/2.23 fof(f16415,plain,(
% 10.70/2.23 ~j(x1)=j(x1)),
% 10.70/2.23 inference(forward_demodulation,[status(thm)],[f26,f16367])).
% 10.70/2.23 fof(f16416,plain,(
% 10.70/2.23 $false),
% 10.70/2.23 inference(trivial_equality_resolution,[status(thm)],[f16415])).
% 10.70/2.23 % SZS output end CNFRefutation for theBenchmark.p
% 2.17/2.26 % Elapsed time: 1.803967 seconds
% 2.17/2.26 % CPU time: 13.677853 seconds
% 2.17/2.26 % Total memory used: 231.965 MB
% 2.17/2.26 % Net memory used: 226.629 MB
%------------------------------------------------------------------------------