diff --git a/plain2xtc.hs b/plain2xtc.hs
new file mode 100644
--- /dev/null
+++ b/plain2xtc.hs
@@ -0,0 +1,13 @@
+import qualified TPDB.Data as D
+import qualified TPDB.Input as I
+import qualified TPDB.XTC as X
+import System.Environment (getArgs)
+import qualified Data.ByteString.Lazy as L
+
+main = do
+  [f] <- getArgs
+  s <- I.get_trs f
+  L.putStrLn $ X.renderLBS X.def $ X.document
+    $ D.Problem { D.type_ = D.Termination, D.trs = s
+                , D.strategy = Just D.Full
+                }
diff --git a/src/TPDB/CPF/Proof/Read.hs b/src/TPDB/CPF/Proof/Read.hs
--- a/src/TPDB/CPF/Proof/Read.hs
+++ b/src/TPDB/CPF/Proof/Read.hs
@@ -39,12 +39,28 @@
     returnA -< CertificationProblem 
         { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin }
 
-getInput = getTerminationInput <+> getComplexityInput
+getInput = getTerminationInput <+> getComplexityInput <+> getACTerminationInput
 
 getTerminationInput = hasName "input" >>> proc x -> do
     trsI <- getTrsInput <<< getChild "trsInput" -< x    
     returnA -< TrsInput $ RS { rules = trsI, separate = False }
 
+getACTerminationInput = hasName "input" >>> proc x -> do
+    acrs <- getChild "acRewriteSystem" -< x
+    trsI <- getTrsInput -< acrs
+    as <- listA getSymbol <<< getChild "Asymbols" -< acrs
+    cs <- listA getSymbol <<< getChild "Csymbols" -< acrs
+    returnA -< ACRewriteSystem
+      { trsinput_trs = RS { rules = trsI, separate = False }
+      , asymbols = as
+      , csymbols = cs
+      }
+
+getSymbol = proc x -> do
+  s <- getText <<< gotoChild "name" -< x
+  returnA -< mk 0 s
+
+
 getComplexityInput = hasName "input" >>> proc x -> do
     y <- getChild "complexityInput" -< x
     trsI <- getTrsInput <<< getChild "trsInput" -< y
@@ -80,6 +96,7 @@
        <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )
        <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )
        <+> getDummy "complexityProof" ( ComplexityProof undefined )
