never { accept_init: s0_init: if :: (p) && (q) && !(r) -> goto s2 :: (p) && !(q) && !(r) -> goto s3 :: (r) -> goto s1 :: !(p) -> goto s1 fi; s1: if :: (p) && (r) -> goto s4 :: !(p) -> goto s7 :: (p) && (q) && !(r) -> goto s7 :: (p) && !(q) && !(r) -> goto s40 fi; s2: if :: !(p) -> goto s7 :: (p) && (r) -> goto s9 :: (p) && (q) && !(r) -> goto accept_s5 :: (p) && !(q) && !(r) -> goto s47 fi; s3: if :: (p) && (r) -> goto s4 :: !(p) && (q) -> goto s7 :: (p) && (q) && !(r) -> goto accept_s5 :: (p) && !(q) && !(r) -> goto s6 :: !(p) && !(q) && (r) -> goto s7 :: !(p) && !(q) && !(r) -> goto s8 fi; s4: if :: (q) -> goto s4 :: (p) && !(q) && !(r) -> goto s60 :: (r) -> goto s4 :: !(p) -> goto s4 fi; s6: if :: !(p) && (q) && !(r) -> goto accept_s30 :: (r) -> goto s4 :: !(p) && !(q) && !(r) -> goto s31 :: (p) && (q) && !(r) -> goto accept_s5 :: (p) && !(q) && !(r) -> goto s6 fi; s7: if :: (p) && (q) -> goto s9 :: !(p) -> goto s11 :: (p) && !(q) && (r) -> goto s9 :: (p) && !(q) && !(r) -> goto s28 fi; s8: if :: (p) && !(q) && !(r) -> goto s10 :: (p) && !(q) && (r) -> goto s9 :: !(p) && !(q) && !(r) -> goto s12 :: !(p) && !(q) && (r) -> goto s11 :: (p) && (q) -> goto s9 :: !(p) && (q) -> goto s11 fi; s9: if :: (p) && (q) && !(r) -> goto s7 :: (p) && !(q) && !(r) -> goto s25 :: !(p) -> goto s7 :: (p) && (r) -> goto s13 fi; s10: if :: !(p) && (q) -> goto s7 :: !(p) && !(q) && !(r) -> goto s8 :: (p) && (r) -> goto s13 :: !(p) && !(q) && (r) -> goto s7 :: (p) && !(q) && !(r) -> goto s23 :: (p) && (q) && !(r) -> goto s7 fi; s11: if :: !(p) -> goto s13 :: (p) && !(q) && !(r) -> goto s21 :: (q) -> goto s13 :: (r) -> goto s13 fi; s12: if :: (q) -> goto s13 :: (r) -> goto s13 :: (p) && !(q) && !(r) -> goto s14 :: !(p) && !(q) && !(r) -> goto s15 fi; s13: if :: !(p) -> goto s11 :: (r) -> goto s11 :: (q) -> goto s11 :: (p) && !(q) && !(r) -> goto s17 fi; s14: if :: (r) -> goto s11 :: (q) -> goto s11 :: !(q) && !(r) -> goto s16 fi; s15: if :: (q) -> goto s11 :: !(q) && !(r) -> goto s12 :: (r) -> goto s11 fi; s16: if :: (r) -> goto s13 :: (q) -> goto s13 :: !(q) && !(r) -> goto s14 fi; s17: if :: !(p) && !(q) && !(r) -> goto s19 :: (r) -> goto s13 :: (p) && !(q) && !(r) -> goto s18 :: (q) -> goto s13 fi; s18: if :: (r) -> goto s11 :: !(q) && !(r) -> goto s20 :: (q) -> goto s11 fi; s19: if :: !(q) && !(r) -> goto s17 :: (q) -> goto s11 :: (r) -> goto s11 fi; s20: if :: (q) -> goto s13 :: (r) -> goto s13 :: !(q) && !(r) -> goto s18 fi; s21: if :: !(p) && !(q) && !(r) -> goto s22 :: (q) -> goto s11 :: (r) -> goto s11 :: (p) && !(q) && !(r) -> goto s20 fi; s22: if :: !(q) && !(r) -> goto s21 :: (q) -> goto s13 :: (r) -> goto s13 fi; s23: if :: !(p) && (q) -> goto s11 :: (p) && (q) && !(r) -> goto s9 :: (r) -> goto s11 :: (p) && !(q) && !(r) -> goto s24 :: !(p) && !(q) && !(r) -> goto s16 fi; s24: if :: !(q) && !(r) -> goto s23 :: (r) -> goto s13 :: (q) && !(r) -> goto s7 fi; s25: if :: (p) && (q) && !(r) -> goto s9 :: !(p) && (q) -> goto s11 :: (r) -> goto s11 :: (p) && !(q) && !(r) -> goto s26 :: !(p) && !(q) && !(r) -> goto s22 fi; s26: if :: (r) -> goto s13 :: (q) && !(r) -> goto s7 :: !(q) && !(r) -> goto s27 fi; s27: if :: (p) && !(q) && !(r) -> goto s26 :: (p) && (q) && !(r) -> goto s9 :: !(p) && !(q) && !(r) -> goto s20 :: !(p) && (q) -> goto s11 :: (r) -> goto s11 fi; s28: if :: (p) && !(q) && !(r) -> goto s27 :: (p) && (q) && !(r) -> goto s7 :: !(p) && !(q) && (r) -> goto s7 :: !(p) && !(q) && !(r) -> goto s29 :: (p) && (r) -> goto s13 :: !(p) && (q) -> goto s7 fi; s29: if :: !(p) && (q) -> goto s11 :: (p) && (q) -> goto s9 :: !(p) && !(q) && !(r) -> goto s17 :: !(p) && !(q) && (r) -> goto s11 :: (p) && !(q) && !(r) -> goto s28 :: (p) && !(q) && (r) -> goto s9 fi; s31: if :: (r) -> goto s4 :: !(p) && (q) && !(r) -> goto accept_s34 :: !(p) && !(q) && !(r) -> goto s35 :: (p) && (q) && !(r) -> goto accept_s32 :: (p) && !(q) && !(r) -> goto s33 fi; s33: if :: (r) -> goto s4 :: (q) && !(r) -> goto accept_s30 :: !(q) && !(r) -> goto s31 fi; s35: if :: (r) -> goto s4 :: (q) && !(r) -> goto accept_s34 :: !(q) && !(r) -> goto s35 fi; s36: if :: !(p) && !(q) && !(r) -> goto s38 :: (p) && !(q) && !(r) -> goto s37 :: (q) -> goto s4 :: (r) -> goto s4 fi; s37: if :: !(q) && !(r) -> goto s39 :: (r) -> goto s4 :: (q) -> goto s4 fi; s38: if :: (r) -> goto s4 :: (q) -> goto s4 :: !(q) && !(r) -> goto s36 fi; s39: if :: (q) -> goto s4 :: !(q) && !(r) -> goto s37 :: (r) -> goto s4 fi; s40: if :: (p) && !(q) && !(r) -> goto s41 :: (r) -> goto s4 :: (p) && (q) && !(r) -> goto s9 :: !(p) && !(q) && !(r) -> goto s42 :: !(p) && (q) && !(r) -> goto s11 fi; s41: if :: (r) -> goto s4 :: !(q) && !(r) -> goto s46 :: (q) && !(r) -> goto s7 fi; s42: if :: (q) && !(r) -> goto s13 :: (r) -> goto s4 :: !(q) && !(r) -> goto s43 fi; s43: if :: (q) && !(r) -> goto s11 :: (p) && !(q) && !(r) -> goto s44 :: (r) -> goto s4 :: !(p) && !(q) && !(r) -> goto s42 fi; s44: if :: (q) && !(r) -> goto s13 :: !(q) && !(r) -> goto s45 :: (r) -> goto s4 fi; s45: if :: !(q) && !(r) -> goto s44 :: (r) -> goto s4 :: (q) && !(r) -> goto s11 fi; s46: if :: (r) -> goto s4 :: !(p) && !(q) && !(r) -> goto s44 :: !(p) && (q) && !(r) -> goto s11 :: (p) && !(q) && !(r) -> goto s41 :: (p) && (q) && !(r) -> goto s9 fi; s47: if :: !(p) && (q) && !(r) -> goto accept_s30 :: !(p) && !(q) && !(r) -> goto s49 :: (p) && (q) && !(r) -> goto accept_s5 :: (p) && !(q) && !(r) -> goto s48 :: !(p) && (r) -> goto s7 :: (p) && (r) -> goto s13 fi; s48: if :: (p) && (q) && !(r) -> goto accept_s5 :: (p) && !(q) && !(r) -> goto s57 :: !(p) && (q) && !(r) -> goto accept_s30 :: !(p) && !(q) && !(r) -> goto s58 :: (r) -> goto s11 fi; s49: if :: (p) && (r) -> goto s9 :: !(p) && (q) && !(r) -> goto accept_s34 :: !(p) && !(q) && !(r) -> goto s51 :: (p) && (q) && !(r) -> goto accept_s32 :: !(p) && (r) -> goto s11 :: (p) && !(q) && !(r) -> goto s50 fi; s50: if :: (p) && !(q) && !(r) -> goto s55 :: (p) && (r) -> goto s13 :: (q) && !(r) -> goto accept_s30 :: !(p) && !(q) && !(r) -> goto s49 :: !(p) && (r) -> goto s7 fi; s51: if :: (q) && !(r) -> goto accept_s34 :: !(p) && !(q) && !(r) -> goto s53 :: (r) -> goto s13 :: (p) && !(q) && !(r) -> goto s52 fi; s52: if :: (q) && !(r) -> goto accept_s34 :: (r) -> goto s11 :: !(q) && !(r) -> goto s54 fi; s53: if :: !(q) && !(r) -> goto s51 :: (q) && !(r) -> goto accept_s34 :: (r) -> goto s11 fi; s54: if :: !(q) && !(r) -> goto s52 :: (q) && !(r) -> goto accept_s34 :: (r) -> goto s13 fi; s55: if :: (p) && !(q) && !(r) -> goto s56 :: (p) && (q) && !(r) -> goto accept_s32 :: !(p) && !(q) && !(r) -> goto s54 :: !(p) && (q) && !(r) -> goto accept_s34 :: (r) -> goto s11 fi; s56: if :: !(q) && !(r) -> goto s55 :: (q) && !(r) -> goto accept_s30 :: (r) -> goto s13 fi; s57: if :: !(p) && !(q) && !(r) -> goto s55 :: !(p) && (q) && !(r) -> goto accept_s30 :: (r) -> goto s13 :: (p) && !(q) && !(r) -> goto s48 :: (p) && (q) && !(r) -> goto accept_s5 fi; s58: if :: (p) && (q) && !(r) -> goto accept_s32 :: (p) && !(q) && !(r) -> goto s59 :: (r) -> goto s13 :: !(p) && (q) && !(r) -> goto accept_s34 :: !(p) && !(q) && !(r) -> goto s52 fi; s59: if :: (r) -> goto s11 :: !(q) && !(r) -> goto s58 :: (q) && !(r) -> goto accept_s30 fi; s60: if :: (r) -> goto s4 :: (q) -> goto s4 :: !(p) && !(q) && !(r) -> goto s62 :: (p) && !(q) && !(r) -> goto s61 fi; s61: if :: !(q) && !(r) -> goto s61 :: (r) -> goto s4 :: (q) -> goto s4 fi; s62: if :: (q) -> goto s4 :: !(q) && !(r) -> goto s60 :: (r) -> goto s4 fi; accept_s5: if :: (p) && (r) -> goto s9 :: !(p) -> goto s7 :: (p) && !(q) && !(r) -> goto s47 :: (p) && (q) && !(r) -> goto accept_s5 fi; accept_s30: if :: (p) && (q) -> goto s9 :: (p) && !(q) && !(r) -> goto s10 :: (p) && !(q) && (r) -> goto s9 :: !(p) -> goto s4 fi; accept_s32: if :: (p) && !(q) && !(r) -> goto s40 :: (p) && (r) -> goto s4 :: (p) && (q) && !(r) -> goto s7 :: !(p) -> goto s7 fi; accept_s34: if :: (q) -> goto s4 :: (r) -> goto s4 :: !(p) -> goto s4 :: (p) && !(q) && !(r) -> goto s36 fi; }