diff --git a/src/main/scala/at/logic/skeptik/algorithm/compressor/RecycleUnits.scala b/src/main/scala/at/logic/skeptik/algorithm/compressor/RecycleUnits.scala
index 93043e37..7888c67a 100644
--- a/src/main/scala/at/logic/skeptik/algorithm/compressor/RecycleUnits.scala
+++ b/src/main/scala/at/logic/skeptik/algorithm/compressor/RecycleUnits.scala
@@ -9,15 +9,10 @@ import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}
 import scala.collection.mutable.{HashMap => MMap}
 import scala.collection.mutable.{HashSet => MSet}
 
-object RecycleUnits extends (Proof[SequentProofNode] => Proof[SequentProofNode]) {
+object RecycleUnits extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes {
   
   def isUnit[P <: ProofNode[Sequent,P]](n: P) = n.conclusion.width == 1
   
-  def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedLeft: SequentProofNode, fixedRight: SequentProofNode):SequentProofNode = {
-    if ((left eq fixedLeft) && (right eq fixedRight)) node 
-    else R(fixedLeft,fixedRight,pivot,true)
-  }
-  
   def apply(proof: Proof[SequentProofNode]) = {
     //stores the unit descendend unit nodes of all proof nodes
     val descUnits = new MMap[SequentProofNode,MSet[SequentProofNode]]
diff --git a/src/main/scala/at/logic/skeptik/algorithm/compressor/Subsumption.scala b/src/main/scala/at/logic/skeptik/algorithm/compressor/Subsumption.scala
index 53b70236..d8afcbcc 100644
--- a/src/main/scala/at/logic/skeptik/algorithm/compressor/Subsumption.scala
+++ b/src/main/scala/at/logic/skeptik/algorithm/compressor/Subsumption.scala
@@ -1,6 +1,7 @@
 package at.logic.skeptik.algorithm.compressor
 
-import at.logic.skeptik.proof.Proof
+import at.logic.skeptik.expression.E
+import at.logic.skeptik.proof._
 import at.logic.skeptik.proof.sequent._
 import at.logic.skeptik.proof.sequent.lk._
 import at.logic.skeptik.judgment.immutable.{SeqSequent => Sequent}
@@ -10,7 +11,7 @@ import scala.collection.mutable.{HashSet => MSet}
 import scala.collection.immutable.{HashSet => ISet}
 
 abstract class AbstractSubsumption 
-extends (Proof[SequentProofNode] => Proof[SequentProofNode])
+extends (Proof[SequentProofNode] => Proof[SequentProofNode]) with fixNodes
 
 object TopDownLeftRightSubsumption extends AbstractSubsumption {
   
@@ -25,16 +26,12 @@ object TopDownLeftRightSubsumption extends AbstractSubsumption {
           node match {
             case Axiom(conclusion) => nodeMap += (conclusion -> node) ; node
             case R(left, right, pivot, _) => {
-  	          val fixedLeft  = fixedPremises.head
-              val fixedRight = fixedPremises.last
-              val newNode = 
-    		        if ((left eq fixedLeft) && (right eq fixedRight)) node 
-    		        else R(fixedLeft,fixedRight,pivot,true)
+  	          val newNode = fixNode(node,pivot,left,right,fixedPremises)
   		        nodeMap += (newNode.conclusion -> newNode)
   		        newNode
   	        }
-              case _ => node
-            }
+            case _ => node
+          }
         })
       })
     })
@@ -70,14 +67,7 @@ abstract class BottomUpRightLeftSubsumption extends AbstractSubsumption {
     	
       replaceNodes.getOrElse(node,{
         node match {
-          case R(left, right, pivot, _) => {
-            val fixedLeft  = fixedPremises.head
-	        val fixedRight = fixedPremises.last
-	        val newNode = 
-	          if ((left eq fixedLeft) && (right eq fixedRight)) node 
-	          else R(fixedLeft,fixedRight,pivot,true)
-	          newNode
-          }
+          case R(left, right, pivot, _) => fixNode(node,pivot,left,right,fixedPremises)
           case _ => node
         }
       })
@@ -104,3 +94,18 @@ object BottomUpRightLeftSubsumptionMemory extends BottomUpRightLeftSubsumption {
     !(node existsAmongAncestors {_ eq ancestor})
   }
 }
