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
@@ -35,15 +35,23 @@
 cp = CertificationProblem
   { cpfVersion = "3.4"
   , input = TrsInput
-    { trsinput_trs = RS { rules = [ ru ] }
+    { trsinput_trs = RS { rules = [ rs, rw ] }
     }
   , proof = TrsTerminationProof RIsEmpty
   , origin = ignoredOrigin
   }
 
-ru = let a = SymName $ mk 0 "s" in Rule
+rs = let a = SymName $ mk 0 "s" in Rule
         { top = False
         , relation = TPDB.Data.Strict
+        , lhs = Node a []
+        , rhs = Node a []
+        , original_variable = Nothing
+        }
+
+rw = let a = SymName $ mk 0 "s" in Rule
+        { top = False
+        , relation = TPDB.Data.Weak
         , lhs = Node a []
         , rhs = Node a []
         , original_variable = Nothing
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
@@ -66,7 +66,16 @@
    parseContents = error "parseContents not implemented"
 
    toContents i = case i of
-      TrsInput {} -> rmkel "trsInput" $ toContents (trsinput_trs i )
+      TrsInput {} ->
+        let sys = trsinput_trs i
+            s = standard sys
+            r = relative sys
+        in  rmkel "trsInput" $
+                toContents s
+                <> if null (T.rules r) then []
+                   else rmkel "relativeRules" $
+                        rmkel "rules" $
+                        concatMap toContents $ T.rules r
       ComplexityInput {} -> rmkel "complexityInput" $ concat
           [ rmkel "trsInput" $ toContents $ trsinput_trs i
           ]
@@ -153,7 +162,7 @@
 instance XmlContent (TrsTerminationProof Relative) where
    parseContents = error "parseContents not implemented"
 
-   toContents p = rmkel "relativeTerminationProof" $ case p of
+   toContents p = rmkel "trsTerminationProof" $ case p of
       RIsEmpty -> rmkel "rIsEmpty" []
       SIsEmpty {} -> rmkel "sIsEmpty" $ concat
           [ toContents $ trsTerminationProof_Standard p
@@ -178,8 +187,7 @@
           ]
       RuleRemoval {} -> rmkel "ruleRemoval" $ concat
           [ toContents $ rr_orderingConstraintProof p
-          , toContents $ standard $ trs p
-          , toContents $ relative $ trs p
+          , toContents $ trs_deleted p
           , toContents $ trsTerminationProof p
           ]
       EqualityRemoval {} -> rmkel "equalityRemoval" $ concat
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,7 +1,7 @@
-Cabal-Version: 3.0
+Cabal-Version: 3.8
 
 Name: tpdb
-Version: 2.8.0
+Version: 2.8.1
 
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann