//
// This file has been generated with Kappa
//
// -- state encoding: instances
// -- compaction : absolute
// -- further compaction: no

nondeterministic

module impl4000 

tg : [0..62] init 0; 
n : [0..147] init 0;

[] (tg=0)&(n=0)-> 0.500000:(tg'=1)&(n'=0) + 0.500000:(tg'=2)&(n'=0) ;
[] (tg=0)&(n=0)-> 0.500000:(tg'=3)&(n'=0) + 0.500000:(tg'=4)&(n'=0) ;
[] (tg=1)&(n=0)-> 0.500000:(tg'=5)&(n'=0) + 0.500000:(tg'=6)&(n'=0) ;
[] (tg=1)&(n=0)-> 1.000000:(tg'=9)&(n'=0) ;
[] (tg=2)&(n=0)-> 0.500000:(tg'=7)&(n'=0) + 0.500000:(tg'=8)&(n'=0) ;
[] (tg=2)&(n=0)-> 1.000000:(tg'=10)&(n'=0) ;
[] (tg=3)&(n=0)-> 1.000000:(tg'=11)&(n'=0) ;
[] (tg=3)&(n=0)-> 0.500000:(tg'=5)&(n'=0) + 0.500000:(tg'=7)&(n'=0) ;
[] (tg=4)&(n=0)-> 1.000000:(tg'=12)&(n'=0) ;
[] (tg=4)&(n=0)-> 0.500000:(tg'=6)&(n'=0) + 0.500000:(tg'=8)&(n'=0) ;
[] (tg=5)&(n=0)-> 1.000000:(tg'=13)&(n'=0) ;
[] (tg=5)&(n=0)-> 1.000000:(tg'=15)&(n'=0) ;
[] (tg=6)&(n=0)-> 1.000000:(tg'=14)&(n'=0) ;
[] (tg=6)&(n=0)-> 1.000000:(tg'=16)&(n'=0) ;
[] (tg=9)&(n=0)-> 0.500000:(tg'=15)&(n'=0) + 0.500000:(tg'=16)&(n'=0) ;
[] (tg=7)&(n=0)-> 1.000000:(tg'=17)&(n'=0) ;
[] (tg=7)&(n=0)-> 1.000000:(tg'=19)&(n'=0) ;
[] (tg=8)&(n=0)-> 1.000000:(tg'=18)&(n'=0) ;
[] (tg=8)&(n=0)-> 1.000000:(tg'=20)&(n'=0) ;
[] (tg=10)&(n=0)-> 0.500000:(tg'=19)&(n'=0) + 0.500000:(tg'=20)&(n'=0) ;
[] (tg=11)&(n=0)-> 0.500000:(tg'=13)&(n'=0) + 0.500000:(tg'=17)&(n'=0) ;
[] (tg=12)&(n=0)-> 0.500000:(tg'=14)&(n'=0) + 0.500000:(tg'=18)&(n'=0) ;
[] (tg=13)&(n=0)| (tg=15)&(n=0)-> 1.000000:(tg'=31)&(n'=0) ;
[] (tg=14)&(n=0)| (tg=16)&(n=0)-> 1.000000:(tg'=32)&(n'=0) ;
[] (tg=17)&(n=0)| (tg=19)&(n=0)-> 1.000000:(tg'=33)&(n'=0) ;
[] (tg=18)&(n=0)| (tg=20)&(n=0)-> 1.000000:(tg'=34)&(n'=0) ;
[] (tg=31)&(n=0)-> 1.000000:(tg'=40)&(n'=0) ;
[] (tg=31)&(n=0)-> 1.000000:(tg'=42)&(n'=0) ;
[] (tg=32)&(n=0)-> 1.000000:(tg'=41)&(n'=0) ;
[] (tg=33)&(n=0)-> 1.000000:(tg'=43)&(n'=0) ;
[] (tg=34)&(n=0)-> 1.000000:(tg'=41)&(n'=1) ;
[] (tg=34)&(n=0)-> 1.000000:(tg'=43)&(n'=1) ;
[] (tg=40)&(n=0)-> 1.000000:(tg'=46)&(n'=0) ;
[] (tg=40)&(n=0)-> 1.000000:(tg'=55)&(n'=0) ;
[] (tg=42)&(n=0)-> 1.000000:(tg'=46)&(n'=1) ;
[] (tg=42)&(n=0)-> 1.000000:(tg'=57)&(n'=0) ;
[] (tg=41)&(n=0)-> 1.000000:(tg'=56)&(n'=0) ;
[] (tg=43)&(n=0)-> 1.000000:(tg'=58)&(n'=0) ;
[] (tg=41)&(n=1)-> 1.000000:(tg'=46)&(n'=2) ;
[] (tg=41)&(n=1)-> 1.000000:(tg'=56)&(n'=1) ;
[] (tg=43)&(n=1)-> 1.000000:(tg'=46)&(n'=3) ;
[] (tg=43)&(n=1)-> 1.000000:(tg'=58)&(n'=1) ;
[] (tg=46)&(n=0)-> 1.000000:(tg'=49)&(n'=0) ;
[] (tg=46)&(n=0)-> 1.000000:(tg'=50)&(n'=0) ;
[] (tg=55)&(n=0)-> 1.000000:(tg'=59)&(n'=0) ;
[] (tg=46)&(n=1)-> 1.000000:(tg'=49)&(n'=1) ;
[] (tg=46)&(n=1)-> 1.000000:(tg'=50)&(n'=1) ;
[] (tg=57)&(n=0)-> 1.000000:(tg'=60)&(n'=0) ;
[] (tg=56)&(n=0)-> 1.000000:(tg'=59)&(n'=1) ;
[] (tg=58)&(n=0)-> 1.000000:(tg'=60)&(n'=1) ;
[] (tg=46)&(n=2)-> 1.000000:(tg'=49)&(n'=2) ;
[] (tg=46)&(n=2)-> 1.000000:(tg'=50)&(n'=2) ;
[] (tg=56)&(n=1)-> 1.000000:(tg'=59)&(n'=2) ;
[] (tg=46)&(n=3)-> 1.000000:(tg'=49)&(n'=3) ;
[] (tg=46)&(n=3)-> 1.000000:(tg'=50)&(n'=3) ;
[] (tg=58)&(n=1)-> 1.000000:(tg'=60)&(n'=2) ;
[] (tg=49)&(n=0)-> 0.500000:(tg'=51)&(n'=0) + 0.500000:(tg'=52)&(n'=0) ;
[] (tg=49)&(n=0)| (tg=50)&(n=0)-> 1.000000:(tg'=0)&(n'=1) ;
[] (tg=50)&(n=0)-> 0.500000:(tg'=53)&(n'=0) + 0.500000:(tg'=54)&(n'=0) ;
[] (tg=49)&(n=1)-> 0.500000:(tg'=51)&(n'=1) + 0.500000:(tg'=52)&(n'=1) ;
[] (tg=49)&(n=1)| (tg=50)&(n=1)-> 1.000000:(tg'=0)&(n'=2) ;
[] (tg=50)&(n=1)-> 0.500000:(tg'=53)&(n'=1) + 0.500000:(tg'=54)&(n'=1) ;
[] (tg=49)&(n=2)-> 0.500000:(tg'=51)&(n'=2) + 0.500000:(tg'=52)&(n'=2) ;
[] (tg=49)&(n=2)| (tg=50)&(n=2)-> 1.000000:(tg'=0)&(n'=3) ;
[] (tg=50)&(n=2)-> 0.500000:(tg'=53)&(n'=2) + 0.500000:(tg'=54)&(n'=2) ;
[] (tg=49)&(n=3)-> 0.500000:(tg'=51)&(n'=3) + 0.500000:(tg'=52)&(n'=3) ;
[] (tg=49)&(n=3)| (tg=50)&(n=3)-> 1.000000:(tg'=0)&(n'=4) ;
[] (tg=50)&(n=3)-> 0.500000:(tg'=53)&(n'=3) + 0.500000:(tg'=54)&(n'=3) ;
[] (tg=51)&(n=0)-> 1.000000:(tg'=1)&(n'=1) ;
[] (tg=52)&(n=0)-> 1.000000:(tg'=2)&(n'=1) ;
[] (tg=53)&(n=0)-> 1.000000:(tg'=3)&(n'=2) ;
[] (tg=54)&(n=0)-> 1.000000:(tg'=4)&(n'=2) ;
[] (tg=51)&(n=1)-> 1.000000:(tg'=1)&(n'=3) ;
[] (tg=52)&(n=1)-> 1.000000:(tg'=2)&(n'=3) ;
[] (tg=0)&(n=1..2)-> 0.500000:(tg'=1)&(n'=2) + 0.500000:(tg'=2)&(n'=2) ;
[] (tg=0)&(n=1..2)-> 0.500000:(tg'=3)&(n'=1) + 0.500000:(tg'=4)&(n'=1) ;
[] (tg=53)&(n=1)-> 1.000000:(tg'=3)&(n'=3) ;
[] (tg=54)&(n=1)-> 1.000000:(tg'=4)&(n'=3) ;
[] (tg=51)&(n=2)-> 1.000000:(tg'=1)&(n'=4) ;
[] (tg=52)&(n=2)-> 1.000000:(tg'=2)&(n'=4) ;
[] (tg=53)&(n=2)-> 1.000000:(tg'=3)&(n'=5) ;
[] (tg=54)&(n=2)-> 1.000000:(tg'=4)&(n'=5) ;
[] (tg=51)&(n=3)-> 1.000000:(tg'=1)&(n'=6) ;
[] (tg=52)&(n=3)-> 1.000000:(tg'=2)&(n'=6) ;
[] (tg=0)&(n=3..4)-> 0.500000:(tg'=1)&(n'=5) + 0.500000:(tg'=2)&(n'=5) ;
[] (tg=0)&(n=3..4)-> 0.500000:(tg'=3)&(n'=4) + 0.500000:(tg'=4)&(n'=4) ;
[] (tg=53)&(n=3)-> 1.000000:(tg'=3)&(n'=6) ;
[] (tg=54)&(n=3)-> 1.000000:(tg'=4)&(n'=6) ;
[] (tg=1)&(n=1)-> 1.000000:(tg'=9)&(n'=1) ;
[] (tg=2)&(n=1)-> 1.000000:(tg'=10)&(n'=1) ;
[] (tg=1)&(n=2)-> 0.500000:(tg'=5)&(n'=2) + 0.500000:(tg'=6)&(n'=2) ;
[] (tg=1)&(n=2)-> 1.000000:(tg'=9)&(n'=2) ;
[] (tg=2)&(n=2)-> 0.500000:(tg'=7)&(n'=2) + 0.500000:(tg'=8)&(n'=2) ;
[] (tg=2)&(n=2)-> 1.000000:(tg'=10)&(n'=2) ;
[] (tg=3)&(n=1)-> 1.000000:(tg'=11)&(n'=1) ;
[] (tg=3)&(n=1)-> 0.500000:(tg'=5)&(n'=2) + 0.500000:(tg'=7)&(n'=2) ;
[] (tg=4)&(n=1)-> 1.000000:(tg'=12)&(n'=1) ;
[] (tg=4)&(n=1)-> 0.500000:(tg'=6)&(n'=2) + 0.500000:(tg'=8)&(n'=2) ;
[] (tg=3)&(n=2)-> 1.000000:(tg'=11)&(n'=2) ;
[] (tg=4)&(n=2)-> 1.000000:(tg'=12)&(n'=2) ;
[] (tg=1)&(n=1)| (tg=1)&(n=3)-> 0.500000:(tg'=5)&(n'=1) + 0.500000:(tg'=6)&(n'=1) ;
[] (tg=1)&(n=3)-> 1.000000:(tg'=9)&(n'=3) ;
[] (tg=2)&(n=1)| (tg=2)&(n=3)-> 0.500000:(tg'=7)&(n'=1) + 0.500000:(tg'=8)&(n'=1) ;
[] (tg=2)&(n=3)-> 1.000000:(tg'=10)&(n'=3) ;
[] (tg=3)&(n=3)-> 1.000000:(tg'=11)&(n'=3) ;
[] (tg=3)&(n=2..3)-> 0.500000:(tg'=5)&(n'=3) + 0.500000:(tg'=7)&(n'=3) ;
[] (tg=4)&(n=3)-> 1.000000:(tg'=12)&(n'=3) ;
[] (tg=4)&(n=2..3)-> 0.500000:(tg'=6)&(n'=3) + 0.500000:(tg'=8)&(n'=3) ;
[] (tg=1)&(n=4)-> 1.000000:(tg'=9)&(n'=4) ;
[] (tg=2)&(n=4)-> 1.000000:(tg'=10)&(n'=4) ;
[] (tg=1)&(n=5)-> 0.500000:(tg'=5)&(n'=5) + 0.500000:(tg'=6)&(n'=5) ;
[] (tg=1)&(n=5)-> 1.000000:(tg'=9)&(n'=5) ;
[] (tg=2)&(n=5)-> 0.500000:(tg'=7)&(n'=5) + 0.500000:(tg'=8)&(n'=5) ;
[] (tg=2)&(n=5)-> 1.000000:(tg'=10)&(n'=5) ;
[] (tg=3)&(n=4)-> 1.000000:(tg'=11)&(n'=4) ;
[] (tg=3)&(n=4)-> 0.500000:(tg'=5)&(n'=5) + 0.500000:(tg'=7)&(n'=5) ;
[] (tg=4)&(n=4)-> 1.000000:(tg'=12)&(n'=4) ;
[] (tg=4)&(n=4)-> 0.500000:(tg'=6)&(n'=5) + 0.500000:(tg'=8)&(n'=5) ;
[] (tg=3)&(n=5)-> 1.000000:(tg'=11)&(n'=5) ;
[] (tg=4)&(n=5)-> 1.000000:(tg'=12)&(n'=5) ;
[] (tg=1)&(n=4)| (tg=1)&(n=6)-> 0.500000:(tg'=5)&(n'=4) + 0.500000:(tg'=6)&(n'=4) ;
[] (tg=1)&(n=6)-> 1.000000:(tg'=9)&(n'=6) ;
[] (tg=2)&(n=4)| (tg=2)&(n=6)-> 0.500000:(tg'=7)&(n'=4) + 0.500000:(tg'=8)&(n'=4) ;
[] (tg=2)&(n=6)-> 1.000000:(tg'=10)&(n'=6) ;
[] (tg=3)&(n=6)-> 1.000000:(tg'=11)&(n'=6) ;
[] (tg=3)&(n=5..6)-> 0.500000:(tg'=5)&(n'=6) + 0.500000:(tg'=7)&(n'=6) ;
[] (tg=4)&(n=6)-> 1.000000:(tg'=12)&(n'=6) ;
[] (tg=4)&(n=5..6)-> 0.500000:(tg'=6)&(n'=6) + 0.500000:(tg'=8)&(n'=6) ;
[] (tg=5)&(n=1)-> 1.000000:(tg'=13)&(n'=1) ;
[] (tg=5)&(n=1)-> 1.000000:(tg'=15)&(n'=1) ;
[] (tg=6)&(n=1)-> 1.000000:(tg'=14)&(n'=1) ;
[] (tg=6)&(n=1)-> 1.000000:(tg'=16)&(n'=1) ;
[] (tg=7)&(n=1)-> 1.000000:(tg'=17)&(n'=1) ;
[] (tg=7)&(n=1)-> 1.000000:(tg'=19)&(n'=1) ;
[] (tg=8)&(n=1)-> 1.000000:(tg'=18)&(n'=1) ;
[] (tg=8)&(n=1)-> 1.000000:(tg'=20)&(n'=1) ;
[] (tg=5)&(n=2)-> 1.000000:(tg'=13)&(n'=2) ;
[] (tg=5)&(n=2)-> 1.000000:(tg'=15)&(n'=2) ;
[] (tg=6)&(n=2)-> 1.000000:(tg'=14)&(n'=2) ;
[] (tg=6)&(n=2)-> 1.000000:(tg'=16)&(n'=2) ;
[] (tg=9)&(n=2)-> 0.500000:(tg'=15)&(n'=2) + 0.500000:(tg'=16)&(n'=2) ;
[] (tg=7)&(n=2)-> 1.000000:(tg'=17)&(n'=2) ;
[] (tg=7)&(n=2)-> 1.000000:(tg'=19)&(n'=2) ;
[] (tg=8)&(n=2)-> 1.000000:(tg'=18)&(n'=2) ;
[] (tg=8)&(n=2)-> 1.000000:(tg'=20)&(n'=2) ;
[] (tg=10)&(n=2)-> 0.500000:(tg'=19)&(n'=2) + 0.500000:(tg'=20)&(n'=2) ;
[] (tg=11)&(n=1)-> 0.500000:(tg'=13)&(n'=2) + 0.500000:(tg'=17)&(n'=2) ;
[] (tg=12)&(n=1)-> 0.500000:(tg'=14)&(n'=2) + 0.500000:(tg'=18)&(n'=2) ;
[] (tg=5)&(n=3)-> 1.000000:(tg'=13)&(n'=3) ;
[] (tg=5)&(n=3)-> 1.000000:(tg'=15)&(n'=3) ;
[] (tg=7)&(n=3)-> 1.000000:(tg'=17)&(n'=3) ;
[] (tg=7)&(n=3)-> 1.000000:(tg'=19)&(n'=3) ;
[] (tg=6)&(n=3)-> 1.000000:(tg'=14)&(n'=3) ;
[] (tg=6)&(n=3)-> 1.000000:(tg'=16)&(n'=3) ;
[] (tg=8)&(n=3)-> 1.000000:(tg'=18)&(n'=3) ;
[] (tg=8)&(n=3)-> 1.000000:(tg'=20)&(n'=3) ;
[] (tg=9)&(n=1)| (tg=9)&(n=3)-> 0.500000:(tg'=15)&(n'=1) + 0.500000:(tg'=16)&(n'=1) ;
[] (tg=10)&(n=1)| (tg=10)&(n=3)-> 0.500000:(tg'=19)&(n'=1) + 0.500000:(tg'=20)&(n'=1) ;
[] (tg=11)&(n=2..3)-> 0.500000:(tg'=13)&(n'=3) + 0.500000:(tg'=17)&(n'=3) ;
[] (tg=12)&(n=2..3)-> 0.500000:(tg'=14)&(n'=3) + 0.500000:(tg'=18)&(n'=3) ;
[] (tg=5)&(n=4)-> 1.000000:(tg'=13)&(n'=4) ;
[] (tg=5)&(n=4)-> 1.000000:(tg'=15)&(n'=4) ;
[] (tg=6)&(n=4)-> 1.000000:(tg'=14)&(n'=4) ;
[] (tg=6)&(n=4)-> 1.000000:(tg'=16)&(n'=4) ;
[] (tg=7)&(n=4)-> 1.000000:(tg'=17)&(n'=4) ;
[] (tg=7)&(n=4)-> 1.000000:(tg'=19)&(n'=4) ;
[] (tg=8)&(n=4)-> 1.000000:(tg'=18)&(n'=4) ;
[] (tg=8)&(n=4)-> 1.000000:(tg'=20)&(n'=4) ;
[] (tg=5)&(n=5)-> 1.000000:(tg'=13)&(n'=5) ;
[] (tg=5)&(n=5)-> 1.000000:(tg'=15)&(n'=5) ;
[] (tg=6)&(n=5)-> 1.000000:(tg'=14)&(n'=5) ;
[] (tg=6)&(n=5)-> 1.000000:(tg'=16)&(n'=5) ;
[] (tg=9)&(n=5)-> 0.500000:(tg'=15)&(n'=5) + 0.500000:(tg'=16)&(n'=5) ;
[] (tg=7)&(n=5)-> 1.000000:(tg'=17)&(n'=5) ;
[] (tg=7)&(n=5)-> 1.000000:(tg'=19)&(n'=5) ;
[] (tg=8)&(n=5)-> 1.000000:(tg'=18)&(n'=5) ;
[] (tg=8)&(n=5)-> 1.000000:(tg'=20)&(n'=5) ;
[] (tg=10)&(n=5)-> 0.500000:(tg'=19)&(n'=5) + 0.500000:(tg'=20)&(n'=5) ;
[] (tg=11)&(n=4)-> 0.500000:(tg'=13)&(n'=5) + 0.500000:(tg'=17)&(n'=5) ;
[] (tg=12)&(n=4)-> 0.500000:(tg'=14)&(n'=5) + 0.500000:(tg'=18)&(n'=5) ;
[] (tg=5)&(n=6)-> 1.000000:(tg'=13)&(n'=6) ;
[] (tg=5)&(n=6)-> 1.000000:(tg'=15)&(n'=6) ;
[] (tg=7)&(n=6)-> 1.000000:(tg'=17)&(n'=6) ;
[] (tg=7)&(n=6)-> 1.000000:(tg'=19)&(n'=6) ;
[] (tg=6)&(n=6)-> 1.000000:(tg'=14)&(n'=6) ;
[] (tg=6)&(n=6)-> 1.000000:(tg'=16)&(n'=6) ;
[] (tg=8)&(n=6)-> 1.000000:(tg'=18)&(n'=6) ;
[] (tg=8)&(n=6)-> 1.000000:(tg'=20)&(n'=6) ;
[] (tg=9)&(n=4)| (tg=9)&(n=6)-> 0.500000:(tg'=15)&(n'=4) + 0.500000:(tg'=16)&(n'=4) ;
[] (tg=10)&(n=4)| (tg=10)&(n=6)-> 0.500000:(tg'=19)&(n'=4) + 0.500000:(tg'=20)&(n'=4) ;
[] (tg=11)&(n=5..6)-> 0.500000:(tg'=13)&(n'=6) + 0.500000:(tg'=17)&(n'=6) ;
[] (tg=12)&(n=5..6)-> 0.500000:(tg'=14)&(n'=6) + 0.500000:(tg'=18)&(n'=6) ;
[] (tg=13)&(n=1)| (tg=15)&(n=1)-> 1.000000:(tg'=31)&(n'=1) ;
[] (tg=14)&(n=1)| (tg=16)&(n=1)-> 1.000000:(tg'=32)&(n'=1) ;
[] (tg=17)&(n=1)| (tg=19)&(n=1)-> 1.000000:(tg'=33)&(n'=1) ;
[] (tg=18)&(n=1)| (tg=20)&(n=1)-> 1.000000:(tg'=34)&(n'=1) ;
[] (tg=13)&(n=2)| (tg=15)&(n=2)-> 1.000000:(tg'=31)&(n'=2) ;
[] (tg=14)&(n=2)| (tg=16)&(n=2)-> 1.000000:(tg'=32)&(n'=2) ;
[] (tg=17)&(n=2)| (tg=19)&(n=2)-> 1.000000:(tg'=33)&(n'=2) ;
[] (tg=18)&(n=2)| (tg=20)&(n=2)-> 1.000000:(tg'=34)&(n'=2) ;
[] (tg=13)&(n=3)| (tg=15)&(n=3)-> 1.000000:(tg'=31)&(n'=3) ;
[] (tg=17)&(n=3)| (tg=19)&(n=3)-> 1.000000:(tg'=33)&(n'=3) ;
[] (tg=14)&(n=3)| (tg=16)&(n=3)-> 1.000000:(tg'=32)&(n'=3) ;
[] (tg=18)&(n=3)| (tg=20)&(n=3)-> 1.000000:(tg'=34)&(n'=3) ;
[] (tg=13)&(n=4)| (tg=15)&(n=4)-> 1.000000:(tg'=31)&(n'=4) ;
[] (tg=14)&(n=4)| (tg=16)&(n=4)-> 1.000000:(tg'=32)&(n'=4) ;
[] (tg=17)&(n=4)| (tg=19)&(n=4)-> 1.000000:(tg'=33)&(n'=4) ;
[] (tg=18)&(n=4)| (tg=20)&(n=4)-> 1.000000:(tg'=34)&(n'=4) ;
[] (tg=13)&(n=5)| (tg=15)&(n=5)-> 1.000000:(tg'=31)&(n'=5) ;
[] (tg=14)&(n=5)| (tg=16)&(n=5)-> 1.000000:(tg'=32)&(n'=5) ;
[] (tg=17)&(n=5)| (tg=19)&(n=5)-> 1.000000:(tg'=33)&(n'=5) ;
[] (tg=18)&(n=5)| (tg=20)&(n=5)-> 1.000000:(tg'=34)&(n'=5) ;
[] (tg=13)&(n=6)| (tg=15)&(n=6)-> 1.000000:(tg'=31)&(n'=6) ;
[] (tg=17)&(n=6)| (tg=19)&(n=6)-> 1.000000:(tg'=33)&(n'=6) ;
[] (tg=14)&(n=6)| (tg=16)&(n=6)-> 1.000000:(tg'=32)&(n'=6) ;
[] (tg=18)&(n=6)| (tg=20)&(n=6)-> 1.000000:(tg'=34)&(n'=6) ;
[] (tg=31)&(n=1)-> 1.000000:(tg'=40)&(n'=1) ;
[] (tg=31)&(n=1)-> 1.000000:(tg'=42)&(n'=1) ;
[] (tg=32)&(n=1)-> 1.000000:(tg'=41)&(n'=2) ;
[] (tg=33)&(n=1)-> 1.000000:(tg'=43)&(n'=2) ;
[] (tg=34)&(n=1)-> 1.000000:(tg'=41)&(n'=3) ;
[] (tg=34)&(n=1)-> 1.000000:(tg'=43)&(n'=3) ;
[] (tg=31)&(n=2)-> 1.000000:(tg'=40)&(n'=2) ;
[] (tg=31)&(n=2)-> 1.000000:(tg'=42)&(n'=2) ;
[] (tg=32)&(n=2)-> 1.000000:(tg'=41)&(n'=4) ;
[] (tg=33)&(n=2)-> 1.000000:(tg'=43)&(n'=4) ;
[] (tg=34)&(n=2)-> 1.000000:(tg'=41)&(n'=5) ;
[] (tg=34)&(n=2)-> 1.000000:(tg'=43)&(n'=5) ;
[] (tg=31)&(n=3)-> 1.000000:(tg'=40)&(n'=3) ;
[] (tg=31)&(n=3)-> 1.000000:(tg'=42)&(n'=3) ;
[] (tg=33)&(n=3)-> 1.000000:(tg'=43)&(n'=6) ;
[] (tg=32)&(n=3)-> 1.000000:(tg'=41)&(n'=6) ;
[] (tg=34)&(n=3)-> 1.000000:(tg'=41)&(n'=7) ;
[] (tg=34)&(n=3)-> 1.000000:(tg'=43)&(n'=7) ;
[] (tg=31)&(n=4)-> 1.000000:(tg'=40)&(n'=4) ;
[] (tg=31)&(n=4)-> 1.000000:(tg'=42)&(n'=4) ;
[] (tg=32)&(n=4)-> 1.000000:(tg'=41)&(n'=8) ;
[] (tg=33)&(n=4)-> 1.000000:(tg'=43)&(n'=8) ;
[] (tg=34)&(n=4)-> 1.000000:(tg'=41)&(n'=9) ;
[] (tg=34)&(n=4)-> 1.000000:(tg'=43)&(n'=9) ;
[] (tg=31)&(n=5)-> 1.000000:(tg'=40)&(n'=5) ;
[] (tg=31)&(n=5)-> 1.000000:(tg'=42)&(n'=5) ;
[] (tg=32)&(n=5)-> 1.000000:(tg'=41)&(n'=10) ;
[] (tg=33)&(n=5)-> 1.000000:(tg'=43)&(n'=10) ;
[] (tg=34)&(n=5)-> 1.000000:(tg'=41)&(n'=11) ;
[] (tg=34)&(n=5)-> 1.000000:(tg'=43)&(n'=11) ;
[] (tg=31)&(n=6)-> 1.000000:(tg'=40)&(n'=6) ;
[] (tg=31)&(n=6)-> 1.000000:(tg'=42)&(n'=6) ;
[] (tg=33)&(n=6)-> 1.000000:(tg'=43)&(n'=12) ;
[] (tg=32)&(n=6)-> 1.000000:(tg'=41)&(n'=12) ;
[] (tg=34)&(n=6)-> 1.000000:(tg'=41)&(n'=13) ;
[] (tg=34)&(n=6)-> 1.000000:(tg'=43)&(n'=13) ;
[] (tg=40)&(n=1)-> 1.000000:(tg'=46)&(n'=4) ;
[] (tg=40)&(n=1)-> 1.000000:(tg'=55)&(n'=1) ;
[] (tg=42)&(n=1)-> 1.000000:(tg'=46)&(n'=5) ;
[] (tg=42)&(n=1)-> 1.000000:(tg'=57)&(n'=1) ;
[] (tg=41)&(n=2)-> 1.000000:(tg'=56)&(n'=2) ;
[] (tg=43)&(n=2)-> 1.000000:(tg'=58)&(n'=2) ;
[] (tg=41)&(n=3)-> 1.000000:(tg'=46)&(n'=6) ;
[] (tg=41)&(n=3)-> 1.000000:(tg'=56)&(n'=3) ;
[] (tg=43)&(n=3)-> 1.000000:(tg'=46)&(n'=7) ;
[] (tg=43)&(n=3)-> 1.000000:(tg'=58)&(n'=3) ;
[] (tg=40)&(n=2)-> 1.000000:(tg'=46)&(n'=8) ;
[] (tg=40)&(n=2)-> 1.000000:(tg'=55)&(n'=2) ;
[] (tg=42)&(n=2)-> 1.000000:(tg'=46)&(n'=9) ;
[] (tg=42)&(n=2)-> 1.000000:(tg'=57)&(n'=2) ;
[] (tg=41)&(n=4)-> 1.000000:(tg'=56)&(n'=4) ;
[] (tg=43)&(n=4)-> 1.000000:(tg'=58)&(n'=4) ;
[] (tg=41)&(n=5)-> 1.000000:(tg'=46)&(n'=10) ;
[] (tg=41)&(n=5)-> 1.000000:(tg'=56)&(n'=5) ;
[] (tg=43)&(n=5)-> 1.000000:(tg'=46)&(n'=11) ;
[] (tg=43)&(n=5)-> 1.000000:(tg'=58)&(n'=5) ;
[] (tg=40)&(n=3)-> 1.000000:(tg'=46)&(n'=12) ;
[] (tg=40)&(n=3)-> 1.000000:(tg'=55)&(n'=3) ;
[] (tg=42)&(n=3)-> 1.000000:(tg'=46)&(n'=13) ;
[] (tg=42)&(n=3)-> 1.000000:(tg'=57)&(n'=3) ;
[] (tg=43)&(n=6)-> 1.000000:(tg'=58)&(n'=6) ;
[] (tg=41)&(n=6)-> 1.000000:(tg'=56)&(n'=6) ;
[] (tg=41)&(n=7)-> 1.000000:(tg'=46)&(n'=14) ;
[] (tg=41)&(n=7)-> 1.000000:(tg'=56)&(n'=7) ;
[] (tg=43)&(n=7)-> 1.000000:(tg'=46)&(n'=15) ;
[] (tg=43)&(n=7)-> 1.000000:(tg'=58)&(n'=7) ;
[] (tg=40)&(n=4)-> 1.000000:(tg'=46)&(n'=16) ;
[] (tg=40)&(n=4)-> 1.000000:(tg'=55)&(n'=4) ;
[] (tg=42)&(n=4)-> 1.000000:(tg'=46)&(n'=17) ;
[] (tg=42)&(n=4)-> 1.000000:(tg'=57)&(n'=4) ;
[] (tg=41)&(n=8)-> 1.000000:(tg'=56)&(n'=8) ;
[] (tg=43)&(n=8)-> 1.000000:(tg'=58)&(n'=8) ;
[] (tg=41)&(n=9)-> 1.000000:(tg'=46)&(n'=18) ;
[] (tg=41)&(n=9)-> 1.000000:(tg'=56)&(n'=9) ;
[] (tg=43)&(n=9)-> 1.000000:(tg'=46)&(n'=19) ;
[] (tg=43)&(n=9)-> 1.000000:(tg'=58)&(n'=9) ;
[] (tg=40)&(n=5)-> 1.000000:(tg'=46)&(n'=20) ;
[] (tg=40)&(n=5)-> 1.000000:(tg'=55)&(n'=5) ;
[] (tg=42)&(n=5)-> 1.000000:(tg'=46)&(n'=21) ;
[] (tg=42)&(n=5)-> 1.000000:(tg'=57)&(n'=5) ;
[] (tg=41)&(n=10)-> 1.000000:(tg'=56)&(n'=10) ;
[] (tg=43)&(n=10)-> 1.000000:(tg'=58)&(n'=10) ;
[] (tg=41)&(n=11)-> 1.000000:(tg'=46)&(n'=22) ;
[] (tg=41)&(n=11)-> 1.000000:(tg'=56)&(n'=11) ;
[] (tg=43)&(n=11)-> 1.000000:(tg'=46)&(n'=23) ;
[] (tg=43)&(n=11)-> 1.000000:(tg'=58)&(n'=11) ;
[] (tg=40)&(n=6)-> 1.000000:(tg'=46)&(n'=24) ;
[] (tg=40)&(n=6)-> 1.000000:(tg'=55)&(n'=6) ;
[] (tg=42)&(n=6)-> 1.000000:(tg'=46)&(n'=25) ;
[] (tg=42)&(n=6)-> 1.000000:(tg'=57)&(n'=6) ;
[] (tg=43)&(n=12)-> 1.000000:(tg'=58)&(n'=12) ;
[] (tg=41)&(n=12)-> 1.000000:(tg'=56)&(n'=12) ;
[] (tg=41)&(n=13)-> 1.000000:(tg'=46)&(n'=26) ;
[] (tg=41)&(n=13)-> 1.000000:(tg'=56)&(n'=13) ;
[] (tg=43)&(n=13)-> 1.000000:(tg'=46)&(n'=27) ;
[] (tg=43)&(n=13)-> 1.000000:(tg'=58)&(n'=13) ;
[] (tg=46)&(n=4)-> 1.000000:(tg'=49)&(n'=4) ;
[] (tg=46)&(n=4)-> 1.000000:(tg'=50)&(n'=4) ;
[] (tg=55)&(n=1)-> 1.000000:(tg'=59)&(n'=3) ;
[] (tg=57)&(n=1)-> 1.000000:(tg'=60)&(n'=3) ;
[] (tg=56)&(n=2)-> 1.000000:(tg'=59)&(n'=4) ;
[] (tg=58)&(n=2)-> 1.000000:(tg'=60)&(n'=4) ;
[] (tg=46)&(n=6)-> 1.000000:(tg'=49)&(n'=6) ;
[] (tg=46)&(n=6)-> 1.000000:(tg'=50)&(n'=6) ;
[] (tg=56)&(n=3)-> 1.000000:(tg'=59)&(n'=5) ;
[] (tg=58)&(n=3)-> 1.000000:(tg'=60)&(n'=5) ;
[] (tg=55)&(n=2)-> 1.000000:(tg'=59)&(n'=6) ;
[] (tg=46)&(n=5)| (tg=46)&(n=9)-> 1.000000:(tg'=49)&(n'=5) ;
[] (tg=46)&(n=5)| (tg=46)&(n=9)-> 1.000000:(tg'=50)&(n'=5) ;
[] (tg=57)&(n=2)-> 1.000000:(tg'=60)&(n'=6) ;
[] (tg=56)&(n=4)-> 1.000000:(tg'=59)&(n'=7) ;
[] (tg=58)&(n=4)-> 1.000000:(tg'=60)&(n'=7) ;
[] (tg=56)&(n=5)-> 1.000000:(tg'=59)&(n'=8) ;
[] (tg=46)&(n=7)| (tg=46)&(n=11)-> 1.000000:(tg'=49)&(n'=7) ;
[] (tg=46)&(n=7)| (tg=46)&(n=11)-> 1.000000:(tg'=50)&(n'=7) ;
[] (tg=58)&(n=5)-> 1.000000:(tg'=60)&(n'=8) ;
[] (tg=46)&(n=8)| (tg=46)&(n=12)-> 1.000000:(tg'=49)&(n'=8) ;
[] (tg=46)&(n=8)| (tg=46)&(n=12)-> 1.000000:(tg'=50)&(n'=8) ;
[] (tg=55)&(n=3)-> 1.000000:(tg'=59)&(n'=9) ;
[] (tg=46)&(n=13)-> 1.000000:(tg'=49)&(n'=10) ;
[] (tg=46)&(n=13)-> 1.000000:(tg'=50)&(n'=10) ;
[] (tg=57)&(n=3)-> 1.000000:(tg'=60)&(n'=9) ;
[] (tg=58)&(n=6)-> 1.000000:(tg'=60)&(n'=10) ;
[] (tg=56)&(n=6)-> 1.000000:(tg'=59)&(n'=10) ;
[] (tg=46)&(n=10)| (tg=46)&(n=14)-> 1.000000:(tg'=49)&(n'=9) ;
[] (tg=46)&(n=10)| (tg=46)&(n=14)-> 1.000000:(tg'=50)&(n'=9) ;
[] (tg=56)&(n=7)-> 1.000000:(tg'=59)&(n'=11) ;
[] (tg=46)&(n=15)-> 1.000000:(tg'=49)&(n'=11) ;
[] (tg=46)&(n=15)-> 1.000000:(tg'=50)&(n'=11) ;
[] (tg=58)&(n=7)-> 1.000000:(tg'=60)&(n'=11) ;
[] (tg=46)&(n=16)-> 1.000000:(tg'=49)&(n'=12) ;
[] (tg=46)&(n=16)-> 1.000000:(tg'=50)&(n'=12) ;
[] (tg=55)&(n=4)-> 1.000000:(tg'=59)&(n'=12) ;
[] (tg=57)&(n=4)-> 1.000000:(tg'=60)&(n'=12) ;
[] (tg=56)&(n=8)-> 1.000000:(tg'=59)&(n'=13) ;
[] (tg=58)&(n=8)-> 1.000000:(tg'=60)&(n'=13) ;
[] (tg=46)&(n=18)-> 1.000000:(tg'=49)&(n'=14) ;
[] (tg=46)&(n=18)-> 1.000000:(tg'=50)&(n'=14) ;
[] (tg=56)&(n=9)-> 1.000000:(tg'=59)&(n'=14) ;
[] (tg=58)&(n=9)-> 1.000000:(tg'=60)&(n'=14) ;
[] (tg=55)&(n=5)-> 1.000000:(tg'=59)&(n'=15) ;
[] (tg=46)&(n=17)| (tg=46)&(n=21)-> 1.000000:(tg'=49)&(n'=13) ;
[] (tg=46)&(n=17)| (tg=46)&(n=21)-> 1.000000:(tg'=50)&(n'=13) ;
[] (tg=57)&(n=5)-> 1.000000:(tg'=60)&(n'=15) ;
[] (tg=56)&(n=10)-> 1.000000:(tg'=59)&(n'=16) ;
[] (tg=58)&(n=10)-> 1.000000:(tg'=60)&(n'=16) ;
[] (tg=56)&(n=11)-> 1.000000:(tg'=59)&(n'=17) ;
[] (tg=46)&(n=19)| (tg=46)&(n=23)-> 1.000000:(tg'=49)&(n'=15) ;
[] (tg=46)&(n=19)| (tg=46)&(n=23)-> 1.000000:(tg'=50)&(n'=15) ;
[] (tg=58)&(n=11)-> 1.000000:(tg'=60)&(n'=17) ;
[] (tg=46)&(n=20)| (tg=46)&(n=24)-> 1.000000:(tg'=49)&(n'=16) ;
[] (tg=46)&(n=20)| (tg=46)&(n=24)-> 1.000000:(tg'=50)&(n'=16) ;
[] (tg=55)&(n=6)-> 1.000000:(tg'=59)&(n'=18) ;
[] (tg=46)&(n=25)-> 1.000000:(tg'=49)&(n'=18) ;
[] (tg=46)&(n=25)-> 1.000000:(tg'=50)&(n'=18) ;
[] (tg=57)&(n=6)-> 1.000000:(tg'=60)&(n'=18) ;
[] (tg=58)&(n=12)-> 1.000000:(tg'=60)&(n'=19) ;
[] (tg=56)&(n=12)-> 1.000000:(tg'=59)&(n'=19) ;
[] (tg=46)&(n=22)| (tg=46)&(n=26)-> 1.000000:(tg'=49)&(n'=17) ;
[] (tg=46)&(n=22)| (tg=46)&(n=26)-> 1.000000:(tg'=50)&(n'=17) ;
[] (tg=56)&(n=13)-> 1.000000:(tg'=59)&(n'=20) ;
[] (tg<