diff --git a/src/TPDB/ARI.hs b/src/TPDB/ARI.hs
new file mode 100644
--- /dev/null
+++ b/src/TPDB/ARI.hs
@@ -0,0 +1,93 @@
+{-# language OverloadedStrings #-}
+{-   # options_ghc -fdefer-typed-holes #-}
+
+module TPDB.ARI where
+
+import Data.AttoLisp
+import qualified Data.Attoparsec.ByteString as DAB
+import Data.Attoparsec.Number
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Lazy as BSL
+import qualified Data.Text as T
+import qualified Data.HashMap.Strict as M
+import Control.Applicative (many)
+import Control.Monad (guard)
+import TPDB.Data
+import TPDB.Plain.Write
+import TPDB.Pretty
+
+-- writer
+put :: TRS Identifier Identifier -> BSL.ByteString
+put = BSL.concat . map encodeLn . w
+
+encodeLn x = encode x `BSL.snoc` lf
+  where lf = fromIntegral $ fromEnum '\n' -- HACK
+
+w :: TRS Identifier Identifier -> [Lisp]
+w sys =
+  let sym s = Symbol $ name s
+      sig = do
+        s <- signature sys
+        return $ List [ Symbol "fun", sym s
+                 , Number $ I $ fromIntegral $ arity s
+                      ]
+      trm t = case t of
+        Var v -> sym v
+        Node f args -> List $ sym f : map trm args
+      rul = do
+         u <- rules sys
+         return $ List
+               $ [ Symbol "rule", trm (lhs u), trm (rhs u) ]
+               <> case relation u of
+                   Strict -> []
+                   Weak -> [ Symbol ":cost", Number (I 0) ]
+  in  [ List [Symbol "format", Symbol "TRS" ] ]
+      <> sig
+      <> rul
+
+
+-- parser
+
+get :: BS.ByteString -> Either String (TRS Identifier Identifier)
+get s = DAB.parseOnly ( p <* DAB.atEnd ) s
+
+p :: DAB.Parser (TRS Identifier Identifier)
+p = do
+  cl : auses <- many lisp
+  guard $ cl == List [Symbol "format", Symbol "TRS"]
+  let symbolize s0 = maybe s0 id $ do
+        ('|', s1) <- T.uncons s0; (s2, '|') <- T.unsnoc s1; return s2
+      funs = do
+        List [Symbol "fun", Symbol s, Number (I a)] <- auses
+        return (s, mk (fromIntegral a) $ symbolize s)
+      sig = M.fromListWith (error "conflict") funs
+  let rs :: [ Rule (Term Identifier Identifier) ]
+      rs = do
+        List (Symbol "rule" : l : r : trailer) <- auses
+        return $ Rule { lhs = termof sig l
+                      , rhs = termof sig r
+                      , relation = case trailer of
+                          [ ] -> Strict
+                          [ Symbol ":cost", Number (I 0) ]
+                             -> Weak
+                      , top = False
+                      , original_variable = Nothing
+                      }
+  return $ RS
+    { signature = map snd funs
+    , rules = rs
+    , separate = False
+    }
+
+termof :: M.HashMap T.Text Identifier -> Lisp
+  -> Term Identifier Identifier
+termof sig (List (Symbol s : args)) =
+  case M.lookup s sig of
+    Just f | arity f == length args ->
+             Node f $ map (termof sig) args
+termof sig (Symbol s) = case M.lookup s sig of
+  Nothing -> Var $ mk 0 s
+  Just f -> Node f [] -- ?
+        
+                           
+                          
diff --git a/src/TPDB/Input/File.hs b/src/TPDB/Input/File.hs
--- a/src/TPDB/Input/File.hs
+++ b/src/TPDB/Input/File.hs
@@ -2,15 +2,17 @@
 
 import TPDB.Data
 import TPDB.Convert
+import qualified TPDB.ARI
 
 import qualified TPDB.Input.Memory as TIM
 
 import qualified Data.Text.Lazy as T
 import qualified Data.Text.Lazy.IO as T
+import qualified Data.ByteString as BS
 import System.FilePath.Posix ( takeExtension )
 
 -- | read input from file with given name.
--- can have extension .srs, .trs, .xml.
+-- can have extension .srs, .trs, .xml, .ari
 -- unknown extension is considered as .xml, because of 
 -- http://starexec.forumotion.com/t60-restore-file-extension-for-renamed-benchmarks
 
@@ -23,9 +25,17 @@
         Right x -> return x 
         Left err -> error err
 
-getE f = do
-  s <- T.readFile f
-  TIM.get f s
+getE :: FilePath 
+         -> IO (Either String
+                 ( Either (TRS Identifier Identifier) 
+                        ( SRS Identifier ) ) )
+getE f = case takeExtension f of
+  ".ari" -> do
+    s <- BS.readFile f
+    return $ fmap Left $ TPDB.ARI.get s
+  _ ->  do
+    s <- T.readFile f
+    TIM.get f s
 
 get_trs f = do
     x <- get f
diff --git a/src/TPDB/Input/Memory.hs b/src/TPDB/Input/Memory.hs
--- a/src/TPDB/Input/Memory.hs
+++ b/src/TPDB/Input/Memory.hs
@@ -7,12 +7,13 @@
 import TPDB.Data
 import TPDB.Plain.Read
 import TPDB.XTC.Read
+import qualified TPDB.ARI
 
 import qualified Data.Text.Lazy as T
 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)
+-- first arg. is needed to pick the proper parser (SRS, TRS, XTC, ARI)
 get :: String -> T.Text
     -> IO (Either String (Either (TRS Identifier Identifier) (SRS Identifier)))
 get f s = case takeExtension f of
diff --git a/src/TPDB/Pretty.hs b/src/TPDB/Pretty.hs
--- a/src/TPDB/Pretty.hs
+++ b/src/TPDB/Pretty.hs
@@ -53,9 +53,6 @@
 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 ]
