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
@@ -172,19 +172,16 @@
           , toContents $ relative $ trs p
           , toContents $ trsTerminationProof p
           ]
-      FlatContextClosure {} -> rmkel "flatContextClosure" $ concat
+      FlatContextClosure {} -> rmkel "flatContextClosure" $ concat $
           [ rmkel "flatContexts" $ concatMap toContents
                $ flatContexts p
-          , toContents $ standard $ trs p
-          , toContents $ relative $ trs p
-          , toContents $ trsTerminationProof p
           ]
-      Semlab {} -> rmkel "semlab" $ concat
-          [ toContents $ model p
-          , toContents $ standard $ trs p
-          , toContents $ relative $ trs p
-          , toContents $ trsTerminationProof p
-          ]
+          <> toco_relative (trs p)
+          <> [ toContents $ trsTerminationProof p ]
+      Semlab {} -> rmkel "semlab" $ concat $
+          [ toContents $ model p ]
+          <> toco_relative (trs p)
+          <> [ toContents $ trsTerminationProof p ]
       RuleRemoval {} -> rmkel "ruleRemoval" $ concat
           [ toContents $ rr_orderingConstraintProof p
           , toContents $ trs_deleted p
@@ -201,6 +198,11 @@
 
 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 $ standard s ]
+   <> [ toContents $ relative s | not $ null $ filter T.weak  $ T.rules s ]
+
 
 symbolize trs = 
     ( fmap (T.tmap SymName) trs )
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.2
+Version: 2.8.3
 
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann