MAYBE
Rewrite Rules:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(?x,?y) -> *(?y,?x),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Apply Direct Methods...
Inner CPs:
   [ +(+(?y,?x),?z_1) = +(?x,+(?y,?z_1)),
     +(?x_2,?z_1) = +(0,+(?x_2,?z_1)),
     +(s(+(?x_3,?y_3)),?z_1) = +(s(?x_3),+(?y_3,?z_1)),
     .(.(.(?x_9,?y_9),?z_9),?z_8) = .(?x_9,.(.(?y_9,?z_9),?z_8)),
     .(.(.(b,a),b),?z_8) = .(a,.(.(b,a),?z_8)),
     .(?x_9,.(?x_8,.(?y_8,?z_8))) = .(.(?x_9,.(?x_8,?y_8)),?z_8),
     .(?x_9,.(.(b,a),b)) = .(.(?x_9,a),.(b,a)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     .(.(?x,.(?y,?z)),?z_1) = .(.(?x,?y),.(?z,?z_1)),
     .(?x_1,.(.(?x,?y),?z)) = .(.(?x_1,?x),.(?y,?z)) ]
Outer CPs:
   [ +(?y,+(?x_1,?y_1)) = +(?x_1,+(?y_1,?y)),
     +(?y,0) = ?y,
     +(?y,s(?x_3)) = s(+(?x_3,?y)),
     *(?y_5,0) = 0,
     *(?y_5,s(?x_7)) = +(?y_5,*(?x_7,?y_5)),
     .(?x_8,.(?y_8,.(?y_9,?z_9))) = .(.(.(?x_8,?y_8),?y_9),?z_9),
     .(.(a,b),a) = .(.(b,a),b) ]
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,+(?x_1,?y_1)),
     ?y = +(?y,0),
     s(+(?x_3,?y)) = +(?y,s(?x_3)),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(?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_4,?y))) = +(s(?x_4),+(?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_4,?y)),?z) = +(s(?x_4),+(?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_5,?y)),+(?z,?z_1)) = +(+(s(?x_5),+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?x,0) = ?x,
     +(0,+(?x,?z_3)) = +(?x,?z_3),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_3)) = +(s(+(?x,?y)),?z_3),
     0 = *(?y,0),
     +(?y,*(?x_7,?y)) = *(?y,s(?x_7)),
     *(?y,0) = 0,
     *(?y,s(?x)) = +(?y,*(?x,?y)),
     .(.(.(?x_10,.(?y_10,?y)),?y_9),?z_9) = .(.(?x_10,?y_10),.(?y,.(?y_9,?z_9))),
     .(.(.(.(?x,?y_19),?z_19),?y_9),?z_9) = .(?x,.(.(?y_19,?z_19),.(?y_9,?z_9))),
     .(.(.(.(b,a),b),?y_9),?z_9) = .(a,.(.(b,a),.(?y_9,?z_9))),
     .(.(.(?x,?y),?y_9),?z_9) = .(?x,.(?y,.(?y_9,?z_9))),
     .(.(?x_1,.(?y_1,?y)),?z) = .(.(?x_1,?y_1),.(?y,?z)),
     .(.(.(?x,?y_10),?z_10),?z) = .(?x,.(.(?y_10,?z_10),?z)),
     .(.(.(b,a),b),?z) = .(a,.(.(b,a),?z)),
     .(.(?x_2,.(?y_2,?y)),.(?z,?z_1)) = .(.(.(?x_2,?y_2),.(?y,?z)),?z_1),
     .(.(.(?x,?y_11),?z_11),.(?z,?z_1)) = .(.(?x,.(.(?y_11,?z_11),?z)),?z_1),
     .(.(.(b,a),b),.(?z,?z_1)) = .(.(a,.(.(b,a),?z)),?z_1),
     .(.(?x_10,.(?x_11,.(?y_11,?y))),?z) = .(?x_10,.(.(?x_11,?y_11),.(?y,?z))),
     .(.(?x_10,.(.(?x,?y_20),?z_20)),?z) = .(?x_10,.(?x,.(.(?y_20,?z_20),?z))),
     .(.(?x_10,.(.(b,a),b)),?z) = .(?x_10,.(a,.(.(b,a),?z))),
     .(.(?x,?y),.(?z,?z_1)) = .(.(?x,.(?y,?z)),?z_1),
     .(.(?x_10,.(?x,?y)),?z) = .(?x_10,.(?x,.(?y,?z))),
     .(?x_9,.(?y_9,.(.(?y,?y_10),?z_10))) = .(.(.(?x_9,?y_9),?y),.(?y_10,?z_10)),
     .(?x_9,.(?y_9,.(?x_19,.(?y_19,?z)))) = .(.(.(?x_9,?y_9),.(?x_19,?y_19)),?z),
     .(?x_9,.(?y_9,.(.(b,a),b))) = .(.(.(?x_9,?y_9),a),.(b,a)),
     .(?x_9,.(?y_9,.(?y,?z))) = .(.(.(?x_9,?y_9),?y),?z),
     .(.(b,a),b) = .(.(a,b),a),
     .(?x,.(.(?y,?y_1),?z_1)) = .(.(?x,?y),.(?y_1,?z_1)),
     .(?x,.(?x_10,.(?y_10,?z))) = .(.(?x,.(?x_10,?y_10)),?z),
     .(?x,.(.(b,a),b)) = .(.(?x,a),.(b,a)),
     .(.(?x_1,?x),.(.(?y,?y_2),?z_2)) = .(?x_1,.(.(?x,?y),.(?y_2,?z_2))),
     .(.(?x_1,?x),.(?x_11,.(?y_11,?z))) = .(?x_1,.(.(?x,.(?x_11,?y_11)),?z)),
     .(.(?x_1,?x),.(.(b,a),b)) = .(?x_1,.(.(?x,a),.(b,a))),
     .(?x,.(.(.(?y,?y_11),?z_11),?z_10)) = .(.(.(?x,?y),.(?y_11,?z_11)),?z_10),
     .(?x,.(.(?x_20,.(?y_20,?z)),?z_10)) = .(.(.(?x,.(?x_20,?y_20)),?z),?z_10),
     .(?x,.(.(.(b,a),b),?z_10)) = .(.(.(?x,a),.(b,a)),?z_10),
     .(.(?x_1,?x),.(?y,?z)) = .(?x_1,.(.(?x,?y),?z)),
     .(?x,.(.(?y,?z),?z_10)) = .(.(.(?x,?y),?z),?z_10),
     .(.(a,b),a) = .(.(b,a),b),
     .(a,.(.(b,a),?z_8)) = .(.(.(b,a),b),?z_8),
     .(.(?x_9,a),.(b,a)) = .(?x_9,.(.(b,a),b)) ]
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 <+(+(?y,?x),?z_1), +(?x,+(?y,?z_1))> by Rules <0, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],0),([],1)], []>
 joinable by a reduction of rules <[([],1),([(+,2)],0)], [([],0),([],1)]>
