diff --git a/Cargo.lock b/Cargo.lock
index 9075aa4..dad8ed9 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -67,6 +67,12 @@ version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8"
 
+[[package]]
+name = "bitflags"
+version = "2.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "812e12b5285cc515a9c72a5c1d3b6d46a19dac5acfef5265968c166106e31dd3"
+
 [[package]]
 name = "cfg-if"
 version = "1.0.4"
@@ -79,6 +85,15 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
 
+[[package]]
+name = "convert_case"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "633458d4ef8c78b72454de2d54fd6ab2e60f9e02be22f3c6104cdc8a4e0fceb9"
+dependencies = [
+ "unicode-segmentation",
+]
+
 [[package]]
 name = "corosensei"
 version = "0.3.2"
@@ -92,6 +107,64 @@ dependencies = [
  "windows-sys 0.59.0",
 ]
 
+[[package]]
+name = "crossterm"
+version = "0.29.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d8b9f2e4c67f833b660cdb0a3523065869fb35570177239812ed4c905aeff87b"
+dependencies = [
+ "bitflags",
+ "crossterm_winapi",
+ "derive_more",
+ "document-features",
+ "mio",
+ "parking_lot",
+ "rustix",
+ "signal-hook",
+ "signal-hook-mio",
+ "winapi",
+]
+
+[[package]]
+name = "crossterm_winapi"
+version = "0.9.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b"
+dependencies = [
+ "winapi",
+]
+
+[[package]]
+name = "derive_more"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d751e9e49156b02b44f9c1815bcb94b984cdcc4396ecc32521c739452808b134"
+dependencies = [
+ "derive_more-impl",
+]
+
+[[package]]
+name = "derive_more-impl"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "799a97264921d8623a957f6c3b9011f3b5492f557bbb7a5a19b7fa6d06ba8dcb"
+dependencies = [
+ "convert_case",
+ "proc-macro2",
+ "quote",
+ "rustc_version",
+ "syn",
+]
+
+[[package]]
+name = "document-features"
+version = "0.2.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d4b8a88685455ed29a21542a33abd9cb6510b6b129abadabdcef0f4c55bc8f61"
+dependencies = [
+ "litrs",
+]
+
 [[package]]
 name = "env_filter"
 version = "0.1.4"
@@ -115,6 +188,16 @@ dependencies = [
  "log",
 ]
 
+[[package]]
+name = "errno"
+version = "0.3.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
+dependencies = [
+ "libc",
+ "windows-sys 0.61.2",
+]
+
 [[package]]
 name = "is_terminal_polyfill"
 version = "1.70.2"
@@ -151,6 +234,27 @@ version = "0.2.180"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc"
 
+[[package]]
+name = "linux-raw-sys"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "df1d3c3b53da64cf5760482273a98e575c651a67eec7f77df96b5b642de8f039"
+
+[[package]]
+name = "litrs"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "11d3d7f243d5c5a8b9bb5d6dd2b1602c0cb0b9db1621bafc7ed66e35ff9fe092"
+
+[[package]]
+name = "lock_api"
+version = "0.4.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "224399e74b87b5f3557511d98dff8b14089b3dadafcab6bb93eab67d3aace965"
+dependencies = [
+ "scopeguard",
+]
+
 [[package]]
 name = "log"
 version = "0.4.29"
@@ -163,11 +267,24 @@ version = "2.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79"
 
