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