Critical Pair <+(?x_2,?z_1), +(0,+(?x_2,?z_1))> by Rules <2, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <+(s(+(?x_3,?y_3)),?z_1), +(s(?x_3),+(?y_3,?z_1))> by Rules <3, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([],3),([(s,1)],1)], [([],3)]>
Critical Pair <.(.(.(?x_9,?y_9),?z_9),?z_8), .(?x_9,.(.(?y_9,?z_9),?z_8))> by Rules <9, 8> preceded by [(.,1)]
 joinable by a reduction of rules <[([(.,1)],8)], [([],9)]>
Critical Pair <.(.(.(b,a),b),?z_8), .(a,.(.(b,a),?z_8))> by Rules <10, 8> preceded by [(.,1)]
 joinable by a reduction of rules <[], [([],9),([(.,1)],10)]>
Critical Pair <.(?x_9,.(?x_8,.(?y_8,?z_8))), .(.(?x_9,.(?x_8,?y_8)),?z_8)> by Rules <8, 9> preceded by [(.,2)]
 joinable by a reduction of rules <[([(.,2)],9)], [([],8)]>
Critical Pair <.(?x_9,.(.(b,a),b)), .(.(?x_9,a),.(b,a))> by Rules <10, 9> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([],8),([(.,2)],10)]>
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),([(+,2)],1)], [([],1)]>
Critical Pair <.(.(?x,.(?y,?z)),?z_1), .(.(?x,?y),.(?z,?z_1))> by Rules <8, 8> preceded by [(.,1)]
 joinable by a reduction of rules <[([(.,1)],9)], [([],9)]>