+[[package]]
+name = "mio"
+version = "1.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a69bcab0ad47271a0234d9422b131806bf3968021e5dc9328caf2d4cd58557fc"
+dependencies = [
+ "libc",
+ "log",
+ "wasi",
+ "windows-sys 0.61.2",
+]
+
 [[package]]
 name = "nanolog"
 version = "0.1.0"
 dependencies = [
  "corosensei",
+ "crossterm",
  "env_logger",
  "log",
  "winnow",
@@ -179,6 +296,29 @@ version = "1.70.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
 
+[[package]]
+name = "parking_lot"
+version = "0.12.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "93857453250e3077bd71ff98b6a65ea6621a19bb0f559a85248955ac12c45a1a"
+dependencies = [
+ "lock_api",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "parking_lot_core"
+version = "0.9.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2621685985a2ebf1c516881c026032ac7deafcda1a2c9b7850dc81e3dfcb64c1"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "redox_syscall",
+ "smallvec",
+ "windows-link",
+]
+
 [[package]]
 name = "portable-atomic"
 version = "1.13.1"
@@ -212,6 +352,15 @@ dependencies = [
  "proc-macro2",
 ]
 
+[[package]]
+name = "redox_syscall"
+version = "0.5.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "regex"
 version = "1.12.3"
@@ -241,12 +390,40 @@ version = "0.8.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a96887878f22d7bad8a3b6dc5b7440e0ada9a245242924394987b21cf2210a4c"
 
+[[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
+[[package]]
+name = "rustix"
+version = "1.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "146c9e247ccc180c1f61615433868c99f3de3ae256a30a43b49f67c2d9171f34"
+dependencies = [
+ "bitflags",
+ "errno",
+ "libc",
+ "linux-raw-sys",
+ "windows-sys 0.61.2",
+]
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
+[[package]]
+name = "semver"
+version = "1.0.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2"
+
 [[package]]
 name = "serde_core"
 version = "1.0.228"
@@ -267,6 +444,43 @@ dependencies = [
  "syn",
 ]
 
+[[package]]
+name = "signal-hook"
+version = "0.3.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d881a16cf4426aa584979d30bd82cb33429027e42122b169753d6ef1085ed6e2"
+dependencies = [
+ "libc",
+ "signal-hook-registry",
+]
+
+[[package]]
+name = "signal-hook-mio"
+version = "0.2.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b75a19a7a740b25bc7944bdee6172368f988763b744e3d4dfe753f6b4ece40cc"
+dependencies = [
+ "libc",
+ "mio",
+ "signal-hook",
+]
+
+[[package]]
+name = "signal-hook-registry"
+version = "1.4.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c4db69cba1110affc0e9f7bcd48bbf87b3f4fc7c61fc9155afd4c469eb3d6c1b"
+dependencies = [
+ "errno",
+ "libc",
+]
+
+[[package]]
+name = "smallvec"
+version = "1.15.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03"
+
 [[package]]
 name = "syn"
 version = "2.0.114"
@@ -284,12 +498,46 @@ version = "1.0.22"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9312f7c4f6ff9069b165498234ce8be658059c6728633667c526e27dc2cf1df5"
 
+[[package]]
+name = "unicode-segmentation"
+version = "1.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f6ccf251212114b54433ec949fd6a7841275f9ada20dddd2f29e9ceea4501493"
+
 [[package]]
 name = "utf8parse"
 version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
+[[package]]
+name = "wasi"
+version = "0.11.1+wasi-snapshot-preview1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
+
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+
 [[package]]
 name = "windows-link"
 version = "0.2.1"
diff --git a/Cargo.toml b/Cargo.toml
index b277a62..9e43a23 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,6 +5,7 @@ edition = "2024"
 
 [dependencies]
 corosensei = "0.3.2"
+crossterm = "0.29.0"
 env_logger = "0.11.8"
 log = "0.4.29"
 winnow = "0.7.14"
diff --git a/src/main.rs b/src/main.rs
index d313fe1..a5d1095 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,12 +1,12 @@
-use corosensei::Coroutine;
 use nanolog::ast::Body;
 use nanolog::ast::Module;
 use nanolog::ast::Predicate;
+use nanolog::prover::Constraints;
 
 fn main()
 {
     env_logger::builder()
-        .filter_level(log::LevelFilter::Info)
+        .filter_level(log::LevelFilter::Debug)
         .format_timestamp(None)
         .format_module_path(false)
         .init();
@@ -16,21 +16,32 @@ fn main()
         integer(s(X)) :- integer(X).
         add(X, zero, X).
         add(X, s(Y), Z) :- add(s(X), Y, Z).
+        mult(zero, X, zero).
+        mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
+
     "
     .into();
 
-    // let a: Predicate = "integer(s(zero))".into();
+    // let a: Predicate = "integer(s(Y))".into();
     // let b: Predicate = "integer(s(X))".into();
     //
-    // println!("{:?}", a.unify(&b));
+    // println!("{}", a.unify(&b).unwrap());
 
-    let body: Body = "add(s(s(zero)), s(zero), s(s(s(zero))))".into();
-    let body: Body = "add(s(zero), s(zero), X).".into();
-    body.prove_in_module(&module).next().next();
-
-    // let body: Body = "integer(X).".into();
+    // let body: Body = "add(s(s(zero)), s(zero), s(s(s(zero))))".into();
+    // let body: Body = "add(s(zero), s(zero), X).".into();
     // body.prove_in_module(&module).next().next();
+    //
 
+    let body: Body = "mult(s(zero), s(s(zero)), X)".into();
+    let mut prover = body.prove_in_module(&module, Constraints::default());
+    while let Some(c) = prover.prove()
+    {
+        println!("{}", c.simplified());
+        //println!("{}", c);
+
+        let _ = std::io::stdin().read_line(&mut String::new());
+    }
+    //
     //println!("{}", module);
     //
 }
diff --git a/src/prover.rs b/src/prover.rs
index e971a34..137b8e0 100644
--- a/src/prover.rs
+++ b/src/prover.rs
@@ -1,31 +1,32 @@
 use std::cell::Cell;
-use std::cell::RefCell;
 use std::collections::HashMap;
 use std::fmt::Display;
 use std::fmt::write;
+use std::ops;
+use std::ops::Rem;
 use std::rc::Rc;
 
 use corosensei::Coroutine;
 use corosensei::Yielder;
+use log::debug;
 use log::info;
-use log::warn;
 
 use crate::ast::Body;
 use crate::ast::Clause;
 use crate::ast::Module;
 use crate::ast::Predicate;
+use crate::prover;
 
 #[derive(Clone, Debug)]
-pub struct Constraint
+pub struct Constraints
 {
-    variable: String,
-    predicate: Predicate,
+    set: HashMap<String, Predicate>,
 }
 
 struct Context<'a, 'b>
 {
     module: &'a Module,
-    yielder: &'b Yielder<(), Vec<Constraint>>,
+    yielder: &'b Yielder<(), Constraints>,
     depth: usize,
     global_counter: Rc<Cell<usize>>,
 }
@@ -45,36 +46,55 @@ impl Context<'_, '_>
 
 pub struct Prover
 {
-    coroutine: Coroutine<(), Vec<Constraint>, ()>,
+    coroutine: Option<Coroutine<(), Constraints, ()>>,
 }
 
 impl Prover
 {
-    pub fn next(mut self) -> Prover
+    pub fn prove(&mut self) -> Option<Constraints>
     {
-        self.coroutine.resume(());
-        self
+        if let Some(coroutine) = self.coroutine.as_mut()
+        {
+            match coroutine.resume(())
+            {
+                corosensei::CoroutineResult::Yield(constraints) => Some(constraints),
+                corosensei::CoroutineResult::Return(_) =>
+                {
+                    self.coroutine = None;
+                    None
+                }
+            }
+        }
+        else
+        {
+            None
+        }
     }
 }
 
 impl Body
 {
-    pub fn prove_in_module(&self, module: &Module) -> Prover
+    pub fn prove_in_module(&self, module: &Module, constraints: Constraints) -> Prover
     {
         let cloned_body = self.clone();
         let cloned_module = module.clone();
         let coroutine = Coroutine::new(move |yielder, ()| {
-            cloned_body.prove(Context {
-                module: &cloned_module,
-                depth: 0,
-                yielder,
-                global_counter: Rc::new(Cell::new(0)),
-            });
+            cloned_body.prove(
+                Context {
+                    module: &cloned_module,
+                    depth: 0,
+                    yielder,
+                    global_counter: Rc::new(Cell::new(0)),
+                },
+                &constraints,
+            );
         });
-        Prover { coroutine }
+        Prover {
+            coroutine: Some(coroutine),
+        }
     }
 
-    fn prove(&self, context: Context<'_, '_>)
+    fn prove(&self, context: Context<'_, '_>, constraints: &Constraints)
     {
         match self
         {
@@ -85,24 +105,41 @@ impl Body
                     predicate.prove_with_clause(
                         &candidate.unique(context.global_counter.clone()),
                         context.descend(),
+                        constraints,
                     );
                 }
             }
-            Body::And(x) => x.iter().for_each(|x| x.prove(context.descend())),
+            Body::And(x) =>
+            {
+                if x.len() == 1
+                {
+                    x[0].prove(context.descend(), constraints)
+                }
+                else
+                {
+                    let last = x.last().unwrap();
+                    let first = Body::And(Vec::from(&x[..(x.len() - 1)]));
+                    let mut prover = first.prove_in_module(context.module, constraints.clone());
+                    while let Some(new_constraints) = prover.prove()
+                    {
+                        last.clone().prove(context.descend(), &new_constraints);
+                    }
+                }
+            }
             Body::Or(x) => x.iter().for_each(|x| {
                 info!(target: "Proving", "{}", self);
-                x.prove(context.descend())
+                x.prove(context.descend(), constraints)
             }),
         }
     }
 
-    pub fn substitute(&mut self, constraint: &Constraint)
+    pub fn substitute(&mut self, constraints: &Constraints)
     {
         match self
         {
-            Body::Term(predicate) => predicate.substitute(constraint),
-            Body::And(items) => items.iter_mut().for_each(|x| x.substitute(constraint)),
-            Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraint)),
+            Body::Term(predicate) => predicate.substitute(constraints),
+            Body::And(items) => items.iter_mut().for_each(|x| x.substitute(constraints)),
+            Body::Or(items) => items.iter_mut().for_each(|x| x.substitute(constraints)),
         }
     }
 
