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

nondeterministic

module abs10000 

tg : [0..11] init 0; 
n : [0..55] 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=2)&(n=0)-> 0.500000:(tg'=7)&(n'=0) + 0.500000:(tg'=8)&(n'=0) ;
[] (tg=3)&(n=0)-> 0.500000:(tg'=5)&(n'=0) + 0.500000:(tg'=7)&(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'=0)&(n'=1) ;
[] (tg=5)&(n=0)-> 1.000000:(tg'=9)&(n'=0) ;
[] (tg=8)&(n=0)-> 1.000000:(tg'=0)&(n'=2) ;
[] (tg=6)&(n=0)| (tg=7)&(n=0)| (tg=8)&(n=0)-> 1.000000:(tg'=9)&(n'=1) ;
[] (tg=0)&(n=1)-> 0.500000:(tg'=1)&(n'=1) + 0.500000:(tg'=2)&(n'=1) ;
[] (tg=0)&(n=1)-> 0.500000:(tg'=3)&(n'=1) + 0.500000:(tg'=4)&(n'=1) ;
[] (tg=0)&(n=2)-> 0.500000:(tg'=1)&(n'=2) + 0.500000:(tg'=2)&(n'=2) ;
[] (tg=0)&(n=2)-> 0.500000:(tg'=3)&(n'=2) + 0.500000:(tg'=4)&(n'=2) ;
[] (tg=1)&(n=1)-> 0.500000:(tg'=5)&(n'=1) + 0.500000:(tg'=6)&(n'=1) ;
[] (tg=2)&(n=1)-> 0.500000:(tg'=7)&(n'=1) + 0.500000:(tg'=8)&(n'=1) ;
[] (tg=3)&(n=1)-> 0.500000:(tg'=5)&(n'=1) + 0.500000:(tg'=7)&(n'=1) ;
[] (tg=4)&(n=1)-> 0.500000:(tg'=6)&(n'=1) + 0.500000:(tg'=8)&(n'=1) ;
[] (tg=1)&(n=2)-> 0.500000:(tg'=5)&(n'=2) + 0.500000:(tg'=6)&(n'=2) ;
[] (tg=2)&(n=2)-> 0.500000:(tg'=7)&(n'=2) + 0.500000:(tg'=8)&(n'=2) ;
[] (tg=3)&(n=2)-> 0.500000:(tg'=5)&(n'=2) + 0.500000:(tg'=7)&(n'=2) ;
[] (tg=4)&(n=2)-> 0.500000:(tg'=6)&(n'=2) + 0.500000:(tg'=8)&(n'=2) ;
[] (tg=5)&(n=1)-> 1.000000:(tg'=0)&(n'=3) ;
[] (tg=5)&(n=1)-> 1.000000:(tg'=9)&(n'=2) ;
[] (tg=8)&(n=1)| (tg=5)&(n=2)-> 1.000000:(tg'=0)&(n'=4) ;
[] (tg=6)&(n=1)| (tg=7)&(n=1)| (tg=8)&(n=1)| (tg=5)&(n=2)-> 1.000000:(tg'=9)&(n'=3) ;
[] (tg=8)&(n=2)-> 1.000000:(tg'=0)&(n'=5) ;
[] (tg=6)&(n=2)| (tg=7)&(n=2)| (tg=8)&(n=2)-> 1.000000:(tg'=9)&(n'=4) ;
[] (tg=0)&(n=3)-> 0.500000:(tg'=1)&(n'=3) + 0.500000:(tg'=2)&(n'=3) ;
[] (tg=0)&(n=3)-> 0.500000:(tg'=3)&(n'=3) + 0.500000:(tg'=4)&(n'=3) ;
[] (tg=0)&(n=4)-> 0.500000:(tg'=1)&(n'=4) + 0.500000:(tg'=2)&(n'=4) ;
[] (tg=0)&(n=4)-> 0.500000:(tg'=3)&(n'=4) + 0.500000:(tg'=4)&(n'=4) ;
[] (tg=0)&(n=5)-> 0.500000:(tg'=1)&(n'=5) + 0.500000:(tg'=2)&(n'=5) ;
[] (tg=0)&(n=5)-> 0.500000:(tg'=3)&(n'=5) + 0.500000:(tg'=4)&(n'=5) ;
[] (tg=1)&(n=3)-> 0.500000:(tg'=5)&(n'=3) + 0.500000:(tg'=6)&(n'=3) ;
[] (tg=2)&(n=3)-> 0.500000:(tg'=7)&(n'=3) + 0.500000:(tg'=8)&(n'=3) ;
[] (tg=3)&(n=3)-> 0.500000:(tg'=5)&(n'=3) + 0.500000:(tg'=7)&(n'=3) ;
[] (tg=4)&(n=3)-> 0.500000:(tg'=6)&(n'=3) + 0.500000:(tg'=8)&(n'=3) ;
[] (tg=1)&(n=4)-> 0.500000:(tg'=5)&(n'=4) + 0.500000:(tg'=6)&(n'=4) ;
[] (tg=2)&(n=4)-> 0.500000:(tg'=7)&(n'=4) + 0.500000:(tg'=8)&(n'=4) ;
[] (tg=3)&(n=4)-> 0.500000:(tg'=5)&(n'=4) + 0.500000:(tg'=7)&(n'=4) ;
[] (tg=4)&(n=4)-> 0.500000:(tg'=6)&(n'=4) + 0.500000:(tg'=8)&(n'=4) ;
[] (tg=1)&(n=5)-> 0.500000:(tg'=5)&(n'=5) + 0.500000:(tg'=6)&(n'=5) ;
[] (tg=2)&(n=5)-> 0.500000:(tg'=7)&(n'=5) + 0.500000:(tg'=8)&(n'=5) ;
[] (tg=3)&(n=5)-> 0.500000:(tg'=5)&(n'=5) + 0.500000:(tg'=7)&(n'=5) ;
[] (tg=4)&(n=5)-> 0.500000:(tg'=6)&(n'=5) + 0.500000:(tg'=8)&(n'=5) ;
[] (tg=5)&(n=3)-> 1.000000:(tg'=0)&(n'=6) ;
[] (tg=5)&(n=3)-> 1.000000:(tg'=9)&(n'=5) ;
[] (tg=8)&(n=3)| (tg=5)&(n=4)-> 1.000000:(tg'=0)&(n'=7) ;
[] (tg=6)&(n=3)| (tg=7)&(n=3)| (tg=8)&(n=3)| (tg=5)&(n=4)-> 1.000000:(tg'=9)&(n'=6) ;
[] (tg=8)&(n=4)| (tg=5)&(n=5)-> 1.000000:(tg'=0)&(n'=8) ;
[] (tg=6)&(n=4)| (tg=7)&(n=4)| (tg=8)&(n=4)| (tg=5)&(n=5)-> 1.000000:(tg'=9)&(n'=7) ;
[] (tg=8)&(n=5)-> 1.000000:(tg'=0)&(n'=9) ;
[] (tg=6)&(n=5)| (tg=7)&(n=5)| (tg=8)&(n=5)-> 1.000000:(tg'=9)&(n'=8) ;
[] (tg=0)&(n=6)-> 0.500000:(tg'=1)&(n'=6) + 0.500000:(tg'=2)&(n'=6) ;
[] (tg=0)&(n=6)-> 0.500000:(tg'=3)&(n'=6) + 0.500000:(tg'=4)&(n'=6) ;
[] (tg=0)&(n=7)-> 0.500000:(tg'=1)&(n'=7) + 0.500000:(tg'=2)&(n'=7) ;
[] (tg=0)&(n=7)-> 0.500000:(tg'=3)&(n'=7) + 0.500000:(tg'=4)&(n'=7) ;
[] (tg=0)&(n=8)-> 0.500000:(tg'=1)&(n'=8) + 0.500000:(tg'=2)&(n'=8) ;
[] (tg=0)&(n=8)-> 0.500000:(tg'=3)&(n'=8) + 0.500000:(tg'=4)&(n'=8) ;
[] (tg=0)&(n=9)-> 0.500000:(tg'=1)&(n'=9) + 0.500000:(tg'=2)&(n'=9) ;
[] (tg=0)&(n=9)-> 0.500000:(tg'=3)&(n'=9) + 0.500000:(tg'=4)&(n'=9) ;
[] (tg=1)&(n=6)-> 0.500000:(tg'=5)&(n'=6) + 0.500000:(tg'=6)&(n'=6) ;
[] (tg=2)&(n=6)-> 0.500000:(tg'=7)&(n'=6) + 0.500000:(tg'=8)&(n'=6) ;
[] (tg=3)&(n=6)-> 0.500000:(tg'=5)&(n'=6) + 0.500000:(tg'=7)&(n'=6) ;
[] (tg=4)&(n=6)-> 0.500000:(tg'=6)&(n'=6) + 0.500000:(tg'=8)&(n'=6) ;
[] (tg=1)&(n=7)-> 0.500000:(tg'=5)&(n'=7) + 0.500000:(tg'=6)&(n'=7) ;
[] (tg=2)&(n=7)-> 0.500000:(tg'=7)&(n'=7) + 0.500000:(tg'=8)&(n'=7) ;
[] (tg=3)&(n=7)-> 0.500000:(tg'=5)&(n'=7) + 0.500000:(tg'=7)&(n'=7) ;
[] (tg=4)&(n=7)-> 0.500000:(tg'=6)&(n'=7) + 0.500000:(tg'=8)&(n'=7) ;
[] (tg=1)&(n=8)-> 0.500000:(tg'=5)&(n'=8) + 0.500000:(tg'=6)&(n'=8) ;
[] (tg=2)&(n=8)-> 0.500000:(tg'=7)&(n'=8) + 0.500000:(tg'=8)&(n'=8) ;
[] (tg=3)&(n=8)-> 0.500000:(tg'=5)&(n'=8) + 0.500000:(tg'=7)&(n'=8) ;
[] (tg=4)&(n=8)-> 0.500000:(tg'=6)&(n'=8) + 0.500000:(tg'=8)&(n'=8) ;
[] (tg=1)&(n=9)-> 0.500000:(tg'=5)&(n'=9) + 0.500000:(tg'=6)&(n'=9) ;
[] (tg=2)&(n=9)-> 0.500000:(tg'=7)&(n'=9) + 0.500000:(tg'=8)&(n'=9) ;
[] (tg=3)&(n=9)-> 0.500000:(tg'=5)&(n'=9) + 0.500000:(tg'=7)&(n'=9) ;
[] (tg=4)&(n=9)-> 0.500000:(tg'=6)&(n'=9) + 0.500000:(tg'=8)&(n'=9) ;
[] (tg=5)&(n=6)-> 1.000000:(tg'=0)&(n'=10) ;
[] (tg=5)&(n=6)-> 1.000000:(tg'=9)&(n'=9) ;
[] (tg=8)&(n=6)| (tg=5)&(n=7)-> 1.000000:(tg'=0)&(n'=11) ;
[] (tg=6)&(n=6)| (tg=7)&(n=6)| (tg=8)&(n=6)| (tg=5)&(n=7)-> 1.000000:(tg'=9)&(n'=10) ;
[] (tg=8)&(n=7)| (tg=5)&(n=8)-> 1.000000:(tg'=0)&(n'=12) ;
[] (tg=6)&(n=7)| (tg=7)&(n=7)| (tg=8)&(n=7)| (tg=5)&(n=8)-> 1.000000:(tg'=9)&(n'=11) ;
[] (tg=8)&(n=8)| (tg=5)&(n=9)-> 1.000000:(tg'=0)&(n'=13) ;
[] (tg=6)&(n=8)| (tg=7)&(n=8)| (tg=8)&(n=8)| (tg=5)&(n=9)-> 1.000000:(tg'=9)&(n'=12) ;
[] (tg=8)&(n=9)-> 1.000000:(tg'=0)&(n'=14) ;
[] (tg=6)&(n=9)| (tg=7)&(n=9)| (tg=8)&(n=9)-> 1.000000:(tg'=9)&(n'=13) ;
[] (tg=0)&(n=10)-> 0.500000:(tg'=1)&(n'=10) + 0.500000:(tg'=2)&(n'=10) ;
[] (tg=0)&(n=10)-> 0.500000:(tg'=3)&(n'=10) + 0.500000:(tg'=4)&(n'=10) ;
[] (tg=0)&(n=11)-> 0.500000:(tg'=1)&(n'=11) + 0.500000:(tg'=2)&(n'=11) ;
[] (tg=0)&(n=11)-> 0.500000:(tg'=3)&(n'=11) + 0.500000:(tg'=4)&(n'=11) ;
[] (tg=0)&(n=12)-> 0.500000:(tg'=1)&(n'=12) + 0.500000:(tg'=2)&(n'=12) ;
[] (tg=0)&(n=12)-> 0.500000:(tg'=3)&(n'=12) + 0.500000:(tg'=4)&(n'=12) ;
[] (tg=0)&(n=13)-> 0.500000:(tg'=1)&(n'=13) + 0.500000:(tg'=2)&(n'=13) ;
[] (tg=0)&(n=13)-> 0.500000:(tg'=3)&(n'=13) + 0.500000:(tg'=4)&(n'=13) ;
[] (tg=0)&(n=14)-> 0.500000:(tg'=1)&(n'=14) + 0.500000:(tg'=2)&(n'=14) ;
[] (tg=0)&(n=14)-> 0.500000:(tg'=3)&(n'=14) + 0.500000:(tg'=4)&(n'=14) ;
[] (tg=1)&(n=10)-> 0.500000:(tg'=5)&(n'=10) + 0.500000:(tg'=6)&(n'=10) ;
[] (tg=2)&(n=10)-> 0.500000:(tg'=7)&(n'=10) + 0.500000:(tg'=8)&(n'=10) ;
[] (tg=3)&(n=10)-> 0.500000:(tg'=5)&(n'=10) + 0.500000:(tg'=7)&(n'=10) ;
[] (tg=4)&(n=10)-> 0.500000:(tg'=6)&(n'=10) + 0.500000:(tg'=8)&(n'=10) ;
[] (tg=1)&(n=11)-> 0.500000:(tg'=5)&(n'=11) + 0.500000:(tg'=6)&(n'=11) ;
[] (tg=2)&(n=11)-> 0.500000:(tg'=7)&(n'=11) + 0.500000:(tg'=8)&(n'=11) ;
[] (tg=3)&(n=11)-> 0.500000:(tg'=5)&(n'=11) + 0.500000:(tg'=7)&(n'=11) ;
[] (tg=4)&(n=11)-> 0.500000:(tg'=6)&(n'=11) + 0.500000:(tg'=8)&(n'=11) ;
[] (tg=1)&(n=12)-> 0.500000:(tg'=5)&(n'=12) + 0.500000:(tg'=6)&(n'=12) ;
[] (tg=2)&(n=12)-> 0.500000:(tg'=7)&(n'=12) + 0.500000:(tg'=8)&(n'=12) ;
[] (tg=3)&(n=12)-> 0.500000:(tg'=5)&(n'=12) + 0.500000:(tg'=7)&(n'=12) ;
[] (tg=4)&(n=12)-> 0.500000:(tg'=6)&(n'=12) + 0.500000:(tg'=8)&(n'=12) ;
[] (tg=1)&(n=13)-> 0.500000:(tg'=5)&(n'=13) + 0.500000:(tg'=6)&(n'=13) ;
[] (tg=2)&(n=13)-> 0.500000:(tg'=7)&(n'=13) + 0.500000:(tg'=8)&(n'=13) ;
[] (tg=3)&(n=13)-> 0.500000:(tg'=5)&(n'=13) + 0.500000:(tg'=7)&(n'=13) ;
[] (tg=4)&(n=13)-> 0.500000:(tg'=6)&(n'=13) + 0.500000:(tg'=8)&(n'=13) ;
[] (tg=1)&(n=14)-> 0.500000:(tg'=5)&(n'=14) + 0.500000:(tg'=6)&(n'=14) ;
[] (tg=2)&(n=14)-> 0.500000:(tg'=7)&(n'=14) + 0.500000:(tg'=8)&(n'=14) ;
[] (tg=3)&(n=14)-> 0.500000:(tg'=5)&(n'=14) + 0.500000:(tg'=7)&(n'=14) ;
[] (tg=4)&(n=14)-> 0.500000:(tg'=6)&(n'=14) + 0.500000:(tg'=8)&(n'=14) ;
[] (tg=5)&(n=10)-> 1.000000:(tg'=0)&(n'=15) ;
[] (tg=5)&(n=10)-> 1.000000:(tg'=9)&(n'=14) ;
[] (tg=8)&(n=10)| (tg=5)&(n=11)-> 1.000000:(tg'=0)&(n'=16) ;
[] (tg=6)&(n=10)| (tg=7)&(n=10)| (tg=8)&(n=10)| (tg=5)&(n=11)-> 1.000000:(tg'=9)&(n'=15) ;
[] (tg=8)&(n=11)| (tg=5)&(n=12)-> 1.000000:(tg'=0)&(n'=17) ;
[] (tg=6)&(n=11)| (tg=7)&(n=11)| (tg=8)&(n=11)| (tg=5)&(n=12)-> 1.000000:(tg'=9)&(n'=16) ;
[] (tg=8)&(n=12)| (tg=5)&(n=13)-> 1.000000:(tg'=0)&(n'=18) ;
[] (tg=6)&(n=12)| (tg=7)&(n=12)| (tg=8)&(n=12)| (tg=5)&(n=13)-> 1.000000:(tg'=9)&(n'=17) ;
[] (tg=8)&(n=13)| (tg=5)&(n=14)-> 1.000000:(tg'=0)&(n'=19) ;
[] (tg=6)&(n=13)| (tg=7)&(n=13)| (tg=8)&(n=13)| (tg=5)&(n=14)-> 1.000000:(tg'=9)&(n'=18) ;
[] (tg=8)&(n=14)-> 1.000000:(tg'=0)&(n'=20) ;
[] (tg=6)&(n=14)| (tg=7)&(n=14)| (tg=8)&(n=14)-> 1.000000:(tg'=9)&(n'=19) ;
[] (tg=0)&(n=15)-> 0.500000:(tg'=1)&(n'=15) + 0.500000:(tg'=2)&(n'=15) ;
[] (tg=0)&(n=15)-> 0.500000:(tg'=3)&(n'=15) + 0.500000:(tg'=4)&(n'=15) ;
[] (tg=0)&(n=16)-> 0.500000:(tg'=1)&(n'=16) + 0.500000:(tg'=2)&(n'=16) ;
[] (tg=0)&(n=16)-> 0.500000:(tg'=3)&(n'=16) + 0.500000:(tg'=4)&(n'=16) ;
[] (tg=0)&(n=17)-> 0.500000:(tg'=1)&(n'=17) + 0.500000:(tg'=2)&(n'=17) ;
[] (tg=0)&(n=17)-> 0.500000:(tg'=3)&(n'=17) + 0.500000:(tg'=4)&(n'=17) ;
[] (tg=0)&(n=18)-> 0.500000:(tg'=1)&(n'=18) + 0.500000:(tg'=2)&(n'=18) ;
[] (tg=0)&(n=18)-> 0.500000:(tg'=3)&(n'=18) + 0.500000:(tg'=4)&(n'=18) ;
[] (tg=0)&(n=19)-> 0.500000:(tg'=1)&(n'=19) + 0.500000:(tg'=2)&(n'=19) ;
[] (tg=0)&(n=19)-> 0.500000:(tg'=3)&(n'=19) + 0.500000:(tg'=4)&(n'=19) ;
[] (tg=0)&(n=20)-> 0.500000:(tg'=1)&(n'=20) + 0.500000:(tg'=2)&(n'=20) ;
[] (tg=0)&(n=20)-> 0.500000:(tg'=3)&(n'=20) + 0.500000:(tg'=4)&(n'=20) ;
[] (tg=1)&(n=15)-> 0.500000:(tg'=5)&(n'=15) + 0.500000:(tg'=6)&(n'=15) ;
[] (tg=2)&(n=15)-> 0.500000:(tg'=7)&(n'=15) + 0.500000:(tg'=8)&(n'=15) ;
[] (tg=3)&(n=15)-> 0.500000:(tg'=5)&(n'=15) + 0.500000:(tg'=7)&(n'=15) ;
[] (tg=4)&(n=15)-> 0.500000:(tg'=6)&(n'=15) + 0.500000:(tg'=8)&(n'=15) ;
[] (tg=1)&(n=16)-> 0.500000:(tg'=5)&(n'=16) + 0.500000:(tg'=6)&(n'=16) ;
[] (tg=2)&(n=16)-> 0.500000:(tg'=7)&(n'=16) + 0.500000:(tg'=8)&(n'=16) ;
[] (tg=3)&(n=16)-> 0.500000:(tg'=5)&(n'=16) + 0.500000:(tg'=7)&(n'=16) ;
[] (tg=4)&(n=16)-> 0.500000:(tg'=6)&(n'=16) + 0.500000:(tg'=8)&(n'=16) ;
[] (tg=1)&(n=17)-> 0.500000:(tg'=5)&(n'=17) + 0.500000:(tg'=6)&(n'=17) ;
[] (tg=2)&(n=17)-> 0.500000:(tg'=7)&(n'=17) + 0.500000:(tg'=8)&(n'=17) ;
[] (tg=3)&(n=17)-> 0.500000:(tg'=5)&(n'=17) + 0.500000:(tg'=7)&(n'=17) ;
[] (tg=4)&(n=17)-> 0.500000:(tg'=6)&(n'=17) + 0.500000:(tg'=8)&(n'=17) ;
[] (tg=1)&(n=18)-> 0.500000:(tg'=5)&(n'=18) + 0.500000:(tg'=6)&(n'=18) ;
[] (tg=2)&(n=18)-> 0.500000:(tg'=7)&(n'=18) + 0.500000:(tg'=8)&(n'=18) ;
[] (tg=3)&(n=18)-> 0.500000:(tg'=5)&(n'=18) + 0.500000:(tg'=7)&(n'=18) ;
[] (tg=4)&(n=18)-> 0.500000:(tg'=6)&(n'=18) + 0.500000:(tg'=8)&(n'=18) ;
[] (tg=1)&(n=19)-> 0.500000:(tg'=5)&(n'=19) + 0.500000:(tg'=6)&(n'=19) ;
[] (tg=2)&(n=19)-> 0.500000:(tg'=7)&(n'=19) + 0.500000:(tg'=8)&(n'=19) ;
[] (tg=3)&(n=19)-> 0.500000:(tg'=5)&(n'=19) + 0.500000:(tg'=7)&(n'=19) ;
[] (tg=4)&(n=19)-> 0.500000:(tg'=6)&(n'=19) + 0.500000:(tg'=8)&(n'=19) ;
[] (tg=1)&(n=20)-> 0.500000:(tg'=5)&(n'=20) + 0.500000:(tg'=6)&(n'=20) ;
[] (tg=2)&(n=20)-> 0.500000:(tg'=7)&(n'=20) + 0.500000:(tg'=8)&(n'=20) ;
[] (tg=3)&(n=20)-> 0.500000:(tg'=5)&(n'=20) + 0.500000:(tg'=7)&(n'=20) ;
[] (tg=4)&(n=20)-> 0.500000:(tg'=6)&(n'=20) + 0.500000:(tg'=8)&(n'=20) ;
[] (tg=5)&(n=15)-> 1.000000:(tg'=0)&(n'=21) ;
[] (tg=5)&(n=15)-> 1.000000:(tg'=9)&(n'=20) ;
[] (tg=8)&(n=15)| (tg=5)&(n=16)-> 1.000000:(tg'=0)&(n'=22) ;
[] (tg=6)&(n=15)| (tg=7)&(n=15)| (tg=8)&(n=15)| (tg=5)&(n=16)-> 1.000000:(tg'=9)&(n'=21) ;
[] (tg=8)&(n=16)| (tg=5)&(n=17)-> 1.000000:(tg'=0)&(n'=23) ;
[] (tg=6)&(n=16)| (tg=7)&(n=16)| (tg=8)&(n=16)| (tg=5)&(n=17)-> 1.000000:(tg'=9)&(n'=22) ;
[] (tg=8)&(n=17)| (tg=5)&(n=18)-> 1.000000:(tg'=0)&(n'=24) ;
[] (tg=6)&(n=17)| (tg=7)&(n=17)| (tg=8)&(n=17)| (tg=5)&(n=18)-> 1.000000:(tg'=9)&(n'=23) ;
[] (tg=8)&(n=18)| (tg=5)&(n=19)-> 1.000000:(tg'=0)&(n'=25) ;
[] (tg=6)&(n=18)| (tg=7)&(n=18)| (tg=8)&(n=18)| (tg=5)&(n=19)-> 1.000000:(tg'=9)&(n'=24) ;
[] (tg=8)&(n=19)| (tg=5)&(n=20)-> 1.000000:(tg'=0)&(n'=26) ;
[] (tg=6)&(n=19)| (tg=7)&(n=19)| (tg=8)&(n=19)| (tg=5)&(n=20)-> 1.000000:(tg'=9)&(n'=25) ;
[] (tg=8)&(n=20)-> 1.000000:(tg'=0)&(n'=27) ;
[] (tg=6)&(n=20)| (tg=7)&(n=20)| (tg=8)&(n=20)-> 1.000000:(tg'=9)&(n'=26) ;
[] (tg=0)&(n=21)-> 0.500000:(tg'=1)&(n'=21) + 0.500000:(tg'=2)&(n'=21) ;
[] (tg=0)&(n=21)-> 0.500000:(tg'=3)&(n'=21) + 0.500000:(tg'=4)&(n'=21) ;
[] (tg=0)&(n=22)-> 0.500000:(tg'=1)&(n'=22) + 0.500000:(tg'=2)&(n'=22) ;
[] (tg=0)&(n=22)-> 0.500000:(tg'=3)&(n'=22) + 0.500000:(tg'=4)&(n'=22) ;
[] (tg=0)&(n=23)-> 0.500000:(tg'=1)&(n'=23) + 0.500000:(tg'=2)&(n'=23) ;
[] (tg=0)&(n=23)-> 0.500000:(tg'=3)&(n'=23) + 0.500000:(tg'=4)&(n'=23) ;
[] (tg=0)&(n=24)-> 0.500000:(tg'=1)&(n'=24) + 0.500000:(tg'=2)&(n'=24) ;
[] (tg=0)&(n=24)-> 0.500000:(tg'=3)&(n'=24) + 0.500000:(tg'=4)&(n'=24) ;
[] (tg=0)&(n=25)-> 0.500000:(tg'=1)&(n'=25) + 0.500000:(tg'=2)&(n'=25) ;
[] (tg=0)&(n=25)-> 0.500000:(tg'=3)&(n'=25) + 0.500000:(tg'=4)&(n'=25) ;
[] (tg=0)&(n=26)-> 0.500000:(tg'=1)&(n'=26) + 0.500000:(tg'=2)&(n'=26) ;
[] (tg=0)&(n=26)-> 0.500000:(tg'=3)&(n'=26) + 0.500000:(tg'=4)&(n'=26) ;
[] (tg=0)&(n=27)-> 0.500000:(tg'=1)&(n'=27) + 0.500000:(tg'=2)&(n'=27) ;
[] (tg=0)&(n=27)-> 0.500000:(tg'=3)&(n'=27) + 0.500000:(tg'=4)&(n'=27) ;
[] (tg=1)&(n=21)-> 0.500000:(tg'=5)&(n'=21) + 0.500000:(tg'=6)&(n'=21) ;
[] (tg=2)&(n=21)-> 0.500000:(tg'=7)&(n'=21) + 0.500000:(tg'=8)&(n'=21) ;
[] (tg=3)&(n=21)-> 0.500000:(tg'=5)&(n'=21) + 0.500000:(tg'=7)&(n'=21) ;
[] (tg=4)&(n=21)-> 0.500000:(tg'=6)&(n'=21) + 0.500000:(tg'=8)&(n'=21) ;
[] (tg=1)&(n=22)-> 0.500000:(tg'=5)&(n'=22) + 0.500000:(tg'=6)&(n'=22) ;
[] (tg=2)&(n=22)-> 0.500000:(tg'=7)&(n'=22) + 0.500000:(tg'=8)&(n'=22) ;
[] (tg=3)&(n=22)-> 0.500000:(tg'=5)&(n'=22) + 0.500000:(tg'=7)&(n'=22) ;
[] (tg=4)&(n=22)-> 0.500000:(tg'=6)&(n'=22) + 0.500000:(tg'=8)&(n'=22) ;
[] (tg=1)&(n=23)-> 0.500000:(tg'=5)&(n'=23) + 0.500000:(tg'=6)&(n'=23) ;
[] (tg=2)&(n=23)-> 0.500000:(tg'=7)&(n'=23) + 0.500000:(tg'=8)&(n'=23) ;
[] (tg=3)&(n=23)-> 0.500000:(tg'=5)&(n'=23) + 0.500000:(tg'=7)&(n'=23) ;
[] (tg=4)&(n=23)-> 0.500000:(tg'=6)&(n'=23) + 0.500000:(tg'=8)&(n'=23) ;
[] (tg=1)&(n=24)-> 0.500000:(tg'=5)&(n'=24) + 0.500000:(tg'=6)&(n'=24) ;
[] (tg=2)&(n=24)-> 0.500000:(tg'=7)&(n'=24) + 0.500000:(tg'=8)&(n'=24) ;
[] (tg=3)&(n=24)-> 0.500000:(tg'=5)&(n'=24) + 0.500000:(tg'=7)&(n'=24) ;
[] (tg=4)&(n=24)-> 0.500000:(tg'=6)&(n'=24) + 0.500000:(tg'=8)&(n'=24) ;
[] (tg=1)&(n=25)-> 0.500000:(tg'=5)&(n'=25) + 0.500000:(tg'=6)&(n'=25) ;
[] (tg=2)&(n=25)-> 0.500000:(tg'=7)&(n'=25) + 0.500000:(tg'=8)&(n'=25) ;
[] (tg=3)&(n=25)-> 0.500000:(tg'=5)&(n'=25) + 0.500000:(tg'=7)&(n'=25) ;
[] (tg=4)&(n=25)-> 0.500000:(tg'=6)&(n'=25) + 0.500000:(tg'=8)&(n'=25) ;
[] (tg=1)&(n=26)-> 0.500000:(tg'=5)&(n'=26) + 0.500000:(tg'=6)&(n'=26) ;
[] (tg=2)&(n=26)-> 0.500000:(tg'=7)&(n'=26) + 0.500000:(tg'=8)&(n'=26) ;
[] (tg=3)&(n=26)-> 0.500000:(tg'=5)&(n'=26) + 0.500000:(tg'=7)&(n'=26) ;
[] (tg=4)&(n=26)-> 0.500000:(tg'=6)&(n'=26) + 0.500000:(tg'=8)&(n'=26) ;
[] (tg=1)&(n=27)-> 0.500000:(tg'=5)&(n'=27) + 0.500000:(tg'=6)&(n'=27) ;
[] (tg=2)&(n=27)-> 0.500000:(tg'=7)&(n'=27) + 0.500000:(tg'=8)&(n'=27) ;
[] (tg=3)&(n=27)-> 0.500000:(tg'=5)&(n'=27) + 0.500000:(tg'=7)&(n'=27) ;
[] (tg=4)&(n=27)-> 0.500000:(tg'=6)&(n'=27) + 0.500000:(tg'=8)&(n'=27) ;
[] (tg=5)&(n=21)-> 1.000000:(tg'=0)&(n'=28) ;
[] (tg=5)&(n=21)-> 1.000000:(tg'=9)&(n'=27) ;
[] (tg=8)&(n=21)| (tg=5)&(n=22)-> 1.000000:(tg'=0)&(n'=29) ;
[] (tg=6)&(n=21)| (tg=7)&(n=21)| (tg=8)&(n=21)| (tg=5)&(n=22)-> 1.000000:(tg'=9)&(n'=28) ;
[] (tg=8)&(n=22)| (tg=5)&(n=23)-> 1.000000:(tg'=0)&(n'=30) ;
[] (tg=6)&(n=22)| (tg=7)&(n=22)| (tg=8)&(n=22)| (tg=5)&(n=23)-> 1.000000:(tg'=9)&(n'=29) ;
[] (tg=8)&(n=23)| (tg=5)&(n=24)-> 1.000000:(tg'=0)&(n'=31) ;
[] (tg=6)&(n=23)| (tg=7)&(n=23)| (tg=8)&(n=23)| (tg=5)&(n=24)-> 1.000000:(tg'=9)&(n'=30) ;
[] (tg=8)&(n=24)| (tg=5)&(n=25)-> 1.000000:(tg'=0)&(n'=32) ;
[] (tg=6)&(n=24)| (tg=7)&(n=24)| (tg=8)&(n=24)| (tg=5)&(n=25)-> 1.000000:(tg'=9)&(n'=31) ;
[] (tg=8)&(n=25)| (tg=5)&(n=26)-> 1.000000:(tg'=0)&(n'=33) ;
[] (tg=6)&(n=25)| (tg=7)&(n=25)| (tg=8)&(n=25)| (tg=5)&(n=26)-> 1.000000:(tg'=9)&(n'=32) ;
[] (tg=6)&(n=26)| (tg=7)&(n=26)| (tg=8)&(n=26)| (tg=5)&(n=27)-> 1.000000:(tg'=9)&(n'=33) ;
[] (tg=0)&(n=28)-> 0.500000:(tg'=1)&(n'=28) + 0.500000:(tg'=2)&(n'=28) ;
[] (tg=0)&(n=28)-> 0.500000:(tg'=3)&(n'=28) + 0.500000:(tg'=4)&(n'=28) ;
[] (tg=0)&(n=29)-> 0.500000:(tg'=1)&(n'=29) + 0.500000:(tg'=2)&(n'=29) ;
[] (tg=0)&(n=29)-> 0.500000:(tg'=3)&(n'=29) + 0.500000:(tg'=4)&(n'=29) ;
[] (tg=0)&(n=30)-> 0.500000:(tg'=1)&(n'=30) + 0.500000:(tg'=2)&(n'=30) ;
[] (tg=0)&(n=30)-> 0.500000:(tg'=3)&(n'=30) + 0.500000:(tg'=4)&(n'=30) ;
[] (tg=0)&(n=31)-> 0.500000:(tg'=1)&(n'=31) + 0.500000:(tg'=2)&(n'=31) ;
[] (tg=0)&(n=31)-> 0.500000:(tg'=3)&(n'=31) + 0.500000:(tg'=4)&(n'=31) ;
[] (tg=0)&(n=32)-> 0.500000:(tg'=1)&(n'=32) + 0.500000:(tg'=2)&(n'=32) ;
[] (tg=0)&(n=32)-> 0.500000:(tg'=3)&(n'=32) + 0.500000:(tg'=4)&(n'=32) ;
[] (tg=0)&(n=33)-> 0.500000:(tg'=1)&(n'=33) + 0.500000:(tg'=2)&(n'=33) ;
[] (tg=0)&(n=33)-> 0.500000:(tg'=3)&(n'=33) + 0.500000:(tg'=4)&(n'=33) ;
[] (tg=0)&(n=34)-> 0.500000:(tg'=1)&(n'=34) + 0.500000:(tg'=2)&(n'=34) ;
[] (tg=0)&(n=34)-> 0.500000:(tg'=3)&(n'=34) + 0.500000:(tg'=4)&(n'=34) ;
[] (tg=1)&(n=28)-> 0.500000:(tg'=5)&(n'=28) + 0.500000:(tg'=6)&(n'=28) ;
[] (tg=2)&(n=28)-> 0.500000:(tg'=7)&(n'=28) + 0.500000:(tg'=8)&(n'=28) ;
[] (tg=3)&(n=28)-> 0.500000:(tg'=5)&(n'=28) + 0.500000:(tg'=7)&(n'=28) ;
[] (tg=4)&(n=28)-> 0.500000:(tg'=6)&(n'=28) + 0.500000:(tg'=8)&(n'=28) ;
[] (tg=1)&(n=29)-> 0.500000:(tg'=5)&(n'=29) + 0.500000:(tg'=6)&(n'=29) ;
[] (tg=2)&(n=29)-> 0.500000:(tg'=7)&(n'=29) + 0.500000:(tg'=8)&(n'=29) ;
[] (tg=3)&(n=29)-> 0.500000:(tg'=5)&(n'=29) + 0.500000:(tg'=7)&(n'=29) ;
[] (tg=4)&(n=29)-> 0.500000:(tg'=6)&(n'=29) + 0.500000:(tg'=8)&(n'=29) ;
[] (tg=1)&(n=30)-> 0.500000:(tg'=5)&(n'=30) + 0.500000:(tg'=6)&(n'=30) ;
[] (tg=2)&(n=30)-> 0.500000:(tg'=7)&(n'=30) + 0.500000:(tg'=8)&(n'=30) ;
[] (tg=3)&(n=30)-> 0.500000:(tg'=5)&(n'=30) + 0.500000:(tg'=7)&(n'=30) ;
[] (tg=4)&(n=30)-> 0.500000:(tg'=6)&(n'=30) + 0.500000:(tg'=8)&(n'=30) ;
[] (tg=1)&(n=31)-> 0.500000:(tg'=5)&(n'=31) + 0.500000:(tg'=6)&(n'=31) ;
[] (tg=2)&(n=31)-> 0.500000:(tg'=7)&(n'=31) + 0.500000:(tg'=8)&(n'=31) ;
[] (tg=3)&(n=31)-> 0.500000:(tg'=5)&(n'=31) + 0.500000:(tg'=7)&(n'=31) ;
[] (tg=4)&(n=31)-> 0.500000:(tg'=6)&(n'=31) + 0.500000:(tg'=8)&(n'=31) ;
[] (tg=1)&(n=32)-> 0.500000:(tg'=5)&(n'=32) + 0.500000:(tg'=6)&(n'=32) ;
[] (tg=2)&(n=32)-> 0.500000:(tg'=7)&(n'=32) + 0.500000:(tg'=8)&(n'=32) ;
[] (tg=3)&(n=32)-> 0.500000:(tg'=5)&(n'=32) + 0.500000:(tg'=7)&(n'=32) ;
[] (tg=4)&(n=32)-> 0.500000:(tg'=6)&(n'=32) + 0.500000:(tg'=8)&(n'=32) ;
[] (tg=1)&(n=33)-> 0.500000:(tg'=5)&(n'=33) + 0.500000:(tg'=6)&(n'=33) ;
[] (tg=2)&(n=33)-> 0.500000:(tg'=7)&(n'=33) + 0.500000:(tg'=8)&(n'=33) ;
[] (tg=3)&(n=33)-> 0.500000:(tg'=5)&(n'=33) + 0.500000:(tg'=7)&(n'=33) ;
[] (tg=4)&(n=33)-> 0.500000:(tg'=6)&(n'=33) + 0.500000:(tg'=8)&(n'=33) ;
[] (tg=1)&(n=34)-> 0.500000:(tg'=5)&(n'=34) + 0.500000:(tg'=6)&(n'=34) ;
[] (tg=2)&(n=34)-> 0.500000:(tg'=7)&(n'=34) + 0.500000:(tg'=8)&(n'=34) ;
[] (tg=3)&(n=34)-> 0.500000:(tg'=5)&(n'=34) + 0.500000:(tg'=7)&(n'=34) ;
[] (tg=4)&(n=34)-> 0.500000:(tg'=6)&(n'=34) + 0.500000:(tg'=8)&(n'=34) ;
[] (tg=5)&(n=28)-> 1.000000:(tg'=0)&(n'=35) ;
[] (tg=5)&(n=28)-> 1.000000:(tg'=9)&(n'=35) ;
[] (tg=8)&(n=28)| (tg=5)&(n=29)-> 1.000000:(tg'=0)&(n'=36) ;
[] (tg=6)&(n=28)| (tg=7)&(n=28)| (tg=8)&(n=28)| (tg=5)&(n=29)-> 1.000000:(tg'=9)&(n'=36) ;
[] (tg=8)&(n=29)| (tg=5)&(n=30)-> 1.000000:(tg'=0)&(n'=37) ;
[] (tg=6)&(n=29)| (tg=7)&(n=29)| (tg=8)&(n=29)| (tg=5)&(n=30)-> 1.000000:(tg'=9)&(n'=37) ;
[] (tg=8)&(n=30)| (tg=5)&(n=31)-> 1.000000:(tg'=0)&(n'=38) ;
[] (tg=6)&(n=30)| (tg=7)&(n=30)| (tg=8)&(n=30)| (tg=5)&(n=31)-> 1.000000:(tg'=9)&(n'=38) ;
[] (tg=8)&(n=31)| (tg=5)&(n=32)-> 1.000000:(tg'=0)&(n'=39) ;
[] (tg=6)&(n=31)| (tg=7)&(n=31)| (tg=8)&(n=31)| (tg=5)&(n=32)-> 1.000000:(tg'=9)&(n'=39) ;
[] (tg=6)&(n=32)| (tg=7)&(n=32)| (tg=8)&(n=32)| (tg=5)&(n=33)-> 1.000000:(tg'=9)&(n'=40) ;
[] (tg=0)&(n=35)-> 0.500000:(tg'=1)&(n'=35) + 0.500000:(tg'=2)&(n'=35) ;
[] (tg=0)&(n=35)-> 0.500000:(tg'=3)&(n'=35) + 0.500000:(tg'=4)&(n'=35) ;
[] (tg=0)&(n=36)-> 0.500000:(tg'=1)&(n'=36) + 0.500000:(tg'=2)&(n'=36) ;
[] (tg=0)&(n=36)-> 0.500000:(tg'=3)&(n'=36) + 0.500000:(tg'=4)&(n'=36) ;
[] (tg=0)&(n=37)-> 0.500000:(tg'=1)&(n'=37) + 0.500000:(tg'=2)&(n'=37) ;
[] (tg=0)&(n=37)-> 0.500000:(tg'=3)&(n'=37) + 0.500000:(tg'=4)&(n'=37) ;
[] (tg=0)&(n=38)-> 0.500000:(tg'=1)&(n'=38) + 0.500000:(tg'=2)&(n'=38) ;
[] (tg=0)&(n=38)-> 0.500000:(tg'=3)&(n'=38) + 0.500000:(tg'=4)&(n'=38) ;
[] (tg=0)&(n=39)-> 0.500000:(tg'=1)&(n'=39) + 0.500000:(tg'=2)&(n'=39) ;
[] (tg=0)&(n=39)-> 0.500000:(tg'=3)&(n'=39) + 0.500000:(tg'=4)&(n'=39) ;
[] (tg=1)&(n=35)-> 0.500000:(tg'=5)&(n'=35) + 0.500000:(tg'=6)&(n'=35) ;
[] (tg=2)&(n=35)-> 0.500000:(tg'=7)&(n'=35) + 0.500000:(tg'=8)&(n'=35) ;
[] (tg=3)&(n=35)-> 0.500000:(tg'=5)&(n'=35) + 0.500000:(tg'=7)&(n'=35) ;
[] (tg=4)&(n=35)-> 0.500000:(tg'=6)&(n'=35) + 0.500000:(tg'=8)&(n'=35) ;
[] (tg=1)&(n=36)-> 0.500000:(tg'=5)&(n'=36) + 0.500000:(tg'=6)&(n'=36) ;
[] (tg=2)&(n=36)-> 0.500000:(tg'=7)&(n'=36) + 0.500000:(tg'=8)&(n'=36) ;
[] (tg=3)&(n=36)-> 0.500000:(tg'=5)&(n'=36) + 0.500000:(tg'=7)&(n'=36) ;
[] (tg=4)&(n=36)-> 0.500000:(tg'=6)&(n'=36) + 0.500000:(tg'=8)&(n'=36) ;
[] (tg=1)&(n=37)-> 0.500000:(tg'=5)&(n'=37) + 0.500000:(tg'=6)&(n'=37) ;
[] (tg=2)&(n=37)-> 0.500000:(tg'=7)&(n'=37) + 0.500000:(tg'=8)&(n'=37) ;
[] (tg=3)&(n=37)-> 0.500000:(tg'=5)&(n'=37) + 0.500000:(tg'=7)&(n'=37) ;
[] (tg=4)&(n=37)-> 0.500000:(tg'=6)&(n'=37) + 0.500000:(tg'=8)&(n'=37) ;
[] (tg=1)&(n=38)-> 0.500000:(tg'=5)&(n'=38) + 0.500000:(tg'=6)&(n'=38) ;
[] (tg=2)&(n=38)-> 0.500000:(tg'=7)&(n'=38) + 0.500000:(tg'=8)&(n'=38) ;
[] (tg=3)&(n=38)-> 0.500000:(tg'=5)&(n'=38) + 0.500000:(tg'=7)&(n'=38) ;
[] (tg=4)&(n=38)-> 0.500000:(tg'=6)&(n'=38) + 0.500000:(tg'=8)&(n'=38) ;
[] (tg=1)&(n=39)-> 0.500000:(tg'=5)&(n'=39) + 0.500000:(tg'=6)&(n'=39) ;
[] (tg=2)&(n=39)-> 0.500000:(tg'=7)&(n'=39) + 0.500000:(tg'=8)&(n'=39) ;
[] (tg=3)&(n=39)-> 0.500000:(tg'=5)&(n'=39) + 0.500000:(tg'=7)&(n'=39) ;
[] (tg=4)&(n=39)-> 0.500000:(tg'=6)&(n'=39) + 0.500000:(tg'=8)&(n'=39) ;
[] (tg=5)&(n=35)-> 1.000000:(tg'=0)&(n'=40) ;
[] (tg=5)&(n=35)-> 1.000000:(tg'=9)&(n'=41) ;
[] (tg=8)&(n=35)| (tg=5)&(n=36)-> 1.000000:(tg'=0)&(n'=41) ;
[] (tg=6)&(n=35)| (tg=7)&(n=35)| (tg=8)&(n=35)| (tg=5)&(n=36)-> 1.000000:(tg'=9)&(n'=42) ;
[] (tg=8)&(n=36)| (tg=5)&(n=37)-> 1.000000:(tg'=0)&(n'=42) ;
[] (tg=6)&(n=36)| (tg=7)&(n=36)| (tg=8)&(n=36)| (tg=5)&(n=37)-> 1.000000:(tg'=9)&(n'=43) ;
[] (tg=8)&(n=37)| (tg=5)&(n=38)-> 1.000000:(tg'=0)&(n'=43) ;
[] (tg=6)&(n=37)| (tg=7)&(n=37)| (tg=8)&(n=37)| (tg=5)&(n=38)-> 1.000000:(tg'=9)&(n'=44) ;
[] (tg=6)&(n=38)| (tg=7)&(n=38)| (tg=8)&(n=38)| (tg=5)&(n=39)-> 1.000000:(tg'=9)&(n'=45) ;
[] (tg=0)&(n=40)-> 0.500000:(tg'=1)&(n'=40) + 0.500000:(tg'=2)&(n'=40) ;
[] (tg=0)&(n=40)-> 0.500000:(tg'=3)&(n'=40) + 0.500000:(tg'=4)&(n'=40) ;
[] (tg=0)&(n=41)-> 0.500000:(tg'=1)&(n'=41) + 0.500000:(tg'=2)&(n'=41) ;
[] (tg=0)&(n=41)-> 0.500000:(tg'=3)&(n'=41) + 0.500000:(tg'=4)&(n'=41) ;
[] (tg=0)&(n=42)-> 0.500000:(tg'=1)&(n'=42) + 0.500000:(tg'=2)&(n'=42) ;
[] (tg=0)&(n=42)-> 0.500000:(tg'=3)&(n'=42) + 0.500000:(tg'=4)&(n'=42) ;
[] (tg=0)&(n=43)-> 0.500000:(tg'=1)&(n'=43) + 0.500000:(tg'=2)&(n'=43) ;
[] (tg=0)&(n=43)-> 0.500000:(tg'=3)&(n'=43) + 0.500000:(tg'=4)&(n'=43) ;
[] (tg=1)&(n=40)-> 0.500000:(tg'=5)&(n'=40) + 0.500000:(tg'=6)&(n'=40) ;
[] (tg=2)&(n=40)-> 0.500000:(tg'=7)&(n'=40) + 0.500000:(tg'=8)&(n'=40) ;
[] (tg=3)&(n=40)-> 0.500000:(tg'=5)&(n'=40) + 0.500000:(tg'=7)&(n'=40) ;
[] (tg=4)&(n=40)-> 0.500000:(tg'=6)&(n'=40) + 0.500000:(tg'=8)&(n'=40) ;
[] (tg=1)&(n=41)-> 0.500000:(tg'=5)&(n'=41) + 0.500000:(tg'=6)&(n'=41) ;
[] (tg=2)&(n=41)-> 0.500000:(tg'=7)&(n'=41) + 0.500000:(tg'=8)&(n'=41) ;
[] (tg=3)&(n=41)-> 0.500000:(tg'=5)&(n'=41) + 0.500000:(tg'=7)&(n'=41) ;
[] (tg=4)&(n=41)-> 0.500000:(tg'=6)&(n'=41) + 0.500000:(tg'=8)&(n'=41) ;
[] (tg=1)&(n=42)-> 0.500000:(tg'=5)&(n'=42) + 0.500000:(tg'=6)&(n'=42) ;
[] (tg=2)&(n=42)-> 0.500000:(tg'=7)&(n'=42) + 0.500000:(tg'=8)&(n'=42) ;
[] (tg=3)&(n=42)-> 0.500000:(tg'=5)&(n'=42) + 0.500000:(tg'=7)&(n'=42) ;
[] (tg=4)&(n=42)-> 0.500000:(tg'=6)&(n'=42) + 0.500000:(tg'=8)&(n'=42) ;
[] (tg=1)&(n=43)-> 0.500000:(tg'=5)&(n'=43) + 0.500000:(tg'=6)&(n'=43) ;
[] (tg=2)&(n=43)-> 0.500000:(tg'=7)&(n'=43) + 0.500000:(tg'=8)&(n'=43) ;
[] (tg=3)&(n=43)-> 0.500000:(tg'=5)&(n'=43) + 0.500000:(tg'=7)&(n'=43) ;
[] (tg=4)&(n=43)-> 0.500000:(tg'=6)&(n'=43) + 0.500000:(tg'=8)&(n'=43) ;
[] (tg=5)&(n=40)-> 1.000000:(tg'=0)&(n'=44) ;
[] (tg=5)&(n=40)-> 1.000000:(tg'=9)&(n'=46) ;
[] (tg=8)&(n=40)| (tg=5)&(n=41)-> 1.000000:(tg'=0)&(n'=45) ;
[] (tg=6)&(n=40)| (tg=7)&(n=40)| (tg=8)&(n=40)| (tg=5)&(n=41)-> 1.000000:(tg'=9)&(n'=47) ;
[] (tg=8)&(n=41)| (tg=5)&(n=42)-> 1.000000:(tg'=0)&(n'=46) ;
[] (tg=6)&(n=41)| (tg=7)&(n=41)| (tg=8)&(n=41)| (tg=5)&(n=42)-> 1.000000:(tg'=9)&(n'=48) ;
[] (tg=6)&(n=42)| (tg=7)&(n=42)| (tg=8)&(n=42)| (tg=5)&(n=43)-> 1.000000:(tg'=9)&(n'=49) ;
[] (tg=0)&(n=44)-> 0.500000:(tg'=1)&(n'=44) + 0.500000:(tg'=2)&(n'=44) ;
[] (tg=0)&(n=44)-> 0.500000:(tg'=3)&(n'=44) + 0.500000:(tg'=4)&(n'=44) ;
[] (tg=0)&(n=45)-> 0.500000:(tg'=1)&(n'=45) + 0.500000:(tg'=2)&(n'=45) ;
[] (tg=0)&(n=45)-> 0.500000:(tg'=3)&(n'=45) + 0.500000:(tg'=4)&(n'=45) ;
[] (tg=0)&(n=46)-> 0.500000:(tg'=1)&(n'=46) + 0.500000:(tg'=2)&(n'=46) ;
[] (tg=0)&(n=46)-> 0.500000:(tg'=3)&(n'=46) + 0.500000:(tg'=4)&(n'=46) ;
[] (tg=1)&(n=44)-> 0.500000:(tg'=5)&(n'=44) + 0.500000:(tg'=6)&(n'=44) ;
[] (tg=2)&(n=44)-> 0.500000:(tg'=7)&(n'=44) + 0.500000:(tg'=8)&(n'=44) ;
[] (tg=3)&(n=44)-> 0.500000:(tg'=5)&(n'=44) + 0.500000:(tg'=7)&(n'=44) ;
[] (tg=4)&(n=44)-> 0.500000:(tg'=6)&(n'=44) + 0.500000:(tg'=8)&(n'=44) ;
[] (tg=1)&(n=45)-> 0.500000:(tg'=5)&(n'=45) + 0.500000:(tg'=6)&(n'=45) ;
[] (tg=2)&(n=45)-> 0.500000:(tg'=7)&(n'=45) + 0.500000:(tg'=8)&(n'=45) ;
[] (tg=3)&(n=45)-> 0.500000:(tg'=5)&(n'=45) + 0.500000:(tg'=7)&(n'=45) ;
[] (tg=4)&(n=45)-> 0.500000:(tg'=6)&(n'=45) + 0.500000:(tg'=8)&(n'=45) ;
[] (tg=1)&(n=46)-> 0.500000:(tg'=5)&(n'=46) + 0.500000:(tg'=6)&(n'=46) ;
[] (tg=2)&(n=46)-> 0.500000:(tg'=7)&(n'=46) + 0.500000:(tg'=8)&(n'=46) ;
[] (tg=3)&(n=46)-> 0.500000:(tg'=5)&(n'=46) + 0.500000:(tg'=7)&(n'=46) ;
[] (tg=4)&(n=46)-> 0.500000:(tg'=6)&(n'=46) + 0.500000:(tg'=8)&(n'=46) ;
[] (tg=5)&(n=44)-> 1.000000:(tg'=0)&(n'=47) ;
[] (tg=5)&(n=44)-> 1.000000:(tg'=9)&(n'=50) ;
[] (tg=8)&(n=44)| (tg=5)&(n=45)-> 1.000000:(tg'=0)&(n'=48) ;
[] (tg=6)&(n=44)| (tg=7)&(n=44)| (tg=8)&(n=44)| (tg=5)&(n=45)-> 1.000000:(tg'=9)&(n'=51) ;
[] (tg=6)&(n=45)| (tg=7)&(n=45)| (tg=8)&(n=45)| (tg=5)&(n=46)-> 1.000000:(tg'=9)&(n'=52) ;
[] (tg=0)&(n=47)-> 0.500000:(tg'=1)&(n'=47) + 0.500000:(tg'=2)&(n'=47) ;
[] (tg=0)&(n=47)-> 0.500000:(tg'=3)&(n'=47) + 0.500000:(tg'=4)&(n'=47) ;
[] (tg=0)&(n=48)-> 0.500000:(tg'=1)&(n'=48) + 0.500000:(tg'=2)&(n'=48) ;
[] (tg=0)&(n=48)-> 0.500000:(tg'=3)&(n'=48) + 0.500000:(tg'=4)&(n'=48) ;
[] (tg=1)&(n=47)-> 0.500000:(tg'=5)&(n'=47) + 0.500000:(tg'=6)&(n'=47) ;
[] (tg=2)&(n=47)-> 0.500000:(tg'=7)&(n'=47) + 0.500000:(tg'=8)&(n'=47) ;
[] (tg=3)&(n=47)-> 0.500000:(tg'=5)&(n'=47) + 0.500000:(tg'=7)&(n'=47) ;
[] (tg=4)&(n=47)-> 0.500000:(tg'=6)&(n'=47) + 0.500000:(tg'=8)&(n'=47) ;
[] (tg=1)&(n=48)-> 0.500000:(tg'=5)&(n'=48) + 0.500000:(tg'=6)&(n'=48) ;
[] (tg=2)&(n=48)-> 0.500000:(tg'=7)&(n'=48) + 0.500000:(tg'=8)&(n'=48) ;
[] (tg=3)&(n=48)-> 0.500000:(tg'=5)&(n'=48) + 0.500000:(tg'=7)&(n'=48) ;
[] (tg=4)&(n=48)-> 0.500000:(tg'=6)&(n'=48) + 0.500000:(tg'=8)&(n'=48) ;
[] (tg=5)&(n=47)-> 1.000000:(tg'=0)&(n'=49) ;
[] (tg=5)&(n=47)-> 1.000000:(tg'=9)&(n'=53) ;
[] (tg=8)&(n=47)| (tg=5)&(n=48)-> 1.000000:(tg'=0)&(n'=50) ;
[] (tg=6)&(n=47)| (tg=7)&(n=47)| (tg=8)&(n=47)| (tg=5)&(n=48)-> 1.000000:(tg'=9)&(n'=54) ;
[] (tg=0)&(n=49)-> 0.500000:(tg'=1)&(n'=49) + 0.500000:(tg'=2)&(n'=49) ;
[] (tg=0)&(n=49)-> 0.500000:(tg'=3)&(n'=49) + 0.500000:(tg'=4)&(n'=49) ;
[] (tg=0)&(n=50)-> 0.500000:(tg'=1)&(n'=50) + 0.500000:(tg'=2)&(n'=50) ;
[] (tg=0)&(n=50)-> 0.500000:(tg'=3)&(n'=50) + 0.500000:(tg'=4)&(n'=50) ;
[] (tg=1)&(n=49)-> 0.500000:(tg'=5)&(n'=49) + 0.500000:(tg'=6)&(n'=49) ;
[] (tg=2)&(n=49)-> 0.500000:(tg'=7)&(n'=49) + 0.500000:(tg'=8)&(n'=49) ;
[] (tg=3)&(n=49)-> 0.500000:(tg'=5)&(n'=49) + 0.500000:(tg'=7)&(n'=49) ;
[] (tg=4)&(n=49)-> 0.500000:(tg'=6)&(n'=49) + 0.500000:(tg'=8)&(n'=49) ;
[] (tg=1)&(n=50)-> 0.500000:(tg'=5)&(n'=50) + 0.500000:(tg'=6)&(n'=50) ;
[] (tg=2)&(n=50)-> 0.500000:(tg'=7)&(n'=50) + 0.500000:(tg'=8)&(n'=50) ;
[] (tg=3)&(n=50)-> 0.500000:(tg'=5)&(n'=50) + 0.500000:(tg'=7)&(n'=50) ;
[] (tg=4)&(n=50)-> 0.500000:(tg'=6)&(n'=50) + 0.500000:(tg'=8)&(n'=50) ;
[] (tg=5)&(n=49)-> 1.000000:(tg'=0)&(n'=51) ;
[] (tg=5)&(n=49)-> 1.000000:(tg'=9)&(n'=55) ;
[] (tg=0)&(n=51)-> 0.500000:(tg'=1)&(n'=51) + 0.500000:(tg'=2)&(n'=51) ;
[] (tg=0)&(n=51)-> 0.500000:(tg'=3)&(n'=51) + 0.500000:(tg'=4)&(n'=51) ;
[] (tg=9)&(n=0..33)| (tg=9)&(n=35..55)-> 1.000000:(tg'=10)&(n'=0) ;
[] (tg=9)&(n=19)| (tg=9)&(n=24..26)| (tg=9)&(n=29..34)| (tg=9)&(n=36..55)-> 1.000000:(tg'=11)&(n'=0) ;
[] (tg=1)&(n=51)-> 0.500000:(tg'=5)&(n'=51) + 0.500000:(tg'=6)&(n'=51) ;
[] (tg=2)&(n=51)-> 0.500000:(tg'=7)&(n'=51) + 0.500000:(tg'=8)&(n'=51) ;
[] (tg=3)&(n=51)-> 0.500000:(tg'=5)&(n'=51) + 0.500000:(tg'=7)&(n'=51) ;
[] (tg=4)&(n=51)-> 0.500000:(tg'=6)&(n'=51) + 0.500000:(tg'=8)&(n'=51) ;
[] (tg=5)&(n=27)| (tg=8)&(n=26..27)| (tg=5)&(n=33..34)| (tg=8)&(n=32..34)| (tg=5)&(n=39)| (tg=8)&(n=38..39)| (tg=5)&(n=43)| (tg=8)&(n=42..43)| (tg=5)&(n=46)| (tg=8)&(n=45..46)| (tg=5)&(n=50..51)| (tg=8)&(n=48..51)-> 1.000000:(tg'=0)&(n'=34) ;
[] (tg=6)&(n=27)| (tg=7)&(n=27)| (tg=8)&(n=27)| (tg=5)&(n=34)| (tg=6)&(n=33..34)| (tg=7)&(n=33..34)| (tg=8)&(n=33..34)| (tg=6)&(n=39)| (tg=7)&(n=39)| (tg=8)&(n=39)| (tg=6)&(n=43)| (tg=7)&(n=43)| (tg=8)&(n=43)| (tg=6)&(n=46)| (tg=7)&(n=46)| (tg=8)&(n=46)| (tg=5)&(n=50..51)| (tg=6)&(n=48..51)| (tg=7)&(n=48..51)| (tg=8)&(n=48..51)-> 1.000000:(tg'=9)&(n'=34) ;


endmodule