// // This file has been generated with Kappa // // -- state encoding: instances // -- compaction : relative // -- further compaction: yes nondeterministic module impl4000 tg : [0..62] init 0; n : [0..147] init 0; [] (tg=46)&(n=146)-> 1.000000:(tg'=50)&(n'=97) ; [] (tg=46)&(n=146)-> 1.000000:(tg'=49)&(n'=97) ; [] (tg=57)&(n=36)-> 1.000000:(tg'=60)&(n'=108) ; [] (tg=46)&(n=145)-> 1.000000:(tg'=50)&(n'=98) ; [] (tg=46)&(n=145)-> 1.000000:(tg'=49)&(n'=98) ; [] (tg=55)&(n=36)-> 1.000000:(tg'=59)&(n'=108) ; [] (tg=57)&(n=35)-> 1.000000:(tg'=60)&(n'=105) ; [] (tg=55)&(n=35)-> 1.000000:(tg'=59)&(n'=105) ; [] (tg=57)&(n=34)-> 1.000000:(tg'=60)&(n'=102) ; [] (tg=55)&(n=34)-> 1.000000:(tg'=59)&(n'=102) ; [] (tg=43)&(n=73)-> 1.000000:(tg'=46)&(n'=147) ; [] (tg=42)&(n=36)-> 1.000000:(tg'=46)&(n'=145) ; [] (tg=40)&(n=36)-> 1.000000:(tg'=46)&(n'=144) ; [] (tg=41)&(n=71)-> 1.000000:(tg'=46)&(n'=142) ; [] (tg=42)&(n=35)-> 1.000000:(tg'=46)&(n'=141) ; [] (tg=40)&(n=35)-> 1.000000:(tg'=46)&(n'=140) ; [] (tg=42)&(n=34)-> 1.000000:(tg'=46)&(n'=137) ; [] (tg=40)&(n=34)-> 1.000000:(tg'=46)&(n'=136) ; [] (tg=34)&(n=36)-> 1.000000:(tg'=43)&(n'=73) ; [] (tg=34)&(n=36)-> 1.000000:(tg'=41)&(n'=73) ; [] (tg=12)&(n=64..66)-> 0.500000:(tg'=14)&(n'=36) + 0.500000:(tg'=18)&(n'=36) ; [] (tg=11)&(n=64..66)-> 0.500000:(tg'=13)&(n'=36) + 0.500000:(tg'=17)&(n'=36) ; [] (tg=10)&(n=64..66)-> 0.500000:(tg'=19)&(n'=34) + 0.500000:(tg'=20)&(n'=34) ; [] (tg=9)&(n=64..66)-> 0.500000:(tg'=15)&(n'=34) + 0.500000:(tg'=16)&(n'=34) ; [] (tg=4)&(n=64..66)-> 0.500000:(tg'=6)&(n'=36) + 0.500000:(tg'=8)&(n'=36) ; [] (tg=3)&(n=64..66)-> 0.500000:(tg'=5)&(n'=36) + 0.500000:(tg'=7)&(n'=36) ; [] (tg=2)&(n=64..66)-> 0.500000:(tg'=7)&(n'=34) + 0.500000:(tg'=8)&(n'=34) ; [] (tg=1)&(n=64..66)-> 0.500000:(tg'=5)&(n'=34) + 0.500000:(tg'=6)&(n'=34) ; [] (tg=54)&(n=82)-> 1.000000:(tg'=4)&(n'=66) ; [] (tg=53)&(n=82)-> 1.000000:(tg'=3)&(n'=66) ; [] (tg=52)&(n=82)-> 1.000000:(tg'=2)&(n'=66) ; [] (tg=51)&(n=82)-> 1.000000:(tg'=1)&(n'=66) ; [] (tg=54)&(n=80)-> 1.000000:(tg'=4)&(n'=65) ; [] (tg=53)&(n=80)-> 1.000000:(tg'=3)&(n'=65) ; [] (tg=52)&(n=80)-> 1.000000:(tg'=2)&(n'=65) ; [] (tg=51)&(n=80)-> 1.000000:(tg'=1)&(n'=65) ; [] (tg=52)&(n=77)-> 1.000000:(tg'=2)&(n'=64) ; [] (tg=51)&(n=77)-> 1.000000:(tg'=1)&(n'=64) ; [] (tg=0)&(n=51)-> 0.500000:(tg'=3)&(n'=62) + 0.500000:(tg'=4)&(n'=62) ; [] (tg=0)&(n=51)-> 0.500000:(tg'=1)&(n'=63) + 0.500000:(tg'=2)&(n'=63) ; [] (tg=52)&(n=76)-> 1.000000:(tg'=2)&(n'=62) ; [] (tg=51)&(n=76)-> 1.000000:(tg'=1)&(n'=62) ; [] (tg=57)&(n=33)-> 1.000000:(tg'=60)&(n'=99) ; [] (tg=46)&(n=133)-> 1.000000:(tg'=50)&(n'=90) ; [] (tg=46)&(n=133)-> 1.000000:(tg'=49)&(n'=90) ; [] (tg=55)&(n=33)-> 1.000000:(tg'=59)&(n'=99) ; [] (tg=57)&(n=32)-> 1.000000:(tg'=60)&(n'=96) ; [] (tg=55)&(n=32)-> 1.000000:(tg'=59)&(n'=96) ; [] (tg=57)&(n=31)-> 1.000000:(tg'=60)&(n'=93) ; [] (tg=55)&(n=31)-> 1.000000:(tg'=59)&(n'=93) ; [] (tg=57)&(n=30)-> 1.000000:(tg'=60)&(n'=90) ; [] (tg=46)&(n=121)-> 1.000000:(tg'=50)&(n'=82) ; [] (tg=46)&(n=121)-> 1.000000:(tg'=49)&(n'=82) ; [] (tg=55)&(n=30)-> 1.000000:(tg'=59)&(n'=90) ; [] (tg=57)&(n=29)-> 1.000000:(tg'=60)&(n'=87) ; [] (tg=55)&(n=29)-> 1.000000:(tg'=59)&(n'=87) ; [] (tg=57)&(n=28)-> 1.000000:(tg'=60)&(n'=84) ; [] (tg=55)&(n=28)-> 1.000000:(tg'=59)&(n'=84) ; [] (tg=43)&(n=67)-> 1.000000:(tg'=46)&(n'=135) ; [] (tg=42)&(n=33)-> 1.000000:(tg'=46)&(n'=133) ; [] (tg=40)&(n=33)-> 1.000000:(tg'=46)&(n'=132) ; [] (tg=41)&(n=65)-> 1.000000:(tg'=46)&(n'=130) ; [] (tg=42)&(n=32)-> 1.000000:(tg'=46)&(n'=129) ; [] (tg=40)&(n=32)-> 1.000000:(tg'=46)&(n'=128) ; [] (tg=42)&(n=31)-> 1.000000:(tg'=46)&(n'=125) ; [] (tg=40)&(n=31)-> 1.000000:(tg'=46)&(n'=124) ; [] (tg=43)&(n=61)-> 1.000000:(tg'=46)&(n'=123) ; [] (tg=42)&(n=30)-> 1.000000:(tg'=46)&(n'=121) ; [] (tg=40)&(n=30)-> 1.000000:(tg'=46)&(n'=120) ; [] (tg=41)&(n=59)-> 1.000000:(tg'=46)&(n'=118) ; [] (tg=42)&(n=29)-> 1.000000:(tg'=46)&(n'=117) ; [] (tg=40)&(n=29)-> 1.000000:(tg'=46)&(n'=116) ; [] (tg=42)&(n=28)-> 1.000000:(tg'=46)&(n'=113) ; [] (tg=40)&(n=28)-> 1.000000:(tg'=46)&(n'=112) ; [] (tg=12)&(n=60..61)-> 0.500000:(tg'=14)&(n'=27) + 0.500000:(tg'=18)&(n'=27) ; [] (tg=11)&(n=60..61)-> 0.500000:(tg'=13)&(n'=27) + 0.500000:(tg'=17)&(n'=27) ; [] (tg=12)&(n=58)| (tg=12)&(n=55)-> 0.500000:(tg'=14)&(n'=33) + 0.500000:(tg'=18)&(n'=33) ; [] (tg=11)&(n=58)| (tg=11)&(n=55)-> 0.500000:(tg'=13)&(n'=33) + 0.500000:(tg'=17)&(n'=33) ; [] (tg=10)&(n=58)| (tg=10)&(n=55)-> 0.500000:(tg'=19)&(n'=31) + 0.500000:(tg'=20)&(n'=31) ; [] (tg=9)&(n=58)| (tg=9)&(n=55)-> 0.500000:(tg'=15)&(n'=31) + 0.500000:(tg'=16)&(n'=31) ; [] (tg=4)&(n=60..61)-> 0.500000:(tg'=6)&(n'=27) + 0.500000:(tg'=8)&(n'=27) ; [] (tg=3)&(n=60..61)-> 0.500000:(tg'=5)&(n'=27) + 0.500000:(tg'=7)&(n'=27) ; [] (tg=4)&(n=58)| (tg=4)&(n=55)-> 0.500000:(tg'=6)&(n'=33) + 0.500000:(tg'=8)&(n'=33) ; [] (tg=3)&(n=58)| (tg=3)&(n=55)-> 0.500000:(tg'=5)&(n'=33) + 0.500000:(tg'=7)&(n'=33) ; [] (tg=2)&(n=58)| (tg=2)&(n=55)-> 0.500000:(tg'=7)&(n'=31) + 0.500000:(tg'=8)&(n'=31) ; [] (tg=1)&(n=58)| (tg=1)&(n=55)-> 0.500000:(tg'=5)&(n'=31) + 0.500000:(tg'=6)&(n'=31) ; [] (tg=54)&(n=93)| (tg=54)&(n=69)-> 1.000000:(tg'=4)&(n'=60) ; [] (tg=53)&(n=93)| (tg=53)&(n=69)-> 1.000000:(tg'=3)&(n'=60) ; [] (tg=52)&(n=93)| (tg=52)&(n=85)| (tg=52)&(n=69)-> 1.000000:(tg'=2)&(n'=60) ; [] (tg=51)&(n=93)| (tg=51)&(n=85)| (tg=51)&(n=69)-> 1.000000:(tg'=1)&(n'=60) ; [] (tg=54)&(n=64)-> 1.000000:(tg'=4)&(n'=61) ; [] (tg=53)&(n=64)-> 1.000000:(tg'=3)&(n'=61) ; [] (tg=52)&(n=64)-> 1.000000:(tg'=2)&(n'=61) ; [] (tg=51)&(n=64)-> 1.000000:(tg'=1)&(n'=61) ; [] (tg=0)&(n=49..50)-> 0.500000:(tg'=3)&(n'=42) + 0.500000:(tg'=4)&(n'=42) ; [] (tg=0)&(n=49..50)-> 0.500000:(tg'=1)&(n'=43) + 0.500000:(tg'=2)&(n'=43) ; [] (tg=54)&(n=92)| (tg=54)&(n=84)| (tg=54)&(n=60)-> 1.000000:(tg'=4)&(n'=43) ; [] (tg=53)&(n=92)| (tg=53)&(n=84)| (tg=53)&(n=60)-> 1.000000:(tg'=3)&(n'=43) ; [] (tg=52)&(n=92)| (tg=52)&(n=84)| (tg=52)&(n=68)| (tg=52)&(n=60)-> 1.000000:(tg'=2)&(n'=42) ; [] (tg=51)&(n=92)| (tg=51)&(n=84)| (tg=51)&(n=68)| (tg=51)&(n=60)-> 1.000000:(tg'=1)&(n'=42) ; [] (tg=54)&(n=99)| (tg=54)&(n=91)| (tg=54)&(n=83)| (tg=54)&(n=75)| (tg=54)&(n=67)| (tg=54)&(n=59)-> 1.000000:(tg'=4)&(n'=47) ; [] (tg=53)&(n=99)| (tg=53)&(n=91)| (tg=53)&(n=83)| (tg=53)&(n=75)| (tg=53)&(n=67)| (tg=53)&(n=59)-> 1.000000:(tg'=3)&(n'=47) ; [] (tg=57)&(n=27)-> 1.000000:(tg'=60)&(n'=81) ; [] (tg=46)&(n=109)-> 1.000000:(tg'=50)&(n'=74) ; [] (tg=46)&(n=109)-> 1.000000:(tg'=49)&(n'=74) ; [] (tg=55)&(n=27)-> 1.000000:(tg'=59)&(n'=81) ; [] (tg=57)&(n=26)-> 1.000000:(tg'=60)&(n'=78) ; [] (tg=55)&(n=26)-> 1.000000:(tg'=59)&(n'=78) ; [] (tg=57)&(n=25)-> 1.000000:(tg'=60)&(n'=75) ; [] (tg=55)&(n=25)-> 1.000000:(tg'=59)&(n'=75) ; [] (tg=57)&(n=24)-> 1.000000:(tg'=60)&(n'=72) ; [] (tg=46)&(n=97)-> 1.000000:(tg'=50)&(n'=66) ; [] (tg=46)&(n=97)-> 1.000000:(tg'=49)&(n'=66) ; [] (tg=55)&(n=24)-> 1.000000:(tg'=59)&(n'=72) ; [] (tg=57)&(n=23)-> 1.000000:(tg'=60)&(n'=69) ; [] (tg=55)&(n=23)-> 1.000000:(tg'=59)&(n'=69) ; [] (tg=57)&(n=22)-> 1.000000:(tg'=60)&(n'=66) ; [] (tg=55)&(n=22)-> 1.000000:(tg'=59)&(n'=66) ; [] (tg=57)&(n=21)-> 1.000000:(tg'=60)&(n'=63) ; [] (tg=46)&(n=85)-> 1.000000:(tg'=50)&(n'=58) ; [] (tg=46)&(n=85)-> 1.000000:(tg'=49)&(n'=58) ; [] (tg=55)&(n=21)-> 1.000000:(tg'=59)&(n'=63) ; [] (tg=57)&(n=20)-> 1.000000:(tg'=60)&(n'=60) ; [] (tg=55)&(n=20)-> 1.000000:(tg'=59)&(n'=60) ; [] (tg=57)&(n=19)-> 1.000000:(tg'=60)&(n'=57) ; [] (tg=55)&(n=19)-> 1.000000:(tg'=59)&(n'=57) ; [] (tg=46)&(n=73)-> 1.000000:(tg'=50)&(n'=50) ; [] (tg=46)&(n=73)-> 1.000000:(tg'=49)&(n'=50) ; [] (tg=43)&(n=55)-> 1.000000:(tg'=46)&(n'=111) ; [] (tg=42)&(n=27)-> 1.000000:(tg'=46)&(n'=109) ; [] (tg=40)&(n=27)-> 1.000000:(tg'=46)&(n'=108) ; [] (tg=41)&(n=53)-> 1.000000:(tg'=46)&(n'=106) ; [] (tg=42)&(n=26)-> 1.000000:(tg'=46)&(n'=105) ; [] (tg=40)&(n=26)-> 1.000000:(tg'=46)&(n'=104) ; [] (tg=42)&(n=25)-> 1.000000:(tg'=46)&(n'=101) ; [] (tg=40)&(n=25)-> 1.000000:(tg'=46)&(n'=100) ; [] (tg=43)&(n=49)-> 1.000000:(tg'=46)&(n'=99) ; [] (tg=41)&(n=47)-> 1.000000:(tg'=46)&(n'=94) ; [] (tg=43)&(n=43)-> 1.000000:(tg'=46)&(n'=87) ; [] (tg=41)&(n=41)-> 1.000000:(tg'=46)&(n'=82) ; [] (tg=43)&(n=37)-> 1.000000:(tg'=46)&(n'=75) ; [] (tg=41)&(n=35)-> 1.000000:(tg'=46)&(n'=70) ; [] (tg=10)&(n=60..61)| (tg=10)&(n=46)-> 0.500000:(tg'=19)&(n'=25) + 0.500000:(tg'=20)&(n'=25) ; [] (tg=9)&(n=60..61)| (tg=9)&(n=46)-> 0.500000:(tg'=15)&(n'=25) + 0.500000:(tg'=16)&(n'=25) ; [] (tg=10)&(n=45)| (tg=10)&(n=40)-> 0.500000:(tg'=19)&(n'=22) + 0.500000:(tg'=20)&(n'=22) ; [] (tg=9)&(n=45)| (tg=9)&(n=40)-> 0.500000:(tg'=15)&(n'=22) + 0.500000:(tg'=16)&(n'=22) ; [] (tg=12)&(n=45)| (tg=12)&(n=39)-> 0.500000:(tg'=14)&(n'=24) + 0.500000:(tg'=18)&(n'=24) ; [] (tg=11)&(n=45)| (tg=11)&(n=39)-> 0.500000:(tg'=13)&(n'=24) + 0.500000:(tg'=17)&(n'=24) ; [] (tg=12)&(n=32)-> 0.500000:(tg'=14)&(n'=18) + 0.500000:(tg'=18)&(n'=18) ; [] (tg=11)&(n=32)-> 0.500000:(tg'=13)&(n'=18) + 0.500000:(tg'=17)&(n'=18) ; [] (tg=10)&(n=32)-> 0.500000:(tg'=19)&(n'=16) + 0.500000:(tg'=20)&(n'=16) ; [] (tg=9)&(n=32)-> 0.500000:(tg'=15)&(n'=16) + 0.500000:(tg'=16)&(n'=16) ; [] (tg=12)&(n=31)-> 0.500000:(tg'=14)&(n'=21) + 0.500000:(tg'=18)&(n'=21) ; [] (tg=11)&(n=31)-> 0.500000:(tg'=13)&(n'=21) + 0.500000:(tg'=17)&(n'=21) ; [] (tg=10)&(n=31)-> 0.500000:(tg'=19)&(n'=19) + 0.500000:(tg'=20)&(n'=19) ; [] (tg=9)&(n=31)-> 0.500000:(tg'=15)&(n'=19) + 0.500000:(tg'=16)&(n'=19) ; [] (tg=2)&(n=60..61)| (tg=2)&(n=46)-> 0.500000:(tg'=7)&(n'=25) + 0.500000:(tg'=8)&(n'=25) ; [] (tg=1)&(n=60..61)| (tg=1)&(n=46)-> 0.500000:(tg'=5)&(n'=25) + 0.500000:(tg'=6)&(n'=25) ; [] (tg=2)&(n=45)| (tg=2)&(n=40)-> 0.500000:(tg'=7)&(n'=22) + 0.500000:(tg'=8)&(n'=22) ; [] (tg=1)&(n=45)| (tg=1)&(n=40)-> 0.500000:(tg'=5)&(n'=22) + 0.500000:(tg'=6)&(n'=22) ; [] (tg=4)&(n=45)| (tg=4)&(n=39)-> 0.500000:(tg'=6)&(n'=24) + 0.500000:(tg'=8)&(n'=24) ; [] (tg=3)&(n=45)| (tg=3)&(n=39)-> 0.500000:(tg'=5)&(n'=24) + 0.500000:(tg'=7)&(n'=24) ; [] (tg=4)&(n=32)-> 0.500000:(tg'=6)&(n'=18) + 0.500000:(tg'=8)&(n'=18) ; [] (tg=3)&(n=32)-> 0.500000:(tg'=5)&(n'=18) + 0.500000:(tg'=7)&(n'=18) ; [] (tg=2)&(n=32)-> 0.500000:(tg'=7)&(n'=16) + 0.500000:(tg'=8)&(n'=16) ; [] (tg=1)&(n=32)-> 0.500000:(tg'=5)&(n'=16) + 0.500000:(tg'=6)&(n'=16) ; [] (tg=4)&(n=31)-> 0.500000:(tg'=6)&(n'=21) + 0.500000:(tg'=8)&(n'=21) ; [] (tg=3)&(n=31)-> 0.500000:(tg'=5)&(n'=21) + 0.500000:(tg'=7)&(n'=21) ; [] (tg=2)&(n=31)-> 0.500000:(tg'=7)&(n'=19) + 0.500000:(tg'=8)&(n'=19) ; [] (tg=1)&(n=31)-> 0.500000:(tg'=5)&(n'=19) + 0.500000:(tg'=6)&(n'=19) ; [] (tg=46)&(n=61)-> 1.000000:(tg'=50)&(n'=42) ; [] (tg=46)&(n=61)-> 1.000000:(tg'=49)&(n'=42) ; [] (tg=46)&(n=49)-> 1.000000:(tg'=50)&(n'=34) ; [] (tg=46)&(n=49)-> 1.000000:(tg'=49)&(n'=34) ; [] (tg=46)&(n=37)-> 1.000000:(tg'=50)&(n'=26) ; [] (tg=46)&(n=37)-> 1.000000:(tg'=49)&(n'=26) ; [] (tg=43)&(n=31)-> 1.000000:(tg'=46)&(n'=63) ; [] (tg=41)&(n=29)-> 1.000000:(tg'=46)&(n'=58) ; [] (tg=43)&(n=25)-> 1.000000:(tg'=46)&(n'=51) ; [] (tg=41)&(n=23)-> 1.000000:(tg'=46)&(n'=46) ; [] (tg=43)&(n=19)-> 1.000000:(tg'=46)&(n'=39) ; [] (tg=41)&(n=17)-> 1.000000:(tg'=46)&(n'=34) ; [] (tg=10)&(n=22)-> 0.500000:(tg'=19)&(n'=13) + 0.500000:(tg'=20)&(n'=13) ; [] (tg=9)&(n=22)-> 0.500000:(tg'=15)&(n'=13) + 0.500000:(tg'=16)&(n'=13) ; [] (tg=12)&(n=15)-> 0.500000:(tg'=14)&(n'=9) + 0.500000:(tg'=18)&(n'=9) ; [] (tg=11)&(n=15)-> 0.500000:(tg'=13)&(n'=9) + 0.500000:(tg'=17)&(n'=9) ; [] (tg=12)&(n=21)| (tg=12)&(n=14)-> 0.500000:(tg'=14)&(n'=12) + 0.500000:(tg'=18)&(n'=12) ; [] (tg=11)&(n=21)| (tg=11)&(n=14)-> 0.500000:(tg'=13)&(n'=12) + 0.500000:(tg'=17)&(n'=12) ; [] (tg=10)&(n=21)| (tg=10)&(n=14)-> 0.500000:(tg'=19)&(n'=10) + 0.500000:(tg'=20)&(n'=10) ; [] (tg=9)&(n=21)| (tg=9)&(n=14)-> 0.500000:(tg'=15)&(n'=10) + 0.500000:(tg'=16)&(n'=10) ; [] (tg=2)&(n=22)-> 0.500000:(tg'=7)&(n'=13) + 0.500000:(tg'=8)&(n'=13) ; [] (tg=1)&(n=22)-> 0.500000:(tg'=5)&(n'=13) + 0.500000:(tg'=6)&(n'=13) ; [] (tg=4)&(n=15)-> 0.500000:(tg'=6)&(n'=9) + 0.500000:(tg'=8)&(n'=9) ; [] (tg=3)&(n=15)-> 0.500000:(tg'=5)&(n'=9) + 0.500000:(tg'=7)&(n'=9) ; [] (tg=4)&(n=21)| (tg=4)&(n=14)-> 0.500000:(tg'=6)&(n'=12) + 0.500000:(tg'=8)&(n'=12) ; [] (tg=3)&(n=21)| (tg=3)&(n=14)-> 0.500000:(tg'=5)&(n'=12) + 0.500000:(tg'=7)&(n'=12) ; [] (tg=2)&(n=21)| (tg=2)&(n=14)-> 0.500000:(tg'=7)&(n'=10) + 0.500000:(tg'=8)&(n'=10) ; [] (tg=1)&(n=21)| (tg=1)&(n=14)-> 0.500000:(tg'=5)&(n'=10) + 0.500000:(tg'=6)&(n'=10) ; [] (tg=0)&(n=16)-> 0.500000:(tg'=3)&(n'=10) + 0.500000:(tg'=4)&(n'=10) ; [] (tg=0)&(n=16)-> 0.500000:(tg'=1)&(n'=11) + 0.500000:(tg'=2)&(n'=11) ; [] (tg=0)&(n=11)-> 0.500000:(tg'=3)&(n'=7) + 0.500000:(tg'=4)&(n'=7) ; [] (tg=0)&(n=11)-> 0.500000:(tg'=1)&(n'=8) + 0.500000:(tg'=2)&(n'=8) ; [] (tg=46)&(n=25)-> 1.000000:(tg'=50)&(n'=18) ; [] (tg=46)&(n=25)-> 1.000000:(tg'=49)&(n'=18) ; [] (tg=46)&(n=13)-> 1.000000:(tg'=50)&(n'=10) ; [] (tg=46)&(n=13)-> 1.000000:(tg'=49)&(n'=10) ; [] (tg=46)&(n=10)-> 1.000000:(tg'=50)&(n'=9) ; [] (tg=46)&(n=10)-> 1.000000:(tg'=49)&(n'=9) ; [] (tg=43)&(n=13)-> 1.000000:(tg'=46)&(n'=27) ; [] (tg=41)&(n=11)-> 1.000000:(tg'=46)&(n'=22) ; [] (tg=43)&(n=7)-> 1.000000:(tg'=46)&(n'=15) ; [] (tg=41)&(n=5)-> 1.000000:(tg'=46)&(n'=10) ; [] (tg=52)&(n=0)-> 1.000000:(tg'=2)&(n'=1) ; [] (tg=51)&(n=0)-> 1.000000:(tg'=1)&(n'=1) ; [] (tg=57)&(n=0)-> 1.000000:(tg'=60)&(n'=0) ; [] (tg=55)&(n=0)-> 1.000000:(tg'=59)&(n'=0) ; [] (tg=43)&(n=1)-> 1.000000:(tg'=46)&(n'=3) ; [] (tg=40)&(n=0)-> 1.000000:(tg'=46)&(n'=0) ; [] (tg=33)&(n=0)-> 1.000000:(tg'=43)&(n'=0) ; [] (tg=32)&(n=0)-> 1.000000:(tg'=41)&(n'=0) ; [] (tg=42)&(n=0)| (tg=41)&(n=1)-> 1.000000:(tg'=46)&(n'=n+1) ; [] (tg=56)&(n=0..1)-> 1.000000:(tg'=59)&(n'=n+1) ; [] (tg=58)&(n=0..1)-> 1.000000:(tg'=60)&(n'=n+1) ; [] (tg=59)&(n=0)| (tg=60)&(n=0)-> 1.000000:(tg'=47) ; [] (tg=59)&(n=1)| (tg=60)&(n=1)-> 1.000000:(tg'=47)&(n'=n-1) ; [] (tg=59)&(n=2)| (tg=60)&(n=2)-> 1.000000:(tg'=47)&(n'=n-2) ; [] (tg=53)&(n=0..1)-> 1.000000:(tg'=3)&(n'=n+2) ; [] (tg=54)&(n=0..1)-> 1.000000:(tg'=4)&(n'=n+2) ; [] (tg=51)&(n=1..2)-> 1.000000:(tg'=1)&(n'=n+2) ; [] (tg=52)&(n=1..2)-> 1.000000:(tg'=2)&(n'=n+2) ; [] (tg=34)&(n=0)| (tg=32)&(n=1)-> 1.000000:(tg'=41)&(n'=n+1) ; [] (tg=34)&(n=0)| (tg=33)&(n=1)-> 1.000000:(tg'=43)&(n'=n+1) ; [] (tg=34)&(n=1)| (tg=32)&(n=2)-> 1.000000:(tg'=41)&(n'=n+2) ; [] (tg=34)&(n=1)| (tg=33)&(n=2)-> 1.000000:(tg'=43)&(n'=n+2) ; [] (tg=34)&(n=2)| (tg=33)&(n=3)-> 1.000000:(tg'=43)&(n'=n+3) ; [] (tg=34)&(n=2)| (tg=32)&(n=3)-> 1.000000:(tg'=41)&(n'=n+3) ; [] (tg=34)&(n=3)| (tg=32)&(n=4)-> 1.000000:(tg'=41)&(n'=n+4) ; [] (tg=34)&(n=3)| (tg=33)&(n=4)-> 1.000000:(tg'=43)&(n'=n+4) ; [] (tg=34)&(n=4)| (tg=32)&(n=5)-> 1.000000:(tg'=41)&(n'=n+5) ; [] (tg=34)&(n=4)| (tg=33)&(n=5)-> 1.000000:(tg'=43)&(n'=n+5) ; [] (tg=34)&(n=5)| (tg=33)&(n=6)-> 1.000000:(tg'=43)&(n'=n+6) ; [] (tg=34)&(n=5)| (tg=32)&(n=6)-> 1.000000:(tg'=41)&(n'=n+6) ; [] (tg=40)&(n=1)| (tg=41)&(n=3)-> 1.000000:(tg'=46)&(n'=n+3) ; [] (tg=42)&(n=1)| (tg=43)&(n=3)-> 1.000000:(tg'=46)&(n'=n+4) ; [] (tg=40)&(n=2)| (tg=43)&(n=5)-> 1.000000:(tg'=46)&(n'=n+6) ; [] (tg=42)&(n=2)| (tg=41)&(n=7)-> 1.000000:(tg'=46)&(n'=n+7) ; [] (tg=40)&(n=3)| (tg=41)&(n=9)-> 1.000000:(tg'=46)&(n'=n+9) ; [] (tg=42)&(n=3)| (tg=43)&(n=9)-> 1.000000:(tg'=46)&(n'=n+10) ; [] (tg=40)&(n=4)| (tg=43)&(n=11)-> 1.000000:(tg'=46)&(n'=n+12) ; [] (tg=42)&(n=4)| (tg=41)&(n=13)-> 1.000000:(tg'=46)&(n'=n+13) ; [] (tg=55)&(n=1)| (tg=56)&(n=2..3)-> 1.000000:(tg'=59)&(n'=n+2) ; [] (tg=57)&(n=1)| (tg=58)&(n=2..3)-> 1.000000:(tg'=60)&(n'=n+2) ; [] (tg=46)&(n=0..8)-> 1.000000:(tg'=49) ; [] (tg=46)&(n=0..8)-> 1.000000:(tg'=50) ; [] (tg=56)&(n=4..5)-> 1.000000:(tg'=59)&(n'=n+3) ; [] (tg=58)&(n=4..5)-> 1.000000:(tg'=60)&(n'=n+3) ; [] (tg=55)&(n=2)| (tg=56)&(n=6..7)-> 1.000000:(tg'=59)&(n'=n+4) ; [] (tg=57)&(n=2)| (tg=58)&(n=6..7)-> 1.000000:(tg'=60)&(n'=n+4) ; [] (tg=56)&(n=8..9)-> 1.000000:(tg'=59)&(n'=n+5) ; [] (tg=58)&(n=8..9)-> 1.000000:(tg'=60)&(n'=n+5) ; [] (tg=46)&(n=9)| (tg=46)&(n=11..12)| (tg=46)&(n=15..20)-> 1.000000:(tg'=49)&(n'=n-4) ; [] (tg=46)&(n=9)| (tg=46)&(n=11..12)| (tg=46)&(n=15..20)-> 1.000000:(tg'=50)&(n'=n-4) ; [] (tg=46)&(n=14)| (tg=46)&(n=22)-> 1.000000:(tg'=49)&(n'=n-5) ; [] (tg=46)&(n=14)| (tg=46)&(n=22)-> 1.000000:(tg'=50)&(n'=n-5) ; [] (tg=55)&(n=3)| (tg=56)&(n=10..11)-> 1.000000:(tg'=59)&(n'=n+6) ; [] (tg=57)&(n=3)| (tg=58)&(n=10..11)-> 1.000000:(tg'=60)&(n'=n+6) ; [] (tg=56)&(n=12..13)-> 1.000000:(tg'=59)&(n'=n+7) ; [] (tg=58)&(n=12..13)-> 1.000000:(tg'=60)&(n'=n+7) ; [] (tg=59)&(n=3)| (tg=60)&(n=3)-> 1.000000:(tg'=47)&(n'=n-3) ; [] (tg=59)&(n=4)| (tg=60)&(n=4)-> 1.000000:(tg'=47)&(n'=n-4) ; [] (tg=59)&(n=5)| (tg=60)&(n=5)-> 1.000000:(tg'=47)&(n'=n-5) ; [] (tg=59)&(n=6)| (tg=60)&(n=6)-> 1.000000:(tg'=47)&(n'=n-6) ; [] (tg=59)&(n=7)| (tg=60)&(n=7)-> 1.000000:(tg'=47)&(n'=n-7) ; [] (tg=59)&(n=8)| (tg=60)&(n=8)-> 1.000000:(tg'=47)&(n'=n-8) ; [] (tg=59)&(n=9)| (tg=60)&(n=9)-> 1.000000:(tg'=47)&(n'=n-9) ; [] (tg=60)&(n=10)| (tg=59)&(n=10)-> 1.000000:(tg'=47)&(n'=n-10) ; [] (tg=49)&(n=0..11)| (tg=50)&(n=0..11)-> 1.000000:(tg'=0)&(n'=n+1) ; [] (tg=59)&(n=11)| (tg=60)&(n=11)-> 1.000000:(tg'=47)&(n'=n-11) ; [] (tg=59)&(n=12)| (tg=60)&(n=12)-> 1.000000:(tg'=47)&(n'=n-12) ; [] (tg=59)&(n=13)| (tg=60)&(n=13)-> 1.000000:(tg'=47)&(n'=n-13) ; [] (tg=59)&(n=13)| (tg=60)&(n=13)-> 1.000000:(tg'=48)&(n'=n-13) ; [] (tg=59)&(n=14)| (tg=60)&(n=14)-> 1.000000:(tg'=47)&(n'=n-14) ; [] (tg=59)&(n=14)| (tg=60)&(n=14)-> 1.000000:(tg'=48)&(n'=n-14) ; [] (tg=59)&(n=15)| (tg=60)&(n=15)-> 1.000000:(tg'=47)&(n'=n-15) ; [] (tg=59)&(n=16)| (tg=60)&(n=16)-> 1.000000:(tg'=47)&(n'=n-16) ; [] (tg=59)&(n=16)| (tg=60)&(n=16)-> 1.000000:(tg'=48)&(n'=n-16) ; [] (tg=49)&(n=13..17)| (tg=50)&(n=13..17)-> 1.000000:(tg'=0) ; [] (tg=59)&(n=17)| (tg=60)&(n=17)-> 1.000000:(tg'=47)&(n'=n-17) ; [] (tg=59)&(n=17)| (tg=60)&(n=17)-> 1.000000:(tg'=48)&(n'=n-17) ; [] (tg=59)&(n=18)| (tg=60)&(n=18)-> 1.000000:(tg'=47)&(n'=n-18) ; [] (tg=60)&(n=19)| (tg=59)&(n=19)-> 1.000000:(tg'=47)&(n'=n-19) ; [] (tg=60)&(n=19)| (tg=59)&(n=19)-> 1.000000:(tg'=48)&(n'=n-19) ; [] (tg=59)&(n=20)| (tg=60)&(n=20)-> 1.000000:(tg'=47)&(n'=n-20) ; [] (tg=59)&(n=20)| (tg=60)&(n=20)-> 1.000000:(tg'=48)&(n'=n-20) ; [] (tg=0)&(n=9)| (tg=0)&(n=12)-> 0.500000:(tg'=1)&(n'=n-1) + 0.500000:(tg'=2)&(n'=n-1) ; [] (tg=0)&(n=9)| (tg=0)&(n=12)-> 0.500000:(tg'=3)&(n'=n-2) + 0.500000:(tg'=4)&(n'=n-2) ; [] (tg=1)&(n=0..2)| (tg=1)&(n=4..5)| (tg=1)&(n=7..8)| (tg=1)&(n=10..11)-> 0.500000:(tg'=5) + 0.500000:(tg'=6) ; [] (tg=2)&(n=0..2)| (tg=2)&(n=4..5)| (tg=2)&(n=7..8)| (tg=2)&(n=10..11)-> 0.500000:(tg'=7) + 0.500000:(tg'=8) ; [] (tg=3)&(n=1..2)| (tg=3)&(n=4..5)| (tg=3)&(n=7..8)| (tg=3)&(n=10..11)-> 0.500000:(tg'=5)&(n'=n+1) + 0.500000:(tg'=7)&(n'=n+1) ; [] (tg=4)&(n=1..2)| (tg=4)&(n=4..5)| (tg=4)&(n=7..8)| (tg=4)&(n=10..11)-> 0.500000:(tg'=6)&(n'=n+1) + 0.500000:(tg'=8)&(n'=n+1) ; [] (tg=1)&(n=3)| (tg=1)&(n=6)| (tg=1)&(n=9)| (tg=1)&(n=12)-> 0.500000:(tg'=5)&(n'=n-2) + 0.500000:(tg'=6)&(n'=n-2) ; [] (tg=2)&(n=3)| (tg=2)&(n=6)| (tg=2)&(n=9)| (tg=2)&(n=12)-> 0.500000:(tg'=7)&(n'=n-2) + 0.500000:(tg'=8)&(n'=n-2) ; [] (tg=3)&(n=0)| (tg=3)&(n=3)| (tg=3)&(n=6)| (tg=3)&(n=9)| (tg=3)&(n=12)-> 0.500000:(tg'=5) + 0.500000:(tg'=7) ; [] (tg=4)&(n=0)| (tg=4)&(n=3)| (tg=4)&(n=6)| (tg=4)&(n=9)| (tg=4)&(n=12)-> 0.500000:(tg'=6) + 0.500000:(tg'=8) ; [] (tg=1)&(n=13)| (tg=1)&(n=16)-> 0.500000:(tg'=5)&(n'=n-6) + 0.500000:(tg'=6)&(n'=n-6) ; [] (tg=2)&(n=13)| (tg=2)&(n=16)-> 0.500000:(tg'=7)&(n'=n-6) + 0.500000:(tg'=8)&(n'=n-6) ; [] (tg=1)&(n=18..19)-> 0.500000:(tg'=5)&(n'=n-5) + 0.500000:(tg'=6)&(n'=n-5) ; [] (tg=2)&(n=18..19)-> 0.500000:(tg'=7)&(n'=n-5) + 0.500000:(tg'=8)&(n'