diff --git a/src/TPDB/CPF/Proof/Type.hs b/src/TPDB/CPF/Proof/Type.hs
--- a/src/TPDB/CPF/Proof/Type.hs
+++ b/src/TPDB/CPF/Proof/Type.hs
@@ -97,8 +97,49 @@
               }
      | StringReversal { trs :: TRS Identifier Identifier
                       , trsTerminationProof :: TrsTerminationProof  
-                      }  
+                      }
+     | Bounds { trs :: TRS Identifier Identifier
+              , bounds_type :: Bounds_Type
+              , bounds_bound :: Int
+              , bounds_finalStates :: [ State ]
+              , bounds_closedTreeAutomaton :: ClosedTreeAutomaton
+              }
    deriving ( Typeable, Eq )
+
+data Bounds_Type = Roof | Match
+  deriving ( Typeable, Eq )
+
+data ClosedTreeAutomaton = ClosedTreeAutomaton
+  { cta_treeAutomaton :: TreeAutomaton
+  , cta_criterion :: Criterion
+  }
+  deriving ( Typeable, Eq )
+
+data Criterion = Compatibility
+  deriving ( Typeable, Eq )
+
+data TreeAutomaton = TreeAutomaton
+  { ta_finalStates :: [ State ]
+  , ta_transitions :: [ Transition ]
+  }
+   deriving ( Typeable, Eq )
+
+data State = State Int
+   deriving ( Typeable, Eq )
+
+data Transition = Transition
+  { transition_lhs :: Transition_Lhs
+  , transition_rhs :: [ State ]
+  }
+  deriving ( Typeable, Eq )
+
+data Transition_Lhs
+  = Transition_Symbol { tr_symbol :: Symbol
+                      , tr_height :: Int
+                      , tr_arguments :: [ State ]
+                      }                    
+  | Transition_Epsilon State
+  deriving ( Typeable, Eq )
 
 data Model = FiniteModel Int [Interpret]
    deriving ( Typeable, Eq )
diff --git a/src/TPDB/CPF/Proof/Write.hs b/src/TPDB/CPF/Proof/Write.hs
--- a/src/TPDB/CPF/Proof/Write.hs
+++ b/src/TPDB/CPF/Proof/Write.hs
@@ -120,10 +120,60 @@
           , toContents $ symbolize $ trs p
           , toContents $ trsTerminationProof p
           ]
+      Bounds {} -> rmkel "bounds" $ concat
+          [ toContents $ symbolize $ trs p
+          , toContents $ bounds_type p
+          , rmkel "bound" $ toContents $ bounds_bound p 
+          , rmkel "finalStates" $ concat
+             $ map toContents $ bounds_finalStates p
+          , toContents $ bounds_closedTreeAutomaton p
+          ]
 
 symbolize trs = 
     ( fmap (fmap SymName) trs )
     { T.signature = map SymName $ T.signature trs }
+
+instance XmlContent Bounds_Type where
+  toContents t = case t of
+    Roof -> rmkel "roof" []
+    Match -> rmkel "match" []
+
+instance XmlContent State where
+  toContents (State s) = rmkel "state"  $ toContents s
+
+instance XmlContent ClosedTreeAutomaton where
+  toContents c = concat
+    [ toContents $ cta_treeAutomaton c
+    , toContents $ cta_criterion c
+    ]
+
+instance XmlContent Criterion where
+  toContents c = case c of
+    Compatibility -> rmkel "compatibility" []
+
+instance XmlContent TreeAutomaton where
+  toContents a = rmkel "treeAutomaton" $ concat
+    [ rmkel "finalStates" $ concat
+       $ map toContents $ ta_finalStates a
+    , rmkel "transitions" $ concat
+       $ map toContents $ ta_transitions a
+    ]
+
+instance XmlContent Transition where
+  toContents t = rmkel "transition" $ concat
+    [ rmkel "lhs" $ toContents $ transition_lhs t
+    , rmkel "rhs" $ concat
+       $ map toContents $ transition_rhs t
+    ]
+
+instance XmlContent Transition_Lhs where
+  toContents s = case s of
+    Transition_Symbol {} -> concat
+      [ toContents $ tr_symbol s
+      , rmkel "height" $ toContents $ tr_height s
+      , concat $ map toContents $ tr_arguments s
+      ]
+    Transition_Epsilon s -> toContents s
 
 instance XmlContent Model where
   parseContents = error "parseContents not implemented"
