0.00/0.25	MAYBE
0.00/0.25	(ignored inputs)COMMENT submitted by: Nao Hirokawa
0.00/0.25	Conditional Rewrite Rules:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> 0 | ?x == 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Check whether all rules are type 3
0.00/0.25	OK
0.00/0.25	Check whether the input is deterministic
0.00/0.25	OK
0.00/0.25	Result of unraveling:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Check whether U(R) is terminating
0.00/0.25	failed to show termination
0.00/0.25	Check whether the input is weakly left-linear
0.00/0.25	OK
0.00/0.25	Conditional critical pairs (CCPs):
0.00/0.25	   [ 0 = 0 | 0 == 0,
0.00/0.25	     +(?y_2,0) = ?y_2,
0.00/0.25	     0 = 0 | 0 == 0,
0.00/0.25	     +(0,?x_2) = 0 | ?x_2 == 0,
0.00/0.25	     ?x = +(?x,0),
0.00/0.25	     0 = +(0,?x_1) | ?x_1 == 0 ]
0.00/0.25	Check whether the input is almost orthogonale
0.00/0.25	not almost orthogonal
0.00/0.25	OK
0.00/0.25	Check U(R) is confluent
0.00/0.25	Rewrite Rules:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Apply Direct Methods...
0.00/0.25	Inner CPs:
0.00/0.25	   [  ]
0.00/0.25	Outer CPs:
0.00/0.25	   [ 0 = U0(0,0),
0.00/0.25	     ?x = +(?x,0),
0.00/0.25	     U0(?x_1,?x_1) = +(0,?x_1) ]
0.00/0.25	Overlay, check Innermost Termination...
0.00/0.25	unknown Innermost Terminating
0.00/0.25	unknown Knuth & Bendix
0.00/0.25	Left-Linear, not Right-Linear
0.00/0.25	unknown Development Closed
0.00/0.25	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.25	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.25	(inner) Parallel CPs: (not computed)
0.00/0.25	unknown Toyama (Parallel CPs)
0.00/0.25	Simultaneous CPs:
0.00/0.25	   [ U0(0,0) = 0,
0.00/0.25	     +(?x,0) = ?x,
0.00/0.25	     0 = U0(0,0),
0.00/0.25	     +(0,?x) = U0(?x,?x),
0.00/0.25	     ?y = +(?y,0),
0.00/0.25	     U0(?x,?x) = +(0,?x) ]
0.00/0.25	unknown Okui (Simultaneous CPs)
0.00/0.25	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.25	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.25	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.25	Critical Pair <U0(0,0), 0> by Rules <1, 0> preceded by []
0.00/0.25	 joinable by a reduction of rules <[([],2)], []>
0.00/0.25	Critical Pair <+(?y_3,0), ?y_3> by Rules <3, 0> preceded by []
0.00/0.25	 joinable by a reduction of rules <[([],3),([],0)], []>
0.00/0.25	Critical Pair <+(0,?x_3), U0(?x_3,?x_3)> by Rules <3, 1> preceded by []
0.00/0.25	 joinable by a reduction of rules <[([],3),([],1)], []>
0.00/0.25	unknown Diagram Decreasing
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x_1,0) -> U0(?x_1,?x_1),
0.00/0.25	     U0(0,?x_2) -> 0,
0.00/0.25	     +(?x_3,?y_3) -> +(?y_3,?x_3) ]
0.00/0.25	Sort Assignment:
0.00/0.25	 + : 13*13=>13
0.00/0.25	 0 : =>13
0.00/0.25	 U0 : 13*13=>13
0.00/0.25	non-linear variables: {?x_1}
0.00/0.25	non-linear types: {13}
0.00/0.25	types leq non-linear types: {13}
0.00/0.25	rules applicable to terms of non-linear types:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x_1,0) -> U0(?x_1,?x_1),
0.00/0.25	     U0(0,?x_2) -> 0,
0.00/0.25	     +(?x_3,?y_3) -> +(?y_3,?x_3) ]
0.00/0.25	Rnl:
0.00/0.25	0: {}
0.00/0.25	1: {0,1,2,3}
0.00/0.25	2: {}
0.00/0.25	3: {}
0.00/0.25	unknown innermost-termination for terms of non-linear types
0.00/0.25	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x_1,0) -> U0(?x_1,?x_1),
0.00/0.25	     U0(0,?x_2) -> 0,
0.00/0.25	     +(?x_3,?y_3) -> +(?y_3,?x_3) ]
0.00/0.25	Sort Assignment:
0.00/0.25	 + : 13*13=>13
0.00/0.25	 0 : =>13
0.00/0.25	 U0 : 13*13=>13
0.00/0.25	non-linear variables: {?x_1}
0.00/0.25	non-linear types: {13}
0.00/0.25	types leq non-linear types: {13}
0.00/0.25	rules applicable to terms of non-linear types:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x_1,0) -> U0(?x_1,?x_1),
0.00/0.25	     U0(0,?x_2) -> 0,
0.00/0.25	     +(?x_3,?y_3) -> +(?y_3,?x_3) ]
0.00/0.25	unknown innermost-termination for terms of non-linear types
0.00/0.25	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.25	Check relative termination:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Polynomial Interpretation:
0.00/0.25	  +:= (12)+(12)*x1+(12)*x1*x1+(12)*x2+(12)*x2*x2
0.00/0.25	  0:= 0
0.00/0.25	  U0:= (9)*x1*x1+(1)*x1*x2+(10)*x2
0.00/0.25	retract +(0,?x) -> ?x
0.00/0.25	retract +(?x,0) -> U0(?x,?x)
0.00/0.25	Polynomial Interpretation:
0.00/0.25	  +:= (5)+(8)*x1*x1+(8)*x2*x2
0.00/0.25	  0:= 0
0.00/0.25	  U0:= (4)+(8)*x1+(1)*x1*x1+(3)*x1*x2+(2)*x2
0.00/0.25	relatively terminating
0.00/0.25	unknown Huet (modulo AC)
0.00/0.25	check by Reduction-Preserving Completion...
0.00/0.25	STEP: 1 (parallel)
0.00/0.25	S:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	P:
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	S: terminating
0.00/0.25	CP(S,S):
0.00/0.25	<U0(0,0), 0> --> <0, 0> => yes
0.00/0.25	<0, U0(0,0)> --> <0, 0> => yes
0.00/0.25	PCP_in(symP,S):
0.00/0.25	CP(S,symP):
0.00/0.25	<?x, +(?x,0)> --> <?x, U0(?x,?x)> => no
0.00/0.25	<U0(?x,?x), +(0,?x)> --> <U0(?x,?x), ?x> => no
0.00/0.25	check joinability condition:
0.00/0.25	check modulo joinability of ?x and U0(?x,?x): maybe not joinable
0.00/0.25	check modulo joinability of U0(?x,?x) and ?x: maybe not joinable
0.00/0.25	failed
0.00/0.25	failure(Step 1)
0.00/0.25	   [ ]
0.00/0.25	Added S-Rules:
0.00/0.25	   [ ]
0.00/0.25	Added P-Rules:
0.00/0.25	   [ ]
0.00/0.25	STEP: 2 (linear)
0.00/0.25	S:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	P:
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	S: not linear
0.00/0.25	failure(Step 2)
0.00/0.25	STEP: 3 (relative)
0.00/0.25	S:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	P:
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Check relative termination:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Polynomial Interpretation:
0.00/0.25	  +:= (12)+(12)*x1+(12)*x1*x1+(12)*x2+(12)*x2*x2
0.00/0.25	  0:= 0
0.00/0.25	  U0:= (9)*x1*x1+(1)*x1*x2+(10)*x2
0.00/0.25	retract +(0,?x) -> ?x
0.00/0.25	retract +(?x,0) -> U0(?x,?x)
0.00/0.25	Polynomial Interpretation:
0.00/0.25	  +:= (5)+(8)*x1*x1+(8)*x2*x2
0.00/0.25	  0:= 0
0.00/0.25	  U0:= (4)+(8)*x1+(1)*x1*x1+(3)*x1*x2+(2)*x2
0.00/0.25	relatively terminating
0.00/0.25	S/P: relatively terminating
0.00/0.25	check CP condition:
0.00/0.25	failed
0.00/0.25	failure(Step 3)
0.00/0.25	failure(no possibility remains)
0.00/0.25	unknown Reduction-Preserving Completion
0.00/0.25	check by Ordered Rewriting...
0.00/0.25	remove redundants rules and split
0.00/0.25	R-part:
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0 ]
0.00/0.25	E-part:
0.00/0.25	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Perform abstraction and check...
0.00/0.25	Increase tree depth and check...
0.00/0.25	unknown Confluence by Ordered Rewriting
0.00/0.25	Direct Methods: Can't judge
0.00/0.25	
0.00/0.25	Try Persistent Decomposition for...
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Sort Assignment:
0.00/0.25	 + : 13*13=>13
0.00/0.25	 0 : =>13
0.00/0.25	 U0 : 13*13=>13
0.00/0.25	maximal types: {13}
0.00/0.25	Persistent Decomposition failed: Can't judge
0.00/0.25	
0.00/0.25	Try Layer Preserving Decomposition for...
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Layer Preserving Decomposition failed: Can't judge
0.00/0.25	
0.00/0.25	Try Commutative Decomposition for...
0.00/0.25	   [ +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x),
0.00/0.25	     U0(0,?x) -> 0,
0.00/0.25	     +(?x,?y) -> +(?y,?x) ]
0.00/0.25	Outside Critical Pair: <U0(0,0), 0> by Rules <1, 0>
0.00/0.25	develop reducts from lhs term...
0.00/0.25	<{2}, 0>
0.00/0.25	<{}, U0(0,0)>
0.00/0.25	develop reducts from rhs term...
0.00/0.25	<{}, 0>
0.00/0.25	Outside Critical Pair: <+(?y_3,0), ?y_3> by Rules <3, 0>
0.00/0.25	develop reducts from lhs term...
0.00/0.25	<{3}, +(0,?y_3)>
0.00/0.25	<{1}, U0(?y_3,?y_3)>
0.00/0.25	<{}, +(?y_3,0)>
0.00/0.25	develop reducts from rhs term...
0.00/0.25	<{}, ?y_3>
0.00/0.25	Outside Critical Pair: <+(0,?x_3), U0(?x_3,?x_3)> by Rules <3, 1>
0.00/0.25	develop reducts from lhs term...
0.00/0.25	<{3}, +(?x_3,0)>
0.00/0.25	<{0}, ?x_3>
0.00/0.25	<{}, +(0,?x_3)>
0.00/0.25	develop reducts from rhs term...
0.00/0.25	<{}, U0(?x_3,?x_3)>
0.00/0.25	Try A Minimal Decomposition {3,0,1}{2}
0.00/0.25	{3,0,1}
0.00/0.25	(cm)Rewrite Rules:
0.00/0.25	   [ +(?x,?y) -> +(?y,?x),
0.00/0.25	     +(0,?x) -> ?x,
0.00/0.25	     +(?x,0) -> U0(?x,?x) ]
0.00/0.25	Apply Direct Methods...
0.00/0.25	Inner CPs:
0.00/0.25	   [  ]
0.00/0.25	Outer CPs:
0.00/0.25	   [ +(?y,0) = ?y,
0.00/0.25	     +(0,?x) = U0(?x,?x),
0.00/0.25	     0 = U0(0,0) ]
0.00/0.25	Overlay, check Innermost Termination...
0.00/0.25	unknown Innermost Terminating
0.00/0.25	unknown Knuth & Bendix
0.00/0.25	Left-Linear, not Right-Linear
0.00/0.25	unknown Development Closed
0.00/0.25	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.25	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.25	(inner) Parallel CPs: (not computed)
0.00/0.25	unknown Toyama (Parallel CPs)
0.00/0.25	Simultaneous CPs:
0.00/0.25	   [ ?y = +(?y,0),
0.00/0.25	     U0(?x,?x) = +(0,?x),
0.00/0.25	     +(?x,0) = ?x,
0.00/0.25	     U0(0,0) = 0,
0.00/0.25	     +(0,?x) = U0(?x,?x),
0.00/0.25	     0 = U0(0,0) ]
0.00/0.26	unknown Okui (Simultaneous CPs)
0.00/0.26	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.26	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.26	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.26	Critical Pair <?x_1, +(?x_1,0)> by Rules <1, 0> preceded by []
0.00/0.26	 joinable by a reduction of rules <[], [([],0),([],1)]>
0.00/0.26	Critical Pair <U0(?x_2,?x_2), +(0,?x_2)> by Rules <2, 0> preceded by []
0.00/0.26	 joinable by a reduction of rules <[], [([],0),([],2)]>
0.00/0.26	Critical Pair <U0(0,0), 0> by Rules <2, 1> preceded by []
0.00/0.26	unknown Diagram Decreasing
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x_1) -> ?x_1,
0.00/0.26	     +(?x_2,0) -> U0(?x_2,?x_2) ]
0.00/0.26	Sort Assignment:
0.00/0.26	 + : 10*10=>10
0.00/0.26	 0 : =>10
0.00/0.26	 U0 : 10*10=>10
0.00/0.26	non-linear variables: {?x_2}
0.00/0.26	non-linear types: {10}
0.00/0.26	types leq non-linear types: {10}
0.00/0.26	rules applicable to terms of non-linear types:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x_1) -> ?x_1,
0.00/0.26	     +(?x_2,0) -> U0(?x_2,?x_2) ]
0.00/0.26	Rnl:
0.00/0.26	0: {}
0.00/0.26	1: {}
0.00/0.26	2: {0,1,2}
0.00/0.26	unknown innermost-termination for terms of non-linear types
0.00/0.26	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x_1) -> ?x_1,
0.00/0.26	     +(?x_2,0) -> U0(?x_2,?x_2) ]
0.00/0.26	Sort Assignment:
0.00/0.26	 + : 10*10=>10
0.00/0.26	 0 : =>10
0.00/0.26	 U0 : 10*10=>10
0.00/0.26	non-linear variables: {?x_2}
0.00/0.26	non-linear types: {10}
0.00/0.26	types leq non-linear types: {10}
0.00/0.26	rules applicable to terms of non-linear types:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x_1) -> ?x_1,
0.00/0.26	     +(?x_2,0) -> U0(?x_2,?x_2) ]
0.00/0.26	unknown innermost-termination for terms of non-linear types
0.00/0.26	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.26	Check relative termination:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	Polynomial Interpretation:
0.00/0.26	  +:= (15)+(9)*x1+(8)*x1*x1+(9)*x2+(8)*x2*x2
0.00/0.26	  0:= 0
0.00/0.26	  U0:= (8)*x1+(1)*x2+(4)*x2*x2
0.00/0.26	relatively terminating
0.00/0.26	unknown Huet (modulo AC)
0.00/0.26	check by Reduction-Preserving Completion...
0.00/0.26	STEP: 1 (parallel)
0.00/0.26	S:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	P:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	S: terminating
0.00/0.26	CP(S,S):
0.00/0.26	<U0(0,0), 0> --> <U0(0,0), 0> => no
0.00/0.26	<0, U0(0,0)> --> <0, U0(0,0)> => no
0.00/0.26	PCP_in(symP,S):
0.00/0.26	CP(S,symP):
0.00/0.26	<?x, +(?x,0)> --> <?x, U0(?x,?x)> => no
0.00/0.26	<U0(?x,?x), +(0,?x)> --> <U0(?x,?x), ?x> => no
0.00/0.26	check joinability condition:
0.00/0.26	check modulo joinability of U0(0,0) and 0: maybe not joinable
0.00/0.26	check modulo joinability of 0 and U0(0,0): maybe not joinable
0.00/0.26	check modulo joinability of ?x and U0(?x,?x): maybe not joinable
0.00/0.26	check modulo joinability of U0(?x,?x) and ?x: maybe not joinable
0.00/0.26	failed
0.00/0.26	failure(Step 1)
0.00/0.26	   [ ]
0.00/0.26	Added S-Rules:
0.00/0.26	   [ ]
0.00/0.26	Added P-Rules:
0.00/0.26	   [ ]
0.00/0.26	STEP: 2 (linear)
0.00/0.26	S:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	P:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	S: not linear
0.00/0.26	failure(Step 2)
0.00/0.26	STEP: 3 (relative)
0.00/0.26	S:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	P:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	Check relative termination:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	Polynomial Interpretation:
0.00/0.26	  +:= (15)+(9)*x1+(8)*x1*x1+(9)*x2+(8)*x2*x2
0.00/0.26	  0:= 0
0.00/0.26	  U0:= (8)*x1+(1)*x2+(4)*x2*x2
0.00/0.26	relatively terminating
0.00/0.26	S/P: relatively terminating
0.00/0.26	check CP condition:
0.00/0.26	failed
0.00/0.26	failure(Step 3)
0.00/0.26	failure(no possibility remains)
0.00/0.26	unknown Reduction-Preserving Completion
0.00/0.26	check by Ordered Rewriting...
0.00/0.26	remove redundants rules and split
0.00/0.26	R-part:
0.00/0.26	   [ +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	E-part:
0.00/0.26	   [ +(?x,?y) -> +(?y,?x) ]
0.00/0.26	Perform abstraction and check...
0.00/0.26	Increase tree depth and check...
0.00/0.26	unknown Confluence by Ordered Rewriting
0.00/0.26	Direct Methods: Can't judge
0.00/0.26	
0.00/0.26	Try Persistent Decomposition for...
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	Sort Assignment:
0.00/0.26	 + : 10*10=>10
0.00/0.26	 0 : =>10
0.00/0.26	 U0 : 10*10=>10
0.00/0.26	maximal types: {10}
0.00/0.26	Persistent Decomposition failed: Can't judge
0.00/0.26	
0.00/0.26	Try Layer Preserving Decomposition for...
0.00/0.26	   [ +(?x,?y) -> +(?y,?x),
0.00/0.26	     +(0,?x) -> ?x,
0.00/0.26	     +(?x,0) -> U0(?x,?x) ]
0.00/0.26	Layer Preserving Decomposition failed: Can't judge
0.00/0.26	No further decomposition possible
0.00/0.26	
0.00/0.26	{2}
0.00/0.26	(cm)Rewrite Rules:
0.00/0.26	   [ U0(0,?x) -> 0 ]
0.00/0.26	Apply Direct Methods...
0.00/0.26	Inner CPs:
0.00/0.26	   [  ]
0.00/0.26	Outer CPs:
0.00/0.26	   [  ]
0.00/0.26	Overlay, check Innermost Termination...
0.00/0.26	Innermost Terminating (hence Terminating), WCR
0.00/0.26	Knuth & Bendix
0.00/0.26	Direct Methods: CR
0.00/0.26	Commutative Decomposition failed: Can't judge
0.00/0.26	No further decomposition possible
0.00/0.26	
0.00/0.26	
0.00/0.26	Combined result: Can't judge
0.00/0.26	failed to show confluence of U(R)
0.00/0.26	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.26	(53 msec.)
0.00/0.26	EOF