@@ -129,28 +166,40 @@ impl Body
 
 impl Predicate
 {
-    fn prove_with_clause(&self, clause: &Clause, context: Context<'_, '_>)
+    fn prove_with_clause(
+        &self,
+        clause: &Clause,
+        context: Context<'_, '_>,
+        constraints: &Constraints,
+    )
     {
         info!(target: "With", "{}", clause);
-        if let Some(constraints) = self.unify(&clause.head)
+        if let Some(unification_constraints) = self.unify(&clause.head)
         {
-            for x in constraints.iter()
+            let new_constraints = if let Some(c) = unification_constraints.merged(constraints)
             {
-                info!(target: "Constraints", "{}", x);
+                c
             }
+            else
+            {
+                info!(target: "Contradiction", "backtracking");
+                return; // Contradiction, backtrack
+            };
+
+            info!(target: "Constraints", "{}", new_constraints);
 
             match &clause.body
             {
                 Some(body) =>
                 {
                     let mut next = body.clone();
-                    constraints.iter().for_each(|x| next.substitute(x));
-                    next.prove(context.descend())
+                    next.substitute(constraints);
+                    next.prove(context.descend(), &new_constraints)
                 }
                 None =>
                 {
                     info!(target: "[Solution]", "true.");
-                    context.yielder.suspend(constraints);
+                    context.yielder.suspend(new_constraints.clone());
                 }
             }
         }
@@ -160,42 +209,40 @@ impl Predicate
         }
     }
 