diff --git a/src/TPDB/DP/Graph.hs b/src/TPDB/DP/Graph.hs
--- a/src/TPDB/DP/Graph.hs
+++ b/src/TPDB/DP/Graph.hs
@@ -1,3 +1,5 @@
+{-# language OverloadedStrings #-}
+
 module TPDB.DP.Graph where
 
 import TPDB.DP.TCap
diff --git a/src/TPDB/Data.hs b/src/TPDB/Data.hs
--- a/src/TPDB/Data.hs
+++ b/src/TPDB/Data.hs
@@ -4,12 +4,15 @@
 
 ( module TPDB.Data
 , module TPDB.Data.Term
+, module TPDB.Data.Rule
 )
 
 where
 
 
 import TPDB.Data.Term
+import TPDB.Data.Rule
+import TPDB.Data.Attributes
 
 import Data.Typeable
 import Control.Monad ( guard )
@@ -36,39 +39,20 @@
 
 ---------------------------------------------------------------------
 
-data Relation = Strict |  Weak | Equal deriving ( Eq, Ord, Typeable, Show )
 
-data Rule a = Rule { lhs :: a, rhs :: a 
-                   , relation :: Relation
-                   , top :: Bool
-                   }
-    deriving ( Eq, Ord, Typeable )
-
-strict :: Rule a -> Bool
-strict u = case relation u of Strict -> True ; _ -> False
-
-weak :: Rule a -> Bool
-weak u = case relation u of Weak -> True ; _ -> False
-
-equal :: Rule a -> Bool
-equal u = case relation u of Equal -> True ; _ -> False
-
-instance Functor (RS s) where
-    fmap f rs = rs { rules = map (fmap f) $ rules rs }
-
-instance Functor Rule where 
-    fmap f u = u { lhs = f $ lhs u, rhs = f $ rhs u } 
-
 data RS s r = 
      RS { signature :: [ s ] -- ^ better keep order in signature (?)
-         , rules :: [ Rule r ]
+        , rules :: [ Rule r ]
         , separate :: Bool -- ^ if True, write comma between rules
-         }
+        }
    deriving ( Typeable )
 
 instance Eq r => Eq (RS s r) where
     (==) = (==) `on` rules
 
+instance Functor (RS s) where
+    fmap f rs = rs { rules = map (fmap f) $ rules rs }
+
 strict_rules sys = 
     do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
 weak_rules sys = 
@@ -86,6 +70,7 @@
              , strategy :: Maybe Strategy
              -- , metainformation :: Metainformation
              , startterm :: Maybe Startterm  
+             , attributes :: Attributes
              }
 
 data Type = Termination | Complexity
@@ -101,7 +86,7 @@
 
 ------------------------------------------------------
 
--- | legaca stuff (used in matchbox)
+-- | legacy stuff (used in matchbox)
 
 type TES = TRS Identifier Identifier
 type SES = SRS Identifier
