BEST_CASE(Omega(n^2),?)

Solution:
---------

  "#0" :: ["a"(0, 0)] -(0)-> "a"(0, 0)
  "#1" :: ["a"(0, 0)] -(0)-> "a"(0, 0)
  "O" :: ["a"(0, 0)] -(0)-> "a"(0, 0)
  "choice" :: ["a"(0, 0)] -(1)-> "a"(0, 0)
  "dd" :: ["a"(0, 0) x "a"(3, 0)] -(3)-> "a"(3, 0)
  "dd" :: ["a"(0, 0) x "a"(0, 0)] -(0)-> "a"(0, 0)
  "dd" :: ["a"(0, 0) x "a"(2, 1)] -(2)-> "a"(1, 1)
  "dd" :: ["a"(0, 0) x "a"(3, 3)] -(3)-> "a"(0, 3)
  "dd" :: ["a"(0, 0) x "a"(1, 1)] -(1)-> "a"(0, 1)
  "eq" :: ["a"(0, 0) x "a"(0, 0)] -(1)-> "a"(4, 11)
  "false" :: [] -(0)-> "a"(12, 12)
  "false" :: [] -(0)-> "a"(0, 0)
  "false" :: [] -(0)-> "a"(2, 4)
  "false" :: [] -(0)-> "a"(2, 7)
  "guess" :: ["a"(1, 1)] -(1)-> "a"(0, 1)
  "if" :: ["a"(12, 12) x "a"(0, 0) x "a"(0, 0)] -(1)-> "a"(0, 0)
  "member" :: ["a"(0, 0) x "a"(3, 0)] -(1)-> "a"(0, 0)
  "negate" :: ["a"(0, 0)] -(1)-> "a"(0, 0)
  "nil" :: [] -(0)-> "a"(3, 0)
  "nil" :: [] -(0)-> "a"(0, 0)
  "nil" :: [] -(0)-> "a"(1, 1)
  "nil" :: [] -(0)-> "a"(0, 3)
  "sat" :: ["a"(1, 1)] -(3)-> "a"(0, 0)
  "satck" :: ["a"(0, 0) x "a"(0, 1)] -(3)-> "a"(0, 0)
  "true" :: [] -(0)-> "a"(12, 12)
  "true" :: [] -(0)-> "a"(0, 0)
  "true" :: [] -(0)-> "a"(2, 4)
  "unsat" :: [] -(0)-> "a"(0, 0)
  "verify" :: ["a"(0, 3)] -(1)-> "a"(0, 0)


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

  "#0" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "#1" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "O" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "choice" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "dd" :: ["a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "dd" :: ["a"_cf(0, 0) x "a"_cf(1, 0)] -(1)-> "a"_cf(1, 0)
  "eq" :: ["a"_cf(0, 0) x "a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "false" :: [] -(0)-> "a"_cf(0, 0)
  "guess" :: ["a"_cf(1, 0)] -(0)-> "a"_cf(1, 0)
  "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(0, 0)
  "negate" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)
  "nil" :: [] -(0)-> "a"_cf(0, 0)
  "nil" :: [] -(0)-> "a"_cf(1, 0)
  "true" :: [] -(0)-> "a"_cf(0, 0)
  "verify" :: ["a"_cf(0, 0)] -(0)-> "a"_cf(0, 0)


Base Constructors:
------------------
  "\"#0\"_a" :: ["a"(1, 1)] -(1)-> "a"(1, 0)
  "\"#0\"_a" :: ["a"(1, 1)] -(1)-> "a"(0, 1)
  "\"#1\"_a" :: ["a"(1, 0)] -(1)-> "a"(1, 0)
  "\"#1\"_a" :: ["a"(0, 8)] -(1)-> "a"(0, 1)
  "\"O\"_a" :: ["a"(2, 0)] -(1)-> "a"(1, 0)
  "\"O\"_a" :: ["a"(0, 8)] -(1)-> "a"(0, 1)
  "\"dd\"_a" :: ["a"(0, 0) x "a"(1, 0)] -(1)-> "a"(1, 0)
  "\"dd\"_a" :: ["a"(0, 0) 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)