###keys
glock pc[p1] pc[p2] pc[p3] next[p1] next[p2] next[p3] lock[p1] lock[p2] lock[p3] pred[p1] pred[p2] pred[p3]

###textDisplay

###states
(glock: nop (pc[p1]: rs) (pc[p2]: rs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) || 
(glock: nop (pc[p1]: rs) (pc[p2]: l1) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) || 
(glock: nop (pc[p1]: l1) (pc[p2]: l1) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) || 
(glock: nop (pc[p1]: l1) (pc[p2]: l1) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) ||
(glock: nop (pc[p1]: l1) (pc[p2]: l1) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) ||
(glock: p3 (pc[p1]: l1) (pc[p2]: l1) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l1) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l2) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: nop) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l3) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: nop) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l4) (pc[p3]: cs) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l4) (pc[p3]: l7) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l4) (pc[p3]: l7) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l4) (pc[p3]: l8) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l5) (pc[p3]: l8) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l6) (pc[p3]: l8) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l6) (pc[p3]: l10) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l10) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: cs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l7) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l4) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l4) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l1) (pc[p3]: l4) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: l4) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l6) (pc[p2]: l3) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l6) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: cs) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l7) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l11) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l4) (pc[p3]: cs) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l5) (pc[p3]: cs) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l5) (pc[p3]: l7) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: rs) (pc[p2]: l5) (pc[p3]: l7) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: rs) (pc[p2]: l5) (pc[p3]: l8) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: rs) (pc[p2]: l5) (pc[p3]: l10) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l5) (pc[p3]: l10) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l6) (pc[p3]: l10) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l6) (pc[p3]: l11) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l6) (pc[p3]: l12) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l6) (pc[p3]: l12) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: cs) (pc[p3]: l12) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: cs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: cs) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: cs) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l7) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l8) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l8) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l8) (pc[p3]: l4) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l8) (pc[p3]: l4) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l8) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l8) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l10) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l10) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l12) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l7) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l1) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: l11) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: l12) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l2) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: l2) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: l2) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l8) (pc[p2]: l2) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l8) (pc[p2]: l3) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l10) (pc[p2]: l3) (pc[p3]: rs) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l10) (pc[p2]: l3) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l10) (pc[p2]: l4) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l10) (pc[p2]: l5) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p2 (pc[p1]: l10) (pc[p2]: l5) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l5) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l6) (pc[p3]: l3) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l6) (pc[p3]: l3) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l6) (pc[p3]: l4) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l6) (pc[p3]: l5) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l5) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: rs) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: rs) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l1) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l7) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l12) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l12) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l12) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: rs) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l7) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: rs) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: rs) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: rs) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l8) (pc[p2]: rs) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l8) (pc[p2]: rs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: l9) (pc[p2]: rs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: rs) (pc[p2]: rs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: rs) (pc[p2]: l1) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: rs) (pc[p2]: l1) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: rs) (pc[p2]: l2) (pc[p3]: l1) (next[p1]: nop) (next[p2]: nop) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: rs) (pc[p2]: l2) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: nop (pc[p1]: l1) (pc[p2]: l2) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l1) (pc[p2]: l2) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l3) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l1) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l2) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l5) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l6) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l7) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l6) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: cs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l7) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l7) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p1) (next[p3]: p2) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: l12) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: rs) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: rs) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: l1) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p1) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: l2) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p3) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l7) (pc[p2]: l3) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l8) (pc[p2]: l3) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: nop) ||
(glock: p2 (pc[p1]: l8) (pc[p2]: l4) (pc[p3]: l2) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: nop) ||
(glock: p3 (pc[p1]: l8) (pc[p2]: l4) (pc[p3]: l3) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l8) (pc[p2]: l4) (pc[p3]: l4) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l8) (pc[p2]: l4) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l4) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l5) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l6) (pc[p3]: l5) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l6) (pc[p3]: l5) (next[p1]: p2) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: rs) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l1) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: p2) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l2) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p2) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: l6) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l3) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l4) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: cs) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l7) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l5) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: true) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l11) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l6) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: cs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l7) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l11) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: true) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l6) (pc[p2]: l12) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: l12) (pc[p3]: l12) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: l12) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: rs) (pc[p3]: rs) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: cs) (pc[p2]: rs) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: rs) (pc[p3]: l1) (next[p1]: nop) (next[p2]: p3) (next[p3]: p1) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l7) (pc[p2]: rs) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p1 (pc[p1]: l8) (pc[p2]: rs) (pc[p3]: l2) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p2) ||
(glock: p3 (pc[p1]: l8) (pc[p2]: rs) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: rs) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l1) (pc[p3]: l3) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l1) (pc[p3]: l4) (next[p1]: nop) (next[p2]: p3) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l2) (pc[p3]: l4) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l2) (pc[p3]: l5) (next[p1]: nop) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l10) (pc[p2]: l2) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p3 (pc[p1]: l11) (pc[p2]: l2) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p1) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l11) (pc[p2]: l3) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: true) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l3) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l4) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l5) (pc[p3]: l6) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l5) (pc[p3]: cs) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l5) (pc[p3]: l7) (next[p1]: p3) (next[p2]: nop) (next[p3]: nop) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l7) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l11) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: true) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: l12) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) ||
(glock: p2 (pc[p1]: l12) (pc[p2]: l6) (pc[p3]: rs) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1) || 
glock: p2 (pc[p1]: rs) (pc[p2]: l6) (pc[p3]: rs) (next[p1]: p3) (next[p2]: nop) (next[p3]: p2) (lock[p1]: false) (lock[p2]: false) (lock[p3]: false) (pred[p1]: p3) (pred[p2]: p3) pred[p3]: p1