diff --git a/TPDB/CPF/Proof/Read.hs b/TPDB/CPF/Proof/Read.hs
--- a/TPDB/CPF/Proof/Read.hs
+++ b/TPDB/CPF/Proof/Read.hs
@@ -28,21 +28,24 @@
 -}
 
 readCP :: String -> IO [ CertificationProblem ]
-readCP s = runX ( X.withTraceLevel 0 $ readString [] s >>> getCP )
+readCP = readCP_with_tracelevel 0
 
-getCP = atTag "certificationProblem" >>> proc x -> do
+readCP_with_tracelevel l s = runX ( X.withTraceLevel l $ readString [] s >>> getCP )
+
+getCP = getChild "certificationProblem" >>> proc x -> do
     inp <- getInput <<< getChild "input" -< x
     pro <- getProof <<< getChild "proof" -< x
     ver <- getText <<< gotoChild "cpfVersion" -< x
-    returnA -< CertificationProblem { input = inp, proof = pro, cpfVersion = "2.2" }
+    returnA -< CertificationProblem 
+        { input = inp, proof = pro, cpfVersion = ver, origin = ignoredOrigin }
 
 getInput = getTerminationInput <+> getComplexityInput
 
-getTerminationInput = atTag "input" >>> proc x -> do
+getTerminationInput = hasName "input" >>> proc x -> do
     trsI <- getTrsInput <<< getChild "trsInput" -< x    
     returnA -< TrsInput $ RS { rules = trsI, separate = False }
 
-getComplexityInput = atTag "input" >>> proc x -> do
+getComplexityInput = hasName "input" >>> proc x -> do
     y <- getChild "complexityInput" -< x
     trsI <- getTrsInput <<< getChild "trsInput" -< y
     cm <- getComplexityMeasure -< y
@@ -73,12 +76,13 @@
     returnA -< str
 
 getProof = getDummy "trsTerminationProof" ( TrsTerminationProof undefined )
-       <+> getDummy "trsNonTerminationProof" ( TrsNonterminationProof undefined )
+       <+> getDummy "trsNonterminationProof" ( TrsNonterminationProof undefined )
        <+> getDummy "relativeTerminationProof" ( RelativeTerminationProof undefined )
-       <+> getDummy "relativeNonTerminationProof" ( RelativeNonterminationProof undefined )
+       <+> getDummy "relativeNonterminationProof" ( RelativeNonterminationProof undefined )
        <+> getDummy "complexityProof" ( ComplexityProof undefined )
 
-getDummy t c = atTag t >>> proc x -> do
+getDummy t c = proc x -> do 
+    getChild t -< x
     returnA -< c 
 
 getRules str = proc x -> do
@@ -109,5 +113,5 @@
 getChild tag = proc x -> do
     returnA <<< hasName tag <<< isElem <<< getChildren -< x
 
-atTag tag = deep (isElem >>> hasName tag)
+
 