-    pub fn unify(&self, other: &Predicate) -> Option<Vec<Constraint>>
+    pub fn unify(&self, other: &Predicate) -> Option<Constraints>
     {
         match self
         {
-            Predicate::Variable(variable) => Some(vec![Constraint {
-                variable: variable.clone(),
-                predicate: other.clone(),
-            }]),
+            Predicate::Variable(variable) =>
+            {
+                let mut c = Constraints::new();
+                c.append(variable.clone(), other.clone());
+                Some(c)
+            }
             Predicate::Fixed(name, predicates) => match other
             {
-                Predicate::Variable(variable) => Some(vec![Constraint {
-                    variable: variable.clone(),
-                    predicate: self.clone(),
-                }]),
+                Predicate::Variable(variable) =>
+                {
+                    let mut c = Constraints::new();
+                    c.append(variable.clone(), self.clone());
+                    Some(c)
+                }
                 Predicate::Fixed(other_name, other_predicates)
                     if other_name == name && predicates.len() == other_predicates.len() =>
                 {
                     if predicates.is_empty()
                     {
-                        Some(vec![])
+                        Some(Constraints::new())
                     }
                     else
                     {
-                        let mut new_constraints = vec![];
+                        let mut new_constraints = Constraints::new();
                         for (a, b) in predicates.iter().zip(other_predicates)
                         {
-                            if let Some(constraints) = a.unify(b)
+                            if let Some(constraints) = b.unify(a)
+                                && let Some(merged) = constraints.merged(&new_constraints)
                             {
-                                for c in constraints.iter()
-                                {
-                                    if c.merge_into(&mut new_constraints).is_none()
-                                    {
-                                        warn!(target: "Contradiction", "The property is contradictory.");
-                                        return None;
-                                    }
-                                }
+                                new_constraints = merged;
                             }
                             else
                             {
@@ -210,19 +257,35 @@ impl Predicate
         }
     }
 
-    pub fn substitute(&mut self, constraint: &Constraint)
+    pub fn substitute(&mut self, constraints: &Constraints)
     {
         match self
         {
-            Predicate::Variable(name) if *name == constraint.variable =>
+            Predicate::Variable(name) =>
             {
-                *self = constraint.predicate.clone()
-            }
-            Predicate::Variable(_) => (),
-            Predicate::Fixed(_, predicates) =>
-            {
-                predicates.iter_mut().for_each(|x| x.substitute(constraint))
+                if let Some(predicate) = constraints.set.get(name)
+                {
+                    let mut predicate = predicate.clone();
+                    predicate.substitute(constraints);
+                    *self = predicate;
+                }
             }
+            Predicate::Fixed(_, predicates) => predicates
+                .iter_mut()
+                .for_each(|x| x.substitute(constraints)),
+        }
+    }
+
+    pub fn contains_variable(&self, variable: &String) -> bool
+    {
+        match self
+        {
+            Predicate::Variable(name) => name == variable,
+            Predicate::Fixed(_, predicates) => predicates
+                .iter()
+                .map(|x| x.contains_variable(variable))
+                .reduce(|a, b| a || b)
+                .unwrap_or(false),
         }
     }
 
@@ -276,33 +339,108 @@ impl Clause
     }
 }
 
-impl Display for Constraint
+impl Constraints
 {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    pub fn new() -> Self
     {
-        write!(f, "{} = {}", self.variable, self.predicate)
+        Constraints {
+            set: HashMap::new(),
+        }
     }
-}
 
-impl Constraint
-{
-    fn merge_into(&self, constraints: &mut Vec<Constraint>) -> Option<()>
+    pub fn simplified(&self) -> Constraints
     {
-        // Check if constraint is contradictory with other constraints
-        for c in constraints.iter()
+        // Perform max substitution
+        let mut new_set = Constraints::new();
+        for (var, predicate) in self.set.iter()
         {
-            if self.variable == c.variable
+            let mut simpler = predicate.clone();
+            simpler.substitute(self);
+            new_set.set.insert(var.clone(), simpler);
+        }
+
+        // Remove stray variables
+        let mut cleaned_set = new_set.clone();
+        'outer: for (var, _) in new_set.set.iter()
+        {
+            if var.chars().next().is_some_and(|x| x == '_')
             {
-                let unification = self.predicate.unify(&c.predicate);
-                if unification.is_none()
+                for (_, pred) in new_set.set.iter()
                 {
-                    info!(target: "Constraint", "Contradiction. Abort");
-                    return None;
+                    if pred.contains_variable(var)
+                    {
+                        continue 'outer;
+                    }
+                    cleaned_set.set.remove(var);
                 }
             }
         }
+        cleaned_set
+    }
 
-        constraints.push(self.clone());
-        Some(())
+    pub fn merged(&self, constraints: &Constraints) -> Option<Constraints>
+    {
+        let mut new = self.clone();
+        for (var, pred) in constraints.set.iter()
+        {
+            if !new.append(var.clone(), pred.clone())
+            {
+                return None;
+            };
+        }
+        Some(new)
+    }
+
+    pub fn append(&mut self, variable: String, predicate: Predicate) -> bool
+    {
+        if let Some(constraint) = self.set.get(&variable)
+        {
+            if let Some(constraints) = predicate.unify(constraint)
+            {
+                if let Some(new) = self.merged(&constraints)
+                {
+                    *self = new;
+                    true
+                }
+                else
+                {
+                    false
+                }
+            }
+            else
+            {
+                false
+            }
+        }
+        else
+        {
+            self.set.insert(variable, predicate);
+            true
+        }
+    }
+}
+
+impl Default for Constraints
+{
+    fn default() -> Self
+    {
+        Self::new()
+    }
+}
+
+impl Display for Constraints
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
+    {
+        let len = self.set.len();
+        for (i, (variable, predicate)) in self.set.iter().enumerate()
+        {
+            write!(f, "{} = {}", variable, predicate)?;
+            if i != len - 1
+            {
+                write!(f, ", ")?;
+            }
+        }
+        Ok(())
     }
 }