WORST_CASE(?,O(n^2))

Solution:
---------

  #0 :: [] -(0)-> b(0, 0)
  #0 :: [] -(0)-> b(3, 0)
  #and :: [a(0, 0) x a(0, 0)] -(1)-> a(0, 0)
  #eq :: [b(0, 0) x b(3, 0)] -(1)-> a(0, 0)
  #equal :: [b(0, 0) x b(3, 0)] -(2)-> a(0, 0)
  #false :: [] -(0)-> a(0, 0)
  #neg :: [b(3, 0)] -(3)-> b(3, 0)
  #neg :: [b(0, 0)] -(0)-> b(0, 0)
  #pos :: [b(3, 0)] -(3)-> b(3, 0)
  #pos :: [b(0, 0)] -(0)-> b(0, 0)
  #s :: [b(3, 0)] -(3)-> b(3, 0)
  #s :: [b(0, 0)] -(0)-> b(0, 0)
  #true :: [] -(0)-> a(0, 0)
  and :: [a(0, 0) x a(0, 0)] -(2)-> a(0, 0)
  dd :: [b(0, 0) x b(0, 0)] -(0)-> b(0, 0)
  dd :: [b(7, 0) x b(7, 0)] -(7)-> b(7, 0)
  dd :: [b(4, 12) x b(16, 12)] -(4)-> b(4, 12)
  dd :: [b(11, 12) x b(23, 12)] -(11)-> b(11, 12)
  dd :: [b(3, 0) x b(3, 0)] -(3)-> b(3, 0)
  eq :: [b(0, 0) x b(7, 0)] -(3)-> a(0, 0)
  eq#1 :: [b(0, 0) x b(7, 0)] -(2)-> a(0, 0)
  eq#2 :: [b(0, 0)] -(1)-> a(0, 0)
  eq#3 :: [b(7, 0) x b(0, 0) x b(0, 0)] -(1)-> a(0, 0)
  nil :: [] -(0)-> b(0, 0)
  nil :: [] -(0)-> b(7, 0)
  nil :: [] -(0)-> b(4, 12)
  nil :: [] -(0)-> b(11, 12)
  nil :: [] -(0)-> b(3, 0)
  nub :: [b(4, 12)] -(2)-> b(0, 0)
  nub#1 :: [b(4, 12)] -(1)-> b(0, 0)
  remove :: [b(0, 0) x b(11, 12)] -(2)-> b(4, 12)
  remove#1 :: [b(11, 12) x b(0, 0)] -(1)-> b(4, 12)
  remove#2 :: [a(0, 0) x b(0, 0) x b(4, 12) x b(23, 12)] -(7)-> b(4, 12)


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

  #0 :: [] -(0)-> b_cf(0, 0)
  #and :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  #eq :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> a_cf(0, 0)
  #equal :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> a_cf(0, 0)
  #false :: [] -(0)-> a_cf(0, 0)
  #neg :: [b_cf(0, 0)] -(0)-> b_cf(0, 0)
  #pos :: [b_cf(0, 0)] -(0)-> b_cf(0, 0)
  #s :: [b_cf(0, 0)] -(0)-> b_cf(0, 0)
  #true :: [] -(0)-> a_cf(0, 0)
  and :: [a_cf(0, 0) x a_cf(0, 0)] -(0)-> a_cf(0, 0)
  dd :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  dd :: [b_cf(12, 0) x b_cf(12, 0)] -(12)-> b_cf(12, 0)
  eq :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> a_cf(0, 0)
  eq#1 :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> a_cf(0, 0)
  eq#2 :: [b_cf(0, 0)] -(0)-> a_cf(0, 0)
  eq#3 :: [b_cf(0, 0) x b_cf(0, 0) x b_cf(0, 0)] -(0)-> a_cf(0, 0)
  nil :: [] -(0)-> b_cf(0, 0)
  nil :: [] -(0)-> b_cf(12, 0)
  nub :: [b_cf(0, 0)] -(0)-> b_cf(0, 0)
  nub#1 :: [b_cf(0, 0)] -(0)-> b_cf(0, 0)
  remove :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  remove :: [b_cf(0, 0) x b_cf(12, 0)] -(0)-> b_cf(12, 0)
  remove :: [b_cf(0, 0) x b_cf(12, 0)] -(0)-> b_cf(0, 0)
  remove#1 :: [b_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  remove#1 :: [b_cf(12, 0) x b_cf(0, 0)] -(0)-> b_cf(12, 0)
  remove#1 :: [b_cf(12, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  remove#2 :: [a_cf(0, 0) x b_cf(0, 0) x b_cf(0, 0) x b_cf(0, 0)] -(0)-> b_cf(0, 0)
  remove#2 :: [a_cf(0, 0) x b_cf(0, 0) x b_cf(12, 0) x b_cf(12, 0)] -(12)-> b_cf(12, 0)
  remove#2 :: [a_cf(0, 0) x b_cf(0, 0) x b_cf(0, 0) x b_cf(12, 0)] -(0)-> b_cf(0, 0)


Base Constructors:
------------------
  #0_b :: [] -(0)-> b(0)
  #false_a :: [] -(0)-> a(0)
  #neg_b :: [b(0)] -(0)-> b(0)
  #pos_b :: [b(0)] -(0)-> b(0)
  #s_b :: [b(0)] -(0)-> b(0)
  #true_a :: [] -(0)-> a(0)
  dd_b :: [b(1, 0) x b(1, 0)] -(1)-> b(1, 0)
  dd_b :: [b(0, 1) x b(1, 1)] -(0)-> b(0, 1)
  nil_b :: [] -(0)-> b(1, 0)
  nil_b :: [] -(0)-> b(0, 1)