%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV959-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:53:24 PM UTC 2026
% Result : Unsatisfiable 35.54s 9.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV959-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n001.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 09:40:04 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.13/5.41 % Drodi V4.1.1
% 35.54/9.99 % Refutation found
% 35.54/9.99 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 35.54/9.99 % SZS output start CNFRefutation for theBenchmark
% 35.54/9.99 fof(f1,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f4,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_v,V_D,V_F,V_e,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))| c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f5,axiom,(
% 35.54/9.99 (![V_T,V_P,V_D,V_E,V_F,V_e,V_h,V_v]: (( V_T = c_Type_Oty_OVoid| c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f6,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)| c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f157,axiom,(
% 35.54/9.99 (![V_P,V_T_092_060_094isub_0621,V_x,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_x)| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621)| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean)| c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f158,axiom,(
% 35.54/9.99 (![V_P,V_x,V_T_092_060_094isub_0622,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x))| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_x)| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean)| c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f226,axiom,(
% 35.54/9.99 (![V_P,V_T_092_060_094isub_0621,V_x,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))| ~ c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0622,V_x)| ~ c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621)| ~ c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OBoolean)| c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f227,axiom,(
% 35.54/9.99 (![V_P,V_x,V_T_092_060_094isub_0622,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x))| ~ c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)| ~ c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_x)| ~ c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OBoolean)| c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f310,axiom,(
% 35.54/9.99 c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f311,axiom,(
% 35.54/9.99 (![V_E,V_T]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____)),V_T))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f314,axiom,(
% 35.54/9.99 (![V_T,V_P,V_h,V_E,V_v,V_D,V_F,V_e]: (( V_T = c_Type_Oty_OVoid| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f318,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_v,V_D,V_F,V_e,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f322,axiom,(
% 35.54/9.99 (![V_Ea,V_Ta]: (( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_Ea,v_e_Ha____,v_sko__local__XIH__1(V_Ea,v_P,V_Ta,v_e_Ha____,v_h_Ha____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_Ea,v_ea____,V_Ta)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_Ea,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f323,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f325,axiom,(
% 35.54/9.99 v_T____ = c_Type_Oty_OVoid ),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f334,axiom,(
% 35.54/9.99 (![V_E,V_T]: (( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_Ha____,v_sko__local__XFAssRed1__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f343,axiom,(
% 35.54/9.99 (![V_E,V_T]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____)),V_T))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f350,axiom,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____) ),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f351,axiom,(
% 35.54/9.99 (![V_P,T_a,V_T]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_T),V_T)) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f356,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_e,V_v,V_D,V_F,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f358,axiom,(
% 35.54/9.99 (![V_Ea,V_Ta]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(V_Ea,v_P,V_Ta,v_e_Ha____,v_h_Ha____)),V_Ta))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_Ea,v_ea____,V_Ta)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_Ea,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f362,axiom,(
% 35.54/9.99 (![V_P,V_h,V_E,V_v,V_D,V_F,V_e,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f365,axiom,(
% 35.54/9.99 (![V_P,V_x,V_T_092_060_094isub_0622,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_x)| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean)| c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f366,axiom,(
% 35.54/9.99 (![V_P,V_T_092_060_094isub_0621,V_x,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: (( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_x)| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621)| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean)| c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f372,axiom,(
% 35.54/9.99 (![V_E,V_T]: (( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f380,axiom,(
% 35.54/9.99 (![V_T_092_060_094isub_0622,V_TF,V_C]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_TF))| ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C)) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f381,axiom,(
% 35.54/9.99 (![V_T_092_060_094isub_0622,V_TF,V_C]: (( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_TF))| ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C)) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f382,axiom,(
% 35.54/9.99 ( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT) ) ),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f383,axiom,(
% 35.54/9.99 ( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT) ) ),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f384,negated_conjecture,(
% 35.54/9.99 (![V_x]: (( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),v_T____))| ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),V_x) ) ))),
% 35.54/9.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 35.54/9.99 fof(f387,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_e,V_D,V_F,V_v]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v))))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f1])).
% 35.54/9.99 fof(f388,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X4,X2,X5,X0,X3,X1,X6)))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f387])).
% 35.54/9.99 fof(f392,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_v,V_D,V_F,V_e]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))|c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f4])).
% 35.54/9.99 fof(f393,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(X2,X0,X1,X3))|c_TypeRel_Ohas__field(X0,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X4,X2,X5,X0,X6,X1,X3),X5,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X6,X1,X3),X4,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X6,X5,X4,X3,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f392])).
% 35.54/9.99 fof(f394,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (X0=c_Type_Oty_OVoid|c_TypeRel_Ohas__field(X1,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X2,X3,X4,X1,X5,X6,X7),X4,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X2,X3,X4,X1,X5,X6,X7),X2,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(X1,X6,X3,c_Expr_Oexp_OFAss(X5,X4,X2,X7,tc_List_Olist(tc_String_Ochar)),X0))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f5])).
% 35.54/9.99 fof(f395,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_e,V_D,V_F,V_v]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f6])).
% 35.54/9.99 fof(f396,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT)|c_TypeRel_Ohas__field(X0,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X4,X2,X5,X0,X3,X1,X6),X5,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X3,X1,X6),X4,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f395])).
% 35.54/9.99 fof(f567,plain,(
% 35.54/9.99 ![V_P,V_T_092_060_094isub_0621,V_x]: ((![V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_x))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean))|c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f157])).
% 35.54/9.99 fof(f568,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~c_Progress_OWTrt_H(X0,X3,X4,X5,X2)|~c_Progress_OWTrt_H(X0,X3,X4,X6,X1)|~c_Progress_OWTrt_H(X0,X3,X4,X7,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(X0,X3,X4,c_Expr_Oexp_OCond(X7,X6,X5,tc_List_Olist(tc_String_Ochar)),X2)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f567])).
% 35.54/9.99 fof(f569,plain,(
% 35.54/9.99 ![V_P,V_x,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((![V_T_092_060_094isub_0622]: ((hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x)))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_x))|~c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean))|c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f158])).
% 35.54/9.99 fof(f570,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1))|~c_Progress_OWTrt_H(X0,X3,X4,X5,X2)|~c_Progress_OWTrt_H(X0,X3,X4,X6,X1)|~c_Progress_OWTrt_H(X0,X3,X4,X7,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(X0,X3,X4,c_Expr_Oexp_OCond(X7,X6,X5,tc_List_Olist(tc_String_Ochar)),X1))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f569])).
% 35.54/9.99 fof(f652,plain,(
% 35.54/9.99 ![V_P,V_T_092_060_094isub_0621,V_x]: ((![V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))|~c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0622,V_x))|~c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621))|~c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OBoolean))|c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f226])).
% 35.54/9.99 fof(f653,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~c_WellType_OWT(X0,X3,X4,X2)|~c_WellType_OWT(X0,X3,X5,X1)|~c_WellType_OWT(X0,X3,X6,c_Type_Oty_OBoolean)|c_WellType_OWT(X0,X3,c_Expr_Oexp_OCond(X6,X5,X4,tc_List_Olist(tc_String_Ochar)),X2)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f652])).
% 35.54/9.99 fof(f654,plain,(
% 35.54/9.99 ![V_P,V_x,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((![V_T_092_060_094isub_0622]: ((hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x)))|~c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)))|~c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_x))|~c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OBoolean))|c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f227])).
% 35.54/9.99 fof(f655,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1))|~c_WellType_OWT(X0,X3,X4,X2)|~c_WellType_OWT(X0,X3,X5,X1)|~c_WellType_OWT(X0,X3,X6,c_Type_Oty_OBoolean)|c_WellType_OWT(X0,X3,c_Expr_Oexp_OCond(X6,X5,X4,tc_List_Olist(tc_String_Ochar)),X1))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f654])).
% 35.54/9.99 fof(f766,plain,(
% 35.54/9.99 c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f310])).
% 35.54/9.99 fof(f767,plain,(
% 35.54/9.99 ![V_E]: ((![V_T]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____)),V_T))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f311])).
% 35.54/9.99 fof(f768,plain,(
% 35.54/9.99 ![X0,X1]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____)),X1))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f767])).
% 35.54/9.99 fof(f772,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (X0=c_Type_Oty_OVoid|c_WellTypeRT_OWTrt(X1,X2,X3,X4,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X5,X3,X6,X1,X7,X2,X4))|~c_WellTypeRT_OWTrt(X1,X2,X3,c_Expr_Oexp_OFAss(X7,X6,X5,X4,tc_List_Olist(tc_String_Ochar)),X0))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f314])).
% 35.54/9.99 fof(f778,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_v,V_D,V_F,V_e]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))|c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f318])).
% 35.54/9.99 fof(f779,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(X2,X0,X1,X3))|c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X4,X2,X5,X0,X6,X1,X3))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X6,X5,X4,X3,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f778])).
% 35.54/9.99 fof(f784,plain,(
% 35.54/9.99 ![V_Ea]: ((![V_Ta]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_Ea,v_e_Ha____,v_sko__local__XIH__1(V_Ea,v_P,V_Ta,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_Ea,v_ea____,V_Ta)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_Ea,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f322])).
% 35.54/9.99 fof(f785,plain,(
% 35.54/9.99 ![X0,X1]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,X0,v_e_Ha____,v_sko__local__XIH__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f784])).
% 35.54/9.99 fof(f786,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_e,V_D,V_F,V_v]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v))))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f323])).
% 35.54/9.99 fof(f787,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X4,X2,X5,X0,X3,X1,X6)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X3,X1,X6)))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f786])).
% 35.54/9.99 fof(f789,plain,(
% 35.54/9.99 v_T____=c_Type_Oty_OVoid),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f325])).
% 35.54/9.99 fof(f803,plain,(
% 35.54/9.99 ![V_E]: ((![V_T]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_Ha____,v_sko__local__XFAssRed1__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f334])).
% 35.54/9.99 fof(f804,plain,(
% 35.54/9.99 ![X0,X1]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,X0,v_e_Ha____,v_sko__local__XFAssRed1__2__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f803])).
% 35.54/9.99 fof(f814,plain,(
% 35.54/9.99 ![V_E]: ((![V_T]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____)),V_T))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f343])).
% 35.54/9.99 fof(f815,plain,(
% 35.54/9.99 ![X0,X1]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____)),X1))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f814])).
% 35.54/9.99 fof(f823,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____)),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f350])).
% 35.54/9.99 fof(f824,plain,(
% 35.54/9.99 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X2)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f351])).
% 35.54/9.99 fof(f831,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_e,V_v,V_D,V_F]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f356])).
% 35.54/9.99 fof(f832,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(X0,X1,X2,X4,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X5,X2,X6,X0,X3,X1,X4))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X6,X5,X4,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f831])).
% 35.54/9.99 fof(f834,plain,(
% 35.54/9.99 ![V_Ea]: ((![V_Ta]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(V_Ea,v_P,V_Ta,v_e_Ha____,v_h_Ha____)),V_Ta))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_Ea,v_ea____,V_Ta)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_Ea,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f358])).
% 35.54/9.99 fof(f835,plain,(
% 35.54/9.99 ![X0,X1]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____)),X1))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f834])).
% 35.54/9.99 fof(f841,plain,(
% 35.54/9.99 ![V_P,V_h,V_E,V_v,V_D,V_F,V_e]: ((c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(V_E,V_P,V_h,V_v))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v))))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f362])).
% 35.54/9.99 fof(f842,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(X2,X0,X1,X3))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X4,X2,X5,X0,X6,X1,X3)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X6,X1,X3)))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X6,X5,X4,X3,tc_List_Olist(tc_String_Ochar)),X7))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f841])).
% 35.54/9.99 fof(f846,plain,(
% 35.54/9.99 ![V_P,V_x,V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((![V_T_092_060_094isub_0622]: ((hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0622))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_x)))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_x))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean))|c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f365])).
% 35.54/9.99 fof(f847,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1))|~c_WellTypeRT_OWTrt(X0,X3,X4,X5,X2)|~c_WellTypeRT_OWTrt(X0,X3,X4,X6,X1)|~c_WellTypeRT_OWTrt(X0,X3,X4,X7,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(X0,X3,X4,c_Expr_Oexp_OCond(X7,X6,X5,tc_List_Olist(tc_String_Ochar)),X1))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f846])).
% 35.54/9.99 fof(f848,plain,(
% 35.54/9.99 ![V_P,V_T_092_060_094isub_0621,V_x]: ((![V_h,V_E,V_e_092_060_094isub_0622,V_e_092_060_094isub_0621,V_e]: ((((~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0621),V_x))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_x))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,V_T_092_060_094isub_0621))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OBoolean))|c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCond(V_e,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_x)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_x),V_T_092_060_094isub_0621)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f366])).
% 35.54/9.99 fof(f849,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X1),X2))|~c_WellTypeRT_OWTrt(X0,X3,X4,X5,X2)|~c_WellTypeRT_OWTrt(X0,X3,X4,X6,X1)|~c_WellTypeRT_OWTrt(X0,X3,X4,X7,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(X0,X3,X4,c_Expr_Oexp_OCond(X7,X6,X5,tc_List_Olist(tc_String_Ochar)),X2)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X2),X1)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f848])).
% 35.54/9.99 fof(f855,plain,(
% 35.54/9.99 ![V_E]: ((![V_T]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_ea____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f372])).
% 35.54/9.99 fof(f856,plain,(
% 35.54/9.99 ![X0,X1]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,X0,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(X0,v_P,X1,v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_ea____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f855])).
% 35.54/9.99 fof(f865,plain,(
% 35.54/9.99 ![V_C]: ((![V_T_092_060_094isub_0622]: ((![V_TF]: ((hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_TF)))|~c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f380])).
% 35.54/9.99 fof(f866,plain,(
% 35.54/9.99 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),X1))|~c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f865])).
% 35.54/9.99 fof(f867,plain,(
% 35.54/9.99 ![V_C]: ((![V_T_092_060_094isub_0622]: ((![V_TF]: ((c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622),V_TF)))|~c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C)))),
% 35.54/9.99 inference(miniscoping,[status(thm)],[f381])).
% 35.54/9.99 fof(f868,plain,(
% 35.54/9.99 ![X0,X1,X2]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),X1))|~c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2)))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f867])).
% 35.54/9.99 fof(f869,plain,(
% 35.54/9.99 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f382])).
% 35.54/9.99 fof(f870,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f383])).
% 35.54/9.99 fof(f871,plain,(
% 35.54/9.99 ![X0]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),v_T____))|~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X0))),
% 35.54/9.99 inference(cnf_transformation,[status(thm)],[f384])).
% 35.54/9.99 fof(f875,definition,(
% 35.54/9.99 sQ0_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f876,plain,(
% 35.54/9.99 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))|~sQ0_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f875])).
% 35.54/9.99 fof(f878,definition,(
% 35.54/9.99 ![X0,X1,X2]: (sQ1_spl <=> (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),X1))|~c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f879,plain,(
% 35.54/9.99 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),X1))|~c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))|~sQ1_spl)),
% 35.54/9.99 inference(component_clause,[status(thm)],[f878])).
% 35.54/9.99 fof(f881,plain,(
% 35.54/9.99 sQ0_spl|sQ1_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f866,f875,f878])).
% 35.54/9.99 fof(f882,definition,(
% 35.54/9.99 sQ2_spl <=> (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f883,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~sQ2_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f882])).
% 35.54/9.99 fof(f885,plain,(
% 35.54/9.99 sQ2_spl|sQ1_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f868,f882,f878])).
% 35.54/9.99 fof(f886,definition,(
% 35.54/9.99 sQ3_spl <=> (c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f889,plain,(
% 35.54/9.99 sQ0_spl|~sQ3_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f869,f875,f886])).
% 35.54/9.99 fof(f890,plain,(
% 35.54/9.99 sQ2_spl|~sQ3_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f870,f882,f886])).
% 35.54/9.99 fof(f892,plain,(
% 35.54/9.99 ![X0]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),c_Type_Oty_OVoid))|~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X0))),
% 35.54/9.99 inference(backward_demodulation,[status(thm)],[f789,f871])).
% 35.54/9.99 fof(f898,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)),
% 35.54/9.99 inference(forward_demodulation,[status(thm)],[f789,f823])).
% 35.54/9.99 fof(f901,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/9.99 inference(resolution,[status(thm)],[f898,f388])).
% 35.54/9.99 fof(f902,definition,(
% 35.54/9.99 sQ4_spl <=> (c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(v_E____,v_P,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f905,definition,(
% 35.54/9.99 sQ5_spl <=> (c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f906,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ5_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f905])).
% 35.54/9.99 fof(f909,definition,(
% 35.54/9.99 sQ6_spl <=> (c_Type_Oty_OVoid=c_Type_Oty_OVoid)),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f913,plain,(
% 35.54/9.99 sQ3_spl|sQ5_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f901,f886,f905])).
% 35.54/9.99 fof(f916,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(v_E____,v_P,v_ha____,v_e_092_060_094isub_0622____))|c_TypeRel_Ohas__field(v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))),
% 35.54/9.99 inference(resolution,[status(thm)],[f393,f898])).
% 35.54/9.99 fof(f917,definition,(
% 35.54/9.99 sQ7_spl <=> (c_TypeRel_Ohas__field(v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f918,plain,(
% 35.54/9.99 c_TypeRel_Ohas__field(v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~sQ7_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f917])).
% 35.54/9.99 fof(f920,plain,(
% 35.54/9.99 sQ4_spl|sQ7_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f916,f902,f917])).
% 35.54/9.99 fof(f921,plain,(
% 35.54/9.99 c_Type_Oty_OVoid=c_Type_Oty_OVoid|c_TypeRel_Ohas__field(v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))),
% 35.54/9.99 inference(resolution,[status(thm)],[f394,f898])).
% 35.54/9.99 fof(f922,plain,(
% 35.54/9.99 sQ6_spl|sQ7_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f921,f909,f917])).
% 35.54/9.99 fof(f923,plain,(
% 35.54/9.99 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)|c_TypeRel_Ohas__field(v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))),
% 35.54/9.99 inference(resolution,[status(thm)],[f396,f898])).
% 35.54/9.99 fof(f924,plain,(
% 35.54/9.99 sQ3_spl|sQ7_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f923,f886,f917])).
% 35.54/9.99 fof(f1541,plain,(
% 35.54/9.99 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/9.99 inference(resolution,[status(thm)],[f768,f906])).
% 35.54/9.99 fof(f1542,definition,(
% 35.54/9.99 sQ8_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f1543,plain,(
% 35.54/9.99 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~sQ8_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f1542])).
% 35.54/9.99 fof(f1545,definition,(
% 35.54/9.99 sQ9_spl <=> (c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f1547,plain,(
% 35.54/9.99 ~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|sQ9_spl),
% 35.54/9.99 inference(component_clause,[status(thm)],[f1545])).
% 35.54/9.99 fof(f1548,plain,(
% 35.54/9.99 sQ8_spl|~sQ9_spl|~sQ5_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f1541,f1542,f1545,f905])).
% 35.54/9.99 fof(f1554,plain,(
% 35.54/9.99 c_Type_Oty_OVoid=c_Type_Oty_OVoid|c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),
% 35.54/9.99 inference(resolution,[status(thm)],[f772,f898])).
% 35.54/9.99 fof(f1555,definition,(
% 35.54/9.99 sQ10_spl <=> (c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/9.99 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 35.54/9.99 fof(f1558,plain,(
% 35.54/9.99 sQ6_spl|sQ10_spl),
% 35.54/9.99 inference(split_clause,[status(thm)],[f1554,f909,f1555])).
% 35.54/9.99 fof(f1562,plain,(
% 35.54/9.99 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellType_OWT(v_P,X0,X1,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ8_spl)),
% 35.54/9.99 inference(resolution,[status(thm)],[f1543,f655])).
% 35.54/9.99 fof(f1563,plain,(
% 35.54/9.99 ![X0,X1,X2,X3]: (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ8_spl)),
% 35.54/9.99 inference(resolution,[status(thm)],[f1543,f653])).
% 35.54/9.99 fof(f1565,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ8_spl)),
% 35.54/9.99 inference(resolution,[status(thm)],[f1543,f570])).
% 35.54/9.99 fof(f1566,plain,(
% 35.54/9.99 ![X0,X1,X2,X3,X4]: (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ8_spl)),
% 35.54/9.99 inference(resolution,[status(thm)],[f1543,f568])).
% 35.54/9.99 fof(f1568,definition,(
% 35.54/9.99 sQ11_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1571,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ12_spl <=> (~c_WellType_OWT(v_P,X0,X1,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1574,plain,(
% 35.54/10.00 sQ11_spl|sQ12_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1562,f1568,f1571,f1542])).
% 35.54/10.00 fof(f1575,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ13_spl <=> (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1578,plain,(
% 35.54/10.00 sQ13_spl|sQ11_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1563,f1575,f1568,f1542])).
% 35.54/10.00 fof(f1579,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ14_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1582,plain,(
% 35.54/10.00 sQ11_spl|sQ14_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1565,f1568,f1579,f1542])).
% 35.54/10.00 fof(f1583,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ15_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1586,plain,(
% 35.54/10.00 sQ15_spl|sQ11_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1566,f1583,f1568,f1542])).
% 35.54/10.00 fof(f1621,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(v_E____,v_P,v_ha____,v_e_092_060_094isub_0622____))|c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),
% 35.54/10.00 inference(resolution,[status(thm)],[f779,f898])).
% 35.54/10.00 fof(f1622,plain,(
% 35.54/10.00 sQ4_spl|sQ10_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1621,f902,f1555])).
% 35.54/10.00 fof(f1660,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f785,f906])).
% 35.54/10.00 fof(f1661,definition,(
% 35.54/10.00 sQ20_spl <=> (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1664,plain,(
% 35.54/10.00 sQ20_spl|~sQ9_spl|~sQ5_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1660,f1661,f1545,f905])).
% 35.54/10.00 fof(f1665,plain,(
% 35.54/10.00 $false|sQ9_spl),
% 35.54/10.00 inference(forward_subsumption_resolution,[status(thm)],[f1547,f766])).
% 35.54/10.00 fof(f1666,plain,(
% 35.54/10.00 sQ9_spl),
% 35.54/10.00 inference(contradiction_clause,[status(thm)],[f1665])).
% 35.54/10.00 fof(f1667,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/10.00 inference(resolution,[status(thm)],[f787,f898])).
% 35.54/10.00 fof(f1668,definition,(
% 35.54/10.00 sQ21_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1669,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ21_spl),
% 35.54/10.00 inference(component_clause,[status(thm)],[f1668])).
% 35.54/10.00 fof(f1671,plain,(
% 35.54/10.00 sQ3_spl|sQ21_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1667,f886,f1668])).
% 35.54/10.00 fof(f1736,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f906,f804])).
% 35.54/10.00 fof(f1743,definition,(
% 35.54/10.00 sQ25_spl <=> (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1746,plain,(
% 35.54/10.00 sQ25_spl|~sQ9_spl|~sQ5_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1736,f1743,f1545,f905])).
% 35.54/10.00 fof(f1796,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f815,f906])).
% 35.54/10.00 fof(f1797,definition,(
% 35.54/10.00 sQ31_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1798,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~sQ31_spl),
% 35.54/10.00 inference(component_clause,[status(thm)],[f1797])).
% 35.54/10.00 fof(f1800,plain,(
% 35.54/10.00 sQ31_spl|~sQ9_spl|~sQ5_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1796,f1797,f1545,f905])).
% 35.54/10.00 fof(f1874,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),
% 35.54/10.00 inference(resolution,[status(thm)],[f832,f898])).
% 35.54/10.00 fof(f1875,plain,(
% 35.54/10.00 sQ3_spl|sQ10_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1874,f886,f1555])).
% 35.54/10.00 fof(f1962,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ8_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f847,f1543])).
% 35.54/10.00 fof(f1966,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ38_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f1969,plain,(
% 35.54/10.00 sQ11_spl|sQ38_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f1962,f1568,f1966,f1542])).
% 35.54/10.00 fof(f2189,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~sQ2_spl),
% 35.54/10.00 inference(forward_demodulation,[status(thm)],[f789,f883])).
% 35.54/10.00 fof(f2230,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____))|~sQ0_spl),
% 35.54/10.00 inference(forward_demodulation,[status(thm)],[f789,f876])).
% 35.54/10.00 fof(f2231,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),c_Type_Oty_OVoid))|~sQ0_spl),
% 35.54/10.00 inference(forward_demodulation,[status(thm)],[f789,f2230])).
% 35.54/10.00 fof(f2232,plain,(
% 35.54/10.00 ~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))|~sQ0_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f2231,f892])).
% 35.54/10.00 fof(f2243,plain,(
% 35.54/10.00 $false|~sQ2_spl|~sQ0_spl),
% 35.54/10.00 inference(forward_subsumption_resolution,[status(thm)],[f2232,f2189])).
% 35.54/10.00 fof(f2244,plain,(
% 35.54/10.00 ~sQ2_spl|~sQ0_spl),
% 35.54/10.00 inference(contradiction_clause,[status(thm)],[f2243])).
% 35.54/10.00 fof(f2256,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(v_E____,v_P,v_ha____,v_e_092_060_094isub_0622____))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/10.00 inference(resolution,[status(thm)],[f898,f842])).
% 35.54/10.00 fof(f2270,plain,(
% 35.54/10.00 sQ4_spl|sQ21_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f2256,f902,f1668])).
% 35.54/10.00 fof(f2302,plain,(
% 35.54/10.00 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f906,f856])).
% 35.54/10.00 fof(f2303,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|~sQ5_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f906,f835])).
% 35.54/10.00 fof(f2313,definition,(
% 35.54/10.00 sQ48_spl <=> (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f2316,plain,(
% 35.54/10.00 sQ48_spl|~sQ9_spl|~sQ5_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f2302,f2313,f1545,f905])).
% 35.54/10.00 fof(f2317,definition,(
% 35.54/10.00 sQ49_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f2318,plain,(
% 35.54/10.00 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))))|~sQ49_spl),
% 35.54/10.00 inference(component_clause,[status(thm)],[f2317])).
% 35.54/10.00 fof(f2320,plain,(
% 35.54/10.00 sQ49_spl|~sQ9_spl|~sQ5_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f2303,f2317,f1545,f905])).
% 35.54/10.00 fof(f2335,plain,(
% 35.54/10.00 ![X0]: (~c_TypeRel_Ohas__field(v_P,X0,v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X0))|~sQ1_spl|~sQ21_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f879,f1669])).
% 35.54/10.00 fof(f2337,plain,(
% 35.54/10.00 ![X0,X1]: (~c_TypeRel_Ohas__field(v_P,X0,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X1)|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X0))|~sQ1_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f879,f824])).
% 35.54/10.00 fof(f2339,definition,(
% 35.54/10.00 ![X0]: (sQ50_spl <=> (~c_TypeRel_Ohas__field(v_P,X0,v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X0))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f2340,plain,(
% 35.54/10.00 ![X0]: (~c_TypeRel_Ohas__field(v_P,X0,v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X0))|~sQ50_spl)),
% 35.54/10.00 inference(component_clause,[status(thm)],[f2339])).
% 35.54/10.00 fof(f2342,plain,(
% 35.54/10.00 sQ50_spl|~sQ10_spl|~sQ1_spl|~sQ21_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f2335,f2339,f1555,f878,f1668])).
% 35.54/10.00 fof(f2503,plain,(
% 35.54/10.00 ~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ1_spl|~sQ7_spl),
% 35.54/10.00 inference(resolution,[status(thm)],[f2337,f918])).
% 35.54/10.00 fof(f2504,definition,(
% 35.54/10.00 sQ62_spl <=> (c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f2507,plain,(
% 35.54/10.00 ~sQ62_spl|~sQ5_spl|~sQ1_spl|~sQ7_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f2503,f2504,f905,f878,f917])).
% 35.54/10.00 fof(f4793,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f849])).
% 35.54/10.00 fof(f4794,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f847])).
% 35.54/10.00 fof(f4796,plain,(
% 35.54/10.00 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellType_OWT(v_P,X0,X1,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f655])).
% 35.54/10.00 fof(f4797,plain,(
% 35.54/10.00 ![X0,X1,X2,X3]: (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f653])).
% 35.54/10.00 fof(f4799,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f570])).
% 35.54/10.00 fof(f4800,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ31_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1798,f568])).
% 35.54/10.00 fof(f4810,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ81_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4813,definition,(
% 35.54/10.00 sQ82_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4816,plain,(
% 35.54/10.00 sQ81_spl|sQ82_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4793,f4810,f4813,f1797])).
% 35.54/10.00 fof(f4817,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ83_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4820,plain,(
% 35.54/10.00 sQ82_spl|sQ83_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4794,f4813,f4817,f1797])).
% 35.54/10.00 fof(f4821,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ84_spl <=> (~c_WellType_OWT(v_P,X0,X1,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4824,plain,(
% 35.54/10.00 sQ82_spl|sQ84_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4796,f4813,f4821,f1797])).
% 35.54/10.00 fof(f4825,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ85_spl <=> (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4828,plain,(
% 35.54/10.00 sQ85_spl|sQ82_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4797,f4825,f4813,f1797])).
% 35.54/10.00 fof(f4829,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ86_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4832,plain,(
% 35.54/10.00 sQ82_spl|sQ86_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4799,f4813,f4829,f1797])).
% 35.54/10.00 fof(f4833,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ87_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XFAssRed1__Xhyps__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f4836,plain,(
% 35.54/10.00 sQ87_spl|sQ82_spl|~sQ31_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f4800,f4833,f4813,f1797])).
% 35.54/10.00 fof(f8318,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ8_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f1543,f849])).
% 35.54/10.00 fof(f8332,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ89_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XFAssRed1__2__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f8335,plain,(
% 35.54/10.00 sQ89_spl|sQ11_spl|~sQ8_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f8318,f8332,f1568,f1542])).
% 35.54/10.00 fof(f13585,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f849])).
% 35.54/10.00 fof(f13586,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f847])).
% 35.54/10.00 fof(f13588,plain,(
% 35.54/10.00 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_WellType_OWT(v_P,X0,X1,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f655])).
% 35.54/10.00 fof(f13589,plain,(
% 35.54/10.00 ![X0,X1,X2,X3]: (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f653])).
% 35.54/10.00 fof(f13591,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f570])).
% 35.54/10.00 fof(f13592,plain,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____)))|~sQ49_spl)),
% 35.54/10.00 inference(resolution,[status(thm)],[f2318,f568])).
% 35.54/10.00 fof(f13599,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ91_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13602,definition,(
% 35.54/10.00 sQ92_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____))),v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13605,plain,(
% 35.54/10.00 sQ91_spl|sQ92_spl|~sQ49_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f13585,f13599,f13602,f2317])).
% 35.54/10.00 fof(f13606,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ93_spl <=> (~c_WellTypeRT_OWTrt(v_P,X0,X1,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellTypeRT_OWTrt(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_WellTypeRT_OWTrt(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13609,plain,(
% 35.54/10.00 sQ92_spl|sQ93_spl|~sQ49_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f13586,f13602,f13606,f2317])).
% 35.54/10.00 fof(f13610,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ94_spl <=> (~c_WellType_OWT(v_P,X0,X1,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13613,plain,(
% 35.54/10.00 sQ92_spl|sQ94_spl|~sQ49_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f13588,f13602,f13610,f2317])).
% 35.54/10.00 fof(f13614,definition,(
% 35.54/10.00 ![X0,X1,X2,X3]: (sQ95_spl <=> (~c_WellType_OWT(v_P,X0,X1,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_WellType_OWT(v_P,X0,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_WellType_OWT(v_P,X0,X3,c_Type_Oty_OBoolean)|c_WellType_OWT(v_P,X0,c_Expr_Oexp_OCond(X3,X2,X1,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13617,plain,(
% 35.54/10.00 sQ95_spl|sQ92_spl|~sQ49_spl),
% 35.54/10.00 inference(split_clause,[status(thm)],[f13589,f13614,f13602,f2317])).
% 35.54/10.00 fof(f13618,definition,(
% 35.54/10.00 ![X0,X1,X2,X3,X4]: (sQ96_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 35.54/10.00 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 35.54/10.00 fof(f13621,plain,(
% 35.54/10.00 sQ92_spl|sQ96_spl|~sQ49_spl),
% 19.59/10.02 inference(split_clause,[status(thm)],[f13591,f13602,f13618,f2317])).
% 19.59/10.02 fof(f13622,definition,(
% 19.59/10.02 ![X0,X1,X2,X3,X4]: (sQ97_spl <=> (~c_Progress_OWTrt_H(v_P,X0,X1,X2,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~c_Progress_OWTrt_H(v_P,X0,X1,X3,v_sko__local__XIH__1(v_E____,v_P,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)),v_e_Ha____,v_h_Ha____))|~c_Progress_OWTrt_H(v_P,X0,X1,X4,c_Type_Oty_OBoolean)|c_Progress_OWTrt_H(v_P,X0,X1,c_Expr_Oexp_OCond(X4,X3,X2,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))))),
% 19.59/10.02 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 19.59/10.02 fof(f13625,plain,(
% 19.59/10.02 sQ97_spl|sQ92_spl|~sQ49_spl),
% 19.59/10.02 inference(split_clause,[status(thm)],[f13592,f13622,f13602,f2317])).
% 19.59/10.02 fof(f13626,plain,(
% 19.59/10.02 ~c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,v_e_092_060_094isub_0622____)))|~sQ50_spl|~sQ7_spl),
% 19.59/10.02 inference(resolution,[status(thm)],[f2340,f918])).
% 19.59/10.02 fof(f13627,plain,(
% 19.59/10.02 ~sQ5_spl|~sQ50_spl|~sQ7_spl),
% 19.59/10.02 inference(split_clause,[status(thm)],[f13626,f905,f2339,f917])).
% 19.59/10.02 fof(f13628,plain,(
% 19.59/10.02 $false),
% 19.59/10.02 inference(sat_refutation,[status(thm)],[f881,f885,f889,f890,f913,f920,f922,f924,f1548,f1558,f1574,f1578,f1582,f1586,f1622,f1664,f1666,f1671,f1746,f1800,f1875,f1969,f2244,f2270,f2316,f2320,f2342,f2507,f4816,f4820,f4824,f4828,f4832,f4836,f8335,f13605,f13609,f13613,f13617,f13621,f13625,f13627])).
% 19.59/10.02 % SZS output end CNFRefutation for theBenchmark.p
% 19.59/10.09 % Elapsed time: 4.695129 seconds
% 19.59/10.09 % CPU time: 36.754758 seconds
% 19.59/10.09 % Total memory used: 738.120 MB
% 19.59/10.09 % Net memory used: 732.116 MB
%------------------------------------------------------------------------------