MAYBE
Rewrite Rules:
   [ from(?x) -> :(?x,from(s(?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     f(c(?x)) -> ?x,
     f(+(c(?x),?y)) -> ?x,
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(?y,*(?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ +(+(+(?x_2,?y_2),?z_2),?z_1) = +(?x_2,+(+(?y_2,?z_2),?z_1)),
     +(?x_3,?z_1) = +(0,+(?x_3,?z_1)),
     +(?x_4,?z_1) = +(?x_4,+(0,?z_1)),
     +(?x_2,+(?x_1,+(?y_1,?z_1))) = +(+(?x_2,+(?x_1,?y_1)),?z_1),
     +(?x_2,?x_3) = +(+(?x_2,0),?x_3),
     +(?x_2,?x_4) = +(+(?x_2,?x_4),0),
     f(+(+(c(?x_6),?y_2),?z_2)) = ?x_6,
     f(c(?x_6)) = ?x_6,
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ]
Outer CPs:
   [ +(?x_1,+(?y_1,+(?y_2,?z_2))) = +(+(+(?x_1,?y_1),?y_2),?z_2),
     +(?x_1,+(?y_1,0)) = +(?x_1,?y_1),
     +(+(0,?y_2),?z_2) = +(?y_2,?z_2),
     0 = 0 ]
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
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ +(+(+(?x_3,+(?y_3,?y)),?y_2),?z_2) = +(+(?x_3,?y_3),+(?y,+(?y_2,?z_2))),
     +(+(+(+(?x,?y_5),?z_5),?y_2),?z_2) = +(?x,+(+(?y_5,?z_5),+(?y_2,?z_2))),
     +(+(?y,?y_2),?z_2) = +(0,+(?y,+(?y_2,?z_2))),
     +(+(?x,?y_2),?z_2) = +(?x,+(0,+(?y_2,?z_2))),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
     +(+(?x,?y_3),?z_3) = +(?x,+(+(?y_3,?z_3),0)),
     ?y = +(0,+(?y,0)),
     ?x = +(?x,+(0,0)),
     +(+(+(?x,?y),?y_2),?z_2) = +(?x,+(?y,+(?y_2,?z_2))),
     +(?x,?y) = +(?x,+(?y,0)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(+(?x,?y_3),?z_3),?z) = +(?x,+(+(?y_3,?z_3),?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(?x,?z) = +(?x,+(0,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(+(+(?x,?y_4),?z_4),+(?z,?z_1)) = +(+(?x,+(+(?y_4,?z_4),?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1),
     +(+(?x_3,+(?x_4,+(?y_4,?y))),?z) = +(?x_3,+(+(?x_4,?y_4),+(?y,?z))),
     +(+(?x_3,+(+(?x,?y_6),?z_6)),?z) = +(?x_3,+(?x,+(+(?y_6,?z_6),?z))),
     +(+(?x_3,?x),?z) = +(?x_3,+(?x,+(0,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_3,+(?x,?y)),?z) = +(?x_3,+(?x,+(?y,?z))),
     +(?x_2,+(?y_2,+(+(?y,?y_3),?z_3))) = +(+(+(?x_2,?y_2),?y),+(?y_3,?z_3)),
     +(?x_2,+(?y_2,+(?x_5,+(?y_5,?z)))) = +(+(+(?x_2,?y_2),+(?x_5,?y_5)),?z),
     +(?x_2,+(?y_2,?z)) = +(+(+(?x_2,?y_2),0),?z),
     +(?x_2,+(?y_2,?y)) = +(+(+(?x_2,?y_2),?y),0),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     ?z = +(+(0,0),?z),
     ?y = +(+(0,?y),0),
     +(?x_2,+(?y_2,+(?y,?z))) = +(+(+(?x_2,?y_2),?y),?z),
     +(?y,?z) = +(+(0,?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,+(?x_3,+(?y_3,?z))) = +(+(?x,+(?x_3,?y_3)),?z),
     +(?x,?z) = +(+(?x,0),?z),
     +(?x,?y) = +(+(?x,?y),0),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),+(?x_4,+(?y_4,?z))) = +(?x_1,+(+(?x,+(?x_4,?y_4)),?z)),
     +(+(?x_1,?x),?z) = +(?x_1,+(+(?x,0),?z)),
     +(?x,+(+(+(?y,?y_4),?z_4),?z_3)) = +(+(+(?x,?y),+(?y_4,?z_4)),?z_3),
     +(?x,+(+(?x_6,+(?y_6,?z)),?z_3)) = +(+(+(?x,+(?x_6,?y_6)),?z),?z_3),
     +(?x,+(?z,?z_3)) = +(+(+(?x,0),?z),?z_3),
     ?x_7 = f(+(+(c(?x_7),?y),+(?y_8,?z_8))),
     ?x_7 = f(+(+(c(?x_7),+(?x_10,?y_10)),?z)),
     ?x_7 = f(+(+(c(?x_7),0),?z)),
     ?x_7 = f(+(+(c(?x_7),?y),0)),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_3)) = +(+(+(?x,?y),?z),?z_3),
     ?x_7 = f(+(+(c(?x_7),?y),?z)),
     +(+(0,?y_3),?z_3) = +(?y_3,?z_3),
     0 = 0,
     +(0,+(?x,?z_3)) = +(?x,?z_3),
     +(+(?x_4,0),?x) = +(?x_4,?x),
     +(?x_2,+(?y_2,0)) = +(?x_2,?y_2),
     +(?x,+(0,?z_3)) = +(?x,?z_3),
     +(+(?x_4,?x),0) = +(?x_4,?x),
     ?x_7 = f(c(?x_7)),
     f(+(+(c(?x),?y_4),?z_4)) = ?x,
     f(c(?x)) = ?x ]
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_2,?y_2),?z_2),?z_1), +(?x_2,+(+(?y_2,?z_2),?z_1))> by Rules <2, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],1)], [([],2)]>
Critical Pair <+(?x_3,?z_1), +(0,+(?x_3,?z_1))> by Rules <3, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <+(?x_4,?z_1), +(?x_4,+(0,?z_1))> by Rules <4, 1> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([(+,2)],3)]>
Critical Pair <+(?x_2,+(?x_1,+(?y_1,?z_1))), +(+(?x_2,+(?x_1,?y_1)),?z_1)> by Rules <1, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],2)], [([],1)]>
Critical Pair <+(?x_2,?x_3), +(+(?x_2,0),?x_3)> by Rules <3, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],4)]>
Critical Pair <+(?x_2,?x_4), +(+(?x_2,?x_4),0)> by Rules <4, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],4)]>
Critical Pair <f(+(+(c(?x_6),?y_2),?z_2)), ?x_6> by Rules <2, 6> preceded by [(f,1)]
 joinable by a reduction of rules <[([(f,1)],1),([],6)], []>
