WORST_CASE(?,O(n^2))

Solution:
---------

  #0 :: [a(12, 3)] -(3)-> a(9, 3)
  #0 :: [a(9, 3)] -(3)-> a(6, 3)
  #1 :: [a(8, 0)] -(8)-> a(8, 0)
  #1 :: [a(0, 0)] -(0)-> a(0, 0)
  #1 :: [a(12, 3)] -(9)-> a(9, 3)
  #1 :: [a(4, 2)] -(2)-> a(2, 2)
  O :: [a(0, 0)] -(0)-> a(0, 0)
  O :: [a(8, 0)] -(8)-> a(8, 0)
  choice :: [a(0, 15)] -(1)-> a(15, 15)
  dd :: [a(11, 0) x a(11, 0)] -(11)-> a(11, 0)
  dd :: [a(15, 15) x a(15, 15)] -(15)-> a(0, 15)
  dd :: [a(12, 12) x a(12, 12)] -(12)-> a(0, 12)
  eq :: [a(0, 0) x a(8, 0)] -(2)-> a(12, 12)
  false :: [] -(0)-> a(0, 0)
  false :: [] -(0)-> a(7, 7)
  false :: [] -(0)-> a(15, 15)
  guess :: [a(0, 15)] -(3)-> a(0, 12)
  if :: [a(0, 0) x a(0, 0) x a(3, 9)] -(1)-> a(0, 0)
  member :: [a(0, 0) x a(11, 0)] -(3)-> a(0, 0)
  negate :: [a(9, 3)] -(0)-> a(2, 2)
  nil :: [] -(0)-> a(11, 0)
  nil :: [] -(0)-> a(0, 0)
  nil :: [] -(0)-> a(8, 0)
  nil :: [] -(0)-> a(0, 15)
  nil :: [] -(0)-> a(0, 12)
  nil :: [] -(0)-> a(7, 15)
  sat :: [a(15, 15)] -(15)-> a(0, 0)
  satck :: [a(0, 0) x a(0, 12)] -(11)-> a(0, 0)
  true :: [] -(0)-> a(0, 0)
  true :: [] -(0)-> a(7, 7)
  true :: [] -(0)-> a(15, 15)
  unsat :: [] -(0)-> a(14, 15)
  verify :: [a(0, 12)] -(5)-> 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(15, 0)] -(14)-> a_cf(0, 0)
  choice :: [a_cf(12, 0)] -(0)-> a_cf(12, 0)
  dd :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  dd :: [a_cf(15, 0) x a_cf(15, 0)] -(15)-> a_cf(15, 0)
  dd :: [a_cf(12, 0) x a_cf(12, 0)] -(12)-> a_cf(12, 0)
  eq :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(13, 13)
  eq :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  eq :: [a_cf(0, 0) x a_cf(0, 0)] -(1)-> a_cf(0, 0)
  false :: [] -(0)-> a_cf(13, 15)
  false :: [] -(0)-> a_cf(1, 1)
  false :: [] -(0)-> a_cf(15, 15)
  false :: [] -(0)-> a_cf(0, 0)
  false :: [] -(0)-> a_cf(11, 15)
  guess :: [a_cf(15, 0)] -(0)-> a_cf(12, 0)
  if :: [a_cf(1, 1) x a_cf(12, 14) x a_cf(12, 13)] -(0)-> a_cf(12, 13)
  if :: [a_cf(1, 1) x a_cf(4, 14) x a_cf(4, 13)] -(0)-> a_cf(4, 13)
  if :: [a_cf(1, 1) x a_cf(6, 14) x a_cf(6, 14)] -(0)-> a_cf(6, 14)
  member :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(12, 13)
  member :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(6, 14)
  negate :: [a_cf(0, 0)] -(0)-> a_cf(0, 0)
  nil :: [] -(0)-> a_cf(0, 0)
  nil :: [] -(0)-> a_cf(15, 0)
  nil :: [] -(0)-> a_cf(15, 2)
  true :: [] -(0)-> a_cf(1, 1)
  true :: [] -(0)-> a_cf(15, 15)
  true :: [] -(0)-> a_cf(13, 15)
  true :: [] -(0)-> a_cf(0, 0)
  true :: [] -(0)-> a_cf(7, 15)
  verify :: [a_cf(0, 0)] -(0)-> a_cf(4, 13)


Base Constructors:
------------------
  #0_a :: [a(0)] -(0)-> a(0)
  #1_a :: [a(0)] -(0)-> a(0)
  O_a :: [a(1, 0)] -(1)-> a(1, 0)
  O_a :: [a(1, 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)