MAYBE
Rewrite Rules:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(a,?y)) -> eq(?x,?y),
     rep(0,?x) -> nil,
     rep(s(?x),?y) -> *(?x,rep(?x,?y)),
     hd(*(c(?x),?y)) -> ?x,
     lt(*(?x,c(?y))) -> ?y,
     tl(*(c(?x),?y)) -> ?y,
     lem1(?x) -> eq(*(hd(?x),tl(?x)),?x),
     lem2(*(?x,?y)) -> eq(lt(*(?x,?y)),lt(tl(*(?x,?y)))),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ *(?x,*(?x_1,*(?y_1,?z_1))) = *(*(?x,*(?x_1,?y_1)),?z_1),
     *(*(*(?x,?y),?z),?z_1) = *(?x,*(*(?y,?z),?z_1)),
     eq(a,*(*(?x,?y),?z)) = F,
     eq(a,*(?x_1,*(?y_1,?z_1))) = F,
     eq(*(*(a,?y),?z),*(a,?y_4)) = eq(*(?y,?z),?y_4),
     eq(*(a,?x_4),*(*(a,?y),?z)) = eq(?x_4,*(?y,?z)),
     hd(*(*(c(?x_7),?y),?z)) = ?x_7,
     lt(*(?x_1,*(?y_1,c(?y_8)))) = ?y_8,
     tl(*(*(c(?x_9),?y),?z)) = *(?y,?z),
     lem2(*(*(?x,?y),?z)) = eq(lt(*(?x,*(?y,?z))),lt(tl(*(?x,*(?y,?z))))),
     lem2(*(?x_1,*(?y_1,?z_1))) = eq(lt(*(*(?x_1,?y_1),?z_1)),lt(tl(*(*(?x_1,?y_1),?z_1)))),
     +(+(?y_12,?x_12),?z_13) = +(?x_12,+(?y_12,?z_13)),
     +(?x_14,?z_13) = +(0,+(?x_14,?z_13)),
     +(s(+(?x_15,?y_15)),?z_13) = +(s(?x_15),+(?y_15,?z_13)),
     *(?x_1,*(*(?x,?y),?z)) = *(*(?x_1,?x),*(?y,?z)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ *(*(*(?x_1,?y_1),?y),?z) = *(?x_1,*(?y_1,*(?y,?z))),
     eq(a,a) = T,
     eq(*(?x_3,?y_3),a) = F,
     eq(*(a,?y_4),*(a,?x_4)) = eq(?x_4,?y_4),
     +(?y_12,+(?x_13,?y_13)) = +(?x_13,+(?y_13,?y_12)),
     +(?y_12,0) = ?y_12,
     +(?y_12,s(?x_15)) = s(+(?x_15,?y_12)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development 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:
   [ *(?x_1,*(?y_1,*(*(?y,?y_2),?z_2))) = *(*(*(?x_1,?y_1),?y),*(?y_2,?z_2)),
     *(?x_1,*(?y_1,*(?x_3,*(?y_3,?z)))) = *(*(*(?x_1,?y_1),*(?x_3,?y_3)),?z),
     *(?x_1,*(?y_1,*(?y,?z))) = *(*(*(?x_1,?y_1),?y),?z),
     *(?x,*(*(?y,?y_1),?z_1)) = *(*(?x,?y),*(?y_1,?z_1)),
     *(?x,*(?x_2,*(?y_2,?z))) = *(*(?x,*(?x_2,?y_2)),?z),
     *(*(?x_1,?x),*(*(?y,?y_2),?z_2)) = *(?x_1,*(*(?x,?y),*(?y_2,?z_2))),
     *(*(?x_1,?x),*(?x_3,*(?y_3,?z))) = *(?x_1,*(*(?x,*(?x_3,?y_3)),?z)),
     *(?x,*(*(*(?y,?y_3),?z_3),?z_2)) = *(*(*(?x,?y),*(?y_3,?z_3)),?z_2),
     *(?x,*(*(?x_4,*(?y_4,?z)),?z_2)) = *(*(*(?x,*(?x_4,?y_4)),?z),?z_2),
     F = eq(a,*(*(?x,?y),*(?y_1,?z_1))),
     F = eq(a,*(*(?x,*(?x_2,?y_2)),?z)),
     eq(*(*(?y,?y_6),?z_6),?y_5) = eq(*(*(a,?y),*(?y_6,?z_6)),*(a,?y_5)),
     eq(*(?x_7,*(?y_7,?z)),?y_5) = eq(*(*(a,*(?x_7,?y_7)),?z),*(a,?y_5)),
     eq(?x_5,*(*(?y,?y_6),?z_6)) = eq(*(a,?x_5),*(*(a,?y),*(?y_6,?z_6))),
     eq(?x_5,*(?x_7,*(?y_7,?z))) = eq(*(a,?x_5),*(*(a,*(?x_7,?y_7)),?z)),
     ?x_8 = hd(*(*(c(?x_8),?y),*(?y_9,?z_9))),
     ?x_8 = hd(*(*(c(?x_8),*(?x_10,?y_10)),?z)),
     *(*(?y,?y_11),?z_11) = tl(*(*(c(?x_10),?y),*(?y_11,?z_11))),
     *(?x_12,*(?y_12,?z)) = tl(*(*(c(?x_10),*(?x_12,?y_12)),?z)),
     eq(lt(*(?x,*(*(?y,?y_1),?z_1))),lt(tl(*(?x,*(*(?y,?y_1),?z_1))))) = lem2(*(*(?x,?y),*(?y_1,?z_1))),
     eq(lt(*(?x,*(?x_2,*(?y_2,?z)))),lt(tl(*(?x,*(?x_2,*(?y_2,?z)))))) = lem2(*(*(?x,*(?x_2,?y_2)),?z)),
     *(*(?x_1,?x),*(?y,?z)) = *(?x_1,*(*(?x,?y),?z)),
     *(?x,*(*(?y,?z),?z_2)) = *(*(*(?x,?y),?z),?z_2),
     F = eq(a,*(*(?x,?y),?z)),
     eq(*(?y,?z),?y_5) = eq(*(*(a,?y),?z),*(a,?y_5)),
     eq(?x_5,*(?y,?z)) = eq(*(a,?x_5),*(*(a,?y),?z)),
     ?x_8 = hd(*(*(c(?x_8),?y),?z)),
     *(?y,?z) = tl(*(*(c(?x_10),?y),?z)),
     eq(lt(*(?x,*(?y,?z))),lt(tl(*(?x,*(?y,?z))))) = lem2(*(*(?x,?y),?z)),
     *(*(*(?x_2,*(?y_2,?y)),?y_1),?z_1) = *(*(?x_2,?y_2),*(?y,*(?y_1,?z_1))),
     *(*(*(*(?x,?y_3),?z_3),?y_1),?z_1) = *(?x,*(*(?y_3,?z_3),*(?y_1,?z_1))),
     *(*(*(?x,?y),?y_1),?z_1) = *(?x,*(?y,*(?y_1,?z_1))),
     *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)),
     *(*(*(?x,?y_2),?z_2),?z) = *(?x,*(*(?y_2,?z_2),?z)),
     *(*(?x_2,*(?y_2,?y)),*(?z,?z_1)) = *(*(*(?x_2,?y_2),*(?y,?z)),?z_1),
     *(*(*(?x,?y_3),?z_3),*(?z,?z_1)) = *(*(?x,*(*(?y_3,?z_3),?z)),?z_1),
     *(*(?x_2,*(?x_3,*(?y_3,?y))),?z) = *(?x_2,*(*(?x_3,?y_3),*(?y,?z))),
     *(*(?x_2,*(*(?x,?y_4),?z_4)),?z) = *(?x_2,*(?x,*(*(?y_4,?z_4),?z))),
     F = eq(a,*(?x,*(*(?y_2,?z_2),?z))),
     ?y_9 = lt(*(*(?x_10,?y_10),*(?y,c(?y_9)))),
     ?y_9 = lt(*(?x,*(*(?y_11,?z_11),c(?y_9)))),
     eq(lt(*(*(?x_1,*(?y_1,?y)),?z)),lt(tl(*(*(?x_1,*(?y_1,?y)),?z)))) = lem2(*(*(?x_1,?y_1),*(?y,?z))),
     eq(lt(*(*(*(?x,?y_2),?z_2),?z)),lt(tl(*(*(*(?x,?y_2),?z_2),?z)))) = lem2(*(?x,*(*(?y_2,?z_2),?z))),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(*(?x_2,*(?x,?y)),?z) = *(?x_2,*(?x,*(?y,?z))),
     F = eq(a,*(?x,*(?y,?z))),
     ?y_9 = lt(*(?x,*(?y,c(?y_9)))),
     eq(lt(*(*(?x,?y),?z)),lt(tl(*(*(?x,?y),?z)))) = lem2(*(?x,*(?y,?z))),
     T = eq(a,a),
     F = eq(*(?x_3,?y_3),a),
     eq(?x_4,?y_4) = eq(*(a,?y_4),*(a,?x_4)),
     eq(a,a) = T,
     eq(*(*(?x,?y_2),?z_2),a) = F,
     eq(*(?x_3,*(?y_3,?y)),a) = F,
     eq(*(?x,?y),a) = F,
     eq(a,*(*(?x,?y_2),?z_2)) = F,
     eq(a,*(?x_3,*(?y_3,?y))) = F,
     eq(*(*(a,?y_4),?z_4),*(*(a,?y_2),?z_2)) = eq(*(?y_2,?z_2),*(?y_4,?z_4)),
     eq(*(a,?y),*(*(a,?y_2),?z_2)) = eq(*(?y_2,?z_2),?y),
     eq(*(*(a,?y_2),?z_2),*(a,?x)) = eq(?x,*(?y_2,?z_2)),
     eq(*(*(a,?y_2),?z_2),*(*(a,?y_4),?z_4)) = eq(*(?y_2,?z_2),*(?y_4,?z_4)),
     eq(*(a,?y),*(a,?x)) = eq(?x,?y),
     eq(*(*(a,?y_2),?z_2),*(a,?y)) = eq(*(?y_2,?z_2),?y),
     eq(*(a,?x),*(*(a,?y_2),?z_2)) = eq(?x,*(?y_2,?z_2)),
     hd(*(*(c(?x),?y_2),?z_2)) = ?x,
     lt(*(?x_3,*(?y_3,c(?y)))) = ?y,
     tl(*(*(c(?x),?y_2),?z_2)) = *(?y_2,?z_2),
     lem2(*(*(?x,?y_2),?z_2)) = eq(lt(*(?x,*(?y_2,?z_2))),lt(tl(*(?x,*(?y_2,?z_2))))),
     lem2(*(?x_3,*(?y_3,?y))) = eq(lt(*(*(?x_3,?y_3),?y)),lt(tl(*(*(?x_3,?y_3),?y)))),
     +(?x_13,+(?y_13,?y)) = +(?y,+(?x_13,?y_13)),
     ?y = +(?y,0),
     s(+(?x_15,?y)) = +(?y,s(?x_15)),
     +(?x,+(?y,?z_14)) = +(+(?y,?x),?z_14),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,s(+(?x_16,?y))) = +(s(?x_16),+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(s(+(?x_16,?y)),?z) = +(s(?x_16),+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(s(+(?x_17,?y)),+(?z,?z_1)) = +(+(s(?x_17),+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?x,0) = ?x,
     +(0,+(?x,?z_15)) = +(?x,?z_15),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_15)) = +(s(+(?x,?y)),?z_15) ]
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 <*(?x,*(?x_1,*(?y_1,?z_1))), *(*(?x,*(?x_1,?y_1)),?z_1)> by Rules <1, 0> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],0)], [([],1)]>
Critical Pair <*(*(*(?x,?y),?z),?z_1), *(?x,*(*(?y,?z),?z_1))> by Rules <0, 1> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],1)], [([],0)]>
Critical Pair <eq(a,*(*(?x,?y),?z)), F> by Rules <0, 4> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],4)], []>
Critical Pair <eq(a,*(?x_1,*(?y_1,?z_1))), F> by Rules <1, 4> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],4)], []>
Critical Pair <eq(*(*(a,?y),?z),*(a,?y_4)), eq(*(?y,?z),?y_4)> by Rules <0, 5> preceded by [(eq,1)]
 joinable by a reduction of rules <[([(eq,1)],1),([],5)], []>