diff --git a/src/TPDB/Data/Attributes.hs b/src/TPDB/Data/Attributes.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Data/Attributes.hs
@@ -0,0 +1,74 @@
+{-# language OverloadedStrings #-}
+
+module TPDB.Data.Attributes where
+
+import TPDB.Data.Term
+import TPDB.Data.Rule
+import TPDB.Pretty 
+
+import qualified Data.Set as S
+import qualified Data.Map.Strict as M
+
+data Attributes = Attributes
+  { size_of_signature :: Int
+  , max_arity :: Int
+  , total_term_size :: Int
+  , max_term_size :: Int
+  , max_term_depth :: Int
+  , left_linear :: Bool
+  , right_linear :: Bool
+  , linear :: Bool
+  , max_var_count :: Int
+  , max_var_depth :: Int
+  }
+
+instance Pretty Attributes where
+  pretty a = "Attributes" <+> braces ( fsep $ punctuate comma
+       [ "size_of_signature =" <+> pretty (size_of_signature a)
+       , "max_arity =" <+> pretty (max_arity a)
+       , "total_term_size =" <+> pretty (total_term_size a)
+       , "max_term_size =" <+> pretty (max_term_size a)
+       , "max_term_depth =" <+> pretty (max_term_depth a)
+       , "left_linear =" <+> pretty (left_linear a)
+       , "right_linear =" <+> pretty (right_linear a)
+       , "linear =" <+> pretty (linear a)
+       , "max_var_count =" <+> pretty (max_var_count a)
+       , "max_var_depth =" <+> pretty (max_var_depth a)
+       ] )
+  
+
+compute_attributes
+  :: (Ord v, Ord c)
+  => [Rule (Term v c)] -> Attributes
+compute_attributes us =
+  let terms = do u <- us; [lhs u, rhs u]
+      sterms = terms >>= subterms
+      sig = S.fromList ( terms >>= symsl )
+      term_sizes = map size terms
+      term_depths = map depth terms
+      vcs = map varcount us
+  in Attributes
+     { size_of_signature = S.size sig
+     , max_arity = maximum $ do
+       u <- us ; t <- [lhs u, rhs u]
+       Node f args <- subterms t
+       return $ length args
+     , total_term_size = sum term_sizes
+     , max_term_size = maximum term_sizes
+     , max_term_depth = maximum term_depths
+     , left_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l <= 1
+     , right_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ r <= 1
+     , linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l == 1 && r == 1 -- FIXME: or (l == r) ?
+     , max_var_count = maximum $ map M.size vcs
+     , max_var_depth = maximum $ map length $ terms >>= varpos
+     }
+
+varcount :: Ord v => Rule (Term v c) -> M.Map v (Int,Int)
+varcount u = M.mergeWithKey ( \ k l r -> Just (l,r)) ( M.map ( \k -> (k,0))) (M.map ( \k -> (0,k)))
+        (varcount_term $ lhs u) (varcount_term $ rhs u)
+
+varcount_term :: Ord v => Term v c -> M.Map v Int
+varcount_term t = M.fromListWith (+) $ do
+  (p, Var v) <- positions t
+  return (v, 1)
+  
diff --git a/src/TPDB/Data/Rule.hs b/src/TPDB/Data/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Data/Rule.hs
@@ -0,0 +1,23 @@
+module TPDB.Data.Rule where
+
+import Data.Typeable
+
+data Relation = Strict |  Weak | Equal deriving ( Eq, Ord, Typeable, Show )
+
+data Rule a = Rule { lhs :: a, rhs :: a 
+                   , relation :: Relation
+                   , top :: Bool
+                   }
+    deriving ( Eq, Ord, Typeable )
+
+strict :: Rule a -> Bool
+strict u = case relation u of Strict -> True ; _ -> False
+
+weak :: Rule a -> Bool
+weak u = case relation u of Weak -> True ; _ -> False
+
+equal :: Rule a -> Bool
+equal u = case relation u of Equal -> True ; _ -> False
+
+instance Functor Rule where 
+    fmap f u = u { lhs = f $ lhs u, rhs = f $ rhs u } 
diff --git a/src/TPDB/Data/Term.hs b/src/TPDB/Data/Term.hs
--- a/src/TPDB/Data/Term.hs
+++ b/src/TPDB/Data/Term.hs
@@ -26,10 +26,23 @@
           -> [ ( Position, Term v c ) ]
 positions t = ( [], t ) : case t of
     Node c args -> do ( k, arg ) <- zip [ 0 .. ] args
-		      ( p, s   ) <- positions arg
-		      return ( k : p , s )
+                      ( p, s   ) <- positions arg
+                      return ( k : p , s )
     _ -> []
 
+-- FIXME: inefficient implementation (walks the tree),
+-- should store the result in each node instead,
+-- but this would break pattern matching.
+size :: Term v c -> Int
+size t = length $ positions t
+
+depth :: Term v c -> Int
+depth t = case t of
+  Var {} -> 0
+  Node f args -> case args of
+    [] -> 0
+    _  -> 1 + maximum (map depth args)
+
 -- | all positions
 pos :: Term v c 
     -> [ Position ]
@@ -62,10 +75,10 @@
 {-# inline subterms #-}
 
 subterms :: Term v c 
-	 -> [ Term v c ]
+         -> [ Term v c ]
 subterms t = t : case t of
     Node c args -> do arg <- args
-		      subterms arg
+                      subterms arg
     _ -> []
 
 -- Note: following implementation relies on @subterms@
@@ -93,8 +106,8 @@
      -> Term v d
 rpmap f t = helper [] t where
     helper p ( Node c args ) = Node ( f p c ) $ do
-	     ( k, arg ) <- zip [0..] args
-	     return $ helper ( k : p ) arg
+             ( k, arg ) <- zip [0..] args
+             return $ helper ( k : p ) arg
     helper p ( Var v) = Var v
 
 
@@ -111,7 +124,7 @@
 peek_symbol t p = 
     case peek t p of
          Node c args -> c
-	 _ -> error "Autolib.TES.Position.peek_symbol called for non-symbol"
+         _ -> error "Autolib.TES.Position.peek_symbol called for non-symbol"
 
 -- | warning: don't check arity
 poke_symbol ::  Term v c 
@@ -120,7 +133,7 @@
 poke_symbol t ( p, c ) =  
     case peek t p of
          Node _ args -> poke t ( p, Node c args )
-	 _ -> error "Autolib.TES.Position.poke_symbol called for non-symbol"
+         _ -> error "Autolib.TES.Position.poke_symbol called for non-symbol"
 
 poke :: Term v c 
      -> ( Position , Term v c )
diff --git a/src/TPDB/Input.hs b/src/TPDB/Input.hs
--- a/src/TPDB/Input.hs
+++ b/src/TPDB/Input.hs
@@ -1,64 +1,7 @@
-module TPDB.Input where
-
-import TPDB.Data
-import TPDB.Plain.Read
-import TPDB.XTC.Read
-import TPDB.Convert
-
-import System.FilePath.Posix ( takeExtension )
-
--- | read input from file with given name.
--- can have extension .srs, .trs, .xml.
--- unknown extension is considered as .xml, because of 
--- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
-
-get :: FilePath 
-         -> IO ( Either (TRS Identifier Identifier) 
-                        ( SRS Identifier ) )
-get f = do
-    m <- getE f
-    case m of
-        Right x -> return x 
-        Left err -> error err
-
-getE f = case takeExtension f of
-      ".srs" -> do
-          s <- readFile f    
-          case srs s of
-              Left err -> return $ Left err
-              Right t -> return $ Right $ Right t
-      ".trs" -> do        
-          s <- readFile f
-          case TPDB.Plain.Read.trs s of
-              Left err -> return $ Left err
-              Right t -> return $ Right $ Left t 
-      _ -> do
-          ps <- readProblems f
-          case ps of 
-              [ p ] -> return $ Right $ Left $ TPDB.Data.trs p
-              [] -> return $ Left "no TRS"
-              _ -> return $ Left "more than one TRS"
-
-get_trs f = do
-    x <- get f
-    return $ case x of
-        Right x -> srs2trs x
-        Left  x -> x
+module TPDB.Input {-# deprecated "use TPDB.INput.File instead" #-}
 
-getE_trs f = do
-    e <- getE f
-    return $ case e of
-        Right x -> Right $ case x of
-            Right x -> srs2trs x
-            Left  x -> x
-        Left e -> Left e
+( module TPDB.Input.File )
 
-get_srs f = do
-    x <- get f
-    return $ case x of
-        Right x -> x
-        Left  x -> case trs2srs x of
-            Nothing -> error "not an SRS"
-            Just x -> x
-            
+where
 
+import TPDB.Input.File
diff --git a/src/TPDB/Input/File.hs b/src/TPDB/Input/File.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Input/File.hs
@@ -0,0 +1,51 @@
+module TPDB.Input.File where
+
+import TPDB.Data
+import TPDB.Convert
+
+import qualified TPDB.Input.Memory as TIM
+
+import qualified Data.ByteString.Lazy as B
+import System.FilePath.Posix ( takeExtension )
+
+-- | read input from file with given name.
+-- can have extension .srs, .trs, .xml.
+-- unknown extension is considered as .xml, because of 
+-- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
+
+get :: FilePath 
+         -> IO ( Either (TRS Identifier Identifier) 
+                        ( SRS Identifier ) )
+get f = do
+    m <- getE f
+    case m of
+        Right x -> return x 
+        Left err -> error err
+
+getE f = do
+  s <- B.readFile f
+  TIM.get f s
+
+get_trs f = do
+    x <- get f
+    return $ case x of
+        Right x -> srs2trs x
+        Left  x -> x
+
+getE_trs f = do
+    e <- getE f
+    return $ case e of
+        Right x -> Right $ case x of
+            Right x -> srs2trs x
+            Left  x -> x
+        Left e -> Left e
+
+get_srs f = do
+    x <- get f
+    return $ case x of
+        Right x -> x
+        Left  x -> case trs2srs x of
+            Nothing -> error "not an SRS"
+            Just x -> x
+            
+
diff --git a/src/TPDB/Input/Memory.hs b/src/TPDB/Input/Memory.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/Input/Memory.hs
@@ -0,0 +1,32 @@
+-- | read benchmark from in-memory data (e.g., from a ByteString)
+
+module TPDB.Input.Memory
+
+where
+
+import TPDB.Data
+import TPDB.Plain.Read
+import TPDB.XTC.Read
+
+import qualified Data.ByteString.Lazy as B
+import System.FilePath.Posix ( takeExtension )
+
+-- | first argument is file name, second argument is file contents.
+-- first arg. is needed to pick the proper parser (SRS, TRS, XTC)
+get :: String -> B.ByteString
+    -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier)))
+get f s = case takeExtension f of
+      ".srs" -> do
+          case srs s of
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Right t
+      ".trs" -> do        
+          case TPDB.Plain.Read.trs s of
+              Left err -> return $ Left err
+              Right t -> return $ Right $ Left t 
+      _ -> do
+          ps <- readProblemsBS s
+          case ps of 
+              [ p ] -> return $ Right $ Left $ TPDB.Data.trs p
+              [] -> return $ Left "no TRS"
+              _ -> return $ Left "more than one TRS"
diff --git a/src/TPDB/Plain/Read.hs b/src/TPDB/Plain/Read.hs
--- a/src/TPDB/Plain/Read.hs
+++ b/src/TPDB/Plain/Read.hs
@@ -7,10 +7,19 @@
 
 import TPDB.Data
 
