prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
prove ostr (Theory sig thsens) _freedefs = do
  let str = map (\ c -> if c == '/' then '-' else c) ostr
      oSens = toNamedList thsens
      (fsig, sens) = addUniformRestr sig oSens
      (disAxs, disGoals) = partition isAxiom oSens
      rMap = Map.fromList $ map (\ SenAttr { senAttr = n } ->
                (map toUpper $ transString n, n)) disGoals
#ifdef TAR_PACKAGE
  moveVSEFiles str
#endif
  (inp, out, cp) <- prepareAndCallVSE
  sendMyMsg inp $ "(" ++ str ++ ")"
  readMyMsg cp out linksP
  sendMyMsg inp "nil"
  readMyMsg cp out sigP
  sendMyMsg inp $ show $ prettySExpr $ vseSignToSExpr fsig
  readMyMsg cp out lemsP
  sendMyMsg inp $ show $ prettySExpr $ SList $ map (namedSenToSExpr fsig) sens
  ms <- readFinalVSEOutput cp out
#ifdef TAR_PACKAGE
  createVSETarFile str
#endif
  case ms of
    Nothing -> return []
    Just lemMap -> return
          $ foldr (\ s r -> case Map.lookup s rMap of
                 Nothing -> r
                 Just n -> mkVseProofStatus n (map senAttr disAxs) : r) []
          $ Map.findWithDefault [] (map toUpper str) lemMap
prove :: String -> Theory VSESign Sentence () -> a -> IO [ProofStatus ()]
prove ostr (Theory sig thsens) _freedefs = do
  let str = map (\ c -> if c == '/' then '-' else c) ostr
      oSens = toNamedList thsens
      (fsig, sens) = addUniformRestr sig oSens
      (disAxs, disGoals) = partition isAxiom oSens
      rMap = Map.fromList $ map (\ SenAttr { senAttr = n } ->
                (map toUpper $ transString n, n)) disGoals
#ifdef TAR_PACKAGE
  moveVSEFiles str
#endif
  (inp, out, cp) <- prepareAndCallVSE
  sendMyMsg inp $ "(" ++ str ++ ")"
  readMyMsg cp out linksP
  sendMyMsg inp "nil"
  readMyMsg cp out sigP
  sendMyMsg inp $ show $ prettySExpr $ vseSignToSExpr fsig
  readMyMsg cp out lemsP
  sendMyMsg inp $ show $ prettySExpr $ SList $ map (namedSenToSExpr fsig) sens
  ms <- readFinalVSEOutput cp out
#ifdef TAR_PACKAGE
  createVSETarFile str
#endif
  case ms of
    Nothing -> return []
    Just lemMap -> return
          $ foldr (\ s r -> case Map.lookup s rMap of
                 Nothing -> r
                 Just n -> mkVseProofStatus n (map senAttr disAxs) : r) []
          $ Map.findWithDefault [] (map toUpper str) lemMap
prove ostr (Theory sig thsens) _freedefs = do
  let str = map (\ c -> if c == '/' then '-' else c) ostr
      oSens = toNamedList thsens
      (fsig, sens) = addUniformRestr sig oSens
      (disAxs, disGoals) = partition isAxiom oSens
      rMap = Map.fromList $ map (\ SenAttr { senAttr = n } ->
                (map toUpper $ transString n, n)) disGoals
#ifdef TAR_PACKAGE
  moveVSEFiles str
#endif
  (inp, out, cp) <- prepareAndCallVSE
  sendMyMsg inp $ "(" ++ str ++ ")"
  readMyMsg cp out linksP
  sendMyMsg inp "nil"
  readMyMsg cp out sigP
  sendMyMsg inp $ show $ prettySExpr $ vseSignToSExpr fsig
  readMyMsg cp out lemsP
  sendMyMsg inp $ show $ prettySExpr $ SList $ map (namedSenToSExpr fsig) sens
  ms <- readFinalVSEOutput cp out
#ifdef TAR_PACKAGE
  createVSETarFile str
#endif
  case ms of
    Nothing -> return []
    Just lemMap -> return
          $ foldr (\ s r -> case Map.lookup s rMap of
                 Nothing -> r
                 Just n -> mkVseProofStatus n (map senAttr disAxs) : r) []
          $ Map.findWithDefault [] (map toUpper str) lemMap