MAYBE
(ignored inputs)COMMENT [117] Example 4.3.12 submitted by: Aart Middeldorp
Rewrite Rules:
   [ max(L(?x)) -> ?x,
     max(N(L(0),L(?y))) -> ?y,
     max(N(L(s(?x)),L(s(?y)))) -> s(max(N(L(?x),L(?y)))),
     max(N(L(?x),N(?y,?z))) -> max(N(L(?x),L(max(N(?y,?z))))),
     N(?x,N(?y,?z)) -> N(N(?x,?y),?z),
     N(N(?x,?y),?z) -> N(?x,N(?y,?z)),
     N(?x,?y) -> N(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ max(N(L(?y_1),L(0))) = ?y_1,
     max(N(L(s(?y_2)),L(s(?x_2)))) = s(max(N(L(?x_2),L(?y_2)))),
     max(N(N(L(?x_3),?y_4),?z_4)) = max(N(L(?x_3),L(max(N(?y_4,?z_4))))),
     max(N(L(?x_3),N(N(?x_4,?y_4),?z_4))) = max(N(L(?x_3),L(max(N(?x_4,N(?y_4,?z_4)))))),
     max(N(L(?x_3),N(?x_5,N(?y_5,?z_5)))) = max(N(L(?x_3),L(max(N(N(?x_5,?y_5),?z_5))))),
     max(N(N(?y_3,?z_3),L(?x_3))) = max(N(L(?x_3),L(max(N(?y_3,?z_3))))),
     max(N(L(?x_3),N(?y_6,?x_6))) = max(N(L(?x_3),L(max(N(?x_6,?y_6))))),
     N(?x_4,N(?x_5,N(?y_5,?z_5))) = N(N(?x_4,N(?x_5,?y_5)),?z_5),
     N(?x_4,N(?y_6,?x_6)) = N(N(?x_4,?x_6),?y_6),
     N(N(N(?x_4,?y_4),?z_4),?z_5) = N(?x_4,N(N(?y_4,?z_4),?z_5)),
     N(N(?y_6,?x_6),?z_5) = N(?x_6,N(?y_6,?z_5)),
     N(?x_1,N(N(?x,?y),?z)) = N(N(?x_1,?x),N(?y,?z)),
     N(N(?x,N(?y,?z)),?z_1) = N(N(?x,?y),N(?z,?z_1)) ]
Outer CPs:
   [ N(N(N(?x_5,?y_5),?y_4),?z_4) = N(?x_5,N(?y_5,N(?y_4,?z_4))),
     N(N(?x_4,?y_4),?z_4) = N(N(?y_4,?z_4),?x_4),
     N(?x_5,N(?y_5,?z_5)) = N(?z_5,N(?x_5,?y_5)) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
540.trs: Failure(unknown CR)
(0 msec.)