diff --git a/src/arachne.c b/src/arachne.c
index 9eed29c..65cf1ca 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2231,6 +2231,147 @@ iterate_buffer_attacks (void)
     }
 }
 
+//! Arachne single claim
+int
+arachneClaim (Claimlist cl)
+{
+  // Skip the dummy claims
+  if (!isTermEqual (cl->type, CLAIM_Empty))
+    {
+      // Any other claims might be filterered
+      if (switches.filterClaim == NULL || switches.filterClaim == cl->type)
+	{
+	  // Some claims are always true!
+	  if (!cl->alwaystrue)
+	    {
+	      // others we simply test...
+	      int run;
+	      int newruns;
+	      Protocol p;
+	      Role r;
+
+	      newruns = 0;
+	      sys->current_claim = cl;
+	      attack_length = INT_MAX;
+	      attack_leastcost = INT_MAX;
+	      cl->complete = 1;
+	      p = (Protocol) cl->protocol;
+	      r = (Role) cl->role;
+
+	      if (switches.output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Testing Claim ");
+		  termPrint (cl->type);
+		  eprintf (" from ");
+		  termPrint (p->nameterm);
+		  eprintf (", ");
+		  termPrint (r->nameterm);
+		  eprintf (" at index %i.\n", cl->ev);
+		}
+	      indentDepth++;
+
+	      run = semiRunCreate (p, r);
+	      newruns++;
+	      {
+		int newgoals;
+
+		int realStart (void)
+		{
+#ifdef DEBUG
+		  if (DEBUGL (5))
+		    {
+		      printSemiState ();
+		    }
+#endif
+		  return iterate_buffer_attacks ();
+		}
+
+		proof_suppose_run (run, 0, cl->ev + 1);
+		newgoals = add_read_goals (run, 0, cl->ev + 1);
+
+		    /**
+		     * Add initial knowledge node
+		     */
+		{
+		  Termlist m0tl;
+		  Term m0t;
+		  int m0run;
+
+		  m0tl = knowledgeSet (sys->know);
+		  m0t = termlist_to_tuple (m0tl);
+		  // eprintf("Initial intruder knowledge node for ");
+		  // termPrint(m0t);
+		  // eprintf("\n");
+		  I_M->roledef->message = m0t;
+		  m0run = semiRunCreate (INTRUDER, I_M);
+		  newruns++;
+		  proof_suppose_run (m0run, 0, 1);
+		  sys->runs[m0run].height = 1;
+
+		  {
+		      /**
+		       * Add specific goal info and iterate algorithm
+		       */
+		    add_claim_specifics (sys, cl,
+					 roledef_shift (sys->runs[run].
+							start, cl->ev),
+					 realStart);
+		  }
+
+
+		  // remove initial knowledge node
+		  termDelete (m0t);
+		  termlistDelete (m0tl);
+		  semiRunDestroy ();
+		  newruns--;
+		}
+		// remove claiming run goals 
+		goal_remove_last (newgoals);
+		semiRunDestroy ();
+		newruns--;
+	      }
+	      //! Destroy
+	      while (sys->maxruns > 0 && newruns > 0)
+		{
+		  semiRunDestroy ();
+		  newruns--;
+		}
+#ifdef DEBUG
+	      if (sys->bindings != NULL)
+		{
+		  error ("sys->bindings NOT empty after claim test.");
+		}
+	      if (sys->maxruns != 0)
+		{
+		  error ("%i undestroyed runs left after claim test.",
+			 sys->maxruns);
+		}
+	      if (newruns != 0)
+		{
+		  error ("Lost %i runs after claim test.", newruns);
+		}
+#endif
+
+	      //! Indent back
+	      indentDepth--;
+
+	      if (switches.output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Proof complete for this claim.\n");
+		}
+	    }
+	}
+      return true;
+    }
+  else
+    {
+      return false;
+    }
+}
+
+
 //! Main code for Arachne
 /**
  * For this test, we manually set up some stuff.
@@ -2241,6 +2382,7 @@ int
 arachne ()
 {
   Claimlist cl;
+  int count;
 
   int print_send (Protocol p, Role r, Roledef rd, int index)
   {
@@ -2304,145 +2446,21 @@ arachne ()
   indentDepth = 0;
   proofDepth = 0;
   cl = sys->claimlist;
+  count = 0;
   while (cl != NULL)
     {
       /**
        * Check each claim
        */
