0.00/0.16	NO
0.00/0.16	(ignored inputs)COMMENT [5] p. 287 , attributed to Sivakumar submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
0.00/0.16	Rewrite Rules:
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x,g(?x)) -> b,
0.00/0.16	     h(c,?y) -> f(h(?y,c),h(?y,?y)) ]
0.00/0.16	Apply Direct Methods...
0.00/0.16	Inner CPs:
0.00/0.16	   [  ]
0.00/0.16	Outer CPs:
0.00/0.16	   [  ]
0.00/0.16	Overlay, check Innermost Termination...
0.00/0.16	unknown Innermost Terminating
0.00/0.16	unknown Knuth & Bendix
0.00/0.16	not Left-Linear, not Right-Linear
0.00/0.16	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.16	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.16	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	Sort Assignment:
0.00/0.16	 b : =>14
0.00/0.16	 c : =>11
0.00/0.16	 f : 14*14=>14
0.00/0.16	 g : 14=>14
0.00/0.16	 h : 11*11=>14
0.00/0.16	non-linear variables: {?x,?x_1}
0.00/0.16	non-linear types: {14}
0.00/0.16	types leq non-linear types: {14}
0.00/0.16	rules applicable to terms of non-linear types:
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	unknown innermost-termination for terms of non-linear types
0.00/0.16	unknown Quasi-Left-Linear & Parallel-Closed
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	Sort Assignment:
0.00/0.16	 b : =>14
0.00/0.16	 c : =>11
0.00/0.16	 f : 14*14=>14
0.00/0.16	 g : 14=>14
0.00/0.16	 h : 11*11=>14
0.00/0.16	non-linear variables: {?x,?x_1,?y_2}
0.00/0.16	non-linear types: {14,11}
0.00/0.16	types leq non-linear types: {14,11}
0.00/0.16	rules applicable to terms of non-linear types:
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	Rnl:
0.00/0.16	0: {0,1,2}
0.00/0.16	1: {0,1,2}
0.00/0.16	2: {}
0.00/0.16	unknown innermost-termination for terms of non-linear types
0.00/0.16	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	Sort Assignment:
0.00/0.16	 b : =>14
0.00/0.16	 c : =>11
0.00/0.16	 f : 14*14=>14
0.00/0.16	 g : 14=>14
0.00/0.16	 h : 11*11=>14
0.00/0.16	non-linear variables: {?x,?x_1,?y_2}
0.00/0.16	non-linear types: {14,11}
0.00/0.16	types leq non-linear types: {14,11}
0.00/0.16	rules applicable to terms of non-linear types:
0.00/0.16	   [ f(?x,?x) -> g(?x),
0.00/0.16	     f(?x_1,g(?x_1)) -> b,
0.00/0.16	     h(c,?y_2) -> f(h(?y_2,c),h(?y_2,?y_2)) ]
0.00/0.16	unknown innermost-termination for terms of non-linear types
0.00/0.16	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.16	check Non-Confluence...
0.00/0.16	obtain 11 rules by 3 steps unfolding
0.00/0.16	obtain 100 candidates for checking non-joinability
0.00/0.16	check by TCAP-Approximation (success)
0.00/0.16	Witness for Non-Confluence: <g(b) <- h(c,c) -> b>
0.00/0.16	Direct Methods: not CR
0.00/0.16	
0.00/0.16	Combined result: not CR
0.00/0.16	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(not CR)
0.00/0.16	(97 msec.)
0.00/0.16	EOF