MAYBE
Rewrite Rules:
   [ a -> b,
     b -> c,
     c -> a,
     f(s(a)) -> a,
     f(s(b)) -> f(s(a)),
     f(s(c)) -> f(s(b)),
     +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
Apply Direct Methods...
Inner CPs:
   [ f(s(b)) = a,
     f(s(c)) = f(s(a)),
     f(s(a)) = f(s(b)),
     +(?x_1,+(?y,?x)) = +(+(?x_1,?x),?y),
     +(?x_1,+(?x_2,+(?y_2,?z_2))) = +(+(?x_1,+(?x_2,?y_2)),?z_2),
     +(?x_1,?x_3) = +(+(?x_1,0),?x_3),
     +(?x_1,s(+(?x_4,?y_4))) = +(+(?x_1,s(?x_4)),?y_4),
     +(+(?y,?x),?z_2) = +(?x,+(?y,?z_2)),
     +(+(+(?x_1,?y_1),?z_1),?z_2) = +(?x_1,+(+(?y_1,?z_1),?z_2)),
     +(?x_3,?z_2) = +(0,+(?x_3,?z_2)),
     +(s(+(?x_4,?y_4)),?z_2) = +(s(?x_4),+(?y_4,?z_2)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(+(?y_1,?z_1),?x) = +(+(?x,?y_1),?z_1),
     +(?y,+(?x_2,?y_2)) = +(?x_2,+(?y_2,?y)),
     +(?y,0) = ?y,
     +(?y,s(?x_4)) = s(+(?x_4,?y)),
     +(+(+(?x_2,?y_2),?y_1),?z_1) = +(?x_2,+(?y_2,+(?y_1,?z_1))),
     +(+(0,?y_1),?z_1) = +(?y_1,?z_1),
     +(+(s(?x_4),?y_1),?z_1) = s(+(?x_4,+(?y_1,?z_1))) ]
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:
   [ a = f(s(b)),
     f(s(a)) = f(s(c)),
     f(s(b)) = f(s(a)),
     f(s(b)) = a,
     f(s(c)) = f(s(a)),
     f(s(a)) = f(s(b)),
     +(+(?x,?y_1),?z_1) = +(+(?y_1,?z_1),?x),
     +(?x_2,+(?y_2,?y)) = +(?y,+(?x_2,?y_2)),
     ?y = +(?y,0),
     s(+(?x_4,?y)) = +(?y,s(?x_4)),
     +(+(?x_2,?x),?y) = +(?x_2,+(?y,?x)),
     +(?x,+(?y,?z_3)) = +(+(?y,?x),?z_3),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(+(?x_3,+(?y_3,?z)),?x) = +(+(?x,+(?x_3,?y_3)),?z),
     +(?z,?x) = +(+(?x,0),?z),
     +(s(+(?x_5,?z)),?x) = +(+(?x,s(?x_5)),?z),
     +(?x_2,+(?y_2,+(+(?y,?y_3),?z_3))) = +(+(+(?x_2,?y_2),?y),+(?y_3,?z_3)),
     +(?x_2,+(?y_2,+(?z,?y))) = +(+(+(?x_2,?y_2),?y),?z),
     +(?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,s(+(?x_7,?z)))) = +(+(+(?x_2,?y_2),s(?x_7)),?z),
     +(+(?y,?y_1),?z_1) = +(+(0,?y),+(?y_1,?z_1)),
     +(?z,?y) = +(+(0,?y),?z),
     +(?x_3,+(?y_3,?z)) = +(+(0,+(?x_3,?y_3)),?z),
     ?z = +(+(0,0),?z),
     s(+(?x_5,?z)) = +(+(0,s(?x_5)),?z),
     s(+(?x_4,+(+(?y,?y_5),?z_5))) = +(+(s(?x_4),?y),+(?y_5,?z_5)),
     s(+(?x_4,+(?z,?y))) = +(+(s(?x_4),?y),?z),
     s(+(?x_4,+(?x_7,+(?y_7,?z)))) = +(+(s(?x_4),+(?x_7,?y_7)),?z),
     s(+(?x_4,?z)) = +(+(s(?x_4),0),?z),
     s(+(?x_4,s(+(?x_9,?z)))) = +(+(s(?x_4),s(?x_9)),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x_2,+(?y_2,+(?y,?z))) = +(+(+(?x_2,?y_2),?y),?z),
     +(?y,?z) = +(+(0,?y),?z),
     s(+(?x_4,+(?y,?z))) = +(+(s(?x_4),?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(?x,+(?x_3,+(?y_3,?z))) = +(+(?x,+(?x_3,?y_3)),?z),
     +(?x,?z) = +(+(?x,0),?z),
     +(?x,s(+(?x_5,?z))) = +(+(?x,s(?x_5)),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     +(+(?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_1,?x),s(+(?x_6,?z))) = +(?x_1,+(+(?x,s(?x_6)),?z)),
     +(?x,+(+(+(?y,?y_4),?z_4),?z_3)) = +(+(+(?x,?y),+(?y_4,?z_4)),?z_3),
     +(?x,+(+(?z,?y),?z_3)) = +(+(+(?x,?y),?z),?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,+(s(+(?x_8,?z)),?z_3)) = +(+(+(?x,s(?x_8)),?z),?z_3),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_3)) = +(+(+(?x,?y),?z),?z_3),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(+(?x,?y_3),?z_3)) = +(?x,+(+(?y_3,?z_3),?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,s(+(?x_5,?y))) = +(s(?x_5),+(?y,?z)),
     +(+(+(?x_3,+(?y_3,?y)),?y_2),?z_2) = +(+(?x_3,?y_3),+(?y,+(?y_2,?z_2))),
     +(+(+(?y,?x),?y_2),?z_2) = +(?x,+(?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))),
     +(+(s(+(?x_7,?y)),?y_2),?z_2) = +(s(?x_7),+(?y,+(?y_2,?z_2))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(+(?x,?y),?y_2),?z_2) = +(?x,+(?y,+(?y_2,?z_2))),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(+(?x,?y_3),?z_3),?z) = +(?x,+(+(?y_3,?z_3),?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(s(+(?x_5,?y)),?z) = +(s(?x_5),+(?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),
     +(+(+(?x,?y_4),?z_4),+(?z,?z_1)) = +(+(?x,+(+(?y_4,?z_4),?z)),?z_1),
     +(s(+(?x_6,?y)),+(?z,?z_1)) = +(+(s(?x_6),+(?y,?z)),?z_1),
     +(+(?x_3,+(?x_4,+(?y_4,?y))),?z) = +(?x_3,+(+(?x_4,?y_4),+(?y,?z))),
     +(+(?x_3,+(?y,?x)),?z) = +(?x_3,+(?x,+(?y,?z))),
     +(+(?x_3,+(+(?x,?y_6),?z_6)),?z) = +(?x_3,+(?x,+(+(?y_6,?z_6),?z))),
     +(+(?x_3,?y),?z) = +(?x_3,+(0,+(?y,?z))),
     +(+(?x_3,s(+(?x_8,?y))),?z) = +(?x_3,+(s(?x_8),+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_3,+(?x,?y)),?z) = +(?x_3,+(?x,+(?y,?z))),
     +(?x,0) = ?x,
     +(+(0,?y_2),?z_2) = +(?y_2,?z_2),
     +(+(?x_3,0),?x) = +(?x_3,?x),
     +(0,+(?x,?z_4)) = +(?x,?z_4),
     +(?y,s(?x)) = s(+(?x,?y)),
     +(+(s(?x),?y_2),?z_2) = s(+(?x,+(?y_2,?z_2))),
     +(+(?x_3,s(?x)),?y) = +(?x_3,s(+(?x,?y))),
     +(s(?x),+(?y,?z_4)) = +(s(+(?x,?y)),?z_4) ]
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 <f(s(b)), a> by Rules <0, 3> preceded by [(f,1),(s,1)]
 joinable by a reduction of rules <[([],4),([],3)], []>
Critical Pair <f(s(c)), f(s(a))> by Rules <1, 4> preceded by [(f,1),(s,1)]
 joinable by a reduction of rules <[([(f,1),(s,1)],2)], []>
 joinable by a reduction of rules <[([],5)], [([(f,1),(s,1)],0)]>
Critical Pair <f(s(a)), f(s(b))> by Rules <2, 5> preceded by [(f,1),(s,1)]
 joinable by a reduction of rules <[([(f,1),(s,1)],0)], []>
 joinable by a reduction of rules <[], [([],4)]>
Critical Pair <+(?x_1,+(?y,?x)), +(+(?x_1,?x),?y)> by Rules <6, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],6)], [([],8)]>
Critical Pair <+(?x_1,+(?x_2,+(?y_2,?z_2))), +(+(?x_1,+(?x_2,?y_2)),?z_2)> by Rules <8, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],7)], [([],8)]>
Critical Pair <+(?x_1,?x_3), +(+(?x_1,0),?x_3)> by Rules <9, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([(+,1)],6),([(+,1)],9)]>
 joinable by a reduction of rules <[], [([],8),([(+,2)],9)]>
