diff --git a/tests/PrimitiveProjections.v b/tests/PrimitiveProjections.v index 2b5f28259..8c53a3f98 100644 --- a/tests/PrimitiveProjections.v +++ b/tests/PrimitiveProjections.v @@ -3,12 +3,16 @@ Set Implicit Arguments. Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. +Local Set Warnings "-notation-overridden". + Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. + Definition bar := @projT1. Definition baz A P (x : @sigT A P) := projT1 x. -Definition foo (A: Type) (B: A -> Type) (C: A -> Type) (c: {x : A & {_ : B x & C x}}) : {x : A & {_ : C x & B x}}. +Definition foo (A: Type) (B: A -> Type) (C: A -> Type) + (c: { x : A & { _ : B x & C x }}) : { x : A & { _ : C x & B x }}. Proof. exists (projT1 c). exists (projT2 (projT2 c)). diff --git a/tests/Test.v b/tests/Test.v index b1c46fd10..2b5c32693 100644 --- a/tests/Test.v +++ b/tests/Test.v @@ -19,6 +19,8 @@ Set Implicit Arguments. (** ** Definitions *) +Declare Scope test_list_scope. + Section Lists. Variable A : Type. @@ -27,9 +29,9 @@ Section Lists. | nil : list | cons : A -> list -> list. - Infix "::" := cons (at level 60, right associativity) : list_scope. + Infix "::" := cons (at level 60, right associativity) : test_list_scope. - Open Scope list_scope. + Open Scope test_list_scope. (** Head and tail *) Definition head (l:list) := @@ -76,21 +78,21 @@ Axiom size_nil : size nil = 0. | a :: l1 => a :: app l1 m end. - Infix "++" := app (right associativity, at level 60) : list_scope. + Infix "++" := app (right associativity, at level 60) : test_list_scope. End Lists. (** Exporting list notations and tactics *) Arguments nil {A}. -Infix "::" := cons (at level 60, right associativity) : list_scope. -Infix "++" := app (right associativity, at level 60) : list_scope. +Infix "::" := cons (at level 60, right associativity) : test_list_scope. +Infix "++" := app (right associativity, at level 60) : test_list_scope. -Open Scope list_scope. +Open Scope test_list_scope. -Delimit Scope list_scope with list. +Delimit Scope test_list_scope with lst. -Bind Scope list_scope with list. +Bind Scope test_list_scope with list. Arguments list _%type_scope. @@ -211,7 +213,7 @@ Section Facts. now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). rewrite <- IHl; auto. Qed. - Hint Resolve app_ass. + Hint Resolve app_ass : core. Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n. Proof. @@ -412,7 +414,7 @@ Section Elts. Proof. unfold lt in |- *; induction n as [| n hn]; simpl in |- *. destruct l; simpl in |- *; [ inversion 2 | auto ]. - destruct l as [| a l hl]; simpl in |- *. + destruct l as [| a l ]; simpl in |- *. inversion 2. intros d ie; right; apply hn; auto with arith. Qed. @@ -786,7 +788,7 @@ Section ListOps. | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l)) | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''. - Hint Constructors Permutation. + Hint Constructors Permutation : core. (** Some facts about [Permutation] *) @@ -821,7 +823,7 @@ Section ListOps. exact perm_trans. Qed. - Hint Resolve Permutation_refl Permutation_sym Permutation_trans. + Hint Resolve Permutation_refl Permutation_sym Permutation_trans : core. (** Compatibility with others operations on lists *) @@ -876,7 +878,7 @@ Section ListOps. apply perm_swap; auto. apply perm_skip; auto. Qed. - Hint Resolve Permutation_cons_app. + Hint Resolve Permutation_cons_app : core. Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'. Proof. @@ -1075,7 +1077,7 @@ Section Map. rewrite IHl; auto. Qed. - Hint Constructors Permutation. + Hint Constructors Permutation : core. Lemma Permutation_map : forall l l', Permutation l l' -> Permutation (map l) (map l'). @@ -1591,19 +1593,19 @@ Section SetIncl. Variable A : Type. Definition incl (l m:list A) := forall a:A, In a l -> In a m. - Hint Unfold incl. + Hint Unfold incl : core. Lemma incl_refl : forall l:list A, incl l l. Proof. auto. Qed. - Hint Resolve incl_refl. + Hint Resolve incl_refl : core. Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). Proof. auto with datatypes. Qed. - Hint Immediate incl_tl. + Hint Immediate incl_tl : core. Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. Proof. @@ -1614,13 +1616,13 @@ Section SetIncl. Proof. auto with datatypes. Qed. - Hint Immediate incl_appl. + Hint Immediate incl_appl : core. Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). Proof. auto with datatypes. Qed. - Hint Immediate incl_appr. + Hint Immediate incl_appr : core. Lemma incl_cons : forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. @@ -1635,7 +1637,7 @@ Section SetIncl. now_show (In a0 l -> In a0 m). auto. Qed. - Hint Resolve incl_cons. + Hint Resolve incl_cons : core. Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. @@ -1643,7 +1645,7 @@ Section SetIncl. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. - Hint Resolve incl_app. + Hint Resolve incl_app : core. End SetIncl. @@ -1733,6 +1735,8 @@ End Cutting. Module ReDun. + Section Dummy. + Variable A : Type. Inductive NoDup : list A -> Prop := @@ -1790,6 +1794,7 @@ Module ReDun. destruct (NoDup_remove_2 _ _ _ H0 H). Qed. + End Dummy. End ReDun. diff --git a/tests/graph.dot.oracle b/tests/graph.dot.oracle index 87aad5c44..7e868f9d1 100644 --- a/tests/graph.dot.oracle +++ b/tests/graph.dot.oracle @@ -1,25 +1,23 @@ digraph tests/graph { graph [ratio=0.5] node [style=filled] -Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; Test_exists_last [label="exists_last", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_removelast [label="removelast", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; Test_last [label="last", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_sind [label="NoDup_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; +Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_sind [label="NoDup_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; +Test_remove [label="remove", URL=, fillcolor="#F070D1"] ; Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; -Test_remove [label="remove", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup [label="NoDup", URL=, fillcolor="#E2CDFA"] ; +Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup [label="NoDup", URL=, fillcolor="#E2CDFA"] ; Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_A [label="A", URL=, fillcolor="#FACDEF"] ; Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_nth_overflow [label="nth_overflow", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_seq_nth [label="seq_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; @@ -184,57 +182,52 @@ Test_count_occ_nil [label="count_occ_nil", URL=, periph Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_count_occ_In [label="count_occ_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_count_occ [label="count_occ", URL=, fillcolor="#F070D1"] ; - Test_removelast_app -> Test_removelast [] ; - Test_removelast_app -> Test_app [] ; - Test_removelast_app -> Test_list_ind [] ; +Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; Test_exists_last -> Test_app [] ; Test_exists_last -> Test_list_rect [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; - Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; - Test_ReDun_NoDup_Permutation -> Test_In_split [] ; Test_app_removelast_last -> Test_removelast [] ; Test_app_removelast_last -> Test_last [] ; Test_app_removelast_last -> Test_app [] ; Test_app_removelast_last -> Test_list_ind [] ; - Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ; - Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; + Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; + Test_ReDun_NoDup_Permutation -> Test_In_split [] ; Test_removelast -> Test_cons [] ; Test_removelast -> Test_nil [] ; Test_removelast -> Test_list [] ; + Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ; + Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; + Test_last -> Test_list [] ; Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup [] ; Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ; - Test_last -> Test_list [] ; - Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ; Test_remove_In -> Test_remove [] ; Test_remove_In -> Test_In [] ; Test_remove_In -> Test_list_ind [] ; + Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ; + Test_remove -> Test_cons [] ; + Test_remove -> Test_nil [] ; + Test_remove -> Test_list [] ; Test_ReDun_NoDup_ind -> Test_ReDun_NoDup [] ; - Test_ReDun_NoDup_cons -> Test_ReDun_A [] ; Test_ReDun_NoDup_cons -> Test_In [] ; Test_ReDun_NoDup_cons -> Test_cons [] ; Test_ReDun_NoDup_cons -> Test_nil [] ; - Test_remove -> Test_cons [] ; - Test_remove -> Test_nil [] ; - Test_remove -> Test_list [] ; - Test_ReDun_NoDup_nil -> Test_ReDun_A [] ; - Test_ReDun_NoDup_nil -> Test_In [] ; - Test_ReDun_NoDup_nil -> Test_cons [] ; - Test_ReDun_NoDup_nil -> Test_nil [] ; Test_app_nth2 -> Test_nth [] ; Test_app_nth2 -> Test_app [] ; Test_app_nth2 -> Test_length [] ; Test_app_nth2 -> Test_list_ind [] ; - Test_ReDun_NoDup -> Test_ReDun_A [] ; - Test_ReDun_NoDup -> Test_In [] ; - Test_ReDun_NoDup -> Test_cons [] ; - Test_ReDun_NoDup -> Test_nil [] ; + Test_ReDun_NoDup_nil -> Test_In [] ; + Test_ReDun_NoDup_nil -> Test_cons [] ; + Test_ReDun_NoDup_nil -> Test_nil [] ; Test_app_nth1 -> Test_nth [] ; Test_app_nth1 -> Test_app [] ; Test_app_nth1 -> Test_length [] ; Test_app_nth1 -> Test_list_ind [] ; + Test_ReDun_NoDup -> Test_In [] ; + Test_ReDun_NoDup -> Test_cons [] ; + Test_ReDun_NoDup -> Test_nil [] ; Test_nth_indep -> Test_nth [] ; Test_nth_indep -> Test_length [] ; Test_nth_indep -> Test_list_ind [] ; @@ -616,8 +609,11 @@ Test_count_occ [label="count_occ", URL=, fillcolor="#F070D1 Test_count_occ_In -> Test_In [] ; Test_count_occ_In -> Test_list_ind [] ; Test_count_occ -> Test_list [] ; + Test_removelast_app -> Test_removelast [] ; + Test_removelast_app -> Test_app [] ; + Test_removelast_app -> Test_list_ind [] ; subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled -Test_ReDun_A; Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; -Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_length; Test_split_combine; Test_combine_split; Test_size; Test_in_combine_l; Test_size_nil; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_destruct_list; Test_list_prod; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_lel; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_In_dec; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_nth_in_or_default; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_nth_error; Test_seq; Test_nth_default; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; Test_removelast_app; }; +Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; +Test_removelast_app; Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_length; Test_split_combine; Test_combine_split; Test_size; Test_in_combine_l; Test_size_nil; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_destruct_list; Test_list_prod; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_lel; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_In_dec; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_nth_in_or_default; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_nth_error; Test_seq; Test_nth_default; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; }; } /* END */ diff --git a/tests/graph.dpd.oracle b/tests/graph.dpd.oracle index 7164690c2..b14c2f0cd 100644 --- a/tests/graph.dpd.oracle +++ b/tests/graph.dpd.oracle @@ -1,1100 +1,1091 @@ -N: 9 "A" [body=no, kind=cnst, prop=no, path="Test.ReDun", ]; -N: 170 "In" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 159 "In_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 117 "In_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 161 "In_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 169 "In" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 158 "In_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 116 "In_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 160 "In_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; N: 1 "NoDup_Permutation" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; N: 5 "NoDup_ind" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; N: 3 "NoDup_remove_1" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; N: 2 "NoDup_remove_2" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; N: 4 "NoDup_sind" [body=yes, kind=cnst, prop=no, path="Test.ReDun", ]; -N: 93 "Permutation_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 94 "Permutation_app_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 87 "Permutation_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 84 "Permutation_app_inv_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 83 "Permutation_app_inv_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 92 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 95 "Permutation_app_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 91 "Permutation_cons_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 85 "Permutation_cons_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 86 "Permutation_cons_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 96 "Permutation_in" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 103 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 88 "Permutation_ind_bis" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 90 "Permutation_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 74 "Permutation_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 101 "Permutation_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 100 "Permutation_nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 99 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 89 "Permutation_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 102 "Permutation_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 98 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 97 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 169 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 156 "app_ass" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 154 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 158 "app_cons_not_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 153 "app_eq_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 152 "app_eq_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 151 "app_inj_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 147 "app_inv_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 146 "app_inv_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 150 "app_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 157 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 136 "app_nth1" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 135 "app_nth2" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 130 "app_removelast_last" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 155 "ass_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 46 "combine" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 41 "combine_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 40 "combine_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 44 "combine_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 127 "count_occ" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 126 "count_occ_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 123 "count_occ_cons_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 122 "count_occ_cons_neq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 125 "count_occ_inv_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 124 "count_occ_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 167 "destruct_list" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 120 "distr_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 129 "exists_last" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 61 "existsb" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 60 "existsb_exists" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 59 "existsb_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 56 "filter" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 55 "filter_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 54 "find" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 19 "firstn" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 16 "firstn_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 14 "firstn_removelast" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 17 "firstn_skipn" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 73 "flat_map" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 69 "fold_left" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 68 "fold_left_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 67 "fold_left_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 64 "fold_left_rev_right" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 66 "fold_right" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 65 "fold_right_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 63 "fold_symmetric" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 58 "forallb" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 57 "forallb_forall" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 175 "hd" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 176 "head" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 165 "head_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 166 "head_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 149 "in_app_or" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 43 "in_combine_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 42 "in_combine_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 163 "in_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 164 "in_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 72 "in_flat_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 160 "in_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 80 "in_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 79 "in_map_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 162 "in_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 148 "in_or_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 37 "in_prod" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 38 "in_prod_aux" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 36 "in_prod_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 51 "in_split_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 50 "in_split_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 27 "incl" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 20 "incl_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 23 "incl_appl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 22 "incl_appr" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 21 "incl_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 26 "incl_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 25 "incl_tl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 24 "incl_tran" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 132 "last" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 34 "lel" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 30 "lel_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 31 "lel_cons_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 28 "lel_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 33 "lel_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 29 "lel_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 32 "lel_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 173 "length" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 82 "list_eq_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 179 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 62 "list_power" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 39 "list_prod" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 178 "list_rec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 180 "list_rect" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 177 "list_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 81 "map" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 76 "map_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 70 "map_ext" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 78 "map_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 71 "map_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 77 "map_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 75 "map_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 168 "nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 145 "nth" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 139 "nth_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 142 "nth_S_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 140 "nth_default" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 141 "nth_error" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 143 "nth_in_or_default" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 137 "nth_indep" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 144 "nth_ok" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 138 "nth_overflow" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 53 "partition" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 35 "prod_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 134 "remove" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 133 "remove_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 131 "removelast" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 128 "removelast_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 15 "removelast_firstn" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 121 "rev" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 113 "rev'" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 111 "rev_alt" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 114 "rev_append" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 112 "rev_append_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 109 "rev_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 118 "rev_involutive" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 116 "rev_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 110 "rev_list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 115 "rev_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 119 "rev_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 13 "seq" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 12 "seq_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 11 "seq_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 10 "seq_shift" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 172 "size" [body=no, kind=cnst, prop=no, path="Test", ]; -N: 171 "size_nil" [body=no, kind=cnst, prop=yes, path="Test", ]; -N: 18 "skipn" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 52 "split" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 45 "split_combine" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 48 "split_length_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 47 "split_length_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 49 "split_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 174 "tail" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 92 "Permutation_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 93 "Permutation_app_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 86 "Permutation_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 83 "Permutation_app_inv_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 82 "Permutation_app_inv_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 91 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 94 "Permutation_app_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 90 "Permutation_cons_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 84 "Permutation_cons_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 85 "Permutation_cons_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 95 "Permutation_in" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 102 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 87 "Permutation_ind_bis" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 89 "Permutation_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 73 "Permutation_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 100 "Permutation_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 99 "Permutation_nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 98 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 88 "Permutation_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 101 "Permutation_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 97 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 96 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 168 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 155 "app_ass" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 153 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 157 "app_cons_not_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 152 "app_eq_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 151 "app_eq_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 150 "app_inj_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 146 "app_inv_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 145 "app_inv_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 149 "app_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 156 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 135 "app_nth1" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 134 "app_nth2" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 129 "app_removelast_last" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 154 "ass_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 45 "combine" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 40 "combine_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 39 "combine_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 43 "combine_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 126 "count_occ" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 125 "count_occ_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 122 "count_occ_cons_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 121 "count_occ_cons_neq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 124 "count_occ_inv_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 123 "count_occ_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 166 "destruct_list" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 119 "distr_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 128 "exists_last" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 60 "existsb" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 59 "existsb_exists" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 58 "existsb_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 55 "filter" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 54 "filter_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 53 "find" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 18 "firstn" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 15 "firstn_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 13 "firstn_removelast" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 16 "firstn_skipn" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 72 "flat_map" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 68 "fold_left" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 67 "fold_left_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 66 "fold_left_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 63 "fold_left_rev_right" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 65 "fold_right" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 64 "fold_right_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 62 "fold_symmetric" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 57 "forallb" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 56 "forallb_forall" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 174 "hd" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 175 "head" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 164 "head_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 165 "head_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 148 "in_app_or" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 42 "in_combine_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 41 "in_combine_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 162 "in_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 163 "in_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 71 "in_flat_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 159 "in_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 79 "in_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 78 "in_map_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 161 "in_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 147 "in_or_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 36 "in_prod" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 37 "in_prod_aux" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 35 "in_prod_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 50 "in_split_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 49 "in_split_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 26 "incl" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 19 "incl_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 22 "incl_appl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 21 "incl_appr" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 20 "incl_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 25 "incl_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 24 "incl_tl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 23 "incl_tran" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 131 "last" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 33 "lel" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 29 "lel_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 30 "lel_cons_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 27 "lel_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 32 "lel_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 28 "lel_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 31 "lel_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 172 "length" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 81 "list_eq_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 178 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 61 "list_power" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 38 "list_prod" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 177 "list_rec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 179 "list_rect" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 176 "list_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 80 "map" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 75 "map_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 69 "map_ext" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 77 "map_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 70 "map_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 76 "map_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 74 "map_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 167 "nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 144 "nth" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 138 "nth_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 141 "nth_S_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 139 "nth_default" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 140 "nth_error" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 142 "nth_in_or_default" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 136 "nth_indep" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 143 "nth_ok" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 137 "nth_overflow" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 52 "partition" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 34 "prod_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 133 "remove" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 132 "remove_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 130 "removelast" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 127 "removelast_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 14 "removelast_firstn" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 120 "rev" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 112 "rev'" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 110 "rev_alt" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 113 "rev_append" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 111 "rev_append_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 108 "rev_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 117 "rev_involutive" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 115 "rev_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 109 "rev_list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 114 "rev_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 118 "rev_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 12 "seq" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 11 "seq_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 10 "seq_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 9 "seq_shift" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 171 "size" [body=no, kind=cnst, prop=no, path="Test", ]; +N: 170 "size_nil" [body=no, kind=cnst, prop=yes, path="Test", ]; +N: 17 "skipn" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 51 "split" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 44 "split_combine" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 47 "split_length_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 46 "split_length_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 48 "split_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 173 "tail" [body=yes, kind=cnst, prop=no, path="Test", ]; N: 8 "NoDup" [kind=inductive, prop=no, path="Test.ReDun", ]; -N: 108 "Permutation" [kind=inductive, prop=no, path="Test", ]; -N: 183 "list" [kind=inductive, prop=no, path="Test", ]; +N: 107 "Permutation" [kind=inductive, prop=no, path="Test", ]; +N: 182 "list" [kind=inductive, prop=no, path="Test", ]; N: 7 "NoDup_nil" [kind=construct, prop=yes, path="Test.ReDun", ]; -N: 107 "perm_nil" [kind=construct, prop=yes, path="Test", ]; -N: 182 "nil" [kind=construct, prop=no, path="Test", ]; +N: 106 "perm_nil" [kind=construct, prop=yes, path="Test", ]; +N: 181 "nil" [kind=construct, prop=no, path="Test", ]; N: 6 "NoDup_cons" [kind=construct, prop=yes, path="Test.ReDun", ]; -N: 106 "perm_skip" [kind=construct, prop=yes, path="Test", ]; -N: 181 "cons" [kind=construct, prop=no, path="Test", ]; -N: 105 "perm_swap" [kind=construct, prop=yes, path="Test", ]; -N: 104 "perm_trans" [kind=construct, prop=yes, path="Test", ]; +N: 105 "perm_skip" [kind=construct, prop=yes, path="Test", ]; +N: 180 "cons" [kind=construct, prop=no, path="Test", ]; +N: 104 "perm_swap" [kind=construct, prop=yes, path="Test", ]; +N: 103 "perm_trans" [kind=construct, prop=yes, path="Test", ]; E: 1 2 [weight=1, ]; E: 1 3 [weight=1, ]; E: 1 8 [weight=26, ]; -E: 1 9 [weight=392, ]; -E: 1 91 [weight=1, ]; -E: 1 107 [weight=1, ]; -E: 1 108 [weight=16, ]; +E: 1 90 [weight=1, ]; +E: 1 106 [weight=1, ]; +E: 1 107 [weight=16, ]; +E: 1 147 [weight=2, ]; E: 1 148 [weight=2, ]; -E: 1 149 [weight=2, ]; -E: 1 161 [weight=1, ]; -E: 1 169 [weight=37, ]; -E: 1 170 [weight=125, ]; -E: 1 179 [weight=1, ]; -E: 1 181 [weight=78, ]; -E: 1 182 [weight=20, ]; -E: 1 183 [weight=65, ]; +E: 1 160 [weight=1, ]; +E: 1 168 [weight=37, ]; +E: 1 169 [weight=125, ]; +E: 1 178 [weight=1, ]; +E: 1 180 [weight=78, ]; +E: 1 181 [weight=20, ]; +E: 1 182 [weight=65, ]; E: 2 8 [weight=21, ]; -E: 2 9 [weight=272, ]; -E: 2 148 [weight=1, ]; -E: 2 169 [weight=43, ]; -E: 2 170 [weight=33, ]; -E: 2 179 [weight=1, ]; -E: 2 181 [weight=66, ]; -E: 2 182 [weight=8, ]; -E: 2 183 [weight=80, ]; +E: 2 147 [weight=1, ]; +E: 2 168 [weight=43, ]; +E: 2 169 [weight=33, ]; +E: 2 178 [weight=1, ]; +E: 2 180 [weight=66, ]; +E: 2 181 [weight=8, ]; +E: 2 182 [weight=80, ]; E: 3 6 [weight=1, ]; E: 3 8 [weight=34, ]; -E: 3 9 [weight=244, ]; +E: 3 147 [weight=1, ]; E: 3 148 [weight=1, ]; -E: 3 149 [weight=1, ]; -E: 3 169 [weight=37, ]; -E: 3 170 [weight=27, ]; -E: 3 179 [weight=1, ]; -E: 3 181 [weight=67, ]; -E: 3 182 [weight=8, ]; -E: 3 183 [weight=75, ]; +E: 3 168 [weight=37, ]; +E: 3 169 [weight=27, ]; +E: 3 178 [weight=1, ]; +E: 3 180 [weight=67, ]; +E: 3 181 [weight=8, ]; +E: 3 182 [weight=75, ]; E: 4 8 [weight=8, ]; -E: 4 9 [weight=19, ]; -E: 4 170 [weight=3, ]; +E: 4 169 [weight=3, ]; +E: 4 180 [weight=2, ]; E: 4 181 [weight=2, ]; -E: 4 182 [weight=2, ]; -E: 4 183 [weight=9, ]; +E: 4 182 [weight=9, ]; E: 5 8 [weight=8, ]; -E: 5 9 [weight=19, ]; -E: 5 170 [weight=3, ]; +E: 5 169 [weight=3, ]; +E: 5 180 [weight=2, ]; E: 5 181 [weight=2, ]; -E: 5 182 [weight=2, ]; -E: 5 183 [weight=9, ]; -E: 6 9 [weight=5, ]; -E: 6 170 [weight=1, ]; +E: 5 182 [weight=9, ]; +E: 6 169 [weight=1, ]; +E: 6 180 [weight=1, ]; E: 6 181 [weight=1, ]; E: 6 182 [weight=1, ]; -E: 6 183 [weight=1, ]; -E: 7 9 [weight=5, ]; -E: 7 170 [weight=1, ]; +E: 7 169 [weight=1, ]; +E: 7 180 [weight=1, ]; E: 7 181 [weight=1, ]; E: 7 182 [weight=1, ]; -E: 7 183 [weight=1, ]; -E: 8 9 [weight=5, ]; -E: 8 170 [weight=1, ]; +E: 8 169 [weight=1, ]; +E: 8 180 [weight=1, ]; E: 8 181 [weight=1, ]; E: 8 182 [weight=1, ]; -E: 8 183 [weight=1, ]; -E: 10 13 [weight=14, ]; -E: 10 81 [weight=6, ]; -E: 10 181 [weight=3, ]; -E: 10 182 [weight=1, ]; -E: 10 183 [weight=10, ]; -E: 11 13 [weight=12, ]; -E: 11 145 [weight=12, ]; -E: 11 181 [weight=3, ]; -E: 12 13 [weight=6, ]; -E: 12 173 [weight=6, ]; -E: 13 181 [weight=1, ]; -E: 13 182 [weight=1, ]; -E: 13 183 [weight=3, ]; -E: 14 19 [weight=30, ]; -E: 14 128 [weight=1, ]; -E: 14 131 [weight=17, ]; -E: 14 169 [weight=3, ]; -E: 14 173 [weight=26, ]; -E: 14 181 [weight=17, ]; -E: 14 182 [weight=27, ]; -E: 14 183 [weight=42, ]; -E: 15 19 [weight=30, ]; -E: 15 128 [weight=1, ]; -E: 15 131 [weight=11, ]; -E: 15 169 [weight=3, ]; -E: 15 173 [weight=18, ]; -E: 15 181 [weight=16, ]; -E: 15 182 [weight=37, ]; -E: 15 183 [weight=50, ]; -E: 16 19 [weight=10, ]; -E: 16 173 [weight=20, ]; +E: 9 12 [weight=14, ]; +E: 9 80 [weight=6, ]; +E: 9 180 [weight=3, ]; +E: 9 181 [weight=1, ]; +E: 9 182 [weight=10, ]; +E: 10 12 [weight=12, ]; +E: 10 144 [weight=12, ]; +E: 10 180 [weight=3, ]; +E: 11 12 [weight=6, ]; +E: 11 172 [weight=6, ]; +E: 12 180 [weight=1, ]; +E: 12 181 [weight=1, ]; +E: 12 182 [weight=3, ]; +E: 13 18 [weight=30, ]; +E: 13 127 [weight=1, ]; +E: 13 130 [weight=17, ]; +E: 13 168 [weight=3, ]; +E: 13 172 [weight=26, ]; +E: 13 180 [weight=17, ]; +E: 13 181 [weight=27, ]; +E: 13 182 [weight=42, ]; +E: 14 18 [weight=30, ]; +E: 14 127 [weight=1, ]; +E: 14 130 [weight=11, ]; +E: 14 168 [weight=3, ]; +E: 14 172 [weight=18, ]; +E: 14 180 [weight=16, ]; +E: 14 181 [weight=37, ]; +E: 14 182 [weight=50, ]; +E: 15 18 [weight=10, ]; +E: 15 172 [weight=20, ]; +E: 15 180 [weight=4, ]; +E: 15 181 [weight=4, ]; +E: 15 182 [weight=11, ]; +E: 16 17 [weight=13, ]; +E: 16 18 [weight=13, ]; +E: 16 168 [weight=13, ]; +E: 16 180 [weight=10, ]; E: 16 181 [weight=4, ]; -E: 16 182 [weight=4, ]; -E: 16 183 [weight=11, ]; -E: 17 18 [weight=13, ]; -E: 17 19 [weight=13, ]; -E: 17 169 [weight=13, ]; -E: 17 181 [weight=10, ]; -E: 17 182 [weight=4, ]; -E: 17 183 [weight=30, ]; -E: 18 182 [weight=1, ]; -E: 18 183 [weight=10, ]; -E: 19 181 [weight=1, ]; -E: 19 182 [weight=2, ]; -E: 19 183 [weight=10, ]; -E: 20 27 [weight=6, ]; -E: 20 149 [weight=1, ]; -E: 20 169 [weight=4, ]; -E: 20 170 [weight=16, ]; -E: 20 183 [weight=12, ]; -E: 21 27 [weight=4, ]; -E: 21 170 [weight=18, ]; -E: 21 181 [weight=3, ]; -E: 21 183 [weight=8, ]; -E: 22 27 [weight=4, ]; -E: 22 148 [weight=1, ]; -E: 22 169 [weight=2, ]; -E: 22 170 [weight=3, ]; -E: 22 183 [weight=6, ]; -E: 23 27 [weight=4, ]; -E: 23 148 [weight=1, ]; -E: 23 169 [weight=2, ]; -E: 23 170 [weight=3, ]; -E: 23 183 [weight=6, ]; -E: 24 27 [weight=6, ]; -E: 24 170 [weight=1, ]; -E: 24 183 [weight=6, ]; -E: 25 27 [weight=4, ]; -E: 25 163 [weight=1, ]; -E: 25 170 [weight=1, ]; -E: 25 181 [weight=2, ]; -E: 25 183 [weight=4, ]; -E: 26 27 [weight=2, ]; -E: 26 170 [weight=1, ]; -E: 26 183 [weight=2, ]; -E: 27 170 [weight=2, ]; -E: 27 183 [weight=4, ]; -E: 28 34 [weight=5, ]; -E: 28 173 [weight=1, ]; -E: 28 179 [weight=1, ]; -E: 28 181 [weight=2, ]; -E: 28 182 [weight=11, ]; -E: 28 183 [weight=9, ]; -E: 29 34 [weight=4, ]; -E: 29 173 [weight=8, ]; -E: 29 181 [weight=6, ]; -E: 29 183 [weight=4, ]; -E: 30 34 [weight=4, ]; -E: 30 173 [weight=8, ]; -E: 30 181 [weight=3, ]; -E: 30 183 [weight=4, ]; -E: 31 34 [weight=4, ]; -E: 31 173 [weight=14, ]; -E: 31 181 [weight=6, ]; -E: 31 183 [weight=4, ]; -E: 32 34 [weight=6, ]; -E: 32 173 [weight=7, ]; -E: 32 183 [weight=6, ]; -E: 33 34 [weight=2, ]; -E: 33 173 [weight=1, ]; -E: 33 183 [weight=2, ]; -E: 34 173 [weight=2, ]; -E: 34 183 [weight=4, ]; -E: 35 39 [weight=10, ]; +E: 16 182 [weight=30, ]; +E: 17 181 [weight=1, ]; +E: 17 182 [weight=10, ]; +E: 18 180 [weight=1, ]; +E: 18 181 [weight=2, ]; +E: 18 182 [weight=10, ]; +E: 19 26 [weight=6, ]; +E: 19 148 [weight=1, ]; +E: 19 168 [weight=4, ]; +E: 19 169 [weight=16, ]; +E: 19 182 [weight=12, ]; +E: 20 26 [weight=4, ]; +E: 20 169 [weight=18, ]; +E: 20 180 [weight=3, ]; +E: 20 182 [weight=8, ]; +E: 21 26 [weight=4, ]; +E: 21 147 [weight=1, ]; +E: 21 168 [weight=2, ]; +E: 21 169 [weight=3, ]; +E: 21 182 [weight=6, ]; +E: 22 26 [weight=4, ]; +E: 22 147 [weight=1, ]; +E: 22 168 [weight=2, ]; +E: 22 169 [weight=3, ]; +E: 22 182 [weight=6, ]; +E: 23 26 [weight=6, ]; +E: 23 169 [weight=1, ]; +E: 23 182 [weight=6, ]; +E: 24 26 [weight=4, ]; +E: 24 162 [weight=1, ]; +E: 24 169 [weight=1, ]; +E: 24 180 [weight=2, ]; +E: 24 182 [weight=4, ]; +E: 25 26 [weight=2, ]; +E: 25 169 [weight=1, ]; +E: 25 182 [weight=2, ]; +E: 26 169 [weight=2, ]; +E: 26 182 [weight=4, ]; +E: 27 33 [weight=5, ]; +E: 27 172 [weight=1, ]; +E: 27 178 [weight=1, ]; +E: 27 180 [weight=2, ]; +E: 27 181 [weight=11, ]; +E: 27 182 [weight=9, ]; +E: 28 33 [weight=4, ]; +E: 28 172 [weight=8, ]; +E: 28 180 [weight=6, ]; +E: 28 182 [weight=4, ]; +E: 29 33 [weight=4, ]; +E: 29 172 [weight=8, ]; +E: 29 180 [weight=3, ]; +E: 29 182 [weight=4, ]; +E: 30 33 [weight=4, ]; +E: 30 172 [weight=14, ]; +E: 30 180 [weight=6, ]; +E: 30 182 [weight=4, ]; +E: 31 33 [weight=6, ]; +E: 31 172 [weight=7, ]; +E: 31 182 [weight=6, ]; +E: 32 33 [weight=2, ]; +E: 32 172 [weight=1, ]; +E: 32 182 [weight=2, ]; +E: 33 172 [weight=2, ]; +E: 33 182 [weight=4, ]; +E: 34 38 [weight=10, ]; +E: 34 77 [weight=1, ]; +E: 34 80 [weight=4, ]; +E: 34 149 [weight=1, ]; +E: 34 168 [weight=1, ]; +E: 34 172 [weight=31, ]; +E: 34 178 [weight=1, ]; +E: 34 180 [weight=2, ]; +E: 34 181 [weight=2, ]; +E: 34 182 [weight=11, ]; +E: 35 36 [weight=1, ]; +E: 35 38 [weight=12, ]; E: 35 78 [weight=1, ]; -E: 35 81 [weight=4, ]; -E: 35 150 [weight=1, ]; -E: 35 169 [weight=1, ]; -E: 35 173 [weight=31, ]; -E: 35 179 [weight=1, ]; +E: 35 80 [weight=10, ]; +E: 35 148 [weight=1, ]; +E: 35 168 [weight=1, ]; +E: 35 169 [weight=85, ]; +E: 35 178 [weight=1, ]; +E: 35 180 [weight=2, ]; E: 35 181 [weight=2, ]; -E: 35 182 [weight=2, ]; -E: 35 183 [weight=11, ]; +E: 35 182 [weight=6, ]; E: 36 37 [weight=1, ]; -E: 36 39 [weight=12, ]; -E: 36 79 [weight=1, ]; -E: 36 81 [weight=10, ]; -E: 36 149 [weight=1, ]; -E: 36 169 [weight=1, ]; -E: 36 170 [weight=85, ]; -E: 36 179 [weight=1, ]; +E: 36 38 [weight=9, ]; +E: 36 80 [weight=5, ]; +E: 36 147 [weight=1, ]; +E: 36 169 [weight=27, ]; +E: 36 178 [weight=1, ]; +E: 36 180 [weight=2, ]; E: 36 181 [weight=2, ]; -E: 36 182 [weight=2, ]; -E: 36 183 [weight=6, ]; -E: 37 38 [weight=1, ]; -E: 37 39 [weight=9, ]; -E: 37 81 [weight=5, ]; -E: 37 148 [weight=1, ]; -E: 37 170 [weight=27, ]; -E: 37 179 [weight=1, ]; +E: 36 182 [weight=11, ]; +E: 37 80 [weight=8, ]; +E: 37 169 [weight=16, ]; +E: 37 178 [weight=1, ]; +E: 37 180 [weight=2, ]; E: 37 181 [weight=2, ]; -E: 37 182 [weight=2, ]; -E: 37 183 [weight=11, ]; -E: 38 81 [weight=8, ]; -E: 38 170 [weight=16, ]; -E: 38 179 [weight=1, ]; -E: 38 181 [weight=2, ]; -E: 38 182 [weight=2, ]; -E: 38 183 [weight=4, ]; -E: 39 81 [weight=1, ]; -E: 39 169 [weight=1, ]; -E: 39 182 [weight=1, ]; -E: 39 183 [weight=12, ]; -E: 40 46 [weight=13, ]; -E: 40 145 [weight=39, ]; -E: 40 173 [weight=24, ]; -E: 40 179 [weight=1, ]; -E: 40 181 [weight=25, ]; -E: 40 182 [weight=25, ]; -E: 40 183 [weight=15, ]; -E: 41 46 [weight=8, ]; -E: 41 173 [weight=24, ]; -E: 41 179 [weight=1, ]; -E: 41 181 [weight=8, ]; -E: 41 182 [weight=4, ]; -E: 41 183 [weight=13, ]; -E: 42 46 [weight=10, ]; -E: 42 170 [weight=21, ]; -E: 42 179 [weight=1, ]; -E: 42 181 [weight=5, ]; -E: 42 182 [weight=3, ]; -E: 42 183 [weight=13, ]; -E: 43 46 [weight=10, ]; -E: 43 170 [weight=21, ]; -E: 43 179 [weight=1, ]; -E: 43 181 [weight=7, ]; -E: 43 182 [weight=3, ]; -E: 43 183 [weight=13, ]; -E: 44 46 [weight=10, ]; -E: 44 52 [weight=10, ]; -E: 44 173 [weight=30, ]; -E: 44 179 [weight=1, ]; -E: 44 181 [weight=23, ]; -E: 44 182 [weight=23, ]; -E: 44 183 [weight=94, ]; -E: 45 46 [weight=16, ]; -E: 45 52 [weight=7, ]; -E: 45 179 [weight=1, ]; -E: 45 181 [weight=17, ]; -E: 45 182 [weight=3, ]; -E: 45 183 [weight=73, ]; -E: 46 181 [weight=1, ]; -E: 46 182 [weight=2, ]; -E: 46 183 [weight=16, ]; -E: 47 52 [weight=7, ]; -E: 47 173 [weight=22, ]; -E: 47 179 [weight=1, ]; -E: 47 181 [weight=8, ]; -E: 47 182 [weight=2, ]; -E: 47 183 [weight=52, ]; -E: 48 52 [weight=7, ]; -E: 48 173 [weight=22, ]; -E: 48 179 [weight=1, ]; -E: 48 181 [weight=8, ]; -E: 48 182 [weight=2, ]; -E: 48 183 [weight=52, ]; -E: 49 52 [weight=32, ]; -E: 49 145 [weight=66, ]; -E: 49 179 [weight=1, ]; -E: 49 181 [weight=39, ]; -E: 49 182 [weight=15, ]; -E: 49 183 [weight=196, ]; -E: 50 52 [weight=8, ]; -E: 50 170 [weight=28, ]; -E: 50 179 [weight=1, ]; -E: 50 181 [weight=10, ]; -E: 50 182 [weight=2, ]; -E: 50 183 [weight=64, ]; -E: 51 52 [weight=8, ]; -E: 51 170 [weight=28, ]; -E: 51 179 [weight=1, ]; -E: 51 181 [weight=10, ]; -E: 51 182 [weight=2, ]; -E: 51 183 [weight=64, ]; +E: 37 182 [weight=4, ]; +E: 38 80 [weight=1, ]; +E: 38 168 [weight=1, ]; +E: 38 181 [weight=1, ]; +E: 38 182 [weight=12, ]; +E: 39 45 [weight=13, ]; +E: 39 144 [weight=39, ]; +E: 39 172 [weight=24, ]; +E: 39 178 [weight=1, ]; +E: 39 180 [weight=25, ]; +E: 39 181 [weight=25, ]; +E: 39 182 [weight=15, ]; +E: 40 45 [weight=8, ]; +E: 40 172 [weight=24, ]; +E: 40 178 [weight=1, ]; +E: 40 180 [weight=8, ]; +E: 40 181 [weight=4, ]; +E: 40 182 [weight=13, ]; +E: 41 45 [weight=10, ]; +E: 41 169 [weight=21, ]; +E: 41 178 [weight=1, ]; +E: 41 180 [weight=5, ]; +E: 41 181 [weight=3, ]; +E: 41 182 [weight=13, ]; +E: 42 45 [weight=10, ]; +E: 42 169 [weight=21, ]; +E: 42 178 [weight=1, ]; +E: 42 180 [weight=7, ]; +E: 42 181 [weight=3, ]; +E: 42 182 [weight=13, ]; +E: 43 45 [weight=10, ]; +E: 43 51 [weight=10, ]; +E: 43 172 [weight=30, ]; +E: 43 178 [weight=1, ]; +E: 43 180 [weight=23, ]; +E: 43 181 [weight=23, ]; +E: 43 182 [weight=94, ]; +E: 44 45 [weight=16, ]; +E: 44 51 [weight=7, ]; +E: 44 178 [weight=1, ]; +E: 44 180 [weight=17, ]; +E: 44 181 [weight=3, ]; +E: 44 182 [weight=73, ]; +E: 45 180 [weight=1, ]; +E: 45 181 [weight=2, ]; +E: 45 182 [weight=16, ]; +E: 46 51 [weight=7, ]; +E: 46 172 [weight=22, ]; +E: 46 178 [weight=1, ]; +E: 46 180 [weight=8, ]; +E: 46 181 [weight=2, ]; +E: 46 182 [weight=52, ]; +E: 47 51 [weight=7, ]; +E: 47 172 [weight=22, ]; +E: 47 178 [weight=1, ]; +E: 47 180 [weight=8, ]; +E: 47 181 [weight=2, ]; +E: 47 182 [weight=52, ]; +E: 48 51 [weight=32, ]; +E: 48 144 [weight=66, ]; +E: 48 178 [weight=1, ]; +E: 48 180 [weight=39, ]; +E: 48 181 [weight=15, ]; +E: 48 182 [weight=196, ]; +E: 49 51 [weight=8, ]; +E: 49 169 [weight=28, ]; +E: 49 178 [weight=1, ]; +E: 49 180 [weight=10, ]; +E: 49 181 [weight=2, ]; +E: 49 182 [weight=64, ]; +E: 50 51 [weight=8, ]; +E: 50 169 [weight=28, ]; +E: 50 178 [weight=1, ]; +E: 50 180 [weight=10, ]; +E: 50 181 [weight=2, ]; +E: 50 182 [weight=64, ]; +E: 51 180 [weight=2, ]; +E: 51 181 [weight=2, ]; +E: 51 182 [weight=24, ]; +E: 52 180 [weight=2, ]; E: 52 181 [weight=2, ]; -E: 52 182 [weight=2, ]; -E: 52 183 [weight=24, ]; -E: 53 181 [weight=2, ]; -E: 53 182 [weight=2, ]; -E: 53 183 [weight=26, ]; -E: 54 183 [weight=6, ]; -E: 55 56 [weight=49, ]; -E: 55 170 [weight=107, ]; -E: 55 179 [weight=1, ]; -E: 55 181 [weight=5, ]; -E: 55 182 [weight=2, ]; -E: 55 183 [weight=6, ]; -E: 56 181 [weight=1, ]; -E: 56 182 [weight=1, ]; -E: 56 183 [weight=10, ]; -E: 57 58 [weight=25, ]; -E: 57 170 [weight=19, ]; -E: 57 179 [weight=1, ]; -E: 57 181 [weight=2, ]; -E: 57 182 [weight=2, ]; -E: 57 183 [weight=4, ]; -E: 58 183 [weight=6, ]; -E: 59 61 [weight=13, ]; -E: 59 145 [weight=11, ]; -E: 59 173 [weight=24, ]; -E: 59 179 [weight=1, ]; -E: 59 181 [weight=3, ]; -E: 59 182 [weight=19, ]; -E: 59 183 [weight=4, ]; -E: 60 61 [weight=37, ]; -E: 60 170 [weight=55, ]; -E: 60 179 [weight=1, ]; -E: 60 181 [weight=2, ]; -E: 60 182 [weight=2, ]; -E: 60 183 [weight=4, ]; -E: 61 183 [weight=6, ]; -E: 62 73 [weight=1, ]; -E: 62 81 [weight=1, ]; -E: 62 181 [weight=2, ]; -E: 62 182 [weight=2, ]; -E: 62 183 [weight=21, ]; -E: 63 66 [weight=18, ]; -E: 63 69 [weight=13, ]; -E: 63 179 [weight=1, ]; -E: 63 181 [weight=4, ]; -E: 63 182 [weight=3, ]; -E: 63 183 [weight=7, ]; -E: 64 65 [weight=1, ]; -E: 64 66 [weight=10, ]; -E: 64 69 [weight=7, ]; -E: 64 121 [weight=9, ]; -E: 64 169 [weight=1, ]; -E: 64 179 [weight=1, ]; -E: 64 181 [weight=6, ]; -E: 64 182 [weight=6, ]; -E: 64 183 [weight=4, ]; -E: 65 66 [weight=30, ]; -E: 65 169 [weight=11, ]; -E: 65 179 [weight=1, ]; -E: 65 181 [weight=2, ]; -E: 65 182 [weight=2, ]; -E: 65 183 [weight=11, ]; -E: 66 183 [weight=6, ]; -E: 67 69 [weight=8, ]; -E: 67 173 [weight=12, ]; -E: 67 179 [weight=1, ]; +E: 52 182 [weight=26, ]; +E: 53 182 [weight=6, ]; +E: 54 55 [weight=49, ]; +E: 54 169 [weight=107, ]; +E: 54 178 [weight=1, ]; +E: 54 180 [weight=5, ]; +E: 54 181 [weight=2, ]; +E: 54 182 [weight=6, ]; +E: 55 180 [weight=1, ]; +E: 55 181 [weight=1, ]; +E: 55 182 [weight=10, ]; +E: 56 57 [weight=25, ]; +E: 56 169 [weight=19, ]; +E: 56 178 [weight=1, ]; +E: 56 180 [weight=2, ]; +E: 56 181 [weight=2, ]; +E: 56 182 [weight=4, ]; +E: 57 182 [weight=6, ]; +E: 58 60 [weight=13, ]; +E: 58 144 [weight=11, ]; +E: 58 172 [weight=24, ]; +E: 58 178 [weight=1, ]; +E: 58 180 [weight=3, ]; +E: 58 181 [weight=19, ]; +E: 58 182 [weight=4, ]; +E: 59 60 [weight=37, ]; +E: 59 169 [weight=55, ]; +E: 59 178 [weight=1, ]; +E: 59 180 [weight=2, ]; +E: 59 181 [weight=2, ]; +E: 59 182 [weight=4, ]; +E: 60 182 [weight=6, ]; +E: 61 72 [weight=1, ]; +E: 61 80 [weight=1, ]; +E: 61 180 [weight=2, ]; +E: 61 181 [weight=2, ]; +E: 61 182 [weight=21, ]; +E: 62 65 [weight=18, ]; +E: 62 68 [weight=13, ]; +E: 62 178 [weight=1, ]; +E: 62 180 [weight=4, ]; +E: 62 181 [weight=3, ]; +E: 62 182 [weight=7, ]; +E: 63 64 [weight=1, ]; +E: 63 65 [weight=10, ]; +E: 63 68 [weight=7, ]; +E: 63 120 [weight=9, ]; +E: 63 168 [weight=1, ]; +E: 63 178 [weight=1, ]; +E: 63 180 [weight=6, ]; +E: 63 181 [weight=6, ]; +E: 63 182 [weight=4, ]; +E: 64 65 [weight=30, ]; +E: 64 168 [weight=11, ]; +E: 64 178 [weight=1, ]; +E: 64 180 [weight=2, ]; +E: 64 181 [weight=2, ]; +E: 64 182 [weight=11, ]; +E: 65 182 [weight=6, ]; +E: 66 68 [weight=8, ]; +E: 66 172 [weight=12, ]; +E: 66 178 [weight=1, ]; +E: 66 180 [weight=2, ]; +E: 66 181 [weight=2, ]; +E: 66 182 [weight=7, ]; +E: 67 68 [weight=16, ]; +E: 67 168 [weight=5, ]; +E: 67 178 [weight=1, ]; +E: 67 180 [weight=2, ]; E: 67 181 [weight=2, ]; -E: 67 182 [weight=2, ]; -E: 67 183 [weight=7, ]; -E: 68 69 [weight=16, ]; -E: 68 169 [weight=5, ]; -E: 68 179 [weight=1, ]; -E: 68 181 [weight=2, ]; -E: 68 182 [weight=2, ]; -E: 68 183 [weight=10, ]; -E: 69 183 [weight=6, ]; -E: 70 81 [weight=16, ]; -E: 70 179 [weight=1, ]; -E: 70 181 [weight=7, ]; -E: 70 182 [weight=3, ]; -E: 70 183 [weight=15, ]; -E: 71 81 [weight=20, ]; -E: 71 179 [weight=1, ]; -E: 71 181 [weight=5, ]; -E: 71 182 [weight=3, ]; -E: 71 183 [weight=14, ]; -E: 72 73 [weight=30, ]; -E: 72 148 [weight=1, ]; -E: 72 149 [weight=1, ]; -E: 72 169 [weight=3, ]; -E: 72 170 [weight=123, ]; -E: 72 179 [weight=1, ]; -E: 72 181 [weight=2, ]; -E: 72 182 [weight=2, ]; -E: 72 183 [weight=6, ]; -E: 73 169 [weight=1, ]; -E: 73 182 [weight=1, ]; -E: 73 183 [weight=12, ]; -E: 74 81 [weight=24, ]; -E: 74 103 [weight=1, ]; -E: 74 104 [weight=1, ]; -E: 74 105 [weight=1, ]; -E: 74 106 [weight=1, ]; -E: 74 107 [weight=1, ]; -E: 74 108 [weight=14, ]; -E: 74 181 [weight=6, ]; -E: 74 182 [weight=2, ]; -E: 74 183 [weight=12, ]; -E: 75 76 [weight=1, ]; -E: 75 81 [weight=19, ]; -E: 75 121 [weight=18, ]; -E: 75 169 [weight=6, ]; -E: 75 179 [weight=1, ]; -E: 75 181 [weight=9, ]; -E: 75 182 [weight=10, ]; -E: 75 183 [weight=17, ]; -E: 76 81 [weight=23, ]; -E: 76 169 [weight=14, ]; -E: 76 179 [weight=1, ]; -E: 76 181 [weight=5, ]; -E: 76 182 [weight=2, ]; -E: 76 183 [weight=21, ]; -E: 77 81 [weight=8, ]; -E: 77 145 [weight=21, ]; -E: 77 179 [weight=1, ]; -E: 77 181 [weight=5, ]; -E: 77 182 [weight=6, ]; -E: 77 183 [weight=4, ]; -E: 78 81 [weight=6, ]; -E: 78 173 [weight=12, ]; -E: 78 179 [weight=1, ]; -E: 78 181 [weight=2, ]; -E: 78 182 [weight=2, ]; -E: 78 183 [weight=4, ]; -E: 79 81 [weight=50, ]; -E: 79 170 [weight=125, ]; -E: 79 179 [weight=1, ]; -E: 79 181 [weight=21, ]; -E: 79 182 [weight=13, ]; -E: 79 183 [weight=4, ]; -E: 80 81 [weight=8, ]; -E: 80 170 [weight=16, ]; -E: 80 179 [weight=1, ]; -E: 80 181 [weight=2, ]; -E: 80 182 [weight=2, ]; -E: 80 183 [weight=4, ]; -E: 81 181 [weight=1, ]; -E: 81 182 [weight=1, ]; -E: 81 183 [weight=9, ]; -E: 82 168 [weight=2, ]; -E: 82 180 [weight=1, ]; -E: 82 181 [weight=70, ]; -E: 82 182 [weight=14, ]; -E: 82 183 [weight=116, ]; -E: 83 87 [weight=1, ]; -E: 83 108 [weight=12, ]; -E: 83 157 [weight=2, ]; -E: 83 169 [weight=11, ]; -E: 83 179 [weight=1, ]; +E: 67 182 [weight=10, ]; +E: 68 182 [weight=6, ]; +E: 69 80 [weight=16, ]; +E: 69 178 [weight=1, ]; +E: 69 180 [weight=7, ]; +E: 69 181 [weight=3, ]; +E: 69 182 [weight=15, ]; +E: 70 80 [weight=20, ]; +E: 70 178 [weight=1, ]; +E: 70 180 [weight=5, ]; +E: 70 181 [weight=3, ]; +E: 70 182 [weight=14, ]; +E: 71 72 [weight=30, ]; +E: 71 147 [weight=1, ]; +E: 71 148 [weight=1, ]; +E: 71 168 [weight=3, ]; +E: 71 169 [weight=123, ]; +E: 71 178 [weight=1, ]; +E: 71 180 [weight=2, ]; +E: 71 181 [weight=2, ]; +E: 71 182 [weight=6, ]; +E: 72 168 [weight=1, ]; +E: 72 181 [weight=1, ]; +E: 72 182 [weight=12, ]; +E: 73 80 [weight=24, ]; +E: 73 102 [weight=1, ]; +E: 73 103 [weight=1, ]; +E: 73 104 [weight=1, ]; +E: 73 105 [weight=1, ]; +E: 73 106 [weight=1, ]; +E: 73 107 [weight=14, ]; +E: 73 180 [weight=6, ]; +E: 73 181 [weight=2, ]; +E: 73 182 [weight=12, ]; +E: 74 75 [weight=1, ]; +E: 74 80 [weight=19, ]; +E: 74 120 [weight=18, ]; +E: 74 168 [weight=6, ]; +E: 74 178 [weight=1, ]; +E: 74 180 [weight=9, ]; +E: 74 181 [weight=10, ]; +E: 74 182 [weight=17, ]; +E: 75 80 [weight=23, ]; +E: 75 168 [weight=14, ]; +E: 75 178 [weight=1, ]; +E: 75 180 [weight=5, ]; +E: 75 181 [weight=2, ]; +E: 75 182 [weight=21, ]; +E: 76 80 [weight=8, ]; +E: 76 144 [weight=21, ]; +E: 76 178 [weight=1, ]; +E: 76 180 [weight=5, ]; +E: 76 181 [weight=6, ]; +E: 76 182 [weight=4, ]; +E: 77 80 [weight=6, ]; +E: 77 172 [weight=12, ]; +E: 77 178 [weight=1, ]; +E: 77 180 [weight=2, ]; +E: 77 181 [weight=2, ]; +E: 77 182 [weight=4, ]; +E: 78 80 [weight=50, ]; +E: 78 169 [weight=125, ]; +E: 78 178 [weight=1, ]; +E: 78 180 [weight=21, ]; +E: 78 181 [weight=13, ]; +E: 78 182 [weight=4, ]; +E: 79 80 [weight=8, ]; +E: 79 169 [weight=16, ]; +E: 79 178 [weight=1, ]; +E: 79 180 [weight=2, ]; +E: 79 181 [weight=2, ]; +E: 79 182 [weight=4, ]; +E: 80 180 [weight=1, ]; +E: 80 181 [weight=1, ]; +E: 80 182 [weight=9, ]; +E: 81 167 [weight=2, ]; +E: 81 179 [weight=1, ]; +E: 81 180 [weight=70, ]; +E: 81 181 [weight=14, ]; +E: 81 182 [weight=116, ]; +E: 82 86 [weight=1, ]; +E: 82 107 [weight=12, ]; +E: 82 156 [weight=2, ]; +E: 82 168 [weight=11, ]; +E: 82 178 [weight=1, ]; +E: 82 180 [weight=2, ]; +E: 82 181 [weight=3, ]; +E: 82 182 [weight=18, ]; +E: 83 85 [weight=1, ]; +E: 83 107 [weight=12, ]; +E: 83 168 [weight=14, ]; +E: 83 178 [weight=1, ]; +E: 83 180 [weight=4, ]; E: 83 181 [weight=2, ]; -E: 83 182 [weight=3, ]; -E: 83 183 [weight=18, ]; +E: 83 182 [weight=18, ]; E: 84 86 [weight=1, ]; -E: 84 108 [weight=12, ]; -E: 84 169 [weight=14, ]; -E: 84 179 [weight=1, ]; -E: 84 181 [weight=4, ]; -E: 84 182 [weight=2, ]; -E: 84 183 [weight=18, ]; -E: 85 87 [weight=1, ]; -E: 85 108 [weight=3, ]; -E: 85 169 [weight=3, ]; -E: 85 181 [weight=4, ]; -E: 85 182 [weight=1, ]; -E: 85 183 [weight=6, ]; +E: 84 107 [weight=3, ]; +E: 84 168 [weight=3, ]; +E: 84 180 [weight=4, ]; +E: 84 181 [weight=1, ]; +E: 84 182 [weight=6, ]; +E: 85 86 [weight=1, ]; +E: 85 107 [weight=3, ]; +E: 85 180 [weight=4, ]; +E: 85 181 [weight=2, ]; +E: 85 182 [weight=4, ]; E: 86 87 [weight=1, ]; -E: 86 108 [weight=3, ]; -E: 86 181 [weight=4, ]; -E: 86 182 [weight=2, ]; -E: 86 183 [weight=4, ]; -E: 87 88 [weight=1, ]; -E: 87 91 [weight=6, ]; -E: 87 96 [weight=1, ]; -E: 87 98 [weight=23, ]; -E: 87 99 [weight=6, ]; -E: 87 104 [weight=10, ]; -E: 87 105 [weight=3, ]; -E: 87 106 [weight=15, ]; -E: 87 108 [weight=191, ]; -E: 87 148 [weight=1, ]; -E: 87 161 [weight=1, ]; -E: 87 169 [weight=631, ]; -E: 87 170 [weight=4, ]; -E: 87 181 [weight=975, ]; -E: 87 182 [weight=35, ]; -E: 87 183 [weight=914, ]; -E: 88 99 [weight=6, ]; -E: 88 103 [weight=1, ]; +E: 86 90 [weight=6, ]; +E: 86 95 [weight=1, ]; +E: 86 97 [weight=23, ]; +E: 86 98 [weight=6, ]; +E: 86 103 [weight=10, ]; +E: 86 104 [weight=3, ]; +E: 86 105 [weight=15, ]; +E: 86 107 [weight=191, ]; +E: 86 147 [weight=1, ]; +E: 86 160 [weight=1, ]; +E: 86 168 [weight=631, ]; +E: 86 169 [weight=4, ]; +E: 86 180 [weight=975, ]; +E: 86 181 [weight=35, ]; +E: 86 182 [weight=914, ]; +E: 87 98 [weight=6, ]; +E: 87 102 [weight=1, ]; +E: 87 104 [weight=1, ]; +E: 87 107 [weight=13, ]; +E: 87 178 [weight=2, ]; +E: 87 180 [weight=23, ]; +E: 87 181 [weight=4, ]; +E: 87 182 [weight=34, ]; +E: 88 91 [weight=1, ]; +E: 88 96 [weight=1, ]; +E: 88 97 [weight=2, ]; +E: 88 98 [weight=1, ]; E: 88 105 [weight=1, ]; -E: 88 108 [weight=13, ]; -E: 88 179 [weight=2, ]; -E: 88 181 [weight=23, ]; +E: 88 107 [weight=6, ]; +E: 88 120 [weight=12, ]; +E: 88 168 [weight=3, ]; +E: 88 178 [weight=1, ]; +E: 88 180 [weight=12, ]; +E: 88 181 [weight=7, ]; E: 88 182 [weight=4, ]; -E: 88 183 [weight=34, ]; -E: 89 92 [weight=1, ]; -E: 89 97 [weight=1, ]; -E: 89 98 [weight=2, ]; -E: 89 99 [weight=1, ]; -E: 89 106 [weight=1, ]; -E: 89 108 [weight=6, ]; -E: 89 121 [weight=12, ]; -E: 89 169 [weight=3, ]; -E: 89 179 [weight=1, ]; -E: 89 181 [weight=12, ]; -E: 89 182 [weight=7, ]; -E: 89 183 [weight=4, ]; -E: 90 103 [weight=1, ]; -E: 90 108 [weight=5, ]; -E: 90 173 [weight=24, ]; -E: 90 181 [weight=6, ]; -E: 90 182 [weight=2, ]; -E: 90 183 [weight=12, ]; -E: 91 99 [weight=1, ]; -E: 91 104 [weight=2, ]; -E: 91 105 [weight=1, ]; -E: 91 106 [weight=3, ]; -E: 91 108 [weight=12, ]; -E: 91 169 [weight=22, ]; -E: 91 179 [weight=1, ]; -E: 91 181 [weight=27, ]; -E: 91 182 [weight=2, ]; -E: 91 183 [weight=19, ]; -E: 92 97 [weight=3, ]; -E: 92 98 [weight=3, ]; -E: 92 99 [weight=2, ]; +E: 89 102 [weight=1, ]; +E: 89 107 [weight=5, ]; +E: 89 172 [weight=24, ]; +E: 89 180 [weight=6, ]; +E: 89 181 [weight=2, ]; +E: 89 182 [weight=12, ]; +E: 90 98 [weight=1, ]; +E: 90 103 [weight=2, ]; +E: 90 104 [weight=1, ]; +E: 90 105 [weight=3, ]; +E: 90 107 [weight=12, ]; +E: 90 168 [weight=22, ]; +E: 90 178 [weight=1, ]; +E: 90 180 [weight=27, ]; +E: 90 181 [weight=2, ]; +E: 90 182 [weight=19, ]; +E: 91 96 [weight=3, ]; +E: 91 97 [weight=3, ]; +E: 91 98 [weight=2, ]; +E: 91 104 [weight=1, ]; +E: 91 105 [weight=3, ]; +E: 91 107 [weight=11, ]; +E: 91 153 [weight=1, ]; +E: 91 156 [weight=2, ]; +E: 91 168 [weight=43, ]; +E: 91 178 [weight=2, ]; +E: 91 180 [weight=42, ]; +E: 91 181 [weight=6, ]; +E: 91 182 [weight=18, ]; +E: 92 93 [weight=1, ]; +E: 92 94 [weight=1, ]; +E: 92 96 [weight=2, ]; +E: 92 97 [weight=2, ]; +E: 92 102 [weight=1, ]; +E: 92 104 [weight=1, ]; E: 92 105 [weight=1, ]; -E: 92 106 [weight=3, ]; -E: 92 108 [weight=11, ]; -E: 92 154 [weight=1, ]; -E: 92 157 [weight=2, ]; -E: 92 169 [weight=43, ]; -E: 92 179 [weight=2, ]; -E: 92 181 [weight=42, ]; -E: 92 182 [weight=6, ]; -E: 92 183 [weight=18, ]; -E: 93 94 [weight=1, ]; -E: 93 95 [weight=1, ]; -E: 93 97 [weight=2, ]; -E: 93 98 [weight=2, ]; -E: 93 103 [weight=1, ]; +E: 92 107 [weight=22, ]; +E: 92 153 [weight=10, ]; +E: 92 168 [weight=53, ]; +E: 92 180 [weight=66, ]; +E: 92 182 [weight=36, ]; E: 93 105 [weight=1, ]; -E: 93 106 [weight=1, ]; -E: 93 108 [weight=22, ]; -E: 93 154 [weight=10, ]; -E: 93 169 [weight=53, ]; -E: 93 181 [weight=66, ]; -E: 93 183 [weight=36, ]; -E: 94 106 [weight=1, ]; -E: 94 108 [weight=7, ]; -E: 94 154 [weight=2, ]; -E: 94 169 [weight=14, ]; -E: 94 179 [weight=1, ]; -E: 94 181 [weight=6, ]; -E: 94 183 [weight=12, ]; -E: 95 97 [weight=1, ]; -E: 95 98 [weight=2, ]; -E: 95 99 [weight=1, ]; -E: 95 103 [weight=1, ]; -E: 95 105 [weight=1, ]; -E: 95 106 [weight=1, ]; -E: 95 108 [weight=14, ]; -E: 95 169 [weight=28, ]; -E: 95 181 [weight=10, ]; -E: 95 182 [weight=2, ]; -E: 95 183 [weight=14, ]; +E: 93 107 [weight=7, ]; +E: 93 153 [weight=2, ]; +E: 93 168 [weight=14, ]; +E: 93 178 [weight=1, ]; +E: 93 180 [weight=6, ]; +E: 93 182 [weight=12, ]; +E: 94 96 [weight=1, ]; +E: 94 97 [weight=2, ]; +E: 94 98 [weight=1, ]; +E: 94 102 [weight=1, ]; +E: 94 104 [weight=1, ]; +E: 94 105 [weight=1, ]; +E: 94 107 [weight=14, ]; +E: 94 168 [weight=28, ]; +E: 94 180 [weight=10, ]; +E: 94 181 [weight=2, ]; +E: 94 182 [weight=14, ]; +E: 95 102 [weight=1, ]; +E: 95 107 [weight=5, ]; +E: 95 169 [weight=40, ]; +E: 95 180 [weight=6, ]; +E: 95 181 [weight=2, ]; +E: 95 182 [weight=12, ]; E: 96 103 [weight=1, ]; -E: 96 108 [weight=5, ]; -E: 96 170 [weight=40, ]; -E: 96 181 [weight=6, ]; -E: 96 182 [weight=2, ]; -E: 96 183 [weight=12, ]; +E: 96 107 [weight=3, ]; +E: 96 182 [weight=3, ]; +E: 97 102 [weight=1, ]; +E: 97 103 [weight=1, ]; E: 97 104 [weight=1, ]; -E: 97 108 [weight=3, ]; -E: 97 183 [weight=3, ]; -E: 98 103 [weight=1, ]; -E: 98 104 [weight=1, ]; +E: 97 105 [weight=1, ]; +E: 97 106 [weight=1, ]; +E: 97 107 [weight=10, ]; +E: 97 182 [weight=12, ]; E: 98 105 [weight=1, ]; E: 98 106 [weight=1, ]; -E: 98 107 [weight=1, ]; -E: 98 108 [weight=10, ]; -E: 98 183 [weight=12, ]; -E: 99 106 [weight=1, ]; -E: 99 107 [weight=1, ]; -E: 99 108 [weight=3, ]; -E: 99 179 [weight=1, ]; -E: 99 183 [weight=4, ]; -E: 100 101 [weight=1, ]; -E: 100 108 [weight=3, ]; -E: 100 168 [weight=1, ]; -E: 100 181 [weight=5, ]; -E: 100 182 [weight=4, ]; -E: 100 183 [weight=4, ]; -E: 101 103 [weight=1, ]; -E: 101 108 [weight=5, ]; -E: 101 168 [weight=2, ]; -E: 101 181 [weight=10, ]; -E: 101 182 [weight=23, ]; -E: 101 183 [weight=30, ]; -E: 102 108 [weight=14, ]; -E: 102 181 [weight=12, ]; -E: 102 182 [weight=4, ]; -E: 102 183 [weight=30, ]; -E: 103 108 [weight=14, ]; -E: 103 181 [weight=12, ]; -E: 103 182 [weight=4, ]; -E: 103 183 [weight=30, ]; -E: 104 181 [weight=6, ]; -E: 104 182 [weight=2, ]; -E: 104 183 [weight=6, ]; -E: 105 181 [weight=6, ]; -E: 105 182 [weight=2, ]; -E: 105 183 [weight=6, ]; -E: 106 181 [weight=6, ]; -E: 106 182 [weight=2, ]; -E: 106 183 [weight=6, ]; -E: 107 181 [weight=6, ]; -E: 107 182 [weight=2, ]; -E: 107 183 [weight=6, ]; -E: 108 181 [weight=6, ]; -E: 108 182 [weight=2, ]; -E: 108 183 [weight=6, ]; -E: 109 110 [weight=1, ]; -E: 109 118 [weight=1, ]; -E: 109 121 [weight=9, ]; -E: 109 169 [weight=2, ]; -E: 109 181 [weight=3, ]; -E: 109 182 [weight=4, ]; -E: 109 183 [weight=11, ]; -E: 110 121 [weight=7, ]; -E: 110 179 [weight=1, ]; -E: 110 181 [weight=2, ]; -E: 110 182 [weight=2, ]; -E: 110 183 [weight=8, ]; -E: 111 112 [weight=1, ]; -E: 111 114 [weight=2, ]; -E: 111 121 [weight=4, ]; -E: 111 157 [weight=1, ]; -E: 111 169 [weight=1, ]; -E: 111 182 [weight=4, ]; -E: 111 183 [weight=6, ]; -E: 112 114 [weight=7, ]; -E: 112 121 [weight=9, ]; -E: 112 155 [weight=1, ]; -E: 112 169 [weight=10, ]; -E: 112 179 [weight=1, ]; -E: 112 181 [weight=9, ]; -E: 112 182 [weight=5, ]; -E: 112 183 [weight=21, ]; -E: 113 114 [weight=1, ]; -E: 113 182 [weight=1, ]; -E: 113 183 [weight=3, ]; -E: 114 181 [weight=1, ]; -E: 114 183 [weight=12, ]; -E: 115 116 [weight=2, ]; -E: 115 121 [weight=36, ]; -E: 115 135 [weight=1, ]; -E: 115 136 [weight=1, ]; -E: 115 145 [weight=43, ]; -E: 115 169 [weight=10, ]; -E: 115 173 [weight=78, ]; -E: 115 179 [weight=1, ]; -E: 115 181 [weight=30, ]; -E: 115 182 [weight=37, ]; -E: 115 183 [weight=4, ]; -E: 116 121 [weight=9, ]; -E: 116 150 [weight=1, ]; -E: 116 169 [weight=1, ]; -E: 116 173 [weight=22, ]; -E: 116 179 [weight=1, ]; -E: 116 181 [weight=7, ]; -E: 116 182 [weight=7, ]; -E: 116 183 [weight=4, ]; -E: 117 121 [weight=30, ]; -E: 117 148 [weight=2, ]; -E: 117 149 [weight=1, ]; -E: 117 169 [weight=5, ]; -E: 117 170 [weight=62, ]; -E: 117 179 [weight=1, ]; -E: 117 181 [weight=16, ]; -E: 117 182 [weight=18, ]; -E: 117 183 [weight=4, ]; +E: 98 107 [weight=3, ]; +E: 98 178 [weight=1, ]; +E: 98 182 [weight=4, ]; +E: 99 100 [weight=1, ]; +E: 99 107 [weight=3, ]; +E: 99 167 [weight=1, ]; +E: 99 180 [weight=5, ]; +E: 99 181 [weight=4, ]; +E: 99 182 [weight=4, ]; +E: 100 102 [weight=1, ]; +E: 100 107 [weight=5, ]; +E: 100 167 [weight=2, ]; +E: 100 180 [weight=10, ]; +E: 100 181 [weight=23, ]; +E: 100 182 [weight=30, ]; +E: 101 107 [weight=14, ]; +E: 101 180 [weight=12, ]; +E: 101 181 [weight=4, ]; +E: 101 182 [weight=30, ]; +E: 102 107 [weight=14, ]; +E: 102 180 [weight=12, ]; +E: 102 181 [weight=4, ]; +E: 102 182 [weight=30, ]; +E: 103 180 [weight=6, ]; +E: 103 181 [weight=2, ]; +E: 103 182 [weight=6, ]; +E: 104 180 [weight=6, ]; +E: 104 181 [weight=2, ]; +E: 104 182 [weight=6, ]; +E: 105 180 [weight=6, ]; +E: 105 181 [weight=2, ]; +E: 105 182 [weight=6, ]; +E: 106 180 [weight=6, ]; +E: 106 181 [weight=2, ]; +E: 106 182 [weight=6, ]; +E: 107 180 [weight=6, ]; +E: 107 181 [weight=2, ]; +E: 107 182 [weight=6, ]; +E: 108 109 [weight=1, ]; +E: 108 117 [weight=1, ]; +E: 108 120 [weight=9, ]; +E: 108 168 [weight=2, ]; +E: 108 180 [weight=3, ]; +E: 108 181 [weight=4, ]; +E: 108 182 [weight=11, ]; +E: 109 120 [weight=7, ]; +E: 109 178 [weight=1, ]; +E: 109 180 [weight=2, ]; +E: 109 181 [weight=2, ]; +E: 109 182 [weight=8, ]; +E: 110 111 [weight=1, ]; +E: 110 113 [weight=2, ]; +E: 110 120 [weight=4, ]; +E: 110 156 [weight=1, ]; +E: 110 168 [weight=1, ]; +E: 110 181 [weight=4, ]; +E: 110 182 [weight=6, ]; +E: 111 113 [weight=7, ]; +E: 111 120 [weight=9, ]; +E: 111 154 [weight=1, ]; +E: 111 168 [weight=10, ]; +E: 111 178 [weight=1, ]; +E: 111 180 [weight=9, ]; +E: 111 181 [weight=5, ]; +E: 111 182 [weight=21, ]; +E: 112 113 [weight=1, ]; +E: 112 181 [weight=1, ]; +E: 112 182 [weight=3, ]; +E: 113 180 [weight=1, ]; +E: 113 182 [weight=12, ]; +E: 114 115 [weight=2, ]; +E: 114 120 [weight=36, ]; +E: 114 134 [weight=1, ]; +E: 114 135 [weight=1, ]; +E: 114 144 [weight=43, ]; +E: 114 168 [weight=10, ]; +E: 114 172 [weight=78, ]; +E: 114 178 [weight=1, ]; +E: 114 180 [weight=30, ]; +E: 114 181 [weight=37, ]; +E: 114 182 [weight=4, ]; +E: 115 120 [weight=9, ]; +E: 115 149 [weight=1, ]; +E: 115 168 [weight=1, ]; +E: 115 172 [weight=22, ]; +E: 115 178 [weight=1, ]; +E: 115 180 [weight=7, ]; +E: 115 181 [weight=7, ]; +E: 115 182 [weight=4, ]; +E: 116 120 [weight=30, ]; +E: 116 147 [weight=2, ]; +E: 116 148 [weight=1, ]; +E: 116 168 [weight=5, ]; +E: 116 169 [weight=62, ]; +E: 116 178 [weight=1, ]; +E: 116 180 [weight=16, ]; +E: 116 181 [weight=18, ]; +E: 116 182 [weight=4, ]; +E: 117 118 [weight=1, ]; +E: 117 120 [weight=17, ]; +E: 117 168 [weight=1, ]; +E: 117 178 [weight=1, ]; +E: 117 180 [weight=8, ]; +E: 117 181 [weight=4, ]; +E: 117 182 [weight=17, ]; E: 118 119 [weight=1, ]; -E: 118 121 [weight=17, ]; -E: 118 169 [weight=1, ]; -E: 118 179 [weight=1, ]; -E: 118 181 [weight=8, ]; -E: 118 182 [weight=4, ]; -E: 118 183 [weight=17, ]; -E: 119 120 [weight=1, ]; -E: 119 121 [weight=2, ]; -E: 119 169 [weight=1, ]; -E: 119 181 [weight=3, ]; -E: 119 182 [weight=2, ]; -E: 119 183 [weight=3, ]; -E: 120 121 [weight=29, ]; -E: 120 156 [weight=1, ]; -E: 120 157 [weight=1, ]; -E: 120 169 [weight=20, ]; -E: 120 179 [weight=1, ]; -E: 120 181 [weight=8, ]; -E: 120 182 [weight=13, ]; -E: 120 183 [weight=23, ]; -E: 121 169 [weight=1, ]; -E: 121 181 [weight=1, ]; +E: 118 120 [weight=2, ]; +E: 118 168 [weight=1, ]; +E: 118 180 [weight=3, ]; +E: 118 181 [weight=2, ]; +E: 118 182 [weight=3, ]; +E: 119 120 [weight=29, ]; +E: 119 155 [weight=1, ]; +E: 119 156 [weight=1, ]; +E: 119 168 [weight=20, ]; +E: 119 178 [weight=1, ]; +E: 119 180 [weight=8, ]; +E: 119 181 [weight=13, ]; +E: 119 182 [weight=23, ]; +E: 120 168 [weight=1, ]; +E: 120 180 [weight=1, ]; +E: 120 181 [weight=2, ]; +E: 120 182 [weight=9, ]; +E: 121 126 [weight=10, ]; +E: 121 180 [weight=2, ]; E: 121 182 [weight=2, ]; -E: 121 183 [weight=9, ]; -E: 122 127 [weight=10, ]; -E: 122 181 [weight=2, ]; -E: 122 183 [weight=2, ]; -E: 123 127 [weight=10, ]; +E: 122 126 [weight=10, ]; +E: 122 180 [weight=2, ]; +E: 122 182 [weight=2, ]; +E: 123 126 [weight=2, ]; E: 123 181 [weight=2, ]; -E: 123 183 [weight=2, ]; -E: 124 127 [weight=2, ]; -E: 124 182 [weight=2, ]; -E: 125 127 [weight=19, ]; -E: 125 179 [weight=1, ]; -E: 125 181 [weight=3, ]; -E: 125 182 [weight=11, ]; -E: 125 183 [weight=14, ]; -E: 126 127 [weight=29, ]; -E: 126 170 [weight=27, ]; -E: 126 179 [weight=1, ]; -E: 126 181 [weight=2, ]; -E: 126 182 [weight=2, ]; -E: 126 183 [weight=4, ]; -E: 127 183 [weight=6, ]; -E: 128 131 [weight=38, ]; -E: 128 169 [weight=35, ]; +E: 124 126 [weight=19, ]; +E: 124 178 [weight=1, ]; +E: 124 180 [weight=3, ]; +E: 124 181 [weight=11, ]; +E: 124 182 [weight=14, ]; +E: 125 126 [weight=29, ]; +E: 125 169 [weight=27, ]; +E: 125 178 [weight=1, ]; +E: 125 180 [weight=2, ]; +E: 125 181 [weight=2, ]; +E: 125 182 [weight=4, ]; +E: 126 182 [weight=6, ]; +E: 127 130 [weight=38, ]; +E: 127 168 [weight=35, ]; +E: 127 178 [weight=1, ]; +E: 127 180 [weight=26, ]; +E: 127 181 [weight=30, ]; +E: 127 182 [weight=77, ]; +E: 128 168 [weight=25, ]; E: 128 179 [weight=1, ]; -E: 128 181 [weight=26, ]; -E: 128 182 [weight=30, ]; -E: 128 183 [weight=77, ]; -E: 129 169 [weight=25, ]; -E: 129 180 [weight=1, ]; -E: 129 181 [weight=50, ]; -E: 129 182 [weight=46, ]; -E: 129 183 [weight=78, ]; -E: 130 131 [weight=13, ]; -E: 130 132 [weight=13, ]; -E: 130 169 [weight=13, ]; -E: 130 179 [weight=1, ]; -E: 130 181 [weight=44, ]; -E: 130 182 [weight=35, ]; -E: 130 183 [weight=37, ]; -E: 131 181 [weight=1, ]; -E: 131 182 [weight=2, ]; -E: 131 183 [weight=13, ]; -E: 132 183 [weight=9, ]; -E: 133 134 [weight=12, ]; -E: 133 170 [weight=11, ]; -E: 133 179 [weight=1, ]; -E: 133 181 [weight=4, ]; -E: 133 182 [weight=2, ]; -E: 133 183 [weight=5, ]; -E: 134 181 [weight=1, ]; -E: 134 182 [weight=1, ]; -E: 134 183 [weight=10, ]; -E: 135 145 [weight=26, ]; -E: 135 169 [weight=8, ]; -E: 135 173 [weight=30, ]; -E: 135 179 [weight=1, ]; -E: 135 181 [weight=9, ]; -E: 135 182 [weight=6, ]; -E: 135 183 [weight=9, ]; -E: 136 145 [weight=24, ]; -E: 136 169 [weight=11, ]; -E: 136 173 [weight=24, ]; -E: 136 179 [weight=1, ]; -E: 136 181 [weight=9, ]; -E: 136 182 [weight=19, ]; -E: 136 183 [weight=9, ]; -E: 137 145 [weight=14, ]; -E: 137 173 [weight=13, ]; -E: 137 179 [weight=1, ]; -E: 137 181 [weight=3, ]; -E: 137 182 [weight=3, ]; -E: 137 183 [weight=4, ]; -E: 138 145 [weight=9, ]; -E: 138 173 [weight=18, ]; -E: 138 179 [weight=1, ]; +E: 128 180 [weight=50, ]; +E: 128 181 [weight=46, ]; +E: 128 182 [weight=78, ]; +E: 129 130 [weight=13, ]; +E: 129 131 [weight=13, ]; +E: 129 168 [weight=13, ]; +E: 129 178 [weight=1, ]; +E: 129 180 [weight=44, ]; +E: 129 181 [weight=35, ]; +E: 129 182 [weight=37, ]; +E: 130 180 [weight=1, ]; +E: 130 181 [weight=2, ]; +E: 130 182 [weight=13, ]; +E: 131 182 [weight=9, ]; +E: 132 133 [weight=12, ]; +E: 132 169 [weight=11, ]; +E: 132 178 [weight=1, ]; +E: 132 180 [weight=4, ]; +E: 132 181 [weight=2, ]; +E: 132 182 [weight=5, ]; +E: 133 180 [weight=1, ]; +E: 133 181 [weight=1, ]; +E: 133 182 [weight=10, ]; +E: 134 144 [weight=26, ]; +E: 134 168 [weight=8, ]; +E: 134 172 [weight=30, ]; +E: 134 178 [weight=1, ]; +E: 134 180 [weight=9, ]; +E: 134 181 [weight=6, ]; +E: 134 182 [weight=9, ]; +E: 135 144 [weight=24, ]; +E: 135 168 [weight=11, ]; +E: 135 172 [weight=24, ]; +E: 135 178 [weight=1, ]; +E: 135 180 [weight=9, ]; +E: 135 181 [weight=19, ]; +E: 135 182 [weight=9, ]; +E: 136 144 [weight=14, ]; +E: 136 172 [weight=13, ]; +E: 136 178 [weight=1, ]; +E: 136 180 [weight=3, ]; +E: 136 181 [weight=3, ]; +E: 136 182 [weight=4, ]; +E: 137 144 [weight=9, ]; +E: 137 172 [weight=18, ]; +E: 137 178 [weight=1, ]; +E: 137 180 [weight=6, ]; +E: 137 181 [weight=6, ]; +E: 137 182 [weight=4, ]; +E: 138 144 [weight=14, ]; +E: 138 169 [weight=14, ]; +E: 138 172 [weight=19, ]; +E: 138 180 [weight=6, ]; E: 138 181 [weight=6, ]; -E: 138 182 [weight=6, ]; -E: 138 183 [weight=4, ]; -E: 139 145 [weight=14, ]; -E: 139 170 [weight=14, ]; -E: 139 173 [weight=19, ]; -E: 139 181 [weight=6, ]; -E: 139 182 [weight=6, ]; -E: 139 183 [weight=14, ]; -E: 140 141 [weight=1, ]; -E: 140 183 [weight=2, ]; -E: 141 183 [weight=9, ]; -E: 142 145 [weight=7, ]; -E: 142 170 [weight=6, ]; +E: 138 182 [weight=14, ]; +E: 139 140 [weight=1, ]; +E: 139 182 [weight=2, ]; +E: 140 182 [weight=9, ]; +E: 141 144 [weight=7, ]; +E: 141 169 [weight=6, ]; +E: 141 180 [weight=4, ]; +E: 141 182 [weight=3, ]; +E: 142 144 [weight=32, ]; +E: 142 169 [weight=16, ]; +E: 142 177 [weight=1, ]; +E: 142 180 [weight=9, ]; E: 142 181 [weight=4, ]; -E: 142 183 [weight=3, ]; -E: 143 145 [weight=32, ]; -E: 143 170 [weight=16, ]; -E: 143 178 [weight=1, ]; -E: 143 181 [weight=9, ]; -E: 143 182 [weight=4, ]; -E: 143 183 [weight=4, ]; -E: 144 183 [weight=9, ]; -E: 145 183 [weight=9, ]; -E: 146 150 [weight=2, ]; -E: 146 169 [weight=36, ]; -E: 146 173 [weight=46, ]; -E: 146 179 [weight=1, ]; -E: 146 181 [weight=38, ]; -E: 146 182 [weight=13, ]; -E: 146 183 [weight=105, ]; -E: 147 169 [weight=18, ]; -E: 147 179 [weight=1, ]; -E: 147 181 [weight=7, ]; -E: 147 182 [weight=2, ]; -E: 147 183 [weight=48, ]; -E: 148 169 [weight=11, ]; -E: 148 170 [weight=40, ]; -E: 148 179 [weight=1, ]; +E: 142 182 [weight=4, ]; +E: 143 182 [weight=9, ]; +E: 144 182 [weight=9, ]; +E: 145 149 [weight=2, ]; +E: 145 168 [weight=36, ]; +E: 145 172 [weight=46, ]; +E: 145 178 [weight=1, ]; +E: 145 180 [weight=38, ]; +E: 145 181 [weight=13, ]; +E: 145 182 [weight=105, ]; +E: 146 168 [weight=18, ]; +E: 146 178 [weight=1, ]; +E: 146 180 [weight=7, ]; +E: 146 181 [weight=2, ]; +E: 146 182 [weight=48, ]; +E: 147 168 [weight=11, ]; +E: 147 169 [weight=40, ]; +E: 147 178 [weight=1, ]; +E: 147 180 [weight=2, ]; +E: 147 181 [weight=2, ]; +E: 147 182 [weight=7, ]; +E: 148 168 [weight=9, ]; +E: 148 169 [weight=39, ]; +E: 148 178 [weight=1, ]; +E: 148 180 [weight=2, ]; E: 148 181 [weight=2, ]; -E: 148 182 [weight=2, ]; -E: 148 183 [weight=7, ]; -E: 149 169 [weight=9, ]; -E: 149 170 [weight=39, ]; -E: 149 179 [weight=1, ]; +E: 148 182 [weight=7, ]; +E: 149 168 [weight=6, ]; +E: 149 172 [weight=19, ]; +E: 149 178 [weight=1, ]; +E: 149 180 [weight=2, ]; E: 149 181 [weight=2, ]; -E: 149 182 [weight=2, ]; -E: 149 183 [weight=7, ]; -E: 150 169 [weight=6, ]; -E: 150 173 [weight=19, ]; -E: 150 179 [weight=1, ]; -E: 150 181 [weight=2, ]; -E: 150 182 [weight=2, ]; -E: 150 183 [weight=11, ]; -E: 151 158 [weight=2, ]; -E: 151 169 [weight=41, ]; -E: 151 179 [weight=1, ]; -E: 151 181 [weight=88, ]; -E: 151 182 [weight=78, ]; -E: 151 183 [weight=119, ]; -E: 152 157 [weight=1, ]; -E: 152 158 [weight=1, ]; -E: 152 169 [weight=19, ]; -E: 152 181 [weight=87, ]; -E: 152 182 [weight=107, ]; -E: 152 183 [weight=118, ]; -E: 153 169 [weight=12, ]; -E: 153 181 [weight=21, ]; -E: 153 182 [weight=56, ]; -E: 153 183 [weight=62, ]; -E: 154 169 [weight=3, ]; -E: 154 181 [weight=3, ]; -E: 154 183 [weight=6, ]; -E: 155 156 [weight=1, ]; -E: 155 169 [weight=8, ]; -E: 155 183 [weight=8, ]; -E: 156 169 [weight=29, ]; -E: 156 179 [weight=1, ]; -E: 156 181 [weight=5, ]; -E: 156 182 [weight=2, ]; -E: 156 183 [weight=18, ]; -E: 157 169 [weight=6, ]; -E: 157 179 [weight=1, ]; -E: 157 181 [weight=5, ]; -E: 157 182 [weight=9, ]; -E: 157 183 [weight=14, ]; -E: 158 169 [weight=7, ]; -E: 158 181 [weight=12, ]; -E: 158 182 [weight=10, ]; -E: 158 183 [weight=30, ]; -E: 159 162 [weight=1, ]; -E: 159 170 [weight=36, ]; -E: 159 178 [weight=1, ]; -E: 159 181 [weight=6, ]; +E: 149 182 [weight=11, ]; +E: 150 157 [weight=2, ]; +E: 150 168 [weight=41, ]; +E: 150 178 [weight=1, ]; +E: 150 180 [weight=88, ]; +E: 150 181 [weight=78, ]; +E: 150 182 [weight=119, ]; +E: 151 156 [weight=1, ]; +E: 151 157 [weight=1, ]; +E: 151 168 [weight=19, ]; +E: 151 180 [weight=87, ]; +E: 151 181 [weight=107, ]; +E: 151 182 [weight=118, ]; +E: 152 168 [weight=12, ]; +E: 152 180 [weight=21, ]; +E: 152 181 [weight=56, ]; +E: 152 182 [weight=62, ]; +E: 153 168 [weight=3, ]; +E: 153 180 [weight=3, ]; +E: 153 182 [weight=6, ]; +E: 154 155 [weight=1, ]; +E: 154 168 [weight=8, ]; +E: 154 182 [weight=8, ]; +E: 155 168 [weight=29, ]; +E: 155 178 [weight=1, ]; +E: 155 180 [weight=5, ]; +E: 155 181 [weight=2, ]; +E: 155 182 [weight=18, ]; +E: 156 168 [weight=6, ]; +E: 156 178 [weight=1, ]; +E: 156 180 [weight=5, ]; +E: 156 181 [weight=9, ]; +E: 156 182 [weight=14, ]; +E: 157 168 [weight=7, ]; +E: 157 180 [weight=12, ]; +E: 157 181 [weight=10, ]; +E: 157 182 [weight=30, ]; +E: 158 161 [weight=1, ]; +E: 158 169 [weight=36, ]; +E: 158 177 [weight=1, ]; +E: 158 180 [weight=6, ]; +E: 158 181 [weight=2, ]; +E: 158 182 [weight=4, ]; +E: 159 169 [weight=10, ]; +E: 159 180 [weight=2, ]; E: 159 182 [weight=2, ]; -E: 159 183 [weight=4, ]; -E: 160 170 [weight=10, ]; -E: 160 181 [weight=2, ]; -E: 160 183 [weight=2, ]; -E: 161 169 [weight=25, ]; -E: 161 170 [weight=8, ]; -E: 161 179 [weight=1, ]; -E: 161 181 [weight=46, ]; -E: 161 182 [weight=6, ]; -E: 161 183 [weight=103, ]; -E: 162 170 [weight=3, ]; +E: 160 168 [weight=25, ]; +E: 160 169 [weight=8, ]; +E: 160 178 [weight=1, ]; +E: 160 180 [weight=46, ]; +E: 160 181 [weight=6, ]; +E: 160 182 [weight=103, ]; +E: 161 169 [weight=3, ]; +E: 161 181 [weight=3, ]; +E: 162 169 [weight=6, ]; +E: 162 180 [weight=2, ]; E: 162 182 [weight=3, ]; -E: 163 170 [weight=6, ]; -E: 163 181 [weight=2, ]; -E: 163 183 [weight=3, ]; -E: 164 170 [weight=3, ]; -E: 164 181 [weight=2, ]; -E: 164 183 [weight=3, ]; -E: 165 176 [weight=2, ]; +E: 163 169 [weight=3, ]; +E: 163 180 [weight=2, ]; +E: 163 182 [weight=3, ]; +E: 164 175 [weight=2, ]; +E: 164 180 [weight=2, ]; +E: 164 182 [weight=2, ]; +E: 165 175 [weight=2, ]; E: 165 181 [weight=2, ]; -E: 165 183 [weight=2, ]; -E: 166 176 [weight=2, ]; -E: 166 182 [weight=2, ]; -E: 167 180 [weight=1, ]; -E: 167 181 [weight=12, ]; -E: 167 182 [weight=8, ]; -E: 167 183 [weight=32, ]; -E: 168 181 [weight=4, ]; -E: 168 182 [weight=4, ]; -E: 168 183 [weight=10, ]; -E: 169 181 [weight=1, ]; -E: 169 183 [weight=12, ]; -E: 170 183 [weight=6, ]; -E: 171 172 [weight=1, ]; +E: 166 179 [weight=1, ]; +E: 166 180 [weight=12, ]; +E: 166 181 [weight=8, ]; +E: 166 182 [weight=32, ]; +E: 167 180 [weight=4, ]; +E: 167 181 [weight=4, ]; +E: 167 182 [weight=10, ]; +E: 168 180 [weight=1, ]; +E: 168 182 [weight=12, ]; +E: 169 182 [weight=6, ]; +E: 170 171 [weight=1, ]; +E: 170 181 [weight=1, ]; E: 171 182 [weight=1, ]; -E: 172 183 [weight=1, ]; -E: 173 183 [weight=6, ]; -E: 174 182 [weight=1, ]; -E: 174 183 [weight=7, ]; -E: 175 183 [weight=5, ]; -E: 176 183 [weight=5, ]; -E: 177 181 [weight=2, ]; -E: 177 182 [weight=2, ]; -E: 177 183 [weight=10, ]; -E: 178 180 [weight=1, ]; -E: 178 181 [weight=1, ]; -E: 178 182 [weight=1, ]; -E: 178 183 [weight=4, ]; +E: 172 182 [weight=6, ]; +E: 173 181 [weight=1, ]; +E: 173 182 [weight=7, ]; +E: 174 182 [weight=5, ]; +E: 175 182 [weight=5, ]; +E: 176 180 [weight=2, ]; +E: 176 181 [weight=2, ]; +E: 176 182 [weight=10, ]; +E: 177 179 [weight=1, ]; +E: 177 180 [weight=1, ]; +E: 177 181 [weight=1, ]; +E: 177 182 [weight=4, ]; +E: 178 180 [weight=2, ]; +E: 178 181 [weight=2, ]; +E: 178 182 [weight=10, ]; +E: 179 180 [weight=2, ]; E: 179 181 [weight=2, ]; -E: 179 182 [weight=2, ]; -E: 179 183 [weight=10, ]; -E: 180 181 [weight=2, ]; -E: 180 182 [weight=2, ]; -E: 180 183 [weight=10, ]; +E: 179 182 [weight=10, ]; diff --git a/tests/graph.without.dot.oracle b/tests/graph.without.dot.oracle index 632fd7594..0e82e307a 100644 --- a/tests/graph.without.dot.oracle +++ b/tests/graph.without.dot.oracle @@ -1,16 +1,15 @@ digraph tests/graph { graph [ratio=0.5] node [style=filled] -Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; -Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; @@ -132,12 +131,12 @@ Test_count_occ_cons_eq [label="count_occ_cons_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_count_occ_In [label="count_occ_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; - Test_removelast_app -> Test_list_ind [] ; +Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; + Test_app_removelast_last -> Test_list_ind [] ; Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; Test_ReDun_NoDup_Permutation -> Test_In_split [] ; - Test_app_removelast_last -> Test_list_ind [] ; Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; @@ -273,8 +272,9 @@ Test_count_occ_In [label="count_occ_In", URL=, peripheri Test_distr_rev -> Test_app_nil_end [] ; Test_count_occ_inv_nil -> Test_list_ind [] ; Test_count_occ_In -> Test_list_ind [] ; + Test_removelast_app -> Test_list_ind [] ; subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; -Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left_app; Test_fold_left_length; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_existsb_exists; Test_existsb_nth; Test_forallb_forall; Test_filter_In; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_split_nth; Test_split_length_l; Test_split_length_r; Test_split_combine; Test_combine_split; Test_in_combine_l; Test_size_nil; Test_in_combine_r; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_app_inv_tail; Test_firstn_skipn; Test_firstn_length; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove_In; Test_app_removelast_last; Test_removelast_app; }; +Test_removelast_app; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left_app; Test_fold_left_length; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_existsb_exists; Test_existsb_nth; Test_forallb_forall; Test_filter_In; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_split_nth; Test_split_length_l; Test_split_length_r; Test_split_combine; Test_combine_split; Test_in_combine_l; Test_size_nil; Test_in_combine_r; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_app_inv_tail; Test_firstn_skipn; Test_firstn_length; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove_In; Test_app_removelast_last; }; } /* END */ diff --git a/tests/graph2.dot.oracle b/tests/graph2.dot.oracle index 53b16808d..446f902ee 100644 --- a/tests/graph2.dot.oracle +++ b/tests/graph2.dot.oracle @@ -1,4 +1,4 @@ -digraph tests/graph2 { +digraph graph2 { graph [ratio=0.5] node [style=filled] Test_Permutation_app_swap [label="Permutation_app_swap", URL=, peripheries=3, fillcolor="#7FFFD4"] ; diff --git a/tests/graph2.dpd.oracle b/tests/graph2.dpd.oracle index 94f186f98..4de8015e8 100644 --- a/tests/graph2.dpd.oracle +++ b/tests/graph2.dpd.oracle @@ -1,95 +1,95 @@ -N: 184 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 205 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 188 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 185 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 192 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 193 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 187 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 186 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 190 "eq_ind" [body=yes, kind=cnst, prop=yes, ]; -N: 191 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ]; -N: 201 "eq_sym" [body=yes, kind=cnst, prop=yes, ]; -N: 189 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 194 "Permutation" [kind=inductive, prop=no, path="Test", ]; -N: 202 "eq" [kind=inductive, prop=no, ]; -N: 195 "list" [kind=inductive, prop=no, path="Test", ]; -N: 204 "perm_nil" [kind=construct, prop=yes, path="Test", ]; -N: 203 "eq_refl" [kind=construct, prop=yes, ]; -N: 198 "nil" [kind=construct, prop=no, path="Test", ]; -N: 196 "perm_skip" [kind=construct, prop=yes, path="Test", ]; -N: 199 "cons" [kind=construct, prop=no, path="Test", ]; -N: 197 "perm_swap" [kind=construct, prop=yes, path="Test", ]; -N: 200 "perm_trans" [kind=construct, prop=yes, path="Test", ]; -E: 184 185 [weight=3, ]; -E: 184 186 [weight=2, ]; -E: 184 187 [weight=1, ]; -E: 184 188 [weight=2, ]; -E: 184 189 [weight=2, ]; -E: 184 190 [weight=2, ]; -E: 184 191 [weight=1, ]; -E: 184 192 [weight=3, ]; -E: 184 193 [weight=43, ]; -E: 184 194 [weight=11, ]; -E: 184 195 [weight=18, ]; -E: 184 196 [weight=3, ]; -E: 184 197 [weight=1, ]; -E: 184 198 [weight=6, ]; -E: 184 199 [weight=42, ]; -E: 185 194 [weight=10, ]; -E: 185 195 [weight=12, ]; -E: 185 196 [weight=1, ]; -E: 185 197 [weight=1, ]; -E: 185 200 [weight=1, ]; -E: 185 204 [weight=1, ]; -E: 185 205 [weight=1, ]; -E: 186 189 [weight=1, ]; -E: 186 190 [weight=1, ]; -E: 186 193 [weight=6, ]; -E: 186 195 [weight=14, ]; -E: 186 198 [weight=9, ]; -E: 186 199 [weight=5, ]; -E: 186 202 [weight=6, ]; -E: 186 203 [weight=2, ]; +N: 183 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 204 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 187 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 184 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 191 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 192 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 186 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 185 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 189 "eq_ind" [body=yes, kind=cnst, prop=yes, ]; +N: 190 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ]; +N: 200 "eq_sym" [body=yes, kind=cnst, prop=yes, ]; +N: 188 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 193 "Permutation" [kind=inductive, prop=no, path="Test", ]; +N: 201 "eq" [kind=inductive, prop=no, ]; +N: 194 "list" [kind=inductive, prop=no, path="Test", ]; +N: 203 "perm_nil" [kind=construct, prop=yes, path="Test", ]; +N: 202 "eq_refl" [kind=construct, prop=yes, ]; +N: 197 "nil" [kind=construct, prop=no, path="Test", ]; +N: 195 "perm_skip" [kind=construct, prop=yes, path="Test", ]; +N: 198 "cons" [kind=construct, prop=no, path="Test", ]; +N: 196 "perm_swap" [kind=construct, prop=yes, path="Test", ]; +N: 199 "perm_trans" [kind=construct, prop=yes, path="Test", ]; +E: 183 184 [weight=3, ]; +E: 183 185 [weight=2, ]; +E: 183 186 [weight=1, ]; +E: 183 187 [weight=2, ]; +E: 183 188 [weight=2, ]; +E: 183 189 [weight=2, ]; +E: 183 190 [weight=1, ]; +E: 183 191 [weight=3, ]; +E: 183 192 [weight=43, ]; +E: 183 193 [weight=11, ]; +E: 183 194 [weight=18, ]; +E: 183 195 [weight=3, ]; +E: 183 196 [weight=1, ]; +E: 183 197 [weight=6, ]; +E: 183 198 [weight=42, ]; +E: 184 193 [weight=10, ]; +E: 184 194 [weight=12, ]; +E: 184 195 [weight=1, ]; +E: 184 196 [weight=1, ]; +E: 184 199 [weight=1, ]; +E: 184 203 [weight=1, ]; +E: 184 204 [weight=1, ]; +E: 185 188 [weight=1, ]; +E: 185 189 [weight=1, ]; +E: 185 192 [weight=6, ]; +E: 185 194 [weight=14, ]; +E: 185 197 [weight=9, ]; +E: 185 198 [weight=5, ]; +E: 185 201 [weight=6, ]; +E: 185 202 [weight=2, ]; +E: 186 192 [weight=3, ]; +E: 186 194 [weight=6, ]; +E: 186 198 [weight=3, ]; +E: 186 201 [weight=1, ]; +E: 186 202 [weight=1, ]; +E: 187 188 [weight=1, ]; E: 187 193 [weight=3, ]; -E: 187 195 [weight=6, ]; -E: 187 199 [weight=3, ]; -E: 187 202 [weight=1, ]; +E: 187 194 [weight=4, ]; +E: 187 195 [weight=1, ]; E: 187 203 [weight=1, ]; -E: 188 189 [weight=1, ]; -E: 188 194 [weight=3, ]; -E: 188 195 [weight=4, ]; -E: 188 196 [weight=1, ]; -E: 188 204 [weight=1, ]; -E: 189 195 [weight=10, ]; -E: 189 198 [weight=2, ]; -E: 189 199 [weight=2, ]; -E: 190 202 [weight=4, ]; -E: 191 190 [weight=1, ]; -E: 191 201 [weight=1, ]; -E: 191 202 [weight=2, ]; -E: 192 194 [weight=3, ]; -E: 192 195 [weight=3, ]; -E: 192 200 [weight=1, ]; -E: 193 195 [weight=12, ]; -E: 193 199 [weight=1, ]; -E: 194 195 [weight=6, ]; -E: 194 198 [weight=2, ]; -E: 194 199 [weight=6, ]; -E: 196 195 [weight=6, ]; -E: 196 198 [weight=2, ]; -E: 196 199 [weight=6, ]; -E: 197 195 [weight=6, ]; -E: 197 198 [weight=2, ]; -E: 197 199 [weight=6, ]; -E: 200 195 [weight=6, ]; -E: 200 198 [weight=2, ]; -E: 200 199 [weight=6, ]; -E: 201 202 [weight=6, ]; -E: 201 203 [weight=1, ]; -E: 204 195 [weight=6, ]; -E: 204 198 [weight=2, ]; -E: 204 199 [weight=6, ]; -E: 205 194 [weight=14, ]; -E: 205 195 [weight=30, ]; -E: 205 198 [weight=4, ]; -E: 205 199 [weight=12, ]; +E: 188 194 [weight=10, ]; +E: 188 197 [weight=2, ]; +E: 188 198 [weight=2, ]; +E: 189 201 [weight=4, ]; +E: 190 189 [weight=1, ]; +E: 190 200 [weight=1, ]; +E: 190 201 [weight=2, ]; +E: 191 193 [weight=3, ]; +E: 191 194 [weight=3, ]; +E: 191 199 [weight=1, ]; +E: 192 194 [weight=12, ]; +E: 192 198 [weight=1, ]; +E: 193 194 [weight=6, ]; +E: 193 197 [weight=2, ]; +E: 193 198 [weight=6, ]; +E: 195 194 [weight=6, ]; +E: 195 197 [weight=2, ]; +E: 195 198 [weight=6, ]; +E: 196 194 [weight=6, ]; +E: 196 197 [weight=2, ]; +E: 196 198 [weight=6, ]; +E: 199 194 [weight=6, ]; +E: 199 197 [weight=2, ]; +E: 199 198 [weight=6, ]; +E: 200 201 [weight=6, ]; +E: 200 202 [weight=1, ]; +E: 203 194 [weight=6, ]; +E: 203 197 [weight=2, ]; +E: 203 198 [weight=6, ]; +E: 204 193 [weight=14, ]; +E: 204 194 [weight=30, ]; +E: 204 197 [weight=4, ]; +E: 204 198 [weight=12, ];