%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV978-1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n014.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:53 EDT 2022 % Result : Unknown 42.88s 42.95s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV978-1 : TPTP v8.1.0. Released v4.1.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 05:49:09 EDT 2022 % 0.13/0.34 % CPUTime : % 42.64/42.76 ----- Otter 3.3f, August 2004 ----- % 42.64/42.76 The process was started by sandbox on n014.cluster.edu, % 42.64/42.76 Wed Jul 27 05:49:09 2022 % 42.64/42.76 The command was "./otter". The process ID is 32108. % 42.64/42.76 % 42.64/42.76 set(prolog_style_variables). % 42.64/42.76 set(auto). % 42.64/42.76 dependent: set(auto1). % 42.64/42.76 dependent: set(process_input). % 42.64/42.76 dependent: clear(print_kept). % 42.64/42.76 dependent: clear(print_new_demod). % 42.64/42.76 dependent: clear(print_back_demod). % 42.64/42.76 dependent: clear(print_back_sub). % 42.64/42.76 dependent: set(control_memory). % 42.64/42.76 dependent: assign(max_mem, 12000). % 42.64/42.76 dependent: assign(pick_given_ratio, 4). % 42.64/42.76 dependent: assign(stats_level, 1). % 42.64/42.76 dependent: assign(max_seconds, 10800). % 42.64/42.76 clear(print_given). % 42.64/42.76 % 42.64/42.76 list(usable). % 42.64/42.76 0 [] A=A. % 42.64/42.76 0 [] c_Map_Odom(c_Fun_Ofun__upd(V_f,V_x,c_Option_Ooption_ONone(T_b),T_a,tc_Option_Ooption(T_b)),T_a,T_b)=c_HOL_Ominus__class_Ominus(c_Map_Odom(V_f,T_a,T_b),c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(V_m,V_x,V_y,T_a,tc_Option_Ooption(T_b)),V_D,T_a,T_b)=c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,c_HOL_Ominus__class_Ominus(V_D,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),V_x,V_y,T_a,tc_Option_Ooption(T_b))| -hBOOL(c_in(V_x,V_D,T_a)). % 42.64/42.76 0 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,V_D,T_a,T_b),V_x,V_y,T_a,tc_Option_Ooption(T_b))=c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,c_HOL_Ominus__class_Ominus(V_D,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),V_x,V_y,T_a,tc_Option_Ooption(T_b))| -hBOOL(c_in(V_x,V_D,T_a)). % 42.64/42.76 0 [] c_Set_Oimage(c_Fun_Ofun__upd(V_f,V_x,V_y,T_b,T_a),V_A,T_b,T_a)=c_Set_Oinsert(V_y,c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b),tc_fun(T_b,tc_bool)),T_b,T_a),T_a)| -hBOOL(c_in(V_x,V_A,T_b)). % 42.64/42.76 0 [] c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)|hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] -hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b))| -c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b). % 42.64/42.76 0 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,V_D,T_a,T_b),V_x,V_y,T_a,tc_Option_Ooption(T_b))=c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,c_HOL_Ominus__class_Ominus(V_D,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),V_x,V_y,T_a,tc_Option_Ooption(T_b)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))| -hBOOL(c_in(V_x,V_B,T_a)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool))=c_Set_Oinsert(V_x,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)|hBOOL(c_in(V_x,V_B,T_a)). % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)=V_A| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.76 0 [] c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -class_Lattices_Oboolean__algebra(T_a)|c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(T_a),T_a)=c_Orderings_Otop__class_Otop(T_a). % 42.64/42.76 0 [] -class_HOL_Ouminus(T_b)|hAPP(c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(t_a,T_b)),v_x)=c_HOL_Ouminus__class_Ouminus(hAPP(V_A,v_x),T_b). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))!=c_HOL_Ouminus__class_Ouminus(V_B,tc_fun(T_a,tc_bool))|V_A=V_B. % 42.64/42.76 0 [] -class_OrderedGroup_Ogroup__add(T_a)|c_HOL_Ouminus__class_Ouminus(V_a,T_a)!=c_HOL_Ouminus__class_Ouminus(V_b,T_a)|V_a=V_b. % 42.64/42.76 0 [] -class_Lattices_Oboolean__algebra(T_a)|c_HOL_Ouminus__class_Ouminus(V_x,T_a)!=c_HOL_Ouminus__class_Ouminus(V_y,T_a)|V_x=V_y. % 42.64/42.76 0 [] c_HOL_Ouminus__class_Ouminus(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -class_Lattices_Oboolean__algebra(T_a)|c_HOL_Ouminus__class_Ouminus(c_Orderings_Otop__class_Otop(T_a),T_a)=c_Orderings_Obot__class_Obot(T_a). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(V_A,V_A,tc_fun(T_a,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_A. % 42.64/42.76 0 [] -hBOOL(c_in(V_c,V_B,T_a))| -hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(V_c,V_A,T_a))| -hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_Fun_Oinj__on(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))|hBOOL(c_in(V_c,V_A,T_a)). % 42.64/42.76 0 [] -hBOOL(c_in(V_c,V_A,T_a))| -hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] hAPP(V_f,V_x)!=c_Option_Ooption_ONone(T_a)|c_HOL_Ominus__class_Ominus(c_Map_Odom(V_f,T_b,T_a),c_Set_Oinsert(V_x,V_A,T_b),tc_fun(T_b,tc_bool))=c_HOL_Ominus__class_Ominus(c_Map_Odom(V_f,T_b,T_a),V_A,tc_fun(T_b,tc_bool)). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))=c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -class_OrderedGroup_Oab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a)!=c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)|V_xa=V_y. % 42.64/42.76 0 [] -class_OrderedGroup_Oab__group__add(T_a)|c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)!=c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)|V_x_H=V_y_H. % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)=c_Set_Oinsert(V_a,V_A,T_a). % 42.64/42.76 0 [] hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))|hBOOL(c_in(V_c,V_B,T_a))| -hBOOL(c_in(V_c,V_A,T_a)). % 42.64/42.76 0 [] hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))|hBOOL(c_in(V_c,V_B,T_a))| -hBOOL(c_in(V_c,V_A,T_a)). % 42.64/42.76 0 [] c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b)=c_HOL_Ominus__class_Ominus(c_Set_Oimage(V_f,V_A,T_a,T_b),c_Set_Oimage(V_f,V_B,T_a,T_b),tc_fun(T_b,tc_bool))| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] -class_HOL_Ominus(T_b)|hAPP(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(t_a,T_b)),v_x)=c_HOL_Ominus__class_Ominus(hAPP(V_A,v_x),hAPP(V_B,v_x),T_b). % 42.64/42.76 0 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_a),c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool))=V_A|hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.76 0 [] c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))=V_A. % 42.64/42.76 0 [] -class_OrderedGroup_Ogroup__add(T_a)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a)=V_a. % 42.64/42.76 0 [] -class_Lattices_Oboolean__algebra(T_a)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_x,T_a),T_a)=V_x. % 42.64/42.76 0 [] -class_OrderedGroup_Ogroup__add(T_a)|V_b=c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a). % 42.64/42.76 0 [] -class_OrderedGroup_Ogroup__add(T_a)|V_a=c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a). % 42.64/42.76 0 [] -class_OrderedGroup_Ogroup__add(T_a)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a)=V_b. % 42.64/42.76 0 [] -class_OrderedGroup_Oab__group__add(T_a)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a)=c_HOL_Ominus__class_Ominus(V_b,V_a,T_a). % 42.64/42.76 0 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(V_m,V_x,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b)),c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b)=c_Map_Orestrict__map(V_m,c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,V_D,T_a,T_b),V_x,c_Option_Ooption_ONone(T_b),T_a,tc_Option_Ooption(T_b))=c_Map_Orestrict__map(V_m,c_HOL_Ominus__class_Ominus(V_D,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b)| -hBOOL(c_in(V_x,V_D,T_a)). % 42.64/42.76 0 [] c_Map_Odom(V_f,T_a,T_b)!=c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_f=c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),V_x,hAPP(c_Option_Ooption_OSome(T_b),c_Map_Osko__Map__Xdom__e_q__singleton__conv__1__1(V_f,V_x,T_a,T_b)),T_a,tc_Option_Ooption(T_b)). % 42.64/42.76 0 [] c_Fun_Ooverride__on(V_f,V_g,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a,T_b)=V_f. % 42.64/42.76 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))=c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a). % 42.64/42.76 0 [] c_Set_Oimage(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_f,T_a,T_b),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_a)=V_A| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] c_Set_Oimage(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_f,T_a,T_b),c_Set_Oimage(V_f,V_X,T_a,T_b),T_b,T_a)=V_X| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))| -hBOOL(hAPP(V_P,hAPP(V_f2,v_sko__Option__Xoption__Xsplit__1(V_P,V_f2,V_x))))| -hBOOL(hAPP(V_P,V_f1)). % 42.64/42.76 0 [] hAPP(c_Fun_Othe__inv__into(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_f,T_a,T_b),hAPP(V_f,V_x))=V_x| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b))=hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))|hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b)))=hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))). % 42.64/42.76 0 [] c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b))=hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))|hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b)))=hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))). % 42.64/42.76 0 [] hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b))!=hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))|hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b)))!=hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b)))|c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a). % 42.64/42.76 0 [] hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b))!=hAPP(V_g,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b))|hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b)))!=hAPP(V_g,hAPP(V_f,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b)))|c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a). % 42.64/42.76 0 [] c_Option_Oset(c_Option_Ooption_ONone(T_a),T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -hBOOL(hAPP(V_P,V_x))| -hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)!=c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_a=V_b. % 42.64/42.76 0 [] c_Conform_Oconf(V_P,V_h,V_v,V_T_H,T_a)| -c_TypeRel_Owiden(V_P,V_T,V_T_H,T_a)| -c_Conform_Oconf(V_P,V_h,V_v,V_T,T_a). % 42.64/42.76 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). % 42.64/42.76 0 [] c_TypeRel_Owiden(V_P,V_T,V_T,T_a). % 42.64/42.76 0 [] c_Fun_Oinj__on(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_Set_Oinsert(V_xa,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)=c_Set_Oinsert(V_x,c_Set_Oinsert(V_xa,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a). % 42.64/42.76 0 [] c_Map_Odom(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),T_a,T_b)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -class_Orderings_Obot(T_b)|hAPP(c_Orderings_Obot__class_Obot(tc_fun(t_a,T_b)),v_x)=c_Orderings_Obot__class_Obot(T_b). % 42.64/42.76 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))!=c_Set_Oimage(V_f,V_A,T_b,T_a)|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 42.64/42.76 0 [] c_Set_Oinsert(V_a,V_A,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] hBOOL(c_in(V_x,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] hAPP(V_f,V_x)!=hAPP(V_f,V_y)| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b)|V_x=V_y. % 42.64/42.76 0 [] hAPP(c_Map_Orestrict__map(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),t_a),V_D,t_a,T_b),v_x)=c_Option_Ooption_ONone(T_b). % 42.64/42.76 0 [] hAPP(V_f2,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_xa,V_f2,V_g2,T_aa,T_a))!=hAPP(V_g2,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_xa,V_f2,V_g2,T_aa,T_a))|c_Option_Ooption_Ooption__case(V_x,V_f2,V_xa,T_a,T_aa)=c_Option_Ooption_Ooption__case(V_x,V_g2,V_xa,T_a,T_aa). % 42.64/42.76 0 [] -hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)). % 42.64/42.76 0 [] c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))| -hBOOL(hAPP(V_P,hAPP(V_f2,v_sko__Option__Xoption__Xsplit__asm__1(V_P,V_f2,V_x))))| -hBOOL(hAPP(V_P,V_f1)). % 42.64/42.76 0 [] hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_x)). % 42.64/42.76 0 [] -class_Orderings_Otop(T_b)|hAPP(c_Orderings_Otop__class_Otop(tc_fun(t_a,T_b)),v_x)=c_Orderings_Otop__class_Otop(T_b). % 42.64/42.76 0 [] c_Option_Oset(V_xo,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_xo=c_Option_Ooption_ONone(T_a). % 42.64/42.76 0 [] hAPP(c_Map_Orestrict__map(V_m,V_A,T_a,T_b),V_x)=hAPP(V_m,V_x)| -hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_a=V_d|V_a=V_c. % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_b=V_c|V_a=V_c. % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_a=V_d|V_b=V_d. % 42.64/42.76 0 [] c_Set_Oinsert(V_a,c_Set_Oinsert(V_b,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)!=c_Set_Oinsert(V_c,c_Set_Oinsert(V_d,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)|V_b=V_c|V_b=V_d. % 42.64/42.76 0 [] hAPP(c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),v_x)=c_in(v_x,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a). % 42.64/42.76 0 [] c_Map_Odom(V_f,T_a,T_b)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_f=c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a). % 42.64/42.76 0 [] c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))!=c_Set_Oinsert(V_a,V_A,T_a). % 42.64/42.76 0 [] c_Map_Oran(c_COMBK(c_Option_Ooption_ONone(T_a),tc_Option_Ooption(T_a),T_b),T_b,T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] -hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] -hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,V_x))| -hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] -hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)). % 42.64/42.76 0 [] hAPP(c_Fun_Ocomp(V_f,V_g,T_c,T_b,t_a),v_x)=hAPP(V_f,hAPP(V_g,v_x)). % 42.64/42.76 0 [] c_Option_Oset(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)=c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 42.64/42.76 0 [] c_Map_Odom(c_COMBK(hAPP(c_Option_Ooption_OSome(T_b),V_y),tc_Option_Ooption(T_b),T_a),T_a,T_b)=c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_f,T_a,T_b),hAPP(V_f,V_x))=V_x| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_aa,tc_bool)),T_aa,T_a)|hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(T_aa,tc_bool)),V_f,T_aa,T_a),hAPP(V_f,V_x))=V_x. % 42.64/42.76 0 [] c_Set_Oimage(V_f,V_A,T_b,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 42.64/42.76 0 [] hAPP(c_Map_Orestrict__map(V_m,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,T_b),v_x)=c_Option_Ooption_ONone(T_b). % 42.64/42.76 0 [] c_Fun_Ocomp(c_Fun_Ocomp(V_g,c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),V_f,T_a,T_b),T_a,T_c,T_b),V_f,T_b,T_c,T_a)=V_g| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.76 0 [] hBOOL(c_in(V_y,c_List_Oset(V_xs,T_a),T_a))|V_y=V_x| -hBOOL(c_in(V_y,c_List_Oset(c_List_Olist_OCons(V_x,V_xs,T_a),T_a),T_a)). % 42.64/42.76 0 [] c_Set_Oinsert(V_x,V_xa,T_a)!=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))|hBOOL(c_in(V_x,V_xa,T_a)). % 42.64/42.76 0 [] V_b=V_a| -hBOOL(c_in(V_b,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(V_x,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a)). % 42.64/42.76 0 [] hAPP(V_m,V_a)!=hAPP(c_Option_Ooption_OSome(T_a),V_b)|hBOOL(c_in(V_b,c_Map_Oran(V_m,T_b,T_a),T_a)). % 42.64/42.76 0 [] V_xo=hAPP(c_Option_Ooption_OSome(T_a),V_x)| -hBOOL(c_in(V_x,c_Option_Oset(V_xo,T_a),T_a)). % 42.64/42.76 0 [] hAPP(V_m,V_a)!=hAPP(c_Option_Ooption_OSome(T_a),V_b)|hBOOL(c_in(V_a,c_Map_Odom(V_m,T_b,T_a),T_b)). % 42.64/42.76 0 [] hBOOL(c_in(V_x,c_Option_Oset(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_bool)),T_b,T_a),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_b,T_a),V_x),V_A,T_b))| -hBOOL(c_in(V_x,c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)). % 42.64/42.76 0 [] hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_a,T_b),V_x)!=hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_a,T_b),V_y)|V_x=V_y| -hBOOL(c_in(V_y,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -hBOOL(c_in(V_x,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)). % 42.64/42.76 0 [] hAPP(V_f,hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_b,T_a),V_y))=V_y| -hBOOL(c_in(V_y,c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)). % 42.64/42.76 0 [] c_List_Oset(c_List_Olist_OCons(V_x,V_xs,T_a),T_a)=c_Set_Oinsert(V_x,c_List_Oset(V_xs,T_a),T_a). % 42.64/42.76 0 [] hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_a,T_b),hAPP(V_f,V_x))=V_x| -hBOOL(c_in(V_x,V_A,T_a))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] -hBOOL(c_in(V_x,V_A,T_aa))| -c_Fun_Oinj__on(V_f,V_A,T_aa,T_a)|hAPP(c_Hilbert__Choice_Oinv__into(V_A,V_f,T_aa,T_a),hAPP(V_f,V_x))=V_x. % 42.64/42.76 0 [] hAPP(c_Fun_Othe__inv__into(V_A,V_f,T_a,T_b),hAPP(V_f,V_x))=V_x| -hBOOL(c_in(V_x,V_A,T_a))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] -c_Fun_Oinj__on(V_f,V_A,T_aa,T_a)|hAPP(c_Fun_Othe__inv__into(V_A,V_f,T_aa,T_a),hAPP(V_f,V_x))=V_x| -hBOOL(c_in(V_x,V_A,T_aa)). % 42.64/42.76 0 [] hAPP(c_Map_Orestrict__map(V_m,V_A,T_a,T_b),V_x)=c_Option_Ooption_ONone(T_b)|hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.76 0 [] hAPP(V_m,V_a)!=c_Option_Ooption_ONone(T_b)| -hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(V_a,c_Map_Odom(V_m,T_a,T_b),T_a))|hAPP(V_m,V_a)=c_Option_Ooption_ONone(T_b). % 42.64/42.76 0 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(V_m,V_x,V_y,T_a,tc_Option_Ooption(T_b)),V_D,T_a,T_b)=c_Map_Orestrict__map(V_m,V_D,T_a,T_b)|hBOOL(c_in(V_x,V_D,T_a)). % 42.64/42.76 0 [] hAPP(V_f,V_x)!=hAPP(c_Option_Ooption_OSome(T_a),V_y)|c_Set_Oinsert(V_x,c_Map_Odom(V_f,T_b,T_a),T_b)=c_Map_Odom(V_f,T_b,T_a). % 42.64/42.76 0 [] c_Fun_Oinj__on(c_Fun_Othe__inv__into(V_A,V_f,T_a,T_b),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_a)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] c_Set_Oimage(V_f,V_A,T_a,T_b)!=c_Set_Oimage(V_f,V_B,T_a,T_b)| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b)|V_A=V_B. % 42.64/42.76 0 [] c_Set_Oimage(c_Fun_Othe__inv__into(V_A,V_f,T_a,T_b),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_a)=V_A| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.76 0 [] c_Set_Oimage(c_COMBK(V_c,T_a,T_b),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a)=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)). % 42.64/42.76 0 [] c_Map_Orestrict__map(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)=c_Fun_Ofun__upd(c_Map_Orestrict__map(V_f,V_A,T_a,T_b),V_a,hAPP(V_f,V_a),T_a,tc_Option_Ooption(T_b)). % 42.64/42.76 0 [] hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m)=hAPP(V_l2,V_m)| -hBOOL(c_in(V_m,c_Map_Odom(V_l2,T_a,T_b),T_a)). % 42.64/42.76 0 [] hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m)=hAPP(V_l2,V_m)|hBOOL(c_in(V_m,c_Map_Odom(V_l1,T_a,T_b),T_a)). % 42.64/42.76 0 [] hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m)=hAPP(V_l1,V_m)|hBOOL(c_in(V_m,c_Map_Odom(V_l2,T_a,T_b),T_a)). % 42.64/42.76 0 [] hAPP(c_Fun_Ocomp(c_COMBK(V_c,T_b,T_c),V_f,T_c,T_b,t_a),v_x)=V_c. % 42.64/42.76 0 [] hAPP(c_Map_Omap__upds(V_f,V_xs,V_ys,T_a,T_b),V_x)=hAPP(V_f,V_x)|hBOOL(c_in(V_x,c_List_Oset(V_xs,T_a),T_a)). % 42.64/42.76 0 [] hAPP(V_m_092_060_094isub_0621,V_x)=hAPP(V_m_092_060_094isub_0622,V_x)| -hBOOL(c_in(V_x,c_Map_Odom(V_m_092_060_094isub_0621,T_a,T_b),T_a))| -c_Map_Omap__le(V_m_092_060_094isub_0621,V_m_092_060_094isub_0622,T_a,T_b). % 42.64/42.76 0 [] c_Option_Ooption_Ooption__case(V_x,V_f2,V_xa,T_a,T_aa)=c_Option_Ooption_Ooption__case(V_x,V_g2,V_xa,T_a,T_aa)|V_xa=hAPP(c_Option_Ooption_OSome(T_aa),c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_xa,V_f2,V_g2,T_aa,T_a)). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))|V_x=hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__asm__1(V_P,V_f2,V_x))| -hBOOL(hAPP(V_P,V_f1)). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))|V_x=hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__1(V_P,V_f2,V_x))| -hBOOL(hAPP(V_P,V_f1)). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))| -hBOOL(hAPP(V_P,hAPP(V_f2,v_sko__Option__Xoption__Xsplit__1(V_P,V_f2,V_x))))|V_x=c_Option_Ooption_ONone(t_b). % 42.64/42.76 0 [] hAPP(V_f2,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_x,V_f2,V_g2,T_a,T_b))!=hAPP(V_g2,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_x,V_f2,V_g2,T_a,T_b))|V_x=c_Option_Ooption_ONone(T_a)|c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,T_b,T_a)=c_Option_Ooption_Ooption__case(V_g1,V_g2,V_x,T_b,T_a). % 42.64/42.76 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))| -hBOOL(hAPP(V_P,hAPP(V_f2,v_sko__Option__Xoption__Xsplit__asm__1(V_P,V_f2,V_x))))|V_x=c_Option_Ooption_ONone(t_b). % 42.64/42.76 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_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T). % 42.64/42.76 0 [] c_Decl_Ois__class(V_P,V_C,T_a)| -c_Decl_Ois__type(V_P,c_Type_Oty_OClass(V_C),T_a). % 42.64/42.76 0 [] c_Decl_Ois__type(V_P,c_Type_Oty_OClass(V_C),T_a)| -c_Decl_Ois__class(V_P,V_C,T_a). % 42.64/42.76 0 [] c_Map_Omap__comp(V_m1,V_m2,V_k,T_b,T_a,T_c)!=c_Option_Ooption_ONone(T_a)|hAPP(V_m1,c_Map_Osko__Map__Xmap__comp__None__iff__1__1(V_k,V_m1,V_m2,T_c,T_b,T_a))=c_Option_Ooption_ONone(T_a)|hAPP(V_m2,V_k)=c_Option_Ooption_ONone(T_b). % 42.64/42.76 0 [] -hBOOL(c_in(V_x,V_A,T_aa))|hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)). % 42.64/42.76 0 [] -hBOOL(c_in(V_x,V_A,T_b))|hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)). % 42.64/42.76 0 [] hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a))| -hBOOL(c_in(V_x,V_A,T_b)). % 42.64/42.76 0 [] hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.76 0 [] c_Fun_Ocomp(V_f,c_Fun_Oswap(V_a,V_b,V_g,T_a,T_c),T_c,T_b,T_a)=c_Fun_Oswap(V_a,V_b,c_Fun_Ocomp(V_f,V_g,T_c,T_b,T_a),T_a,T_b). % 42.64/42.76 0 [] c_Map_Omap__le(c_Map_Omap__add(V_f,V_g,T_a,T_b),V_h,T_a,T_b)| -c_Map_Omap__le(V_f,c_Map_Omap__add(V_f,V_g,T_a,T_b),T_a,T_b)| -c_Map_Omap__le(V_g,V_h,T_a,T_b)| -c_Map_Omap__le(V_f,V_h,T_a,T_b). % 42.64/42.76 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T_092_060_094isub_0622)| -c_TypeRel_Owiden(V_P,V_T_092_060_094isub_0621,V_T_092_060_094isub_0622,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,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(V_C)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),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). % 42.64/42.76 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T)| -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,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(V_C)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e_092_060_094isub_0622,V_T)| -c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_T). % 42.64/42.76 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T_092_060_094isub_0622)| -c_TypeRel_Owiden(V_P,V_T_092_060_094isub_0621,V_T_092_060_094isub_0622,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,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(V_C)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),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). % 42.64/42.76 0 [] c_TypeRel_Owiden(v_P,v_Te_H____,v_Te____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.64/42.76 0 [] hAPP(c_Fun_Ocomp(c_Option_Omap(V_f,T_c,T_b),c_COMBK(c_Option_Ooption_ONone(T_c),tc_Option_Ooption(T_c),t_a),tc_Option_Ooption(T_c),tc_Option_Ooption(T_b),t_a),v_x)=c_Option_Ooption_ONone(T_b). % 42.64/42.76 0 [] c_Map_Omap__upds(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_b),V_b),T_a,tc_Option_Ooption(T_b)),V_as,V_bs,T_a,T_b)=c_Fun_Ofun__upd(c_Map_Omap__upds(V_m,V_as,V_bs,T_a,T_b),V_a,hAPP(c_Option_Ooption_OSome(T_b),V_b),T_a,tc_Option_Ooption(T_b))|hBOOL(c_in(V_a,c_List_Oset(V_as,T_a),T_a)). % 42.64/42.76 0 [] c_Map_Omap__add(c_Fun_Ofun__upd(V_e1,V_m,hAPP(c_Option_Ooption_OSome(T_b),V_u1),T_a,tc_Option_Ooption(T_b)),V_e2,T_a,T_b)=c_Fun_Ofun__upd(c_Map_Omap__add(V_e1,V_e2,T_a,T_b),V_m,hAPP(c_Option_Ooption_OSome(T_b),V_u1),T_a,tc_Option_Ooption(T_b))|hBOOL(c_in(V_m,c_Map_Odom(V_e2,T_a,T_b),T_a)). % 42.64/42.76 0 [] hAPP(V_m,V_a)!=c_Option_Ooption_ONone(T_a)|c_Map_Oran(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_a),V_b),T_b,tc_Option_Ooption(T_a)),T_b,T_a)=c_Set_Oinsert(V_b,c_Map_Oran(V_m,T_b,T_a),T_a). % 42.64/42.76 0 [] hBOOL(c_in(c_ATP__Linkup_Osko__Option__Xospec__1__1(hAPP(c_Option_Ooption_OSome(T_a),V_x),V_P,T_a),c_Option_Oset(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a),T_a))|hBOOL(hAPP(V_P,V_x)). % 42.64/42.77 0 [] hAPP(c_Fun_Othe__inv__into(V_A,c_Fun_Ocomp(V_f,V_g,T_a,T_b,T_c),T_c,T_b),V_x)=hAPP(c_Fun_Ocomp(c_Fun_Othe__inv__into(V_A,V_g,T_c,T_a),c_Fun_Othe__inv__into(c_Set_Oimage(V_g,V_A,T_c,T_a),V_f,T_a,T_b),T_a,T_c,T_b),V_x)| -hBOOL(c_in(V_x,c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_a),T_a,T_b),T_b))| -c_Fun_Oinj__on(V_g,V_A,T_c,T_a)| -c_Fun_Oinj__on(V_f,c_Set_Oimage(V_g,V_A,T_c,T_a),T_a,T_b). % 42.64/42.77 0 [] hAPP(c_Hilbert__Choice_Oinv__into(V_A,c_Fun_Ocomp(V_f,V_g,T_a,T_b,T_c),T_c,T_b),V_x)=hAPP(c_Fun_Ocomp(c_Hilbert__Choice_Oinv__into(V_A,V_g,T_c,T_a),c_Hilbert__Choice_Oinv__into(c_Set_Oimage(V_g,V_A,T_c,T_a),V_f,T_a,T_b),T_a,T_c,T_b),V_x)| -hBOOL(c_in(V_x,c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_a),T_a,T_b),T_b))| -c_Fun_Oinj__on(V_g,V_A,T_c,T_a)| -c_Fun_Oinj__on(V_f,c_Set_Oimage(V_g,V_A,T_c,T_a),T_a,T_b). % 42.64/42.77 0 [] c_Set_Oimage(c_COMBK(V_c,T_b,T_a),V_A,T_a,T_b)=c_Set_Oinsert(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b)| -hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.77 0 [] c_Map_Omap__comp(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_c),V_m,v_x,T_c,T_b,t_a)=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] c_Map_Omap__comp(V_m,c_COMBK(c_Option_Ooption_ONone(T_c),tc_Option_Ooption(T_c),t_a),v_x,T_c,T_b,t_a)=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] c_Map_Omap__comp(V_m1,V_m2,V_k,T_b,T_a,T_c)!=c_Option_Ooption_ONone(T_a)|hAPP(V_m2,V_k)=hAPP(c_Option_Ooption_OSome(T_b),c_Map_Osko__Map__Xmap__comp__None__iff__1__1(V_k,V_m1,V_m2,T_c,T_b,T_a))|hAPP(V_m2,V_k)=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),t_a),V_x,c_Option_Ooption_ONone(T_b),t_a,tc_Option_Ooption(T_b)),v_xa)=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))|V_x=hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__1(V_P,V_f2,V_x))|V_x=c_Option_Ooption_ONone(t_b). % 42.64/42.77 0 [] c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,T_b,T_a)=c_Option_Ooption_Ooption__case(V_g1,V_g2,V_x,T_b,T_a)|V_x=hAPP(c_Option_Ooption_OSome(T_a),c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(V_x,V_f2,V_g2,T_a,T_b))|V_x=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,V_x,t_a,t_b)))|V_x=hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__asm__1(V_P,V_f2,V_x))|V_x=c_Option_Ooption_ONone(t_b). % 42.64/42.77 0 [] c_Map_Odom(c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,tc_Option_Ooption(T_b)),T_a,T_b)=c_Set_Oinsert(V_x,c_Map_Odom(V_f,T_a,T_b),T_a)|V_y=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] -class_OrderedGroup_Ocomm__monoid__mult(T_c)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b)|c_Finite__Set_Osetprod(V_h,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_c)=c_Finite__Set_Osetprod(c_Fun_Ocomp(V_h,V_f,T_b,T_c,T_a),V_A,T_a,T_c). % 42.64/42.77 0 [] -class_OrderedGroup_Ocomm__monoid__mult(T_c)|c_Finite__Set_Osetprod(V_h,c_Set_Oimage(V_f,V_B,T_a,T_b),T_b,T_c)=c_Finite__Set_Osetprod(c_Fun_Ocomp(V_h,V_f,T_b,T_c,T_a),V_B,T_a,T_c)| -c_Fun_Oinj__on(V_f,V_B,T_a,T_b). % 42.64/42.77 0 [] -class_OrderedGroup_Ocomm__monoid__add(T_c)|c_Finite__Set_Osetsum(V_h,c_Set_Oimage(V_f,V_B,T_a,T_b),T_b,T_c)=c_Finite__Set_Osetsum(c_Fun_Ocomp(V_h,V_f,T_b,T_c,T_a),V_B,T_a,T_c)| -c_Fun_Oinj__on(V_f,V_B,T_a,T_b). % 42.64/42.77 0 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(V_m,V_D,T_a,T_b),V_x,c_Option_Ooption_ONone(T_b),T_a,tc_Option_Ooption(T_b))=c_Map_Orestrict__map(V_m,V_D,T_a,T_b)|hBOOL(c_in(V_x,V_D,T_a)). % 42.64/42.77 0 [] c_Set_Oimage(c_COMBK(V_c,T_a,T_b),V_A,T_b,T_a)=c_Set_Oinsert(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)|V_A=c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b),V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(V_A,V_f,V_g,T_a,T_b),V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b),V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_g,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_a),T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_a)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(V_A,V_f,V_g,T_a,T_b),V_A,T_a)). % 42.64/42.77 0 [] hAPP(V_f,hAPP(c_Fun_Othe__inv__into(V_A,V_f,T_a,T_b),V_y))=V_y| -hBOOL(c_in(V_y,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.77 0 [] hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -hBOOL(c_in(V_a,V_A,T_a))| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.77 0 [] hBOOL(c_in(V_a,V_A,T_a))| -hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -c_Fun_Oinj__on(V_f,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)),T_a,T_b). % 42.64/42.77 0 [] c_Option_Ois__none(v_x,t_a)=c_fe_qual(v_x,c_Option_Ooption_ONone(t_a),tc_Option_Ooption(t_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Map_Omap__add(V_m,V_m_H,T_a,T_b),c_Map_Odom(V_m_H,T_a,T_b),T_a,tc_Option_Ooption(T_b))| -c_Fun_Oinj__on(V_m_H,c_Map_Odom(V_m_H,T_a,T_b),T_a,tc_Option_Ooption(T_b)). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_m_H,c_Map_Odom(V_m_H,T_a,T_b),T_a,tc_Option_Ooption(T_b))| -c_Fun_Oinj__on(c_Map_Omap__add(V_m,V_m_H,T_a,T_b),c_Map_Odom(V_m_H,T_a,T_b),T_a,tc_Option_Ooption(T_b)). % 42.64/42.77 0 [] c_Map_Odom(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),V_x,hAPP(c_Option_Ooption_OSome(T_b),V_xa),T_a,tc_Option_Ooption(T_b)),T_a,T_b)=c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a). % 42.64/42.77 0 [] c_Map_Omap__le(V_f,c_Map_Omap__add(V_g,V_f,T_a,T_b),T_a,T_b). % 42.64/42.77 0 [] hAPP(V_m2,V_k)!=c_Option_Ooption_ONone(T_a)|c_Map_Omap__comp(V_m1,V_m2,V_k,T_a,T_c,T_b)=c_Option_Ooption_ONone(T_c). % 42.64/42.77 0 [] hAPP(V_m2,V_k)!=c_Option_Ooption_ONone(T_b)|c_Map_Omap__comp(V_m1,V_m2,V_k,T_b,T_a,T_c)=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] hAPP(V_l,V_V)!=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),V_v)| -c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a)|c_Conform_Oconf(V_P,V_h,V_v,c_Conform_Osko__Conform__Xlconf__def__1__1(V_E,V_P,V_V,V_h,V_v,T_a),T_a). % 42.64/42.77 0 [] V_xs!=c_List_Olist_OCons(V_x,V_xs,T_a). % 42.64/42.77 0 [] c_List_Olist_OCons(V_x,V_t,T_a)!=V_t. % 42.64/42.77 0 [] hAPP(V_m,V_k)!=c_Option_Ooption_ONone(T_a)|hAPP(V_n,V_k)!=c_Option_Ooption_ONone(T_a)|hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_f,V_A,T_a,T_b)| -c_Fun_Oinj__on(c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b),V_A,T_a,T_b)| -hBOOL(c_in(V_b,V_A,T_a))| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b),V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b)| -hBOOL(c_in(V_b,V_A,T_a))| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b),V_A,T_a,T_b)| -hBOOL(c_in(V_b,V_A,T_a))| -hBOOL(c_in(V_a,V_A,T_a))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Fun_Ocomp(V_g,V_f,T_b,T_c,T_a),V_A,T_a,T_c)| -c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_c)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.77 0 [] hAPP(c_Option_Omap(V_f,T_b,T_a),c_Option_Ooption_ONone(T_b))=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] c_Set_Oinsert(V_a,V_A,T_a)=V_A| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] V_x=c_Option_Ooption_ONone(T_a)| -hBOOL(c_Option_Ois__none(V_x,T_a)). % 42.64/42.77 0 [] c_Set_Oinsert(V_x,V_A,T_a)!=c_Set_Oinsert(V_x,V_B,T_a)|hBOOL(c_in(V_x,V_B,T_a))|hBOOL(c_in(V_x,V_A,T_a))|V_A=V_B. % 42.64/42.77 0 [] c_Set_Oinsert(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)=c_Set_Oimage(V_f,V_A,T_a,T_b)| -hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.77 0 [] hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x))| -hBOOL(hAPP(V_A,V_x)). % 42.64/42.77 0 [] c_Conform_Oconf(V_P,V_h_H,V_v,V_T,T_a)| -c_Conform_Oconf(V_P,V_h,V_v,V_T,T_a)| -c_Objects_Ohext(V_h,V_h_H). % 42.64/42.77 0 [] c_Objects_Ohext(V_h,V_h). % 42.64/42.77 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). % 42.64/42.77 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). % 42.64/42.77 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). % 42.64/42.77 0 [] hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)!=c_Option_Ooption_ONone(T_a)|hAPP(V_n,V_k)=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)!=c_Option_Ooption_ONone(T_a)|hAPP(V_m,V_k)=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] hAPP(V_m,V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_x)|hAPP(V_n,V_k)!=c_Option_Ooption_ONone(T_a)|hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_x). % 42.64/42.77 0 [] c_Fun_Oswap(V_a,V_b,c_Fun_Oswap(V_b,V_c,c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b),T_a,T_b),T_a,T_b)=c_Fun_Oswap(V_a,V_c,V_f,T_a,T_b)|V_b=V_c|V_a=V_c. % 42.64/42.77 0 [] -c_SmallStep_Oassigned(v_V____,v_ea____). % 42.64/42.77 0 [] hAPP(V_f,V_x)!=hAPP(V_f,V_y)| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b)|V_x=V_y| -hBOOL(c_in(V_y,V_A,T_a))| -hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.77 0 [] hAPP(V_f,V_x)!=hAPP(V_f,V_xa)| -hBOOL(c_in(V_xa,V_A,T_a))| -hBOOL(c_in(V_x,V_A,T_a))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b)|V_x=V_xa. % 42.64/42.77 0 [] hAPP(V_f,V_x)!=hAPP(V_f,V_y)| -hBOOL(c_in(V_y,V_A,T_a))| -hBOOL(c_in(V_x,V_A,T_a))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b)|V_x=V_y. % 42.64/42.77 0 [] hAPP(V_f,V_x)!=hAPP(V_f,V_y)| -hBOOL(c_in(V_y,V_A,T_a))| -hBOOL(c_in(V_x,V_A,T_a))|V_x=V_y| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.77 0 [] c_Option_Ooption_Ooption__rec(V_f1,V_f2,c_Option_Ooption_ONone(T_b),T_a,T_b)=V_f1. % 42.64/42.77 0 [] c_Map_Omap__add(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),V_m,T_a,T_b)=V_m. % 42.64/42.77 0 [] c_Map_Omap__add(V_m,c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),T_a,T_b)=V_m. % 42.64/42.77 0 [] -hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,c_Option_Ooption_ONone(t_b),t_a,t_b)))|hBOOL(hAPP(V_P,V_f1)). % 42.64/42.77 0 [] hAPP(c_COMBK(V_P,T_a,T_b),V_Q)=V_P. % 42.64/42.77 0 [] hAPP(c_COMBI(T_a),V_P)=V_P. % 42.64/42.77 0 [] hBOOL(hAPP(V_S,V_x))| -hBOOL(c_in(V_x,V_S,T_a)). % 42.64/42.77 0 [] hBOOL(c_in(V_x,V_S,T_a))| -hBOOL(hAPP(V_S,V_x)). % 42.64/42.77 0 [] c_Set_Oinsert(V_x,c_Set_Oinsert(V_y,V_A,T_a),T_a)=c_Set_Oinsert(V_y,c_Set_Oinsert(V_x,V_A,T_a),T_a). % 42.64/42.77 0 [] hBOOL(c_in(V_x,c_Set_Oinsert(V_x,V_B,T_a),T_a)). % 42.64/42.77 0 [] hBOOL(c_in(V_a,c_Set_Oinsert(V_a,V_B,T_a),T_a)). % 42.64/42.77 0 [] hBOOL(c_in(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a)). % 42.64/42.77 0 [] c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b)=c_Fun_Oswap(V_b,V_a,V_f,T_a,T_b). % 42.64/42.77 0 [] c_Fun_Oswap(V_a,V_b,c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b),T_a,T_b)=V_f. % 42.64/42.77 0 [] c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_c),T_c,T_b)| -c_Fun_Oinj__on(c_Fun_Ocomp(V_g,V_f,T_c,T_b,T_a),V_A,T_a,T_b). % 42.64/42.77 0 [] c_Map_Omap__le(c_Map_Omap__upds(V_f,V_as,V_bs,T_a,T_b),c_Map_Omap__upds(V_g,V_as,V_bs,T_a,T_b),T_a,T_b)| -c_Map_Omap__le(V_f,V_g,T_a,T_b). % 42.64/42.77 0 [] c_Fun_Oinj__on(V_f,V_A,T_a,T_b)| -c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b). % 42.64/42.77 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). % 42.64/42.77 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). % 42.64/42.77 0 [] c_Set_Oimage(c_COMBI(T_a),V_Y,T_a,T_a)=V_Y. % 42.64/42.77 0 [] hAPP(c_Fun_Ooverride__on(V_f,V_g,V_A,T_a,T_b),V_a)=hAPP(V_f,V_a)|hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_COMBI(T_a),V_A,T_a,T_a). % 42.64/42.77 0 [] c_Map_Omap__le(V_g,V_h,T_a,T_b)| -c_Map_Omap__le(c_Map_Omap__add(V_f,V_g,T_a,T_b),V_h,T_a,T_b). % 42.64/42.77 0 [] c_Set_Oinsert(V_x,c_Set_Oinsert(V_x,V_A,T_a),T_a)=c_Set_Oinsert(V_x,V_A,T_a). % 42.64/42.77 0 [] c_Fun_Oswap(V_a,V_a,V_f,T_a,T_b)=V_f. % 42.64/42.77 0 [] c_Map_Omap__le(V_f,V_f,T_a,T_b). % 42.64/42.77 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). % 42.64/42.77 0 [] hBOOL(hAPP(V_A,V_x))|V_y=V_x| -hBOOL(hAPP(c_Set_Oinsert(V_y,V_A,T_a),V_x)). % 42.64/42.77 0 [] c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a)|hAPP(V_l,c_Conform_Osko__Conform__Xlconf__def__1__2(V_E,V_P,V_h,V_l,T_a))=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),c_Conform_Osko__Conform__Xlconf__def__1__3(V_E,V_P,V_h,V_l,T_a)). % 42.64/42.77 0 [] c_Type_Oty_OClass(V_list)!=c_Type_Oty_OClass(V_list_H)|V_list=V_list_H. % 42.64/42.77 0 [] hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x)=hAPP(V_f,hAPP(V_g,V_x)). % 42.64/42.77 0 [] hAPP(V_a,hAPP(V_b,V_v))=hAPP(c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a),V_v). % 42.64/42.77 0 [] hAPP(c_Fun_Ooverride__on(V_f,V_g,V_A,T_a,T_b),V_a)=hAPP(V_g,V_a)| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] c_WellType_OWT(V_P,V_E,V_e_092_060_094isub_0621,V_T)| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T). % 42.64/42.77 0 [] c_Map_Omap__add(V_m1,c_Map_Omap__add(V_m2,V_m3,T_a,T_b),T_a,T_b)=c_Map_Omap__add(c_Map_Omap__add(V_m1,V_m2,T_a,T_b),V_m3,T_a,T_b). % 42.64/42.77 0 [] c_Map_Omap__add(V_m1,c_Map_Omap__upds(V_m2,V_xs,V_ys,T_a,T_b),T_a,T_b)=c_Map_Omap__upds(c_Map_Omap__add(V_m1,V_m2,T_a,T_b),V_xs,V_ys,T_a,T_b). % 42.64/42.77 0 [] hAPP(c_Option_Omap(V_f,T_b,T_a),V_opt)!=c_Option_Ooption_ONone(T_a)|V_opt=c_Option_Ooption_ONone(T_b). % 42.64/42.77 0 [] c_Map_Omap__add(V_f,V_g,T_a,T_b)=c_Map_Omap__add(V_g,V_f,T_a,T_b)| -c_Map_Omap__le(V_f,c_Map_Omap__add(V_f,V_g,T_a,T_b),T_a,T_b). % 42.64/42.77 0 [] c_Map_Omap__add(V_f,V_g,T_a,T_b)!=c_Map_Omap__add(V_g,V_f,T_a,T_b)|c_Map_Omap__le(V_f,c_Map_Omap__add(V_f,V_g,T_a,T_b),T_a,T_b). % 42.64/42.77 0 [] hAPP(c_Option_Omap(V_f,T_b,T_a),hAPP(c_Option_Omap(V_g,T_c,T_b),V_opt))=hAPP(c_Option_Omap(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),T_c,T_a),V_opt). % 42.64/42.77 0 [] hBOOL(c_in(V_a,V_A,T_a))|V_a=V_b| -hBOOL(c_in(V_a,c_Set_Oinsert(V_b,V_A,T_a),T_a)). % 42.64/42.77 0 [] c_Map_Omap__le(c_Fun_Ofun__upd(V_f,V_x,c_Option_Ooption_ONone(T_b),T_a,tc_Option_Ooption(T_b)),V_f,T_a,T_b). % 42.64/42.77 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). % 42.64/42.77 0 [] hBOOL(c_Option_Ois__none(c_Option_Ooption_ONone(T_a),T_a)). % 42.64/42.77 0 [] c_Option_Ooption_Ooption__case(V_f1,V_f2,c_Option_Ooption_ONone(T_b),T_a,T_b)=V_f1. % 42.64/42.77 0 [] c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a)!=c_Expr_Oexp_OBlock(V_a,V_ty,V_exp,T_a). % 42.64/42.77 0 [] c_Map_Omap__le(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),V_g,T_a,T_b). % 42.64/42.77 0 [] c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a)=c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a). % 42.64/42.77 0 [] hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_x)|hAPP(V_n,V_k)=c_Option_Ooption_ONone(T_a)|hAPP(V_n,V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_x). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,T_b),V_A,T_a,T_b)|hBOOL(c_in(V_y,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b))| -c_Fun_Oinj__on(V_f,V_A,T_a,T_b). % 42.64/42.77 0 [] c_Set_Oimage(c_Fun_Ofun__upd(V_f,V_x,V_y,T_b,T_a),V_A,T_b,T_a)=c_Set_Oimage(V_f,V_A,T_b,T_a)|hBOOL(c_in(V_x,V_A,T_b)). % 42.64/42.77 0 [] c_Fun_Ocomp(V_f,c_Fun_Ocomp(V_g,V_h,T_d,T_c,T_a),T_c,T_b,T_a)=c_Fun_Ocomp(c_Fun_Ocomp(V_f,V_g,T_c,T_b,T_d),V_h,T_d,T_b,T_a). % 42.64/42.77 0 [] hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)). % 42.64/42.77 0 [] c_Set_Oimage(c_Fun_Ocomp(V_f,V_g,T_c,T_a,T_b),V_r,T_b,T_a)=c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_r,T_b,T_c),T_c,T_a). % 42.64/42.77 0 [] hAPP(V_m1,V_x)!=c_Option_Ooption_ONone(T_a)|hAPP(V_m2,V_k)!=hAPP(c_Option_Ooption_OSome(T_b),V_x)|c_Map_Omap__comp(V_m1,V_m2,V_k,T_b,T_a,T_c)=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] c_List_Olist_OCons(V_a,V_list,T_a)!=c_List_Olist_OCons(V_a_H,V_list_H,T_a)|V_a=V_a_H. % 42.64/42.77 0 [] c_List_Olist_OCons(V_a,V_list,T_a)!=c_List_Olist_OCons(V_a_H,V_list_H,T_a)|V_list=V_list_H. % 42.64/42.77 0 [] hBOOL(c_in(V_a,c_Set_Oinsert(V_b,V_B,T_a),T_a))| -hBOOL(c_in(V_a,V_B,T_a)). % 42.64/42.77 0 [] hBOOL(c_in(V_a,c_Set_Oinsert(V_b,V_A,T_a),T_a))| -hBOOL(c_in(V_a,V_A,T_a)). % 42.64/42.77 0 [] c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a)!=c_Fun_Ocomp(V_c,V_d,T_d,T_b,T_a)|hAPP(V_a,hAPP(V_b,V_v))=hAPP(V_c,hAPP(V_d,V_v)). % 42.64/42.77 0 [] hAPP(V_f,hAPP(V_g,V_x))!=hAPP(V_f_H,hAPP(V_g_H,V_x_H))|hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x)=hAPP(c_Fun_Ocomp(V_f_H,V_g_H,T_d,T_a,T_e),V_x_H). % 42.64/42.77 0 [] c_Expr_Oexp_OBlock(V_a,V_ty,V_exp,T_a)!=c_Expr_Oexp_OBlock(V_a_H,V_ty_H,V_exp_H,T_a)|V_exp=V_exp_H. % 42.64/42.77 0 [] c_Expr_Oexp_OBlock(V_a,V_ty,V_exp,T_a)!=c_Expr_Oexp_OBlock(V_a_H,V_ty_H,V_exp_H,T_a)|V_ty=V_ty_H. % 42.64/42.77 0 [] c_Expr_Oexp_OBlock(V_a,V_ty,V_exp,T_a)!=c_Expr_Oexp_OBlock(V_a_H,V_ty_H,V_exp_H,T_a)|V_a=V_a_H. % 42.64/42.77 0 [] c_Expr_Oexp_OBlock(V_a,V_ty,V_exp,T_a)!=c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a). % 42.64/42.77 0 [] c_Expr_Oexp_OTryCatch(V_exp1,V_list,V_a,V_exp2,T_a)!=c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a)|V_exp2=V_exp2_H. % 42.64/42.77 0 [] c_Expr_Oexp_OTryCatch(V_exp1,V_list,V_a,V_exp2,T_a)!=c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a)|V_a=V_a_H. % 42.64/42.77 0 [] c_Expr_Oexp_OTryCatch(V_exp1,V_list,V_a,V_exp2,T_a)!=c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a)|V_list=V_list_H. % 42.64/42.77 0 [] c_Expr_Oexp_OTryCatch(V_exp1,V_list,V_a,V_exp2,T_a)!=c_Expr_Oexp_OTryCatch(V_exp1_H,V_list_H,V_a_H,V_exp2_H,T_a)|V_exp1=V_exp1_H. % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b))!=c_Fun_Ofun__upd(V_n,V_a,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b))|V_x=V_y. % 42.64/42.77 0 [] c_Option_Othe(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)=V_x. % 42.64/42.77 0 [] c_Option_Ooption_Ooption__rec(V_f1,V_f2,hAPP(c_Option_Ooption_OSome(T_b),V_a),T_a,T_b)=hAPP(V_f2,V_a). % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,T_b),V_z)=hAPP(V_f,V_z)|V_z=V_x. % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_f,V_x,V_y,T_b,T_a),V_z)=hAPP(V_f,V_z)|V_z=V_x. % 42.64/42.77 0 [] hAPP(V_t,V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_x)|c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_a),V_x),T_b,tc_Option_Ooption(T_a))=V_t. % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_m,V_xa,hAPP(c_Option_Ooption_OSome(T_a),V_x),T_aa,tc_Option_Ooption(T_a)),V_xa)=hAPP(c_Option_Ooption_OSome(T_a),V_x). % 42.64/42.77 0 [] hAPP(V_m1,V_x)!=hAPP(c_Option_Ooption_OSome(T_a),V_v)|hAPP(V_m2,V_k)!=hAPP(c_Option_Ooption_OSome(T_b),V_x)|c_Map_Omap__comp(V_m1,V_m2,V_k,T_b,T_a,T_c)=hAPP(c_Option_Ooption_OSome(T_a),V_v). % 42.64/42.77 0 [] c_Map_Omap__add(V_f,c_Fun_Ofun__upd(V_g,V_x,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b)),T_a,T_b)=c_Fun_Ofun__upd(c_Map_Omap__add(V_f,V_g,T_a,T_b),V_x,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b)). % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_f,V_x,hAPP(V_f,V_x),T_aa,T_a)=V_f. % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,T_aa),V_x)=V_y. % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_f,V_x,hAPP(V_f,V_x),T_a,T_b)=V_f. % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_f,V_x,V_y,T_b,T_a),V_x)=V_y. % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_f,V_x,hAPP(V_f,V_x),T_b,T_a)=V_f. % 42.64/42.77 0 [] c_Fun_Oswap(V_a,V_b,V_f,T_a,T_b)=c_Fun_Ofun__upd(c_Fun_Ofun__upd(V_f,V_a,hAPP(V_f,V_b),T_a,T_b),V_b,hAPP(V_f,V_a),T_a,T_b). % 42.64/42.77 0 [] c_Fun_Ofun__upd(c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,T_b),V_x,V_z,T_a,T_b)=c_Fun_Ofun__upd(V_f,V_x,V_z,T_a,T_b). % 42.64/42.77 0 [] c_Conform_Olconf(V_P,V_h,c_Fun_Ofun__upd(V_l,V_V,hAPP(c_Option_Ooption_OSome(tc_Value_Oval),V_v),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)),c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_T),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),T_a)| -c_Conform_Oconf(V_P,V_h,V_v,V_T,T_a)| -c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a). % 42.64/42.77 0 [] c_Fun_Ofun__upd(c_Fun_Ooverride__on(V_f,c_Fun_Ofun__upd(V_g,V_a,hAPP(c_Option_Ooption_OSome(T_b),V_b),T_a,tc_Option_Ooption(T_b)),V_A,T_a,tc_Option_Ooption(T_b)),V_a,hAPP(V_g,V_a),T_a,tc_Option_Ooption(T_b))=c_Fun_Ooverride__on(V_f,V_g,c_Set_Oinsert(V_a,V_A,T_a),T_a,tc_Option_Ooption(T_b)). % 42.64/42.77 0 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,c_Fun_Ofun__upd(v_E____,v_V____,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),v_T____),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),v_e_Ha____,v_Te_H____). % 42.64/42.77 0 [] c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OBlock(V_V,V_T,V_e,tc_List_Olist(tc_String_Ochar)),V_T_H)| -c_WellTypeRT_OWTrt(V_P,V_h,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_T),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e,V_T_H). % 42.64/42.77 0 [] -hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,hAPP(c_Option_Ooption_OSome(t_b),V_xa),t_a,t_b)))|hBOOL(hAPP(V_P,hAPP(V_f2,V_xa))). % 42.64/42.77 0 [] -hBOOL(hAPP(V_P,c_Option_Ooption_Ooption__case(V_f1,V_f2,hAPP(c_Option_Ooption_OSome(t_b),V_a),t_a,t_b)))|hBOOL(hAPP(V_P,hAPP(V_f2,V_a))). % 42.64/42.77 0 [] c_Fun_Oinj__on(c_Option_Ooption_OSome(T_a),V_A,T_a,tc_Option_Ooption(T_a)). % 42.64/42.77 0 [] -hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(T_a),V_x),T_a)). % 42.64/42.77 0 [] c_Fun_Ofun__upd(c_Fun_Ofun__upd(V_m,V_a,V_b,T_a,T_b),V_c,V_d,T_a,T_b)=c_Fun_Ofun__upd(c_Fun_Ofun__upd(V_m,V_c,V_d,T_a,T_b),V_a,V_b,T_a,T_b)|V_a=V_c. % 42.64/42.77 0 [] c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OBlock(V_V,V_T,V_e,tc_List_Olist(tc_String_Ochar)),V_T_H)| -c_WellType_OWT(V_P,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_T),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e,V_T_H)| -c_Decl_Ois__type(V_P,V_T,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.64/42.77 0 [] hAPP(c_Option_Ooption_OSome(T_a),V_a)!=hAPP(c_Option_Ooption_OSome(T_a),V_a_H)|V_a=V_a_H. % 42.64/42.77 0 [] hAPP(c_Option_Ooption_OSome(T_a),V_xa)!=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] hAPP(c_Option_Ooption_OSome(T_a),V_a_H)!=c_Option_Ooption_ONone(T_a). % 42.64/42.77 0 [] c_Map_Omap__le(c_Fun_Ofun__upd(V_f,V_a,V_b,T_a,tc_Option_Ooption(T_b)),c_Fun_Ofun__upd(V_g,V_a,V_b,T_a,tc_Option_Ooption(T_b)),T_a,T_b)| -c_Map_Omap__le(V_f,V_g,T_a,T_b). % 42.64/42.77 0 [] c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OBlock(V_V,V_T,V_e,tc_List_Olist(tc_String_Ochar)),V_T_H)|c_SmallStep_Oassigned(V_V,V_e)| -c_Progress_OWTrt_H(V_P,V_h,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_T),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e,V_T_H). % 42.64/42.77 0 [] c_Map_Omap__le(c_Fun_Ofun__upd(V_m1,V_x,c_Option_Ooption_ONone(T_b),T_a,tc_Option_Ooption(T_b)),c_Fun_Ofun__upd(V_m2,V_x,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b)),T_a,T_b)| -c_Map_Omap__le(V_m1,V_m2,T_a,T_b). % 42.64/42.77 0 [] c_WellType_OWT(V_P,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(V_C)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e_092_060_094isub_0622,V_T)| -c_WellType_OWT(V_P,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T). % 42.64/42.77 0 [] hAPP(V_E,c_Conform_Osko__Conform__Xlconf__def__1__2(V_E,V_P,V_h,V_l,T_a))!=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_x)|c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a)| -c_Conform_Oconf(V_P,V_h,c_Conform_Osko__Conform__Xlconf__def__1__3(V_E,V_P,V_h,V_l,T_a),V_x,T_a). % 42.64/42.77 0 [] hAPP(V_m,V_x)!=hAPP(c_Option_Ooption_OSome(T_a),V_y)|V_x=V_a|hAPP(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_a),V_b),T_b,tc_Option_Ooption(T_a)),V_x)=hAPP(c_Option_Ooption_OSome(T_a),V_y). % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_a),V_b),T_b,tc_Option_Ooption(T_a)),V_x)!=hAPP(c_Option_Ooption_OSome(T_a),V_y)|hAPP(V_m,V_x)=hAPP(c_Option_Ooption_OSome(T_a),V_y)|V_b=V_y. % 42.64/42.77 0 [] hAPP(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_a),V_b),T_b,tc_Option_Ooption(T_a)),V_x)!=hAPP(c_Option_Ooption_OSome(T_a),V_y)|hAPP(V_m,V_x)=hAPP(c_Option_Ooption_OSome(T_a),V_y)|V_x=V_a. % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b))!=c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a). % 42.64/42.77 0 [] hAPP(V_E,V_V)!=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),V_T)| -c_Conform_Oconf(V_P,V_h,V_v,V_T,T_a)| -c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a)|c_Conform_Olconf(V_P,V_h,c_Fun_Ofun__upd(V_l,V_V,hAPP(c_Option_Ooption_OSome(tc_Value_Oval),V_v),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)),V_E,T_a). % 42.64/42.77 0 [] hAPP(V_l,V_V)!=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),V_v)| -c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a)|hAPP(V_E,V_V)=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Conform_Osko__Conform__Xlconf__def__1__1(V_E,V_P,V_V,V_h,V_v,T_a)). % 42.64/42.77 0 [] c_Option_Ooption_Ooption__case(V_f1,V_f2,hAPP(c_Option_Ooption_OSome(T_b),V_a),T_a,T_b)=hAPP(V_f2,V_a). % 42.64/42.77 0 [] c_Fun_Ocomp(c_Option_Omap(V_f,T_c,T_b),c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_c),V_b),T_a,tc_Option_Ooption(T_c)),tc_Option_Ooption(T_c),tc_Option_Ooption(T_b),T_a)=c_Fun_Ofun__upd(c_Fun_Ocomp(c_Option_Omap(V_f,T_c,T_b),V_m,tc_Option_Ooption(T_c),tc_Option_Ooption(T_b),T_a),V_a,hAPP(c_Option_Ooption_OSome(T_b),hAPP(V_f,V_b)),T_a,tc_Option_Ooption(T_b)). % 42.64/42.77 0 [] hAPP(v_l_Ha____,v_V____)=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),v_v____). % 42.64/42.77 0 [] c_Map_Omap__upds(V_m,c_List_Olist_OCons(V_a,V_as,T_a),c_List_Olist_OCons(V_b,V_bs,T_b),T_a,T_b)=c_Map_Omap__upds(c_Fun_Ofun__upd(V_m,V_a,hAPP(c_Option_Ooption_OSome(T_b),V_b),T_a,tc_Option_Ooption(T_b)),V_as,V_bs,T_a,T_b). % 42.64/42.77 0 [] V_b=V_y|hAPP(c_Fun_Ofun__upd(V_m,V_x,hAPP(c_Option_Ooption_OSome(T_aa),V_b),T_a,tc_Option_Ooption(T_aa)),V_x)!=hAPP(c_Option_Ooption_OSome(T_aa),V_y). % 42.64/42.77 0 [] c_Fun_Ocomp(V_f,c_Fun_Ofun__upd(V_g,V_x,V_y,T_a,T_c),T_c,T_b,T_a)=c_Fun_Ofun__upd(c_Fun_Ocomp(V_f,V_g,T_c,T_b,T_a),V_x,hAPP(V_f,V_y),T_a,T_b). % 42.64/42.77 0 [] c_Option_Ooption_ONone(T_a)!=hAPP(c_Option_Ooption_OSome(T_a),V_y). % 42.64/42.77 0 [] c_Option_Ooption_ONone(T_a)!=hAPP(c_Option_Ooption_OSome(T_a),V_a_H). % 42.64/42.77 0 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OBlock(v_V____,v_T____,v_ea____,tc_List_Olist(tc_String_Ochar)),v_Te____). % 42.64/42.77 0 [] c_Set_Oimage(c_Fun_Ofun__upd(V_m,V_x,hAPP(c_Option_Ooption_OSome(T_b),V_y),T_a,tc_Option_Ooption(T_b)),V_A,T_a,tc_Option_Ooption(T_b))=c_Set_Oimage(V_m,V_A,T_a,tc_Option_Ooption(T_b))|hBOOL(c_in(V_x,V_A,T_a)). % 42.64/42.77 0 [] hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_x)|hAPP(V_m,V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_x)|hAPP(V_n,V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_x). % 42.64/42.77 0 [] hAPP(c_Option_Omap(V_f,T_b,T_a),hAPP(c_Option_Ooption_OSome(T_b),V_x))=hAPP(c_Option_Ooption_OSome(T_a),hAPP(V_f,V_x)). % 42.64/42.77 0 [] c_WellTypeRT_OWTrt(V_P,V_h,c_Fun_Ofun__upd(V_E,V_V,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(V_C)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),V_e_092_060_094isub_0622,V_T)| -c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T). % 42.64/42.77 0 [] c_Conform_Olconf(V_P,V_h_H,V_l,V_E,T_a)| -c_Objects_Ohext(V_h,V_h_H)| -c_Conform_Olconf(V_P,V_h,V_l,V_E,T_a). % 42.64/42.77 0 [] hAPP(V_m2,V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_k_H)|c_Map_Omap__comp(V_m1,V_m2,V_k,T_a,T_c,T_b)=hAPP(V_m1,V_k_H). % 42.64/42.77 0 [] -hBOOL(hAPP(V_P,c_ATP__Linkup_Osko__Option__Xospec__1__1(hAPP(c_Option_Ooption_OSome(T_a),V_x),V_P,T_a)))|hBOOL(hAPP(V_P,V_x)). % 42.64/42.77 0 [] hAPP(c_COMBI(t_a),v_P)=v_P. % 42.64/42.77 0 [] hAPP(V_n,V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_xx)|hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_xx). % 42.64/42.77 0 [] hAPP(V_n,V_k)!=hAPP(c_Option_Ooption_OSome(T_a),V_x)|hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k)=hAPP(c_Option_Ooption_OSome(T_a),V_x). % 42.64/42.77 0 [] c_Fun_Ofun__upd(V_f,V_x,V_y,T_a,T_b)!=V_f|hAPP(V_f,V_x)=V_y. % 42.64/42.77 0 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OBlock(v_V____,v_T____,v_ea____,tc_List_Olist(tc_String_Ochar)),v_Te____). % 42.64/42.77 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)))). % 42.64/42.77 0 [] -c_Conform_Olconf(v_P,v_h_Ha____,v_l_Ha____,c_Fun_Ofun__upd(v_E____,v_V____,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),v_T____),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.64/42.77 0 [] class_Lattices_Oboolean__algebra(tc_fun(T_2,T_1))| -class_Lattices_Oboolean__algebra(T_1). % 42.64/42.77 0 [] class_Orderings_Otop(tc_fun(T_2,T_1))| -class_Orderings_Otop(T_1). % 42.64/42.77 0 [] class_Orderings_Obot(tc_fun(T_2,T_1))| -class_Orderings_Obot(T_1). % 42.64/42.77 0 [] class_HOL_Ouminus(tc_fun(T_2,T_1))| -class_HOL_Ouminus(T_1). % 42.64/42.77 0 [] class_HOL_Ominus(tc_fun(T_2,T_1))| -class_HOL_Ominus(T_1). % 42.64/42.77 0 [] class_OrderedGroup_Ocomm__monoid__mult(tc_nat). % 42.64/42.77 0 [] class_OrderedGroup_Ocomm__monoid__add(tc_nat). % 42.64/42.77 0 [] class_Orderings_Obot(tc_nat). % 42.64/42.77 0 [] class_HOL_Ominus(tc_nat). % 42.64/42.77 0 [] class_Lattices_Oboolean__algebra(tc_bool). % 42.64/42.77 0 [] class_Orderings_Otop(tc_bool). % 42.64/42.77 0 [] class_Orderings_Obot(tc_bool). % 42.64/42.77 0 [] class_HOL_Ouminus(tc_bool). % 42.64/42.77 0 [] class_HOL_Ominus(tc_bool). % 42.64/42.77 0 [] hBOOL(c_fe_qual(V_x,V_x,T_a)). % 42.64/42.77 0 [] V_X=V_Y| -hBOOL(c_fe_qual(V_X,V_Y,T_a)). % 42.64/42.77 end_of_list. % 42.64/42.77 % 42.64/42.77 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 42.64/42.77 % 42.64/42.77 This ia a non-Horn set with equality. The strategy will be % 42.64/42.77 Knuth-Bendix, ordered hyper_res, factoring, and unit % 42.64/42.77 deletion, with positive clauses in sos and nonpositive % 42.64/42.77 clauses in usable. % 42.64/42.77 % 42.64/42.77 dependent: set(knuth_bendix). % 42.64/42.77 dependent: set(anl_eq). % 42.64/42.77 dependent: set(para_from). % 42.64/42.77 dependent: set(para_into). % 42.64/42.77 dependent: clear(para_from_right). % 42.64/42.77 dependent: clear(para_into_right). % 42.64/42.77 dependent: set(para_from_vars). % 42.64/42.77 dependent: set(eq_units_both_ways). % 42.64/42.77 dependent: set(dynamic_demod_all). % 42.64/42.77 dependent: set(dynamic_demod). % 42.64/42.77 dependent: set(order_eq). % 42.64/42.77 dependent: set(back_demod). % 42.64/42.77 dependent: set(lrpo). % 42.64/42.77 dependent: set(hyper_res). % 42.64/42.77 dependent: set(unit_deletion). % 42.64/42.77 dependent: set(factor). % 42.64/42.77 % 42.64/42.77 ------------> process usable: % 42.64/42.77 ** KEPT (pick-wt=39): 1 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(A,B,C,D,tc_Option_Ooption(E)),F,D,E)=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,c_HOL_Ominus__class_Ominus(F,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),B,C,D,tc_Option_Ooption(E))| -hBOOL(c_in(B,F,D)). % 42.64/42.77 ** KEPT (pick-wt=39): 3 [copy,2,flip.1] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(C,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),C,F,D,tc_Option_Ooption(E))=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,D,E),C,F,D,tc_Option_Ooption(E))| -hBOOL(c_in(C,B,D)). % 42.64/42.77 ** KEPT (pick-wt=35): 5 [copy,4,flip.1] c_Set_Oinsert(A,c_Set_Oimage(B,c_HOL_Ominus__class_Ominus(C,c_Set_Oinsert(D,c_Orderings_Obot__class_Obot(tc_fun(E,tc_bool)),E),tc_fun(E,tc_bool)),E,F),F)=c_Set_Oimage(c_Fun_Ofun__upd(B,D,A,E,F),C,E,F)| -hBOOL(c_in(D,C,E)). % 42.64/42.77 ** KEPT (pick-wt=35): 6 [] c_Fun_Oinj__on(A,c_Set_Oinsert(B,C,D),D,E)|hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,c_HOL_Ominus__class_Ominus(C,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),E))| -c_Fun_Oinj__on(A,C,D,E). % 42.64/42.77 ** KEPT (pick-wt=30): 7 [] -hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,c_HOL_Ominus__class_Ominus(C,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),E))| -c_Fun_Oinj__on(A,c_Set_Oinsert(B,C,D),D,E). % 42.64/42.77 ** KEPT (pick-wt=21): 8 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,C),D,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(B,D,tc_fun(C,tc_bool))| -hBOOL(c_in(A,D,C)). % 42.64/42.77 ** KEPT (pick-wt=22): 9 [] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=B| -hBOOL(c_in(A,B,C)). % 42.64/42.77 ** KEPT (pick-wt=9): 11 [copy,10,flip.2] -class_Lattices_Oboolean__algebra(A)|c_Orderings_Otop__class_Otop(A)=c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(A),A). % 42.64/42.77 ** KEPT (pick-wt=15): 12 [] -class_HOL_Ouminus(A)|hAPP(c_HOL_Ouminus__class_Ouminus(B,tc_fun(t_a,A)),v_x)=c_HOL_Ouminus__class_Ouminus(hAPP(B,v_x),A). % 42.64/42.77 ** KEPT (pick-wt=14): 13 [] c_HOL_Ouminus__class_Ouminus(A,tc_fun(B,tc_bool))!=c_HOL_Ouminus__class_Ouminus(C,tc_fun(B,tc_bool))|A=C. % 42.64/42.77 ** KEPT (pick-wt=12): 14 [] -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(B,A)!=c_HOL_Ouminus__class_Ouminus(C,A)|B=C. % 42.64/42.77 ** KEPT (pick-wt=12): 15 [] -class_Lattices_Oboolean__algebra(A)|c_HOL_Ouminus__class_Ouminus(B,A)!=c_HOL_Ouminus__class_Ouminus(C,A)|B=C. % 42.64/42.77 ** KEPT (pick-wt=9): 16 [] -class_Lattices_Oboolean__algebra(A)|c_HOL_Ouminus__class_Ouminus(c_Orderings_Otop__class_Otop(A),A)=c_Orderings_Obot__class_Obot(A). % 42.64/42.77 ** KEPT (pick-wt=15): 17 [] -hBOOL(c_in(A,B,C))| -hBOOL(c_in(A,c_HOL_Ominus__class_Ominus(D,B,tc_fun(C,tc_bool)),C)). % 42.64/42.77 ** KEPT (pick-wt=15): 18 [] hBOOL(c_in(A,B,C))| -hBOOL(c_in(A,c_HOL_Ominus__class_Ominus(B,D,tc_fun(C,tc_bool)),C)). % 42.64/42.77 ** KEPT (pick-wt=15): 19 [] c_Fun_Oinj__on(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D,E)| -c_Fun_Oinj__on(A,B,D,E). % 42.64/42.77 ** KEPT (pick-wt=14): 20 [] -hBOOL(c_in(A,B,C))| -hBOOL(c_in(A,c_HOL_Ouminus__class_Ouminus(B,tc_fun(C,tc_bool)),C)). % 42.64/42.77 ** KEPT (pick-wt=28): 21 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),c_Set_Oinsert(B,E,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),E,tc_fun(D,tc_bool)). % 42.64/42.77 ** KEPT (pick-wt=14): 22 [] -class_OrderedGroup_Oab__group__add(A)|c_HOL_Ominus__class_Ominus(B,C,A)!=c_HOL_Ominus__class_Ominus(D,D,A)|B=C. % 42.64/42.77 ** KEPT (pick-wt=14): 23 [] -class_OrderedGroup_Oab__group__add(A)|c_HOL_Ominus__class_Ominus(B,B,A)!=c_HOL_Ominus__class_Ominus(C,D,A)|C=D. % 42.64/42.77 ** KEPT (pick-wt=20): 24 [] hBOOL(c_in(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D))|hBOOL(c_in(A,C,D))| -hBOOL(c_in(A,B,D)). % 42.64/42.77 Following clause subsumed by 24 during input processing: 0 [] hBOOL(c_in(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D))|hBOOL(c_in(A,C,D))| -hBOOL(c_in(A,B,D)). % 42.64/42.77 ** KEPT (pick-wt=33): 25 [] c_Set_Oimage(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D,E)=c_HOL_Ominus__class_Ominus(c_Set_Oimage(A,B,D,E),c_Set_Oimage(A,C,D,E),tc_fun(E,tc_bool))| -c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(D,tc_bool)),D,E). % 42.64/42.77 ** KEPT (pick-wt=19): 26 [] -class_HOL_Ominus(A)|hAPP(c_HOL_Ominus__class_Ominus(B,C,tc_fun(t_a,A)),v_x)=c_HOL_Ominus__class_Ominus(hAPP(B,v_x),hAPP(C,v_x),A). % 42.64/42.77 ** KEPT (pick-wt=9): 27 [] -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B. % 42.64/42.77 ** KEPT (pick-wt=9): 28 [] -class_Lattices_Oboolean__algebra(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B. % 42.64/42.77 Following clause subsumed by 27 during input processing: 0 [flip.2] -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B. % 42.64/42.77 Following clause subsumed by 27 during input processing: 0 [flip.2] -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B. % 42.64/42.77 Following clause subsumed by 27 during input processing: 0 [] -class_OrderedGroup_Ogroup__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(B,A),A)=B. % 42.64/42.77 ** KEPT (pick-wt=13): 29 [] -class_OrderedGroup_Oab__group__add(A)|c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(B,C,A),A)=c_HOL_Ominus__class_Ominus(C,B,A). % 42.64/42.77 ** KEPT (pick-wt=34): 30 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,C,D),E,c_Option_Ooption_ONone(D),C,tc_Option_Ooption(D))=c_Map_Orestrict__map(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C,D)| -hBOOL(c_in(E,B,C)). % 42.64/42.77 ** KEPT (pick-wt=33): 32 [copy,31,flip.2] c_Map_Odom(A,B,C)!=c_Set_Oinsert(D,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)|c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),B),D,hAPP(c_Option_Ooption_OSome(C),c_Map_Osko__Map__Xdom__e_q__singleton__conv__1__1(A,D,B,C)),B,tc_Option_Ooption(C))=A. % 42.64/42.77 ** KEPT (pick-wt=26): 33 [] c_Set_Oimage(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,A,C),c_Set_Oimage(B,D,A,C),C,A)=D| -c_Fun_Oinj__on(B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A,C). % 42.64/42.77 Following clause subsumed by 33 during input processing: 0 [] c_Set_Oimage(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,A,C),c_Set_Oimage(B,D,A,C),C,A)=D| -c_Fun_Oinj__on(B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A,C). % 42.64/42.77 ** KEPT (pick-wt=22): 34 [] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))| -hBOOL(hAPP(A,hAPP(C,v_sko__Option__Xoption__Xsplit__1(A,C,D))))| -hBOOL(hAPP(A,B)). % 42.64/42.77 ** KEPT (pick-wt=22): 35 [] hAPP(c_Fun_Othe__inv__into(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,A,C),hAPP(B,D))=D| -c_Fun_Oinj__on(B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A,C). % 42.64/42.77 ** KEPT (pick-wt=57): 37 [copy,36,flip.4,flip.5] c_Fun_Oinj__on(A,B,C,D)| -c_Fun_Oinj__on(A,c_Set_Oimage(E,B,C,C),C,D)| -c_Fun_Oinj__on(E,B,C,C)|hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,E,A,C,D))=hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,E,A,C,D))|hAPP(A,hAPP(E,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,E,A,C,D)))=hAPP(A,hAPP(E,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,E,A,C,D))). % 42.64/42.77 ** KEPT (pick-wt=57): 39 [copy,38,flip.4,flip.5] c_Fun_Oinj__on(A,c_Set_Oimage(B,C,D,D),D,E)| -c_Fun_Oinj__on(A,C,D,E)| -c_Fun_Oinj__on(B,C,D,D)|hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(C,B,A,D,E))=hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(C,B,A,D,E))|hAPP(A,hAPP(B,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(C,B,A,D,E)))=hAPP(A,hAPP(B,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(C,B,A,D,E))). % 42.64/42.77 ** KEPT (pick-wt=57): 41 [copy,40,flip.1,flip.2] hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,C,A,D,E))!=hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,C,A,D,E))|hAPP(A,hAPP(C,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,C,A,D,E)))!=hAPP(A,hAPP(C,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,C,A,D,E)))|c_Fun_Oinj__on(A,B,D,E)| -c_Fun_Oinj__on(A,c_Set_Oimage(C,B,D,D),D,E)| -c_Fun_Oinj__on(C,B,D,D). % 42.64/42.77 ** KEPT (pick-wt=57): 43 [copy,42,flip.1,flip.2] hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,C,A,D,E))!=hAPP(A,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,C,A,D,E))|hAPP(A,hAPP(C,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,C,A,D,E)))!=hAPP(A,hAPP(C,c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,C,A,D,E)))|c_Fun_Oinj__on(A,c_Set_Oimage(C,B,D,D),D,E)| -c_Fun_Oinj__on(A,B,D,E)| -c_Fun_Oinj__on(C,B,D,D). % 42.64/42.77 ** KEPT (pick-wt=12): 44 [] -hBOOL(hAPP(A,B))| -hBOOL(c_in(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C)). % 42.64/42.77 ** KEPT (pick-wt=18): 45 [] c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)!=c_Set_Oinsert(C,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)|A=C. % 42.64/42.77 ** KEPT (pick-wt=17): 46 [] c_Conform_Oconf(A,B,C,D,E)| -c_TypeRel_Owiden(A,F,D,E)| -c_Conform_Oconf(A,B,C,F,E). % 42.64/42.77 ** KEPT (pick-wt=15): 47 [] c_TypeRel_Owiden(A,B,C,D)| -c_TypeRel_Owiden(A,E,C,D)| -c_TypeRel_Owiden(A,B,E,D). % 42.64/42.77 ** KEPT (pick-wt=11): 48 [] -class_Orderings_Obot(A)|hAPP(c_Orderings_Obot__class_Obot(tc_fun(t_a,A)),v_x)=c_Orderings_Obot__class_Obot(A). % 42.64/42.77 ** KEPT (pick-wt=16): 49 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oimage(B,C,D,A)|C=c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)). % 42.64/42.77 ** KEPT (pick-wt=9): 50 [] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 42.64/42.77 ** KEPT (pick-wt=18): 51 [] hAPP(A,B)!=hAPP(A,C)| -c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(D,tc_bool)),D,E)|B=C. % 42.64/42.77 ** KEPT (pick-wt=30): 52 [] hAPP(A,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(B,A,C,D,E))!=hAPP(C,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(B,A,C,D,E))|c_Option_Ooption_Ooption__case(F,A,B,E,D)=c_Option_Ooption_Ooption__case(F,C,B,E,D). % 42.64/42.77 ** KEPT (pick-wt=7): 53 [] -hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B)). % 42.64/42.77 ** KEPT (pick-wt=9): 54 [] c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool))!=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 42.64/42.77 ** KEPT (pick-wt=22): 55 [] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))| -hBOOL(hAPP(A,hAPP(C,v_sko__Option__Xoption__Xsplit__asm__1(A,C,D))))| -hBOOL(hAPP(A,B)). % 42.64/42.77 ** KEPT (pick-wt=11): 56 [] -class_Orderings_Otop(A)|hAPP(c_Orderings_Otop__class_Otop(tc_fun(t_a,A)),v_x)=c_Orderings_Otop__class_Otop(A). % 42.64/42.77 ** KEPT (pick-wt=12): 57 [] c_Option_Oset(A,B)!=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool))|A=c_Option_Ooption_ONone(B). % 42.64/42.77 ** KEPT (pick-wt=16): 58 [] hAPP(c_Map_Orestrict__map(A,B,C,D),E)=hAPP(A,E)| -hBOOL(c_in(E,B,C)). % 42.64/42.77 ** KEPT (pick-wt=27): 59 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|A=E|A=D. % 42.64/42.77 ** KEPT (pick-wt=27): 60 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|B=D|A=D. % 42.64/42.77 ** KEPT (pick-wt=27): 61 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|A=E|B=E. % 42.64/42.77 ** KEPT (pick-wt=27): 62 [] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)!=c_Set_Oinsert(D,c_Set_Oinsert(E,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)|B=D|B=E. % 42.64/42.77 ** KEPT (pick-wt=17): 63 [] c_Map_Odom(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool))|A=c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),B). % 42.64/42.77 ** KEPT (pick-wt=9): 64 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oinsert(B,C,A). % 42.64/42.77 ** KEPT (pick-wt=8): 65 [] -hBOOL(c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)). % 42.64/42.77 Following clause subsumed by 65 during input processing: 0 [] -hBOOL(c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)). % 42.64/42.77 Following clause subsumed by 65 during input processing: 0 [] hBOOL(hAPP(A,B))| -hBOOL(c_in(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C)). % 42.64/42.77 Following clause subsumed by 65 during input processing: 0 [] -hBOOL(c_in(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)). % 42.64/42.77 ** KEPT (pick-wt=22): 66 [] hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),B,A,C),hAPP(B,D))=D| -c_Fun_Oinj__on(B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool)),A,C). % 42.68/42.78 Following clause subsumed by 66 during input processing: 0 [] -c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),B,C)|hAPP(c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),A,B,C),hAPP(A,D))=D. % 42.68/42.78 ** KEPT (pick-wt=16): 67 [] c_Set_Oimage(A,B,C,D)!=c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool))|B=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 42.68/42.78 ** KEPT (pick-wt=28): 68 [] c_Fun_Ocomp(c_Fun_Ocomp(A,c_Hilbert__Choice_Oinv__into(c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),C,B,D),B,E,D),C,D,E,B)=A| -c_Fun_Oinj__on(C,c_Orderings_Otop__class_Otop(tc_fun(B,tc_bool)),B,D). % 42.68/42.78 ** KEPT (pick-wt=20): 69 [] hBOOL(c_in(A,c_List_Oset(B,C),C))|A=D| -hBOOL(c_in(A,c_List_Oset(c_List_Olist_OCons(D,B,C),C),C)). % 42.68/42.78 Following clause subsumed by 50 during input processing: 0 [] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool))|hBOOL(c_in(A,B,C)). % 42.68/42.78 ** KEPT (pick-wt=14): 70 [] A=B| -hBOOL(c_in(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),C)). % 42.68/42.78 ** KEPT (pick-wt=16): 71 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hBOOL(c_in(D,c_Map_Oran(A,E,C),C)). % 42.68/42.78 ** KEPT (pick-wt=13): 72 [] A=hAPP(c_Option_Ooption_OSome(B),C)| -hBOOL(c_in(C,c_Option_Oset(A,B),B)). % 42.68/42.78 ** KEPT (pick-wt=16): 73 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hBOOL(c_in(B,c_Map_Odom(A,E,C),E)). % 42.68/42.78 ** KEPT (pick-wt=20): 74 [] hBOOL(c_in(hAPP(c_Hilbert__Choice_Oinv__into(A,B,C,D),E),A,C))| -hBOOL(c_in(E,c_Set_Oimage(B,A,C,D),D)). % 42.68/42.78 ** KEPT (pick-wt=36): 75 [] hAPP(c_Hilbert__Choice_Oinv__into(A,B,C,D),E)!=hAPP(c_Hilbert__Choice_Oinv__into(A,B,C,D),F)|E=F| -hBOOL(c_in(F,c_Set_Oimage(B,A,C,D),D))| -hBOOL(c_in(E,c_Set_Oimage(B,A,C,D),D)). % 42.68/42.78 ** KEPT (pick-wt=20): 76 [] hAPP(A,hAPP(c_Hilbert__Choice_Oinv__into(B,A,C,D),E))=E| -hBOOL(c_in(E,c_Set_Oimage(A,B,C,D),D)). % 42.68/42.78 ** KEPT (pick-wt=21): 77 [] hAPP(c_Hilbert__Choice_Oinv__into(A,B,C,D),hAPP(B,E))=E| -hBOOL(c_in(E,A,C))| -c_Fun_Oinj__on(B,A,C,D). % 42.68/42.78 Following clause subsumed by 77 during input processing: 0 [] -hBOOL(c_in(A,B,C))| -c_Fun_Oinj__on(D,B,C,E)|hAPP(c_Hilbert__Choice_Oinv__into(B,D,C,E),hAPP(D,A))=A. % 42.68/42.78 ** KEPT (pick-wt=21): 78 [] hAPP(c_Fun_Othe__inv__into(A,B,C,D),hAPP(B,E))=E| -hBOOL(c_in(E,A,C))| -c_Fun_Oinj__on(B,A,C,D). % 42.68/42.78 Following clause subsumed by 78 during input processing: 0 [] -c_Fun_Oinj__on(A,B,C,D)|hAPP(c_Fun_Othe__inv__into(B,A,C,D),hAPP(A,E))=E| -hBOOL(c_in(E,B,C)). % 42.68/42.78 ** KEPT (pick-wt=14): 79 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)| -hBOOL(c_in(B,c_Map_Odom(A,D,C),D)). % 42.68/42.78 ** KEPT (pick-wt=20): 80 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|c_Set_Oinsert(B,c_Map_Odom(A,E,C),E)=c_Map_Odom(A,E,C). % 42.68/42.78 ** KEPT (pick-wt=18): 81 [] c_Fun_Oinj__on(c_Fun_Othe__inv__into(A,B,C,D),c_Set_Oimage(B,A,C,D),D,C)| -c_Fun_Oinj__on(B,A,C,D). % 42.68/42.78 ** KEPT (pick-wt=22): 82 [] c_Set_Oimage(A,B,C,D)!=c_Set_Oimage(A,E,C,D)| -c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,D)|B=E. % 42.68/42.78 ** KEPT (pick-wt=20): 83 [] c_Set_Oimage(c_Fun_Othe__inv__into(A,B,C,D),c_Set_Oimage(B,A,C,D),D,C)=A| -c_Fun_Oinj__on(B,A,C,D). % 42.68/42.78 ** KEPT (pick-wt=19): 84 [] hAPP(c_Map_Omap__add(A,B,C,D),E)=hAPP(B,E)| -hBOOL(c_in(E,c_Map_Odom(B,C,D),C)). % 42.68/42.78 ** KEPT (pick-wt=20): 85 [] hAPP(A,B)=hAPP(C,B)| -hBOOL(c_in(B,c_Map_Odom(A,D,E),D))| -c_Map_Omap__le(A,C,D,E). % 42.68/42.78 ** KEPT (pick-wt=22): 87 [copy,86,flip.2] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))|hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__asm__1(A,C,D))=D| -hBOOL(hAPP(A,B)). % 42.68/42.78 ** KEPT (pick-wt=22): 89 [copy,88,flip.2] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))|hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__1(A,C,D))=D| -hBOOL(hAPP(A,B)). % 42.68/42.78 ** KEPT (pick-wt=22): 90 [] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))| -hBOOL(hAPP(A,hAPP(C,v_sko__Option__Xoption__Xsplit__1(A,C,D))))|D=c_Option_Ooption_ONone(t_b). % 42.68/42.78 ** KEPT (pick-wt=34): 91 [] hAPP(A,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(B,A,C,D,E))!=hAPP(C,c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(B,A,C,D,E))|B=c_Option_Ooption_ONone(D)|c_Option_Ooption_Ooption__case(F,A,B,E,D)=c_Option_Ooption_Ooption__case(G,C,B,E,D). % 42.68/42.78 ** KEPT (pick-wt=22): 92 [] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))| -hBOOL(hAPP(A,hAPP(C,v_sko__Option__Xoption__Xsplit__asm__1(A,C,D))))|D=c_Option_Ooption_ONone(t_b). % 42.68/42.78 ** KEPT (pick-wt=21): 93 [] 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_OTryCatch(D,B,E,F,tc_List_Olist(tc_String_Ochar)),G). % 42.68/42.78 ** KEPT (pick-wt=9): 94 [] c_Decl_Ois__class(A,B,C)| -c_Decl_Ois__type(A,c_Type_Oty_OClass(B),C). % 42.68/42.78 ** KEPT (pick-wt=9): 95 [] c_Decl_Ois__type(A,c_Type_Oty_OClass(B),C)| -c_Decl_Ois__class(A,B,C). % 42.68/42.78 ** KEPT (pick-wt=28): 96 [] c_Map_Omap__comp(A,B,C,D,E,F)!=c_Option_Ooption_ONone(E)|hAPP(A,c_Map_Osko__Map__Xmap__comp__None__iff__1__1(C,A,B,F,D,E))=c_Option_Ooption_ONone(E)|hAPP(B,C)=c_Option_Ooption_ONone(D). % 42.68/42.78 ** KEPT (pick-wt=16): 97 [] -hBOOL(c_in(A,B,C))|hBOOL(c_in(hAPP(D,A),c_Set_Oimage(D,B,C,E),E)). % 42.68/42.78 Following clause subsumed by 97 during input processing: 0 [] -hBOOL(c_in(A,B,C))|hBOOL(c_in(hAPP(D,A),c_Set_Oimage(D,B,C,E),E)). % 42.68/42.78 Following clause subsumed by 97 during input processing: 0 [] hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,C,D,E),E))| -hBOOL(c_in(B,C,D)). % 42.68/42.78 Following clause subsumed by 97 during input processing: 0 [] hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,C,D,E),E))| -hBOOL(c_in(B,C,D)). % 42.68/42.78 ** KEPT (pick-wt=28): 98 [] c_Map_Omap__le(c_Map_Omap__add(A,B,C,D),E,C,D)| -c_Map_Omap__le(A,c_Map_Omap__add(A,B,C,D),C,D)| -c_Map_Omap__le(B,E,C,D)| -c_Map_Omap__le(A,E,C,D). % 42.68/42.78 ** KEPT (pick-wt=46): 99 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OTryCatch(D,E,F,G,tc_List_Olist(tc_String_Ochar)),H)| -c_TypeRel_Owiden(A,I,H,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_Fun_Ofun__upd(C,F,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(E)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),G,H)| -c_Progress_OWTrt_H(A,B,C,D,I). % 42.68/42.78 ** KEPT (pick-wt=42): 100 [] c_WellType_OWT(A,B,c_Expr_Oexp_OTryCatch(C,D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -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_WellType_OWT(A,c_Fun_Ofun__upd(B,E,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(D)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),F,G)| -c_WellType_OWT(A,B,C,G). % 42.68/42.78 ** KEPT (pick-wt=46): 101 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OTryCatch(D,E,F,G,tc_List_Olist(tc_String_Ochar)),H)| -c_TypeRel_Owiden(A,I,H,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_Fun_Ofun__upd(C,F,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(E)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),G,H)| -c_WellTypeRT_OWTrt(A,B,C,D,I). % 42.68/42.78 ** KEPT (pick-wt=27): 102 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|c_Map_Oran(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),E,C)=c_Set_Oinsert(D,c_Map_Oran(A,E,C),C). % 42.68/42.78 ** KEPT (pick-wt=60): 104 [copy,103,flip.1] hAPP(c_Fun_Ocomp(c_Fun_Othe__inv__into(A,B,C,D),c_Fun_Othe__inv__into(c_Set_Oimage(B,A,C,D),E,D,F),D,C,F),G)=hAPP(c_Fun_Othe__inv__into(A,c_Fun_Ocomp(E,B,D,F,C),C,F),G)| -hBOOL(c_in(G,c_Set_Oimage(E,c_Set_Oimage(B,A,C,D),D,F),F))| -c_Fun_Oinj__on(B,A,C,D)| -c_Fun_Oinj__on(E,c_Set_Oimage(B,A,C,D),D,F). % 42.68/42.78 ** KEPT (pick-wt=60): 106 [copy,105,flip.1] hAPP(c_Fun_Ocomp(c_Hilbert__Choice_Oinv__into(A,B,C,D),c_Hilbert__Choice_Oinv__into(c_Set_Oimage(B,A,C,D),E,D,F),D,C,F),G)=hAPP(c_Hilbert__Choice_Oinv__into(A,c_Fun_Ocomp(E,B,D,F,C),C,F),G)| -hBOOL(c_in(G,c_Set_Oimage(E,c_Set_Oimage(B,A,C,D),D,F),F))| -c_Fun_Oinj__on(B,A,C,D)| -c_Fun_Oinj__on(E,c_Set_Oimage(B,A,C,D),D,F). % 42.68/42.78 ** KEPT (pick-wt=21): 107 [] c_Set_Oimage(c_COMBK(A,B,C),D,C,B)=c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),B)| -hBOOL(c_in(E,D,C)). % 42.68/42.78 ** KEPT (pick-wt=30): 108 [] c_Map_Omap__comp(A,B,C,D,E,F)!=c_Option_Ooption_ONone(E)|hAPP(B,C)=hAPP(c_Option_Ooption_OSome(D),c_Map_Osko__Map__Xmap__comp__None__iff__1__1(C,A,B,F,D,E))|hAPP(B,C)=c_Option_Ooption_ONone(D). % 42.68/42.78 ** KEPT (pick-wt=27): 109 [] -class_OrderedGroup_Ocomm__monoid__mult(A)| -c_Fun_Oinj__on(B,C,D,E)|c_Finite__Set_Osetprod(F,c_Set_Oimage(B,C,D,E),E,A)=c_Finite__Set_Osetprod(c_Fun_Ocomp(F,B,E,A,D),C,D,A). % 42.68/42.78 Following clause subsumed by 109 during input processing: 0 [] -class_OrderedGroup_Ocomm__monoid__mult(A)|c_Finite__Set_Osetprod(B,c_Set_Oimage(C,D,E,F),F,A)=c_Finite__Set_Osetprod(c_Fun_Ocomp(B,C,F,A,E),D,E,A)| -c_Fun_Oinj__on(C,D,E,F). % 42.68/42.78 ** KEPT (pick-wt=27): 110 [] -class_OrderedGroup_Ocomm__monoid__add(A)|c_Finite__Set_Osetsum(B,c_Set_Oimage(C,D,E,F),F,A)=c_Finite__Set_Osetsum(c_Fun_Ocomp(B,C,F,A,E),D,E,A)| -c_Fun_Oinj__on(C,D,E,F). % 42.68/42.78 ** KEPT (pick-wt=29): 111 [] c_Fun_Oinj__on(A,c_Set_Oimage(B,C,D,D),D,E)| -c_Fun_Oinj__on(A,C,D,E)| -c_Fun_Oinj__on(B,C,D,D)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(C,B,A,D,E),C,D)). % 42.68/42.78 ** KEPT (pick-wt=29): 112 [] c_Fun_Oinj__on(A,B,C,D)| -c_Fun_Oinj__on(A,c_Set_Oimage(E,B,C,C),C,D)| -c_Fun_Oinj__on(E,B,C,C)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__1(B,E,A,C,D),B,C)). % 42.68/42.78 ** KEPT (pick-wt=29): 113 [] c_Fun_Oinj__on(A,c_Set_Oimage(B,C,D,D),D,E)| -c_Fun_Oinj__on(A,C,D,E)| -c_Fun_Oinj__on(B,C,D,D)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(C,B,A,D,E),C,D)). % 42.68/42.78 ** KEPT (pick-wt=29): 114 [] c_Fun_Oinj__on(A,B,C,D)| -c_Fun_Oinj__on(A,c_Set_Oimage(E,B,C,C),C,D)| -c_Fun_Oinj__on(E,B,C,C)|hBOOL(c_in(c_ATP__Linkup_Osko__Fun__Xinj__on__image__iff__1__2(B,E,A,C,D),B,C)). % 42.68/42.78 ** KEPT (pick-wt=25): 115 [] hAPP(A,hAPP(c_Fun_Othe__inv__into(B,A,C,D),E))=E| -hBOOL(c_in(E,c_Set_Oimage(A,B,C,D),D))| -c_Fun_Oinj__on(A,B,C,D). % 42.68/42.78 Following clause subsumed by 97 during input processing: 0 [] hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,C,D,E),E))| -hBOOL(c_in(B,C,D))| -c_Fun_Oinj__on(A,c_Orderings_Otop__class_Otop(tc_fun(D,tc_bool)),D,E). % 42.68/42.78 ** KEPT (pick-wt=24): 116 [] hBOOL(c_in(A,B,C))| -hBOOL(c_in(hAPP(D,A),c_Set_Oimage(D,B,C,E),E))| -c_Fun_Oinj__on(D,c_Orderings_Otop__class_Otop(tc_fun(C,tc_bool)),C,E). % 42.68/42.78 ** KEPT (pick-wt=22): 117 [] c_Fun_Oinj__on(c_Map_Omap__add(A,B,C,D),c_Map_Odom(B,C,D),C,tc_Option_Ooption(D))| -c_Fun_Oinj__on(B,c_Map_Odom(B,C,D),C,tc_Option_Ooption(D)). % 42.68/42.78 ** KEPT (pick-wt=22): 118 [] c_Fun_Oinj__on(A,c_Map_Odom(A,B,C),B,tc_Option_Ooption(C))| -c_Fun_Oinj__on(c_Map_Omap__add(D,A,B,C),c_Map_Odom(A,B,C),B,tc_Option_Ooption(C)). % 42.68/42.78 ** KEPT (pick-wt=16): 119 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|c_Map_Omap__comp(D,A,B,C,E,F)=c_Option_Ooption_ONone(E). % 42.68/42.78 Following clause subsumed by 119 during input processing: 0 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|c_Map_Omap__comp(D,A,B,C,E,F)=c_Option_Ooption_ONone(E). % 42.68/42.78 ** KEPT (pick-wt=26): 120 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),C)| -c_Conform_Olconf(D,E,A,F,G)|c_Conform_Oconf(D,E,C,c_Conform_Osko__Conform__Xlconf__def__1__1(F,D,B,E,C,G),G). % 42.68/42.78 ** KEPT (pick-wt=6): 122 [copy,121,flip.1] c_List_Olist_OCons(A,B,C)!=B. % 42.68/42.78 Following clause subsumed by 122 during input processing: 0 [] c_List_Olist_OCons(A,B,C)!=B. % 42.68/42.78 ** KEPT (pick-wt=22): 123 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|hAPP(D,B)!=c_Option_Ooption_ONone(C)|hAPP(c_Map_Omap__add(A,D,E,C),B)=c_Option_Ooption_ONone(C). % 42.68/42.78 ** KEPT (pick-wt=25): 124 [] c_Fun_Oinj__on(A,B,C,D)| -c_Fun_Oinj__on(c_Fun_Oswap(E,F,A,C,D),B,C,D)| -hBOOL(c_in(F,B,C))| -hBOOL(c_in(E,B,C)). % 42.68/42.78 ** KEPT (pick-wt=25): 125 [] c_Fun_Oinj__on(c_Fun_Oswap(A,B,C,D,E),F,D,E)| -c_Fun_Oinj__on(C,F,D,E)| -hBOOL(c_in(B,F,D))| -hBOOL(c_in(A,F,D)). % 42.68/42.78 Following clause subsumed by 125 during input processing: 0 [] c_Fun_Oinj__on(c_Fun_Oswap(A,B,C,D,E),F,D,E)| -hBOOL(c_in(B,F,D))| -hBOOL(c_in(A,F,D))| -c_Fun_Oinj__on(C,F,D,E). % 42.68/42.78 ** KEPT (pick-wt=24): 126 [] c_Fun_Oinj__on(c_Fun_Ocomp(A,B,C,D,E),F,E,D)| -c_Fun_Oinj__on(A,c_Set_Oimage(B,F,E,C),C,D)| -c_Fun_Oinj__on(B,F,E,C). % 42.68/42.78 ** KEPT (pick-wt=11): 127 [] c_Set_Oinsert(A,B,C)=B| -hBOOL(c_in(A,B,C)). % 42.68/42.78 ** KEPT (pick-wt=8): 128 [] A=c_Option_Ooption_ONone(B)| -hBOOL(c_Option_Ois__none(A,B)). % 42.68/42.78 ** KEPT (pick-wt=22): 129 [] c_Set_Oinsert(A,B,C)!=c_Set_Oinsert(A,D,C)|hBOOL(c_in(A,D,C))|hBOOL(c_in(A,B,C))|B=D. % 42.68/42.78 ** KEPT (pick-wt=21): 130 [] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,C,D,E)| -hBOOL(c_in(B,C,D)). % 42.68/42.78 ** KEPT (pick-wt=11): 131 [] hBOOL(hAPP(c_Set_Oinsert(A,B,C),D))| -hBOOL(hAPP(B,D)). % 42.68/42.78 ** KEPT (pick-wt=15): 132 [] c_Conform_Oconf(A,B,C,D,E)| -c_Conform_Oconf(A,F,C,D,E)| -c_Objects_Ohext(F,B). % 42.68/42.78 ** KEPT (pick-wt=9): 133 [] c_Objects_Ohext(A,B)| -c_Objects_Ohext(C,B)| -c_Objects_Ohext(A,C). % 42.68/42.78 ** KEPT (pick-wt=15): 134 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_Objects_Ohext(F,B)| -c_WellTypeRT_OWTrt(A,F,C,D,E). % 42.68/42.78 ** KEPT (pick-wt=11): 135 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_WellType_OWT(A,C,D,E). % 42.68/42.78 ** KEPT (pick-wt=16): 136 [] hAPP(c_Map_Omap__add(A,B,C,D),E)!=c_Option_Ooption_ONone(D)|hAPP(B,E)=c_Option_Ooption_ONone(D). % 42.68/42.78 ** KEPT (pick-wt=16): 137 [] hAPP(c_Map_Omap__add(A,B,C,D),E)!=c_Option_Ooption_ONone(D)|hAPP(A,E)=c_Option_Ooption_ONone(D). % 42.68/42.78 ** KEPT (pick-wt=26): 138 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hAPP(E,B)!=c_Option_Ooption_ONone(C)|hAPP(c_Map_Omap__add(A,E,F,C),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.78 ** KEPT (pick-wt=3): 139 [] -c_SmallStep_Oassigned(v_V____,v_ea____). % 42.68/42.78 ** KEPT (pick-wt=25): 140 [] hAPP(A,B)!=hAPP(A,C)| -c_Fun_Oinj__on(A,D,E,F)|B=C| -hBOOL(c_in(C,D,E))| -hBOOL(c_in(B,D,E)). % 42.68/42.78 Following clause subsumed by 140 during input processing: 0 [] hAPP(A,B)!=hAPP(A,C)| -hBOOL(c_in(C,D,E))| -hBOOL(c_in(B,D,E))| -c_Fun_Oinj__on(A,D,E,F)|B=C. % 42.68/42.78 Following clause subsumed by 140 during input processing: 0 [] hAPP(A,B)!=hAPP(A,C)| -hBOOL(c_in(C,D,E))| -hBOOL(c_in(B,D,E))| -c_Fun_Oinj__on(A,D,E,F)|B=C. % 42.68/42.78 Following clause subsumed by 140 during input processing: 0 [] hAPP(A,B)!=hAPP(A,C)| -hBOOL(c_in(C,D,E))| -hBOOL(c_in(B,D,E))|B=C| -c_Fun_Oinj__on(A,D,E,F). % 42.68/42.78 ** KEPT (pick-wt=14): 141 [] -hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,c_Option_Ooption_ONone(t_b),t_a,t_b)))|hBOOL(hAPP(A,B)). % 42.68/42.78 ** KEPT (pick-wt=9): 142 [] hBOOL(hAPP(A,B))| -hBOOL(c_in(B,A,C)). % 42.68/42.78 ** KEPT (pick-wt=9): 143 [] hBOOL(c_in(A,B,C))| -hBOOL(hAPP(B,A)). % 42.68/42.78 ** KEPT (pick-wt=19): 144 [] c_Fun_Oinj__on(A,c_Set_Oimage(B,C,D,E),E,F)| -c_Fun_Oinj__on(c_Fun_Ocomp(A,B,E,F,D),C,D,F). % 42.68/42.78 ** KEPT (pick-wt=20): 145 [] c_Map_Omap__le(c_Map_Omap__upds(A,B,C,D,E),c_Map_Omap__upds(F,B,C,D,E),D,E)| -c_Map_Omap__le(A,F,D,E). % 42.68/42.78 ** KEPT (pick-wt=13): 146 [] c_Fun_Oinj__on(A,B,C,D)| -c_Fun_Oinj__on(A,c_Set_Oinsert(E,B,C),C,D). % 42.68/42.78 ** KEPT (pick-wt=12): 147 [] c_WellTypeRT_OWTrt(A,B,C,D,E)| -c_Progress_OWTrt_H(A,B,C,D,E). % 42.68/42.78 ** KEPT (pick-wt=12): 148 [] c_Progress_OWTrt_H(A,B,C,D,E)| -c_WellTypeRT_OWTrt(A,B,C,D,E). % 42.68/42.78 ** KEPT (pick-wt=14): 149 [] c_Map_Omap__le(A,B,C,D)| -c_Map_Omap__le(c_Map_Omap__add(E,A,C,D),B,C,D). % 42.68/42.78 ** KEPT (pick-wt=15): 150 [] c_Map_Omap__le(A,B,C,D)| -c_Map_Omap__le(E,B,C,D)| -c_Map_Omap__le(A,E,C,D). % 42.68/42.78 ** KEPT (pick-wt=14): 151 [] hBOOL(hAPP(A,B))|C=B| -hBOOL(hAPP(c_Set_Oinsert(C,A,D),B)). % 42.68/42.78 ** KEPT (pick-wt=8): 152 [] c_Type_Oty_OClass(A)!=c_Type_Oty_OClass(B)|A=B. % 42.68/42.78 ** KEPT (pick-wt=17): 153 [] hAPP(c_Fun_Ooverride__on(A,B,C,D,E),F)=hAPP(B,F)| -hBOOL(c_in(F,C,D)). % 42.68/42.78 ** KEPT (pick-wt=16): 154 [] c_WellType_OWT(A,B,C,D)| -c_WellType_OWT(A,B,c_Expr_Oexp_OTryCatch(C,E,F,G,tc_List_Olist(tc_String_Ochar)),D). % 42.68/42.78 ** KEPT (pick-wt=13): 155 [] hAPP(c_Option_Omap(A,B,C),D)!=c_Option_Ooption_ONone(C)|D=c_Option_Ooption_ONone(B). % 42.68/42.78 ** KEPT (pick-wt=20): 156 [] c_Map_Omap__add(A,B,C,D)=c_Map_Omap__add(B,A,C,D)| -c_Map_Omap__le(A,c_Map_Omap__add(A,B,C,D),C,D). % 42.68/42.78 ** KEPT (pick-wt=20): 157 [] c_Map_Omap__add(A,B,C,D)!=c_Map_Omap__add(B,A,C,D)|c_Map_Omap__le(A,c_Map_Omap__add(A,B,C,D),C,D). % 42.68/42.78 ** KEPT (pick-wt=16): 158 [] hBOOL(c_in(A,B,C))|A=D| -hBOOL(c_in(A,c_Set_Oinsert(D,B,C),C)). % 42.68/42.78 ** KEPT (pick-wt=13): 159 [] A=B| -c_Map_Omap__le(B,A,C,D)| -c_Map_Omap__le(A,B,C,D). % 42.68/42.78 ** KEPT (pick-wt=12): 160 [] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OBlock(F,G,H,E). % 42.68/42.78 ** KEPT (pick-wt=26): 161 [] hAPP(c_Map_Omap__add(A,B,C,D),E)!=hAPP(c_Option_Ooption_OSome(D),F)|hAPP(B,E)=c_Option_Ooption_ONone(D)|hAPP(B,E)=hAPP(c_Option_Ooption_OSome(D),F). % 42.68/42.78 ** KEPT (pick-wt=24): 162 [] c_Fun_Oinj__on(c_Fun_Ofun__upd(A,B,C,D,E),F,D,E)|hBOOL(c_in(C,c_Set_Oimage(A,F,D,E),E))| -c_Fun_Oinj__on(A,F,D,E). % 42.68/42.78 ** KEPT (pick-wt=24): 163 [] hAPP(A,B)!=c_Option_Ooption_ONone(C)|hAPP(D,E)!=hAPP(c_Option_Ooption_OSome(F),B)|c_Map_Omap__comp(A,D,E,F,C,G)=c_Option_Ooption_ONone(C). % 42.68/42.78 ** KEPT (pick-wt=12): 164 [] c_List_Olist_OCons(A,B,C)!=c_List_Olist_OCons(D,E,C)|A=D. % 42.68/42.78 ** KEPT (pick-wt=12): 165 [] c_List_Olist_OCons(A,B,C)!=c_List_Olist_OCons(D,E,C)|B=E. % 42.68/42.78 ** KEPT (pick-wt=13): 166 [] hBOOL(c_in(A,c_Set_Oinsert(B,C,D),D))| -hBOOL(c_in(A,C,D)). % 42.68/42.78 Following clause subsumed by 166 during input processing: 0 [] hBOOL(c_in(A,c_Set_Oinsert(B,C,D),D))| -hBOOL(c_in(A,C,D)). % 42.68/42.78 ** KEPT (pick-wt=24): 167 [] c_Fun_Ocomp(A,B,C,D,E)!=c_Fun_Ocomp(F,G,H,D,E)|hAPP(A,hAPP(B,I))=hAPP(F,hAPP(G,I)). % 42.68/42.78 ** KEPT (pick-wt=28): 168 [] hAPP(A,hAPP(B,C))!=hAPP(D,hAPP(E,F))|hAPP(c_Fun_Ocomp(A,B,G,H,I),C)=hAPP(c_Fun_Ocomp(D,E,J,H,K),F). % 42.68/42.78 ** KEPT (pick-wt=14): 169 [] c_Expr_Oexp_OBlock(A,B,C,D)!=c_Expr_Oexp_OBlock(E,F,G,D)|C=G. % 42.68/42.78 ** KEPT (pick-wt=14): 170 [] c_Expr_Oexp_OBlock(A,B,C,D)!=c_Expr_Oexp_OBlock(E,F,G,D)|B=F. % 42.68/42.78 ** KEPT (pick-wt=14): 171 [] c_Expr_Oexp_OBlock(A,B,C,D)!=c_Expr_Oexp_OBlock(E,F,G,D)|A=E. % 42.68/42.78 ** KEPT (pick-wt=12): 172 [] c_Expr_Oexp_OBlock(A,B,C,D)!=c_Expr_Oexp_OTryCatch(E,F,G,H,D). % 42.68/42.78 ** KEPT (pick-wt=16): 173 [] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OTryCatch(F,G,H,I,E)|D=I. % 42.68/42.78 ** KEPT (pick-wt=16): 174 [] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OTryCatch(F,G,H,I,E)|C=H. % 42.68/42.78 ** KEPT (pick-wt=16): 175 [] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OTryCatch(F,G,H,I,E)|B=G. % 42.68/42.78 ** KEPT (pick-wt=16): 176 [] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OTryCatch(F,G,H,I,E)|A=F. % 42.68/42.78 ** KEPT (pick-wt=24): 177 [] c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))!=c_Fun_Ofun__upd(F,B,hAPP(c_Option_Ooption_OSome(C),G),E,tc_Option_Ooption(C))|D=G. % 42.68/42.78 ** KEPT (pick-wt=20): 178 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))=A. % 42.68/42.78 ** KEPT (pick-wt=28): 179 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hAPP(E,F)!=hAPP(c_Option_Ooption_OSome(G),B)|c_Map_Omap__comp(A,E,F,G,C,H)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.78 ** KEPT (pick-wt=38): 180 [] c_Conform_Olconf(A,B,c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(tc_Value_Oval),E),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)),c_Fun_Ofun__upd(F,D,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),G),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),H)| -c_Conform_Oconf(A,B,E,G,H)| -c_Conform_Olconf(A,B,C,F,H). % 42.68/42.78 ** KEPT (pick-wt=27): 181 [] c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OBlock(D,E,F,tc_List_Olist(tc_String_Ochar)),G)| -c_WellTypeRT_OWTrt(A,B,c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),E),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),F,G). % 42.68/42.78 ** KEPT (pick-wt=18): 182 [] -hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,hAPP(c_Option_Ooption_OSome(t_b),D),t_a,t_b)))|hBOOL(hAPP(A,hAPP(C,D))). % 42.68/42.78 Following clause subsumed by 182 during input processing: 0 [] -hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,hAPP(c_Option_Ooption_OSome(t_b),D),t_a,t_b)))|hBOOL(hAPP(A,hAPP(C,D))). % 42.68/42.78 ** KEPT (pick-wt=7): 183 [] -hBOOL(c_Option_Ois__none(hAPP(c_Option_Ooption_OSome(A),B),A)). % 42.68/42.78 ** KEPT (pick-wt=35): 184 [] c_WellType_OWT(A,B,c_Expr_Oexp_OBlock(C,D,E,tc_List_Olist(tc_String_Ochar)),F)| -c_WellType_OWT(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),D),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),E,F)| -c_Decl_Ois__type(A,D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.68/42.78 ** KEPT (pick-wt=12): 185 [] hAPP(c_Option_Ooption_OSome(A),B)!=hAPP(c_Option_Ooption_OSome(A),C)|B=C. % 42.68/42.78 ** KEPT (pick-wt=7): 186 [] hAPP(c_Option_Ooption_OSome(A),B)!=c_Option_Ooption_ONone(A). % 42.68/42.78 Following clause subsumed by 186 during input processing: 0 [] hAPP(c_Option_Ooption_OSome(A),B)!=c_Option_Ooption_ONone(A). % 42.68/42.78 ** KEPT (pick-wt=22): 187 [] c_Map_Omap__le(c_Fun_Ofun__upd(A,B,C,D,tc_Option_Ooption(E)),c_Fun_Ofun__upd(F,B,C,D,tc_Option_Ooption(E)),D,E)| -c_Map_Omap__le(A,F,D,E). % 42.68/42.78 ** KEPT (pick-wt=30): 188 [] c_Progress_OWTrt_H(A,B,C,c_Expr_Oexp_OBlock(D,E,F,tc_List_Olist(tc_String_Ochar)),G)|c_SmallStep_Oassigned(D,F)| -c_Progress_OWTrt_H(A,B,c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),E),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),F,G). % 42.68/42.79 ** KEPT (pick-wt=26): 189 [] c_Map_Omap__le(c_Fun_Ofun__upd(A,B,c_Option_Ooption_ONone(C),D,tc_Option_Ooption(C)),c_Fun_Ofun__upd(E,B,hAPP(c_Option_Ooption_OSome(C),F),D,tc_Option_Ooption(C)),D,C)| -c_Map_Omap__le(A,E,D,C). % 42.68/42.79 ** KEPT (pick-wt=27): 190 [] c_WellType_OWT(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(D)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),E,F)| -c_WellType_OWT(A,B,c_Expr_Oexp_OTryCatch(G,D,C,E,tc_List_Olist(tc_String_Ochar)),F). % 42.68/42.79 ** KEPT (pick-wt=30): 191 [] hAPP(A,c_Conform_Osko__Conform__Xlconf__def__1__2(A,B,C,D,E))!=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),F)|c_Conform_Olconf(B,C,D,A,E)| -c_Conform_Oconf(B,C,c_Conform_Osko__Conform__Xlconf__def__1__3(A,B,C,D,E),F,E). % 42.68/42.79 ** KEPT (pick-wt=28): 192 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|B=E|hAPP(c_Fun_Ofun__upd(A,E,hAPP(c_Option_Ooption_OSome(C),F),G,tc_Option_Ooption(C)),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.79 ** KEPT (pick-wt=28): 193 [] hAPP(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F)!=hAPP(c_Option_Ooption_OSome(C),G)|hAPP(A,F)=hAPP(c_Option_Ooption_OSome(C),G)|D=G. % 42.68/42.79 ** KEPT (pick-wt=28): 194 [] hAPP(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F)!=hAPP(c_Option_Ooption_OSome(C),G)|hAPP(A,F)=hAPP(c_Option_Ooption_OSome(C),G)|F=B. % 42.68/42.79 ** KEPT (pick-wt=17): 195 [] c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))!=c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),E). % 42.68/42.79 ** KEPT (pick-wt=36): 196 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),C)| -c_Conform_Oconf(D,E,F,C,G)| -c_Conform_Olconf(D,E,H,A,G)|c_Conform_Olconf(D,E,c_Fun_Ofun__upd(H,B,hAPP(c_Option_Ooption_OSome(tc_Value_Oval),F),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)),A,G). % 42.68/42.79 ** KEPT (pick-wt=28): 197 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),C)| -c_Conform_Olconf(D,E,A,F,G)|hAPP(F,B)=hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Conform_Osko__Conform__Xlconf__def__1__1(F,D,B,E,C,G)). % 42.68/42.79 ** KEPT (pick-wt=20): 198 [] A=B|hAPP(c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(E),A),F,tc_Option_Ooption(E)),D)!=hAPP(c_Option_Ooption_OSome(E),B). % 42.68/42.79 Following clause subsumed by 186 during input processing: 0 [flip.1] hAPP(c_Option_Ooption_OSome(A),B)!=c_Option_Ooption_ONone(A). % 42.68/42.79 Following clause subsumed by 186 during input processing: 0 [flip.1] hAPP(c_Option_Ooption_OSome(A),B)!=c_Option_Ooption_ONone(A). % 42.68/42.79 ** KEPT (pick-wt=28): 199 [] hAPP(c_Map_Omap__add(A,B,C,D),E)!=hAPP(c_Option_Ooption_OSome(D),F)|hAPP(A,E)=hAPP(c_Option_Ooption_OSome(D),F)|hAPP(B,E)=hAPP(c_Option_Ooption_OSome(D),F). % 42.68/42.79 ** KEPT (pick-wt=29): 200 [] c_WellTypeRT_OWTrt(A,B,c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),c_Type_Oty_OClass(E)),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),F,G)| -c_WellTypeRT_OWTrt(A,B,C,c_Expr_Oexp_OTryCatch(H,E,D,F,tc_List_Olist(tc_String_Ochar)),G). % 42.68/42.79 ** KEPT (pick-wt=15): 201 [] c_Conform_Olconf(A,B,C,D,E)| -c_Objects_Ohext(F,B)| -c_Conform_Olconf(A,F,C,D,E). % 42.68/42.79 ** KEPT (pick-wt=19): 202 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|c_Map_Omap__comp(E,A,B,C,F,G)=hAPP(E,D). % 42.68/42.79 ** KEPT (pick-wt=14): 203 [] -hBOOL(hAPP(A,c_ATP__Linkup_Osko__Option__Xospec__1__1(hAPP(c_Option_Ooption_OSome(B),C),A,B)))|hBOOL(hAPP(A,C)). % 42.68/42.79 ** KEPT (pick-wt=20): 204 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hAPP(c_Map_Omap__add(E,A,F,C),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.79 Following clause subsumed by 204 during input processing: 0 [] hAPP(A,B)!=hAPP(c_Option_Ooption_OSome(C),D)|hAPP(c_Map_Omap__add(E,A,F,C),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.79 ** KEPT (pick-wt=13): 205 [] c_Fun_Ofun__upd(A,B,C,D,E)!=A|hAPP(A,B)=C. % 42.68/42.79 ** KEPT (pick-wt=22): 206 [] -c_Conform_Olconf(v_P,v_h_Ha____,v_l_Ha____,c_Fun_Ofun__upd(v_E____,v_V____,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),v_T____),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.68/42.79 ** KEPT (pick-wt=6): 207 [] class_Lattices_Oboolean__algebra(tc_fun(A,B))| -class_Lattices_Oboolean__algebra(B). % 42.68/42.79 ** KEPT (pick-wt=6): 208 [] class_Orderings_Otop(tc_fun(A,B))| -class_Orderings_Otop(B). % 42.68/42.79 ** KEPT (pick-wt=6): 209 [] class_Orderings_Obot(tc_fun(A,B))| -class_Orderings_Obot(B). % 42.68/42.79 ** KEPT (pick-wt=6): 210 [] class_HOL_Ouminus(tc_fun(A,B))| -class_HOL_Ouminus(B). % 42.68/42.79 ** KEPT (pick-wt=6): 211 [] class_HOL_Ominus(tc_fun(A,B))| -class_HOL_Ominus(B). % 42.68/42.79 ** KEPT (pick-wt=8): 212 [] A=B| -hBOOL(c_fe_qual(A,B,C)). % 42.68/42.79 Following clause subsumed by 64 during input processing: 0 [copy,50,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))!=c_Set_Oinsert(B,C,A). % 42.68/42.79 Following clause subsumed by 50 during input processing: 0 [copy,64,flip.1] c_Set_Oinsert(A,B,C)!=c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)). % 42.68/42.79 65 back subsumes 44. % 42.68/42.79 Following clause subsumed by 172 during input processing: 0 [copy,160,flip.1] c_Expr_Oexp_OBlock(A,B,C,D)!=c_Expr_Oexp_OTryCatch(E,F,G,H,D). % 42.68/42.79 Following clause subsumed by 160 during input processing: 0 [copy,172,flip.1] c_Expr_Oexp_OTryCatch(A,B,C,D,E)!=c_Expr_Oexp_OBlock(F,G,H,E). % 42.68/42.79 ** KEPT (pick-wt=17): 234 [copy,195,flip.1] c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B)!=c_Fun_Ofun__upd(C,D,hAPP(c_Option_Ooption_OSome(A),E),B,tc_Option_Ooption(A)). % 42.68/42.79 Following clause subsumed by 195 during input processing: 0 [copy,234,flip.1] c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))!=c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),E). % 42.68/42.79 % 42.68/42.79 ------------> process sos: % 42.68/42.79 ** KEPT (pick-wt=3): 236 [] A=A. % 42.68/42.79 ** KEPT (pick-wt=27): 237 [] c_Map_Odom(c_Fun_Ofun__upd(A,B,c_Option_Ooption_ONone(C),D,tc_Option_Ooption(C)),D,C)=c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=34): 239 [copy,238,flip.1] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(C,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),C,F,D,tc_Option_Ooption(E))=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,D,E),C,F,D,tc_Option_Ooption(E)). % 42.68/42.79 ---> New Demodulator: 240 [new_demod,239] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(C,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),D,E),C,F,D,tc_Option_Ooption(E))=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,D,E),C,F,D,tc_Option_Ooption(E)). % 42.68/42.79 ** KEPT (pick-wt=24): 242 [copy,241,flip.1] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,C,tc_fun(D,tc_bool)),D)=c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,D),C,tc_fun(D,tc_bool))|hBOOL(c_in(A,C,D)). % 42.68/42.79 ** KEPT (pick-wt=13): 244 [copy,243,flip.1] c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool))=c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),tc_fun(A,tc_bool)). % 42.68/42.79 ---> New Demodulator: 245 [new_demod,244] c_Orderings_Otop__class_Otop(tc_fun(A,tc_bool))=c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),tc_fun(A,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=18): 247 [copy,246,demod,245] c_HOL_Ominus__class_Ominus(A,c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 42.68/42.79 ---> New Demodulator: 248 [new_demod,247] c_HOL_Ominus__class_Ominus(A,c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=17): 250 [copy,249,demod,245] c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),tc_fun(A,tc_bool)),tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 42.68/42.79 ---> New Demodulator: 251 [new_demod,250] c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),tc_fun(A,tc_bool)),tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=14): 252 [] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 42.68/42.79 ---> New Demodulator: 253 [new_demod,252] c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=19): 255 [copy,254,demod,245] c_HOL_Ouminus__class_Ouminus(A,tc_fun(B,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool)),A,tc_fun(B,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=11): 256 [] c_HOL_Ominus__class_Ominus(A,A,tc_fun(B,tc_bool))=c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=11): 257 [] c_HOL_Ominus__class_Ominus(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 42.68/42.79 ---> New Demodulator: 258 [new_demod,257] c_HOL_Ominus__class_Ominus(A,c_Orderings_Obot__class_Obot(tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 42.68/42.79 ** KEPT (pick-wt=27): 259 [] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=27): 260 [] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(D,tc_bool)),D),tc_fun(D,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=14): 261 [] hBOOL(c_in(A,c_HOL_Ouminus__class_Ouminus(B,tc_fun(C,tc_bool)),C))|hBOOL(c_in(A,B,C)). % 42.68/42.79 ** KEPT (pick-wt=18): 262 [] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)). % 42.68/42.79 ---> New Demodulator: 263 [new_demod,262] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=20): 264 [] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=c_Set_Oinsert(A,B,C). % 42.68/42.79 ---> New Demodulator: 265 [new_demod,264] c_Set_Oinsert(A,c_HOL_Ominus__class_Ominus(B,c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool)),C)=c_Set_Oinsert(A,B,C). % 42.68/42.79 ** KEPT (pick-wt=22): 266 [] c_HOL_Ominus__class_Ominus(c_Set_Oinsert(A,B,C),c_Set_Oinsert(A,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C),tc_fun(C,tc_bool))=B|hBOOL(c_in(A,B,C)). % 42.68/42.79 ** KEPT (pick-wt=11): 267 [] c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(A,tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 42.68/42.79 ---> New Demodulator: 268 [new_demod,267] c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(A,tc_fun(B,tc_bool)),tc_fun(B,tc_bool))=A. % 42.68/42.79 ** KEPT (pick-wt=40): 269 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(E,tc_bool)),E),tc_fun(E,tc_bool)),E,C)=c_Map_Orestrict__map(A,c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(E,tc_bool)),E),tc_fun(E,tc_bool)),E,C). % 42.68/42.79 ---> New Demodulator: 270 [new_demod,269] c_Map_Orestrict__map(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(E,tc_bool)),E),tc_fun(E,tc_bool)),E,C)=c_Map_Orestrict__map(A,c_HOL_Ouminus__class_Ouminus(c_Set_Oinsert(B,c_Orderings_Obot__class_Obot(tc_fun(E,tc_bool)),E),tc_fun(E,tc_bool)),E,C). % 42.68/42.79 ** KEPT (pick-wt=11): 271 [] c_Fun_Ooverride__on(A,B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,D)=A. % 42.68/42.79 ---> New Demodulator: 272 [new_demod,271] c_Fun_Ooverride__on(A,B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,D)=A. % 42.68/42.79 ** KEPT (pick-wt=13): 273 [] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Set_Oimage(B,c_Orderings_Obot__class_Obot(tc_fun(C,tc_bool)),C,A). % 42.68/42.79 ** KEPT (pick-wt=9): 275 [copy,274,flip.1] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Option_Oset(c_Option_Ooption_ONone(A),A). % 42.68/42.79 ---> New Demodulator: 276 [new_demod,275] c_Orderings_Obot__class_Obot(tc_fun(A,tc_bool))=c_Option_Oset(c_Option_Ooption_ONone(A),A). % 42.68/42.79 ** KEPT (pick-wt=5): 277 [] c_TypeRel_Owiden(A,B,B,C). % 42.68/42.79 ** KEPT (pick-wt=8): 279 [copy,278,demod,276] c_Fun_Oinj__on(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B,C). % 42.68/42.79 ** KEPT (pick-wt=13): 281 [copy,280,demod,276,276] c_Set_Oimage(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B,C)=c_Option_Oset(c_Option_Ooption_ONone(C),C). % 42.68/42.79 ** KEPT (pick-wt=21): 283 [copy,282,demod,276,276] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),C)=c_Set_Oinsert(B,c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),C). % 42.68/42.79 ** KEPT (pick-wt=14): 285 [copy,284,demod,276] c_Map_Odom(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),B,A)=c_Option_Oset(c_Option_Ooption_ONone(B),B). % 42.68/42.79 ** KEPT (pick-wt=12): 287 [copy,286,demod,245,276] hBOOL(c_in(A,c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(B),B),tc_fun(B,tc_bool)),B)). % 42.68/42.79 ** KEPT (pick-wt=15): 288 [] hAPP(c_Map_Orestrict__map(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),t_a),B,t_a,A),v_x)=c_Option_Ooption_ONone(A). % 42.68/42.79 ---> New Demodulator: 289 [new_demod,288] hAPP(c_Map_Orestrict__map(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),t_a),B,t_a,A),v_x)=c_Option_Ooption_ONone(A). % 42.68/42.79 ** KEPT (pick-wt=11): 291 [copy,290,demod,245,276] hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(A),A),tc_fun(A,tc_bool)),B)). % 42.68/42.79 ** KEPT (pick-wt=14): 293 [copy,292,demod,276,276] hAPP(c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),v_x)=c_in(v_x,c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),t_a). % 42.68/42.79 ---> New Demodulator: 294 [new_demod,293] hAPP(c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),v_x)=c_in(v_x,c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),t_a). % 42.68/42.79 ** KEPT (pick-wt=14): 296 [copy,295,demod,276] c_Map_Oran(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),B,A)=c_Option_Oset(c_Option_Ooption_ONone(A),A). % 42.68/42.79 ---> New Demodulator: 297 [new_demod,296] c_Map_Oran(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),B,A)=c_Option_Oset(c_Option_Ooption_ONone(A),A). % 42.68/42.79 ** KEPT (pick-wt=14): 298 [] hAPP(c_Fun_Ocomp(A,B,C,D,t_a),v_x)=hAPP(A,hAPP(B,v_x)). % 42.68/42.79 ---> New Demodulator: 299 [new_demod,298] hAPP(c_Fun_Ocomp(A,B,C,D,t_a),v_x)=hAPP(A,hAPP(B,v_x)). % 42.68/42.79 ** KEPT (pick-wt=14): 301 [copy,300,demod,276] c_Option_Oset(hAPP(c_Option_Ooption_OSome(A),B),A)=c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(A),A),A). % 42.68/42.79 ---> New Demodulator: 302 [new_demod,301] c_Option_Oset(hAPP(c_Option_Ooption_OSome(A),B),A)=c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(A),A),A). % 42.68/42.79 ** KEPT (pick-wt=20): 304 [copy,303,demod,245,276] c_Map_Odom(c_COMBK(hAPP(c_Option_Ooption_OSome(A),B),tc_Option_Ooption(A),C),C,A)=c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(C),C),tc_fun(C,tc_bool)). % 42.68/42.79 ** KEPT (pick-wt=13): 306 [copy,305,demod,276] hAPP(c_Map_Orestrict__map(A,c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),t_a,B),v_x)=c_Option_Ooption_ONone(B). % 42.68/42.79 ** KEPT (pick-wt=11): 308 [copy,307,demod,276] hBOOL(c_in(A,c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B),B)). % 42.68/42.79 Following clause subsumed by 308 during input processing: 0 [demod,302] hBOOL(c_in(A,c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B),B)). % 42.68/42.79 ** KEPT (pick-wt=18): 310 [copy,309,demod,245,276] hBOOL(c_in(hAPP(A,B),c_Set_Oimage(A,c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(C),C),tc_fun(C,tc_bool)),C,D),D)). % 42.68/42.79 ** KEPT (pick-wt=13): 311 [] c_List_Oset(c_List_Olist_OCons(A,B,C),C)=c_Set_Oinsert(A,c_List_Oset(B,C),C). % 42.68/42.79 ---> New Demodulator: 312 [new_demod,311] c_List_Oset(c_List_Olist_OCons(A,B,C),C)=c_Set_Oinsert(A,c_List_Oset(B,C),C). % 42.68/42.79 ** KEPT (pick-wt=15): 313 [] hAPP(c_Map_Orestrict__map(A,B,C,D),E)=c_Option_Ooption_ONone(D)|hBOOL(c_in(E,B,C)). % 42.68/42.79 ** KEPT (pick-wt=14): 314 [] hBOOL(c_in(A,c_Map_Odom(B,C,D),C))|hAPP(B,A)=c_Option_Ooption_ONone(D). % 42.68/42.79 ** KEPT (pick-wt=22): 315 [] c_Map_Orestrict__map(c_Fun_Ofun__upd(A,B,C,D,tc_Option_Ooption(E)),F,D,E)=c_Map_Orestrict__map(A,F,D,E)|hBOOL(c_in(B,F,D)). % 42.68/42.79 Following clause subsumed by 281 during input processing: 0 [demod,276,276] c_Set_Oimage(c_COMBK(A,B,C),c_Option_Oset(c_Option_Ooption_ONone(C),C),C,B)=c_Option_Oset(c_Option_Ooption_ONone(B),B). % 42.68/42.79 ** KEPT (pick-wt=22): 316 [] c_Map_Orestrict__map(A,c_Set_Oinsert(B,C,D),D,E)=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,C,D,E),B,hAPP(A,B),D,tc_Option_Ooption(E)). % 42.68/42.79 ** KEPT (pick-wt=19): 317 [] hAPP(c_Map_Omap__add(A,B,C,D),E)=hAPP(B,E)|hBOOL(c_in(E,c_Map_Odom(A,C,D),C)). % 42.68/42.79 ** KEPT (pick-wt=19): 318 [] hAPP(c_Map_Omap__add(A,B,C,D),E)=hAPP(A,E)|hBOOL(c_in(E,c_Map_Odom(B,C,D),C)). % 42.68/42.79 ** KEPT (pick-wt=10): 320 [copy,319,demod,299] hAPP(c_COMBK(A,B,C),hAPP(D,v_x))=A. % 42.68/42.79 ---> New Demodulator: 321 [new_demod,320] hAPP(c_COMBK(A,B,C),hAPP(D,v_x))=A. % 42.68/42.79 ** KEPT (pick-wt=19): 322 [] hAPP(c_Map_Omap__upds(A,B,C,D,E),F)=hAPP(A,F)|hBOOL(c_in(F,c_List_Oset(B,D),D)). % 42.68/42.79 ** KEPT (pick-wt=24): 324 [copy,323,flip.2] c_Option_Ooption_Ooption__case(A,B,C,D,E)=c_Option_Ooption_Ooption__case(A,F,C,D,E)|hAPP(c_Option_Ooption_OSome(E),c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(C,B,F,E,D))=C. % 42.68/42.79 ** KEPT (pick-wt=23): 326 [copy,325,flip.1] c_Fun_Oswap(A,B,c_Fun_Ocomp(C,D,E,F,G),G,F)=c_Fun_Ocomp(C,c_Fun_Oswap(A,B,D,G,E),E,F,G). % 42.68/42.79 ---> New Demodulator: 327 [new_demod,326] c_Fun_Oswap(A,B,c_Fun_Ocomp(C,D,E,F,G),G,F)=c_Fun_Ocomp(C,c_Fun_Oswap(A,B,D,G,E),E,F,G). % 42.68/42.79 ** KEPT (pick-wt=11): 328 [] c_TypeRel_Owiden(v_P,v_Te_H____,v_Te____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))). % 42.68/42.79 ** KEPT (pick-wt=16): 330 [copy,329,demod,299] hAPP(c_Option_Omap(A,B,C),hAPP(c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),t_a),v_x))=c_Option_Ooption_ONone(C). % 42.68/42.79 ** KEPT (pick-wt=38): 331 [] c_Map_Omap__upds(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F,G,E,C)=c_Fun_Ofun__upd(c_Map_Omap__upds(A,F,G,E,C),B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))|hBOOL(c_in(B,c_List_Oset(F,E),E)). % 42.68/42.79 ** KEPT (pick-wt=37): 332 [] c_Map_Omap__add(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F,E,C)=c_Fun_Ofun__upd(c_Map_Omap__add(A,F,E,C),B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C))|hBOOL(c_in(B,c_Map_Odom(F,E,C),E)). % 42.68/42.79 ** KEPT (pick-wt=21): 334 [copy,333,demod,302] hBOOL(c_in(c_ATP__Linkup_Osko__Option__Xospec__1__1(hAPP(c_Option_Ooption_OSome(A),B),C,A),c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(A),A),A),A))|hBOOL(hAPP(C,B)). % 42.68/42.79 ** KEPT (pick-wt=15): 335 [] c_Map_Omap__comp(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,v_x,B,A,t_a)=c_Option_Ooption_ONone(A). % 42.68/42.79 ---> New Demodulator: 336 [new_demod,335] c_Map_Omap__comp(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,v_x,B,A,t_a)=c_Option_Ooption_ONone(A). % 42.68/42.79 ** KEPT (pick-wt=15): 337 [] c_Map_Omap__comp(A,c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),t_a),v_x,B,C,t_a)=c_Option_Ooption_ONone(C). % 42.68/42.79 ** KEPT (pick-wt=18): 338 [] hAPP(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),t_a),B,c_Option_Ooption_ONone(A),t_a,tc_Option_Ooption(A)),v_xa)=c_Option_Ooption_ONone(A). % 42.68/42.79 ---> New Demodulator: 339 [new_demod,338] hAPP(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),t_a),B,c_Option_Ooption_ONone(A),t_a,tc_Option_Ooption(A)),v_xa)=c_Option_Ooption_ONone(A). % 42.68/42.79 ** KEPT (pick-wt=22): 341 [copy,340,flip.2] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))|hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__1(A,C,D))=D|D=c_Option_Ooption_ONone(t_b). % 42.68/42.79 ** KEPT (pick-wt=28): 343 [copy,342,flip.2] c_Option_Ooption_Ooption__case(A,B,C,D,E)=c_Option_Ooption_Ooption__case(F,G,C,D,E)|hAPP(c_Option_Ooption_OSome(E),c_ATP__Linkup_Osko__Option__Xoption__Xcase__cong__1__1(C,B,G,E,D))=C|C=c_Option_Ooption_ONone(E). % 42.68/42.79 ** KEPT (pick-wt=22): 345 [copy,344,flip.2] hBOOL(hAPP(A,c_Option_Ooption_Ooption__case(B,C,D,t_a,t_b)))|hAPP(c_Option_Ooption_OSome(t_b),v_sko__Option__Xoption__Xsplit__asm__1(A,C,D))=D|D=c_Option_Ooption_ONone(t_b). % 42.68/42.79 ** KEPT (pick-wt=22): 346 [] c_Map_Odom(c_Fun_Ofun__upd(A,B,C,D,tc_Option_Ooption(E)),D,E)=c_Set_Oinsert(B,c_Map_Odom(A,D,E),D)|C=c_Option_Ooption_ONone(E). % 42.68/42.79 ** KEPT (pick-wt=23): 347 [] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,C,D),E,c_Option_Ooption_ONone(D),C,tc_Option_Ooption(D))=c_Map_Orestrict__map(A,B,C,D)|hBOOL(c_in(E,B,C)). % 42.68/42.79 ** KEPT (pick-wt=22): 349 [copy,348,demod,276,276] c_Set_Oimage(c_COMBK(A,B,C),D,C,B)=c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B)|D=c_Option_Oset(c_Option_Ooption_ONone(C),C). % 42.68/42.79 ** KEPT (pick-wt=10): 351 [copy,350,flip.1] c_fe_qual(v_x,c_Option_Ooption_ONone(t_a),tc_Option_Ooption(t_a))=c_Option_Ois__none(v_x,t_a). % 42.68/42.79 ---> New Demodulator: 352 [new_demod,351] c_fe_qual(v_x,c_Option_Ooption_ONone(t_a),tc_Option_Ooption(t_a))=c_Option_Ois__none(v_x,t_a). % 42.68/42.79 ** KEPT (pick-wt=26): 354 [copy,353,demod,276] c_Map_Odom(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,hAPP(c_Option_Ooption_OSome(A),D),B,tc_Option_Ooption(A)),B,A)=c_Set_Oinsert(C,c_Option_Oset(c_Option_Ooption_ONone(B),B),B). % 42.68/42.79 ** KEPT (pick-wt=9): 355 [] c_Map_Omap__le(A,c_Map_Omap__add(B,A,C,D),C,D). % 42.68/42.79 ** KEPT (pick-wt=10): 356 [] hAPP(c_Option_Omap(A,B,C),c_Option_Ooption_ONone(B))=c_Option_Ooption_ONone(C). % 42.68/42.79 ** KEPT (pick-wt=3): 357 [] c_Objects_Ohext(A,A). % 42.68/42.79 ** KEPT (pick-wt=29): 358 [] c_Fun_Oswap(A,B,c_Fun_Oswap(B,C,c_Fun_Oswap(A,B,D,E,F),E,F),E,F)=c_Fun_Oswap(A,C,D,E,F)|B=C|A=C. % 42.68/42.79 ** KEPT (pick-wt=9): 359 [] c_Option_Ooption_Ooption__rec(A,B,c_Option_Ooption_ONone(C),D,C)=A. % 42.68/42.79 ---> New Demodulator: 360 [new_demod,359] c_Option_Ooption_Ooption__rec(A,B,c_Option_Ooption_ONone(C),D,C)=A. % 42.68/42.79 ** KEPT (pick-wt=12): 361 [] c_Map_Omap__add(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,B,A)=C. % 42.68/42.79 ---> New Demodulator: 362 [new_demod,361] c_Map_Omap__add(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,B,A)=C. % 42.68/42.79 ** KEPT (pick-wt=12): 363 [] c_Map_Omap__add(A,c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),C),C,B)=A. % 42.68/42.79 ---> New Demodulator: 364 [new_demod,363] c_Map_Omap__add(A,c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),C),C,B)=A. % 42.68/42.79 ** KEPT (pick-wt=8): 365 [] hAPP(c_COMBK(A,B,C),D)=A. % 42.68/42.79 ---> New Demodulator: 366 [new_demod,365] hAPP(c_COMBK(A,B,C),D)=A. % 42.68/42.79 ** KEPT (pick-wt=6): 367 [] hAPP(c_COMBI(A),B)=B. % 42.68/42.79 ---> New Demodulator: 368 [new_demod,367] hAPP(c_COMBI(A),B)=B. % 42.68/42.79 ** KEPT (pick-wt=15): 369 [] c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),D)=c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),D). % 42.68/42.79 ** KEPT (pick-wt=8): 370 [] hBOOL(c_in(A,c_Set_Oinsert(A,B,C),C)). % 42.68/42.79 Following clause subsumed by 370 during input processing: 0 [] hBOOL(c_in(A,c_Set_Oinsert(A,B,C),C)). % 42.68/42.79 Following clause subsumed by 370 during input processing: 0 [] hBOOL(c_in(A,c_Set_Oinsert(A,B,C),C)). % 42.68/42.79 ** KEPT (pick-wt=13): 371 [] c_Fun_Oswap(A,B,C,D,E)=c_Fun_Oswap(B,A,C,D,E). % 42.68/42.79 ** KEPT (pick-wt=13): 372 [] c_Fun_Oswap(A,B,c_Fun_Oswap(A,B,C,D,E),D,E)=C. % 42.68/42.79 ---> New Demodulator: 373 [new_demod,372] c_Fun_Oswap(A,B,c_Fun_Oswap(A,B,C,D,E),D,E)=C. % 42.68/42.79 ** KEPT (pick-wt=8): 374 [] c_Set_Oimage(c_COMBI(A),B,A,A)=B. % 42.68/42.79 ---> New Demodulator: 375 [new_demod,374] c_Set_Oimage(c_COMBI(A),B,A,A)=B. % 42.68/42.79 ** KEPT (pick-wt=17): 376 [] hAPP(c_Fun_Ooverride__on(A,B,C,D,E),F)=hAPP(A,F)|hBOOL(c_in(F,C,D)). % 42.68/42.79 ** KEPT (pick-wt=6): 377 [] c_Fun_Oinj__on(c_COMBI(A),B,A,A). % 42.68/42.79 ** KEPT (pick-wt=12): 378 [] c_Set_Oinsert(A,c_Set_Oinsert(A,B,C),C)=c_Set_Oinsert(A,B,C). % 42.68/42.79 ---> New Demodulator: 379 [new_demod,378] c_Set_Oinsert(A,c_Set_Oinsert(A,B,C),C)=c_Set_Oinsert(A,B,C). % 42.68/42.79 ** KEPT (pick-wt=8): 380 [] c_Fun_Oswap(A,A,B,C,D)=B. % 42.68/42.79 ---> New Demodulator: 381 [new_demod,380] c_Fun_Oswap(A,A,B,C,D)=B. % 42.68/42.79 ** KEPT (pick-wt=5): 382 [] c_Map_Omap__le(A,A,B,C). % 42.68/42.79 ** KEPT (pick-wt=24): 383 [] c_Conform_Olconf(A,B,C,D,E)|hAPP(C,c_Conform_Osko__Conform__Xlconf__def__1__2(D,A,B,C,E))=hAPP(c_Option_Ooption_OSome(tc_Value_Oval),c_Conform_Osko__Conform__Xlconf__def__1__3(D,A,B,C,E)). % 42.68/42.79 ** KEPT (pick-wt=14): 384 [] hAPP(c_Fun_Ocomp(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 42.68/42.79 ---> New Demodulator: 385 [new_demod,384] hAPP(c_Fun_Ocomp(A,B,C,D,E),F)=hAPP(A,hAPP(B,F)). % 42.68/42.79 Following clause subsumed by 236 during input processing: 0 [demod,385] hAPP(A,hAPP(B,C))=hAPP(A,hAPP(B,C)). % 42.68/42.79 ** KEPT (pick-wt=19): 387 [copy,386,flip.1] c_Map_Omap__add(c_Map_Omap__add(A,B,C,D),E,C,D)=c_Map_Omap__add(A,c_Map_Omap__add(B,E,C,D),C,D). % 42.68/42.79 ---> New Demodulator: 388 [new_demod,387] c_Map_Omap__add(c_Map_Omap__add(A,B,C,D),E,C,D)=c_Map_Omap__add(A,c_Map_Omap__add(B,E,C,D),C,D). % 42.68/42.79 ** KEPT (pick-wt=21): 389 [] c_Map_Omap__add(A,c_Map_Omap__upds(B,C,D,E,F),E,F)=c_Map_Omap__upds(c_Map_Omap__add(A,B,E,F),C,D,E,F). % 42.68/42.79 ---> New Demodulator: 390 [new_demod,389] c_Map_Omap__add(A,c_Map_Omap__upds(B,C,D,E,F),E,F)=c_Map_Omap__upds(c_Map_Omap__add(A,B,E,F),C,D,E,F). % 42.68/42.79 ** KEPT (pick-wt=23): 392 [copy,391,flip.1] hAPP(c_Option_Omap(c_Fun_Ocomp(A,B,C,D,E),E,D),F)=hAPP(c_Option_Omap(A,C,D),hAPP(c_Option_Omap(B,E,C),F)). % 42.68/42.79 ---> New Demodulator: 393 [new_demod,392] hAPP(c_Option_Omap(c_Fun_Ocomp(A,B,C,D,E),E,D),F)=hAPP(c_Option_Omap(A,C,D),hAPP(c_Option_Omap(B,E,C),F)). % 42.68/42.79 ** KEPT (pick-wt=12): 394 [] c_Map_Omap__le(c_Fun_Ofun__upd(A,B,c_Option_Ooption_ONone(C),D,tc_Option_Ooption(C)),A,D,C). % 42.68/42.79 ** KEPT (pick-wt=5): 395 [] hBOOL(c_Option_Ois__none(c_Option_Ooption_ONone(A),A)). % 42.68/42.79 ** KEPT (pick-wt=9): 396 [] c_Option_Ooption_Ooption__case(A,B,c_Option_Ooption_ONone(C),D,C)=A. % 42.68/42.79 ---> New Demodulator: 397 [new_demod,396] c_Option_Ooption_Ooption__case(A,B,c_Option_Ooption_ONone(C),D,C)=A. % 42.68/42.79 ** KEPT (pick-wt=10): 398 [] c_Map_Omap__le(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,B,A). % 42.68/42.79 ** KEPT (pick-wt=19): 400 [copy,399,flip.1] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,c_Set_Oinsert(B,C,D),D,E). % 42.68/42.79 ---> New Demodulator: 401 [new_demod,400] c_Set_Oinsert(hAPP(A,B),c_Set_Oimage(A,C,D,E),E)=c_Set_Oimage(A,c_Set_Oinsert(B,C,D),D,E). % 42.68/42.79 ** KEPT (pick-wt=21): 402 [] c_Set_Oimage(c_Fun_Ofun__upd(A,B,C,D,E),F,D,E)=c_Set_Oimage(A,F,D,E)|hBOOL(c_in(B,F,D)). % 42.68/42.79 ** KEPT (pick-wt=23): 404 [copy,403,flip.1] c_Fun_Ocomp(c_Fun_Ocomp(A,B,C,D,E),F,E,D,G)=c_Fun_Ocomp(A,c_Fun_Ocomp(B,F,E,C,G),C,D,G). % 42.68/42.79 ---> New Demodulator: 405 [new_demod,404] c_Fun_Ocomp(c_Fun_Ocomp(A,B,C,D,E),F,E,D,G)=c_Fun_Ocomp(A,c_Fun_Ocomp(B,F,E,C,G),C,D,G). % 42.68/42.79 ** KEPT (pick-wt=7): 406 [] hBOOL(hAPP(c_Set_Oinsert(A,B,C),A)). % 42.68/42.79 ** KEPT (pick-wt=20): 407 [] c_Set_Oimage(c_Fun_Ocomp(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 42.68/42.79 ---> New Demodulator: 408 [new_demod,407] c_Set_Oimage(c_Fun_Ocomp(A,B,C,D,E),F,E,D)=c_Set_Oimage(A,c_Set_Oimage(B,F,E,C),C,D). % 42.68/42.79 ** KEPT (pick-wt=8): 409 [] c_Option_Othe(hAPP(c_Option_Ooption_OSome(A),B),A)=B. % 42.68/42.79 ---> New Demodulator: 410 [new_demod,409] c_Option_Othe(hAPP(c_Option_Ooption_OSome(A),B),A)=B. % 42.68/42.79 ** KEPT (pick-wt=13): 411 [] c_Option_Ooption_Ooption__rec(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,C)=hAPP(B,D). % 42.68/42.79 ** KEPT (pick-wt=15): 412 [] hAPP(c_Fun_Ofun__upd(A,B,C,D,E),F)=hAPP(A,F)|F=B. % 42.68/42.79 Following clause subsumed by 412 during input processing: 0 [] hAPP(c_Fun_Ofun__upd(A,B,C,D,E),F)=hAPP(A,F)|F=B. % 42.68/42.79 ** KEPT (pick-wt=17): 413 [] hAPP(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.79 ---> New Demodulator: 414 [new_demod,413] hAPP(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),B)=hAPP(c_Option_Ooption_OSome(C),D). % 42.68/42.79 ** KEPT (pick-wt=29): 415 [] c_Map_Omap__add(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)),F,D)=c_Fun_Ofun__upd(c_Map_Omap__add(A,B,F,D),C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)). % 42.68/42.79 ---> New Demodulator: 416 [new_demod,415] c_Map_Omap__add(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)),F,D)=c_Fun_Ofun__upd(c_Map_Omap__add(A,B,F,D),C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)). % 42.68/42.79 ** KEPT (pick-wt=10): 417 [] c_Fun_Ofun__upd(A,B,hAPP(A,B),C,D)=A. % 42.68/42.79 ---> New Demodulator: 418 [new_demod,417] c_Fun_Ofun__upd(A,B,hAPP(A,B),C,D)=A. % 42.68/42.79 ** KEPT (pick-wt=10): 419 [] hAPP(c_Fun_Ofun__upd(A,B,C,D,E),B)=C. % 42.68/42.79 ---> New Demodulator: 420 [new_demod,419] hAPP(c_Fun_Ofun__upd(A,B,C,D,E),B)=C. % 42.68/42.79 Following clause subsumed by 236 during input processing: 0 [demod,418] A=A. % 42.68/42.79 Following clause subsumed by 236 during input processing: 0 [demod,420] C=C. % 42.68/42.80 Following clause subsumed by 236 during input processing: 0 [demod,418] A=A. % 42.68/42.80 ** KEPT (pick-wt=22): 421 [] c_Fun_Oswap(A,B,C,D,E)=c_Fun_Ofun__upd(c_Fun_Ofun__upd(C,A,hAPP(C,B),D,E),B,hAPP(C,A),D,E). % 42.68/42.80 ** KEPT (pick-wt=18): 422 [] c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,B,C,D,E),B,F,D,E)=c_Fun_Ofun__upd(A,B,F,D,E). % 42.68/42.80 ---> New Demodulator: 423 [new_demod,422] c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,B,C,D,E),B,F,D,E)=c_Fun_Ofun__upd(A,B,F,D,E). % 42.68/42.80 ** KEPT (pick-wt=35): 424 [] c_Fun_Ofun__upd(c_Fun_Ooverride__on(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)),G,F,tc_Option_Ooption(D)),C,hAPP(B,C),F,tc_Option_Ooption(D))=c_Fun_Ooverride__on(A,B,c_Set_Oinsert(C,G,F),F,tc_Option_Ooption(D)). % 42.68/42.80 ** KEPT (pick-wt=16): 425 [] c_WellTypeRT_OWTrt(v_P,v_h_Ha____,c_Fun_Ofun__upd(v_E____,v_V____,hAPP(c_Option_Ooption_OSome(tc_Type_Oty),v_T____),tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Type_Oty)),v_e_Ha____,v_Te_H____). % 42.68/42.80 ** KEPT (pick-wt=7): 426 [] c_Fun_Oinj__on(c_Option_Ooption_OSome(A),B,A,tc_Option_Ooption(A)). % 42.68/42.80 ** KEPT (pick-wt=26): 427 [] c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,B,C,D,E),F,G,D,E)=c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,F,G,D,E),B,C,D,E)|B=F. % 42.68/42.80 ** KEPT (pick-wt=13): 428 [] c_Option_Ooption_Ooption__case(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,C)=hAPP(B,D). % 42.68/42.80 ** KEPT (pick-wt=43): 429 [] c_Fun_Ocomp(c_Option_Omap(A,B,C),c_Fun_Ofun__upd(D,E,hAPP(c_Option_Ooption_OSome(B),F),G,tc_Option_Ooption(B)),tc_Option_Ooption(B),tc_Option_Ooption(C),G)=c_Fun_Ofun__upd(c_Fun_Ocomp(c_Option_Omap(A,B,C),D,tc_Option_Ooption(B),tc_Option_Ooption(C),G),E,hAPP(c_Option_Ooption_OSome(C),hAPP(A,F)),G,tc_Option_Ooption(C)). % 42.68/42.80 ** KEPT (pick-wt=8): 431 [copy,430,flip.1] hAPP(c_Option_Ooption_OSome(tc_Value_Oval),v_v____)=hAPP(v_l_Ha____,v_V____). % 42.68/42.80 ---> New Demodulator: 432 [new_demod,431] hAPP(c_Option_Ooption_OSome(tc_Value_Oval),v_v____)=hAPP(v_l_Ha____,v_V____). % 42.68/42.80 ** KEPT (pick-wt=28): 433 [] c_Map_Omap__upds(A,c_List_Olist_OCons(B,C,D),c_List_Olist_OCons(E,F,G),D,G)=c_Map_Omap__upds(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(G),E),D,tc_Option_Ooption(G)),C,F,D,G). % 42.68/42.80 ** KEPT (pick-wt=25): 435 [copy,434,flip.1] c_Fun_Ofun__upd(c_Fun_Ocomp(A,B,C,D,E),F,hAPP(A,G),E,D)=c_Fun_Ocomp(A,c_Fun_Ofun__upd(B,F,G,E,C),C,D,E). % 42.68/42.80 ---> New Demodulator: 436 [new_demod,435] c_Fun_Ofun__upd(c_Fun_Ocomp(A,B,C,D,E),F,hAPP(A,G),E,D)=c_Fun_Ocomp(A,c_Fun_Ofun__upd(B,F,G,E,C),C,D,E). % 42.68/42.80 ** KEPT (pick-wt=11): 437 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OBlock(v_V____,v_T____,v_ea____,tc_List_Olist(tc_String_Ochar)),v_Te____). % 42.68/42.80 Following clause subsumed by 402 during input processing: 0 [] c_Set_Oimage(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F,E,tc_Option_Ooption(C))=c_Set_Oimage(A,F,E,tc_Option_Ooption(C))|hBOOL(c_in(B,F,E)). % 42.68/42.80 ** KEPT (pick-wt=16): 438 [] hAPP(c_Option_Omap(A,B,C),hAPP(c_Option_Ooption_OSome(B),D))=hAPP(c_Option_Ooption_OSome(C),hAPP(A,D)). % 42.68/42.80 Following clause subsumed by 236 during input processing: 0 [demod,368] v_P=v_P. % 42.68/42.80 Following clause subsumed by 437 during input processing: 0 [] c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OBlock(v_V____,v_T____,v_ea____,tc_List_Olist(tc_String_Ochar)),v_Te____). % 42.68/42.80 ** KEPT (pick-wt=25): 439 [] 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)))). % 42.68/42.80 ** KEPT (pick-wt=2): 440 [] class_OrderedGroup_Ocomm__monoid__mult(tc_nat). % 42.68/42.80 ** KEPT (pick-wt=2): 441 [] class_OrderedGroup_Ocomm__monoid__add(tc_nat). % 42.68/42.80 ** KEPT (pick-wt=2): 442 [] class_Orderings_Obot(tc_nat). % 42.68/42.80 ** KEPT (pick-wt=2): 443 [] class_HOL_Ominus(tc_nat). % 42.68/42.80 ** KEPT (pick-wt=2): 444 [] class_Lattices_Oboolean__algebra(tc_bool). % 42.68/42.80 ** KEPT (pick-wt=2): 445 [] class_Orderings_Otop(tc_bool). % 42.68/42.80 ** KEPT (pick-wt=2): 446 [] class_Orderings_Obot(tc_bool). % 42.68/42.80 ** KEPT (pick-wt=2): 447 [] class_HOL_Ouminus(tc_bool). % 42.68/42.80 ** KEPT (pick-wt=2): 448 [] class_HOL_Ominus(tc_bool). % 42.68/42.80 ** KEPT (pick-wt=5): 449 [] hBOOL(c_fe_qual(A,A,B)). % 42.68/42.80 Following clause subsumed by 236 during input processing: 0 [copy,236,flip.1] A=A. % 42.68/42.80 236 back subsumes 232. % 42.68/42.80 236 back subsumes 231. % 42.68/42.80 236 back subsumes 230. % 42.68/42.80 236 back subsumes 221. % 42.68/42.80 ** KEPT (pick-wt=27): 450 [copy,237,flip.1,demod,276] c_HOL_Ominus__class_Ominus(c_Map_Odom(A,B,C),c_Set_Oinsert(D,c_Option_Oset(c_Option_Ooption_ONone(B),B),B),tc_fun(B,tc_bool))=c_Map_Odom(c_Fun_Ofun__upd(A,D,c_Option_Ooption_ONone(C),B,tc_Option_Ooption(C)),B,C). % 42.68/42.80 >>>> Starting back demodulation with 240. % 42.68/42.80 >> back demodulating 3 with 240. % 42.68/42.80 >> back demodulating 1 with 240. % 42.68/42.80 >>>> Starting back demodulation with 245. % 42.68/42.80 >> back demodulating 116 with 245. % 42.68/42.80 >> back demodulating 82 with 245. % 42.68/42.80 >> back demodulating 68 with 245. % 42.68/42.80 >> back demodulating 66 with 245. % 42.68/42.80 >> back demodulating 54 with 245. % 42.68/42.80 >> back demodulating 51 with 245. % 42.68/42.80 >> back demodulating 35 with 245. % 42.68/42.80 >> back demodulating 33 with 245. % 42.68/42.80 >> back demodulating 25 with 245. % 42.68/42.80 >>>> Starting back demodulation with 248. % 42.68/42.80 >>>> Starting back demodulation with 251. % 42.68/42.80 >>>> Starting back demodulation with 253. % 42.68/42.80 ** KEPT (pick-wt=19): 462 [copy,255,flip.1,demod,276] c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(A),A),tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_HOL_Ouminus__class_Ouminus(B,tc_fun(A,tc_bool)). % 42.68/42.80 ** KEPT (pick-wt=11): 463 [copy,256,flip.1,demod,276] c_Option_Oset(c_Option_Ooption_ONone(A),A)=c_HOL_Ominus__class_Ominus(B,B,tc_fun(A,tc_bool)). % 42.68/42.80 >>>> Starting back demodulation with 258. % 42.68/42.80 ** KEPT (pick-wt=27): 464 [copy,259,flip.1,demod,276] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,D,C),tc_fun(C,tc_bool)). % 42.68/42.80 ** KEPT (pick-wt=27): 465 [copy,260,flip.1,demod,276] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_Set_Oinsert(D,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)). % 42.68/42.80 >>>> Starting back demodulation with 263. % 42.68/42.80 >>>> Starting back demodulation with 265. % 42.68/42.80 >> back demodulating 9 with 265. % 42.68/42.80 >>>> Starting back demodulation with 268. % 42.68/42.80 >> back demodulating 250 with 268. % 42.68/42.80 >>>> Starting back demodulation with 270. % 42.68/42.80 >>>> Starting back demodulation with 272. % 42.68/42.80 Following clause subsumed by 281 during input processing: 0 [copy,273,flip.1,demod,276,276] c_Set_Oimage(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B,C)=c_Option_Oset(c_Option_Ooption_ONone(C),C). % 42.68/42.80 >>>> Starting back demodulation with 276. % 42.68/42.80 >> back demodulating 273 with 276. % 42.68/42.80 >> back demodulating 271 with 276. % 42.68/42.80 >> back demodulating 269 with 276. % 42.68/42.80 >> back demodulating 266 with 276. % 42.68/42.80 >> back demodulating 264 with 276. % 42.68/42.80 >> back demodulating 260 with 276. % 42.68/42.80 >> back demodulating 259 with 276. % 42.68/42.80 >> back demodulating 257 with 276. % 42.68/42.80 >> back demodulating 256 with 276. % 42.68/42.80 >> back demodulating 255 with 276. % 42.68/42.80 >> back demodulating 252 with 276. % 42.68/42.80 >> back demodulating 247 with 276. % 42.68/42.80 >> back demodulating 244 with 276. % 42.68/42.80 >> back demodulating 239 with 276. % 42.68/42.80 >> back demodulating 237 with 276. % 42.68/42.80 >> back demodulating 220 with 276. % 42.68/42.80 >> back demodulating 219 with 276. % 42.68/42.80 >> back demodulating 218 with 276. % 42.68/42.80 >> back demodulating 217 with 276. % 42.68/42.80 >> back demodulating 107 with 276. % 42.68/42.80 >> back demodulating 70 with 276. % 42.68/42.80 >> back demodulating 67 with 276. % 42.68/42.80 >> back demodulating 65 with 276. % 42.68/42.80 >> back demodulating 64 with 276. % 42.68/42.80 >> back demodulating 63 with 276. % 42.68/42.80 >> back demodulating 62 with 276. % 42.68/42.80 >> back demodulating 61 with 276. % 42.68/42.80 >> back demodulating 60 with 276. % 42.68/42.80 >> back demodulating 59 with 276. % 42.68/42.80 >> back demodulating 57 with 276. % 42.68/42.80 >> back demodulating 53 with 276. % 42.68/42.80 >> back demodulating 50 with 276. % 42.68/42.80 >> back demodulating 49 with 276. % 42.68/42.80 >> back demodulating 45 with 276. % 42.68/42.80 >> back demodulating 32 with 276. % 42.68/42.80 >> back demodulating 30 with 276. % 42.68/42.80 >> back demodulating 7 with 276. % 42.68/42.80 >> back demodulating 6 with 276. % 42.68/42.80 >> back demodulating 5 with 276. % 42.68/42.80 Following clause subsumed by 467 during input processing: 0 [copy,281,flip.1] c_Option_Oset(c_Option_Ooption_ONone(A),A)=c_Set_Oimage(B,c_Option_Oset(c_Option_Ooption_ONone(C),C),C,A). % 42.68/42.80 Following clause subsumed by 369 during input processing: 0 [copy,283,flip.1] c_Set_Oinsert(A,c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),C)=c_Set_Oinsert(B,c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),C). % 42.68/42.80 ** KEPT (pick-wt=14): 514 [copy,285,flip.1] c_Option_Oset(c_Option_Ooption_ONone(A),A)=c_Map_Odom(c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),A),A,B). % 42.68/42.80 >>>> Starting back demodulation with 289. % 42.68/42.80 >>>> Starting back demodulation with 294. % 42.68/42.80 >>>> Starting back demodulation with 297. % 42.68/42.80 >>>> Starting back demodulation with 299. % 42.68/42.80 >>>> Starting back demodulation with 302. % 42.68/42.80 ** KEPT (pick-wt=20): 515 [copy,304,flip.1] c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(A),A),tc_fun(A,tc_bool))=c_Map_Odom(c_COMBK(hAPP(c_Option_Ooption_OSome(B),C),tc_Option_Ooption(B),A),A,B). % 42.68/42.80 ** KEPT (pick-wt=13): 516 [copy,306,flip.1] c_Option_Ooption_ONone(A)=hAPP(c_Map_Orestrict__map(B,c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),t_a,A),v_x). % 42.68/42.80 >>>> Starting back demodulation with 312. % 42.68/42.80 >> back demodulating 69 with 312. % 42.68/42.80 ** KEPT (pick-wt=22): 517 [copy,316,flip.1] c_Fun_Ofun__upd(c_Map_Orestrict__map(A,B,C,D),E,hAPP(A,E),C,tc_Option_Ooption(D))=c_Map_Orestrict__map(A,c_Set_Oinsert(E,B,C),C,D). % 42.68/42.80 >>>> Starting back demodulation with 321. % 42.68/42.80 >>>> Starting back demodulation with 327. % 42.68/42.80 ** KEPT (pick-wt=10): 518 [copy,330,flip.1,demod,366] c_Option_Ooption_ONone(A)=hAPP(c_Option_Omap(B,C,A),c_Option_Ooption_ONone(C)). % 42.68/42.80 >>>> Starting back demodulation with 336. % 42.68/42.80 ** KEPT (pick-wt=15): 519 [copy,337,flip.1] c_Option_Ooption_ONone(A)=c_Map_Omap__comp(B,c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),t_a),v_x,C,A,t_a). % 42.68/42.80 >>>> Starting back demodulation with 339. % 42.68/42.80 >>>> Starting back demodulation with 352. % 42.68/42.80 ** KEPT (pick-wt=26): 520 [copy,354,flip.1] c_Set_Oinsert(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B)=c_Map_Odom(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(C),tc_Option_Ooption(C),B),A,hAPP(c_Option_Ooption_OSome(C),D),B,tc_Option_Ooption(C)),B,C). % 42.68/42.80 Following clause subsumed by 518 during input processing: 0 [copy,356,flip.1] c_Option_Ooption_ONone(A)=hAPP(c_Option_Omap(B,C,A),c_Option_Ooption_ONone(C)). % 42.68/42.80 >>>> Starting back demodulation with 360. % 42.68/42.80 >>>> Starting back demodulation with 362. % 42.68/42.80 >>>> Starting back demodulation with 364. % 42.68/42.80 >>>> Starting back demodulation with 366. % 42.68/42.80 >> back demodulating 330 with 366. % 42.68/42.80 >> back demodulating 320 with 366. % 42.68/42.80 >>>> Starting back demodulation with 368. % 42.68/42.80 Following clause subsumed by 369 during input processing: 0 [copy,369,flip.1] c_Set_Oinsert(A,c_Set_Oinsert(B,C,D),D)=c_Set_Oinsert(B,c_Set_Oinsert(A,C,D),D). % 42.68/42.80 369 back subsumes 283. % 42.68/42.80 370 back subsumes 308. % 42.68/42.80 Following clause subsumed by 371 during input processing: 0 [copy,371,flip.1] c_Fun_Oswap(A,B,C,D,E)=c_Fun_Oswap(B,A,C,D,E). % 42.68/42.80 >>>> Starting back demodulation with 373. % 42.68/42.80 >>>> Starting back demodulation with 375. % 42.68/42.80 >>>> Starting back demodulation with 379. % 42.68/42.80 >>>> Starting back demodulation with 381. % 42.68/42.80 >> back demodulating 229 with 381. % 42.68/42.80 >> back demodulating 228 with 381. % 42.68/42.80 382 back subsumes 223. % 42.68/42.80 382 back subsumes 222. % 42.68/42.80 >>>> Starting back demodulation with 385. % 42.68/42.80 >> back demodulating 298 with 385. % 42.68/42.80 >> back demodulating 168 with 385. % 42.68/42.80 >> back demodulating 106 with 385. % 42.68/42.80 >> back demodulating 104 with 385. % 42.68/42.80 >>>> Starting back demodulation with 388. % 42.68/42.80 >>>> Starting back demodulation with 390. % 42.68/42.80 >>>> Starting back demodulation with 393. % 42.68/42.80 >>>> Starting back demodulation with 397. % 42.68/42.80 >> back demodulating 141 with 397. % 42.68/42.80 >>>> Starting back demodulation with 401. % 42.68/42.80 >> back demodulating 130 with 401. % 42.68/42.80 >>>> Starting back demodulation with 405. % 42.68/42.80 >>>> Starting back demodulation with 408. % 42.68/42.80 >>>> Starting back demodulation with 410. % 42.68/42.80 ** KEPT (pick-wt=13): 524 [copy,411,flip.1] hAPP(A,B)=c_Option_Ooption_Ooption__rec(C,A,hAPP(c_Option_Ooption_OSome(D),B),E,D). % 42.68/42.80 >>>> Starting back demodulation with 414. % 42.68/42.80 >> back demodulating 198 with 414. % 42.68/42.80 >>>> Starting back demodulation with 416. % 42.68/42.80 >>>> Starting back demodulation with 418. % 42.68/42.80 >>>> Starting back demodulation with 420. % 42.68/42.80 >> back demodulating 413 with 420. % 42.68/42.80 ** KEPT (pick-wt=22): 525 [copy,421,flip.1] c_Fun_Ofun__upd(c_Fun_Ofun__upd(A,B,hAPP(A,C),D,E),C,hAPP(A,B),D,E)=c_Fun_Oswap(B,C,A,D,E). % 42.68/42.80 >>>> Starting back demodulation with 423. % 42.68/42.80 ** KEPT (pick-wt=35): 526 [copy,424,flip.1] c_Fun_Ooverride__on(A,B,c_Set_Oinsert(C,D,E),E,tc_Option_Ooption(F))=c_Fun_Ofun__upd(c_Fun_Ooverride__on(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(F),G),E,tc_Option_Ooption(F)),D,E,tc_Option_Ooption(F)),C,hAPP(B,C),E,tc_Option_Ooption(F)). % 42.68/42.80 ** KEPT (pick-wt=13): 527 [copy,428,flip.1] hAPP(A,B)=c_Option_Ooption_Ooption__case(C,A,hAPP(c_Option_Ooption_OSome(D),B),E,D). % 42.68/42.80 ** KEPT (pick-wt=43): 528 [copy,429,flip.1] c_Fun_Ofun__upd(c_Fun_Ocomp(c_Option_Omap(A,B,C),D,tc_Option_Ooption(B),tc_Option_Ooption(C),E),F,hAPP(c_Option_Ooption_OSome(C),hAPP(A,G)),E,tc_Option_Ooption(C))=c_Fun_Ocomp(c_Option_Omap(A,B,C),c_Fun_Ofun__upd(D,F,hAPP(c_Option_Ooption_OSome(B),G),E,tc_Option_Ooption(B)),tc_Option_Ooption(B),tc_Option_Ooption(C),E). % 42.68/42.80 >>>> Starting back demodulation with 432. % 42.68/42.80 ** KEPT (pick-wt=28): 529 [copy,433,flip.1] c_Map_Omap__upds(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,tc_Option_Ooption(C)),F,G,E,C)=c_Map_Omap__upds(A,c_List_Olist_OCons(B,F,E),c_List_Olist_OCons(D,G,C),E,C). % 42.68/42.80 >>>> Starting back demodulation with 436. % 42.68/42.80 ** KEPT (pick-wt=16): 530 [copy,438,flip.1] hAPP(c_Option_Ooption_OSome(A),hAPP(B,C))=hAPP(c_Option_Omap(B,D,A),hAPP(c_Option_Ooption_OSome(D),C)). % 42.68/42.80 Following clause subsumed by 489 during input processing: 0 [copy,450,flip.1] c_Map_Odom(c_Fun_Ofun__upd(A,B,c_Option_Ooption_ONone(C),D,tc_Option_Ooption(C)),D,C)=c_HOL_Ominus__class_Ominus(c_Map_Odom(A,D,C),c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(D),D),D),tc_fun(D,tc_bool)). % 42.68/42.80 Following clause subsumed by 480 during input processing: 0 [copy,462,flip.1] c_HOL_Ouminus__class_Ouminus(A,tc_fun(B,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(B),B),tc_fun(B,tc_bool)),A,tc_fun(B,tc_bool)). % 42.68/42.80 Following clause subsumed by 479 during input processing: 0 [copy,463,flip.1] c_HOL_Ominus__class_Ominus(A,A,tc_fun(B,tc_bool))=c_Option_Oset(c_Option_Ooption_ONone(B),B). % 42.68/42.80 Following clause subsumed by 476 during input processing: 0 [copy,464,flip.1] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(D),D),D),tc_fun(D,tc_bool)),C,tc_fun(D,tc_bool)). % 42.68/42.80 Following clause subsumed by 475 during input processing: 0 [copy,465,flip.1] c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,C,D),tc_fun(D,tc_bool))=c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,C,tc_fun(D,tc_bool)),c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(D),D),D),tc_fun(D,tc_bool)). % 42.68/42.80 Following clause subsumed by 281 during input processing: 0 [copy,467,flip.1] c_Set_Oimage(A,c_Option_Oset(c_Option_Ooption_ONone(B),B),B,C)=c_Option_Oset(c_Option_Ooption_ONone(C),C). % 42.68/42.80 >>>> Starting back demodulation with 469. % 42.68/42.80 >>>> Starting back demodulation with 471. % 42.68/42.80 >>>> Starting back demodulation with 474. % 42.68/42.80 >> back demodulating 466 with 474. % 42.68/42.80 Following clause subsumed by 465 during input processing: 0 [copy,475,flip.1] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,B,tc_fun(C,tc_bool)),c_Set_Oinsert(D,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(D,B,C),tc_fun(C,tc_bool)). % 42.68/42.80 Following clause subsumed by 464 during input processing: 0 [copy,476,flip.1] c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,c_Option_Oset(c_Option_Ooption_ONone(C),C),C),tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool))=c_HOL_Ominus__class_Ominus(A,c_Set_Oinsert(B,D,C),tc_fun(C,tc_bool)). % 42.68/42.80 >>>> Starting back demodulation with 478. % 42.68/42.80 Following clause subsumed by 463 during input processing: 0 [copy,479,flip.1] c_Option_Oset(c_Option_Ooption_ONone(A),A)=c_HOL_Ominus__class_Ominus(B,B,tc_fun(A,tc_bool)). % 42.68/42.80 Following clause subsumed by 462 during input processing: 0 [copy,480,flip.1] c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(A),A),tc_fun(A,tc_bool)),B,tc_fun(A,tc_bool))=c_HOL_Ouminus__class_Ouminus(B,tc_fun(A,tc_bool)). % 42.68/42.80 >>>> Starting back demodulation with 482. % 42.68/42.80 >>>> Starting back demodulation with 484. % 42.68/42.80 >>>> Starting back demodulation with 486. % 42.68/42.80 >>>> Starting back demodulation with 488. % 42.68/42.80 >> back demodulating 452 with 488. % 42.68/42.80 >> back demodulating 451 with 488. % 42.68/42.80 Following clause subsumed by 450 during input processing: 0 [copy,489,flip.1] c_HOL_Ominus__class_Ominus(c_Map_Odom(A,B,C),c_Set_Oinsert(D,c_Option_Oset(c_Option_Ooption_ONone(B),B),B),tc_fun(B,tc_bool))=c_Map_Odom(c_Fun_Ofun__upd(A,D,c_Option_Ooption_ONone(C),B,tc_Option_Ooption(C)),B,C). % 42.68/42.80 Following clause subsumed by 506 during input processing: 0 [copy,498,flip.1] c_Set_Oinsert(A,B,C)!=c_Option_Oset(c_Option_Ooption_ONone(C),C). % 42.68/42.80 Following clause subsumed by 498 during input processing: 0 [copy,506,flip.1] c_Option_Oset(c_Option_Ooption_ONone(A),A)!=c_Set_Oinsert(B,C,A). % 42.68/42.80 Following clause subsumed by 285 during input processing: 0 [copy,514,flip.1] c_Map_Odom(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),B,A)=c_Option_Oset(c_Option_Ooption_ONone(B),B). % 42.68/42.80 Following clause subsumed by 304 during input processing: 0 [copy,515,flip.1] c_Map_Odom(c_COMBK(hAPP(c_Option_Ooption_OSome(A),B),tc_Option_Ooption(A),C),C,A)=c_HOL_Ouminus__class_Ouminus(c_Option_Oset(c_Option_Ooption_ONone(C),C),tc_fun(C,tc_bool)). % 42.68/42.80 Following clause subsumed by 306 during input processing: 0 [copy,516,flip.1] hAPP(c_Map_Orestrict__map(A,c_Option_Oset(c_Option_Ooption_ONone(t_a),t_a),t_a,B),v_x)=c_Option_Ooption_ONone(B). % 42.68/42.80 Following clause subsumed by 316 during input processing: 0 [copy,517,flip.1] c_Map_Orestrict__map(A,c_Set_Oinsert(B,C,D),D,E)=c_Fun_Ofun__upd(c_Map_Orestrict__map(A,C,D,E),B,hAPP(A,B),D,tc_Option_Ooption(E)). % 42.68/42.80 Following clause subsumed by 356 during input processing: 0 [copy,518,flip.1] hAPP(c_Option_Omap(A,B,C),c_Option_Ooption_ONone(B))=c_Option_Ooption_ONone(C). % 42.68/42.80 Following clause subsumed by 337 during input processing: 0 [copy,519,flip.1] c_Map_Omap__comp(A,c_COMBK(c_Option_Ooption_ONone(B),tc_Option_Ooption(B),t_a),v_x,B,C,t_a)=c_Option_Ooption_ONone(C). % 42.68/42.80 Following clause subsumed by 354 during input processing: 0 [copy,520,flip.1] c_Map_Odom(c_Fun_Ofun__upd(c_COMBK(c_Option_Ooption_ONone(A),tc_Option_Ooption(A),B),C,hAPP(c_Option_Ooption_OSome(A),D),B,tc_Option_Ooption(A)),B,A)=c_Set_Oinsert(C,c_Option_Oset(c_Option_Ooption_ONone(B),B),B). % 42.68/42.80 Following clause subsumed by 411 during input processing: 0 [copy,524,flip.1] c_Option_Ooption_Ooption__rec(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,C)=hAPP(B,D). % 42.68/42.80 Following clause subsumed by 421 during input processing: 0 [copy,525,flip.1] c_Fun_Oswap(A,B,C,D,E)=c_Fun_Ofun__upd(c_Fun_Ofun__upd(C,A,hAPP(C,B),D,E),B,hAPP(C,A),D,E). % 42.68/42.80 Following clause subsumed by 424 during input processing: 0 [copy,526,flip.1] c_Fun_Ofun__upd(c_Fun_Ooverride__on(A,c_Fun_Ofun__upd(B,C,hAPP(c_Option_Ooption_OSome(D),E),F,tc_Option_Ooption(D)),G,F,tc_Option_Ooption(D)),C,hAPP(B,C),F,tc_Option_Ooption(D))=c_Fun_Ooverride__on(A,B,c_Set_Oinsert(C,G,F),F,tc_Option_Ooption(D)). % 42.68/42.80 Following clause subsumed by 428 during input processing: 0 [copy,527,flip.1] c_Option_Ooption_Ooption__case(A,B,hAPP(c_Option_Ooption_OSome(C),D),E,C)=hAPP(B,D). % 42.68/42.80 Following clause subsumed by 429 during input processing: 0 [copy,528,flip.1] c_Fun_Ocomp(c_Option_Omap(A,B,C),c_Fun_Ofun__upd(D,E,hAPP(c_Option_Ooption_OSome(B),F),G,tc_Option_Ooption(B)),tc_Option_Ooption(B),tc_Option_Ooption(C),G)=c_Fun_Ofun__upd(c_Fun_Ocomp(c_Option_Omap(A,B,C),D,tc_Option_Ooption(B),tc_Option_Ooption(C),G),E,hAPP(c_Option_Ooption_OSome(C),hAPP(A,F)),G,tc_Option_Ooption(C)). % 42.68/42.80 Following clause subsumed by 433 during input processing: 0 [copy,529,flip.1] c_Map_Omap__upds(A,c_List_Olist_OCons(B,C,D),c_List_Olist_OCons(E,F,G),D,G)=c_Map_Omap__upds(c_Fun_Ofun__upd(A,B,hAPP(c_Option_Ooption_OSome(G),E),D,tc_Option_Ooption(G)),C,F,D,G). % 42.84/42.95 Following clause subsumed by 438 during input processing: 0 [copy,530,flip.1] hAPP(c_Option_Omap(A,B,C),hAPP(c_Option_Ooption_OSome(B),D))=hAPP(c_Option_Ooption_OSome(C),hAPP(A,D)). % 42.84/42.95 % 42.84/42.95 ======= end of input processing ======= % 42.84/42.95 % 42.84/42.95 =========== start of search =========== % 42.84/42.95 % 42.84/42.95 % 42.84/42.95 Resetting weight limit to 2. % 42.84/42.95 % 42.84/42.95 % 42.84/42.95 Resetting weight limit to 2. % 42.84/42.95 % 42.84/42.95 sos_size=177 % 42.84/42.95 % 42.84/42.95 Search stopped in tp_alloc by max_mem option. % 42.84/42.95 % 42.84/42.95 Search stopped in tp_alloc by max_mem option. % 42.84/42.95 % 42.84/42.95 ============ end of search ============ % 42.84/42.95 % 42.84/42.95 -------------- statistics ------------- % 42.84/42.95 clauses given 80 % 42.84/42.95 clauses generated 11752 % 42.84/42.95 clauses kept 425 % 42.84/42.95 clauses forward subsumed 96 % 42.84/42.95 clauses back subsumed 9 % 42.84/42.95 Kbytes malloced 11718 % 42.84/42.95 % 42.84/42.95 ----------- times (seconds) ----------- % 42.84/42.95 user CPU time 0.21 (0 hr, 0 min, 0 sec) % 42.84/42.95 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 42.84/42.95 wall-clock time 43 (0 hr, 0 min, 43 sec) % 42.84/42.95 % 42.84/42.95 Process 32108 finished Wed Jul 27 05:49:52 2022 % 42.88/42.95 Otter interrupted % 42.88/42.95 PROOF NOT FOUND %------------------------------------------------------------------------------