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