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
   [1>3, 3>4, 3>5, 4>6, 5>6]
 sort attachment (strict)
   g : 2 x 2 x 2 -> 2
   f : 3 x 3 x 3 x 3 x 3 -> 1
   a : 4
   b : 5
   0 : 6
 -----
 0:f(x,y,x,y,z) -> f(a(),b(),z,z,z)
   a() -> 0()
   b() -> 0()
   Open
 
 
 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
    DP Processor:
     DPs:
      
     TRS:
      g(x,x,y) -> y
      g(x,y,y) -> x
     Qed