diff --git a/TPDB/CPF/Proof/Type.hs b/TPDB/CPF/Proof/Type.hs
--- a/TPDB/CPF/Proof/Type.hs
+++ b/TPDB/CPF/Proof/Type.hs
@@ -1,4 +1,6 @@
-{-# OPTIONS -fglasgow-exts #-}
+{-# language StandaloneDeriving #-}
+{-# language ExistentialQuantification #-}
+{-# language DeriveDataTypeable #-}
 
 -- | internal representation of CPF termination proofs,
 -- see <http://cl-informatik.uibk.ac.at/software/cpf/>
@@ -23,13 +25,18 @@
                           , proof :: Proof 
                           , origin :: Origin  
                           }  
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
-data Origin = ProofOrigin Tool 
-    deriving Typeable
-data Tool = Tool { name :: String , version :: String } 
-    deriving Typeable
+data Origin = ProofOrigin { tool :: Tool }
+    deriving ( Typeable, Eq )
 
+ignoredOrigin = ProofOrigin { tool = Tool "ignored" "ignored"  }
+
+data Tool = Tool { name :: String 
+                 , version :: String
+                 } 
+    deriving ( Typeable, Eq )
+
 data CertificationProblemInput 
     = TrsInput { trsinput_trs :: TRS Identifier Identifier }
       -- ^ this is actually not true, since instead of copying from XTC,
@@ -39,38 +46,39 @@
                       , complexityMeasure :: ComplexityMeasure
                       , complexityClass :: ComplexityClass      
                       }
-   deriving ( Typeable )      
+   deriving ( Typeable, Eq )      
 
 data Proof = TrsTerminationProof TrsTerminationProof
            | TrsNonterminationProof TrsNonterminationProof
            | RelativeTerminationProof TrsTerminationProof
            | RelativeNonterminationProof TrsNonterminationProof
            | ComplexityProof ComplexityProof
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
-data DPS = forall s . ( XmlContent s , Typeable s ) 
+data DPS = forall s . ( XmlContent s , Typeable s, Eq s ) 
         => DPS [ Rule (Term Identifier s) ]
    deriving ( Typeable )
 
+instance Eq DPS where x == y = error "instance Eq DPS"
 
 
 data ComplexityProof = ComplexityProofFIXME ()
-    deriving ( Typeable )
+    deriving ( Typeable, Eq )
 
 data ComplexityMeasure 
      = DerivationalComplexity
      | RuntimeComplexity
-    deriving ( Typeable )
+    deriving ( Typeable, Eq )
 
 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 ( Eq, Typeable )
+    deriving ( Typeable, Eq )
 
 data TrsNonterminationProof = TrsNonterminationProofFIXME ()
-    deriving ( Typeable )
+    deriving ( Typeable, Eq )
 
 data TrsTerminationProof 
      = RIsEmpty
@@ -90,10 +98,10 @@
      | StringReversal { trs :: TRS Identifier Identifier
                       , trsTerminationProof :: TrsTerminationProof  
                       }  
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Model = FiniteModel Int [Interpret]
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
        
 data DpProof = PIsEmpty  
              | RedPairProc { rppOrderingConstraintProof :: OrderingConstraintProof
@@ -112,53 +120,53 @@
                           , ulpTrs :: DPS
                           , ulpDpProof :: DpProof
                           }
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data DepGraphComponent =
      DepGraphComponent { dgcRealScc :: Bool
                        , dgcDps :: DPS
                        , dgcDpProof :: DpProof
                        }
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data OrderingConstraintProof = OCPRedPair RedPair
-                             deriving ( Typeable )
+                             deriving ( Typeable, Eq )
 
 data RedPair = RPInterpretation Interpretation
              | RPPathOrder      PathOrder
-             deriving ( Typeable )
+             deriving ( Typeable, Eq )
 
 data Interpretation =
      Interpretation { interpretation_type :: Interpretation_Type
                     , interprets :: [ Interpret  ]
                     }
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Interpretation_Type = 
    Matrix_Interpretation { domain :: Domain, dimension :: Int
                          , strictDimension :: Int
                          }
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Domain = Naturals 
             | Rationals Rational
             | Arctic Domain
             | Tropical Domain
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Interpret = Interpret 
     { symbol :: Symbol , arity :: Int , value :: Value }
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Value = Polynomial    Polynomial
            | ArithFunction ArithFunction
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data Polynomial = Sum [ Polynomial ]
                 | Product [ Polynomial ]
                 | Polynomial_Coefficient Coefficient
                 | Polynomial_Variable String
-   deriving ( Typeable )
+   deriving ( Typeable, Eq )
 
 data ArithFunction = AFNatural  Integer
                    | AFVariable Integer
@@ -167,39 +175,41 @@
                    | AFMin      [ArithFunction]
                    | AFMax      [ArithFunction]
                    | AFIfEqual  ArithFunction ArithFunction ArithFunction ArithFunction
-                   deriving ( Typeable )
+                   deriving ( Typeable, Eq )
 
 data Symbol = SymName  Identifier
             | SymSharp Symbol
             | SymLabel Symbol Label
-            deriving ( Typeable )
+            deriving ( Typeable, Eq )
 
 data Label = LblNumber [Integer]
            | LblSymbol [Symbol]
-           deriving ( Typeable )
+           deriving ( Typeable, Eq )
 
 data Coefficient = Vector [ Coefficient ]
            | Matrix [ Coefficient ]
-           | forall a . XmlContent a => Coefficient_Coefficient a
+           | forall a . (Eq a, XmlContent a ) => Coefficient_Coefficient a
    deriving ( Typeable )
 
+instance Eq Coefficient where x == y = error "instance Eq Coefficient"
+
 data Exotic = Minus_Infinite | E_Integer Integer | E_Rational Rational | Plus_Infinite
-   deriving Typeable
+   deriving ( Typeable, Eq )
 
 class ToExotic a where toExotic :: a -> Exotic
 
 data PathOrder = PathOrder [PrecedenceEntry] [ArgumentFilterEntry]
-               deriving Typeable
+               deriving ( Typeable, Eq )
 
 data PrecedenceEntry = PrecedenceEntry { peSymbol     :: Symbol
                                        , peArity      :: Int
                                        , pePrecedence :: Integer
                                        }
-                     deriving Typeable
+                     deriving ( Typeable, Eq )
 
 data ArgumentFilterEntry = 
      ArgumentFilterEntry { afeSymbol :: Symbol
                          , afeArity  :: Int
                          , afeFilter :: Either Int [Int]
                          }
-     deriving Typeable
+     deriving ( Typeable, Eq )
diff --git a/TPDB/CPF/Proof/Write.hs b/TPDB/CPF/Proof/Write.hs
--- a/TPDB/CPF/Proof/Write.hs
+++ b/TPDB/CPF/Proof/Write.hs
@@ -12,7 +12,7 @@
 
 import Text.XML.HaXml.Types (QName (..) )
 import Text.XML.HaXml.XmlContent.Haskell hiding ( element, many )
-import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..) )
+import Text.XML.HaXml.Types ( EncodingDecl(..), emptyST, XMLDecl(..), Misc (PI) )
 
 import TPDB.Xml 
 import TPDB.Data.Xml 