Critical Pair <eq(*(a,?x_4),*(*(a,?y),?z)), eq(?x_4,*(?y,?z))> by Rules <0, 5> preceded by [(eq,2)]
 joinable by a reduction of rules <[([(eq,2)],1),([],5)], []>
Critical Pair <hd(*(*(c(?x_7),?y),?z)), ?x_7> by Rules <0, 8> preceded by [(hd,1)]
 joinable by a reduction of rules <[([(hd,1)],1),([],8)], []>
Critical Pair <lt(*(?x_1,*(?y_1,c(?y_8)))), ?y_8> by Rules <1, 9> preceded by [(lt,1)]
 joinable by a reduction of rules <[([(lt,1)],0),([],9)], []>
Critical Pair <tl(*(*(c(?x_9),?y),?z)), *(?y,?z)> by Rules <0, 10> preceded by [(tl,1)]
 joinable by a reduction of rules <[([(tl,1)],1),([],10)], []>
Critical Pair <lem2(*(*(?x,?y),?z)), eq(lt(*(?x,*(?y,?z))),lt(tl(*(?x,*(?y,?z)))))> by Rules <0, 12> preceded by [(lem2,1)]
 joinable by a reduction of rules <[([(lem2,1)],1),([],12)], []>
 joinable by a reduction of rules <[([],12),([(eq,2),(lt,1),(tl,1)],1)], [([(eq,1),(lt,1)],0)]>
 joinable by a reduction of rules <[([],12),([(eq,1),(lt,1)],1)], [([(eq,2),(lt,1),(tl,1)],0)]>
 joinable by a reduction of rules <[([],12)], [([(eq,2),(lt,1),(tl,1)],0),([(eq,1),(lt,1)],0)]>
 joinable by a reduction of rules <[([],12)], [([(eq,1),(lt,1)],0),([(eq,2),(lt,1),(tl,1)],0)]>
