0.00/0.34	MAYBE
0.00/0.34	(ignored inputs)COMMENT doi:10.1016/j.jlap.2009.08.001 [73] Example 9 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.34	Conditional Rewrite Rules:
0.00/0.34	   [ div(?x,?y) -> pair(0,?y) | greater(?y,?x) == true,
0.00/0.34	     div(?x,?y) -> pair(s(?q),?r) | leq(?y,?x) == true,div(m(?x,?y),?y) == pair(?q,?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Check whether all rules are type 3
0.00/0.34	OK
0.00/0.34	Check whether the input is deterministic
0.00/0.34	OK
0.00/0.34	Result of unraveling:
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Check whether U(R) is terminating
0.00/0.34	failed to show termination
0.00/0.34	Check whether the input is weakly left-linear
0.00/0.34	OK
0.00/0.34	Conditional critical pairs (CCPs):
0.00/0.34	   [ pair(s(?q_1),?r_1) = pair(0,?y_1) | leq(?y_1,?x_1) == true,div(m(?x_1,?y_1),?y_1) == pair(?q_1,?r_1),greater(?y_1,?x_1) == true,
0.00/0.34	     pair(0,?y) = pair(s(?q_1),?r_1) | greater(?y,?x) == true,leq(?y,?x) == true,div(m(?x,?y),?y) == pair(?q_1,?r_1),
0.00/0.34	     0 = 0,
0.00/0.34	     0 = 0 ]
0.00/0.34	Check whether the input is almost orthogonale
0.00/0.34	not almost orthogonal
0.00/0.34	OK
0.00/0.34	Check U(R) is confluent
0.00/0.34	Rewrite Rules:
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [ U1(greater(?y,?x),?x,?y) = U1(leq(?y,?x),?x,?y),
0.00/0.34	     pair(0,?y_1) = U2(div(m(?x_1,?y_1),?y_1),?x_1,?y_1),
0.00/0.34	     0 = 0 ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	unknown Innermost Terminating
0.00/0.34	unknown Knuth & Bendix
0.00/0.34	Left-Linear, not Right-Linear
0.00/0.34	unknown Development Closed
0.00/0.34	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.34	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.34	(inner) Parallel CPs: (not computed)
0.00/0.34	unknown Toyama (Parallel CPs)
0.00/0.34	Simultaneous CPs:
0.00/0.34	   [ U1(leq(?y,?x),?x,?y) = U1(greater(?y,?x),?x,?y),
0.00/0.34	     U2(div(m(?x,?y),?y),?x,?y) = pair(0,?y),
0.00/0.34	     U1(greater(?y,?x),?x,?y) = U1(leq(?y,?x),?x,?y),
0.00/0.34	     pair(0,?y) = U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     0 = 0 ]
0.00/0.34	unknown Okui (Simultaneous CPs)
0.00/0.34	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.34	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.34	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.34	Critical Pair <U1(leq(?y_2,?x_2),?x_2,?y_2), U1(greater(?y_2,?x_2),?x_2,?y_2)> by Rules <2, 0> preceded by []
0.00/0.34	unknown Diagram Decreasing
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x_1,?y_1) -> pair(0,?y_1),
0.00/0.34	     div(?x_2,?y_2) -> U1(leq(?y_2,?x_2),?x_2,?y_2),
0.00/0.34	     U1(true,?x_3,?y_3) -> U2(div(m(?x_3,?y_3),?y_3),?x_3,?y_3),
0.00/0.34	     U2(pair(?q_4,?r_4),?x_4,?y_4) -> pair(s(?q_4),?r_4),
0.00/0.34	     m(?x_5,0) -> ?x_5,
0.00/0.34	     m(0,?y_6) -> 0,
0.00/0.34	     m(s(?x_7),s(?y_7)) -> m(?x_7,?y_7),
0.00/0.34	     greater(s(?x_8),s(?y_8)) -> greater(?x_8,?y_8),
0.00/0.34	     greater(s(?x_9),0) -> true,
0.00/0.34	     leq(s(?x_10),s(?y_10)) -> leq(?x_10,?y_10),
0.00/0.34	     leq(0,?x_11) -> true ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>54
0.00/0.34	 m : 54*54=>54
0.00/0.34	 s : 54=>54
0.00/0.34	 U1 : 50*54*54=>57
0.00/0.34	 U2 : 57*54*54=>57
0.00/0.34	 div : 54*54=>57
0.00/0.34	 leq : 54*54=>50
0.00/0.34	 pair : 54*54=>57
0.00/0.34	 true : =>50
0.00/0.34	 greater : 54*54=>50
0.00/0.34	non-linear variables: {?y,?x,?y_2,?x_2,?x_3,?y_3}
0.00/0.34	non-linear types: {54}
0.00/0.34	types leq non-linear types: {54}
0.00/0.34	rules applicable to terms of non-linear types:
0.00/0.34	   [ m(?x_5,0) -> ?x_5,
0.00/0.34	     m(0,?y_6) -> 0,
0.00/0.34	     m(s(?x_7),s(?y_7)) -> m(?x_7,?y_7) ]
0.00/0.34	Rnl:
0.00/0.34	0: {5,6,7}
0.00/0.34	1: {}
0.00/0.34	2: {5,6,7}
0.00/0.34	3: {5,6,7}
0.00/0.34	4: {}
0.00/0.34	5: {}
0.00/0.34	6: {}
0.00/0.34	7: {}
0.00/0.34	8: {}
0.00/0.34	9: {}
0.00/0.34	10: {}
0.00/0.34	11: {}
0.00/0.34	terms of non-linear types are innermost terminating
0.00/0.34	Critical Pair <U1(leq(?y_2,?x_2),?x_2,?y_2), U1(greater(?y_2,?x_2),?x_2,?y_2)> by Rules <2, 0>
0.00/0.34	no joinable sequence for some critical pairs
0.00/0.34	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x_1,?y_1) -> pair(0,?y_1),
0.00/0.34	     div(?x_2,?y_2) -> U1(leq(?y_2,?x_2),?x_2,?y_2),
0.00/0.34	     U1(true,?x_3,?y_3) -> U2(div(m(?x_3,?y_3),?y_3),?x_3,?y_3),
0.00/0.34	     U2(pair(?q_4,?r_4),?x_4,?y_4) -> pair(s(?q_4),?r_4),
0.00/0.34	     m(?x_5,0) -> ?x_5,
0.00/0.34	     m(0,?y_6) -> 0,
0.00/0.34	     m(s(?x_7),s(?y_7)) -> m(?x_7,?y_7),
0.00/0.34	     greater(s(?x_8),s(?y_8)) -> greater(?x_8,?y_8),
0.00/0.34	     greater(s(?x_9),0) -> true,
0.00/0.34	     leq(s(?x_10),s(?y_10)) -> leq(?x_10,?y_10),
0.00/0.34	     leq(0,?x_11) -> true ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>54
0.00/0.34	 m : 54*54=>54
0.00/0.34	 s : 54=>54
0.00/0.34	 U1 : 50*54*54=>57
0.00/0.34	 U2 : 57*54*54=>57
0.00/0.34	 div : 54*54=>57
0.00/0.34	 leq : 54*54=>50
0.00/0.34	 pair : 54*54=>57
0.00/0.34	 true : =>50
0.00/0.34	 greater : 54*54=>50
0.00/0.34	non-linear variables: {?y,?x,?y_2,?x_2,?x_3,?y_3}
0.00/0.34	non-linear types: {54}
0.00/0.34	types leq non-linear types: {54}
0.00/0.34	rules applicable to terms of non-linear types:
0.00/0.34	   [ m(?x_5,0) -> ?x_5,
0.00/0.34	     m(0,?y_6) -> 0,
0.00/0.34	     m(s(?x_7),s(?y_7)) -> m(?x_7,?y_7) ]
0.00/0.34	terms of non-linear types are terminating
0.00/0.34	Check Joinablility of CP from NLR:
0.00/0.34	Critical Pair <0, 0> by Rules <6, 5>
0.00/0.34	done.
0.00/0.34	Critical Pair <U1(leq(?y_2,?x_2),?x_2,?y_2), U1(greater(?y_2,?x_2),?x_2,?y_2)> by Rules <2, 0>
0.00/0.34	no joinable sequence for some critical pairs
0.00/0.34	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.34	unknown Huet (modulo AC)
0.00/0.34	check by Reduction-Preserving Completion...
0.00/0.34	failure(empty P)
0.00/0.34	unknown Reduction-Preserving Completion
0.00/0.34	check by Ordered Rewriting...
0.00/0.34	remove redundants rules and split
0.00/0.34	R-part:
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	E-part:
0.00/0.34	   [ ]
0.00/0.34	...failed to find a suitable LPO.
0.00/0.34	unknown Confluence by Ordered Rewriting
0.00/0.34	Direct Methods: Can't judge
0.00/0.34	
0.00/0.34	Try Persistent Decomposition for...
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>54
0.00/0.34	 m : 54*54=>54
0.00/0.34	 s : 54=>54
0.00/0.34	 U1 : 50*54*54=>57
0.00/0.34	 U2 : 57*54*54=>57
0.00/0.34	 div : 54*54=>57
0.00/0.34	 leq : 54*54=>50
0.00/0.34	 pair : 54*54=>57
0.00/0.34	 true : =>50
0.00/0.34	 greater : 54*54=>50
0.00/0.34	maximal types: {50,54,57}
0.00/0.34	Persistent Decomposition failed: Can't judge
0.00/0.34	
0.00/0.34	Try Layer Preserving Decomposition for...
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Layer Preserving Decomposition failed: Can't judge
0.00/0.34	
0.00/0.34	Try Commutative Decomposition for...
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y),
0.00/0.34	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r),
0.00/0.34	     m(?x,0) -> ?x,
0.00/0.34	     m(0,?y) -> 0,
0.00/0.34	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.34	     greater(s(?x),s(?y)) -> greater(?x,?y),
0.00/0.34	     greater(s(?x),0) -> true,
0.00/0.34	     leq(s(?x),s(?y)) -> leq(?x,?y),
0.00/0.34	     leq(0,?x) -> true ]
0.00/0.34	Outside Critical Pair: <U1(leq(?y_2,?x_2),?x_2,?y_2), U1(greater(?y_2,?x_2),?x_2,?y_2)> by Rules <2, 0>
0.00/0.34	develop reducts from lhs term...
0.00/0.34	<{}, U1(leq(?y_2,?x_2),?x_2,?y_2)>
0.00/0.34	develop reducts from rhs term...
0.00/0.34	<{}, U1(greater(?y_2,?x_2),?x_2,?y_2)>
0.00/0.34	Outside Critical Pair: <U2(div(m(?x_3,?y_3),?y_3),?x_3,?y_3), pair(0,?y_3)> by Rules <3, 1>
0.00/0.34	develop reducts from lhs term...
0.00/0.34	<{2}, U2(U1(leq(?y_3,m(?x_3,?y_3)),m(?x_3,?y_3),?y_3),?x_3,?y_3)>
0.00/0.34	<{0}, U2(U1(greater(?y_3,m(?x_3,?y_3)),m(?x_3,?y_3),?y_3),?x_3,?y_3)>
0.00/0.34	<{}, U2(div(m(?x_3,?y_3),?y_3),?x_3,?y_3)>
0.00/0.34	develop reducts from rhs term...
0.00/0.34	<{}, pair(0,?y_3)>
0.00/0.34	Outside Critical Pair: <0, 0> by Rules <6, 5>
0.00/0.34	develop reducts from lhs term...
0.00/0.34	<{}, 0>
0.00/0.34	develop reducts from rhs term...
0.00/0.34	<{}, 0>
0.00/0.34	Try A Minimal Decomposition {0,2}{1,3}{4}{5}{6}{7}{8}{9}{10}{11}
0.00/0.34	{0,2}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ div(?x,?y) -> U1(greater(?y,?x),?x,?y),
0.00/0.34	     div(?x,?y) -> U1(leq(?y,?x),?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [ U1(greater(?y,?x),?x,?y) = U1(leq(?y,?x),?x,?y) ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), not WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: not CR
0.00/0.34	{1,3}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ U1(true,?x,?y) -> pair(0,?y),
0.00/0.34	     U1(true,?x,?y) -> U2(div(m(?x,?y),?y),?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [ pair(0,?y) = U2(div(m(?x,?y),?y),?x,?y) ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), not WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: not CR
0.00/0.34	{4}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{5}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ m(?x,0) -> ?x ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{6}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ m(0,?y) -> 0 ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{7}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ m(s(?x),s(?y)) -> m(?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{8}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ greater(s(?x),s(?y)) -> greater(?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{9}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ greater(s(?x),0) -> true ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{10}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ leq(s(?x),s(?y)) -> leq(?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{11}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ leq(0,?x) -> true ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	Commutative Decomposition failed: Can't judge
0.00/0.34	No further decomposition possible
0.00/0.34	
0.00/0.34	
0.00/0.34	Combined result: Can't judge
0.00/0.34	failed to show confluence of U(R)
0.00/0.34	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.34	(221 msec.)
0.00/0.34	EOF