Critical Pair <.(?x_1,.(.(?x,?y),?z)), .(.(?x_1,?x),.(?y,?z))> by Rules <9, 9> preceded by [(.,2)]
 joinable by a reduction of rules <[([(.,2)],8)], [([],8)]>
Critical Pair <+(?x_1,+(?y_1,?z_1)), +(?z_1,+(?x_1,?y_1))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],1)]>
Critical Pair <?x_2, +(?x_2,0)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],2)]>
Critical Pair <s(+(?x_3,?y_3)), +(?y_3,s(?x_3))> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],3)]>
Critical Pair <0, *(?y_6,0)> by Rules <6, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],6)]>
Critical Pair <+(?y_7,*(?x_7,?y_7)), *(?y_7,s(?x_7))> by Rules <7, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],7)]>
Critical Pair <.(.(.(?x_8,?y_8),?y_9),?z_9), .(?x_8,.(?y_8,.(?y_9,?z_9)))> by Rules <9, 8> preceded by []
 joinable by a reduction of rules <[([],8)], [([],9)]>
Critical Pair <.(.(b,a),b), .(.(a,b),a)> by Rules <10, 9> preceded by []
 joinable by a reduction of rules <[], [([],8),([],10)]>
unknown Diagram Decreasing
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)),
     .(.(?x_8,?y_8),?z_8) -> .(?x_8,.(?y_8,?z_8)),
     .(?x_9,.(?y_9,?z_9)) -> .(.(?x_9,?y_9),?z_9),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Sort Assignment:
 * : 43*43=>43
 + : 43*43=>43
 . : 40*40=>40
 0 : =>43
 : : 43*43=>43
 a : =>40
 b : =>40
 s : 43=>43
 fib : 43=>43
non-linear variables: {?x_4,?y_7}
non-linear types: {43}
types leq non-linear types: {43}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {0,1,2,3,4,5,6,7}
5: {}
6: {}
7: {0,1,2,3,4,5,6,7}
8: {}
9: {}
10: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)),
     .(.(?x_8,?y_8),?z_8) -> .(?x_8,.(?y_8,?z_8)),
     .(?x_9,.(?y_9,?z_9)) -> .(.(?x_9,?y_9),?z_9),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Sort Assignment:
 * : 43*43=>43
 + : 43*43=>43
 . : 40*40=>40
 0 : =>43
 : : 43*43=>43
 a : =>40
 b : =>40
 s : 43=>43
 fib : 43=>43
