13.72/12.46	MAYBE
13.72/12.46	(ignored inputs)COMMENT doi:10.4230/LIPIcs.FSCD.2016.33 [36] Example 25 submitted by: Takahito Aoto and Yoshihito Toyama
13.72/12.46	Rewrite Rules:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Apply Direct Methods...
13.72/12.46	Inner CPs:
13.72/12.46	   [ -(0) = 0,
13.72/12.46	     -(+(-(?x_3),-(?y_3))) = +(?x_3,?y_3),
13.72/12.46	     -(?x) = +(-(0),-(?x)),
13.72/12.46	     -(?x_1) = +(-(?x_1),-(0)),
13.72/12.46	     -(0) = +(-(1),-(-(1))),
13.72/12.46	     -(0) = +(-(-(1)),-(1)),
13.72/12.46	     -(+(?x_4,+(?y_4,?z_4))) = +(-(+(?x_4,?y_4)),-(?z_4)),
13.72/12.46	     -(+(?y_5,?x_5)) = +(-(?x_5),-(?y_5)),
13.72/12.46	     +(?x,?z_4) = +(0,+(?x,?z_4)),
13.72/12.46	     +(?x_1,?z_4) = +(?x_1,+(0,?z_4)),
13.72/12.46	     +(0,?z_4) = +(1,+(-(1),?z_4)),
13.72/12.46	     +(0,?z_4) = +(-(1),+(1,?z_4)),
13.72/12.46	     +(+(?y_5,?x_5),?z_4) = +(?x_5,+(?y_5,?z_4)),
13.72/12.46	     -(?x) = -(?x),
13.72/12.46	     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
13.72/12.46	Outer CPs:
13.72/12.46	   [ 0 = 0,
13.72/12.46	     ?x = +(?x,0),
13.72/12.46	     +(?x_4,?y_4) = +(?x_4,+(?y_4,0)),
13.72/12.46	     ?x_1 = +(0,?x_1),
13.72/12.46	     0 = +(-(1),1),
13.72/12.46	     0 = +(1,-(1)),
13.72/12.46	     +(?x_4,+(?y_4,?z_4)) = +(?z_4,+(?x_4,?y_4)) ]
13.72/12.46	not Overlay, check Termination...
13.72/12.46	unknown/not Terminating
13.72/12.46	unknown Knuth & Bendix
13.72/12.46	Linear
13.72/12.46	unknown Development Closed
13.72/12.46	unknown Strongly Closed
13.72/12.46	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
13.72/12.46	unknown Upside-Parallel-Closed/Outside-Closed
13.72/12.46	(inner) Parallel CPs: (not computed)
13.72/12.46	unknown Toyama (Parallel CPs)
13.72/12.46	Simultaneous CPs:
13.72/12.46	   [ 0 = 0,
13.72/12.46	     +(?x,0) = ?x,
13.72/12.46	     +(-(0),-(?x)) = -(?x),
13.72/12.46	     +(0,+(?x,?z_5)) = +(?x,?z_5),
13.72/12.46	     +(?x_4,+(?y_4,0)) = +(?x_4,?y_4),
13.72/12.46	     +(0,?x) = ?x,
13.72/12.46	     +(-(?x),-(0)) = -(?x),
13.72/12.46	     +(?x,+(0,?z_5)) = +(?x,?z_5),
13.72/12.46	     +(-(1),1) = 0,
13.72/12.46	     +(-(1),-(-(1))) = -(0),
13.72/12.46	     +(1,+(-(1),?z_4)) = +(0,?z_4),
13.72/12.46	     +(1,-(1)) = 0,
13.72/12.46	     +(-(-(1)),-(1)) = -(0),
13.72/12.46	     +(-(1),+(1,?z_4)) = +(0,?z_4),
13.72/12.46	     0 = -(0),
13.72/12.46	     -(?x_1) = -(?x_1),
13.72/12.46	     -(0) = 0,
13.72/12.46	     -(+(-(?x_4),-(?y_4))) = +(?x_4,?y_4),
13.72/12.46	     ?x_1 = -(-(?x_1)),
13.72/12.46	     +(-(?x_4),-(?y_4)) = -(+(?x_4,?y_4)),
13.72/12.46	     -(?y) = +(-(0),-(?y)),
13.72/12.46	     -(?x) = +(-(?x),-(0)),
13.72/12.46	     -(0) = +(-(1),-(-(1))),
13.72/12.46	     -(0) = +(-(-(1)),-(1)),
13.72/12.46	     -(+(?x_5,+(?y_5,?y))) = +(-(+(?x_5,?y_5)),-(?y)),
13.72/12.46	     -(+(?y,?x)) = +(-(?x),-(?y)),
13.72/12.46	     ?y = -(+(-(0),-(?y))),
13.72/12.46	     ?x = -(+(-(?x),-(0))),
13.72/12.46	     0 = -(+(-(1),-(-(1)))),
13.72/12.46	     0 = -(+(-(-(1)),-(1))),
13.72/12.46	     +(?x_5,+(?y_5,?y)) = -(+(-(+(?x_5,?y_5)),-(?y))),
13.72/12.46	     +(?y,?x) = -(+(-(?x),-(?y))),
13.72/12.46	     +(?x,?y) = -(+(-(?x),-(?y))),
13.72/12.46	     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
13.72/12.46	     ?y = +(0,+(?y,0)),
13.72/12.46	     ?x = +(?x,+(0,0)),
13.72/12.46	     0 = +(1,+(-(1),0)),
13.72/12.46	     0 = +(-(1),+(1,0)),
13.72/12.46	     +(?y,?x) = +(?x,+(?y,0)),
13.72/12.46	     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
13.72/12.46	     +(?z,?y) = +(0,+(?y,?z)),
13.72/12.46	     +(?z,?x) = +(?x,+(0,?z)),
13.72/12.46	     +(?z,0) = +(1,+(-(1),?z)),
13.72/12.46	     +(?z,0) = +(-(1),+(1,?z)),
13.72/12.46	     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) = +(?x,+(?y,0)),
13.72/12.46	     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
13.72/12.46	     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
13.72/12.46	     +(?y,?z) = +(0,+(?y,?z)),
13.72/12.46	     +(?x,?z) = +(?x,+(0,?z)),
13.72/12.46	     +(0,?z) = +(1,+(-(1),?z)),
13.72/12.46	     +(0,?z) = +(-(1),+(1,?z)),
13.72/12.46	     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
13.72/12.46	     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
13.72/12.46	     +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1),
13.72/12.46	     +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1),
13.72/12.46	     +(0,+(?z,?z_1)) = +(+(1,+(-(1),?z)),?z_1),
13.72/12.46	     +(0,+(?z,?z_1)) = +(+(-(1),+(1,?z)),?z_1),
13.72/12.46	     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
13.72/12.46	     +(-(+(?x_1,+(?y_1,?y))),-(?z)) = -(+(+(?x_1,?y_1),+(?y,?z))),
13.72/12.46	     +(-(?y),-(?z)) = -(+(0,+(?y,?z))),
13.72/12.46	     +(-(?x),-(?z)) = -(+(?x,+(0,?z))),
13.72/12.46	     +(-(0),-(?z)) = -(+(1,+(-(1),?z))),
13.72/12.46	     +(-(0),-(?z)) = -(+(-(1),+(1,?z))),
13.72/12.46	     +(-(+(?y,?x)),-(?z)) = -(+(?x,+(?y,?z))),
13.72/12.46	     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
13.72/12.46	     +(-(+(?x,?y)),-(?z)) = -(+(?x,+(?y,?z))),
13.72/12.46	     ?y = +(?y,0),
13.72/12.46	     ?x = +(0,?x),
13.72/12.46	     0 = +(-(1),1),
13.72/12.46	     0 = +(1,-(1)),
13.72/12.46	     +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)),
13.72/12.46	     +(-(?x),-(?y)) = -(+(?y,?x)),
13.72/12.46	     +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6) ]
13.72/12.46	unknown Okui (Simultaneous CPs)
13.72/12.46	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
13.72/12.46	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
13.72/12.46	check Locally Decreasing Diagrams by Rule Labelling...
13.72/12.46	Critical Pair <-(0), 0> by Rules <4, 5> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],4)], []>
13.72/12.46	Critical Pair <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],6),([(+,2)],5),([(+,1)],5)], []>
13.72/12.46	 joinable by a reduction of rules <[([],6),([(+,1)],5),([(+,2)],5)], []>
13.72/12.46	Critical Pair <-(?x), +(-(0),-(?x))> by Rules <0, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[], [([(+,1)],4),([],0)]>
13.72/12.46	Critical Pair <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[], [([(+,2)],4),([],1)]>
13.72/12.46	Critical Pair <-(0), +(-(1),-(-(1)))> by Rules <2, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],4)], [([(+,2)],5),([],3)]>
13.72/12.46	Critical Pair <-(0), +(-(-(1)),-(1))> by Rules <3, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],4)], [([(+,1)],5),([],2)]>
13.72/12.46	Critical Pair <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],6),([(+,2)],6)], [([(+,1)],6),([],7)]>
13.72/12.46	Critical Pair <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[([],6)], [([],8)]>
13.72/12.46	Critical Pair <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[], [([],0)]>
13.72/12.46	Critical Pair <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[], [([(+,2)],0)]>
13.72/12.46	Critical Pair <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],3)]>
13.72/12.46	 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],3)]>
13.72/12.46	Critical Pair <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],2)]>
13.72/12.46	 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],2)]>
13.72/12.46	Critical Pair <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[([(+,1)],8),([],7)], []>
13.72/12.46	 joinable by a reduction of rules <[([],7),([(+,2)],8)], [([],8),([],7)]>
13.72/12.46	Critical Pair <-(?x), -(?x)> by Rules <5, 5> preceded by [(-,1)]
13.72/12.46	 joinable by a reduction of rules <[], []>
13.72/12.46	Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <7, 7> preceded by [(+,1)]
13.72/12.46	 joinable by a reduction of rules <[([],7),([(+,2)],7)], [([],7)]>
13.72/12.46	Critical Pair <0, 0> by Rules <1, 0> preceded by []
13.72/12.46	 joinable by a reduction of rules <[], []>
13.72/12.46	Critical Pair <+(?y_5,0), ?y_5> by Rules <8, 0> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([],1)], []>
13.72/12.46	Critical Pair <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([(+,2)],1)], []>
13.72/12.46	Critical Pair <+(0,?x_5), ?x_5> by Rules <8, 1> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([],0)], []>
13.72/12.46	Critical Pair <+(-(1),1), 0> by Rules <8, 2> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([],3)], []>
13.72/12.46	Critical Pair <+(1,-(1)), 0> by Rules <8, 3> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([],2)], []>
13.72/12.46	Critical Pair <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7> preceded by []
13.72/12.46	 joinable by a reduction of rules <[([],8),([],7)], []>
13.72/12.46	unknown Diagram Decreasing
13.72/12.46	check Non-Confluence...
13.72/12.46	obtain 11 rules by 3 steps unfolding
13.72/12.46	obtain 100 candidates for checking non-joinability
13.72/12.46	check by TCAP-Approximation (failure)
13.72/12.46	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
13.72/12.46	check by Interpretation(mod2) (failure)
13.72/12.46	check by Descendants-Approximation, check by Ordering(poly) (failure)
13.72/12.46	unknown Non-Confluence
13.72/12.46	Check relative termination:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46	   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Polynomial Interpretation:
13.72/12.46	  +:= (2)+(1)*x1+(1)*x2
13.72/12.46	  -:= (2)*x1+(2)*x1*x1
13.72/12.46	  0:= 0
13.72/12.46	  1:= 0
13.72/12.46	retract +(0,?x) -> ?x
13.72/12.46	retract +(?x,0) -> ?x
13.72/12.46	retract +(1,-(1)) -> 0
13.72/12.46	retract +(-(1),1) -> 0
13.72/12.46	retract -(+(?x,?y)) -> +(-(?x),-(?y))
13.72/12.46	Polynomial Interpretation:
13.72/12.46	  +:= (2)+(1)*x1+(1)*x2
13.72/12.46	  -:= (1)+(2)*x1+(2)*x1*x1
13.72/12.46	  0:= 0
13.72/12.46	  1:= 0
13.72/12.46	relatively terminating
13.72/12.46	unknown Huet (modulo AC)
13.72/12.46	check by Reduction-Preserving Completion...
13.72/12.46	STEP: 1 (parallel)
13.72/12.46	S:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46	P:
13.72/12.46	   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	S: terminating
13.72/12.46	CP(S,S):
13.72/12.46	<0, 0> --> <0, 0> => yes
13.72/12.46	<0, 0> --> <0, 0> => yes
13.72/12.46	<-(0), 0> --> <0, 0> => yes
13.72/12.46	<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
13.72/12.46	<-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes
13.72/12.46	<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
13.72/12.46	<-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes
13.72/12.46	<-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
13.72/12.46	<-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
13.72/12.46	PCP_in(symP,S):
13.72/12.46	<-(+(?x_3,?y_3)), +(-(?y_3),-(?x_3))> --> <+(-(?x_3),-(?y_3)), +(-(?y_3),-(?x_3))> => yes
13.72/12.46	<-(+(+(?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
13.72/12.46	<-(+(?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
13.72/12.46	CP(S,symP):
13.72/12.46	<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46	<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
13.72/12.46	<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46	<?x, +(?x,0)> --> <?x, ?x> => yes
13.72/12.46	<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
13.72/12.46	<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46	<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46	<?x, +(0,?x)> --> <?x, ?x> => yes
13.72/12.46	<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
13.72/12.46	<+(?x,0), +(+(?x,1),-(1))> --> <?x, +(+(?x,1),-(1))> => no
13.72/12.46	<0, +(-(1),1)> --> <0, 0> => yes
13.72/12.46	<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
13.72/12.46	<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
13.72/12.46	<0, +(1,-(1))> --> <0, 0> => yes
13.72/12.46	check joinability condition:
13.72/12.46	check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
13.72/12.46	check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
13.72/12.46	check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
13.72/12.46	check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
13.72/12.46	failed
13.72/12.46	failure(Step 1)
13.72/12.46	   [ ]
13.72/12.46	Added S-Rules:
13.72/12.46	   [ ]
13.72/12.46	Added P-Rules:
13.72/12.46	   [ ]
13.72/12.46	STEP: 2 (linear)
13.72/12.46	S:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46	P:
13.72/12.46	   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	S: terminating
13.72/12.46	CP(S,S):
13.72/12.46	<0, 0> --> <0, 0> => yes
13.72/12.46	<0, 0> --> <0, 0> => yes
13.72/12.46	<-(0), 0> --> <0, 0> => yes
13.72/12.46	<-(?x), -(?x)> --> <-(?x), -(?x)> => yes
13.72/12.46	<-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes
13.72/12.46	<-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes
13.72/12.46	<-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes
13.72/12.46	<-(0), +(-(1),-(-(1)))> --> <0, 0> => yes
13.72/12.46	<-(0), +(-(-(1)),-(1))> --> <0, 0> => yes
13.72/12.46	CP_in(symP,S):
13.72/12.46	<-(+(?x,+(?y,?z))), +(-(+(?x,?y)),-(?z))> --> <+(-(?x),+(-(?y),-(?z))), +(+(-(?x),-(?y)),-(?z))> => yes
13.72/12.46	<-(+(+(?x,?y),?z)), +(-(?x),-(+(?y,?z)))> --> <+(+(-(?x),-(?y)),-(?z)), +(-(?x),+(-(?y),-(?z)))> => yes
13.72/12.46	<-(+(?x,?y)), +(-(?y),-(?x))> --> <+(-(?x),-(?y)), +(-(?y),-(?x))> => yes
13.72/12.46	CP(S,symP):
13.72/12.46	<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46	<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
13.72/12.46	<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46	<?x, +(?x,0)> --> <?x, ?x> => yes
13.72/12.46	<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
13.72/12.46	<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
13.72/12.46	<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
13.72/12.46	<?x, +(0,?x)> --> <?x, ?x> => yes
13.72/12.46	<+(0,?z), +(1,+(-(1),?z))> --> <?z, +(1,+(-(1),?z))> => no
13.72/12.46	<+(?x,0), +(+(?x,1),-(1))> --> <?x, +(+(?x,1),-(1))> => no
13.72/12.46	<0, +(-(1),1)> --> <0, 0> => yes
13.72/12.46	<+(0,?z), +(-(1),+(1,?z))> --> <?z, +(-(1),+(1,?z))> => no
13.72/12.46	<+(?x,0), +(+(?x,-(1)),1)> --> <?x, +(+(?x,-(1)),1)> => no
13.72/12.46	<0, +(1,-(1))> --> <0, 0> => yes
13.72/12.46	check joinability condition:
13.72/12.46	check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable
13.72/12.46	check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable
13.72/12.46	check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable
13.72/12.46	check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable
13.72/12.46	failed
13.72/12.46	failure(Step 2)
13.72/12.46	   [ ]
13.72/12.46	Added S-Rules:
13.72/12.46	   [ ]
13.72/12.46	Added P-Rules:
13.72/12.46	   [ ]
13.72/12.46	STEP: 3 (relative)
13.72/12.46	S:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46	P:
13.72/12.46	   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Check relative termination:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
13.72/12.46	   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Polynomial Interpretation:
13.72/12.46	  +:= (2)+(1)*x1+(1)*x2
13.72/12.46	  -:= (2)*x1+(2)*x1*x1
13.72/12.46	  0:= 0
13.72/12.46	  1:= 0
13.72/12.46	retract +(0,?x) -> ?x
13.72/12.46	retract +(?x,0) -> ?x
13.72/12.46	retract +(1,-(1)) -> 0
13.72/12.46	retract +(-(1),1) -> 0
13.72/12.46	retract -(+(?x,?y)) -> +(-(?x),-(?y))
13.72/12.46	Polynomial Interpretation:
13.72/12.46	  +:= (2)+(1)*x1+(1)*x2
13.72/12.46	  -:= (1)+(2)*x1+(2)*x1*x1
13.72/12.46	  0:= 0
13.72/12.46	  1:= 0
13.72/12.46	relatively terminating
13.72/12.46	S/P: relatively terminating
13.72/12.46	check CP condition:
13.72/12.46	failed
13.72/12.46	failure(Step 3)
13.72/12.46	failure(no possibility remains)
13.72/12.46	unknown Reduction-Preserving Completion
13.72/12.46	check by Ordered Rewriting...
13.72/12.46	remove redundants rules and split
13.72/12.46	R-part:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ]
13.72/12.46	E-part:
13.72/12.46	   [ +(?x,?y) -> +(?y,?x),
13.72/12.46	     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46	Perform abstraction and check...
13.72/12.46	Increase tree depth and check...
13.72/12.46	Apply reduction-preserving transformation...
13.72/12.46	Rules to add:
13.72/12.46	   [ +(1,+(?x_6,-(1))) -> ?x_6 ]
13.72/12.46	remove redundants rules and split
13.72/12.46	R-part:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(1,+(?x_6,-(1))) -> ?x_6 ]
13.72/12.46	E-part:
13.72/12.46	   [ +(?x,?y) -> +(?y,?x),
13.72/12.46	     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46	Perform abstraction and check...
13.72/12.46	Increase tree depth and check...
13.72/12.46	Apply reduction-preserving transformation...
13.72/12.46	Rules to add:
13.72/12.46	   [ +(1,+(-(1),?x_6)) -> ?x_6 ]
13.72/12.46	remove redundants rules and split
13.72/12.46	R-part:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46	     +(1,+(-(1),?x_6)) -> ?x_6 ]
13.72/12.46	E-part:
13.72/12.46	   [ +(?x,?y) -> +(?y,?x),
13.72/12.46	     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46	Perform abstraction and check...
13.72/12.46	Increase tree depth and check...
13.72/12.46	Apply reduction-preserving transformation...
13.72/12.46	Rules to add:
13.72/12.46	   [ +(-(1),+(?x_8,1)) -> ?x_8 ]
13.72/12.46	remove redundants rules and split
13.72/12.46	R-part:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46	     +(1,+(-(1),?x_6)) -> ?x_6,
13.72/12.46	     +(-(1),+(?x_8,1)) -> ?x_8 ]
13.72/12.46	E-part:
13.72/12.46	   [ +(?x,?y) -> +(?y,?x),
13.72/12.46	     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46	Perform abstraction and check...
13.72/12.46	Increase tree depth and check...
13.72/12.46	Apply reduction-preserving transformation...
13.72/12.46	Rules to add:
13.72/12.46	   [ +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ]
13.72/12.46	remove redundants rules and split
13.72/12.46	R-part:
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(1,+(?x_6,-(1))) -> ?x_6,
13.72/12.46	     +(1,+(-(1),?x_6)) -> ?x_6,
13.72/12.46	     +(-(1),+(?x_8,1)) -> ?x_8,
13.72/12.46	     +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ]
13.72/12.46	E-part:
13.72/12.46	   [ +(?x,?y) -> +(?y,?x),
13.72/12.46	     +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ]
13.72/12.46	Perform abstraction and check...
13.72/12.46	Increase tree depth and check...
13.72/12.46	unknown Confluence by Ordered Rewriting
13.72/12.46	Direct Methods: Can't judge
13.72/12.46	
13.72/12.46	Try Persistent Decomposition for...
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Sort Assignment:
13.72/12.46	 + : 18*18=>18
13.72/12.46	 - : 18=>18
13.72/12.46	 0 : =>18
13.72/12.46	 1 : =>18
13.72/12.46	maximal types: {18}
13.72/12.46	Persistent Decomposition failed: Can't judge
13.72/12.46	
13.72/12.46	Try Layer Preserving Decomposition for...
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Layer Preserving Decomposition failed: Can't judge
13.72/12.46	
13.72/12.46	Try Commutative Decomposition for...
13.72/12.46	   [ +(0,?x) -> ?x,
13.72/12.46	     +(?x,0) -> ?x,
13.72/12.46	     +(1,-(1)) -> 0,
13.72/12.46	     +(-(1),1) -> 0,
13.72/12.46	     -(0) -> 0,
13.72/12.46	     -(-(?x)) -> ?x,
13.72/12.46	     -(+(?x,?y)) -> +(-(?x),-(?y)),
13.72/12.46	     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
13.72/12.46	     +(?x,?y) -> +(?y,?x) ]
13.72/12.46	Outside Critical Pair: <0, 0> by Rules <1, 0>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{}, 0>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, 0>
13.72/12.46	Outside Critical Pair: <+(?y_5,0), ?y_5> by Rules <8, 0>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(0,?y_5)>
13.72/12.46	<{1}, ?y_5>
13.72/12.46	<{}, +(?y_5,0)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, ?y_5>
13.72/12.46	Outside Critical Pair: <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(+(0,?y_4),?x_4)>
13.72/12.46	<{1,8}, +(?y_4,?x_4)>
13.72/12.46	<{8}, +(+(?y_4,0),?x_4)>
13.72/12.46	<{8}, +(?x_4,+(0,?y_4))>
13.72/12.46	<{1}, +(?x_4,?y_4)>
13.72/12.46	<{}, +(?x_4,+(?y_4,0))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(?y_4,?x_4)>
13.72/12.46	<{}, +(?x_4,?y_4)>
13.72/12.46	Outside Critical Pair: <+(0,?x_5), ?x_5> by Rules <8, 1>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?x_5,0)>
13.72/12.46	<{0}, ?x_5>
13.72/12.46	<{}, +(0,?x_5)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, ?x_5>
13.72/12.46	Outside Critical Pair: <+(-(1),1), 0> by Rules <8, 2>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(1,-(1))>
13.72/12.46	<{3}, 0>
13.72/12.46	<{}, +(-(1),1)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, 0>
13.72/12.46	Outside Critical Pair: <+(1,-(1)), 0> by Rules <8, 3>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(-(1),1)>
13.72/12.46	<{2}, 0>
13.72/12.46	<{}, +(1,-(1))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, 0>
13.72/12.46	Outside Critical Pair: <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(+(?y_4,?x_4),?y_5)>
13.72/12.46	<{8}, +(+(?x_4,?y_4),?y_5)>
13.72/12.46	<{8}, +(?y_5,+(?y_4,?x_4))>
13.72/12.46	<{}, +(?y_5,+(?x_4,?y_4))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?y_5,?y_4),?x_4)>
13.72/12.46	<{8}, +(+(?y_4,?y_5),?x_4)>
13.72/12.46	<{8}, +(?x_4,+(?y_5,?y_4))>
13.72/12.46	<{}, +(?x_4,+(?y_4,?y_5))>
13.72/12.46	Inside Critical Pair: <-(0), 0> by Rules <4, 5>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{4}, 0>
13.72/12.46	<{}, -(0)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{}, 0>
13.72/12.46	Inside Critical Pair: <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{6}, +(-(-(?x_3)),-(-(?y_3)))>
13.72/12.46	<{8}, -(+(-(?y_3),-(?x_3)))>
13.72/12.46	<{}, -(+(-(?x_3),-(?y_3)))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(?y_3,?x_3)>
13.72/12.46	<{}, +(?x_3,?y_3)>
13.72/12.46	Inside Critical Pair: <-(?x), +(-(0),-(?x))> by Rules <0, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{}, -(?x)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{4,8}, +(-(?x),0)>
13.72/12.46	<{8}, +(-(?x),-(0))>
13.72/12.46	<{4}, +(0,-(?x))>
13.72/12.46	<{}, +(-(0),-(?x))>
13.72/12.46	Inside Critical Pair: <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{}, -(?x_1)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{4,8}, +(0,-(?x_1))>
13.72/12.46	<{8}, +(-(0),-(?x_1))>
13.72/12.46	<{4}, +(-(?x_1),0)>
13.72/12.46	<{}, +(-(?x_1),-(0))>
13.72/12.46	Inside Critical Pair: <-(0), +(-(1),-(-(1)))> by Rules <2, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{4}, 0>
13.72/12.46	<{}, -(0)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{5,8}, +(1,-(1))>
13.72/12.46	<{8}, +(-(-(1)),-(1))>
13.72/12.46	<{5}, +(-(1),1)>
13.72/12.46	<{}, +(-(1),-(-(1)))>
13.72/12.46	Inside Critical Pair: <-(0), +(-(-(1)),-(1))> by Rules <3, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{4}, 0>
13.72/12.46	<{}, -(0)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{5,8}, +(-(1),1)>
13.72/12.46	<{8}, +(-(1),-(-(1)))>
13.72/12.46	<{5}, +(1,-(1))>
13.72/12.46	<{}, +(-(-(1)),-(1))>
13.72/12.46	Inside Critical Pair: <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{6,8}, +(-(?x_4),-(+(?z_4,?y_4)))>
13.72/12.46	<{6}, +(-(?x_4),-(+(?y_4,?z_4)))>
13.72/12.46	<{8}, -(+(+(?z_4,?y_4),?x_4))>
13.72/12.46	<{8}, -(+(+(?y_4,?z_4),?x_4))>
13.72/12.46	<{8}, -(+(?x_4,+(?z_4,?y_4)))>
13.72/12.46	<{}, -(+(?x_4,+(?y_4,?z_4)))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{6,8}, +(-(?z_4),+(-(?x_4),-(?y_4)))>
13.72/12.46	<{8}, +(-(?z_4),-(+(?y_4,?x_4)))>
13.72/12.46	<{8}, +(-(?z_4),-(+(?x_4,?y_4)))>
13.72/12.46	<{6}, +(+(-(?x_4),-(?y_4)),-(?z_4))>
13.72/12.46	<{8}, +(-(+(?y_4,?x_4)),-(?z_4))>
13.72/12.46	<{}, +(-(+(?x_4,?y_4)),-(?z_4))>
13.72/12.46	Inside Critical Pair: <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{6}, +(-(?y_5),-(?x_5))>
13.72/12.46	<{8}, -(+(?x_5,?y_5))>
13.72/12.46	<{}, -(+(?y_5,?x_5))>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(-(?y_5),-(?x_5))>
13.72/12.46	<{}, +(-(?x_5),-(?y_5))>
13.72/12.46	Inside Critical Pair: <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?z_4,?x)>
13.72/12.46	<{}, +(?x,?z_4)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?z_4,?x),0)>
13.72/12.46	<{8}, +(+(?x,?z_4),0)>
13.72/12.46	<{0,8}, +(?z_4,?x)>
13.72/12.46	<{0}, +(?x,?z_4)>
13.72/12.46	<{8}, +(0,+(?z_4,?x))>
13.72/12.46	<{}, +(0,+(?x,?z_4))>
13.72/12.46	Inside Critical Pair: <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?z_4,?x_1)>
13.72/12.46	<{}, +(?x_1,?z_4)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?z_4,0),?x_1)>
13.72/12.46	<{0,8}, +(?z_4,?x_1)>
13.72/12.46	<{8}, +(+(0,?z_4),?x_1)>
13.72/12.46	<{8}, +(?x_1,+(?z_4,0))>
13.72/12.46	<{0}, +(?x_1,?z_4)>
13.72/12.46	<{}, +(?x_1,+(0,?z_4))>
13.72/12.46	Inside Critical Pair: <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?z_4,0)>
13.72/12.46	<{0}, ?z_4>
13.72/12.46	<{}, +(0,?z_4)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?z_4,-(1)),1)>
13.72/12.46	<{8}, +(+(-(1),?z_4),1)>
13.72/12.46	<{8}, +(1,+(?z_4,-(1)))>
13.72/12.46	<{}, +(1,+(-(1),?z_4))>
13.72/12.46	Inside Critical Pair: <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?z_4,0)>
13.72/12.46	<{0}, ?z_4>
13.72/12.46	<{}, +(0,?z_4)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?z_4,1),-(1))>
13.72/12.46	<{8}, +(+(1,?z_4),-(1))>
13.72/12.46	<{8}, +(-(1),+(?z_4,1))>
13.72/12.46	<{}, +(-(1),+(1,?z_4))>
13.72/12.46	Inside Critical Pair: <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7>
13.72/12.46	develop reducts from lhs term...
13.72/12.46	<{8}, +(?z_4,+(?x_5,?y_5))>
13.72/12.46	<{8}, +(?z_4,+(?y_5,?x_5))>
13.72/12.46	<{7}, +(?y_5,+(?x_5,?z_4))>
13.72/12.46	<{8}, +(+(?x_5,?y_5),?z_4)>
13.72/12.46	<{}, +(+(?y_5,?x_5),?z_4)>
13.72/12.46	develop reducts from rhs term...
13.72/12.46	<{8}, +(+(?z_4,?y_5),?x_5)>
13.72/12.46	<{8}, +(+(?y_5,?z_4),?x_5)>
13.72/12.46	<{8}, +(?x_5,+(?z_4,?y_5))>
13.72/12.46	<{}, +(?x_5,+(?y_5,?z_4))>
13.72/12.46	Commutative Decomposition failed: Can't judge
13.72/12.46	No further decomposition possible
13.72/12.46	
13.72/12.46	
13.72/12.46	Combined result: Can't judge
13.72/12.46	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
13.72/12.46	(5152 msec.)
13.72/12.46	EOF