%var: 'kp0' 3 %var: 'ku1' 14 %var: 'kp1' 15 %var: 'ku2' 98 %var: 'kp2' 75 %var: 'ku3' 686 %var: 'kp3' 375 %var: 'ku4' 4802 %var: 'kp4' 1875 %var: 'ku5' 33614 %var: 'kp5' 9375 %var: 'ku6' 235298 %agent: A(s1~u~p,s2~u~p,s3~u~p,s4~u~p,s5~u~p,s6~u~p,p) %agent: P(l,r) %init: 100 A(p!1) , P(l!1,r) A(s1~u,p!1) , P(l!1,r) -> A(s1~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s2~u,p!1) , P(l!1,r) -> A(s2~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s3~u,p!1) , P(l!1,r) -> A(s3~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s4~u,p!1) , P(l!1,r) -> A(s4~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s5~u,p!1) , P(l!1,r) -> A(s5~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s6~u,p!1) , P(l!1,r) -> A(s6~p,p!1) , P(l!2,r) , P(l!1,r!2) @kp0 A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s1~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r) @ku1 A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s2~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r) @ku1 A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s3~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r) @ku1 A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s4~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r) @ku1 A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s5~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r) @ku1 A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r) -> A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) @kp1 A(s6~p,p!1) , P(l!2,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r) @ku1 A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) -> A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) @kp2 A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r) @ku2 A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) -> A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) @kp3 A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r) @ku3 A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) -> A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) @kp4 A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r) @ku4 A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) -> A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) @kp5 A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r) @ku5 A(s1~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s1~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6 A(s2~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s2~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6 A(s3~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s3~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6 A(s4~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s4~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6 A(s5~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s5~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6 A(s6~p,p!1) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r!7) , P(l!7,r) , P(l!1,r!2) -> A(s6~u,p!1) , P(l!1,r!2) , P(l!2,r!3) , P(l!3,r!4) , P(l!4,r!5) , P(l!5,r!6) , P(l!6,r) @ku6