Problem:
 g(x,x,y) -> y
 g(x,y,y) -> x
 f(x,y,x,y,z) -> f(a(),b(),z,z,z)
 a() -> 0()
 b() -> 0()

Proof:
 sorted: (order)
 0:f(x,y,x,y,z) -> f(a(),b(),z,z,z)
   a() -> 0()
   b() -> 0()
 1:g(x,x,y) -> y
   g(x,y,y) -> x
 -----
 sorts
   [0>2, 2>3, 2>4, 3>5, 4>5]
 sort attachment (strict)
   g : 1 x 1 x 1 -> 1
   f : 2 x 2 x 2 x 2 x 2 -> 0
   a : 3
   b : 4
   0 : 5
 -----
 0:f(x,y,x,y,z) -> f(a(),b(),z,z,z)
   a() -> 0()
   b() -> 0()
   Qed (SakaiOyamaguchiOgawa14)
 
 
 1:g(x,x,y) -> y
   g(x,y,y) -> x
   Church Rosser Transformation Processor (kb):
    g(x,x,y) -> y
    g(x,y,y) -> x
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [g](x0, x1, x2) = x0 + 6x1 + 4x2 + 4
     orientation:
      g(x,x,y) = 7x + 4y + 4 >= y = y
      
      g(x,y,y) = x + 10y + 4 >= x = x
     problem:
      
     Qed