NO
Rewrite Rules:
   [ sum(leaf(?x)) -> ?x,
     sum(node(?x,?yt,?zt)) -> +(+(?x,sum(?yt)),sum(?zt)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,?y) -> +(?y,?x),
     node(?x,?yt,?zt) -> node(?x,?zt,?yt) ]
Apply Direct Methods...
Inner CPs:
   [ sum(node(?x_5,?zt_5,?yt_5)) = +(+(?x_5,sum(?yt_5)),sum(?zt_5)) ]
Outer CPs:
   [ ?y_2 = +(?y_2,0),
     s(+(?x_3,?y_3)) = +(?y_3,s(?x_3)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ sum(node(?x,?zt,?yt)) = +(+(?x,sum(?yt)),sum(?zt)),
     +(?y,0) = ?y,
     +(?y,s(?x)) = s(+(?x,?y)),
     ?y = +(?y,0),
     s(+(?x_4,?y)) = +(?y,s(?x_4)),
     +(+(?x,sum(?yt)),sum(?zt)) = sum(node(?x,?zt,?yt)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <sum(node(?x_5,?zt_5,?yt_5)), +(+(?x_5,sum(?yt_5)),sum(?zt_5))> by Rules <5, 1> preceded by [(sum,1)]
 joinable by a reduction of rules <[([(sum,1)],5),([],1)], []>
Critical Pair <+(?y_4,0), ?y_4> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([],4),([],2)], []>
Critical Pair <+(?y_4,s(?x_3)), s(+(?x_3,?y_4))> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([],4),([],3)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 9 rules by 3 steps unfolding
obtain 51 candidates for checking non-joinability
check by TCAP-Approximation   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (failure)
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
   [ sum(leaf(?x:Nat)) -> ?x:Nat,
     sum(node(?x:Nat,?yt:Tree,?zt:Tree)) -> +(+(?x:Nat,sum(?yt:Tree)),sum(?zt:Tree)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,?y:Nat) -> +(?y:Nat,?x:Nat),
     node(?x:Nat,?yt:Tree,?zt:Tree) -> node(?x:Nat,?zt:Tree,?yt:Tree) ]
 (success)
<F,Q,Q_f,Delta> where
   F = {(+,2),(0,0),(s,1),(c_1,0),(c_2,0),(c_3,0),(sum,1),(leaf,1),(node,3)}
   Q = {q_0,q_1,q_{+(*,*)},q_{c_1},q_{c_2},q_{c_3},q_{*},q_{+(c_1,sum(c_2))},q_{+(c_1,sum(c_3))},q_{+(*,sum(*))},q_{sum(*)},q_{sum(c_2)},q_{sum(c_3)}}
   Qf = {q_0,q_1}
   Delta = 
   [ +(q_{c_1},q_{sum(c_2)}) -> q_{+(c_1,sum(c_2))},
     +(q_{c_1},q_{sum(c_3)}) -> q_{+(c_1,sum(c_3))},
     +(q_{*},q_{*}) -> q_{+(*,*)},
     +(q_{*},q_{*}) -> q_{*},
     +(q_{*},q_{*}) -> q_{+(*,sum(*))},
     +(q_{*},q_{*}) -> q_{sum(*)},
     +(q_{*},q_{sum(*)}) -> q_{+(*,*)},
     +(q_{*},q_{sum(*)}) -> q_{+(*,sum(*))},
     +(q_{*},q_{sum(*)}) -> q_{sum(*)},
     +(q_{+(c_1,sum(c_2))},q_{sum(c_3)}) -> q_0,
     +(q_{+(c_1,sum(c_3))},q_{sum(c_2)}) -> q_1,
     +(q_{+(*,sum(*))},q_{sum(*)}) -> q_{+(*,*)},
     +(q_{+(*,sum(*))},q_{sum(*)}) -> q_{+(*,sum(*))},
     +(q_{+(*,sum(*))},q_{sum(*)}) -> q_{sum(*)},
     +(q_{sum(*)},q_{*}) -> q_{+(*,*)},
     +(q_{sum(*)},q_{*}) -> q_{+(*,sum(*))},
     +(q_{sum(*)},q_{*}) -> q_{sum(*)},
     +(q_{sum(*)},q_{+(*,sum(*))}) -> q_{+(*,*)},
     +(q_{sum(*)},q_{+(*,sum(*))}) -> q_{+(*,sum(*))},
     +(q_{sum(*)},q_{+(*,sum(*))}) -> q_{sum(*)},
     +(q_{sum(c_2)},q_{c_1}) -> q_{+(c_1,sum(c_2))},
     +(q_{sum(c_2)},q_{+(c_1,sum(c_3))}) -> q_1,
     +(q_{sum(c_3)},q_{c_1}) -> q_{+(c_1,sum(c_3))},
     +(q_{sum(c_3)},q_{+(c_1,sum(c_2))}) -> q_0,
     0 -> q_{+(*,*)},
     0 -> q_{*},
     0 -> q_{+(*,sum(*))},
     0 -> q_{sum(*)},
     s(q_{+(*,*)}) -> q_{+(*,*)},
     s(q_{+(*,*)}) -> q_{+(*,sum(*))},
     s(q_{+(*,*)}) -> q_{sum(*)},
     s(q_{*}) -> q_{+(*,*)},
     s(q_{*}) -> q_{*},
     s(q_{*}) -> q_{+(*,sum(*))},
     s(q_{*}) -> q_{sum(*)},
     c_1 -> q_{+(*,*)},
     c_1 -> q_{c_1},
     c_1 -> q_{*},
     c_1 -> q_{+(*,sum(*))},
     c_1 -> q_{sum(*)},
     c_2 -> q_{+(*,*)},
     c_2 -> q_{c_2},
     c_2 -> q_{*},
     c_2 -> q_{+(*,sum(*))},
     c_2 -> q_{sum(*)},
     c_3 -> q_{+(*,*)},
     c_3 -> q_{c_3},
     c_3 -> q_{*},
     c_3 -> q_{+(*,sum(*))},
     c_3 -> q_{sum(*)},
     sum(q_{c_2}) -> q_{sum(c_2)},
     sum(q_{c_3}) -> q_{sum(c_3)},
     sum(q_{*}) -> q_{+(*,*)},
     sum(q_{*}) -> q_{*},
     sum(q_{*}) -> q_{+(*,sum(*))},
     sum(q_{*}) -> q_{sum(*)},
     leaf(q_{*}) -> q_{+(*,*)},
     leaf(q_{*}) -> q_{*},
     leaf(q_{*}) -> q_{+(*,sum(*))},
     leaf(q_{*}) -> q_{sum(*)},
     node(q_{*},q_{*},q_{*}) -> q_{+(*,*)},
     node(q_{*},q_{*},q_{*}) -> q_{*},
     node(q_{*},q_{*},q_{*}) -> q_{+(*,sum(*))},
     node(q_{*},q_{*},q_{*}) -> q_{sum(*)} ]
Witness for Non-Confluence: <+(+(c_1,sum(c_2)),sum(c_3)), +(+(c_1,sum(c_3)),sum(c_2))>
Direct Methods: not CR

Final result: not CR
new/tree6.trs: Success(not CR)
(4184 msec.)