Critical Pair <f(c(?x_6)), ?x_6> by Rules <4, 6> preceded by [(f,1)]
 joinable by a reduction of rules <[([],5)], []>
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)], [([],2)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <2, 2> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],1)], [([],1)]>
Critical Pair <+(+(+(?x_1,?y_1),?y_2),?z_2), +(?x_1,+(?y_1,+(?y_2,?z_2)))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],1)], [([],2)]>
Critical Pair <+(?x_1,?y_1), +(?x_1,+(?y_1,0))> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[], [([(+,2)],4)]>
Critical Pair <+(?y_2,?z_2), +(+(0,?y_2),?z_2)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([(+,1)],3)]>
Critical Pair <0, 0> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
   [ from(?x) -> :(?x,from(s(?x))),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(?x_2,+(?y_2,?z_2)) -> +(+(?x_2,?y_2),?z_2),
     +(0,?x_3) -> ?x_3,
     +(?x_4,0) -> ?x_4,
     f(c(?x_5)) -> ?x_5,
     f(+(c(?x_6),?y_6)) -> ?x_6,
     *(0,?y_7) -> 0,
     *(s(?x_8),?y_8) -> +(?y_8,*(?x_8,?y_8)) ]
Sort Assignment:
 * : 34*34=>34
 + : 34*34=>34
 0 : =>34
 : : 34*24=>24
 c : 36=>34
 f : 34=>36
 s : 34=>34
 from : 34=>24