non-linear variables: {?x_4,?y_7}
non-linear types: {43}
types leq non-linear types: {43}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 21 rules by 3 steps unfolding
strenghten *(?x_12,0) and 0
strenghten *(0,?x_10) and 0
strenghten +(?x_2,0) and ?x_2
strenghten +(0,?x_14) and ?x_14
strenghten *(fib(?x_18),0) and 0
strenghten s(+(?x_3,0)) and s(?x_3)
strenghten +(0,*(?x_7,0)) and 0
strenghten +(?y_3,s(?x_3)) and s(+(?x_3,?y_3))
strenghten +(?x_1,+(?y_1,0)) and +(?x_1,?y_1)
strenghten +(?x_14,+(0,?z_1)) and +(?x_14,?z_1)
strenghten +(0,+(?x_2,?z_1)) and +(?x_2,?z_1)
strenghten +(?y_7,*(?x_7,?y_7)) and *(?y_7,s(?x_7))
strenghten +(?x,+(?y,?z_1)) and +(+(?y,?x),?z_1)
strenghten +(?z_1,+(?x_1,?y_1)) and +(?x_1,+(?y_1,?z_1))
strenghten .(.(a,b),a) and .(.(b,a),b)
strenghten *(0,:(?x_4,+(fib(?x_4),fib(s(?x_4))))) and 0
strenghten +(s(?x_3),+(?y_3,?z_1)) and +(s(+(?x_3,?y_3)),?z_1)
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 Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)),
     .(a,.(b,a)) -> .(.(b,a),b),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z) ]
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
not relatively terminatiing
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)) ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?x,?y) -> *(?y,?x),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 1)
STEP: 2 (linear)
S:
   [ +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)) ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?x,?y) -> *(?y,?x),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 2)
STEP: 3 (relative)
S:
   [ +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)) ]
P:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?x,?y) -> *(?y,?x),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(?x,?y) -> *(?y,?x),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)),
     .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Sort Assignment:
 * : 43*43=>43
 + : 43*43=>43
 . : 40*40=>40
 0 : =>43
 : : 43*43=>43
 a : =>40
 b : =>40
 s : 43=>43
 fib : 43=>43
maximal types: {40}{43}
{40}
(ps)Rewrite Rules:
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Apply Direct Methods...
Inner CPs:
   [ .(.(.(?x_1,?y_1),?z_1),?z) = .(?x_1,.(.(?y_1,?z_1),?z)),
     .(.(.(b,a),b),?z) = .(a,.(.(b,a),?z)),
     .(?x_1,.(?x,.(?y,?z))) = .(.(?x_1,.(?x,?y)),?z),
     .(?x_1,.(.(b,a),b)) = .(.(?x_1,a),.(b,a)),
     .(.(?x,.(?y,?z)),?z_1) = .(.(?x,?y),.(?z,?z_1)),
     .(?x_1,.(.(?x,?y),?z)) = .(.(?x_1,?x),.(?y,?z)) ]
Outer CPs:
   [ .(?x,.(?y,.(?y_1,?z_1))) = .(.(.(?x,?y),?y_1),?z_1),
     .(.(a,b),a) = .(.(b,a),b) ]
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:
   [ .(.(.(?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))),
     .(.(.(.(b,a),b),?y_1),?z_1) = .(a,.(.(b,a),.(?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)),
     .(.(.(b,a),b),?z) = .(a,.(.(b,a),?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),
     .(.(.(b,a),b),.(?z,?z_1)) = .(.(a,.(.(b,a),?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))),
     .(.(?x_2,.(.(b,a),b)),?z) = .(?x_2,.(a,.(.(b,a),?z))),
     .(.(?x,?y),.(?z,?z_1)) = .(.(?x,.(?y,?z)),?z_1),
     .(.(?x_2,.(?x,?y)),?z) = .(?x_2,.(?x,.(?y,?z))),
     .(?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,.(.(b,a),b))) = .(.(.(?x_1,?y_1),a),.(b,a)),
     .(?x_1,.(?y_1,.(?y,?z))) = .(.(.(?x_1,?y_1),?y),?z),
     .(.(b,a),b) = .(.(a,b),a),
     .(?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,.(.(b,a),b)) = .(.(?x,a),.(b,a)),
     .(.(?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_1,?x),.(.(b,a),b)) = .(?x_1,.(.(?x,a),.(b,a))),
     .(?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),
     .(?x,.(.(.(b,a),b),?z_2)) = .(.(.(?x,a),.(b,a)),?z_2),
     .(.(?x_1,?x),.(?y,?z)) = .(?x_1,.(.(?x,?y),?z)),
     .(?x,.(.(?y,?z),?z_2)) = .(.(.(?x,?y),?z),?z_2),
     .(.(a,b),a) = .(.(b,a),b),
     .(a,.(.(b,a),?z)) = .(.(.(b,a),b),?z),
     .(.(?x_1,a),.(b,a)) = .(?x_1,.(.(b,a),b)) ]
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_1,?y_1),?z_1),?z), .(?x_1,.(.(?y_1,?z_1),?z))> by Rules <1, 0> preceded by [(.,1)]
 joinable by a reduction of rules <[([(.,1)],0)], [([],1)]>
