MAYBE

Problem:
 a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))

Proof:
 DP Processor:
  DPs:
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(f(),a(f(),a(f(),x))))
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(f(),a(f(),a(f(),x)))))
   a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
  TRS:
   a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
  EDG Processor:
   DPs:
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(f(),a(f(),a(f(),x))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(f(),a(f(),a(f(),x)))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
   TRS:
    a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
   graph:
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(f(),a(f(),a(f(),x))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(f(),a(f(),a(f(),x)))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x))) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(f(),a(f(),a(f(),x))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(f(),a(f(),a(f(),x)))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x)) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(f(),a(f(),a(f(),x))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(f(),a(f(),a(f(),x)))))
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x) ->
    a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
   SCC Processor:
    #sccs: 1
    #rules: 3
    #arcs: 18/36
    DPs:
     a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),a(f(),x)))
     a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),a(f(),x))
     a#(f(),a(f(),a(g(),a(g(),x)))) -> a#(f(),x)
    TRS:
     a(f(),a(f(),a(g(),a(g(),x)))) -> a(g(),a(g(),a(g(),a(f(),a(f(),a(f(),x))))))
    Open