You are the detective in a crime. From your research you know that Jill and John are lying however the others may be telling the truth or lying. What can you deduce from the statements below?

Jill said: IF John is not involved and Joe told the truth THEN Mike is not involved

John said: IF Abby is involved or Sue is involved THEN Joe is involved

Abby said: IF Cindy is not involved or Joe is not involved THEN Mike is involved or Jill is not involved

Cindy said: IF Mike is involved and Joe told the truth THEN John is not involved or Jill is involved

Sue said: IF Joe is involved or Sue is not involved THEN Cindy is involved or Abby is not involved

Mike said: IF Cindy is not involved and Abby is involved THEN John is not involved or Jill is not involved

Joe said: IF Jill is telling the truth or Cindy is lying THEN Sue is telling the truth or Mike is telling the truth

If this is possible it would be helpful to show the coding and output in order to determine the complexity involved.

Any number of frameworks (programming languages, logic systems, constraint-solving frameworks) can handle such problems, with varying degrees of ease. My favorite tools to use are SMT solvers. When paired with a good programming language interface, you can code such problems with ease.

The following is one way to solve this problem, using the z3 SMT solver, and the Haskell bindings called SBV:

{-# LANGUAGE    DeriveAnyClass, StandaloneDeriving, TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}

module Puzzle where

import Data.SBV

data Person = Jill | John | Joe | Mike | Abby | Sue | Cindy
mkSymbolicEnumeration ''Person

involved, lying, notInvolved, tellsTruth :: Person -> SBool
involved    = uninterpret "involved" . literal
lying       = uninterpret "lying"    . literal
notInvolved = sNot . involved
tellsTruth  = sNot . lying

puzzle :: Goal
puzzle = do
  let infixr 1 `said`
      said p s = constrain $ tellsTruth p .== s

  -- We know Jill and John are lying
  constrain $ lying Jill
  constrain $ lying John

  -- Jill said: IF John is not involved and Joe told the truth THEN Mike is not involved
  Jill `said` (notInvolved John .&& tellsTruth Joe) .=> notInvolved Mike

  -- John said: IF Abby is involved or Sue is involved THEN Joe is involved
  John `said` (involved Abby .|| involved Sue) .=> involved Joe

  -- Abby said: IF Cindy is not involved or Joe is not involved THEN Mike is involved or Jill is not involved
  Abby `said` (notInvolved Cindy .|| notInvolved Joe) .=> (involved Mike .|| notInvolved Jill)

  -- Cindy said: IF Mike is involved and Joe told the truth THEN John is not involved or Jill is involved
  Cindy `said` (involved Mike .&& tellsTruth Joe) .=> (notInvolved John .|| involved Jill)

  -- Sue said: IF Joe is involved or Sue is not involved THEN Cindy is involved or Abby is not involved
  Sue `said` (involved Joe .|| notInvolved Sue) .=> (involved Cindy .|| notInvolved Abby)

  -- Mike said: IF Cindy is not involved and Abby is involved THEN John is not involved or Jill is not involved
  Mike `said` (notInvolved Cindy .&& involved Abby) .=> (notInvolved John .|| notInvolved Jill)

  -- Joe said: IF Jill is telling the truth or Cindy is lying THEN Sue is telling the truth or Mike is telling the truth
  Joe `said` (tellsTruth Jill .|| lying Cindy) .=> (tellsTruth Sue .|| tellsTruth Mike)

When run, this prints:

*Puzzle> sat puzzle
Satisfiable. Model:
  involved :: Person -> Bool
  involved Mike = True
  involved Abby = True
  involved _    = False

  lying :: Person -> Bool
  lying Sue  = True
  lying John = True
  lying Jill = True
  lying _    = False

The nice thing is you can easily get all satisfying solutions as well. Simply run:

*Puzzle> allSat puzzle
... output elided, prints 12 different solutions

All of this is done pretty much instantaneously, so solving time is more or less irrelevant.

Deductions

Note that the above program finds some assignment to the characters that make all the statements true. But it doesn't tell us what's necessarily true, i.e., what we can deduce for sure. The beauty of using an SMT solver with a programming language is that you can program such things with ease. In this case, we want to check if any of the predicates we have is forced. Here's the extra code you need:

deriving instance Enum    Person
deriving instance Bounded Person

isForced :: Person -> SBool -> IO (Maybe (Either Person Person))
isForced p chk = do isSatPos <- isSatisfiable $ puzzle >> constrain chk
                    isSatNeg <- isSatisfiable $ puzzle >> constrain (sNot chk)
                    case (isSatPos, isSatNeg) of
                      (True,  True)  -> return Nothing
                      (True,  False) -> return (Just (Left p))
                      (False, True)  -> return (Just (Right p))
                      (False, False) -> error "Neither positive nor negative version of the prediate is satisfiable!"

forced :: IO ()
forced = do let persons = [minBound .. maxBound]
            forcedLies     <- sequence [isForced p (lying    p) | p <- persons]
            forcedInvolved <- sequence [isForced p (involved p) | p <- persons]

            putStrLn "Conclusions:"
            putStrLn $ "  Definitely     lying   : " ++ unwords [show p | Just (Left  p) <- forcedLies]
            putStrLn $ "  Definitely NOT lying   : " ++ unwords [show p | Just (Right p) <- forcedLies]
            putStrLn $ "  Definitely     involved: " ++ unwords [show p | Just (Left  p) <- forcedInvolved]
            putStrLn $ "  Definitely NOT involved: " ++ unwords [show p | Just (Right p) <- forcedInvolved]

Now, we get:

*Puzzle> forced
Conclusions:
  Definitely     lying   : Jill John
  Definitely NOT lying   : Joe Mike Abby Cindy
  Definitely     involved: Mike
  Definitely NOT involved: John Joe

which shows us what we can definitely conclude from the given predicates.