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