Test CoRW1 Allowed
States 1
0:X1=0; [x]=1;
No
Witnesses
Positive: 0 Negative: 1
Condition exists (0:X1=1 /\ [x]=1)
Observation CoRW1 Never 0 1
Time CoRW1 0.00
Hash=a2b90612a7d7f2b901c98ff5ffbc3eaf

Test MP+READ Allowed
States 6
1:X1=0; 1:X3=0; 1:X5=0;
1:X1=0; 1:X3=0; 1:X5=1;
1:X1=0; 1:X3=1; 1:X5=0;
1:X1=0; 1:X3=1; 1:X5=1;
1:X1=1; 1:X3=0; 1:X5=1;
1:X1=1; 1:X3=1; 1:X5=1;
No
Witnesses
Positive: 0 Negative: 6
Condition exists (1:X1=1 /\ 1:X3=0 /\ 1:X5=0)
Observation MP+READ Never 0 6
Time MP+READ 0.00
Hash=d3469448002a4e30ba23332d32e23a33

Test CoRW2 Allowed
States 3
1:X1=0; [x]=1;
1:X1=0; [x]=2;
1:X1=2; [x]=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:X1=2 /\ [x]=2)
Observation CoRW2 Never 0 3
Time CoRW2 0.00
Hash=8a02f168b6c0e7b1ef6d936e273d58c1

Test CoWW Allowed
States 1
[x]=1;
No
Witnesses
Positive: 0 Negative: 1
Condition exists ([x]=2)
Observation CoWW Never 0 1
Time CoWW 0.00
Hash=dd4abd515d300a7fed59627163f4d2d3

Test CoRR Allowed
States 3
1:X1=0; 1:X2=0; [x]=1;
1:X1=0; 1:X2=1; [x]=1;
1:X1=1; 1:X2=1; [x]=1;
No
Witnesses
Positive: 0 Negative: 3
Condition exists (1:X1=1 /\ 1:X2=0 /\ [x]=1)
Observation CoRR Never 0 3
Time CoRR 0.00
Hash=090ba3e35c0dcd26952a8a3a230b46bd

Test SB+po+posW-posW-po Required
States 8
0:X3=0; 1:X5=0; [x]=1; [y]=3;
0:X3=0; 1:X5=1; [x]=1; [y]=3;
0:X3=1; 1:X5=0; [x]=1; [y]=3;
0:X3=1; 1:X5=1; [x]=1; [y]=3;
0:X3=2; 1:X5=0; [x]=1; [y]=3;
0:X3=2; 1:X5=1; [x]=1; [y]=3;
0:X3=3; 1:X5=0; [x]=1; [y]=3;
0:X3=3; 1:X5=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation SB+po+posW-posW-po Always 8 0
Time SB+po+posW-posW-po 0.01
Hash=efd1d5d5d74c6d03f208a967d358f2da

Test CoWR0 Allowed
States 1
0:X2=1; [x]=1;
No
Witnesses
Positive: 0 Negative: 1
Condition exists (0:X2=0 /\ [x]=1)
Observation CoWR0 Never 0 1
Time CoWR0 0.00
Hash=1a415c90f6519b69702edc2de46c93f8

Test R+posW-posW-po+po Required
States 8
1:X3=0; [x]=3; [y]=1;
1:X3=0; [x]=3; [y]=2;
1:X3=1; [x]=3; [y]=1;
1:X3=1; [x]=3; [y]=2;
1:X3=2; [x]=3; [y]=1;
1:X3=2; [x]=3; [y]=2;
1:X3=3; [x]=3; [y]=1;
1:X3=3; [x]=3; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+posW-posW-po+po Always 8 0
Time R+posW-posW-po+po 0.01
Hash=be97a44025c0347d64074dae28da9184

Test R+posW-pos+poW-po Required
States 5
1:X4=1; [x]=3; [y]=1;
1:X4=2; [x]=3; [y]=1;
1:X4=3; [x]=3; [y]=1;
1:X4=4; [x]=3; [y]=1;
1:X4=4; [x]=4; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+posW-pos+poW-po Always 10 0
Time R+posW-pos+poW-po 0.01
Hash=b6613a951547025ed0478966c91707cd

Test R+po+posW-posW-po Required
States 4
1:X5=0; [x]=1; [y]=1;
1:X5=0; [x]=1; [y]=4;
1:X5=1; [x]=1; [y]=1;
1:X5=1; [x]=1; [y]=4;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+posW-posW-po Always 8 0
Time R+po+posW-posW-po 0.00
Hash=2f6d0d2dab67a1c1e94273e343cc9a86

Test MP+posW-posW-po+po Required
States 8
1:X1=0; 1:X3=0; [x]=3; [y]=1;
1:X1=0; 1:X3=1; [x]=3; [y]=1;
1:X1=0; 1:X3=2; [x]=3; [y]=1;
1:X1=0; 1:X3=3; [x]=3; [y]=1;
1:X1=1; 1:X3=0; [x]=3; [y]=1;
1:X1=1; 1:X3=1; [x]=3; [y]=1;
1:X1=1; 1:X3=2; [x]=3; [y]=1;
1:X1=1; 1:X3=3; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+posW-posW-po+po Always 8 0
Time MP+posW-posW-po+po 0.01
Hash=6d9198fe95747282e357ac2381b128a2

Test R+posW-pos+poR-po Required
States 5
1:X4=1; [x]=3;
1:X4=2; [x]=3;
1:X4=3; [x]=3;
1:X4=4; [x]=3;
1:X4=4; [x]=4;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+posW-pos+poR-po Always 10 0
Time R+posW-pos+poR-po 0.01
Hash=de362bd7cfe46830a5e6081396e99fbc

Test MP+posW-pos+poR-po Required
States 10
1:X1=0; 1:X4=0; [x]=3;
1:X1=0; 1:X4=1; [x]=3;
1:X1=0; 1:X4=2; [x]=3;
1:X1=0; 1:X4=3; [x]=3;
1:X1=1; 1:X4=1; [x]=3;
1:X1=1; 1:X4=2; [x]=3;
1:X1=1; 1:X4=3; [x]=3;
1:X1=2; 1:X4=2; [x]=3;
1:X1=2; 1:X4=3; [x]=3;
1:X1=3; 1:X4=3; [x]=3;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+posW-pos+poR-po Always 10 0
Time MP+posW-pos+poR-po 0.01
Hash=f2e3dfe578e9b33af955ba0e6e1ab2f8

Test 2+2W+posW-pos+poW-po Required
States 2
[x]=1; [y]=1;
[x]=4; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation 2+2W+posW-pos+poW-po Always 10 0
Time 2+2W+posW-pos+poW-po 0.00
Hash=5da9a527ddfe69fd3f526fa707d2d849

Test MP+posW-pos+poW-po Required
States 10
1:X1=0; 1:X4=0; [x]=3; [y]=1;
1:X1=0; 1:X4=1; [x]=3; [y]=1;
1:X1=0; 1:X4=2; [x]=3; [y]=1;
1:X1=0; 1:X4=3; [x]=3; [y]=1;
1:X1=1; 1:X4=1; [x]=3; [y]=1;
1:X1=1; 1:X4=2; [x]=3; [y]=1;
1:X1=1; 1:X4=3; [x]=3; [y]=1;
1:X1=2; 1:X4=2; [x]=3; [y]=1;
1:X1=2; 1:X4=3; [x]=3; [y]=1;
1:X1=3; 1:X4=3; [x]=3; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+posW-pos+poW-po Always 10 0
Time MP+posW-pos+poW-po 0.01
Hash=2dc353bf848bee6596fa0dbbc621c8b7

Test S+posW-pos+poW-po Required
States 7
1:X1=0; [x]=1; [y]=1;
1:X1=0; [x]=4; [y]=1;
1:X1=2; [x]=1; [y]=1;
1:X1=2; [x]=4; [y]=1;
1:X1=3; [x]=1; [y]=1;
1:X1=3; [x]=4; [y]=1;
1:X1=4; [x]=1; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+posW-pos+poW-po Always 10 0
Time S+posW-pos+poW-po 0.01
Hash=ba7cbec508ca5d75570afe91b2c91ef3

