//
// This file has been generated with Kappa
//
// -- state encoding: explicit
// -- compaction : none
// -- further compaction: no

nondeterministic

module impl4000 

s : [0..2598] init 0;
[] (s = 0) -> 0.500000:(s' = 1) + 0.500000:(s' = 2);
[] (s = 0) -> 0.500000:(s' = 3) + 0.500000:(s' = 4);
[] (s = 1) -> 0.500000:(s' = 5) + 0.500000:(s' = 6);
[] (s = 1) -> 1.000000:(s' = 7) ;
[] (s = 2) -> 0.500000:(s' = 8) + 0.500000:(s' = 9);
[] (s = 2) -> 1.000000:(s' = 10) ;
[] (s = 3) -> 1.000000:(s' = 11) ;
[] (s = 3) -> 0.500000:(s' = 5) + 0.500000:(s' = 8);
[] (s = 4) -> 1.000000:(s' = 12) ;
[] (s = 4) -> 0.500000:(s' = 6) + 0.500000:(s' = 9);
[] (s = 5) -> 1.000000:(s' = 13) ;
[] (s = 5) -> 1.000000:(s' = 14) ;
[] (s = 6) -> 1.000000:(s' = 15) ;
[] (s = 6) -> 1.000000:(s' = 16) ;
[] (s = 7) -> 0.500000:(s' = 14) + 0.500000:(s' = 16);
[] (s = 8) -> 1.000000:(s' = 17) ;
[] (s = 8) -> 1.000000:(s' = 18) ;
[] (s = 9) -> 1.000000:(s' = 19) ;
[] (s = 9) -> 1.000000:(s' = 20) ;
[] (s = 10) -> 0.500000:(s' = 18) + 0.500000:(s' = 20);
[] (s = 11) -> 0.500000:(s' = 13) + 0.500000:(s' = 17);
[] (s = 12) -> 0.500000:(s' = 15) + 0.500000:(s' = 19);
[] (s = 13) -> 1.000000:(s' = 21) ;
[] (s = 14) -> 1.000000:(s' = 21) ;
[] (s = 15) -> 1.000000:(s' = 22) ;
[] (s = 16) -> 1.000000:(s' = 22) ;
[] (s = 17) -> 1.000000:(s' = 23) ;
[] (s = 18) -> 1.000000:(s' = 23) ;
[] (s = 19) -> 1.000000:(s' = 24) ;
[] (s = 20) -> 1.000000:(s' = 24) ;
[] (s = 21) -> 1.000000:(s' = 25) ;
[] (s = 21) -> 1.000000:(s' = 26) ;
[] (s = 22) -> 1.000000:(s' = 27) ;
[] (s = 23) -> 1.000000:(s' = 28) ;
[] (s = 24) -> 1.000000:(s' = 29) ;
[] (s = 24) -> 1.000000:(s' = 30) ;
[] (s = 25) -> 1.000000:(s' = 31) ;
[] (s = 25) -> 1.000000:(s' = 32) ;
[] (s = 26) -> 1.000000:(s' = 33) ;
[] (s = 26) -> 1.000000:(s' = 34) ;
[] (s = 27) -> 1.000000:(s' = 35) ;
[] (s = 28) -> 1.000000:(s' = 36) ;
[] (s = 29) -> 1.000000:(s' = 37) ;
[] (s = 29) -> 1.000000:(s' = 38) ;
[] (s = 30) -> 1.000000:(s' = 39) ;
[] (s = 30) -> 1.000000:(s' = 40) ;
[] (s = 31) -> 1.000000:(s' = 41) ;
[] (s = 31) -> 1.000000:(s' = 42) ;
[] (s = 32) -> 1.000000:(s' = 43) ;
[] (s = 33) -> 1.000000:(s' = 44) ;
[] (s = 33) -> 1.000000:(s' = 45) ;
[] (s = 34) -> 1.000000:(s' = 46) ;
[] (s = 35) -> 1.000000:(s' = 47) ;
[] (s = 36) -> 1.000000:(s' = 48) ;
[] (s = 37) -> 1.000000:(s' = 49) ;
[] (s = 37) -> 1.000000:(s' = 50) ;
[] (s = 38) -> 1.000000:(s' = 51) ;
[] (s = 39) -> 1.000000:(s' = 52) ;
[] (s = 39) -> 1.000000:(s' = 53) ;
[] (s = 40) -> 1.000000:(s' = 54) ;
[] (s = 41) -> 0.500000:(s' = 55) + 0.500000:(s' = 56);
[] (s = 41) -> 1.000000:(s' = 57) ;
[] (s = 42) -> 1.000000:(s' = 57) ;
[] (s = 42) -> 0.500000:(s' = 58) + 0.500000:(s' = 59);
[] (s = 43) -> 1.000000:(s' = 60) ;
[] (s = 44) -> 0.500000:(s' = 61) + 0.500000:(s' = 62);
[] (s = 44) -> 1.000000:(s' = 63) ;
[] (s = 45) -> 1.000000:(s' = 63) ;
[] (s = 45) -> 0.500000:(s' = 64) + 0.500000:(s' = 65);
[] (s = 46) -> 1.000000:(s' = 60) ;
[] (s = 47) -> 1.000000:(s' = 60) ;
[] (s = 48) -> 1.000000:(s' = 60) ;
[] (s = 49) -> 0.500000:(s' = 66) + 0.500000:(s' = 67);
[] (s = 49) -> 1.000000:(s' = 68) ;
[] (s = 50) -> 1.000000:(s' = 68) ;
[] (s = 50) -> 0.500000:(s' = 69) + 0.500000:(s' = 70);
[] (s = 51) -> 1.000000:(s' = 60) ;
[] (s = 52) -> 0.500000:(s' = 71) + 0.500000:(s' = 72);
[] (s = 52) -> 1.000000:(s' = 73) ;
[] (s = 53) -> 1.000000:(s' = 73) ;
[] (s = 53) -> 0.500000:(s' = 74) + 0.500000:(s' = 75);
[] (s = 54) -> 1.000000:(s' = 60) ;
[] (s = 55) -> 1.000000:(s' = 76) ;
[] (s = 56) -> 1.000000:(s' = 77) ;
[] (s = 57) -> 0.500000:(s' = 78) + 0.500000:(s' = 79);
[] (s = 57) -> 0.500000:(s' = 80) + 0.500000:(s' = 81);
[] (s = 58) -> 1.000000:(s' = 82) ;
[] (s = 59) -> 1.000000:(s' = 83) ;
[] (s = 61) -> 1.000000:(s' = 84) ;
[] (s = 62) -> 1.000000:(s' = 85) ;
[] (s = 63) -> 0.500000:(s' = 78) + 0.500000:(s' = 79);
[] (s = 63) -> 0.500000:(s' = 80) + 0.500000:(s' = 81);
[] (s = 64) -> 1.000000:(s' = 86) ;
[] (s = 65) -> 1.000000:(s' = 87) ;
[] (s = 66) -> 1.000000:(s' = 88) ;
[] (s = 67) -> 1.000000:(s' = 89) ;
[] (s = 68) -> 0.500000:(s' = 90) + 0.500000:(s' = 91);
[] (s = 68) -> 0.500000:(s' = 92) + 0.500000:(s' = 93);
[] (s = 69) -> 1.000000:(s' = 94) ;
[] (s = 70) -> 1.000000:(s' = 95) ;
[] (s = 71) -> 1.000000:(s' = 96) ;
[] (s = 72) -> 1.000000:(s' = 97) ;
[] (s = 73) -> 0.500000:(s' = 90) + 0.500000:(s' = 91);
[] (s = 73) -> 0.500000:(s' = 92) + 0.500000:(s' = 93);
[] (s = 74) -> 1.000000:(s' = 98) ;
[] (s = 75) -> 1.000000:(s' = 99) ;
[] (s = 76) -> 0.500000:(s' = 100) + 0.500000:(s' = 101);
[] (s = 76) -> 1.000000:(s' = 102) ;
[] (s = 77) -> 0.500000:(s' = 103) + 0.500000:(s' = 104);
[] (s = 77) -> 1.000000:(s' = 105) ;
[] (s = 78) -> 0.500000:(s' = 106) + 0.500000:(s' = 107);
[] (s = 78) -> 1.000000:(s' = 108) ;
[] (s = 79) -> 0.500000:(s' = 109) + 0.500000:(s' = 110);
[] (s = 79) -> 1.000000:(s' = 111) ;
[] (s = 80) -> 1.000000:(s' = 112) ;
[] (s = 80) -> 0.500000:(s' = 106) + 0.500000:(s' = 109);
[] (s = 81) -> 1.000000:(s' = 113) ;
[] (s = 81) -> 0.500000:(s' = 107) + 0.500000:(s' = 110);
[] (s = 82) -> 1.000000:(s' = 114) ;
[] (s = 82) -> 0.500000:(s' = 115) + 0.500000:(s' = 116);
[] (s = 83) -> 1.000000:(s' = 117) ;
[] (s = 83) -> 0.500000:(s' = 118) + 0.500000:(s' = 119);
[] (s = 84) -> 0.500000:(s' = 100) + 0.500000:(s' = 101);
[] (s = 84) -> 1.000000:(s' = 120) ;
[] (s = 85) -> 0.500000:(s' = 103) + 0.500000:(s' = 104);
[] (s = 85) -> 1.000000:(s' = 121) ;
[] (s = 86) -> 1.000000:(s' = 122) ;
[] (s = 86) -> 0.500000:(s' = 115) + 0.500000:(s' = 116);
[] (s = 87) -> 1.000000:(s' = 123) ;
[] (s = 87) -> 0.500000:(s' = 118) + 0.500000:(s' = 119);
[] (s = 88) -> 0.500000:(s' = 124) + 0.500000:(s' = 125);
[] (s = 88) -> 1.000000:(s' = 126) ;
[] (s = 89) -> 0.500000:(s' = 127) + 0.500000:(s' = 128);
[] (s = 89) -> 1.000000:(s' = 129) ;
[] (s = 90) -> 0.500000:(s' = 130) + 0.500000:(s' = 131);
[] (s = 90) -> 1.000000:(s' = 132) ;
[] (s = 91) -> 0.500000:(s' = 133) + 0.500000:(s' = 134);
[] (s = 91) -> 1.000000:(s' = 135) ;
[] (s = 92) -> 1.000000:(s' = 136) ;
[] (s = 92) -> 0.500000:(s' = 130) + 0.500000:(s' = 133);
[] (s = 93) -> 1.000000:(s' = 137) ;
[] (s = 93) -> 0.500000:(s' = 131) + 0.500000:(s' = 134);
[] (s = 94) -> 1.000000:(s' = 138) ;
[] (s = 94) -> 0.500000:(s' = 139) + 0.500000:(s' = 140);
[] (s = 95) -> 1.000000:(s' = 141) ;
[] (s = 95) -> 0.500000:(s' = 142) + 0.500000:(s' = 143);
[] (s = 96) -> 0.500000:(s' = 124) + 0.500000:(s' = 125);
[] (s = 96) -> 1.000000:(s' = 144) ;
[] (s = 97) -> 0.500000:(s' = 127) + 0.500000:(s' = 128);
[] (s = 97) -> 1.000000:(s' = 145) ;
[] (s = 98) -> 1.000000:(s' = 146) ;
[] (s = 98) -> 0.500000:(s' = 139) + 0.500000:(s' = 140);
[] (s = 99) -> 1.000000:(s' = 147) ;
[] (s = 99) -> 0.500000:(s' = 142) + 0.500000:(s' = 143);
[] (s = 100) -> 1.000000:(s' = 148) ;
[] (s = 100) -> 1.000000:(s' = 149) ;
[] (s = 101) -> 1.000000:(s' = 150) ;
[] (s = 101) -> 1.000000:(s' = 151) ;
[] (s = 102) -> 0.500000:(s' = 149) + 0.500000:(s' = 151);
[] (s = 103) -> 1.000000:(s' = 152) ;
[] (s = 103) -> 1.000000:(s' = 153) ;
[] (s = 104) -> 1.000000:(s' = 154) ;
[] (s = 104) -> 1.000000:(s' = 155) ;
[] (s = 105) -> 0.500000:(s' = 153) + 0.500000:(s' = 155);
[] (s = 106) -> 1.000000:(s' = 156) ;
[] (s = 106) -> 1.000000:(s' = 157) ;
[] (s = 107) -> 1.000000:(s' = 158) ;
[] (s = 107) -> 1.000000:(s' = 159) ;
[] (s = 108) -> 0.500000:(s' = 157) + 0.500000:(s' = 159);
[] (s = 109) -> 1.000000:(s' = 160) ;
[] (s = 109) -> 1.000000:(s' = 161) ;
[] (s = 110) -> 1.000000:(s' = 162) ;
[] (s = 110) -> 1.000000:(s' = 163) ;
[] (s = 111) -> 0.500000:(s' = 161) + 0.500000:(s' = 163);
[] (s = 112) -> 0.500000:(s' = 156) + 0.500000:(s' = 160);
[] (s = 113) -> 0.500000:(s' = 158) + 0.500000:(s' = 162);
[] (s = 114) -> 0.500000:(s' = 164) + 0.500000:(s' = 165);
[] (s = 115) -> 1.000000:(s' = 164) ;
[] (s = 115) -> 1.000000:(s' = 166) ;
[] (s = 116) -> 1.000000:(s' = 165) ;
[] (s = 116) -> 1.000000:(s' = 167) ;
[] (s = 117) -> 0.500000:(s' = 168) + 0.500000:(s' = 169);
[] (s = 118) -> 1.000000:(s' = 168) ;
[] (s = 118) -> 1.000000:(s' = 170) ;
[] (s = 119) -> 1.000000:(s' = 169) ;
[] (s = 119) -> 1.000000:(s' = 171) ;
[] (s = 120) -> 0.500000:(s' = 149) + 0.500000:(s' = 151);
[] (s = 121) -> 0.500000:(s' = 153) + 0.500000:(s' = 155);
[] (s = 122) -> 0.500000:(s' = 164) + 0.500000:(s' = 165);
[] (s = 123) -> 0.500000:(s' = 168) + 0.500000:(s' = 169);
[] (s = 124) -> 1.000000:(s' = 172) ;
[] (s = 124) -> 1.000000:(s' = 173) ;
[] (s = 125) -> 1.000000:(s' = 174) ;
[] (s = 125) -> 1.000000:(s' = 175) ;
[] (s = 126) -> 0.500000:(s' = 173) + 0.500000:(s' = 175);
[] (s = 127) -> 1.000000:(s' = 176) ;
[] (s = 127) -> 1.000000:(s' = 177) ;
[] (s = 128) -> 1.000000:(s' = 178) ;
[] (s = 128) -> 1.000000:(s' = 179) ;
[] (s = 129) -> 0.500000:(s' = 177) + 0.500000:(s' = 179);
[] (s = 130) -> 1.000000:(s' = 180) ;
[] (s = 130) -> 1.000000:(s' = 181) ;
[] (s = 131) -> 1.000000:(s' = 182) ;
[] (s = 131) -> 1.000000:(s' = 183) ;
[] (s = 132) -> 0.500000:(s' = 181) + 0.500000:(s' = 183);
[] (s = 133) -> 1.000000:(s' = 184) ;
[] (s = 133) -> 1.000000:(s' = 185) ;
[] (s = 134) -> 1.000000:(s' = 186) ;
[] (s = 134) -> 1.000000:(s' = 187) ;
[] (s = 135) -> 0.500000:(s' = 185) + 0.500000:(s' = 187);
[] (s = 136) -> 0.500000:(s' = 180) + 0.500000:(s' = 184);
[] (s = 137) -> 0.500000:(s' = 182) + 0.500000:(s' = 186);
[] (s = 138) -> 0.500000:(s' = 188) + 0.500000:(s' = 189);
[] (s = 139) -> 1.000000:(s' = 188) ;
[] (s = 139) -> 1.000000:(s' = 190) ;
[] (s = 140) -> 1.000000:(s' = 189) ;
[] (s = 140) -> 1.000000:(s' = 191) ;
[] (s = 141) -> 0.500000:(s' = 192) + 0.500000:(s' = 193);
[] (s = 142) -> 1.000000:(s' = 192) ;
[] (s = 142) -> 1.000000:(s' = 194) ;
[] (s = 143) -> 1.000000:(s' = 193) ;
[] (s = 143) -> 1.000000:(s' = 195) ;
[] (s = 144) -> 0.500000:(s' = 173) + 0.500000:(s' = 175);
[] (s = 145) -> 0.500000:(s' = 177) + 0.500000:(s' = 179);
[] (s = 146) -> 0.500000:(s' = 188) + 0.500000:(s' = 189);
[] (s = 147) -> 0.500000:(s' = 192) + 0.500000:(s' = 193);
[] (s = 148) -> 1.000000:(s' = 196) ;
[] (s = 149) -> 1.000000:(s' = 196) ;
[] (s = 150) -> 1.000000:(s' = 197) ;
[] (s = 151) -> 1.000000:(s' = 197) ;
[] (s = 152) -> 1.000000:(s' = 198) ;
[] (s = 153) -> 1.000000:(s' = 198) ;
[] (s = 154) -> 1.000000:(s' = 199) ;
[] (s = 155) -> 1.000000:(s' = 199) ;
[] (s = 156) -> 1.000000:(s' = 200) ;
[] (s = 157) -> 1.000000:(s' = 200) ;
[] (s = 158) -> 1.000000:(s' = 201) ;
[] (s = 159) -> 1.000000:(s' = 201) ;
[] (s = 160) -> 1.000000:(s' = 202) ;
[] (s = 161) -> 1.000000:(s' = 202) ;
[] (s = 162) -> 1.000000:(s' = 203) ;
[] (s = 163) -> 1.000000:(s' = 203) ;
[] (s = 164) -> 1.000000:(s' = 204) ;
[] (s = 165) -> 1.000000:(s' = 205) ;
[] (s = 166) -> 1.000000:(s' = 204) ;
[] (s = 167) -> 1.000000:(s' = 205) ;
[] (s = 168) -> 1.000000:(s' = 206) ;
[] (s = 169) -> 1.000000:(s' = 207) ;
[] (s = 170) -> 1.000000:(s' = 206) ;
[] (s = 171) -> 1.000000:(s' = 207) ;
[] (s = 172) -> 1.000000:(s' = 208) ;
[] (s = 173) -> 1.000000:(s' = 208) ;
[] (s = 174) -> 1.000000:(s' = 209) ;
[] (s = 175) -> 1.000000:(s' = 209) ;
[] (s = 176) -> 1.000000:(s' = 210) ;
[] (s = 177) -> 1.000000:(s' = 210) ;
[] (s = 178) -> 1.000000:(s' = 211) ;
[] (s = 179) -> 1.000000:(s' = 211) ;
[] (s = 180) -> 1.000000:(s' = 212) ;
[] (s = 181) -> 1.000000:(s' = 212) ;
[] (s = 182) -> 1.000000:(s' = 213) ;
[] (s = 183) -> 1.000000:(s' = 213) ;
[] (s = 184) -> 1.000000:(s' = 214) ;
[] (s = 185) -> 1.000000:(s' = 214) ;
[] (s = 186) -> 1.000000:(s' = 215) ;
[] (s = 187) -> 1.000000:(s' = 215) ;
[] (s = 188) -> 1.000000:(s' = 216) ;
[] (s = 189) -> 1.000000:(s' = 217) ;
[] (s = 190) -> 1.000000:(s' = 216) ;
[] (s = 191) -> 1.000000:(s' = 217) ;
[] (s = 192) -> 1.000000:(s' = 218) ;
[] (s = 193) -> 1.000000:(s' = 219) ;
[] (s = 194) -> 1.000000:(s' = 218) ;
[] (s = 195) -> 1.000000:(s' = 219) ;
[] (s = 196) -> 1.000000:(s' = 220) ;
[] (s = 196) -> 1.000000:(s' = 221) ;
[] (s = 197) -> 1.000000:(s' = 222) ;
[] (s = 198) -> 1.000000:(s' = 223) ;
[] (s = 199) -> 1.000000:(s' = 224) ;
[] (s = 199) -> 1.000000:(s' = 225) ;
[] (s = 200) -> 1.000000:(s' = 226) ;
[] (s = 200) -> 1.000000:(s' = 227) ;
[] (s = 201) -> 1.000000:(s' = 228) ;
[] (s = 202) -> 1.000000:(s' = 229) ;
[] (s = 203) -> 1.000000:(s' = 230) ;
[] (s = 203) -> 1.000000:(s' = 231) ;
[] (s = 204) -> 1.000000:(s' = 232) ;
[] (s = 204) -> 1.000000:(s' = 233) ;
[] (s = 205) -> 1.000000:(s' = 234) ;
[] (s = 206) -> 1.000000:(s' = 235) ;
[] (s = 207) -> 1.000000:(s' = 236) ;
[] (s = 207) -> 1.000000:(s' = 237) ;
[] (s = 208) -> 1.000000:(s' = 238) ;
[] (s = 208) -> 1.000000:(s' = 239) ;
[] (s = 209) -> 1.000000:(s' = 240) ;
[] (s = 210) -> 1.000000:(s' = 241) ;
[] (s = 211) -> 1.000000:(s' = 242) ;
[] (s = 211) -> 1.000000:(s' = 243) ;
[] (s = 212) -> 1.000000:(s' = 244) ;
[] (s = 212) -> 1.000000:(s' = 245) ;
[] (s = 213) -> 1.000000:(s' = 246) ;
[] (s = 214) -> 1.000000:(s' = 247) ;
[] (s = 215) -> 1.000000:(s' = 248) ;
[] (s = 215) -> 1.000000:(s' = 249) ;
[] (s = 216) -> 1.000000:(s' = 250) ;
[] (s = 216) -> 1.000000:(s' = 251) ;
[] (s = 217) -> 1.000000:(s' = 252) ;
[] (s = 218) -> 1.000000:(s' = 253) ;
[] (s = 219) -> 1.000000:(s' = 254) ;
[] (s = 219) -> 1.000000:(s' = 255) ;
[] (s = 220) -> 1.000000:(s' = 256) ;
[] (s = 220) -> 1.000000:(s' = 257) ;
[] (s = 221) -> 1.000000:(s' = 258) ;
[] (s = 221) -> 1.000000:(s' = 259) ;
[] (s = 222) -> 1.000000:(s' = 260) ;
[] (s = 223) -> 1.000000:(s' = 261) ;
[] (s = 224) -> 1.000000:(s' = 262) ;
[] (s = 224) -> 1.000000:(s' = 263) ;
[] (s = 225) -> 1.000000:(s' = 264) ;
[] (s = 225) -> 1.000000:(s' = 265) ;
[] (s = 226) -> 1.000000:(s' = 266) ;
[] (s = 226) -> 1.000000:(s' = 267) ;
[] (s = 227) -> 1.000000:(s' = 268) ;
[] (s = 227) -> 1.000000:(s' = 269) ;
[] (s = 228) -> 1.000000:(s' = 270) ;
[] (s = 229) -> 1.000000:(s' = 271) ;
[] (s = 230) -> 1.000000:(s' = 272) ;
[] (s = 230) -> 1.000000:(s' = 273) ;
[] (s = 231) -> 1.000000:(s' = 274) ;
[] (s = 231) -> 1.000000:(s' = 275) ;
[] (s = 232) -> 1.000000:(s' = 276) ;
[] (s = 232) -> 1.000000:(s' = 277) ;
[] (s = 233) -> 1.000000:(s' = 278) ;
[] (s = 233) -> 1.000000:(s' = 279) ;
[] (s = 234) -> 1.000000:(s' = 280) ;
[] (s = 235) -> 1.000000:(s' = 281) ;
[] (s = 236) -> 1.000000:(s' = 282) ;
[] (s = 236) -> 1.000000:(s' = 283) ;
[] (s = 237) -> 1.000000:(s' = 284) ;
[] (s = 237) -> 1.000000:(s' = 285) ;
[] (s = 238) -> 1.000000:(s' = 286) ;
[] (s = 238) -> 1.000000:(s' = 287) ;
[] (s = 239) -> 1.000000:(s' = 288) ;
[] (s = 239) -> 1.000000:(s' = 289) ;
[] (s = 240) -> 1.000000:(s' = 290) ;
[] (s = 241) -> 1.000000:(s' = 291) ;
[] (s = 242) -> 1.000000:(s' = 292) ;
[] (s = 242) -> 1.000000:(s' = 293) ;
[] (s = 243) -> 1.000000:(s' = 294) ;
[] (s = 243) -> 1.000000:(s' = 295) ;
[] (s = 244) -> 1.000000:(s' = 296) ;
[] (s = 244) -> 1.000000:(s' = 297) ;
[] (s = 245) -> 1.000000:(s' = 298) ;
[] (s = 245) -> 1.000000:(s' = 299) ;
[] (s = 246) -> 1.000000:(s' = 300) ;
[] (s = 247) -> 1.000000:(s' = 301) ;
[] (s = 248) -> 1.000000:(s' = 302) ;
[] (s = 248) -> 1.000000:(s' = 303) ;
[] (s = 249) -> 1.000000:(s' = 304) ;
[] (s = 249) -> 1.000000:(s' = 305) ;
[] (s = 250) -> 1.000000:(s' = 306) ;
[] (s = 250) -> 1.000000:(s' = 307) ;
[] (s = 251) -> 1.000000:(s' = 308) ;
[] (s = 251) -> 1.000000:(s' = 309) ;
[] (s = 252) -> 1.000000:(s' = 310) ;
[] (s = 253) -> 1.000000:(s' = 311) ;
[] (s = 254) -> 1.000000:(s' = 312) ;
[] (s = 254) -> 1.000000:(s' = 313) ;
[] (s = 255) -> 1.000000:(s' = 314) ;
[] (s = 255) -> 1.000000:(s' = 315) ;
[] (s = 256) -> 1.000000:(s' = 316) ;
[] (s = 256) -> 1.000000:(s' = 317) ;
[] (s = 257) -> 1.000000:(s' = 318) ;
[] (s = 258) -> 1.000000:(s' = 319) ;
[] (s = 258) -> 1.000000:(s' = 320) ;
[] (s = 259) -> 1.000000:(s' = 321) ;
[] (s = 260) -> 1.000000:(s' = 322) ;
[] (s = 261) -> 1.000000:(s' = 323) ;
[] (s = 262) -> 1.000000:(s' = 324) ;
[] (s = 262) -> 1.000000:(s' = 325) ;
[] (s = 263) -> 1.000000:(s' = 326) ;
[] (s = 264) -> 1.000000:(s' = 327) ;
[] (s = 264) -> 1.000000:(s' = 328) ;
[] (s = 265) -> 1.000000:(s' = 329) ;
[] (s = 266) -> 1.000000:(s' = 330) ;
[] (s = 266) -> 1.000000:(s' = 331) ;
[] (s = 267) -> 1.000000:(s' = 332) ;
[] (s = 268) -> 1.000000:(s' = 319) ;
[] (s = 268) -> 1.000000:(s' = 320) ;
[] (s = 269) -> 1.000000:(s' = 333) ;
[] (s = 270) -> 1.000000:(s' = 334) ;
[] (s = 271) -> 1.000000:(s' = 335) ;
[] (s = 272) -> 1.000000:(s' = 336) ;
[] (s = 272) -> 1.000000:(s' = 337) ;
[] (s = 273) -> 1.000000:(s' = 338) ;
[] (s = 274) -> 1.000000:(s' = 327) ;
[] (s = 274) -> 1.000000:(s' = 328) ;
[] (s = 275) -> 1.000000:(s' = 339) ;
[] (s = 276) -> 1.000000:(s' = 330) ;
[] (s = 276) -> 1.000000:(s' = 331) ;
[] (s = 277) -> 1.000000:(s' = 340) ;
[] (s = 278) -> 1.000000:(s' = 341) ;
[] (s = 278) -> 1.000000:(s' = 342) ;
[] (s = 279) -> 1.000000:(s' = 343) ;
[] (s = 280) -> 1.000000:(s' = 344) ;
[] (s = 281) -> 1.000000:(s' = 345) ;
[] (s = 282) -> 1.000000:(s' = 336) ;
[] (s = 282) -> 1.000000:(s' = 337) ;
[] (s = 283) -> 1.000000:(s' = 346) ;
[] (s = 284) -> 1.000000:(s' = 347) ;
[] (s = 284) -> 1.000000:(s' = 348) ;
[] (s = 285) -> 1.000000:(s' = 349) ;
[] (s = 286) -> 1.000000:(s' = 350) ;
[] (s = 286) -> 1.000000:(s' = 351) ;
[] (s = 287) -> 1.000000:(s' = 352) ;
[] (s = 288) -> 1.000000:(s' = 353) ;
[] (s = 288) -> 1.000000:(s' = 354) ;
[] (s = 289) -> 1.000000:(s' = 355) ;
[] (s = 290) -> 1.000000:(s' = 356) ;
[] (s = 291) -> 1.000000:(s' = 357) ;
[] (s = 292) -> 1.000000:(s' = 358) ;
[] (s = 292) -> 1.000000:(s' = 359) ;
[] (s = 293) -> 1.000000:(s' = 360) ;
[] (s = 294) -> 1.000000:(s' = 361) ;
[] (s = 294) -> 1.000000:(s' = 362) ;
[] (s = 295) -> 1.000000:(s' = 363) ;
[] (s = 296) -> 1.000000:(s' = 364) ;
[] (s = 296) -> 1.000000:(s' = 365) ;
[] (s = 297) -> 1.000000:(s' = 366) ;
[] (s = 298) -> 1.000000:(s' = 353) ;
[] (s = 298) -> 1.000000:(s' = 354) ;
[] (s = 299) -> 1.000000:(s' = 367) ;
[] (s = 300) -> 1.000000:(s' = 368) ;
[] (s = 301) -> 1.000000:(s' = 369) ;
[] (s = 302) -> 1.000000:(s' = 370) ;
[] (s = 302) -> 1.000000:(s' = 371) ;
[] (s = 303) -> 1.000000:(s' = 372) ;
[] (s = 304) -> 1.000000:(s' = 361) ;
[] (s = 304) -> 1.000000:(s' = 362) ;
[] (s = 305) -> 1.000000:(s' = 373) ;
[] (s = 306) -> 1.000000:(s' = 364) ;
[] (s = 306) -> 1.000000:(s' = 365) ;
[] (s = 307) -> 1.000000:(s' = 374) ;
[] (s = 308) -> 1.000000:(s' = 375) ;
[] (s = 308) -> 1.000000:(s' = 376) ;
[] (s = 309) -> 1.000000:(s' = 377) ;
[] (s = 310) -> 1.000000:(s' = 378) ;
[] (s = 311) -> 1.000000:(s' = 379) ;
[] (s = 312) -> 1.000000:(s' = 370) ;
[] (s = 312) -> 1.000000:(s' = 371) ;
[] (s = 313) -> 1.000000:(s' = 380) ;
[] (s = 314) -> 1.000000:(s' = 381) ;
[] (s = 314) -> 1.000000:(s' = 382) ;
[] (s = 315) -> 1.000000:(s' = 383) ;
[] (s = 316) -> 0.500000:(s' = 384) + 0.500000:(s' = 385);
[] (s = 316) -> 1.000000:(s' = 386) ;
[] (s = 317) -> 1.000000:(s' = 386) ;
[] (s = 317) -> 0.500000:(s' = 387) + 0.500000:(s' = 388);
[] (s = 318) -> 1.000000:(s' = 60) ;
[] (s = 319) -> 0.500000:(s' = 389) + 0.500000:(s' = 390);
[] (s = 319) -> 1.000000:(s' = 391) ;
[] (s = 320) -> 1.000000:(s' = 391) ;
[] (s = 320) -> 0.500000:(s' = 392) + 0.500000:(s' = 393);
[] (s = 321) -> 1.000000:(s' = 60) ;
[] (s = 322) -> 1.000000:(s' = 60) ;
[] (s = 323) -> 1.000000:(s' = 60) ;
[] (s = 324) -> 0.500000:(s' = 394) + 0.500000:(s' = 395);
[] (s = 324) -> 1.000000:(s' = 396) ;
[] (s = 325) -> 1.000000:(s' = 396) ;
[] (s = 325) -> 0.500000:(s' = 397) + 0.500000:(s' = 398);
[] (s = 326) -> 1.000000:(s' = 60) ;
[] (s = 327) -> 0.500000:(s' = 399) + 0.500000:(s' = 400);
[] (s = 327) -> 1.000000:(s' = 401) ;
[] (s = 328) -> 1.000000:(s' = 401) ;
[] (s = 328) -> 0.500000:(s' = 402) + 0.500000:(s' = 403);
[] (s = 329) -> 1.000000:(s' = 60) ;
[] (s = 330) -> 0.500000:(s' = 404) + 0.500000:(s' = 405);
[] (s = 330) -> 1.000000:(s' = 406) ;
[] (s = 331) -> 1.000000:(s' = 406) ;
[] (s = 331) -> 0.500000:(s' = 407) + 0.500000:(s' = 408);
[] (s = 332) -> 1.000000:(s' = 60) ;
[] (s = 333) -> 1.000000:(s' = 60) ;
[] (s = 334) -> 1.000000:(s' = 60) ;
[] (s = 335) -> 1.000000:(s' = 60) ;
[] (s = 336) -> 0.500000:(s' = 409) + 0.500000:(s' = 410);
[] (s = 336) -> 1.000000:(s' = 411) ;
[] (s = 337) -> 1.000000:(s' = 411) ;
[] (s = 337) -> 0.500000:(s' = 412) + 0.500000:(s' = 413);
[] (s = 338) -> 1.000000:(s' = 60) ;
[] (s = 339) -> 1.000000:(s' = 60) ;
[] (s = 340) -> 1.000000:(s' = 60) ;
[] (s = 341) -> 0.500000:(s' = 414) + 0.500000:(s' = 415);
[] (s = 341) -> 1.000000:(s' = 416) ;
[] (s = 342) -> 1.000000:(s' = 416) ;
[] (s = 342) -> 0.500000:(s' = 417) + 0.500000:(s' = 418);
[] (s = 343) -> 1.000000:(s' = 60) ;
[] (s = 344) -> 1.000000:(s' = 60) ;
[] (s = 345) -> 1.000000:(s' = 60) ;
[] (s = 346) -> 1.000000:(s' = 60) ;
[] (s = 347) -> 0.500000:(s' = 419) + 0.500000:(s' = 420);
[] (s = 347) -> 1.000000:(s' = 421) ;
[] (s = 348) -> 1.000000:(s' = 421) ;
[] (s = 348) -> 0.500000:(s' = 422) + 0.500000:(s' = 423);
[] (s = 349) -> 1.000000:(s' = 60) ;
[] (s = 350) -> 0.500000:(s' = 424) + 0.500000:(s' = 425);
[] (s = 350) -> 1.000000:(s' = 396) ;
[] (s = 351) -> 1.000000:(s' = 396) ;
[] (s = 351) -> 0.500000:(s' = 426) + 0.500000:(s' = 427);
[] (s = 352) -> 1.000000:(s' = 60) ;
[] (s = 353) -> 0.500000:(s' = 428) + 0.500000:(s' = 429);
[] (s = 353) -> 1.000000:(s' = 430) ;
[] (s = 354) -> 1.000000:(s' = 430) ;
[] (s = 354) -> 0.500000:(s' = 431) + 0.500000:(s' = 432);
[] (s = 355) -> 1.000000:(s' = 60) ;
[] (s = 356) -> 1.000000:(s' = 60) ;
[] (s = 356) -> 1.000000:(s' = 433) ;
[] (s = 357) -> 1.000000:(s' = 60) ;
[] (s = 357) -> 1.000000:(s' = 433) ;
[] (s = 358) -> 0.500000:(s' = 434) + 0.500000:(s' = 435);
[] (s = 358) -> 1.000000:(s' = 436) ;
[] (s = 359) -> 1.000000:(s' = 436) ;
[] (s = 359) -> 0.500000:(s' = 437) + 0.500000:(s' = 438);
[] (s = 360) -> 1.000000:(s' = 60) ;
[] (s = 360) -> 1.000000:(s' = 433) ;
[] (s = 361) -> 0.500000:(s' = 439) + 0.500000:(s' = 440);
[] (s = 361) -> 1.000000:(s' = 441) ;
[] (s = 362) -> 1.000000:(s' = 441) ;
[] (s = 362) -> 0.500000:(s' = 442) + 0.500000:(s' = 443);
[] (s = 363) -> 1.000000:(s' = 60) ;
[] (s = 363) -> 1.000000:(s' = 433) ;
[] (s = 364) -> 0.500000:(s' = 444) + 0.500000:(s' = 445);
[] (s = 364) -> 1.000000:(s' = 446) ;
[] (s = 365) -> 1.000000:(s' = 446) ;
[] (s = 365) -> 0.500000:(s' = 447) + 0.500000:(s' = 448);
[] (s = 366) -> 1.000000:(s' = 60) ;
[] (s = 367) -> 1.000000:(s' = 60) ;
[] (s = 368) -> 1.000000:(s' = 60) ;
[] (s = 368) -> 1.000000:(s' = 433) ;
[] (s = 369) -> 1.000000:(s' = 60) ;
[] (s = 369) -> 1.000000:(s' = 433) ;
[] (s = 370) -> 0.500000:(s' = 449) + 0.500000:(s' = 450);
[] (s = 370) -> 1.000000:(s' = 451) ;
[] (s = 371) -> 1.000000:(s' = 451) ;
[] (s = 371) -> 0.500000:(s' = 452) + 0.500000:(s' = 453);
[] (s = 372) -> 1.000000:(s' = 60) ;
[] (s = 372) -> 1.000000:(s' = 433) ;
[] (s = 373) -> 1.000000:(s' = 60) ;
[] (s = 373) -> 1.000000:(s' = 433) ;
[] (s = 374) -> 1.000000:(s' = 60) ;
[] (s = 375) -> 0.500000:(s' = 454) + 0.500000:(s' = 455);
[] (s = 375) -> 1.000000:(s' = 421) ;
[] (s = 376) -> 1.000000:(s' = 421) ;
[] (s = 376) -> 0.500000:(s' = 456) + 0.500000:(s' = 457);
[] (s = 377) -> 1.000000:(s' = 60) ;
[] (s = 378) -> 1.000000:(s' = 60) ;
[] (s = 378) -> 1.000000:(s' = 433) ;
[] (s = 379) -> 1.000000:(s' = 60) ;
[] (s = 379) -> 1.000000:(s' = 433) ;
[] (s = 380) -> 1.000000:(s' = 60) ;
[] (s = 380) -> 1.000000:(s' = 433) ;
[] (s = 381) -> 0.500000:(s' = 458) + 0.500000:(s' = 459);
[] (s = 381) -> 1.000000:(s' = 460) ;
[] (s = 382) -> 1.000000:(s' = 460) ;
[] (s = 382) -> 0.500000:(s' = 461) + 0.500000:(s' = 462);
[] (s = 383) -> 1.000000:(s' = 60) ;
[] (s = 383) -> 1.000000:(s' = 433) ;
[] (s = 384) -> 1.000000:(s' = 463) ;
[] (s = 385) -> 1.000000:(s' = 464) ;
[] (s = 386) -> 0.500000:(s' = 465) + 0.500000:(s' = 466);
[] (s = 386) -> 0.500000:(s' = 467) + 0.500000:(s' = 468);
[] (s = 387) -> 1.000000:(s' = 469) ;
[] (s = 388) -> 1.000000:(s' = 470) ;
[] (s = 389) -> 1.000000:(s' = 471) ;
[] (s = 390) -> 1.000000:(s' = 472) ;
[] (s = 391) -> 0.500000:(s' = 465) + 0.500000:(s' = 466);
[] (s = 391) -> 0.500000:(s' = 467) + 0.500000:(s' = 468);
[] (s = 392) -> 1.000000:(s' = 473) ;
[] (s = 393) -> 1.000000:(s' = 474) ;
[] (s = 394) -> 1.000000:(s' = 475) ;
[] (s = 395) -> 1.000000:(s' = 476) ;
[] (s = 396) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 396) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 397) -> 1.000000:(s' = 481) ;
[] (s = 398) -> 1.000000:(s' = 482) ;
[] (s = 399) -> 1.000000:(s' = 483) ;
[] (s = 400) -> 1.000000:(s' = 484) ;
[] (s = 401) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 401) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 402) -> 1.000000:(s' = 485) ;
[] (s = 403) -> 1.000000:(s' = 486) ;
[] (s = 404) -> 1.000000:(s' = 487) ;
[] (s = 405) -> 1.000000:(s' = 488) ;
[] (s = 406) -> 0.500000:(s' = 465) + 0.500000:(s' = 466);
[] (s = 406) -> 0.500000:(s' = 467) + 0.500000:(s' = 468);
[] (s = 407) -> 1.000000:(s' = 489) ;
[] (s = 408) -> 1.000000:(s' = 490) ;
[] (s = 409) -> 1.000000:(s' = 491) ;
[] (s = 410) -> 1.000000:(s' = 492) ;
[] (s = 411) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 411) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 412) -> 1.000000:(s' = 493) ;
[] (s = 413) -> 1.000000:(s' = 494) ;
[] (s = 414) -> 1.000000:(s' = 495) ;
[] (s = 415) -> 1.000000:(s' = 496) ;
[] (s = 416) -> 0.500000:(s' = 465) + 0.500000:(s' = 466);
[] (s = 416) -> 0.500000:(s' = 467) + 0.500000:(s' = 468);
[] (s = 417) -> 1.000000:(s' = 497) ;
[] (s = 418) -> 1.000000:(s' = 498) ;
[] (s = 419) -> 1.000000:(s' = 499) ;
[] (s = 420) -> 1.000000:(s' = 500) ;
[] (s = 421) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 421) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 422) -> 1.000000:(s' = 501) ;
[] (s = 423) -> 1.000000:(s' = 502) ;
[] (s = 424) -> 1.000000:(s' = 475) ;
[] (s = 425) -> 1.000000:(s' = 476) ;
[] (s = 426) -> 1.000000:(s' = 481) ;
[] (s = 427) -> 1.000000:(s' = 482) ;
[] (s = 428) -> 1.000000:(s' = 503) ;
[] (s = 429) -> 1.000000:(s' = 504) ;
[] (s = 430) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 430) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 431) -> 1.000000:(s' = 505) ;
[] (s = 432) -> 1.000000:(s' = 506) ;
[] (s = 434) -> 1.000000:(s' = 507) ;
[] (s = 435) -> 1.000000:(s' = 508) ;
[] (s = 436) -> 0.500000:(s' = 509) + 0.500000:(s' = 510);
[] (s = 436) -> 0.500000:(s' = 511) + 0.500000:(s' = 512);
[] (s = 437) -> 1.000000:(s' = 513) ;
[] (s = 438) -> 1.000000:(s' = 514) ;
[] (s = 439) -> 1.000000:(s' = 515) ;
[] (s = 440) -> 1.000000:(s' = 516) ;
[] (s = 441) -> 0.500000:(s' = 509) + 0.500000:(s' = 510);
[] (s = 441) -> 0.500000:(s' = 511) + 0.500000:(s' = 512);
[] (s = 442) -> 1.000000:(s' = 517) ;
[] (s = 443) -> 1.000000:(s' = 518) ;
[] (s = 444) -> 1.000000:(s' = 519) ;
[] (s = 445) -> 1.000000:(s' = 520) ;
[] (s = 446) -> 0.500000:(s' = 477) + 0.500000:(s' = 478);
[] (s = 446) -> 0.500000:(s' = 479) + 0.500000:(s' = 480);
[] (s = 447) -> 1.000000:(s' = 521) ;
[] (s = 448) -> 1.000000:(s' = 522) ;
[] (s = 449) -> 1.000000:(s' = 523) ;
[] (s = 450) -> 1.000000:(s' = 524) ;
[] (s = 451) -> 0.500000:(s' = 509) + 0.500000:(