non-linear variables: {?x,?y_8}
non-linear types: {34}
types leq non-linear types: {34}
rules applicable to terms of non-linear types:
   [ +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(?x_2,+(?y_2,?z_2)) -> +(+(?x_2,?y_2),?z_2),
     +(0,?x_3) -> ?x_3,
     +(?x_4,0) -> ?x_4,
     f(c(?x_5)) -> ?x_5,
     f(+(c(?x_6),?y_6)) -> ?x_6,
     *(0,?y_7) -> 0,
     *(s(?x_8),?y_8) -> +(?y_8,*(?x_8,?y_8)) ]
NLR:
0: {1,2,3,4,5,6,7,8}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {1,2,3,4,5,6,7,8}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ from(?x) -> :(?x,from(s(?x))),
     +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(?x_2,+(?y_2,?z_2)) -> +(+(?x_2,?y_2),?z_2),
     +(0,?x_3) -> ?x_3,
     +(?x_4,0) -> ?x_4,
     f(c(?x_5)) -> ?x_5,
     f(+(c(?x_6),?y_6)) -> ?x_6,
     *(0,?y_7) -> 0,
     *(s(?x_8),?y_8) -> +(?y_8,*(?x_8,?y_8)) ]
Sort Assignment:
 * : 34*34=>34
 + : 34*34=>34
 0 : =>34
 : : 34*24=>24
 c : 36=>34
 f : 34=>36
 s : 34=>34
 from : 34=>24
non-linear variables: {?x,?y_8}
non-linear types: {34}
types leq non-linear types: {34}
rules applicable to terms of non-linear types:
   [ +(+(?x_1,?y_1),?z_1) -> +(?x_1,+(?y_1,?z_1)),
     +(?x_2,+(?y_2,?z_2)) -> +(+(?x_2,?y_2),?z_2),
     +(0,?x_3) -> ?x_3,
     +(?x_4,0) -> ?x_4,
     f(c(?x_5)) -> ?x_5,
     f(+(c(?x_6),?y_6)) -> ?x_6,
     *(0,?y_7) -> 0,
     *(s(?x_8),?y_8) -> +(?y_8,*(?x_8,?y_8)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 19 rules by 3 steps unfolding
strenghten *(0,?y_15) and 0
strenghten f(c(?x_6)) and ?x_6
strenghten +(?x_1,+(?y_1,0)) and +(?x_1,?y_1)
strenghten +(?x_4,+(0,?z_1)) and +(?x_4,?z_1)
strenghten +(+(?x_2,?x_4),0) and +(?x_2,?x_4)
strenghten +(+(?x_2,0),?x_3) and +(?x_2,?x_3)
strenghten +(+(0,?y_2),?z_2) and +(?y_2,?z_2)
strenghten +(0,+(?x_3,?z_1)) and +(?x_3,?z_1)
strenghten *(0,:(?x,from(s(?x)))) and 0
strenghten f(+(+(c(?x_6),?y_2),?z_2)) and ?x_6
strenghten +(?x_1,+(?y_1,+(?y_2,?z_2))) and +(+(+(?x_1,?y_1),?y_2),?z_2)
strenghten +(?x_2,+(+(?y_2,?z_2),?z_1)) and +(+(+(?x_2,?y_2),?z_2),?z_1)
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_2,+(?x_1,?y_1)),?z_1) and +(?x_2,+(?x_1,+(?y_1,?z_1)))
obtain 34 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)sample2.trs: Failure(timeout)
(60899 msec.)