+
+object ForwardAxiomSubsumption extends AbstractSubsumption {
+  def apply(proof: Proof[SequentProofNode]) = {
+    val axioms = MMap[Sequent,SequentProofNode]()
+    proof foldDown { (node: SequentProofNode, fixedPremises: Seq[SequentProofNode]) => node match {
+      case Axiom(conclusion) => {
+        val subsumed = axioms.find(A => A._1 subsequentOf conclusion)
+        val subsMap = subsumed.map(A => A._2)
+        subsMap.getOrElse({axioms += (conclusion -> node); node})
+      }
+      case R(left, right, pivot, _) => fixNode(node,pivot,left,right,fixedPremises)
+      case _ => node
+    }}
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/at/logic/skeptik/algorithm/compressor/package.scala b/src/main/scala/at/logic/skeptik/algorithm/compressor/package.scala
index 308243bd..7d83c208 100644
--- a/src/main/scala/at/logic/skeptik/algorithm/compressor/package.scala
+++ b/src/main/scala/at/logic/skeptik/algorithm/compressor/package.scala
@@ -1,6 +1,11 @@
 package at.logic.skeptik.algorithm
 
 import at.logic.skeptik.algorithm.compressor.split._
+import at.logic.skeptik.expression.E
+import at.logic.skeptik.proof.ProofNode
+import at.logic.skeptik.proof.sequent.SequentProofNode
+import at.logic.skeptik.judgment.Sequent
+import at.logic.skeptik.proof.sequent.lk.R
 
 // Algorithm names should contain only alphanumeric characters
 
@@ -30,6 +35,20 @@ package object compressor {
     "MSplit4" -> new TimeoutMultiSplit(4,5000),
     "TDLRS" -> TopDownLeftRightSubsumption,
     "BURLSt" -> BottomUpRightLeftSubsumptionTime,
-    "BURLSm" -> BottomUpRightLeftSubsumptionMemory
+    "BURLSm" -> BottomUpRightLeftSubsumptionMemory,
+    "FAS" -> ForwardAxiomSubsumption
   )
+  trait fixNodes {
+    def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedLeft: SequentProofNode, fixedRight: SequentProofNode):SequentProofNode = {
+      if ((left eq fixedLeft) && (right eq fixedRight)) node 
+      else R(fixedLeft,fixedRight,pivot,true)
+    }
+      def fixNode[P <: ProofNode[Sequent,P]](node: SequentProofNode, pivot: E, left: P, right: P, fixedPremises: Seq[SequentProofNode]):SequentProofNode = {
+        val fixedLeft  = fixedPremises.head
+        val fixedRight = fixedPremises.last
+        fixNode(node,pivot,left,right,fixedLeft,fixedRight)
+    }
+  }
 }
+
+
diff --git a/src/test/scala/at/logic/skeptik/algorithm/compressor/ForwardSubsumption.scala b/src/test/scala/at/logic/skeptik/algorithm/compressor/ForwardSubsumption.scala
index 7bb42320..7095428a 100644
--- a/src/test/scala/at/logic/skeptik/algorithm/compressor/ForwardSubsumption.scala
+++ b/src/test/scala/at/logic/skeptik/algorithm/compressor/ForwardSubsumption.scala
@@ -50,11 +50,11 @@ class ForwardSubsumptionSpecification extends SpecificationWithJUnit {
 	
     "Forward Subsumption" should {
       "compress the proof" in {
-        val compproof = FWS.apply(r6)
+        val compproof = TopDownLeftRightSubsumption.apply(r6)
         proof.size must beGreaterThan(compproof.size)
       }
       "conclude the empty clause" in {
-        val compproof = FWS.apply(r6)
+        val compproof = TopDownLeftRightSubsumption.apply(r6)
         compproof.root.conclusion.isEmpty must beTrue
       }
 	}