MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ node(?x,?y) -> node(?y,?x),
     max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     height(leaf) -> 0,
     height(node(?x,?y)) -> s(max(height(?x),height(?y))) ]
Constructors: {0,s,leaf,node}
Defined function symbols: {max,height}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     height(leaf) -> 0,
     height(node(?x,?y)) -> s(max(height(?x),height(?y))) ]
   [ node(?x,?y) -> node(?y,?x) ]
Trying with:
R:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     height(leaf) -> 0,
     height(node(?x,?y)) -> s(max(height(?x),height(?y))) ]
E:
   [ node(?x,?y) = node(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Tree}
Signature:
   [ max : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat,
     node : Tree,Tree -> Tree,
     leaf : Tree,
     height : Tree -> Nat ]
Rule Part:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     height(leaf) -> 0,
     height(node(?x,?y)) -> s(max(height(?x),height(?y))) ]
Conjecture Part:
   [ node(?x,?y) = node(?y,?x) ]
Precedence (by weight): {(0,3),(s,4),(max,6),(leaf,5),(node,7),(height,2)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ max(?x,0) -> ?x,
     max(0,?y) -> ?y,
     max(s(?x),s(?y)) -> s(max(?x,?y)),
     height(leaf) -> 0,
     height(node(?x,?y)) -> s(max(height(?x),height(?y))) ]
Conjectures:
   [ node(?x,?y) = node(?y,?x) ]
STEP 0
ES:
   [ node(?x,?y) = node(?y,?x) ]
HS:
   [ ]
ES0:
   [ node(?x,?y) = node(?y,?x) ]
HS0:
   [ ]
ES1:
   [ node(?x,?y) = node(?y,?x) ]
HS1:
   [ ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
new/tree3.trs: Failure(unknown)
(15 msec.)