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
@@ -3,7 +3,7 @@
 module TPDB.CPF.Proof.Read where
 
 import TPDB.CPF.Proof.Type as Type
-import TPDB.Data
+import TPDB.Data hiding (Type (..))
 
 {-
 import Text.XML.HXT.Arrow.XmlArrow
@@ -65,10 +65,17 @@
   ( CertificationProblem
      <$> (c $/ element "cpfVersion" &/ content )
      <*> (c $/ element "input" &/ getInput )
+     <*> (c $/ element "property" &/ getProperty )
+     <*> (c $/ element "answer" &/ getAnswer )
      <*> (c $/ element "proof" &/ getProof)
      <*> (c $/ element "origin" >=> return [ignoredOrigin] )
   )
 
+getProperty = (element "termination" >> return [ Termination])
+
+getAnswer = (element "no" >> return [No])
+       <>   (element "yes" >> return [Yes])
+
 getInput =  getTerminationInput
    <> getComplexityInput
    <> getACTerminationInput
@@ -85,7 +92,6 @@
       , asymbols = as
       , csymbols = cs
       }
-
 
 getComplexityInput = element "input" >=> \ c -> do
     trsI <- c $/ element "complexityInput" &/ element "trsInput" &/ getTrsInput
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
@@ -18,7 +18,7 @@
 
 where
 
-import TPDB.Data
+import TPDB.Data hiding (Type(..))
 import TPDB.Plain.Write ()
 import Data.Typeable
 import TPDB.Pretty
@@ -33,10 +33,12 @@
 
 cp :: CertificationProblem
 cp = CertificationProblem
-  { cpfVersion = "3.4"
+  { cpfVersion = "3.6"
   , input = TrsInput
     { trsinput_trs = RS { rules = [ rs, rw ] }
     }
+  , property = Termination
+  , answer = Yes
   , proof = TrsTerminationProof RIsEmpty
   , origin = ignoredOrigin
   }
@@ -57,10 +59,15 @@
         , original_variable = Nothing
         }
 
+data Property = Termination deriving (Typeable, Eq, Generic)
+data Answer = No | Yes deriving (Typeable, Eq, Generic)
+
 data CertificationProblem =
      CertificationProblem { cpfVersion :: Text
-                          , input :: CertificationProblemInput
-                          , proof :: Proof 
+                          , input :: !CertificationProblemInput
+                          , property :: !Property
+                          , answer :: !Answer
+                          , proof :: !Proof 
                           , origin :: Origin  
                           }  
    deriving ( Typeable, Eq, Generic )
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
@@ -42,12 +42,21 @@
          [ mkel "cpfVersion" [ nospaceString $ cpfVersion cp ]
          , mkel "lookupTables"  []
          , mkel "input" $ toContents ( input cp )
-         , mkel "property" $ rmkel "termination" []
-         , mkel "answer" $ rmkel "yes" [] -- FIXME (no?)
+         , mkel "property" $ toContents (property cp)
+         , mkel "answer" $ toContents (answer cp)
          , mkel "proof" $ toContents ( proof cp )
          , mkel "origin" $ toContents ( origin cp )
          ]
 
+instance XmlContent Property where
+  toContents p = case p of
+    Termination -> rmkel "termination" []
+
+instance XmlContent Answer where
+  toContents a = case a of
+    No -> rmkel "no" []
+    Yes -> rmkel "yes" []
+
 instance XmlContent Origin where
    parseContents = error "parseContents not implemented"
 
@@ -168,7 +177,8 @@
           [ toContents $ trsTerminationProof_Standard p
           ]
       StringReversal {} -> rmkel "stringReversal" $ concat
-          [ toContents $ standard $ trs p
+          [ -- toContents $ trs p
+            toContents $ standard $ trs p
           , toContents $ relative $ trs p
           , toContents $ trsTerminationProof p
           ]
@@ -198,6 +208,8 @@
 
 standard trs = trs `T.with_rules` filter T.strict (T.rules trs)
 relative trs = trs `T.with_rules` filter T.weak   (T.rules trs)
+
+toco_relative s = [ toContents s ]
 
 toco_relative s = 
       [ toContents $ standard s ]
diff --git a/src/TPDB/Data.hs b/src/TPDB/Data.hs
--- a/src/TPDB/Data.hs
+++ b/src/TPDB/Data.hs
@@ -115,7 +115,7 @@
              }
 
 data Type = Termination | Complexity
-     deriving Show
+  deriving Show
 
 data Strategy = Full | Innermost | Outermost
      deriving Show
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.3
+Version: 2.8.4
 
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann