%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT135+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 : n015.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 0.13s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT135+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n015.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 21 04:37:07 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.50 % Refutation found
% 0.13/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.50 fof(f2,axiom,(
% 0.13/0.50 c_Arrow__Order__Mirabelle_OIIA(v_F) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f4,axiom,(
% 0.13/0.50 v_a____ != v_b____ ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f5,axiom,(
% 0.13/0.50 v_a____ != v_b_H____ ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f6,axiom,(
% 0.13/0.50 v_b____ != v_a_H____ ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f7,axiom,(
% 0.13/0.50 v_a_H____ != v_b_H____ ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f8,axiom,(
% 0.13/0.50 (! [B_i] :( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f9,axiom,(
% 0.13/0.50 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_P____,c_Arrow__Order__Mirabelle_OProf) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f10,axiom,(
% 0.13/0.50 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_P_H____,c_Arrow__Order__Mirabelle_OProf) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f14,axiom,(
% 0.13/0.50 (! [V_P_Ha_2,V_Pa_2,V_b_Ha_2,V_a_Ha_2,V_ba_2,V_aa_2] :( V_aa_2 != V_ba_2=> ( V_a_Ha_2 != V_b_Ha_2=> ( V_aa_2 != V_b_Ha_2=> ( V_ba_2 != V_a_Ha_2=> ( 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_Pa_2,c_Arrow__Order__Mirabelle_OProf)=> ( 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_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)=> ( (! [B_i] :( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)) ))=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) ) ) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f15,axiom,(
% 0.13/0.50 (! [V_y_2,V_x_2,V_R_2,T_b,T_a] :( hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(T_a,T_b,V_R_2),V_x_2),V_y_2))<=> c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f24,axiom,(
% 0.13/0.50 (! [V_A_2,V_x_2,T_a] :( c_member(T_a,V_x_2,V_A_2)<=> hBOOL(hAPP(V_A_2,V_x_2)) ) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f26,axiom,(
% 0.13/0.50 (! [V_Fa_2] :( c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)<=> (! [B_x] :( 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_xa] :( 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_xa,c_Arrow__Order__Mirabelle_OProf)=> (! [B_a,B_b] :( (! [B_i] :( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)) ))=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)) ) ) )) )) )) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f27,axiom,(
% 0.13/0.50 (! [V_Fa_2] :( c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)<=> (! [B_x] :( 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] : c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_x)) ) )) )) )),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f521,conjecture,(
% 0.13/0.50 ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ) ),
% 0.13/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.50 fof(f522,negated_conjecture,(
% 0.13/0.50 ~(( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))<=> c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)) ) )),
% 0.13/0.50 inference(negated_conjecture,[status(cth)],[f521])).
% 0.13/0.50 fof(f526,plain,(
% 0.13/0.50 c_Arrow__Order__Mirabelle_OIIA(v_F)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.50 fof(f528,plain,(
% 0.13/0.50 ~v_a____=v_b____),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.50 fof(f529,plain,(
% 0.13/0.50 ~v_a____=v_b_H____),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.50 fof(f530,plain,(
% 0.13/0.50 ~v_b____=v_a_H____),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.50 fof(f531,plain,(
% 0.13/0.50 ~v_a_H____=v_b_H____),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.50 fof(f532,plain,(
% 0.13/0.50 ![B_i]: ((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i))))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f8])).
% 0.13/0.50 fof(f533,plain,(
% 0.13/0.50 (![B_i]: (~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i))))&(![B_i]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,B_i))))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f532])).
% 0.13/0.50 fof(f534,plain,(
% 0.13/0.50 ![X0]: (~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,X0))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,X0)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f533])).
% 0.13/0.50 fof(f535,plain,(
% 0.13/0.50 ![X0]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,X0))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,X0)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f533])).
% 0.13/0.50 fof(f536,plain,(
% 0.13/0.50 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_P____,c_Arrow__Order__Mirabelle_OProf)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.50 fof(f537,plain,(
% 0.13/0.50 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_P_H____,c_Arrow__Order__Mirabelle_OProf)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.50 fof(f564,plain,(
% 0.13/0.50 ![V_P_Ha_2,V_Pa_2,V_b_Ha_2,V_a_Ha_2,V_ba_2,V_aa_2]: (V_aa_2=V_ba_2|(V_a_Ha_2=V_b_Ha_2|(V_aa_2=V_b_Ha_2|(V_ba_2=V_a_Ha_2|(~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_Pa_2,c_Arrow__Order__Mirabelle_OProf)|(~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_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)|((?[B_i]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))<~>c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i))))|(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2))))))))))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.13/0.50 fof(f565,plain,(
% 0.13/0.50 ![V_P_Ha_2,V_Pa_2,V_b_Ha_2,V_a_Ha_2,V_ba_2,V_aa_2]: (V_aa_2=V_ba_2|(V_a_Ha_2=V_b_Ha_2|(V_aa_2=V_b_Ha_2|(V_ba_2=V_a_Ha_2|(~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_Pa_2,c_Arrow__Order__Mirabelle_OProf)|(~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_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)|((?[B_i]: ((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)))))|(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2))))))))))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f564])).
% 0.13/0.50 fof(f566,plain,(
% 0.13/0.50 ![V_ba_2,V_aa_2]: (V_aa_2=V_ba_2|(![V_b_Ha_2,V_a_Ha_2]: (V_a_Ha_2=V_b_Ha_2|(V_aa_2=V_b_Ha_2|(V_ba_2=V_a_Ha_2|(![V_Pa_2]: (~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_Pa_2,c_Arrow__Order__Mirabelle_OProf)|(![V_P_Ha_2]: (~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_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)|((?[B_i]: ((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,B_i)))))|(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)))))))))))))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f565])).
% 0.13/0.50 fof(f567,plain,(
% 0.13/0.50 ![V_ba_2,V_aa_2]: (V_aa_2=V_ba_2|(![V_b_Ha_2,V_a_Ha_2]: (V_a_Ha_2=V_b_Ha_2|(V_aa_2=V_b_Ha_2|(V_ba_2=V_a_Ha_2|(![V_Pa_2]: (~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_Pa_2,c_Arrow__Order__Mirabelle_OProf)|(![V_P_Ha_2]: (~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_P_Ha_2,c_Arrow__Order__Mirabelle_OProf)|(((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,sK1_skl(V_P_Ha_2,V_Pa_2,V_a_Ha_2,V_b_Ha_2,V_aa_2,V_ba_2)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,sK1_skl(V_P_Ha_2,V_Pa_2,V_a_Ha_2,V_b_Ha_2,V_aa_2,V_ba_2))))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(V_Pa_2,sK1_skl(V_P_Ha_2,V_Pa_2,V_a_Ha_2,V_b_Ha_2,V_aa_2,V_ba_2)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(V_P_Ha_2,sK1_skl(V_P_Ha_2,V_Pa_2,V_a_Ha_2,V_b_Ha_2,V_aa_2,V_ba_2)))))|(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_aa_2,V_ba_2),hAPP(v_F,V_Pa_2))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,V_a_Ha_2,V_b_Ha_2),hAPP(v_F,V_P_Ha_2)))))))))))))),
% 0.13/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_i,sK1_skl(V_P_Ha_2,V_Pa_2,V_a_Ha_2,V_b_Ha_2,V_aa_2,V_ba_2))],[f566])).
% 0.13/0.50 fof(f568,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4,X5]: (X0=X1|X2=X3|X0=X3|X1=X2|~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)),X4,c_Arrow__Order__Mirabelle_OProf)|~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)),X5,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X4,sK1_skl(X5,X4,X2,X3,X0,X1)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X5,sK1_skl(X5,X4,X2,X3,X0,X1)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X4))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X5)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f567])).
% 0.13/0.50 fof(f569,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4,X5]: (X0=X1|X2=X3|X0=X3|X1=X2|~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)),X4,c_Arrow__Order__Mirabelle_OProf)|~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)),X5,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X4,sK1_skl(X5,X4,X2,X3,X0,X1)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X5,sK1_skl(X5,X4,X2,X3,X0,X1)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X4))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X5)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f567])).
% 0.13/0.50 fof(f570,plain,(
% 0.13/0.50 ![V_y_2,V_x_2,V_R_2,T_b,T_a]: ((~hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(T_a,T_b,V_R_2),V_x_2),V_y_2))|c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2))&(hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(T_a,T_b,V_R_2),V_x_2),V_y_2))|~c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f15])).
% 0.13/0.50 fof(f571,plain,(
% 0.13/0.50 (![V_y_2,V_x_2,V_R_2,T_b,T_a]: (~hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(T_a,T_b,V_R_2),V_x_2),V_y_2))|c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)))&(![V_y_2,V_x_2,V_R_2,T_b,T_a]: (hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(T_a,T_b,V_R_2),V_x_2),V_y_2))|~c_member(tc_prod(T_a,T_b),c_Product__Type_OPair(T_a,T_b,V_x_2,V_y_2),V_R_2)))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f570])).
% 0.13/0.50 fof(f572,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(X0,X1,X2),X3),X4))|c_member(tc_prod(X0,X1),c_Product__Type_OPair(X0,X1,X3,X4),X2))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f571])).
% 0.13/0.50 fof(f573,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(X0,X1,X2),X3),X4))|~c_member(tc_prod(X0,X1),c_Product__Type_OPair(X0,X1,X3,X4),X2))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f571])).
% 0.13/0.50 fof(f609,plain,(
% 0.13/0.50 ![V_A_2,V_x_2,T_a]: ((~c_member(T_a,V_x_2,V_A_2)|hBOOL(hAPP(V_A_2,V_x_2)))&(c_member(T_a,V_x_2,V_A_2)|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f24])).
% 0.13/0.50 fof(f610,plain,(
% 0.13/0.50 (![V_A_2,V_x_2]: ((![T_a]: ~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]: c_member(T_a,V_x_2,V_A_2))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f609])).
% 0.13/0.50 fof(f611,plain,(
% 0.13/0.50 ![X0,X1,X2]: (~c_member(X0,X1,X2)|hBOOL(hAPP(X2,X1)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f610])).
% 0.13/0.50 fof(f612,plain,(
% 0.13/0.50 ![X0,X1,X2]: (c_member(X0,X1,X2)|~hBOOL(hAPP(X2,X1)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f610])).
% 0.13/0.50 fof(f614,plain,(
% 0.13/0.50 ![V_Fa_2]: (c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)<=>(![B_x]: (~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_xa]: (~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_xa,c_Arrow__Order__Mirabelle_OProf)|(![B_a,B_b]: ((?[B_i]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))<~>c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i))))|(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa))))))))))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.13/0.50 fof(f615,plain,(
% 0.13/0.50 ![V_Fa_2]: ((~c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(![B_x]: (~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_xa]: (~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_xa,c_Arrow__Order__Mirabelle_OProf)|(![B_a,B_b]: ((?[B_i]: ((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))))|((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))))))))))&(c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(?[B_x]: (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_xa]: (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_xa,c_Arrow__Order__Mirabelle_OProf)&(?[B_a,B_b]: ((![B_i]: ((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))))&((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa))))))))))))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f614])).
% 0.13/0.50 fof(f616,plain,(
% 0.13/0.50 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(![B_x]: (~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_xa]: (~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_xa,c_Arrow__Order__Mirabelle_OProf)|(![B_a,B_b]: ((?[B_i]: ((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))))|((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa))))))))))))&(![V_Fa_2]: (c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(?[B_x]: (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_xa]: (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_xa,c_Arrow__Order__Mirabelle_OProf)&(?[B_a,B_b]: (((![B_i]: (~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i))))&(![B_i]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,B_i)))))&((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa))))))))))))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f615])).
% 0.13/0.50 fof(f617,plain,(
% 0.13/0.50 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(![B_x]: (~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_xa]: (~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_xa,c_Arrow__Order__Mirabelle_OProf)|(![B_a,B_b]: (((c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_xa,B_x,V_Fa_2)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,sK6_skl(B_b,B_a,B_xa,B_x,V_Fa_2))))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_xa,B_x,V_Fa_2)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_xa,sK6_skl(B_b,B_a,B_xa,B_x,V_Fa_2)))))|((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa)))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_xa))))))))))))&(![V_Fa_2]: (c_Arrow__Order__Mirabelle_OIIA(V_Fa_2)|(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)&(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)),sK8_skl(V_Fa_2),c_Arrow__Order__Mirabelle_OProf)&(((![B_i]: (~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(sK7_skl(V_Fa_2),B_i))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(sK8_skl(V_Fa_2),B_i))))&(![B_i]: (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(sK7_skl(V_Fa_2),B_i))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(sK8_skl(V_Fa_2),B_i)))))&((~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(V_Fa_2,sK7_skl(V_Fa_2)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(V_Fa_2,sK8_skl(V_Fa_2))))&(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(V_Fa_2,sK7_skl(V_Fa_2)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK9_skl(V_Fa_2),sK10_skl(V_Fa_2)),hAPP(V_Fa_2,sK8_skl(V_Fa_2))))))))))),
% 0.13/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(B_i,sK6_skl(B_b,B_a,B_xa,B_x,V_Fa_2)),skolemize(B_x,sK7_skl(V_Fa_2)),skolemize(B_xa,sK8_skl(V_Fa_2)),skolemize(B_a,sK9_skl(V_Fa_2)),skolemize(B_b,sK10_skl(V_Fa_2))],[f616])).
% 0.13/0.50 fof(f618,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X1,sK6_skl(X4,X3,X2,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X2,sK6_skl(X4,X3,X2,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X1))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X2)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f617])).
% 0.13/0.50 fof(f619,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X1,sK6_skl(X4,X3,X2,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X2,sK6_skl(X4,X3,X2,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X1))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X2)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f617])).
% 0.13/0.50 fof(f620,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X1,sK6_skl(X4,X3,X2,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X2,sK6_skl(X4,X3,X2,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X1))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X2)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f617])).
% 0.13/0.50 fof(f621,plain,(
% 0.13/0.50 ![X0,X1,X2,X3,X4]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X1,sK6_skl(X4,X3,X2,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X2,sK6_skl(X4,X3,X2,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X1))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X3,X4),hAPP(X0,X2)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f617])).
% 0.13/0.50 fof(f628,plain,(
% 0.13/0.50 ![V_Fa_2]: (c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)<=>(![B_x]: (~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]: ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_x)))))))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.13/0.50 fof(f629,plain,(
% 0.13/0.50 ![V_Fa_2]: ((~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~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]: ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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]: (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]: c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))&~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_x))))))))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f628])).
% 0.13/0.50 fof(f630,plain,(
% 0.13/0.50 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~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]: ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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]: (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]: c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,B_i)))&~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(V_Fa_2,B_x))))))))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f629])).
% 0.13/0.50 fof(f631,plain,(
% 0.13/0.50 (![V_Fa_2]: (~c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)|(![B_x]: (~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]: (~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_a,B_b),hAPP(B_x,sK11_skl(B_b,B_a,B_x,V_Fa_2)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),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)|(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)),sK12_skl(V_Fa_2),c_Arrow__Order__Mirabelle_OProf)&((![B_i]: c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK13_skl(V_Fa_2),sK14_skl(V_Fa_2)),hAPP(sK12_skl(V_Fa_2),B_i)))&~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK13_skl(V_Fa_2),sK14_skl(V_Fa_2)),hAPP(V_Fa_2,sK12_skl(V_Fa_2)))))))),
% 0.13/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(B_i,sK11_skl(B_b,B_a,B_x,V_Fa_2)),skolemize(B_x,sK12_skl(V_Fa_2)),skolemize(B_a,sK13_skl(V_Fa_2)),skolemize(B_b,sK14_skl(V_Fa_2))],[f630])).
% 0.13/0.50 fof(f632,plain,(
% 0.13/0.50 ![X0,X1,X2,X3]: (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|~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)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X1,sK11_skl(X3,X2,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X0,X1)))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f631])).
% 0.13/0.50 fof(f2079,plain,(
% 0.13/0.50 (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))<~>c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)))),
% 0.13/0.50 inference(pre_NNF_transformation,[status(thm)],[f522])).
% 0.13/0.50 fof(f2080,plain,(
% 0.13/0.50 (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)))&(~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)))),
% 0.13/0.50 inference(NNF_transformation,[status(thm)],[f2079])).
% 0.13/0.50 fof(f2081,plain,(
% 0.13/0.50 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.13/0.50 fof(f2082,plain,(
% 0.13/0.50 ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.13/0.50 fof(f2097,definition,(
% 0.13/0.50 sQ0_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2098,plain,(
% 0.13/0.50 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|~sQ0_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2097])).
% 0.13/0.50 fof(f2100,definition,(
% 0.13/0.50 sQ1_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2101,plain,(
% 0.13/0.50 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))|~sQ1_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2100])).
% 0.13/0.50 fof(f2103,plain,(
% 0.13/0.50 sQ0_spl|sQ1_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f2081,f2097,f2100])).
% 0.13/0.50 fof(f2104,plain,(
% 0.13/0.50 ~sQ0_spl|~sQ1_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f2082,f2097,f2100])).
% 0.13/0.50 fof(f2208,plain,(
% 0.13/0.50 ![X0,X1,X2]: (v_a_H____=v_b_H____|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ1_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f568,f2101])).
% 0.13/0.50 fof(f2209,definition,(
% 0.13/0.50 sQ2_spl <=> (v_a_H____=v_b_H____)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2210,plain,(
% 0.13/0.50 v_a_H____=v_b_H____|~sQ2_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2209])).
% 0.13/0.50 fof(f2212,definition,(
% 0.13/0.50 ![X0,X1,X2]: (sQ3_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2213,plain,(
% 0.13/0.50 ![X0,X1,X2]: (X0=X1|v_a_H____=X1|v_b_H____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ3_spl)),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2212])).
% 0.13/0.50 fof(f2215,definition,(
% 0.13/0.50 sQ4_spl <=> (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_P_H____,c_Arrow__Order__Mirabelle_OProf))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2217,plain,(
% 0.13/0.50 ~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|sQ4_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2215])).
% 0.13/0.50 fof(f2218,plain,(
% 0.13/0.50 sQ2_spl|sQ3_spl|~sQ4_spl|~sQ1_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f2208,f2209,f2212,f2215,f2100])).
% 0.13/0.50 fof(f2219,plain,(
% 0.13/0.50 $false|sQ4_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2217,f537])).
% 0.13/0.50 fof(f2220,plain,(
% 0.13/0.50 sQ4_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f2219])).
% 0.13/0.50 fof(f2221,plain,(
% 0.13/0.50 $false|~sQ2_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f2210,f531])).
% 0.13/0.50 fof(f2222,plain,(
% 0.13/0.50 ~sQ2_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f2221])).
% 0.13/0.50 fof(f2225,plain,(
% 0.13/0.50 ![X0,X1,X2]: (v_a_H____=v_b_H____|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ1_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f569,f2101])).
% 0.13/0.50 fof(f2226,definition,(
% 0.13/0.50 ![X0,X1,X2]: (sQ5_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2227,plain,(
% 0.13/0.50 ![X0,X1,X2]: (X0=X1|v_a_H____=X1|v_b_H____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ5_spl)),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2226])).
% 0.13/0.50 fof(f2229,plain,(
% 0.13/0.50 sQ2_spl|sQ5_spl|~sQ4_spl|~sQ1_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f2225,f2209,f2226,f2215,f2100])).
% 0.13/0.50 fof(f2230,plain,(
% 0.13/0.50 ![X0]: (hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,X0)),v_a_H____),v_b_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,X0)))),
% 0.13/0.50 inference(resolution,[status(thm)],[f573,f534])).
% 0.13/0.50 fof(f2239,plain,(
% 0.13/0.50 ![X0,X1,X2]: (v_a____=v_b____|X0=X1|v_a____=X1|v_b____=X0|~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_P____,c_Arrow__Order__Mirabelle_OProf)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ0_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f2098,f569])).
% 0.13/0.50 fof(f2240,plain,(
% 0.13/0.50 ![X0,X1,X2]: (v_a____=v_b____|X0=X1|v_a____=X1|v_b____=X0|~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_P____,c_Arrow__Order__Mirabelle_OProf)|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ0_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f2098,f568])).
% 0.13/0.50 fof(f2242,definition,(
% 0.13/0.50 sQ6_spl <=> (v_a____=v_b____)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2243,plain,(
% 0.13/0.50 v_a____=v_b____|~sQ6_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2242])).
% 0.13/0.50 fof(f2245,definition,(
% 0.13/0.50 ![X0,X1,X2]: (sQ7_spl <=> (X0=X1|v_a____=X1|v_b____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2246,plain,(
% 0.13/0.50 ![X0,X1,X2]: (X0=X1|v_a____=X1|v_b____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ7_spl)),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2245])).
% 0.13/0.50 fof(f2248,definition,(
% 0.13/0.50 sQ8_spl <=> (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_P____,c_Arrow__Order__Mirabelle_OProf))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f2250,plain,(
% 0.13/0.50 ~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_P____,c_Arrow__Order__Mirabelle_OProf)|sQ8_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f2248])).
% 0.13/0.50 fof(f2251,plain,(
% 0.13/0.50 sQ6_spl|sQ7_spl|~sQ8_spl|~sQ0_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f2239,f2242,f2245,f2248,f2097])).
% 0.13/0.50 fof(f2252,definition,(
% 0.13/0.50 ![X0,X1,X2]: (sQ9_spl <=> (X0=X1|v_a____=X1|v_b____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2253,plain,(
% 0.13/0.51 ![X0,X1,X2]: (X0=X1|v_a____=X1|v_b____=X0|~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)),X2,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(X2,sK1_skl(X2,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,X2))|~sQ9_spl)),
% 0.13/0.51 inference(component_clause,[status(thm)],[f2252])).
% 0.13/0.51 fof(f2255,plain,(
% 0.13/0.51 sQ6_spl|sQ9_spl|~sQ8_spl|~sQ0_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2240,f2242,f2252,f2248,f2097])).
% 0.13/0.51 fof(f2256,plain,(
% 0.13/0.51 $false|sQ8_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2250,f536])).
% 0.13/0.51 fof(f2257,plain,(
% 0.13/0.51 sQ8_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f2256])).
% 0.13/0.51 fof(f2258,plain,(
% 0.13/0.51 $false|~sQ6_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2243,f528])).
% 0.13/0.51 fof(f2259,plain,(
% 0.13/0.51 ~sQ6_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f2258])).
% 0.13/0.51 fof(f2261,plain,(
% 0.13/0.51 ![X0,X1]: (X0=X1|v_a____=X1|v_b____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,X0,X1,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ9_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2253,f537])).
% 0.13/0.51 fof(f2266,plain,(
% 0.13/0.51 v_a_H____=v_b_H____|v_a____=v_b_H____|v_b____=v_a_H____|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|~sQ9_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2261,f535])).
% 0.13/0.51 fof(f2272,definition,(
% 0.13/0.51 sQ11_spl <=> (v_a____=v_b_H____)),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2273,plain,(
% 0.13/0.51 v_a____=v_b_H____|~sQ11_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f2272])).
% 0.13/0.51 fof(f2275,definition,(
% 0.13/0.51 sQ12_spl <=> (v_b____=v_a_H____)),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2276,plain,(
% 0.13/0.51 v_b____=v_a_H____|~sQ12_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f2275])).
% 0.13/0.51 fof(f2278,definition,(
% 0.13/0.51 sQ13_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2279,plain,(
% 0.13/0.51 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|~sQ13_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f2278])).
% 0.13/0.51 fof(f2281,plain,(
% 0.13/0.51 sQ2_spl|sQ11_spl|sQ12_spl|sQ13_spl|sQ1_spl|~sQ9_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2266,f2209,f2272,f2275,f2278,f2100,f2252])).
% 0.13/0.51 fof(f2282,plain,(
% 0.13/0.51 $false|~sQ12_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2276,f530])).
% 0.13/0.51 fof(f2283,plain,(
% 0.13/0.51 ~sQ12_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f2282])).
% 0.13/0.51 fof(f2284,plain,(
% 0.13/0.51 $false|~sQ11_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2273,f529])).
% 0.13/0.51 fof(f2285,plain,(
% 0.13/0.51 ~sQ11_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f2284])).
% 0.13/0.51 fof(f2292,plain,(
% 0.13/0.51 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2213,f537])).
% 0.13/0.51 fof(f2293,plain,(
% 0.13/0.51 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P____))|~sQ3_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2213,f536])).
% 0.13/0.51 fof(f2303,plain,(
% 0.13/0.51 hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____))),v_a_H____),v_b_H____))|~sQ13_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2279,f2230])).
% 0.13/0.51 fof(f2305,plain,(
% 0.13/0.51 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|~sQ13_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2303,f572])).
% 0.13/0.51 fof(f2308,plain,(
% 0.13/0.51 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl|~sQ5_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2292,f2227])).
% 0.13/0.51 fof(f2320,definition,(
% 0.13/0.51 ![X0,X1]: (sQ15_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|X0=X1|v_a_H____=X1|v_b_H____=X0|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2323,plain,(
% 0.13/0.51 sQ15_spl|~sQ4_spl|~sQ3_spl|~sQ5_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2308,f2320,f2215,f2212,f2226])).
% 0.13/0.51 fof(f2362,plain,(
% 0.13/0.51 hBOOL(hAPP(hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____)))|~sQ13_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f611,f2279])).
% 0.13/0.51 fof(f2366,plain,(
% 0.13/0.51 ![X0,X1]: (hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____)))|X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f611,f2292])).
% 0.13/0.51 fof(f2411,plain,(
% 0.13/0.51 ![X0]: (c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|~sQ13_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2362,f612])).
% 0.13/0.51 fof(f2416,plain,(
% 0.13/0.51 v_a_H____=v_b_H____|v_a____=v_b_H____|v_b____=v_a_H____|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))|~sQ7_spl|~sQ13_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2246,f2411])).
% 0.13/0.51 fof(f2417,definition,(
% 0.13/0.51 sQ19_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2419,plain,(
% 0.13/0.51 ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P____,v_a_H____,v_b_H____,v_a____,v_b____)))|sQ19_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f2417])).
% 0.13/0.51 fof(f2420,plain,(
% 0.13/0.51 sQ2_spl|sQ11_spl|sQ12_spl|~sQ4_spl|~sQ19_spl|sQ1_spl|~sQ7_spl|~sQ13_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2416,f2209,f2272,f2275,f2215,f2417,f2100,f2245,f2278])).
% 0.13/0.51 fof(f2421,plain,(
% 0.13/0.51 $false|~sQ13_spl|sQ19_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f2419,f2305])).
% 0.13/0.51 fof(f2422,plain,(
% 0.13/0.51 ~sQ13_spl|sQ19_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f2421])).
% 0.13/0.51 fof(f2426,plain,(
% 0.13/0.51 hBOOL(hAPP(hAPP(v_F,v_P_H____),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____)))|~sQ1_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2101,f611])).
% 0.13/0.51 fof(f2459,plain,(
% 0.13/0.51 ![X0,X1,X2,X3]: (~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)),X0,c_Arrow__Order__Mirabelle_OProf)|~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)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X0,sK6_skl(X3,X2,X1,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X1,sK6_skl(X3,X2,X1,X0,v_F)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X0))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X1)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f618,f526])).
% 0.13/0.51 fof(f2460,plain,(
% 0.13/0.51 ![X0,X1,X2,X3]: (~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)),X0,c_Arrow__Order__Mirabelle_OProf)|~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)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X0,sK6_skl(X3,X2,X1,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(X1,sK6_skl(X3,X2,X1,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X0))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X2,X3),hAPP(v_F,X1)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f619,f526])).
% 0.13/0.51 fof(f2461,plain,(
% 0.13/0.51 ![X0,X1]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X1,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,X1))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0))))),
% 0.13/0.51 inference(resolution,[status(thm)],[f620,f534])).
% 0.13/0.51 fof(f2462,definition,(
% 0.13/0.51 ![X0,X1]: (sQ20_spl <=> (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X1,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,X1))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2465,plain,(
% 0.13/0.51 sQ20_spl|~sQ4_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2461,f2462,f2215])).
% 0.13/0.51 fof(f2466,plain,(
% 0.13/0.51 ![X0]: (c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,v_P_H____))|~sQ1_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2426,f612])).
% 0.13/0.51 fof(f2486,plain,(
% 0.13/0.51 ![X0,X1]: (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X1,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,X1))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0))))),
% 0.13/0.51 inference(resolution,[status(thm)],[f621,f534])).
% 0.13/0.51 fof(f2487,definition,(
% 0.13/0.51 ![X0,X1]: (sQ21_spl <=> (~c_Arrow__Order__Mirabelle_OIIA(X0)|~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)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X1,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,X1))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X1,X0)))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2490,plain,(
% 0.13/0.51 sQ21_spl|~sQ4_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2486,f2487,f2215])).
% 0.13/0.51 fof(f2502,plain,(
% 0.13/0.51 ![X0,X1]: (hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____)))|X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))|~sQ3_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f2366,f611])).
% 0.13/0.51 fof(f2508,plain,(
% 0.13/0.51 ![X0,X1,X2]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))|c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|~sQ3_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2502,f612])).
% 0.13/0.52 fof(f2514,plain,(
% 0.13/0.52 ![X0,X1,X2,X3]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(X3,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|~sQ3_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2508,f612])).
% 0.13/0.52 fof(f2515,plain,(
% 0.13/0.52 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl|~sQ5_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2508,f2227])).
% 0.13/0.52 fof(f2520,definition,(
% 0.13/0.52 ![X0,X1]: (sQ23_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1)))|X0=X1|v_a_H____=X1|v_b_H____=X0|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2523,plain,(
% 0.13/0.52 sQ23_spl|~sQ4_spl|~sQ3_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2515,f2520,f2215,f2212,f2226])).
% 0.13/0.52 fof(f2526,plain,(
% 0.13/0.52 ![X0,X1,X2]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl|~sQ5_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2514,f2227])).
% 0.13/0.52 fof(f2537,plain,(
% 0.13/0.52 ![X0,X1,X2]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____))),X0),X1))|~sQ3_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2514,f573])).
% 0.13/0.52 fof(f2541,definition,(
% 0.13/0.52 ![X0,X1,X2]: (sQ24_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|c_member(X2,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|X0=X1|v_a_H____=X1|v_b_H____=X0|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2544,plain,(
% 0.13/0.52 sQ24_spl|~sQ4_spl|~sQ3_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2526,f2541,f2215,f2212,f2226])).
% 0.13/0.52 fof(f2562,plain,(
% 0.13/0.52 ![X0]: (~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~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)),X0,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK6_skl(v_b_H____,v_a_H____,X0,v_P_H____,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,sK6_skl(v_b_H____,v_a_H____,X0,v_P_H____,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,X0))|~sQ1_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2459,f2466])).
% 0.13/0.52 fof(f2563,definition,(
% 0.13/0.52 ![X0]: (sQ26_spl <=> (~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)),X0,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK6_skl(v_b_H____,v_a_H____,X0,v_P_H____,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,sK6_skl(v_b_H____,v_a_H____,X0,v_P_H____,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2566,plain,(
% 0.13/0.52 ~sQ4_spl|sQ26_spl|~sQ1_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2562,f2215,f2563,f2100])).
% 0.13/0.52 fof(f2567,plain,(
% 0.13/0.52 ![X0]: (~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)),X0,c_Arrow__Order__Mirabelle_OProf)|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,X0))|~sQ1_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2460,f2466])).
% 0.13/0.52 fof(f2568,definition,(
% 0.13/0.52 ![X0]: (sQ27_spl <=> (~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)),X0,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK6_skl(v_b_H____,v_a_H____,v_P_H____,X0,v_F)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_F,X0))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2571,plain,(
% 0.13/0.52 sQ27_spl|~sQ4_spl|~sQ1_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2567,f2568,f2215,f2100])).
% 0.13/0.52 fof(f2614,plain,(
% 0.13/0.52 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____))),X0),X1))|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|~sQ3_spl|~sQ5_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2537,f2227])).
% 0.13/0.52 fof(f2621,definition,(
% 0.13/0.52 ![X0,X1]: (sQ29_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))|hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____))),X0),X1))|X0=X1|v_a_H____=X1|v_b_H____=X0|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P_H____,sK1_skl(v_P_H____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P_H____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2624,plain,(
% 0.13/0.52 sQ29_spl|~sQ4_spl|~sQ3_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2614,f2621,f2215,f2212,f2226])).
% 0.13/0.52 fof(f2626,plain,(
% 0.13/0.52 ![X0,X1]: (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P____))|X0=X1|v_a_H____=X1|v_b_H____=X0|~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_P____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P____))|~sQ3_spl|~sQ5_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2293,f2227])).
% 0.13/0.52 fof(f2633,plain,(
% 0.13/0.52 v_a____=v_b____|v_a_H____=v_b____|v_b_H____=v_a____|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____))),v_a_H____),v_b_H____))|~sQ3_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f2293,f2230])).
% 0.13/0.52 fof(f2637,definition,(
% 0.13/0.52 ![X0,X1]: (sQ30_spl <=> (X0=X1|v_a_H____=X1|v_b_H____=X0|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P____))|X0=X1|v_a_H____=X1|v_b_H____=X0|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,X0,X1,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),hAPP(v_F,v_P____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2640,plain,(
% 0.13/0.52 sQ30_spl|~sQ8_spl|~sQ3_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2626,f2637,f2248,f2212,f2226])).
% 0.13/0.52 fof(f2641,definition,(
% 0.13/0.52 sQ31_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2642,plain,(
% 0.13/0.52 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|~sQ31_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f2641])).
% 0.13/0.52 fof(f2652,definition,(
% 0.13/0.52 sQ34_spl <=> (hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____))),v_a_H____),v_b_H____)))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2653,plain,(
% 0.13/0.52 hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____))),v_a_H____),v_b_H____))|~sQ34_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f2652])).
% 0.13/0.52 fof(f2655,plain,(
% 0.13/0.52 sQ6_spl|sQ12_spl|sQ11_spl|sQ31_spl|sQ0_spl|sQ34_spl|~sQ3_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2633,f2242,f2275,f2272,f2641,f2097,f2652,f2212])).
% 0.13/0.52 fof(f2656,plain,(
% 0.13/0.52 v_a____=v_b____|v_a_H____=v_b____|v_b_H____=v_a____|~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_P____,c_Arrow__Order__Mirabelle_OProf)|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_F,v_P____))|~sQ31_spl|~sQ5_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f2642,f2227])).
% 0.13/0.52 fof(f2657,plain,(
% 0.13/0.52 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|~sQ31_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f2642,f535])).
% 0.13/0.52 fof(f2661,definition,(
% 0.13/0.52 sQ35_spl <=> (c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2663,plain,(
% 0.13/0.52 ~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|sQ35_spl),
% 0.13/0.52 inference(component_clause,[status(thm)],[f2661])).
% 0.13/0.52 fof(f2664,plain,(
% 0.13/0.52 sQ6_spl|sQ12_spl|sQ11_spl|~sQ8_spl|~sQ35_spl|sQ0_spl|~sQ31_spl|~sQ5_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2656,f2242,f2275,f2272,f2248,f2661,f2097,f2641,f2226])).
% 0.13/0.52 fof(f2730,plain,(
% 0.13/0.52 ![X0]: (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|~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_P_H____,c_Arrow__Order__Mirabelle_OProf)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK11_skl(v_b_H____,v_a_H____,v_P_H____,X0))))),
% 0.13/0.52 inference(resolution,[status(thm)],[f632,f534])).
% 0.13/0.52 fof(f2731,definition,(
% 0.13/0.52 ![X0]: (sQ44_spl <=> (~c_Arrow__Order__Mirabelle_Ounanimity(X0)|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(X0,v_P_H____))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK11_skl(v_b_H____,v_a_H____,v_P_H____,X0)))))),
% 0.13/0.52 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.13/0.52 fof(f2734,plain,(
% 0.13/0.52 sQ44_spl|~sQ4_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2730,f2731,f2215])).
% 0.13/0.52 fof(f2743,plain,(
% 0.13/0.52 hBOOL(hAPP(hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____)))|~sQ31_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f2657,f611])).
% 0.13/0.52 fof(f2744,plain,(
% 0.13/0.52 ![X0]: (c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|~sQ31_spl)),
% 0.13/0.52 inference(resolution,[status(thm)],[f2743,f612])).
% 0.13/0.52 fof(f2830,plain,(
% 0.13/0.52 $false|~sQ31_spl|sQ35_spl),
% 0.13/0.52 inference(forward_subsumption_resolution,[status(thm)],[f2663,f2744])).
% 0.13/0.52 fof(f2831,plain,(
% 0.13/0.52 ~sQ31_spl|sQ35_spl),
% 0.13/0.52 inference(contradiction_clause,[status(thm)],[f2830])).
% 0.13/0.52 fof(f2844,plain,(
% 0.13/0.52 c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a_H____,v_b_H____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_a____,v_b____,v_a_H____,v_b_H____)))|~sQ34_spl),
% 0.13/0.52 inference(resolution,[status(thm)],[f2653,f572])).
% 0.13/0.52 fof(f2846,plain,(
% 0.13/0.52 sQ31_spl|~sQ34_spl),
% 0.13/0.52 inference(split_clause,[status(thm)],[f2844,f2641,f2652])).
% 0.13/0.52 fof(f2847,plain,(
% 0.13/0.52 $false),
% 0.13/0.52 inference(sat_refutation,[status(thm)],[f2103,f2104,f2218,f2220,f2222,f2229,f2251,f2255,f2257,f2259,f2281,f2283,f2285,f2323,f2420,f2422,f2465,f2490,f2523,f2544,f2566,f2571,f2624,f2640,f2655,f2664,f2734,f2831,f2846])).
% 0.13/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.52 % Elapsed time: 0.172305 seconds
% 0.13/0.52 % CPU time: 0.989896 seconds
% 0.13/0.52 % Total memory used: 162.631 MB
% 0.13/0.52 % Net memory used: 161.708 MB
%------------------------------------------------------------------------------