%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP777+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 : n010.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 : Theorem 124.63s 16.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP777+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 20:39:54 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 124.63/16.15 % Refutation found
% 124.63/16.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 124.63/16.15 % SZS output start CNFRefutation for theBenchmark
% 124.63/16.15 fof(f1,axiom,(
% 124.63/16.15 (! [B,A] : difference(A,product(A,B)) = B )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f2,axiom,(
% 124.63/16.15 (! [B,A] : product(A,difference(A,B)) = B )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f3,axiom,(
% 124.63/16.15 (! [B,A] : quotient(product(A,B),B) = A )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f4,axiom,(
% 124.63/16.15 (! [B,A] : product(quotient(A,B),B) = A )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f5,axiom,(
% 124.63/16.15 (! [D,C,B,A] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)) )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f6,axiom,(
% 124.63/16.15 (! [A] : product(A,A) = A )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f7,axiom,(
% 124.63/16.15 (! [B,A] : product(product(product(A,B),B),product(B,product(B,A))) = B )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f8,axiom,(
% 124.63/16.15 (! [C,B,A] : bigC(A,B,C) = product(product(A,B),product(C,A)) )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f9,axiom,(
% 124.63/16.15 product(product(a,c),product(c,b)) = product(a,b) ),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f10,conjecture,(
% 124.63/16.15 (! [X0] : bigC(a,b,X0) = bigC(c,c,X0) )),
% 124.63/16.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 124.63/16.15 fof(f11,negated_conjecture,(
% 124.63/16.15 ~((! [X0] : bigC(a,b,X0) = bigC(c,c,X0) ))),
% 124.63/16.15 inference(negated_conjecture,[status(cth)],[f10])).
% 124.63/16.15 fof(f12,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,product(X0,X1))=X1)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f1])).
% 124.63/16.15 fof(f13,plain,(
% 124.63/16.15 ![X0,X1]: (product(X0,difference(X0,X1))=X1)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f2])).
% 124.63/16.15 fof(f14,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),X1)=X0)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f3])).
% 124.63/16.15 fof(f15,plain,(
% 124.63/16.15 ![X0,X1]: (product(quotient(X0,X1),X1)=X0)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f4])).
% 124.63/16.15 fof(f16,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(product(X0,X1),product(X2,X3))=product(product(X0,X2),product(X1,X3)))),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f5])).
% 124.63/16.15 fof(f17,plain,(
% 124.63/16.15 ![X0]: (product(X0,X0)=X0)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f6])).
% 124.63/16.15 fof(f18,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(product(X0,X1),X1),product(X1,product(X1,X0)))=X1)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f7])).
% 124.63/16.15 fof(f19,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X0,X1),product(X2,X0)))),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f8])).
% 124.63/16.15 fof(f20,plain,(
% 124.63/16.15 product(product(a,c),product(c,b))=product(a,b)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f9])).
% 124.63/16.15 fof(f21,plain,(
% 124.63/16.15 (?[X0]: ~bigC(a,b,X0)=bigC(c,c,X0))),
% 124.63/16.15 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 124.63/16.15 fof(f22,plain,(
% 124.63/16.15 ~bigC(a,b,sK0_skl)=bigC(c,c,sK0_skl)),
% 124.63/16.15 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f21])).
% 124.63/16.15 fof(f23,plain,(
% 124.63/16.15 ~bigC(a,b,sK0_skl)=bigC(c,c,sK0_skl)),
% 124.63/16.15 inference(cnf_transformation,[status(thm)],[f22])).
% 124.63/16.15 fof(f31,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(X0,difference(X1,X0))=X1)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f14])).
% 124.63/16.15 fof(f32,plain,(
% 124.63/16.15 ![X0]: (quotient(X0,X0)=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f14])).
% 124.63/16.15 fof(f36,plain,(
% 124.63/16.15 ![X0,X1]: (difference(quotient(X0,X1),X0)=X1)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f12])).
% 124.63/16.15 fof(f47,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(quotient(X0,X1),X1,X2)=product(X0,product(X2,quotient(X0,X1))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f19])).
% 124.63/16.15 fof(f48,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,difference(X0,X1),X2)=product(X1,product(X2,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f19])).
% 124.63/16.15 fof(f49,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(X0,X0,X1)=product(X0,product(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f19])).
% 124.63/16.15 fof(f51,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,quotient(X2,X0))=product(product(X0,X1),X2))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f19])).
% 124.63/16.15 fof(f52,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(difference(X0,X1),X2,X0)=product(product(difference(X0,X1),X2),X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f19])).
% 124.63/16.15 fof(f53,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(X0,X1,X0)=product(product(X0,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f19])).
% 124.63/16.15 fof(f54,plain,(
% 124.63/16.15 ![X0,X1,X2]: (quotient(bigC(X0,X1,X2),product(X2,X0))=product(X0,X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f19,f14])).
% 124.63/16.15 fof(f55,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X0,X1,X2))=product(X2,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f19,f12])).
% 124.63/16.15 fof(f67,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,bigC(X0,X0,X1))=product(X1,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f49,f12])).
% 124.63/16.15 fof(f81,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(bigC(X0,X1,X0),X0)=product(X0,X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f53,f14])).
% 124.63/16.15 fof(f89,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X0,X2),product(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f19,f16])).
% 124.63/16.15 fof(f96,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(bigC(X0,X1,X0),product(X2,X3))=product(product(product(X0,X1),X2),product(X0,X3)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f53,f16])).
% 124.63/16.15 fof(f97,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,product(X1,X2))=product(product(quotient(X0,X3),X1),product(X3,X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f16])).
% 124.63/16.15 fof(f99,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,product(X1,X2))=product(product(X3,X1),product(difference(X3,X0),X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f16])).
% 124.63/16.15 fof(f100,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(product(X0,X1),product(X0,X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f16])).
% 124.63/16.15 fof(f108,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(product(X0,X2),product(X1,X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f16])).
% 124.63/16.15 fof(f134,plain,(
% 124.63/16.15 ![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)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f16,f53])).
% 124.63/16.15 fof(f161,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X3),product(X0,X1))=product(bigC(X0,X2,X0),product(product(X1,X3),X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f96,f134])).
% 124.63/16.15 fof(f163,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X3),product(X0,X1))=product(bigC(X0,X2,X0),bigC(X1,X3,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f53,f161])).
% 124.63/16.15 fof(f218,plain,(
% 124.63/16.15 ![X0,X1,X2]: (quotient(bigC(difference(X0,X1),X2,X0),X1)=product(difference(X0,X1),X2))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f54])).
% 124.63/16.15 fof(f233,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(X0,bigC(quotient(X0,X1),X1,X2))=product(X2,quotient(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f55])).
% 124.63/16.15 fof(f259,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(X0,X1),product(X1,product(X1,quotient(X0,X1))))=X1)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f18])).
% 124.63/16.15 fof(f318,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X0,X2,X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f19,f89])).
% 124.63/16.15 fof(f327,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,product(X2,X0))=product(bigC(X0,X0,X2),product(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f49,f89])).
% 124.63/16.15 fof(f328,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,difference(X0,X2))=product(X2,product(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f89])).
% 124.63/16.15 fof(f329,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(X0,X1,X0)=product(X0,product(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f89])).
% 124.63/16.15 fof(f335,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,product(X0,X1),X2)=product(product(X0,X2),bigC(X0,X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f53,f89])).
% 124.63/16.15 fof(f336,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,quotient(X1,X0),X2)=product(product(X0,X2),X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f89])).
% 124.63/16.15 fof(f339,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(X0,X0,X1)=product(product(X0,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f17,f89])).
% 124.63/16.15 fof(f350,plain,(
% 124.63/16.15 ![X0,X1,X2,X3,X4]: (product(product(X0,product(X1,X2)),product(X3,product(X4,X1)))=product(product(X0,X3),bigC(X1,X4,X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f89,f16])).
% 124.63/16.15 fof(f351,plain,(
% 124.63/16.15 ![X0,X1,X2,X3,X4]: (product(product(product(X0,X1),X2),product(product(X3,X0),X4))=product(bigC(X0,X3,X1),product(X2,X4)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f89,f16])).
% 124.63/16.15 fof(f354,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(X0,X1),product(X2,X0),product(X0,X1))=product(bigC(X0,X2,X1),product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f89,f53])).
% 124.63/16.15 fof(f359,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X0,X2,X1))=product(X2,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f89,f12])).
% 124.63/16.15 fof(f374,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(bigC(X0,X1,X0),bigC(X2,X0,X2))=product(bigC(X0,X1,X2),product(X0,X2)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f163,f354])).
% 124.63/16.15 fof(f389,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(bigC(X0,X0,X1),X0)=product(X0,X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f318,f81])).
% 124.63/16.15 fof(f390,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,bigC(X0,X1,X0))=product(X1,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f318,f67])).
% 124.63/16.15 fof(f530,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(product(X0,X0),X1),X0)=product(X0,quotient(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f51,f389])).
% 124.63/16.15 fof(f538,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),X0)=product(X0,quotient(X1,X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f530])).
% 124.63/16.15 fof(f542,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,product(X1,product(X0,X0)))=product(difference(X0,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f48,f390])).
% 124.63/16.15 fof(f550,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,product(X1,X0))=product(difference(X0,X1),X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f542])).
% 124.63/16.15 fof(f569,plain,(
% 124.63/16.15 quotient(product(a,b),product(c,b))=product(a,c)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f20,f14])).
% 124.63/16.15 fof(f601,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(X0,X1)=product(X1,quotient(difference(X1,X0),X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f538])).
% 124.63/16.15 fof(f605,plain,(
% 124.63/16.15 ![X0,X1]: (difference(product(X0,quotient(X1,X0)),product(X0,X1))=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f538,f36])).
% 124.63/16.15 fof(f620,plain,(
% 124.63/16.15 ![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)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f16,f550])).
% 124.63/16.15 fof(f622,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(difference(product(X0,X1),product(X1,X2)),product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f19,f550])).
% 124.63/16.15 fof(f625,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,X1)=product(difference(X0,quotient(X1,X0)),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f15,f550])).
% 124.63/16.15 fof(f632,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),product(difference(X1,X0),X1))=X1)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f550,f31])).
% 124.63/16.15 fof(f656,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(product(quotient(difference(X0,X1),X0),X0),X0),product(X0,quotient(X1,X0)))=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f601,f18])).
% 124.63/16.15 fof(f669,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,quotient(X1,X0))=quotient(difference(X0,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f601,f12])).
% 124.63/16.15 fof(f681,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(difference(X0,X1),X0),product(X0,quotient(X1,X0)))=X0)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f15,f656])).
% 124.63/16.15 fof(f780,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(difference(X0,quotient(X1,X0)),X0,X2)=product(difference(X0,X1),product(X2,difference(X0,quotient(X1,X0)))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f625,f19])).
% 124.63/16.15 fof(f782,plain,(
% 124.63/16.15 ![X0,X1]: (difference(difference(X0,quotient(X1,X0)),difference(X0,X1))=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f625,f12])).
% 124.63/16.15 fof(f860,plain,(
% 124.63/16.15 ~bigC(a,b,sK0_skl)=bigC(c,sK0_skl,c)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f318,f23])).
% 124.63/16.15 fof(f931,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(difference(X1,X2),X1))=product(X2,product(difference(X1,X0),X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f48,f328])).
% 124.63/16.15 fof(f1405,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=product(product(X0,X1),bigC(quotient(X0,X3),X3,X2)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f47,f100])).
% 124.63/16.15 fof(f1406,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,product(X2,X0)))=product(product(X0,X1),bigC(X0,X2,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f329,f100])).
% 124.63/16.15 fof(f1408,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,difference(X0,X2)))=product(product(X0,X1),X2))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13,f100])).
% 124.63/16.15 fof(f1472,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,product(X2,X0)))=bigC(X0,product(X0,X2),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f335,f1406])).
% 124.63/16.15 fof(f1539,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=product(difference(X0,X1),quotient(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f625,f52])).
% 124.63/16.15 fof(f2617,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X0)=product(bigC(X0,X0,X1),product(X2,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f339,f108])).
% 124.63/16.15 fof(f2688,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X1),X3)=product(product(product(X0,X1),X3),product(product(X2,X0),X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f108,f89])).
% 124.63/16.15 fof(f2722,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X0)=bigC(X0,X2,product(X1,X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f327,f2617])).
% 124.63/16.15 fof(f2787,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(bigC(X0,X1,X0),bigC(X2,X0,X2))=bigC(product(X0,X2),product(X1,X2),X0))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f2788,f374])).
% 124.63/16.15 fof(f2788,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (bigC(product(X0,X1),product(X2,X1),X3)=product(bigC(X0,X2,X1),product(X3,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f351,f2688])).
% 124.63/16.15 fof(f4234,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),product(X0,product(X0,quotient(difference(X0,quotient(X1,X0)),X0))))=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f625,f259])).
% 124.63/16.15 fof(f4335,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),product(X0,product(X0,difference(X0,quotient(quotient(X1,X0),X0)))))=X0)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f669,f4234])).
% 124.63/16.15 fof(f4336,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),product(product(X0,X0),quotient(quotient(X1,X0),X0)))=X0)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f1408,f4335])).
% 124.63/16.15 fof(f4337,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),product(X0,quotient(quotient(X1,X0),X0)))=X0)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f4336])).
% 124.63/16.15 fof(f4613,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (quotient(product(X0,product(X1,X2)),product(X3,X2))=product(quotient(X0,X3),X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f97,f14])).
% 124.63/16.15 fof(f5283,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(X0,bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0))))=product(X2,product(difference(X0,X1),X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f681,f359])).
% 124.63/16.15 fof(f5290,plain,(
% 124.63/16.15 ![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))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f681,f329])).
% 124.63/16.15 fof(f5292,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=product(X0,product(X2,product(difference(X0,X1),X0))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f681,f89])).
% 124.63/16.15 fof(f5301,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=product(product(product(X0,quotient(X1,X0)),X2),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f681,f19])).
% 124.63/16.15 fof(f5367,plain,(
% 124.63/16.15 ![X0,X1]: (product(bigC(X0,difference(X0,X1),X0),bigC(quotient(X1,X0),X0,quotient(X1,X0)))=product(product(X0,quotient(X1,X0)),X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f163,f5290])).
% 124.63/16.15 fof(f5368,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(product(X0,quotient(X1,X0)),X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f2787,f5367])).
% 124.63/16.15 fof(f5369,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=bigC(X0,X0,quotient(X1,X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f339,f5368])).
% 124.63/16.15 fof(f5370,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(product(X0,X0),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f51,f5369])).
% 124.63/16.15 fof(f5371,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(product(X0,quotient(X1,X0)),product(difference(X0,X1),quotient(X1,X0)),X0)=product(X0,X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f5370])).
% 124.63/16.15 fof(f5375,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=bigC(X0,product(X0,difference(X0,X1)),X2))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f1472,f5292])).
% 124.63/16.15 fof(f5376,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(X0,bigC(X0,X1,X2))=product(X2,product(difference(X0,X1),X0)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f5377,f5283])).
% 124.63/16.15 fof(f5377,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(difference(X0,X1),X0),X2,product(X0,quotient(X1,X0)))=bigC(X0,X1,X2))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f13,f5375])).
% 124.63/16.15 fof(f5390,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=bigC(X0,X2,product(quotient(X1,X0),X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f2722,f5301])).
% 124.63/16.15 fof(f5393,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(product(X0,quotient(X1,X0)),X2,product(difference(X0,X1),X0))=bigC(X0,X2,X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f15,f5390])).
% 124.63/16.15 fof(f5423,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(difference(X1,X2),X1))=difference(X1,bigC(X1,X0,X2)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f5376,f931])).
% 124.63/16.15 fof(f6027,plain,(
% 124.63/16.15 ![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))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f99,f89])).
% 124.63/16.15 fof(f6037,plain,(
% 124.63/16.15 ![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))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f99,f19])).
% 124.63/16.15 fof(f6039,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(X2,product(X1,X3)))=product(difference(X0,X2),X3))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f99,f12])).
% 124.63/16.15 fof(f6104,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(product(X0,X1),bigC(quotient(X0,X2),X2,X2))=bigC(X2,X1,X0))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6106,f5393])).
% 124.63/16.15 fof(f6106,plain,(
% 124.63/16.15 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),X2,product(difference(X0,X3),X4))=product(product(X3,X2),bigC(X1,X0,X4)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f350,f6027])).
% 124.63/16.15 fof(f6117,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(X0,X1),bigC(quotient(X0,X1),X1,quotient(X0,X1)))=product(X1,X0))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6121,f5371])).
% 124.63/16.15 fof(f6121,plain,(
% 124.63/16.15 ![X0,X1,X2,X3,X4]: (bigC(product(X0,X1),product(difference(X0,X2),X3),X4)=product(product(X2,X4),bigC(X1,X0,X3)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f350,f6037])).
% 124.63/16.15 fof(f6131,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,product(X2,quotient(X0,X2))))=bigC(X2,X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f1405,f6104])).
% 124.63/16.15 fof(f6132,plain,(
% 124.63/16.15 ![X0,X1]: (product(X0,product(X1,product(quotient(X0,X1),quotient(X0,X1))))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f1405,f6117])).
% 124.63/16.15 fof(f6136,plain,(
% 124.63/16.15 ![X0,X1]: (product(X0,product(X1,quotient(X0,X1)))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f6132])).
% 124.63/16.15 fof(f6151,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),product(X0,difference(X0,quotient(X1,X0))))=product(X0,difference(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f669,f6136])).
% 124.63/16.15 fof(f6160,plain,(
% 124.63/16.15 ![X0,X1]: (product(product(X0,X1),product(X1,X0))=product(X1,product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f14,f6136])).
% 124.63/16.15 fof(f6164,plain,(
% 124.63/16.15 ![X0,X1]: (product(X0,product(difference(X1,X0),X1))=product(difference(X1,X0),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f31,f6136])).
% 124.63/16.15 fof(f6222,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,product(X1,X0))=product(X1,quotient(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6136,f12])).
% 124.63/16.15 fof(f6224,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=product(X0,difference(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f780,f6151])).
% 124.63/16.15 fof(f6225,plain,(
% 124.63/16.15 ![X0,X1]: (X0=product(difference(X1,X0),quotient(X0,X1)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6226,f1539])).
% 124.63/16.15 fof(f6226,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(difference(X0,quotient(X1,X0)),X0,X0)=X1)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f13,f6224])).
% 124.63/16.15 fof(f6246,plain,(
% 124.63/16.15 ![X0,X1]: (bigC(X0,X1,X1)=product(X1,product(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f89,f6160])).
% 124.63/16.15 fof(f6255,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,bigC(X0,X1,X1))=product(difference(X0,X1),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f5423,f6164])).
% 124.63/16.15 fof(f6338,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X2,X0),quotient(bigC(X0,X1,X2),product(X0,X1))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f55,f6225])).
% 124.63/16.15 fof(f6360,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,quotient(X0,X2)))=product(product(X2,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6225,f99])).
% 124.63/16.15 fof(f6398,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(X0,quotient(X0,X1))=difference(X1,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6225,f14])).
% 124.63/16.15 fof(f6421,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(quotient(X0,X1),X1,X2)=product(product(X1,X2),X0))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6360,f47])).
% 124.63/16.15 fof(f6525,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=product(product(X0,X1),product(product(X3,X2),X0)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6421,f1405])).
% 124.63/16.15 fof(f6542,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(X0,product(product(X1,X2),X0))=product(X2,quotient(X0,X1)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6421,f233])).
% 124.63/16.15 fof(f6612,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,product(X1,X1),X2)=bigC(X1,X2,X0))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6613,f6131])).
% 124.63/16.15 fof(f6613,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,quotient(X0,X3))))=bigC(X0,product(X3,X2),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f89,f6525])).
% 124.63/16.15 fof(f6662,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(X2,quotient(product(X0,X1),X1)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6667,f622])).
% 124.63/16.15 fof(f6663,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (difference(product(X0,X1),product(product(X2,X0),product(X3,X1)))=product(X3,quotient(product(X0,X1),X2)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6667,f620])).
% 124.63/16.15 fof(f6667,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(difference(X0,product(X1,X2)),X0)=product(X2,quotient(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f550,f6542])).
% 124.63/16.15 fof(f6697,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=bigC(X1,X2,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f17,f6612])).
% 124.63/16.15 fof(f6728,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),bigC(X1,X2,X0))=product(X2,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f14,f6662])).
% 124.63/16.15 fof(f6753,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,difference(X0,X1),X2)=product(product(difference(X0,X1),X2),X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f52,f6697])).
% 124.63/16.15 fof(f6761,plain,(
% 124.63/16.15 ~bigC(a,b,sK0_skl)=bigC(sK0_skl,c,c)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6697,f860])).
% 124.63/16.15 fof(f6834,plain,(
% 124.63/16.15 ![X0,X1,X2]: (quotient(bigC(X0,X1,X2),product(X0,X1))=product(X1,X2))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6697,f54])).
% 124.63/16.15 fof(f6840,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(difference(X0,X1),X2,X0)=product(X1,product(X2,X0)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6860,f52])).
% 124.63/16.15 fof(f6860,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(product(difference(X2,X0),X1),X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f48,f6753])).
% 124.63/16.15 fof(f6874,plain,(
% 124.63/16.15 ![X0,X1,X2]: (bigC(X0,X1,X2)=product(product(X2,X0),product(X1,X2)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6834,f6338])).
% 124.63/16.15 fof(f6930,plain,(
% 124.63/16.15 ![X0,X1,X2]: (quotient(product(X0,product(X1,X2)),X0)=product(difference(X2,X0),X1))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f6840,f218])).
% 124.63/16.15 fof(f7030,plain,(
% 124.63/16.15 ![X0,X1,X2]: (product(X0,quotient(product(X1,X2),X0))=product(difference(X2,X0),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f538,f6930])).
% 124.63/16.15 fof(f7254,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),X1)=difference(product(difference(X1,X0),X1),product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f632,f6398])).
% 124.63/16.15 fof(f7256,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),X0)=difference(X1,product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f14,f6398])).
% 124.63/16.15 fof(f7286,plain,(
% 124.63/16.15 ![X0,X1]: (X0=difference(product(difference(X1,X0),X1),product(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f14,f7254])).
% 124.63/16.15 fof(f9506,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),X0)=product(X1,quotient(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f550,f6222])).
% 124.63/16.15 fof(f9524,plain,(
% 124.63/16.15 ![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))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f16,f6222])).
% 124.63/16.15 fof(f9558,plain,(
% 124.63/16.15 ![X0,X1]: (difference(difference(X0,quotient(product(X1,X0),X0)),product(X1,quotient(X0,X1)))=X0)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6222,f782])).
% 124.63/16.15 fof(f9559,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,quotient(product(X1,X0),X0))=quotient(product(X1,quotient(X0,X1)),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6222,f669])).
% 124.63/16.15 fof(f9605,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(difference(X0,product(X1,X0)),X1)=product(X1,quotient(quotient(X0,X1),X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f6222,f538])).
% 124.63/16.15 fof(f9697,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,quotient(product(X1,X2),X3))=product(product(X3,X0),quotient(product(X1,X2),product(X3,X0))))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f6663,f9524])).
% 124.63/16.15 fof(f9748,plain,(
% 124.63/16.15 ![X0,X1,X2,X3]: (product(X0,quotient(product(X1,X2),X3))=product(difference(X2,product(X3,X0)),X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f7030,f9697])).
% 124.63/16.15 fof(f9817,plain,(
% 124.63/16.15 ![X0,X1]: (difference(difference(X0,X1),product(X1,quotient(X0,X1)))=X0)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f14,f9558])).
% 124.63/16.15 fof(f9818,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,X1)=quotient(product(X1,quotient(X0,X1)),X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f14,f9559])).
% 124.63/16.15 fof(f9915,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(difference(X0,X1),X0),X1)=product(X1,quotient(quotient(X0,X1),X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f550,f9605])).
% 124.63/16.15 fof(f10162,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),X0)=product(difference(X1,X0),X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f7286,f31])).
% 124.63/16.15 fof(f10644,plain,(
% 124.63/16.15 ![X0,X1]: (product(X0,product(difference(X1,X0),X1))=product(product(X0,X1),quotient(product(difference(X1,X0),X1),product(X0,X1))))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f7286,f9506])).
% 124.63/16.15 fof(f10776,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,bigC(X0,X1,X1))=product(product(X1,X0),quotient(product(difference(X0,X1),X0),product(X1,X0))))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f5423,f10644])).
% 124.63/16.15 fof(f10777,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),X1)=product(product(X1,X0),quotient(product(difference(X0,X1),X0),product(X1,X0))))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f6255,f10776])).
% 124.63/16.15 fof(f10778,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),X1)=product(difference(X0,product(X1,X0)),difference(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f7030,f10777])).
% 124.63/16.15 fof(f10779,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),X1)=product(X0,quotient(product(difference(X0,X1),X0),X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f9748,f10778])).
% 124.63/16.15 fof(f11088,plain,(
% 124.63/16.15 ![X0,X1]: (difference(product(X0,X1),X0)=quotient(product(X0,difference(X1,product(X0,X1))),product(X0,X1)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f7256,f9818])).
% 124.63/16.15 fof(f11092,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,difference(X1,X0))=quotient(product(difference(X1,X0),X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f31,f9818])).
% 124.63/16.15 fof(f11119,plain,(
% 124.63/16.15 ![X0,X1]: (difference(product(X0,X1),X0)=quotient(product(X0,product(difference(X1,X0),X1)),product(X0,X1)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f550,f11088])).
% 124.63/16.15 fof(f11120,plain,(
% 124.63/16.15 ![X0,X1]: (difference(product(X0,X1),X0)=product(quotient(X0,X0),difference(X1,X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f4613,f11119])).
% 124.63/16.15 fof(f11127,plain,(
% 124.63/16.15 ![X0,X1]: (difference(product(X0,X1),X0)=product(X0,difference(X1,X0)))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f32,f11120])).
% 124.63/16.15 fof(f11130,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),X1)=product(X0,difference(X1,difference(X0,X1))))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f11092,f10779])).
% 124.63/16.15 fof(f11131,plain,(
% 124.63/16.15 ![X0,X1]: (difference(X0,difference(X1,X0))=product(X0,quotient(quotient(X1,X0),X0)))),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f11092,f9915])).
% 124.63/16.15 fof(f11153,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(X0,X1),difference(X0,difference(X1,X0)))=X0)),
% 124.63/16.15 inference(backward_demodulation,[status(thm)],[f11131,f4337])).
% 124.63/16.15 fof(f13425,plain,(
% 124.63/16.15 ![X0,X1]: (product(difference(product(X0,X1),product(X0,quotient(X1,X0))),difference(product(X0,X1),X0))=product(X0,X1))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f605,f11153])).
% 124.63/16.15 fof(f13543,plain,(
% 124.63/16.15 ![X0,X1]: (product(quotient(X0,X1),quotient(product(difference(product(X1,X0),X1),product(X1,X0)),X1))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f9748,f13425])).
% 124.63/16.15 fof(f13544,plain,(
% 124.63/16.15 ![X0,X1]: (product(quotient(X0,X1),difference(X1,difference(product(X1,X0),X1)))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f11092,f13543])).
% 124.63/16.15 fof(f13545,plain,(
% 124.63/16.15 ![X0,X1]: (product(quotient(X0,X1),difference(X1,product(X1,difference(X0,X1))))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f11127,f13544])).
% 124.63/16.15 fof(f13546,plain,(
% 124.63/16.15 ![X0,X1]: (product(quotient(X0,X1),difference(X0,X1))=product(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f12,f13545])).
% 124.63/16.15 fof(f14182,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),quotient(X1,X0))=product(difference(difference(X1,X0),quotient(X1,X0)),difference(X1,X0)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13546,f10162])).
% 124.63/16.15 fof(f14212,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),product(difference(difference(X1,X0),quotient(X1,X0)),difference(X1,X0)))=difference(X1,X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f13546,f632])).
% 124.63/16.15 fof(f14361,plain,(
% 124.63/16.15 ![X0,X1]: (quotient(product(X0,X1),quotient(product(X0,X1),quotient(X1,X0)))=difference(X1,X0))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f14182,f14212])).
% 124.63/16.15 fof(f14363,plain,(
% 124.63/16.15 ![X0,X1]: (difference(quotient(X0,X1),product(X1,X0))=difference(X0,X1))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f6398,f14361])).
% 124.63/16.15 fof(f19113,plain,(
% 124.63/16.15 ![X0,X1,X2]: (difference(product(X0,X1),product(product(X1,X0),X2))=product(quotient(X2,X1),X0))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f336,f6728])).
% 124.63/16.15 fof(f26668,plain,(
% 124.63/16.15 difference(product(a,c),product(product(c,b),product(a,b)))=difference(product(a,b),product(c,b))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f569,f14363])).
% 124.63/16.15 fof(f26677,plain,(
% 124.63/16.15 difference(difference(product(a,b),product(c,b)),product(product(c,b),product(a,c)))=product(a,b)),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f569,f9817])).
% 124.63/16.15 fof(f26706,plain,(
% 124.63/16.15 difference(product(a,c),product(product(c,a),b))=difference(product(a,b),product(c,b))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f108,f26668])).
% 124.63/16.15 fof(f26708,plain,(
% 124.63/16.15 product(quotient(b,c),a)=difference(product(a,b),product(c,b))),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f19113,f26706])).
% 124.63/16.15 fof(f26734,plain,(
% 124.63/16.15 difference(product(quotient(b,c),a),product(product(c,b),product(a,c)))=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f26708,f26677])).
% 124.63/16.15 fof(f26735,plain,(
% 124.63/16.15 product(difference(quotient(b,c),product(c,b)),c)=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f6039,f26734])).
% 124.63/16.15 fof(f26736,plain,(
% 124.63/16.15 product(b,quotient(product(c,quotient(b,c)),c))=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f9748,f26735])).
% 124.63/16.15 fof(f26737,plain,(
% 124.63/16.15 product(b,product(c,quotient(quotient(b,c),c)))=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f538,f26736])).
% 124.63/16.15 fof(f26738,plain,(
% 124.63/16.15 product(b,difference(c,difference(b,c)))=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f11131,f26737])).
% 124.63/16.15 fof(f26742,plain,(
% 124.63/16.15 product(difference(b,c),c)=product(a,b)),
% 124.63/16.15 inference(forward_demodulation,[status(thm)],[f11130,f26738])).
% 124.63/16.15 fof(f41027,plain,(
% 124.63/16.15 ![X0]: (product(c,product(X0,c))=product(product(b,X0),product(a,b)))),
% 124.63/16.15 inference(paramodulation,[status(thm)],[f26742,f99])).
% 121.47/16.29 fof(f41104,plain,(
% 121.47/16.29 ![X0]: (bigC(X0,c,c)=product(product(b,X0),product(a,b)))),
% 121.47/16.29 inference(forward_demodulation,[status(thm)],[f6246,f41027])).
% 121.47/16.29 fof(f41105,plain,(
% 121.47/16.29 ~bigC(a,b,sK0_skl)=bigC(sK0_skl,a,b)),
% 121.47/16.29 inference(backward_demodulation,[status(thm)],[f41110,f6761])).
% 121.47/16.29 fof(f41110,plain,(
% 121.47/16.29 ![X0]: (bigC(X0,c,c)=bigC(X0,a,b))),
% 121.47/16.29 inference(forward_demodulation,[status(thm)],[f6874,f41104])).
% 121.47/16.29 fof(f41186,plain,(
% 121.47/16.29 $false),
% 121.47/16.29 inference(forward_subsumption_resolution,[status(thm)],[f41105,f6697])).
% 121.47/16.29 % SZS output end CNFRefutation for theBenchmark.p
% 31.61/16.34 % Elapsed time: 15.953159 seconds
% 31.61/16.34 % CPU time: 126.258567 seconds
% 31.61/16.34 % Total memory used: 767.810 MB
% 31.61/16.34 % Net memory used: 722.622 MB
%------------------------------------------------------------------------------