0.00/0.04	YES
0.00/0.04	(ignored inputs)COMMENT doi:10.1007/978-3-319-08918-8_31 [46] Example 6 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ f(?x,?x) -> a,
0.00/0.04	     g(?x) -> a | g(?x) == b,
0.00/0.04	     a -> b,
0.00/0.04	     b -> 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,?x) -> a,
0.00/0.04	     g(?x) -> U0(g(?x),?x),
0.00/0.04	     U0(b,?x) -> a,
0.00/0.04	     a -> b,
0.00/0.04	     b -> 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	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	   [ f(?x,?x) -> a,
0.00/0.04	     g(?x) -> U0(g(?x),?x),
0.00/0.04	     U0(b,?x) -> a,
0.00/0.04	     a -> b,
0.00/0.04	     b -> a ]
0.00/0.04	Apply Direct Methods...
0.00/0.04	Inner CPs:
0.00/0.04	   [ U0(a,?x_2) = a ]
0.00/0.04	Outer CPs:
0.00/0.04	   [  ]
0.00/0.04	not Overlay, check Termination...
0.00/0.04	unknown/not 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,?x) -> a,
0.00/0.04	     g(?x_1) -> U0(g(?x_1),?x_1),
0.00/0.04	     U0(b,?x_2) -> a,
0.00/0.04	     a -> b,
0.00/0.04	     b -> a ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>14
0.00/0.04	 b : =>14
0.00/0.04	 f : 7*7=>14
0.00/0.04	 g : 12=>14
0.00/0.04	 U0 : 14*12=>14
0.00/0.04	non-linear variables: {?x}
0.00/0.04	non-linear types: {7}
0.00/0.04	types leq non-linear types: {7}
0.00/0.04	rules applicable to terms of non-linear types:
0.00/0.04	   [ ]
0.00/0.04	terms of non-linear types are innermost terminating
0.00/0.04	inner CP <p,q> = <U0(a,?x_2:12), a>
0.00/0.04	parallel reducts of p: {U0(a,?x_2:12),U0(b,?x_2:12)}
0.00/0.04	unknown Quasi-Left-Linear & Parallel-Closed
0.00/0.04	   [ f(?x,?x) -> a,
0.00/0.04	     g(?x_1) -> U0(g(?x_1),?x_1),
0.00/0.04	     U0(b,?x_2) -> a,
0.00/0.04	     a -> b,
0.00/0.04	     b -> a ]
0.00/0.04	Sort Assignment:
0.00/0.04	 a : =>14
0.00/0.04	 b : =>14
0.00/0.04	 f : 7*7=>14
0.00/0.04	 g : 12=>14
0.00/0.04	 U0 : 14*12=>14
0.00/0.04	non-linear variables: {?x,?x_1}
0.00/0.04	non-linear types: {7,12}
0.00/0.04	types leq non-linear types: {7,12}
0.00/0.04	rules applicable to terms of non-linear types:
0.00/0.04	   [ ]
0.00/0.04	Rnl:
0.00/0.04	0: {}
0.00/0.04	1: {}
0.00/0.04	2: {}
0.00/0.04	3: {}
0.00/0.04	4: {}
0.00/0.04	terms of non-linear types are innermost terminating
0.00/0.04	Critical Pair <U0(a,?x_2), a> by Rules <4, 2>
0.00/0.04	 convertible by a reduction of rules [->(3),->(2)]
0.00/0.04	Satisfiable by 4>2>1,0,3
0.00/0.04	Quasi-Linear & Linearized-Decreasing
0.00/0.04	Direct Methods: CR
0.00/0.04	
0.00/0.04	Combined result: CR
0.00/0.04	U(R) is confluent
0.00/0.04	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.04	(2 msec.)
0.00/0.04	EOF