Test 2+2W+po+posW-posW-po Required
States 4
[x]=1; [y]=1;
[x]=1; [y]=4;
[x]=2; [y]=1;
[x]=2; [y]=4;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+posW-posW-po Always 8 0
Time 2+2W+po+posW-posW-po 0.00
Hash=3300def767cf05fa77da727ba898324b

Test 2+2W+posW-pos+poR-po Required
States 2
[x]=1;
[x]=4;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation 2+2W+posW-pos+poR-po Always 10 0
Time 2+2W+posW-pos+poR-po 0.00
Hash=8c696f0b278f3f1d76666c75e2eba129

Test S+posW-posW-po+po Required
States 4
1:X1=0; [x]=1; [y]=1;
1:X1=0; [x]=4; [y]=1;
1:X1=1; [x]=1; [y]=1;
1:X1=1; [x]=4; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posW-posW-po+po Always 8 0
Time S+posW-posW-po+po 0.00
Hash=ee28b0ca7cd98c28d612f13177f9b7de

Test S+posW-pos+poR-po Required
States 7
1:X1=0; [x]=1;
1:X1=0; [x]=4;
1:X1=2; [x]=1;
1:X1=2; [x]=4;
1:X1=3; [x]=1;
1:X1=3; [x]=4;
1:X1=4; [x]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+posW-pos+poR-po Always 10 0
Time S+posW-pos+poR-po 0.01
Hash=5611fc40725cc27c679186e93b4c95e2

Test 2+2W+po+poW-posW-pos Required
States 4
[x]=3; [y]=1;
[x]=3; [y]=2;
[x]=4; [y]=1;
[x]=4; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+poW-posW-pos Always 8 0
Time 2+2W+po+poW-posW-pos 0.00
Hash=3fc2c879c22fd4c87761881dd8bca3d0

Test MP+poW-posW-pos+po Required
States 8
1:X1=0; 1:X3=0; [x]=1; [y]=3;
1:X1=0; 1:X3=1; [x]=1; [y]=3;
1:X1=1; 1:X3=0; [x]=1; [y]=3;
1:X1=1; 1:X3=1; [x]=1; [y]=3;
1:X1=2; 1:X3=0; [x]=1; [y]=3;
1:X1=2; 1:X3=1; [x]=1; [y]=3;
1:X1=3; 1:X3=0; [x]=1; [y]=3;
1:X1=3; 1:X3=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+poW-posW-pos+po Always 8 0
Time MP+poW-posW-pos+po 0.01
Hash=6f16fbefd7a06489055251e4cce4bf14

Test R+poW-posW-pos+po Required
States 4
1:X3=0; [x]=1; [y]=3;
1:X3=0; [x]=1; [y]=4;
1:X3=1; [x]=1; [y]=3;
1:X3=1; [x]=1; [y]=4;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+poW-posW-pos+po Always 8 0
Time R+poW-posW-pos+po 0.00
Hash=afb097a48188640ebe170403b4506fa2

Test R+posW-posR-po+po Required
States 6
0:X3=2; 1:X3=0; [x]=2; [y]=1;
0:X3=2; 1:X3=0; [x]=2; [y]=2;
0:X3=2; 1:X3=1; [x]=2; [y]=1;
0:X3=2; 1:X3=1; [x]=2; [y]=2;
0:X3=2; 1:X3=2; [x]=2; [y]=1;
0:X3=2; 1:X3=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation R+posW-posR-po+po Always 6 0
Time R+posW-posR-po+po 0.01
Hash=dab722810bc5db66ac8aabccb8662b86

Test S+po+poW-posW-pos Required
States 4
1:X1=0; [x]=3; [y]=1;
1:X1=0; [x]=4; [y]=1;
1:X1=1; [x]=3; [y]=1;
1:X1=1; [x]=4; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+poW-posW-pos Always 8 0
Time S+po+poW-posW-pos 0.00
Hash=183037c9c286da921f0dde654f66459a

Test MP+posW-posR-po+po Required
States 6
0:X3=2; 1:X1=0; 1:X3=0; [x]=2; [y]=1;
0:X3=2; 1:X1=0; 1:X3=1; [x]=2; [y]=1;
0:X3=2; 1:X1=0; 1:X3=2; [x]=2; [y]=1;
0:X3=2; 1:X1=1; 1:X3=0; [x]=2; [y]=1;
0:X3=2; 1:X1=1; 1:X3=1; [x]=2; [y]=1;
0:X3=2; 1:X1=1; 1:X3=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+posW-posR-po+po Always 6 0
Time MP+posW-posR-po+po 0.01
Hash=aa4f151ba8edb2b5f54a00d6f580ebbb

Test SB+posW-pos+poW-po Required
States 5
0:X3=2; 1:X4=1; [x]=2; [y]=1;
0:X3=2; 1:X4=2; [x]=2; [y]=1;
0:X3=2; 1:X4=3; [x]=2; [y]=1;
0:X3=2; 1:X4=3; [x]=3; [y]=1;
0:X3=3; 1:X4=3; [x]=3; [y]=1;
Ok
Witnesses
Positive: 7 Negative: 0
Condition forall (true)
Observation SB+posW-pos+poW-po Always 7 0
Time SB+posW-pos+poW-po 0.01
Hash=adbbf718bd61e530b91abb77e7c04603

Test SB+posW-pos+poR-po Required
States 5
0:X3=2; 1:X4=1; [x]=2;
0:X3=2; 1:X4=2; [x]=2;
0:X3=2; 1:X4=3; [x]=2;
0:X3=2; 1:X4=3; [x]=3;
0:X3=3; 1:X4=3; [x]=3;
Ok
Witnesses
Positive: 7 Negative: 0
Condition forall (true)
Observation SB+posW-pos+poR-po Always 7 0
Time SB+posW-pos+poR-po 0.01
Hash=4e64d2149b9f288c90269e67ff6cf174

Test LB+po+poW-posW-pos Required
States 8
0:X1=0; 1:X1=0; [x]=3; [y]=1;
0:X1=0; 1:X1=1; [x]=3; [y]=1;
0:X1=1; 1:X1=0; [x]=3; [y]=1;
0:X1=1; 1:X1=1; [x]=3; [y]=1;
0:X1=2; 1:X1=0; [x]=3; [y]=1;
0:X1=2; 1:X1=1; [x]=3; [y]=1;
0:X1=3; 1:X1=0; [x]=3; [y]=1;
0:X1=3; 1:X1=1; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation LB+po+poW-posW-pos Always 8 0
Time LB+po+poW-posW-pos 0.01
Hash=3350cd65cc1819f4b2761d0f69812d1f

Test SB+po+posW-posR-po Required
States 6
0:X3=0; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
0:X3=0; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
0:X3=1; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
0:X3=1; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
0:X3=2; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
0:X3=2; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation SB+po+posW-posR-po Always 6 0
Time SB+po+posW-posR-po 0.01
Hash=667e174453cc704701c3314031a17121

Test 2+2W+po+posW-posR-po Required
States 6
1:X3=1; [x]=1; [y]=1;
1:X3=1; [x]=2; [y]=1;
1:X3=3; [x]=1; [y]=1;
1:X3=3; [x]=1; [y]=3;
1:X3=3; [x]=2; [y]=1;
1:X3=3; [x]=2; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+posW-posR-po Always 8 0
Time 2+2W+po+posW-posR-po 0.01
Hash=46dde64be6aedad6d2fa634514ee77d9

Test R+po+posW-posR-po Required
States 6
1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X3=3; 1:X5=0; [x]=1; [y]=1;
1:X3=3; 1:X5=0; [x]=1; [y]=3;
1:X3=3; 1:X5=1; [x]=1; [y]=1;
1:X3=3; 1:X5=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+posW-posR-po Always 8 0
Time R+po+posW-posR-po 0.01
Hash=01e1e7c9319b40ab81a060064d432a09

Test R+poW-po+posW-pos Required
States 4
1:X3=1; [x]=1; [y]=1;
1:X3=3; [x]=1; [y]=1;
1:X3=3; [x]=3; [y]=1;
1:X3=4; [x]=1; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+poW-po+posW-pos Always 10 0
Time R+poW-po+posW-pos 0.01
Hash=1c6d5f40533de934b33f025fcd162cfc

