MAYBE
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ -(0) = 0,
     -(+(-(?x_2),-(?y_2))) = +(?x_2,?y_2),
     -(?x) = +(-(0),-(?x)),
     -(0) = +(-(1),-(-(1))),
     -(+(?x_3,+(?y_3,?z_3))) = +(-(+(?x_3,?y_3)),-(?z_3)),
     -(+(?y_4,?x_4)) = +(-(?x_4),-(?y_4)),
     +(?x,?z_3) = +(0,+(?x,?z_3)),
     +(0,?z_3) = +(1,+(-(1),?z_3)),
     +(+(?y_4,?x_4),?z_3) = +(?x_4,+(?y_4,?z_3)),
     -(?x) = -(?x),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ ?x = +(?x,0),
     0 = +(-(1),1),
     +(?x_3,+(?y_3,?z_3)) = +(?z_3,+(?x_3,?y_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:
   [ +(?x,0) = ?x,
     +(-(0),-(?x)) = -(?x),
     +(0,+(?x,?z_4)) = +(?x,?z_4),
     +(-(1),1) = 0,
     +(-(1),-(-(1))) = -(0),
     +(1,+(-(1),?z_3)) = +(0,?z_3),
     0 = -(0),
     -(?x_1) = -(?x_1),
     -(0) = 0,
     -(+(-(?x_3),-(?y_3))) = +(?x_3,?y_3),
     ?x_1 = -(-(?x_1)),
     +(-(?x_3),-(?y_3)) = -(+(?x_3,?y_3)),
     -(?y) = +(-(0),-(?y)),
     -(0) = +(-(1),-(-(1))),
     -(+(?x_4,+(?y_4,?y))) = +(-(+(?x_4,?y_4)),-(?y)),
     -(+(?y,?x)) = +(-(?x),-(?y)),
     ?y = -(+(-(0),-(?y))),
     0 = -(+(-(1),-(-(1)))),
     +(?x_4,+(?y_4,?y)) = -(+(-(+(?x_4,?y_4)),-(?y))),
     +(?y,?x) = -(+(-(?x),-(?y))),
     +(?x,?y) = -(+(-(?x),-(?y))),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?y) = +(0,+(?y,?z)),
     +(?z,0) = +(1,+(-(1),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?y,?z) = +(0,+(?y,?z)),
     +(0,?z) = +(1,+(-(1),?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
     +(0,+(?z,?z_1)) = +(+(1,+(-(1),?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(-(+(?x_1,+(?y_1,?y))),-(?z)) = -(+(+(?x_1,?y_1),+(?y,?z))),
     +(-(?y),-(?z)) = -(+(0,+(?y,?z))),
     +(-(0),-(?z)) = -(+(1,+(-(1),?z))),
     +(-(+(?y,?x)),-(?z)) = -(+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(-(+(?x,?y)),-(?z)) = -(+(?x,+(?y,?z))),
     ?y = +(?y,0),
     0 = +(-(1),1),
     +(?x_4,+(?y_4,?y)) = +(?y,+(?x_4,?y_4)),
     +(-(?x),-(?y)) = -(+(?y,?x)),
     +(?x,+(?y,?z_5)) = +(+(?y,?x),?z_5) ]
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 <-(0), 0> by Rules <2, 3> preceded by [(-,1)]
 joinable by a reduction of rules <[([],2)], []>
Critical Pair <-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> by Rules <4, 3> preceded by [(-,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],3),([(+,1)],3)], []>
 joinable by a reduction of rules <[([],4),([(+,1)],3),([(+,2)],3)], []>
Critical Pair <-(?x), +(-(0),-(?x))> by Rules <0, 4> preceded by [(-,1)]
 joinable by a reduction of rules <[], [([(+,1)],2),([],0)]>
Critical Pair <-(0), +(-(1),-(-(1)))> by Rules <1, 4> preceded by [(-,1)]
 joinable by a reduction of rules <[([],2)], [([(+,2)],3),([],6),([],1)]>
 joinable by a reduction of rules <[([],2)], [([],6),([(+,1)],3),([],1)]>
Critical Pair <-(+(?x_3,+(?y_3,?z_3))), +(-(+(?x_3,?y_3)),-(?z_3))> by Rules <5, 4> preceded by [(-,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],4)], [([(+,1)],4),([],5)]>
Critical Pair <-(+(?y_4,?x_4)), +(-(?x_4),-(?y_4))> by Rules <6, 4> preceded by [(-,1)]
 joinable by a reduction of rules <[([],4)], [([],6)]>
Critical Pair <+(?x,?z_3), +(0,+(?x,?z_3))> by Rules <0, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([],0)]>
Critical Pair <+(0,?z_3), +(1,+(-(1),?z_3))> by Rules <1, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([],6)], [([(+,2)],6),([],6),([],5),([(+,2)],6),([(+,2)],1)]>
 joinable by a reduction of rules <[([],6)], [([],6),([(+,1)],6),([],5),([(+,2)],6),([(+,2)],1)]>
 joinable by a reduction of rules <[([],6)], [([],6),([],5),([],6),([],5),([(+,2)],1)]>
Critical Pair <+(+(?y_4,?x_4),?z_3), +(?x_4,+(?y_4,?z_3))> by Rules <6, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],6),([],5)], []>
 joinable by a reduction of rules <[([],5),([(+,2)],6)], [([],6),([],5)]>
Critical Pair <-(?x), -(?x)> by Rules <3, 3> preceded by [(-,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <5, 5> preceded by [(+,1)]
 joinable by a reduction of rules <[([],5),([(+,2)],5)], [([],5)]>
Critical Pair <+(?y_4,0), ?y_4> by Rules <6, 0> preceded by []
 joinable by a reduction of rules <[([],6),([],0)], []>
Critical Pair <+(-(1),1), 0> by Rules <6, 1> preceded by []
 joinable by a reduction of rules <[([],6),([],1)], []>
Critical Pair <+(?y_4,+(?x_3,?y_3)), +(?x_3,+(?y_3,?y_4))> by Rules <6, 5> preceded by []
 joinable by a reduction of rules <[([],6),([],5)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 17 rules by 3 steps unfolding
strenghten -(0) and 0
strenghten +(?x_7,0) and ?x_7
strenghten +(0,?x_5) and ?x_5
strenghten +(-(0),?x_10) and ?x_10
strenghten +(-(1),1) and 0
strenghten +(-(?x_5),-(0)) and -(?x_5)
strenghten +(-(0),-(?x)) and -(?x)
strenghten +(?x_3,+(?y_3,0)) and +(?x_3,?y_3)
strenghten +(?x_5,+(0,?z_3)) and +(?x_5,?z_3)
strenghten +(0,+(?x,?z_3)) and +(?x,?z_3)
strenghten +(-(?x_10),-(-(0))) and -(?x_10)
strenghten +(-(1),-(-(1))) and -(0)
strenghten +(-(?x_4),-(?y_4)) and -(+(?y_4,?x_4))
strenghten +(?x_3,+(?y_3,-(0))) and +(?x_3,?y_3)
strenghten +(?x_10,+(-(0),?z_3)) and +(?x_10,?z_3)
strenghten +(1,+(-(1),?z_3)) and +(0,?z_3)
strenghten -(+(-(?x_2),-(?y_2))) and +(?x_2,?y_2)
strenghten +(?x_3,+(?y_3,?y_4)) and +(?y_4,+(?x_3,?y_3))
strenghten +(?x_4,+(?y_4,?z_3)) and +(+(?y_4,?x_4),?z_3)
strenghten +(-(+(?x_3,?y_3)),-(?z_3)) and -(+(?x_3,+(?y_3,?z_3)))
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,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  -:= (1)*x1
  0:= (8)
  1:= 0
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (6)+(2)*x1
  0:= (8)
  1:= 0
retract +(0,?x) -> ?x
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (6)+(4)*x1*x1
  0:= (9)
  1:= 0
retract +(0,?x) -> ?x
retract -(0) -> 0
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  -:= (1)*x1
  0:= 0
  1:= (1)
retract +(0,?x) -> ?x
retract +(1,-(1)) -> 0
retract -(0) -> 0
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)+(1)*x1+(1)*x2
  -:= (2)+(4)*x1*x1
  0:= 0
  1:= (1)
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<-(0), 0> --> <0, 0> => yes
<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
<-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> --> <+(?x_2,?y_2), +(?x_2,?y_2)> => yes
<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
<-(0), +(-(1),-(-(1)))> --> <0, +(-(1),1)> => no
PCP_in(symP,S):
<-(+(?x_3,?y_3)), +(-(?y_3),-(?x_3))> --> <+(-(?x_3),-(?y_3)), +(-(?y_3),-(?x_3))> => yes
<-(+(+(?x_2,?y_2),?z_2)), +(-(?x_2),-(+(?y_2,?z_2)))> --> <+(+(-(?x_2),-(?y_2)),-(?z_2)), +(-(?x_2),+(-(?y_2),-(?z_2)))> => yes
<-(+(?x_1,+(?y_1,?z_1))), +(-(+(?x_1,?y_1)),-(?z_1))> --> <+(-(?x_1),+(-(?y_1),-(?z_1))), +(+(-(?x_1),-(?y_1)),-(?z_1))> => yes
CP(S,symP):
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <+(?x,0), +(+(?x,1),-(1))> => no
<0, +(-(1),1)> --> <0, +(-(1),1)> => no
check joinability condition:
check modulo joinability of 0 and +(-(1),1): joinable by {0}
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo reachablity from +(?x,0) to +(+(?x,1),-(1)): maybe not reachable
check modulo reachablity from 0 to +(-(1),1): maybe not reachable
failed
failure(Step 1)
   [ +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<-(0), 0> --> <0, 0> => yes
<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
<-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> --> <+(?x_2,?y_2), +(?x_2,?y_2)> => yes
<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
<-(0), +(-(1),-(-(1)))> --> <0, +(-(1),1)> => no
CP_in(symP,S):
<-(+(?x,+(?y,?z))), +(-(+(?x,?y)),-(?z))> --> <+(-(?x),+(-(?y),-(?z))), +(+(-(?x),-(?y)),-(?z))> => yes
<-(+(+(?x,?y),?z)), +(-(?x),-(+(?y,?z)))> --> <+(+(-(?x),-(?y)),-(?z)), +(-(?x),+(-(?y),-(?z)))> => yes
<-(+(?x,?y)), +(-(?y),-(?x))> --> <+(-(?x),-(?y)), +(-(?y),-(?x))> => yes
CP(S,symP):
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(+(?x_1,0),?x)> => no
<?x, +(?x,0)> --> <?x, +(?x,0)> => no
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <+(?x,0), +(+(?x,1),-(1))> => no
<0, +(-(1),1)> --> <0, +(-(1),1)> => no
check joinability condition:
check modulo joinability of 0 and +(-(1),1): maybe not joinable
check modulo reachablity from +(?x_1,?x) to +(+(?x_1,0),?x): maybe not reachable
check modulo reachablity from ?x to +(?x,0): maybe not reachable
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo reachablity from +(?x,0) to +(+(?x,1),-(1)): maybe not reachable
check modulo reachablity from 0 to +(-(1),1): maybe not reachable
failed
failure(Step 2)
   [ +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
Added S-Rules:
   [ +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  -:= (1)*x1
  0:= (8)
  1:= 0
retract +(0,?x) -> ?x
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (6)+(2)*x1
  0:= (8)
  1:= 0
retract +(0,?x) -> ?x
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)*x1+(1)*x2
  -:= (6)+(4)*x1*x1
  0:= (9)
  1:= 0
retract +(0,?x) -> ?x
retract -(0) -> 0
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  -:= (1)*x1
  0:= 0
  1:= (1)
retract +(0,?x) -> ?x
retract +(1,-(1)) -> 0
retract -(0) -> 0
retract -(-(?x)) -> ?x
Polynomial Interpretation:
  +:= (1)+(1)*x1+(1)*x2
  -:= (2)+(4)*x1*x1
  0:= 0
  1:= (1)
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<-(0), 0> --> <0, 0> => yes
<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
<-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> --> <+(?x_2,?y_2), +(?x_2,?y_2)> => yes
<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
<-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
<-(?x_3), +(-(?x_3),-(0))> --> <-(?x_3), -(?x_3)> => yes
<-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
PCP_in(symP,S):
<-(+(?x_3,?y_3)), +(-(?y_3),-(?x_3))> --> <+(-(?x_3),-(?y_3)), +(-(?y_3),-(?x_3))> => yes
<-(+(+(?x_2,?y_2),?z_2)), +(-(?x_2),-(+(?y_2,?z_2)))> --> <+(+(-(?x_2),-(?y_2)),-(?z_2)), +(-(?x_2),+(-(?y_2),-(?z_2)))> => yes
<-(+(?x_1,+(?y_1,?z_1))), +(-(+(?x_1,?y_1)),-(?z_1))> --> <+(-(?x_1),+(-(?y_1),-(?z_1))), +(+(-(?x_1),-(?y_1)),-(?z_1))> => yes
CP(S,symP):
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <?x, +(+(?x,1),-(1))> => no
<0, +(-(1),1)> --> <0, 0> => yes
<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, ?x> => yes
<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
<0, +(1,-(1))> --> <0, 0> => yes
check joinability condition:
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 5 (linear)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<-(0), 0> --> <0, 0> => yes
<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
<-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> --> <+(?x_2,?y_2), +(?x_2,?y_2)> => yes
<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
<-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
<-(?x_3), +(-(?x_3),-(0))> --> <-(?x_3), -(?x_3)> => yes
<-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
CP_in(symP,S):
<-(+(?x,+(?y,?z))), +(-(+(?x,?y)),-(?z))> --> <+(-(?x),+(-(?y),-(?z))), +(+(-(?x),-(?y)),-(?z))> => yes
<-(+(+(?x,?y),?z)), +(-(?x),-(+(?y,?z)))> --> <+(+(-(?x),-(?y)),-(?z)), +(-(?x),+(-(?y),-(?z)))> => yes
<-(+(?x,?y)), +(-(?y),-(?x))> --> <+(-(?x),-(?y)), +(-(?y),-(?x))> => yes
CP(S,symP):
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
<+(?x,0), +(+(?x,1),-(1))> --> <?x, +(+(?x,1),-(1))> => no
<0, +(-(1),1)> --> <0, 0> => yes
<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, ?x> => yes
<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
<0, +(1,-(1))> --> <0, 0> => yes
check joinability condition:
check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
STEP: 6 (relative)
S:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Check relative termination:
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(?x,0) -> ?x,
     +(-(1),1) -> 0 ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Polynomial Interpretation:
  +:= (3)+(1)*x1+(1)*x2
  -:= (1)*x1+(8)*x1*x1
  0:= 0
  1:= 0
retract +(0,?x) -> ?x
retract +(1,-(1)) -> 0
retract -(+(?x,?y)) -> +(-(?x),-(?y))
retract +(?x,0) -> ?x
retract +(-(1),1) -> 0
Polynomial Interpretation:
  +:= (3)+(1)*x1+(1)*x2
  -:= (3)+(4)*x1+(1)*x1*x1
  0:= 0
  1:= 0
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Sort Assignment:
 + : 17*17=>17
 - : 17=>17
 0 : =>17
 1 : =>17
maximal types: {17}
Persistent Decomposition failed: Can't judge

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

Try Commutative Decomposition for...
   [ +(0,?x) -> ?x,
     +(1,-(1)) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Outside Critical Pair: <+(?y_4,0), ?y_4> by Rules <6, 0>
develop reducts from lhs term...
<{6}, +(0,?y_4)>
<{}, +(?y_4,0)>
develop reducts from rhs term...
<{}, ?y_4>
Outside Critical Pair: <+(-(1),1), 0> by Rules <6, 1>
develop reducts from lhs term...
<{6}, +(1,-(1))>
<{}, +(-(1),1)>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <+(?y_4,+(?x_3,?y_3)), +(?x_3,+(?y_3,?y_4))> by Rules <6, 5>
develop reducts from lhs term...
<{6}, +(+(?y_3,?x_3),?y_4)>
<{6}, +(+(?x_3,?y_3),?y_4)>
<{6}, +(?y_4,+(?y_3,?x_3))>
<{}, +(?y_4,+(?x_3,?y_3))>
develop reducts from rhs term...
<{6}, +(+(?y_4,?y_3),?x_3)>
<{6}, +(+(?y_3,?y_4),?x_3)>
<{6}, +(?x_3,+(?y_4,?y_3))>
<{}, +(?x_3,+(?y_3,?y_4))>
Inside Critical Pair: <-(0), 0> by Rules <2, 3>
develop reducts from lhs term...
<{2}, 0>
<{}, -(0)>
develop reducts from rhs term...
<{}, 0>
Inside Critical Pair: <-(+(-(?x_2),-(?y_2))), +(?x_2,?y_2)> by Rules <4, 3>
develop reducts from lhs term...
<{4}, +(-(-(?x_2)),-(-(?y_2)))>
<{6}, -(+(-(?y_2),-(?x_2)))>
<{}, -(+(-(?x_2),-(?y_2)))>
develop reducts from rhs term...
<{6}, +(?y_2,?x_2)>
<{}, +(?x_2,?y_2)>
Inside Critical Pair: <-(?x), +(-(0),-(?x))> by Rules <0, 4>
develop reducts from lhs term...
<{}, -(?x)>
develop reducts from rhs term...
<{2,6}, +(-(?x),0)>
<{6}, +(-(?x),-(0))>
<{2}, +(0,-(?x))>
<{}, +(-(0),-(?x))>
Inside Critical Pair: <-(0), +(-(1),-(-(1)))> by Rules <1, 4>
develop reducts from lhs term...
<{2}, 0>
<{}, -(0)>
develop reducts from rhs term...
<{3,6}, +(1,-(1))>
<{6}, +(-(-(1)),-(1))>
<{3}, +(-(1),1)>
<{}, +(-(1),-(-(1)))>
Inside Critical Pair: <-(+(?x_3,+(?y_3,?z_3))), +(-(+(?x_3,?y_3)),-(?z_3))> by Rules <5, 4>
develop reducts from lhs term...
<{4,6}, +(-(?x_3),-(+(?z_3,?y_3)))>
<{4}, +(-(?x_3),-(+(?y_3,?z_3)))>
<{6}, -(+(+(?z_3,?y_3),?x_3))>
<{6}, -(+(+(?y_3,?z_3),?x_3))>
<{6}, -(+(?x_3,+(?z_3,?y_3)))>
<{}, -(+(?x_3,+(?y_3,?z_3)))>
develop reducts from rhs term...
<{4,6}, +(-(?z_3),+(-(?x_3),-(?y_3)))>
<{6}, +(-(?z_3),-(+(?y_3,?x_3)))>
<{6}, +(-(?z_3),-(+(?x_3,?y_3)))>
<{4}, +(+(-(?x_3),-(?y_3)),-(?z_3))>
<{6}, +(-(+(?y_3,?x_3)),-(?z_3))>
<{}, +(-(+(?x_3,?y_3)),-(?z_3))>
Inside Critical Pair: <-(+(?y_4,?x_4)), +(-(?x_4),-(?y_4))> by Rules <6, 4>
develop reducts from lhs term...
<{4}, +(-(?y_4),-(?x_4))>
<{6}, -(+(?x_4,?y_4))>
<{}, -(+(?y_4,?x_4))>
develop reducts from rhs term...
<{6}, +(-(?y_4),-(?x_4))>
<{}, +(-(?x_4),-(?y_4))>
Inside Critical Pair: <+(?x,?z_3), +(0,+(?x,?z_3))> by Rules <0, 5>
develop reducts from lhs term...
<{6}, +(?z_3,?x)>
<{}, +(?x,?z_3)>
develop reducts from rhs term...
<{6}, +(+(?z_3,?x),0)>
<{6}, +(+(?x,?z_3),0)>
<{0,6}, +(?z_3,?x)>
<{0}, +(?x,?z_3)>
<{6}, +(0,+(?z_3,?x))>
<{}, +(0,+(?x,?z_3))>
Inside Critical Pair: <+(0,?z_3), +(1,+(-(1),?z_3))> by Rules <1, 5>
develop reducts from lhs term...
<{6}, +(?z_3,0)>
<{0}, ?z_3>
<{}, +(0,?z_3)>
develop reducts from rhs term...
<{6}, +(+(?z_3,-(1)),1)>
<{6}, +(+(-(1),?z_3),1)>
<{6}, +(1,+(?z_3,-(1)))>
<{}, +(1,+(-(1),?z_3))>
Inside Critical Pair: <+(+(?y_4,?x_4),?z_3), +(?x_4,+(?y_4,?z_3))> by Rules <6, 5>
develop reducts from lhs term...
<{6}, +(?z_3,+(?x_4,?y_4))>
<{6}, +(?z_3,+(?y_4,?x_4))>
<{5}, +(?y_4,+(?x_4,?z_3))>
<{6}, +(+(?x_4,?y_4),?z_3)>
<{}, +(+(?y_4,?x_4),?z_3)>
develop reducts from rhs term...
<{6}, +(+(?z_3,?y_4),?x_4)>
<{6}, +(+(?y_4,?z_3),?x_4)>
<{6}, +(?x_4,+(?z_3,?y_4))>
<{}, +(?x_4,+(?y_4,?z_3))>
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
185.trs: Failure(unknown)
(4506 msec.)