// // This file has been generated with Kappa // // -- state encoding: instances // -- compaction : relative // -- further compaction: no nondeterministic module impl4000 tg : [0..62] init 0; n : [0..147] init 0; [] (tg=32)&(n=0)-> 1.000000:(tg'=41) ; [] (tg=33)&(n=0)-> 1.000000:(tg'=43) ; [] (tg=40)&(n=0)-> 1.000000:(tg'=46) ; [] (tg=42)&(n=0)| (tg=41)&(n=1)-> 1.000000:(tg'=46)&(n'=n+1) ; [] (tg=43)&(n=1)-> 1.000000:(tg'=46)&(n'=n+2) ; [] (tg=55)&(n=0)-> 1.000000:(tg'=59) ; [] (tg=57)&(n=0)-> 1.000000:(tg'=60) ; [] (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=51)&(n=0)-> 1.000000:(tg'=1)&(n'=n+1) ; [] (tg=52)&(n=0)-> 1.000000:(tg'=2)&(n'=n+1) ; [] (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=41)&(n=5)-> 1.000000:(tg'=46)&(n'=n+5) ; [] (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=43)&(n=7)-> 1.000000:(tg'=46)&(n'=n+8) ; [] (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=41)&(n=11)-> 1.000000:(tg'=46)&(n'=n+11) ; [] (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=43)&(n=13)-> 1.000000:(tg'=46)&(n'=n+14) ; [] (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=46)&(n=10)-> 1.000000:(tg'=49)&(n'=n-1) ; [] (tg=46)&(n=10)-> 1.000000:(tg'=50)&(n'=n-1) ; [] (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=46)&(n=13)-> 1.000000:(tg'=49)&(n'=n-3) ; [] (tg=46)&(n=13)-> 1.000000:(tg'=50)&(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=46)&(n=25)-> 1.000000:(tg'=49)&(n'=n-7) ; [] (tg=46)&(n=25)-> 1.000000:(tg'=50)&(n'=n-7) ; [] (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=11)-> 0.500000:(tg'=1)&(n'=n-3) + 0.500000:(tg'=2)&(n'=n-3) ; [] (tg=0)&(n=11)-> 0.500000:(tg'=3)&(n'=n-4) + 0.500000:(tg'=4)&(n'=n-4) ; [] (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=0)&(n=16)-> 0.500000:(tg'=1)&(n'=n-5) + 0.500000:(tg'=2)&(n'=n-5) ; [] (tg=0)&(n=16)-> 0.500000:(tg'=3)&(n'=n-6) + 0.500000:(tg'=4)&(n'=n-6) ; [] (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=14)-> 0.500000:(tg'=5)&(n'=n-4) + 0.500000:(tg'=6)&(n'=n-4) ; [] (tg=2)&(n=14)-> 0.500000:(tg'=7)&(n'=n-4) + 0.500000:(tg'=8)&(n'=n-4) ; [] (tg=3)&(n=14)-> 0.500000:(tg'=5)&(n'=n-2) + 0.500000:(tg'=7)&(n'=n-2) ; [] (tg=4)&(n=14)-> 0.500000:(tg'=6)&(n'=n-2) + 0.500000:(tg'=8)&(n'=n-2) ; [] (tg=3)&(n=15)-> 0.500000:(tg'=5)&(n'=n-6) + 0.500000:(tg'=7)&(n'=n-6) ; [] (tg=4)&(n=15)-> 0.500000:(tg'=6)&(n'=n-6) + 0.500000:(tg'=8)&(n'=n-6) ; [] (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'=n-5) ; [] (tg=3)&(n=13)| (tg=3)&(n=16)| (tg=3)&(n=18..19)-> 0.500000:(tg'=5)&(n'=n-4) + 0.500000:(tg'=7)&(n'=n-4) ; [] (tg=4)&(n=13)| (tg=4)&(n=16)| (tg=4)&(n=18..19)-> 0.500000:(tg'=6)&(n'=n-4) + 0.500000:(tg'=8)&(n'=n-4) ; [] (tg=1)&(n=17)| (tg=1)&(n=20)-> 0.500000:(tg'=5)&(n'=n-7) + 0.500000:(tg'=6)&(n'=n-7) ; [] (tg=2)&(n=17)| (tg=2)&(n=20)-> 0.500000:(tg'=7)&(n'=n-7) + 0.500000:(tg'=8)&(n'=n-7) ; [] (tg=3)&(n=17)| (tg=3)&(n=20)-> 0.500000:(tg'=5)&(n'=n-5) + 0.500000:(tg'=7)&(n'=n-5) ; [] (tg=4)&(n=17)| (tg=4)&(n=20)-> 0.500000:(tg'=6)&(n'=n-5) + 0.500000:(tg'=8)&(n'=n-5) ; [] (tg=1)&(n=21)-> 0.500000:(tg'=5)&(n'=n-11) + 0.500000:(tg'=6)&(n'=n-11) ; [] (tg=2)&(n=21)-> 0.500000:(tg'=7)&(n'=n-11) + 0.500000:(tg'=8)&(n'=n-11) ; [] (tg=3)&(n=21)-> 0.500000:(tg'=5)&(n'=n-9) + 0.500000:(tg'=7)&(n'=n-9) ; [] (tg=4)&(n=21)-> 0.500000:(tg'=6)&(n'=n-9) + 0.500000:(tg'=8)&(n'=n-9) ; [] (tg=1)&(n=22)-> 0.500000:(tg'=5)&(n'=n-9) + 0.500000:(tg'=6)&(n'=n-9) ; [] (tg=2)&(n=22)-> 0.500000:(tg'=7)&(n'=n-9) + 0.500000:(tg'=8)&(n'=n-9) ; [] (tg=9)&(n=0..2)| (tg=9)&(n=4..5)| (tg=9)&(n=7..8)| (tg=9)&(n=10..11)-> 0.500000:(tg'=15) + 0.500000:(tg'=16) ; [] (tg=10)&(n=0..2)| (tg=10)&(n=4..5)| (tg=10)&(n=7..8)| (tg=10)&(n=10..11)-> 0.500000:(tg'=19) + 0.500000:(tg'=20) ; [] (tg=11)&(n=1..2)| (tg=11)&(n=4..5)| (tg=11)&(n=7..8)| (tg=11)&(n=10..11)-> 0.500000:(tg'=13)&(n'=n+1) + 0.500000:(tg'=17)&(n'=n+1) ; [] (tg=12)&(n=1..2)| (tg=12)&(n=4..5)| (tg=12)&(n=7..8)| (tg=12)&(n=10..11)-> 0.500000:(tg'=14)&(n'=n+1) + 0.500000:(tg'=18)&(n'=n+1) ; [] (tg=9)&(n=3)| (tg=9)&(n=6)| (tg=9)&(n=9)| (tg=9)&(n=12)-> 0.500000:(tg'=15)&(n'=n-2) + 0.500000:(tg'=16)&(n'=n-2) ; [] (tg=10)&(n=3)| (tg=10)&(n=6)| (tg=10)&(n=9)| (tg=10)&(n=12)-> 0.500000:(tg'=19)&(n'=n-2) + 0.500000:(tg'=20)&(n'=n-2) ; [] (tg=11)&(n=0)| (tg=11)&(n=3)| (tg=11)&(n=6)| (tg=11)&(n=9)| (tg=11)&(n=12)-> 0.500000:(tg'=13) + 0.500000:(tg'=17) ; [] (tg=12)&(n=0)| (tg=12)&(n=3)| (tg=12)&(n=6)| (tg=12)&(n=9)| (tg=12)&(n=12)-> 0.500000:(tg'=14) + 0.500000:(tg'=18) ; [] (tg=9)&(n=14)-> 0.500000:(tg'=15)&(n'=n-4) + 0.500000:(tg'=16)&(n'=n-4) ; [] (tg=10)&(n=14)-> 0.500000:(tg'=19)&(n'=n-4) + 0.500000:(tg'=20)&(n'=n-4) ; [] (tg=11)&(n=14)-> 0.500000:(tg'=13)&(n'=n-2) + 0.500000:(tg'=17)&(n'=n-2) ; [] (tg=12)&(n=14)-> 0.500000:(tg'=14)&(n'=n-2) + 0.500000:(tg'=18)&(n'=n-2) ; [] (tg=11)&(n=15)-> 0.500000:(tg'=13)&(n'=n-6) + 0.500000:(tg'=17)&(n'=n-6) ; [] (tg=12)&(n=15)-> 0.500000:(tg'=14)&(n'=n-6) + 0.500000:(tg'=18)&(n'=n-6) ; [] (tg=9)&(n=13)| (tg=9)&(n=16)-> 0.500000:(tg'=15)&(n'=n-6) + 0.500000:(tg'=16)&(n'=n-6) ; [] (tg=10)&(n=13)| (tg=10)&(n=16)-> 0.500000:(tg'=19)&(n'=n-6) + 0.500000:(tg'=20)&(n'=n-6) ; [] (tg=9)&(n=18..19)-> 0.500000:(tg'=15)&(n'=n-5) + 0.500000:(tg'=16)&(n'=n-5) ; [] (tg=10)&(n=18..19)-> 0.500000:(tg'=19)&(n'=n-5) + 0.500000:(tg'=20)&(n'=n-5) ; [] (tg=11)&(n=13)| (tg=11)&(n=16)| (tg=11)&(n=18..19)-> 0.500000:(tg'=13)&(n'=n-4) + 0.500000:(tg'=17)&(n'=n-4) ; [] (tg=12)&(n=13)| (tg=12)&(n=16)| (tg=12)&(n=18..19)-> 0.500000:(tg'=14)&(n'=n-4) + 0.500000:(tg'=18)&(n'=n-4) ; [] (tg=9)&(n=17)| (tg=9)&(n=20)-> 0.500000:(tg'=15)&(n'=n-7) + 0.500000:(tg'=16)&(n'=n-7) ; [] (tg=10)&(n=17)| (tg=10)&(n=20)-> 0.500000:(tg'=19)&(n'=n-7) + 0.500000:(tg'=20)&(n'=n-7) ; [] (tg=11)&(n=17)| (tg=11)&(n=20)-> 0.500000:(tg'=13)&(n'=n-5) + 0.500000:(tg'=17)&(n'=n-5) ; [] (tg=12)&(n=17)| (tg=12)&(n=20)-> 0.500000:(tg'=14)&(n'=n-5) + 0.500000:(tg'=18)&(n'=n-5) ; [] (tg=9)&(n=21)-> 0.500000:(tg'=15)&(n'=n-11) + 0.500000:(tg'=16)&(n'=n-11) ; [] (tg=10)&(n=21)-> 0.500000:(tg'=19)&(n'=n-11) + 0.500000:(tg'=20)&(n'=n-11) ; [] (tg=11)&(n=21)-> 0.500000:(tg'=13)&(n'=n-9) + 0.500000:(tg'=17)&(n'=n-9) ; [] (tg=12)&(n=21)-> 0.500000:(tg'=14)&(n'=n-9) + 0.500000:(tg'=18)&(n'=n-9) ; [] (tg=9)&(n=22)-> 0.500000:(tg'=15)&(n'=n-9) + 0.500000:(tg'=16)&(n'=n-9) ; [] (tg=10)&(n=22)-> 0.500000:(tg'=19)&(n'=n-9) + 0.500000:(tg'=20)&(n'=n-9) ; [] (tg=34)&(n=6)| (tg=32)&(n=7)-> 1.000000:(tg'=41)&(n'=n+7) ; [] (tg=34)&(n=6)| (tg=33)&(n=7)-> 1.000000:(tg'=43)&(n'=n+7) ; [] (tg=34)&(n=7)| (tg=32)&(n=8)-> 1.000000:(tg'=41)&(n'=n+8) ; [] (tg=34)&(n=7)| (tg=33)&(n=8)-> 1.000000:(tg'=43)&(n'=n+8) ; [] (tg=34)&(n=8)| (tg=33)&(n=9)-> 1.000000:(tg'=43)&(n'=n+9) ; [] (tg=34)&(n=8)| (tg=32)&(n=9)-> 1.000000:(tg'=41)&(n'=n+9) ; [] (tg=34)&(n=9)| (tg=32)&(n=10)-> 1.000000:(tg'=41)&(n'=n+10) ; [] (tg=34)&(n=9)| (tg=33)&(n=10)-> 1.000000:(tg'=43)&(n'=n+10) ; [] (tg=34)&(n=10)| (tg=32)&(n=11)-> 1.000000:(tg'=41)&(n'=n+11) ; [] (tg=34)&(n=10)| (tg=33)&(n=11)-> 1.000000:(tg'=43)&(n'=n+11) ; [] (tg=34)&(n=11)| (tg=33)&(n=12)-> 1.000000:(tg'=43)&(n'=n+12) ; [] (tg=34)&(n=11)| (tg=32)&(n=12)-> 1.000000:(tg'=41)&(n'=n+12) ; [] (tg=34)&(n=12)| (tg=32)&(n=13)-> 1.000000:(tg'=41)&(n'=n+13) ; [] (tg=34)&(n=12)| (tg=33)&(n=13)-> 1.000000:(tg'=43)&(n'=n+13) ; [] (tg=34)&(n=13)| (tg=32)&(n=14)-> 1.000000:(tg'=41)&(n'=n+14) ; [] (tg=34)&(n=13)| (tg=33)&(n=14)-> 1.000000:(tg'=43)&(n'=n+14) ; [] (tg=34)&(n=14)| (tg=33)&(n=15)-> 1.000000:(tg'=43)&(n'=n+15) ; [] (tg=34)&(n=14)| (tg=32)&(n=15)-> 1.000000:(tg'=41)&(n'=n+15) ; [] (tg=40)&(n=5)| (tg=41)&(n=15)-> 1.000000:(tg'=46)&(n'=n+15) ; [] (tg=42)&(n=5)| (tg=43)&(n=15)-> 1.000000:(tg'=46)&(n'=n+16) ; [] (tg=41)&(n=17)-> 1.000000:(tg'=46)&(n'=n+17) ; [] (tg=40)&(n=6)| (tg=43)&(n=17)-> 1.000000:(tg'=46)&(n'=n+18) ; [] (tg=42)&(n=6)| (tg=41)&(n=19)-> 1.000000:(tg'=46)&(n'=n+19) ; [] (tg=43)&(n=19)-> 1.000000:(tg'=46)&(n'=n+20) ; [] (tg=40)&(n=7)| (tg=41)&(n=21)-> 1.000000:(tg'=46)&(n'=n+21) ; [] (tg=42)&(n=7)| (tg=43)&(n=21)-> 1.000000:(tg'=46)&(n'=n+22) ; [] (tg=41)&(n=23)-> 1.000000:(tg'=46)&(n'=n+23) ; [] (tg=40)&(n=8)| (tg=43)&(n=23)-> 1.000000:(tg'=46)&(n'=n+24) ; [] (tg=42)&(n=8)| (tg=41)&(n=25)-> 1.000000:(tg'=46)&(n'=n+25) ; [] (tg=43)&(n=25)-> 1.000000:(tg'=46)&(n'=n+26) ; [] (tg=40)&(n=9)| (tg=41)&(n=27)-> 1.000000:(tg'=46)&(n'=n+27) ; [] (tg=42)&(n=9)| (tg=43)&(n=27)-> 1.000000:(tg'=46)&(n'=n+28) ; [] (tg=41)&(n=29)-> 1.000000:(tg'=46)&(n'=n+29) ; [] (tg=40)&(n=10)| (tg=43)&(n=29)-> 1.000000:(tg'=46)&(n'=n+30) ; [] (tg=42)&(n=10)| (tg=41)&(n=31)-> 1.000000:(tg'=46)&(n'=n+31) ; [] (tg=43)&(n=31)-> 1.000000:(tg'=46)&(n'=n+32) ; [] (tg=55)&(n=4)| (tg=56)&(n=14..15)-> 1.000000:(tg'=59)&(n'=n+8) ; [] (tg=57)&(n=4)| (tg=58)&(n=14..15)-> 1.000000:(tg'=60)&(n'=n+8) ; [] (tg=46)&(n=21)| (tg=46)&(n=23..24)| (tg=46)&(n=27..32)-> 1.000000:(tg'=49)&(n'=n-8) ; [] (tg=46)&(n=21)| (tg=46)&(n=23..24)| (tg=46)&(n=27..32)-> 1.000000:(tg'=50)&(n'=n-8) ; [] (tg=46)&(n=26)| (tg=46)&(n=34)-> 1.000000:(tg'=49)&(n'=n-9) ; [] (tg=46)&(n=26)| (tg=46)&(n=34)-> 1.000000:(tg'=50)&(n'=n-9) ; [] (tg=56)&(n=16..17)-> 1.000000:(tg'=59)&(n'=n+9) ; [] (tg=58)&(n=16..17)-> 1.000000:(tg'=60)&(n'=n+9) ; [] (tg=46)&(n=37)-> 1.000000:(tg'=49)&(n'=n-11) ; [] (tg=46)&(n=37)-> 1.000000:(tg'=50)&(n'=n-11) ; [] (tg=55)&(n=5)| (tg=56)&(n=18..19)-> 1.000000:(tg'=59)&(n'=n+10) ; [] (tg=57)&(n=5)| (tg=58)&(n=18..19)-> 1.000000:(tg'=60)&(n'=n+10) ; [] (tg=56)&(n=20..21)-> 1.000000:(tg'=59)&(n'=n+11) ; [] (tg=58)&(n=20..21)-> 1.000000:(tg'=60)&(n'=n+11) ; [] (tg=46)&(n=33)| (tg=46)&(n=35..36)| (tg=46)&(n=39..44)-> 1.000000:(tg'=49)&(n'=n-12) ; [] (tg=46)&(n=33)| (tg=46)&(n=35..36)| (tg=46)&(n=39..44)-> 1.000000:(tg'=50)&(n'=n-12) ; [] (tg=46)&(n=38)| (tg=46)&(n=46)-> 1.000000:(tg'=49)&(n'=n-13) ; [] (tg=46)&(n=38)| (tg=46)&(n=46)-> 1.000000:(tg'=50)&(n'=n-13) ; [] (tg=55)&(n=6)| (tg=56)&(n=22..23)-> 1.000000:(tg'=59)&(n'=n+12) ; [] (tg=57)&(n=6)| (tg=58)&(n=22..23)-> 1.000000:(tg'=60)&(n'=n+12) ; [] (tg=46)&(n=49)-> 1.000000:(tg'=49)&(n'=n-15) ; [] (tg=46)&(n=49)-> 1.000000:(tg'=50)&(n'=n-15) ; [] (tg=56)&(n=24..25)-> 1.000000:(tg'=59)&(n'=n+13) ; [] (tg=58)&(n=24..25)-> 1.000000:(tg'=60)&(n'=n+13) ; [] (tg=55)&(n=7)| (tg=56)&(n=26..27)-> 1.000000:(tg'=59)&(n'=n+14) ; [] (tg=57)&(n=7)| (tg=58)&(n=26..27)-> 1.000000:(tg'=60)&(n'=n+14) ; [] (tg=46)&(n=45)| (tg=46)&(n=47..48)| (tg=46)&(n=51..56)-> 1.000000:(tg'=49)&(n'=n-16) ; [] (tg=46)&(n=45)| (tg=46)&(n=47..48)| (tg=46)&(n=51..56)-> 1.000000:(tg'=50)&(n'=n-16) ; [] (tg=46)&(n=50)| (tg=46)&(n=58)-> 1.000000:(tg'=49)&(n'=n-17) ; [] (tg=46)&(n=50)| (tg=46)&(n=58)-> 1.000000:(tg'=50)&(n'=n-17) ; [] (tg=56)&(n=28..29)-> 1.000000:(tg'=59)&(n'=n+15) ; [] (tg=58)&(n=28..29)-> 1.000000:(tg'=60)&(n'=n+15) ; [] (tg=46)&(n=61)-> 1.000000:(tg'=49)&(n'=n-19) ; [] (tg=46)&(n=61)-> 1.000000:(tg'=50)&(n'=n-19) ; [] (tg=55)&(n=8)| (tg=56)&(n=30..31)-> 1.000000:(tg'=59)&(n'=n+16) ; [] (tg=57)&(n=8)| (tg=58)&(n=30..31)-> 1.000000:(tg'=60)&(n'=n+16) ; [] (tg=59)&(n=21)| (tg=60)&(n=21)-> 1.000000:(tg'=47)&(n'=n-21) ; [] (tg=59)&(n=22)| (tg=60)&(n=22)-> 1.000000:(tg'=47)&(n'=n-22) ; [] (tg=59)&(n=22)| (tg=60)&(n=22)-> 1.000000:(tg'=48)&(n'=n-22) ; [] (tg=59)&(n=23)| (tg=60)&(n=23)-> 1.000000:(tg'=47)&(n'=n-23) ; [] (tg=59)&(n=23)| (tg=60)&(n=23)-> 1.000000:(tg'=48)&(n'=n-23) ; [] (tg=59)&(n=24)| (tg=60)&(n=24)-> 1.000000:(tg'=47)&(n'=n-24) ; [] (tg=59)&(n=25)| (tg=60)&(n=25)-> 1.000000:(tg'=47)&(n'=n-25) ; [] (tg=59)&(n=25)| (tg=60)&(n=25)-> 1.000000:(tg'=48)&(n'=n-25) ; [] (tg=59)&(n=26)| (tg=60)&(n=26)-> 1.000000:(tg'=47)&(n'=n-26) ; [] (tg=59)&(n=26)| (tg=60)&(n=26)-> 1.000000:(tg'=48)&(n'=n-26) ; [] (tg=59)&(n=27)| (tg=60)&(n=27)-> 1.000000:(tg'=47)&(n'=n-27) ; [] (tg=60)&(n=28)| (tg=59)&(n=28)-> 1.000000:(tg'=47)&(n'=n-28) ; [] (tg=60)&(n=28)| (tg=59)&(n=28)-> 1.000000:(tg'=48)&(n'=n-28) ; [] (tg=49)&(n=19..27)| (tg=50)&(n=19..27)-> 1.000000:(tg'=0)&(n'=n-1) ; [] (tg=59)&(n=29)| (tg=60)&(n=29)-> 1.000000:(tg'=47)&(n'=n-29) ; [] (tg=59)&(n=29)| (tg=60)&(n=29)-> 1.000000:(tg'=48)&(n'=n-29) ; [] (tg=49)&(n=28)| (tg=50)&(n=28)-> 1.000000:(tg'=0)&(n'=n-7) ; [] (tg=59)&(n=30)| (tg=60)&(n=30)-> 1.000000:(tg'=47)&(n'=n-30) ; [] (tg=59)&(n=30)| (tg=60)&(n=30)-> 1.000000:(tg'=48)&(n'=n-30) ; [] (tg=59)&(n=31)| (tg=60)&(n=31)-> 1.000000:(tg'=47)&(n'=n-31) ; [] (tg=59)&(n=31)| (tg=60)&(n=31)-> 1.000000:(tg'=48)&(n'=n-31) ; [] (tg=59)&(n=32)| (tg=60)&(n=32)-> 1.000000:(tg'=47)&(n'=n-32) ; [] (tg=59)&(n=32)| (tg=60)&(n=32)-> 1.000000:(tg'=48)&(n'=n-32) ; [] (tg=59)&(n=33)| (tg=60)&(n=33)-> 1.000000:(tg'=47)&(n'=n-33) ; [] (tg=59)&(n=33)| (tg=60)&(n=33)-> 1.000000:(tg'=48)&(n'=n-33) ; [] (tg=59)&(n=34)| (tg=60)&(n=34)-> 1.000000:(tg'=47)&(n'=n-34) ; [] (tg=59)&(n=34)| (tg=60)&(n=34)-> 1.000000:(tg'=48)&(n'=n-34) ; [] (tg=49)&(n=29..33)| (tg=50)&(n=29..33)-> 1.000000:(tg'=0)&(n'=n-2) ; [] (tg=59)&(n=35)| (tg=60)&(n=35)-> 1.000000:(tg'=47)&(n'=n-35) ; [] (tg=59)&(n=35)| (tg=60)&(n=35)-> 1.000000:(tg'=48)&(n'=n-35) ; [] (tg=59)&(n=36)| (tg=60)&(n=36)-> 1.000000:(tg'=47)&(n'=n-36) ; [] (tg=59)&(n=36)| (tg=60)&(n=36)-> 1.000000:(tg'=48)&(n'=n-36) ; [] (tg=60)&(n=37)| (tg=59)&(n=37)-> 1.000000:(tg'=47