%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT158+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:23 PM UTC 2026
% Result : Theorem 158.93s 30.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SCT158+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/10.32 % Computer : n012.cluster.edu
% 0.05/10.32 % Model : x86_64 x86_64
% 0.05/10.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/10.32 % Memory : 8046.5625MB
% 0.05/10.32 % OS : Linux 6.8.0-71-generic
% 0.05/10.32 % CPULimit : 300
% 0.05/10.32 % WCLimit : 300
% 0.05/10.32 % DateTime : Mon Sep 21 04:35:08 UTC 2026
% 0.05/10.32 % CPUTime :
% 0.05/10.35 % Drodi V4.1.1
% 158.93/30.42 % Refutation found
% 158.93/30.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 158.93/30.42 % SZS output start CNFRefutation for theBenchmark
% 158.93/30.42 fof(f4,axiom,(
% 158.93/30.42 v_a____ != v_b____ ),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f6,axiom,(
% 158.93/30.42 ( v_a____ = v_b_H____& v_b____ = v_a_H____ ) ),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f7,axiom,(
% 158.93/30.42 (! [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)) ) )),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f11,axiom,(
% 158.93/30.42 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) ),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f12,axiom,(
% 158.93/30.42 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) ),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f16,axiom,(
% 158.93/30.42 (! [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) ) )),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f18,axiom,(
% 158.93/30.42 (! [V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2] :( V_aa_2 != V_ba_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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2)) ) ) ) ) ) )),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f26,axiom,(
% 158.93/30.42 (! [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)) ) )),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f529,conjecture,(
% 158.93/30.42 ( c_member(tc_prod(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____)) ) ),
% 158.93/30.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 158.93/30.42 fof(f530,negated_conjecture,(
% 158.93/30.42 ~(( c_member(tc_prod(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____)) ) )),
% 158.93/30.43 inference(negated_conjecture,[status(cth)],[f529])).
% 158.93/30.43 fof(f536,plain,(
% 158.93/30.43 ~v_a____=v_b____),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f4])).
% 158.93/30.43 fof(f538,plain,(
% 158.93/30.43 v_a____=v_b_H____),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f6])).
% 158.93/30.43 fof(f539,plain,(
% 158.93/30.43 v_b____=v_a_H____),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f6])).
% 158.93/30.43 fof(f540,plain,(
% 158.93/30.43 ![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))))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f7])).
% 158.93/30.43 fof(f541,plain,(
% 158.93/30.43 (![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))))),
% 158.93/30.43 inference(miniscoping,[status(thm)],[f540])).
% 158.93/30.43 fof(f542,plain,(
% 158.93/30.43 ![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)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f541])).
% 158.93/30.43 fof(f543,plain,(
% 158.93/30.43 ![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)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f541])).
% 158.93/30.43 fof(f556,plain,(
% 158.93/30.43 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)),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f11])).
% 158.93/30.43 fof(f557,plain,(
% 158.93/30.43 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)),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f12])).
% 158.93/30.43 fof(f584,plain,(
% 158.93/30.43 ![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)))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f16])).
% 158.93/30.43 fof(f585,plain,(
% 158.93/30.43 (![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)))),
% 158.93/30.43 inference(miniscoping,[status(thm)],[f584])).
% 158.93/30.43 fof(f586,plain,(
% 158.93/30.43 ![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))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f585])).
% 158.93/30.43 fof(f587,plain,(
% 158.93/30.43 ![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))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f585])).
% 158.93/30.43 fof(f591,plain,(
% 158.93/30.43 ![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2]: (V_aa_2=V_ba_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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2)))))))),
% 158.93/30.43 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 158.93/30.43 fof(f592,definition,(
% 158.93/30.43 ![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2,B_i]: (sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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,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_ba_2,V_aa_2),hAPP(V_P_Ha_2,B_i))))),
% 158.93/30.43 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 158.93/30.43 fof(f593,plain,(
% 158.93/30.43 ![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2]: (V_aa_2=V_ba_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]: sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2)))))))),
% 158.93/30.43 inference(formula_renaming,[status(thm)],[f591,f592])).
% 158.93/30.43 fof(f594,plain,(
% 158.93/30.43 ![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2]: (V_aa_2=V_ba_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]: sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2))))))))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f593])).
% 158.93/30.43 fof(f595,plain,(
% 158.93/30.43 ![V_ba_2,V_aa_2]: (V_aa_2=V_ba_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]: sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2))))))))))),
% 158.93/30.43 inference(miniscoping,[status(thm)],[f594])).
% 158.93/30.43 fof(f596,plain,(
% 158.93/30.43 ![V_ba_2,V_aa_2]: (V_aa_2=V_ba_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)|(sP1_prd(sK1_skl(V_P_Ha_2,V_Pa_2,V_aa_2,V_ba_2),V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_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_ba_2,V_aa_2),hAPP(v_F,V_P_Ha_2))))))))))),
% 158.93/30.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_i,sK1_skl(V_P_Ha_2,V_Pa_2,V_aa_2,V_ba_2))],[f595])).
% 158.93/30.43 fof(f597,plain,(
% 158.93/30.43 ![X0,X1,X2,X3]: (X0=X1|~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_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X3,c_Arrow__Order__Mirabelle_OProf)|sP1_prd(sK1_skl(X3,X2,X0,X1),X0,X1,X2,X3)|~c_member(tc_prod(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))|c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),hAPP(v_F,X3)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f596])).
% 158.93/30.43 fof(f598,plain,(
% 158.93/30.43 ![X0,X1,X2,X3]: (X0=X1|~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_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X3,c_Arrow__Order__Mirabelle_OProf)|sP1_prd(sK1_skl(X3,X2,X0,X1),X0,X1,X2,X3)|c_member(tc_prod(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))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),hAPP(v_F,X3)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f596])).
% 158.93/30.43 fof(f631,plain,(
% 158.93/30.43 ![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))))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f26])).
% 158.93/30.43 fof(f632,plain,(
% 158.93/30.43 (![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))))),
% 158.93/30.43 inference(miniscoping,[status(thm)],[f631])).
% 158.93/30.43 fof(f633,plain,(
% 158.93/30.43 ![X0,X1,X2]: (~c_member(X0,X1,X2)|hBOOL(hAPP(X2,X1)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f632])).
% 158.93/30.43 fof(f634,plain,(
% 158.93/30.43 ![X0,X1,X2]: (c_member(X0,X1,X2)|~hBOOL(hAPP(X2,X1)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f632])).
% 158.93/30.43 fof(f2130,plain,(
% 158.93/30.43 (c_member(tc_prod(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____)))),
% 158.93/30.43 inference(pre_NNF_transformation,[status(thm)],[f530])).
% 158.93/30.43 fof(f2131,plain,(
% 158.93/30.43 (c_member(tc_prod(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____)))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f2130])).
% 158.93/30.43 fof(f2132,plain,(
% 158.93/30.43 c_member(tc_prod(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____))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f2131])).
% 158.93/30.43 fof(f2133,plain,(
% 158.93/30.43 ~c_member(tc_prod(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____))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f2131])).
% 158.93/30.43 fof(f2139,plain,(
% 158.93/30.43 ![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2,B_i]: ((~sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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,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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(V_P_Ha_2,B_i)))))&(sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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,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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(V_P_Ha_2,B_i))))))),
% 158.93/30.43 inference(NNF_transformation,[status(thm)],[f592])).
% 158.93/30.43 fof(f2140,plain,(
% 158.93/30.43 (![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2,B_i]: (~sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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,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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(V_P_Ha_2,B_i))))))&(![V_P_Ha_2,V_Pa_2,V_ba_2,V_aa_2,B_i]: (sP1_prd(B_i,V_aa_2,V_ba_2,V_Pa_2,V_P_Ha_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,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_ba_2,V_aa_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_ba_2,V_aa_2),hAPP(V_P_Ha_2,B_i))))))),
% 158.93/30.43 inference(miniscoping,[status(thm)],[f2139])).
% 158.93/30.43 fof(f2141,plain,(
% 158.93/30.43 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,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,X1,X2),hAPP(X3,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,X1),hAPP(X4,X0)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f2140])).
% 158.93/30.43 fof(f2142,plain,(
% 158.93/30.43 ![X0,X1,X2,X3,X4]: (~sP1_prd(X0,X1,X2,X3,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,X1,X2),hAPP(X3,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,X1),hAPP(X4,X0)))),
% 158.93/30.43 inference(cnf_transformation,[status(thm)],[f2140])).
% 158.93/30.43 fof(f2247,plain,(
% 158.93/30.43 ~c_member(tc_prod(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_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(backward_demodulation,[status(thm)],[f538,f2133])).
% 158.93/30.43 fof(f2248,plain,(
% 158.93/30.43 c_member(tc_prod(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_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(backward_demodulation,[status(thm)],[f538,f2132])).
% 158.93/30.43 fof(f2249,plain,(
% 158.93/30.43 ![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_b____,v_b_H____),hAPP(v_P_H____,X0)))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f539,f542])).
% 158.93/30.43 fof(f2250,plain,(
% 158.93/30.43 ![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_b____,v_a____),hAPP(v_P_H____,X0)))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f538,f2249])).
% 158.93/30.43 fof(f2251,plain,(
% 158.93/30.43 ![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_b____,v_b_H____),hAPP(v_P_H____,X0)))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f539,f543])).
% 158.93/30.43 fof(f2252,plain,(
% 158.93/30.43 ![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_b____,v_a____),hAPP(v_P_H____,X0)))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f538,f2251])).
% 158.93/30.43 fof(f2257,plain,(
% 158.93/30.43 ~c_member(tc_prod(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_b____,v_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f539,f2247])).
% 158.93/30.43 fof(f2258,plain,(
% 158.93/30.43 c_member(tc_prod(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_b____,v_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(forward_demodulation,[status(thm)],[f539,f2248])).
% 158.93/30.43 fof(f2276,plain,(
% 158.93/30.43 ![X0]: (hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,X0)),v_b____),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____,v_b____),hAPP(v_P____,X0)))),
% 158.93/30.43 inference(resolution,[status(thm)],[f587,f2250])).
% 158.93/30.43 fof(f2283,plain,(
% 158.93/30.43 ![X0]: (v_b____=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_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)|sP1_prd(sK1_skl(X0,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_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____,v_b____),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,v_a____,v_b____),hAPP(v_F,v_P____)))),
% 158.93/30.43 inference(resolution,[status(thm)],[f597,f2258])).
% 158.93/30.43 fof(f2284,plain,(
% 158.93/30.43 ![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)|sP1_prd(sK1_skl(X0,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_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____,v_b____),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,v_a____,v_b____),hAPP(v_F,v_P____)))),
% 158.93/30.43 inference(forward_subsumption_resolution,[status(thm)],[f2283,f536])).
% 158.93/30.43 fof(f2288,plain,(
% 158.93/30.43 ![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)|sP1_prd(sK1_skl(X0,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_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____,v_b____),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,v_a____,v_b____),hAPP(v_F,v_P____)))),
% 158.93/30.43 inference(forward_subsumption_resolution,[status(thm)],[f2284,f557])).
% 158.93/30.43 fof(f2290,plain,(
% 158.93/30.43 sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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____,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____,v_b____),hAPP(v_F,v_P____))),
% 158.93/30.43 inference(resolution,[status(thm)],[f2288,f556])).
% 158.93/30.43 fof(f2291,plain,(
% 158.93/30.43 sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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____,v_b____),hAPP(v_F,v_P____))),
% 158.93/30.43 inference(duplicate_literals_removal,[status(thm)],[f2290])).
% 158.93/30.43 fof(f2312,plain,(
% 158.93/30.43 ![X0,X1,X2]: (X0=X1|~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)|sP1_prd(sK1_skl(v_P____,X2,X0,X1),X0,X1,X2,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,X0,X1),hAPP(v_F,X2))|~c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),hAPP(v_F,v_P____)))),
% 158.93/30.43 inference(resolution,[status(thm)],[f598,f556])).
% 158.93/30.43 fof(f2336,plain,(
% 158.93/30.43 ![X0,X1]: (X0=X1|sP1_prd(sK1_skl(v_P____,v_P_H____,X0,X1),X0,X1,v_P_H____,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,X0,X1),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,X1,X0),hAPP(v_F,v_P____)))),
% 158.93/30.43 inference(resolution,[status(thm)],[f2312,f557])).
% 158.93/30.43 fof(f2359,plain,(
% 158.93/30.43 ![X0,X1,X2,X3]: (c_member(X0,X1,X2)|~c_member(X3,X1,X2))),
% 158.93/30.43 inference(resolution,[status(thm)],[f634,f633])).
% 158.93/30.43 fof(f2453,plain,(
% 158.93/30.43 v_b____=v_a____|sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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_b____,v_a____),hAPP(v_F,v_P_H____))|sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,v_P____)),
% 158.93/30.43 inference(resolution,[status(thm)],[f2336,f2291])).
% 158.93/30.43 fof(f2458,plain,(
% 158.93/30.43 v_b____=v_a____|sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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_b____,v_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(duplicate_literals_removal,[status(thm)],[f2453])).
% 158.93/30.43 fof(f2459,plain,(
% 158.93/30.43 sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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_b____,v_a____),hAPP(v_F,v_P_H____))),
% 158.93/30.43 inference(forward_subsumption_resolution,[status(thm)],[f2458,f536])).
% 158.93/30.43 fof(f2519,plain,(
% 158.93/30.43 sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,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____,v_b____),hAPP(v_F,v_P____))),
% 158.93/30.43 inference(resolution,[status(thm)],[f2459,f2257])).
% 158.93/30.43 fof(f2525,plain,(
% 158.93/30.43 sP1_prd(sK1_skl(v_P____,v_P_H____,v_b____,v_a____),v_b____,v_a____,v_P_H____,v_P____)),
% 120.12/30.55 inference(forward_subsumption_resolution,[status(thm)],[f2519,f2291])).
% 120.12/30.55 fof(f5629,plain,(
% 120.12/30.55 ![X0,X1]: (~c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,X1))|hBOOL(hAPP(hAPP(c_FunDef_Oin__rel(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,hAPP(v_P_H____,X1)),v_b____),v_a____)))),
% 120.12/30.55 inference(resolution,[status(thm)],[f2359,f2276])).
% 120.12/30.55 fof(f5632,plain,(
% 120.12/30.55 ![X0,X1]: (~c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_b____,v_a____),hAPP(v_P_H____,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____,v_b____),hAPP(v_P____,X1)))),
% 120.12/30.55 inference(resolution,[status(thm)],[f2359,f2252])).
% 120.12/30.55 fof(f6638,plain,(
% 120.12/30.55 ![X0,X1]: (~c_member(X0,c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,v_a____,v_b____),hAPP(v_P____,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_b____,v_a____),hAPP(v_P_H____,X1)))),
% 120.12/30.55 inference(resolution,[status(thm)],[f5629,f586])).
% 120.12/30.55 fof(f24875,plain,(
% 120.12/30.55 c_member(tc_prod(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_b____,v_a____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_b____,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____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_b____,v_a____)))),
% 120.12/30.55 inference(resolution,[status(thm)],[f2141,f2525])).
% 120.12/30.55 fof(f24969,plain,(
% 120.12/30.55 c_member(tc_prod(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_b____,v_a____)))),
% 120.12/30.55 inference(forward_subsumption_resolution,[status(thm)],[f24875,f5632])).
% 120.12/30.55 fof(f25056,plain,(
% 120.12/30.55 ~c_member(tc_prod(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_b____,v_a____),hAPP(v_P_H____,sK1_skl(v_P____,v_P_H____,v_b____,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____,v_b____),hAPP(v_P____,sK1_skl(v_P____,v_P_H____,v_b____,v_a____)))),
% 120.12/30.55 inference(resolution,[status(thm)],[f2142,f2525])).
% 120.12/30.55 fof(f25150,plain,(
% 120.12/30.55 ~c_member(tc_prod(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_b____,v_a____)))),
% 120.12/30.55 inference(forward_subsumption_resolution,[status(thm)],[f25056,f6638])).
% 120.12/30.55 fof(f36769,plain,(
% 120.12/30.55 $false),
% 120.12/30.55 inference(forward_subsumption_resolution,[status(thm)],[f25150,f24969])).
% 120.12/30.55 % SZS output end CNFRefutation for theBenchmark.p
% 9.96/30.62 % Elapsed time: 20.279648 seconds
% 9.96/30.62 % CPU time: 160.454782 seconds
% 9.96/30.62 % Total memory used: 1.579 GB
% 9.96/30.62 % Net memory used: 1.454 GB
%------------------------------------------------------------------------------