%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP774+1 : TPTP v9.3.1. Released v4.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:18 PM UTC 2026
% Result : Theorem 11.95s 6.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP774+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n020.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 20 20:40:22 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 11.95/6.94 % Refutation found
% 11.95/6.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.95/6.94 % SZS output start CNFRefutation for theBenchmark
% 11.95/6.94 fof(f1,axiom,(
% 11.95/6.94 (! [C,B,A] : product(product(A,B),C) = product(A,product(B,C)) )),
% 11.95/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.95/6.94 fof(f2,axiom,(
% 11.95/6.94 (! [A] : product(A,A) = A )),
% 11.95/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.95/6.94 fof(f3,axiom,(
% 11.95/6.94 (! [X0,X1] :( d(X0,X1)<=> ( product(X0,product(X1,X0)) = X0& product(X1,product(X0,X1)) = X1 ) ) )),
% 11.95/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.95/6.94 fof(f4,conjecture,(
% 11.95/6.94 (! [X2,X3,X4,X5] :( ( d(X2,X3)& d(X4,X5) )=> d(product(X2,X4),product(X3,X5)) ) )),
% 11.95/6.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.95/6.94 fof(f5,negated_conjecture,(
% 11.95/6.94 ~((! [X2,X3,X4,X5] :( ( d(X2,X3)& d(X4,X5) )=> d(product(X2,X4),product(X3,X5)) ) ))),
% 11.95/6.94 inference(negated_conjecture,[status(cth)],[f4])).
% 11.95/6.94 fof(f6,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(X0,product(X1,X2)))),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f1])).
% 11.95/6.94 fof(f7,plain,(
% 11.95/6.94 ![X0]: (product(X0,X0)=X0)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f2])).
% 11.95/6.94 fof(f8,plain,(
% 11.95/6.94 ![X0,X1]: ((~d(X0,X1)|(product(X0,product(X1,X0))=X0&product(X1,product(X0,X1))=X1))&(d(X0,X1)|(~product(X0,product(X1,X0))=X0|~product(X1,product(X0,X1))=X1)))),
% 11.95/6.94 inference(NNF_transformation,[status(thm)],[f3])).
% 11.95/6.94 fof(f9,plain,(
% 11.95/6.94 (![X0,X1]: (~d(X0,X1)|(product(X0,product(X1,X0))=X0&product(X1,product(X0,X1))=X1)))&(![X0,X1]: (d(X0,X1)|(~product(X0,product(X1,X0))=X0|~product(X1,product(X0,X1))=X1)))),
% 11.95/6.94 inference(miniscoping,[status(thm)],[f8])).
% 11.95/6.94 fof(f10,plain,(
% 11.95/6.94 ![X0,X1]: (~d(X0,X1)|product(X0,product(X1,X0))=X0)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f9])).
% 11.95/6.94 fof(f11,plain,(
% 11.95/6.94 ![X0,X1]: (~d(X0,X1)|product(X1,product(X0,X1))=X1)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f9])).
% 11.95/6.94 fof(f12,plain,(
% 11.95/6.94 ![X0,X1]: (d(X0,X1)|~product(X0,product(X1,X0))=X0|~product(X1,product(X0,X1))=X1)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f9])).
% 11.95/6.94 fof(f13,plain,(
% 11.95/6.94 (?[X2,X3,X4,X5]: ((d(X2,X3)&d(X4,X5))&~d(product(X2,X4),product(X3,X5))))),
% 11.95/6.94 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 11.95/6.94 fof(f14,plain,(
% 11.95/6.94 ((d(sK0_skl,sK1_skl)&d(sK2_skl,sK3_skl))&~d(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl)))),
% 11.95/6.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(X2,sK0_skl),skolemize(X3,sK1_skl),skolemize(X4,sK2_skl),skolemize(X5,sK3_skl)],[f13])).
% 11.95/6.94 fof(f15,plain,(
% 11.95/6.94 d(sK0_skl,sK1_skl)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f14])).
% 11.95/6.94 fof(f16,plain,(
% 11.95/6.94 d(sK2_skl,sK3_skl)),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f14])).
% 11.95/6.94 fof(f17,plain,(
% 11.95/6.94 ~d(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl))),
% 11.95/6.94 inference(cnf_transformation,[status(thm)],[f14])).
% 11.95/6.94 fof(f18,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,X1)=product(X0,product(X1,product(X0,X1))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f7,f6])).
% 11.95/6.94 fof(f20,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,X1)=product(X0,product(X0,X1)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f7,f6])).
% 11.95/6.94 fof(f24,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(X0,product(X1,product(product(X0,X1),X2))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f6,f20])).
% 11.95/6.94 fof(f30,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(X1,product(product(X0,X1),X2))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f24])).
% 11.95/6.94 fof(f31,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(X1,product(X0,product(X1,X2)))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f30])).
% 11.95/6.94 fof(f38,plain,(
% 11.95/6.94 product(sK2_skl,product(sK3_skl,sK2_skl))=sK2_skl),
% 11.95/6.94 inference(resolution,[status(thm)],[f10,f16])).
% 11.95/6.94 fof(f39,plain,(
% 11.95/6.94 product(sK0_skl,product(sK1_skl,sK0_skl))=sK0_skl),
% 11.95/6.94 inference(resolution,[status(thm)],[f10,f15])).
% 11.95/6.94 fof(f40,plain,(
% 11.95/6.94 product(sK3_skl,product(sK2_skl,sK3_skl))=sK3_skl),
% 11.95/6.94 inference(resolution,[status(thm)],[f11,f16])).
% 11.95/6.94 fof(f41,plain,(
% 11.95/6.94 product(sK1_skl,product(sK0_skl,sK1_skl))=sK1_skl),
% 11.95/6.94 inference(resolution,[status(thm)],[f11,f15])).
% 11.95/6.94 fof(f43,plain,(
% 11.95/6.94 ![X0]: (product(sK2_skl,X0)=product(sK2_skl,product(product(sK3_skl,sK2_skl),X0)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f38,f6])).
% 11.95/6.94 fof(f45,plain,(
% 11.95/6.94 ![X0]: (product(sK2_skl,X0)=product(sK2_skl,product(sK3_skl,product(sK2_skl,X0))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f43])).
% 11.95/6.94 fof(f47,plain,(
% 11.95/6.94 ![X0]: (product(sK0_skl,X0)=product(sK0_skl,product(product(sK1_skl,sK0_skl),X0)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f39,f6])).
% 11.95/6.94 fof(f49,plain,(
% 11.95/6.94 ![X0]: (product(sK0_skl,X0)=product(sK0_skl,product(sK1_skl,product(sK0_skl,X0))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f47])).
% 11.95/6.94 fof(f51,plain,(
% 11.95/6.94 ![X0]: (product(sK3_skl,X0)=product(sK3_skl,product(product(sK2_skl,sK3_skl),X0)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f40,f6])).
% 11.95/6.94 fof(f53,plain,(
% 11.95/6.94 ![X0]: (product(sK3_skl,X0)=product(sK3_skl,product(sK2_skl,product(sK3_skl,X0))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f51])).
% 11.95/6.94 fof(f55,plain,(
% 11.95/6.94 ![X0]: (product(sK1_skl,X0)=product(sK1_skl,product(product(sK0_skl,sK1_skl),X0)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f41,f6])).
% 11.95/6.94 fof(f57,plain,(
% 11.95/6.94 ![X0]: (product(sK1_skl,X0)=product(sK1_skl,product(sK0_skl,product(sK1_skl,X0))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f55])).
% 11.95/6.94 fof(f58,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(X0,product(X1,product(X2,product(product(X0,X1),X2)))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f6,f18])).
% 11.95/6.94 fof(f78,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(X1,product(X2,product(product(X0,X1),X2)))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f58])).
% 11.95/6.94 fof(f79,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(X1,product(X2,product(X0,product(X1,X2))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f78])).
% 11.95/6.94 fof(f113,plain,(
% 11.95/6.94 ~product(product(sK0_skl,sK2_skl),product(product(sK1_skl,sK3_skl),product(sK0_skl,sK2_skl)))=product(sK0_skl,sK2_skl)|~product(product(sK1_skl,sK3_skl),product(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl)))=product(sK1_skl,sK3_skl)),
% 11.95/6.94 inference(resolution,[status(thm)],[f12,f17])).
% 11.95/6.94 fof(f116,definition,(
% 11.95/6.94 sQ0_spl <=> (product(product(sK0_skl,sK2_skl),product(product(sK1_skl,sK3_skl),product(sK0_skl,sK2_skl)))=product(sK0_skl,sK2_skl))),
% 11.95/6.94 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 11.95/6.94 fof(f118,plain,(
% 11.95/6.94 ~product(product(sK0_skl,sK2_skl),product(product(sK1_skl,sK3_skl),product(sK0_skl,sK2_skl)))=product(sK0_skl,sK2_skl)|sQ0_spl),
% 11.95/6.94 inference(component_clause,[status(thm)],[f116])).
% 11.95/6.94 fof(f119,definition,(
% 11.95/6.94 sQ1_spl <=> (product(product(sK1_skl,sK3_skl),product(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl)))=product(sK1_skl,sK3_skl))),
% 11.95/6.94 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 11.95/6.94 fof(f121,plain,(
% 11.95/6.94 ~product(product(sK1_skl,sK3_skl),product(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl)))=product(sK1_skl,sK3_skl)|sQ1_spl),
% 11.95/6.94 inference(component_clause,[status(thm)],[f119])).
% 11.95/6.94 fof(f122,plain,(
% 11.95/6.94 ~sQ0_spl|~sQ1_spl),
% 11.95/6.94 inference(split_clause,[status(thm)],[f113,f116,f119])).
% 11.95/6.94 fof(f123,plain,(
% 11.95/6.94 ~product(sK0_skl,product(sK2_skl,product(product(sK1_skl,sK3_skl),product(sK0_skl,sK2_skl))))=product(sK0_skl,sK2_skl)|sQ0_spl),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f118])).
% 11.95/6.94 fof(f124,plain,(
% 11.95/6.94 ~product(sK0_skl,product(sK2_skl,product(sK1_skl,product(sK3_skl,product(sK0_skl,sK2_skl)))))=product(sK0_skl,sK2_skl)|sQ0_spl),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f123])).
% 11.95/6.94 fof(f225,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(product(X0,X1),product(X2,X3))=product(X0,product(X1,product(X2,product(product(X0,X1),product(X2,X3))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f6,f31])).
% 11.95/6.94 fof(f278,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,X3)))=product(X0,product(X1,product(X2,product(product(X0,X1),product(X2,X3))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f225])).
% 11.95/6.94 fof(f279,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,X3)))=product(X0,product(X1,product(X2,product(X0,product(X1,product(X2,X3)))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f278])).
% 11.95/6.94 fof(f328,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(product(X0,X1),product(X2,X3))=product(X0,product(X1,product(X2,product(X3,product(product(X0,X1),product(X2,X3)))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f6,f79])).
% 11.95/6.94 fof(f403,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,X3)))=product(X0,product(X1,product(X2,product(X3,product(product(X0,X1),product(X2,X3)))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f328])).
% 11.95/6.94 fof(f404,plain,(
% 11.95/6.94 ![X0,X1,X2,X3]: (product(X0,product(X1,product(X2,X3)))=product(X0,product(X1,product(X2,product(X3,product(X0,product(X1,product(X2,X3))))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f403])).
% 11.95/6.94 fof(f1748,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK1_skl,product(sK0_skl,product(sK1_skl,X1))))=product(X0,product(sK1_skl,product(sK0_skl,product(X0,product(sK1_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f57,f279])).
% 11.95/6.94 fof(f1752,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,product(sK2_skl,product(sK3_skl,X1))))=product(X0,product(sK3_skl,product(sK2_skl,product(X0,product(sK3_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f53,f279])).
% 11.95/6.94 fof(f1753,plain,(
% 11.95/6.94 ![X0]: (product(X0,product(sK3_skl,product(sK2_skl,sK3_skl)))=product(X0,product(sK3_skl,product(sK2_skl,product(X0,sK3_skl)))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f40,f279])).
% 11.95/6.94 fof(f1756,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK0_skl,product(sK1_skl,product(sK0_skl,X1))))=product(X0,product(sK0_skl,product(sK1_skl,product(X0,product(sK0_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f49,f279])).
% 11.95/6.94 fof(f1760,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK2_skl,product(sK3_skl,product(sK2_skl,X1))))=product(X0,product(sK2_skl,product(sK3_skl,product(X0,product(sK2_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f45,f279])).
% 11.95/6.94 fof(f1761,plain,(
% 11.95/6.94 ![X0]: (product(X0,product(sK2_skl,product(sK3_skl,sK2_skl)))=product(X0,product(sK2_skl,product(sK3_skl,product(X0,sK2_skl)))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f38,f279])).
% 11.95/6.94 fof(f1771,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(product(X1,X2),product(X1,X2)))=product(X0,product(product(X1,X2),product(X1,product(X0,product(X1,X2))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f7,f279])).
% 11.95/6.94 fof(f1922,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK1_skl,X1))=product(X0,product(sK1_skl,product(sK0_skl,product(X0,product(sK1_skl,X1))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f57,f1748])).
% 11.95/6.94 fof(f1926,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(sK3_skl,product(sK2_skl,product(X0,product(sK3_skl,X1))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f53,f1752])).
% 11.95/6.94 fof(f1927,plain,(
% 11.95/6.94 ![X0]: (product(X0,sK3_skl)=product(X0,product(sK3_skl,product(sK2_skl,product(X0,sK3_skl)))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f40,f1753])).
% 11.95/6.94 fof(f1930,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK0_skl,X1))=product(X0,product(sK0_skl,product(sK1_skl,product(X0,product(sK0_skl,X1))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f49,f1756])).
% 11.95/6.94 fof(f1934,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK2_skl,X1))=product(X0,product(sK2_skl,product(sK3_skl,product(X0,product(sK2_skl,X1))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f45,f1760])).
% 11.95/6.94 fof(f1935,plain,(
% 11.95/6.94 ![X0]: (product(X0,sK2_skl)=product(X0,product(sK2_skl,product(sK3_skl,product(X0,sK2_skl)))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f38,f1761])).
% 11.95/6.94 fof(f1947,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,product(X2,product(X1,X2))))=product(X0,product(product(X1,X2),product(X1,product(X0,product(X1,X2))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f1771])).
% 11.95/6.94 fof(f1948,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(product(X1,X2),product(X1,product(X0,product(X1,X2))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f18,f1947])).
% 11.95/6.94 fof(f1949,plain,(
% 11.95/6.94 ![X0,X1,X2]: (product(X0,product(X1,X2))=product(X0,product(X1,product(X2,product(X1,product(X0,product(X1,X2)))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f1948])).
% 11.95/6.94 fof(f3788,plain,(
% 11.95/6.94 ![X0]: (product(X0,product(sK3_skl,product(X0,product(sK2_skl,product(X0,sK3_skl)))))=product(X0,product(sK3_skl,product(sK2_skl,product(X0,sK3_skl)))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f1949,f1926])).
% 11.95/6.94 fof(f3884,plain,(
% 11.95/6.94 ![X0]: (product(X0,product(sK3_skl,product(X0,product(sK2_skl,product(X0,sK3_skl)))))=product(X0,sK3_skl))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f1927,f3788])).
% 11.95/6.94 fof(f4073,plain,(
% 11.95/6.94 ![X0]: (product(sK3_skl,product(X0,product(sK2_skl,product(X0,sK3_skl))))=product(sK3_skl,product(X0,sK3_skl)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f3884,f31])).
% 11.95/6.94 fof(f4090,plain,(
% 11.95/6.94 ![X0,X1]: (product(product(X0,sK3_skl),X1)=product(X0,product(product(sK3_skl,product(X0,product(sK2_skl,product(X0,sK3_skl)))),X1)))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f3884,f6])).
% 11.95/6.94 fof(f4220,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(product(sK3_skl,product(X0,product(sK2_skl,product(X0,sK3_skl)))),X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f4090])).
% 11.95/6.94 fof(f4221,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(sK3_skl,product(product(X0,product(sK2_skl,product(X0,sK3_skl))),X1))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f4220])).
% 11.95/6.94 fof(f4222,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(sK3_skl,product(X0,product(product(sK2_skl,product(X0,sK3_skl)),X1)))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f4221])).
% 11.95/6.94 fof(f4223,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(sK3_skl,product(X0,product(sK2_skl,product(product(X0,sK3_skl),X1))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f4222])).
% 11.95/6.94 fof(f4224,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK3_skl,X1))=product(X0,product(sK3_skl,product(X0,product(sK2_skl,product(X0,product(sK3_skl,X1)))))))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f4223])).
% 11.95/6.94 fof(f5184,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK0_skl,product(X1,product(sK1_skl,product(X0,product(sK0_skl,X1))))))=product(X0,product(sK0_skl,product(sK1_skl,product(X0,product(sK0_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f404,f1930])).
% 11.95/6.94 fof(f5195,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK1_skl,product(X1,product(sK0_skl,product(X0,product(sK1_skl,X1))))))=product(X0,product(sK1_skl,product(sK0_skl,product(X0,product(sK1_skl,X1))))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f404,f1922])).
% 11.95/6.94 fof(f5881,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK0_skl,product(X1,product(sK1_skl,product(X0,product(sK0_skl,X1))))))=product(X0,product(sK0_skl,X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f1930,f5184])).
% 11.95/6.94 fof(f5896,plain,(
% 11.95/6.94 ![X0,X1]: (product(X0,product(sK1_skl,product(X1,product(sK0_skl,product(X0,product(sK1_skl,X1))))))=product(X0,product(sK1_skl,X1)))),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f1922,f5195])).
% 11.95/6.94 fof(f24371,plain,(
% 11.95/6.94 product(sK0_skl,product(sK2_skl,product(sK1_skl,product(sK3_skl,product(sK0_skl,sK2_skl)))))=product(sK0_skl,product(sK2_skl,product(sK3_skl,product(sK0_skl,sK2_skl))))),
% 11.95/6.94 inference(paramodulation,[status(thm)],[f5881,f1934])).
% 11.95/6.94 fof(f24997,plain,(
% 11.95/6.94 product(sK0_skl,product(sK2_skl,product(sK1_skl,product(sK3_skl,product(sK0_skl,sK2_skl)))))=product(sK0_skl,sK2_skl)),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f1935,f24371])).
% 11.95/6.94 fof(f24998,plain,(
% 11.95/6.94 $false|sQ0_spl),
% 11.95/6.94 inference(forward_subsumption_resolution,[status(thm)],[f24997,f124])).
% 11.95/6.94 fof(f24999,plain,(
% 11.95/6.94 sQ0_spl),
% 11.95/6.94 inference(contradiction_clause,[status(thm)],[f24998])).
% 11.95/6.94 fof(f25352,plain,(
% 11.95/6.94 ~product(sK1_skl,product(sK3_skl,product(product(sK0_skl,sK2_skl),product(sK1_skl,sK3_skl))))=product(sK1_skl,sK3_skl)|sQ1_spl),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f121])).
% 11.95/6.94 fof(f25353,plain,(
% 11.95/6.94 ~product(sK1_skl,product(sK3_skl,product(sK0_skl,product(sK2_skl,product(sK1_skl,sK3_skl)))))=product(sK1_skl,sK3_skl)|sQ1_spl),
% 11.95/6.94 inference(forward_demodulation,[status(thm)],[f6,f25352])).
% 11.95/6.94 fof(f25834,plain,(
% 11.95/6.94 product(sK1_skl,product(sK3_skl,product(sK0_skl,product(sK2_skl,product(sK1_skl,sK3_skl)))))=product(sK1_skl,product(sK3_skl,product(sK1_skl,product(sK2_skl,product(sK1_skl,sK3_skl)))))),
% 11.95/6.97 inference(paramodulation,[status(thm)],[f5896,f4224])).
% 11.95/6.97 fof(f26519,plain,(
% 11.95/6.97 product(sK1_skl,product(sK3_skl,product(sK0_skl,product(sK2_skl,product(sK1_skl,sK3_skl)))))=product(sK1_skl,product(sK3_skl,product(sK1_skl,sK3_skl)))),
% 11.95/6.97 inference(forward_demodulation,[status(thm)],[f4073,f25834])).
% 11.95/6.97 fof(f26520,plain,(
% 11.95/6.97 product(sK1_skl,product(sK3_skl,product(sK0_skl,product(sK2_skl,product(sK1_skl,sK3_skl)))))=product(sK1_skl,sK3_skl)),
% 11.95/6.97 inference(forward_demodulation,[status(thm)],[f18,f26519])).
% 11.95/6.97 fof(f26521,plain,(
% 11.95/6.97 $false|sQ1_spl),
% 11.95/6.97 inference(forward_subsumption_resolution,[status(thm)],[f26520,f25353])).
% 11.95/6.97 fof(f26522,plain,(
% 11.95/6.97 sQ1_spl),
% 11.95/6.97 inference(contradiction_clause,[status(thm)],[f26521])).
% 11.95/6.97 fof(f26523,plain,(
% 11.95/6.97 $false),
% 11.95/6.97 inference(sat_refutation,[status(thm)],[f122,f24999,f26522])).
% 11.95/6.97 % SZS output end CNFRefutation for theBenchmark.p
% 11.95/7.00 % Elapsed time: 1.607416 seconds
% 11.95/7.00 % CPU time: 12.497009 seconds
% 11.95/7.00 % Total memory used: 245.220 MB
% 11.95/7.00 % Net memory used: 240.348 MB
%------------------------------------------------------------------------------