-import Text.Parsec
+import Text.Parsec (parse)
+
+import qualified Data.ByteString.Lazy as B
+import Data.ByteString.Lazy (ByteString)
+import qualified Data.ByteString.Lazy.Char8 as C
+
+import Text.Parsec.ByteString.Lazy as P
 import Text.Parsec.Token
 import Text.Parsec.Language
 import Text.Parsec.Char
+import Control.Applicative
+-- import Text.Parsec.Combinator
+import Data.Functor.Identity (Identity)
 
 import TPDB.Pretty (pretty)
 import TPDB.Plain.Write ()
@@ -18,33 +27,38 @@
 import Control.Monad ( guard, void )
 import Data.List ( nub )
 
-trs :: String -> Either String ( TRS Identifier Identifier )
+trs :: ByteString -> Either String ( TRS Identifier Identifier )
 trs s = case Text.Parsec.parse reader "input" s of
     Left err -> Left $ show err
     Right t  -> Right t
 
-srs :: String -> Either String ( SRS Identifier )
+srs :: ByteString -> Either String ( SRS Identifier )
 srs s = case Text.Parsec.parse reader "input" s of
     Left err -> Left $ show err
     Right t  -> Right t
 
-type Parser = Parsec String () 
+-- type Parser = Parsec ByteString () 
 
