diff --git a/src/TPDB/Data.hs b/src/TPDB/Data.hs
--- a/src/TPDB/Data.hs
+++ b/src/TPDB/Data.hs
@@ -3,7 +3,10 @@
 -- A termination problem is @Problem v s@. This contains a rewrite system plus extra
 -- information (strategy, theory, etc.)
 
-{-# language DeriveDataTypeable #-}
+{-# language DeriveDataTypeable,
+    FlexibleInstances, FlexibleContexts,
+    MultiParamTypeClasses, TypeFamilies
+#-}
 
 module TPDB.Data 
 
@@ -22,9 +25,11 @@
 import Data.Typeable
 import Control.Monad ( guard )
 
+import Data.Void
 import Data.Hashable
 import Data.Function (on)
 import qualified Data.Text as T
+import qualified Data.Set as S
 
 data Identifier =
      Identifier { _identifier_hash :: ! Int
@@ -42,7 +47,18 @@
 mk a n = Identifier { _identifier_hash = hash (a,n)
                     , arity = a, name = n }
 
+class Ord (Var t) => Variables t where
+  type Var t
+  variables :: t -> S.Set (Var t)
 
+instance Ord v => Variables (Term v c) where
+  type Var (Term v c) = v
+  variables = vars
+
+instance Variables [c] where
+  type Var [c] = ()
+  variables _ = S.empty
+
 ---------------------------------------------------------------------
 
 -- | according to XTC spec
@@ -87,6 +103,19 @@
 type TRS v s = RS s ( Term v s )
 
 type SRS s = RS s [ s ]
+
+instance Variables r => Variables (Rule r) where
+  type Var (Rule r) = Var r
+  variables u =
+    S.unions [ variables (lhs u), variables (rhs u) ]
+
+instance Ord v => Variables (TRS v s) where
+  type Var (TRS v s) = v
+  variables sys = S.unions $ map variables $ rules sys
+
+instance Variables (SRS s) where
+  type Var (SRS s) = Void
+  variables sys = S.empty
 
 data Problem v s =
      Problem { type_ :: Type
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
@@ -177,3 +177,4 @@
 -- | list of variables (in pre-order, with duplicates)
 voccs :: Term v c -> [ v ]
 voccs t = do ( p, Var v ) <- positions t ; return v
+
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
@@ -3,6 +3,7 @@
 
 {-# language FlexibleContexts #-}
 {-# language OverloadedStrings #-}
+{-# language UndecidableInstances #-}
 
 module TPDB.Plain.Write where
 
@@ -11,6 +12,7 @@
 
 import Data.List ( nub )
 import Data.String ( fromString )
+import qualified Data.Set as S
 import qualified Data.Text as T
 
 instance Pretty Identifier where
@@ -42,19 +44,22 @@
 instance ( Pretty v, Pretty s ) => PrettyTerm ( Term v s ) where
     prettyTerm = pretty
 
-instance ( Pretty s, PrettyTerm r ) => Pretty ( RS s r ) where
+instance ( Pretty s, PrettyTerm r, Variables (RS s r)
+  , Pretty (Var (RS s r)))
+  => Pretty ( RS s r ) where
     pretty sys = vcat 
-        [ parens $ "RULES" <+>
+        [ let vs = S.toList $ variables sys
+	  in if null vs
+	     then empty   
+	     else parens $ "VAR" <+> vcat (map pretty vs)
+	, parens $ "RULES" <+>
           vcat ( ( if separate sys then punctuate comma else id )
                  $ map pretty $ rules sys 
                )
-        -- FIXME: variables are not shown (and it is impossible to compute
-        -- them here, this is actually a TPDB format design error, 
-        -- since variables should be local (per rule), not global)
         -- FIXME: output strategy, theory
         ]
 
-instance ( Pretty s, Pretty r ) => Pretty ( Problem s r ) where
+instance ( Pretty s, Pretty r, Variables (Term s r) ) => Pretty ( Problem s r ) where
     pretty p = vcat
        [ pretty $ trs p 
        , case strategy p of  
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
@@ -1,6 +1,8 @@
 -- | construct data object from XML tree.
 
-{-# language NoMonomorphismRestriction, PatternSignatures, OverloadedStrings #-}
+{-# language NoMonomorphismRestriction, PatternSignatures, OverloadedStrings
+  , BangPatterns
+#-}
 
 
 module TPDB.XTC.Read (readProblemF, readProblemT ) where
@@ -26,11 +28,12 @@
     ps -> error "input contains more than one XTC problem"
 
 readProblemT :: LT.Text -> Either SomeException (Problem Identifier Identifier)
-readProblemT t = do
-  [p] <- ( getProblem . fromDocument ) <$> Text.XML.parseText Text.XML.def t
-  return p
+readProblemT t = case ( getProblem . fromDocument ) <$> Text.XML.parseText Text.XML.def t of
+  Right [ p ] -> Right p
+  Left ex -> Left ex
 
 
+getProblem :: Cursor -> [ Problem Identifier Identifier ]
 getProblem = element "problem" >=> \ c -> do
     let ! ty = case c $| attribute "type" of
          [ "termination" ] -> Termination
diff --git a/srs2trs.hs b/srs2trs.hs
new file mode 100644
--- /dev/null
+++ b/srs2trs.hs
@@ -0,0 +1,15 @@
+{-# language LambdaCase #-}
+
+module Main where
+
+import TPDB.Input (get_srs)
+import TPDB.Pretty
+import TPDB.Plain.Write
+import TPDB.Convert (srs2trs)
+import System.IO (stdout)
+import System.Environment
+
+main = getArgs >>= \ case
+  [ fp ] -> displayIO stdout . renderWide . pretty . srs2trs =<< get_srs fp
+  
+  
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,6 @@
 Name: tpdb
-Version: 2.1.1
+Version: 2.2.0
+
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic
@@ -47,6 +48,10 @@
 Executable plain2xtc
   build-depends: base==4.*, tpdb, bytestring
   main-is: plain2xtc.hs
+
+Executable srs2trs
+  build-depends: base==4.*, tpdb, bytestring
+  main-is: srs2trs.hs
 
 -- Executable Compressor
 --     Main-is: Compressor.hs