Test S+poW-posW-pos+po Required
States 8
1:X1=0; [x]=1; [y]=3;
1:X1=0; [x]=2; [y]=3;
1:X1=1; [x]=1; [y]=3;
1:X1=1; [x]=2; [y]=3;
1:X1=2; [x]=1; [y]=3;
1:X1=2; [x]=2; [y]=3;
1:X1=3; [x]=1; [y]=3;
1:X1=3; [x]=2; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+poW-posW-pos+po Always 8 0
Time S+poW-posW-pos+po 0.01
Hash=41e7bc0b1e98a618a656173a1111406f

Test S+posW-posR-po+po Required
States 6
0:X3=1; 1:X1=0; [x]=1; [y]=1;
0:X3=1; 1:X1=1; [x]=1; [y]=1;
0:X3=3; 1:X1=0; [x]=1; [y]=1;
0:X3=3; 1:X1=0; [x]=3; [y]=1;
0:X3=3; 1:X1=1; [x]=1; [y]=1;
0:X3=3; 1:X1=1; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posW-posR-po+po Always 8 0
Time S+posW-posR-po+po 0.01
Hash=5a428bcf145b5a8895391bec77278217

Test R+poR-po+posW-pos Required
States 4
1:X3=1; [x]=1;
1:X3=3; [x]=1;
1:X3=3; [x]=3;
1:X3=4; [x]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+poR-po+posW-pos Always 10 0
Time R+poR-po+posW-pos 0.01
Hash=a595ab4d3d9343147f3b73be59148e70

Test SB+po+poW-posW-pos Required
States 6
0:X3=0; 1:X5=2; [x]=2; [y]=1;
0:X3=0; 1:X5=2; [x]=3; [y]=1;
0:X3=0; 1:X5=3; [x]=3; [y]=1;
0:X3=1; 1:X5=2; [x]=2; [y]=1;
0:X3=1; 1:X5=2; [x]=3; [y]=1;
0:X3=1; 1:X5=3; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation SB+po+poW-posW-pos Always 8 0
Time SB+po+poW-posW-pos 0.01
Hash=71297801e286760c350f30da72190bca

Test R+po+poW-posW-pos Required
States 6
1:X5=2; [x]=2; [y]=1;
1:X5=2; [x]=2; [y]=2;
1:X5=2; [x]=3; [y]=1;
1:X5=2; [x]=3; [y]=2;
1:X5=3; [x]=3; [y]=1;
1:X5=3; [x]=3; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+poW-posW-pos Always 8 0
Time R+po+poW-posW-pos 0.01
Hash=cfb33793cf2387ab9f31416f7418da41

Test MP+po+poW-posW-pos Required
States 6
1:X1=0; 1:X5=2; [x]=2; [y]=1;
1:X1=0; 1:X5=2; [x]=3; [y]=1;
1:X1=0; 1:X5=3; [x]=3; [y]=1;
1:X1=1; 1:X5=2; [x]=2; [y]=1;
1:X1=1; 1:X5=2; [x]=3; [y]=1;
1:X1=1; 1:X5=3; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+poW-posW-pos Always 8 0
Time MP+po+poW-posW-pos 0.01
Hash=5575bf3f807c17e9d8383905d5bc3b2e

Test R+posR-pos+poW-po Required
States 6
0:X2=1; 1:X4=1; [x]=2; [y]=1;
0:X2=1; 1:X4=2; [x]=2; [y]=1;
0:X2=1; 1:X4=3; [x]=2; [y]=1;
0:X2=1; 1:X4=3; [x]=3; [y]=1;
0:X2=3; 1:X4=2; [x]=2; [y]=1;
0:X2=3; 1:X4=3; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+posR-pos+poW-po Always 8 0
Time R+posR-pos+poW-po 0.01
Hash=70888d86fdc0ab445cb8620699f2879d

Test SB+po+posR-posW-po Required
States 6
0:X3=0; 1:X2=1; 1:X5=0; [x]=1; [y]=2;
0:X3=0; 1:X2=1; 1:X5=1; [x]=1; [y]=2;
0:X3=1; 1:X2=1; 1:X5=0; [x]=1; [y]=2;
0:X3=1; 1:X2=1; 1:X5=1; [x]=1; [y]=2;
0:X3=2; 1:X2=1; 1:X5=0; [x]=1; [y]=2;
0:X3=2; 1:X2=1; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation SB+po+posR-posW-po Always 6 0
Time SB+po+posR-posW-po 0.01
Hash=f450b7e8bf0cbf2084cda9efa5a5d75f

Test R+posR-posW-po+po Required
States 6
0:X2=1; 1:X3=0; [x]=2; [y]=1;
0:X2=1; 1:X3=0; [x]=2; [y]=2;
0:X2=1; 1:X3=1; [x]=2; [y]=1;
0:X2=1; 1:X3=1; [x]=2; [y]=2;
0:X2=1; 1:X3=2; [x]=2; [y]=1;
0:X2=1; 1:X3=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation R+posR-posW-po+po Always 6 0
Time R+posR-posW-po+po 0.01
Hash=12e41f4a2163bdd67ec21605d9770837

Test MP+posR-pos+poW-po Required
States 6
0:X2=1; 1:X1=0; 1:X4=0; [x]=2; [y]=1;
0:X2=1; 1:X1=0; 1:X4=1; [x]=2; [y]=1;
0:X2=1; 1:X1=0; 1:X4=2; [x]=2; [y]=1;
0:X2=1; 1:X1=1; 1:X4=1; [x]=2; [y]=1;
0:X2=1; 1:X1=1; 1:X4=2; [x]=2; [y]=1;
0:X2=1; 1:X1=2; 1:X4=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+posR-pos+poW-po Always 6 0
Time MP+posR-pos+poW-po 0.01
Hash=09542428376654fcb88930ccdd77993e

Test R+po+posR-posW-po Required
States 6
1:X2=1; 1:X5=0; [x]=1; [y]=3;
1:X2=1; 1:X5=1; [x]=1; [y]=3;
1:X2=2; 1:X5=0; [x]=1; [y]=1;
1:X2=2; 1:X5=0; [x]=1; [y]=3;
1:X2=2; 1:X5=1; [x]=1; [y]=1;
1:X2=2; 1:X5=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+posR-posW-po Always 8 0
Time R+po+posR-posW-po 0.01
Hash=14bff3f5f523013241f996dd2068d473

Test MP+posR-posW-po+po Required
States 6
0:X2=1; 1:X1=0; 1:X3=0; [x]=2; [y]=1;
0:X2=1; 1:X1=0; 1:X3=1; [x]=2; [y]=1;
0:X2=1; 1:X1=0; 1:X3=2; [x]=2; [y]=1;
0:X2=1; 1:X1=1; 1:X3=0; [x]=2; [y]=1;
0:X2=1; 1:X1=1; 1:X3=1; [x]=2; [y]=1;
0:X2=1; 1:X1=1; 1:X3=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+posR-posW-po+po Always 6 0
Time MP+posR-posW-po+po 0.01
Hash=216771d0290ff705ef15377b770f34c6

Test R+posR-pos+poR-po Required
States 6
0:X2=1; 1:X4=1; [x]=2;
0:X2=1; 1:X4=2; [x]=2;
0:X2=1; 1:X4=3; [x]=2;
0:X2=1; 1:X4=3; [x]=3;
0:X2=3; 1:X4=2; [x]=2;
0:X2=3; 1:X4=3; [x]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+posR-pos+poR-po Always 8 0
Time R+posR-pos+poR-po 0.01
Hash=14696baed2c2c024f89170464105040c

Test MP+posR-pos+poR-po Required
States 6
0:X2=1; 1:X1=0; 1:X4=0; [x]=2;
0:X2=1; 1:X1=0; 1:X4=1; [x]=2;
0:X2=1; 1:X1=0; 1:X4=2; [x]=2;
0:X2=1; 1:X1=1; 1:X4=1; [x]=2;
0:X2=1; 1:X1=1; 1:X4=2; [x]=2;
0:X2=1; 1:X1=2; 1:X4=2; [x]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+posR-pos+poR-po Always 6 0
Time MP+posR-pos+poR-po 0.01
Hash=f668695c9a1921cbfa7cc97805f6865a

