diff --git a/research/pr4546-extended-ceilings/.gitattributes b/research/pr4546-extended-ceilings/.gitattributes new file mode 100644 index 0000000000..d047169fb5 --- /dev/null +++ b/research/pr4546-extended-ceilings/.gitattributes @@ -0,0 +1,4 @@ +PR4546-RESULT.json -text +PR4581-RESULT.json -text +PR4582-RESULT.json -text +PR4587-RESULT.json -text diff --git a/research/pr4546-extended-ceilings/PR4546-RESULT.json b/research/pr4546-extended-ceilings/PR4546-RESULT.json new file mode 100644 index 0000000000..f2f411003d --- /dev/null +++ b/research/pr4546-extended-ceilings/PR4546-RESULT.json @@ -0,0 +1 @@ +{"controls":{"actual_small_paths_checked":68,"enumerated_words_per_sign_case":22621,"exact_equality_control":true,"exit_charge_control":true,"incompatible_exit_control":true,"word_counts":{"(-1, -1)":84,"(-1, 1)":84,"(1, -1)":84,"(1, 1)":84}},"excluded_window_count":12,"new_kappa":false,"not_covered":["geometric attainability of relaxed profiles","nonadjacent or larger windows","joint overlapping rewrites","physical native admission","global ceiling or new kappa"],"scale":1000000000000000000,"schema":"four-shear-window-ceilings/v1","source_head":"b9a13c1673e0e9697de410de16e8bbf3207a7363","status":"PASS_FINITE_ALPHABET_CEILINGS","tested_saving":"60403/20000000","tested_windows":12,"total_eligible_windows":128,"windows":[{"certified_no_strict_gain":true,"coefficients":[-1,1],"compatible_words":84,"exit_dimensions":[0,2,0],"index":10554,"old_paid":{"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":2,"phase":"B","relaxed_profiles":1,"roles":[162,172,513],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[1,1],"compatible_words":84,"exit_dimensions":[2,0,0],"index":10555,"old_paid":{"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":3,"phase":"B","relaxed_profiles":1,"roles":[172,196,513],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10557,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":5,"phase":"B","relaxed_profiles":1,"roles":[140,144,502],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,1],"compatible_words":84,"exit_dimensions":[1,1,1],"index":10558,"old_paid":{"1":2},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":6,"phase":"B","relaxed_profiles":1,"roles":[144,187,502],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,1],"compatible_words":84,"exit_dimensions":[1,2,1],"index":10560,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":8,"phase":"B","relaxed_profiles":1,"roles":[168,150,548],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10561,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":9,"phase":"B","relaxed_profiles":1,"roles":[150,115,548],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10563,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":11,"phase":"B","relaxed_profiles":1,"roles":[131,117,560],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,1],"index":10564,"old_paid":{"1":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":12,"phase":"B","relaxed_profiles":1,"roles":[117,584,560],"start_dimensions":[0,1,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,2,3],"index":10575,"old_paid":{"1":1,"2":1,"3":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":23,"phase":"B","relaxed_profiles":4,"roles":[205,170,452],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,3],"index":10577,"old_paid":{"1":2,"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":25,"phase":"B","relaxed_profiles":1,"roles":[118,194,453],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,2,3],"index":10579,"old_paid":{"1":1,"2":1,"3":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":27,"phase":"B","relaxed_profiles":4,"roles":[120,207,454],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,3],"index":10581,"old_paid":{"1":2,"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":29,"phase":"B","relaxed_profiles":1,"roles":[192,179,455],"start_dimensions":[0,0,1]}]} diff --git a/research/pr4546-extended-ceilings/PR4581-RESULT.json b/research/pr4546-extended-ceilings/PR4581-RESULT.json new file mode 100644 index 0000000000..3fec4b9b51 --- /dev/null +++ b/research/pr4546-extended-ceilings/PR4581-RESULT.json @@ -0,0 +1,10742 @@ +{ + "failure_controls": { + "drop_directed_dependency": { + "falsely_admitted": [ + 2, + 1 + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10557 + }, + "drop_exit_intersection": { + "falsely_admitted": [ + 2, + 2 + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11078 + }, + "drop_terminal_charge": { + "falsely_admitted": [], + "incumbent": [ + 2 + ], + "index": 10554 + } + }, + "geometric_control": { + "concave_basis_checks": 90, + "endpoint_words": 84, + "geometric_paths": 2868 + }, + "new_kappa": false, + "profile_count_histogram": { + "1": 93, + "2": 9, + "3": 6, + "4": 2, + "5": 13, + "7": 4, + "9": 1 + }, + "reachable_states": 1303, + "schema": "receiver-window-all-length-floor/v1", + "source_base": "f626db5c3a3d781d8f7695038776c621651f75e1", + "source_files_checked": 7, + "status": "PASS_ALL_LENGTH_RECEIVER_FLOOR", + "window_count": 128, + "window_profile_pairs": 239, + "windows": [ + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [], + [] + ], + "exit_bases": [ + [], + [ + 224, + 30 + ], + [] + ], + "incumbent": [ + 2 + ], + "index": 10554, + "phase": "B", + "reachable_states": 4, + "roles": [ + 162, + 172, + 513 + ], + "start_bases": [ + [], + [], + [] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + 1, + 1 + ], + "contact_bases": [ + [], + [] + ], + "exit_bases": [ + [ + 224, + 30 + ], + [], + [] + ], + "incumbent": [ + 2 + ], + "index": 10555, + "phase": "B", + "reachable_states": 4, + "roles": [ + 172, + 196, + 513 + ], + "start_bases": [ + [], + [], + [] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 30 + ], + [ + 30 + ] + ], + "exit_bases": [ + [ + 416, + 30 + ], + [ + 30 + ], + [ + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10557, + "phase": "B", + "reachable_states": 9, + "roles": [ + 140, + 144, + 502 + ], + "start_bases": [ + [], + [], + [ + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 30 + ], + [ + 30 + ] + ], + "exit_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 30 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 10558, + "phase": "B", + "reachable_states": 9, + "roles": [ + 144, + 187, + 502 + ], + "start_bases": [ + [], + [], + [ + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + 1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 51 + ], + [ + 388, + 51 + ], + [ + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10560, + "phase": "B", + "reachable_states": 9, + "roles": [ + 168, + 150, + 548 + ], + "start_bases": [ + [], + [], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 388, + 51 + ], + [ + 51 + ], + [ + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10561, + "phase": "B", + "reachable_states": 9, + "roles": [ + 150, + 115, + 548 + ], + "start_bases": [ + [], + [], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 196, + 51 + ], + [ + 51 + ], + [ + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10563, + "phase": "B", + "reachable_states": 9, + "roles": [ + 131, + 117, + 560 + ], + "start_bases": [ + [], + [], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 51 + ] + ], + "incumbent": [ + 1 + ], + "index": 10564, + "phase": "B", + "reachable_states": 6, + "roles": [ + 117, + 584, + 560 + ], + "start_bases": [ + [], + [ + 51 + ], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [], + [] + ], + "exit_bases": [ + [ + 30 + ], + [ + 491, + 30 + ], + [ + 459, + 38, + 30 + ] + ], + "incumbent": [ + 3, + 2, + 1 + ], + "index": 10575, + "phase": "B", + "reachable_states": 20, + "roles": [ + 205, + 170, + 452 + ], + "start_bases": [ + [], + [], + [] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 1, + 1, + 1 + ], + [ + 3, + 2, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 30 + ], + [ + 30 + ] + ], + "exit_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 448, + 21, + 11 + ] + ], + "incumbent": [ + 2, + 1, + 1 + ], + "index": 10577, + "phase": "B", + "reachable_states": 9, + "roles": [ + 118, + 194, + 453 + ], + "start_bases": [ + [], + [], + [ + 30 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [], + [] + ], + "exit_bases": [ + [ + 51 + ], + [ + 37, + 22 + ], + [ + 448, + 38, + 21 + ] + ], + "incumbent": [ + 3, + 2, + 1 + ], + "index": 10579, + "phase": "B", + "reachable_states": 20, + "roles": [ + 120, + 207, + 454 + ], + "start_bases": [ + [], + [], + [] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 1, + 1, + 1 + ], + [ + 3, + 2, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 469, + 51, + 11 + ] + ], + "incumbent": [ + 2, + 1, + 1 + ], + "index": 10581, + "phase": "B", + "reachable_states": 9, + "roles": [ + 192, + 179, + 455 + ], + "start_bases": [ + [], + [], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [], + [] + ], + "exit_bases": [ + [ + 321, + 30 + ], + [], + [ + 289, + 140, + 30 + ] + ], + "incumbent": [ + 3, + 2 + ], + "index": 10607, + "phase": "B", + "reachable_states": 8, + "roles": [ + 145, + 135, + 583 + ], + "start_bases": [ + [], + [], + [] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1 + ], + [ + 3, + 2 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 51 + ], + [ + 51 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 392, + 67, + 51 + ] + ], + "incumbent": [ + 4, + 4, + 2 + ], + "index": 10788, + "phase": "B", + "reachable_states": 20, + "roles": [ + 622, + 624, + 548 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 51 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 2, + 1, + 1 + ], + [ + 4, + 4, + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 10791, + "phase": "B", + "reachable_states": 47, + "roles": [ + 622, + 623, + 401 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 264, + 136, + 85, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 3, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 264, + 136, + 66, + 35, + 16, + 7 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 10792, + "phase": "B", + "reachable_states": 24, + "roles": [ + 623, + 624, + 401 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "incumbent": [ + 1 + ], + "index": 10795, + "phase": "B", + "reachable_states": 5, + "roles": [ + 622, + 623, + 403 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 264, + 136, + 85, + 51 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 1, + 6, + 50, + 82, + 136, + 264 + ] + ], + "incumbent": [ + 4, + 1 + ], + "index": 10796, + "phase": "B", + "reachable_states": 6, + "roles": [ + 623, + 625, + 403 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 51 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 264, + 136, + 65, + 32, + 19, + 7 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "incumbent": [ + 1 + ], + "index": 10798, + "phase": "B", + "reachable_states": 4, + "roles": [ + 622, + 624, + 626 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 2, + 5, + 49, + 80, + 136, + 264 + ] + ], + "incumbent": [ + 1 + ], + "index": 10799, + "phase": "B", + "reachable_states": 4, + "roles": [ + 624, + 625, + 626 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 82, + 51, + 10, + 7 + ], + [ + 257, + 129, + 82, + 51, + 9, + 7 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 10801, + "phase": "B", + "reachable_states": 4, + "roles": [ + 623, + 624, + 627 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "exit_bases": [ + [ + 257, + 129, + 82, + 51, + 9, + 7 + ], + [ + 7, + 24, + 43, + 74, + 136, + 264 + ], + [ + 7, + 27, + 40, + 73, + 136, + 264 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 10802, + "phase": "B", + "reachable_states": 4, + "roles": [ + 624, + 625, + 627 + ], + "start_bases": [ + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ], + [ + 7, + 51, + 82, + 136, + 264 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 414, + 81, + 51 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "exit_bases": [ + [ + 414, + 81, + 51 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11073, + "phase": "B", + "reachable_states": 9, + "roles": [ + 283, + 277, + 281 + ], + "start_bases": [ + [ + 81, + 51 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 463, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 388, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "exit_bases": [ + [ + 388, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11076, + "phase": "B", + "reachable_states": 9, + "roles": [ + 100, + 273, + 12 + ], + "start_bases": [ + [ + 388, + 51 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 41, + 26 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 388, + 81, + 51 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "exit_bases": [ + [ + 388, + 81, + 48, + 3 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11078, + "phase": "B", + "reachable_states": 9, + "roles": [ + 56, + 282, + 285 + ], + "start_bases": [ + [ + 388, + 51 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 81, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 463, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "exit_bases": [ + [ + 391, + 72, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 388, + 75, + 41, + 26 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11081, + "phase": "B", + "reachable_states": 9, + "roles": [ + 287, + 275, + 31 + ], + "start_bases": [ + [ + 463, + 51 + ], + [ + 388, + 75, + 41, + 26 + ], + [ + 41, + 26 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 273, + 145, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "exit_bases": [ + [ + 273, + 145, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11099, + "phase": "B", + "reachable_states": 9, + "roles": [ + 299, + 293, + 297 + ], + "start_bases": [ + [ + 273, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 145, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 324, + 196, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "exit_bases": [ + [ + 324, + 196, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11102, + "phase": "B", + "reachable_states": 9, + "roles": [ + 54, + 289, + 101 + ], + "start_bases": [ + [ + 196, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 324, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 273, + 196, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "exit_bases": [ + [ + 273, + 136, + 76, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11104, + "phase": "B", + "reachable_states": 9, + "roles": [ + 102, + 298, + 301 + ], + "start_bases": [ + [ + 196, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 273, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 324, + 145, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "exit_bases": [ + [ + 264, + 145, + 76, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 273, + 145, + 85, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11107, + "phase": "B", + "reachable_states": 9, + "roles": [ + 303, + 291, + 55 + ], + "start_bases": [ + [ + 145, + 51 + ], + [ + 273, + 145, + 85, + 51 + ], + [ + 324, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 385, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "exit_bases": [ + [ + 385, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11127, + "phase": "B", + "reachable_states": 9, + "roles": [ + 315, + 309, + 313 + ], + "start_bases": [ + [ + 385, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 44, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 429, + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "exit_bases": [ + [ + 429, + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11130, + "phase": "B", + "reachable_states": 9, + "roles": [ + 48, + 305, + 98 + ], + "start_bases": [ + [ + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 487, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 385, + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "exit_bases": [ + [ + 385, + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 384, + 74, + 44, + 30, + 1 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11132, + "phase": "B", + "reachable_states": 7, + "roles": [ + 32, + 314, + 317 + ], + "start_bases": [ + [ + 385, + 74, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 385, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 459, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "exit_bases": [ + [ + 391, + 76, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11135, + "phase": "B", + "reachable_states": 9, + "roles": [ + 319, + 307, + 85 + ], + "start_bases": [ + [ + 44, + 30 + ], + [ + 385, + 74, + 44, + 30 + ], + [ + 487, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 321, + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "exit_bases": [ + [ + 321, + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11154, + "phase": "B", + "reachable_states": 9, + "roles": [ + 331, + 325, + 329 + ], + "start_bases": [ + [ + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 321, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 266, + 138, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "exit_bases": [ + [ + 266, + 138, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11157, + "phase": "B", + "reachable_states": 9, + "roles": [ + 34, + 321, + 49 + ], + "start_bases": [ + [ + 266, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 138, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 266, + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "exit_bases": [ + [ + 266, + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 266, + 138, + 74, + 30, + 1 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11159, + "phase": "B", + "reachable_states": 7, + "roles": [ + 50, + 330, + 333 + ], + "start_bases": [ + [ + 266, + 193, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 193, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 321, + 138, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "exit_bases": [ + [ + 288, + 138, + 97, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 266, + 138, + 75, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11162, + "phase": "B", + "reachable_states": 9, + "roles": [ + 335, + 323, + 33 + ], + "start_bases": [ + [ + 321, + 30 + ], + [ + 266, + 138, + 75, + 30 + ], + [ + 138, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 429, + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "exit_bases": [ + [ + 429, + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11180, + "phase": "B", + "reachable_states": 9, + "roles": [ + 347, + 341, + 345 + ], + "start_bases": [ + [ + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 491, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 416, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "exit_bases": [ + [ + 416, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 257, + 161, + 70, + 19, + 13 + ] + ], + "incumbent": [ + 1, + 1, + 1, + 1 + ], + "index": 11183, + "phase": "B", + "reachable_states": 9, + "roles": [ + 82, + 337, + 6 + ], + "start_bases": [ + [ + 416, + 30 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 19, + 13 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 416, + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "exit_bases": [ + [ + 416, + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11185, + "phase": "B", + "reachable_states": 7, + "roles": [ + 75, + 346, + 349 + ], + "start_bases": [ + [ + 416, + 70, + 30 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 70, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 486, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ] + ], + "exit_bases": [ + [ + 486, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 257, + 161, + 70, + 19, + 13 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11188, + "phase": "B", + "reachable_states": 7, + "roles": [ + 351, + 339, + 1 + ], + "start_bases": [ + [ + 486, + 19, + 13 + ], + [ + 416, + 70, + 19, + 13 + ], + [ + 19, + 13 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 262, + 134, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "exit_bases": [ + [ + 262, + 134, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11205, + "phase": "B", + "reachable_states": 9, + "roles": [ + 363, + 357, + 361 + ], + "start_bases": [ + [ + 262, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 134, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 352, + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "exit_bases": [ + [ + 352, + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11208, + "phase": "B", + "reachable_states": 9, + "roles": [ + 73, + 353, + 83 + ], + "start_bases": [ + [ + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 352, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 262, + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "exit_bases": [ + [ + 262, + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11210, + "phase": "B", + "reachable_states": 7, + "roles": [ + 84, + 362, + 365 + ], + "start_bases": [ + [ + 262, + 224, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 262, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 352, + 134, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "exit_bases": [ + [ + 352, + 134, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 262, + 134, + 102, + 30 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11213, + "phase": "B", + "reachable_states": 7, + "roles": [ + 367, + 355, + 74 + ], + "start_bases": [ + [ + 352, + 134, + 30 + ], + [ + 262, + 134, + 102, + 30 + ], + [ + 352, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 392, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "exit_bases": [ + [ + 392, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11231, + "phase": "B", + "reachable_states": 9, + "roles": [ + 379, + 373, + 377 + ], + "start_bases": [ + [ + 392, + 51 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 37, + 22 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 414, + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "exit_bases": [ + [ + 414, + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11234, + "phase": "B", + "reachable_states": 9, + "roles": [ + 67, + 369, + 80 + ], + "start_bases": [ + [ + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 477, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 392, + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "exit_bases": [ + [ + 392, + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11236, + "phase": "B", + "reachable_states": 7, + "roles": [ + 3, + 378, + 381 + ], + "start_bases": [ + [ + 392, + 67, + 51 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 392, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 459, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "exit_bases": [ + [ + 459, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11239, + "phase": "B", + "reachable_states": 7, + "roles": [ + 383, + 371, + 88 + ], + "start_bases": [ + [ + 459, + 37, + 22 + ], + [ + 392, + 67, + 37, + 22 + ], + [ + 477, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 328, + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "exit_bases": [ + [ + 328, + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11260, + "phase": "B", + "reachable_states": 9, + "roles": [ + 395, + 389, + 393 + ], + "start_bases": [ + [ + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 328, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 259, + 131, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "exit_bases": [ + [ + 259, + 131, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11263, + "phase": "B", + "reachable_states": 9, + "roles": [ + 5, + 385, + 68 + ], + "start_bases": [ + [ + 259, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 131, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 259, + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "exit_bases": [ + [ + 259, + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11265, + "phase": "B", + "reachable_states": 7, + "roles": [ + 69, + 394, + 397 + ], + "start_bases": [ + [ + 259, + 200, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 200, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 328, + 131, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "exit_bases": [ + [ + 328, + 131, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 259, + 131, + 75, + 51 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11268, + "phase": "B", + "reachable_states": 7, + "roles": [ + 399, + 387, + 4 + ], + "start_bases": [ + [ + 328, + 131, + 51 + ], + [ + 259, + 131, + 75, + 51 + ], + [ + 131, + 51 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "incumbent": [ + 4, + 4 + ], + "index": 11472, + "phase": "B", + "reachable_states": 24, + "roles": [ + 586, + 587, + 349 + ], + "start_bases": [ + [], + [], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 1, + 1 + ], + [ + 4, + 4 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 266, + 138, + 74, + 45, + 30 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 11473, + "phase": "B", + "reachable_states": 24, + "roles": [ + 587, + 588, + 349 + ], + "start_bases": [ + [], + [], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "incumbent": [], + "index": 11475, + "phase": "B", + "reachable_states": 4, + "roles": [ + 586, + 587, + 243 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 32, + 19, + 13 + ] + ], + "incumbent": [ + 4, + 1 + ], + "index": 11476, + "phase": "B", + "reachable_states": 6, + "roles": [ + 587, + 589, + 243 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 271, + 143, + 79, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "incumbent": [ + 1 + ], + "index": 11478, + "phase": "B", + "reachable_states": 4, + "roles": [ + 586, + 588, + 365 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 37, + 22, + 8 + ] + ], + "incumbent": [ + 1 + ], + "index": 11479, + "phase": "B", + "reachable_states": 4, + "roles": [ + 588, + 589, + 365 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 41, + 26, + 4 + ], + [ + 320, + 192, + 44, + 30, + 1 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11481, + "phase": "B", + "reachable_states": 4, + "roles": [ + 587, + 588, + 361 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "exit_bases": [ + [ + 320, + 192, + 44, + 30, + 1 + ], + [ + 262, + 134, + 70, + 45, + 30 + ], + [ + 259, + 131, + 67, + 45, + 30 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11482, + "phase": "B", + "reachable_states": 4, + "roles": [ + 588, + 589, + 361 + ], + "start_bases": [ + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ], + [ + 320, + 192, + 45, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 5, + 5 + ], + "index": 11495, + "phase": "B", + "reachable_states": 29, + "roles": [ + 590, + 591, + 558 + ], + "start_bases": [ + [], + [], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1, + 1 + ], + [ + 3, + 3, + 2, + 2 + ], + [ + 4, + 4, + 1, + 1 + ], + [ + 5, + 5 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 264, + 145, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 5, + 5, + 1 + ], + "index": 11496, + "phase": "B", + "reachable_states": 29, + "roles": [ + 591, + 592, + 558 + ], + "start_bases": [ + [], + [], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1, + 1, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1, + 1, + 1 + ], + [ + 3, + 3, + 2, + 2, + 1 + ], + [ + 4, + 4, + 1, + 1, + 1 + ], + [ + 5, + 5, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [], + "index": 11499, + "phase": "B", + "reachable_states": 4, + "roles": [ + 590, + 591, + 559 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 401, + 80, + 32, + 8, + 5, + 2 + ] + ], + "incumbent": [ + 5, + 1 + ], + "index": 11500, + "phase": "B", + "reachable_states": 6, + "roles": [ + 591, + 593, + 559 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 5, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 385, + 72, + 40, + 24, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 1 + ], + "index": 11503, + "phase": "B", + "reachable_states": 4, + "roles": [ + 590, + 592, + 544 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 280, + 129, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 1 + ], + "index": 11504, + "phase": "B", + "reachable_states": 4, + "roles": [ + 592, + 593, + 544 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 408, + 80, + 40, + 4, + 2, + 1 + ], + [ + 273, + 136, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11506, + "phase": "B", + "reachable_states": 5, + "roles": [ + 591, + 592, + 405 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "exit_bases": [ + [ + 273, + 136, + 80, + 40, + 5, + 2 + ], + [ + 392, + 65, + 40, + 17, + 5, + 2 + ], + [ + 257, + 152, + 80, + 40, + 5, + 2 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11507, + "phase": "B", + "reachable_states": 4, + "roles": [ + 592, + 593, + 405 + ], + "start_bases": [ + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ], + [ + 409, + 80, + 40, + 5, + 2 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 272, + 144, + 74, + 42, + 6, + 1 + ] + ], + "incumbent": [ + 4, + 4, + 2 + ], + "index": 11524, + "phase": "B", + "reachable_states": 24, + "roles": [ + 595, + 596, + 410 + ], + "start_bases": [ + [], + [], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 2, + 1, + 1 + ], + [ + 4, + 4, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "incumbent": [], + "index": 11526, + "phase": "B", + "reachable_states": 4, + "roles": [ + 594, + 595, + 417 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 272, + 144, + 67, + 34, + 8, + 7 + ] + ], + "incumbent": [ + 4, + 2 + ], + "index": 11527, + "phase": "B", + "reachable_states": 6, + "roles": [ + 595, + 597, + 417 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 4, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 266, + 138, + 75, + 42, + 26, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "incumbent": [ + 2 + ], + "index": 11529, + "phase": "B", + "reachable_states": 4, + "roles": [ + 594, + 596, + 419 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 259, + 131, + 75, + 42, + 19, + 7 + ] + ], + "incumbent": [ + 2 + ], + "index": 11530, + "phase": "B", + "reachable_states": 4, + "roles": [ + 596, + 597, + 419 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 272, + 144, + 72, + 41, + 4, + 3 + ], + [ + 264, + 136, + 75, + 42, + 24, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "incumbent": [ + 2, + 2 + ], + "index": 11532, + "phase": "B", + "reachable_states": 8, + "roles": [ + 595, + 596, + 421 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "exit_bases": [ + [ + 264, + 136, + 75, + 42, + 24, + 7 + ], + [ + 257, + 129, + 75, + 42, + 17, + 7 + ], + [ + 272, + 144, + 65, + 32, + 10, + 7 + ] + ], + "incumbent": [ + 2, + 2, + 2 + ], + "index": 11533, + "phase": "B", + "reachable_states": 20, + "roles": [ + 596, + 597, + 421 + ], + "start_bases": [ + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ], + [ + 144, + 75, + 42, + 7 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 75, + 42, + 25 + ] + ], + "exit_bases": [ + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 75, + 42, + 25 + ] + ], + "incumbent": [ + 4, + 4 + ], + "index": 11551, + "phase": "B", + "reachable_states": 24, + "roles": [ + 598, + 599, + 1 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 260, + 132, + 75, + 42, + 25 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 1, + 1 + ], + [ + 4, + 4 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 75, + 42, + 25 + ] + ], + "exit_bases": [ + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 75, + 42, + 25 + ], + [ + 260, + 132, + 66, + 35, + 16, + 9 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 11552, + "phase": "B", + "reachable_states": 24, + "roles": [ + 599, + 600, + 1 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 260, + 132, + 75, + 42, + 25 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 391, + 68, + 34, + 17 + ], + [ + 391, + 68, + 34, + 17 + ] + ], + "exit_bases": [ + [ + 391, + 68, + 34, + 17 + ], + [ + 391, + 68, + 34, + 17 + ], + [ + 391, + 68, + 34, + 17 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 11575, + "phase": "B", + "reachable_states": 19, + "roles": [ + 602, + 603, + 426 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 391, + 68, + 34, + 17 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 391, + 68, + 34, + 17 + ], + [ + 391, + 68, + 34, + 17 + ] + ], + "exit_bases": [ + [ + 391, + 68, + 34, + 17 + ], + [ + 391, + 68, + 34, + 17 + ], + [ + 385, + 66, + 34, + 17, + 8, + 6 + ] + ], + "incumbent": [ + 3, + 3, + 2 + ], + "index": 11576, + "phase": "B", + "reachable_states": 19, + "roles": [ + 603, + 604, + 426 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 391, + 68, + 34, + 17 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1 + ], + [ + 3, + 3, + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ] + ], + "exit_bases": [ + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ] + ], + "incumbent": [ + 4, + 4 + ], + "index": 11596, + "phase": "B", + "reachable_states": 24, + "roles": [ + 606, + 607, + 545 + ], + "start_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 1, + 1 + ], + [ + 4, + 4 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ] + ], + "exit_bases": [ + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ], + [ + 257, + 129, + 66, + 36, + 16, + 14 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 11597, + "phase": "B", + "reachable_states": 24, + "roles": [ + 607, + 608, + 545 + ], + "start_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 257, + 129, + 76, + 42, + 30 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 423, + 65, + 20, + 10 + ], + [ + 423, + 65, + 20, + 10 + ] + ], + "exit_bases": [ + [ + 423, + 65, + 20, + 10 + ], + [ + 423, + 65, + 20, + 10 + ], + [ + 423, + 65, + 20, + 10 + ] + ], + "incumbent": [ + 4, + 4 + ], + "index": 11623, + "phase": "B", + "reachable_states": 24, + "roles": [ + 610, + 611, + 250 + ], + "start_bases": [ + [], + [], + [ + 423, + 65, + 20, + 10 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 1, + 1 + ], + [ + 4, + 4 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 423, + 65, + 20, + 10 + ], + [ + 423, + 65, + 20, + 10 + ] + ], + "exit_bases": [ + [ + 423, + 65, + 20, + 10 + ], + [ + 423, + 65, + 20, + 10 + ], + [ + 388, + 65, + 32, + 20, + 9, + 3 + ] + ], + "incumbent": [ + 4, + 4, + 2 + ], + "index": 11624, + "phase": "B", + "reachable_states": 24, + "roles": [ + 611, + 612, + 250 + ], + "start_bases": [ + [], + [], + [ + 423, + 65, + 20, + 10 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 2, + 1, + 1 + ], + [ + 4, + 4, + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "incumbent": [ + 4, + 4 + ], + "index": 11647, + "phase": "B", + "reachable_states": 24, + "roles": [ + 614, + 615, + 524 + ], + "start_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2 + ], + [ + 3, + 3, + 1, + 1 + ], + [ + 4, + 4 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 66, + 16, + 9, + 7 + ] + ], + "incumbent": [ + 4, + 4, + 1 + ], + "index": 11648, + "phase": "B", + "reachable_states": 24, + "roles": [ + 615, + 616, + 524 + ], + "start_bases": [ + [ + 30 + ], + [ + 30 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1 + ], + [ + 4, + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "incumbent": [], + "index": 11651, + "phase": "B", + "reachable_states": 4, + "roles": [ + 614, + 615, + 557 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 265, + 137, + 75, + 41, + 25, + 7 + ] + ], + "incumbent": [ + 4, + 1 + ], + "index": 11652, + "phase": "B", + "reachable_states": 6, + "roles": [ + 615, + 617, + 557 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 30 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 4, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 67, + 17, + 8, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "incumbent": [ + 1 + ], + "index": 11654, + "phase": "B", + "reachable_states": 4, + "roles": [ + 614, + 616, + 536 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 264, + 136, + 75, + 40, + 25, + 7 + ] + ], + "incumbent": [ + 1 + ], + "index": 11655, + "phase": "B", + "reachable_states": 4, + "roles": [ + 616, + 617, + 536 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 75, + 34, + 25, + 7 + ], + [ + 259, + 131, + 75, + 35, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11657, + "phase": "B", + "reachable_states": 5, + "roles": [ + 615, + 616, + 442 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "exit_bases": [ + [ + 259, + 131, + 75, + 35, + 25, + 7 + ], + [ + 288, + 160, + 72, + 25, + 4, + 3 + ], + [ + 288, + 160, + 73, + 25, + 5, + 2 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11658, + "phase": "B", + "reachable_states": 4, + "roles": [ + 616, + 617, + 442 + ], + "start_bases": [ + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ], + [ + 288, + 160, + 75, + 25, + 7 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "incumbent": [ + 5, + 5 + ], + "index": 11672, + "phase": "B", + "reachable_states": 29, + "roles": [ + 618, + 619, + 333 + ], + "start_bases": [ + [], + [], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1, + 1 + ], + [ + 3, + 3, + 2, + 2 + ], + [ + 4, + 4, + 1, + 1 + ], + [ + 5, + 5 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 392, + 66, + 34, + 24, + 6, + 1 + ] + ], + "incumbent": [ + 5, + 5, + 1 + ], + "index": 11673, + "phase": "B", + "reachable_states": 29, + "roles": [ + 619, + 620, + 333 + ], + "start_bases": [ + [], + [], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 2, + 1, + 1, + 1 + ], + [ + 3, + 3, + 1, + 1, + 1, + 1, + 1 + ], + [ + 3, + 3, + 2, + 2, + 1 + ], + [ + 4, + 4, + 1, + 1, + 1 + ], + [ + 5, + 5, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "incumbent": [], + "index": 11675, + "phase": "B", + "reachable_states": 4, + "roles": [ + 618, + 619, + 317 + ], + "start_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 296, + 130, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "incumbent": [ + 1, + 1 + ], + "index": 11679, + "phase": "B", + "reachable_states": 5, + "roles": [ + 618, + 620, + 257 + ], + "start_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 427, + 96, + 24, + 6 + ] + ], + "terminal_profiles": [ + [ + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 424, + 96, + 24, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 1 + ], + "index": 11680, + "phase": "B", + "reachable_states": 4, + "roles": [ + 620, + 621, + 257 + ], + "start_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 258, + 168, + 96, + 24, + 6, + 1 + ], + [ + 418, + 96, + 16, + 8, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11682, + "phase": "B", + "reachable_states": 5, + "roles": [ + 619, + 620, + 245 + ], + "start_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 427, + 96, + 24, + 6 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "exit_bases": [ + [ + 418, + 96, + 16, + 8, + 6, + 1 + ], + [ + 290, + 136, + 96, + 24, + 6, + 1 + ], + [ + 386, + 72, + 40, + 24, + 6, + 1 + ] + ], + "incumbent": [ + 1, + 1, + 1 + ], + "index": 11683, + "phase": "B", + "reachable_states": 4, + "roles": [ + 620, + 621, + 245 + ], + "start_bases": [ + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ], + [ + 426, + 96, + 24, + 6, + 1 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 11705, + "phase": "B", + "reachable_states": 19, + "roles": [ + 628, + 629, + 241 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 400, + 65, + 48, + 9, + 4, + 3 + ] + ], + "incumbent": [ + 3, + 3, + 2 + ], + "index": 11706, + "phase": "B", + "reachable_states": 19, + "roles": [ + 629, + 630, + 241 + ], + "start_bases": [ + [ + 51 + ], + [ + 51 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2, + 1, + 1 + ], + [ + 3, + 3, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "incumbent": [], + "index": 11708, + "phase": "B", + "reachable_states": 4, + "roles": [ + 628, + 629, + 234 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 3, + 4, + 48, + 72, + 144, + 265 + ] + ], + "incumbent": [ + 3, + 2 + ], + "index": 11709, + "phase": "B", + "reachable_states": 6, + "roles": [ + 629, + 631, + 234 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 51 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 3, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 280, + 129, + 72, + 48, + 4, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "incumbent": [ + 2 + ], + "index": 11711, + "phase": "B", + "reachable_states": 4, + "roles": [ + 628, + 630, + 229 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 3, + 4, + 24, + 40, + 72, + 385 + ] + ], + "incumbent": [ + 2 + ], + "index": 11712, + "phase": "B", + "reachable_states": 4, + "roles": [ + 630, + 631, + 229 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 257, + 152, + 72, + 48, + 4, + 3 + ], + [ + 393, + 72, + 32, + 16, + 4, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "incumbent": [ + 2, + 2 + ], + "index": 11714, + "phase": "B", + "reachable_states": 8, + "roles": [ + 629, + 630, + 227 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "exit_bases": [ + [ + 393, + 72, + 32, + 16, + 4, + 3 + ], + [ + 3, + 4, + 48, + 72, + 137, + 272 + ], + [ + 1, + 2, + 4, + 48, + 72, + 408 + ] + ], + "incumbent": [ + 2, + 2, + 2 + ], + "index": 11715, + "phase": "B", + "reachable_states": 20, + "roles": [ + 630, + 631, + 227 + ], + "start_bases": [ + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ], + [ + 413, + 72, + 48, + 3 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "exit_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "incumbent": [], + "index": 11735, + "phase": "B", + "reachable_states": 4, + "roles": [ + 49, + 83, + 225 + ], + "start_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "exit_bases": [ + [ + 388, + 65, + 36, + 16, + 9, + 3 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "incumbent": [ + 2 + ], + "index": 11739, + "phase": "B", + "reachable_states": 4, + "roles": [ + 49, + 98, + 281 + ], + "start_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "exit_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 276, + 131, + 66, + 36, + 9 + ] + ], + "incumbent": [ + 1 + ], + "index": 11740, + "phase": "B", + "reachable_states": 4, + "roles": [ + 98, + 101, + 281 + ], + "start_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "exit_bases": [ + [ + 387, + 66, + 32, + 16, + 9, + 4 + ], + [ + 262, + 129, + 66, + 36, + 16, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "incumbent": [ + 2, + 2 + ], + "index": 11742, + "phase": "B", + "reachable_states": 8, + "roles": [ + 83, + 98, + 393 + ], + "start_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "exit_bases": [ + [ + 262, + 129, + 66, + 36, + 16, + 9 + ], + [ + 406, + 66, + 36, + 8, + 1 + ], + [ + 259, + 148, + 66, + 36, + 9 + ] + ], + "incumbent": [ + 2, + 1, + 1 + ], + "index": 11743, + "phase": "B", + "reachable_states": 4, + "roles": [ + 98, + 101, + 393 + ], + "start_bases": [ + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ], + [ + 407, + 66, + 36, + 9 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "incumbent": [], + "index": 11763, + "phase": "B", + "reachable_states": 4, + "roles": [ + 68, + 80, + 377 + ], + "start_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "exit_bases": [ + [ + 257, + 129, + 76, + 45, + 25, + 3 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "incumbent": [ + 2 + ], + "index": 11767, + "phase": "B", + "reachable_states": 4, + "roles": [ + 68, + 88, + 381 + ], + "start_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 84, + 44, + 1 + ] + ], + "incumbent": [ + 1 + ], + "index": 11768, + "phase": "B", + "reachable_states": 4, + "roles": [ + 88, + 31, + 381 + ], + "start_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 72, + 41, + 25, + 4 + ], + [ + 258, + 130, + 70, + 39, + 19, + 10 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "incumbent": [ + 2, + 2 + ], + "index": 11770, + "phase": "B", + "reachable_states": 8, + "roles": [ + 80, + 88, + 345 + ], + "start_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "terminal_profiles": [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 2 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "exit_bases": [ + [ + 258, + 130, + 70, + 39, + 19, + 10 + ], + [ + 258, + 130, + 85, + 37, + 8 + ], + [ + 258, + 130, + 74, + 45, + 31 + ] + ], + "incumbent": [ + 2, + 1, + 1 + ], + "index": 11771, + "phase": "B", + "reachable_states": 4, + "roles": [ + 88, + 31, + 345 + ], + "start_bases": [ + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ], + [ + 258, + 130, + 85, + 45 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "exit_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "incumbent": [], + "index": 11791, + "phase": "B", + "reachable_states": 4, + "roles": [ + 33, + 55, + 329 + ], + "start_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "terminal_profiles": [ + [] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "exit_bases": [ + [ + 388, + 64, + 33, + 17, + 12, + 3 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "incumbent": [ + 2 + ], + "index": 11795, + "phase": "B", + "reachable_states": 4, + "roles": [ + 33, + 74, + 297 + ], + "start_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "exit_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 259, + 132, + 64, + 33, + 18, + 12 + ] + ], + "incumbent": [ + 2 + ], + "index": 11796, + "phase": "B", + "reachable_states": 4, + "roles": [ + 74, + 85, + 297 + ], + "start_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "terminal_profiles": [ + [ + 2 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "exit_bases": [ + [ + 387, + 64, + 33, + 18, + 8, + 4 + ], + [ + 385, + 70, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "incumbent": [ + 2, + 1 + ], + "index": 11798, + "phase": "B", + "reachable_states": 4, + "roles": [ + 55, + 74, + 313 + ], + "start_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "terminal_profiles": [ + [ + 2, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "exit_bases": [ + [ + 385, + 70, + 33, + 18, + 12 + ], + [ + 262, + 193, + 33, + 18, + 12 + ], + [ + 260, + 131, + 64, + 33, + 18, + 12 + ] + ], + "incumbent": [ + 2, + 1, + 1 + ], + "index": 11799, + "phase": "B", + "reachable_states": 4, + "roles": [ + 74, + 85, + 313 + ], + "start_bases": [ + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ], + [ + 455, + 33, + 18, + 12 + ] + ], + "terminal_profiles": [ + [ + 2, + 1, + 1 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "exit_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 12491, + "phase": "cleanup_tail", + "reachable_states": 17, + "roles": [ + 408, + 567, + 105 + ], + "start_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 1, + 6, + 50, + 82, + 136, + 264 + ], + [ + 257, + 129, + 68, + 34, + 22, + 8 + ] + ], + "terminal_profiles": [ + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "exit_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 12494, + "phase": "cleanup_tail", + "reachable_states": 17, + "roles": [ + 412, + 569, + 414 + ], + "start_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 3, + 4, + 48, + 72, + 144, + 265 + ], + [ + 10, + 20, + 32, + 65, + 132, + 259 + ] + ], + "terminal_profiles": [ + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + 1, + -1 + ], + "contact_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "exit_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 12497, + "phase": "cleanup_tail", + "reachable_states": 17, + "roles": [ + 424, + 575, + 44 + ], + "start_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 7, + 27, + 40, + 73, + 136, + 264 + ], + [ + 2, + 8, + 20, + 32, + 65, + 389 + ] + ], + "terminal_profiles": [ + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + -1, + -1 + ], + "contact_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "exit_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 3, + 3 + ], + "index": 12500, + "phase": "cleanup_tail", + "reachable_states": 17, + "roles": [ + 428, + 577, + 430 + ], + "start_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 1, + 2, + 4, + 48, + 72, + 408 + ], + [ + 257, + 129, + 73, + 42, + 27, + 5 + ] + ], + "terminal_profiles": [ + [ + 2, + 2, + 1, + 1 + ], + [ + 3, + 3 + ] + ] + }, + { + "coefficients": [ + -1, + 1 + ], + "contact_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "exit_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "incumbent": [ + 1 + ], + "index": 12655, + "phase": "cleanup_tail", + "reachable_states": 6, + "roles": [ + 40, + 18, + 226 + ], + "start_bases": [ + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + [ + 256, + 128, + 64, + 34, + 16, + 10, + 4, + 1 + ], + [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ] + ], + "terminal_profiles": [ + [ + 1 + ] + ] + } + ] +} diff --git a/research/pr4546-extended-ceilings/PR4582-RESULT.json b/research/pr4546-extended-ceilings/PR4582-RESULT.json new file mode 100644 index 0000000000..3e13f2b641 --- /dev/null +++ b/research/pr4546-extended-ceilings/PR4582-RESULT.json @@ -0,0 +1,162 @@ +{ + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "controls": { + "accepted_geometric_prefixes": 496, + "actual_geometric_prefixes": 894, + "chronology_mutation_rejected": true, + "cost_order_mutation_rejected": true, + "directed_coefficient_prefixes": 22621, + "incompatible_contact_rejected": true, + "positive_improvement_fixture": true, + "terminal_mass_mutation_rejected": true, + "zero_rank_loop_checked": true + }, + "dijkstra_cost_checks": 248, + "new_kappa": false, + "profile_count_histogram": { + "1": 93, + "2": 9, + "3": 6, + "4": 2, + "5": 13, + "7": 4, + "9": 1 + }, + "reachable_states": 1496, + "schema": "receiver-window-all-length-floor/v1", + "source_pr4470_head": "b9a13c1673e0e9697de410de16e8bbf3207a7363", + "status": "PASS_RECEIVER_WINDOW_ALL_LENGTH_FLOOR", + "terminal_profiles_checked": 239, + "transition_edges": 4730, + "windows_checked": 128, + "windows": [ + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[], []], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[], [], []], "entrance_dimensions": [0, 0, 0], "exit_bases": [[], [224, 30], []], "exit_dimensions": [0, 2, 0], "incumbent_gaps_by_field": [[], [2], []], "incumbent_profile": [2], "index": 10554, "pair_bounds_ab_ax_bx": [[0, 0], [0, 0], [0, 0]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [162, 172, 513], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, 1], "contact_bases": [[], []], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[], [], []], "entrance_dimensions": [0, 0, 0], "exit_bases": [[224, 30], [], []], "exit_dimensions": [2, 0, 0], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 10555, "pair_bounds_ab_ax_bx": [[0, 0], [0, 0], [0, 0]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [172, 196, 513], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[30], [30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[], [], [30]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[416, 30], [30], [30]], "exit_dimensions": [2, 1, 1], "incumbent_gaps_by_field": [[1, 1], [1], []], "incumbent_profile": [1, 1, 1], "index": 10557, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[1, 1, 1]], "roles": [140, 144, 502], "transition_edges": 22}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[30], [30]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[], [], [30]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[30], [30], [30]], "exit_dimensions": [1, 1, 1], "incumbent_gaps_by_field": [[1], [1], []], "incumbent_profile": [1, 1], "index": 10558, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[1, 1]], "roles": [144, 187, 502], "transition_edges": 22}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, 1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[], [], [51]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[51], [388, 51], [51]], "exit_dimensions": [1, 2, 1], "incumbent_gaps_by_field": [[1], [1, 1], []], "incumbent_profile": [1, 1, 1], "index": 10560, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[1, 1, 1]], "roles": [168, 150, 548], "transition_edges": 22}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[], [], [51]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[388, 51], [51], [51]], "exit_dimensions": [2, 1, 1], "incumbent_gaps_by_field": [[1, 1], [1], []], "incumbent_profile": [1, 1, 1], "index": 10561, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[1, 1, 1]], "roles": [150, 115, 548], "transition_edges": 22}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[], [], [51]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[196, 51], [51], [51]], "exit_dimensions": [2, 1, 1], "incumbent_gaps_by_field": [[1, 1], [1], []], "incumbent_profile": [1, 1, 1], "index": 10563, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[1, 1, 1]], "roles": [131, 117, 560], "transition_edges": 22}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[], [51], [51]], "entrance_dimensions": [0, 1, 1], "exit_bases": [[51], [51], [51]], "exit_dimensions": [1, 1, 1], "incumbent_gaps_by_field": [[1], [], []], "incumbent_profile": [1], "index": 10564, "pair_bounds_ab_ax_bx": [[1, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[1]], "roles": [117, 584, 560], "transition_edges": 18}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[], []], "dijkstra_truncated_cost_minima": [3, 5, 6], "entrance_bases": [[], [], []], "entrance_dimensions": [0, 0, 0], "exit_bases": [[30], [491, 30], [459, 38, 30]], "exit_dimensions": [1, 2, 3], "incumbent_gaps_by_field": [[1], [2], [3]], "incumbent_profile": [3, 2, 1], "index": 10575, "pair_bounds_ab_ax_bx": [[0, 1], [0, 1], [0, 1]], "phase": "B", "reachable_states": 13, "relaxed_profiles": [[2, 1, 1, 1, 1], [2, 2, 1, 1], [3, 1, 1, 1], [3, 2, 1]], "roles": [205, 170, 452], "transition_edges": 51}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[30], [30]], "dijkstra_truncated_cost_minima": [3, 4], "entrance_bases": [[], [], [30]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[30], [30], [448, 21, 11]], "exit_dimensions": [1, 1, 3], "incumbent_gaps_by_field": [[1], [1], [2]], "incumbent_profile": [2, 1, 1], "index": 10577, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[2, 1, 1]], "roles": [118, 194, 453], "transition_edges": 22}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[], []], "dijkstra_truncated_cost_minima": [3, 5, 6], "entrance_bases": [[], [], []], "entrance_dimensions": [0, 0, 0], "exit_bases": [[51], [37, 22], [448, 38, 21]], "exit_dimensions": [1, 2, 3], "incumbent_gaps_by_field": [[1], [2], [3]], "incumbent_profile": [3, 2, 1], "index": 10579, "pair_bounds_ab_ax_bx": [[0, 1], [0, 1], [0, 1]], "phase": "B", "reachable_states": 13, "relaxed_profiles": [[2, 1, 1, 1, 1], [2, 2, 1, 1], [3, 1, 1, 1], [3, 2, 1]], "roles": [120, 207, 454], "transition_edges": 51}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [3, 4], "entrance_bases": [[], [], [51]], "entrance_dimensions": [0, 0, 1], "exit_bases": [[51], [51], [469, 51, 11]], "exit_dimensions": [1, 1, 3], "incumbent_gaps_by_field": [[1], [1], [2]], "incumbent_profile": [2, 1, 1], "index": 10581, "pair_bounds_ab_ax_bx": [[0, 1], [1, 1], [1, 1]], "phase": "B", "reachable_states": 7, "relaxed_profiles": [[2, 1, 1]], "roles": [192, 179, 455], "transition_edges": 22}, + {"accepting_states": 2, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[], []], "dijkstra_truncated_cost_minima": [2, 4, 5], "entrance_bases": [[], [], []], "entrance_dimensions": [0, 0, 0], "exit_bases": [[321, 30], [], [289, 140, 30]], "exit_dimensions": [2, 0, 3], "incumbent_gaps_by_field": [[2], [], [3]], "incumbent_profile": [3, 2], "index": 10607, "pair_bounds_ab_ax_bx": [[0, 0], [0, 1], [0, 0]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[2, 1, 1, 1], [3, 2]], "roles": [145, 135, 583], "transition_edges": 18}, + {"accepting_states": 12, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[51], [51]], "dijkstra_truncated_cost_minima": [3, 6, 8, 10], "entrance_bases": [[51], [51], [51]], "entrance_dimensions": [1, 1, 1], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [392, 67, 51]], "exit_dimensions": [5, 5, 3], "incumbent_gaps_by_field": [[4], [4], [2]], "incumbent_profile": [4, 4, 2], "index": 10788, "pair_bounds_ab_ax_bx": [[1, 5], [1, 1], [1, 1]], "phase": "B", "reachable_states": 26, "relaxed_profiles": [[2, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1, 1, 1], [2, 2, 2, 2, 2], [3, 3, 2, 1, 1], [4, 4, 2]], "roles": [622, 624, 548], "transition_edges": 70}, + {"accepting_states": 33, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[51], [51], [264, 136, 85, 51]], "entrance_dimensions": [1, 1, 4], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 10791, "pair_bounds_ab_ax_bx": [[1, 5], [4, 5], [4, 5]], "phase": "B", "reachable_states": 91, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1, 1], [2, 2, 2, 2, 1], [3, 2, 1, 1, 1, 1], [3, 3, 1, 1, 1], [4, 3, 1, 1], [4, 4, 1]], "roles": [622, 623, 401], "transition_edges": 352}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[51], [51], [7, 51, 82, 136, 264]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [264, 136, 66, 35, 16, 7]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 10792, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1], [3, 3, 1, 1, 1], [4, 4, 1]], "roles": [623, 624, 401], "transition_edges": 137}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [264, 136, 85, 51]], "entrance_dimensions": [5, 5, 4], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 10795, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [622, 623, 403], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [2, 3, 4, 5], "entrance_bases": [[7, 51, 82, 136, 264], [51], [7, 51, 82, 136, 264]], "entrance_dimensions": [5, 1, 5], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [1, 6, 50, 82, 136, 264]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [4], [1]], "incumbent_profile": [4, 1], "index": 10796, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[4, 1]], "roles": [623, 625, 403], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[264, 136, 65, 32, 19, 7], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[1], [], []], "incumbent_profile": [1], "index": 10798, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [622, 624, 626], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [2, 5, 49, 80, 136, 264]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 10799, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [624, 625, 626], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[258, 130, 82, 51, 10, 7], [257, 129, 82, 51, 9, 7], [7, 51, 82, 136, 264]], "exit_dimensions": [6, 6, 5], "incumbent_gaps_by_field": [[1], [1], []], "incumbent_profile": [1, 1], "index": 10801, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [623, 624, 627], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[7, 51, 82, 136, 264], [7, 51, 82, 136, 264], [7, 51, 82, 136, 264]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[257, 129, 82, 51, 9, 7], [7, 24, 43, 74, 136, 264], [7, 27, 40, 73, 136, 264]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 10802, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [624, 625, 627], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[414, 81, 51], [388, 75, 41, 26]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[81, 51], [388, 75, 41, 26], [463, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[414, 81, 51], [388, 75, 41, 26], [388, 75, 41, 26]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11073, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [283, 277, 281], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[388, 41, 26], [388, 75, 41, 26]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[388, 51], [388, 75, 41, 26], [41, 26]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[388, 41, 26], [388, 75, 41, 26], [388, 75, 41, 26]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11076, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [100, 273, 12], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[388, 81, 51], [388, 75, 41, 26]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[388, 51], [388, 75, 41, 26], [81, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[388, 81, 48, 3], [388, 75, 41, 26], [388, 75, 41, 26]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11078, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [56, 282, 285], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[463, 41, 26], [388, 75, 41, 26]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[463, 51], [388, 75, 41, 26], [41, 26]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[391, 72, 41, 26], [388, 75, 41, 26], [388, 75, 41, 26]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11081, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [287, 275, 31], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[273, 145, 51], [273, 145, 85, 51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[273, 51], [273, 145, 85, 51], [145, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[273, 145, 51], [273, 145, 85, 51], [273, 145, 85, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11099, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [299, 293, 297], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[324, 196, 51], [273, 145, 85, 51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[196, 51], [273, 145, 85, 51], [324, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[324, 196, 51], [273, 145, 85, 51], [273, 145, 85, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11102, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [54, 289, 101], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[273, 196, 51], [273, 145, 85, 51]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[196, 51], [273, 145, 85, 51], [273, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[273, 136, 76, 51], [273, 145, 85, 51], [273, 145, 85, 51]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11104, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [102, 298, 301], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[324, 145, 51], [273, 145, 85, 51]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[145, 51], [273, 145, 85, 51], [324, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[264, 145, 76, 51], [273, 145, 85, 51], [273, 145, 85, 51]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11107, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [303, 291, 55], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[385, 44, 30], [385, 74, 44, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[385, 30], [385, 74, 44, 30], [44, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[385, 44, 30], [385, 74, 44, 30], [385, 74, 44, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11127, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [315, 309, 313], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[429, 74, 30], [385, 74, 44, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[74, 30], [385, 74, 44, 30], [487, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[429, 74, 30], [385, 74, 44, 30], [385, 74, 44, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11130, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [48, 305, 98], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[385, 74, 30], [385, 74, 44, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[385, 74, 30], [385, 74, 44, 30], [385, 30]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[385, 74, 30], [385, 74, 44, 30], [384, 74, 44, 30, 1]], "exit_dimensions": [3, 4, 5], "incumbent_gaps_by_field": [[], [], [1, 1, 1]], "incumbent_profile": [1, 1, 1], "index": 11132, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [32, 314, 317], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[459, 44, 30], [385, 74, 44, 30]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[44, 30], [385, 74, 44, 30], [487, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[391, 76, 44, 30], [385, 74, 44, 30], [385, 74, 44, 30]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11135, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [319, 307, 85], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[321, 193, 30], [266, 138, 75, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[193, 30], [266, 138, 75, 30], [321, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[321, 193, 30], [266, 138, 75, 30], [266, 138, 75, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11154, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [331, 325, 329], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[266, 138, 30], [266, 138, 75, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[266, 30], [266, 138, 75, 30], [138, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[266, 138, 30], [266, 138, 75, 30], [266, 138, 75, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11157, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [34, 321, 49], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[266, 193, 30], [266, 138, 75, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[266, 193, 30], [266, 138, 75, 30], [193, 30]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[266, 193, 30], [266, 138, 75, 30], [266, 138, 74, 30, 1]], "exit_dimensions": [3, 4, 5], "incumbent_gaps_by_field": [[], [], [1, 1, 1]], "incumbent_profile": [1, 1, 1], "index": 11159, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [50, 330, 333], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[321, 138, 30], [266, 138, 75, 30]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[321, 30], [266, 138, 75, 30], [138, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[288, 138, 97, 30], [266, 138, 75, 30], [266, 138, 75, 30]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[1, 1], [], [1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11162, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [335, 323, 33], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[429, 70, 30], [416, 70, 19, 13]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[70, 30], [416, 70, 19, 13], [491, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[429, 70, 30], [416, 70, 19, 13], [416, 70, 19, 13]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11180, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [347, 341, 345], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[416, 19, 13], [416, 70, 19, 13]], "dijkstra_truncated_cost_minima": [4], "entrance_bases": [[416, 30], [416, 70, 19, 13], [19, 13]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[416, 19, 13], [416, 70, 19, 13], [257, 161, 70, 19, 13]], "exit_dimensions": [3, 4, 5], "incumbent_gaps_by_field": [[1], [], [1, 1, 1]], "incumbent_profile": [1, 1, 1, 1], "index": 11183, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1, 1]], "roles": [82, 337, 6], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[416, 70, 30], [416, 70, 19, 13]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[416, 70, 30], [416, 70, 19, 13], [70, 30]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[416, 70, 30], [416, 70, 19, 13], [416, 70, 19, 13]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11185, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [75, 346, 349], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[486, 19, 13], [416, 70, 19, 13]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[486, 19, 13], [416, 70, 19, 13], [19, 13]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[486, 19, 13], [416, 70, 19, 13], [257, 161, 70, 19, 13]], "exit_dimensions": [3, 4, 5], "incumbent_gaps_by_field": [[], [], [1, 1, 1]], "incumbent_profile": [1, 1, 1], "index": 11188, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [351, 339, 1], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[262, 134, 30], [262, 134, 102, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[262, 30], [262, 134, 102, 30], [134, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[262, 134, 30], [262, 134, 102, 30], [262, 134, 102, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11205, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [363, 357, 361], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[352, 224, 30], [262, 134, 102, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[224, 30], [262, 134, 102, 30], [352, 30]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[352, 224, 30], [262, 134, 102, 30], [262, 134, 102, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11208, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [73, 353, 83], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[262, 224, 30], [262, 134, 102, 30]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[262, 224, 30], [262, 134, 102, 30], [262, 30]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[262, 224, 30], [262, 134, 102, 30], [262, 134, 102, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11210, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [84, 362, 365], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[352, 134, 30], [262, 134, 102, 30]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[352, 134, 30], [262, 134, 102, 30], [352, 30]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[352, 134, 30], [262, 134, 102, 30], [262, 134, 102, 30]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11213, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [367, 355, 74], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[392, 37, 22], [392, 67, 37, 22]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[392, 51], [392, 67, 37, 22], [37, 22]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[392, 37, 22], [392, 67, 37, 22], [392, 67, 37, 22]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11231, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [379, 373, 377], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[414, 67, 51], [392, 67, 37, 22]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[67, 51], [392, 67, 37, 22], [477, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[414, 67, 51], [392, 67, 37, 22], [392, 67, 37, 22]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11234, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [67, 369, 80], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[392, 67, 51], [392, 67, 37, 22]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[392, 67, 51], [392, 67, 37, 22], [392, 51]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[392, 67, 51], [392, 67, 37, 22], [392, 67, 37, 22]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11236, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [3, 378, 381], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[459, 37, 22], [392, 67, 37, 22]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[459, 37, 22], [392, 67, 37, 22], [477, 51]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[459, 37, 22], [392, 67, 37, 22], [392, 67, 37, 22]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11239, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [383, 371, 88], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[328, 200, 51], [259, 131, 75, 51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[200, 51], [259, 131, 75, 51], [328, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[328, 200, 51], [259, 131, 75, 51], [259, 131, 75, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11260, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [395, 389, 393], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[259, 131, 51], [259, 131, 75, 51]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[259, 51], [259, 131, 75, 51], [131, 51]], "entrance_dimensions": [2, 4, 2], "exit_bases": [[259, 131, 51], [259, 131, 75, 51], [259, 131, 75, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[1], [], [1, 1]], "incumbent_profile": [1, 1, 1], "index": 11263, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [5, 385, 68], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[259, 200, 51], [259, 131, 75, 51]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[259, 200, 51], [259, 131, 75, 51], [200, 51]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[259, 200, 51], [259, 131, 75, 51], [259, 131, 75, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11265, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [69, 394, 397], "transition_edges": 6}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[328, 131, 51], [259, 131, 75, 51]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[328, 131, 51], [259, 131, 75, 51], [131, 51]], "entrance_dimensions": [3, 4, 2], "exit_bases": [[328, 131, 51], [259, 131, 75, 51], [259, 131, 75, 51]], "exit_dimensions": [3, 4, 4], "incumbent_gaps_by_field": [[], [], [1, 1]], "incumbent_profile": [1, 1], "index": 11268, "pair_bounds_ab_ax_bx": [null, [3, 3], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [399, 387, 4], "transition_edges": 6}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8], "entrance_bases": [[], [], [320, 192, 45, 30]], "entrance_dimensions": [0, 0, 4], "exit_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[4], [4], []], "incumbent_profile": [4, 4], "index": 11472, "pair_bounds_ab_ax_bx": [[0, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1], [2, 2, 2, 2], [3, 3, 1, 1], [4, 4]], "roles": [586, 587, 349], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[], [], [320, 192, 45, 30]], "entrance_dimensions": [0, 0, 4], "exit_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [266, 138, 74, 45, 30]], "exit_dimensions": [4, 4, 5], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 11473, "pair_bounds_ab_ax_bx": [[0, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1], [3, 3, 1, 1, 1], [4, 4, 1]], "roles": [587, 588, 349], "transition_edges": 137}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11475, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [586, 587, 243], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [2, 3, 4, 5], "entrance_bases": [[320, 192, 45, 30], [], [320, 192, 45, 30]], "entrance_dimensions": [4, 0, 4], "exit_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 32, 19, 13]], "exit_dimensions": [4, 4, 5], "incumbent_gaps_by_field": [[], [4], [1]], "incumbent_profile": [4, 1], "index": 11476, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[4, 1]], "roles": [587, 589, 243], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[271, 143, 79, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "exit_dimensions": [5, 4, 4], "incumbent_gaps_by_field": [[1], [], []], "incumbent_profile": [1], "index": 11478, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [586, 588, 365], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 37, 22, 8]], "exit_dimensions": [4, 4, 5], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11479, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [588, 589, 365], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[320, 192, 41, 26, 4], [320, 192, 44, 30, 1], [320, 192, 45, 30]], "exit_dimensions": [5, 5, 4], "incumbent_gaps_by_field": [[1], [1], []], "incumbent_profile": [1, 1], "index": 11481, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [587, 588, 361], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[320, 192, 45, 30], [320, 192, 45, 30]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[320, 192, 45, 30], [320, 192, 45, 30], [320, 192, 45, 30]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[320, 192, 44, 30, 1], [262, 134, 70, 45, 30], [259, 131, 67, 45, 30]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11482, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [588, 589, 361], "transition_edges": 12}, + {"accepting_states": 7, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8, 10], "entrance_bases": [[], [], [409, 80, 40, 5, 2]], "entrance_dimensions": [0, 0, 5], "exit_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[5], [5], []], "incumbent_profile": [5, 5], "index": 11495, "pair_bounds_ab_ax_bx": [[0, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 64, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1, 1], [3, 3, 1, 1, 1, 1], [3, 3, 2, 2], [4, 4, 1, 1], [5, 5]], "roles": [590, 591, 558], "transition_edges": 218}, + {"accepting_states": 7, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9, 11], "entrance_bases": [[], [], [409, 80, 40, 5, 2]], "entrance_dimensions": [0, 0, 5], "exit_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [264, 145, 80, 40, 5, 2]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[5], [5], [1]], "incumbent_profile": [5, 5, 1], "index": 11496, "pair_bounds_ab_ax_bx": [[0, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 64, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1, 1, 1], [3, 3, 1, 1, 1, 1, 1], [3, 3, 2, 2, 1], [4, 4, 1, 1, 1], [5, 5, 1]], "roles": [591, 592, 558], "transition_edges": 218}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11499, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [590, 591, 559], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [2, 3, 4, 5, 6], "entrance_bases": [[409, 80, 40, 5, 2], [], [409, 80, 40, 5, 2]], "entrance_dimensions": [5, 0, 5], "exit_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [401, 80, 32, 8, 5, 2]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [5], [1]], "incumbent_profile": [5, 1], "index": 11500, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[5, 1]], "roles": [591, 593, 559], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[385, 72, 40, 24, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[1], [], []], "incumbent_profile": [1], "index": 11503, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [590, 592, 544], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [280, 129, 80, 40, 5, 2]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11504, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [592, 593, 544], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [80, 40, 5, 2]], "entrance_dimensions": [5, 5, 4], "exit_bases": [[408, 80, 40, 4, 2, 1], [273, 136, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "exit_dimensions": [6, 6, 5], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11506, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [591, 592, 405], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[409, 80, 40, 5, 2], [409, 80, 40, 5, 2], [409, 80, 40, 5, 2]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[273, 136, 80, 40, 5, 2], [392, 65, 40, 17, 5, 2], [257, 152, 80, 40, 5, 2]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11507, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [592, 593, 405], "transition_edges": 12}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [3, 6, 8, 10], "entrance_bases": [[], [], [144, 75, 42, 7]], "entrance_dimensions": [0, 0, 4], "exit_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [272, 144, 74, 42, 6, 1]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[4], [4], [2]], "incumbent_profile": [4, 4, 2], "index": 11524, "pair_bounds_ab_ax_bx": [[0, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[2, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1, 1, 1], [2, 2, 2, 2, 2], [3, 3, 2, 1, 1], [4, 4, 2]], "roles": [595, 596, 410], "transition_edges": 137}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11526, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [594, 595, 417], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [2, 4, 5, 6], "entrance_bases": [[144, 75, 42, 7], [], [144, 75, 42, 7]], "entrance_dimensions": [4, 0, 4], "exit_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [272, 144, 67, 34, 8, 7]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[], [4], [2]], "incumbent_profile": [4, 2], "index": 11527, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[4, 2]], "roles": [595, 597, 417], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[266, 138, 75, 42, 26, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "exit_dimensions": [6, 4, 4], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 11529, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [594, 596, 419], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [259, 131, 75, 42, 19, 7]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[], [], [2]], "incumbent_profile": [2], "index": 11530, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [596, 597, 419], "transition_edges": 12}, + {"accepting_states": 2, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [2, 4], "entrance_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[272, 144, 72, 41, 4, 3], [264, 136, 75, 42, 24, 7], [144, 75, 42, 7]], "exit_dimensions": [6, 6, 4], "incumbent_gaps_by_field": [[2], [2], []], "incumbent_profile": [2, 2], "index": 11532, "pair_bounds_ab_ax_bx": [[4, 5], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[1, 1, 1, 1], [2, 2]], "roles": [595, 596, 421], "transition_edges": 18}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[144, 75, 42, 7], [144, 75, 42, 7]], "dijkstra_truncated_cost_minima": [3, 6], "entrance_bases": [[144, 75, 42, 7], [144, 75, 42, 7], [144, 75, 42, 7]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[264, 136, 75, 42, 24, 7], [257, 129, 75, 42, 17, 7], [272, 144, 65, 32, 10, 7]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[2], [2], [2]], "incumbent_profile": [2, 2, 2], "index": 11533, "pair_bounds_ab_ax_bx": [[4, 5], [4, 5], [4, 5]], "phase": "B", "reachable_states": 13, "relaxed_profiles": [[1, 1, 1, 1, 1, 1], [2, 1, 1, 1, 1], [2, 2, 2]], "roles": [596, 597, 421], "transition_edges": 51}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[260, 132, 75, 42, 25], [260, 132, 75, 42, 25]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8], "entrance_bases": [[51], [51], [260, 132, 75, 42, 25]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[260, 132, 75, 42, 25], [260, 132, 75, 42, 25], [260, 132, 75, 42, 25]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[4], [4], []], "incumbent_profile": [4, 4], "index": 11551, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1], [2, 2, 2, 2], [3, 3, 1, 1], [4, 4]], "roles": [598, 599, 1], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[260, 132, 75, 42, 25], [260, 132, 75, 42, 25]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[51], [51], [260, 132, 75, 42, 25]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[260, 132, 75, 42, 25], [260, 132, 75, 42, 25], [260, 132, 66, 35, 16, 9]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 11552, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1], [3, 3, 1, 1, 1], [4, 4, 1]], "roles": [599, 600, 1], "transition_edges": 137}, + {"accepting_states": 3, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[391, 68, 34, 17], [391, 68, 34, 17]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[51], [51], [391, 68, 34, 17]], "entrance_dimensions": [1, 1, 4], "exit_bases": [[391, 68, 34, 17], [391, 68, 34, 17], [391, 68, 34, 17]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[3], [3], []], "incumbent_profile": [3, 3], "index": 11575, "pair_bounds_ab_ax_bx": [[1, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 24, "relaxed_profiles": [[1, 1, 1, 1, 1, 1], [2, 2, 1, 1], [3, 3]], "roles": [602, 603, 426], "transition_edges": 79}, + {"accepting_states": 3, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[391, 68, 34, 17], [391, 68, 34, 17]], "dijkstra_truncated_cost_minima": [3, 6, 8], "entrance_bases": [[51], [51], [391, 68, 34, 17]], "entrance_dimensions": [1, 1, 4], "exit_bases": [[391, 68, 34, 17], [391, 68, 34, 17], [385, 66, 34, 17, 8, 6]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[3], [3], [2]], "incumbent_profile": [3, 3, 2], "index": 11576, "pair_bounds_ab_ax_bx": [[1, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 24, "relaxed_profiles": [[2, 1, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1], [3, 3, 2]], "roles": [603, 604, 426], "transition_edges": 79}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[257, 129, 76, 42, 30], [257, 129, 76, 42, 30]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8], "entrance_bases": [[30], [30], [257, 129, 76, 42, 30]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[257, 129, 76, 42, 30], [257, 129, 76, 42, 30], [257, 129, 76, 42, 30]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[4], [4], []], "incumbent_profile": [4, 4], "index": 11596, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1], [2, 2, 2, 2], [3, 3, 1, 1], [4, 4]], "roles": [606, 607, 545], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[257, 129, 76, 42, 30], [257, 129, 76, 42, 30]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[30], [30], [257, 129, 76, 42, 30]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[257, 129, 76, 42, 30], [257, 129, 76, 42, 30], [257, 129, 66, 36, 16, 14]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 11597, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1], [3, 3, 1, 1, 1], [4, 4, 1]], "roles": [607, 608, 545], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[423, 65, 20, 10], [423, 65, 20, 10]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8], "entrance_bases": [[], [], [423, 65, 20, 10]], "entrance_dimensions": [0, 0, 4], "exit_bases": [[423, 65, 20, 10], [423, 65, 20, 10], [423, 65, 20, 10]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[4], [4], []], "incumbent_profile": [4, 4], "index": 11623, "pair_bounds_ab_ax_bx": [[0, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1], [2, 2, 2, 2], [3, 3, 1, 1], [4, 4]], "roles": [610, 611, 250], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[423, 65, 20, 10], [423, 65, 20, 10]], "dijkstra_truncated_cost_minima": [3, 6, 8, 10], "entrance_bases": [[], [], [423, 65, 20, 10]], "entrance_dimensions": [0, 0, 4], "exit_bases": [[423, 65, 20, 10], [423, 65, 20, 10], [388, 65, 32, 20, 9, 3]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[4], [4], [2]], "incumbent_profile": [4, 4, 2], "index": 11624, "pair_bounds_ab_ax_bx": [[0, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[2, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1, 1, 1], [2, 2, 2, 2, 2], [3, 3, 2, 1, 1], [4, 4, 2]], "roles": [611, 612, 250], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8], "entrance_bases": [[30], [30], [288, 160, 75, 25, 7]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[4], [4], []], "incumbent_profile": [4, 4], "index": 11647, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1], [2, 2, 2, 2], [3, 3, 1, 1], [4, 4]], "roles": [614, 615, 524], "transition_edges": 137}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9], "entrance_bases": [[30], [30], [288, 160, 75, 25, 7]], "entrance_dimensions": [1, 1, 5], "exit_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 66, 16, 9, 7]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[4], [4], [1]], "incumbent_profile": [4, 4, 1], "index": 11648, "pair_bounds_ab_ax_bx": [[1, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 41, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1], [3, 3, 1, 1, 1], [4, 4, 1]], "roles": [615, 616, 524], "transition_edges": 137}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11651, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [614, 615, 557], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [2, 3, 4, 5], "entrance_bases": [[288, 160, 75, 25, 7], [30], [288, 160, 75, 25, 7]], "entrance_dimensions": [5, 1, 5], "exit_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [265, 137, 75, 41, 25, 7]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [4], [1]], "incumbent_profile": [4, 1], "index": 11652, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[4, 1]], "roles": [615, 617, 557], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[288, 160, 67, 17, 8, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[1], [], []], "incumbent_profile": [1], "index": 11654, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [614, 616, 536], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [264, 136, 75, 40, 25, 7]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11655, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [616, 617, 536], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25]], "entrance_dimensions": [5, 5, 4], "exit_bases": [[258, 130, 75, 34, 25, 7], [259, 131, 75, 35, 25, 7], [288, 160, 75, 25, 7]], "exit_dimensions": [6, 6, 5], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11657, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [615, 616, 442], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[288, 160, 75, 25, 7], [288, 160, 75, 25, 7], [288, 160, 75, 25, 7]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[259, 131, 75, 35, 25, 7], [288, 160, 72, 25, 4, 3], [288, 160, 73, 25, 5, 2]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11658, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [616, 617, 442], "transition_edges": 12}, + {"accepting_states": 7, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [2, 4, 6, 8, 10], "entrance_bases": [[], [], [426, 96, 24, 6, 1]], "entrance_dimensions": [0, 0, 5], "exit_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[5], [5], []], "incumbent_profile": [5, 5], "index": 11672, "pair_bounds_ab_ax_bx": [[0, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 64, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1, 1], [3, 3, 1, 1, 1, 1], [3, 3, 2, 2], [4, 4, 1, 1], [5, 5]], "roles": [618, 619, 333], "transition_edges": 218}, + {"accepting_states": 7, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [3, 5, 7, 9, 11], "entrance_bases": [[], [], [426, 96, 24, 6, 1]], "entrance_dimensions": [0, 0, 5], "exit_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [392, 66, 34, 24, 6, 1]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[5], [5], [1]], "incumbent_profile": [5, 5, 1], "index": 11673, "pair_bounds_ab_ax_bx": [[0, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 64, "relaxed_profiles": [[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], [2, 2, 1, 1, 1, 1, 1, 1, 1], [2, 2, 2, 2, 1, 1, 1], [3, 3, 1, 1, 1, 1, 1], [3, 3, 2, 2, 1], [4, 4, 1, 1, 1], [5, 5, 1]], "roles": [619, 620, 333], "transition_edges": 218}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "exit_dimensions": [5, 5, 5], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11675, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [618, 619, 317], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [2], "entrance_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [427, 96, 24, 6]], "entrance_dimensions": [5, 5, 4], "exit_bases": [[296, 130, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[1], [], [1]], "incumbent_profile": [1, 1], "index": 11679, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1]], "roles": [618, 620, 257], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [424, 96, 24, 4, 2, 1]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11680, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [620, 621, 257], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [427, 96, 24, 6]], "entrance_dimensions": [5, 5, 4], "exit_bases": [[258, 168, 96, 24, 6, 1], [418, 96, 16, 8, 6, 1], [426, 96, 24, 6, 1]], "exit_dimensions": [6, 6, 5], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11682, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [619, 620, 245], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "dijkstra_truncated_cost_minima": [3], "entrance_bases": [[426, 96, 24, 6, 1], [426, 96, 24, 6, 1], [426, 96, 24, 6, 1]], "entrance_dimensions": [5, 5, 5], "exit_bases": [[418, 96, 16, 8, 6, 1], [290, 136, 96, 24, 6, 1], [386, 72, 40, 24, 6, 1]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[1], [1], [1]], "incumbent_profile": [1, 1, 1], "index": 11683, "pair_bounds_ab_ax_bx": [[5, 5], [5, 5], [5, 5]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1, 1, 1]], "roles": [620, 621, 245], "transition_edges": 12}, + {"accepting_states": 3, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[51], [51], [413, 72, 48, 3]], "entrance_dimensions": [1, 1, 4], "exit_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[3], [3], []], "incumbent_profile": [3, 3], "index": 11705, "pair_bounds_ab_ax_bx": [[1, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 24, "relaxed_profiles": [[1, 1, 1, 1, 1, 1], [2, 2, 1, 1], [3, 3]], "roles": [628, 629, 241], "transition_edges": 79}, + {"accepting_states": 3, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [3, 6, 8], "entrance_bases": [[51], [51], [413, 72, 48, 3]], "entrance_dimensions": [1, 1, 4], "exit_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [400, 65, 48, 9, 4, 3]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[3], [3], [2]], "incumbent_profile": [3, 3, 2], "index": 11706, "pair_bounds_ab_ax_bx": [[1, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 24, "relaxed_profiles": [[2, 1, 1, 1, 1, 1, 1], [2, 2, 2, 1, 1], [3, 3, 2]], "roles": [629, 630, 241], "transition_edges": 79}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11708, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [628, 629, 234], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [2, 4, 5], "entrance_bases": [[413, 72, 48, 3], [51], [413, 72, 48, 3]], "entrance_dimensions": [4, 1, 4], "exit_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [3, 4, 48, 72, 144, 265]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[], [3], [2]], "incumbent_profile": [3, 2], "index": 11709, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[3, 2]], "roles": [629, 631, 234], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[280, 129, 72, 48, 4, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "exit_dimensions": [6, 4, 4], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 11711, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [628, 630, 229], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [3, 4, 24, 40, 72, 385]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[], [], [2]], "incumbent_profile": [2], "index": 11712, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [630, 631, 229], "transition_edges": 12}, + {"accepting_states": 2, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [2, 4], "entrance_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[257, 152, 72, 48, 4, 3], [393, 72, 32, 16, 4, 3], [413, 72, 48, 3]], "exit_dimensions": [6, 6, 4], "incumbent_gaps_by_field": [[2], [2], []], "incumbent_profile": [2, 2], "index": 11714, "pair_bounds_ab_ax_bx": [[4, 5], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[1, 1, 1, 1], [2, 2]], "roles": [629, 630, 227], "transition_edges": 18}, + {"accepting_states": 5, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[413, 72, 48, 3], [413, 72, 48, 3]], "dijkstra_truncated_cost_minima": [3, 6], "entrance_bases": [[413, 72, 48, 3], [413, 72, 48, 3], [413, 72, 48, 3]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[393, 72, 32, 16, 4, 3], [3, 4, 48, 72, 137, 272], [1, 2, 4, 48, 72, 408]], "exit_dimensions": [6, 6, 6], "incumbent_gaps_by_field": [[2], [2], [2]], "incumbent_profile": [2, 2, 2], "index": 11715, "pair_bounds_ab_ax_bx": [[4, 5], [4, 5], [4, 5]], "phase": "B", "reachable_states": 13, "relaxed_profiles": [[1, 1, 1, 1, 1, 1], [2, 1, 1, 1, 1], [2, 2, 2]], "roles": [630, 631, 227], "transition_edges": 51}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[407, 66, 36, 9], [407, 66, 36, 9]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11735, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [49, 83, 225], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[407, 66, 36, 9], [407, 66, 36, 9]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[388, 65, 36, 16, 9, 3], [407, 66, 36, 9], [407, 66, 36, 9]], "exit_dimensions": [6, 4, 4], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 11739, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [49, 98, 281], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[407, 66, 36, 9], [407, 66, 36, 9]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [276, 131, 66, 36, 9]], "exit_dimensions": [4, 4, 5], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11740, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [98, 101, 281], "transition_edges": 12}, + {"accepting_states": 2, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[407, 66, 36, 9], [407, 66, 36, 9]], "dijkstra_truncated_cost_minima": [2, 4], "entrance_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[387, 66, 32, 16, 9, 4], [262, 129, 66, 36, 16, 9], [407, 66, 36, 9]], "exit_dimensions": [6, 6, 4], "incumbent_gaps_by_field": [[2], [2], []], "incumbent_profile": [2, 2], "index": 11742, "pair_bounds_ab_ax_bx": [[4, 5], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[1, 1, 1, 1], [2, 2]], "roles": [83, 98, 393], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[407, 66, 36, 9], [407, 66, 36, 9]], "dijkstra_truncated_cost_minima": [3, 4], "entrance_bases": [[407, 66, 36, 9], [407, 66, 36, 9], [407, 66, 36, 9]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[262, 129, 66, 36, 16, 9], [406, 66, 36, 8, 1], [259, 148, 66, 36, 9]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[2], [1], [1]], "incumbent_profile": [2, 1, 1], "index": 11743, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2, 1, 1]], "roles": [98, 101, 393], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[258, 130, 85, 45], [258, 130, 85, 45]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11763, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [68, 80, 377], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[258, 130, 85, 45], [258, 130, 85, 45]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[257, 129, 76, 45, 25, 3], [258, 130, 85, 45], [258, 130, 85, 45]], "exit_dimensions": [6, 4, 4], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 11767, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [68, 88, 381], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[258, 130, 85, 45], [258, 130, 85, 45]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 84, 44, 1]], "exit_dimensions": [4, 4, 5], "incumbent_gaps_by_field": [[], [], [1]], "incumbent_profile": [1], "index": 11768, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[1]], "roles": [88, 31, 381], "transition_edges": 12}, + {"accepting_states": 2, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[258, 130, 85, 45], [258, 130, 85, 45]], "dijkstra_truncated_cost_minima": [2, 4], "entrance_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[258, 130, 72, 41, 25, 4], [258, 130, 70, 39, 19, 10], [258, 130, 85, 45]], "exit_dimensions": [6, 6, 4], "incumbent_gaps_by_field": [[2], [2], []], "incumbent_profile": [2, 2], "index": 11770, "pair_bounds_ab_ax_bx": [[4, 5], [4, 4], [4, 4]], "phase": "B", "reachable_states": 6, "relaxed_profiles": [[1, 1, 1, 1], [2, 2]], "roles": [80, 88, 345], "transition_edges": 18}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[258, 130, 85, 45], [258, 130, 85, 45]], "dijkstra_truncated_cost_minima": [3, 4], "entrance_bases": [[258, 130, 85, 45], [258, 130, 85, 45], [258, 130, 85, 45]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[258, 130, 70, 39, 19, 10], [258, 130, 85, 37, 8], [258, 130, 74, 45, 31]], "exit_dimensions": [6, 5, 5], "incumbent_gaps_by_field": [[2], [1], [1]], "incumbent_profile": [2, 1, 1], "index": 11771, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2, 1, 1]], "roles": [88, 31, 345], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[455, 33, 18, 12], [455, 33, 18, 12]], "dijkstra_truncated_cost_minima": [0], "entrance_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "exit_dimensions": [4, 4, 4], "incumbent_gaps_by_field": [[], [], []], "incumbent_profile": [], "index": 11791, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[]], "roles": [33, 55, 329], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[455, 33, 18, 12], [455, 33, 18, 12]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[388, 64, 33, 17, 12, 3], [455, 33, 18, 12], [455, 33, 18, 12]], "exit_dimensions": [6, 4, 4], "incumbent_gaps_by_field": [[2], [], []], "incumbent_profile": [2], "index": 11795, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [33, 74, 297], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[455, 33, 18, 12], [455, 33, 18, 12]], "dijkstra_truncated_cost_minima": [1, 2], "entrance_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [259, 132, 64, 33, 18, 12]], "exit_dimensions": [4, 4, 6], "incumbent_gaps_by_field": [[], [], [2]], "incumbent_profile": [2], "index": 11796, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2]], "roles": [74, 85, 297], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[455, 33, 18, 12], [455, 33, 18, 12]], "dijkstra_truncated_cost_minima": [2, 3], "entrance_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[387, 64, 33, 18, 8, 4], [385, 70, 33, 18, 12], [455, 33, 18, 12]], "exit_dimensions": [6, 5, 4], "incumbent_gaps_by_field": [[2], [1], []], "incumbent_profile": [2, 1], "index": 11798, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2, 1]], "roles": [55, 74, 313], "transition_edges": 12}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[455, 33, 18, 12], [455, 33, 18, 12]], "dijkstra_truncated_cost_minima": [3, 4], "entrance_bases": [[455, 33, 18, 12], [455, 33, 18, 12], [455, 33, 18, 12]], "entrance_dimensions": [4, 4, 4], "exit_bases": [[385, 70, 33, 18, 12], [262, 193, 33, 18, 12], [260, 131, 64, 33, 18, 12]], "exit_dimensions": [5, 5, 6], "incumbent_gaps_by_field": [[1], [1], [2]], "incumbent_profile": [2, 1, 1], "index": 11799, "pair_bounds_ab_ax_bx": [[4, 4], [4, 4], [4, 4]], "phase": "B", "reachable_states": 4, "relaxed_profiles": [[2, 1, 1]], "roles": [74, 85, 313], "transition_edges": 12}, + {"accepting_states": 4, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [1, 6, 50, 82, 136, 264], [257, 129, 68, 34, 22, 8]], "entrance_dimensions": [9, 6, 6], "exit_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "exit_dimensions": [9, 9, 9], "incumbent_gaps_by_field": [[], [3], [3]], "incumbent_profile": [3, 3], "index": 12491, "pair_bounds_ab_ax_bx": [[9, 9], [9, 9], [8, 9]], "phase": "cleanup_tail", "reachable_states": 11, "relaxed_profiles": [[2, 2, 1, 1], [3, 3]], "roles": [408, 567, 105], "transition_edges": 35}, + {"accepting_states": 4, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [3, 4, 48, 72, 144, 265], [10, 20, 32, 65, 132, 259]], "entrance_dimensions": [9, 6, 6], "exit_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "exit_dimensions": [9, 9, 9], "incumbent_gaps_by_field": [[], [3], [3]], "incumbent_profile": [3, 3], "index": 12494, "pair_bounds_ab_ax_bx": [[9, 9], [9, 9], [8, 9]], "phase": "cleanup_tail", "reachable_states": 11, "relaxed_profiles": [[2, 2, 1, 1], [3, 3]], "roles": [412, 569, 414], "transition_edges": 35}, + {"accepting_states": 4, "all_concave_costs_certified": true, "coefficients": [1, -1], "contact_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [7, 27, 40, 73, 136, 264], [2, 8, 20, 32, 65, 389]], "entrance_dimensions": [9, 6, 6], "exit_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "exit_dimensions": [9, 9, 9], "incumbent_gaps_by_field": [[], [3], [3]], "incumbent_profile": [3, 3], "index": 12497, "pair_bounds_ab_ax_bx": [[9, 9], [9, 9], [8, 9]], "phase": "cleanup_tail", "reachable_states": 11, "relaxed_profiles": [[2, 2, 1, 1], [3, 3]], "roles": [424, 575, 44], "transition_edges": 35}, + {"accepting_states": 4, "all_concave_costs_certified": true, "coefficients": [-1, -1], "contact_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "dijkstra_truncated_cost_minima": [2, 4, 6], "entrance_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [1, 2, 4, 48, 72, 408], [257, 129, 73, 42, 27, 5]], "entrance_dimensions": [9, 6, 6], "exit_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "exit_dimensions": [9, 9, 9], "incumbent_gaps_by_field": [[], [3], [3]], "incumbent_profile": [3, 3], "index": 12500, "pair_bounds_ab_ax_bx": [[9, 9], [9, 9], [8, 9]], "phase": "cleanup_tail", "reachable_states": 11, "relaxed_profiles": [[2, 2, 1, 1], [3, 3]], "roles": [428, 577, 430], "transition_edges": 35}, + {"accepting_states": 1, "all_concave_costs_certified": true, "coefficients": [-1, 1], "contact_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "dijkstra_truncated_cost_minima": [1], "entrance_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 34, 16, 10, 4, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "entrance_dimensions": [9, 8, 9], "exit_bases": [[256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1], [256, 128, 64, 32, 16, 8, 4, 2, 1]], "exit_dimensions": [9, 9, 9], "incumbent_gaps_by_field": [[], [1], []], "incumbent_profile": [1], "index": 12655, "pair_bounds_ab_ax_bx": [[9, 9], [9, 9], [9, 9]], "phase": "cleanup_tail", "reachable_states": 6, "relaxed_profiles": [[1]], "roles": [40, 18, 226], "transition_edges": 18} + ] +} diff --git a/research/pr4546-extended-ceilings/PR4587-RESULT.json b/research/pr4546-extended-ceilings/PR4587-RESULT.json new file mode 100644 index 0000000000..be079e0bcf --- /dev/null +++ b/research/pr4546-extended-ceilings/PR4587-RESULT.json @@ -0,0 +1,141 @@ +{ + "status": "PASS_RECEIVER_ALL_LENGTH_CONCAVE_FLOOR", + "window_count": 128, + "state_count": 1603, + "partition_count": 239, + "boundary_sha256": "8cdc8a25f3d880fc398fe21aaf3c2c4668d9d453102ba7b6e5cae00cbdb578ae", + "word_length_cap": null, + "coefficient_cap": null, + "cost_scope": "Every increasing concave rank weight f with f(0)=0; in particular r^q for 0= 5: + # Meet in the middle: word = p + q with M(q) M(p) = T, i.e. M(p) = M(q)^-1 T. + pre = {n: defaultdict(list) for n in (2, 3)} + for n in (2, 3): + for m, w in words_of_length(n): + pre[n][m].append(w) + for n in range(5, max_len + 1): + lp, lq = (2, 3) if n == 5 else (3, 3) + for _, q in words_of_length(lq): + # M(q) = E_qk ... E_q1, so M(q)^-1 T = E_q1^-1 ... E_qk^-1 T: apply inverses from the last gate. + inv = T + for (i, j, s) in reversed(q): + inv = act(inv, (i, j, -s)) + for p in pre[lp].get(inv, ()): + found.append(p + q) + visited += 12 ** n + return tuple(found), visited + + +# ---------------------------------------------------------------- binary frames +@lru_cache(None) +def span(basis): + vals = {0} + for v in basis: + vals |= {x ^ v for x in vals} + return frozenset(vals) + + +def dim(sp): + return len(sp).bit_length() - 1 + + +@lru_cache(None) +def ssum(a, b): + basis = [] + for v in list(a) + list(b): + for bv in basis: + v = min(v, v ^ bv) + if v: + basis.append(v) + return span(tuple(sorted(basis))) + + +def relaxed(starts, ends, word): + if not all(a <= b for a, b in zip(starts, ends)): + return set() + cur, lower = list(starts), [] + for i, j, _ in word: + f = ssum(cur[i], cur[j]) + lower.append(f) + cur[i] = cur[j] = f + cur, upper = list(ends), [None] * len(word) + for k in range(len(word) - 1, -1, -1): + i, j, _ = word[k] + f = cur[i] & cur[j] + upper[k] = f + cur[i] = cur[j] = f + if not all(a <= b for a, b in zip(lower, upper)): + return set() + bounds = [(dim(a), dim(b)) for a, b in zip(lower, upper)] + s0, e0 = tuple(dim(x) for x in starts), tuple(dim(x) for x in ends) + out = set() + + def visit(k, state, hist): + if k == len(word): + h = list(hist) + for a, b in zip(state, e0): + if b > a: + h[b - a] += 1 + need(sum(r * n for r, n in enumerate(h)) == sum(e0) - sum(s0), "rank mass") + out.add(tuple(h)) + return + i, j, _ = word[k] + lo, hi = bounds[k] + for dd in range(max(lo, state[i], state[j]), min(hi, e0[i], e0[j]) + 1): + h, st = list(hist), list(state) + for r in (i, j): + if dd > st[r]: + h[dd - st[r]] += 1 + st[r] = dd + visit(k + 1, tuple(st), tuple(h)) + + visit(0, s0, (0,) * 10) + return out + + +# ---------------------------------------------------------------- certified rank prices r^(1-C) +def ln_bounds(y, terms=80): + y = Fr(y) + e = 0 + while y >= 2: + y /= 2 + e += 1 + + def core(v): + z = (v - 1) / (v + 1) + s, p = Fr(0), z + for k in range(terms): + s += 2 * p / (2 * k + 1) + p *= z * z + return s, s + 2 * p / ((2 * terms + 1) * (1 - z * z)) + + a, b = core(y) + c, d = core(Fr(2)) + return a + e * c, b + e * d + + +def prices(): + out = {1: (Fr(1), Fr(1))} + for r in range(2, 10): + lo, hi = ln_bounds(r) + xs = (C * lo, C * hi) + + def expm(x, terms=30): # exp(-x) for 0 < x < 1/100: alternating series bounds + t, s = Fr(1), Fr(1) + for n in range(1, terms): + t *= -x / n + s += t + return s - abs(t * x / terms), s + abs(t * x / terms) + + out[r] = (r * expm(xs[1])[0], r * expm(xs[0])[1]) + return out + + +PRICE = prices() + + +def gain_upper(old, new): + """Upper bound on cost(old) - cost(new) with certified prices; exact 0 for identical profiles.""" + if old == new: + return Fr(0) + tot = Fr(0) + for r in range(1, 10): + n = old[r] - new[r] + if n: + tot += n * (PRICE[r][1] if n > 0 else PRICE[r][0]) + return tot + + +# ---------------------------------------------------------------- windows from the canonical constructor +def construct(): + with tempfile.TemporaryDirectory(prefix="ext-ceiling-cache-") as cache: + code = ("import json,sys;sys.path.insert(0,sys.argv[1]);import native_joint;" + "c,p,b,o,n=native_joint.construct();print(json.dumps({'c':c,'p':p['forward']}))") + run = subprocess.run([sys.executable, "-I", "-B", "-X", "pycache_prefix=" + cache, "-c", code, + str(ROOT / "research/joint-helper-lattice")], capture_output=True, check=True, timeout=120) + data = json.loads(run.stdout) + return data["c"], data["p"] + + +def extract_windows(c, program): + word = [e for e in program if e[0] != "climb"] + frames = c["frames"] + state = list(c["start"]) + phase, out = None, [] + + def roles(e): + g = e[1] + return g[1:3] if g[0] in ("add", "copy") else g[1:2] + + for pos, e in enumerate(word): + if e[0] == "phase": + phase = e[1] + if phase in ("B", "cleanup_tail") and pos + 1 < len(word): + f = word[pos + 1] + if e[0] == f[0] == "scalar" and e[1][0] == f[1][0] == "add" and all(r[0] == "L" for r in roles(e) + roles(f)): + a, x, b, y = e[1][1][1], e[1][2][1], f[1][1][1], f[1][2][1] + ca, cb = Fr(*e[1][3:]), Fr(*f[1][3:]) + if x == y and len({a, b, x}) == 3 and ca in (-1, 1) and cb in (-1, 1): + owners = (a, b, x) + starts = [span(tuple(frames[state[r]])) for r in owners] + ends = [] + for r in owners: + t = c["final"][r] + for later in word[pos + 2:]: + if later[0] == "scalar" and ["L", r] in roles(later): + t = later[2] + break + if later[0] == "warp" and later[1] == ["L", r]: + t = later[3] + break + ends.append(span(tuple(frames[t]))) + actual = [span(tuple(frames[e[2]])), span(tuple(frames[f[2]]))] + out.append({"index": pos, "phase": phase, "roles": list(owners), "coefficients": [int(ca), int(cb)], + "starts": starts, "ends": ends, "frames": actual}) + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + state[r[1]] = e[2] + elif e[0] == "warp": + state[e[1][1]] = e[4] + return out + + +def actual_profile(starts, ends, frames): + word = ((0, 2, 0), (1, 2, 0)) + st, h = list(starts), [0] * 10 + for (i, j, _), f in zip(word, frames): + for r in (i, j): + need(st[r] <= f, "actual frame monotone") + if dim(f) > dim(st[r]): + h[dim(f) - dim(st[r])] += 1 + st[r] = f + for a, b in zip(st, ends): + need(a <= b, "actual exit monotone") + if dim(b) > dim(a): + h[dim(b) - dim(a)] += 1 + return tuple(h) + + +def extract_nonadjacent(c, program): + """Pairs a += ca x ... b += cb x (unit ca, cb) in phases B/cleanup_tail separated by >= 1 operation, none of which + touches a, b or x (so the pair can be rewritten in place). Starts are taken at the first shear, exits after the second.""" + word = [e for e in program if e[0] != "climb"] + frames = c["frames"] + + def roles(e): + g = e[1] + return g[1:3] if g[0] in ("add", "copy") else g[1:2] + + def touches(e, fields): + if e[0] == "scalar": + return any(r[0] == "L" and r[1] in fields for r in roles(e)) + return e[0] == "warp" and e[1][0] == "L" and e[1][1] in fields + + state, phase, states = list(c["start"]), None, [] + for e in word: + if e[0] == "phase": + phase = e[1] + states.append((phase, list(state))) + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + state[r[1]] = e[2] + elif e[0] == "warp": + state[e[1][1]] = e[4] + out = [] + for pos, e in enumerate(word): + ph, st = states[pos] + if ph not in ("B", "cleanup_tail") or e[0] != "scalar" or e[1][0] != "add" or not all(r[0] == "L" for r in roles(e)): + continue + a, x, ca = e[1][1][1], e[1][2][1], Fr(*e[1][3:]) + if ca not in (-1, 1): + continue + for q in range(pos + 1, len(word)): + f = word[q] + if f[0] == "phase": + break + if (f[0] == "scalar" and f[1][0] == "add" and all(r[0] == "L" for r in roles(f)) and f[1][2][1] == x + and f[1][1][1] not in (a, x) and Fr(*f[1][3:]) in (-1, 1) and q > pos + 1): + b = f[1][1][1] + if not any(touches(word[k], {a, b, x}) for k in range(pos + 1, q)): + owners = (a, b, x) + ends = [] + for r in owners: + t = c["final"][r] + for later in word[q + 1:]: + if later[0] == "scalar" and ["L", r] in roles(later): + t = later[2] + break + if later[0] == "warp" and later[1] == ["L", r]: + t = later[3] + break + ends.append(span(tuple(frames[t]))) + out.append({"index": pos, "partner": q, "coefficients": [int(ca), int(Fr(*f[1][3:]))], + "starts": [span(tuple(frames[st[r]])) for r in owners], "ends": ends, + "frames": [span(tuple(frames[e[2]])), span(tuple(frames[f[2]]))]}) + if touches(f, {a, x}): + break + return out + + +def subspaces_between(L, U, k): + """Every subspace F with L <= F <= U and dim F = k.""" + if not L <= U or not dim(L) <= k <= dim(U): + return [] + found, seen, stack = set(), {L}, [L] + while stack: + cur = stack.pop() + if dim(cur) == k: + found.add(cur) + continue + for vec in U: + if vec not in cur: + nxt = ssum(cur, span((vec,))) + if nxt not in seen: + seen.add(nxt) + stack.append(nxt) + return list(found) + + +def geometric_best_gain(starts, ends, old, word): + """Exact search over actual nested subspaces (joint incidence enforced) for one word; None if infeasible.""" + cur, upper = list(ends), [None] * len(word) + for k in range(len(word) - 1, -1, -1): + i, j, _ = word[k] + f = cur[i] & cur[j] + upper[k] = f + cur[i] = cur[j] = f + best = [None] + + def rec(k, state, hist): + if k == len(word): + h = list(hist) + for r in range(3): + if not state[r] <= ends[r]: + return + g = dim(ends[r]) - dim(state[r]) + if g: + h[g] += 1 + gain = gain_upper(old, tuple(h)) + if best[0] is None or gain > best[0]: + best[0] = gain + return + i, j, _ = word[k] + L, U = ssum(state[i], state[j]), upper[k] + for dd in range(dim(L), dim(U) + 1): + for F in subspaces_between(L, U, dd): + h, st = list(hist), list(state) + for r in (i, j): + g = dim(F) - dim(st[r]) + if g: + h[g] += 1 + st[r] = F + rec(k + 1, tuple(st), tuple(h)) + + rec(0, tuple(starts), (0,) * 10) + return best[0] + + +def single_contact_retiming(c, program): + """For every two-operand scalar contact in the whole word (all phases), compare the incumbent contact dimension with + every admissible dimension between the operands' current-frame sum and their next-contact (exit) intersection. + Any dimension in that range is realisable by a nested subspace, so this is exact for single-contact retiming.""" + word = [e for e in program if e[0] != "climb"] + frames = c["frames"] + + def roles(e): + g = e[1] + return g[1:3] if g[0] in ("add", "copy") else g[1:2] + + exit_after, cur = [None] * len(word), {} + for k in range(len(word) - 1, -1, -1): + e = word[k] + exit_after[k] = dict(cur) + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + cur[r[1]] = e[2] + elif e[0] == "warp" and e[1][0] == "L": + cur[e[1][1]] = e[3] + + def cost(h): + return sum(n * PRICE[r][1] for r, n in enumerate(h) if n and r) + + state, phase, tally = list(c["start"]), None, Counter() + for k, e in enumerate(word): + if e[0] == "phase": + phase = e[1] + if e[0] == "scalar" and len(roles(e)) == 2 and all(r[0] == "L" for r in roles(e)): + i, j = roles(e)[0][1], roles(e)[1][1] + Si, Sj = span(tuple(frames[state[i]])), span(tuple(frames[state[j]])) + Ei = span(tuple(frames[exit_after[k].get(i, c["final"][i])])) + Ej = span(tuple(frames[exit_after[k].get(j, c["final"][j])])) + F0 = span(tuple(frames[e[2]])) + L, U = ssum(Si, Sj), Ei & Ej + need(L <= F0 <= U, "incumbent contact inside its bounds") + + def prof(dd): + h = [0] * 10 + for lo_, hi_ in ((dim(Si), dd), (dd, dim(Ei)), (dim(Sj), dd), (dd, dim(Ej))): + if hi_ > lo_: + h[hi_ - lo_] += 1 + return tuple(h) + + incumbent = cost(prof(dim(F0))) + need(all(cost(prof(dd)) >= incumbent for dd in range(dim(L), dim(U) + 1)), f"single-contact optimum at {k}") + tally[phase] += 1 + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + state[r[1]] = e[2] + elif e[0] == "warp": + state[e[1][1]] = e[4] + return dict(tally) + + +def two_contact_retiming(c, program): + """Joint retiming of two consecutive contacts k1 < k2 of one field r (other operands p at k1, q at k2, p != q): + F1 >= S_r + S_p, F1 <= E_p, F1 <= F2, F2 >= F1 + S_q, F2 <= E_r & E_q. First a dimension relaxation; where it is + positive, an exact search over actual nested subspaces. Returns tallies; any exact gain fails the check.""" + word = [e for e in program if e[0] != "climb"] + frames = c["frames"] + + def roles(e): + g = e[1] + return g[1:3] if g[0] in ("add", "copy") else g[1:2] + + def fr(i): + return span(tuple(frames[i])) + + def is2(e): + return e[0] == "scalar" and len(roles(e)) == 2 and all(r[0] == "L" for r in roles(e)) + + state, before = list(c["start"]), [] + for e in word: + before.append(list(state)) + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + state[r[1]] = e[2] + elif e[0] == "warp": + state[e[1][1]] = e[4] + nexttouch, cur = [None] * len(word), {} + for k in range(len(word) - 1, -1, -1): + e = word[k] + nexttouch[k] = dict(cur) + if e[0] == "scalar": + for r in roles(e): + if r[0] == "L": + cur[r[1]] = k + elif e[0] == "warp" and e[1][0] == "L": + cur[e[1][1]] = k + + def exit_frame(field, k): + t = nexttouch[k].get(field) + if t is None: + return fr(c["final"][field]) + return fr(word[t][2]) if word[t][0] == "scalar" else fr(word[t][3]) + + def cost(h): + return sum(n * PRICE[r][1] for r, n in enumerate(h) if n and r) + + tally = Counter() + for k1, e1 in enumerate(word): + if not is2(e1): + continue + f1 = [r[1] for r in roles(e1)] + for r in f1: + k2 = nexttouch[k1].get(r) + if k2 is None or not is2(word[k2]): + continue + p = [x for x in f1 if x != r][0] + q = [x[1] for x in roles(word[k2]) if x[1] != r][0] + if q == p: + continue + Sr, Sp, Sq = fr(before[k1][r]), fr(before[k1][p]), fr(before[k2][q]) + Ep, Er, Eq = exit_frame(p, k1), exit_frame(r, k2), exit_frame(q, k2) + + def prof(d1, d2): + h = [0] * 10 + for lo_, hi_ in ((dim(Sr), d1), (d1, d2), (d2, dim(Er)), (dim(Sp), d1), (d1, dim(Ep)), (dim(Sq), d2), (d2, dim(Eq))): + if hi_ > lo_: + h[hi_ - lo_] += 1 + return tuple(h) + + base = cost(prof(dim(fr(e1[2])), dim(fr(word[k2][2])))) + L1, U2 = ssum(Sr, Sp), Er & Eq + U1 = Ep & U2 + need(L1 <= U1, "incumbent bounds consistent") + relaxed_best = min(cost(prof(d1, d2)) for d1 in range(dim(L1), dim(U1) + 1) + for d2 in range(max(d1, dim(ssum(L1, Sq))), dim(U2) + 1)) + if relaxed_best >= base: + tally["zero_by_relaxation"] += 1 + continue + exact = None + for d1 in range(dim(L1), dim(U1) + 1): + for F1 in subspaces_between(L1, U1, d1): + L2 = ssum(F1, Sq) + for d2 in range(dim(L2), dim(U2) + 1): + if subspaces_between(L2, U2, d2): + cc = cost(prof(d1, d2)) + exact = cc if exact is None or cc < exact else exact + need(exact is None or exact >= base, f"two-contact retiming gain at {k1},{k2}") + tally["zero_by_exact_geometry"] += 1 + return dict(tally) + + +def geometric_profiles(starts, ends, word): + """Every exactly realisable profile of one word (actual nested subspaces, joint incidence enforced).""" + cur, upper = list(ends), [None] * len(word) + for k in range(len(word) - 1, -1, -1): + i, j, _ = word[k] + f = cur[i] & cur[j] + upper[k] = f + cur[i] = cur[j] = f + out = set() + + def rec(k, state, hist): + if k == len(word): + h = list(hist) + for r in range(3): + if not state[r] <= ends[r]: + return + g = dim(ends[r]) - dim(state[r]) + if g: + h[g] += 1 + out.add(tuple(h)) + return + i, j, _ = word[k] + L, U = ssum(state[i], state[j]), upper[k] + for dd in range(dim(L), dim(U) + 1): + for F in subspaces_between(L, U, dd): + h, st = list(hist), list(state) + for r in (i, j): + g = dim(F) - dim(st[r]) + if g: + h[g] += 1 + st[r] = F + rec(k + 1, tuple(st), tuple(h)) + + rec(0, tuple(starts), (0,) * 10) + return out + + +def matches_alphabet(ca, cb, coefs, max_len): + """All words of length <= max_len over shears y_i += c y_j (c in coefs) with the window endpoint (meet in middle).""" + gates = tuple((i, j, c) for i in range(3) for j in range(3) if i != j for c in coefs) + + def layer(n): + out = [(IDENTITY, ())] + for _ in range(n): + out = [(act(m, g), w + (g,)) for m, w in out for g in gates] + return out + + half = max_len // 2 + pre = defaultdict(list) + for n in range(half + 1): + for m, w in layer(n): + pre[n, m].append(w) + T, found = target(ca, cb), [] + for total in range(max_len + 1): + lp = min(half, total) + lq = total - lp + for _, q in layer(lq): + inv = T + for (i, j, c) in reversed(q): + inv = act(inv, (i, j, -c)) + found += [p + q for p in pre.get((lp, inv), ())] + return found + + +def main(): + raw = RESULT.read_bytes() + need(hashlib.sha256(raw).hexdigest() == RESULT_SHA256, "vendored #4546 RESULT.json") + ref = {w["index"]: w for w in json.loads(raw)["windows"]} + c, program = construct() + wins = extract_windows(c, program) + need(len(wins) == 128, "#4546's 128 eligible windows") + every = wins + wins = wins[:12] + rows = [] + for w in wins: + r = ref[w["index"]] + need(w["roles"] == r["roles"] and w["coefficients"] == r["coefficients"] and w["phase"] == r["phase"], "window identity") + need([dim(x) for x in w["starts"]] == r["start_dimensions"] and [dim(x) for x in w["ends"]] == r["exit_dimensions"], + "window dimensions") + old = actual_profile(w["starts"], w["ends"], w["frames"]) + need({str(k): v for k, v in enumerate(old) if v} == r["old_paid"], "old paid profile") + row = {"index": w["index"], "old_paid": {str(k): v for k, v in enumerate(old) if v}} + for L in (4, 5, 6): + ms, visited = matches(*w["coefficients"], L) + profiles = set() + compatible = 0 + for word in ms: + ps = relaxed(w["starts"], w["ends"], word) + if ps: + compatible += 1 + profiles |= ps + best = max(gain_upper(old, p) for p in profiles) + if L == 4: + need(visited == 22621 and len(ms) == 84 == r["compatible_words"] == compatible, "length-4 census") + need(len(profiles) == r["relaxed_profiles"], "length-4 relaxed profile count") + need(best == 0, "length-4 zero ceiling") + row[f"len<={L}"] = {"matching_words": len(ms), "compatible": compatible, "relaxed_profiles": len(profiles), + "best_gain_upper": str(best), "positive": best > 0} + rows.append(row) + summary = {L: sum(1 for r in rows if r[f"len<={L}"]["positive"]) for L in (4, 5, 6)} + # All 128 eligible windows (#4546 tested only the first twelve): lengths <= 4 and <= 6. + phases = Counter(w["phase"] for w in every) + profile_counts = Counter() + for w in every: + old = actual_profile(w["starts"], w["ends"], w["frames"]) + for L in (4, 6): + ms, _ = matches(*w["coefficients"], L) + profiles = set() + for word in ms: + profiles |= relaxed(w["starts"], w["ends"], word) + need(profiles and max(gain_upper(old, p) for p in profiles) == 0, f"zero ceiling, window {w['index']}, len<={L}") + if L == 6: + profile_counts[len(profiles)] += 1 + # Cross-check with #4581's all-length certificate: its terminal partitions per window against this file's + # finite (length <= 6) relaxed profile sets, and an independent recheck of its capped-rank majorization. + raw81 = PR4581.read_bytes() + need(hashlib.sha256(raw81).hexdigest() == PR4581_SHA256, "vendored #4581 RESULT.json") + allen = {w["index"]: w for w in json.loads(raw81)["windows"]} + need(len(allen) == len(every) == 128, "same 128 windows") + + def partition(h): + return sorted((r for r, n in enumerate(h) for _ in range(n)), reverse=True) + + def capped(part, k): + return sum(min(r, k) for r in part) + + agree = 0 + for w in every: + a = allen[w["index"]] + old = actual_profile(w["starts"], w["ends"], w["frames"]) + need(sorted(a["incumbent"], reverse=True) == partition(old), "same incumbent") + ms, _ = matches(*w["coefficients"], 6) + mine = set() + for word in ms: + mine |= relaxed(w["starts"], w["ends"], word) + mine_parts = sorted(tuple(partition(h)) for h in mine) + theirs = sorted(tuple(sorted(p, reverse=True)) for p in a["terminal_profiles"]) + need(mine_parts == theirs, f"finite length-6 set equals #4581's all-length set, window {w['index']}") + u = partition(old) + for v_ in theirs: + need(sum(u) == sum(v_) and all(capped(u, k) <= capped(v_, k) for k in range(1, 10)), "majorization") + agree += 1 + others = {} + for prn, (path, digest, key) in OTHER_CERTS.items(): + raw_o = path.read_bytes() + need(hashlib.sha256(raw_o).hexdigest() == digest, f"vendored #{prn} RESULT.json") + table = {w["index"]: sorted(tuple(sorted(p, reverse=True)) for p in w[key]) for w in json.loads(raw_o)["windows"]} + need(len(table) == 128, f"#{prn}: 128 windows") + others[prn] = table + for w in every: + ms, _ = matches(*w["coefficients"], 6) + mine = set() + for word in ms: + mine |= relaxed(w["starts"], w["ends"], word) + mine_parts = sorted(tuple(partition(h)) for h in mine) + for prn, table in others.items(): + need(table[w["index"]] == mine_parts, f"#{prn} agrees in window {w['index']}") + # Telescoping: f(r) = delta_9 r + sum_{k<9} (delta_k - delta_{k+1}) min(r, k) for any f with f(0) = 0 (exact check). + for trial in range(200): + fvals = [Fr(0)] + [Fr(((trial * 7919 + r * 104729) % 997) + 1, 13) for r in range(1, 10)] + delta = [None] + [fvals[k] - fvals[k - 1] for k in range(1, 10)] + for r in range(0, 10): + need(fvals[r] == delta[9] * r + sum((delta[k] - delta[k + 1]) * min(r, k) for k in range(1, 9)), "telescoping") + # Nonunit coefficients: optimistic in the rewrite's favour (their scalar-height cost is not charged). + nonunit = {} + for coefs, L in (((-2, -1, 1, 2), 6), ((-3, -2, -1, 1, 2, 3), 5)): + cache = {} + for w in every: + key = tuple(w["coefficients"]) + if key not in cache: + cache[key] = matches_alphabet(key[0], key[1], coefs, L) + old = actual_profile(w["starts"], w["ends"], w["frames"]) + profiles = set() + for word in cache[key]: + profiles |= relaxed(w["starts"], w["ends"], word) + need(profiles and max(gain_upper(old, p) for p in profiles) == 0, f"zero ceiling with coefficients {coefs}") + nonunit[f"coefficients {sorted(set(abs(c) for c in coefs))}, len<={L}"] = { + "matching_words_per_sign_case": len(next(iter(cache.values()))), "windows_zero": len(every)} + # Nonadjacent pairs (a model change #4546 suggests): relaxation first; exact joint geometry where it is positive. + nonadj = extract_nonadjacent(c, program) + na = Counter() + for w in nonadj: + old = actual_profile(w["starts"], w["ends"], w["frames"]) + ms, _ = matches(*w["coefficients"], 6) + positive_words = [] + for word in ms: + ps = relaxed(w["starts"], w["ends"], word) + if ps and max(gain_upper(old, p) for p in ps) > 0: + positive_words.append(word) + if not positive_words: + na["zero_by_relaxation"] += 1 + continue + for word in positive_words: + g = geometric_best_gain(w["starts"], w["ends"], old, word) + need(g is None or g <= 0, f"exact geometry: no gain, window {w['index']}") + na["zero_by_exact_geometry"] += 1 + na["exact_geometry_words_checked"] += len(positive_words) + need(len(nonadj) == 88 and na["zero_by_relaxation"] + na["zero_by_exact_geometry"] == 88, "88 nonadjacent pairs") + # #4543's receiver-sharing word a += s b; b += cb x; a -= s b with s = -ca cb, on all 128 windows. The relaxation + # contains every actual monotone path, so "infeasible" here means the rewrite cannot meet the frame contract at all. + rs = Counter() + for w in every: + ca, cb = w["coefficients"] + sgn = -ca * cb + word = ((0, 1, sgn), (1, 2, cb), (0, 1, -sgn)) + m = IDENTITY + for g in word: + m = act(m, g) + need(m == target(ca, cb), "receiver-sharing endpoint identity with s = -ca*cb") + old = actual_profile(w["starts"], w["ends"], w["frames"]) + profiles = relaxed(w["starts"], w["ends"], word) + if not profiles: + # The certain obstruction: the first gate a += s b needs a common frame containing b's entrance frame + # inside a's exit frame. + need(not (w["starts"][1] <= w["ends"][0]), "infeasibility explained by S_b not inside E_a") + rs["infeasible", w["phase"]] += 1 + continue + need(max(gain_upper(old, p) for p in profiles) == 0, "receiver sharing never improves") + rs["incumbent_admitted" if old in profiles else "incumbent_excluded", w["phase"]] += 1 + exact = geometric_profiles(w["starts"], w["ends"], word) + need(old in exact and max(gain_upper(old, p) for p in exact) == 0, + f"receiver sharing exactly realises the incumbent, window {w['index']}") + rs["incumbent_exactly_realised"] += 1 + print(json.dumps({"status": "PASS_PR4546_EXTENDED_CEILINGS", "windows": rows, + "nonunit_coefficients_all_windows": nonunit, + "agreement_with_4581_4582_4587_all_length": {"windows_with_identical_profile_sets": agree, + "also_identical": sorted(others), + "majorization_rechecked": True}, + "single_contact_retiming_all_phases": single_contact_retiming(c, program), + "two_contact_retiming_all_phases": two_contact_retiming(c, program), + "nonadjacent_pairs_len<=6": {"count": len(nonadj), **dict(na)}, + "receiver_sharing_4543_all_windows": {(f"{k[0]}:{k[1]}" if isinstance(k, tuple) else k): v + for k, v in sorted(rs.items(), key=str)}, + "windows_with_positive_optimistic_gain": summary, + "all_eligible_windows": {"count": len(every), "phases": dict(phases), + "zero_ceiling_len<=4": len(every), "zero_ceiling_len<=6": len(every), + "relaxed_profile_count_histogram_len<=6": dict(sorted(profile_counts.items()))}, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())