Critical Pair <.(.(.(b,a),b),?z), .(a,.(.(b,a),?z))> by Rules <2, 0> preceded by [(.,1)]
 joinable by a reduction of rules <[], [([],1),([(.,1)],2)]>
Critical Pair <.(?x_1,.(?x,.(?y,?z))), .(.(?x_1,.(?x,?y)),?z)> by Rules <0, 1> preceded by [(.,2)]
 joinable by a reduction of rules <[([(.,2)],1)], [([],0)]>
Critical Pair <.(?x_1,.(.(b,a),b)), .(.(?x_1,a),.(b,a))> by Rules <2, 1> preceded by [(.,2)]
 joinable by a reduction of rules <[], [([],0),([(.,2)],2)]>
Critical Pair <.(.(?x,.(?y,?z)),?z_1), .(.(?x,?y),.(?z,?z_1))> by Rules <0, 0> preceded by [(.,1)]
 joinable by a reduction of rules <[([(.,1)],1)], [([],1)]>
Critical Pair <.(?x_1,.(.(?x,?y),?z)), .(.(?x_1,?x),.(?y,?z))> by Rules <1, 1> preceded by [(.,2)]
 joinable by a reduction of rules <[([(.,2)],0)], [([],0)]>
Critical Pair <.(.(.(?x,?y),?y_1),?z_1), .(?x,.(?y,.(?y_1,?z_1)))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <.(.(b,a),b), .(.(a,b),a)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[], [([],0),([],2)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 13 rules by 3 steps unfolding
strenghten .(?x_3,.(?y_3,?z_3)) and .(.(?x_3,?y_3),?z_3)
strenghten .(.(?x_2,?y_2),?z_2) and .(?x_2,.(?y_2,?z_2))
strenghten .(.(a,b),a) and .(.(b,a),b)
strenghten .(.(a,b),a) and .(b,.(a,b))
strenghten .(.(b,a),b) and .(.(a,b),a)
strenghten .(.(b,a),b) and .(a,.(b,a))
strenghten .(.(b,a),b) and .(b,.(a,b))
strenghten .(a,.(b,a)) and .(.(b,a),b)
strenghten .(a,.(b,a)) and .(b,.(a,b))
strenghten .(?x,.(?y,.(?y_1,?z_1))) and .(.(.(?x,?y),?y_1),?z_1)
strenghten .(?x,.(?y,.(?y_2,?z_2))) and .(.(?x,?y),.(?y_2,?z_2))
strenghten .(?x_1,.(.(?y_1,?z_1),?z)) and .(.(.(?x_1,?y_1),?z_1),?z)
strenghten .(?x_2,.(?x_1,.(?y_1,?z_1))) and .(?x_2,.(.(?x_1,?y_1),?z_1))
strenghten .(?x_2,.(.(?x,?y),?z)) and .(?x_2,.(?x,.(?y,?z)))
strenghten .(?x_2,.(.(?y_2,?z_2),?z)) and .(.(?x_2,.(?y_2,?z_2)),?z)
strenghten .(?x_2,.(.(a,b),a)) and .(?x_2,.(.(b,a),b))
strenghten .(?x_2,.(.(a,b),a)) and .(?x_2,.(b,.(a,b)))
strenghten .(?x_2,.(a,.(b,a))) and .(?x_2,.(.(b,a),b))
strenghten .(?x_2,.(a,.(b,a))) and .(?x_2,.(b,.(a,b)))
strenghten .(?x_9,.(?x_11,.(?y_11,?z_9))) and .(.(?x_9,.(?x_11,?y_11)),?z_9)
strenghten .(.(?x,?y),.(?z,?z_1)) and .(.(?x,.(?y,?z)),?z_1)
strenghten .(.(?x_1,?x),.(?y,?z)) and .(?x_1,.(.(?x,?y),?z))
strenghten .(.(?x_1,?x_2),.(?y_2,?z_2)) and .(?x_1,.(?x_2,.(?y_2,?z_2)))
strenghten .(.(?x_1,.(?x,?y)),?z) and .(?x_1,.(?x,.(?y,?z)))
strenghten .(.(?x_1,.(?x_5,?y_5)),?z_5) and .(?x_1,.(.(?x_5,?y_5),?z_5))
strenghten .(.(?x_1,.(?y_1,?z_1)),?z_5) and .(.(.(?x_1,?y_1),?z_1),?z_5)
strenghten .(.(?x_1,.(a,b)),a) and .(?x_1,.(.(b,a),b))
strenghten .(.(?x_1,.(a,b)),a) and .(?x_1,.(b,.(a,b)))
strenghten .(.(?x_1,a),.(b,a)) and .(?x_1,.(.(b,a),b))
strenghten .(.(?x_1,a),.(b,a)) and .(?x_1,.(b,.(a,b)))
strenghten .(.(?x_5,?y_5),.(?z_5,?z)) and .(.(.(?x_5,?y_5),?z_5),?z)
strenghten .(.(.(?x,?y),?z),?z_5) and .(.(?x,.(?y,?z)),?z_5)
strenghten .(.(.(?x_4,?y_4),?y_1),?z_1) and .(?x_4,.(?y_4,.(?y_1,?z_1)))
strenghten .(.(.(?x_5,?y_5),?y_1),?z_1) and .(.(?x_5,?y_5),.(?y_1,?z_1))
strenghten .(.(.(a,b),a),?z_5) and .(.(.(b,a),b),?z_5)
strenghten .(.(.(a,b),a),?z_5) and .(.(b,.(a,b)),?z_5)
strenghten .(.(a,.(b,a)),?z_5) and .(.(.(b,a),b),?z_5)
strenghten .(.(a,.(b,a)),?z_5) and .(.(b,.(a,b)),?z_5)
strenghten .(.(a,b),.(a,?z)) and .(.(.(b,a),b),?z)
strenghten .(.(a,b),.(a,?z)) and .(.(b,.(a,b)),?z)
strenghten .(a,.(.(b,a),?z)) and .(.(.(b,a),b),?z)
strenghten .(a,.(.(b,a),?z)) and .(.(b,.(a,b)),?z)
strenghten .(?x,.(?y,.(?x_8,.(?y_8,?z_6)))) and .(.(?x,?y),.(.(?x_8,?y_8),?z_6))
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 Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ ]
P:
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 1)
STEP: 2 (linear)
S:
   [ ]