Test 2+2W+po+posR-posW-po Required
States 6
1:X2=1; [x]=1; [y]=3;
1:X2=1; [x]=2; [y]=3;
1:X2=2; [x]=1; [y]=1;
1:X2=2; [x]=1; [y]=3;
1:X2=2; [x]=2; [y]=1;
1:X2=2; [x]=2; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+posR-posW-po Always 8 0
Time 2+2W+po+posR-posW-po 0.01
Hash=fca45c49dc7ed343efa567f34f67c02d

Test S+posR-posW-po+po Required
States 6
0:X2=1; 1:X1=0; [x]=3; [y]=1;
0:X2=1; 1:X1=1; [x]=3; [y]=1;
0:X2=2; 1:X1=0; [x]=1; [y]=1;
0:X2=2; 1:X1=0; [x]=3; [y]=1;
0:X2=2; 1:X1=1; [x]=1; [y]=1;
0:X2=2; 1:X1=1; [x]=3; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posR-posW-po+po Always 8 0
Time S+posR-posW-po+po 0.01
Hash=3bda684faf4f0d107ccf198f9fc03179

Test S+posR-pos+poW-po Required
States 7
0:X2=1; 1:X1=0; [x]=3; [y]=1;
0:X2=1; 1:X1=2; [x]=3; [y]=1;
0:X2=2; 1:X1=0; [x]=1; [y]=1;
0:X2=2; 1:X1=0; [x]=3; [y]=1;
0:X2=2; 1:X1=2; [x]=1; [y]=1;
0:X2=2; 1:X1=2; [x]=3; [y]=1;
0:X2=2; 1:X1=3; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posR-pos+poW-po Always 8 0
Time S+posR-pos+poW-po 0.01
Hash=a5c00717cd7f1bf7b817bba31949a6c3

Test 2+2W+posR-pos+poW-po Required
States 5
0:X2=1; [x]=3; [y]=1;
0:X2=2; [x]=1; [y]=1;
0:X2=2; [x]=3; [y]=1;
0:X2=4; [x]=1; [y]=1;
0:X2=4; [x]=3; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation 2+2W+posR-pos+poW-po Always 10 0
Time 2+2W+posR-pos+poW-po 0.01
Hash=521609928e210fe75140132a20bd380f

Test 2+2W+posR-pos+poR-po Required
States 5
0:X2=1; [x]=3;
0:X2=2; [x]=1;
0:X2=2; [x]=3;
0:X2=4; [x]=1;
0:X2=4; [x]=3;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation 2+2W+posR-pos+poR-po Always 10 0
Time 2+2W+posR-pos+poR-po 0.01
Hash=577061c91921b6f0e59b258eee3444d4

Test S+posR-pos+poR-po Required
States 7
0:X2=1; 1:X1=0; [x]=3;
0:X2=1; 1:X1=2; [x]=3;
0:X2=2; 1:X1=0; [x]=1;
0:X2=2; 1:X1=0; [x]=3;
0:X2=2; 1:X1=2; [x]=1;
0:X2=2; 1:X1=2; [x]=3;
0:X2=2; 1:X1=3; [x]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posR-pos+poR-po Always 8 0
Time S+posR-pos+poR-po 0.01
Hash=33f41e231698869e18c3ef2613b85d82

Test R+poW-posR-pos+po Required
States 6
0:X4=1; 1:X3=0; [x]=1; [y]=2;
0:X4=1; 1:X3=0; [x]=1; [y]=3;
0:X4=1; 1:X3=1; [x]=1; [y]=2;
0:X4=1; 1:X3=1; [x]=1; [y]=3;
0:X4=3; 1:X3=0; [x]=1; [y]=2;
0:X4=3; 1:X3=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+poW-posR-pos+po Always 8 0
Time R+poW-posR-pos+po 0.01
Hash=5822b30ca5b89e27445639731b6b8d04

Test MP+poW-posR-pos+po Required
States 6
0:X4=1; 1:X1=0; 1:X3=0; [x]=1; [y]=2;
0:X4=1; 1:X1=0; 1:X3=1; [x]=1; [y]=2;
0:X4=1; 1:X1=1; 1:X3=0; [x]=1; [y]=2;
0:X4=1; 1:X1=1; 1:X3=1; [x]=1; [y]=2;
0:X4=1; 1:X1=2; 1:X3=0; [x]=1; [y]=2;
0:X4=1; 1:X1=2; 1:X3=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+poW-posR-pos+po Always 6 0
Time MP+poW-posR-pos+po 0.01
Hash=1e1f24b33e1a219bc08e1239be70b24f

Test 2+2W+po+poW-posR-pos Required
States 6
1:X4=1; [x]=2; [y]=1;
1:X4=1; [x]=2; [y]=2;
1:X4=1; [x]=3; [y]=1;
1:X4=1; [x]=3; [y]=2;
1:X4=3; [x]=2; [y]=1;
1:X4=3; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+poW-posR-pos Always 8 0
Time 2+2W+po+poW-posR-pos 0.01
Hash=7d51993091ec2e0fe11b3e3b86b0aab9

Test S+po+poW-posR-pos Required
States 6
1:X1=0; 1:X4=1; [x]=2; [y]=1;
1:X1=0; 1:X4=1; [x]=3; [y]=1;
1:X1=0; 1:X4=3; [x]=2; [y]=1;
1:X1=1; 1:X4=1; [x]=2; [y]=1;
1:X1=1; 1:X4=1; [x]=3; [y]=1;
1:X1=1; 1:X4=3; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+poW-posR-pos Always 8 0
Time S+po+poW-posR-pos 0.01
Hash=290cbc54ddc7c1042910361dc9036878

Test S+poW-posR-pos+po Required
States 6
0:X4=1; 1:X1=0; [x]=1; [y]=2;
0:X4=1; 1:X1=0; [x]=2; [y]=2;
0:X4=1; 1:X1=1; [x]=1; [y]=2;
0:X4=1; 1:X1=1; [x]=2; [y]=2;
0:X4=1; 1:X1=2; [x]=1; [y]=2;
0:X4=1; 1:X1=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation S+poW-posR-pos+po Always 6 0
Time S+poW-posR-pos+po 0.01
Hash=e131a7fff17d5a40ae76c110e18c83e1

Test R+posR-posR-po+po Required
States 4
0:X2=1; 0:X3=1; 1:X3=0; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X3=0; [x]=1; [y]=2;
0:X2=1; 0:X3=1; 1:X3=1; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X3=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation R+posR-posR-po+po Always 4 0
Time R+posR-posR-po+po 0.01
Hash=7e415b12533f52ee0b924b251de4be97

Test LB+po+poW-posR-pos Required
States 6
0:X1=0; 1:X1=0; 1:X4=1; [x]=2; [y]=1;
0:X1=0; 1:X1=1; 1:X4=1; [x]=2; [y]=1;
0:X1=1; 1:X1=0; 1:X4=1; [x]=2; [y]=1;
0:X1=1; 1:X1=1; 1:X4=1; [x]=2; [y]=1;
0:X1=2; 1:X1=0; 1:X4=1; [x]=2; [y]=1;
0:X1=2; 1:X1=1; 1:X4=1; [x]=2; [y]=1;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation LB+po+poW-posR-pos Always 6 0
Time LB+po+poW-posR-pos 0.01
Hash=587b0470c2a77a16220c4105fb9d6b95

Test SB+po+posR-posR-po Required
States 4
0:X3=0; 1:X2=1; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
0:X3=0; 1:X2=1; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X2=1; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
0:X3=1; 1:X2=1; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation SB+po+posR-posR-po Always 4 0
Time SB+po+posR-posR-po 0.01
Hash=62e09d4ab58d9aed7f0e41e8ef2849ba

Test MP+posR-posR-po+po Required
States 4
0:X2=1; 0:X3=1; 1:X1=0; 1:X3=0; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X1=0; 1:X3=1; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X1=1; 1:X3=0; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X1=1; 1:X3=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation MP+posR-posR-po+po Always 4 0
Time MP+posR-posR-po+po 0.01
Hash=d97f625a8afccf1797461ce8ce59d017

