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