Problem:
 if(true(),a(),x) -> a()
 if(true(),b(),x) -> b()
 if(true(),g(a()),x) -> g(a())
 if(true(),g(b()),x) -> g(b())
 if(false(),x,a()) -> a()
 if(false(),x,b()) -> b()
 if(false(),x,g(a())) -> g(a())
 if(false(),x,g(b())) -> g(b())
 g(a()) -> g(g(a()))
 g(b()) -> a()
 f(a(),b()) -> b()
 f(g(g(a())),x) -> b()

Proof:
 sorted: (order-sorted)
 0:if(true(),a(),x) -> a()
   if(true(),b(),x) -> b()
   if(true(),g(a()),x) -> g(a())
   if(true(),g(b()),x) -> g(b())
   if(false(),x,a()) -> a()
   if(false(),x,b()) -> b()
   if(false(),x,g(a())) -> g(a())
   if(false(),x,g(b())) -> g(b())
   g(a()) -> g(g(a()))
   g(b()) -> a()
 1:g(a()) -> g(g(a()))
   g(b()) -> a()
   f(a(),b()) -> b()
   f(g(g(a())),x) -> b()
 -----
 sorts
   [0>2, 0>7, 0>8, 1>5, 1>6, 2>3, 2>4, 5>9, 6>10, 7>9, 8>9, 9>10, 9>11]
 sort attachment (non-strict)
   if : 2 x 7 x 8 -> 0
   true : 4
   a : 11
   b : 10
   g : 9 -> 9
   false : 3
   f : 5 x 6 -> 1
 -----
 0:if(true(),a(),x) -> a()
   if(true(),b(),x) -> b()
   if(true(),g(a()),x) -> g(a())
   if(true(),g(b()),x) -> g(b())
   if(false(),x,a()) -> a()
   if(false(),x,b()) -> b()
   if(false(),x,g(a())) -> g(a())
   if(false(),x,g(b())) -> g(b())
   g(a()) -> g(g(a()))
   g(b()) -> a()
   Nonconfluence Processor:
    terms: if(true(),g(g(a())),f7()) *<- if(true(),g(a()),f7()) ->* g(a())
    Qed
    
    first automaton:
     final states: {19}
     transitions:
      true() -> 24*
      a() -> 21*
      g(21) -> 22*
      g(22) -> 22,23
      if(24,23,20) -> 19*
      f7() -> 20*
    
    second automaton:
     final states: {17}
     transitions:
      a() -> 18*
      g(18) -> 17*
      g(17) -> 17*
 
 
 1:g(a()) -> g(g(a()))
   g(b()) -> a()
   f(a(),b()) -> b()
   f(g(g(a())),x) -> b()
   Open