Test SB+posR-pos+poW-po Required
States 5
0:X2=1; 0:X3=1; 1:X4=1; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X4=2; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X4=2; [x]=2; [y]=1;
0:X2=1; 0:X3=2; 1:X4=2; [x]=2; [y]=1;
0:X2=2; 0:X3=2; 1:X4=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 5 Negative: 0
Condition forall (true)
Observation SB+posR-pos+poW-po Always 5 0
Time SB+posR-pos+poW-po 0.01
Hash=7e51eeb2e450439374ae776e96760961

Test R+po+posR-posR-po Required
States 8
1:X2=1; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X2=1; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X2=2; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X2=2; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X2=2; 1:X3=2; 1:X5=0; [x]=1; [y]=1;
1:X2=2; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
1:X2=2; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
1:X2=2; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+posR-posR-po Always 8 0
Time R+po+posR-posR-po 0.01
Hash=a4f58611ba7ce912c63092e38007ad88

Test 2+2W+po+posR-posR-po Required
States 8
1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X2=1; 1:X3=1; [x]=2; [y]=1;
1:X2=2; 1:X3=1; [x]=1; [y]=1;
1:X2=2; 1:X3=1; [x]=2; [y]=1;
1:X2=2; 1:X3=2; [x]=1; [y]=1;
1:X2=2; 1:X3=2; [x]=1; [y]=2;
1:X2=2; 1:X3=2; [x]=2; [y]=1;
1:X2=2; 1:X3=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+posR-posR-po Always 8 0
Time 2+2W+po+posR-posR-po 0.01
Hash=3406f57e32c80bef3de4e2a931f40bdd

Test SB+posR-pos+poR-po Required
States 5
0:X2=1; 0:X3=1; 1:X4=1; [x]=1;
0:X2=1; 0:X3=1; 1:X4=2; [x]=1;
0:X2=1; 0:X3=1; 1:X4=2; [x]=2;
0:X2=1; 0:X3=2; 1:X4=2; [x]=2;
0:X2=2; 0:X3=2; 1:X4=2; [x]=2;
Ok
Witnesses
Positive: 5 Negative: 0
Condition forall (true)
Observation SB+posR-pos+poR-po Always 5 0
Time SB+posR-pos+poR-po 0.01
Hash=a32b2c7d5bb9010f1b4b795d0670a5a4

Test R+poW-po+posR-pos Required
States 7
1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X2=2; 1:X3=1; [x]=1; [y]=1;
1:X2=2; 1:X3=2; [x]=1; [y]=1;
1:X2=2; 1:X3=2; [x]=2; [y]=1;
1:X2=2; 1:X3=3; [x]=1; [y]=1;
1:X2=3; 1:X3=1; [x]=1; [y]=1;
1:X2=3; 1:X3=3; [x]=1; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+poW-po+posR-pos Always 10 0
Time R+poW-po+posR-pos 0.01
Hash=12df19f737405b365ced86c1176da046

Test S+posR-posR-po+po Required
States 8
0:X2=1; 0:X3=1; 1:X1=0; [x]=1; [y]=1;
0:X2=1; 0:X3=1; 1:X1=1; [x]=1; [y]=1;
0:X2=2; 0:X3=1; 1:X1=0; [x]=1; [y]=1;
0:X2=2; 0:X3=1; 1:X1=1; [x]=1; [y]=1;
0:X2=2; 0:X3=2; 1:X1=0; [x]=1; [y]=1;
0:X2=2; 0:X3=2; 1:X1=0; [x]=2; [y]=1;
0:X2=2; 0:X3=2; 1:X1=1; [x]=1; [y]=1;
0:X2=2; 0:X3=2; 1:X1=1; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+posR-posR-po+po Always 8 0
Time S+posR-posR-po+po 0.01
Hash=2a5da03e9f6902c8bad9f5e2b09f5ff4

Test SB+po+poW-posR-pos Required
States 8
0:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
0:X3=0; 1:X4=1; 1:X5=1; [x]=2; [y]=1;
0:X3=0; 1:X4=1; 1:X5=2; [x]=2; [y]=1;
0:X3=0; 1:X4=2; 1:X5=2; [x]=2; [y]=1;
0:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X4=1; 1:X5=1; [x]=2; [y]=1;
0:X3=1; 1:X4=1; 1:X5=2; [x]=2; [y]=1;
0:X3=1; 1:X4=2; 1:X5=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation SB+po+poW-posR-pos Always 8 0
Time SB+po+poW-posR-pos 0.01
Hash=ec3f64864ea1f6e1d161aef59db083c9

Test R+po+poW-posR-pos Required
States 8
1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X4=1; 1:X5=1; [x]=1; [y]=2;
1:X4=1; 1:X5=1; [x]=2; [y]=1;
1:X4=1; 1:X5=1; [x]=2; [y]=2;
1:X4=1; 1:X5=2; [x]=2; [y]=1;
1:X4=1; 1:X5=2; [x]=2; [y]=2;
1:X4=2; 1:X5=2; [x]=2; [y]=1;
1:X4=2; 1:X5=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+poW-posR-pos Always 8 0
Time R+po+poW-posR-pos 0.01
Hash=b7b2523997211eaedeeb49eaee646fe6

Test MP+po+poW-posR-pos Required
States 8
1:X1=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X4=1; 1:X5=1; [x]=2; [y]=1;
1:X1=0; 1:X4=1; 1:X5=2; [x]=2; [y]=1;
1:X1=0; 1:X4=2; 1:X5=2; [x]=2; [y]=1;
1:X1=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X4=1; 1:X5=1; [x]=2; [y]=1;
1:X1=1; 1:X4=1; 1:X5=2; [x]=2; [y]=1;
1:X1=1; 1:X4=2; 1:X5=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+poW-posR-pos Always 8 0
Time MP+po+poW-posR-pos 0.01
Hash=0916067f7eb695a41b015b4c0074f89c

Test S+po+posW-posW-po Required
States 6
1:X1=0; [x]=1; [y]=1;
1:X1=0; [x]=1; [y]=3;
1:X1=0; [x]=2; [y]=1;
1:X1=0; [x]=2; [y]=3;
1:X1=1; [x]=1; [y]=3;
1:X1=1; [x]=2; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+posW-posW-po Always 8 0
Time S+po+posW-posW-po 0.01
Hash=238d17cc288da98011d04b8acf73cec1

Test MP+po+posW-posW-po Required
States 6
1:X1=0; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X5=0; [x]=1; [y]=3;
1:X1=0; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X5=1; [x]=1; [y]=3;
1:X1=1; 1:X5=0; [x]=1; [y]=3;
1:X1=1; 1:X5=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+posW-posW-po Always 8 0
Time MP+po+posW-posW-po 0.01
Hash=48a0b4f142008bd7170ab5d19412524c

Test R+poR-po+posR-pos Required
States 7
1:X2=1; 1:X3=1; [x]=1;
1:X2=2; 1:X3=1; [x]=1;
1:X2=2; 1:X3=2; [x]=1;
1:X2=2; 1:X3=2; [x]=2;
1:X2=2; 1:X3=3; [x]=1;
1:X2=3; 1:X3=1; [x]=1;
1:X2=3; 1:X3=3; [x]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation R+poR-po+posR-pos Always 10 0
Time R+poR-po+posR-pos 0.01
Hash=84eeadf2e1eeae36851925c5382cae75

Test S+poR-po+posW-pos Required
States 5
1:X1=0; [x]=1;
1:X1=0; [x]=3;
1:X1=1; [x]=3;
1:X1=4; [x]=1;
1:X1=4; [x]=3;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+poR-po+posW-pos Always 10 0
Time S+poR-po+posW-pos 0.01
Hash=eec64ee248050789c2f75d803d78589d

Test LB+po+posW-posW-po Required
States 6
0:X1=0; 1:X1=0; [x]=1; [y]=1;
0:X1=0; 1:X1=0; [x]=1; [y]=3;
0:X1=0; 1:X1=1; [x]=1; [y]=3;
0:X1=1; 1:X1=0; [x]=1; [y]=1;
0:X1=1; 1:X1=0; [x]=1; [y]=3;
0:X1=1; 1:X1=1; [x]=1; [y]=3;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation LB+po+posW-posW-po Always 8 0
Time LB+po+posW-posW-po 0.01
Hash=af1c495f8ab6814e3309645844880b96

