// theorem 1 (mutual exclusion)
!((p1>9) & (p2>9)) & !((p1>9) & (p3>9)) & !((p2>9) & (p3>9))

// theorem 2 (liveness - if process 1 tries then eventually it enters the critical section)
(p1=1) => P>=1 [ true U (p1=10) ]

// lemma c (if the crical section is occupied then eventually it becomes clear)
(p1>9) | (p2>9) | (p3>9) => P>=1 [ true U (p1<10) & (p2<10) & (p3<10) ]

// lemma d (if a process is between 4 and 13 (in our version) then eventually some process gets to 14)
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) => P>=1 [ true U (p1=14) | (p2=14) | (p3=14) ]