+       <+> getDummy "acTerminationProof" ( ACTerminationProof undefined )
 
 getDummy t c = proc x -> do 
     getChild t -< x
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
@@ -1,6 +1,7 @@
 {-# language StandaloneDeriving #-}
 {-# language ExistentialQuantification #-}
 {-# language DeriveDataTypeable #-}
+{-# language OverloadedStrings #-}
 
 -- | internal representation of CPF termination proofs,
 -- see <http://cl-informatik.uibk.ac.at/software/cpf/>
@@ -15,7 +16,9 @@
 where
 
 import TPDB.Data
+import TPDB.Plain.Write ()
 import Data.Typeable
+import TPDB.Pretty
 
 import Text.XML.HaXml.XmlContent.Haskell hiding ( text )
 
@@ -46,13 +49,35 @@
                       , complexityMeasure :: ComplexityMeasure
                       , complexityClass :: ComplexityClass      
                       }
+    | ACRewriteSystem { trsinput_trs :: TRS Identifier Identifier
+                      , asymbols :: [ Identifier ]
+                      , csymbols :: [ Identifier ]
+                      }
    deriving ( Typeable, Eq )      
 
+instance Pretty CertificationProblemInput where
+  pretty cpi = case cpi of
+    TrsInput { } ->
+      "TrsInput" <+> vcat [ "trs" <+> pretty (trsinput_trs cpi) ]
+    ComplexityInput { } ->
+      "ComplexityInput" <+> vcat
+         [ "trs" <+> pretty (trsinput_trs cpi)
+         , "measure" <+> text (show $ complexityMeasure cpi )
+         , "class"   <+> text (show $ complexityClass   cpi )
+         ]
+    ACRewriteSystem { } ->
+      "ACRewritesystem" <+> vcat
+         [ "trs" <+> pretty (trsinput_trs cpi)
+         , "asymbols" <+> text (show $ asymbols cpi )
+         , "csymbols" <+> text (show $ csymbols cpi )
+         ]
+
 data Proof = TrsTerminationProof TrsTerminationProof
            | TrsNonterminationProof TrsNonterminationProof
            | RelativeTerminationProof TrsTerminationProof
            | RelativeNonterminationProof TrsNonterminationProof
            | ComplexityProof ComplexityProof
+           | ACTerminationProof ACTerminationProof
    deriving ( Typeable, Eq )
 
 data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) 
@@ -68,14 +93,14 @@
 data ComplexityMeasure 
      = DerivationalComplexity
      | RuntimeComplexity
-    deriving ( Typeable, Eq )
+    deriving ( Typeable, Eq, Show )
 
 data ComplexityClass = 
      ComplexityClassPolynomial { degree :: Int } 
      -- ^ it seems the degree must always be given in CPF,
      -- although the category spec also allows "POLY"
      -- http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/rules.php
-    deriving ( Typeable, Eq )
+    deriving ( Typeable, Eq, Show )
 
 data TrsNonterminationProof = TrsNonterminationProofFIXME ()
     deriving ( Typeable, Eq )
@@ -254,3 +279,7 @@
                          , afeFilter :: Either Int [Int]
                          }
      deriving ( Typeable, Eq )
+
+data ACTerminationProof = ACTerminationProofFIXME ()
+    deriving ( Typeable, Eq )
+
diff --git a/src/TPDB/Convert.hs b/src/TPDB/Convert.hs
--- a/src/TPDB/Convert.hs
+++ b/src/TPDB/Convert.hs
@@ -6,25 +6,27 @@
 srs2trs :: SRS Identifier -> TRS Identifier Identifier
 srs2trs s = s { separate = False
               , rules = map convert_srs_rule $ rules s
-              }  
+              , signature = map (set_arity 1) $ signature s
+              }
 
-convert_srs_rule u = 
+set_arity a s = s { arity = a }
+
+convert_srs_rule u =
     let v = mk 0 "x"
-        set_arity a s = s { arity = a }
         handle = unspine v . map (set_arity 1)
     in  u { lhs = handle $ lhs u
-          , rhs = handle $ rhs u        
-          } 
-                  
+          , rhs = handle $ rhs u
+          }
+
 trs2srs :: Eq v => TRS v s -> Maybe ( SRS s )
 trs2srs t = do
-    us <- forM ( rules t ) convert_trs_rule 
+    us <- forM ( rules t ) convert_trs_rule
     return $ t { separate = True , rules = us }
 
 convert_trs_rule u = do
       ( left_spine, left_base ) <- spine $ lhs u
       ( right_spine, right_base ) <- spine $ rhs u
-      guard $ left_base == right_base     
+      guard $ left_base == right_base
       return $ u { lhs = left_spine, rhs = right_spine }
 
 unspine :: v -> [s] -> Term v s
@@ -36,6 +38,6 @@
 spine t = case t of
     Node f args -> do
       [ arg ] <- return args
-      ( sp, base ) <- spine arg 
+      ( sp, base ) <- spine arg
       return ( f : sp, base )
-    Var v -> return ( [] , v ) 
+    Var v -> 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
@@ -22,6 +22,9 @@
             [] -> pretty f 
             _  -> pretty f <+> ( parens $ fsep $ punctuate comma $ map pretty xs )
 
+class PrettyTerm a where 
+    prettyTerm :: a -> Doc ann
+
 instance PrettyTerm a => Pretty ( Rule a ) where
     pretty u = sep [ prettyTerm $ lhs u
                    , ( case relation u of 
@@ -31,9 +34,6 @@
                    -- FIXME: implement "top" annotation
                      ) <+> prettyTerm ( rhs u )
                    ]