Test S+poW-po+posW-pos Required
States 5
1:X1=0; [x]=1; [y]=1;
1:X1=0; [x]=3; [y]=1;
1:X1=1; [x]=3; [y]=1;
1:X1=4; [x]=1; [y]=1;
1:X1=4; [x]=3; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+poW-po+posW-pos Always 10 0
Time S+poW-po+posW-pos 0.01
Hash=cf34aa57e60fd1119f570126f79bb5eb

Test LB+posW-pos+poW-po Required
States 6
0:X1=0; 1:X1=0; [x]=1; [y]=1;
0:X1=0; 1:X1=0; [x]=3; [y]=1;
0:X1=0; 1:X1=2; [x]=1; [y]=1;
0:X1=0; 1:X1=2; [x]=3; [y]=1;
0:X1=0; 1:X1=3; [x]=1; [y]=1;
0:X1=1; 1:X1=0; [x]=3; [y]=1;
Ok
Witnesses
Positive: 7 Negative: 0
Condition forall (true)
Observation LB+posW-pos+poW-po Always 7 0
Time LB+posW-pos+poW-po 0.01
Hash=b0c03c955bb83b579b45dee95f907617

Test MP+poR-posW-pos+po Required
States 6
0:X3=0; 1:X1=0; 1:X3=0; [x]=1; [y]=2;
0:X3=0; 1:X1=0; 1:X3=1; [x]=1; [y]=2;
0:X3=0; 1:X1=1; 1:X3=0; [x]=1; [y]=2;
0:X3=0; 1:X1=1; 1:X3=1; [x]=1; [y]=2;
0:X3=0; 1:X1=2; 1:X3=0; [x]=1; [y]=2;
0:X3=0; 1:X1=2; 1:X3=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation MP+poR-posW-pos+po Always 6 0
Time MP+poR-posW-pos+po 0.01
Hash=b7d84856993d6e99f5e6e3216c1f9b83

Test LB+posW-pos+poR-po Required
States 6
0:X1=0; 1:X1=0; [x]=1;
0:X1=0; 1:X1=0; [x]=3;
0:X1=0; 1:X1=2; [x]=1;
0:X1=0; 1:X1=2; [x]=3;
0:X1=0; 1:X1=3; [x]=1;
0:X1=1; 1:X1=0; [x]=3;
Ok
Witnesses
Positive: 7 Negative: 0
Condition forall (true)
Observation LB+posW-pos+poR-po Always 7 0
Time LB+posW-pos+poR-po 0.01
Hash=1e0d8a2ad388a188f3d0afb2044f3381

Test R+poR-posW-pos+po Required
States 6
0:X3=0; 1:X3=0; [x]=1; [y]=2;
0:X3=0; 1:X3=0; [x]=1; [y]=3;
0:X3=0; 1:X3=1; [x]=1; [y]=2;
0:X3=0; 1:X3=1; [x]=1; [y]=3;
0:X3=3; 1:X3=0; [x]=1; [y]=2;
0:X3=3; 1:X3=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+poR-posW-pos+po Always 8 0
Time R+poR-posW-pos+po 0.01
Hash=6f9afadfdafac280527e1148db967645

Test 2+2W+po+poR-posW-pos Required
States 6
1:X3=0; [x]=2; [y]=1;
1:X3=0; [x]=2; [y]=2;
1:X3=0; [x]=3; [y]=1;
1:X3=0; [x]=3; [y]=2;
1:X3=3; [x]=2; [y]=1;
1:X3=3; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+poR-posW-pos Always 8 0
Time 2+2W+po+poR-posW-pos 0.01
Hash=c31e4aceda12efcf685e1489ae2e7934

Test S+poR-posW-pos+po Required
States 6
0:X3=0; 1:X1=0; [x]=1; [y]=2;
0:X3=0; 1:X1=0; [x]=2; [y]=2;
0:X3=0; 1:X1=1; [x]=1; [y]=2;
0:X3=0; 1:X1=1; [x]=2; [y]=2;
0:X3=0; 1:X1=2; [x]=1; [y]=2;
0:X3=0; 1:X1=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation S+poR-posW-pos+po Always 6 0
Time S+poR-posW-pos+po 0.01
Hash=0fda93d0095e80b7d685737c34657b63

Test MP+po+posW-posR-po Required
States 8
1:X1=0; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X3=2; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
1:X1=0; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
1:X1=1; 1:X3=2; 1:X5=0; [x]=1; [y]=2;
1:X1=1; 1:X3=2; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+posW-posR-po Always 8 0
Time MP+po+posW-posR-po 0.01
Hash=31b51d242e0e7c5db8763414e7fd078e

Test S+po+poR-posW-pos Required
States 6
1:X1=0; 1:X3=0; [x]=2; [y]=1;
1:X1=0; 1:X3=0; [x]=3; [y]=1;
1:X1=0; 1:X3=3; [x]=2; [y]=1;
1:X1=1; 1:X3=0; [x]=2; [y]=1;
1:X1=1; 1:X3=0; [x]=3; [y]=1;
1:X1=1; 1:X3=3; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+poR-posW-pos Always 8 0
Time S+po+poR-posW-pos 0.01
Hash=fc93ec19accfa65dc818418647526d16

Test LB+po+poR-posW-pos Required
States 6
0:X1=0; 1:X1=0; 1:X3=0; [x]=2; [y]=1;
0:X1=0; 1:X1=1; 1:X3=0; [x]=2; [y]=1;
0:X1=1; 1:X1=0; 1:X3=0; [x]=2; [y]=1;
0:X1=1; 1:X1=1; 1:X3=0; [x]=2; [y]=1;
0:X1=2; 1:X1=0; 1:X3=0; [x]=2; [y]=1;
0:X1=2; 1:X1=1; 1:X3=0; [x]=2; [y]=1;
Ok
Witnesses
Positive: 6 Negative: 0
Condition forall (true)
Observation LB+po+poR-posW-pos Always 6 0
Time LB+po+poR-posW-pos 0.01
Hash=71951b48e7a8fab26c841ed7c993cc2d

Test MP+poW-po+posW-pos Required
States 8
1:X1=0; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X3=2; [x]=1; [y]=1;
1:X1=0; 1:X3=2; [x]=2; [y]=1;
1:X1=0; 1:X3=3; [x]=1; [y]=1;
1:X1=1; 1:X3=2; [x]=2; [y]=1;
1:X1=3; 1:X3=1; [x]=1; [y]=1;
1:X1=3; 1:X3=2; [x]=1; [y]=1;
1:X1=3; 1:X3=2; [x]=2; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+poW-po+posW-pos Always 10 0
Time MP+poW-po+posW-pos 0.01
Hash=4575e37e84704c42b181a6e5c1a4671d

Test S+po+posW-posR-po Required
States 8
1:X1=0; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X3=1; [x]=2; [y]=1;
1:X1=0; 1:X3=2; [x]=1; [y]=1;
1:X1=0; 1:X3=2; [x]=1; [y]=2;
1:X1=0; 1:X3=2; [x]=2; [y]=1;
1:X1=0; 1:X3=2; [x]=2; [y]=2;
1:X1=1; 1:X3=2; [x]=1; [y]=2;
1:X1=1; 1:X3=2; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+posW-posR-po Always 8 0
Time S+po+posW-posR-po 0.01
Hash=07fd9f72259065e659aae0e2bffcedd2

Test LB+po+posW-posR-po Required
States 8
0:X1=0; 1:X1=0; 1:X3=1; [x]=1; [y]=1;
0:X1=0; 1:X1=0; 1:X3=2; [x]=1; [y]=1;
0:X1=0; 1:X1=0; 1:X3=2; [x]=1; [y]=2;
0:X1=0; 1:X1=1; 1:X3=2; [x]=1; [y]=2;
0:X1=1; 1:X1=0; 1:X3=1; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X3=2; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X3=2; [x]=1; [y]=2;
0:X1=1; 1:X1=1; 1:X3=2; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation LB+po+posW-posR-po Always 8 0
Time LB+po+posW-posR-po 0.01
Hash=3425f0095a5a5cefc660ea6d88e86dda

