WORST_CASE(?,O(n^2))

Solution:
---------

  0 :: [] -(0)-> a(0, 0)
  0 :: [] -(0)-> a(1, 0)
  cons :: [a(5, 0) x b(13, 8)] -(5)-> b(5, 8)
  cons :: [a(8, 0) x b(8, 0)] -(8)-> b(8, 0)
  cons :: [a(1, 0) x b(1, 0)] -(1)-> b(1, 0)
  cons :: [a(2, 0) x b(2, 0)] -(2)-> b(2, 0)
  false :: [] -(0)-> c(9, 9)
  false :: [] -(0)-> c(15, 15)
  if'insert :: [c(9, 9) x a(2, 0) x a(5, 0) x b(8, 0)] -(7)-> b(1, 0)
  insert :: [a(2, 0) x b(8, 0)] -(3)-> b(1, 0)
  leq :: [a(0, 0) x a(1, 0)] -(2)-> c(12, 12)
  nil :: [] -(0)-> b(5, 8)
  nil :: [] -(0)-> b(8, 0)
  nil :: [] -(0)-> b(7, 7)
  nil :: [] -(0)-> b(7, 13)
  s :: [a(0, 0)] -(0)-> a(0, 0)
  s :: [a(1, 0)] -(1)-> a(1, 0)
  sort :: [b(5, 8)] -(8)-> b(1, 0)
  true :: [] -(0)-> c(9, 9)
  true :: [] -(0)-> c(15, 15)


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

  0 :: [] -(0)-> a_cf(0, 0)
  cons :: [a_cf(8, 0) x b_cf(8, 0)] -(8)-> b_cf(8, 0)
  cons :: [a_cf(7, 0) x b_cf(7, 0)] -(7)-> b_cf(7, 0)
  cons :: [a_cf(7, 0) x b_cf(15, 8)] -(7)-> b_cf(7, 8)
  cons :: [a_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  cons :: [a_cf(0, 0) x b_cf(1, 1)] -(0)-> b_cf(0, 1)
  false :: [] -(0)-> c_cf(0, 0)
  false :: [] -(0)-> c_cf(9, 11)
  false :: [] -(0)-> c_cf(1, 1)
  false :: [] -(0)-> c_cf(3, 3)
  if'insert :: [c_cf(0, 0) x a_cf(7, 0) x a_cf(7, 0) x b_cf(7, 0)] -(14)-> b_cf(7, 0)
  if'insert :: [c_cf(1, 1) x a_cf(0, 0) x a_cf(0, 0) x b_cf(0, 0)] -(1)-> b_cf(0, 0)
  if'insert :: [c_cf(0, 0) x a_cf(0, 0) x a_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  insert :: [a_cf(7, 0) x b_cf(7, 0)] -(7)-> b_cf(7, 0)
  insert :: [a_cf(0, 0) x b_cf(0, 0)] -(1)-> b_cf(0, 0)
  insert :: [a_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  leq :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> c_cf(8, 8)
  leq :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> c_cf(3, 3)
  leq :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> c_cf(0, 0)
  nil :: [] -(0)-> b_cf(8, 0)
  nil :: [] -(0)-> b_cf(11, 3)
  nil :: [] -(0)-> b_cf(7, 0)
  nil :: [] -(0)-> b_cf(15, 11)
  nil :: [] -(0)-> b_cf(0, 0)
  s :: [a_cf(0, 0)] -(0)-> a_cf(0, 0)
  sort :: [b_cf(8, 0)] -(0)-> b_cf(7, 0)
  true :: [] -(0)-> c_cf(0, 0)
  true :: [] -(0)-> c_cf(11, 11)
  true :: [] -(0)-> c_cf(1, 1)
  true :: [] -(0)-> c_cf(3, 3)


Base Constructors:
------------------
  0_a :: [] -(0)-> a(1, 0)
  0_a :: [] -(0)-> a(0, 1)
  cons_b :: [a(1, 0) x b(1, 0)] -(1)-> b(1, 0)
  cons_b :: [a(0, 0) x b(1, 1)] -(0)-> b(0, 1)
  false_c :: [] -(0)-> c(1, 0)
  false_c :: [] -(0)-> c(0, 1)
  nil_b :: [] -(0)-> b(1, 0)
  nil_b :: [] -(0)-> b(0, 1)
  s_a :: [a(1, 0)] -(1)-> a(1, 0)
  s_a :: [a(0, 0)] -(0)-> a(0, 1)
  true_c :: [] -(0)-> c(1, 0)
  true_c :: [] -(0)-> c(0, 1)