-
-class PrettyTerm a where 
-    prettyTerm :: a -> Doc
 
 instance Pretty s => PrettyTerm [s] where    
     prettyTerm xs = hsep $ map pretty xs
diff --git a/src/TPDB/Pretty.hs b/src/TPDB/Pretty.hs
--- a/src/TPDB/Pretty.hs
+++ b/src/TPDB/Pretty.hs
@@ -1,62 +1,63 @@
-module TPDB.Pretty 
+{-# language NoMonomorphismRestriction #-}
 
-( Doc, SimpleDoc
-, render, renderCompact, displayIO
-, Pretty (..)
+module TPDB.Pretty
+
+( Doc, Pretty (..)
+, render, renderWide, renderCompact, renderPretty
+, displayIO
 , fsep, sep, hsep, vsep, vcat, hcat
 , parens, brackets, angles, braces, enclose
-, punctuate, comma, nest
-, empty, text
-, (<>), (<+>), ($$)
+, encloseSep, punctuate, comma, nest, list, tupled
+  , module Data.Monoid, empty
+, text
+, (<+>), ($$)
+, indent, nest, hang
 )
 
 where
 
-import Text.PrettyPrint.Leijen.Text 
-    hiding ( text, (<+>), vcat, hcat, vsep, hsep, sep, parens )
-import qualified Text.PrettyPrint.Leijen.Text 
+import Data.Text.Prettyprint.Doc
+  ( Doc, Pretty(..), comma
+  , punctuate, encloseSep, align, parens, braces, angles, brackets, nest, enclose
+  , list, tupled
+  , indent, nest, hang
+  )
+import qualified Data.Text.Prettyprint.Doc as D
+import qualified Data.Text.Prettyprint.Doc.Render.Text as T
+
 import Data.String ( fromString )
+import Data.Monoid (mempty, (<>))
 
+empty :: Doc ann 
+empty = mempty
+
 -- class Pretty a where pretty :: a -> Doc
 
-($$) = (<$$>)
-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
+x $$ y = D.vcat [x,y]
+x <+> y = x D.<+> align y
+vcat = align . D.vcat
+hcat = align . D.hcat
+vsep = align . D.vsep
+hsep = align . D.hsep
+fsep = align . D.fillSep
+sep = align . D.sep
 
-text :: String -> Doc
-text = fromString
+render = T.renderLazy . renderPretty
 
-{-
+renderPretty = D.layoutPretty D.defaultLayoutOptions
+renderCompact = D.layoutCompact
+renderWide = D.layoutSmart $ D.LayoutOptions { D.layoutPageWidth = D.Unbounded }
+displayIO = T.renderIO
 
-instance Pretty Int where pretty = text . show
 
-instance ( Pretty a, Pretty b ) => Pretty (a,b) where
-    pretty (x,y) = parens $ fsep $ punctuate comma [ pretty x, pretty y ]
-
-instance ( Pretty a, Pretty b, Pretty c ) => Pretty (a,b,c) where
-    pretty (x,y,z) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z ]
--}
+text :: String -> D.Doc ann
+text = fromString
 
 instance ( Pretty a, Pretty b, Pretty c, Pretty d ) => Pretty (a,b,c,d) where
     pretty (x,y,z,u) = parens $ fsep $ punctuate comma [ pretty x, pretty y, pretty z, pretty u ]
 
-{-
-instance Pretty a => Pretty [a]  where
-    pretty xs = brackets $ fsep $ punctuate comma $ map pretty xs
-
-instance Pretty a => Pretty (Maybe a) where
-    pretty m = case m of
-        Nothing -> text "Nothing"
-        Just x -> text "Just" <+> pretty x -- FIXME: parens missing
--}
+-- | WARNING: there is  instance Pretty a => Pretty (Maybe a) in the back-end
+-- but its spec is "Ignore Nothings, print Just contents"
 
 instance ( Pretty a, Pretty b ) => Pretty (Either a b) where
     pretty (Left x) = text "Left" <+> parens (pretty x)
diff --git a/src/TPDB/XTC.hs b/src/TPDB/XTC.hs
--- a/src/TPDB/XTC.hs
+++ b/src/TPDB/XTC.hs
@@ -2,6 +2,7 @@
 
 ( module TPDB.Data
 , module TPDB.XTC.Read
+, module TPDB.XTC.Write
 )
 
 
@@ -9,4 +10,6 @@
 
 import TPDB.Data
 import TPDB.XTC.Read
+import TPDB.XTC.Write
+
 
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
@@ -58,7 +58,7 @@
                         , type_ = ty
                         , startterm = case stt of
                              [] -> Nothing
-                             [x] -> x
+                             [x] -> Just x
                         , attributes = compute_attributes $ rules rs
                         }
 
