//
// 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)->