-class Reader a where reader :: Parser a
+class Reader a where reader :: P.Parser a
 
 -- | warning: by definition, {}[] may appear in identifiers
+lexer :: GenTokenParser ByteString () Identity
 lexer = makeTokenParser
-    $ emptyDef
-       { identStart  = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
+    $ LanguageDef
+       { nestedComments = True
+       , opStart        = oneOf ":!#$%&*+./<=>?@\\^|-~"
+       , opLetter       = oneOf ":!#$%&*+./<=>?@\\^|-~"
+       , reservedOpNames = []
+       , caseSensitive  = True
+       , identStart  = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
        , identLetter = alphaNum <|> oneOf "_:!#$%&*+./<=>?@\\^|-~{}[]'"
        , commentLine = "" , commentStart = "" , commentEnd = ""
        , reservedNames = [ "VAR", "THEORY", "STRATEGY", "RULES", "->", "->=" ]
        }
 
-
 instance Reader Identifier where 
     reader = do
-        i <- identifier lexer 
+        i :: String <- identifier lexer 
 	return $ mk 0 i
 
 instance Reader s =>  Reader [s] where
@@ -56,7 +70,7 @@
 instance ( Reader v ) => Reader ( Term v Identifier ) where
     reader = do
         f  <- reader 
-        xs <- option [] $ parens lexer $ commaSep lexer reader
+        xs <- ( parens lexer $ commaSep lexer reader ) <|> return []
         return $ Node ( f { arity = length xs } ) xs
 
 instance Reader u => Reader ( Rule u ) where
@@ -79,7 +93,7 @@
        -- ^ this is super-ugly: a parenthesized, possibly nested, 
        -- possibly comma-separated, list of identifiers or strings
 
-declaration :: Reader u => Bool -> Parser ( Declaration u )
+declaration :: Reader u => Bool -> P.Parser ( Declaration u )
 declaration sep = parens lexer $ 
            do reserved lexer "VAR" ; xs <- many reader 
               return $ Var_Declaration xs
diff --git a/src/TPDB/Plain/Write.hs b/src/TPDB/Plain/Write.hs
--- a/src/TPDB/Plain/Write.hs
+++ b/src/TPDB/Plain/Write.hs
@@ -20,17 +20,17 @@
         Var v -> pretty v
         Node f xs -> case xs of
             [] -> pretty f 
-            _  -> pretty f <+> parens ( fsep $ punctuate comma $ map pretty xs )
+            _  -> pretty f <+> ( parens $ fsep $ punctuate comma $ map pretty xs )
 
 instance PrettyTerm a => Pretty ( Rule a ) where
-    pretty u = hsep [ prettyTerm $ lhs u
-                    , case relation u of 
+    pretty u = sep [ prettyTerm $ lhs u
+                   , ( case relation u of 
                          Strict -> "->" 
                          Weak -> "->="
-                         Equal -> "="
-                    -- FIXME: implement "top" annotation
-                    , prettyTerm $ rhs u
-                    ]
+                         Equal -> "=" 
+                   -- FIXME: implement "top" annotation
+                     ) <+> prettyTerm ( rhs u )
+                   ]
 
 class PrettyTerm a where 
     prettyTerm :: a -> Doc
@@ -58,10 +58,10 @@
        [ pretty $ trs p 
        , case strategy p of  
              Nothing -> empty
-             Just s -> fsep [ "strategy"
+             Just s -> sep [ "strategy"
                             , fromString ( show s ) ]
        , case startterm p of  
              Nothing -> empty
-             Just s -> fsep [ "startterm"
+             Just s -> sep [ "startterm"
                             , fromString ( show s ) ] 
        ]
diff --git a/src/TPDB/Pretty.hs b/src/TPDB/Pretty.hs
--- a/src/TPDB/Pretty.hs
+++ b/src/TPDB/Pretty.hs
@@ -3,7 +3,7 @@
 ( Doc, SimpleDoc
 , render, renderCompact, displayIO
 , Pretty (..)
-, fsep , hsep, vsep, vcat, hcat
+, fsep, sep, hsep, vsep, vcat, hcat
 , parens, brackets, angles, braces, enclose
 , punctuate, comma, nest
 , empty, text
@@ -13,17 +13,21 @@
 where
 
 import Text.PrettyPrint.Leijen.Text 
-    hiding ( text, (<+>), vcat )
+    hiding ( text, (<+>), vcat, hcat, vsep, hsep, sep, parens )
 import qualified Text.PrettyPrint.Leijen.Text 
 import Data.String ( fromString )
 
 -- class Pretty a where pretty :: a -> Doc
 
-fsep = fillSep
 ($$) = (<$$>)
-x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align y
-vcat = align . Text.PrettyPrint.Leijen.Text.vcat
-
+x <+> y = x Text.PrettyPrint.Leijen.Text.<+> align (group y)
+vcat = align . Text.PrettyPrint.Leijen.Text.vcat . map group
+hcat = align . Text.PrettyPrint.Leijen.Text.hcat . map group
+vsep = align . Text.PrettyPrint.Leijen.Text.vsep . map group
+hsep = align . Text.PrettyPrint.Leijen.Text.hsep . map group
+fsep = align . Text.PrettyPrint.Leijen.Text.fillSep . map group
+sep = align . Text.PrettyPrint.Leijen.Text.sep . map group
+parens = Text.PrettyPrint.Leijen.Text.parens . group
 render :: Doc -> String
 render = show
 
diff --git a/src/TPDB/XTC/Read.hs b/src/TPDB/XTC/Read.hs
--- a/src/TPDB/XTC/Read.hs
+++ b/src/TPDB/XTC/Read.hs
@@ -8,6 +8,7 @@
 -- http://www.haskell.org/haskellwiki/HXT/Practical/
 
 import TPDB.Data
+import TPDB.Data.Attributes
 
 import Text.XML.HXT.Arrow.XmlArrow
 
@@ -19,6 +20,11 @@
 import Control.Arrow.ArrowList
 import Control.Arrow.ArrowTree
 
+import qualified Data.ByteString.Lazy as BS
+import qualified Data.ByteString.Lazy.Char8 as C
+import Text.XML.HXT.IO.GetFILE
+import Text.XML.HXT.Arrow.ReadDocument
+
 atTag tag = deep (isElem >>> hasName tag)
 
 getTerm = getVar <+> getFunApp
@@ -51,6 +57,7 @@
                         , startterm = case stt of
                              [] -> Nothing
                              [x] -> x
+                        , attributes = compute_attributes $ rules rs
                         }
 
 getType = proc x -> do
@@ -101,9 +108,9 @@
     returnA -< Rule { lhs = l, relation = str, rhs = r, top = False }
 
 readProblems :: FilePath -> IO [ Problem Identifier Identifier ]
-readProblems file = do
-    cs <- readFile file
-    runX ( readString [] cs >>> getProblem )
-
-
+readProblems file =
+   runX ( readDocument [] file >>> getProblem )
 
+readProblemsBS :: BS.ByteString -> IO [ Problem Identifier Identifier ]
+readProblemsBS s =
+   runX ( readString [] (C.unpack s) >>> getProblem )
diff --git a/test/attributes.hs b/test/attributes.hs
new file mode 100644
--- /dev/null
+++ b/test/attributes.hs
@@ -0,0 +1,11 @@
+import TPDB.Data
+import TPDB.Pretty
+import TPDB.XTC
+import TPDB.Plain.Write
+
+import Control.Monad ( forM, void )
+
+main = void $ do
+    [ p ] <- readProblems "test/3.15.xml"
+    print $ pretty p
+    print $ pretty $ attributes p
diff --git a/test/read_print_srs.hs b/test/read_print_srs.hs
--- a/test/read_print_srs.hs
+++ b/test/read_print_srs.hs
@@ -2,10 +2,11 @@
 import TPDB.Plain.Read
 import TPDB.Pretty
 
+import Data.ByteString.Lazy as B
 import Control.Monad ( forM, void )
 
 main = void $ do
-    s <- readFile "test/z001.srs"
+    s <- B.readFile "test/z001.srs"
     case srs s of
         Right t -> print $ pretty t
         Left err -> error err
diff --git a/test/read_print_trs.hs b/test/read_print_trs.hs
--- a/test/read_print_trs.hs
+++ b/test/read_print_trs.hs
@@ -2,10 +2,11 @@
 import TPDB.Plain.Read
 import TPDB.Pretty
 
+import Data.ByteString.Lazy as B
 import Control.Monad ( forM, void )
 
 main = void $ do
-    s <- readFile "test/33.trs"
+    s <- B.readFile "test/33.trs"
     case trs s of
         Right t -> print $ pretty t
         Left err -> error err
diff --git a/test/read_print_trs_2.hs b/test/read_print_trs_2.hs
--- a/test/read_print_trs_2.hs
+++ b/test/read_print_trs_2.hs
@@ -2,10 +2,11 @@
 import TPDB.Plain.Read
 import TPDB.Pretty
 
+import Data.ByteString.Lazy as B
 import Control.Monad ( forM, void )
 
 main = void $ do
-    s <- readFile "test/02.trs"
+    s <- B.readFile "test/02.trs"
     case trs s of
         Right t -> print $ pretty t
         Left err -> error err
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 1.2.0
+Version: 1.3.2
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic
@@ -29,12 +29,16 @@
 
 Library
   Build-Depends: base==4.*, hxt, wl-pprint-text, text, mtl,
-    parsec, time, containers, HaXml, filepath, hashable
+    parsec, time, containers, HaXml, filepath, hashable, bytestring
+  if impl(ghc<7.10)
+     build-depends: transformers
+  if impl(ghc<7.10)
+     Extensions: DeriveDataTypeable
   Hs-Source-Dirs: src
   Exposed-Modules:
-    TPDB.Data,     TPDB.Data.Term, TPDB.Data.Xml
+    TPDB.Data,     TPDB.Data.Term, TPDB.Data.Rule, TPDB.Data.Attributes, TPDB.Data.Xml
     -- TPDB.Compress, 
-    TPDB.Convert, TPDB.Input
+    TPDB.Convert, TPDB.Input, TPDB.Input.File, TPDB.Input.Memory
     TPDB.Mirror
     TPDB.DP, TPDB.DP.Graph, TPDB.DP.Transform, TPDB.DP.Unify, TPDB.DP.Usable,  TPDB.DP.TCap,
     TPDB.Pretty, TPDB.Plain.Write,     TPDB.Plain.Read,
@@ -56,19 +60,19 @@
   hs-source-dirs: test 
 
 Test-Suite TRS
-  Build-Depends: base==4.*, tpdb
+  Build-Depends: base==4.*, tpdb, bytestring
   Type: exitcode-stdio-1.0
   main-is: read_print_trs.hs
   hs-source-dirs: test 
 
 Test-Suite TRS_02
-  Build-Depends: base==4.*, tpdb
+  Build-Depends: base==4.*, tpdb, bytestring
   Type: exitcode-stdio-1.0
   main-is: read_print_trs_2.hs
   hs-source-dirs: test 
 
 Test-Suite SRS
-  Build-Depends: base==4.*, tpdb
+  Build-Depends: base==4.*, tpdb, bytestring
   Type: exitcode-stdio-1.0
   main-is: read_print_srs.hs
   hs-source-dirs: test 
@@ -77,4 +81,10 @@
   Build-Depends: base==4.*, tpdb, HaXml, bytestring, pretty
   Type: exitcode-stdio-1.0
   main-is: speed.hs
+  hs-source-dirs: test 
+
+Test-Suite Attributes
+  Build-Depends: base==4.*, tpdb, HaXml, bytestring, pretty
+  Type: exitcode-stdio-1.0
+  main-is: attributes.hs
   hs-source-dirs: test