P:
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 2)
STEP: 3 (relative)
S:
   [ ]
P:
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
P: not reversible
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Layer Preserving Decomposition for...
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ .(.(?x,?y),?z) -> .(?x,.(?y,?z)),
     .(?x,.(?y,?z)) -> .(.(?x,?y),?z),
     .(a,.(b,a)) -> .(.(b,a),b) ]
Outside Critical Pair: <.(.(.(?x,?y),?y_1),?z_1), .(?x,.(?y,.(?y_1,?z_1)))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, .(.(?x,?y),.(?y_1,?z_1))>
<{0}, .(.(?x,.(?y,?y_1)),?z_1)>
<{}, .(.(.(?x,?y),?y_1),?z_1)>
develop reducts from rhs term...
<{1}, .(.(?x,?y),.(?y_1,?z_1))>
<{1}, .(?x,.(.(?y,?y_1),?z_1))>
<{}, .(?x,.(?y,.(?y_1,?z_1)))>
Outside Critical Pair: <.(.(b,a),b), .(.(a,b),a)> by Rules <2, 1>
develop reducts from lhs term...
<{0}, .(b,.(a,b))>
<{}, .(.(b,a),b)>
develop reducts from rhs term...
<{0}, .(a,.(b,a))>
<{}, .(.(a,b),a)>
Inside Critical Pair: <.(.(.(?x_1,?y_1),?z_1),?z), .(?x_1,.(.(?y_1,?z_1),?z))> by Rules <1, 0>
develop reducts from lhs term...
<{0}, .(.(?x_1,?y_1),.(?z_1,?z))>
<{0}, .(.(?x_1,.(?y_1,?z_1)),?z)>
<{}, .(.(.(?x_1,?y_1),?z_1),?z)>
develop reducts from rhs term...
<{1}, .(.(?x_1,.(?y_1,?z_1)),?z)>
<{0}, .(?x_1,.(?y_1,.(?z_1,?z)))>
<{}, .(?x_1,.(.(?y_1,?z_1),?z))>
Inside Critical Pair: <.(.(.(b,a),b),?z), .(a,.(.(b,a),?z))> by Rules <2, 0>
develop reducts from lhs term...
<{0}, .(.(b,a),.(b,?z))>
<{0}, .(.(b,.(a,b)),?z)>
<{}, .(.(.(b,a),b),?z)>
develop reducts from rhs term...
<{1}, .(.(a,.(b,a)),?z)>
<{0}, .(a,.(b,.(a,?z)))>
<{}, .(a,.(.(b,a),?z))>
Inside Critical Pair: <.(?x_1,.(?x,.(?y,?z))), .(.(?x_1,.(?x,?y)),?z)> by Rules <0, 1>
develop reducts from lhs term...
<{1}, .(.(?x_1,?x),.(?y,?z))>
<{1}, .(?x_1,.(.(?x,?y),?z))>
<{}, .(?x_1,.(?x,.(?y,?z)))>
develop reducts from rhs term...
<{0}, .(?x_1,.(.(?x,?y),?z))>
<{1}, .(.(.(?x_1,?x),?y),?z)>
<{}, .(.(?x_1,.(?x,?y)),?z)>
Inside Critical Pair: <.(?x_1,.(.(b,a),b)), .(.(?x_1,a),.(b,a))> by Rules <2, 1>
develop reducts from lhs term...
<{1}, .(.(?x_1,.(b,a)),b)>
<{0}, .(?x_1,.(b,.(a,b)))>
<{}, .(?x_1,.(.(b,a),b))>
develop reducts from rhs term...
<{1}, .(.(.(?x_1,a),b),a)>
<{0}, .(?x_1,.(a,.(b,a)))>
<{}, .(.(?x_1,a),.(b,a))>
Commutative Decomposition failed: Can't judge
No further decomposition possible

