//
// 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:(s' = 510);
[] (s = 451) -> 0.500000:(s' = 511) + 0.500000:(s' = 512);
[] (s = 452) -> 1.000000:(s' = 525) ;
[] (s = 453) -> 1.000000:(s' = 526) ;
[] (s = 454) -> 1.000000:(s' = 499) ;
[] (s = 455) -> 1.000000:(s' = 500) ;
[] (s = 456) -> 1.000000:(s' = 501) ;
[] (s = 457) -> 1.000000:(s' = 502) ;
[] (s = 458) -> 1.000000:(s' = 527) ;
[] (s = 459) -> 1.000000:(s' = 528) ;
[] (s = 460) -> 0.500000:(s' = 509) + 0.500000:(s' = 510);
[] (s = 460) -> 0.500000:(s' = 511) + 0.500000:(s' = 512);
[] (s = 461) -> 1.000000:(s' = 529) ;
[] (s = 462) -> 1.000000:(s' = 530) ;
[] (s = 463) -> 0.500000:(s' = 531) + 0.500000:(s' = 532);
[] (s = 463) -> 1.000000:(s' = 533) ;
[] (s = 464) -> 0.500000:(s' = 534) + 0.500000:(s' = 535);
[] (s = 464) -> 1.000000:(s' = 536) ;
[] (s = 465) -> 0.500000:(s' = 537) + 0.500000:(s' = 538);
[] (s = 465) -> 1.000000:(s' = 539) ;
[] (s = 466) -> 0.500000:(s' = 540) + 0.500000:(s' = 541);
[] (s = 466) -> 1.000000:(s' = 542) ;
[] (s = 467) -> 1.000000:(s' = 543) ;
[] (s = 467) -> 0.500000:(s' = 537) + 0.500000:(s' = 540);
[] (s = 468) -> 1.000000:(s' = 544) ;
[] (s = 468) -> 0.500000:(s' = 538) + 0.500000:(s' = 541);
[] (s = 469) -> 1.000000:(s' = 545) ;
[] (s = 469) -> 0.500000:(s' = 546) + 0.500000:(s' = 547);
[] (s = 470) -> 1.000000:(s' = 548) ;
[] (s = 470) -> 0.500000:(s' = 549) + 0.500000:(s' = 550);
[] (s = 471) -> 0.500000:(s' = 531) + 0.500000:(s' = 532);
[] (s = 471) -> 1.000000:(s' = 551) ;
[] (s = 472) -> 0.500000:(s' = 534) + 0.500000:(s' = 535);
[] (s = 472) -> 1.000000:(s' = 552) ;
[] (s = 473) -> 1.000000:(s' = 553) ;
[] (s = 473) -> 0.500000:(s' = 546) + 0.500000:(s' = 547);
[] (s = 474) -> 1.000000:(s' = 554) ;
[] (s = 474) -> 0.500000:(s' = 549) + 0.500000:(s' = 550);
[] (s = 475) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 475) -> 1.000000:(s' = 557) ;
[] (s = 476) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 476) -> 1.000000:(s' = 560) ;
[] (s = 477) -> 0.500000:(s' = 561) + 0.500000:(s' = 562);
[] (s = 477) -> 1.000000:(s' = 563) ;
[] (s = 478) -> 0.500000:(s' = 564) + 0.500000:(s' = 565);
[] (s = 478) -> 1.000000:(s' = 566) ;
[] (s = 479) -> 1.000000:(s' = 567) ;
[] (s = 479) -> 0.500000:(s' = 561) + 0.500000:(s' = 564);
[] (s = 480) -> 1.000000:(s' = 568) ;
[] (s = 480) -> 0.500000:(s' = 562) + 0.500000:(s' = 565);
[] (s = 481) -> 1.000000:(s' = 569) ;
[] (s = 481) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 482) -> 1.000000:(s' = 572) ;
[] (s = 482) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 483) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 483) -> 1.000000:(s' = 575) ;
[] (s = 484) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 484) -> 1.000000:(s' = 576) ;
[] (s = 485) -> 1.000000:(s' = 577) ;
[] (s = 485) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 486) -> 1.000000:(s' = 578) ;
[] (s = 486) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 487) -> 0.500000:(s' = 531) + 0.500000:(s' = 532);
[] (s = 487) -> 1.000000:(s' = 579) ;
[] (s = 488) -> 0.500000:(s' = 534) + 0.500000:(s' = 535);
[] (s = 488) -> 1.000000:(s' = 580) ;
[] (s = 489) -> 1.000000:(s' = 581) ;
[] (s = 489) -> 0.500000:(s' = 546) + 0.500000:(s' = 547);
[] (s = 490) -> 1.000000:(s' = 582) ;
[] (s = 490) -> 0.500000:(s' = 549) + 0.500000:(s' = 550);
[] (s = 491) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 491) -> 1.000000:(s' = 583) ;
[] (s = 492) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 492) -> 1.000000:(s' = 584) ;
[] (s = 493) -> 1.000000:(s' = 585) ;
[] (s = 493) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 494) -> 1.000000:(s' = 586) ;
[] (s = 494) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 495) -> 0.500000:(s' = 531) + 0.500000:(s' = 532);
[] (s = 495) -> 1.000000:(s' = 587) ;
[] (s = 496) -> 0.500000:(s' = 534) + 0.500000:(s' = 535);
[] (s = 496) -> 1.000000:(s' = 588) ;
[] (s = 497) -> 1.000000:(s' = 589) ;
[] (s = 497) -> 0.500000:(s' = 546) + 0.500000:(s' = 547);
[] (s = 498) -> 1.000000:(s' = 590) ;
[] (s = 498) -> 0.500000:(s' = 549) + 0.500000:(s' = 550);
[] (s = 499) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 499) -> 1.000000:(s' = 591) ;
[] (s = 500) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 500) -> 1.000000:(s' = 592) ;
[] (s = 501) -> 1.000000:(s' = 593) ;
[] (s = 501) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 502) -> 1.000000:(s' = 594) ;
[] (s = 502) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 503) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 503) -> 1.000000:(s' = 595) ;
[] (s = 504) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 504) -> 1.000000:(s' = 596) ;
[] (s = 505) -> 1.000000:(s' = 597) ;
[] (s = 505) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 506) -> 1.000000:(s' = 598) ;
[] (s = 506) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 507) -> 0.500000:(s' = 599) + 0.500000:(s' = 600);
[] (s = 507) -> 1.000000:(s' = 601) ;
[] (s = 508) -> 0.500000:(s' = 602) + 0.500000:(s' = 603);
[] (s = 508) -> 1.000000:(s' = 604) ;
[] (s = 509) -> 0.500000:(s' = 605) + 0.500000:(s' = 606);
[] (s = 509) -> 1.000000:(s' = 607) ;
[] (s = 510) -> 0.500000:(s' = 608) + 0.500000:(s' = 609);
[] (s = 510) -> 1.000000:(s' = 610) ;
[] (s = 511) -> 1.000000:(s' = 611) ;
[] (s = 511) -> 0.500000:(s' = 605) + 0.500000:(s' = 608);
[] (s = 512) -> 1.000000:(s' = 612) ;
[] (s = 512) -> 0.500000:(s' = 606) + 0.500000:(s' = 609);
[] (s = 513) -> 1.000000:(s' = 613) ;
[] (s = 513) -> 0.500000:(s' = 614) + 0.500000:(s' = 615);
[] (s = 514) -> 1.000000:(s' = 616) ;
[] (s = 514) -> 0.500000:(s' = 617) + 0.500000:(s' = 618);
[] (s = 515) -> 0.500000:(s' = 599) + 0.500000:(s' = 600);
[] (s = 515) -> 1.000000:(s' = 619) ;
[] (s = 516) -> 0.500000:(s' = 602) + 0.500000:(s' = 603);
[] (s = 516) -> 1.000000:(s' = 620) ;
[] (s = 517) -> 1.000000:(s' = 621) ;
[] (s = 517) -> 0.500000:(s' = 614) + 0.500000:(s' = 615);
[] (s = 518) -> 1.000000:(s' = 622) ;
[] (s = 518) -> 0.500000:(s' = 617) + 0.500000:(s' = 618);
[] (s = 519) -> 0.500000:(s' = 555) + 0.500000:(s' = 556);
[] (s = 519) -> 1.000000:(s' = 623) ;
[] (s = 520) -> 0.500000:(s' = 558) + 0.500000:(s' = 559);
[] (s = 520) -> 1.000000:(s' = 624) ;
[] (s = 521) -> 1.000000:(s' = 625) ;
[] (s = 521) -> 0.500000:(s' = 570) + 0.500000:(s' = 571);
[] (s = 522) -> 1.000000:(s' = 626) ;
[] (s = 522) -> 0.500000:(s' = 573) + 0.500000:(s' = 574);
[] (s = 523) -> 0.500000:(s' = 599) + 0.500000:(s' = 600);
[] (s = 523) -> 1.000000:(s' = 627) ;
[] (s = 524) -> 0.500000:(s' = 602) + 0.500000:(s' = 603);
[] (s = 524) -> 1.000000:(s' = 628) ;
[] (s = 525) -> 1.000000:(s' = 629) ;
[] (s = 525) -> 0.500000:(s' = 614) + 0.500000:(s' = 615);
[] (s = 526) -> 1.000000:(s' = 630) ;
[] (s = 526) -> 0.500000:(s' = 617) + 0.500000:(s' = 618);
[] (s = 527) -> 0.500000:(s' = 599) + 0.500000:(s' = 600);
[] (s = 527) -> 1.000000:(s' = 631) ;
[] (s = 528) -> 0.500000:(s' = 602) + 0.500000:(s' = 603);
[] (s = 528) -> 1.000000:(s' = 632) ;
[] (s = 529) -> 1.000000:(s' = 633) ;
[] (s = 529) -> 0.500000:(s' = 614) + 0.500000:(s' = 615);
[] (s = 530) -> 1.000000:(s' = 634) ;
[] (s = 530) -> 0.500000:(s' = 617) + 0.500000:(s' = 618);
[] (s = 531) -> 1.000000:(s' = 635) ;
[] (s = 531) -> 1.000000:(s' = 636) ;
[] (s = 532) -> 1.000000:(s' = 637) ;
[] (s = 532) -> 1.000000:(s' = 638) ;
[] (s = 533) -> 0.500000:(s' = 636) + 0.500000:(s' = 638);
[] (s = 534) -> 1.000000:(s' = 639) ;
[] (s = 534) -> 1.000000:(s' = 640) ;
[] (s = 535) -> 1.000000:(s' = 641) ;
[] (s = 535) -> 1.000000:(s' = 642) ;
[] (s = 536) -> 0.500000:(s' = 640) + 0.500000:(s' = 642);
[] (s = 537) -> 1.000000:(s' = 643) ;
[] (s = 537) -> 1.000000:(s' = 644) ;
[] (s = 538) -> 1.000000:(s' = 645) ;
[] (s = 538) -> 1.000000:(s' = 646) ;
[] (s = 539) -> 0.500000:(s' = 644) + 0.500000:(s' = 646);
[] (s = 540) -> 1.000000:(s' = 647) ;
[] (s = 540) -> 1.000000:(s' = 648) ;
[] (s = 541) -> 1.000000:(s' = 649) ;
[] (s = 541) -> 1.000000:(s' = 650) ;
[] (s = 542) -> 0.500000:(s' = 648) + 0.500000:(s' = 650);
[] (s = 543) -> 0.500000:(s' = 643) + 0.500000:(s' = 647);
[] (s = 544) -> 0.500000:(s' = 645) + 0.500000:(s' = 649);
[] (s = 545) -> 0.500000:(s' = 651) + 0.500000:(s' = 652);
[] (s = 546) -> 1.000000:(s' = 651) ;
[] (s = 546) -> 1.000000:(s' = 653) ;
[] (s = 547) -> 1.000000:(s' = 652) ;
[] (s = 547) -> 1.000000:(s' = 654) ;
[] (s = 548) -> 0.500000:(s' = 655) + 0.500000:(s' = 656);
[] (s = 549) -> 1.000000:(s' = 655) ;
[] (s = 549) -> 1.000000:(s' = 657) ;
[] (s = 550) -> 1.000000:(s' = 656) ;
[] (s = 550) -> 1.000000:(s' = 658) ;
[] (s = 551) -> 0.500000:(s' = 636) + 0.500000:(s' = 638);
[] (s = 552) -> 0.500000:(s' = 640) + 0.500000:(s' = 642);
[] (s = 553) -> 0.500000:(s' = 651) + 0.500000:(s' = 652);
[] (s = 554) -> 0.500000:(s' = 655) + 0.500000:(s' = 656);
[] (s = 555) -> 1.000000:(s' = 659) ;
[] (s = 555) -> 1.000000:(s' = 660) ;
[] (s = 556) -> 1.000000:(s' = 661) ;
[] (s = 556) -> 1.000000:(s' = 662) ;
[] (s = 557) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 558) -> 1.000000:(s' = 663) ;
[] (s = 558) -> 1.000000:(s' = 664) ;
[] (s = 559) -> 1.000000:(s' = 665) ;
[] (s = 559) -> 1.000000:(s' = 666) ;
[] (s = 560) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 561) -> 1.000000:(s' = 667) ;
[] (s = 561) -> 1.000000:(s' = 668) ;
[] (s = 562) -> 1.000000:(s' = 669) ;
[] (s = 562) -> 1.000000:(s' = 670) ;
[] (s = 563) -> 0.500000:(s' = 668) + 0.500000:(s' = 670);
[] (s = 564) -> 1.000000:(s' = 671) ;
[] (s = 564) -> 1.000000:(s' = 672) ;
[] (s = 565) -> 1.000000:(s' = 673) ;
[] (s = 565) -> 1.000000:(s' = 674) ;
[] (s = 566) -> 0.500000:(s' = 672) + 0.500000:(s' = 674);
[] (s = 567) -> 0.500000:(s' = 667) + 0.500000:(s' = 671);
[] (s = 568) -> 0.500000:(s' = 669) + 0.500000:(s' = 673);
[] (s = 569) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 570) -> 1.000000:(s' = 675) ;
[] (s = 570) -> 1.000000:(s' = 677) ;
[] (s = 571) -> 1.000000:(s' = 676) ;
[] (s = 571) -> 1.000000:(s' = 678) ;
[] (s = 572) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 573) -> 1.000000:(s' = 679) ;
[] (s = 573) -> 1.000000:(s' = 681) ;
[] (s = 574) -> 1.000000:(s' = 680) ;
[] (s = 574) -> 1.000000:(s' = 682) ;
[] (s = 575) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 576) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 577) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 578) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 579) -> 0.500000:(s' = 636) + 0.500000:(s' = 638);
[] (s = 580) -> 0.500000:(s' = 640) + 0.500000:(s' = 642);
[] (s = 581) -> 0.500000:(s' = 651) + 0.500000:(s' = 652);
[] (s = 582) -> 0.500000:(s' = 655) + 0.500000:(s' = 656);
[] (s = 583) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 584) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 585) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 586) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 587) -> 0.500000:(s' = 636) + 0.500000:(s' = 638);
[] (s = 588) -> 0.500000:(s' = 640) + 0.500000:(s' = 642);
[] (s = 589) -> 0.500000:(s' = 651) + 0.500000:(s' = 652);
[] (s = 590) -> 0.500000:(s' = 655) + 0.500000:(s' = 656);
[] (s = 591) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 592) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 593) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 594) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 595) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 596) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 597) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 598) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 599) -> 1.000000:(s' = 683) ;
[] (s = 599) -> 1.000000:(s' = 684) ;
[] (s = 600) -> 1.000000:(s' = 685) ;
[] (s = 600) -> 1.000000:(s' = 686) ;
[] (s = 601) -> 0.500000:(s' = 684) + 0.500000:(s' = 686);
[] (s = 602) -> 1.000000:(s' = 687) ;
[] (s = 602) -> 1.000000:(s' = 688) ;
[] (s = 603) -> 1.000000:(s' = 689) ;
[] (s = 603) -> 1.000000:(s' = 690) ;
[] (s = 604) -> 0.500000:(s' = 688) + 0.500000:(s' = 690);
[] (s = 605) -> 1.000000:(s' = 691) ;
[] (s = 605) -> 1.000000:(s' = 692) ;
[] (s = 606) -> 1.000000:(s' = 693) ;
[] (s = 606) -> 1.000000:(s' = 694) ;
[] (s = 607) -> 0.500000:(s' = 692) + 0.500000:(s' = 694);
[] (s = 608) -> 1.000000:(s' = 695) ;
[] (s = 608) -> 1.000000:(s' = 696) ;
[] (s = 609) -> 1.000000:(s' = 697) ;
[] (s = 609) -> 1.000000:(s' = 698) ;
[] (s = 610) -> 0.500000:(s' = 696) + 0.500000:(s' = 698);
[] (s = 611) -> 0.500000:(s' = 691) + 0.500000:(s' = 695);
[] (s = 612) -> 0.500000:(s' = 693) + 0.500000:(s' = 697);
[] (s = 613) -> 0.500000:(s' = 699) + 0.500000:(s' = 700);
[] (s = 614) -> 1.000000:(s' = 699) ;
[] (s = 614) -> 1.000000:(s' = 701) ;
[] (s = 615) -> 1.000000:(s' = 700) ;
[] (s = 615) -> 1.000000:(s' = 702) ;
[] (s = 616) -> 0.500000:(s' = 703) + 0.500000:(s' = 704);
[] (s = 617) -> 1.000000:(s' = 703) ;
[] (s = 617) -> 1.000000:(s' = 705) ;
[] (s = 618) -> 1.000000:(s' = 704) ;
[] (s = 618) -> 1.000000:(s' = 706) ;
[] (s = 619) -> 0.500000:(s' = 684) + 0.500000:(s' = 686);
[] (s = 620) -> 0.500000:(s' = 688) + 0.500000:(s' = 690);
[] (s = 621) -> 0.500000:(s' = 699) + 0.500000:(s' = 700);
[] (s = 622) -> 0.500000:(s' = 703) + 0.500000:(s' = 704);
[] (s = 623) -> 0.500000:(s' = 660) + 0.500000:(s' = 662);
[] (s = 624) -> 0.500000:(s' = 664) + 0.500000:(s' = 666);
[] (s = 625) -> 0.500000:(s' = 675) + 0.500000:(s' = 676);
[] (s = 626) -> 0.500000:(s' = 679) + 0.500000:(s' = 680);
[] (s = 627) -> 0.500000:(s' = 684) + 0.500000:(s' = 686);
[] (s = 628) -> 0.500000:(s' = 688) + 0.500000:(s' = 690);
[] (s = 629) -> 0.500000:(s' = 699) + 0.500000:(s' = 700);
[] (s = 630) -> 0.500000:(s' = 703) + 0.500000:(s' = 704);
[] (s = 631) -> 0.500000:(s' = 684) + 0.500000:(s' = 686);
[] (s = 632) -> 0.500000:(s' = 688) + 0.500000:(s' = 690);
[] (s = 633) -> 0.500000:(s' = 699) + 0.500000:(s' = 700);
[] (s = 634) -> 0.500000:(s' = 703) + 0.500000:(s' = 704);
[] (s = 635) -> 1.000000:(s' = 707) ;
[] (s = 636) -> 1.000000:(s' = 707) ;
[] (s = 637) -> 1.000000:(s' = 708) ;
[] (s = 638) -> 1.000000:(s' = 708) ;
[] (s = 639) -> 1.000000:(s' = 709) ;
[] (s = 640) -> 1.000000:(s' = 709) ;
[] (s = 641) -> 1.000000:(s' = 710) ;
[] (s = 642) -> 1.000000:(s' = 710) ;
[] (s = 643) -> 1.000000:(s' = 711) ;
[] (s = 644) -> 1.000000:(s' = 711) ;
[] (s = 645) -> 1.000000:(s' = 712) ;
[] (s = 646) -> 1.000000:(s' = 712) ;
[] (s = 647) -> 1.000000:(s' = 713) ;
[] (s = 648) -> 1.000000:(s' = 713) ;
[] (s = 649) -> 1.000000:(s' = 714) ;
[] (s = 650) -> 1.000000:(s' = 714) ;
[] (s = 651) -> 1.000000:(s' = 715) ;
[] (s = 652) -> 1.000000:(s' = 716) ;
[] (s = 653) -> 1.000000:(s' = 715) ;
[] (s = 654) -> 1.000000:(s' = 716) ;
[] (s = 655) -> 1.000000:(s' = 717) ;
[] (s = 656) -> 1.000000:(s' = 718) ;
[] (s = 657) -> 1.000000:(s' = 717) ;
[] (s = 658) -> 1.000000:(s' = 718) ;
[] (s = 659) -> 1.000000:(s' = 719) ;
[] (s = 660) -> 1.000000:(s' = 719) ;
[] (s = 661) -> 1.000000:(s' = 720) ;
[] (s = 662) -> 1.000000:(s' = 720) ;
[] (s = 663) -> 1.000000:(s' = 721) ;
[] (s = 664) -> 1.000000:(s' = 721) ;
[] (s = 665) -> 1.000000:(s' = 722) ;
[] (s = 666) -> 1.000000:(s' = 722) ;
[] (s = 667) -> 1.000000:(s' = 723) ;
[] (s = 668) -> 1.000000:(s' = 723) ;
[] (s = 669) -> 1.000000:(s' = 724) ;
[] (s = 670) -> 1.000000:(s' = 724) ;
[] (s = 671) -> 1.000000:(s' = 725) ;
[] (s = 672) -> 1.000000:(s' = 725) ;
[] (s = 673) -> 1.000000:(s' = 726) ;
[] (s = 674) -> 1.000000:(s' = 726) ;
[] (s = 675) -> 1.000000:(s' = 727) ;
[] (s = 676) -> 1.000000:(s' = 728) ;
[] (s = 677) -> 1.000000:(s' = 727) ;
[] (s = 678) -> 1.000000:(s' = 728) ;
[] (s = 679) -> 1.000000:(s' = 729) ;
[] (s = 680) -> 1.000000:(s' = 730) ;
[] (s = 681) -> 1.000000:(s' = 729) ;
[] (s = 682) -> 1.000000:(s' = 730) ;
[] (s = 683) -> 1.000000:(s' = 731) ;
[] (s = 684) -> 1.000000:(s' = 731) ;
[] (s = 685) -> 1.000000:(s' = 732) ;
[] (s = 686) -> 1.000000:(s' = 732) ;
[] (s = 687) -> 1.000000:(s' = 733) ;
[] (s = 688) -> 1.000000:(s' = 733) ;
[] (s = 689) -> 1.000000:(s' = 734) ;
[] (s = 690) -> 1.000000:(s' = 734) ;
[] (s = 691) -> 1.000000:(s' = 735) ;
[] (s = 692) -> 1.000000:(s' = 735) ;
[] (s = 693) -> 1.000000:(s' = 736) ;
[] (s = 694) -> 1.000000:(s' = 736) ;
[] (s = 695) -> 1.000000:(s' = 737) ;
[] (s = 696) -> 1.000000:(s' = 737) ;
[] (s = 697) -> 1.000000:(s' = 738) ;
[] (s = 698) -> 1.000000:(s' = 738) ;
[] (s = 699) -> 1.000000:(s' = 739) ;
[] (s = 700) -> 1.000000:(s' = 740) ;
[] (s = 701) -> 1.000000:(s' = 739) ;
[] (s = 702) -> 1.000000:(s' = 740) ;
[] (s = 703) -> 1.000000:(s' = 741) ;
[] (s = 704) -> 1.000000:(s' = 742) ;
[] (s = 705) -> 1.000000:(s' = 741) ;
[] (s = 706) -> 1.000000:(s' = 742) ;
[] (s = 707) -> 1.000000:(s' = 743) ;
[] (s = 707) -> 1.000000:(s' = 744) ;
[] (s = 708) -> 1.000000:(s' = 745) ;
[] (s = 709) -> 1.000000:(s' = 746) ;
[] (s = 710) -> 1.000000:(s' = 747) ;
[] (s = 710) -> 1.000000:(s' = 748) ;
[] (s = 711) -> 1.000000:(s' = 749) ;
[] (s = 711) -> 1.000000:(s' = 750) ;
[] (s = 712) -> 1.000000:(s' = 751) ;
[] (s = 713) -> 1.000000:(s' = 752) ;
[] (s = 714) -> 1.000000:(s' = 753) ;
[] (s = 714) -> 1.000000:(s' = 754) ;
[] (s = 715) -> 1.000000:(s' = 755) ;
[] (s = 715) -> 1.000000:(s' = 756) ;
[] (s = 716) -> 1.000000:(s' = 757) ;
[] (s = 717) -> 1.000000:(s' = 758) ;
[] (s = 718) -> 1.000000:(s' = 759) ;
[] (s = 718) -> 1.000000:(s' = 760) ;
[] (s = 719) -> 1.000000:(s' = 761) ;
[] (s = 719) -> 1.000000:(s' = 762) ;
[] (s = 720) -> 1.000000:(s' = 763) ;
[] (s = 721) -> 1.000000:(s' = 764) ;
[] (s = 722) -> 1.000000:(s' = 765) ;
[] (s = 722) -> 1.000000:(s' = 766) ;
[] (s = 723) -> 1.000000:(s' = 767) ;
[] (s = 723) -> 1.000000:(s' = 768) ;
[] (s = 724) -> 1.000000:(s' = 769) ;
[] (s = 725) -> 1.000000:(s' = 770) ;
[] (s = 726) -> 1.000000:(s' = 771) ;
[] (s = 726) -> 1.000000:(s' = 772) ;
[] (s = 727) -> 1.000000:(s' = 773) ;
[] (s = 727) -> 1.000000:(s' = 774) ;
[] (s = 728) -> 1.000000:(s' = 775) ;
[] (s = 729) -> 1.000000:(s' = 776) ;
[] (s = 730) -> 1.000000:(s' = 777) ;
[] (s = 730) -> 1.000000:(s' = 778) ;
[] (s = 731) -> 1.000000:(s' = 779) ;
[] (s = 731) -> 1.000000:(s' = 780) ;
[] (s = 732) -> 1.000000:(s' = 781) ;
[] (s = 733) -> 1.000000:(s' = 782) ;
[] (s = 734) -> 1.000000:(s' = 783) ;
[] (s = 734) -> 1.000000:(s' = 784) ;
[] (s = 735) -> 1.000000:(s' = 785) ;
[] (s = 735) -> 1.000000:(s' = 786) ;
[] (s = 736) -> 1.000000:(s' = 787) ;
[] (s = 737) -> 1.000000:(s' = 788) ;
[] (s = 738) -> 1.000000:(s' = 789) ;
[] (s = 738) -> 1.000000:(s' = 790) ;
[] (s = 739) -> 1.000000:(s' = 791) ;
[] (s = 739) -> 1.000000:(s' = 792) ;
[] (s = 740) -> 1.000000:(s' = 793) ;
[] (s = 741) -> 1.000000:(s' = 794) ;
[] (s = 742) -> 1.000000:(s' = 795) ;
[] (s = 742) -> 1.000000:(s' = 796) ;
[] (s = 743) -> 1.000000:(s' = 797) ;
[] (s = 743) -> 1.000000:(s' = 798) ;
[] (s = 744) -> 1.000000:(s' = 799) ;
[] (s = 744) -> 1.000000:(s' = 800) ;
[] (s = 745) -> 1.000000:(s' = 801) ;
[] (s = 746) -> 1.000000:(s' = 802) ;
[] (s = 747) -> 1.000000:(s' = 803) ;
[] (s = 747) -> 1.000000:(s' = 804) ;
[] (s = 748) -> 1.000000:(s' = 805) ;
[] (s = 748) -> 1.000000:(s' = 806) ;
[] (s = 749) -> 1.000000:(s' = 807) ;
[] (s = 749) -> 1.000000:(s' = 808) ;
[] (s = 750) -> 1.000000:(s' = 809) ;
[] (s = 750) -> 1.000000:(s' = 810) ;
[] (s = 751) -> 1.000000:(s' = 811) ;
[] (s = 752) -> 1.000000:(s' = 812) ;
[] (s = 753) -> 1.000000:(s' = 813) ;
[] (s = 753) -> 1.000000:(s' = 814) ;
[] (s = 754) -> 1.000000:(s' = 815) ;
[] (s = 754) -> 1.000000:(s' = 816) ;
[] (s = 755) -> 1.000000:(s' = 817) ;
[] (s = 755) -> 1.000000:(s' = 818) ;
[] (s = 756) -> 1.000000:(s' = 819) ;
[] (s = 756) -> 1.000000:(s' = 820) ;
[] (s = 757) -> 1.000000:(s' = 821) ;
[] (s = 758) -> 1.000000:(s' = 822) ;
[] (s = 759) -> 1.000000:(s' = 823) ;
[] (s = 759) -> 1.000000:(s' = 824) ;
[] (s = 760) -> 1.000000:(s' = 825) ;
[] (s = 760) -> 1.000000:(s' = 826) ;
[] (s = 761) -> 1.000000:(s' = 827) ;
[] (s = 761) -> 1.000000:(s' = 828) ;
[] (s = 762) -> 1.000000:(s' = 829) ;
[] (s = 762) -> 1.000000:(s' = 830) ;
[] (s = 763) -> 1.000000:(s' = 831) ;
[] (s = 764) -> 1.000000:(s' = 832) ;
[] (s = 765) -> 1.000000:(s' = 833) ;
[] (s = 765) -> 1.000000:(s' = 834) ;
[] (s = 766) -> 1.000000:(s' = 835) ;
[] (s = 766) -> 1.000000:(s' = 836) ;
[] (s = 767) -> 1.000000:(s' = 837) ;
[] (s = 767) -> 1.000000:(s' = 838) ;
[] (s = 768) -> 1.000000:(s' = 839) ;
[] (s = 768) -> 1.000000:(s' = 840) ;
[] (s = 769) -> 1.000000:(s' = 841) ;
[] (s = 770) -> 1.000000:(s' = 842) ;
[] (s = 771) -> 1.000000:(s' = 843) ;
[] (s = 771) -> 1.000000:(s' = 844) ;
[] (s = 772) -> 1.000000:(s' = 845) ;
[] (s = 772) -> 1.000000:(s' = 846) ;
[] (s = 773) -> 1.000000:(s' = 847) ;
[] (s = 773) -> 1.000000:(s' = 848) ;
[] (s = 774) -> 1.000000:(s' = 849) ;
[] (s = 774) -> 1.000000:(s' = 850) ;
[] (s = 775) -> 1.000000:(s' = 851) ;
[] (s = 776) -> 1.000000:(s' = 852) ;
[] (s = 777) -> 1.000000:(s' = 853) ;
[] (s = 777) -> 1.000000:(s' = 854) ;
[] (s = 778) -> 1.000000:(s' = 855) ;
[] (s = 778) -> 1.000000:(s' = 856) ;
[] (s = 779) -> 1.000000:(s' = 857) ;
[] (s = 779) -> 1.000000:(s' = 858) ;
[] (s = 780) -> 1.000000:(s' = 859) ;
[] (s = 780) -> 1.000000:(s' = 860) ;
[] (s = 781) -> 1.000000:(s' = 861) ;
[] (s = 782) -> 1.000000:(s' = 862) ;
[] (s = 783) -> 1.000000:(s' = 863) ;
[] (s = 783) -> 1.000000:(s' = 864) ;
[] (s = 784) -> 1.000000:(s' = 865) ;
[] (s = 784) -> 1.000000:(s' = 866) ;
[] (s = 785) -> 1.000000:(s' = 867) ;
[] (s = 785) -> 1.000000:(s' = 868) ;
[] (s = 786) -> 1.000000:(s' = 869) ;
[] (s = 786) -> 1.000000:(s' = 870) ;
[] (s = 787) -> 1.000000:(s' = 871) ;
[] (s = 788) -> 1.000000:(s' = 872) ;
[] (s = 789) -> 1.000000:(s' = 873) ;
[] (s = 789) -> 1.000000:(s' = 874) ;
[] (s = 790) -> 1.000000:(s' = 875) ;
[] (s = 790) -> 1.000000:(s' = 876) ;
[] (s = 791) -> 1.000000:(s' = 877) ;
[] (s = 791) -> 1.000000:(s' = 878) ;
[] (s = 792) -> 1.000000:(s' = 879) ;
[] (s = 792) -> 1.000000:(s' = 880) ;
[] (s = 793) -> 1.000000:(s' = 881) ;
[] (s = 794) -> 1.000000:(s' = 882) ;
[] (s = 795) -> 1.000000:(s' = 883) ;
[] (s = 795) -> 1.000000:(s' = 884) ;
[] (s = 796) -> 1.000000:(s' = 885) ;
[] (s = 796) -> 1.000000:(s' = 886) ;
[] (s = 797) -> 1.000000:(s' = 887) ;
[] (s = 797) -> 1.000000:(s' = 888) ;
[] (s = 798) -> 1.000000:(s' = 889) ;
[] (s = 799) -> 1.000000:(s' = 890) ;
[] (s = 799) -> 1.000000:(s' = 891) ;
[] (s = 800) -> 1.000000:(s' = 892) ;
[] (s = 801) -> 1.000000:(s' = 893) ;
[] (s = 802) -> 1.000000:(s' = 894) ;
[] (s = 803) -> 1.000000:(s' = 895) ;
[] (s = 803) -> 1.000000:(s' = 896) ;
[] (s = 804) -> 1.000000:(s' = 897) ;
[] (s = 805) -> 1.000000:(s' = 898) ;
[] (s = 805) -> 1.000000:(s' = 899) ;
[] (s = 806) -> 1.000000:(s' = 900) ;
[] (s = 807) -> 1.000000:(s' = 901) ;
[] (s = 807) -> 1.000000:(s' = 902) ;
[] (s = 808) -> 1.000000:(s' = 903) ;
[] (s = 809) -> 1.000000:(s' = 890) ;
[] (s = 809) -> 1.000000:(s' = 891) ;
[] (s = 810) -> 1.000000:(s' = 904) ;
[] (s = 811) -> 1.000000:(s' = 905) ;
[] (s = 812) -> 1.000000:(s' = 906) ;
[] (s = 813) -> 1.000000:(s' = 907) ;
[] (s = 813) -> 1.000000:(s' = 908) ;
[] (s = 814) -> 1.000000:(s' = 909) ;
[] (s = 815) -> 1.000000:(s' = 898) ;
[] (s = 815) -> 1.000000:(s' = 899) ;
[] (s = 816) -> 1.000000:(s' = 910) ;
[] (s = 817) -> 1.000000:(s' = 901) ;
[] (s = 817) -> 1.000000:(s' = 902) ;
[] (s = 818) -> 1.000000:(s' = 911) ;
[] (s = 819) -> 1.000000:(s' = 912) ;
[] (s = 819) -> 1.000000:(s' = 913) ;
[] (s = 820) -> 1.000000:(s' = 914) ;
[] (s = 821) -> 1.000000:(s' = 915) ;
[] (s = 822) -> 1.000000:(s' = 916) ;
[] (s = 823) -> 1.000000:(s' = 907) ;
[] (s = 823) -> 1.000000:(s' = 908) ;
[] (s = 824) -> 1.000000:(s' = 917) ;
[] (s = 825) -> 1.000000:(s' = 918) ;
[] (s = 825) -> 1.000000:(s' = 919) ;
[] (s = 826) -> 1.000000:(s' = 920) ;
[] (s = 827) -> 1.000000:(s' = 921) ;
[] (s = 827) -> 1.000000:(s' = 922) ;
[] (s = 828) -> 1.000000:(s' = 923) ;
[] (s = 829) -> 1.000000:(s' = 924) ;
[] (s = 829) -> 1.000000:(s' = 925) ;
[] (s = 830) -> 1.000000:(s' = 926) ;
[] (s = 831) -> 1.000000:(s' = 927) ;
[] (s = 832) -> 1.000000:(s' = 928) ;
[] (s = 833) -> 1.000000:(s' = 929) ;
[] (s = 833) -> 1.000000:(s' = 930) ;
[] (s = 834) -> 1.000000:(s' = 931) ;
[] (s = 835) -> 1.000000:(s' = 932) ;
[] (s = 835) -> 1.000000:(s' = 933) ;
[] (s = 836) -> 1.000000:(s' = 934) ;
[] (s = 837) -> 1.000000:(s' = 935) ;
[] (s = 837) -> 1.000000:(s' = 936) ;
[] (s = 838) -> 1.000000:(s' = 937) ;
[] (s = 839) -> 1.000000:(s' = 924) ;
[] (s = 839) -> 1.000000:(s' = 925) ;
[] (s = 840) -> 1.000000:(s' = 938) ;
[] (s = 841) -> 1.000000:(s' = 939) ;
[] (s = 842) -> 1.000000:(s' = 940) ;
[] (s = 843) -> 1.000000:(s' = 941) ;
[] (s = 843) -> 1.000000:(s' = 942) ;
[] (s = 844) -> 1.000000:(s' = 943) ;
[] (s = 845) -> 1.000000:(s' = 932) ;
[] (s = 845) -> 1.000000:(s' = 933) ;
[] (s = 846) -> 1.000000:(s' = 944) ;
[] (s = 847) -> 1.000000:(s' = 935) ;
[] (s = 847) -> 1.000000:(s' = 936) ;
[] (s = 848) -> 1.000000:(s' = 945) ;
[] (s = 849) -> 1.000000:(s' = 946) ;
[] (s = 849) -> 1.000000:(s' = 947) ;
[] (s = 850) -> 1.000000:(s' = 948) ;
[] (s = 851) -> 1.000000:(s' = 949) ;
[] (s = 852) -> 1.000000:(s' = 950) ;
[] (s = 853) -> 1.000000:(s' = 941) ;
[] (s = 853) -> 1.000000:(s' = 942) ;
[] (s = 854) -> 1.000000:(s' = 951) ;
[] (s = 855) -> 1.000000:(s' = 952) ;
[] (s = 855) -> 1.000000:(s' = 953) ;
[] (s = 856) -> 1.000000:(s' = 954) ;
[] (s = 857) -> 1.000000:(s' = 955) ;
[] (s = 857) -> 1.000000:(s' = 956) ;
[] (s = 858) -> 1.000000:(s' = 957) ;
[] (s = 859) -> 1.000000:(s' = 958) ;
[] (s = 859) -> 1.000000:(s' = 959) ;
[] (s = 860) -> 1.000000:(s' = 960) ;
[] (s = 861) -> 1.000000:(s' = 961) ;
[] (s = 862) -> 1.000000:(s' = 962) ;
[] (s = 863) -> 1.000000:(s' = 963) ;
[] (s = 863) -> 1.000000:(s' = 964) ;
[] (s = 864) -> 1.000000:(s' = 965) ;
[] (s = 865) -> 1.000000:(s' = 966) ;
[] (s = 865) -> 1.000000:(s' = 967) ;
[] (s = 866) -> 1.000000:(s' = 968) ;
[] (s = 867) -> 1.000000:(s' = 969) ;
[] (s = 867) -> 1.000000:(s' = 970) ;
[] (s = 868) -> 1.000000:(s' = 971) ;
[] (s = 869) -> 1.000000:(s' = 958) ;
[] (s = 869) -> 1.000000:(s' = 959) ;
[] (s = 870) -> 1.000000:(s' = 972) ;
[] (s = 871) -> 1.000000:(s' = 973) ;
[] (s = 872) -> 1.000000:(s' = 974) ;
[] (s = 873) -> 1.000000:(s' = 975) ;
[] (s = 873) -> 1.000000:(s' = 976) ;
[] (s = 874) -> 1.000000:(s' = 977) ;
[] (s = 875) -> 1.000000:(s' = 966) ;
[] (s = 875) -> 1.000000:(s' = 967) ;
[] (s = 876) -> 1.000000:(s' = 978) ;
[] (s = 877) -> 1.000000:(s' = 969) ;
[] (s = 877) -> 1.000000:(s' = 970) ;
[] (s = 878) -> 1.000000:(s' = 979) ;
[] (s = 879) -> 1.000000:(s' = 980) ;
[] (s = 879) -> 1.000000:(s' = 981) ;
[] (s = 880) -> 1.000000:(s' = 982) ;
[] (s = 881) -> 1.000000:(s' = 983) ;
[] (s = 882) -> 1.000000:(s' = 984) ;
[] (s = 883) -> 1.000000:(s' = 975) ;
[] (s = 883) -> 1.000000:(s' = 976) ;
[] (s = 884) -> 1.000000:(s' = 985) ;
[] (s = 885) -> 1.000000:(s' = 986) ;
[] (s = 885) -> 1.000000:(s' = 987) ;
[] (s = 886) -> 1.000000:(s' = 988) ;
[] (s = 887) -> 0.500000:(s' = 989) + 0.500000:(s' = 990);
[] (s = 887) -> 1.000000:(s' = 991) ;
[] (s = 888) -> 1.000000:(s' = 991) ;
[] (s = 888) -> 0.500000:(s' = 992) + 0.500000:(s' = 993);
[] (s = 889) -> 1.000000:(s' = 60) ;
[] (s = 890) -> 0.500000:(s' = 994) + 0.500000:(s' = 995);
[] (s = 890) -> 1.000000:(s' = 996) ;
[] (s = 891) -> 1.000000:(s' = 996) ;
[] (s = 891) -> 0.500000:(s' = 997) + 0.500000:(s' = 998);
[] (s = 892) -> 1.000000:(s' = 60) ;
[] (s = 893) -> 1.000000:(s' = 60) ;
[] (s = 893) -> 1.000000:(s' = 433) ;
[] (s = 894) -> 1.000000:(s' = 60) ;
[] (s = 894) -> 1.000000:(s' = 433) ;
[] (s = 895) -> 0.500000:(s' = 999) + 0.500000:(s' = 1000);
[] (s = 895) -> 1.000000:(s' = 1001) ;
[] (s = 896) -> 1.000000:(s' = 1001) ;
[] (s = 896) -> 0.500000:(s' = 1002) + 0.500000:(s' = 1003);
[] (s = 897) -> 1.000000:(s' = 60) ;
[] (s = 897) -> 1.000000:(s' = 433) ;
[] (s = 898) -> 0.500000:(s' = 1004) + 0.500000:(s' = 1005);
[] (s = 898) -> 1.000000:(s' = 1006) ;
[] (s = 899) -> 1.000000:(s' = 1006) ;
[] (s = 899) -> 0.500000:(s' = 1007) + 0.500000:(s' = 1008);
[] (s = 900) -> 1.000000:(s' = 60) ;
[] (s = 900) -> 1.000000:(s' = 433) ;
[] (s = 901) -> 0.500000:(s' = 1009) + 0.500000:(s' = 1010);
[] (s = 901) -> 1.000000:(s' = 1011) ;
[] (s = 902) -> 1.000000:(s' = 1011) ;
[] (s = 902) -> 0.500000:(s' = 1012) + 0.500000:(s' = 1013);
[] (s = 903) -> 1.000000:(s' = 60) ;
[] (s = 904) -> 1.000000:(s' = 60) ;
[] (s = 905) -> 1.000000:(s' = 60) ;
[] (s = 905) -> 1.000000:(s' = 433) ;
[] (s = 906) -> 1.000000:(s' = 60) ;
[] (s = 906) -> 1.000000:(s' = 433) ;
[] (s = 907) -> 0.500000:(s' = 1014) + 0.500000:(s' = 1015);
[] (s = 907) -> 1.000000:(s' = 1016) ;
[] (s = 908) -> 1.000000:(s' = 1016) ;
[] (s = 908) -> 0.500000:(s' = 1017) + 0.500000:(s' = 1018);
[] (s = 909) -> 1.000000:(s' = 60) ;
[] (s = 909) -> 1.000000:(s' = 433) ;
[] (s = 910) -> 1.000000:(s' = 60) ;
[] (s = 910) -> 1.000000:(s' = 433) ;
[] (s = 911) -> 1.000000:(s' = 60) ;
[] (s = 912) -> 0.500000:(s' = 1019) + 0.500000:(s' = 1020);
[] (s = 912) -> 1.000000:(s' = 1021) ;
[] (s = 913) -> 1.000000:(s' = 1021) ;
[] (s = 913) -> 0.500000:(s' = 1022) + 0.500000:(s' = 1023);
[] (s = 914) -> 1.000000:(s' = 60) ;
[] (s = 915) -> 1.000000:(s' = 60) ;
[] (s = 915) -> 1.000000:(s' = 433) ;
[] (s = 916) -> 1.000000:(s' = 60) ;
[] (s = 916) -> 1.000000:(s' = 433) ;
[] (s = 917) -> 1.000000:(s' = 60) ;
[] (s = 917) -> 1.000000:(s' = 433) ;
[] (s = 918) -> 0.500000:(s' = 1024) + 0.500000:(s' = 1025);
[] (s = 918) -> 1.000000:(s' = 1026) ;
[] (s = 919) -> 1.000000:(s' = 1026) ;
[] (s = 919) -> 0.500000:(s' = 1027) + 0.500000:(s' = 1028);
[] (s = 920) -> 1.000000:(s' = 60) ;
[] (s = 920) -> 1.000000:(s' = 433) ;
[] (s = 921) -> 0.500000:(s' = 1029) + 0.500000:(s' = 1030);
[] (s = 921) -> 1.000000:(s' = 1001) ;
[] (s = 922) -> 1.000000:(s' = 1001) ;
[] (s = 922) -> 0.500000:(s' = 1031) + 0.500000:(s' = 1032);
[] (s = 923) -> 1.000000:(s' = 60) ;
[] (s = 923) -> 1.000000:(s' = 433) ;
[] (s = 924) -> 0.500000:(s' = 1033) + 0.500000:(s' = 1034);
[] (s = 924) -> 1.000000:(s' = 1035) ;
[] (s = 925) -> 1.000000:(s' = 1035) ;
[] (s = 925) -> 0.500000:(s' = 1036) + 0.500000:(s' = 1037);
[] (s = 926) -> 1.000000:(s' = 60) ;
[] (s = 926) -> 1.000000:(s' = 433) ;
[] (s = 927) -> 1.000000:(s' = 60) ;
[] (s = 927) -> 1.000000:(s' = 433) ;
[] (s = 928) -> 1.000000:(s' = 60) ;
[] (s = 928) -> 1.000000:(s' = 433) ;
[] (s = 929) -> 0.500000:(s' = 1038) + 0.500000:(s' = 1039);
[] (s = 929) -> 1.000000:(s' = 1040) ;
[] (s = 930) -> 1.000000:(s' = 1040) ;
[] (s = 930) -> 0.500000:(s' = 1041) + 0.500000:(s' = 1042);
[] (s = 931) -> 1.000000:(s' = 60) ;
[] (s = 931) -> 1.000000:(s' = 433) ;
[] (s = 932) -> 0.500000:(s' = 1043) + 0.500000:(s' = 1044);
[] (s = 932) -> 1.000000:(s' = 1045) ;
[] (s = 933) -> 1.000000:(s' = 1045) ;
[] (s = 933) -> 0.500000:(s' = 1046) + 0.500000:(s' = 1047);
[] (s = 934) -> 1.000000:(s' = 60) ;
[] (s = 934) -> 1.000000:(s' = 433) ;
[] (s = 935) -> 0.500000:(s' = 1048) + 0.500000:(s' = 1049);
[] (s = 935) -> 1.000000:(s' = 1050) ;
[] (s = 936) -> 1.000000:(s' = 1050) ;
[] (s = 936) -> 0.500000:(s' = 1051) + 0.500000:(s' = 1052);
[] (s = 937) -> 1.000000:(s' = 60) ;
[] (s = 937) -> 1.000000:(s' = 433) ;
[] (s = 938) -> 1.000000:(s' = 60) ;
[] (s = 938) -> 1.000000:(s' = 433) ;
[] (s = 939) -> 1.000000:(s' = 60) ;
[] (s = 939) -> 1.000000:(s' = 433) ;
[] (s = 940) -> 1.000000:(s' = 60) ;
[] (s = 940) -> 1.000000:(s' = 433) ;
[] (s = 941) -> 0.500000:(s' = 1053) + 0.500000:(s' = 1054);
[] (s = 941) -> 1.000000:(s' = 1055) ;
[] (s = 942) -> 1.000000:(s' = 1055) ;
[] (s = 942) -> 0.500000:(s' = 1056) + 0.500000:(s' = 1057);
[] (s = 943) -> 1.000000:(s' = 60) ;
[] (s = 943) -> 1.000000:(s' = 433) ;
[] (s = 944) -> 1.000000:(s' = 60) ;
[] (s = 944) -> 1.000000:(s' = 433) ;
[] (s = 945) -> 1.000000:(s' = 60) ;
[] (s = 945) -> 1.000000:(s' = 433) ;
[] (s = 946) -> 0.500000:(s' = 1058) + 0.500000:(s' = 1059);
[] (s = 946) -> 1.000000:(s' = 1026) ;
[] (s = 947) -> 1.000000:(s' = 1026) ;
[] (s = 947) -> 0.500000:(s' = 1060) + 0.500000:(s' = 1061);
[] (s = 948) -> 1.000000:(s' = 60) ;
[] (s = 948) -> 1.000000:(s' = 433) ;
[] (s = 949) -> 1.000000:(s' = 60) ;
[] (s = 949) -> 1.000000:(s' = 433) ;
[] (s = 950) -> 1.000000:(s' = 60) ;
[] (s = 950) -> 1.000000:(s' = 433) ;
[] (s = 951) -> 1.000000:(s' = 60) ;
[] (s = 951) -> 1.000000:(s' = 433) ;
[] (s = 952) -> 0.500000:(s' = 1062) + 0.500000:(s' = 1063);
[] (s = 952) -> 1.000000:(s' = 1064) ;
[] (s = 953) -> 1.000000:(s' = 1064) ;
[] (s = 953) -> 0.500000:(s' = 1065) + 0.500000:(s' = 1066);
[] (s = 954) -> 1.000000:(s' = 60) ;
[] (s = 954) -> 1.000000:(s' = 433) ;
[] (s = 955) -> 0.500000:(s' = 1067) + 0.500000:(s' = 1068);
[] (s = 955) -> 1.000000:(s' = 1040) ;
[] (s = 956) -> 1.000000:(s' = 1040) ;
[] (s = 956) -> 0.500000:(s' = 1069) + 0.500000:(s' = 1070);
[] (s = 957) -> 1.000000:(s' = 60) ;
[] (s = 957) -> 1.000000:(s' = 433) ;
[] (s = 958) -> 0.500000:(s' = 1071) + 0.500000:(s' = 1072);
[] (s = 958) -> 1.000000:(s' = 1073) ;
[] (s = 959) -> 1.000000:(s' = 1073) ;
[] (s = 959) -> 0.500000:(s' = 1074) + 0.500000:(s' = 1075);
[] (s = 960) -> 1.000000:(s' = 60) ;
[] (s = 960) -> 1.000000:(s' = 433) ;
[] (s = 961) -> 1.000000:(s' = 433) ;
[] (s = 962) -> 1.000000:(s' = 433) ;
[] (s = 963) -> 0.500000:(s' = 1076) + 0.500000:(s' = 1077);
[] (s = 963) -> 1.000000:(s' = 1078) ;
[] (s = 964) -> 1.000000:(s' = 1078) ;
[] (s = 964) -> 0.500000:(s' = 1079) + 0.500000:(s' = 1080);
[] (s = 965) -> 1.000000:(s' = 433) ;
[] (s = 966) -> 0.500000:(s' = 1081) + 0.500000:(s' = 1082);
[] (s = 966) -> 1.000000:(s' = 1083) ;
[] (s = 967) -> 1.000000:(s' = 1083) ;
[] (s = 967) -> 0.500000:(s' = 1084) + 0.500000:(s' = 1085);
[] (s = 968) -> 1.000000:(s' = 433) ;
[] (s = 969) -> 0.500000:(s' = 1086) + 0.500000:(s' = 1087);
[] (s = 969) -> 1.000000:(s' = 1088) ;
[] (s = 970) -> 1.000000:(s' = 1088) ;
[] (s = 970) -> 0.500000:(s' = 1089) + 0.500000:(s' = 1090);
[] (s = 971) -> 1.000000:(s' = 60) ;
[] (s = 971) -> 1.000000:(s' = 433) ;
[] (s = 972) -> 1.000000:(s' = 60) ;
[] (s = 972) -> 1.000000:(s' = 433) ;
[] (s = 973) -> 1.000000:(s' = 433) ;
[] (s = 974) -> 1.000000:(s' = 433) ;
[] (s = 975) -> 0.500000:(s' = 1091) + 0.500000:(s' = 1092);
[] (s = 975) -> 1.000000:(s' = 1093) ;
[] (s = 976) -> 1.000000:(s' = 1093) ;
[] (s = 976) -> 0.500000:(s' = 1094) + 0.500000:(s' = 1095);
[] (s = 977) -> 1.000000:(s' = 433) ;
[] (s = 978) -> 1.000000:(s' = 433) ;
[] (s = 979) -> 1.000000:(s' = 60) ;
[] (s = 979) -> 1.000000:(s' = 433) ;
[] (s = 980) -> 0.500000:(s' = 1096) + 0.500000:(s' = 1097);
[] (s = 980) -> 1.000000:(s' = 1064) ;
[] (s = 981) -> 1.000000:(s' = 1064) ;
[] (s = 981) -> 0.500000:(s' = 1098) + 0.500000:(s' = 1099);
[] (s = 982) -> 1.000000:(s' = 60) ;
[] (s = 982) -> 1.000000:(s' = 433) ;
[] (s = 983) -> 1.000000:(s' = 433) ;
[] (s = 984) -> 1.000000:(s' = 433) ;
[] (s = 985) -> 1.000000:(s' = 433) ;
[] (s = 986) -> 0.500000:(s' = 1100) + 0.500000:(s' = 1101);
[] (s = 986) -> 1.000000:(s' = 1102) ;
[] (s = 987) -> 1.000000:(s' = 1102) ;
[] (s = 987) -> 0.500000:(s' = 1103) + 0.500000:(s' = 1104);
[] (s = 988) -> 1.000000:(s' = 433) ;
[] (s = 989) -> 1.000000:(s' = 1105) ;
[] (s = 990) -> 1.000000:(s' = 1106) ;
[] (s = 991) -> 0.500000:(s' = 1107) + 0.500000:(s' = 1108);
[] (s = 991) -> 0.500000:(s' = 1109) + 0.500000:(s' = 1110);
[] (s = 992) -> 1.000000:(s' = 1111) ;
[] (s = 993) -> 1.000000:(s' = 1112) ;
[] (s = 994) -> 1.000000:(s' = 1113) ;
[] (s = 995) -> 1.000000:(s' = 1114) ;
[] (s = 996) -> 0.500000:(s' = 1107) + 0.500000:(s' = 1108);
[] (s = 996) -> 0.500000:(s' = 1109) + 0.500000:(s' = 1110);
[] (s = 997) -> 1.000000:(s' = 1115) ;
[] (s = 998) -> 1.000000:(s' = 1116) ;
[] (s = 999) -> 1.000000:(s' = 1117) ;
[] (s = 1000) -> 1.000000:(s' = 1118) ;
[] (s = 1001) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1001) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1002) -> 1.000000:(s' = 1123) ;
[] (s = 1003) -> 1.000000:(s' = 1124) ;
[] (s = 1004) -> 1.000000:(s' = 1125) ;
[] (s = 1005) -> 1.000000:(s' = 1126) ;
[] (s = 1006) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1006) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1007) -> 1.000000:(s' = 1127) ;
[] (s = 1008) -> 1.000000:(s' = 1128) ;
[] (s = 1009) -> 1.000000:(s' = 1129) ;
[] (s = 1010) -> 1.000000:(s' = 1130) ;
[] (s = 1011) -> 0.500000:(s' = 1107) + 0.500000:(s' = 1108);
[] (s = 1011) -> 0.500000:(s' = 1109) + 0.500000:(s' = 1110);
[] (s = 1012) -> 1.000000:(s' = 1131) ;
[] (s = 1013) -> 1.000000:(s' = 1132) ;
[] (s = 1014) -> 1.000000:(s' = 1133) ;
[] (s = 1015) -> 1.000000:(s' = 1134) ;
[] (s = 1016) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1016) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1017) -> 1.000000:(s' = 1135) ;
[] (s = 1018) -> 1.000000:(s' = 1136) ;
[] (s = 1019) -> 1.000000:(s' = 1137) ;
[] (s = 1020) -> 1.000000:(s' = 1138) ;
[] (s = 1021) -> 0.500000:(s' = 1107) + 0.500000:(s' = 1108);
[] (s = 1021) -> 0.500000:(s' = 1109) + 0.500000:(s' = 1110);
[] (s = 1022) -> 1.000000:(s' = 1139) ;
[] (s = 1023) -> 1.000000:(s' = 1140) ;
[] (s = 1024) -> 1.000000:(s' = 1141) ;
[] (s = 1025) -> 1.000000:(s' = 1142) ;
[] (s = 1026) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1026) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1027) -> 1.000000:(s' = 1143) ;
[] (s = 1028) -> 1.000000:(s' = 1144) ;
[] (s = 1029) -> 1.000000:(s' = 1117) ;
[] (s = 1030) -> 1.000000:(s' = 1118) ;
[] (s = 1031) -> 1.000000:(s' = 1123) ;
[] (s = 1032) -> 1.000000:(s' = 1124) ;
[] (s = 1033) -> 1.000000:(s' = 1145) ;
[] (s = 1034) -> 1.000000:(s' = 1146) ;
[] (s = 1035) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1035) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1036) -> 1.000000:(s' = 1147) ;
[] (s = 1037) -> 1.000000:(s' = 1148) ;
[] (s = 1038) -> 1.000000:(s' = 1149) ;
[] (s = 1039) -> 1.000000:(s' = 1150) ;
[] (s = 1040) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1040) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1041) -> 1.000000:(s' = 1155) ;
[] (s = 1042) -> 1.000000:(s' = 1156) ;
[] (s = 1043) -> 1.000000:(s' = 1157) ;
[] (s = 1044) -> 1.000000:(s' = 1158) ;
[] (s = 1045) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1045) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1046) -> 1.000000:(s' = 1159) ;
[] (s = 1047) -> 1.000000:(s' = 1160) ;
[] (s = 1048) -> 1.000000:(s' = 1161) ;
[] (s = 1049) -> 1.000000:(s' = 1162) ;
[] (s = 1050) -> 0.500000:(s' = 1119) + 0.500000:(s' = 1120);
[] (s = 1050) -> 0.500000:(s' = 1121) + 0.500000:(s' = 1122);
[] (s = 1051) -> 1.000000:(s' = 1163) ;
[] (s = 1052) -> 1.000000:(s' = 1164) ;
[] (s = 1053) -> 1.000000:(s' = 1165) ;
[] (s = 1054) -> 1.000000:(s' = 1166) ;
[] (s = 1055) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1055) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1056) -> 1.000000:(s' = 1167) ;
[] (s = 1057) -> 1.000000:(s' = 1168) ;
[] (s = 1058) -> 1.000000:(s' = 1141) ;
[] (s = 1059) -> 1.000000:(s' = 1142) ;
[] (s = 1060) -> 1.000000:(s' = 1143) ;
[] (s = 1061) -> 1.000000:(s' = 1144) ;
[] (s = 1062) -> 1.000000:(s' = 1169) ;
[] (s = 1063) -> 1.000000:(s' = 1170) ;
[] (s = 1064) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1064) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1065) -> 1.000000:(s' = 1171) ;
[] (s = 1066) -> 1.000000:(s' = 1172) ;
[] (s = 1067) -> 1.000000:(s' = 1149) ;
[] (s = 1068) -> 1.000000:(s' = 1150) ;
[] (s = 1069) -> 1.000000:(s' = 1155) ;
[] (s = 1070) -> 1.000000:(s' = 1156) ;
[] (s = 1071) -> 1.000000:(s' = 1173) ;
[] (s = 1072) -> 1.000000:(s' = 1174) ;
[] (s = 1073) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1073) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1074) -> 1.000000:(s' = 1175) ;
[] (s = 1075) -> 1.000000:(s' = 1176) ;
[] (s = 1076) -> 1.000000:(s' = 1177) ;
[] (s = 1077) -> 1.000000:(s' = 1178) ;
[] (s = 1078) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1078) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1079) -> 1.000000:(s' = 1183) ;
[] (s = 1080) -> 1.000000:(s' = 1184) ;
[] (s = 1081) -> 1.000000:(s' = 1185) ;
[] (s = 1082) -> 1.000000:(s' = 1186) ;
[] (s = 1083) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1083) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1084) -> 1.000000:(s' = 1187) ;
[] (s = 1085) -> 1.000000:(s' = 1188) ;
[] (s = 1086) -> 1.000000:(s' = 1189) ;
[] (s = 1087) -> 1.000000:(s' = 1190) ;
[] (s = 1088) -> 0.500000:(s' = 1151) + 0.500000:(s' = 1152);
[] (s = 1088) -> 0.500000:(s' = 1153) + 0.500000:(s' = 1154);
[] (s = 1089) -> 1.000000:(s' = 1191) ;
[] (s = 1090) -> 1.000000:(s' = 1192) ;
[] (s = 1091) -> 1.000000:(s' = 1193) ;
[] (s = 1092) -> 1.000000:(s' = 1194) ;
[] (s = 1093) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1093) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1094) -> 1.000000:(s' = 1195) ;
[] (s = 1095) -> 1.000000:(s' = 1196) ;
[] (s = 1096) -> 1.000000:(s' = 1169) ;
[] (s = 1097) -> 1.000000:(s' = 1170) ;
[] (s = 1098) -> 1.000000:(s' = 1171) ;
[] (s = 1099) -> 1.000000:(s' = 1172) ;
[] (s = 1100) -> 1.000000:(s' = 1197) ;
[] (s = 1101) -> 1.000000:(s' = 1198) ;
[] (s = 1102) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1102) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1103) -> 1.000000:(s' = 1199) ;
[] (s = 1104) -> 1.000000:(s' = 1200) ;
[] (s = 1105) -> 0.500000:(s' = 1201) + 0.500000:(s' = 1202);
[] (s = 1105) -> 1.000000:(s' = 1203) ;
[] (s = 1106) -> 0.500000:(s' = 1204) + 0.500000:(s' = 1205);
[] (s = 1106) -> 1.000000:(s' = 1206) ;
[] (s = 1107) -> 0.500000:(s' = 1207) + 0.500000:(s' = 1208);
[] (s = 1107) -> 1.000000:(s' = 1209) ;
[] (s = 1108) -> 0.500000:(s' = 1210) + 0.500000:(s' = 1211);
[] (s = 1108) -> 1.000000:(s' = 1212) ;
[] (s = 1109) -> 1.000000:(s' = 1213) ;
[] (s = 1109) -> 0.500000:(s' = 1207) + 0.500000:(s' = 1210);
[] (s = 1110) -> 1.000000:(s' = 1214) ;
[] (s = 1110) -> 0.500000:(s' = 1208) + 0.500000:(s' = 1211);
[] (s = 1111) -> 1.000000:(s' = 1215) ;
[] (s = 1111) -> 0.500000:(s' = 1216) + 0.500000:(s' = 1217);
[] (s = 1112) -> 1.000000:(s' = 1218) ;
[] (s = 1112) -> 0.500000:(s' = 1219) + 0.500000:(s' = 1220);
[] (s = 1113) -> 0.500000:(s' = 1201) + 0.500000:(s' = 1202);
[] (s = 1113) -> 1.000000:(s' = 1221) ;
[] (s = 1114) -> 0.500000:(s' = 1204) + 0.500000:(s' = 1205);
[] (s = 1114) -> 1.000000:(s' = 1222) ;
[] (s = 1115) -> 1.000000:(s' = 1223) ;
[] (s = 1115) -> 0.500000:(s' = 1216) + 0.500000:(s' = 1217);
[] (s = 1116) -> 1.000000:(s' = 1224) ;
[] (s = 1116) -> 0.500000:(s' = 1219) + 0.500000:(s' = 1220);
[] (s = 1117) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1117) -> 1.000000:(s' = 1227) ;
[] (s = 1118) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1118) -> 1.000000:(s' = 1230) ;
[] (s = 1119) -> 0.500000:(s' = 1231) + 0.500000:(s' = 1232);
[] (s = 1119) -> 1.000000:(s' = 1233) ;
[] (s = 1120) -> 0.500000:(s' = 1234) + 0.500000:(s' = 1235);
[] (s = 1120) -> 1.000000:(s' = 1236) ;
[] (s = 1121) -> 1.000000:(s' = 1237) ;
[] (s = 1121) -> 0.500000:(s' = 1231) + 0.500000:(s' = 1234);
[] (s = 1122) -> 1.000000:(s' = 1238) ;
[] (s = 1122) -> 0.500000:(s' = 1232) + 0.500000:(s' = 1235);
[] (s = 1123) -> 1.000000:(s' = 1239) ;
[] (s = 1123) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1124) -> 1.000000:(s' = 1242) ;
[] (s = 1124) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1125) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1125) -> 1.000000:(s' = 1245) ;
[] (s = 1126) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1126) -> 1.000000:(s' = 1246) ;
[] (s = 1127) -> 1.000000:(s' = 1247) ;
[] (s = 1127) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1128) -> 1.000000:(s' = 1248) ;
[] (s = 1128) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1129) -> 0.500000:(s' = 1201) + 0.500000:(s' = 1202);
[] (s = 1129) -> 1.000000:(s' = 1249) ;
[] (s = 1130) -> 0.500000:(s' = 1204) + 0.500000:(s' = 1205);
[] (s = 1130) -> 1.000000:(s' = 1250) ;
[] (s = 1131) -> 1.000000:(s' = 1251) ;
[] (s = 1131) -> 0.500000:(s' = 1216) + 0.500000:(s' = 1217);
[] (s = 1132) -> 1.000000:(s' = 1252) ;
[] (s = 1132) -> 0.500000:(s' = 1219) + 0.500000:(s' = 1220);
[] (s = 1133) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1133) -> 1.000000:(s' = 1253) ;
[] (s = 1134) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1134) -> 1.000000:(s' = 1254) ;
[] (s = 1135) -> 1.000000:(s' = 1255) ;
[] (s = 1135) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1136) -> 1.000000:(s' = 1256) ;
[] (s = 1136) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1137) -> 0.500000:(s' = 1201) + 0.500000:(s' = 1202);
[] (s = 1137) -> 1.000000:(s' = 1257) ;
[] (s = 1138) -> 0.500000:(s' = 1204) + 0.500000:(s' = 1205);
[] (s = 1138) -> 1.000000:(s' = 1258) ;
[] (s = 1139) -> 1.000000:(s' = 1259) ;
[] (s = 1139) -> 0.500000:(s' = 1216) + 0.500000:(s' = 1217);
[] (s = 1140) -> 1.000000:(s' = 1260) ;
[] (s = 1140) -> 0.500000:(s' = 1219) + 0.500000:(s' = 1220);
[] (s = 1141) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1141) -> 1.000000:(s' = 1261) ;
[] (s = 1142) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1142) -> 1.000000:(s' = 1262) ;
[] (s = 1143) -> 1.000000:(s' = 1263) ;
[] (s = 1143) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1144) -> 1.000000:(s' = 1264) ;
[] (s = 1144) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1145) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1145) -> 1.000000:(s' = 1265) ;
[] (s = 1146) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1146) -> 1.000000:(s' = 1266) ;
[] (s = 1147) -> 1.000000:(s' = 1267) ;
[] (s = 1147) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1148) -> 1.000000:(s' = 1268) ;
[] (s = 1148) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1149) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1149) -> 1.000000:(s' = 1271) ;
[] (s = 1150) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1150) -> 1.000000:(s' = 1274) ;
[] (s = 1151) -> 0.500000:(s' = 1275) + 0.500000:(s' = 1276);
[] (s = 1151) -> 1.000000:(s' = 1277) ;
[] (s = 1152) -> 0.500000:(s' = 1278) + 0.500000:(s' = 1279);
[] (s = 1152) -> 1.000000:(s' = 1280) ;
[] (s = 1153) -> 1.000000:(s' = 1281) ;
[] (s = 1153) -> 0.500000:(s' = 1275) + 0.500000:(s' = 1278);
[] (s = 1154) -> 1.000000:(s' = 1282) ;
[] (s = 1154) -> 0.500000:(s' = 1276) + 0.500000:(s' = 1279);
[] (s = 1155) -> 1.000000:(s' = 1283) ;
[] (s = 1155) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1156) -> 1.000000:(s' = 1286) ;
[] (s = 1156) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1157) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1157) -> 1.000000:(s' = 1289) ;
[] (s = 1158) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1158) -> 1.000000:(s' = 1290) ;
[] (s = 1159) -> 1.000000:(s' = 1291) ;
[] (s = 1159) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1160) -> 1.000000:(s' = 1292) ;
[] (s = 1160) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1161) -> 0.500000:(s' = 1225) + 0.500000:(s' = 1226);
[] (s = 1161) -> 1.000000:(s' = 1293) ;
[] (s = 1162) -> 0.500000:(s' = 1228) + 0.500000:(s' = 1229);
[] (s = 1162) -> 1.000000:(s' = 1294) ;
[] (s = 1163) -> 1.000000:(s' = 1295) ;
[] (s = 1163) -> 0.500000:(s' = 1240) + 0.500000:(s' = 1241);
[] (s = 1164) -> 1.000000:(s' = 1296) ;
[] (s = 1164) -> 0.500000:(s' = 1243) + 0.500000:(s' = 1244);
[] (s = 1165) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1165) -> 1.000000:(s' = 1297) ;
[] (s = 1166) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1166) -> 1.000000:(s' = 1298) ;
[] (s = 1167) -> 1.000000:(s' = 1299) ;
[] (s = 1167) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1168) -> 1.000000:(s' = 1300) ;
[] (s = 1168) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1169) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1169) -> 1.000000:(s' = 1301) ;
[] (s = 1170) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1170) -> 1.000000:(s' = 1302) ;
[] (s = 1171) -> 1.000000:(s' = 1303) ;
[] (s = 1171) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1172) -> 1.000000:(s' = 1304) ;
[] (s = 1172) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1173) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1173) -> 1.000000:(s' = 1305) ;
[] (s = 1174) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1174) -> 1.000000:(s' = 1306) ;
[] (s = 1175) -> 1.000000:(s' = 1307) ;
[] (s = 1175) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1176) -> 1.000000:(s' = 1308) ;
[] (s = 1176) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1177) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 1177) -> 1.000000:(s' = 1311) ;
[] (s = 1178) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 1178) -> 1.000000:(s' = 1314) ;
[] (s = 1179) -> 0.500000:(s' = 1315) + 0.500000:(s' = 1316);
[] (s = 1179) -> 1.000000:(s' = 1317) ;
[] (s = 1180) -> 0.500000:(s' = 1318) + 0.500000:(s' = 1319);
[] (s = 1180) -> 1.000000:(s' = 1320) ;
[] (s = 1181) -> 1.000000:(s' = 1321) ;
[] (s = 1181) -> 0.500000:(s' = 1315) + 0.500000:(s' = 1318);
[] (s = 1182) -> 1.000000:(s' = 1322) ;
[] (s = 1182) -> 0.500000:(s' = 1316) + 0.500000:(s' = 1319);
[] (s = 1183) -> 1.000000:(s' = 1323) ;
[] (s = 1183) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 1184) -> 1.000000:(s' = 1326) ;
[] (s = 1184) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 1185) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 1185) -> 1.000000:(s' = 1329) ;
[] (s = 1186) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 1186) -> 1.000000:(s' = 1330) ;
[] (s = 1187) -> 1.000000:(s' = 1331) ;
[] (s = 1187) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 1188) -> 1.000000:(s' = 1332) ;
[] (s = 1188) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 1189) -> 0.500000:(s' = 1269) + 0.500000:(s' = 1270);
[] (s = 1189) -> 1.000000:(s' = 1333) ;
[] (s = 1190) -> 0.500000:(s' = 1272) + 0.500000:(s' = 1273);
[] (s = 1190) -> 1.000000:(s' = 1334) ;
[] (s = 1191) -> 1.000000:(s' = 1335) ;
[] (s = 1191) -> 0.500000:(s' = 1284) + 0.500000:(s' = 1285);
[] (s = 1192) -> 1.000000:(s' = 1336) ;
[] (s = 1192) -> 0.500000:(s' = 1287) + 0.500000:(s' = 1288);
[] (s = 1193) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 1193) -> 1.000000:(s' = 1337) ;
[] (s = 1194) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 1194) -> 1.000000:(s' = 1338) ;
[] (s = 1195) -> 1.000000:(s' = 1339) ;
[] (s = 1195) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 1196) -> 1.000000:(s' = 1340) ;
[] (s = 1196) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 1197) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 1197) -> 1.000000:(s' = 1341) ;
[] (s = 1198) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 1198) -> 1.000000:(s' = 1342) ;
[] (s = 1199) -> 1.000000:(s' = 1343) ;
[] (s = 1199) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 1200) -> 1.000000:(s' = 1344) ;
[] (s = 1200) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 1201) -> 1.000000:(s' = 1345) ;
[] (s = 1201) -> 1.000000:(s' = 1346) ;
[] (s = 1202) -> 1.000000:(s' = 1347) ;
[] (s = 1202) -> 1.000000:(s' = 1348) ;
[] (s = 1203) -> 0.500000:(s' = 1346) + 0.500000:(s' = 1348);
[] (s = 1204) -> 1.000000:(s' = 1349) ;
[] (s = 1204) -> 1.000000:(s' = 1350) ;
[] (s = 1205) -> 1.000000:(s' = 1351) ;
[] (s = 1205) -> 1.000000:(s' = 1352) ;
[] (s = 1206) -> 0.500000:(s' = 1350) + 0.500000:(s' = 1352);
[] (s = 1207) -> 1.000000:(s' = 1353) ;
[] (s = 1207) -> 1.000000:(s' = 1354) ;
[] (s = 1208) -> 1.000000:(s' = 1355) ;
[] (s = 1208) -> 1.000000:(s' = 1356) ;
[] (s = 1209) -> 0.500000:(s' = 1354) + 0.500000:(s' = 1356);
[] (s = 1210) -> 1.000000:(s' = 1357) ;
[] (s = 1210) -> 1.000000:(s' = 1358) ;
[] (s = 1211) -> 1.000000:(s' = 1359) ;
[] (s = 1211) -> 1.000000:(s' = 1360) ;
[] (s = 1212) -> 0.500000:(s' = 1358) + 0.500000:(s' = 1360);
[] (s = 1213) -> 0.500000:(s' = 1353) + 0.500000:(s' = 1357);
[] (s = 1214) -> 0.500000:(s' = 1355) + 0.500000:(s' = 1359);
[] (s = 1215) -> 0.500000:(s' = 1361) + 0.500000:(s' = 1362);
[] (s = 1216) -> 1.000000:(s' = 1361) ;
[] (s = 1216) -> 1.000000:(s' = 1363) ;
[] (s = 1217) -> 1.000000:(s' = 1362) ;
[] (s = 1217) -> 1.000000:(s' = 1364) ;
[] (s = 1218) -> 0.500000:(s' = 1365) + 0.500000:(s' = 1366);
[] (s = 1219) -> 1.000000:(s' = 1365) ;
[] (s = 1219) -> 1.000000:(s' = 1367) ;
[] (s = 1220) -> 1.000000:(s' = 1366) ;
[] (s = 1220) -> 1.000000:(s' = 1368) ;
[] (s = 1221) -> 0.500000:(s' = 1346) + 0.500000:(s' = 1348);
[] (s = 1222) -> 0.500000:(s' = 1350) + 0.500000:(s' = 1352);
[] (s = 1223) -> 0.500000:(s' = 1361) + 0.500000:(s' = 1362);
[] (s = 1224) -> 0.500000:(s' = 1365) + 0.500000:(s' = 1366);
[] (s = 1225) -> 1.000000:(s' = 1369) ;
[] (s = 1225) -> 1.000000:(s' = 1370) ;
[] (s = 1226) -> 1.000000:(s' = 1371) ;
[] (s = 1226) -> 1.000000:(s' = 1372) ;
[] (s = 1227) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1228) -> 1.000000:(s' = 1373) ;
[] (s = 1228) -> 1.000000:(s' = 1374) ;
[] (s = 1229) -> 1.000000:(s' = 1375) ;
[] (s = 1229) -> 1.000000:(s' = 1376) ;
[] (s = 1230) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1231) -> 1.000000:(s' = 1377) ;
[] (s = 1231) -> 1.000000:(s' = 1378) ;
[] (s = 1232) -> 1.000000:(s' = 1379) ;
[] (s = 1232) -> 1.000000:(s' = 1380) ;
[] (s = 1233) -> 0.500000:(s' = 1378) + 0.500000:(s' = 1380);
[] (s = 1234) -> 1.000000:(s' = 1381) ;
[] (s = 1234) -> 1.000000:(s' = 1382) ;
[] (s = 1235) -> 1.000000:(s' = 1383) ;
[] (s = 1235) -> 1.000000:(s' = 1384) ;
[] (s = 1236) -> 0.500000:(s' = 1382) + 0.500000:(s' = 1384);
[] (s = 1237) -> 0.500000:(s' = 1377) + 0.500000:(s' = 1381);
[] (s = 1238) -> 0.500000:(s' = 1379) + 0.500000:(s' = 1383);
[] (s = 1239) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1240) -> 1.000000:(s' = 1385) ;
[] (s = 1240) -> 1.000000:(s' = 1387) ;
[] (s = 1241) -> 1.000000:(s' = 1386) ;
[] (s = 1241) -> 1.000000:(s' = 1388) ;
[] (s = 1242) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1243) -> 1.000000:(s' = 1389) ;
[] (s = 1243) -> 1.000000:(s' = 1391) ;
[] (s = 1244) -> 1.000000:(s' = 1390) ;
[] (s = 1244) -> 1.000000:(s' = 1392) ;
[] (s = 1245) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1246) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1247) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1248) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1249) -> 0.500000:(s' = 1346) + 0.500000:(s' = 1348);
[] (s = 1250) -> 0.500000:(s' = 1350) + 0.500000:(s' = 1352);
[] (s = 1251) -> 0.500000:(s' = 1361) + 0.500000:(s' = 1362);
[] (s = 1252) -> 0.500000:(s' = 1365) + 0.500000:(s' = 1366);
[] (s = 1253) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1254) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1255) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1256) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1257) -> 0.500000:(s' = 1346) + 0.500000:(s' = 1348);
[] (s = 1258) -> 0.500000:(s' = 1350) + 0.500000:(s' = 1352);
[] (s = 1259) -> 0.500000:(s' = 1361) + 0.500000:(s' = 1362);
[] (s = 1260) -> 0.500000:(s' = 1365) + 0.500000:(s' = 1366);
[] (s = 1261) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1262) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1263) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1264) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1265) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1266) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1267) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1268) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1269) -> 1.000000:(s' = 1393) ;
[] (s = 1269) -> 1.000000:(s' = 1394) ;
[] (s = 1270) -> 1.000000:(s' = 1395) ;
[] (s = 1270) -> 1.000000:(s' = 1396) ;
[] (s = 1271) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1272) -> 1.000000:(s' = 1397) ;
[] (s = 1272) -> 1.000000:(s' = 1398) ;
[] (s = 1273) -> 1.000000:(s' = 1399) ;
[] (s = 1273) -> 1.000000:(s' = 1400) ;
[] (s = 1274) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1275) -> 1.000000:(s' = 1401) ;
[] (s = 1275) -> 1.000000:(s' = 1402) ;
[] (s = 1276) -> 1.000000:(s' = 1403) ;
[] (s = 1276) -> 1.000000:(s' = 1404) ;
[] (s = 1277) -> 0.500000:(s' = 1402) + 0.500000:(s' = 1404);
[] (s = 1278) -> 1.000000:(s' = 1405) ;
[] (s = 1278) -> 1.000000:(s' = 1406) ;
[] (s = 1279) -> 1.000000:(s' = 1407) ;
[] (s = 1279) -> 1.000000:(s' = 1408) ;
[] (s = 1280) -> 0.500000:(s' = 1406) + 0.500000:(s' = 1408);
[] (s = 1281) -> 0.500000:(s' = 1401) + 0.500000:(s' = 1405);
[] (s = 1282) -> 0.500000:(s' = 1403) + 0.500000:(s' = 1407);
[] (s = 1283) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1284) -> 1.000000:(s' = 1409) ;
[] (s = 1284) -> 1.000000:(s' = 1411) ;
[] (s = 1285) -> 1.000000:(s' = 1410) ;
[] (s = 1285) -> 1.000000:(s' = 1412) ;
[] (s = 1286) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1287) -> 1.000000:(s' = 1413) ;
[] (s = 1287) -> 1.000000:(s' = 1415) ;
[] (s = 1288) -> 1.000000:(s' = 1414) ;
[] (s = 1288) -> 1.000000:(s' = 1416) ;
[] (s = 1289) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1290) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1291) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1292) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1293) -> 0.500000:(s' = 1370) + 0.500000:(s' = 1372);
[] (s = 1294) -> 0.500000:(s' = 1374) + 0.500000:(s' = 1376);
[] (s = 1295) -> 0.500000:(s' = 1385) + 0.500000:(s' = 1386);
[] (s = 1296) -> 0.500000:(s' = 1389) + 0.500000:(s' = 1390);
[] (s = 1297) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1298) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1299) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1300) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1301) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1302) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1303) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1304) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1305) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1306) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1307) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1308) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1309) -> 1.000000:(s' = 1417) ;
[] (s = 1309) -> 1.000000:(s' = 1418) ;
[] (s = 1310) -> 1.000000:(s' = 1419) ;
[] (s = 1310) -> 1.000000:(s' = 1420) ;
[] (s = 1311) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 1312) -> 1.000000:(s' = 1421) ;
[] (s = 1312) -> 1.000000:(s' = 1422) ;
[] (s = 1313) -> 1.000000:(s' = 1423) ;
[] (s = 1313) -> 1.000000:(s' = 1424) ;
[] (s = 1314) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 1315) -> 1.000000:(s' = 1425) ;
[] (s = 1315) -> 1.000000:(s' = 1426) ;
[] (s = 1316) -> 1.000000:(s' = 1427) ;
[] (s = 1316) -> 1.000000:(s' = 1428) ;
[] (s = 1317) -> 0.500000:(s' = 1426) + 0.500000:(s' = 1428);
[] (s = 1318) -> 1.000000:(s' = 1429) ;
[] (s = 1318) -> 1.000000:(s' = 1430) ;
[] (s = 1319) -> 1.000000:(s' = 1431) ;
[] (s = 1319) -> 1.000000:(s' = 1432) ;
[] (s = 1320) -> 0.500000:(s' = 1430) + 0.500000:(s' = 1432);
[] (s = 1321) -> 0.500000:(s' = 1425) + 0.500000:(s' = 1429);
[] (s = 1322) -> 0.500000:(s' = 1427) + 0.500000:(s' = 1431);
[] (s = 1323) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 1324) -> 1.000000:(s' = 1433) ;
[] (s = 1324) -> 1.000000:(s' = 1435) ;
[] (s = 1325) -> 1.000000:(s' = 1434) ;
[] (s = 1325) -> 1.000000:(s' = 1436) ;
[] (s = 1326) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 1327) -> 1.000000:(s' = 1437) ;
[] (s = 1327) -> 1.000000:(s' = 1439) ;
[] (s = 1328) -> 1.000000:(s' = 1438) ;
[] (s = 1328) -> 1.000000:(s' = 1440) ;
[] (s = 1329) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 1330) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 1331) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 1332) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 1333) -> 0.500000:(s' = 1394) + 0.500000:(s' = 1396);
[] (s = 1334) -> 0.500000:(s' = 1398) + 0.500000:(s' = 1400);
[] (s = 1335) -> 0.500000:(s' = 1409) + 0.500000:(s' = 1410);
[] (s = 1336) -> 0.500000:(s' = 1413) + 0.500000:(s' = 1414);
[] (s = 1337) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 1338) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 1339) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 1340) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 1341) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 1342) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 1343) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 1344) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 1345) -> 1.000000:(s' = 1441) ;
[] (s = 1346) -> 1.000000:(s' = 1441) ;
[] (s = 1347) -> 1.000000:(s' = 1442) ;
[] (s = 1348) -> 1.000000:(s' = 1442) ;
[] (s = 1349) -> 1.000000:(s' = 1443) ;
[] (s = 1350) -> 1.000000:(s' = 1443) ;
[] (s = 1351) -> 1.000000:(s' = 1444) ;
[] (s = 1352) -> 1.000000:(s' = 1444) ;
[] (s = 1353) -> 1.000000:(s' = 1445) ;
[] (s = 1354) -> 1.000000:(s' = 1445) ;
[] (s = 1355) -> 1.000000:(s' = 1446) ;
[] (s = 1356) -> 1.000000:(s' = 1446) ;
[] (s = 1357) -> 1.000000:(s' = 1447) ;
[] (s = 1358) -> 1.000000:(s' = 1447) ;
[] (s = 1359) -> 1.000000:(s' = 1448) ;
[] (s = 1360) -> 1.000000:(s' = 1448) ;
[] (s = 1361) -> 1.000000:(s' = 1449) ;
[] (s = 1362) -> 1.000000:(s' = 1450) ;
[] (s = 1363) -> 1.000000:(s' = 1449) ;
[] (s = 1364) -> 1.000000:(s' = 1450) ;
[] (s = 1365) -> 1.000000:(s' = 1451) ;
[] (s = 1366) -> 1.000000:(s' = 1452) ;
[] (s = 1367) -> 1.000000:(s' = 1451) ;
[] (s = 1368) -> 1.000000:(s' = 1452) ;
[] (s = 1369) -> 1.000000:(s' = 1453) ;
[] (s = 1370) -> 1.000000:(s' = 1453) ;
[] (s = 1371) -> 1.000000:(s' = 1454) ;
[] (s = 1372) -> 1.000000:(s' = 1454) ;
[] (s = 1373) -> 1.000000:(s' = 1455) ;
[] (s = 1374) -> 1.000000:(s' = 1455) ;
[] (s = 1375) -> 1.000000:(s' = 1456) ;
[] (s = 1376) -> 1.000000:(s' = 1456) ;
[] (s = 1377) -> 1.000000:(s' = 1457) ;
[] (s = 1378) -> 1.000000:(s' = 1457) ;
[] (s = 1379) -> 1.000000:(s' = 1458) ;
[] (s = 1380) -> 1.000000:(s' = 1458) ;
[] (s = 1381) -> 1.000000:(s' = 1459) ;
[] (s = 1382) -> 1.000000:(s' = 1459) ;
[] (s = 1383) -> 1.000000:(s' = 1460) ;
[] (s = 1384) -> 1.000000:(s' = 1460) ;
[] (s = 1385) -> 1.000000:(s' = 1461) ;
[] (s = 1386) -> 1.000000:(s' = 1462) ;
[] (s = 1387) -> 1.000000:(s' = 1461) ;
[] (s = 1388) -> 1.000000:(s' = 1462) ;
[] (s = 1389) -> 1.000000:(s' = 1463) ;
[] (s = 1390) -> 1.000000:(s' = 1464) ;
[] (s = 1391) -> 1.000000:(s' = 1463) ;
[] (s = 1392) -> 1.000000:(s' = 1464) ;
[] (s = 1393) -> 1.000000:(s' = 1465) ;
[] (s = 1394) -> 1.000000:(s' = 1465) ;
[] (s = 1395) -> 1.000000:(s' = 1466) ;
[] (s = 1396) -> 1.000000:(s' = 1466) ;
[] (s = 1397) -> 1.000000:(s' = 1467) ;
[] (s = 1398) -> 1.000000:(s' = 1467) ;
[] (s = 1399) -> 1.000000:(s' = 1468) ;
[] (s = 1400) -> 1.000000:(s' = 1468) ;
[] (s = 1401) -> 1.000000:(s' = 1469) ;
[] (s = 1402) -> 1.000000:(s' = 1469) ;
[] (s = 1403) -> 1.000000:(s' = 1470) ;
[] (s = 1404) -> 1.000000:(s' = 1470) ;
[] (s = 1405) -> 1.000000:(s' = 1471) ;
[] (s = 1406) -> 1.000000:(s' = 1471) ;
[] (s = 1407) -> 1.000000:(s' = 1472) ;
[] (s = 1408) -> 1.000000:(s' = 1472) ;
[] (s = 1409) -> 1.000000:(s' = 1473) ;
[] (s = 1410) -> 1.000000:(s' = 1474) ;
[] (s = 1411) -> 1.000000:(s' = 1473) ;
[] (s = 1412) -> 1.000000:(s' = 1474) ;
[] (s = 1413) -> 1.000000:(s' = 1475) ;
[] (s = 1414) -> 1.000000:(s' = 1476) ;
[] (s = 1415) -> 1.000000:(s' = 1475) ;
[] (s = 1416) -> 1.000000:(s' = 1476) ;
[] (s = 1417) -> 1.000000:(s' = 1477) ;
[] (s = 1418) -> 1.000000:(s' = 1477) ;
[] (s = 1419) -> 1.000000:(s' = 1478) ;
[] (s = 1420) -> 1.000000:(s' = 1478) ;
[] (s = 1421) -> 1.000000:(s' = 1479) ;
[] (s = 1422) -> 1.000000:(s' = 1479) ;
[] (s = 1423) -> 1.000000:(s' = 1480) ;
[] (s = 1424) -> 1.000000:(s' = 1480) ;
[] (s = 1425) -> 1.000000:(s' = 1481) ;
[] (s = 1426) -> 1.000000:(s' = 1481) ;
[] (s = 1427) -> 1.000000:(s' = 1482) ;
[] (s = 1428) -> 1.000000:(s' = 1482) ;
[] (s = 1429) -> 1.000000:(s' = 1483) ;
[] (s = 1430) -> 1.000000:(s' = 1483) ;
[] (s = 1431) -> 1.000000:(s' = 1484) ;
[] (s = 1432) -> 1.000000:(s' = 1484) ;
[] (s = 1433) -> 1.000000:(s' = 1485) ;
[] (s = 1434) -> 1.000000:(s' = 1486) ;
[] (s = 1435) -> 1.000000:(s' = 1485) ;
[] (s = 1436) -> 1.000000:(s' = 1486) ;
[] (s = 1437) -> 1.000000:(s' = 1487) ;
[] (s = 1438) -> 1.000000:(s' = 1488) ;
[] (s = 1439) -> 1.000000:(s' = 1487) ;
[] (s = 1440) -> 1.000000:(s' = 1488) ;
[] (s = 1441) -> 1.000000:(s' = 1489) ;
[] (s = 1441) -> 1.000000:(s' = 1490) ;
[] (s = 1442) -> 1.000000:(s' = 1491) ;
[] (s = 1443) -> 1.000000:(s' = 1492) ;
[] (s = 1444) -> 1.000000:(s' = 1493) ;
[] (s = 1444) -> 1.000000:(s' = 1494) ;
[] (s = 1445) -> 1.000000:(s' = 1495) ;
[] (s = 1445) -> 1.000000:(s' = 1496) ;
[] (s = 1446) -> 1.000000:(s' = 1497) ;
[] (s = 1447) -> 1.000000:(s' = 1498) ;
[] (s = 1448) -> 1.000000:(s' = 1499) ;
[] (s = 1448) -> 1.000000:(s' = 1500) ;
[] (s = 1449) -> 1.000000:(s' = 1501) ;
[] (s = 1449) -> 1.000000:(s' = 1502) ;
[] (s = 1450) -> 1.000000:(s' = 1503) ;
[] (s = 1451) -> 1.000000:(s' = 1504) ;
[] (s = 1452) -> 1.000000:(s' = 1505) ;
[] (s = 1452) -> 1.000000:(s' = 1506) ;
[] (s = 1453) -> 1.000000:(s' = 1507) ;
[] (s = 1453) -> 1.000000:(s' = 1508) ;
[] (s = 1454) -> 1.000000:(s' = 1509) ;
[] (s = 1455) -> 1.000000:(s' = 1510) ;
[] (s = 1456) -> 1.000000:(s' = 1511) ;
[] (s = 1456) -> 1.000000:(s' = 1512) ;
[] (s = 1457) -> 1.000000:(s' = 1513) ;
[] (s = 1457) -> 1.000000:(s' = 1514) ;
[] (s = 1458) -> 1.000000:(s' = 1515) ;
[] (s = 1459) -> 1.000000:(s' = 1516) ;
[] (s = 1460) -> 1.000000:(s' = 1517) ;
[] (s = 1460) -> 1.000000:(s' = 1518) ;
[] (s = 1461) -> 1.000000:(s' = 1519) ;
[] (s = 1461) -> 1.000000:(s' = 1520) ;
[] (s = 1462) -> 1.000000:(s' = 1521) ;
[] (s = 1463) -> 1.000000:(s' = 1522) ;
[] (s = 1464) -> 1.000000:(s' = 1523) ;
[] (s = 1464) -> 1.000000:(s' = 1524) ;
[] (s = 1465) -> 1.000000:(s' = 1525) ;
[] (s = 1465) -> 1.000000:(s' = 1526) ;
[] (s = 1466) -> 1.000000:(s' = 1527) ;
[] (s = 1467) -> 1.000000:(s' = 1528) ;
[] (s = 1468) -> 1.000000:(s' = 1529) ;
[] (s = 1468) -> 1.000000:(s' = 1530) ;
[] (s = 1469) -> 1.000000:(s' = 1531) ;
[] (s = 1469) -> 1.000000:(s' = 1532) ;
[] (s = 1470) -> 1.000000:(s' = 1533) ;
[] (s = 1471) -> 1.000000:(s' = 1534) ;
[] (s = 1472) -> 1.000000:(s' = 1535) ;
[] (s = 1472) -> 1.000000:(s' = 1536) ;
[] (s = 1473) -> 1.000000:(s' = 1537) ;
[] (s = 1473) -> 1.000000:(s' = 1538) ;
[] (s = 1474) -> 1.000000:(s' = 1539) ;
[] (s = 1475) -> 1.000000:(s' = 1540) ;
[] (s = 1476) -> 1.000000:(s' = 1541) ;
[] (s = 1476) -> 1.000000:(s' = 1542) ;
[] (s = 1477) -> 1.000000:(s' = 1543) ;
[] (s = 1477) -> 1.000000:(s' = 1544) ;
[] (s = 1478) -> 1.000000:(s' = 1545) ;
[] (s = 1479) -> 1.000000:(s' = 1546) ;
[] (s = 1480) -> 1.000000:(s' = 1547) ;
[] (s = 1480) -> 1.000000:(s' = 1548) ;
[] (s = 1481) -> 1.000000:(s' = 1549) ;
[] (s = 1481) -> 1.000000:(s' = 1550) ;
[] (s = 1482) -> 1.000000:(s' = 1551) ;
[] (s = 1483) -> 1.000000:(s' = 1552) ;
[] (s = 1484) -> 1.000000:(s' = 1553) ;
[] (s = 1484) -> 1.000000:(s' = 1554) ;
[] (s = 1485) -> 1.000000:(s' = 1555) ;
[] (s = 1485) -> 1.000000:(s' = 1556) ;
[] (s = 1486) -> 1.000000:(s' = 1557) ;
[] (s = 1487) -> 1.000000:(s' = 1558) ;
[] (s = 1488) -> 1.000000:(s' = 1559) ;
[] (s = 1488) -> 1.000000:(s' = 1560) ;
[] (s = 1489) -> 1.000000:(s' = 1561) ;
[] (s = 1489) -> 1.000000:(s' = 1562) ;
[] (s = 1490) -> 1.000000:(s' = 1563) ;
[] (s = 1490) -> 1.000000:(s' = 1564) ;
[] (s = 1491) -> 1.000000:(s' = 1565) ;
[] (s = 1492) -> 1.000000:(s' = 1566) ;
[] (s = 1493) -> 1.000000:(s' = 1567) ;
[] (s = 1493) -> 1.000000:(s' = 1568) ;
[] (s = 1494) -> 1.000000:(s' = 1569) ;
[] (s = 1494) -> 1.000000:(s' = 1570) ;
[] (s = 1495) -> 1.000000:(s' = 1571) ;
[] (s = 1495) -> 1.000000:(s' = 1572) ;
[] (s = 1496) -> 1.000000:(s' = 1573) ;
[] (s = 1496) -> 1.000000:(s' = 1574) ;
[] (s = 1497) -> 1.000000:(s' = 1575) ;
[] (s = 1498) -> 1.000000:(s' = 1576) ;
[] (s = 1499) -> 1.000000:(s' = 1577) ;
[] (s = 1499) -> 1.000000:(s' = 1578) ;
[] (s = 1500) -> 1.000000:(s' = 1579) ;
[] (s = 1500) -> 1.000000:(s' = 1580) ;
[] (s = 1501) -> 1.000000:(s' = 1581) ;
[] (s = 1501) -> 1.000000:(s' = 1582) ;
[] (s = 1502) -> 1.000000:(s' = 1583) ;
[] (s = 1502) -> 1.000000:(s' = 1584) ;
[] (s = 1503) -> 1.000000:(s' = 1585) ;
[] (s = 1504) -> 1.000000:(s' = 1586) ;
[] (s = 1505) -> 1.000000:(s' = 1587) ;
[] (s = 1505) -> 1.000000:(s' = 1588) ;
[] (s = 1506) -> 1.000000:(s' = 1589) ;
[] (s = 1506) -> 1.000000:(s' = 1590) ;
[] (s = 1507) -> 1.000000:(s' = 1591) ;
[] (s = 1507) -> 1.000000:(s' = 1592) ;
[] (s = 1508) -> 1.000000:(s' = 1593) ;
[] (s = 1508) -> 1.000000:(s' = 1594) ;
[] (s = 1509) -> 1.000000:(s' = 1595) ;
[] (s = 1510) -> 1.000000:(s' = 1596) ;
[] (s = 1511) -> 1.000000:(s' = 1597) ;
[] (s = 1511) -> 1.000000:(s' = 1598) ;
[] (s = 1512) -> 1.000000:(s' = 1599) ;
[] (s = 1512) -> 1.000000:(s' = 1600) ;
[] (s = 1513) -> 1.000000:(s' = 1601) ;
[] (s = 1513) -> 1.000000:(s' = 1602) ;
[] (s = 1514) -> 1.000000:(s' = 1603) ;
[] (s = 1514) -> 1.000000:(s' = 1604) ;
[] (s = 1515) -> 1.000000:(s' = 1605) ;
[] (s = 1516) -> 1.000000:(s' = 1606) ;
[] (s = 1517) -> 1.000000:(s' = 1607) ;
[] (s = 1517) -> 1.000000:(s' = 1608) ;
[] (s = 1518) -> 1.000000:(s' = 1609) ;
[] (s = 1518) -> 1.000000:(s' = 1610) ;
[] (s = 1519) -> 1.000000:(s' = 1611) ;
[] (s = 1519) -> 1.000000:(s' = 1612) ;
[] (s = 1520) -> 1.000000:(s' = 1613) ;
[] (s = 1520) -> 1.000000:(s' = 1614) ;
[] (s = 1521) -> 1.000000:(s' = 1615) ;
[] (s = 1522) -> 1.000000:(s' = 1616) ;
[] (s = 1523) -> 1.000000:(s' = 1617) ;
[] (s = 1523) -> 1.000000:(s' = 1618) ;
[] (s = 1524) -> 1.000000:(s' = 1619) ;
[] (s = 1524) -> 1.000000:(s' = 1620) ;
[] (s = 1525) -> 1.000000:(s' = 1621) ;
[] (s = 1525) -> 1.000000:(s' = 1622) ;
[] (s = 1526) -> 1.000000:(s' = 1623) ;
[] (s = 1526) -> 1.000000:(s' = 1624) ;
[] (s = 1527) -> 1.000000:(s' = 1625) ;
[] (s = 1528) -> 1.000000:(s' = 1626) ;
[] (s = 1529) -> 1.000000:(s' = 1627) ;
[] (s = 1529) -> 1.000000:(s' = 1628) ;
[] (s = 1530) -> 1.000000:(s' = 1629) ;
[] (s = 1530) -> 1.000000:(s' = 1630) ;
[] (s = 1531) -> 1.000000:(s' = 1631) ;
[] (s = 1531) -> 1.000000:(s' = 1632) ;
[] (s = 1532) -> 1.000000:(s' = 1633) ;
[] (s = 1532) -> 1.000000:(s' = 1634) ;
[] (s = 1533) -> 1.000000:(s' = 1635) ;
[] (s = 1534) -> 1.000000:(s' = 1636) ;
[] (s = 1535) -> 1.000000:(s' = 1637) ;
[] (s = 1535) -> 1.000000:(s' = 1638) ;
[] (s = 1536) -> 1.000000:(s' = 1639) ;
[] (s = 1536) -> 1.000000:(s' = 1640) ;
[] (s = 1537) -> 1.000000:(s' = 1641) ;
[] (s = 1537) -> 1.000000:(s' = 1642) ;
[] (s = 1538) -> 1.000000:(s' = 1643) ;
[] (s = 1538) -> 1.000000:(s' = 1644) ;
[] (s = 1539) -> 1.000000:(s' = 1645) ;
[] (s = 1540) -> 1.000000:(s' = 1646) ;
[] (s = 1541) -> 1.000000:(s' = 1647) ;
[] (s = 1541) -> 1.000000:(s' = 1648) ;
[] (s = 1542) -> 1.000000:(s' = 1649) ;
[] (s = 1542) -> 1.000000:(s' = 1650) ;
[] (s = 1543) -> 1.000000:(s' = 1651) ;
[] (s = 1543) -> 1.000000:(s' = 1652) ;
[] (s = 1544) -> 1.000000:(s' = 1653) ;
[] (s = 1544) -> 1.000000:(s' = 1654) ;
[] (s = 1545) -> 1.000000:(s' = 1655) ;
[] (s = 1546) -> 1.000000:(s' = 1656) ;
[] (s = 1547) -> 1.000000:(s' = 1657) ;
[] (s = 1547) -> 1.000000:(s' = 1658) ;
[] (s = 1548) -> 1.000000:(s' = 1659) ;
[] (s = 1548) -> 1.000000:(s' = 1660) ;
[] (s = 1549) -> 1.000000:(s' = 1661) ;
[] (s = 1549) -> 1.000000:(s' = 1662) ;
[] (s = 1550) -> 1.000000:(s' = 1663) ;
[] (s = 1550) -> 1.000000:(s' = 1664) ;
[] (s = 1551) -> 1.000000:(s' = 1665) ;
[] (s = 1552) -> 1.000000:(s' = 1666) ;
[] (s = 1553) -> 1.000000:(s' = 1667) ;
[] (s = 1553) -> 1.000000:(s' = 1668) ;
[] (s = 1554) -> 1.000000:(s' = 1669) ;
[] (s = 1554) -> 1.000000:(s' = 1670) ;
[] (s = 1555) -> 1.000000:(s' = 1671) ;
[] (s = 1555) -> 1.000000:(s' = 1672) ;
[] (s = 1556) -> 1.000000:(s' = 1673) ;
[] (s = 1556) -> 1.000000:(s' = 1674) ;
[] (s = 1557) -> 1.000000:(s' = 1675) ;
[] (s = 1558) -> 1.000000:(s' = 1676) ;
[] (s = 1559) -> 1.000000:(s' = 1677) ;
[] (s = 1559) -> 1.000000:(s' = 1678) ;
[] (s = 1560) -> 1.000000:(s' = 1679) ;
[] (s = 1560) -> 1.000000:(s' = 1680) ;
[] (s = 1561) -> 1.000000:(s' = 1681) ;
[] (s = 1561) -> 1.000000:(s' = 1682) ;
[] (s = 1562) -> 1.000000:(s' = 1683) ;
[] (s = 1563) -> 1.000000:(s' = 1684) ;
[] (s = 1563) -> 1.000000:(s' = 1685) ;
[] (s = 1564) -> 1.000000:(s' = 1686) ;
[] (s = 1565) -> 1.000000:(s' = 1687) ;
[] (s = 1566) -> 1.000000:(s' = 1688) ;
[] (s = 1567) -> 1.000000:(s' = 1689) ;
[] (s = 1567) -> 1.000000:(s' = 1690) ;
[] (s = 1568) -> 1.000000:(s' = 1691) ;
[] (s = 1569) -> 1.000000:(s' = 1692) ;
[] (s = 1569) -> 1.000000:(s' = 1693) ;
[] (s = 1570) -> 1.000000:(s' = 1694) ;
[] (s = 1571) -> 1.000000:(s' = 1695) ;
[] (s = 1571) -> 1.000000:(s' = 1696) ;
[] (s = 1572) -> 1.000000:(s' = 1697) ;
[] (s = 1573) -> 1.000000:(s' = 1684) ;
[] (s = 1573) -> 1.000000:(s' = 1685) ;
[] (s = 1574) -> 1.000000:(s' = 1698) ;
[] (s = 1575) -> 1.000000:(s' = 1699) ;
[] (s = 1576) -> 1.000000:(s' = 1700) ;
[] (s = 1577) -> 1.000000:(s' = 1701) ;
[] (s = 1577) -> 1.000000:(s' = 1702) ;
[] (s = 1578) -> 1.000000:(s' = 1703) ;
[] (s = 1579) -> 1.000000:(s' = 1692) ;
[] (s = 1579) -> 1.000000:(s' = 1693) ;
[] (s = 1580) -> 1.000000:(s' = 1704) ;
[] (s = 1581) -> 1.000000:(s' = 1695) ;
[] (s = 1581) -> 1.000000:(s' = 1696) ;
[] (s = 1582) -> 1.000000:(s' = 1705) ;
[] (s = 1583) -> 1.000000:(s' = 1706) ;
[] (s = 1583) -> 1.000000:(s' = 1707) ;
[] (s = 1584) -> 1.000000:(s' = 1708) ;
[] (s = 1585) -> 1.000000:(s' = 1709) ;
[] (s = 1586) -> 1.000000:(s' = 1710) ;
[] (s = 1587) -> 1.000000:(s' = 1701) ;
[] (s = 1587) -> 1.000000:(s' = 1702) ;
[] (s = 1588) -> 1.000000:(s' = 1711) ;
[] (s = 1589) -> 1.000000:(s' = 1712) ;
[] (s = 1589) -> 1.000000:(s' = 1713) ;
[] (s = 1590) -> 1.000000:(s' = 1714) ;
[] (s = 1591) -> 1.000000:(s' = 1715) ;
[] (s = 1591) -> 1.000000:(s' = 1716) ;
[] (s = 1592) -> 1.000000:(s' = 1717) ;
[] (s = 1593) -> 1.000000:(s' = 1718) ;
[] (s = 1593) -> 1.000000:(s' = 1719) ;
[] (s = 1594) -> 1.000000:(s' = 1720) ;
[] (s = 1595) -> 1.000000:(s' = 1721) ;
[] (s = 1596) -> 1.000000:(s' = 1722) ;
[] (s = 1597) -> 1.000000:(s' = 1723) ;
[] (s = 1597) -> 1.000000:(s' = 1724) ;
[] (s = 1598) -> 1.000000:(s' = 1725) ;
[] (s = 1599) -> 1.000000:(s' = 1726) ;
[] (s = 1599) -> 1.000000:(s' = 1727) ;
[] (s = 1600) -> 1.000000:(s' = 1728) ;
[] (s = 1601) -> 1.000000:(s' = 1729) ;
[] (s = 1601) -> 1.000000:(s' = 1730) ;
[] (s = 1602) -> 1.000000:(s' = 1731) ;
[] (s = 1603) -> 1.000000:(s' = 1718) ;
[] (s = 1603) -> 1.000000:(s' = 1719) ;
[] (s = 1604) -> 1.000000:(s' = 1732) ;
[] (s = 1605) -> 1.000000:(s' = 1733) ;
[] (s = 1606) -> 1.000000:(s' = 1734) ;
[] (s = 1607) -> 1.000000:(s' = 1735) ;
[] (s = 1607) -> 1.000000:(s' = 1736) ;
[] (s = 1608) -> 1.000000:(s' = 1737) ;
[] (s = 1609) -> 1.000000:(s' = 1726) ;
[] (s = 1609) -> 1.000000:(s' = 1727) ;
[] (s = 1610) -> 1.000000:(s' = 1738) ;
[] (s = 1611) -> 1.000000:(s' = 1729) ;
[] (s = 1611) -> 1.000000:(s' = 1730) ;
[] (s = 1612) -> 1.000000:(s' = 1739) ;
[] (s = 1613) -> 1.000000:(s' = 1740) ;
[] (s = 1613) -> 1.000000:(s' = 1741) ;
[] (s = 1614) -> 1.000000:(s' = 1742) ;
[] (s = 1615) -> 1.000000:(s' = 1743) ;
[] (s = 1616) -> 1.000000:(s' = 1744) ;
[] (s = 1617) -> 1.000000:(s' = 1735) ;
[] (s = 1617) -> 1.000000:(s' = 1736) ;
[] (s = 1618) -> 1.000000:(s' = 1745) ;
[] (s = 1619) -> 1.000000:(s' = 1746) ;
[] (s = 1619) -> 1.000000:(s' = 1747) ;
[] (s = 1620) -> 1.000000:(s' = 1748) ;
[] (s = 1621) -> 1.000000:(s' = 1749) ;
[] (s = 1621) -> 1.000000:(s' = 1750) ;
[] (s = 1622) -> 1.000000:(s' = 1751) ;
[] (s = 1623) -> 1.000000:(s' = 1752) ;
[] (s = 1623) -> 1.000000:(s' = 1753) ;
[] (s = 1624) -> 1.000000:(s' = 1754) ;
[] (s = 1625) -> 1.000000:(s' = 1755) ;
[] (s = 1626) -> 1.000000:(s' = 1756) ;
[] (s = 1627) -> 1.000000:(s' = 1757) ;
[] (s = 1627) -> 1.000000:(s' = 1758) ;
[] (s = 1628) -> 1.000000:(s' = 1759) ;
[] (s = 1629) -> 1.000000:(s' = 1760) ;
[] (s = 1629) -> 1.000000:(s' = 1761) ;
[] (s = 1630) -> 1.000000:(s' = 1762) ;
[] (s = 1631) -> 1.000000:(s' = 1763) ;
[] (s = 1631) -> 1.000000:(s' = 1764) ;
[] (s = 1632) -> 1.000000:(s' = 1765) ;
[] (s = 1633) -> 1.000000:(s' = 1752) ;
[] (s = 1633) -> 1.000000:(s' = 1753) ;
[] (s = 1634) -> 1.000000:(s' = 1766) ;
[] (s = 1635) -> 1.000000:(s' = 1767) ;
[] (s = 1636) -> 1.000000:(s' = 1768) ;
[] (s = 1637) -> 1.000000:(s' = 1769) ;
[] (s = 1637) -> 1.000000:(s' = 1770) ;
[] (s = 1638) -> 1.000000:(s' = 1771) ;
[] (s = 1639) -> 1.000000:(s' = 1760) ;
[] (s = 1639) -> 1.000000:(s' = 1761) ;
[] (s = 1640) -> 1.000000:(s' = 1772) ;
[] (s = 1641) -> 1.000000:(s' = 1763) ;
[] (s = 1641) -> 1.000000:(s' = 1764) ;
[] (s = 1642) -> 1.000000:(s' = 1773) ;
[] (s = 1643) -> 1.000000:(s' = 1774) ;
[] (s = 1643) -> 1.000000:(s' = 1775) ;
[] (s = 1644) -> 1.000000:(s' = 1776) ;
[] (s = 1645) -> 1.000000:(s' = 1777) ;
[] (s = 1646) -> 1.000000:(s' = 1778) ;
[] (s = 1647) -> 1.000000:(s' = 1769) ;
[] (s = 1647) -> 1.000000:(s' = 1770) ;
[] (s = 1648) -> 1.000000:(s' = 1779) ;
[] (s = 1649) -> 1.000000:(s' = 1780) ;
[] (s = 1649) -> 1.000000:(s' = 1781) ;
[] (s = 1650) -> 1.000000:(s' = 1782) ;
[] (s = 1651) -> 1.000000:(s' = 1783) ;
[] (s = 1651) -> 1.000000:(s' = 1784) ;
[] (s = 1652) -> 1.000000:(s' = 1785) ;
[] (s = 1653) -> 1.000000:(s' = 1786) ;
[] (s = 1653) -> 1.000000:(s' = 1787) ;
[] (s = 1654) -> 1.000000:(s' = 1788) ;
[] (s = 1655) -> 1.000000:(s' = 1789) ;
[] (s = 1656) -> 1.000000:(s' = 1790) ;
[] (s = 1657) -> 1.000000:(s' = 1791) ;
[] (s = 1657) -> 1.000000:(s' = 1792) ;
[] (s = 1658) -> 1.000000:(s' = 1793) ;
[] (s = 1659) -> 1.000000:(s' = 1794) ;
[] (s = 1659) -> 1.000000:(s' = 1795) ;
[] (s = 1660) -> 1.000000:(s' = 1796) ;
[] (s = 1661) -> 1.000000:(s' = 1797) ;
[] (s = 1661) -> 1.000000:(s' = 1798) ;
[] (s = 1662) -> 1.000000:(s' = 1799) ;
[] (s = 1663) -> 1.000000:(s' = 1786) ;
[] (s = 1663) -> 1.000000:(s' = 1787) ;
[] (s = 1664) -> 1.000000:(s' = 1800) ;
[] (s = 1665) -> 1.000000:(s' = 1801) ;
[] (s = 1666) -> 1.000000:(s' = 1802) ;
[] (s = 1667) -> 1.000000:(s' = 1803) ;
[] (s = 1667) -> 1.000000:(s' = 1804) ;
[] (s = 1668) -> 1.000000:(s' = 1805) ;
[] (s = 1669) -> 1.000000:(s' = 1794) ;
[] (s = 1669) -> 1.000000:(s' = 1795) ;
[] (s = 1670) -> 1.000000:(s' = 1806) ;
[] (s = 1671) -> 1.000000:(s' = 1797) ;
[] (s = 1671) -> 1.000000:(s' = 1798) ;
[] (s = 1672) -> 1.000000:(s' = 1807) ;
[] (s = 1673) -> 1.000000:(s' = 1808) ;
[] (s = 1673) -> 1.000000:(s' = 1809) ;
[] (s = 1674) -> 1.000000:(s' = 1810) ;
[] (s = 1675) -> 1.000000:(s' = 1811) ;
[] (s = 1676) -> 1.000000:(s' = 1812) ;
[] (s = 1677) -> 1.000000:(s' = 1803) ;
[] (s = 1677) -> 1.000000:(s' = 1804) ;
[] (s = 1678) -> 1.000000:(s' = 1813) ;
[] (s = 1679) -> 1.000000:(s' = 1814) ;
[] (s = 1679) -> 1.000000:(s' = 1815) ;
[] (s = 1680) -> 1.000000:(s' = 1816) ;
[] (s = 1681) -> 0.500000:(s' = 1817) + 0.500000:(s' = 1818);
[] (s = 1681) -> 1.000000:(s' = 1819) ;
[] (s = 1682) -> 1.000000:(s' = 1819) ;
[] (s = 1682) -> 0.500000:(s' = 1820) + 0.500000:(s' = 1821);
[] (s = 1683) -> 1.000000:(s' = 60) ;
[] (s = 1683) -> 1.000000:(s' = 433) ;
[] (s = 1684) -> 0.500000:(s' = 1822) + 0.500000:(s' = 1823);
[] (s = 1684) -> 1.000000:(s' = 1824) ;
[] (s = 1685) -> 1.000000:(s' = 1824) ;
[] (s = 1685) -> 0.500000:(s' = 1825) + 0.500000:(s' = 1826);
[] (s = 1686) -> 1.000000:(s' = 60) ;
[] (s = 1686) -> 1.000000:(s' = 433) ;
[] (s = 1687) -> 1.000000:(s' = 60) ;
[] (s = 1687) -> 1.000000:(s' = 433) ;
[] (s = 1688) -> 1.000000:(s' = 60) ;
[] (s = 1688) -> 1.000000:(s' = 433) ;
[] (s = 1689) -> 0.500000:(s' = 1827) + 0.500000:(s' = 1828);
[] (s = 1689) -> 1.000000:(s' = 1829) ;
[] (s = 1690) -> 1.000000:(s' = 1829) ;
[] (s = 1690) -> 0.500000:(s' = 1830) + 0.500000:(s' = 1831);
[] (s = 1691) -> 1.000000:(s' = 60) ;
[] (s = 1691) -> 1.000000:(s' = 433) ;
[] (s = 1692) -> 0.500000:(s' = 1832) + 0.500000:(s' = 1833);
[] (s = 1692) -> 1.000000:(s' = 1834) ;
[] (s = 1693) -> 1.000000:(s' = 1834) ;
[] (s = 1693) -> 0.500000:(s' = 1835) + 0.500000:(s' = 1836);
[] (s = 1694) -> 1.000000:(s' = 60) ;
[] (s = 1694) -> 1.000000:(s' = 433) ;
[] (s = 1695) -> 0.500000:(s' = 1837) + 0.500000:(s' = 1838);
[] (s = 1695) -> 1.000000:(s' = 1839) ;
[] (s = 1696) -> 1.000000:(s' = 1839) ;
[] (s = 1696) -> 0.500000:(s' = 1840) + 0.500000:(s' = 1841);
[] (s = 1697) -> 1.000000:(s' = 60) ;
[] (s = 1697) -> 1.000000:(s' = 433) ;
[] (s = 1698) -> 1.000000:(s' = 60) ;
[] (s = 1698) -> 1.000000:(s' = 433) ;
[] (s = 1699) -> 1.000000:(s' = 60) ;
[] (s = 1699) -> 1.000000:(s' = 433) ;
[] (s = 1700) -> 1.000000:(s' = 60) ;
[] (s = 1700) -> 1.000000:(s' = 433) ;
[] (s = 1701) -> 0.500000:(s' = 1842) + 0.500000:(s' = 1843);
[] (s = 1701) -> 1.000000:(s' = 1844) ;
[] (s = 1702) -> 1.000000:(s' = 1844) ;
[] (s = 1702) -> 0.500000:(s' = 1845) + 0.500000:(s' = 1846);
[] (s = 1703) -> 1.000000:(s' = 60) ;
[] (s = 1703) -> 1.000000:(s' = 433) ;
[] (s = 1704) -> 1.000000:(s' = 60) ;
[] (s = 1704) -> 1.000000:(s' = 433) ;
[] (s = 1705) -> 1.000000:(s' = 60) ;
[] (s = 1705) -> 1.000000:(s' = 433) ;
[] (s = 1706) -> 0.500000:(s' = 1847) + 0.500000:(s' = 1848);
[] (s = 1706) -> 1.000000:(s' = 1849) ;
[] (s = 1707) -> 1.000000:(s' = 1849) ;
[] (s = 1707) -> 0.500000:(s' = 1850) + 0.500000:(s' = 1851);
[] (s = 1708) -> 1.000000:(s' = 60) ;
[] (s = 1708) -> 1.000000:(s' = 433) ;
[] (s = 1709) -> 1.000000:(s' = 60) ;
[] (s = 1709) -> 1.000000:(s' = 433) ;
[] (s = 1710) -> 1.000000:(s' = 60) ;
[] (s = 1710) -> 1.000000:(s' = 433) ;
[] (s = 1711) -> 1.000000:(s' = 60) ;
[] (s = 1711) -> 1.000000:(s' = 433) ;
[] (s = 1712) -> 0.500000:(s' = 1852) + 0.500000:(s' = 1853);
[] (s = 1712) -> 1.000000:(s' = 1854) ;
[] (s = 1713) -> 1.000000:(s' = 1854) ;
[] (s = 1713) -> 0.500000:(s' = 1855) + 0.500000:(s' = 1856);
[] (s = 1714) -> 1.000000:(s' = 60) ;
[] (s = 1714) -> 1.000000:(s' = 433) ;
[] (s = 1715) -> 0.500000:(s' = 1857) + 0.500000:(s' = 1858);
[] (s = 1715) -> 1.000000:(s' = 1829) ;
[] (s = 1716) -> 1.000000:(s' = 1829) ;
[] (s = 1716) -> 0.500000:(s' = 1859) + 0.500000:(s' = 1860);
[] (s = 1717) -> 1.000000:(s' = 60) ;
[] (s = 1717) -> 1.000000:(s' = 433) ;
[] (s = 1718) -> 0.500000:(s' = 1861) + 0.500000:(s' = 1862);
[] (s = 1718) -> 1.000000:(s' = 1863) ;
[] (s = 1719) -> 1.000000:(s' = 1863) ;
[] (s = 1719) -> 0.500000:(s' = 1864) + 0.500000:(s' = 1865);
[] (s = 1720) -> 1.000000:(s' = 60) ;
[] (s = 1720) -> 1.000000:(s' = 433) ;
[] (s = 1721) -> 1.000000:(s' = 433) ;
[] (s = 1722) -> 1.000000:(s' = 433) ;
[] (s = 1723) -> 0.500000:(s' = 1866) + 0.500000:(s' = 1867);
[] (s = 1723) -> 1.000000:(s' = 1078) ;
[] (s = 1724) -> 1.000000:(s' = 1078) ;
[] (s = 1724) -> 0.500000:(s' = 1868) + 0.500000:(s' = 1869);
[] (s = 1725) -> 1.000000:(s' = 433) ;
[] (s = 1726) -> 0.500000:(s' = 1870) + 0.500000:(s' = 1871);
[] (s = 1726) -> 1.000000:(s' = 1083) ;
[] (s = 1727) -> 1.000000:(s' = 1083) ;
[] (s = 1727) -> 0.500000:(s' = 1872) + 0.500000:(s' = 1873);
[] (s = 1728) -> 1.000000:(s' = 433) ;
[] (s = 1729) -> 0.500000:(s' = 1874) + 0.500000:(s' = 1875);
[] (s = 1729) -> 1.000000:(s' = 1876) ;
[] (s = 1730) -> 1.000000:(s' = 1876) ;
[] (s = 1730) -> 0.500000:(s' = 1877) + 0.500000:(s' = 1878);
[] (s = 1731) -> 1.000000:(s' = 60) ;
[] (s = 1731) -> 1.000000:(s' = 433) ;
[] (s = 1732) -> 1.000000:(s' = 60) ;
[] (s = 1732) -> 1.000000:(s' = 433) ;
[] (s = 1733) -> 1.000000:(s' = 433) ;
[] (s = 1734) -> 1.000000:(s' = 433) ;
[] (s = 1735) -> 0.500000:(s' = 1879) + 0.500000:(s' = 1880);
[] (s = 1735) -> 1.000000:(s' = 1093) ;
[] (s = 1736) -> 1.000000:(s' = 1093) ;
[] (s = 1736) -> 0.500000:(s' = 1881) + 0.500000:(s' = 1882);
[] (s = 1737) -> 1.000000:(s' = 433) ;
[] (s = 1738) -> 1.000000:(s' = 433) ;
[] (s = 1739) -> 1.000000:(s' = 60) ;
[] (s = 1739) -> 1.000000:(s' = 433) ;
[] (s = 1740) -> 0.500000:(s' = 1883) + 0.500000:(s' = 1884);
[] (s = 1740) -> 1.000000:(s' = 1854) ;
[] (s = 1741) -> 1.000000:(s' = 1854) ;
[] (s = 1741) -> 0.500000:(s' = 1885) + 0.500000:(s' = 1886);
[] (s = 1742) -> 1.000000:(s' = 60) ;
[] (s = 1742) -> 1.000000:(s' = 433) ;
[] (s = 1743) -> 1.000000:(s' = 433) ;
[] (s = 1744) -> 1.000000:(s' = 433) ;
[] (s = 1745) -> 1.000000:(s' = 433) ;
[] (s = 1746) -> 0.500000:(s' = 1887) + 0.500000:(s' = 1888);
[] (s = 1746) -> 1.000000:(s' = 1102) ;
[] (s = 1747) -> 1.000000:(s' = 1102) ;
[] (s = 1747) -> 0.500000:(s' = 1889) + 0.500000:(s' = 1890);
[] (s = 1748) -> 1.000000:(s' = 433) ;
[] (s = 1749) -> 0.500000:(s' = 1891) + 0.500000:(s' = 1892);
[] (s = 1749) -> 1.000000:(s' = 1078) ;
[] (s = 1750) -> 1.000000:(s' = 1078) ;
[] (s = 1750) -> 0.500000:(s' = 1893) + 0.500000:(s' = 1894);
[] (s = 1751) -> 1.000000:(s' = 433) ;
[] (s = 1752) -> 0.500000:(s' = 1895) + 0.500000:(s' = 1896);
[] (s = 1752) -> 1.000000:(s' = 1897) ;
[] (s = 1753) -> 1.000000:(s' = 1897) ;
[] (s = 1753) -> 0.500000:(s' = 1898) + 0.500000:(s' = 1899);
[] (s = 1754) -> 1.000000:(s' = 433) ;
[] (s = 1755) -> 1.000000:(s' = 433) ;
[] (s = 1756) -> 1.000000:(s' = 433) ;
[] (s = 1757) -> 0.500000:(s' = 1900) + 0.500000:(s' = 1901);
[] (s = 1757) -> 1.000000:(s' = 1078) ;
[] (s = 1758) -> 1.000000:(s' = 1078) ;
[] (s = 1758) -> 0.500000:(s' = 1902) + 0.500000:(s' = 1903);
[] (s = 1759) -> 1.000000:(s' = 433) ;
[] (s = 1760) -> 0.500000:(s' = 1904) + 0.500000:(s' = 1905);
[] (s = 1760) -> 1.000000:(s' = 1083) ;
[] (s = 1761) -> 1.000000:(s' = 1083) ;
[] (s = 1761) -> 0.500000:(s' = 1906) + 0.500000:(s' = 1907);
[] (s = 1762) -> 1.000000:(s' = 433) ;
[] (s = 1763) -> 0.500000:(s' = 1908) + 0.500000:(s' = 1909);
[] (s = 1763) -> 1.000000:(s' = 1910) ;
[] (s = 1764) -> 1.000000:(s' = 1910) ;
[] (s = 1764) -> 0.500000:(s' = 1911) + 0.500000:(s' = 1912);
[] (s = 1765) -> 1.000000:(s' = 433) ;
[] (s = 1766) -> 1.000000:(s' = 433) ;
[] (s = 1767) -> 1.000000:(s' = 433) ;
[] (s = 1768) -> 1.000000:(s' = 433) ;
[] (s = 1769) -> 0.500000:(s' = 1913) + 0.500000:(s' = 1914);
[] (s = 1769) -> 1.000000:(s' = 1093) ;
[] (s = 1770) -> 1.000000:(s' = 1093) ;
[] (s = 1770) -> 0.500000:(s' = 1915) + 0.500000:(s' = 1916);
[] (s = 1771) -> 1.000000:(s' = 433) ;
[] (s = 1772) -> 1.000000:(s' = 433) ;
[] (s = 1773) -> 1.000000:(s' = 433) ;
[] (s = 1774) -> 0.500000:(s' = 1917) + 0.500000:(s' = 1918);
[] (s = 1774) -> 1.000000:(s' = 1102) ;
[] (s = 1775) -> 1.000000:(s' = 1102) ;
[] (s = 1775) -> 0.500000:(s' = 1919) + 0.500000:(s' = 1920);
[] (s = 1776) -> 1.000000:(s' = 433) ;
[] (s = 1777) -> 1.000000:(s' = 433) ;
[] (s = 1778) -> 1.000000:(s' = 433) ;
[] (s = 1779) -> 1.000000:(s' = 433) ;
[] (s = 1780) -> 0.500000:(s' = 1921) + 0.500000:(s' = 1922);
[] (s = 1780) -> 1.000000:(s' = 1102) ;
[] (s = 1781) -> 1.000000:(s' = 1102) ;
[] (s = 1781) -> 0.500000:(s' = 1923) + 0.500000:(s' = 1924);
[] (s = 1782) -> 1.000000:(s' = 433) ;
[] (s = 1783) -> 0.500000:(s' = 1925) + 0.500000:(s' = 1926);
[] (s = 1783) -> 1.000000:(s' = 1078) ;
[] (s = 1784) -> 1.000000:(s' = 1078) ;
[] (s = 1784) -> 0.500000:(s' = 1927) + 0.500000:(s' = 1928);
[] (s = 1785) -> 1.000000:(s' = 433) ;
[] (s = 1786) -> 0.500000:(s' = 1929) + 0.500000:(s' = 1930);
[] (s = 1786) -> 1.000000:(s' = 1897) ;
[] (s = 1787) -> 1.000000:(s' = 1897) ;
[] (s = 1787) -> 0.500000:(s' = 1931) + 0.500000:(s' = 1932);
[] (s = 1788) -> 1.000000:(s' = 433) ;
[] (s = 1789) -> 1.000000:(s' = 433) ;
[] (s = 1790) -> 1.000000:(s' = 433) ;
[] (s = 1791) -> 0.500000:(s' = 1933) + 0.500000:(s' = 1934);
[] (s = 1791) -> 1.000000:(s' = 1078) ;
[] (s = 1792) -> 1.000000:(s' = 1078) ;
[] (s = 1792) -> 0.500000:(s' = 1935) + 0.500000:(s' = 1936);
[] (s = 1793) -> 1.000000:(s' = 433) ;
[] (s = 1794) -> 0.500000:(s' = 1937) + 0.500000:(s' = 1938);
[] (s = 1794) -> 1.000000:(s' = 1083) ;
[] (s = 1795) -> 1.000000:(s' = 1083) ;
[] (s = 1795) -> 0.500000:(s' = 1939) + 0.500000:(s' = 1940);
[] (s = 1796) -> 1.000000:(s' = 433) ;
[] (s = 1797) -> 0.500000:(s' = 1941) + 0.500000:(s' = 1942);
[] (s = 1797) -> 1.000000:(s' = 1910) ;
[] (s = 1798) -> 1.000000:(s' = 1910) ;
[] (s = 1798) -> 0.500000:(s' = 1943) + 0.500000:(s' = 1944);
[] (s = 1799) -> 1.000000:(s' = 433) ;
[] (s = 1800) -> 1.000000:(s' = 433) ;
[] (s = 1801) -> 1.000000:(s' = 433) ;
[] (s = 1802) -> 1.000000:(s' = 433) ;
[] (s = 1803) -> 0.500000:(s' = 1945) + 0.500000:(s' = 1946);
[] (s = 1803) -> 1.000000:(s' = 1093) ;
[] (s = 1804) -> 1.000000:(s' = 1093) ;
[] (s = 1804) -> 0.500000:(s' = 1947) + 0.500000:(s' = 1948);
[] (s = 1805) -> 1.000000:(s' = 433) ;
[] (s = 1806) -> 1.000000:(s' = 433) ;
[] (s = 1807) -> 1.000000:(s' = 433) ;
[] (s = 1808) -> 0.500000:(s' = 1949) + 0.500000:(s' = 1950);
[] (s = 1808) -> 1.000000:(s' = 1102) ;
[] (s = 1809) -> 1.000000:(s' = 1102) ;
[] (s = 1809) -> 0.500000:(s' = 1951) + 0.500000:(s' = 1952);
[] (s = 1810) -> 1.000000:(s' = 433) ;
[] (s = 1811) -> 1.000000:(s' = 433) ;
[] (s = 1812) -> 1.000000:(s' = 433) ;
[] (s = 1813) -> 1.000000:(s' = 433) ;
[] (s = 1814) -> 0.500000:(s' = 1953) + 0.500000:(s' = 1954);
[] (s = 1814) -> 1.000000:(s' = 1102) ;
[] (s = 1815) -> 1.000000:(s' = 1102) ;
[] (s = 1815) -> 0.500000:(s' = 1955) + 0.500000:(s' = 1956);
[] (s = 1816) -> 1.000000:(s' = 433) ;
[] (s = 1817) -> 1.000000:(s' = 1957) ;
[] (s = 1818) -> 1.000000:(s' = 1958) ;
[] (s = 1819) -> 0.500000:(s' = 1959) + 0.500000:(s' = 1960);
[] (s = 1819) -> 0.500000:(s' = 1961) + 0.500000:(s' = 1962);
[] (s = 1820) -> 1.000000:(s' = 1963) ;
[] (s = 1821) -> 1.000000:(s' = 1964) ;
[] (s = 1822) -> 1.000000:(s' = 1965) ;
[] (s = 1823) -> 1.000000:(s' = 1966) ;
[] (s = 1824) -> 0.500000:(s' = 1959) + 0.500000:(s' = 1960);
[] (s = 1824) -> 0.500000:(s' = 1961) + 0.500000:(s' = 1962);
[] (s = 1825) -> 1.000000:(s' = 1967) ;
[] (s = 1826) -> 1.000000:(s' = 1968) ;
[] (s = 1827) -> 1.000000:(s' = 1969) ;
[] (s = 1828) -> 1.000000:(s' = 1970) ;
[] (s = 1829) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1829) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1830) -> 1.000000:(s' = 1975) ;
[] (s = 1831) -> 1.000000:(s' = 1976) ;
[] (s = 1832) -> 1.000000:(s' = 1977) ;
[] (s = 1833) -> 1.000000:(s' = 1978) ;
[] (s = 1834) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1834) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1835) -> 1.000000:(s' = 1979) ;
[] (s = 1836) -> 1.000000:(s' = 1980) ;
[] (s = 1837) -> 1.000000:(s' = 1981) ;
[] (s = 1838) -> 1.000000:(s' = 1982) ;
[] (s = 1839) -> 0.500000:(s' = 1959) + 0.500000:(s' = 1960);
[] (s = 1839) -> 0.500000:(s' = 1961) + 0.500000:(s' = 1962);
[] (s = 1840) -> 1.000000:(s' = 1983) ;
[] (s = 1841) -> 1.000000:(s' = 1984) ;
[] (s = 1842) -> 1.000000:(s' = 1985) ;
[] (s = 1843) -> 1.000000:(s' = 1986) ;
[] (s = 1844) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1844) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1845) -> 1.000000:(s' = 1987) ;
[] (s = 1846) -> 1.000000:(s' = 1988) ;
[] (s = 1847) -> 1.000000:(s' = 1989) ;
[] (s = 1848) -> 1.000000:(s' = 1990) ;
[] (s = 1849) -> 0.500000:(s' = 1959) + 0.500000:(s' = 1960);
[] (s = 1849) -> 0.500000:(s' = 1961) + 0.500000:(s' = 1962);
[] (s = 1850) -> 1.000000:(s' = 1991) ;
[] (s = 1851) -> 1.000000:(s' = 1992) ;
[] (s = 1852) -> 1.000000:(s' = 1993) ;
[] (s = 1853) -> 1.000000:(s' = 1994) ;
[] (s = 1854) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1854) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1855) -> 1.000000:(s' = 1995) ;
[] (s = 1856) -> 1.000000:(s' = 1996) ;
[] (s = 1857) -> 1.000000:(s' = 1969) ;
[] (s = 1858) -> 1.000000:(s' = 1970) ;
[] (s = 1859) -> 1.000000:(s' = 1975) ;
[] (s = 1860) -> 1.000000:(s' = 1976) ;
[] (s = 1861) -> 1.000000:(s' = 1997) ;
[] (s = 1862) -> 1.000000:(s' = 1998) ;
[] (s = 1863) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1863) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1864) -> 1.000000:(s' = 1999) ;
[] (s = 1865) -> 1.000000:(s' = 2000) ;
[] (s = 1866) -> 1.000000:(s' = 1177) ;
[] (s = 1867) -> 1.000000:(s' = 1178) ;
[] (s = 1868) -> 1.000000:(s' = 1183) ;
[] (s = 1869) -> 1.000000:(s' = 1184) ;
[] (s = 1870) -> 1.000000:(s' = 1185) ;
[] (s = 1871) -> 1.000000:(s' = 1186) ;
[] (s = 1872) -> 1.000000:(s' = 1187) ;
[] (s = 1873) -> 1.000000:(s' = 1188) ;
[] (s = 1874) -> 1.000000:(s' = 2001) ;
[] (s = 1875) -> 1.000000:(s' = 2002) ;
[] (s = 1876) -> 0.500000:(s' = 1971) + 0.500000:(s' = 1972);
[] (s = 1876) -> 0.500000:(s' = 1973) + 0.500000:(s' = 1974);
[] (s = 1877) -> 1.000000:(s' = 2003) ;
[] (s = 1878) -> 1.000000:(s' = 2004) ;
[] (s = 1879) -> 1.000000:(s' = 1193) ;
[] (s = 1880) -> 1.000000:(s' = 1194) ;
[] (s = 1881) -> 1.000000:(s' = 1195) ;
[] (s = 1882) -> 1.000000:(s' = 1196) ;
[] (s = 1883) -> 1.000000:(s' = 1993) ;
[] (s = 1884) -> 1.000000:(s' = 1994) ;
[] (s = 1885) -> 1.000000:(s' = 1995) ;
[] (s = 1886) -> 1.000000:(s' = 1996) ;
[] (s = 1887) -> 1.000000:(s' = 1197) ;
[] (s = 1888) -> 1.000000:(s' = 1198) ;
[] (s = 1889) -> 1.000000:(s' = 1199) ;
[] (s = 1890) -> 1.000000:(s' = 1200) ;
[] (s = 1891) -> 1.000000:(s' = 1177) ;
[] (s = 1892) -> 1.000000:(s' = 1178) ;
[] (s = 1893) -> 1.000000:(s' = 1183) ;
[] (s = 1894) -> 1.000000:(s' = 1184) ;
[] (s = 1895) -> 1.000000:(s' = 2005) ;
[] (s = 1896) -> 1.000000:(s' = 2006) ;
[] (s = 1897) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1897) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1898) -> 1.000000:(s' = 2007) ;
[] (s = 1899) -> 1.000000:(s' = 2008) ;
[] (s = 1900) -> 1.000000:(s' = 1177) ;
[] (s = 1901) -> 1.000000:(s' = 1178) ;
[] (s = 1902) -> 1.000000:(s' = 1183) ;
[] (s = 1903) -> 1.000000:(s' = 1184) ;
[] (s = 1904) -> 1.000000:(s' = 1185) ;
[] (s = 1905) -> 1.000000:(s' = 1186) ;
[] (s = 1906) -> 1.000000:(s' = 1187) ;
[] (s = 1907) -> 1.000000:(s' = 1188) ;
[] (s = 1908) -> 1.000000:(s' = 2009) ;
[] (s = 1909) -> 1.000000:(s' = 2010) ;
[] (s = 1910) -> 0.500000:(s' = 1179) + 0.500000:(s' = 1180);
[] (s = 1910) -> 0.500000:(s' = 1181) + 0.500000:(s' = 1182);
[] (s = 1911) -> 1.000000:(s' = 2011) ;
[] (s = 1912) -> 1.000000:(s' = 2012) ;
[] (s = 1913) -> 1.000000:(s' = 1193) ;
[] (s = 1914) -> 1.000000:(s' = 1194) ;
[] (s = 1915) -> 1.000000:(s' = 1195) ;
[] (s = 1916) -> 1.000000:(s' = 1196) ;
[] (s = 1917) -> 1.000000:(s' = 1197) ;
[] (s = 1918) -> 1.000000:(s' = 1198) ;
[] (s = 1919) -> 1.000000:(s' = 1199) ;
[] (s = 1920) -> 1.000000:(s' = 1200) ;
[] (s = 1921) -> 1.000000:(s' = 1197) ;
[] (s = 1922) -> 1.000000:(s' = 1198) ;
[] (s = 1923) -> 1.000000:(s' = 1199) ;
[] (s = 1924) -> 1.000000:(s' = 1200) ;
[] (s = 1925) -> 1.000000:(s' = 1177) ;
[] (s = 1926) -> 1.000000:(s' = 1178) ;
[] (s = 1927) -> 1.000000:(s' = 1183) ;
[] (s = 1928) -> 1.000000:(s' = 1184) ;
[] (s = 1929) -> 1.000000:(s' = 2005) ;
[] (s = 1930) -> 1.000000:(s' = 2006) ;
[] (s = 1931) -> 1.000000:(s' = 2007) ;
[] (s = 1932) -> 1.000000:(s' = 2008) ;
[] (s = 1933) -> 1.000000:(s' = 1177) ;
[] (s = 1934) -> 1.000000:(s' = 1178) ;
[] (s = 1935) -> 1.000000:(s' = 1183) ;
[] (s = 1936) -> 1.000000:(s' = 1184) ;
[] (s = 1937) -> 1.000000:(s' = 1185) ;
[] (s = 1938) -> 1.000000:(s' = 1186) ;
[] (s = 1939) -> 1.000000:(s' = 1187) ;
[] (s = 1940) -> 1.000000:(s' = 1188) ;
[] (s = 1941) -> 1.000000:(s' = 2009) ;
[] (s = 1942) -> 1.000000:(s' = 2010) ;
[] (s = 1943) -> 1.000000:(s' = 2011) ;
[] (s = 1944) -> 1.000000:(s' = 2012) ;
[] (s = 1945) -> 1.000000:(s' = 1193) ;
[] (s = 1946) -> 1.000000:(s' = 1194) ;
[] (s = 1947) -> 1.000000:(s' = 1195) ;
[] (s = 1948) -> 1.000000:(s' = 1196) ;
[] (s = 1949) -> 1.000000:(s' = 1197) ;
[] (s = 1950) -> 1.000000:(s' = 1198) ;
[] (s = 1951) -> 1.000000:(s' = 1199) ;
[] (s = 1952) -> 1.000000:(s' = 1200) ;
[] (s = 1953) -> 1.000000:(s' = 1197) ;
[] (s = 1954) -> 1.000000:(s' = 1198) ;
[] (s = 1955) -> 1.000000:(s' = 1199) ;
[] (s = 1956) -> 1.000000:(s' = 1200) ;
[] (s = 1957) -> 0.500000:(s' = 2013) + 0.500000:(s' = 2014);
[] (s = 1957) -> 1.000000:(s' = 2015) ;
[] (s = 1958) -> 0.500000:(s' = 2016) + 0.500000:(s' = 2017);
[] (s = 1958) -> 1.000000:(s' = 2018) ;
[] (s = 1959) -> 0.500000:(s' = 2019) + 0.500000:(s' = 2020);
[] (s = 1959) -> 1.000000:(s' = 2021) ;
[] (s = 1960) -> 0.500000:(s' = 2022) + 0.500000:(s' = 2023);
[] (s = 1960) -> 1.000000:(s' = 2024) ;
[] (s = 1961) -> 1.000000:(s' = 2025) ;
[] (s = 1961) -> 0.500000:(s' = 2019) + 0.500000:(s' = 2022);
[] (s = 1962) -> 1.000000:(s' = 2026) ;
[] (s = 1962) -> 0.500000:(s' = 2020) + 0.500000:(s' = 2023);
[] (s = 1963) -> 1.000000:(s' = 2027) ;
[] (s = 1963) -> 0.500000:(s' = 2028) + 0.500000:(s' = 2029);
[] (s = 1964) -> 1.000000:(s' = 2030) ;
[] (s = 1964) -> 0.500000:(s' = 2031) + 0.500000:(s' = 2032);
[] (s = 1965) -> 0.500000:(s' = 2013) + 0.500000:(s' = 2014);
[] (s = 1965) -> 1.000000:(s' = 2033) ;
[] (s = 1966) -> 0.500000:(s' = 2016) + 0.500000:(s' = 2017);
[] (s = 1966) -> 1.000000:(s' = 2034) ;
[] (s = 1967) -> 1.000000:(s' = 2035) ;
[] (s = 1967) -> 0.500000:(s' = 2028) + 0.500000:(s' = 2029);
[] (s = 1968) -> 1.000000:(s' = 2036) ;
[] (s = 1968) -> 0.500000:(s' = 2031) + 0.500000:(s' = 2032);
[] (s = 1969) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 1969) -> 1.000000:(s' = 2039) ;
[] (s = 1970) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 1970) -> 1.000000:(s' = 2042) ;
[] (s = 1971) -> 0.500000:(s' = 2043) + 0.500000:(s' = 2044);
[] (s = 1971) -> 1.000000:(s' = 2045) ;
[] (s = 1972) -> 0.500000:(s' = 2046) + 0.500000:(s' = 2047);
[] (s = 1972) -> 1.000000:(s' = 2048) ;
[] (s = 1973) -> 1.000000:(s' = 2049) ;
[] (s = 1973) -> 0.500000:(s' = 2043) + 0.500000:(s' = 2046);
[] (s = 1974) -> 1.000000:(s' = 2050) ;
[] (s = 1974) -> 0.500000:(s' = 2044) + 0.500000:(s' = 2047);
[] (s = 1975) -> 1.000000:(s' = 2051) ;
[] (s = 1975) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 1976) -> 1.000000:(s' = 2054) ;
[] (s = 1976) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 1977) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 1977) -> 1.000000:(s' = 2057) ;
[] (s = 1978) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 1978) -> 1.000000:(s' = 2058) ;
[] (s = 1979) -> 1.000000:(s' = 2059) ;
[] (s = 1979) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 1980) -> 1.000000:(s' = 2060) ;
[] (s = 1980) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 1981) -> 0.500000:(s' = 2013) + 0.500000:(s' = 2014);
[] (s = 1981) -> 1.000000:(s' = 2061) ;
[] (s = 1982) -> 0.500000:(s' = 2016) + 0.500000:(s' = 2017);
[] (s = 1982) -> 1.000000:(s' = 2062) ;
[] (s = 1983) -> 1.000000:(s' = 2063) ;
[] (s = 1983) -> 0.500000:(s' = 2028) + 0.500000:(s' = 2029);
[] (s = 1984) -> 1.000000:(s' = 2064) ;
[] (s = 1984) -> 0.500000:(s' = 2031) + 0.500000:(s' = 2032);
[] (s = 1985) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 1985) -> 1.000000:(s' = 2065) ;
[] (s = 1986) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 1986) -> 1.000000:(s' = 2066) ;
[] (s = 1987) -> 1.000000:(s' = 2067) ;
[] (s = 1987) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 1988) -> 1.000000:(s' = 2068) ;
[] (s = 1988) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 1989) -> 0.500000:(s' = 2013) + 0.500000:(s' = 2014);
[] (s = 1989) -> 1.000000:(s' = 2069) ;
[] (s = 1990) -> 0.500000:(s' = 2016) + 0.500000:(s' = 2017);
[] (s = 1990) -> 1.000000:(s' = 2070) ;
[] (s = 1991) -> 1.000000:(s' = 2071) ;
[] (s = 1991) -> 0.500000:(s' = 2028) + 0.500000:(s' = 2029);
[] (s = 1992) -> 1.000000:(s' = 2072) ;
[] (s = 1992) -> 0.500000:(s' = 2031) + 0.500000:(s' = 2032);
[] (s = 1993) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 1993) -> 1.000000:(s' = 2073) ;
[] (s = 1994) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 1994) -> 1.000000:(s' = 2074) ;
[] (s = 1995) -> 1.000000:(s' = 2075) ;
[] (s = 1995) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 1996) -> 1.000000:(s' = 2076) ;
[] (s = 1996) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 1997) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 1997) -> 1.000000:(s' = 2077) ;
[] (s = 1998) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 1998) -> 1.000000:(s' = 2078) ;
[] (s = 1999) -> 1.000000:(s' = 2079) ;
[] (s = 1999) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 2000) -> 1.000000:(s' = 2080) ;
[] (s = 2000) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 2001) -> 0.500000:(s' = 2037) + 0.500000:(s' = 2038);
[] (s = 2001) -> 1.000000:(s' = 2081) ;
[] (s = 2002) -> 0.500000:(s' = 2040) + 0.500000:(s' = 2041);
[] (s = 2002) -> 1.000000:(s' = 2082) ;
[] (s = 2003) -> 1.000000:(s' = 2083) ;
[] (s = 2003) -> 0.500000:(s' = 2052) + 0.500000:(s' = 2053);
[] (s = 2004) -> 1.000000:(s' = 2084) ;
[] (s = 2004) -> 0.500000:(s' = 2055) + 0.500000:(s' = 2056);
[] (s = 2005) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 2005) -> 1.000000:(s' = 2085) ;
[] (s = 2006) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 2006) -> 1.000000:(s' = 2086) ;
[] (s = 2007) -> 1.000000:(s' = 2087) ;
[] (s = 2007) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 2008) -> 1.000000:(s' = 2088) ;
[] (s = 2008) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 2009) -> 0.500000:(s' = 1309) + 0.500000:(s' = 1310);
[] (s = 2009) -> 1.000000:(s' = 2089) ;
[] (s = 2010) -> 0.500000:(s' = 1312) + 0.500000:(s' = 1313);
[] (s = 2010) -> 1.000000:(s' = 2090) ;
[] (s = 2011) -> 1.000000:(s' = 2091) ;
[] (s = 2011) -> 0.500000:(s' = 1324) + 0.500000:(s' = 1325);
[] (s = 2012) -> 1.000000:(s' = 2092) ;
[] (s = 2012) -> 0.500000:(s' = 1327) + 0.500000:(s' = 1328);
[] (s = 2013) -> 1.000000:(s' = 2093) ;
[] (s = 2013) -> 1.000000:(s' = 2094) ;
[] (s = 2014) -> 1.000000:(s' = 2095) ;
[] (s = 2014) -> 1.000000:(s' = 2096) ;
[] (s = 2015) -> 0.500000:(s' = 2094) + 0.500000:(s' = 2096);
[] (s = 2016) -> 1.000000:(s' = 2097) ;
[] (s = 2016) -> 1.000000:(s' = 2098) ;
[] (s = 2017) -> 1.000000:(s' = 2099) ;
[] (s = 2017) -> 1.000000:(s' = 2100) ;
[] (s = 2018) -> 0.500000:(s' = 2098) + 0.500000:(s' = 2100);
[] (s = 2019) -> 1.000000:(s' = 2101) ;
[] (s = 2019) -> 1.000000:(s' = 2102) ;
[] (s = 2020) -> 1.000000:(s' = 2103) ;
[] (s = 2020) -> 1.000000:(s' = 2104) ;
[] (s = 2021) -> 0.500000:(s' = 2102) + 0.500000:(s' = 2104);
[] (s = 2022) -> 1.000000:(s' = 2105) ;
[] (s = 2022) -> 1.000000:(s' = 2106) ;
[] (s = 2023) -> 1.000000:(s' = 2107) ;
[] (s = 2023) -> 1.000000:(s' = 2108) ;
[] (s = 2024) -> 0.500000:(s' = 2106) + 0.500000:(s' = 2108);
[] (s = 2025) -> 0.500000:(s' = 2101) + 0.500000:(s' = 2105);
[] (s = 2026) -> 0.500000:(s' = 2103) + 0.500000:(s' = 2107);
[] (s = 2027) -> 0.500000:(s' = 2109) + 0.500000:(s' = 2110);
[] (s = 2028) -> 1.000000:(s' = 2109) ;
[] (s = 2028) -> 1.000000:(s' = 2111) ;
[] (s = 2029) -> 1.000000:(s' = 2110) ;
[] (s = 2029) -> 1.000000:(s' = 2112) ;
[] (s = 2030) -> 0.500000:(s' = 2113) + 0.500000:(s' = 2114);
[] (s = 2031) -> 1.000000:(s' = 2113) ;
[] (s = 2031) -> 1.000000:(s' = 2115) ;
[] (s = 2032) -> 1.000000:(s' = 2114) ;
[] (s = 2032) -> 1.000000:(s' = 2116) ;
[] (s = 2033) -> 0.500000:(s' = 2094) + 0.500000:(s' = 2096);
[] (s = 2034) -> 0.500000:(s' = 2098) + 0.500000:(s' = 2100);
[] (s = 2035) -> 0.500000:(s' = 2109) + 0.500000:(s' = 2110);
[] (s = 2036) -> 0.500000:(s' = 2113) + 0.500000:(s' = 2114);
[] (s = 2037) -> 1.000000:(s' = 2117) ;
[] (s = 2037) -> 1.000000:(s' = 2118) ;
[] (s = 2038) -> 1.000000:(s' = 2119) ;
[] (s = 2038) -> 1.000000:(s' = 2120) ;
[] (s = 2039) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2040) -> 1.000000:(s' = 2121) ;
[] (s = 2040) -> 1.000000:(s' = 2122) ;
[] (s = 2041) -> 1.000000:(s' = 2123) ;
[] (s = 2041) -> 1.000000:(s' = 2124) ;
[] (s = 2042) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2043) -> 1.000000:(s' = 2125) ;
[] (s = 2043) -> 1.000000:(s' = 2126) ;
[] (s = 2044) -> 1.000000:(s' = 2127) ;
[] (s = 2044) -> 1.000000:(s' = 2128) ;
[] (s = 2045) -> 0.500000:(s' = 2126) + 0.500000:(s' = 2128);
[] (s = 2046) -> 1.000000:(s' = 2129) ;
[] (s = 2046) -> 1.000000:(s' = 2130) ;
[] (s = 2047) -> 1.000000:(s' = 2131) ;
[] (s = 2047) -> 1.000000:(s' = 2132) ;
[] (s = 2048) -> 0.500000:(s' = 2130) + 0.500000:(s' = 2132);
[] (s = 2049) -> 0.500000:(s' = 2125) + 0.500000:(s' = 2129);
[] (s = 2050) -> 0.500000:(s' = 2127) + 0.500000:(s' = 2131);
[] (s = 2051) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2052) -> 1.000000:(s' = 2133) ;
[] (s = 2052) -> 1.000000:(s' = 2135) ;
[] (s = 2053) -> 1.000000:(s' = 2134) ;
[] (s = 2053) -> 1.000000:(s' = 2136) ;
[] (s = 2054) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2055) -> 1.000000:(s' = 2137) ;
[] (s = 2055) -> 1.000000:(s' = 2139) ;
[] (s = 2056) -> 1.000000:(s' = 2138) ;
[] (s = 2056) -> 1.000000:(s' = 2140) ;
[] (s = 2057) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2058) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2059) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2060) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2061) -> 0.500000:(s' = 2094) + 0.500000:(s' = 2096);
[] (s = 2062) -> 0.500000:(s' = 2098) + 0.500000:(s' = 2100);
[] (s = 2063) -> 0.500000:(s' = 2109) + 0.500000:(s' = 2110);
[] (s = 2064) -> 0.500000:(s' = 2113) + 0.500000:(s' = 2114);
[] (s = 2065) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2066) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2067) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2068) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2069) -> 0.500000:(s' = 2094) + 0.500000:(s' = 2096);
[] (s = 2070) -> 0.500000:(s' = 2098) + 0.500000:(s' = 2100);
[] (s = 2071) -> 0.500000:(s' = 2109) + 0.500000:(s' = 2110);
[] (s = 2072) -> 0.500000:(s' = 2113) + 0.500000:(s' = 2114);
[] (s = 2073) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2074) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2075) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2076) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2077) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2078) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2079) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2080) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2081) -> 0.500000:(s' = 2118) + 0.500000:(s' = 2120);
[] (s = 2082) -> 0.500000:(s' = 2122) + 0.500000:(s' = 2124);
[] (s = 2083) -> 0.500000:(s' = 2133) + 0.500000:(s' = 2134);
[] (s = 2084) -> 0.500000:(s' = 2137) + 0.500000:(s' = 2138);
[] (s = 2085) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 2086) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 2087) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 2088) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 2089) -> 0.500000:(s' = 1418) + 0.500000:(s' = 1420);
[] (s = 2090) -> 0.500000:(s' = 1422) + 0.500000:(s' = 1424);
[] (s = 2091) -> 0.500000:(s' = 1433) + 0.500000:(s' = 1434);
[] (s = 2092) -> 0.500000:(s' = 1437) + 0.500000:(s' = 1438);
[] (s = 2093) -> 1.000000:(s' = 2141) ;
[] (s = 2094) -> 1.000000:(s' = 2141) ;
[] (s = 2095) -> 1.000000:(s' = 2142) ;
[] (s = 2096) -> 1.000000:(s' = 2142) ;
[] (s = 2097) -> 1.000000:(s' = 2143) ;
[] (s = 2098) -> 1.000000:(s' = 2143) ;
[] (s = 2099) -> 1.000000:(s' = 2144) ;
[] (s = 2100) -> 1.000000:(s' = 2144) ;
[] (s = 2101) -> 1.000000:(s' = 2145) ;
[] (s = 2102) -> 1.000000:(s' = 2145) ;
[] (s = 2103) -> 1.000000:(s' = 2146) ;
[] (s = 2104) -> 1.000000:(s' = 2146) ;
[] (s = 2105) -> 1.000000:(s' = 2147) ;
[] (s = 2106) -> 1.000000:(s' = 2147) ;
[] (s = 2107) -> 1.000000:(s' = 2148) ;
[] (s = 2108) -> 1.000000:(s' = 2148) ;
[] (s = 2109) -> 1.000000:(s' = 2149) ;
[] (s = 2110) -> 1.000000:(s' = 2150) ;
[] (s = 2111) -> 1.000000:(s' = 2149) ;
[] (s = 2112) -> 1.000000:(s' = 2150) ;
[] (s = 2113) -> 1.000000:(s' = 2151) ;
[] (s = 2114) -> 1.000000:(s' = 2152) ;
[] (s = 2115) -> 1.000000:(s' = 2151) ;
[] (s = 2116) -> 1.000000:(s' = 2152) ;
[] (s = 2117) -> 1.000000:(s' = 2153) ;
[] (s = 2118) -> 1.000000:(s' = 2153) ;
[] (s = 2119) -> 1.000000:(s' = 2154) ;
[] (s = 2120) -> 1.000000:(s' = 2154) ;
[] (s = 2121) -> 1.000000:(s' = 2155) ;
[] (s = 2122) -> 1.000000:(s' = 2155) ;
[] (s = 2123) -> 1.000000:(s' = 2156) ;
[] (s = 2124) -> 1.000000:(s' = 2156) ;
[] (s = 2125) -> 1.000000:(s' = 2157) ;
[] (s = 2126) -> 1.000000:(s' = 2157) ;
[] (s = 2127) -> 1.000000:(s' = 2158) ;
[] (s = 2128) -> 1.000000:(s' = 2158) ;
[] (s = 2129) -> 1.000000:(s' = 2159) ;
[] (s = 2130) -> 1.000000:(s' = 2159) ;
[] (s = 2131) -> 1.000000:(s' = 2160) ;
[] (s = 2132) -> 1.000000:(s' = 2160) ;
[] (s = 2133) -> 1.000000:(s' = 2161) ;
[] (s = 2134) -> 1.000000:(s' = 2162) ;
[] (s = 2135) -> 1.000000:(s' = 2161) ;
[] (s = 2136) -> 1.000000:(s' = 2162) ;
[] (s = 2137) -> 1.000000:(s' = 2163) ;
[] (s = 2138) -> 1.000000:(s' = 2164) ;
[] (s = 2139) -> 1.000000:(s' = 2163) ;
[] (s = 2140) -> 1.000000:(s' = 2164) ;
[] (s = 2141) -> 1.000000:(s' = 2165) ;
[] (s = 2141) -> 1.000000:(s' = 2166) ;
[] (s = 2142) -> 1.000000:(s' = 2167) ;
[] (s = 2143) -> 1.000000:(s' = 2168) ;
[] (s = 2144) -> 1.000000:(s' = 2169) ;
[] (s = 2144) -> 1.000000:(s' = 2170) ;
[] (s = 2145) -> 1.000000:(s' = 2171) ;
[] (s = 2145) -> 1.000000:(s' = 2172) ;
[] (s = 2146) -> 1.000000:(s' = 2173) ;
[] (s = 2147) -> 1.000000:(s' = 2174) ;
[] (s = 2148) -> 1.000000:(s' = 2175) ;
[] (s = 2148) -> 1.000000:(s' = 2176) ;
[] (s = 2149) -> 1.000000:(s' = 2177) ;
[] (s = 2149) -> 1.000000:(s' = 2178) ;
[] (s = 2150) -> 1.000000:(s' = 2179) ;
[] (s = 2151) -> 1.000000:(s' = 2180) ;
[] (s = 2152) -> 1.000000:(s' = 2181) ;
[] (s = 2152) -> 1.000000:(s' = 2182) ;
[] (s = 2153) -> 1.000000:(s' = 2183) ;
[] (s = 2153) -> 1.000000:(s' = 2184) ;
[] (s = 2154) -> 1.000000:(s' = 2185) ;
[] (s = 2155) -> 1.000000:(s' = 2186) ;
[] (s = 2156) -> 1.000000:(s' = 2187) ;
[] (s = 2156) -> 1.000000:(s' = 2188) ;
[] (s = 2157) -> 1.000000:(s' = 2189) ;
[] (s = 2157) -> 1.000000:(s' = 2190) ;
[] (s = 2158) -> 1.000000:(s' = 2191) ;
[] (s = 2159) -> 1.000000:(s' = 2192) ;
[] (s = 2160) -> 1.000000:(s' = 2193) ;
[] (s = 2160) -> 1.000000:(s' = 2194) ;
[] (s = 2161) -> 1.000000:(s' = 2195) ;
[] (s = 2161) -> 1.000000:(s' = 2196) ;
[] (s = 2162) -> 1.000000:(s' = 2197) ;
[] (s = 2163) -> 1.000000:(s' = 2198) ;
[] (s = 2164) -> 1.000000:(s' = 2199) ;
[] (s = 2164) -> 1.000000:(s' = 2200) ;
[] (s = 2165) -> 1.000000:(s' = 2201) ;
[] (s = 2165) -> 1.000000:(s' = 2202) ;
[] (s = 2166) -> 1.000000:(s' = 2203) ;
[] (s = 2166) -> 1.000000:(s' = 2204) ;
[] (s = 2167) -> 1.000000:(s' = 2205) ;
[] (s = 2168) -> 1.000000:(s' = 2206) ;
[] (s = 2169) -> 1.000000:(s' = 2207) ;
[] (s = 2169) -> 1.000000:(s' = 2208) ;
[] (s = 2170) -> 1.000000:(s' = 2209) ;
[] (s = 2170) -> 1.000000:(s' = 2210) ;
[] (s = 2171) -> 1.000000:(s' = 2211) ;
[] (s = 2171) -> 1.000000:(s' = 2212) ;
[] (s = 2172) -> 1.000000:(s' = 2213) ;
[] (s = 2172) -> 1.000000:(s' = 2214) ;
[] (s = 2173) -> 1.000000:(s' = 2215) ;
[] (s = 2174) -> 1.000000:(s' = 2216) ;
[] (s = 2175) -> 1.000000:(s' = 2217) ;
[] (s = 2175) -> 1.000000:(s' = 2218) ;
[] (s = 2176) -> 1.000000:(s' = 2219) ;
[] (s = 2176) -> 1.000000:(s' = 2220) ;
[] (s = 2177) -> 1.000000:(s' = 2221) ;
[] (s = 2177) -> 1.000000:(s' = 2222) ;
[] (s = 2178) -> 1.000000:(s' = 2223) ;
[] (s = 2178) -> 1.000000:(s' = 2224) ;
[] (s = 2179) -> 1.000000:(s' = 2225) ;
[] (s = 2180) -> 1.000000:(s' = 2226) ;
[] (s = 2181) -> 1.000000:(s' = 2227) ;
[] (s = 2181) -> 1.000000:(s' = 2228) ;
[] (s = 2182) -> 1.000000:(s' = 2229) ;
[] (s = 2182) -> 1.000000:(s' = 2230) ;
[] (s = 2183) -> 1.000000:(s' = 2231) ;
[] (s = 2183) -> 1.000000:(s' = 2232) ;
[] (s = 2184) -> 1.000000:(s' = 2233) ;
[] (s = 2184) -> 1.000000:(s' = 2234) ;
[] (s = 2185) -> 1.000000:(s' = 2235) ;
[] (s = 2186) -> 1.000000:(s' = 2236) ;
[] (s = 2187) -> 1.000000:(s' = 2237) ;
[] (s = 2187) -> 1.000000:(s' = 2238) ;
[] (s = 2188) -> 1.000000:(s' = 2239) ;
[] (s = 2188) -> 1.000000:(s' = 2240) ;
[] (s = 2189) -> 1.000000:(s' = 2241) ;
[] (s = 2189) -> 1.000000:(s' = 2242) ;
[] (s = 2190) -> 1.000000:(s' = 2243) ;
[] (s = 2190) -> 1.000000:(s' = 2244) ;
[] (s = 2191) -> 1.000000:(s' = 2245) ;
[] (s = 2192) -> 1.000000:(s' = 2246) ;
[] (s = 2193) -> 1.000000:(s' = 2247) ;
[] (s = 2193) -> 1.000000:(s' = 2248) ;
[] (s = 2194) -> 1.000000:(s' = 2249) ;
[] (s = 2194) -> 1.000000:(s' = 2250) ;
[] (s = 2195) -> 1.000000:(s' = 2251) ;
[] (s = 2195) -> 1.000000:(s' = 2252) ;
[] (s = 2196) -> 1.000000:(s' = 2253) ;
[] (s = 2196) -> 1.000000:(s' = 2254) ;
[] (s = 2197) -> 1.000000:(s' = 2255) ;
[] (s = 2198) -> 1.000000:(s' = 2256) ;
[] (s = 2199) -> 1.000000:(s' = 2257) ;
[] (s = 2199) -> 1.000000:(s' = 2258) ;
[] (s = 2200) -> 1.000000:(s' = 2259) ;
[] (s = 2200) -> 1.000000:(s' = 2260) ;
[] (s = 2201) -> 1.000000:(s' = 2261) ;
[] (s = 2201) -> 1.000000:(s' = 2262) ;
[] (s = 2202) -> 1.000000:(s' = 2263) ;
[] (s = 2203) -> 1.000000:(s' = 2264) ;
[] (s = 2203) -> 1.000000:(s' = 2265) ;
[] (s = 2204) -> 1.000000:(s' = 2266) ;
[] (s = 2205) -> 1.000000:(s' = 2267) ;
[] (s = 2206) -> 1.000000:(s' = 2268) ;
[] (s = 2207) -> 1.000000:(s' = 2269) ;
[] (s = 2207) -> 1.000000:(s' = 2270) ;
[] (s = 2208) -> 1.000000:(s' = 2271) ;
[] (s = 2209) -> 1.000000:(s' = 2272) ;
[] (s = 2209) -> 1.000000:(s' = 2273) ;
[] (s = 2210) -> 1.000000:(s' = 2274) ;
[] (s = 2211) -> 1.000000:(s' = 2275) ;
[] (s = 2211) -> 1.000000:(s' = 2276) ;
[] (s = 2212) -> 1.000000:(s' = 2277) ;
[] (s = 2213) -> 1.000000:(s' = 2264) ;
[] (s = 2213) -> 1.000000:(s' = 2265) ;
[] (s = 2214) -> 1.000000:(s' = 2278) ;
[] (s = 2215) -> 1.000000:(s' = 2279) ;
[] (s = 2216) -> 1.000000:(s' = 2280) ;
[] (s = 2217) -> 1.000000:(s' = 2281) ;
[] (s = 2217) -> 1.000000:(s' = 2282) ;
[] (s = 2218) -> 1.000000:(s' = 2283) ;
[] (s = 2219) -> 1.000000:(s' = 2272) ;
[] (s = 2219) -> 1.000000:(s' = 2273) ;
[] (s = 2220) -> 1.000000:(s' = 2284) ;
[] (s = 2221) -> 1.000000:(s' = 2275) ;
[] (s = 2221) -> 1.000000:(s' = 2276) ;
[] (s = 2222) -> 1.000000:(s' = 2285) ;
[] (s = 2223) -> 1.000000:(s' = 2286) ;
[] (s = 2223) -> 1.000000:(s' = 2287) ;
[] (s = 2224) -> 1.000000:(s' = 2288) ;
[] (s = 2225) -> 1.000000:(s' = 2289) ;
[] (s = 2226) -> 1.000000:(s' = 2290) ;
[] (s = 2227) -> 1.000000:(s' = 2281) ;
[] (s = 2227) -> 1.000000:(s' = 2282) ;
[] (s = 2228) -> 1.000000:(s' = 2291) ;
[] (s = 2229) -> 1.000000:(s' = 2292) ;
[] (s = 2229) -> 1.000000:(s' = 2293) ;
[] (s = 2230) -> 1.000000:(s' = 2294) ;
[] (s = 2231) -> 1.000000:(s' = 2295) ;
[] (s = 2231) -> 1.000000:(s' = 2296) ;
[] (s = 2232) -> 1.000000:(s' = 2297) ;
[] (s = 2233) -> 1.000000:(s' = 2298) ;
[] (s = 2233) -> 1.000000:(s' = 2299) ;
[] (s = 2234) -> 1.000000:(s' = 2300) ;
[] (s = 2235) -> 1.000000:(s' = 2301) ;
[] (s = 2236) -> 1.000000:(s' = 2302) ;
[] (s = 2237) -> 1.000000:(s' = 2303) ;
[] (s = 2237) -> 1.000000:(s' = 2304) ;
[] (s = 2238) -> 1.000000:(s' = 2305) ;
[] (s = 2239) -> 1.000000:(s' = 2306) ;
[] (s = 2239) -> 1.000000:(s' = 2307) ;
[] (s = 2240) -> 1.000000:(s' = 2308) ;
[] (s = 2241) -> 1.000000:(s' = 2309) ;
[] (s = 2241) -> 1.000000:(s' = 2310) ;
[] (s = 2242) -> 1.000000:(s' = 2311) ;
[] (s = 2243) -> 1.000000:(s' = 2298) ;
[] (s = 2243) -> 1.000000:(s' = 2299) ;
[] (s = 2244) -> 1.000000:(s' = 2312) ;
[] (s = 2245) -> 1.000000:(s' = 2313) ;
[] (s = 2246) -> 1.000000:(s' = 2314) ;
[] (s = 2247) -> 1.000000:(s' = 2315) ;
[] (s = 2247) -> 1.000000:(s' = 2316) ;
[] (s = 2248) -> 1.000000:(s' = 2317) ;
[] (s = 2249) -> 1.000000:(s' = 2306) ;
[] (s = 2249) -> 1.000000:(s' = 2307) ;
[] (s = 2250) -> 1.000000:(s' = 2318) ;
[] (s = 2251) -> 1.000000:(s' = 2309) ;
[] (s = 2251) -> 1.000000:(s' = 2310) ;
[] (s = 2252) -> 1.000000:(s' = 2319) ;
[] (s = 2253) -> 1.000000:(s' = 2320) ;
[] (s = 2253) -> 1.000000:(s' = 2321) ;
[] (s = 2254) -> 1.000000:(s' = 2322) ;
[] (s = 2255) -> 1.000000:(s' = 2323) ;
[] (s = 2256) -> 1.000000:(s' = 2324) ;
[] (s = 2257) -> 1.000000:(s' = 2315) ;
[] (s = 2257) -> 1.000000:(s' = 2316) ;
[] (s = 2258) -> 1.000000:(s' = 2325) ;
[] (s = 2259) -> 1.000000:(s' = 2326) ;
[] (s = 2259) -> 1.000000:(s' = 2327) ;
[] (s = 2260) -> 1.000000:(s' = 2328) ;
[] (s = 2261) -> 0.500000:(s' = 2329) + 0.500000:(s' = 2330);
[] (s = 2261) -> 1.000000:(s' = 2331) ;
[] (s = 2262) -> 1.000000:(s' = 2331) ;
[] (s = 2262) -> 0.500000:(s' = 2332) + 0.500000:(s' = 2333);
[] (s = 2263) -> 1.000000:(s' = 60) ;
[] (s = 2263) -> 1.000000:(s' = 433) ;
[] (s = 2264) -> 0.500000:(s' = 2334) + 0.500000:(s' = 2335);
[] (s = 2264) -> 1.000000:(s' = 2336) ;
[] (s = 2265) -> 1.000000:(s' = 2336) ;
[] (s = 2265) -> 0.500000:(s' = 2337) + 0.500000:(s' = 2338);
[] (s = 2266) -> 1.000000:(s' = 60) ;
[] (s = 2266) -> 1.000000:(s' = 433) ;
[] (s = 2267) -> 1.000000:(s' = 433) ;
[] (s = 2268) -> 1.000000:(s' = 433) ;
[] (s = 2269) -> 0.500000:(s' = 2339) + 0.500000:(s' = 2340);
[] (s = 2269) -> 1.000000:(s' = 1078) ;
[] (s = 2270) -> 1.000000:(s' = 1078) ;
[] (s = 2270) -> 0.500000:(s' = 2341) + 0.500000:(s' = 2342);
[] (s = 2271) -> 1.000000:(s' = 433) ;
[] (s = 2272) -> 0.500000:(s' = 2343) + 0.500000:(s' = 2344);
[] (s = 2272) -> 1.000000:(s' = 1083) ;
[] (s = 2273) -> 1.000000:(s' = 1083) ;
[] (s = 2273) -> 0.500000:(s' = 2345) + 0.500000:(s' = 2346);
[] (s = 2274) -> 1.000000:(s' = 433) ;
[] (s = 2275) -> 0.500000:(s' = 2347) + 0.500000:(s' = 2348);
[] (s = 2275) -> 1.000000:(s' = 2349) ;
[] (s = 2276) -> 1.000000:(s' = 2349) ;
[] (s = 2276) -> 0.500000:(s' = 2350) + 0.500000:(s' = 2351);
[] (s = 2277) -> 1.000000:(s' = 60) ;
[] (s = 2277) -> 1.000000:(s' = 433) ;
[] (s = 2278) -> 1.000000:(s' = 60) ;
[] (s = 2278) -> 1.000000:(s' = 433) ;
[] (s = 2279) -> 1.000000:(s' = 433) ;
[] (s = 2280) -> 1.000000:(s' = 433) ;
[] (s = 2281) -> 0.500000:(s' = 2352) + 0.500000:(s' = 2353);
[] (s = 2281) -> 1.000000:(s' = 1093) ;
[] (s = 2282) -> 1.000000:(s' = 1093) ;
[] (s = 2282) -> 0.500000:(s' = 2354) + 0.500000:(s' = 2355);
[] (s = 2283) -> 1.000000:(s' = 433) ;
[] (s = 2284) -> 1.000000:(s' = 433) ;
[] (s = 2285) -> 1.000000:(s' = 60) ;
[] (s = 2285) -> 1.000000:(s' = 433) ;
[] (s = 2286) -> 0.500000:(s' = 2356) + 0.500000:(s' = 2357);
[] (s = 2286) -> 1.000000:(s' = 2358) ;
[] (s = 2287) -> 1.000000:(s' = 2358) ;
[] (s = 2287) -> 0.500000:(s' = 2359) + 0.500000:(s' = 2360);
[] (s = 2288) -> 1.000000:(s' = 60) ;
[] (s = 2288) -> 1.000000:(s' = 433) ;
[] (s = 2289) -> 1.000000:(s' = 433) ;
[] (s = 2290) -> 1.000000:(s' = 433) ;
[] (s = 2291) -> 1.000000:(s' = 433) ;
[] (s = 2292) -> 0.500000:(s' = 2361) + 0.500000:(s' = 2362);
[] (s = 2292) -> 1.000000:(s' = 1102) ;
[] (s = 2293) -> 1.000000:(s' = 1102) ;
[] (s = 2293) -> 0.500000:(s' = 2363) + 0.500000:(s' = 2364);
[] (s = 2294) -> 1.000000:(s' = 433) ;
[] (s = 2295) -> 0.500000:(s' = 2365) + 0.500000:(s' = 2366);
[] (s = 2295) -> 1.000000:(s' = 1078) ;
[] (s = 2296) -> 1.000000:(s' = 1078) ;
[] (s = 2296) -> 0.500000:(s' = 2367) + 0.500000:(s' = 2368);
[] (s = 2297) -> 1.000000:(s' = 433) ;
[] (s = 2298) -> 0.500000:(s' = 2369) + 0.500000:(s' = 2370);
[] (s = 2298) -> 1.000000:(s' = 1897) ;
[] (s = 2299) -> 1.000000:(s' = 1897) ;
[] (s = 2299) -> 0.500000:(s' = 2371) + 0.500000:(s' = 2372);
[] (s = 2300) -> 1.000000:(s' = 433) ;
[] (s = 2301) -> 1.000000:(s' = 433) ;
[] (s = 2302) -> 1.000000:(s' = 433) ;
[] (s = 2303) -> 0.500000:(s' = 2373) + 0.500000:(s' = 2374);
[] (s = 2303) -> 1.000000:(s' = 1078) ;
[] (s = 2304) -> 1.000000:(s' = 1078) ;
[] (s = 2304) -> 0.500000:(s' = 2375) + 0.500000:(s' = 2376);
[] (s = 2305) -> 1.000000:(s' = 433) ;
[] (s = 2306) -> 0.500000:(s' = 2377) + 0.500000:(s' = 2378);
[] (s = 2306) -> 1.000000:(s' = 1083) ;
[] (s = 2307) -> 1.000000:(s' = 1083) ;
[] (s = 2307) -> 0.500000:(s' = 2379) + 0.500000:(s' = 2380);
[] (s = 2308) -> 1.000000:(s' = 433) ;
[] (s = 2309) -> 0.500000:(s' = 2381) + 0.500000:(s' = 2382);
[] (s = 2309) -> 1.000000:(s' = 1910) ;
[] (s = 2310) -> 1.000000:(s' = 1910) ;
[] (s = 2310) -> 0.500000:(s' = 2383) + 0.500000:(s' = 2384);
[] (s = 2311) -> 1.000000:(s' = 433) ;
[] (s = 2312) -> 1.000000:(s' = 433) ;
[] (s = 2313) -> 1.000000:(s' = 433) ;
[] (s = 2314) -> 1.000000:(s' = 433) ;
[] (s = 2315) -> 0.500000:(s' = 2385) + 0.500000:(s' = 2386);
[] (s = 2315) -> 1.000000:(s' = 1093) ;
[] (s = 2316) -> 1.000000:(s' = 1093) ;
[] (s = 2316) -> 0.500000:(s' = 2387) + 0.500000:(s' = 2388);
[] (s = 2317) -> 1.000000:(s' = 433) ;
[] (s = 2318) -> 1.000000:(s' = 433) ;
[] (s = 2319) -> 1.000000:(s' = 433) ;
[] (s = 2320) -> 0.500000:(s' = 2389) + 0.500000:(s' = 2390);
[] (s = 2320) -> 1.000000:(s' = 1102) ;
[] (s = 2321) -> 1.000000:(s' = 1102) ;
[] (s = 2321) -> 0.500000:(s' = 2391) + 0.500000:(s' = 2392);
[] (s = 2322) -> 1.000000:(s' = 433) ;
[] (s = 2323) -> 1.000000:(s' = 433) ;
[] (s = 2324) -> 1.000000:(s' = 433) ;
[] (s = 2325) -> 1.000000:(s' = 433) ;
[] (s = 2326) -> 0.500000:(s' = 2393) + 0.500000:(s' = 2394);
[] (s = 2326) -> 1.000000:(s' = 1102) ;
[] (s = 2327) -> 1.000000:(s' = 1102) ;
[] (s = 2327) -> 0.500000:(s' = 2395) + 0.500000:(s' = 2396);
[] (s = 2328) -> 1.000000:(s' = 433) ;
[] (s = 2329) -> 1.000000:(s' = 2397) ;
[] (s = 2330) -> 1.000000:(s' = 2398) ;
[] (s = 2331) -> 0.500000:(s' = 2399) + 0.500000:(s' = 2400);
[] (s = 2331) -> 0.500000:(s' = 2401) + 0.500000:(s' = 2402);
[] (s = 2332) -> 1.000000:(s' = 2403) ;
[] (s = 2333) -> 1.000000:(s' = 2404) ;
[] (s = 2334) -> 1.000000:(s' = 2405) ;
[] (s = 2335) -> 1.000000:(s' = 2406) ;
[] (s = 2336) -> 0.500000:(s' = 2399) + 0.500000:(s' = 2400);
[] (s = 2336) -> 0.500000:(s' = 2401) + 0.500000:(s' = 2402);
[] (s = 2337) -> 1.000000:(s' = 2407) ;
[] (s = 2338) -> 1.000000:(s' = 2408) ;
[] (s = 2339) -> 1.000000:(s' = 1177) ;
[] (s = 2340) -> 1.000000:(s' = 1178) ;
[] (s = 2341) -> 1.000000:(s' = 1183) ;
[] (s = 2342) -> 1.000000:(s' = 1184) ;
[] (s = 2343) -> 1.000000:(s' = 1185) ;
[] (s = 2344) -> 1.000000:(s' = 1186) ;
[] (s = 2345) -> 1.000000:(s' = 1187) ;
[] (s = 2346) -> 1.000000:(s' = 1188) ;
[] (s = 2347) -> 1.000000:(s' = 2409) ;
[] (s = 2348) -> 1.000000:(s' = 2410) ;
[] (s = 2349) -> 0.500000:(s' = 2399) + 0.500000:(s' = 2400);
[] (s = 2349) -> 0.500000:(s' = 2401) + 0.500000:(s' = 2402);
[] (s = 2350) -> 1.000000:(s' = 2411) ;
[] (s = 2351) -> 1.000000:(s' = 2412) ;
[] (s = 2352) -> 1.000000:(s' = 1193) ;
[] (s = 2353) -> 1.000000:(s' = 1194) ;
[] (s = 2354) -> 1.000000:(s' = 1195) ;
[] (s = 2355) -> 1.000000:(s' = 1196) ;
[] (s = 2356) -> 1.000000:(s' = 2413) ;
[] (s = 2357) -> 1.000000:(s' = 2414) ;
[] (s = 2358) -> 0.500000:(s' = 2399) + 0.500000:(s' = 2400);
[] (s = 2358) -> 0.500000:(s' = 2401) + 0.500000:(s' = 2402);
[] (s = 2359) -> 1.000000:(s' = 2415) ;
[] (s = 2360) -> 1.000000:(s' = 2416) ;
[] (s = 2361) -> 1.000000:(s' = 1197) ;
[] (s = 2362) -> 1.000000:(s' = 1198) ;
[] (s = 2363) -> 1.000000:(s' = 1199) ;
[] (s = 2364) -> 1.000000:(s' = 1200) ;
[] (s = 2365) -> 1.000000:(s' = 1177) ;
[] (s = 2366) -> 1.000000:(s' = 1178) ;
[] (s = 2367) -> 1.000000:(s' = 1183) ;
[] (s = 2368) -> 1.000000:(s' = 1184) ;
[] (s = 2369) -> 1.000000:(s' = 2005) ;
[] (s = 2370) -> 1.000000:(s' = 2006) ;
[] (s = 2371) -> 1.000000:(s' = 2007) ;
[] (s = 2372) -> 1.000000:(s' = 2008) ;
[] (s = 2373) -> 1.000000:(s' = 1177) ;
[] (s = 2374) -> 1.000000:(s' = 1178) ;
[] (s = 2375) -> 1.000000:(s' = 1183) ;
[] (s = 2376) -> 1.000000:(s' = 1184) ;
[] (s = 2377) -> 1.000000:(s' = 1185) ;
[] (s = 2378) -> 1.000000:(s' = 1186) ;
[] (s = 2379) -> 1.000000:(s' = 1187) ;
[] (s = 2380) -> 1.000000:(s' = 1188) ;
[] (s = 2381) -> 1.000000:(s' = 2009) ;
[] (s = 2382) -> 1.000000:(s' = 2010) ;
[] (s = 2383) -> 1.000000:(s' = 2011) ;
[] (s = 2384) -> 1.000000:(s' = 2012) ;
[] (s = 2385) -> 1.000000:(s' = 1193) ;
[] (s = 2386) -> 1.000000:(s' = 1194) ;
[] (s = 2387) -> 1.000000:(s' = 1195) ;
[] (s = 2388) -> 1.000000:(s' = 1196) ;
[] (s = 2389) -> 1.000000:(s' = 1197) ;
[] (s = 2390) -> 1.000000:(s' = 1198) ;
[] (s = 2391) -> 1.000000:(s' = 1199) ;
[] (s = 2392) -> 1.000000:(s' = 1200) ;
[] (s = 2393) -> 1.000000:(s' = 1197) ;
[] (s = 2394) -> 1.000000:(s' = 1198) ;
[] (s = 2395) -> 1.000000:(s' = 1199) ;
[] (s = 2396) -> 1.000000:(s' = 1200) ;
[] (s = 2397) -> 0.500000:(s' = 2417) + 0.500000:(s' = 2418);
[] (s = 2397) -> 1.000000:(s' = 2419) ;
[] (s = 2398) -> 0.500000:(s' = 2420) + 0.500000:(s' = 2421);
[] (s = 2398) -> 1.000000:(s' = 2422) ;
[] (s = 2399) -> 0.500000:(s' = 2423) + 0.500000:(s' = 2424);
[] (s = 2399) -> 1.000000:(s' = 2425) ;
[] (s = 2400) -> 0.500000:(s' = 2426) + 0.500000:(s' = 2427);
[] (s = 2400) -> 1.000000:(s' = 2428) ;
[] (s = 2401) -> 1.000000:(s' = 2429) ;
[] (s = 2401) -> 0.500000:(s' = 2423) + 0.500000:(s' = 2426);
[] (s = 2402) -> 1.000000:(s' = 2430) ;
[] (s = 2402) -> 0.500000:(s' = 2424) + 0.500000:(s' = 2427);
[] (s = 2403) -> 1.000000:(s' = 2431) ;
[] (s = 2403) -> 0.500000:(s' = 2432) + 0.500000:(s' = 2433);
[] (s = 2404) -> 1.000000:(s' = 2434) ;
[] (s = 2404) -> 0.500000:(s' = 2435) + 0.500000:(s' = 2436);
[] (s = 2405) -> 0.500000:(s' = 2417) + 0.500000:(s' = 2418);
[] (s = 2405) -> 1.000000:(s' = 2437) ;
[] (s = 2406) -> 0.500000:(s' = 2420) + 0.500000:(s' = 2421);
[] (s = 2406) -> 1.000000:(s' = 2438) ;
[] (s = 2407) -> 1.000000:(s' = 2439) ;
[] (s = 2407) -> 0.500000:(s' = 2432) + 0.500000:(s' = 2433);
[] (s = 2408) -> 1.000000:(s' = 2440) ;
[] (s = 2408) -> 0.500000:(s' = 2435) + 0.500000:(s' = 2436);
[] (s = 2409) -> 0.500000:(s' = 2417) + 0.500000:(s' = 2418);
[] (s = 2409) -> 1.000000:(s' = 2441) ;
[] (s = 2410) -> 0.500000:(s' = 2420) + 0.500000:(s' = 2421);
[] (s = 2410) -> 1.000000:(s' = 2442) ;
[] (s = 2411) -> 1.000000:(s' = 2443) ;
[] (s = 2411) -> 0.500000:(s' = 2432) + 0.500000:(s' = 2433);
[] (s = 2412) -> 1.000000:(s' = 2444) ;
[] (s = 2412) -> 0.500000:(s' = 2435) + 0.500000:(s' = 2436);
[] (s = 2413) -> 0.500000:(s' = 2417) + 0.500000:(s' = 2418);
[] (s = 2413) -> 1.000000:(s' = 2445) ;
[] (s = 2414) -> 0.500000:(s' = 2420) + 0.500000:(s' = 2421);
[] (s = 2414) -> 1.000000:(s' = 2446) ;
[] (s = 2415) -> 1.000000:(s' = 2447) ;
[] (s = 2415) -> 0.500000:(s' = 2432) + 0.500000:(s' = 2433);
[] (s = 2416) -> 1.000000:(s' = 2448) ;
[] (s = 2416) -> 0.500000:(s' = 2435) + 0.500000:(s' = 2436);
[] (s = 2417) -> 1.000000:(s' = 2449) ;
[] (s = 2417) -> 1.000000:(s' = 2450) ;
[] (s = 2418) -> 1.000000:(s' = 2451) ;
[] (s = 2418) -> 1.000000:(s' = 2452) ;
[] (s = 2419) -> 0.500000:(s' = 2450) + 0.500000:(s' = 2452);
[] (s = 2420) -> 1.000000:(s' = 2453) ;
[] (s = 2420) -> 1.000000:(s' = 2454) ;
[] (s = 2421) -> 1.000000:(s' = 2455) ;
[] (s = 2421) -> 1.000000:(s' = 2456) ;
[] (s = 2422) -> 0.500000:(s' = 2454) + 0.500000:(s' = 2456);
[] (s = 2423) -> 1.000000:(s' = 2457) ;
[] (s = 2423) -> 1.000000:(s' = 2458) ;
[] (s = 2424) -> 1.000000:(s' = 2459) ;
[] (s = 2424) -> 1.000000:(s' = 2460) ;
[] (s = 2425) -> 0.500000:(s' = 2458) + 0.500000:(s' = 2460);
[] (s = 2426) -> 1.000000:(s' = 2461) ;
[] (s = 2426) -> 1.000000:(s' = 2462) ;
[] (s = 2427) -> 1.000000:(s' = 2463) ;
[] (s = 2427) -> 1.000000:(s' = 2464) ;
[] (s = 2428) -> 0.500000:(s' = 2462) + 0.500000:(s' = 2464);
[] (s = 2429) -> 0.500000:(s' = 2457) + 0.500000:(s' = 2461);
[] (s = 2430) -> 0.500000:(s' = 2459) + 0.500000:(s' = 2463);
[] (s = 2431) -> 0.500000:(s' = 2465) + 0.500000:(s' = 2466);
[] (s = 2432) -> 1.000000:(s' = 2465) ;
[] (s = 2432) -> 1.000000:(s' = 2467) ;
[] (s = 2433) -> 1.000000:(s' = 2466) ;
[] (s = 2433) -> 1.000000:(s' = 2468) ;
[] (s = 2434) -> 0.500000:(s' = 2469) + 0.500000:(s' = 2470);
[] (s = 2435) -> 1.000000:(s' = 2469) ;
[] (s = 2435) -> 1.000000:(s' = 2471) ;
[] (s = 2436) -> 1.000000:(s' = 2470) ;
[] (s = 2436) -> 1.000000:(s' = 2472) ;
[] (s = 2437) -> 0.500000:(s' = 2450) + 0.500000:(s' = 2452);
[] (s = 2438) -> 0.500000:(s' = 2454) + 0.500000:(s' = 2456);
[] (s = 2439) -> 0.500000:(s' = 2465) + 0.500000:(s' = 2466);
[] (s = 2440) -> 0.500000:(s' = 2469) + 0.500000:(s' = 2470);
[] (s = 2441) -> 0.500000:(s' = 2450) + 0.500000:(s' = 2452);
[] (s = 2442) -> 0.500000:(s' = 2454) + 0.500000:(s' = 2456);
[] (s = 2443) -> 0.500000:(s' = 2465) + 0.500000:(s' = 2466);
[] (s = 2444) -> 0.500000:(s' = 2469) + 0.500000:(s' = 2470);
[] (s = 2445) -> 0.500000:(s' = 2450) + 0.500000:(s' = 2452);
[] (s = 2446) -> 0.500000:(s' = 2454) + 0.500000:(s' = 2456);
[] (s = 2447) -> 0.500000:(s' = 2465) + 0.500000:(s' = 2466);
[] (s = 2448) -> 0.500000:(s' = 2469) + 0.500000:(s' = 2470);
[] (s = 2449) -> 1.000000:(s' = 2473) ;
[] (s = 2450) -> 1.000000:(s' = 2473) ;
[] (s = 2451) -> 1.000000:(s' = 2474) ;
[] (s = 2452) -> 1.000000:(s' = 2474) ;
[] (s = 2453) -> 1.000000:(s' = 2475) ;
[] (s = 2454) -> 1.000000:(s' = 2475) ;
[] (s = 2455) -> 1.000000:(s' = 2476) ;
[] (s = 2456) -> 1.000000:(s' = 2476) ;
[] (s = 2457) -> 1.000000:(s' = 2477) ;
[] (s = 2458) -> 1.000000:(s' = 2477) ;
[] (s = 2459) -> 1.000000:(s' = 2478) ;
[] (s = 2460) -> 1.000000:(s' = 2478) ;
[] (s = 2461) -> 1.000000:(s' = 2479) ;
[] (s = 2462) -> 1.000000:(s' = 2479) ;
[] (s = 2463) -> 1.000000:(s' = 2480) ;
[] (s = 2464) -> 1.000000:(s' = 2480) ;
[] (s = 2465) -> 1.000000:(s' = 2481) ;
[] (s = 2466) -> 1.000000:(s' = 2482) ;
[] (s = 2467) -> 1.000000:(s' = 2481) ;
[] (s = 2468) -> 1.000000:(s' = 2482) ;
[] (s = 2469) -> 1.000000:(s' = 2483) ;
[] (s = 2470) -> 1.000000:(s' = 2484) ;
[] (s = 2471) -> 1.000000:(s' = 2483) ;
[] (s = 2472) -> 1.000000:(s' = 2484) ;
[] (s = 2473) -> 1.000000:(s' = 2485) ;
[] (s = 2473) -> 1.000000:(s' = 2486) ;
[] (s = 2474) -> 1.000000:(s' = 2487) ;
[] (s = 2475) -> 1.000000:(s' = 2488) ;
[] (s = 2476) -> 1.000000:(s' = 2489) ;
[] (s = 2476) -> 1.000000:(s' = 2490) ;
[] (s = 2477) -> 1.000000:(s' = 2491) ;
[] (s = 2477) -> 1.000000:(s' = 2492) ;
[] (s = 2478) -> 1.000000:(s' = 2493) ;
[] (s = 2479) -> 1.000000:(s' = 2494) ;
[] (s = 2480) -> 1.000000:(s' = 2495) ;
[] (s = 2480) -> 1.000000:(s' = 2496) ;
[] (s = 2481) -> 1.000000:(s' = 2497) ;
[] (s = 2481) -> 1.000000:(s' = 2498) ;
[] (s = 2482) -> 1.000000:(s' = 2499) ;
[] (s = 2483) -> 1.000000:(s' = 2500) ;
[] (s = 2484) -> 1.000000:(s' = 2501) ;
[] (s = 2484) -> 1.000000:(s' = 2502) ;
[] (s = 2485) -> 1.000000:(s' = 2503) ;
[] (s = 2485) -> 1.000000:(s' = 2504) ;
[] (s = 2486) -> 1.000000:(s' = 2505) ;
[] (s = 2486) -> 1.000000:(s' = 2506) ;
[] (s = 2487) -> 1.000000:(s' = 2507) ;
[] (s = 2488) -> 1.000000:(s' = 2508) ;
[] (s = 2489) -> 1.000000:(s' = 2509) ;
[] (s = 2489) -> 1.000000:(s' = 2510) ;
[] (s = 2490) -> 1.000000:(s' = 2511) ;
[] (s = 2490) -> 1.000000:(s' = 2512) ;
[] (s = 2491) -> 1.000000:(s' = 2513) ;
[] (s = 2491) -> 1.000000:(s' = 2514) ;
[] (s = 2492) -> 1.000000:(s' = 2515) ;
[] (s = 2492) -> 1.000000:(s' = 2516) ;
[] (s = 2493) -> 1.000000:(s' = 2517) ;
[] (s = 2494) -> 1.000000:(s' = 2518) ;
[] (s = 2495) -> 1.000000:(s' = 2519) ;
[] (s = 2495) -> 1.000000:(s' = 2520) ;
[] (s = 2496) -> 1.000000:(s' = 2521) ;
[] (s = 2496) -> 1.000000:(s' = 2522) ;
[] (s = 2497) -> 1.000000:(s' = 2523) ;
[] (s = 2497) -> 1.000000:(s' = 2524) ;
[] (s = 2498) -> 1.000000:(s' = 2525) ;
[] (s = 2498) -> 1.000000:(s' = 2526) ;
[] (s = 2499) -> 1.000000:(s' = 2527) ;
[] (s = 2500) -> 1.000000:(s' = 2528) ;
[] (s = 2501) -> 1.000000:(s' = 2529) ;
[] (s = 2501) -> 1.000000:(s' = 2530) ;
[] (s = 2502) -> 1.000000:(s' = 2531) ;
[] (s = 2502) -> 1.000000:(s' = 2532) ;
[] (s = 2503) -> 1.000000:(s' = 2533) ;
[] (s = 2503) -> 1.000000:(s' = 2534) ;
[] (s = 2504) -> 1.000000:(s' = 2535) ;
[] (s = 2505) -> 1.000000:(s' = 2536) ;
[] (s = 2505) -> 1.000000:(s' = 2537) ;
[] (s = 2506) -> 1.000000:(s' = 2538) ;
[] (s = 2507) -> 1.000000:(s' = 2539) ;
[] (s = 2508) -> 1.000000:(s' = 2540) ;
[] (s = 2509) -> 1.000000:(s' = 2541) ;
[] (s = 2509) -> 1.000000:(s' = 2542) ;
[] (s = 2510) -> 1.000000:(s' = 2543) ;
[] (s = 2511) -> 1.000000:(s' = 2544) ;
[] (s = 2511) -> 1.000000:(s' = 2545) ;
[] (s = 2512) -> 1.000000:(s' = 2546) ;
[] (s = 2513) -> 1.000000:(s' = 2547) ;
[] (s = 2513) -> 1.000000:(s' = 2548) ;
[] (s = 2514) -> 1.000000:(s' = 2549) ;
[] (s = 2515) -> 1.000000:(s' = 2536) ;
[] (s = 2515) -> 1.000000:(s' = 2537) ;
[] (s = 2516) -> 1.000000:(s' = 2550) ;
[] (s = 2517) -> 1.000000:(s' = 2551) ;
[] (s = 2518) -> 1.000000:(s' = 2552) ;
[] (s = 2519) -> 1.000000:(s' = 2553) ;
[] (s = 2519) -> 1.000000:(s' = 2554) ;
[] (s = 2520) -> 1.000000:(s' = 2555) ;
[] (s = 2521) -> 1.000000:(s' = 2544) ;
[] (s = 2521) -> 1.000000:(s' = 2545) ;
[] (s = 2522) -> 1.000000:(s' = 2556) ;
[] (s = 2523) -> 1.000000:(s' = 2547) ;
[] (s = 2523) -> 1.000000:(s' = 2548) ;
[] (s = 2524) -> 1.000000:(s' = 2557) ;
[] (s = 2525) -> 1.000000:(s' = 2558) ;
[] (s = 2525) -> 1.000000:(s' = 2559) ;
[] (s = 2526) -> 1.000000:(s' = 2560) ;
[] (s = 2527) -> 1.000000:(s' = 2561) ;
[] (s = 2528) -> 1.000000:(s' = 2562) ;
[] (s = 2529) -> 1.000000:(s' = 2553) ;
[] (s = 2529) -> 1.000000:(s' = 2554) ;
[] (s = 2530) -> 1.000000:(s' = 2563) ;
[] (s = 2531) -> 1.000000:(s' = 2564) ;
[] (s = 2531) -> 1.000000:(s' = 2565) ;
[] (s = 2532) -> 1.000000:(s' = 2566) ;
[] (s = 2533) -> 0.500000:(s' = 2567) + 0.500000:(s' = 2568);
[] (s = 2533) -> 1.000000:(s' = 1078) ;
[] (s = 2534) -> 1.000000:(s' = 1078) ;
[] (s = 2534) -> 0.500000:(s' = 2569) + 0.500000:(s' = 2570);
[] (s = 2535) -> 1.000000:(s' = 433) ;
[] (s = 2536) -> 0.500000:(s' = 2571) + 0.500000:(s' = 2572);
[] (s = 2536) -> 1.000000:(s' = 1897) ;
[] (s = 2537) -> 1.000000:(s' = 1897) ;
[] (s = 2537) -> 0.500000:(s' = 2573) + 0.500000:(s' = 2574);
[] (s = 2538) -> 1.000000:(s' = 433) ;
[] (s = 2539) -> 1.000000:(s' = 433) ;
[] (s = 2540) -> 1.000000:(s' = 433) ;
[] (s = 2541) -> 0.500000:(s' = 2575) + 0.500000:(s' = 2576);
[] (s = 2541) -> 1.000000:(s' = 1078) ;
[] (s = 2542) -> 1.000000:(s' = 1078) ;
[] (s = 2542) -> 0.500000:(s' = 2577) + 0.500000:(s' = 2578);
[] (s = 2543) -> 1.000000:(s' = 433) ;
[] (s = 2544) -> 0.500000:(s' = 2579) + 0.500000:(s' = 2580);
[] (s = 2544) -> 1.000000:(s' = 1083) ;
[] (s = 2545) -> 1.000000:(s' = 1083) ;
[] (s = 2545) -> 0.500000:(s' = 2581) + 0.500000:(s' = 2582);
[] (s = 2546) -> 1.000000:(s' = 433) ;
[] (s = 2547) -> 0.500000:(s' = 2583) + 0.500000:(s' = 2584);
[] (s = 2547) -> 1.000000:(s' = 1910) ;
[] (s = 2548) -> 1.000000:(s' = 1910) ;
[] (s = 2548) -> 0.500000:(s' = 2585) + 0.500000:(s' = 2586);
[] (s = 2549) -> 1.000000:(s' = 433) ;
[] (s = 2550) -> 1.000000:(s' = 433) ;
[] (s = 2551) -> 1.000000:(s' = 433) ;
[] (s = 2552) -> 1.000000:(s' = 433) ;
[] (s = 2553) -> 0.500000:(s' = 2587) + 0.500000:(s' = 2588);
[] (s = 2553) -> 1.000000:(s' = 1093) ;
[] (s = 2554) -> 1.000000:(s' = 1093) ;
[] (s = 2554) -> 0.500000:(s' = 2589) + 0.500000:(s' = 2590);
[] (s = 2555) -> 1.000000:(s' = 433) ;
[] (s = 2556) -> 1.000000:(s' = 433) ;
[] (s = 2557) -> 1.000000:(s' = 433) ;
[] (s = 2558) -> 0.500000:(s' = 2591) + 0.500000:(s' = 2592);
[] (s = 2558) -> 1.000000:(s' = 1102) ;
[] (s = 2559) -> 1.000000:(s' = 1102) ;
[] (s = 2559) -> 0.500000:(s' = 2593) + 0.500000:(s' = 2594);
[] (s = 2560) -> 1.000000:(s' = 433) ;
[] (s = 2561) -> 1.000000:(s' = 433) ;
[] (s = 2562) -> 1.000000:(s' = 433) ;
[] (s = 2563) -> 1.000000:(s' = 433) ;
[] (s = 2564) -> 0.500000:(s' = 2595) + 0.500000:(s' = 2596);
[] (s = 2564) -> 1.000000:(s' = 1102) ;
[] (s = 2565) -> 1.000000:(s' = 1102) ;
[] (s = 2565) -> 0.500000:(s' = 2597) + 0.500000:(s' = 2598);
[] (s = 2566) -> 1.000000:(s' = 433) ;
[] (s = 2567) -> 1.000000:(s' = 1177) ;
[] (s = 2568) -> 1.000000:(s' = 1178) ;
[] (s = 2569) -> 1.000000:(s' = 1183) ;
[] (s = 2570) -> 1.000000:(s' = 1184) ;
[] (s = 2571) -> 1.000000:(s' = 2005) ;
[] (s = 2572) -> 1.000000:(s' = 2006) ;
[] (s = 2573) -> 1.000000:(s' = 2007) ;
[] (s = 2574) -> 1.000000:(s' = 2008) ;
[] (s = 2575) -> 1.000000:(s' = 1177) ;
[] (s = 2576) -> 1.000000:(s' = 1178) ;
[] (s = 2577) -> 1.000000:(s' = 1183) ;
[] (s = 2578) -> 1.000000:(s' = 1184) ;
[] (s = 2579) -> 1.000000:(s' = 1185) ;
[] (s = 2580) -> 1.000000:(s' = 1186) ;
[] (s = 2581) -> 1.000000:(s' = 1187) ;
[] (s = 2582) -> 1.000000:(s' = 1188) ;
[] (s = 2583) -> 1.000000:(s' = 2009) ;
[] (s = 2584) -> 1.000000:(s' = 2010) ;
[] (s = 2585) -> 1.000000:(s' = 2011) ;
[] (s = 2586) -> 1.000000:(s' = 2012) ;
[] (s = 2587) -> 1.000000:(s' = 1193) ;
[] (s = 2588) -> 1.000000:(s' = 1194) ;
[] (s = 2589) -> 1.000000:(s' = 1195) ;
[] (s = 2590) -> 1.000000:(s' = 1196) ;
[] (s = 2591) -> 1.000000:(s' = 1197) ;
[] (s = 2592) -> 1.000000:(s' = 1198) ;
[] (s = 2593) -> 1.000000:(s' = 1199) ;
[] (s = 2594) -> 1.000000:(s' = 1200) ;
[] (s = 2595) -> 1.000000:(s' = 1197) ;
[] (s = 2596) -> 1.000000:(s' = 1198) ;
[] (s = 2597) -> 1.000000:(s' = 1199) ;
[] (s = 2598) -> 1.000000:(s' = 1200) ;

endmodule