OBJ> obj ABC is
  protecting BOOL .
  sorts element of Bool .
  op a : -> element .
  op b : -> element .
  op c : -> element .
  op _ + _ : element element -> element .
  [e1] eq a + b = b .
  [e2] eq b + c = c .
  [e3] eq c + b = a .
endo

< (a + b) + c , a + (b + c) >   -->   < (a + c) , c >

< (b + c) + b , b + (c + b) >   -->   < (b + a) , a >
< (c + b) + c , c + (b + c) >   -->   < (c + c) , c >

< (a + b) + a , a + (b + a) >   -->   < (a + a) , a >

< (c + b) + a , c + (b + a) >   -->   < (c + a) , a >
< (b + a) + b , b + (a + b) >   -->   < (b + b) , b >

< (c + a) + b , c + (a + b) >   -->   < b , a >

OBJ> obj ABC is
  protecting BOOL .
  sorts element of Bool .
  op a : -> element .
  op b : -> element .
  op c : -> element .
  op _ + _ : element element -> element .
  [e1] eq a + b = b .
  [e2] eq b + c = c .
  [e3] eq c + b = a .
  [e4] eq a + c = c .
  [e5] eq b + a = a .
  [e6] eq c + c = c .
  [e7] eq a + a = a .
  [e8] eq b + b = b .
  [e9] eq c + a = a .
  [e10] eq b = a .
endo

Er zijn geen kritische paren meer die niet oplossen. Dit systeem is dus compleet.