Critical Pair <+(?x_1,s(+(?x_4,?y_4))), +(+(?x_1,s(?x_4)),?y_4)> by Rules <10, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[], [([],8),([(+,2)],10)]>
Critical Pair <+(+(?y,?x),?z_2), +(?x,+(?y,?z_2))> by Rules <6, 8> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],6)], [([],7)]>
Critical Pair <+(+(+(?x_1,?y_1),?z_1),?z_2), +(?x_1,+(+(?y_1,?z_1),?z_2))> by Rules <7, 8> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],8)], [([],7)]>
Critical Pair <+(?x_3,?z_2), +(0,+(?x_3,?z_2))> by Rules <9, 8> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],9)]>
Critical Pair <+(s(+(?x_4,?y_4)),?z_2), +(s(?x_4),+(?y_4,?z_2))> by Rules <10, 8> preceded by [(+,1)]
 joinable by a reduction of rules <[([],10),([(s,1)],8)], [([],10)]>
 joinable by a reduction of rules <[], [([],7),([(+,1)],10)]>
 joinable by a reduction of rules <[([],10)], [([],10),([(s,1)],7)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <7, 7> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],8)], [([],8)]>
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)],7)], [([],7)]>
Critical Pair <+(+(?x_1,?y_1),?z_1), +(+(?y_1,?z_1),?x_1)> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([],8)], [([],6)]>
Critical Pair <+(?x_2,+(?y_2,?z_2)), +(?z_2,+(?x_2,?y_2))> by Rules <8, 6> preceded by []
 joinable by a reduction of rules <[([],7)], [([],6)]>