Test MP+poR-po+posW-pos Required
States 8
1:X1=0; 1:X3=1; [x]=1;
1:X1=0; 1:X3=2; [x]=1;
1:X1=0; 1:X3=2; [x]=2;
1:X1=0; 1:X3=3; [x]=1;
1:X1=1; 1:X3=2; [x]=2;
1:X1=3; 1:X3=1; [x]=1;
1:X1=3; 1:X3=2; [x]=1;
1:X1=3; 1:X3=2; [x]=2;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+poR-po+posW-pos Always 10 0
Time MP+poR-po+posW-pos 0.01
Hash=6e22c29065239be851d95575c2bff8c7

Test SB+po+poR-posW-pos Required
States 8
0:X3=0; 1:X3=0; 1:X5=1; [x]=1; [y]=1;
0:X3=0; 1:X3=0; 1:X5=1; [x]=2; [y]=1;
0:X3=0; 1:X3=0; 1:X5=2; [x]=2; [y]=1;
0:X3=0; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X3=0; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X3=0; 1:X5=1; [x]=2; [y]=1;
0:X3=1; 1:X3=0; 1:X5=2; [x]=2; [y]=1;
0:X3=1; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation SB+po+poR-posW-pos Always 8 0
Time SB+po+poR-posW-pos 0.01
Hash=9eb57686cfcc86f189481ed03e674738

Test MP+po+poR-posW-pos Required
States 8
1:X1=0; 1:X3=0; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X3=0; 1:X5=1; [x]=2; [y]=1;
1:X1=0; 1:X3=0; 1:X5=2; [x]=2; [y]=1;
1:X1=0; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X5=1; [x]=2; [y]=1;
1:X1=1; 1:X3=0; 1:X5=2; [x]=2; [y]=1;
1:X1=1; 1:X3=2; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+poR-posW-pos Always 8 0
Time MP+po+poR-posW-pos 0.01
Hash=728d9b691307b32d35704887c1c6b9aa

Test R+po+poR-posW-pos Required
States 8
1:X3=0; 1:X5=1; [x]=1; [y]=1;
1:X3=0; 1:X5=1; [x]=1; [y]=2;
1:X3=0; 1:X5=1; [x]=2; [y]=1;
1:X3=0; 1:X5=1; [x]=2; [y]=2;
1:X3=0; 1:X5=2; [x]=2; [y]=1;
1:X3=0; 1:X5=2; [x]=2; [y]=2;
1:X3=2; 1:X5=1; [x]=1; [y]=1;
1:X3=2; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+poR-posW-pos Always 8 0
Time R+po+poR-posW-pos 0.01
Hash=cf710b0297885caa713e952b96f7d068

Test MP+po+posR-posW-po Required
States 8
1:X1=0; 1:X2=0; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X5=0; [x]=1; [y]=2;
1:X1=0; 1:X2=0; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X5=1; [x]=1; [y]=2;
1:X1=0; 1:X2=1; 1:X5=0; [x]=1; [y]=2;
1:X1=0; 1:X2=1; 1:X5=1; [x]=1; [y]=2;
1:X1=1; 1:X2=1; 1:X5=0; [x]=1; [y]=2;
1:X1=1; 1:X2=1; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+posR-posW-po Always 8 0
Time MP+po+posR-posW-po 0.01
Hash=ce2d49107a6e147a5c84a1a977771439

Test S+po+posR-posW-po Required
States 8
1:X1=0; 1:X2=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; [x]=1; [y]=2;
1:X1=0; 1:X2=0; [x]=2; [y]=1;
1:X1=0; 1:X2=0; [x]=2; [y]=2;
1:X1=0; 1:X2=1; [x]=1; [y]=2;
1:X1=0; 1:X2=1; [x]=2; [y]=2;
1:X1=1; 1:X2=1; [x]=1; [y]=2;
1:X1=1; 1:X2=1; [x]=2; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+posR-posW-po Always 8 0
Time S+po+posR-posW-po 0.01
Hash=d3c35b08e5ed7ec185bad444ab1cc98f

Test S+poR-po+posR-pos Required
States 9
1:X1=0; 1:X2=0; [x]=1;
1:X1=0; 1:X2=0; [x]=2;
1:X1=0; 1:X2=1; [x]=2;
1:X1=0; 1:X2=3; [x]=1;
1:X1=0; 1:X2=3; [x]=2;
1:X1=1; 1:X2=1; [x]=2;
1:X1=3; 1:X2=1; [x]=2;
1:X1=3; 1:X2=3; [x]=1;
1:X1=3; 1:X2=3; [x]=2;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+poR-po+posR-pos Always 10 0
Time S+poR-po+posR-pos 0.01
Hash=d561eb8063702151d4293642fdcdda56

Test LB+po+posR-posW-po Required
States 8
0:X1=0; 1:X1=0; 1:X2=0; [x]=1; [y]=1;
0:X1=0; 1:X1=0; 1:X2=0; [x]=1; [y]=2;
0:X1=0; 1:X1=0; 1:X2=1; [x]=1; [y]=2;
0:X1=0; 1:X1=1; 1:X2=1; [x]=1; [y]=2;
0:X1=1; 1:X1=0; 1:X2=0; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X2=0; [x]=1; [y]=2;
0:X1=1; 1:X1=0; 1:X2=1; [x]=1; [y]=2;
0:X1=1; 1:X1=1; 1:X2=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation LB+po+posR-posW-po Always 8 0
Time LB+po+posR-posW-po 0.01
Hash=d372982fa0aedca1e5b3d86c71dc3a2e

Test LB+posR-pos+poR-po Required
States 5
0:X1=0; 0:X2=0; 1:X1=0; [x]=1;
0:X1=0; 0:X2=0; 1:X1=0; [x]=2;
0:X1=0; 0:X2=0; 1:X1=2; [x]=1;
0:X1=0; 0:X2=1; 1:X1=0; [x]=2;
0:X1=1; 0:X2=1; 1:X1=0; [x]=2;
Ok
Witnesses
Positive: 5 Negative: 0
Condition forall (true)
Observation LB+posR-pos+poR-po Always 5 0
Time LB+posR-pos+poR-po 0.01
Hash=299af90f9bfd918521d2ea2c350adae3

Test LB+posR-pos+poW-po Required
States 5
0:X1=0; 0:X2=0; 1:X1=0; [x]=1; [y]=1;
0:X1=0; 0:X2=0; 1:X1=0; [x]=2; [y]=1;
0:X1=0; 0:X2=0; 1:X1=2; [x]=1; [y]=1;
0:X1=0; 0:X2=1; 1:X1=0; [x]=2; [y]=1;
0:X1=1; 0:X2=1; 1:X1=0; [x]=2; [y]=1;
Ok
Witnesses
Positive: 5 Negative: 0
Condition forall (true)
Observation LB+posR-pos+poW-po Always 5 0
Time LB+posR-pos+poW-po 0.01
Hash=671a8e76f1f103cdd0706f9445e4d6da

Test R+poR-posR-pos+po Required
States 8
0:X3=0; 0:X4=0; 1:X3=0; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X3=0; [x]=1; [y]=2;
0:X3=0; 0:X4=0; 1:X3=1; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X3=1; [x]=1; [y]=2;
0:X3=0; 0:X4=2; 1:X3=0; [x]=1; [y]=1;
0:X3=0; 0:X4=2; 1:X3=1; [x]=1; [y]=1;
0:X3=2; 0:X4=2; 1:X3=0; [x]=1; [y]=1;
0:X3=2; 0:X4=2; 1:X3=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+poR-posR-pos+po Always 8 0
Time R+poR-posR-pos+po 0.01
Hash=6849d48b694819fa40ec389aa7092aef

Test MP+poR-posR-pos+po Required
States 4
0:X3=0; 0:X4=0; 1:X1=0; 1:X3=0; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X1=0; 1:X3=1; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X1=1; 1:X3=0; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X1=1; 1:X3=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation MP+poR-posR-pos+po Always 4 0
Time MP+poR-posR-pos+po 0.01
Hash=9c204668c80a6fba0f926a5531d2e633

