diff --git a/Cargo.lock b/Cargo.lock
index 30b02f89c..fadc802be 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -875,6 +875,7 @@ version = "0.3.0"
 dependencies = [
  "dyn-clone",
  "fnv",
+ "thiserror",
 ]
 
 [[package]]
diff --git a/pumpkin-checker/src/deductions.rs b/pumpkin-checker/src/deductions.rs
index eafe740b3..2c6e15994 100644
--- a/pumpkin-checker/src/deductions.rs
+++ b/pumpkin-checker/src/deductions.rs
@@ -3,10 +3,10 @@ use std::rc::Rc;
 
 use drcp_format::ConstraintId;
 use drcp_format::IntAtomic;
-use pumpkin_checking::AtomicConstraint;
-use pumpkin_checking::VariableState;
+use pumpkin_checking::SupportingInference;
 
 use crate::inferences::Fact;
+use crate::model::Atomic;
 use crate::model::Nogood;
 
 /// An inference that was ignored when checking a deduction.
@@ -46,212 +46,86 @@ pub fn verify_deduction(
     deduction: &drcp_format::Deduction<Rc<str>, i32>,
     facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
 ) -> Result<Nogood, InvalidDeduction> {
-    // To verify a deduction, we assume that the premises are true. Then we go over all the
-    // facts in the sequence, and if all the premises are satisfied, we apply the consequent.
-    // At some point, this should either reach a fact without a consequent or derive an
-    // inconsistent domain.
-
-    let mut variable_state = VariableState::prepare_for_conflict_check(
-        deduction.premises.iter().cloned().map(Into::into),
-        None,
-    )
-    .map_err(|_| InvalidDeduction::InconsistentPremises)?;
-
-    let mut unused_inferences = Vec::new();
-
-    for constraint_id in deduction.sequence.iter() {
-        // Get the fact associated with the constraint ID from the sequence.
-        let fact = facts_in_proof_stage
-            .get(constraint_id)
-            .ok_or(InvalidDeduction::UnknownInference(*constraint_id))?;
-
-        // Collect all premises that do not evaluate to `true` under the current variable
-        // state.
-        let unsatisfied_premises: Vec<IntAtomic<String, i32>> = fact
-            .premises
-            .iter()
-            .filter_map::<IntAtomic<String, i32>, _>(|premise| {
-                if variable_state.is_true(premise) {
-                    None
-                } else {
-                    // We need to convert the premise name from a `Rc<str>` to a
-                    // `String`. The former does not implement `Send`, but that is
-                    // required for our error type to be used with anyhow.
-                    Some(IntAtomic {
-                        name: String::from(premise.identifier().as_ref()),
-                        comparison: match premise.comparison() {
-                            pumpkin_checking::Comparison::GreaterEqual => {
-                                drcp_format::IntComparison::GreaterEqual
-                            }
-                            pumpkin_checking::Comparison::LessEqual => {
-                                drcp_format::IntComparison::LessEqual
-                            }
-                            pumpkin_checking::Comparison::Equal => {
-                                drcp_format::IntComparison::Equal
-                            }
-                            pumpkin_checking::Comparison::NotEqual => {
-                                drcp_format::IntComparison::NotEqual
-                            }
-                        },
-                        value: premise.value(),
-                    })
-                }
-            })
-            .collect::<Vec<_>>();
-
-        // If at least one premise is unassigned, this fact is ignored for the conflict
-        // check and recorded as unused.
-        if !unsatisfied_premises.is_empty() {
-            unused_inferences.push(IgnoredInference {
-                constraint_id: *constraint_id,
-                unsatisfied_premises,
-            });
+    // First we convert the deduction sequence to the types from the checking library.
+    let inferences = deduction
+        .sequence
+        .iter()
+        .map(|cid| {
+            facts_in_proof_stage
+                .get(cid)
+                .map(|fact| SupportingInference {
+                    premises: fact.premises.clone(),
+                    consequent: fact.consequent.clone(),
+                })
+                .ok_or(InvalidDeduction::UnknownInference(*cid))
+        })
+        .collect::<Result<Vec<_>, _>>()?;
+
+    // Then we convert the deduction premise to the types from the checking library.
+    let premises = deduction.premises.iter().cloned().map(Atomic::IntAtomic);
+
+    match pumpkin_checking::verify_deduction(premises.clone(), inferences) {
+        Ok(_) => Ok(Nogood::from(premises)),
+        Err(error) => Err(convert_error(error, facts_in_proof_stage)),
+    }
+}
 
-            continue;
+fn convert_error(
+    error: pumpkin_checking::InvalidDeduction<Atomic>,
+    facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
+) -> InvalidDeduction {
+    match error {
+        pumpkin_checking::InvalidDeduction::NoConflict(ignored_inferences) => {
+            let mapped_ignored_inferences = ignored_inferences
+                .into_iter()
+                .map(|ignored_inference| {
+                    convert_ignored_inferences(ignored_inference, facts_in_proof_stage)
+                })
+                .collect();
+
+            InvalidDeduction::NoConflict(mapped_ignored_inferences)
         }
-
-        // At this point the premises are satisfied so we handle the consequent of the
-        // inference.
-        match &fact.consequent {
-            Some(consequent) => {
-                if !variable_state.apply(consequent) {
-                    // If applying the consequent yields an empty domain for a
-                    // variable, then the deduction is valid.
-                    return Ok(Nogood::from(deduction.premises.clone()));
-                }
-            }
-            // If the consequent is explicitly false, then the deduction is valid.
-            None => return Ok(Nogood::from(deduction.premises.clone())),
+        pumpkin_checking::InvalidDeduction::InconsistentPremises => {
+            InvalidDeduction::InconsistentPremises
         }
     }
-
-    // Reaching this point means that the conjunction of inferences did not yield to a
-    // conflict. Therefore the deduction is invalid.
-    Err(InvalidDeduction::NoConflict(unused_inferences))
 }
 
-#[cfg(test)]
-mod tests {
-    use super::*;
-    use crate::atomic;
-    use crate::fact;
-    use crate::test_utils::constraint_id;
-    use crate::test_utils::deduction;
-
-    macro_rules! facts {
-        {$($k: expr => $v: expr),* $(,)?} => {
-            ::std::collections::BTreeMap::from([$(($crate::test_utils::constraint_id($k), $v),)*])
-        };
-    }
-
-    #[test]
-    fn a_sequence_is_correctly_traversed() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [1, 2, 3]);
-
-        let facts_in_proof_stage = facts! {
-            1 => fact!([x >= 5] -> [y <= 4]),
-            2 => fact!([y <= 7] -> [z != 10]),
-            3 => fact!([y <= 5] & [z != 10] -> [x <= 4]),
-        };
-
-        let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction");
-        assert_eq!(Nogood::from(premises), nogood);
-    }
-
-    #[test]
-    fn an_inference_implying_false_is_a_valid_stopping_condition() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [1, 2, 3]);
-
-        let facts_in_proof_stage = facts! {
-            1 => fact!([x >= 5] -> [y <= 4]),
-            2 => fact!([y <= 7] -> [z != 10]),
-            3 => fact!([y <= 5] & [z != 10] -> false),
-        };
-
-        let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction");
-        assert_eq!(Nogood::from(premises), nogood);
-    }
-
-    #[test]
-    fn inference_order_does_not_need_to_be_by_constraint_id() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [2, 1, 4]);
-
-        let facts_in_proof_stage = facts! {
-            2 => fact!([x >= 5] -> [y <= 4]),
-            1 => fact!([y <= 7] -> [z != 10]),
-            4 => fact!([y <= 5] & [z != 10] -> false),
-        };
-
-        let nogood = verify_deduction(&deduction, &facts_in_proof_stage).expect("valid deduction");
-        assert_eq!(Nogood::from(premises), nogood);
-    }
-
-    #[test]
-    fn inconsistent_premises_are_identified() {
-        let premises = vec![atomic!([x >= 5]), atomic!([x <= 4])];
-        let deduction = deduction(5, premises.clone(), [2]);
-
-        let facts_in_proof_stage = facts! {
-            2 => fact!([x == 5] -> false),
-        };
-
-        let error =
-            verify_deduction(&deduction, &facts_in_proof_stage).expect_err("inconsistent premises");
-        assert_eq!(InvalidDeduction::InconsistentPremises, error);
-    }
-
-    #[test]
-    fn all_inferences_in_sequence_must_be_in_fact_database() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [1, 2]);
-
-        let facts_in_proof_stage = facts! {
-            2 => fact!([x == 5] -> false),
-        };
-
-        let error =
-            verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference");
-        assert_eq!(InvalidDeduction::UnknownInference(constraint_id(1)), error);
-    }
-
-    #[test]
-    fn sequence_that_does_not_terminate_in_conflict_is_rejected() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [2, 1]);
-
-        let facts_in_proof_stage = facts! {
-            2 => fact!([x >= 5] -> [y <= 4]),
-            1 => fact!([y <= 7] -> [z != 10]),
-            4 => fact!([y <= 5] & [z != 10] -> false),
-        };
-
-        let error =
-            verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference");
-        assert_eq!(InvalidDeduction::NoConflict(vec![]), error);
-    }
-
-    #[test]
-    fn inferences_with_unsatisfied_premises_are_ignored() {
-        let premises = vec![atomic!([x >= 5])];
-        let deduction = deduction(5, premises.clone(), [2, 1]);
-
-        let facts_in_proof_stage = facts! {
-            2 => fact!([x >= 5] -> [y <= 4]),
-            1 => fact!([y <= 7] & [x >= 6] -> [z != 10]),
-            4 => fact!([y <= 5] & [z != 10] -> false),
-        };
+fn convert_ignored_inferences(
+    ignored_inference: pumpkin_checking::IgnoredInference<Atomic>,
+    facts_in_proof_stage: &BTreeMap<ConstraintId, Fact>,
+) -> IgnoredInference {
+    IgnoredInference {
+        constraint_id: facts_in_proof_stage
+            .iter()
+            .find_map(|(constraint_id, inference)| {
+                let constraint_id = *constraint_id;
+                let checker_inference = inference.clone();
+                let ignored_inference_as_checker = Fact::from(ignored_inference.inference.clone());
 
-        let error =
-            verify_deduction(&deduction, &facts_in_proof_stage).expect_err("unknown inference");
-        assert_eq!(
-            InvalidDeduction::NoConflict(vec![IgnoredInference {
-                constraint_id: constraint_id(1),
-                unsatisfied_premises: vec![atomic!([x string >= 6])],
-            }]),
-            error
-        );
+                if checker_inference == ignored_inference_as_checker {
+                    Some(constraint_id)
+                } else {
+                    None
+                }
+            })
+            .expect("one of these will match"),
+
+        unsatisfied_premises: ignored_inference
+            .unsatisfied_premises
+            .into_iter()
+            .map(|premise| match premise {
+                Atomic::True | Atomic::False => unreachable!(),
+
+                Atomic::IntAtomic(int_atomic) => IntAtomic {
+                    // Note: String is required here since the error type needs to
+                    // implement `Send`. By default we use `Rc<str>` everywhere, which
+                    // does not implement `Send`.
+                    name: String::from(int_atomic.name.as_ref()),
+                    comparison: int_atomic.comparison,
+                    value: int_atomic.value,
+                },
+            })
+            .collect(),
     }
 }
diff --git a/pumpkin-checker/src/inferences/mod.rs b/pumpkin-checker/src/inferences/mod.rs
index 6e57893af..760c7a5af 100644
--- a/pumpkin-checker/src/inferences/mod.rs
+++ b/pumpkin-checker/src/inferences/mod.rs
@@ -4,17 +4,27 @@ mod linear;
 mod nogood;
 mod time_table;
 
+use pumpkin_checking::SupportingInference;
 use pumpkin_checking::VariableState;
 
 use crate::model::Atomic;
 use crate::model::Model;
 
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Fact {
     pub premises: Vec<Atomic>,
     pub consequent: Option<Atomic>,
 }
 
+impl From<SupportingInference<Atomic>> for Fact {
+    fn from(value: SupportingInference<Atomic>) -> Self {
+        Fact {
+            premises: value.premises,
+            consequent: value.consequent,
+        }
+    }
+}
+
 impl Fact {
     /// Create a fact `premises -> false`.
     pub fn nogood(premises: Vec<Atomic>) -> Self {
diff --git a/pumpkin-checker/src/test_utils.rs b/pumpkin-checker/src/test_utils.rs
index af003e707..b05888c3d 100644
--- a/pumpkin-checker/src/test_utils.rs
+++ b/pumpkin-checker/src/test_utils.rs
@@ -1,10 +1,8 @@
 //! Contains a bunch of utilities to help write tests for the checker.
 
 use std::num::NonZero;
-use std::rc::Rc;
 
 use drcp_format::ConstraintId;
-use drcp_format::IntAtomic;
 
 /// Create a constraint ID from the given number.
 ///
@@ -90,18 +88,3 @@ macro_rules! fact {
         }
     };
 }
-
-pub(crate) fn deduction(
-    id: u32,
-    premises: impl Into<Vec<IntAtomic<Rc<str>, i32>>>,
-    sequence: impl IntoIterator<Item = u32>,
-) -> drcp_format::Deduction<Rc<str>, i32> {
-    drcp_format::Deduction {
-        constraint_id: constraint_id(id),
-        premises: premises.into(),
-        sequence: sequence
-            .into_iter()
-            .map(|id| NonZero::new(id).expect("constraint ids should be non-zero"))
-            .collect(),
-    }
-}
diff --git a/pumpkin-crates/checking/Cargo.toml b/pumpkin-crates/checking/Cargo.toml
index 485564df6..2bda5514a 100644
--- a/pumpkin-crates/checking/Cargo.toml
+++ b/pumpkin-crates/checking/Cargo.toml
@@ -10,6 +10,7 @@ authors.workspace = true
 [dependencies]
 dyn-clone = "1.0.20"
 fnv = "1.0.7"
+thiserror = "2.0.18"
 
 [lints]
 workspace = true
diff --git a/pumpkin-crates/checking/src/atomic_constraint.rs b/pumpkin-crates/checking/src/atomic_constraint.rs
index 6be4a9508..bfeddaa3a 100644
--- a/pumpkin-crates/checking/src/atomic_constraint.rs
+++ b/pumpkin-crates/checking/src/atomic_constraint.rs
@@ -8,7 +8,7 @@ use std::hash::Hash;
 /// - `identifier` identifies a variable,
 /// - `op` is a [`Comparison`],
 /// - and `value` is an integer.
-pub trait AtomicConstraint: Sized + Debug {
+pub trait AtomicConstraint: Clone + Debug + Sized {
     /// The type of identifier used for variables.
     type Identifier: Hash + Eq;
 
@@ -87,3 +87,34 @@ impl AtomicConstraint for TestAtomic {
         }
     }
 }
+
+/// Create a [`TestAtomic`] using a DSL.
+///
+/// # Example
+/// ```
+/// pumpkin_checking::test_atomic!([x >= 5]);
+/// pumpkin_checking::test_atomic!([y != 10]);
+/// ```
+#[macro_export]
+macro_rules! test_atomic {
+    (@to_comparison >=) => {
+        $crate::Comparison::GreaterEqual
+    };
+    (@to_comparison <=) => {
+        $crate::Comparison::LessEqual
+    };
+    (@to_comparison ==) => {
+        $crate::Comparison::Equal
+    };
+    (@to_comparison !=) => {
+        $crate::Comparison::NotEqual
+    };
+
+    ([$name:ident $comp:tt $value:expr]) => {
+        $crate::TestAtomic {
+            name: stringify!($name),
+            comparison: $crate::test_atomic!(@to_comparison $comp),
+            value: $value,
+        }
+    };
+}
diff --git a/pumpkin-crates/checking/src/deduction_checker.rs b/pumpkin-crates/checking/src/deduction_checker.rs
new file mode 100644
index 000000000..17a63a779
--- /dev/null
+++ b/pumpkin-crates/checking/src/deduction_checker.rs
@@ -0,0 +1,210 @@
+use crate::AtomicConstraint;
+use crate::VariableState;
+
+/// An inference that was ignored when checking a deduction.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct IgnoredInference<Atomic> {
+    /// The inference that was ignored.
+    pub inference: SupportingInference<Atomic>,
+
+    /// The premises that were not satisfied when the inference was evaluated.
+    pub unsatisfied_premises: Vec<Atomic>,
+}
+
+/// A deduction is rejected by the checker.
+#[derive(thiserror::Error, Debug, PartialEq, Eq)]
+#[error("invalid deduction")]
+pub enum InvalidDeduction<Atomic> {
+    /// The inferences in the proof stage do not derive an empty domain or an explicit
+    /// conflict.
+    #[error("no conflict was derived after applying all inferences")]
+    NoConflict(Vec<IgnoredInference<Atomic>>),
+
+    /// The premise contains mutually exclusive atomic constraints.
+    #[error("the deduction contains inconsistent premises")]
+    InconsistentPremises,
+}
+
+/// An inference used to support a deduction.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SupportingInference<Atomic> {
+    /// The premises of the inference.
+    pub premises: Vec<Atomic>,
+    /// The consequent of the inference.
+    ///
+    /// [`None`] represents the literal false. I.e., if the consequent is [`None`], then the
+    /// premises imply false.
+    pub consequent: Option<Atomic>,
+}
+
+/// Verify that a deduction is valid given the inferences in the proof stage.
+///
+/// The `inferences` are considered in the order they are provided.
+pub fn verify_deduction<Atomic>(
+    premises: impl IntoIterator<Item = Atomic>,
+    inferences: impl IntoIterator<Item = SupportingInference<Atomic>>,
+) -> Result<(), InvalidDeduction<Atomic>>
+where
+    Atomic: AtomicConstraint,
+{
+    // To verify a deduction, we assume that the premises are true. Then we go over all the
+    // facts in the sequence, and if all the premises are satisfied, we apply the consequent.
+    // At some point, this should either reach a fact without a consequent or derive an
+    // inconsistent domain.
+
+    let mut variable_state = VariableState::prepare_for_conflict_check(premises, None)
+        .map_err(|_| InvalidDeduction::InconsistentPremises)?;
+
+    let mut unused_inferences = Vec::new();
+
+    for inference in inferences.into_iter() {
+        // Collect all premises that do not evaluate to `true` under the current variable
+        // state.
+        let unsatisfied_premises = inference
+            .premises
+            .iter()
+            .filter(|premise| !variable_state.is_true(premise))
+            .cloned()
+            .collect::<Vec<_>>();
+
+        // If at least one premise is unassigned, this fact is ignored for the conflict
+        // check and recorded as unused.
+        if !unsatisfied_premises.is_empty() {
+            unused_inferences.push(IgnoredInference {
+                inference,
+                unsatisfied_premises,
+            });
+
+            continue;
+        }
+
+        // At this point the premises are satisfied so we handle the consequent of the
+        // inference.
+        match &inference.consequent {
+            Some(consequent) => {
+                if !variable_state.apply(consequent) {
+                    // If applying the consequent yields an empty domain for a
+                    // variable, then the deduction is valid.
+                    return Ok(());
+                }
+            }
+            // If the consequent is explicitly false, then the deduction is valid.
+            None => return Ok(()),
+        }
+    }
+
+    // Reaching this point means that the conjunction of inferences did not yield to a
+    // conflict. Therefore the deduction is invalid.
+    Err(InvalidDeduction::NoConflict(unused_inferences))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::test_atomic;
+
+    /// Create a [`SupportingInference`] in a DSL.
+    ///
+    /// # Example
+    /// ```
+    /// inference!([x >= 5] & [y <= 10] -> [z == 5]);
+    /// inference!([x >= 5] & [y <= 10] -> false);
+    /// ```
+    #[macro_export]
+    macro_rules! inference {
+        // Case: consequent is an Atomic
+        (
+            $($prem:tt)&+ -> [$($cons:tt)+]
+        ) => {
+            SupportingInference {
+                premises: vec![$( test_atomic!($prem) ),+],
+                consequent: Some(test_atomic!([$($cons)+])),
+            }
+        };
+
+        // Case: consequent is false (i.e., None)
+        (
+            $($prem:tt)&+ -> false
+        ) => {
+            SupportingInference {
+                premises: vec![$( test_atomic!($prem) ),+],
+                consequent: None,
+            }
+        };
+    }
+
+    #[test]
+    fn a_sequence_is_correctly_traversed() {
+        let premises = vec![test_atomic!([x >= 5])];
+
+        let inferences = vec![
+            inference!([x >= 5] -> [y <= 4]),
+            inference!([y <= 7] -> [z != 10]),
+            inference!([y <= 5] & [z != 10] -> [x <= 4]),
+        ];
+
+        verify_deduction(premises, inferences).expect("valid deduction");
+    }
+
+    #[test]
+    fn an_inference_implying_false_is_a_valid_stopping_condition() {
+        let premises = vec![test_atomic!([x >= 5])];
+
+        let inferences = vec![
+            inference!([x >= 5] -> [y <= 4]),
+            inference!([y <= 7] -> [z != 10]),
+            inference!([y <= 5] & [z != 10] -> false),
+        ];
+
+        verify_deduction(premises, inferences).expect("valid deduction");
+    }
+
+    #[test]
+    fn inconsistent_premises_are_identified() {
+        let premises = vec![test_atomic!([x >= 5]), test_atomic!([x <= 4])];
+
+        let inferences = vec![inference!([x == 5] -> false)];
+
+        let error = verify_deduction(premises, inferences).expect_err("inconsistent premises");
+        assert_eq!(InvalidDeduction::InconsistentPremises, error);
+    }
+
+    #[test]
+    fn sequence_that_does_not_terminate_in_conflict_is_rejected() {
+        let premises = vec![test_atomic!([x >= 5])];
+
+        let inferences = vec![
+            inference!([x >= 5] -> [y <= 4]),
+            inference!([y <= 7] -> [z != 10]),
+        ];
+
+        let error = verify_deduction(premises, inferences).expect_err("conflict is not reached");
+        assert_eq!(InvalidDeduction::NoConflict(vec![]), error);
+    }
+
+    #[test]
+    fn inferences_with_unsatisfied_premises_are_ignored() {
+        let premises = vec![test_atomic!([x >= 5])];
+
+        let inferences = vec![
+            inference!([x >= 5] -> [y <= 4]),
+            inference!([y <= 7] & [x >= 6] -> [z != 10]),
+            inference!([y <= 5] & [z != 10] -> false),
+        ];
+
+        let error = verify_deduction(premises, inferences).expect_err("premises are not satisfied");
+        assert_eq!(
+            InvalidDeduction::NoConflict(vec![
+                IgnoredInference {
+                    inference: inference!([y <= 7] & [x >= 6] -> [z != 10]),
+                    unsatisfied_premises: vec![test_atomic!([x >= 6])],
+                },
+                IgnoredInference {
+                    inference: inference!([y <= 5] & [z != 10] -> false),
+                    unsatisfied_premises: vec![test_atomic!([z != 10])],
+                }
+            ]),
+            error
+        );
+    }
+}
diff --git a/pumpkin-crates/checking/src/inference_checker.rs b/pumpkin-crates/checking/src/inference_checker.rs
new file mode 100644
index 000000000..f8eed5554
--- /dev/null
+++ b/pumpkin-crates/checking/src/inference_checker.rs
@@ -0,0 +1,49 @@
+use std::fmt::Debug;
+
+use dyn_clone::DynClone;
+
+use crate::AtomicConstraint;
+use crate::VariableState;
+
+/// An inference checker tests whether the given state is a conflict under the sematics of an
+/// inference rule.
+pub trait InferenceChecker<Atomic: AtomicConstraint>: Debug + DynClone {
+    /// Returns `true` if `state` is a conflict, and `false` if not.
+    ///
+    /// For the conflict check, all the premises are true in the state and the consequent, if
+    /// present, if false.
+    fn check(
+        &self,
+        state: VariableState<Atomic>,
+        premises: &[Atomic],
+        consequent: Option<&Atomic>,
+    ) -> bool;
+}
+
+/// Wrapper around `Box<dyn InferenceChecker<Atomic>>` that implements [`Clone`].
+#[derive(Debug)]
+pub struct BoxedChecker<Atomic: AtomicConstraint>(Box<dyn InferenceChecker<Atomic>>);
+
+impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
+    fn clone(&self) -> Self {
+        BoxedChecker(dyn_clone::clone_box(&*self.0))
+    }
+}
+
+impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
+    fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
+        BoxedChecker(value)
+    }
+}
+
+impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
+    /// See [`InferenceChecker::check`].
+    pub fn check(
+        &self,
+        variable_state: VariableState<Atomic>,
+        premises: &[Atomic],
+        consequent: Option<&Atomic>,
+    ) -> bool {
+        self.0.check(variable_state, premises, consequent)
+    }
+}
diff --git a/pumpkin-crates/checking/src/lib.rs b/pumpkin-crates/checking/src/lib.rs
index 6fb8fc265..88ffd94e9 100644
--- a/pumpkin-crates/checking/src/lib.rs
+++ b/pumpkin-crates/checking/src/lib.rs
@@ -4,59 +4,17 @@
 //! inferences are sound w.r.t. an inference rule.
 
 mod atomic_constraint;
