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

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

Try Layer Preserving Decomposition for...
   [ +(0,?x) -> ?x,
     +(?x,0) -> ?x,
     +(1,-(1)) -> 0,
     +(-(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,
     +(?x,0) -> ?x,
     +(1,-(1)) -> 0,
     +(-(1),1) -> 0,
     -(0) -> 0,
     -(-(?x)) -> ?x,
     -(+(?x,?y)) -> +(-(?x),-(?y)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Outside Critical Pair: <0, 0> by Rules <1, 0>
develop reducts from lhs term...
<{}, 0>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <+(?y_5,0), ?y_5> by Rules <8, 0>
develop reducts from lhs term...
<{8}, +(0,?y_5)>
<{1}, ?y_5>
<{}, +(?y_5,0)>
develop reducts from rhs term...
<{}, ?y_5>
Outside Critical Pair: <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1>
develop reducts from lhs term...
<{8}, +(+(0,?y_4),?x_4)>
<{1,8}, +(?y_4,?x_4)>
<{8}, +(+(?y_4,0),?x_4)>
<{8}, +(?x_4,+(0,?y_4))>
<{1}, +(?x_4,?y_4)>
<{}, +(?x_4,+(?y_4,0))>
develop reducts from rhs term...
<{8}, +(?y_4,?x_4)>
<{}, +(?x_4,?y_4)>
Outside Critical Pair: <+(0,?x_5), ?x_5> by Rules <8, 1>
develop reducts from lhs term...
<{8}, +(?x_5,0)>
<{0}, ?x_5>
<{}, +(0,?x_5)>
develop reducts from rhs term...
<{}, ?x_5>
Outside Critical Pair: <+(-(1),1), 0> by Rules <8, 2>
develop reducts from lhs term...
<{8}, +(1,-(1))>
<{3}, 0>
<{}, +(-(1),1)>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <+(1,-(1)), 0> by Rules <8, 3>
develop reducts from lhs term...
<{8}, +(-(1),1)>
<{2}, 0>
<{}, +(1,-(1))>
develop reducts from rhs term...
<{}, 0>
Outside Critical Pair: <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7>
develop reducts from lhs term...
<{8}, +(+(?y_4,?x_4),?y_5)>
<{8}, +(+(?x_4,?y_4),?y_5)>
<{8}, +(?y_5,+(?y_4,?x_4))>
<{}, +(?y_5,+(?x_4,?y_4))>
develop reducts from rhs term...
<{8}, +(+(?y_5,?y_4),?x_4)>
<{8}, +(+(?y_4,?y_5),?x_4)>
<{8}, +(?x_4,+(?y_5,?y_4))>
<{}, +(?x_4,+(?y_4,?y_5))>
Inside Critical Pair: <-(0), 0> by Rules <4, 5>
develop reducts from lhs term...
<{4}, 0>
<{}, -(0)>
develop reducts from rhs term...
<{}, 0>
Inside Critical Pair: <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5>
develop reducts from lhs term...
<{6}, +(-(-(?x_3)),-(-(?y_3)))>
<{8}, -(+(-(?y_3),-(?x_3)))>
<{}, -(+(-(?x_3),-(?y_3)))>
develop reducts from rhs term...
<{8}, +(?y_3,?x_3)>
<{}, +(?x_3,?y_3)>
Inside Critical Pair: <-(?x), +(-(0),-(?x))> by Rules <0, 6>
develop reducts from lhs term...
<{}, -(?x)>
develop reducts from rhs term...
<{4,8}, +(-(?x),0)>
<{8}, +(-(?x),-(0))>
<{4}, +(0,-(?x))>
<{}, +(-(0),-(?x))>
Inside Critical Pair: <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6>
develop reducts from lhs term...
<{}, -(?x_1)>
develop reducts from rhs term...
<{4,8}, +(0,-(?x_1))>
<{8}, +(-(0),-(?x_1))>
<{4}, +(-(?x_1),0)>
<{}, +(-(?x_1),-(0))>
Inside Critical Pair: <-(0), +(-(1),-(-(1)))> by Rules <2, 6>
develop reducts from lhs term...
<{4}, 0>
<{}, -(0)>
develop reducts from rhs term...
<{5,8}, +(1,-(1))>
<{8}, +(-(-(1)),-(1))>
<{5}, +(-(1),1)>
<{}, +(-(1),-(-(1)))>
Inside Critical Pair: <-(0), +(-(-(1)),-(1))> by Rules <3, 6>
develop reducts from lhs term...
<{4}, 0>
<{}, -(0)>
develop reducts from rhs term...
<{5,8}, +(-(1),1)>
<{8}, +(-(1),-(-(1)))>
<{5}, +(1,-(1))>
<{}, +(-(-(1)),-(1))>
Inside Critical Pair: <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6>
develop reducts from lhs term...
<{6,8}, +(-(?x_4),-(+(?z_4,?y_4)))>
<{6}, +(-(?x_4),-(+(?y_4,?z_4)))>
<{8}, -(+(+(?z_4,?y_4),?x_4))>
<{8}, -(+(+(?y_4,?z_4),?x_4))>
<{8}, -(+(?x_4,+(?z_4,?y_4)))>
<{}, -(+(?x_4,+(?y_4,?z_4)))>
develop reducts from rhs term...
<{6,8}, +(-(?z_4),+(-(?x_4),-(?y_4)))>
<{8}, +(-(?z_4),-(+(?y_4,?x_4)))>
<{8}, +(-(?z_4),-(+(?x_4,?y_4)))>
<{6}, +(+(-(?x_4),-(?y_4)),-(?z_4))>
<{8}, +(-(+(?y_4,?x_4)),-(?z_4))>
<{}, +(-(+(?x_4,?y_4)),-(?z_4))>
Inside Critical Pair: <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6>
develop reducts from lhs term...
<{6}, +(-(?y_5),-(?x_5))>
<{8}, -(+(?x_5,?y_5))>
<{}, -(+(?y_5,?x_5))>
develop reducts from rhs term...
<{8}, +(-(?y_5),-(?x_5))>
<{}, +(-(?x_5),-(?y_5))>
Inside Critical Pair: <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7>
develop reducts from lhs term...
<{8}, +(?z_4,?x)>
<{}, +(?x,?z_4)>
develop reducts from rhs term...
<{8}, +(+(?z_4,?x),0)>
<{8}, +(+(?x,?z_4),0)>
<{0,8}, +(?z_4,?x)>
<{0}, +(?x,?z_4)>
<{8}, +(0,+(?z_4,?x))>
<{}, +(0,+(?x,?z_4))>
Inside Critical Pair: <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7>
develop reducts from lhs term...
<{8}, +(?z_4,?x_1)>
<{}, +(?x_1,?z_4)>
develop reducts from rhs term...
<{8}, +(+(?z_4,0),?x_1)>
<{0,8}, +(?z_4,?x_1)>
<{8}, +(+(0,?z_4),?x_1)>
<{8}, +(?x_1,+(?z_4,0))>
<{0}, +(?x_1,?z_4)>
<{}, +(?x_1,+(0,?z_4))>
Inside Critical Pair: <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7>
develop reducts from lhs term...
<{8}, +(?z_4,0)>
<{0}, ?z_4>
<{}, +(0,?z_4)>
develop reducts from rhs term...
<{8}, +(+(?z_4,-(1)),1)>
<{8}, +(+(-(1),?z_4),1)>
<{8}, +(1,+(?z_4,-(1)))>
<{}, +(1,+(-(1),?z_4))>
Inside Critical Pair: <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7>
develop reducts from lhs term...
<{8}, +(?z_4,0)>
<{0}, ?z_4>
<{}, +(0,?z_4)>
develop reducts from rhs term...
<{8}, +(+(?z_4,1),-(1))>
<{8}, +(+(1,?z_4),-(1))>
<{8}, +(-(1),+(?z_4,1))>
<{}, +(-(1),+(1,?z_4))>
Inside Critical Pair: <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7>
develop reducts from lhs term...
<{8}, +(?z_4,+(?x_5,?y_5))>
<{8}, +(?z_4,+(?y_5,?x_5))>
<{7}, +(?y_5,+(?x_5,?z_4))>
<{8}, +(+(?x_5,?y_5),?z_4)>
<{}, +(+(?y_5,?x_5),?z_4)>
develop reducts from rhs term...
<{8}, +(+(?z_4,?y_5),?x_5)>
<{8}, +(+(?y_5,?z_4),?x_5)>
<{8}, +(?x_5,+(?z_4,?y_5))>
<{}, +(?x_5,+(?y_5,?z_4))>
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
183.trs: Failure(unknown)
(4445 msec.)