never { s0_init: if :: (p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s2 :: !(p) && (q) && (r) && (s) && (t) -> goto accept_s1 :: !(p) && !(q) && (r) && (s) && (t) -> goto accept_s1 :: !(p) && (q) && !(r) && (s) && (t) -> goto accept_s1 :: !(p) && !(q) && !(r) && (s) && (t) -> goto accept_s1 :: !(p) && (q) && (r) && !(s) && (t) -> goto accept_s1 :: !(p) && !(q) && (r) && !(s) && (t) -> goto accept_s1 :: !(p) && (q) && !(r) && !(s) && (t) -> goto accept_s1 :: !(p) && !(q) && !(r) && !(s) && (t) -> goto accept_s1 :: !(p) && (q) && (r) && (s) && !(t) -> goto accept_s1 :: !(p) && !(q) && (r) && (s) && !(t) -> goto accept_s1 :: !(p) && (q) && !(r) && (s) && !(t) -> goto accept_s1 :: !(p) && !(q) && !(r) && (s) && !(t) -> goto accept_s1 :: !(p) && (q) && (r) && !(s) && !(t) -> goto accept_s1 :: !(p) && !(q) && (r) && !(s) && !(t) -> goto accept_s1 :: !(p) && (q) && !(r) && !(s) && !(t) -> goto accept_s1 :: !(p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s1 :: (p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: (p) && (q) && (r) && !(s) && !(t) -> goto accept_s3 fi; s4: if :: (p) && !(q) && !(r) && !(s) && !(t) -> goto s4 :: !(p) && !(q) && !(r) && !(s) && !(t) -> goto s4 :: (p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: !(p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: (p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: (p) && (q) && (r) && !(s) && !(t) -> goto s4 :: !(p) && (q) && (r) && !(s) && !(t) -> goto s4 :: (p) && !(q) && (r) && !(s) && !(t) -> goto s4 :: !(p) && !(q) && (r) && !(s) && !(t) -> goto s4 fi; accept_s1: if :: (p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s2 :: !(p) && (q) && (r) && (s) && (t) -> goto accept_s1 :: !(p) && !(q) && (r) && (s) && (t) -> goto accept_s1 :: !(p) && (q) && !(r) && (s) && (t) -> goto accept_s1 :: !(p) && !(q) && !(r) && (s) && (t) -> goto accept_s1 :: !(p) && (q) && (r) && !(s) && (t) -> goto accept_s1 :: !(p) && !(q) && (r) && !(s) && (t) -> goto accept_s1 :: !(p) && (q) && !(r) && !(s) && (t) -> goto accept_s1 :: !(p) && !(q) && !(r) && !(s) && (t) -> goto accept_s1 :: !(p) && (q) && (r) && (s) && !(t) -> goto accept_s1 :: !(p) && !(q) && (r) && (s) && !(t) -> goto accept_s1 :: !(p) && (q) && !(r) && (s) && !(t) -> goto accept_s1 :: !(p) && !(q) && !(r) && (s) && !(t) -> goto accept_s1 :: !(p) && (q) && (r) && !(s) && !(t) -> goto accept_s1 :: !(p) && !(q) && (r) && !(s) && !(t) -> goto accept_s1 :: !(p) && (q) && !(r) && !(s) && !(t) -> goto accept_s1 :: !(p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s1 :: (p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: (p) && (q) && (r) && !(s) && !(t) -> goto accept_s3 fi; accept_s2: if :: (p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: !(p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: (p) && (q) && (r) && !(s) && !(t) -> goto accept_s3 :: !(p) && (q) && (r) && !(s) && !(t) -> goto accept_s3 :: (p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && (s) && !(t) -> goto accept_s2 :: !(p) && !(q) && (r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && !(t) -> goto accept_s2 :: !(p) && !(q) && !(r) && (s) && !(t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && !(t) -> goto accept_s2 :: !(p) && !(q) && (r) && !(s) && !(t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s2 :: !(p) && !(q) && !(r) && !(s) && !(t) -> goto accept_s2 fi; accept_s3: if :: (p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && (s) && (t) -> goto accept_s2 :: (p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && (r) && !(s) && (t) -> goto accept_s2 :: (p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: !(p) && !(q) && !(r) && !(s) && (t) -> goto accept_s2 :: (p) && (q) && (r) && !(s) && !(t) -> goto s4 :: !(p) && (q) && (r) && !(s) && !(t) -> goto s4 :: (p) && !(q) && (r) && !(s) && !(t) -> goto s4 :: !(p) && !(q) && (r) && !(s) && !(t) -> goto s4 :: (p) && !(q) && !(r) && !(s) && !(t) -> goto s4 :: !(p) && !(q) && !(r) && !(s) && !(t) -> goto s4 :: (p) && (q) && (r) && !(s) && (t) -> goto accept_s3 :: !(p) && (q) && (r) && !(s) && (t) -> goto accept_s3 fi; }