MAYBE

Problem:
 plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
 plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

Proof:
 DP Processor:
  DPs:
   plus#(s(X),plus(Y,Z)) -> plus#(s(s(Y)),Z)
   plus#(s(X),plus(Y,Z)) -> plus#(X,plus(s(s(Y)),Z))
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X2,X4)
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X3,plus(X2,X4))
   plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X1,plus(X3,plus(X2,X4)))
  TRS:
   plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
   plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
  SCC Processor:
   #sccs: 1
   #rules: 5
   #arcs: 25/25
   DPs:
    plus#(s(X),plus(Y,Z)) -> plus#(s(s(Y)),Z)
    plus#(s(X),plus(Y,Z)) -> plus#(X,plus(s(s(Y)),Z))
    plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X2,X4)
    plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X3,plus(X2,X4))
    plus#(s(X1),plus(X2,plus(X3,X4))) -> plus#(X1,plus(X3,plus(X2,X4)))
   TRS:
    plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
    plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
   Open