0.00/0.04	MAYBE
0.00/0.04	(ignored inputs)COMMENT [75] Example 14 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ f(?x) -> b | f(?x) == ?z,?x == ?z,
0.00/0.04	     a -> f(a) ]
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
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	   [  ]
0.00/0.04	Check whether the input is almost orthogonale
0.00/0.04	OK
0.00/0.04	Check whether the input is properly oriented
0.00/0.04	OK
0.00/0.04	Check whether the input is right-stable
0.00/0.04	not right-stable
0.00/0.04	OK
0.00/0.04	Check U(R) is confluent
0.00/0.04	Rewrite Rules:
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
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	not Left-Linear, not Right-Linear
0.00/0.04	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>17
0.00/0.04	 b : =>17
0.00/0.04	 f : 17=>17
0.00/0.04	 U0 : 17*17=>17
0.00/0.04	 U1 : 17*17*17=>17
0.00/0.04	non-linear variables: {?z_2}
0.00/0.04	non-linear types: {17}
0.00/0.04	types leq non-linear types: {17}
0.00/0.04	rules applicable to terms of non-linear types:
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	unknown innermost-termination for terms of non-linear types
0.00/0.04	unknown Quasi-Left-Linear & Parallel-Closed
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>17
0.00/0.04	 b : =>17
0.00/0.04	 f : 17=>17
0.00/0.04	 U0 : 17*17=>17
0.00/0.04	 U1 : 17*17*17=>17
0.00/0.04	non-linear variables: {?x,?x_1,?z_2}
0.00/0.04	non-linear types: {17}
0.00/0.04	types leq non-linear types: {17}
0.00/0.04	rules applicable to terms of non-linear types:
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Rnl:
0.00/0.04	0: {0,1,2,3}
0.00/0.04	1: {0,1,2,3}
0.00/0.04	2: {0,1,2,3}
0.00/0.04	3: {}
0.00/0.04	unknown innermost-termination for terms of non-linear types
0.00/0.04	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>17
0.00/0.04	 b : =>17
0.00/0.04	 f : 17=>17
0.00/0.04	 U0 : 17*17=>17
0.00/0.04	 U1 : 17*17*17=>17
0.00/0.04	non-linear variables: {?x,?x_1,?z_2}
0.00/0.04	non-linear types: {17}
0.00/0.04	types leq non-linear types: {17}
0.00/0.04	rules applicable to terms of non-linear types:
0.00/0.04	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z_1,?x_1) -> U1(?x_1,?x_1,?z_1),
0.00/0.04	     U1(?z_2,?x_2,?z_2) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	unknown innermost-termination for terms of non-linear types
0.00/0.04	unknown Strongly Quasi-Linear & Hierarchically Decreasing
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>17
0.00/0.04	 b : =>17
0.00/0.04	 f : 17=>17
0.00/0.04	 U0 : 17*17=>17
0.00/0.04	 U1 : 17*17*17=>17
0.00/0.04	maximal types: {17}
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
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	   [ f(?x) -> U0(f(?x),?x),
0.00/0.04	     U0(?z,?x) -> U1(?x,?x,?z),
0.00/0.04	     U1(?z,?x,?z) -> b,
0.00/0.04	     a -> f(a) ]
0.00/0.04	Commutative Decomposition failed (not left-linear): 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/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.04	(6 msec.)
0.00/0.04	EOF