-
 -- | WARNING: there is  instance Pretty a => Pretty (Maybe a) in the back-end
 -- but its spec is "Ignore Nothings, print Just contents"
 
diff --git a/test/read_ARI.hs b/test/read_ARI.hs
new file mode 100644
--- /dev/null
+++ b/test/read_ARI.hs
@@ -0,0 +1,12 @@
+import TPDB.Data
+import TPDB.Pretty
+import TPDB.Input.File
+import TPDB.Plain.Write
+
+import Control.Monad ( forM, void )
+
+main = void $ do
+    p <- get_trs "test/01.ari"
+    print $ pretty p
+
+
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,7 +1,7 @@
 Cabal-Version: 3.8
 
 Name: tpdb
-Version: 2.8.6
+Version: 2.9.0
 
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
@@ -20,19 +20,20 @@
 
 Homepage: https://github.com/jwaldmann/haskell-tpdb
 
-tested-with: GHC == 9.12.2
+tested-with: GHC == 9.12.2, GHC == 9.14.1
           
 Extra-Source-Files:
    test/*.xml, test/*.trs ,  test/*.srs, test/*.cpf
 
 Source-Repository head
   Type: git
-  Location: git://github.com/jwaldmann/haskell-tpdb.git
+  Location: https://github.com/jwaldmann/haskell-tpdb
 
 Library
-  Build-Depends: base==4.*,  prettyprinter, text, mtl,
+  Build-Depends: base==4.*,  prettyprinter >= 1.7.2, text, mtl,
     xml-hamlet, xml-conduit, data-default,
-    parsec, time, containers, filepath, hashable, bytestring, exceptions
+    parsec, time, containers, filepath, hashable, bytestring, exceptions,
+    attoparsec,atto-lisp,unordered-containers
   Hs-Source-Dirs: src
   default-language: Haskell2010
   Exposed-Modules:
@@ -47,7 +48,8 @@
     TPDB.XTC,  TPDB.XTC.Read, TPDB.XTC.Write, TPDB.Xml, 
     TPDB.CPF.Proof.Write,  TPDB.CPF.Proof.Read,  
     TPDB.CPF.Proof.Xml,  
-    TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util
+    TPDB.CPF.Proof.Type, TPDB.CPF.Proof.Util,
+    TPDB.ARI
 
 Executable plain2xtc
   build-depends: base==4.*, tpdb, bytestring
@@ -150,6 +152,13 @@
   Build-Depends: base==4.*, tpdb
   Type: exitcode-stdio-1.0
   main-is: read_complex.hs
+  hs-source-dirs: test 
+  default-language: Haskell2010
+
+Test-Suite read-ARI
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: read_ARI.hs
   hs-source-dirs: test 
   default-language: Haskell2010