diff --git a/src/internal/assignment.rs b/src/internal/assignment.rs
index 958b083b..ac8f1270 100644
--- a/src/internal/assignment.rs
+++ b/src/internal/assignment.rs
@@ -24,8 +24,6 @@ pub enum Assignment<P: Package, V: Version> {
     Derivation {
         /// The package corresponding to the derivation.
         package: P,
-        /// Term of the derivation.
-        term: Term<V>,
         /// Incompatibility cause of the derivation.
         cause: Incompatibility<P, V>,
     },
@@ -46,7 +44,7 @@ impl<P: Package, V: Version> Assignment<P, V> {
     pub fn as_term(&self) -> Term<V> {
         match &self {
             Self::Decision { version, .. } => Term::exact(version.clone()),
-            Self::Derivation { term, .. } => term.clone(),
+            Self::Derivation { package, cause } => cause.get(&package).unwrap().negate(),
         }
     }
 }
diff --git a/src/internal/core.rs b/src/internal/core.rs
index 743c5c5f..e67f3792 100644
--- a/src/internal/core.rs
+++ b/src/internal/core.rs
@@ -77,26 +77,17 @@ impl<P: Package, V: Version> State<P, V> {
                     // If the partial solution satisfies the incompatibility
                     // we must perform conflict resolution.
                     Relation::Satisfied => {
-                        let root_cause = self.conflict_resolution(&incompat)?;
-                        // root_cause is guaranteed to be almost satisfied by the partial solution
-                        // according to PubGrub documentation.
-                        match self.partial_solution.relation(&root_cause) {
-                            Relation::AlmostSatisfied((package_almost, term)) => {
-                                changed = vec![package_almost.clone()];
-                                // Add (not term) to the partial solution with incompat as cause.
-                                self.partial_solution.add_derivation(package_almost, term.negate(), root_cause);
-                            }
-                            _ => return Err(PubGrubError::Failure("This should never happen, root_cause is guaranteed to be almost satisfied by the partial solution".into())),
-                        }
+                        let (package_almost, root_cause) = self.conflict_resolution(&incompat)?;
+                        changed = vec![package_almost.clone()];
+                        // Add to the partial solution with incompat as cause.
+                        self.partial_solution
+                            .add_derivation(package_almost, root_cause);
                     }
-                    Relation::AlmostSatisfied((package_almost, term)) => {
+                    Relation::AlmostSatisfied(package_almost) => {
                         changed.push(package_almost.clone());
                         // Add (not term) to the partial solution with incompat as cause.
-                        self.partial_solution.add_derivation(
-                            package_almost,
-                            term.negate(),
-                            incompat.clone(),
-                        );
+                        self.partial_solution
+                            .add_derivation(package_almost, incompat.clone());
                     }
                     _ => {}
                 }
@@ -115,7 +106,7 @@ impl<P: Package, V: Version> State<P, V> {
     fn conflict_resolution(
         &mut self,
         incompatibility: &Incompatibility<P, V>,
-    ) -> Result<Incompatibility<P, V>, PubGrubError<P, V>> {
+    ) -> Result<(P, Incompatibility<P, V>), PubGrubError<P, V>> {
         let mut current_incompat = incompatibility.clone();
         let mut current_incompat_changed = false;
         loop {
@@ -128,26 +119,22 @@ impl<P: Package, V: Version> State<P, V> {
                     .partial_solution
                     .find_satisfier_and_previous_satisfier_level(&current_incompat);
                 match satisfier {
-                    Decision { .. } => {
+                    Decision { package, .. } => {
                         self.backtrack(
                             current_incompat.clone(),
                             current_incompat_changed,
                             previous_satisfier_level,
                         );
-                        return Ok(current_incompat);
+                        return Ok((package, current_incompat));
                     }
-                    Derivation {
-                        cause,
-                        term,
-                        package,
-                    } => {
+                    Derivation { cause, package } => {
                         if previous_satisfier_level != satisfier_level {
                             self.backtrack(
                                 current_incompat.clone(),
                                 current_incompat_changed,
                                 previous_satisfier_level,
                             );
-                            return Ok(current_incompat);
+                            return Ok((package, current_incompat));
                         } else {
                             let id = self.incompatibility_store.len();
                             let prior_cause = Incompatibility::prior_cause(
@@ -155,11 +142,7 @@ impl<P: Package, V: Version> State<P, V> {
                                 &current_incompat,
                                 &cause,
                                 &package,
-                                &term,
                             );
-                            // eprintln!("\ncause 1: {}", &current_incompat);
-                            // eprintln!("cause 2: {}", &cause);
-                            // eprintln!("prior cause: {}\n", &prior_cause);
                             self.incompatibility_store.push(prior_cause.clone());
                             current_incompat = prior_cause;
                             current_incompat_changed = true;
diff --git a/src/internal/incompatibility.rs b/src/internal/incompatibility.rs
index 5eba0288..5fa9007c 100644
--- a/src/internal/incompatibility.rs
+++ b/src/internal/incompatibility.rs
@@ -61,7 +61,7 @@ pub enum Relation<P: Package, V: Version> {
     Contradicted(PackageTerm<P, V>),
     /// If S satisfies all but one of I's terms and is inconclusive for the remaining term,
     /// we say S "almost satisfies" I and we call the remaining term the "unsatisfied term".
-    AlmostSatisfied(PackageTerm<P, V>),
+    AlmostSatisfied(P),
     /// Otherwise, we say that their relation is inconclusive.
     Inconclusive,
 }
@@ -203,27 +203,20 @@ impl<P: Package, V: Version> Incompatibility<P, V> {
     }
 
     /// Prior cause of two incompatibilities using the rule of resolution.
-    pub fn prior_cause(
-        id: usize,
-        incompat: &Self,
-        satisfier_cause: &Self,
-        package: &P,
-        satisfier: &Term<V>,
-    ) -> Self {
+    pub fn prior_cause(id: usize, incompat: &Self, satisfier_cause: &Self, package: &P) -> Self {
         let kind = Kind::DerivedFrom(incompat.id, satisfier_cause.id);
-        let mut t1 = incompat.package_terms.clone();
-        let mut t2 = satisfier_cause.package_terms.clone();
-        t1.remove(package);
-        t2.remove(package);
-        let mut prior_cause_terms = Self::intersection(&t1, &t2);
-        let term = incompat.package_terms.get(package).unwrap();
-        let p_term = term.union(&satisfier.negate());
-        if p_term != Term::any() {
-            prior_cause_terms.insert(package.clone(), p_term);
+        let mut incompat1 = incompat.package_terms.clone();
+        let mut incompat2 = satisfier_cause.package_terms.clone();
+        let t1 = incompat1.remove(package).unwrap();
+        let t2 = incompat2.remove(package).unwrap();
+        let mut package_terms = Self::intersection(&incompat1, &incompat2);
+        let term = t1.union(&t2);
+        if term != Term::any() {
+            package_terms.insert(package.clone(), term);
         }
         Self {
             id,
-            package_terms: prior_cause_terms,
+            package_terms,
             kind,
         }
     }
@@ -244,8 +237,7 @@ impl<P: Package, V: Version> Incompatibility<P, V> {
                     // but we systematically remove those from incompatibilities
                     // so we're safe on that front.
                     if relation == Relation::Satisfied {
-                        relation =
-                            Relation::AlmostSatisfied((package.clone(), incompat_term.clone()));
+                        relation = Relation::AlmostSatisfied(package.clone());
                     } else {
                         relation = Relation::Inconclusive;
                     }
@@ -379,7 +371,7 @@ pub mod tests {
             i3.insert("p1", t1);
             i3.insert("p3", t3);
 
-            let i_resolution = Incompatibility::prior_cause(0, &i1, &i2, &"p2", &t2.negate());
+            let i_resolution = Incompatibility::prior_cause(0, &i1, &i2, &"p2");
             assert_eq!(i_resolution.package_terms, i3);
         }
 
diff --git a/src/internal/memory.rs b/src/internal/memory.rs
index fd310678..f403de42 100644
--- a/src/internal/memory.rs
+++ b/src/internal/memory.rs
@@ -48,7 +48,9 @@ impl<P: Package, V: Version> Memory<P, V> {
     pub fn add_assignment(&mut self, assignment: &Assignment<P, V>) {
         match assignment {
             Decision { package, version } => self.add_decision(package.clone(), version.clone()),
-            Derivation { package, term, .. } => self.add_derivation(package.clone(), term.clone()),
+            Derivation { package, cause } => {
+                self.add_derivation(package.clone(), cause.get(&package).unwrap().negate())
+            }
         }
     }
 
diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs
index 8c248081..5bd9fd47 100644
--- a/src/internal/partial_solution.rs
+++ b/src/internal/partial_solution.rs
@@ -88,12 +88,8 @@ impl<P: Package, V: Version> PartialSolution<P, V> {
     }
 
     /// Add a derivation to the partial solution.
-    pub fn add_derivation(&mut self, package: P, term: Term<V>, cause: Incompatibility<P, V>) {
-        self.add_assignment(Derivation {
-            package,
-            term,
-            cause,
-        });
+    pub fn add_derivation(&mut self, package: P, cause: Incompatibility<P, V>) {
+        self.add_assignment(Derivation { package, cause });
     }
 
     /// If a partial solution has, for every positive derivation,