9.48/8.45	YES
9.48/8.45	(ignored inputs)COMMENT from Toyama ( LA symposium 1998 ) submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
9.48/8.45	Rewrite Rules:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	Apply Direct Methods...
9.48/8.45	Inner CPs:
9.48/8.45	   [ f(?x,g(?x)) = g(f(?x,?x)) ]
9.48/8.45	Outer CPs:
9.48/8.45	   [  ]
9.48/8.45	not Overlay, check Termination...
9.48/8.45	unknown/not Terminating
9.48/8.45	unknown Knuth & Bendix
9.48/8.45	not Left-Linear, not Right-Linear
9.48/8.45	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
9.48/8.45	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
9.48/8.45	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	Sort Assignment:
9.48/8.45	 a : 12=>12
9.48/8.45	 f : 12*12=>12
9.48/8.45	 g : 12=>12
9.48/8.45	 h : 12=>12
9.48/8.45	non-linear variables: {?x,?x_1}
9.48/8.45	non-linear types: {12}
9.48/8.45	types leq non-linear types: {12}
9.48/8.45	rules applicable to terms of non-linear types:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	unknown innermost-termination for terms of non-linear types
9.48/8.45	unknown Quasi-Left-Linear & Parallel-Closed
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	Sort Assignment:
9.48/8.45	 a : 12=>12
9.48/8.45	 f : 12*12=>12
9.48/8.45	 g : 12=>12
9.48/8.45	 h : 12=>12
9.48/8.45	non-linear variables: {?x,?x,?x_1,?x_1}
9.48/8.45	non-linear types: {12}
9.48/8.45	types leq non-linear types: {12}
9.48/8.45	rules applicable to terms of non-linear types:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	Rnl:
9.48/8.45	0: {0,1,2,3}
9.48/8.45	1: {0,1,2,3}
9.48/8.45	2: {}
9.48/8.45	3: {}
9.48/8.45	unknown innermost-termination for terms of non-linear types
9.48/8.45	unknown Quasi-Linear & Linearized-Decreasing
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	Sort Assignment:
9.48/8.45	 a : 12=>12
9.48/8.45	 f : 12*12=>12
9.48/8.45	 g : 12=>12
9.48/8.45	 h : 12=>12
9.48/8.45	non-linear variables: {?x,?x,?x_1,?x_1}
9.48/8.45	non-linear types: {12}
9.48/8.45	types leq non-linear types: {12}
9.48/8.45	rules applicable to terms of non-linear types:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x_1,g(?x_1)) -> g(f(?x_1,?x_1)),
9.48/8.45	     a(?x_2) -> ?x_2,
9.48/8.45	     h(?x_3) -> h(a(h(?x_3))) ]
9.48/8.45	unknown innermost-termination for terms of non-linear types
9.48/8.45	unknown Strongly Quasi-Linear & Hierarchically Decreasing
9.48/8.45	check Non-Confluence...
9.48/8.45	obtain 7 rules by 3 steps unfolding
9.48/8.45	obtain 80 candidates for checking non-joinability
9.48/8.45	check by TCAP-Approximation (failure)
9.48/8.45	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
9.48/8.45	check by Interpretation(mod2) (failure)
9.48/8.45	check by Descendants-Approximation, check by Ordering(poly) (failure)
9.48/8.45	unknown Non-Confluence
9.48/8.45	check by Reduction-Preserving Completion...
9.48/8.45	failure(empty P)
9.48/8.45	unknown Reduction-Preserving Completion
9.48/8.45	check by Ordered Rewriting...
9.48/8.45	remove redundants rules and split
9.48/8.45	R-part:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	E-part:
9.48/8.45	   [ ]
9.48/8.45	...failed to find a suitable LPO.
9.48/8.45	unknown Confluence by Ordered Rewriting
9.48/8.45	Direct Methods: Can't judge
9.48/8.45	
9.48/8.45	Try Persistent Decomposition for...
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	Sort Assignment:
9.48/8.45	 a : 12=>12
9.48/8.45	 f : 12*12=>12
9.48/8.45	 g : 12=>12
9.48/8.45	 h : 12=>12
9.48/8.45	maximal types: {12}
9.48/8.45	Persistent Decomposition failed: Can't judge
9.48/8.45	
9.48/8.45	Try Layer Preserving Decomposition for...
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	(lp)   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x ]
9.48/8.45	Rewrite Rules:
9.48/8.45	   [ f(?x,a(g(?x))) -> g(f(?x,?x)),
9.48/8.45	     f(?x,g(?x)) -> g(f(?x,?x)),
9.48/8.45	     a(?x) -> ?x ]
9.48/8.45	Apply Direct Methods...
9.48/8.45	Inner CPs:
9.48/8.45	   [ f(?x,g(?x)) = g(f(?x,?x)) ]
9.48/8.45	Outer CPs:
9.48/8.45	   [  ]
9.48/8.45	not Overlay, check Termination...
9.48/8.45	Terminating, WCR
9.48/8.45	Knuth & Bendix
9.48/8.45	Direct Methods: CR
9.48/8.45	(lp)   [ a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	Rewrite Rules:
9.48/8.45	   [ a(?x) -> ?x,
9.48/8.45	     h(?x) -> h(a(h(?x))) ]
9.48/8.45	Apply Direct Methods...
9.48/8.45	Inner CPs:
9.48/8.45	   [  ]
9.48/8.45	Outer CPs:
9.48/8.45	   [  ]
9.48/8.45	Overlay, check Innermost Termination...
9.48/8.45	unknown Innermost Terminating
9.48/8.45	unknown Knuth & Bendix
9.48/8.45	Linear
9.48/8.45	Development Closed
9.48/8.45	Direct Methods: CR
9.48/8.45	Result by Layer Preserving Decomposition: CR
9.48/8.45	
9.48/8.45	Combined result: CR
9.48/8.45	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
9.48/8.45	(1947 msec.)
9.48/8.45	EOF