0.00/0.04	MAYBE
0.00/0.04	(ignored inputs)COMMENT doi: 10.1007/3-540-54317-1_99 [58] Example 1.1 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> c | b == c ]
0.00/0.04	Check whether all rules are type 3
0.00/0.04	OK
0.00/0.04	Check whether the input is deterministic
0.00/0.04	OK
0.00/0.04	Result of unraveling:
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	Check whether U(R) is terminating
0.00/0.04	failed to show termination
0.00/0.04	Check whether the input is weakly left-linear
0.00/0.04	OK
0.00/0.04	Conditional critical pairs (CCPs):
0.00/0.04	   [ c = b,
0.00/0.04	     b = c ]
0.00/0.04	Check whether the input is almost orthogonale
0.00/0.04	not almost orthogonal
0.00/0.04	OK
0.00/0.04	Check U(R) is confluent
0.00/0.04	Rewrite Rules:
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [  ]
0.00/0.04	Outer CPs:
0.00/0.04	   [ b = c ]
0.00/0.04	Overlay, check Innermost Termination...
0.00/0.04	unknown Innermost Terminating
0.00/0.04	unknown Knuth & Bendix
0.00/0.04	Linear
0.00/0.04	unknown Development Closed
0.00/0.04	unknown Strongly Closed
0.00/0.04	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.04	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.04	(inner) Parallel CPs: (not computed)
0.00/0.04	unknown Toyama (Parallel CPs)
0.00/0.04	Simultaneous CPs:
0.00/0.04	   [ c = b,
0.00/0.04	     b = c ]
0.00/0.04	unknown Okui (Simultaneous CPs)
0.00/0.04	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.04	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.04	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.04	Critical Pair <c, b> by Rules <1, 0> preceded by []
0.00/0.04	unknown Diagram Decreasing
0.00/0.04	unknown Huet (modulo AC)
0.00/0.04	check by Reduction-Preserving Completion...
0.00/0.04	failure(empty P)
0.00/0.04	unknown Reduction-Preserving Completion
0.00/0.04	check by Ordered Rewriting...
0.00/0.04	remove redundants rules and split
0.00/0.04	R-part:
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	E-part:
0.00/0.04	   [ ]
0.00/0.04	...failed to find a suitable LPO.
0.00/0.04	unknown Confluence by Ordered Rewriting
0.00/0.04	Direct Methods: Can't judge
0.00/0.04	
0.00/0.04	Try Persistent Decomposition for...
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>6
0.00/0.04	 b : =>6
0.00/0.04	 c : =>6
0.00/0.04	 U0 : 6=>6
0.00/0.04	maximal types: {6}
0.00/0.04	Persistent Decomposition failed: Can't judge
0.00/0.04	
0.00/0.04	Try Layer Preserving Decomposition for...
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	Layer Preserving Decomposition failed: Can't judge
0.00/0.04	
0.00/0.04	Try Commutative Decomposition for...
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c,
0.00/0.04	     b -> U0(b),
0.00/0.04	     U0(c) -> c ]
0.00/0.04	Outside Critical Pair: <c, b> by Rules <1, 0>
0.00/0.04	develop reducts from lhs term...
0.00/0.04	<{}, c>
0.00/0.04	develop reducts from rhs term...
0.00/0.04	<{2}, U0(b)>
0.00/0.04	<{}, b>
0.00/0.04	Try A Minimal Decomposition {0,1}{2}{3}
0.00/0.04	{0,1}
0.00/0.04	(cm)Rewrite Rules:
0.00/0.04	   [ a -> b,
0.00/0.04	     a -> c ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [  ]
0.00/0.04	Outer CPs:
0.00/0.04	   [ b = c ]
0.00/0.04	Overlay, check Innermost Termination...
0.00/0.04	Innermost Terminating (hence Terminating), not WCR
0.00/0.04	Knuth & Bendix
0.00/0.04	Direct Methods: not CR
0.00/0.04	{2}
0.00/0.04	(cm)Rewrite Rules:
0.00/0.04	   [ b -> U0(b) ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [  ]
0.00/0.04	Outer CPs:
0.00/0.04	   [  ]
0.00/0.04	Overlay, check Innermost Termination...
0.00/0.04	unknown Innermost Terminating
0.00/0.04	unknown Knuth & Bendix
0.00/0.04	Linear
0.00/0.04	Development Closed
0.00/0.04	Direct Methods: CR
0.00/0.04	{3}
0.00/0.04	(cm)Rewrite Rules:
0.00/0.04	   [ U0(c) -> c ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [  ]
0.00/0.04	Outer CPs:
0.00/0.04	   [  ]
0.00/0.04	Overlay, check Innermost Termination...
0.00/0.04	Innermost Terminating (hence Terminating), WCR
0.00/0.04	Knuth & Bendix
0.00/0.04	Direct Methods: CR
0.00/0.04	Commutative Decomposition failed: Can't judge
0.00/0.04	No further decomposition possible
0.00/0.04	
0.00/0.04	
0.00/0.04	Combined result: Can't judge
0.00/0.04	failed to show confluence of U(R)
0.00/0.04	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.04	(7 msec.)
0.00/0.04	EOF