never { accept_init: s0_init: if :: (p) -> goto s1 :: !(p) -> goto s0_init fi; s1: if :: (p) && (q) && (r) -> goto accept_s2 :: (p) && (q) && !(r) -> goto s3 :: !(p) && (q) && (r) -> goto s0_init :: !(p) && (q) && !(r) -> goto s5 :: !(p) && !(q) -> goto accept_s6 :: (p) && !(q) -> goto accept_s4 fi; s3: if :: !(p) && (q) && (r) -> goto s0_init :: !(p) && (q) && !(r) -> goto s5 :: !(p) && !(q) && (r) -> goto accept_s6 :: !(p) && !(q) && !(r) -> goto s10 :: (p) && (q) && (r) -> goto accept_s2 :: (p) && (q) && !(r) -> goto s3 :: (p) && !(q) && (r) -> goto accept_s4 :: (p) && !(q) && !(r) -> goto s9 fi; s5: if :: (p) && !(r) -> goto s3 :: !(p) && !(r) -> goto s5 :: !(p) && (r) -> goto s0_init :: (p) && (r) -> goto accept_s2 fi; s7: if :: (p) && !(q) && (r) -> goto accept_s4 :: (p) && !(q) && !(r) -> goto s9 :: (p) && (q) && (r) -> goto accept_s2 :: (p) && (q) && !(r) -> goto s3 :: !(p) && !(q) && (r) -> goto accept_s6 :: !(p) && !(q) && !(r) -> goto s10 :: !(p) && (q) && (r) -> goto s0_init :: !(p) && (q) && !(r) -> goto s5 fi; s8: if :: (p) && !(q) -> goto accept_s4 :: !(p) && !(q) -> goto accept_s6 :: (p) && (q) && !(r) -> goto s3 :: (p) && (q) && (r) -> goto accept_s2 :: !(p) && (q) && !(r) -> goto s5 :: !(p) && (q) && (r) -> goto s0_init fi; s9: if :: (p) && !(q) && !(r) -> goto s9 :: (p) && !(q) && (r) -> goto accept_s4 :: (p) && (q) && !(r) -> goto s3 :: (p) && (q) && (r) -> goto accept_s2 :: !(p) && !(q) && !(r) -> goto s10 :: !(p) && !(q) && (r) -> goto accept_s6 :: !(p) && (q) && !(r) -> goto s5 :: !(p) && (q) && (r) -> goto s0_init fi; s10: if :: (p) && !(q) && (r) -> goto accept_s4 :: (p) && !(q) && !(r) -> goto s9 :: (p) && (q) && (r) -> goto accept_s2 :: (p) && (q) && !(r) -> goto s3 :: !(p) && !(q) && (r) -> goto accept_s6 :: !(p) && !(q) && !(r) -> goto s10 :: !(p) && (q) && (r) -> goto s0_init :: !(p) && (q) && !(r) -> goto s5 fi; accept_s2: if :: !(p) && (q) && !(r) -> goto s5 :: !(p) && (q) && (r) -> goto s0_init :: (p) && (q) && !(r) -> goto s7 :: (p) && (q) && (r) -> goto s1 :: (p) && !(q) -> goto s8 :: !(p) && !(q) -> goto accept_s6 fi; accept_s4: if :: !(p) && (q) && (r) -> goto s0_init :: !(p) && (q) && !(r) -> goto s5 :: (p) && (q) && (r) -> goto s1 :: (p) && (q) && !(r) -> goto s7 :: (p) && !(q) -> goto s8 :: !(p) && !(q) -> goto accept_s6 fi; accept_s6: if :: (p) && (q) && !(r) -> goto s7 :: (p) && (q) && (r) -> goto s1 :: !(p) && !(q) -> goto accept_s6 :: (p) && !(q) -> goto s8 :: !(p) && (q) && !(r) -> goto s5 :: !(p) && (q) && (r) -> goto s0_init fi; }