%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP005+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:51:47 PM UTC 2026
% Result : Theorem 169.65s 22.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ITP005+4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.39 % Computer : n020.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 20 21:42:02 UTC 2026
% 0.12/0.40 % CPUTime :
% 1.25/1.55 % Drodi V4.1.1
% 169.65/22.90 % Refutation found
% 169.65/22.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 169.65/22.90 % SZS output start CNFRefutation for theBenchmark
% 169.65/22.90 fof(f1307,axiom,(
% 169.65/22.90 (! [A_27a,A_27b,X0_2E0] : s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),X0_2E0))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),X0_2E0))) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f1314,axiom,(
% 169.65/22.90 (! [A_27a,A_27b,A_27c,X0_2E0] : s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),A_27c),X0_2E0))) = s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),A_27c),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c))),c_2Epair_2ECURRY_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),A_27c),X0_2E0))) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f1401,axiom,(
% 169.65/22.90 (! [A_27a,A_27b,A_27c,V0f_2E0] : s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),A_27c),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0))))) = s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f4978,axiom,(
% 169.65/22.90 (! [A_27a,A_27b,X0_2E0] : s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),X0_2E0))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),X0_2E0))) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f4979,axiom,(
% 169.65/22.90 (! [A_27a,A_27b,X0_2E0] : s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),X0_2E0))) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f5132,axiom,(
% 169.65/22.90 (! [A_27a,A_27b] : s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0) = s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f5133,axiom,(
% 169.65/22.90 (! [A_27a,A_27b] : s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0) = s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool))),c_2Epair_2ECURRY_2E0) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f5134,conjecture,(
% 169.65/22.90 (! [A_27a,A_27b,V0R_2E0] : s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0))))) = s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0) )),
% 169.65/22.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.65/22.90 fof(f5135,negated_conjecture,(
% 169.65/22.90 ~((! [A_27a,A_27b,V0R_2E0] : s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0))))) = s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0) ))),
% 169.65/22.90 inference(negated_conjecture,[status(cth)],[f5134])).
% 169.65/22.90 fof(f9415,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2)))=s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2))))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f1307])).
% 169.65/22.90 fof(f9422,plain,(
% 169.65/22.90 ![X0,X1,X2,X3]: (s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),X2),X3)))=s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),X2),tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2))),c_2Epair_2ECURRY_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),X2),X3))))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f1314])).
% 169.65/22.90 fof(f9563,plain,(
% 169.65/22.90 ![X0,X1,X2,X3]: (s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),X2),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),X3)))))=s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,X2)),X3))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f1401])).
% 169.65/22.90 fof(f19301,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2)))=s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2))))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f4978])).
% 169.65/22.90 fof(f19302,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2)))=s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2))))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f4979])).
% 169.65/22.90 fof(f19740,plain,(
% 169.65/22.90 ![X0,X1]: (s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool)),c_2Eset__relation_2Erel__to__reln_2E0)=s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f5132])).
% 169.65/22.90 fof(f19741,plain,(
% 169.65/22.90 ![X0,X1]: (s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))),c_2Eset__relation_2Ereln__to__rel_2E0)=s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))),c_2Epair_2ECURRY_2E0))),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f5133])).
% 169.65/22.90 fof(f19742,plain,(
% 169.65/22.90 (?[A_27a,A_27b,V0R_2E0]: ~s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(A_27a,A_27b),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0)))))=s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0R_2E0))),
% 169.65/22.90 inference(pre_NNF_transformation,[status(thm)],[f5135])).
% 169.65/22.90 fof(f19743,plain,(
% 169.65/22.90 ~s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(sK2264_skl,sK2265_skl),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)))))=s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)),
% 169.65/22.90 inference(skolemize,[status(esa),new_symbols(skolem,[sK2264_skl,sK2265_skl,sK2266_skl]),skolemize(A_27a,sK2264_skl),skolemize(A_27b,sK2265_skl),skolemize(V0R_2E0,sK2266_skl)],[f19742])).
% 169.65/22.90 fof(f19744,plain,(
% 169.65/22.90 ~s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(sK2264_skl,sK2265_skl),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)))))=s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)),
% 169.65/22.90 inference(cnf_transformation,[status(thm)],[f19743])).
% 169.65/22.90 fof(f28330,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2)))=s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool)),c_2Epair_2EUNCURRY_2E0),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2))))),
% 169.65/22.90 inference(backward_demodulation,[status(thm)],[f19740,f19301])).
% 169.65/22.90 fof(f28331,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2)))=s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool))),c_2Epair_2ECURRY_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2))))),
% 169.65/22.90 inference(backward_demodulation,[status(thm)],[f19741,f19302])).
% 169.65/22.90 fof(f29071,plain,(
% 169.65/22.90 ~s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(sK2264_skl,sK2265_skl),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)))))=s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)),
% 169.65/22.90 inference(backward_demodulation,[status(thm)],[f29074,f19744])).
% 169.65/22.90 fof(f29074,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),c_2Eset__relation_2Erel__to__reln_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2)))=s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),X2))))),
% 169.65/22.90 inference(forward_demodulation,[status(thm)],[f9415,f28330])).
% 169.65/22.90 fof(f29076,plain,(
% 169.65/22.90 ![X0,X1,X2]: (s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Eset__relation_2Ereln__to__rel_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2)))=s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(X0,X1),tyop_2Emin_2Ebool),X2))))),
% 44.15/23.18 inference(forward_demodulation,[status(thm)],[f9422,f28331])).
% 44.15/23.18 fof(f29138,plain,(
% 44.15/23.18 ~s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),c_2Epair_2ECURRY_2E1(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(sK2264_skl,sK2265_skl),tyop_2Emin_2Ebool),c_2Epair_2EUNCURRY_2E1(s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)))))=s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)),
% 44.15/23.18 inference(forward_demodulation,[status(thm)],[f29076,f29071])).
% 44.15/23.18 fof(f29139,plain,(
% 44.15/23.18 ~s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)=s(tyop_2Emin_2Efun(sK2264_skl,tyop_2Emin_2Efun(sK2265_skl,tyop_2Emin_2Ebool)),sK2266_skl)),
% 44.15/23.18 inference(forward_demodulation,[status(thm)],[f9563,f29138])).
% 44.15/23.18 fof(f29140,plain,(
% 44.15/23.18 $false),
% 44.15/23.18 inference(trivial_equality_resolution,[status(thm)],[f29139])).
% 44.15/23.18 % SZS output end CNFRefutation for theBenchmark.p
% 44.15/23.23 % Elapsed time: 22.813975 seconds
% 44.15/23.23 % CPU time: 171.845707 seconds
% 44.15/23.23 % Total memory used: 3.018 GB
% 44.15/23.23 % Net memory used: 2.987 GB
%------------------------------------------------------------------------------