Critical Pair <lem2(*(?x_1,*(?y_1,?z_1))), eq(lt(*(*(?x_1,?y_1),?z_1)),lt(tl(*(*(?x_1,?y_1),?z_1))))> by Rules <1, 12> preceded by [(lem2,1)]
 joinable by a reduction of rules <[([(lem2,1)],0),([],12)], []>
 joinable by a reduction of rules <[([],12),([(eq,2),(lt,1),(tl,1)],0)], [([(eq,1),(lt,1)],1)]>
 joinable by a reduction of rules <[([],12),([(eq,1),(lt,1)],0)], [([(eq,2),(lt,1),(tl,1)],1)]>
 joinable by a reduction of rules <[([],12)], [([(eq,2),(lt,1),(tl,1)],1),([(eq,1),(lt,1)],1)]>
 joinable by a reduction of rules <[([],12)], [([(eq,1),(lt,1)],1),([(eq,2),(lt,1),(tl,1)],1)]>
Critical Pair <+(+(?y_12,?x_12),?z_13), +(?x_12,+(?y_12,?z_13))> by Rules <13, 14> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],13),([],14)], []>
 joinable by a reduction of rules <[([],14),([(+,2)],13)], [([],13),([],14)]>
Critical Pair <+(?x_14,?z_13), +(0,+(?x_14,?z_13))> by Rules <15, 14> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],15)]>
Critical Pair <+(s(+(?x_15,?y_15)),?z_13), +(s(?x_15),+(?y_15,?z_13))> by Rules <16, 14> preceded by [(+,1)]
 joinable by a reduction of rules <[([],16),([(s,1)],14)], [([],16)]>