{43}
(ps)Rewrite Rules:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     fib(?x) -> :(?x,+(fib(?x),fib(s(?x)))),
     *(?x,?y) -> *(?y,?x),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ +(+(?y,?x),?z_1) = +(?x,+(?y,?z_1)),
     +(?x_2,?z_1) = +(0,+(?x_2,?z_1)),
     +(s(+(?x_3,?y_3)),?z_1) = +(s(?x_3),+(?y_3,?z_1)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?y,+(?x_1,?y_1)) = +(?x_1,+(?y_1,?y)),
     +(?y,0) = ?y,
     +(?y,s(?x_3)) = s(+(?x_3,?y)),
     *(?y_5,0) = 0,
     *(?y_5,s(?x_7)) = +(?y_5,*(?x_7,?y_5)) ]
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,+(?x_1,?y_1)),
     ?y = +(?y,0),
     s(+(?x_3,?y)) = +(?y,s(?x_3)),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(?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_4,?y))) = +(s(?x_4),+(?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_4,?y)),?z) = +(s(?x_4),+(?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_5,?y)),+(?z,?z_1)) = +(+(s(?x_5),+(?y,?z)),?z_1),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(?x,0) = ?x,
     +(0,+(?x,?z_3)) = +(?x,?z_3),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(s(?x),+(?y,?z_3)) = +(s(+(?x,?y)),?z_3),
     0 = *(?y,0),
     +(?y,*(?x_7,?y)) = *(?y,s(?x_7)),
     *(?y,0) = 0,
     *(?y,s(?x)) = +(?y,*(?x,?y)) ]
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 <+(+(?y,?x),?z_1), +(?x,+(?y,?z_1))> by Rules <0, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],0),([],1)], []>
 joinable by a reduction of rules <[([],1),([(+,2)],0)], [([],0),([],1)]>