Test S+poW-po+posR-pos Required
States 9
1:X1=0; 1:X2=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; [x]=2; [y]=1;
1:X1=0; 1:X2=1; [x]=2; [y]=1;
1:X1=0; 1:X2=3; [x]=1; [y]=1;
1:X1=0; 1:X2=3; [x]=2; [y]=1;
1:X1=1; 1:X2=1; [x]=2; [y]=1;
1:X1=3; 1:X2=1; [x]=2; [y]=1;
1:X1=3; 1:X2=3; [x]=1; [y]=1;
1:X1=3; 1:X2=3; [x]=2; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation S+poW-po+posR-pos Always 10 0
Time S+poW-po+posR-pos 0.01
Hash=1d8ba1df193d6e58541ee3a83862409d

Test S+poR-posR-pos+po Required
States 4
0:X3=0; 0:X4=0; 1:X1=0; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X1=0; [x]=2; [y]=1;
0:X3=0; 0:X4=0; 1:X1=1; [x]=1; [y]=1;
0:X3=0; 0:X4=0; 1:X1=1; [x]=2; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation S+poR-posR-pos+po Always 4 0
Time S+poR-posR-pos+po 0.00
Hash=87426e60ba5ce2648a5426fd08ddf151

Test MP+po+posR-posR-po Required
States 8
1:X1=0; 1:X2=0; 1:X3=0; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=0; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X2=1; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X2=1; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X2=1; 1:X3=1; 1:X5=0; [x]=1; [y]=1;
1:X1=1; 1:X2=1; 1:X3=1; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+posR-posR-po Always 8 0
Time MP+po+posR-posR-po 0.01
Hash=353ad77fa799b8dfc1e9538a27a3507b

Test 2+2W+po+poR-posR-pos Required
States 8
1:X3=0; 1:X4=0; [x]=1; [y]=1;
1:X3=0; 1:X4=0; [x]=1; [y]=2;
1:X3=0; 1:X4=0; [x]=2; [y]=1;
1:X3=0; 1:X4=0; [x]=2; [y]=2;
1:X3=0; 1:X4=2; [x]=1; [y]=1;
1:X3=0; 1:X4=2; [x]=1; [y]=2;
1:X3=2; 1:X4=2; [x]=1; [y]=1;
1:X3=2; 1:X4=2; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation 2+2W+po+poR-posR-pos Always 8 0
Time 2+2W+po+poR-posR-pos 0.01
Hash=4b1d22823324f578b5e14316166e2be8

Test S+po+poR-posR-pos Required
States 8
1:X1=0; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
1:X1=0; 1:X3=0; 1:X4=0; [x]=2; [y]=1;
1:X1=0; 1:X3=0; 1:X4=2; [x]=1; [y]=1;
1:X1=0; 1:X3=2; 1:X4=2; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X4=0; [x]=2; [y]=1;
1:X1=1; 1:X3=0; 1:X4=2; [x]=1; [y]=1;
1:X1=1; 1:X3=2; 1:X4=2; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+poR-posR-pos Always 8 0
Time S+po+poR-posR-pos 0.01
Hash=6498b450fb9f83000f4e30073da8a8d0

Test LB+po+posR-posR-po Required
States 8
0:X1=0; 1:X1=0; 1:X2=0; 1:X3=0; [x]=1; [y]=1;
0:X1=0; 1:X1=0; 1:X2=0; 1:X3=1; [x]=1; [y]=1;
0:X1=0; 1:X1=0; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
0:X1=0; 1:X1=1; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X2=0; 1:X3=0; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X2=0; 1:X3=1; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
0:X1=1; 1:X1=1; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation LB+po+posR-posR-po Always 8 0
Time LB+po+posR-posR-po 0.01
Hash=080ecfff2a3ea068f50a4b032be60d62

Test S+po+posR-posR-po Required
States 8
1:X1=0; 1:X2=0; 1:X3=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=0; [x]=2; [y]=1;
1:X1=0; 1:X2=0; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=1; [x]=2; [y]=1;
1:X1=0; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X2=1; 1:X3=1; [x]=2; [y]=1;
1:X1=1; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X1=1; 1:X2=1; 1:X3=1; [x]=2; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation S+po+posR-posR-po Always 8 0
Time S+po+posR-posR-po 0.01
Hash=c7f92ad9ffc4705dd79598b9d1d433fd

Test LB+po+poR-posR-pos Required
States 4
0:X1=0; 1:X1=0; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
0:X1=0; 1:X1=1; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
0:X1=1; 1:X1=0; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
0:X1=1; 1:X1=1; 1:X3=0; 1:X4=0; [x]=1; [y]=1;
Ok
Witnesses
Positive: 4 Negative: 0
Condition forall (true)
Observation LB+po+poR-posR-pos Always 4 0
Time LB+po+poR-posR-pos 0.01
Hash=3eef66ef7d22b758e16baf715b6160c0

Test R+po+poR-posR-pos Required
States 8
1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=1;
1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=2;
1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=1;
1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=2;
1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=2;
1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=2;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation R+po+poR-posR-pos Always 8 0
Time R+po+poR-posR-pos 0.00
Hash=7fd120601b9041d99279a07c8bcb5369

Test MP+poW-po+posR-pos Required
States 10
1:X1=0; 1:X2=0; 1:X3=0; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X2=0; 1:X3=2; [x]=1; [y]=1;
1:X1=0; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X2=2; 1:X3=1; [x]=1; [y]=1;
1:X1=0; 1:X2=2; 1:X3=2; [x]=1; [y]=1;
1:X1=1; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X1=2; 1:X2=1; 1:X3=1; [x]=1; [y]=1;
1:X1=2; 1:X2=2; 1:X3=1; [x]=1; [y]=1;
1:X1=2; 1:X2=2; 1:X3=2; [x]=1; [y]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+poW-po+posR-pos Always 10 0
Time MP+poW-po+posR-pos 0.01
Hash=d7ca942ece611a6500f610ab5b581a12

Test MP+poR-po+posR-pos Required
States 10
1:X1=0; 1:X2=0; 1:X3=0; [x]=1;
1:X1=0; 1:X2=0; 1:X3=1; [x]=1;
1:X1=0; 1:X2=0; 1:X3=2; [x]=1;
1:X1=0; 1:X2=1; 1:X3=1; [x]=1;
1:X1=0; 1:X2=2; 1:X3=1; [x]=1;
1:X1=0; 1:X2=2; 1:X3=2; [x]=1;
1:X1=1; 1:X2=1; 1:X3=1; [x]=1;
1:X1=2; 1:X2=1; 1:X3=1; [x]=1;
1:X1=2; 1:X2=2; 1:X3=1; [x]=1;
1:X1=2; 1:X2=2; 1:X3=2; [x]=1;
Ok
Witnesses
Positive: 10 Negative: 0
Condition forall (true)
Observation MP+poR-po+posR-pos Always 10 0
Time MP+poR-po+posR-pos 0.01
Hash=ffa0a1fb99f20eb22b328140052785cd

Test MP+po+poR-posR-pos Required
States 8
1:X1=0; 1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=1;
1:X1=0; 1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X1=0; 1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
1:X1=1; 1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation MP+po+poR-posR-pos Always 8 0
Time MP+po+poR-posR-pos 0.01
Hash=39bc50c199246952c568ede0cf44db9d

Test SB+po+poR-posR-pos Required
States 8
0:X3=0; 1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=1;
0:X3=0; 1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=1;
0:X3=0; 1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
0:X3=0; 1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X3=0; 1:X4=0; 1:X5=0; [x]=1; [y]=1;
0:X3=1; 1:X3=0; 1:X4=0; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X3=0; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
0:X3=1; 1:X3=1; 1:X4=1; 1:X5=1; [x]=1; [y]=1;
Ok
Witnesses
Positive: 8 Negative: 0
Condition forall (true)
Observation SB+po+poR-posR-pos Always 8 0
Time SB+po+poR-posR-pos 0.01
Hash=d5e799a0012696e2010676c5a7b94594