@@ -70,15 +70,17 @@
 getStrategy = proc x -> do
     cs <- getText <<< getChildren -< x
     returnA -< case cs of
-        "FULL" -> Just Full
+        "FULL"      -> Just Full
+        "INNERMOST" -> Just Innermost
+        "OUTERMOST" -> Just Outermost
 
 getStartterm = ( proc x -> do
         getChild "constructor-based" -< x
-        returnA -< Just Startterm_Constructor_based
+        returnA -< Startterm_Constructor_based
    ) <+>  ( proc x -> do
         getChild "full" -< x
-        returnA -< Just Startterm_Full
-   ) <+> ( proc x -> do returnA -< Nothing )
+        returnA -< Startterm_Full
+   ) 
 
 getTRS = proc x -> do
     sig <- getSignature -< x
diff --git a/src/TPDB/XTC/Write.hs b/src/TPDB/XTC/Write.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/XTC/Write.hs
@@ -0,0 +1,62 @@
+{-# language OverloadedStrings #-}
+{-# language QuasiQuotes #-}
+
+module TPDB.XTC.Write
+
+( document
+, writeFile, renderLBS, renderText, def
+)
+
+where
+
+import qualified TPDB.Data as D
+import qualified Data.Map as M
+
+import qualified Data.Text as T
+import qualified Text.XML as X
+import Prelude hiding (writeFile)
+import Text.XML (writeFile,renderLBS,renderText)
+import Text.Hamlet.XML
+import Data.Default (def)
+
+document :: D.Problem D.Identifier D.Identifier -> X.Document
+document p = X.Document (X.Prologue [] Nothing []) root [] where
+    root = X.Element "problem"
+      (M.fromList [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")
+                  ,("type","termination")
+                  ,("xsi:noNamespaceSchemaLocation","http://dev.aspsimon.org/xtc.xsd")
+                  ])
+      [xml|
+<trs>^{trs $ D.trs p}
+$maybe s <- D.strategy p
+  <strategy>^{strategy s}
+|]
+
+strategy s = case s of
+  D.Full -> [xml|FULL|]
+
+trs :: D.TRS D.Identifier D.Identifier -> [X.Node]
+trs rs = [xml|
+<rules>
+  $forall u <- D.rules rs
+    <rule>
+      <lhs>^{term $ D.lhs u}
+      <rhs>^{term $ D.rhs u}
+<signature>
+  $forall f <- D.signature rs
+    <funcsym>
+      <name>#{T.pack $ show f}
+      <arity>#{T.pack $ show $ D.arity f}
+|]
+
+term :: D.Term D.Identifier D.Identifier -> [X.Node]
+term t = case t of
+  D.Var v -> [xml|
+<var>#{T.pack $ show v}
+|]
+  D.Node f args -> [xml|
+<funapp>
+  <name>#{T.pack $ show f}
+  $forall arg <- args
+     <arg>^{term arg}
+|]
diff --git a/src/TPDB/Xml/Pretty.hs b/src/TPDB/Xml/Pretty.hs
--- a/src/TPDB/Xml/Pretty.hs
+++ b/src/TPDB/Xml/Pretty.hs
@@ -36,12 +36,15 @@
 --import Char (isSpace)
 
 -- import Text.PrettyPrint.HughesPJ
-import TPDB.Pretty hiding ( text )
+import TPDB.Pretty hiding ( text, Doc )
+import qualified TPDB.Pretty as P
 
 import Text.XML.HaXml.Types
 import Text.XML.HaXml.Namespaces
 
 import Data.String ( fromString )
+
+type Doc = P.Doc ()
 
 text = fromString
 
diff --git a/test/parse_ac.hs b/test/parse_ac.hs
new file mode 100644
--- /dev/null
+++ b/test/parse_ac.hs
@@ -0,0 +1,12 @@
+import TPDB.Data
+import TPDB.Pretty
+import TPDB.XTC
+import TPDB.Plain.Write
+
+import Control.Monad ( forM, void )
+
+main = void $ do
+    [ p ] <- readProblems "test/AC28.xml"
+    print $ pretty p
+    print $ full_signature p
+
diff --git a/test/read_complex.hs b/test/read_complex.hs
new file mode 100644
--- /dev/null
+++ b/test/read_complex.hs
@@ -0,0 +1,12 @@
+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.39.xml"
+    print $ pretty p
+
+
diff --git a/test/read_cpf.hs b/test/read_cpf.hs
new file mode 100644
--- /dev/null
+++ b/test/read_cpf.hs
@@ -0,0 +1,10 @@
+import qualified TPDB.CPF.Proof.Type as CPF
+import qualified TPDB.CPF.Proof.Read as CPF
+import TPDB.Pretty
+import TPDB.Plain.Write
+
+main = do
+    s <- readFile "test/AC28.cpf"
+    [p] <- CPF.readCP_with_tracelevel 0 s
+    print $ pretty $ CPF.input p
+
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
@@ -4,9 +4,10 @@
 
 import Data.ByteString.Lazy as B
 import Control.Monad ( forM, void )
+import System.IO (stdout)
 
 main = void $ do
     s <- B.readFile "test/33.trs"
     case trs s of
-        Right t -> print $ pretty t
+        Right t -> displayIO stdout $ renderWide $ 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.3.3
+Version: 1.5.2
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic
@@ -28,8 +28,9 @@
 --   test/3.15.xml, test/33.trs ,  test/z001.srs
 
 Library
-  Build-Depends: base==4.*, hxt, wl-pprint-text, text, mtl,
-    parsec, time, containers, HaXml, filepath, hashable, bytestring
+  Build-Depends: base==4.*, hxt, prettyprinter, text, mtl,
+    HaXml, xml-hamlet, xml-conduit, data-default,
+    parsec, time, containers, filepath, hashable, bytestring
   if impl(ghc<7.10)
      build-depends: transformers
   if impl(ghc<7.10)
@@ -42,13 +43,17 @@
     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,
-    TPDB.XTC,  TPDB.XTC.Read, TPDB.Xml, 
+    TPDB.XTC,  TPDB.XTC.Read, TPDB.XTC.Write, TPDB.Xml, 
     TPDB.Xml.Pretty,
     -- TPDB.Rainbow.Proof.Xml,  TPDB.Rainbow.Proof.Type
     TPDB.CPF.Proof.Write,  TPDB.CPF.Proof.Read,  
     TPDB.CPF.Proof.Xml,  
     TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util
 
+Executable plain2xtc
+  build-depends: base==4.*, tpdb, bytestring
+  main-is: plain2xtc.hs
+
 -- Executable Compressor
 --     Main-is: Compressor.hs
 --    Build-depends: base==4.*, containers >= 0.5, directory, wl-pprint-text, hxt, parsec, hashable
@@ -93,5 +98,29 @@
   Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_print_xml_theory.hs
+  hs-source-dirs: test 
+
+Test-Suite CPF-AC
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: read_cpf.hs
+  hs-source-dirs: test 
+
+Test-Suite Parse-AC
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: parse_ac.hs
+  hs-source-dirs: test 
+
+Test-Suite read-cpf
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: read_cpf.hs
+  hs-source-dirs: test 
+
+Test-Suite read-complex
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: read_complex.hs
   hs-source-dirs: test