Critical Pair <+(?x_2,?z_1), +(0,+(?x_2,?z_1))> by Rules <2, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],2)]>
Critical Pair <+(s(+(?x_3,?y_3)),?z_1), +(s(?x_3),+(?y_3,?z_1))> by Rules <3, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([],3),([(s,1)],1)], [([],3)]>
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),([(+,2)],1)], [([],1)]>
Critical Pair <+(?x_1,+(?y_1,?z_1)), +(?z_1,+(?x_1,?y_1))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],1)]>
Critical Pair <?x_2, +(?x_2,0)> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],2)]>
Critical Pair <s(+(?x_3,?y_3)), +(?y_3,s(?x_3))> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], [([],0),([],3)]>
Critical Pair <0, *(?y_6,0)> by Rules <6, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],6)]>
Critical Pair <+(?y_7,*(?x_7,?y_7)), *(?y_7,s(?x_7))> by Rules <7, 5> preceded by []
 joinable by a reduction of rules <[], [([],5),([],7)]>
unknown Diagram Decreasing
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
Sort Assignment:
 * : 29*29=>29
 + : 29*29=>29
 0 : =>29
 : : 29*29=>29
 s : 29=>29
 fib : 29=>29
non-linear variables: {?x_4,?y_7}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {0,1,2,3,4,5,6,7}
5: {}
6: {}
7: {0,1,2,3,4,5,6,7}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
Sort Assignment:
 * : 29*29=>29
 + : 29*29=>29
 0 : =>29
 : : 29*29=>29
 s : 29=>29
 fib : 29=>29
non-linear variables: {?x_4,?y_7}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,?y) -> +(?y,?x),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(0,?x_2) -> ?x_2,
     +(s(?x_3),?y_3) -> s(+(?x_3,?y_3)),
     fib(?x_4) -> :(?x_4,+(fib(?x_4),fib(s(?x_4)))),
     *(?x_5,?y_5) -> *(?y_5,?x_5),
     *(0,?y_6) -> 0,
     *(s(?x_7),?y_7) -> +(?y_7,*(?x_7,?y_7)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 18 rules by 3 steps unfolding
strenghten *(?x_10,0) and 0
strenghten *(0,?x_8) and 0
strenghten +(?x_2,0) and ?x_2
strenghten +(0,?x_12) and ?x_12
strenghten *(fib(?x_16),0) and 0
strenghten s(+(?x_3,0)) and s(?x_3)
strenghten +(0,*(?x_7,0)) and 0
strenghten +(?y_3,s(?x_3)) and s(+(?x_3,?y_3))
strenghten +(?x_1,+(?y_1,0)) and +(?x_1,?y_1)
strenghten +(?x_12,+(0,?z_1)) and +(?x_12,?z_1)
strenghten +(0,+(?x_2,?z_1)) and +(?x_2,?z_1)
strenghten +(?y_7,*(?x_7,?y_7)) and *(?y_7,s(?x_7))
strenghten +(?x,+(?y,?z_1)) and +(+(?y,?x),?z_1)
strenghten +(?z_1,+(?x_1,?y_1)) and +(?x_1,+(?y_1,?z_1))
strenghten *(0,:(?x_4,+(fib(?x_4),fib(s(?x_4))))) and 0
strenghten +(s(?x_3),+(?y_3,?z_1)) and +(s(+(?x_3,?y_3)),?z_1)
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 Approximationsample1.trs: Failure(timeout)
(95085 msec.)