Critical Pair <*(?x_1,*(*(?x,?y),?z)), *(*(?x_1,?x),*(?y,?z))> by Rules <0, 0> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],1)], [([],1)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <1, 1> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],0)], [([],0)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <14, 14> preceded by [(+,1)]
 joinable by a reduction of rules <[([],14),([(+,2)],14)], [([],14)]>
Critical Pair <*(?x_1,*(?y_1,*(?y,?z))), *(*(*(?x_1,?y_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <T, eq(a,a)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <F, eq(*(?x_3,?y_3),a)> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[], [([],2),([],4)]>
Critical Pair <eq(?x_4,?y_4), eq(*(a,?y_4),*(a,?x_4))> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],2)], [([],5)]>
Critical Pair <+(?x_13,+(?y_13,?z_13)), +(?z_13,+(?x_13,?y_13))> by Rules <14, 13> preceded by []
 joinable by a reduction of rules <[], [([],13),([],14)]>
Critical Pair <?x_14, +(?x_14,0)> by Rules <15, 13> preceded by []
 joinable by a reduction of rules <[], [([],13),([],15)]>
Critical Pair <s(+(?x_15,?y_15)), +(?y_15,s(?x_15))> by Rules <16, 13> preceded by []
 joinable by a reduction of rules <[], [([],13),([],16)]>
unknown Diagram Decreasing
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x_1,?y_1),?z_1) -> *(?x_1,*(?y_1,?z_1)),
     eq(?x_2,?y_2) -> eq(?y_2,?x_2),
     eq(a,a) -> T,
     eq(a,*(?x_3,?y_3)) -> F,
     eq(*(a,?x_4),*(a,?y_4)) -> eq(?x_4,?y_4),
     rep(0,?x_5) -> nil,
     rep(s(?x_6),?y_6) -> *(?x_6,rep(?x_6,?y_6)),
     hd(*(c(?x_7),?y_7)) -> ?x_7,
     lt(*(?x_8,c(?y_8))) -> ?y_8,
     tl(*(c(?x_9),?y_9)) -> ?y_9,
     lem1(?x_10) -> eq(*(hd(?x_10),tl(?x_10)),?x_10),
     lem2(*(?x_11,?y_11)) -> eq(lt(*(?x_11,?y_11)),lt(tl(*(?x_11,?y_11)))),
     +(?x_12,?y_12) -> +(?y_12,?x_12),
     +(+(?x_13,?y_13),?z_13) -> +(?x_13,+(?y_13,?z_13)),
     +(0,?x_14) -> ?x_14,
     +(s(?x_15),?y_15) -> s(+(?x_15,?y_15)) ]
