%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:19 PM UTC 2026
% Result : Unsatisfiable 82.21s 10.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP777-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.33 % Computer : n020.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Sun Sep 20 20:40:32 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.06/0.34 % Drodi V4.1.1
% 82.21/10.83 % Refutation found
% 82.21/10.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 82.21/10.83 % SZS output start CNFRefutation for theBenchmark
% 82.21/10.83 fof(f1,axiom,(
% 82.21/10.83 (![A,B]: (difference(A,product(A,B)) = B ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f2,axiom,(
% 82.21/10.83 (![A,B]: (product(A,difference(A,B)) = B ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f3,axiom,(
% 82.21/10.83 (![A,B]: (quotient(product(A,B),B) = A ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f4,axiom,(
% 82.21/10.83 (![A,B]: (product(quotient(A,B),B) = A ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f5,axiom,(
% 82.21/10.83 (![A,B,C,D]: (product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)) ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f6,axiom,(
% 82.21/10.83 (![A]: (product(A,A) = A ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f7,axiom,(
% 82.21/10.83 (![A,B]: (product(product(product(A,B),B),product(B,product(B,A))) = B ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f8,axiom,(
% 82.21/10.83 (![A,B,C]: (bigC(A,B,C) = product(product(A,B),product(C,A)) ))),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f9,axiom,(
% 82.21/10.83 product(product(a,c),product(c,b)) = product(a,b) ),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f10,negated_conjecture,(
% 82.21/10.83 bigC(a,b,x0) != bigC(c,c,x0) ),
% 82.21/10.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.21/10.83 fof(f11,plain,(
% 82.21/10.83 ![X0,X1]: (difference(X0,product(X0,X1))=X1)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f1])).
% 82.21/10.83 fof(f12,plain,(
% 82.21/10.83 ![X0,X1]: (product(X0,difference(X0,X1))=X1)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f2])).
% 82.21/10.83 fof(f13,plain,(
% 82.21/10.83 ![X0,X1]: (quotient(product(X0,X1),X1)=X0)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f3])).
% 82.21/10.83 fof(f14,plain,(
% 82.21/10.83 ![X0,X1]: (product(quotient(X0,X1),X1)=X0)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f4])).
% 82.21/10.83 fof(f15,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (product(product(X0,X1),product(X2,X3))=product(product(X0,X2),product(X1,X3)))),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f5])).
% 82.21/10.83 fof(f16,plain,(
% 82.21/10.83 ![X0]: (product(X0,X0)=X0)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f6])).
% 82.21/10.83 fof(f17,plain,(
% 82.21/10.83 ![X0,X1]: (product(product(product(X0,X1),X1),product(X1,product(X1,X0)))=X1)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f7])).
% 82.21/10.83 fof(f18,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X0,X1),product(X2,X0)))),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f8])).
% 82.21/10.83 fof(f19,plain,(
% 82.21/10.83 product(product(a,c),product(c,b))=product(a,b)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f9])).
% 82.21/10.83 fof(f20,plain,(
% 82.21/10.83 ~bigC(a,b,x0)=bigC(c,c,x0)),
% 82.21/10.83 inference(cnf_transformation,[status(thm)],[f10])).
% 82.21/10.83 fof(f28,plain,(
% 82.21/10.83 ![X0,X1]: (quotient(X0,difference(X1,X0))=X1)),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f13])).
% 82.21/10.83 fof(f29,plain,(
% 82.21/10.83 ![X0]: (quotient(X0,X0)=X0)),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f13])).
% 82.21/10.83 fof(f33,plain,(
% 82.21/10.83 ![X0,X1]: (difference(quotient(X0,X1),X0)=X1)),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f11])).
% 82.21/10.83 fof(f44,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(quotient(X0,X1),X1,X2)=product(X0,product(X2,quotient(X0,X1))))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f18])).
% 82.21/10.83 fof(f45,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,difference(X0,X1),X2)=product(X1,product(X2,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f18])).
% 82.21/10.83 fof(f46,plain,(
% 82.21/10.83 ![X0,X1]: (bigC(X0,X0,X1)=product(X0,product(X1,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f18])).
% 82.21/10.83 fof(f48,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,quotient(X2,X0))=product(product(X0,X1),X2))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f18])).
% 82.21/10.83 fof(f49,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(difference(X0,X1),X2,X0)=product(product(difference(X0,X1),X2),X1))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f18])).
% 82.21/10.83 fof(f50,plain,(
% 82.21/10.83 ![X0,X1]: (bigC(X0,X1,X0)=product(product(X0,X1),X0))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f18])).
% 82.21/10.83 fof(f51,plain,(
% 82.21/10.83 ![X0,X1,X2]: (quotient(bigC(X0,X1,X2),product(X2,X0))=product(X0,X1))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f18,f13])).
% 82.21/10.83 fof(f52,plain,(
% 82.21/10.83 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X0,X1,X2))=product(X2,X0))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f18,f11])).
% 82.21/10.83 fof(f64,plain,(
% 82.21/10.83 ![X0,X1]: (difference(X0,bigC(X0,X0,X1))=product(X1,X0))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f46,f11])).
% 82.21/10.83 fof(f78,plain,(
% 82.21/10.83 ![X0,X1]: (quotient(bigC(X0,X1,X0),X0)=product(X0,X1))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f50,f13])).
% 82.21/10.83 fof(f86,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X0,X2),product(X1,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f18,f15])).
% 82.21/10.83 fof(f93,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (product(bigC(X0,X1,X0),product(X2,X3))=product(product(product(X0,X1),X2),product(X0,X3)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f50,f15])).
% 82.21/10.83 fof(f94,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (product(X0,product(X1,X2))=product(product(quotient(X0,X3),X1),product(X3,X2)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f15])).
% 82.21/10.83 fof(f96,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (product(X0,product(X1,X2))=product(product(X3,X1),product(difference(X3,X0),X2)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f15])).
% 82.21/10.83 fof(f97,plain,(
% 82.21/10.83 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(product(X0,X1),product(X0,X2)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f15])).
% 82.21/10.83 fof(f105,plain,(
% 82.21/10.83 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(product(X0,X2),product(X1,X2)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f15])).
% 82.21/10.83 fof(f131,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X3),product(X0,X1))=product(product(product(X0,X2),product(X1,X3)),product(X0,X1)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f15,f50])).
% 82.21/10.83 fof(f158,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X3),product(X0,X1))=product(bigC(X0,X2,X0),product(product(X1,X3),X1)))),
% 82.21/10.83 inference(forward_demodulation,[status(thm)],[f93,f131])).
% 82.21/10.83 fof(f160,plain,(
% 82.21/10.83 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X3),product(X0,X1))=product(bigC(X0,X2,X0),bigC(X1,X3,X1)))),
% 82.21/10.83 inference(forward_demodulation,[status(thm)],[f50,f158])).
% 82.21/10.83 fof(f215,plain,(
% 82.21/10.83 ![X0,X1,X2]: (quotient(bigC(difference(X0,X1),X2,X0),X1)=product(difference(X0,X1),X2))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f51])).
% 82.21/10.83 fof(f230,plain,(
% 82.21/10.83 ![X0,X1,X2]: (difference(X0,bigC(quotient(X0,X1),X1,X2))=product(X2,quotient(X0,X1)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f52])).
% 82.21/10.83 fof(f256,plain,(
% 82.21/10.83 ![X0,X1]: (product(product(X0,X1),product(X1,product(X1,quotient(X0,X1))))=X1)),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f14,f17])).
% 82.21/10.83 fof(f315,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X0,X2,X1))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f18,f86])).
% 82.21/10.83 fof(f324,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,product(X2,X0))=product(bigC(X0,X0,X2),product(X1,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f46,f86])).
% 82.21/10.83 fof(f325,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,X1,difference(X0,X2))=product(X2,product(X1,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f12,f86])).
% 82.21/10.83 fof(f326,plain,(
% 82.21/10.83 ![X0,X1]: (bigC(X0,X1,X0)=product(X0,product(X1,X0)))),
% 82.21/10.83 inference(paramodulation,[status(thm)],[f16,f86])).
% 82.21/10.83 fof(f332,plain,(
% 82.21/10.83 ![X0,X1,X2]: (bigC(X0,product(X0,X1),X2)=product(product(X0,X2),bigC(X0,X1,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f50,f86])).
% 82.21/10.84 fof(f333,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,quotient(X1,X0),X2)=product(product(X0,X2),X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f14,f86])).
% 82.21/10.84 fof(f336,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(X0,X0,X1)=product(product(X0,X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f16,f86])).
% 82.21/10.84 fof(f347,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (product(product(X0,product(X1,X2)),product(X3,product(X4,X1)))=product(product(X0,X3),bigC(X1,X4,X2)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f86,f15])).
% 82.21/10.84 fof(f348,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (product(product(product(X0,X1),X2),product(product(X3,X0),X4))=product(bigC(X0,X3,X1),product(X2,X4)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f86,f15])).
% 82.21/10.84 fof(f351,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(X0,X1),product(X2,X0),product(X0,X1))=product(bigC(X0,X2,X1),product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f86,f50])).
% 82.21/10.84 fof(f356,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X0,X2,X1))=product(X2,X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f86,f11])).
% 82.21/10.84 fof(f371,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(bigC(X0,X1,X0),bigC(X2,X0,X2))=product(bigC(X0,X1,X2),product(X0,X2)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f160,f351])).
% 82.21/10.84 fof(f386,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(bigC(X0,X0,X1),X0)=product(X0,X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f315,f78])).
% 82.21/10.84 fof(f387,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,bigC(X0,X1,X0))=product(X1,X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f315,f64])).
% 82.21/10.84 fof(f527,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(product(X0,X0),X1),X0)=product(X0,quotient(X1,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f48,f386])).
% 82.21/10.84 fof(f535,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),X0)=product(X0,quotient(X1,X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f527])).
% 82.21/10.84 fof(f539,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,product(X1,product(X0,X0)))=product(difference(X0,X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f45,f387])).
% 82.21/10.84 fof(f547,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,product(X1,X0))=product(difference(X0,X1),X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f539])).
% 82.21/10.84 fof(f566,plain,(
% 82.21/10.84 quotient(product(a,b),product(c,b))=product(a,c)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f19,f13])).
% 82.21/10.84 fof(f598,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(X0,X1)=product(X1,quotient(difference(X1,X0),X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f12,f535])).
% 82.21/10.84 fof(f617,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(product(X2,X0),product(X3,X1)))=product(difference(product(X0,X1),product(X2,X3)),product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f15,f547])).
% 82.21/10.84 fof(f619,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(difference(product(X0,X1),product(X1,X2)),product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f18,f547])).
% 82.21/10.84 fof(f622,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,X1)=product(difference(X0,quotient(X1,X0)),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f14,f547])).
% 82.21/10.84 fof(f629,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),product(difference(X1,X0),X1))=X1)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f547,f28])).
% 82.21/10.84 fof(f653,plain,(
% 82.21/10.84 ![X0,X1]: (product(product(product(quotient(difference(X0,X1),X0),X0),X0),product(X0,quotient(X1,X0)))=X0)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f598,f17])).
% 82.21/10.84 fof(f666,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,quotient(X1,X0))=quotient(difference(X0,X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f598,f11])).
% 82.21/10.84 fof(f678,plain,(
% 82.21/10.84 ![X0,X1]: (product(product(difference(X0,X1),X0),product(X0,quotient(X1,X0)))=X0)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f14,f653])).
% 82.21/10.84 fof(f777,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(difference(X0,quotient(X1,X0)),X0,X2)=product(difference(X0,X1),product(X2,difference(X0,quotient(X1,X0)))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f622,f18])).
% 82.21/10.84 fof(f779,plain,(
% 82.21/10.84 ![X0,X1]: (difference(difference(X0,quotient(X1,X0)),difference(X0,X1))=X0)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f622,f11])).
% 82.21/10.84 fof(f926,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(difference(X1,X2),X1))=product(X2,product(difference(X1,X0),X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f45,f325])).
% 82.21/10.84 fof(f1400,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=product(product(X0,X1),bigC(quotient(X0,X3),X3,X2)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f44,f97])).
% 82.21/10.84 fof(f1401,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,product(X2,X0)))=product(product(X0,X1),bigC(X0,X2,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f326,f97])).
% 82.21/10.84 fof(f1403,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,difference(X0,X2)))=product(product(X0,X1),X2))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f12,f97])).
% 82.21/10.84 fof(f1467,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,product(X2,X0)))=bigC(X0,product(X0,X2),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f332,f1401])).
% 82.21/10.84 fof(f1652,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=product(difference(X0,X1),quotient(X1,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f622,f49])).
% 82.21/10.84 fof(f2112,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X0)=product(bigC(X0,X0,X1),product(X2,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f336,f105])).
% 82.21/10.84 fof(f2171,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X1),X3)=product(product(product(X0,X1),X3),product(product(X2,X0),X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f105,f86])).
% 82.21/10.84 fof(f2199,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X0)=bigC(X0,X2,product(X1,X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f324,f2112])).
% 82.21/10.84 fof(f2248,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(bigC(X0,X1,X0),bigC(X2,X0,X2))=bigC(product(X0,X2),product(X1,X2),X0))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f2249,f371])).
% 82.21/10.84 fof(f2249,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X1),X3)=product(bigC(X0,X2,X1),product(X3,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f348,f2171])).
% 82.21/10.84 fof(f4225,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),product(X0,product(X0,quotient(difference(X0,quotient(X1,X0)),X0))))=X0)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f622,f256])).
% 82.21/10.84 fof(f4326,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),product(X0,product(X0,difference(X0,quotient(quotient(X1,X0),X0)))))=X0)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f666,f4225])).
% 82.21/10.84 fof(f4327,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),product(product(X0,X0),quotient(quotient(X1,X0),X0)))=X0)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f1403,f4326])).
% 82.21/10.84 fof(f4328,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),product(X0,quotient(quotient(X1,X0),X0)))=X0)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f4327])).
% 82.21/10.84 fof(f4882,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (quotient(product(X0,product(X1,X2)),product(X3,X2))=product(quotient(X0,X3),X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f94,f13])).
% 82.21/10.84 fof(f5264,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(X0,bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0))))=product(X2,product(difference(X0,X1),X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f678,f356])).
% 82.21/10.84 fof(f5271,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),X0),product(X0,quotient(X1,X0)))=product(product(X0,quotient(X1,X0)),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f678,f326])).
% 82.21/10.84 fof(f5273,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=product(X0,product(X2,product(difference(X0,X1),X0))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f678,f86])).
% 82.21/10.84 fof(f5282,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=product(product(product(X0,quotient(X1,X0)),X2),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f678,f18])).
% 82.21/10.84 fof(f5348,plain,(
% 82.21/10.84 ![X0,X1]: (product(bigC(X0,difference(X0,X1),X0),bigC(quotient(X1,X0),X0,quotient(X1,X0)))=product(product(X0,quotient(X1,X0)),X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f160,f5271])).
% 82.21/10.84 fof(f5349,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(product(X0,quotient(X1,X0)),X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f2248,f5348])).
% 82.21/10.84 fof(f5350,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=bigC(X0,X0,quotient(X1,X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f336,f5349])).
% 82.21/10.84 fof(f5351,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(product(X0,X0),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f48,f5350])).
% 82.21/10.84 fof(f5352,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(X0,X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f5351])).
% 82.21/10.84 fof(f5356,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=bigC(X0,product(X0,difference(X0,X1)),X2))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f1467,f5273])).
% 82.21/10.84 fof(f5357,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(X0,bigC(X0,X1,X2))=product(X2,product(difference(X0,X1),X0)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f5358,f5264])).
% 82.21/10.84 fof(f5358,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=bigC(X0,X1,X2))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f12,f5356])).
% 82.21/10.84 fof(f5371,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=bigC(X0,X2,product(quotient(X1,X0),X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f2199,f5282])).
% 82.21/10.84 fof(f5374,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=bigC(X0,X2,X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f14,f5371])).
% 82.21/10.84 fof(f5404,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(difference(X1,X2),X1))=difference(X1,bigC(X1,X0,X2)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f5357,f926])).
% 82.21/10.84 fof(f6226,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),X2,product(difference(X0,X3),X4))=product(product(X3,product(X1,X4)),product(X2,product(X0,X1))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f96,f86])).
% 82.21/10.84 fof(f6236,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),product(difference(X0,X2),X3),X4)=product(product(X2,product(X1,X3)),product(X4,product(X0,X1))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f96,f18])).
% 82.21/10.84 fof(f6238,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(X2,product(X1,X3)))=product(difference(X0,X2),X3))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f96,f11])).
% 82.21/10.84 fof(f6303,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(product(X0,X1),bigC(quotient(X0,X2),X2,X2))=bigC(X2,X1,X0))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6305,f5374])).
% 82.21/10.84 fof(f6305,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),X2,product(difference(X0,X3),X4))=product(product(X3,X2),bigC(X1,X0,X4)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f347,f6226])).
% 82.21/10.84 fof(f6316,plain,(
% 82.21/10.84 ![X0,X1]: (product(product(X0,X1),bigC(quotient(X0,X1),X1,quotient(X0,X1)))=product(X1,X0))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6320,f5352])).
% 82.21/10.84 fof(f6320,plain,(
% 82.21/10.84 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),product(difference(X0,X2),X3),X4)=product(product(X2,X4),bigC(X1,X0,X3)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f347,f6236])).
% 82.21/10.84 fof(f6332,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,product(X2,quotient(X0,X2))))=bigC(X2,X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f1400,f6303])).
% 82.21/10.84 fof(f6333,plain,(
% 82.21/10.84 ![X0,X1]: (product(X0,product(X1,product(quotient(X0,X1),quotient(X0,X1))))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f1400,f6316])).
% 82.21/10.84 fof(f6337,plain,(
% 82.21/10.84 ![X0,X1]: (product(X0,product(X1,quotient(X0,X1)))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f6333])).
% 82.21/10.84 fof(f6354,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),product(X0,difference(X0,quotient(X1,X0))))=product(X0,difference(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f666,f6337])).
% 82.21/10.84 fof(f6363,plain,(
% 82.21/10.84 ![X0,X1]: (product(product(X0,X1),product(X1,X0))=product(X1,product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f13,f6337])).
% 82.21/10.84 fof(f6367,plain,(
% 82.21/10.84 ![X0,X1]: (product(X0,product(difference(X1,X0),X1))=product(difference(X1,X0),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f28,f6337])).
% 82.21/10.84 fof(f6424,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,product(X1,X0))=product(X1,quotient(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6337,f11])).
% 82.21/10.84 fof(f6426,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=product(X0,difference(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f777,f6354])).
% 82.21/10.84 fof(f6427,plain,(
% 82.21/10.84 ![X0,X1]: (X0=product(difference(X1,X0),quotient(X0,X1)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6428,f1652])).
% 82.21/10.84 fof(f6428,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=X1)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f12,f6426])).
% 82.21/10.84 fof(f6448,plain,(
% 82.21/10.84 ![X0,X1]: (bigC(X0,X1,X1)=product(X1,product(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f86,f6363])).
% 82.21/10.84 fof(f6457,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,bigC(X0,X1,X1))=product(difference(X0,X1),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f5404,f6367])).
% 82.21/10.84 fof(f6541,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X2,X0),quotient(bigC(X0,X1,X2),product(X0,X1))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f52,f6427])).
% 82.21/10.84 fof(f6563,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,quotient(X0,X2)))=product(product(X2,X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6427,f96])).
% 82.21/10.84 fof(f6600,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(X0,quotient(X0,X1))=difference(X1,X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6427,f13])).
% 82.21/10.84 fof(f6623,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(quotient(X0,X1),X1,X2)=product(product(X1,X2),X0))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6563,f44])).
% 82.21/10.84 fof(f6729,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=product(product(X0,X1),product(product(X3,X2),X0)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6623,f1400])).
% 82.21/10.84 fof(f6746,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(X0,product(product(X1,X2),X0))=product(X2,quotient(X0,X1)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6623,f230])).
% 82.21/10.84 fof(f6816,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,product(X1,X1),X2)=bigC(X1,X2,X0))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6817,f6332])).
% 82.21/10.84 fof(f6817,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=bigC(X0,product(X3,X2),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f86,f6729])).
% 82.21/10.84 fof(f6863,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(X2,quotient(product(X0,X1),X1)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6868,f619])).
% 82.21/10.84 fof(f6864,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(product(X2,X0),product(X3,X1)))=product(X3,quotient(product(X0,X1),X2)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f6868,f617])).
% 82.21/10.84 fof(f6868,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(difference(X0,product(X1,X2)),X0)=product(X2,quotient(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f547,f6746])).
% 82.21/10.84 fof(f6904,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X1,X2,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f16,f6816])).
% 82.21/10.84 fof(f6928,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(X2,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f13,f6863])).
% 82.21/10.84 fof(f6952,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X2,X1,X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f315,f6904])).
% 82.21/10.84 fof(f6954,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,difference(X0,X1),X2)=product(product(difference(X0,X1),X2),X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f49,f6904])).
% 82.21/10.84 fof(f6959,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X1,X0,X2))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f315,f6904])).
% 82.21/10.84 fof(f7032,plain,(
% 82.21/10.84 ![X0,X1,X2]: (quotient(bigC(X0,X1,X2),product(X0,X1))=product(X1,X2))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6904,f51])).
% 82.21/10.84 fof(f7038,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(difference(X0,X1),X2,X0)=product(X1,product(X2,X0)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f7058,f49])).
% 82.21/10.84 fof(f7058,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(product(difference(X2,X0),X1),X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f45,f6954])).
% 82.21/10.84 fof(f7072,plain,(
% 82.21/10.84 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X2,X0),product(X1,X2)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f7032,f6541])).
% 82.21/10.84 fof(f7130,plain,(
% 82.21/10.84 ![X0,X1,X2]: (quotient(product(X0,product(X1,X2)),X0)=product(difference(X2,X0),X1))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f7038,f215])).
% 82.21/10.84 fof(f7230,plain,(
% 82.21/10.84 ![X0,X1,X2]: (product(X0,quotient(product(X1,X2),X0))=product(difference(X2,X0),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f535,f7130])).
% 82.21/10.84 fof(f7455,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),X1)=difference(product(difference(X1,X0),X1),product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f629,f6600])).
% 82.21/10.84 fof(f7457,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),X0)=difference(X1,product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f13,f6600])).
% 82.21/10.84 fof(f7486,plain,(
% 82.21/10.84 ![X0,X1]: (X0=difference(product(difference(X1,X0),X1),product(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f13,f7455])).
% 82.21/10.84 fof(f9691,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),X0)=product(X1,quotient(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f547,f6424])).
% 82.21/10.84 fof(f9709,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(product(X2,X0),product(X3,X1)))=product(product(X2,X3),quotient(product(X0,X1),product(X2,X3))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f15,f6424])).
% 82.21/10.84 fof(f9743,plain,(
% 82.21/10.84 ![X0,X1]: (difference(difference(X0,quotient(product(X1,X0),X0)),product(X1,quotient(X0,X1)))=X0)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6424,f779])).
% 82.21/10.84 fof(f9744,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,quotient(product(X1,X0),X0))=quotient(product(X1,quotient(X0,X1)),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6424,f666])).
% 82.21/10.84 fof(f9788,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(difference(X0,product(X1,X0)),X1)=product(X1,quotient(quotient(X0,X1),X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6424,f535])).
% 82.21/10.84 fof(f9878,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (product(X0,quotient(product(X1,X2),X3))=product(product(X3,X0),quotient(product(X1,X2),product(X3,X0))))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f6864,f9709])).
% 82.21/10.84 fof(f9934,plain,(
% 82.21/10.84 ![X0,X1,X2,X3]: (product(X0,quotient(product(X1,X2),X3))=product(difference(X2,product(X3,X0)),X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f7230,f9878])).
% 82.21/10.84 fof(f10005,plain,(
% 82.21/10.84 ![X0,X1]: (difference(difference(X0,X1),product(X1,quotient(X0,X1)))=X0)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f13,f9743])).
% 82.21/10.84 fof(f10006,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,X1)=quotient(product(X1,quotient(X0,X1)),X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f13,f9744])).
% 82.21/10.84 fof(f10101,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(difference(X0,X1),X0),X1)=product(X1,quotient(quotient(X0,X1),X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f547,f9788])).
% 82.21/10.84 fof(f10364,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),X0)=product(difference(X1,X0),X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f7486,f28])).
% 82.21/10.84 fof(f10840,plain,(
% 82.21/10.84 ![X0,X1]: (product(X0,product(difference(X1,X0),X1))=product(product(X0,X1),quotient(product(difference(X1,X0),X1),product(X0,X1))))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f7486,f9691])).
% 82.21/10.84 fof(f10968,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,bigC(X0,X1,X1))=product(product(X1,X0),quotient(product(difference(X0,X1),X0),product(X1,X0))))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f5404,f10840])).
% 82.21/10.84 fof(f10969,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),X1)=product(product(X1,X0),quotient(product(difference(X0,X1),X0),product(X1,X0))))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f6457,f10968])).
% 82.21/10.84 fof(f10970,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),X1)=product(difference(X0,product(X1,X0)),difference(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f7230,f10969])).
% 82.21/10.84 fof(f10971,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),X1)=product(X0,quotient(product(difference(X0,X1),X0),X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f9934,f10970])).
% 82.21/10.84 fof(f11278,plain,(
% 82.21/10.84 ![X0,X1]: (difference(product(X0,X1),X0)=quotient(product(X0,difference(X1,product(X0,X1))),product(X0,X1)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f7457,f10006])).
% 82.21/10.84 fof(f11282,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,difference(X1,X0))=quotient(product(difference(X1,X0),X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f28,f10006])).
% 82.21/10.84 fof(f11310,plain,(
% 82.21/10.84 ![X0,X1]: (difference(product(X0,X1),X0)=quotient(product(X0,product(difference(X1,X0),X1)),product(X0,X1)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f547,f11278])).
% 82.21/10.84 fof(f11311,plain,(
% 82.21/10.84 ![X0,X1]: (difference(product(X0,X1),X0)=product(quotient(X0,X0),difference(X1,X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f4882,f11310])).
% 82.21/10.84 fof(f11318,plain,(
% 82.21/10.84 ![X0,X1]: (difference(product(X0,X1),X0)=product(X0,difference(X1,X0)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f29,f11311])).
% 82.21/10.84 fof(f11321,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),X1)=product(X0,difference(X1,difference(X0,X1))))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f11282,f10971])).
% 82.21/10.84 fof(f11322,plain,(
% 82.21/10.84 ![X0,X1]: (difference(X0,difference(X1,X0))=product(X0,quotient(quotient(X1,X0),X0)))),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f11282,f10101])).
% 82.21/10.84 fof(f11340,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,X1),difference(X0,difference(X1,X0)))=X0)),
% 82.21/10.84 inference(backward_demodulation,[status(thm)],[f11322,f4328])).
% 82.21/10.84 fof(f13265,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(X0,quotient(X0,X1)),difference(X0,X1))=X0)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f33,f11340])).
% 82.21/10.84 fof(f13946,plain,(
% 82.21/10.84 ![X0,X1]: (product(difference(product(X0,X1),product(X0,quotient(X1,X0))),difference(product(X0,X1),X0))=product(X0,X1))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f535,f13265])).
% 82.21/10.84 fof(f14074,plain,(
% 82.21/10.84 ![X0,X1]: (product(quotient(X0,X1),quotient(product(difference(product(X1,X0),X1),product(X1,X0)),X1))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f9934,f13946])).
% 82.21/10.84 fof(f14075,plain,(
% 82.21/10.84 ![X0,X1]: (product(quotient(X0,X1),difference(X1,difference(product(X1,X0),X1)))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f11282,f14074])).
% 82.21/10.84 fof(f14076,plain,(
% 82.21/10.84 ![X0,X1]: (product(quotient(X0,X1),difference(X1,product(X1,difference(X0,X1))))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f11318,f14075])).
% 82.21/10.84 fof(f14077,plain,(
% 82.21/10.84 ![X0,X1]: (product(quotient(X0,X1),difference(X0,X1))=product(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f11,f14076])).
% 82.21/10.84 fof(f15242,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),quotient(X1,X0))=product(difference(difference(X1,X0),quotient(X1,X0)),difference(X1,X0)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f14077,f10364])).
% 82.21/10.84 fof(f15272,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),product(difference(difference(X1,X0),quotient(X1,X0)),difference(X1,X0)))=difference(X1,X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f14077,f629])).
% 82.21/10.84 fof(f15440,plain,(
% 82.21/10.84 ![X0,X1]: (quotient(product(X0,X1),quotient(product(X0,X1),quotient(X1,X0)))=difference(X1,X0))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f15242,f15272])).
% 82.21/10.84 fof(f15441,plain,(
% 82.21/10.84 ![X0,X1]: (difference(quotient(X0,X1),product(X1,X0))=difference(X0,X1))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f6600,f15440])).
% 82.21/10.84 fof(f19251,plain,(
% 82.21/10.84 ![X0,X1,X2]: (difference(product(X0,X1),product(product(X1,X0),X2))=product(quotient(X2,X1),X0))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f333,f6928])).
% 82.21/10.84 fof(f26852,plain,(
% 82.21/10.84 difference(product(a,c),product(product(c,b),product(a,b)))=difference(product(a,b),product(c,b))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f566,f15441])).
% 82.21/10.84 fof(f26864,plain,(
% 82.21/10.84 difference(difference(product(a,b),product(c,b)),product(product(c,b),product(a,c)))=product(a,b)),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f566,f10005])).
% 82.21/10.84 fof(f26891,plain,(
% 82.21/10.84 difference(product(a,c),product(product(c,a),b))=difference(product(a,b),product(c,b))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f105,f26852])).
% 82.21/10.84 fof(f26893,plain,(
% 82.21/10.84 product(quotient(b,c),a)=difference(product(a,b),product(c,b))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f19251,f26891])).
% 82.21/10.84 fof(f26920,plain,(
% 82.21/10.84 difference(product(quotient(b,c),a),product(product(c,b),product(a,c)))=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f26893,f26864])).
% 82.21/10.84 fof(f26921,plain,(
% 82.21/10.84 product(difference(quotient(b,c),product(c,b)),c)=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f6238,f26920])).
% 82.21/10.84 fof(f26922,plain,(
% 82.21/10.84 product(b,quotient(product(c,quotient(b,c)),c))=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f9934,f26921])).
% 82.21/10.84 fof(f26923,plain,(
% 82.21/10.84 product(b,product(c,quotient(quotient(b,c),c)))=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f535,f26922])).
% 82.21/10.84 fof(f26924,plain,(
% 82.21/10.84 product(b,difference(c,difference(b,c)))=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f11322,f26923])).
% 82.21/10.84 fof(f26928,plain,(
% 82.21/10.84 product(difference(b,c),c)=product(a,b)),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f11321,f26924])).
% 82.21/10.84 fof(f41964,plain,(
% 82.21/10.84 ![X0]: (product(c,product(X0,c))=product(product(b,X0),product(a,b)))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f26928,f96])).
% 82.21/10.84 fof(f42039,plain,(
% 82.21/10.84 ![X0]: (bigC(X0,c,c)=product(product(b,X0),product(a,b)))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f6448,f41964])).
% 82.21/10.84 fof(f42041,plain,(
% 82.21/10.84 ![X0]: (bigC(X0,c,c)=bigC(X0,a,b))),
% 82.21/10.84 inference(forward_demodulation,[status(thm)],[f7072,f42039])).
% 82.21/10.84 fof(f42125,plain,(
% 82.21/10.84 ![X0]: (bigC(c,X0,c)=bigC(X0,a,b))),
% 82.21/10.84 inference(paramodulation,[status(thm)],[f6959,f42041])).
% 82.21/11.00 fof(f42127,plain,(
% 82.21/11.00 ![X0]: (bigC(c,c,X0)=bigC(X0,a,b))),
% 82.21/11.00 inference(paramodulation,[status(thm)],[f6952,f42041])).
% 82.21/11.00 fof(f43658,plain,(
% 82.21/11.00 ![X0]: (bigC(c,X0,c)=bigC(a,b,X0))),
% 82.21/11.00 inference(paramodulation,[status(thm)],[f6904,f42125])).
% 82.21/11.00 fof(f43981,plain,(
% 82.21/11.00 ![X0]: (bigC(c,c,X0)=bigC(c,X0,c))),
% 82.21/11.00 inference(paramodulation,[status(thm)],[f42125,f42127])).
% 82.21/11.00 fof(f44144,plain,(
% 82.21/11.00 ~bigC(a,b,x0)=bigC(a,b,x0)),
% 82.21/11.00 inference(backward_demodulation,[status(thm)],[f44172,f20])).
% 82.21/11.00 fof(f44172,plain,(
% 82.21/11.00 ![X0]: (bigC(c,c,X0)=bigC(a,b,X0))),
% 82.21/11.00 inference(forward_demodulation,[status(thm)],[f43658,f43981])).
% 82.21/11.00 fof(f44323,plain,(
% 82.21/11.00 $false),
% 82.21/11.00 inference(trivial_equality_resolution,[status(thm)],[f44144])).
% 82.21/11.00 % SZS output end CNFRefutation for theBenchmark.p
% 5.06/11.04 % Elapsed time: 10.691065 seconds
% 5.06/11.04 % CPU time: 84.497385 seconds
% 5.06/11.04 % Total memory used: 551.698 MB
% 5.06/11.04 % Net memory used: 532.729 MB
%------------------------------------------------------------------------------