diff --git a/src/prover.rs b/src/prover.rs
index 7903f2c..00177c3 100644
--- a/src/prover.rs
+++ b/src/prover.rs
@@ -4,7 +4,6 @@ pub mod constraints;
 pub mod not;
 pub mod or;
 pub mod predicate;
-pub mod proof_cache;
 pub mod tracing;
 pub mod unification;
 
@@ -19,7 +18,6 @@ use crate::ast::Predicate;
 use crate::ast::Variable;
 use crate::prover::body::BodyProver;
 use crate::prover::constraints::Constraints;
-use crate::prover::tracing::EmptyTracer;
 use crate::prover::tracing::IndentedTracer;
 
 #[derive(Clone, Copy, Debug, Default)]
diff --git a/src/prover/proof_cache.rs b/src/prover/proof_cache.rs
deleted file mode 100644
index ef8f354..0000000
--- a/src/prover/proof_cache.rs
+++ /dev/null
@@ -1,239 +0,0 @@
-use std::cell::RefCell;
-use std::num::NonZero;
-use std::rc::Rc;
-
-use bimap::BiHashMap;
-use lru::LruCache;
-
-use crate::ast::Body;
-use crate::ast::Module;
-use crate::ast::Predicate;
-use crate::ast::Variable;
-use crate::prover::GlobalCounter;
-use crate::prover::body::BodyProver;
-use crate::prover::body::{self};
-use crate::prover::constraints;
-use crate::prover::constraints::Constraints;
-use crate::prover::tracing::EmptyTracer;
-
-pub struct PartialProof<T: Iterator<Item = Constraints>>
-{
-    proved: Vec<Constraints>,
-    prover: T,
-}
-
-pub struct CachedProver<'a>
-{
-    module: &'a Module,
-    cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
-    normalized_body: Body,
-    normalized_counter: usize,
-    mapping: VariableMap,
-    constraints: Constraints,
-
-    proof_counter: usize,
-}
-
-pub struct ProofCache<'a>
-{
-    cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
-}
-
-impl<'a> ProofCache<'a>
-{
-    pub fn new(size: NonZero<usize>) -> Self
-    {
-        ProofCache {
-            cache: Rc::new(RefCell::new(LruCache::new(size))),
-        }
-    }
-
-    pub fn prove(
-        &mut self,
-        module: &'a Module,
-        constraints: &Constraints,
-        body: &Body,
-    ) -> CachedProver<'a>
-    {
-        let (varmap, counter, normalized) = body.normalized();
-        CachedProver {
-            module,
-            cache: self.cache.clone(),
-            normalized_body: normalized,
-            normalized_counter: counter,
-            mapping: varmap,
-            proof_counter: 0,
-            constraints: constraints.clone(),
-        }
-    }
-}
-
-impl<'a> Iterator for CachedProver<'a>
-{
-    type Item = Constraints;
-
-    fn next(&mut self) -> Option<Self::Item>
-    {
-        let constraints;
-        {
-            let mut cache_borrow = self.cache.borrow_mut();
-            let partial_proof =
-                cache_borrow.get_or_insert_mut(self.normalized_body.clone(), || PartialProof {
-                    proved: vec![],
-                    prover: BodyProver::new(
-                        self.module,
-                        GlobalCounter::with(self.normalized_counter),
-                        self.normalized_body.clone(),
-                        Constraints::none(),
-                        &mut EmptyTracer,
-                    ),
-                });
-
-            while partial_proof.proved.len() <= self.proof_counter
-            {
-                let constraints = partial_proof.prover.next();
-                match constraints
-                {
-                    Some(constraints) => partial_proof.proved.push(constraints),
-                    None => return None,
-                }
-            }
-            self.proof_counter += 1;
-            let normalized_proof = partial_proof.proved[self.proof_counter]
-                .clone()
-                .contextualized(&self.mapping);
-            // Check if we can get a match
-            constraints = self.constraints.and(&normalized_proof);
-        }
-
-        match constraints
-        {
-            Some(c) => Some(c),
-            None => self.next(),
-        }
-    }
-}
-
-// Normalization
-
-pub struct VariableMap(BiHashMap<Variable, Variable>);
-
-pub trait Normalizable: Sized
-{
-    fn normalized(&self) -> (VariableMap, usize, Self)
-    {
-        let mut bimap = BiHashMap::new();
-        let mut counter = 0;
-        let normalized = self.normalized_with(&mut counter, &mut bimap);
-
-        (VariableMap(bimap), counter, normalized)
-    }
-
-    fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap<Variable, Variable>)
-    -> Self;
-}
-
-impl<T: Normalizable> Normalizable for Vec<T>
-{
-    fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap<Variable, Variable>)
-    -> Self
-    {
-        self.iter()
-            .map(|x| x.normalized_with(counter, map))
-            .collect()
-    }
-}
-
-impl Normalizable for Body
-{
-    fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap<Variable, Variable>)
-    -> Body
-    {
-        match self
-        {
-            Body::Term(predicate) => Body::Term(predicate.normalized_with(counter, map)),
-            Body::And(items) => Body::And(items.normalized_with(counter, map)),
-            Body::Or(items) => Body::Or(items.normalized_with(counter, map)),
-        }
-    }
-}
-
-impl Normalizable for Predicate
-{
-    fn normalized_with(
-        &self,
-        counter: &mut usize,
-        map: &mut BiHashMap<Variable, Variable>,
-    ) -> Predicate
-    {
-        match self
-        {
-            Predicate::Variable(variable) =>
-            {
-                Predicate::Variable(variable.normalized_with(counter, map))
-            }
-            Predicate::Fixed(name, predicates) =>
-            {
-                Predicate::Fixed(name.clone(), predicates.normalized_with(counter, map))
-            }
-        }
-    }
-}
-
-impl Normalizable for Variable
-{
-    fn normalized_with(
-        &self,
-        counter: &mut usize,
-        map: &mut BiHashMap<Variable, Variable>,
-    ) -> Variable
-    {
-        match map.get_by_left(self)
-        {
-            Some(normalized) => normalized.clone(),
-            None =>
-            {
-                let val = *counter;
-                *counter += 1;
-
-                let var = Variable(self.0.clone(), Some(val));
-                map.insert(self.clone(), var.clone());
-                var
-            }
-        }
-    }
-}
-
-impl Predicate
-{
-    fn contextualized(&self, map: &VariableMap) -> Predicate
-    {
-        match self
-        {
-            Predicate::Variable(variable) =>
-            {
-                Predicate::Variable(map.0.get_by_right(variable).unwrap().clone())
-            }
-            Predicate::Fixed(name, predicates) => Predicate::Fixed(
-                name.clone(),
-                predicates.iter().map(|p| p.contextualized(map)).collect(),
-            ),
-        }
-    }
-}
-
-impl Constraints
-{
-    pub fn contextualized(&self, map: &VariableMap) -> Constraints
-    {
-        let mut new = Constraints::none();
-        for (var, pred) in self.set.iter()
-        {
-            let ctx_var = map.0.get_by_right(var).unwrap();
-            let ctx_pred = pred.contextualized(map);
-            new.set.insert(ctx_var.clone(), ctx_pred);
-        }
-
-        new
-    }
-}
diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs
index 2c4fde1..f427793 100644
--- a/src/prover/tracing.rs
+++ b/src/prover/tracing.rs
@@ -5,8 +5,6 @@ use owo_colors::colors::css::DarkGray;
 use owo_colors::colors::css::Gray;
 use std::fmt::Display;
 
-use crate::ast::Variable;
-
 #[derive(Clone, Copy)]
 pub enum ProofType
 {