diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java
index f31e145..7f90582 100644
--- a/src/main/java/org/rairlab/planner/Operations.java
+++ b/src/main/java/org/rairlab/planner/Operations.java
@@ -2,7 +2,7 @@ package org.rairlab.planner;
 
 import org.rairlab.planner.utils.Visualizer;
 import org.rairlab.shadow.prover.core.Prover;
-import org.rairlab.shadow.prover.core.SnarkWrapper;
+import org.rairlab.shadow.prover.core.ccprovers.CognitiveCalculusProver;
 import org.rairlab.shadow.prover.core.proof.Justification;
 import org.rairlab.shadow.prover.representations.formula.BiConditional;
 import org.rairlab.shadow.prover.representations.formula.Formula;
@@ -44,9 +44,7 @@ public class Operations {
         applyCache.clear();
     }
     static {
-        prover = SnarkWrapper.getInstance();
-
-
+        prover =  new CognitiveCalculusProver();
     }
 
     public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {
@@ -192,6 +190,7 @@ public class Operations {
             // Apply binding to get grounded action and calculate the next state
             // newState = (oldState - Deletions(a)) U Additions(a)
             Action groundedAction = action.instantiate(binding);
+
             State newState = State.initializeWith(Sets.union(
                 Sets.difference(state.getFormulae(), groundedAction.getDeletions()),
                 groundedAction.getAdditions()
diff --git a/src/main/java/org/rairlab/planner/State.java b/src/main/java/org/rairlab/planner/State.java
index 8e0e8d9..38de048 100644
--- a/src/main/java/org/rairlab/planner/State.java
+++ b/src/main/java/org/rairlab/planner/State.java
@@ -1,7 +1,5 @@
 package org.rairlab.planner;
 
-import org.rairlab.shadow.prover.core.Prover;
-import org.rairlab.shadow.prover.core.SnarkWrapper;
 import org.rairlab.shadow.prover.representations.formula.Formula;
 import org.rairlab.shadow.prover.utils.CollectionUtils;
 import org.rairlab.shadow.prover.utils.Reader;
@@ -14,7 +12,6 @@ import java.util.Set;
 public class State {
 
     final Set<Formula> formulae;
-    private static final Prover prover = SnarkWrapper.getInstance();
     static Formula FALSE;
 
     static{
diff --git a/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj
new file mode 100644
index 0000000..da85893
--- /dev/null
+++ b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj
@@ -0,0 +1,126 @@
+{:name "GrapeVine"
+    :background [
+        (agent a)
+        (agent b)
+        (agent c)
+        (room p1)
+        (room p2)
+        (not (= a b))
+        (not (= a c))
+        (not (= b c))
+    ]
+    :actions [
+        (define-action left [?a] {
+            :preconditions [
+                (agent ?a) ; Type restriction
+                (at ?a p2)
+            ]
+            :additions [
+                (at ?a p1)
+                (not (at ?a p2))
+            ]
+            :deletions [
+                (at ?a p2)
+                (not (at ?a p1))
+            ]
+        })
+
+
+        (define-action right [?a] {
+            :preconditions [
+                (agent ?a) ; Type restriction
+                (at ?a p1)
+            ]
+            :additions [
+                (at ?a p2)
+                (not (at ?a p1))
+            ]
+            :deletions [
+                (at ?a p1)
+                (not (at ?a p2))
+            ]
+        })
+
+        (define-action share-both [?a1 ?a2 ?a3 ?r] {
+            :preconditions [
+                ; Type restrictions
+                (agent ?a1)
+                (agent ?a2)
+                (agent ?a3)
+                (room ?r)
+                ; Precondition
+                (at ?a1 ?r)
+                (at ?a2 ?r)
+                (at ?a3 ?r)
+                (not (= ?a1 ?a2))
+                (not (= ?a1 ?a3))
+                (not (= ?a2 ?a3))
+            ]
+            :additions [
+                (Believes! ?a2 (the ?a1))
+                (Believes ?a3 (the ?a1))
+                (Believes ?a1 (Believes! ?a2 (the ?a1)))
+                (Believes ?a1 (Believes! ?a3 (the ?a1)))
+            ]
+            :deletions [
+                (not (Believes! ?a2 (the ?a1)))
+                (not (Believes! ?a3 (the ?a1)))
+            ]
+        })
+
+        (define-action share-single [?a1 ?a2 ?a3 ?r] {
+            :preconditions [
+                ; Type restrictions
+                (agent ?a1)
+                (agent ?a2)
+                (agent ?a3)
+                (room ?r)
+                ; Precondition
+                (at ?a1 ?r)
+                (at ?a2 ?r)
+                (not (at ?a3 ?r))
+                (not (= ?a1 ?a2))
+                (not (= ?a1 ?a3))
+                (not (= ?a2 ?a3))
+            ]
+            :additions [
+                (Believes! ?a2 (the ?a1))
+                (Believes! ?a1 (Believes! ?a2 (the ?a1)))
+            ]
+            :deletions [
+                (not (Believes! ?a2 (the ?a1)))
+            ]
+        })
+
+    ]
+    :start [
+        ; Locations
+        (at a p1)
+        (not (at a p2))
+        (at b p1)
+        (not (at b p2))
+        (at c p1)
+        (not (at c p2))
+
+        ; Each agent has a secret
+        (Believes! a (the a))
+        (Believes! b (the b))
+        (Believes! c (the c))
+
+        ; No one believes a's secret
+        (not (Believes! b (the a)))
+        (not (Believes! c (the a)))
+    ]
+    :goal [
+        (Believes! b (the a))
+        (Believes! a (Believes! b (the a)))
+        (not (Believes! c (the a)))
+    ]
+
+}
+
+
+
+
+
+