-
-      // Skip the dummy claims
-      if (!isTermEqual (cl->type, CLAIM_Empty))
+      if (arachneClaim (cl))
 	{
-	  // Any other claims might be filterered
-	  if (switches.filterClaim == NULL
-	      || switches.filterClaim == cl->type)
-	    {
-	      // Some claims are always true!
-	      if (!cl->alwaystrue)
-		{
-		  // others we simply test...
-		  int run;
-		  int newruns;
-		  Protocol p;
-		  Role r;
-
-		  newruns = 0;
-		  sys->current_claim = cl;
-		  attack_length = INT_MAX;
-		  attack_leastcost = INT_MAX;
-		  cl->complete = 1;
-		  p = (Protocol) cl->protocol;
-		  r = (Role) cl->role;
-
-		  if (switches.output == PROOF)
-		    {
-		      indentPrint ();
-		      eprintf ("Testing Claim ");
-		      termPrint (cl->type);
-		      eprintf (" from ");
-		      termPrint (p->nameterm);
-		      eprintf (", ");
-		      termPrint (r->nameterm);
-		      eprintf (" at index %i.\n", cl->ev);
-		    }
-		  indentDepth++;
-
-		  run = semiRunCreate (p, r);
-		  newruns++;
-		  {
-		    int newgoals;
-
-		    int realStart (void)
-		    {
-#ifdef DEBUG
-		      if (DEBUGL (5))
-			{
-			  printSemiState ();
-			}
-#endif
-		      return iterate_buffer_attacks ();
-		    }
-
-		    proof_suppose_run (run, 0, cl->ev + 1);
-		    newgoals = add_read_goals (run, 0, cl->ev + 1);
-
-		    /**
-		     * Add initial knowledge node
-		     */
-		    {
-		      Termlist m0tl;
-		      Term m0t;
-		      int m0run;
-
-		      m0tl = knowledgeSet (sys->know);
-		      m0t = termlist_to_tuple (m0tl);
-		      // eprintf("Initial intruder knowledge node for ");
-		      // termPrint(m0t);
-		      // eprintf("\n");
-		      I_M->roledef->message = m0t;
-		      m0run = semiRunCreate (INTRUDER, I_M);
-		      newruns++;
-		      proof_suppose_run (m0run, 0, 1);
-		      sys->runs[m0run].height = 1;
-
-		      {
-		      /**
-		       * Add specific goal info and iterate algorithm
-		       */
-			add_claim_specifics (sys, cl,
-					     roledef_shift (sys->runs[run].
-							    start, cl->ev),
-					     realStart);
-		      }
-
-
-		      // remove initial knowledge node
-		      termDelete (m0t);
-		      termlistDelete (m0tl);
-		      semiRunDestroy ();
-		      newruns--;
-		    }
-		    // remove claiming run goals 
-		    goal_remove_last (newgoals);
-		    semiRunDestroy ();
-		    newruns--;
-		  }
-		  //! Destroy
-		  while (sys->maxruns > 0 && newruns > 0)
-		    {
-		      semiRunDestroy ();
-		      newruns--;
-		    }
-#ifdef DEBUG
-		  if (sys->bindings != NULL)
-		    {
-		      error ("sys->bindings NOT empty after claim test.");
-		    }
-		  if (sys->maxruns != 0)
-		    {
-		      error ("%i undestroyed runs left after claim test.",
-			     sys->maxruns);
-		    }
-		  if (newruns != 0)
-		    {
-		      error ("Lost %i runs after claim test.", newruns);
-		    }
-#endif
-
-		  //! Indent back
-		  indentDepth--;
-
-		  if (switches.output == PROOF)
-		    {
-		      indentPrint ();
-		      eprintf ("Proof complete for this claim.\n");
-		    }
-		}
-	    }
+	  count++;
 	}
+
       // next
       cl = cl->next;
     }
+  return count;
 }
 
 //! Construct knowledge set at some event, based on a semitrace.