Sort Assignment:
 * : 64*64=>64
 + : 64*64=>64
 0 : =>64
 F : =>68
 T : =>68
 a : =>64
 c : 64=>64
 s : 64=>64
 eq : 64*64=>68
 hd : 64=>64
 lt : 64=>64
 tl : 64=>64
 nil : =>64
 rep : 64*58=>64
 lem1 : 64=>68
 lem2 : 64=>68
non-linear variables: {?x_6,?x_10,?x_11,?y_11}
non-linear types: {64}
types leq non-linear types: {64}
rules applicable to terms of non-linear types:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x_1,?y_1),?z_1) -> *(?x_1,*(?y_1,?z_1)),
     rep(0,?x_5) -> nil,
     rep(s(?x_6),?y_6) -> *(?x_6,rep(?x_6,?y_6)),
     hd(*(c(?x_7),?y_7)) -> ?x_7,
     lt(*(?x_8,c(?y_8))) -> ?y_8,
     tl(*(c(?x_9),?y_9)) -> ?y_9,
     +(?x_12,?y_12) -> +(?y_12,?x_12),
     +(+(?x_13,?y_13),?z_13) -> +(?x_13,+(?y_13,?z_13)),
     +(0,?x_14) -> ?x_14,
     +(s(?x_15),?y_15) -> s(+(?x_15,?y_15)) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {0,1,6,7,8,9,10,13,14,15,16}
8: {}
9: {}
10: {}
11: {0,1,6,7,8,9,10,13,14,15,16}
12: {0,1,6,7,8,9,10,13,14,15,16}
13: {}
14: {}
15: {}
16: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x_1,?y_1),?z_1) -> *(?x_1,*(?y_1,?z_1)),
     eq(?x_2,?y_2) -> eq(?y_2,?x_2),
     eq(a,a) -> T,
     eq(a,*(?x_3,?y_3)) -> F,
     eq(*(a,?x_4),*(a,?y_4)) -> eq(?x_4,?y_4),
     rep(0,?x_5) -> nil,
     rep(s(?x_6),?y_6) -> *(?x_6,rep(?x_6,?y_6)),
     hd(*(c(?x_7),?y_7)) -> ?x_7,
     lt(*(?x_8,c(?y_8))) -> ?y_8,
     tl(*(c(?x_9),?y_9)) -> ?y_9,
     lem1(?x_10) -> eq(*(hd(?x_10),tl(?x_10)),?x_10),
     lem2(*(?x_11,?y_11)) -> eq(lt(*(?x_11,?y_11)),lt(tl(*(?x_11,?y_11)))),
     +(?x_12,?y_12) -> +(?y_12,?x_12),
     +(+(?x_13,?y_13),?z_13) -> +(?x_13,+(?y_13,?z_13)),
     +(0,?x_14) -> ?x_14,
     +(s(?x_15),?y_15) -> s(+(?x_15,?y_15)) ]
