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