Critical Pair <?x_3, +(?x_3,0)> by Rules <9, 6> preceded by []
 joinable by a reduction of rules <[], [([],6),([],9)]>
Critical Pair <s(+(?x_4,?y_4)), +(?y_4,s(?x_4))> by Rules <10, 6> preceded by []
 joinable by a reduction of rules <[], [([],6),([],10)]>
Critical Pair <+(?x_2,+(?y_2,+(?y_1,?z_1))), +(+(+(?x_2,?y_2),?y_1),?z_1)> by Rules <8, 7> preceded by []
 joinable by a reduction of rules <[([],7)], [([],8)]>
Critical Pair <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> by Rules <9, 7> preceded by []
 joinable by a reduction of rules <[], [([(+,1)],9)]>
Critical Pair <s(+(?x_4,+(?y_1,?z_1))), +(+(s(?x_4),?y_1),?z_1)> by Rules <10, 7> preceded by []
 joinable by a reduction of rules <[], [([],8),([],10)]>
 joinable by a reduction of rules <[([(s,1)],7)], [([(+,1)],10),([],10)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 21 rules by 3 steps unfolding
strenghten a and b
strenghten a and c
strenghten b and a
strenghten b and c
strenghten c and a
strenghten c and b
strenghten +(?x_3,0) and ?x_3
strenghten +(0,?x_5) and ?x_5
strenghten f(s(a)) and a
strenghten f(s(b)) and a
strenghten f(s(c)) and a
strenghten f(s(a)) and f(s(b))
strenghten f(s(a)) and f(s(c))
strenghten f(s(b)) and f(s(a))
strenghten f(s(b)) and f(s(c))
strenghten s(+(?x_4,0)) and s(?x_4)
strenghten +(?y_4,s(?x_4)) and s(+(?x_4,?y_4))
strenghten +(?x_2,+(?y_2,0)) and +(?x_2,?y_2)
strenghten +(?x_5,+(0,?z_2)) and +(?x_5,?z_2)
strenghten +(+(?x_1,?x_5),0) and +(?x_1,?x_5)
strenghten +(+(?x_1,0),?x_3) and +(?x_1,?x_3)
strenghten +(+(0,?y_1),?z_1) and +(?y_1,?z_1)
strenghten +(0,+(?x_3,?z_2)) and +(?x_3,?z_2)
strenghten +(?x,+(?y,?z_2)) and +(+(?y,?x),?z_2)
strenghten +(?z_2,+(?x_2,?y_2)) and +(?x_2,+(?y_2,?z_2))
strenghten +(+(?x_1,?x),?y) and +(?x_1,+(?y,?x))
strenghten +(+(?y_1,?z_1),?x_1) and +(+(?x_1,?y_1),?z_1)
strenghten +(+(?x_1,s(?x_4)),?y_4) and +(?x_1,s(+(?x_4,?y_4)))
strenghten +(+(s(?x_4),?y_1),?z_1) and s(+(?x_4,+(?y_1,?z_1)))
strenghten +(s(?x_4),+(?y_4,?z_2)) and +(s(+(?x_4,?y_4)),?z_2)
strenghten +(?x_1,+(+(?y_1,?z_1),?z_2)) and +(+(+(?x_1,?y_1),?z_1),?z_2)
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)))
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:
   [ a -> b,
     b -> c,
     c -> a,
     f(s(a)) -> a,
     f(s(b)) -> f(s(a)),
     f(s(c)) -> f(s(b)),
     +(0,?x) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)) ]
   [ +(?x,?y) -> +(?y,?x),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (15)
  a:= 0
  b:= 0
  c:= 0
  f:= (11)+(8)*x1*x1
  s:= (8)+(1)*x1
retract f(s(a)) -> a
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (14)
  a:= 0
  b:= 0
  c:= (4)
  f:= (10)+(8)*x1*x1
  s:= (8)+(1)*x1
retract c -> a
retract f(s(a)) -> a
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (10)
  a:= 0
  b:= 0
  c:= 0
  f:= (4)+(8)*x1*x1
  s:= (4)+(2)*x1
retract c -> a
retract f(s(a)) -> a
retract +(0,?x) -> ?x
retract +(s(?x),?y) -> s(+(?x,?y))
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (6)
  a:= 0
  b:= (1)
  c:= 0
  f:= (6)+(1)*x1
  s:= (8)*x1
retract b -> c
retract c -> a
retract f(s(a)) -> a
retract f(s(b)) -> f(s(a))
retract +(0,?x) -> ?x
retract +(s(?x),?y) -> s(+(?x,?y))
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (10)
  a:= (1)
  b:= 0
  c:= 0
  f:= (10)+(3)*x1
  s:= (2)*x1
retract a -> b
retract b -> c
retract c -> a
retract f(s(a)) -> a
retract f(s(b)) -> f(s(a))
retract +(0,?x) -> ?x
retract +(s(?x),?y) -> s(+(?x,?y))
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  0:= (8)
  a:= 0
  b:= 0
  c:= (8)
  f:= (14)+(15)*x1
  s:= (8)+(9)*x1
relatively terminating
sample3.trs: Failure(timeout)
(112747 msec.)