%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP020+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:52:02 PM UTC 2026
% Result : Theorem 10.25s 1.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020+1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n016.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 21:56:53 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 10.25/1.79 % Refutation found
% 10.25/1.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.25/1.79 % SZS output start CNFRefutation for theBenchmark
% 10.25/1.79 fof(f2,axiom,(
% 10.25/1.79 (! [V0_2E0,V1_2E0] :( ( p(s(tyop_2Emin_2Ebool,V0_2E0))<=> p(s(tyop_2Emin_2Ebool,V1_2E0)) )=> s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) )),
% 10.25/1.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.79 fof(f4,axiom,(
% 10.25/1.79 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ),
% 10.25/1.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.79 fof(f47,axiom,(
% 10.25/1.79 (! [A_27a,A_27b,V0s_2E0,V1t_2E0] :( (? [V2f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))<=> (? [V3g_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))) )) )),
% 10.25/1.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.79 fof(f58,axiom,(
% 10.25/1.79 (? [V0f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))) )),
% 10.25/1.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.79 fof(f59,conjecture,(
% 10.25/1.79 (? [V0f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))) )),
% 10.25/1.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.25/1.79 fof(f60,negated_conjecture,(
% 10.25/1.79 ~((? [V0f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))) ))),
% 10.25/1.79 inference(negated_conjecture,[status(cth)],[f59])).
% 10.25/1.79 fof(f64,plain,(
% 10.25/1.79 ![V0_2E0,V1_2E0]: ((p(s(tyop_2Emin_2Ebool,V0_2E0))<~>p(s(tyop_2Emin_2Ebool,V1_2E0)))|s(tyop_2Emin_2Ebool,V0_2E0)=s(tyop_2Emin_2Ebool,V1_2E0))),
% 10.25/1.79 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 10.25/1.79 fof(f65,plain,(
% 10.25/1.79 ![V0_2E0,V1_2E0]: (((p(s(tyop_2Emin_2Ebool,V0_2E0))|p(s(tyop_2Emin_2Ebool,V1_2E0)))&(~p(s(tyop_2Emin_2Ebool,V0_2E0))|~p(s(tyop_2Emin_2Ebool,V1_2E0))))|s(tyop_2Emin_2Ebool,V0_2E0)=s(tyop_2Emin_2Ebool,V1_2E0))),
% 10.25/1.79 inference(NNF_transformation,[status(thm)],[f64])).
% 10.25/1.79 fof(f66,plain,(
% 10.25/1.79 ![X0,X1]: (p(s(tyop_2Emin_2Ebool,X0))|p(s(tyop_2Emin_2Ebool,X1))|s(tyop_2Emin_2Ebool,X0)=s(tyop_2Emin_2Ebool,X1))),
% 10.25/1.79 inference(cnf_transformation,[status(thm)],[f65])).
% 10.25/1.79 fof(f69,plain,(
% 10.25/1.79 ~p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 10.25/1.79 inference(cnf_transformation,[status(thm)],[f4])).
% 10.25/1.79 fof(f263,plain,(
% 10.25/1.79 ![A_27a,A_27b,V0s_2E0,V1t_2E0]: (((![V2f_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))|(?[V3g_2E0]: p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0))))))&((?[V2f_2E0]: p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))|(![V3g_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))))))),
% 10.25/1.79 inference(NNF_transformation,[status(thm)],[f47])).
% 10.25/1.79 fof(f264,plain,(
% 10.25/1.79 (![A_27a,A_27b,V0s_2E0,V1t_2E0]: ((![V2f_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))|(?[V3g_2E0]: p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))))))&(![A_27a,A_27b,V0s_2E0,V1t_2E0]: ((?[V2f_2E0]: p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))|(![V3g_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))))))),
% 10.25/1.79 inference(miniscoping,[status(thm)],[f263])).
% 10.25/1.79 fof(f265,plain,(
% 10.25/1.79 (![A_27a,A_27b,V0s_2E0,V1t_2E0]: ((![V2f_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))))|p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),sK25_skl(V1t_2E0,V0s_2E0,A_27b,A_27a)),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0))))))&(![A_27a,A_27b,V0s_2E0,V1t_2E0]: (p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),sK26_skl(V1t_2E0,V0s_2E0,A_27b,A_27a)),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0))))|(![V3g_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))))))),
% 10.25/1.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(V3g_2E0,sK25_skl(V1t_2E0,V0s_2E0,A_27b,A_27a)),skolemize(V2f_2E0,sK26_skl(V1t_2E0,V0s_2E0,A_27b,A_27a))],[f264])).
% 10.25/1.79 fof(f267,plain,(
% 10.25/1.79 ![X0,X1,X2,X3,X4]: (p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X0,X1),sK26_skl(X2,X3,X1,X0)),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2))))|~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(X1,X0),X4),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X2),s(tyop_2Emin_2Efun(X0,tyop_2Emin_2Ebool),X3)))))),
% 10.25/1.79 inference(cnf_transformation,[status(thm)],[f265])).
% 10.25/1.79 fof(f351,plain,(
% 10.25/1.79 p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),sK27_skl),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))))),
% 10.25/1.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(V0f_2E0,sK27_skl)],[f58])).
% 10.25/1.79 fof(f352,plain,(
% 10.25/1.79 p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),sK27_skl),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))))),
% 3.54/1.82 inference(cnf_transformation,[status(thm)],[f351])).
% 3.54/1.82 fof(f353,plain,(
% 3.54/1.82 (![V0f_2E0]: ~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))))),
% 3.54/1.82 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 3.54/1.82 fof(f354,plain,(
% 3.54/1.82 ![X0]: (~p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))))),
% 3.54/1.82 inference(cnf_transformation,[status(thm)],[f353])).
% 3.54/1.82 fof(f564,plain,(
% 3.54/1.82 ![X0,X1]: (p(s(tyop_2Emin_2Ebool,X0))|s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X1),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))=s(tyop_2Emin_2Ebool,X0))),
% 3.54/1.82 inference(resolution,[status(thm)],[f66,f354])).
% 3.54/1.82 fof(f607,plain,(
% 3.54/1.82 ![X0]: (s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))=s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 3.54/1.82 inference(resolution,[status(thm)],[f69,f564])).
% 3.54/1.82 fof(f3087,plain,(
% 3.54/1.82 p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),sK26_skl(c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)),c_2Epred__set_2EUNIV_2E0,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum)),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))))))),
% 3.54/1.82 inference(resolution,[status(thm)],[f267,f352])).
% 3.54/1.82 fof(f3110,plain,(
% 3.54/1.82 p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0))),
% 3.54/1.82 inference(forward_demodulation,[status(thm)],[f607,f3087])).
% 3.54/1.82 fof(f3111,plain,(
% 3.54/1.82 $false),
% 3.54/1.82 inference(forward_subsumption_resolution,[status(thm)],[f3110,f69])).
% 3.54/1.82 % SZS output end CNFRefutation for theBenchmark.p
% 3.54/1.83 % Elapsed time: 1.445659 seconds
% 3.54/1.83 % CPU time: 11.115886 seconds
% 3.54/1.83 % Total memory used: 265.050 MB
% 3.54/1.83 % Net memory used: 255.109 MB
%------------------------------------------------------------------------------