@@ -30,7 +30,8 @@
 tox :: CertificationProblem -> Document ()
 tox p = 
     let xd = XMLDecl "1.0" ( Just $ EncodingDecl "UTF-8" ) Nothing 
-        pro = Prolog ( Just xd ) [] Nothing []
+        style = PI ("xml-stylesheet", "type=\"text/xsl\" href=\"cpfHTML.xsl\"")
+        pro = Prolog ( Just xd ) [] Nothing [style]
         [ CElem e _ ] = toContents p
     in  Document pro emptyST e []
 
@@ -85,8 +86,14 @@
 instance XmlContent Proof where
    parseContents = error "parseContents not implemented"
 
-   toContents p = case p of
+   toContents p = 
+     let missing t = rmkel t $ rmkel "missing-toContents-instance" [] 
+     in  case p of
        TrsTerminationProof p -> toContents p
+       TrsNonterminationProof p -> missing "TrsNonterminationProof"
+       RelativeTerminationProof p -> missing "RelativeTerminationProof"
+       RelativeNonterminationProof p -> missing "RelativeNonterminationProof"
+       ComplexityProof p -> missing "ComplexityProof"
 
 instance XmlContent DPS where
    parseContents = error "parseContents not implemented"
diff --git a/TPDB/DP/Unify.hs b/TPDB/DP/Unify.hs
--- a/TPDB/DP/Unify.hs
+++ b/TPDB/DP/Unify.hs
@@ -1,4 +1,4 @@
-module TPDB.DP.Unify ( mgu, unifies, apply, times ) where
+module TPDB.DP.Unify ( mgu, match, unifies, apply, times ) where
 
 import TPDB.Data
 import qualified Data.Map as M
@@ -8,6 +8,25 @@
 type Substitution v c = M.Map v (Term v c)
 
 unifies t1 t2 = isJust $ mgu t1 t2
+
+-- | view variables as symbols
+pack :: Term v c -> Term any (Either v c)
+pack ( Var v ) = Node ( Left v ) []
+pack ( Node f args ) = Node ( Right f ) ( map pack args )
+
+unpack :: Term any (Either v c) -> Term v c
+unpack ( Node ( Left v ) [] ) = Var v
+unpack ( Node ( Right f ) args ) = Node f ( map unpack args )
+
+-- | will only bind variables in the left side
+match :: ( Ord v, Ord w, Eq c )
+      => Term v c
+      -> Term w c
+      -> Maybe ( M.Map v ( Term w c ) )
+match l r = do
+    u <- mgu ( fmap Right l ) ( pack r )
+    return $ M.map unpack  u
+
 
 -- | naive implementation (worst case exponential)
 mgu
diff --git a/TPDB/Data.hs b/TPDB/Data.hs
--- a/TPDB/Data.hs
+++ b/TPDB/Data.hs
@@ -18,8 +18,10 @@
 import Data.Function (on)
 
 data Identifier = 
-     Identifier { _identifier_hash :: Int
-                , name :: String , arity :: Int }
+     Identifier { _identifier_hash :: ! Int
+                , name :: ! String 
+                , arity :: Int 
+                }
     deriving ( Eq, Ord, Typeable )
 
 instance Hashable Identifier where
diff --git a/TPDB/Xml.hs b/TPDB/Xml.hs
--- a/TPDB/Xml.hs
+++ b/TPDB/Xml.hs
@@ -14,7 +14,7 @@
 rmkel name cs = return $ mkel name cs
 
 nospaceString :: String -> Content ()
-nospaceString s = CString False s ()
+nospaceString s = CString False (escape s) ()
 
 instance Typeable t => HTypeable t where 
     toHType x = let cs = show ( typeOf x ) in Prim cs cs
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 0.9.8
+Version: 1.1.1
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic