%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV956-1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:21:50 EDT 2022 % Result : Unknown 5.78s 5.94s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV956-1 : TPTP v8.1.0. Released v4.1.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.14/0.34 % Computer : n005.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Jul 27 06:17:50 EDT 2022 % 0.14/0.34 % CPUTime : % 5.78/5.92 ----- Otter 3.3f, August 2004 ----- % 5.78/5.92 The process was started by sandbox on n005.cluster.edu, % 5.78/5.92 Wed Jul 27 06:17:50 2022 % 5.78/5.92 The command was "./otter". The process ID is 27190. % 5.78/5.92 % 5.78/5.92 set(prolog_style_variables). % 5.78/5.92 set(auto). % 5.78/5.92 dependent: set(auto1). % 5.78/5.92 dependent: set(process_input). % 5.78/5.92 dependent: clear(print_kept). % 5.78/5.92 dependent: clear(print_new_demod). % 5.78/5.92 dependent: clear(print_back_demod). % 5.78/5.92 dependent: clear(print_back_sub). % 5.78/5.92 dependent: set(control_memory). % 5.78/5.92 dependent: assign(max_mem, 12000). % 5.78/5.92 dependent: assign(pick_given_ratio, 4). % 5.78/5.92 dependent: assign(stats_level, 1). % 5.78/5.92 dependent: assign(max_seconds, 10800). % 5.78/5.92 clear(print_given). % 5.78/5.92 % 5.78/5.92 list(usable). % 5.78/5.92 0 [] A=A. % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T)| -c_Type_Ois__refT(V_T_092_060_094isub_062r)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T_092_060_094isub_062r). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,V_a,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__7__1(V_D,V_E,V_F,V_P,V_T,V_a)))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAcc(V_a,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T)| -c_Type_Ois__refT(V_T_092_060_094isub_062r)| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T_092_060_094isub_062r). % 5.78/5.92 0 [] c_Type_Ois__refT(c_Type_Oty_ONT). % 5.78/5.92 0 [] c_Type_Ois__refT(c_Type_Oty_OClass(V_x)). % 5.78/5.92 0 [] 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__7__1(V_D,V_E,V_F,V_P,V_T,V_e,V_h)))| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a). % 5.78/5.92 0 [] 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__7__1(V_D,V_E,V_F,V_P,V_T,V_e,V_h),V_F,V_T,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_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a)!=c_Expr_Oexp_Onew(V_list,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a). % 5.78/5.92 0 [] 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_Owiden(V_P,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),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). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp_H,T_a)!=c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp_H,T_a)!=c_Expr_Oexp_OCast(V_list,V_exp,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp_H,T_a)!=c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a). % 5.78/5.92 0 [] c_TypeRel_Osees__field(V_P,c_WellType_Osko__WellType__XWT__elim__cases__7__1(V_D,V_E,V_F,V_P,V_T,V_a),V_F,V_T,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAcc(V_a,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp_H,T_a)!=c_Expr_Oexp_OSe_q(V_exp1,V_exp2,T_a). % 5.78/5.92 0 [] V_T=c_Type_Oty_OVoid|c_TypeRel_Owiden(V_P,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),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). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCast(V_C,V_e,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(V_C))| -c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Type_Ois__refT(V_T)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a)|V_exp=V_exp_H. % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OCast(V_C,V_e,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(V_C))| -c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Type_Ois__refT(V_T)| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_Decl_Ois__class(V_P,V_C,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_Onew(V_C,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Decl_Ois__class(V_P,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCast(V_D,V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a)|V_list2=V_list2_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a)|V_list1=V_list1_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a)|V_exp=V_exp_H. % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a). % 5.78/5.92 0 [] V_T=c_Type_Oty_OVoid| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T)| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_ONT). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|c_TypeRel_Owiden(V_P,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),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). % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)!=c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1,V_exp2,T_a)!=c_Expr_Oexp_Othrow(V_exp_H,T_a). % 5.78/5.92 0 [] c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp_H,V_list1_H,V_list2_H,T_a)!=c_Expr_Oexp_OCast(V_list,V_exp,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Othrow(V_exp_H,T_a)!=c_Expr_Oexp_Onew(V_list,T_a). % 5.78/5.92 0 [] c_Decl_Ois__class(V_P,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_OCast(V_D,V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)!=c_Expr_Oexp_OFAcc(V_exp,V_list1,V_list2,T_a). % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] c_Type_Oty_OVoid!=c_Type_Oty_OClass(V_list_H). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -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,c_Type_Oty_ONT). % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(V_C,V_P,V_T,T_a))|V_T=c_Type_Oty_ONT| -c_TypeRel_Owiden(V_P,V_T,c_Type_Oty_OClass(V_C),T_a). % 5.78/5.92 0 [] c_Pair(V_a,V_b,T_a,T_b)!=c_Pair(V_a_H,V_b_H,T_a,T_b)|V_b=V_b_H. % 5.78/5.92 0 [] c_Pair(V_a,V_b,T_a,T_b)!=c_Pair(V_a_H,V_b_H,T_a,T_b)|V_a=V_a_H. % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)!=c_Expr_Oexp_Onew(V_list,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a). % 5.78/5.92 0 [] 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)))). % 5.78/5.92 0 [] c_Type_Oty_ONT!=c_Type_Oty_OClass(V_list_H). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -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,c_Type_Oty_ONT). % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] 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))|V_T=c_Type_Oty_OVoid| -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). % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)!=c_Expr_Oexp_OCast(V_list,V_exp,T_a). % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] V_D_H=V_D| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T_H,V_D_H,T_a)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,T_a). % 5.78/5.92 0 [] V_T_H=V_T| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T_H,V_D_H,T_a)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,T_a). % 5.78/5.92 0 [] c_Type_Oty_ONT!=c_Type_Oty_OVoid. % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(V_C))| -c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__6__1(V_D,V_E,V_P,V_e)))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCast(V_D,V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Type_Oty_OClass(V_list_H)!=c_Type_Oty_OVoid. % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(V_C))| -c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a)!=c_Expr_Oexp_Onew(V_list,T_a). % 5.78/5.92 0 [] c_TypeRel_Osees__field(V_P,c_WellType_Osko__WellType__XWT__elim__cases__8__1(V_D,V_E,V_F,V_P,V_a,V_v),V_F,c_WellType_Osko__WellType__XWT__elim__cases__8__2(V_D,V_E,V_F,V_P,V_a,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_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_a,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] V_a1=c_Type_Oty_ONT|V_a1=c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__1(V_P,V_a1,V_a2))|V_a2=V_a1| -c_TypeRel_Owiden(V_P,V_a1,V_a2,t_a). % 5.78/5.92 0 [] V_a1=c_Type_Oty_ONT|V_a2=c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__2(V_P,V_a1,V_a2))|V_a2=V_a1| -c_TypeRel_Owiden(V_P,V_a1,V_a2,t_a). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(V_C))| -c_Decl_Ois__class(V_P,V_C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_WellType_OWT(V_P,V_E,V_e,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT)|V_T=c_Type_Oty_OVoid| -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). % 5.78/5.92 0 [] c_Type_Oty_OClass(V_list_H)!=c_Type_Oty_ONT. % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T)| -c_TypeRel_Ohas__field(V_P,V_C,V_F,V_T,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] c_TypeRel_Ohas__field(V_P,V_C,V_F,V_T,V_D,T_a)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_Onew(V_list_H,T_a)|V_list=V_list_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)!=c_Expr_Oexp_Onew(V_list,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_Onew(V_list,T_a)!=c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a)|V_list=V_list_H. % 5.78/5.92 0 [] c_Expr_Oexp_OCast(V_list,V_exp,T_a)!=c_Expr_Oexp_OCast(V_list_H,V_exp_H,T_a)|V_exp=V_exp_H. % 5.78/5.92 0 [] c_Type_Oty_OVoid!=c_Type_Oty_ONT. % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)!=c_Expr_Oexp_OCast(V_list,V_exp,T_a). % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAcc(V_e,V_F,V_D,tc_List_Olist(tc_String_Ochar)),V_T)| -c_TypeRel_Ohas__field(V_P,V_C,V_F,V_T,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,V_e,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] c_TypeRel_Osees__field(V_P,V_D,V_F,V_T,V_D,T_a)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)!=c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a). % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1,V_exp2,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)|V_exp2=V_exp2_H. % 5.78/5.92 0 [] c_Expr_Oexp_OSe_q(V_exp1,V_exp2,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a)|V_exp1=V_exp1_H. % 5.78/5.92 0 [] 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)))). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(V_P,V_T_092_060_094isub_0622,V_T,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)| -c_TypeRel_Ohas__field(V_P,V_C,V_F,V_T,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e_092_060_094isub_0621,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] V_T=c_Type_Oty_OVoid| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_a,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(V_P,V_T_092_060_094isub_0622,V_T,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,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)| -c_TypeRel_Ohas__field(V_P,V_C,V_F,V_T,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,V_e_092_060_094isub_0621,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,V_a,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__8__1(V_D,V_E,V_F,V_P,V_a,V_v)))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_a,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Objects_Ohext(V_h,V_h). % 5.78/5.92 0 [] c_Objects_Ohext(V_h,V_h_H_H)| -c_Objects_Ohext(V_h_H,V_h_H_H)| -c_Objects_Ohext(V_h,V_h_H). % 5.78/5.92 0 [] c_TypeRel_Owiden(V_P,c_Type_Oty_ONT,c_Type_Oty_OClass(V_C),T_a). % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_sko__local__XIH__1(V_Ea,v_P,V_Ta,v_e_Ha____,v_h_Ha____),V_Ta,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_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)))). % 5.78/5.92 0 [] c_TypeRel_Owiden(V_P,V_S,V_T,T_a)| -c_TypeRel_Owiden(V_P,V_U,V_T,T_a)| -c_TypeRel_Owiden(V_P,V_S,V_U,T_a). % 5.78/5.92 0 [] c_TypeRel_Owiden(V_P,V_T,V_T,T_a). % 5.78/5.92 0 [] c_COMBI(V_P,T_a)=V_P. % 5.78/5.92 0 [] 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). % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_sko__local__XFAssRed1__Xhyps__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____),V_T,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____,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)))). % 5.78/5.92 0 [] 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)))). % 5.78/5.92 0 [] c_Map_Omap__le(V_f,V_f,T_a,T_b). % 5.78/5.92 0 [] c_Map_Omap__le(V_m1,V_m3,T_a,T_b)| -c_Map_Omap__le(V_m2,V_m3,T_a,T_b)| -c_Map_Omap__le(V_m1,V_m2,T_a,T_b). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E_H,V_e,V_T)| -c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)| -c_WellType_OWT(V_P,V_E,V_e,V_T). % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(V_D)| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OCast(V_D,V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Type_Oty_OClass(V_list)!=c_Type_Oty_OClass(V_list_H)|V_list=V_list_H. % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(V_C)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)|V_exp2=V_exp2_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)|V_list2=V_list2_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)|V_list1=V_list1_H. % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_OFAss(V_exp1_H,V_list1_H,V_list2_H,V_exp2_H,T_a)|V_exp1=V_exp1_H. % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_sko__unknown__thm__BwWC__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____,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_ONT). % 5.78/5.92 0 [] v_T____=c_Type_Oty_OVoid. % 5.78/5.92 0 [] c_Expr_Oexp_OFAss(V_exp1,V_list1,V_list2,V_exp2,T_a)!=c_Expr_Oexp_OSe_q(V_exp1_H,V_exp2_H,T_a). % 5.78/5.92 0 [] 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)))). % 5.78/5.92 0 [] V_T=c_Type_Oty_OVoid|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). % 5.78/5.92 0 [] V_f=V_g| -c_Map_Omap__le(V_g,V_f,T_a,T_b)| -c_Map_Omap__le(V_f,V_g,T_a,T_b). % 5.78/5.92 0 [] V_T=c_Type_Oty_OVoid|V_T=c_Type_Oty_OVoid| -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). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,V_v,c_WellType_Osko__WellType__XWT__elim__cases__8__3(V_D,V_E,V_F,V_P,V_a,V_v))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_a,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(V_C)| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_Onew(V_C,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_TypeRel_Owiden(V_P,c_WellType_Osko__WellType__XWT__elim__cases__8__3(V_D,V_E,V_F,V_P,V_a,V_v),c_WellType_Osko__WellType__XWT__elim__cases__8__2(V_D,V_E,V_F,V_P,V_a,V_v),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_a,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OSe_q(V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T_092_060_094isub_0622)| -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_T_092_060_094isub_0621). % 5.78/5.92 0 [] 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__unknown__thm__BwWC__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). % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_sko__local__XFAssRed1__2__1(V_E,v_P,V_T,v_e_Ha____,v_h_Ha____),V_T,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____,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)))). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(V_P,V_T_H,V_T,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0622,V_T_H)| -c_TypeRel_Osees__field(V_P,V_C,V_F,V_T,V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,c_Type_Oty_OClass(V_C)). % 5.78/5.92 0 [] 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_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). % 5.78/5.92 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OSe_q(V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T_092_060_094isub_0622)| -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_T_092_060_094isub_0621). % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(V_T))| -c_TypeRel_Owiden(V_P,c_Type_Oty_OClass(V_C),V_T,T_a). % 5.78/5.92 0 [] V_T=c_Type_Oty_OClass(V_D)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OCast(V_D,V_e,tc_List_Olist(tc_String_Ochar)),V_T). % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_U____,c_Type_Oty_OClass(v_C____),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 0 [] 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)))). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OSe_q(V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T_092_060_094isub_0622)| -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_T_092_060_094isub_0621). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(v_C____)). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E_H,V_e,V_T)| -c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T)| -c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_TypeRel_Owiden(v_P,v_T_092_060_094isub_0622____,v_TF____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 0 [] 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____). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T)| -c_WellType_OWT(V_P,V_E,V_e,V_T). % 5.78/5.92 0 [] c_WellTypeRT_OWTrt(V_P,V_h_H,V_E,V_e,V_T)| -c_Objects_Ohext(V_h,V_h_H)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T). % 5.78/5.92 0 [] c_COMBI(v_P,t_a)=v_P. % 5.78/5.92 0 [] -c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____). % 5.78/5.92 0 [] c_fe_qual(V_x,V_x,T_a). % 5.78/5.92 0 [] V_X=V_Y| -c_fe_qual(V_X,V_Y,T_a). % 5.78/5.92 end_of_list. % 5.78/5.92 % 5.78/5.92 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 5.78/5.92 % 5.78/5.92 This ia a non-Horn set with equality. The strategy will be % 5.78/5.92 Knuth-Bendix, ordered hyper_res, factoring, and unit % 5.78/5.92 deletion, with positive clauses in sos and nonpositive % 5.78/5.92 clauses in usable. % 5.78/5.92 % 5.78/5.92 dependent: set(knuth_bendix). % 5.78/5.92 dependent: set(anl_eq). % 5.78/5.92 dependent: set(para_from). % 5.78/5.92 dependent: set(para_into). % 5.78/5.92 dependent: clear(para_from_right). % 5.78/5.92 dependent: clear(para_into_right). % 5.78/5.92 dependent: set(para_from_vars). % 5.78/5.92 dependent: set(eq_units_both_ways). % 5.78/5.92 dependent: set(dynamic_demod_all). % 5.78/5.92 dependent: set(dynamic_demod). % 5.78/5.92 dependent: set(order_eq). % 5.78/5.92 dependent: set(back_demod). % 5.78/5.92 dependent: set(lrpo). % 5.78/5.92 dependent: set(hyper_res). % 5.78/5.92 dependent: set(unit_deletion). % 5.78/5.92 dependent: set(factor). % 5.78/5.92 % 5.78/5.92 ------------> process usable: % 5.78/5.92 ** KEPT (pick-wt=17): 1 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_Othrow(D,tc_List_Olist(tc_String_Ochar)),E)| -c_Type_Ois__refT(F)| -c_WellTypeRT_OWTrt(A,B,C,D,F). % 5.78/5.92 ** KEPT (pick-wt=22): 2 [] c_WellType_OWT(A,B,C,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__7__1(D,B,E,A,F,C)))| -c_WellType_OWT(A,B,c_Expr_Oexp_OFAcc(C,E,D,tc_List_Olist(tc_String_Ochar)),F). % 5.78/5.92 ** KEPT (pick-wt=17): 3 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_Othrow(D,tc_List_Olist(tc_String_Ochar)),E)| -c_Type_Ois__refT(F)| -c_Progress_OWTrt_H(A,B,C,D,F). % 5.78/5.92 ** KEPT (pick-wt=31): 4 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__7__1(E,C,F,A,G,D,B)))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAcc(D,F,E,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=9): 5 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_Othrow(E,D). % 5.78/5.92 ** KEPT (pick-wt=37): 6 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_TypeRel_Ohas__field(A,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__7__1(E,C,F,A,G,D,B),F,G,E,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAcc(D,F,E,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=9): 7 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_Onew(E,D). % 5.78/5.92 ** KEPT (pick-wt=10): 8 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_Othrow(F,E). % 5.78/5.92 ** KEPT (pick-wt=9): 9 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OFAcc(C,D,E,B). % 5.78/5.92 ** KEPT (pick-wt=47): 10 [] c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D))|c_TypeRel_Owiden(A,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(E,C,F,A,G,B,D),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(E,C,F,A,G,B,D),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(G,F,E,D,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=9): 11 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OFAcc(C,D,E,B). % 5.78/5.92 ** KEPT (pick-wt=8): 12 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OCast(C,D,B). % 5.78/5.92 ** KEPT (pick-wt=10): 13 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OFAss(C,D,E,F,B). % 5.78/5.92 ** KEPT (pick-wt=7): 14 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_Othrow(C,B). % 5.78/5.92 ** KEPT (pick-wt=29): 15 [] c_TypeRel_Osees__field(A,c_WellType_Osko__WellType__XWT__elim__cases__7__1(B,C,D,A,E,F),D,E,B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,C,c_Expr_Oexp_OFAcc(F,D,B,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 ** KEPT (pick-wt=10): 16 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OFAcc(D,E,F,C). % 5.78/5.92 ** KEPT (pick-wt=8): 17 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OSe_q(C,D,B). % 5.78/5.92 ** KEPT (pick-wt=40): 18 [] A=c_Type_Oty_OVoid|c_TypeRel_Owiden(B,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(C,D,E,B,F,G,H),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(C,D,E,B,F,G,H),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(B,G,D,c_Expr_Oexp_OFAss(F,E,C,H,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=29): 19 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OCast(D,E,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(D))| -c_Decl_Ois__class(A,D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Type_Ois__refT(F)| -c_WellTypeRT_OWTrt(A,B,C,E,F). % 5.78/5.92 ** KEPT (pick-wt=10): 20 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_Othrow(C,B)|A=C. % 5.78/5.92 ** KEPT (pick-wt=29): 21 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OCast(D,E,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(D))| -c_Decl_Ois__class(A,D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Type_Ois__refT(F)| -c_Progress_OWTrt_H(A,B,C,E,F). % 5.78/5.92 ** KEPT (pick-wt=19): 22 [] c_Decl_Ois__class(A,B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,C,D,c_Expr_Oexp_Onew(B,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 ** KEPT (pick-wt=19): 23 [] c_Decl_Ois__class(A,B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,C,c_Expr_Oexp_OCast(B,D,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 ** KEPT (pick-wt=10): 24 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OSe_q(E,F,D). % 5.78/5.92 ** KEPT (pick-wt=14): 25 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OFAcc(E,F,G,D)|C=G. % 5.78/5.92 ** KEPT (pick-wt=14): 26 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OFAcc(E,F,G,D)|B=F. % 5.78/5.92 ** KEPT (pick-wt=14): 27 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OFAcc(E,F,G,D)|A=E. % 5.78/5.92 ** KEPT (pick-wt=17): 28 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAcc(D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT). % 5.78/5.92 ** KEPT (pick-wt=8): 29 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_Othrow(D,C). % 5.78/5.92 ** KEPT (pick-wt=11): 30 [] A=c_Type_Oty_OVoid| -c_WellType_OWT(B,C,c_Expr_Oexp_Othrow(D,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=17): 31 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OFAcc(D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -c_Progress_OWTrt_H(A,B,C,D,c_Type_Oty_ONT). % 5.78/5.92 ** KEPT (pick-wt=43): 32 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_TypeRel_Owiden(A,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(E,C,F,A,D,B,G),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(E,C,F,A,D,B,G),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,F,E,G,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=12): 33 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAcc(F,G,H,E). % 5.78/5.92 ** KEPT (pick-wt=8): 34 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_Othrow(D,C). % 5.78/5.92 ** KEPT (pick-wt=18): 35 [] c_Decl_Ois__class(A,B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,C,c_Expr_Oexp_Onew(B,tc_List_Olist(tc_String_Ochar)),D). % 5.78/5.92 ** KEPT (pick-wt=10): 36 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OCast(E,F,D). % 5.78/5.92 ** KEPT (pick-wt=12): 37 [] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OFAss(E,F,G,H,D). % 5.78/5.92 ** KEPT (pick-wt=7): 38 [] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_Onew(C,B). % 5.78/5.92 ** KEPT (pick-wt=20): 39 [] c_Decl_Ois__class(A,B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,C,D,c_Expr_Oexp_OCast(B,E,tc_List_Olist(tc_String_Ochar)),F). % 5.78/5.92 ** KEPT (pick-wt=10): 40 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OFAcc(D,E,F,C). % 5.78/5.92 ** KEPT (pick-wt=45): 41 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_TypeRel_Ohas__field(A,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(E,C,F,A,D,B,G),F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(E,C,F,A,D,B,G),E,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,F,E,G,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=4): 43 [copy,42,flip.1] c_Type_Oty_OClass(A)!=c_Type_Oty_OVoid. % 5.78/5.92 ** KEPT (pick-wt=24): 44 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,E,F,G,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_WellTypeRT_OWTrt(A,B,C,G,H)| -c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT). % 5.78/5.92 ** KEPT (pick-wt=17): 46 [copy,45,flip.1] c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__Xwiden__Class__1__1(A,B,C,D))=C|C=c_Type_Oty_ONT| -c_TypeRel_Owiden(B,C,c_Type_Oty_OClass(A),D). % 5.78/5.92 ** KEPT (pick-wt=14): 47 [] c_Pair(A,B,C,D)!=c_Pair(E,F,C,D)|B=F. % 5.78/5.92 ** KEPT (pick-wt=14): 48 [] c_Pair(A,B,C,D)!=c_Pair(E,F,C,D)|A=E. % 5.78/5.92 ** KEPT (pick-wt=8): 49 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_Onew(D,C). % 5.78/5.92 ** KEPT (pick-wt=9): 50 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OSe_q(D,E,C). % 5.78/5.92 ** KEPT (pick-wt=8): 51 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OSe_q(C,D,B). % 5.78/5.92 ** KEPT (pick-wt=4): 53 [copy,52,flip.1] c_Type_Oty_OClass(A)!=c_Type_Oty_ONT. % 5.78/5.92 ** KEPT (pick-wt=24): 54 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OFAss(D,E,F,G,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_Progress_OWTrt_H(A,B,C,G,H)| -c_Progress_OWTrt_H(A,B,C,D,c_Type_Oty_ONT). % 5.78/5.92 ** KEPT (pick-wt=28): 55 [] A=c_Type_Oty_OVoid|c_WellTypeRT_OWTrt(B,C,D,E,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(F,D,G,B,H,C,E))| -c_WellTypeRT_OWTrt(B,C,D,c_Expr_Oexp_OFAss(H,G,F,E,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=25): 56 [] c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D))|E=c_Type_Oty_OVoid| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(F,G,H,D,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 ** KEPT (pick-wt=11): 57 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OCast(F,G,E). % 5.78/5.92 ** KEPT (pick-wt=35): 58 [] c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D))|c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(E,C,F,A,G,B,D))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(G,F,E,D,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=17): 59 [] A=B| -c_TypeRel_Osees__field(C,D,E,F,A,G)| -c_TypeRel_Osees__field(C,D,E,H,B,G). % 5.78/5.92 ** KEPT (pick-wt=17): 60 [] A=B| -c_TypeRel_Osees__field(C,D,E,A,F,G)| -c_TypeRel_Osees__field(C,D,E,B,H,G). % 5.78/5.92 ** KEPT (pick-wt=3): 62 [copy,61,flip.1] c_Type_Oty_OVoid!=c_Type_Oty_ONT. % 5.78/5.92 ** KEPT (pick-wt=20): 63 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_Onew(D,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(D))| -c_Decl_Ois__class(A,D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 ** KEPT (pick-wt=19): 64 [] c_WellType_OWT(A,B,C,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__6__1(D,B,A,C)))| -c_WellType_OWT(A,B,c_Expr_Oexp_OCast(D,C,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 Following clause subsumed by 43 during input processing: 0 [] c_Type_Oty_OClass(A)!=c_Type_Oty_OVoid. % 5.78/5.92 ** KEPT (pick-wt=29): 65 [] c_WellType_OWT(A,B,c_Expr_Oexp_OFAcc(C,D,E,tc_List_Olist(tc_String_Ochar)),F)| -c_TypeRel_Osees__field(A,G,D,F,E,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,B,C,c_Type_Oty_OClass(G)). % 5.78/5.92 ** KEPT (pick-wt=19): 66 [] c_WellType_OWT(A,B,c_Expr_Oexp_Onew(C,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(C))| -c_Decl_Ois__class(A,C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 ** KEPT (pick-wt=49): 67 [] c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D))|c_TypeRel_Ohas__field(A,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(E,C,F,A,G,B,D),F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(E,C,F,A,G,B,D),E,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(G,F,E,D,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=8): 68 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_Onew(D,C). % 5.78/5.92 ** KEPT (pick-wt=36): 69 [] c_TypeRel_Osees__field(A,c_WellType_Osko__WellType__XWT__elim__cases__8__1(B,C,D,A,E,F),D,c_WellType_Osko__WellType__XWT__elim__cases__8__2(B,C,D,A,E,F),B,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,C,c_Expr_Oexp_OFAss(E,D,B,F,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=18): 71 [copy,70,flip.2] A=c_Type_Oty_ONT|c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__1(B,A,C))=A|C=A| -c_TypeRel_Owiden(B,A,C,t_a). % 5.78/5.92 ** KEPT (pick-wt=18): 73 [copy,72,flip.2] A=c_Type_Oty_ONT|c_Type_Oty_OClass(v_sko__TypeRel__Xwiden__Xcases__2(B,A,C))=C|C=A| -c_TypeRel_Owiden(B,A,C,t_a). % 5.78/5.92 ** KEPT (pick-wt=20): 74 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_Onew(D,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OClass(D))| -c_Decl_Ois__class(A,D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.92 ** KEPT (pick-wt=11): 75 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OFAss(D,E,F,G,C). % 5.78/5.92 ** KEPT (pick-wt=14): 76 [] c_WellType_OWT(A,B,c_Expr_Oexp_Othrow(C,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_WellType_OWT(A,B,C,c_Type_Oty_OClass(D)). % 5.78/5.92 ** KEPT (pick-wt=21): 77 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|E=c_Type_Oty_OVoid| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,F,G,H,tc_List_Olist(tc_String_Ochar)),E). % 5.78/5.92 Following clause subsumed by 53 during input processing: 0 [] c_Type_Oty_OClass(A)!=c_Type_Oty_ONT. % 5.78/5.92 ** KEPT (pick-wt=31): 78 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(A,B,C,E,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(F,C,G,A,D,B,E))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,G,F,E,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=31): 79 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OFAcc(D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -c_TypeRel_Ohas__field(A,H,E,G,F,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(A,B,C,D,c_Type_Oty_OClass(H)). % 5.78/5.92 ** KEPT (pick-wt=14): 80 [] c_TypeRel_Ohas__field(A,B,C,D,E,F)| -c_TypeRel_Osees__field(A,B,C,D,E,F). % 5.78/5.92 ** KEPT (pick-wt=10): 81 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OFAss(C,D,E,F,B). % 5.78/5.92 ** KEPT (pick-wt=10): 82 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_Onew(C,B)|A=C. % 5.78/5.92 ** KEPT (pick-wt=10): 83 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_Onew(F,E). % 5.78/5.92 ** KEPT (pick-wt=8): 84 [] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OCast(C,D,B). % 5.78/5.92 ** KEPT (pick-wt=12): 85 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OCast(D,E,C)|A=D. % 5.78/5.92 ** KEPT (pick-wt=12): 86 [] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OCast(D,E,C)|B=E. % 5.78/5.92 Following clause subsumed by 62 during input processing: 0 [] c_Type_Oty_OVoid!=c_Type_Oty_ONT. % 5.78/5.92 ** KEPT (pick-wt=9): 87 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OCast(D,E,C). % 5.78/5.92 ** KEPT (pick-wt=42): 88 [] A=c_Type_Oty_OVoid|c_TypeRel_Ohas__field(B,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(C,D,E,B,F,G,H),E,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(C,D,E,B,F,G,H),C,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(B,G,D,c_Expr_Oexp_OFAss(F,E,C,H,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=31): 89 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAcc(D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -c_TypeRel_Ohas__field(A,H,E,G,F,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_OClass(H)). % 5.78/5.92 ** KEPT (pick-wt=14): 90 [] c_TypeRel_Osees__field(A,B,C,D,B,E)| -c_TypeRel_Osees__field(A,F,C,D,B,E). % 5.78/5.92 ** KEPT (pick-wt=11): 91 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OFAss(D,E,F,G,C). % 5.78/5.92 ** KEPT (pick-wt=12): 92 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OSe_q(D,E,C)|B=E. % 5.78/5.92 ** KEPT (pick-wt=12): 93 [] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OSe_q(D,E,C)|A=D. % 5.78/5.92 ** KEPT (pick-wt=42): 94 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,A,v_e_Ha____,v_sko__local__XFAssRed1__Xhyps__2__1(A,v_P,B,v_e_Ha____,v_h_Ha____))| -c_WellTypeRT_OWTrt(v_P,v_ha____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=49): 95 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OFAss(D,E,F,G,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(A,H,I,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(A,B,C,G,H)| -c_TypeRel_Ohas__field(A,J,E,I,F,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_Progress_OWTrt_H(A,B,C,D,c_Type_Oty_OClass(J)). % 5.78/5.92 ** KEPT (pick-wt=14): 96 [] A=c_Type_Oty_OVoid| -c_WellType_OWT(B,C,c_Expr_Oexp_OFAss(D,E,F,G,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=49): 97 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,E,F,G,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(A,H,I,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,G,H)| -c_TypeRel_Ohas__field(A,J,E,I,F,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_OClass(J)). % 5.78/5.92 ** KEPT (pick-wt=23): 98 [] c_WellType_OWT(A,B,C,c_Type_Oty_OClass(c_WellType_Osko__WellType__XWT__elim__cases__8__1(D,B,E,A,C,F)))| -c_WellType_OWT(A,B,c_Expr_Oexp_OFAss(C,E,D,F,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=9): 99 [] c_Objects_Ohext(A,B)| -c_Objects_Ohext(C,B)| -c_Objects_Ohext(A,C). % 5.78/5.92 ** KEPT (pick-wt=47): 100 [] c_TypeRel_Owiden(v_P,v_sko__local__XIH__1(A,v_P,B,v_e_Ha____,v_h_Ha____),B,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____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=15): 101 [] c_TypeRel_Owiden(A,B,C,D)| -c_TypeRel_Owiden(A,E,C,D)| -c_TypeRel_Owiden(A,B,E,D). % 5.78/5.92 ** KEPT (pick-wt=32): 102 [] c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_ONT)|c_WellTypeRT_OWTrt(A,B,C,D,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(E,C,F,A,D,B,G)))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(D,F,E,G,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.92 ** KEPT (pick-wt=47): 103 [] c_TypeRel_Owiden(v_P,v_sko__local__XFAssRed1__Xhyps__2__1(A,v_P,B,v_e_Ha____,v_h_Ha____),B,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____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=42): 104 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,A,v_e_Ha____,v_sko__local__XFAssRed1__2__1(A,v_P,B,v_e_Ha____,v_h_Ha____))| -c_WellTypeRT_OWTrt(v_P,v_ha____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=15): 105 [] c_Map_Omap__le(A,B,C,D)| -c_Map_Omap__le(E,B,C,D)| -c_Map_Omap__le(A,E,C,D). % 5.78/5.92 ** KEPT (pick-wt=16): 106 [] c_WellType_OWT(A,B,C,D)| -c_Map_Omap__le(E,B,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)| -c_WellType_OWT(A,E,C,D). % 5.78/5.92 ** KEPT (pick-wt=13): 107 [] A=c_Type_Oty_OClass(B)| -c_WellType_OWT(C,D,c_Expr_Oexp_OCast(B,E,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=8): 108 [] c_Type_Oty_OClass(A)!=c_Type_Oty_OClass(B)|A=B. % 5.78/5.92 ** KEPT (pick-wt=13): 109 [] A=c_Type_Oty_OClass(B)| -c_WellTypeRT_OWTrt(C,D,E,c_Expr_Oexp_Onew(B,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=16): 110 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAss(F,G,H,I,E)|D=I. % 5.78/5.92 ** KEPT (pick-wt=16): 111 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAss(F,G,H,I,E)|C=H. % 5.78/5.92 ** KEPT (pick-wt=16): 112 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAss(F,G,H,I,E)|B=G. % 5.78/5.92 ** KEPT (pick-wt=16): 113 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAss(F,G,H,I,E)|A=F. % 5.78/5.92 ** KEPT (pick-wt=25): 114 [] c_TypeRel_Owiden(v_P,v_sko__unknown__thm__BwWC__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____,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_ONT). % 5.78/5.92 ** KEPT (pick-wt=11): 115 [] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OSe_q(F,G,E). % 5.78/5.92 ** KEPT (pick-wt=42): 116 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,A,v_e_Ha____,v_sko__local__XIH__1(A,v_P,B,v_e_Ha____,v_h_Ha____))| -c_WellTypeRT_OWTrt(v_P,v_ha____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=29): 117 [] A=c_Type_Oty_OVoid|c_WellTypeRT_OWTrt(B,C,D,E,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(F,D,G,B,E,C,H)))| -c_WellTypeRT_OWTrt(B,C,D,c_Expr_Oexp_OFAss(E,G,F,H,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=13): 118 [] A=B| -c_Map_Omap__le(B,A,C,D)| -c_Map_Omap__le(A,B,C,D). % 5.78/5.92 ** KEPT (pick-wt=15): 120 [copy,119,factor_simp] A=c_Type_Oty_OVoid| -c_WellTypeRT_OWTrt(B,C,D,c_Expr_Oexp_OFAss(E,F,G,H,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=22): 121 [] c_WellType_OWT(A,B,C,c_WellType_Osko__WellType__XWT__elim__cases__8__3(D,B,E,A,F,C))| -c_WellType_OWT(A,B,c_Expr_Oexp_OFAss(F,E,D,C,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=12): 122 [] A=c_Type_Oty_OClass(B)| -c_WellType_OWT(C,D,c_Expr_Oexp_Onew(B,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.92 ** KEPT (pick-wt=34): 123 [] c_TypeRel_Owiden(A,c_WellType_Osko__WellType__XWT__elim__cases__8__3(B,C,D,A,E,F),c_WellType_Osko__WellType__XWT__elim__cases__8__2(B,C,D,A,E,F),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,C,c_Expr_Oexp_OFAss(E,D,B,F,tc_List_Olist(tc_String_Ochar)),G). % 5.78/5.92 ** KEPT (pick-wt=22): 124 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OSe_q(D,E,tc_List_Olist(tc_String_Ochar)),F)| -c_Progress_OWTrt_H(A,B,C,E,F)| -c_Progress_OWTrt_H(A,B,C,D,G). % 5.78/5.92 ** KEPT (pick-wt=26): 125 [] 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__unknown__thm__BwWC__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). % 5.78/5.92 ** KEPT (pick-wt=47): 126 [] c_TypeRel_Owiden(v_P,v_sko__local__XFAssRed1__2__1(A,v_P,B,v_e_Ha____,v_h_Ha____),B,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____,A,v_ea____,B)| -c_TypeSafe__Mirabelle_Osconf(v_P,A,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)))). % 5.78/5.92 ** KEPT (pick-wt=46): 127 [] c_WellType_OWT(A,B,c_Expr_Oexp_OFAss(C,D,E,F,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)| -c_TypeRel_Owiden(A,G,H,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,B,F,G)| -c_TypeRel_Osees__field(A,I,D,H,E,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))| -c_WellType_OWT(A,B,C,c_Type_Oty_OClass(I)). % 5.78/5.92 ** KEPT (pick-wt=36): 128 [] c_WellTypeRT_OWTrt(A,B,C,D,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__4(C,A,B,D))|c_WellTypeRT_OWTrt(A,B,C,E,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(F,C,G,A,E,B,D)))| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OFAss(E,G,F,D,tc_List_Olist(tc_String_Ochar)),H). % 5.78/5.93 ** KEPT (pick-wt=19): 129 [] c_WellType_OWT(A,B,c_Expr_Oexp_OSe_q(C,D,tc_List_Olist(tc_String_Ochar)),E)| -c_WellType_OWT(A,B,D,E)| -c_WellType_OWT(A,B,C,F). % 5.78/5.93 ** KEPT (pick-wt=11): 131 [copy,130,flip.1] c_Type_Oty_OClass(c_TypeRel_Osko__TypeRel__XClass__widen__1__1(A))=A| -c_TypeRel_Owiden(B,c_Type_Oty_OClass(C),A,D). % 5.78/5.93 ** KEPT (pick-wt=14): 132 [] A=c_Type_Oty_OClass(B)| -c_WellTypeRT_OWTrt(C,D,E,c_Expr_Oexp_OCast(B,F,tc_List_Olist(tc_String_Ochar)),A). % 5.78/5.93 ** KEPT (pick-wt=22): 133 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OSe_q(D,E,tc_List_Olist(tc_String_Ochar)),F)| -c_WellTypeRT_OWTrt(A,B,C,E,F)| -c_WellTypeRT_OWTrt(A,B,C,D,G). % 5.78/5.93 ** KEPT (pick-wt=18): 134 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_Map_Omap__le(F,C,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)| -c_WellTypeRT_OWTrt(A,B,F,D,E). % 5.78/5.93 ** KEPT (pick-wt=12): 135 [] c_Progress_OWTrt_H(A,B,C,D,E)| -c_WellTypeRT_OWTrt(A,B,C,D,E). % 5.78/5.93 ** KEPT (pick-wt=12): 136 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_Progress_OWTrt_H(A,B,C,D,E). % 5.78/5.93 ** KEPT (pick-wt=11): 137 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_WellType_OWT(A,C,D,E). % 5.78/5.93 ** KEPT (pick-wt=15): 138 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_Objects_Ohext(F,B)| -c_WellTypeRT_OWTrt(A,F,C,D,E). % 5.78/5.93 ** KEPT (pick-wt=6): 139 [] -c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____). % 5.78/5.93 ** KEPT (pick-wt=7): 140 [] A=B| -c_fe_qual(A,B,C). % 5.78/5.93 Following clause subsumed by 11 during input processing: 0 [copy,5,flip.1] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OFAcc(C,D,E,B). % 5.78/5.93 Following clause subsumed by 9 during input processing: 0 [copy,7,flip.1] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OFAcc(C,D,E,B). % 5.78/5.93 Following clause subsumed by 13 during input processing: 0 [copy,8,flip.1] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OFAss(C,D,E,F,B). % 5.78/5.93 Following clause subsumed by 7 during input processing: 0 [copy,9,flip.1] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_Onew(E,D). % 5.78/5.93 Following clause subsumed by 5 during input processing: 0 [copy,11,flip.1] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_Othrow(E,D). % 5.78/5.93 Following clause subsumed by 29 during input processing: 0 [copy,12,flip.1] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_Othrow(D,C). % 5.78/5.93 Following clause subsumed by 8 during input processing: 0 [copy,13,flip.1] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_Othrow(F,E). % 5.78/5.93 Following clause subsumed by 38 during input processing: 0 [copy,14,flip.1] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_Onew(C,B). % 5.78/5.93 Following clause subsumed by 36 during input processing: 0 [copy,16,flip.1] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OCast(E,F,D). % 5.78/5.93 Following clause subsumed by 34 during input processing: 0 [copy,17,flip.1] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_Othrow(D,C). % 5.78/5.93 Following clause subsumed by 40 during input processing: 0 [copy,24,flip.1] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OFAcc(D,E,F,C). % 5.78/5.93 Following clause subsumed by 12 during input processing: 0 [copy,29,flip.1] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OCast(C,D,B). % 5.78/5.93 Following clause subsumed by 37 during input processing: 0 [copy,33,flip.1] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OFAss(E,F,G,H,D). % 5.78/5.93 Following clause subsumed by 17 during input processing: 0 [copy,34,flip.1] c_Expr_Oexp_Othrow(A,B)!=c_Expr_Oexp_OSe_q(C,D,B). % 5.78/5.93 Following clause subsumed by 16 during input processing: 0 [copy,36,flip.1] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OFAcc(D,E,F,C). % 5.78/5.93 Following clause subsumed by 33 during input processing: 0 [copy,37,flip.1] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OFAcc(F,G,H,E). % 5.78/5.93 Following clause subsumed by 14 during input processing: 0 [copy,38,flip.1] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_Othrow(C,B). % 5.78/5.93 Following clause subsumed by 24 during input processing: 0 [copy,40,flip.1] c_Expr_Oexp_OFAcc(A,B,C,D)!=c_Expr_Oexp_OSe_q(E,F,D). % 5.78/5.93 Following clause subsumed by 51 during input processing: 0 [copy,49,flip.1] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OSe_q(C,D,B). % 5.78/5.93 Following clause subsumed by 87 during input processing: 0 [copy,50,flip.1] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OCast(D,E,C). % 5.78/5.93 Following clause subsumed by 49 during input processing: 0 [copy,51,flip.1] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_Onew(D,C). % 5.78/5.93 Following clause subsumed by 75 during input processing: 0 [copy,57,flip.1] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OFAss(D,E,F,G,C). % 5.78/5.93 Following clause subsumed by 84 during input processing: 0 [copy,68,flip.1] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OCast(C,D,B). % 5.78/5.93 Following clause subsumed by 57 during input processing: 0 [copy,75,flip.1] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OCast(F,G,E). % 5.78/5.93 Following clause subsumed by 83 during input processing: 0 [copy,81,flip.1] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_Onew(F,E). % 5.78/5.93 Following clause subsumed by 81 during input processing: 0 [copy,83,flip.1] c_Expr_Oexp_Onew(A,B)!=c_Expr_Oexp_OFAss(C,D,E,F,B). % 5.78/5.93 Following clause subsumed by 68 during input processing: 0 [copy,84,flip.1] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_Onew(D,C). % 5.78/5.93 Following clause subsumed by 50 during input processing: 0 [copy,87,flip.1] c_Expr_Oexp_OCast(A,B,C)!=c_Expr_Oexp_OSe_q(D,E,C). % 5.78/5.93 Following clause subsumed by 115 during input processing: 0 [copy,91,flip.1] c_Expr_Oexp_OFAss(A,B,C,D,E)!=c_Expr_Oexp_OSe_q(F,G,E). % 5.78/5.93 Following clause subsumed by 91 during input processing: 0 [copy,115,flip.1] c_Expr_Oexp_OSe_q(A,B,C)!=c_Expr_Oexp_OFAss(D,E,F,G,C). % 5.78/5.93 120 back subsumes 117. % 5.78/5.93 120 back subsumes 88. % 5.78/5.93 120 back subsumes 77. % 5.78/5.93 120 back subsumes 56. % 5.78/5.93 120 back subsumes 55. % 5.78/5.93 120 back subsumes 18. % 5.78/5.93 % 5.78/5.93 ------------> process sos: % 5.78/5.93 ** KEPT (pick-wt=3): 153 [] A=A. % 5.78/5.93 ** KEPT (pick-wt=2): 154 [] c_Type_Ois__refT(c_Type_Oty_ONT). % 5.78/5.93 ** KEPT (pick-wt=3): 155 [] c_Type_Ois__refT(c_Type_Oty_OClass(A)). % 5.78/5.93 ** KEPT (pick-wt=25): 156 [] 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)))). % 5.78/5.93 ** KEPT (pick-wt=3): 157 [] c_Objects_Ohext(A,A). % 5.78/5.93 ** KEPT (pick-wt=6): 158 [] c_TypeRel_Owiden(A,c_Type_Oty_ONT,c_Type_Oty_OClass(B),C). % 5.78/5.93 ** KEPT (pick-wt=5): 159 [] c_TypeRel_Owiden(A,B,B,C). % 5.78/5.93 ** KEPT (pick-wt=5): 160 [] c_COMBI(A,B)=A. % 5.78/5.93 ---> New Demodulator: 161 [new_demod,160] c_COMBI(A,B)=A. % 5.78/5.93 ** KEPT (pick-wt=5): 162 [] c_Map_Omap__le(A,A,B,C). % 5.78/5.93 ** KEPT (pick-wt=3): 163 [] v_T____=c_Type_Oty_OVoid. % 5.78/5.93 ---> New Demodulator: 164 [new_demod,163] v_T____=c_Type_Oty_OVoid. % 5.78/5.93 ** KEPT (pick-wt=12): 165 [] c_TypeRel_Owiden(v_P,v_U____,c_Type_Oty_OClass(v_C____),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.93 ** KEPT (pick-wt=13): 166 [] 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)))). % 5.78/5.93 ** KEPT (pick-wt=6): 167 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____). % 5.78/5.93 ** KEPT (pick-wt=6): 168 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,v_U____). % 5.78/5.93 ** KEPT (pick-wt=7): 169 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(v_C____)). % 5.78/5.93 ** KEPT (pick-wt=11): 170 [] c_TypeRel_Owiden(v_P,v_T_092_060_094isub_0622____,v_TF____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 5.78/5.93 ** KEPT (pick-wt=12): 172 [copy,171,demod,164] 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). % 5.78/5.93 Following clause subsumed by 153 during input processing: 0 [demod,161] v_P=v_P. % 5.78/5.93 ** KEPT (pick-wt=4): 173 [] c_fe_qual(A,A,B). % 5.78/5.93 Following clause subsumed by 153 during input processing: 0 [copy,153,flip.1] A=A. % 5.78/5.93 153 back subsumes 148. % 5.78/5.93 153 back subsumes 145. % 5.78/5.93 153 back subsumes 144. % 5.78/5.93 153 back subsumes 143. % 5.78/5.93 >>>> Starting back demodulation with 161. % 5.78/5.93 >>>> Starting back demodulation with 164. % 5.78/5.94 >> back demodulating 125 with 164. % 5.78/5.94 >> back demodulating 114 with 164. % 5.78/5.94 % 5.78/5.94 ======= end of input processing ======= % 5.78/5.94 % 5.78/5.94 =========== start of search =========== % 5.78/5.94 % 5.78/5.94 Search stopped in tp_alloc by max_mem option. % 5.78/5.94 % 5.78/5.94 Search stopped in tp_alloc by max_mem option. % 5.78/5.94 % 5.78/5.94 ============ end of search ============ % 5.78/5.94 % 5.78/5.94 -------------- statistics ------------- % 5.78/5.94 clauses given 6 % 5.78/5.94 clauses generated 907 % 5.78/5.94 clauses kept 1004 % 5.78/5.94 clauses forward subsumed 86 % 5.78/5.94 clauses back subsumed 13 % 5.78/5.94 Kbytes malloced 11718 % 5.78/5.94 % 5.78/5.94 ----------- times (seconds) ----------- % 5.78/5.94 user CPU time 0.03 (0 hr, 0 min, 0 sec) % 5.78/5.94 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 5.78/5.94 wall-clock time 6 (0 hr, 0 min, 6 sec) % 5.78/5.94 % 5.78/5.94 Process 27190 finished Wed Jul 27 06:17:56 2022 % 5.78/5.94 Otter interrupted % 5.78/5.94 PROOF NOT FOUND %------------------------------------------------------------------------------