%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT131+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 02:07:21 PM UTC 2026
% Result : Theorem 41.26s 5.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT131+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 04:31:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.46 % Drodi V4.1.1
% 41.26/5.78 % Refutation found
% 41.26/5.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 41.26/5.78 % SZS output start CNFRefutation for theBenchmark
% 41.26/5.78 fof(f2,axiom,(
% 41.26/5.78 c_Arrow__Order__Mirabelle_Ounanimity(v_F) ),
% 41.26/5.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.78 fof(f6,axiom,(
% 41.26/5.78 (! [V_i_2] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_Q____,V_i_2))) )),
% 41.26/5.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.78 fof(f31,axiom,(
% 41.26/5.78 (! [V_A_2,V_x_2,T_a] :( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))<=> hBOOL(hAPP(V_A_2,V_x_2)) ) )),
% 41.26/5.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.78 fof(f32,axiom,(
% 41.26/5.78 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)) ),
% 41.26/5.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.79 fof(f47,axiom,(
% 41.26/5.79 (! [V_Fa_2] :( c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)<=> (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))=> (! [B_a,B_b] :( (! [B_i] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x))) ) )) )) )),
% 41.26/5.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.79 fof(f535,conjecture,(
% 41.26/5.79 hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))) ),
% 41.26/5.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 41.26/5.79 fof(f536,negated_conjecture,(
% 41.26/5.79 ~(hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))) )),
% 41.26/5.79 inference(negated_conjecture,[status(cth)],[f535])).
% 41.26/5.79 fof(f540,plain,(
% 41.26/5.79 c_Arrow__Order__Mirabelle_Ounanimity(v_F)),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f2])).
% 41.26/5.79 fof(f544,plain,(
% 41.26/5.79 ![X0]: (hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_Q____,X0))))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f6])).
% 41.26/5.79 fof(f628,plain,(
% 41.26/5.79 ![V_A_2,V_x_2,T_a]: ((~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|hBOOL(hAPP(V_A_2,V_x_2)))&(hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 41.26/5.79 inference(NNF_transformation,[status(thm)],[f31])).
% 41.26/5.79 fof(f629,plain,(
% 41.26/5.79 (![V_A_2,V_x_2]: ((![T_a]: ~hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)))|hBOOL(hAPP(V_A_2,V_x_2))))&(![V_A_2,V_x_2]: ((![T_a]: hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 41.26/5.79 inference(miniscoping,[status(thm)],[f628])).
% 41.26/5.79 fof(f630,plain,(
% 41.26/5.79 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hBOOL(hAPP(X2,X1)))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f629])).
% 41.26/5.79 fof(f631,plain,(
% 41.26/5.79 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|~hBOOL(hAPP(X2,X1)))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f629])).
% 41.26/5.79 fof(f632,plain,(
% 41.26/5.79 hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f32])).
% 41.26/5.79 fof(f720,plain,(
% 41.26/5.79 ![V_Fa_2]: (c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)<=>(![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))|(![B_a,B_b]: ((?[B_i]: ~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x))))))))),
% 41.26/5.79 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 41.26/5.79 fof(f721,plain,(
% 41.26/5.79 ![V_Fa_2]: ((~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))|(![B_a,B_b]: ((?[B_i]: ~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x))))))))&(c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))&(?[B_a,B_b]: ((![B_i]: hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))&~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x)))))))))),
% 41.26/5.79 inference(NNF_transformation,[status(thm)],[f720])).
% 41.26/5.79 fof(f722,plain,(
% 41.26/5.79 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))|(![B_a,B_b]: ((?[B_i]: ~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x)))))))))&(![V_Fa_2]: (c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))&(?[B_a,B_b]: ((![B_i]: hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))))&~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x)))))))))),
% 41.26/5.79 inference(miniscoping,[status(thm)],[f721])).
% 41.26/5.79 fof(f723,plain,(
% 41.26/5.79 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))|(![B_a,B_b]: (~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,sK6_skl(B_b,B_a,B_x,V_Fa_2))))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x)))))))))&(![V_Fa_2]: (c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK7_skl(V_Fa_2)),c_Arrow__Order__Mirabelle_OProf))&((![B_i]: hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK8_skl(V_Fa_2)),sK9_skl(V_Fa_2))),hAPP(sK7_skl(V_Fa_2),B_i))))&~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK8_skl(V_Fa_2)),sK9_skl(V_Fa_2))),hAPP(V_Fa_2,sK7_skl(V_Fa_2))))))))),
% 41.26/5.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(B_i,sK6_skl(B_b,B_a,B_x,V_Fa_2)),skolemize(B_x,sK7_skl(V_Fa_2)),skolemize(B_a,sK8_skl(V_Fa_2)),skolemize(B_b,sK9_skl(V_Fa_2))],[f722])).
% 41.26/5.79 fof(f724,plain,(
% 41.26/5.79 ![X0,X1,X2,X3]: (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_Arrow__Order__Mirabelle_OProf))|~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X3)),hAPP(X1,sK6_skl(X3,X2,X1,X0))))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X3)),hAPP(X0,X1))))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f723])).
% 41.26/5.79 fof(f2191,plain,(
% 41.26/5.79 ~hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____)))),
% 41.26/5.79 inference(cnf_transformation,[status(thm)],[f536])).
% 41.26/5.79 fof(f2293,plain,(
% 41.26/5.79 hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_Q____))),
% 41.26/5.79 inference(resolution,[status(thm)],[f632,f630])).
% 41.26/5.79 fof(f2298,plain,(
% 41.26/5.79 ![X0]: (hBOOL(hAPP(hAPP(c_member(X0),v_Q____),c_Arrow__Order__Mirabelle_OProf)))),
% 41.26/5.79 inference(resolution,[status(thm)],[f2293,f631])).
% 41.26/5.79 fof(f4239,plain,(
% 41.26/5.79 ![X0]: (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf))|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(X0,v_Q____))))),
% 41.26/5.79 inference(resolution,[status(thm)],[f724,f544])).
% 41.26/5.79 fof(f4242,definition,(
% 41.26/5.79 ![X0]: (sQ144_spl <=> (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(X0,v_Q____)))))),
% 41.26/5.79 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 41.26/5.79 fof(f4243,plain,(
% 41.26/5.79 ![X0]: (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(X0,v_Q____)))|~sQ144_spl)),
% 36.62/5.82 inference(component_clause,[status(thm)],[f4242])).
% 36.62/5.82 fof(f4245,definition,(
% 36.62/5.82 sQ145_spl <=> (hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)))),
% 36.62/5.82 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 36.62/5.82 fof(f4247,plain,(
% 36.62/5.82 ~hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf))|sQ145_spl),
% 36.62/5.82 inference(component_clause,[status(thm)],[f4245])).
% 36.62/5.82 fof(f4248,plain,(
% 36.62/5.82 sQ144_spl|~sQ145_spl),
% 36.62/5.82 inference(split_clause,[status(thm)],[f4239,f4242,f4245])).
% 36.62/5.82 fof(f4619,plain,(
% 36.62/5.82 $false|sQ145_spl),
% 36.62/5.82 inference(forward_subsumption_resolution,[status(thm)],[f4247,f2298])).
% 36.62/5.82 fof(f4620,plain,(
% 36.62/5.82 sQ145_spl),
% 36.62/5.82 inference(contradiction_clause,[status(thm)],[f4619])).
% 36.62/5.82 fof(f14029,plain,(
% 36.62/5.82 hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____)))|~sQ144_spl),
% 36.62/5.82 inference(resolution,[status(thm)],[f4243,f540])).
% 36.62/5.82 fof(f14030,plain,(
% 36.62/5.82 $false|~sQ144_spl),
% 36.62/5.82 inference(forward_subsumption_resolution,[status(thm)],[f14029,f2191])).
% 36.62/5.82 fof(f14031,plain,(
% 36.62/5.82 ~sQ144_spl),
% 36.62/5.82 inference(contradiction_clause,[status(thm)],[f14030])).
% 36.62/5.82 fof(f14032,plain,(
% 36.62/5.82 $false),
% 36.62/5.82 inference(sat_refutation,[status(thm)],[f4248,f4620,f14031])).
% 36.62/5.82 % SZS output end CNFRefutation for theBenchmark.p
% 36.62/5.86 % Elapsed time: 5.470049 seconds
% 36.62/5.86 % CPU time: 42.361044 seconds
% 36.62/5.86 % Total memory used: 522.512 MB
% 36.62/5.86 % Net memory used: 493.250 MB
%------------------------------------------------------------------------------