WORST_CASE(?,O(n^2))

Solution:
---------

  "#0" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "#0" :: ["a"(0, 0)] -(0)-> "a"(0, 10)
  "#1" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "#1" :: ["a"(0, 0)] -(0)-> "a"(0, 0)
  "O" :: ["a"(0, 0)] -(0)-> "a"(0, 0)
  "O" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "choice" :: ["a"(0, 8)] -(0)-> "a"(8, 6)
  "dd" :: ["a"(3, 0) x "a"(3, 0)] -(3)-> "a"(3, 0)
  "dd" :: ["a"(8, 8) x "a"(8, 8)] -(8)-> "a"(0, 8)
  "dd" :: ["a"(13, 13) x "a"(13, 13)] -(13)-> "a"(0, 13)
  "dd" :: ["a"(3, 3) x "a"(3, 3)] -(3)-> "a"(0, 3)
  "eq" :: ["a"(0, 0) x "a"(1, 0)] -(1)-> "a"(12, 12)
  "false" :: [] -(0)-> "a"(0, 0)
  "false" :: [] -(0)-> "a"(8, 8)
  "false" :: [] -(0)-> "a"(12, 12)
  "false" :: [] -(0)-> "a"(15, 12)
  "guess" :: ["a"(0, 13)] -(7)-> "a"(0, 3)
  "if" :: ["a"(0, 0) x "a"(0, 0) x "a"(8, 0)] -(1)-> "a"(0, 0)
  "member" :: ["a"(0, 0) x "a"(3, 0)] -(1)-> "a"(0, 0)
  "negate" :: ["a"(1, 0)] -(0)-> "a"(0, 0)
  "nil" :: [] -(0)-> "a"(3, 0)
  "nil" :: [] -(0)-> "a"(0, 0)
  "nil" :: [] -(0)-> "a"(1, 0)
  "nil" :: [] -(0)-> "a"(0, 13)
  "nil" :: [] -(0)-> "a"(0, 3)
  "nil" :: [] -(0)-> "a"(12, 12)
  "sat" :: ["a"(15, 15)] -(16)-> "a"(0, 0)
  "satck" :: ["a"(6, 0) x "a"(0, 3)] -(8)-> "a"(0, 0)
  "true" :: [] -(0)-> "a"(0, 0)
  "true" :: [] -(0)-> "a"(15, 12)
  "true" :: [] -(0)-> "a"(12, 12)
  "true" :: [] -(0)-> "a"(8, 8)
  "unsat" :: [] -(0)-> "a"(8, 8)
  "verify" :: ["a"(0, 3)] -(1)-> "a"(0, 0)


Cost Free Signatures:
---------------------

  "#0" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "#0" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 12)
  "#1" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "#1" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 9)
  "O" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "choice" :: ["a"_cf(8, 0)] -(0)-> "a"_cf(0, 0)
  "choice" :: ["a"_cf(3, 0)] -(2)-> "a"_cf(3, 0)
  "dd" :: ["a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "dd" :: ["a"_cf(8, 0) x "a"_cf(8, 0)] -(8)-> "a"_cf(8, 0)
  "dd" :: ["a"_cf(13, 0) x "a"_cf(13, 0)] -(13)-> "a"_cf(13, 0)
  "dd" :: ["a"_cf(3, 0) x "a"_cf(3, 0)] -(3)-> "a"_cf(3, 0)
  "eq" :: ["a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "false" :: [] -(0)-> "a"_cf(12, 4)
  "false" :: [] -(0)-> "a"_cf(0, 0)
  "false" :: [] -(0)-> "a"_cf(8, 8)
  "guess" :: ["a"_cf(13, 0)] -(0)-> "a"_cf(3, 0)
  "if" :: ["a"_cf(0, 0) x "a"_cf(8, 0) x "a"_cf(8, 0)] -(0)-> "a"_cf(8, 0)
  "if" :: ["a"_cf(0, 0) x "a"_cf(8, 8) x "a"_cf(8, 8)] -(0)-> "a"_cf(8, 8)
  "if" :: ["a"_cf(0, 0) x "a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "member" :: ["a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(8, 0)
  "member" :: ["a"_cf(0, 8) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "negate" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 9)
  "nil" :: [] -(0)-> "a"_cf(0, 0)
  "nil" :: [] -(0)-> "a"_cf(13, 0)
  "nil" :: [] -(0)-> "a"_cf(8, 0)
  "true" :: [] -(0)-> "a"_cf(0, 0)
  "true" :: [] -(0)-> "a"_cf(8, 0)
  "true" :: [] -(0)-> "a"_cf(8, 8)
  "verify" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(8, 8)


Base Constructors:
------------------
  "\"#0\"_a" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "\"#0\"_a" :: ["a"(0, 0)] -(0)-> "a"(0, 1)
  "\"#1\"_a" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "\"#1\"_a" :: ["a"(0, 0)] -(0)-> "a"(0, 1)
  "\"O\"_a" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "\"O\"_a" :: ["a"(0, 0)] -(0)-> "a"(0, 1)
  "\"dd\"_a" :: ["a"(1, 0) x "a"(1, 0)] -(1)-> "a"(1, 0)
  "\"dd\"_a" :: ["a"(1, 1) x "a"(1, 1)] -(1)-> "a"(0, 1)
  "\"false\"_a" :: [] -(0)-> "a"(1, 0)
  "\"false\"_a" :: [] -(0)-> "a"(0, 1)
  "\"nil\"_a" :: [] -(0)-> "a"(1, 0)
  "\"nil\"_a" :: [] -(0)-> "a"(0, 1)
  "\"true\"_a" :: [] -(0)-> "a"(1, 0)
  "\"true\"_a" :: [] -(0)-> "a"(0, 1)
  "\"unsat\"_a" :: [] -(0)-> "a"(1, 0)
  "\"unsat\"_a" :: [] -(0)-> "a"(0, 1)