Sort Assignment:
 * : 64*64=>64
 + : 64*64=>64
 0 : =>64
 F : =>68
 T : =>68
 a : =>64
 c : 64=>64
 s : 64=>64
 eq : 64*64=>68
 hd : 64=>64
 lt : 64=>64
 tl : 64=>64
 nil : =>64
 rep : 64*58=>64
 lem1 : 64=>68
 lem2 : 64=>68
non-linear variables: {?x_6,?x_10,?x_11,?y_11}
non-linear types: {64}
types leq non-linear types: {64}
rules applicable to terms of non-linear types:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x_1,?y_1),?z_1) -> *(?x_1,*(?y_1,?z_1)),
     rep(0,?x_5) -> nil,
     rep(s(?x_6),?y_6) -> *(?x_6,rep(?x_6,?y_6)),
     hd(*(c(?x_7),?y_7)) -> ?x_7,
     lt(*(?x_8,c(?y_8))) -> ?y_8,
     tl(*(c(?x_9),?y_9)) -> ?y_9,
     +(?x_12,?y_12) -> +(?y_12,?x_12),
     +(+(?x_13,?y_13),?z_13) -> +(?x_13,+(?y_13,?z_13)),
     +(0,?x_14) -> ?x_14,
     +(s(?x_15),?y_15) -> s(+(?x_15,?y_15)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 27 rules by 3 steps unfolding
strenghten +(?x_14,0) and ?x_14
strenghten +(0,?x_16) and ?x_16
strenghten eq(a,a) and T
strenghten +(?x_23,?y_23) and +(?y_23,?x_23)
strenghten s(+(?x_15,0)) and s(?x_15)
strenghten eq(*(?x_3,?y_3),a) and F
strenghten +(?y_15,s(?x_15)) and s(+(?x_15,?y_15))
strenghten s(+(?x_15,?x_24)) and +(?x_24,s(?x_15))
strenghten s(+(?x_15,?y_22)) and +(s(?x_15),?y_22)
strenghten +(?x_13,+(?y_13,0)) and +(?x_13,?y_13)
strenghten +(?x_16,+(0,?z_13)) and +(?x_16,?z_13)
strenghten +(0,+(?x_14,?z_13)) and +(?x_14,?z_13)
strenghten eq(a,*(?x_1,*(?y_1,?z_1))) and F
strenghten eq(a,*(*(?x,?y),?z)) and F
strenghten hd(*(*(c(?x_7),?y),?z)) and ?x_7
strenghten lt(*(?x_1,*(?y_1,c(?y_8)))) and ?y_8
strenghten +(?x_12,+(?y_12,?z_13)) and +(+(?y_12,?x_12),?z_13)
strenghten +(?x_13,+(?y_13,?x_24)) and +(?x_24,+(?x_13,?y_13))
strenghten +(?x_13,+(?y_13,?y_22)) and +(+(?x_13,?y_13),?y_22)
strenghten +(?z_13,+(?x_13,?y_13)) and +(?x_13,+(?y_13,?z_13))
strenghten eq(*(a,?y_4),*(a,?x_4)) and eq(?x_4,?y_4)
strenghten tl(*(*(c(?x_9),?y),?z)) and *(?y,?z)
strenghten rep(0,eq(*(hd(?x_10),tl(?x_10)),?x_10)) and nil
strenghten +(s(?x_15),+(?y_15,?z_13)) and +(s(+(?x_15,?y_15)),?z_13)
strenghten *(?x,*(*(?y,?z),?z_1)) and *(*(*(?x,?y),?z),?z_1)
strenghten *(*(?x,?y),*(?z,?z_1)) and *(*(?x,*(?y,?z)),?z_1)
strenghten *(*(?x,*(?x_1,?y_1)),?z_1) and *(?x,*(?x_1,*(?y_1,?z_1)))
strenghten *(*(?x_1,?x),*(?y,?z)) and *(?x_1,*(*(?x,?y),?z))
strenghten *(*(*(?x_1,?y_1),?y),?z) and *(?x_1,*(?y_1,*(?y,?z)))
strenghten +(+(?x,?y),+(?z,?z_1)) and +(+(?x,+(?y,?z)),?z_1)
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximationsample4.trs: Failure(timeout)
(120116 msec.)