+mod deduction_checker;
+mod inference_checker;
 mod int_ext;
 mod union;
 mod variable;
 mod variable_state;
 
-use std::fmt::Debug;
-
 pub use atomic_constraint::*;
-use dyn_clone::DynClone;
+pub use deduction_checker::*;
+pub use inference_checker::*;
 pub use int_ext::*;
 pub use union::*;
 pub use variable::*;
 pub use variable_state::*;
-
-/// An inference checker tests whether the given state is a conflict under the sematics of an
-/// inference rule.
-pub trait InferenceChecker<Atomic: AtomicConstraint>: Debug + DynClone {
-    /// Returns `true` if `state` is a conflict, and `false` if not.
-    ///
-    /// For the conflict check, all the premises are true in the state and the consequent, if
-    /// present, if false.
-    fn check(
-        &self,
-        state: VariableState<Atomic>,
-        premises: &[Atomic],
-        consequent: Option<&Atomic>,
-    ) -> bool;
-}
-
-/// Wrapper around `Box<dyn InferenceChecker<Atomic>>` that implements [`Clone`].
-#[derive(Debug)]
-pub struct BoxedChecker<Atomic: AtomicConstraint>(Box<dyn InferenceChecker<Atomic>>);
-
-impl<Atomic: AtomicConstraint> Clone for BoxedChecker<Atomic> {
-    fn clone(&self) -> Self {
-        BoxedChecker(dyn_clone::clone_box(&*self.0))
-    }
-}
-
-impl<Atomic: AtomicConstraint> From<Box<dyn InferenceChecker<Atomic>>> for BoxedChecker<Atomic> {
-    fn from(value: Box<dyn InferenceChecker<Atomic>>) -> Self {
-        BoxedChecker(value)
-    }
-}
-
-impl<Atomic: AtomicConstraint> BoxedChecker<Atomic> {
-    /// See [`InferenceChecker::check`].
-    pub fn check(
-        &self,
-        variable_state: VariableState<Atomic>,
-        premises: &[Atomic],
-        consequent: Option<&Atomic>,
-    ) -> bool {
-        self.0.check(variable_state, premises, consequent)
-    }
-}