0.00/0.06	MAYBE
0.00/0.06	(ignored inputs)COMMENT doi:10.1007/s002000100064 [65] Example 5.1 ( R_P ) submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ pin(?x) -> pout(g(?x)),
0.00/0.06	     pin(?x) -> pout(f(?y)) | pin(?x) == pout(g(?y)) ]
0.00/0.06	Check whether all rules are type 3
0.00/0.06	OK
0.00/0.06	Check whether the input is deterministic
0.00/0.06	OK
0.00/0.06	Result of unraveling:
0.00/0.06	   [ pin(?x) -> pout(g(?x)),
0.00/0.06	     pin(?x) -> U0(pin(?x),?x),
0.00/0.06	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.06	Check whether U(R) is terminating
0.00/0.06	failed to show termination
0.00/0.06	Check whether the input is weakly left-linear
0.00/0.06	OK
0.00/0.06	Conditional critical pairs (CCPs):
0.00/0.06	   [ pout(f(?y_1)) = pout(g(?x_1)) | pin(?x_1) == pout(g(?y_1)),
0.00/0.06	     pout(g(?x)) = pout(f(?y_1)) | pin(?x) == pout(g(?y_1)) ]
0.00/0.06	Check whether the input is almost orthogonale
0.00/0.06	not almost orthogonal
0.00/0.06	OK
0.00/0.06	Check U(R) is confluent
0.00/0.06	Rewrite Rules:
0.00/0.06	   [ pin(?x) -> pout(g(?x)),
0.00/0.06	     pin(?x) -> U0(pin(?x),?x),
0.00/0.06	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.06	Apply Direct Methods...
0.00/0.06	Inner CPs:
0.00/0.06	   [  ]
0.00/0.06	Outer CPs:
0.00/0.06	   [ pout(g(?x)) = U0(pin(?x),?x) ]
0.00/0.06	Overlay, check Innermost Termination...
0.00/0.06	unknown Innermost Terminating
0.00/0.06	unknown Knuth & Bendix
0.00/0.06	Left-Linear, not Right-Linear
0.00/0.06	unknown Development Closed
0.00/0.06	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.06	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.06	(inner) Parallel CPs: (not computed)
0.00/0.06	unknown Toyama (Parallel CPs)
0.00/0.06	Simultaneous CPs:
0.00/0.06	   [ U0(pin(?x),?x) = pout(g(?x)),
0.00/0.06	     pout(g(?x)) = U0(pin(?x),?x) ]
0.00/0.06	unknown Okui (Simultaneous CPs)
0.00/0.06	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.06	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.06	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.06	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0> preceded by []
0.00/0.06	unknown Diagram Decreasing
0.00/0.06	   [ pin(?x) -> pout(g(?x)),
0.00/0.06	     pin(?x_1) -> U0(pin(?x_1),?x_1),
0.00/0.06	     U0(pout(g(?y_2)),?x_2) -> pout(f(?y_2)) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 f : 5=>14
0.00/0.06	 g : 5=>14
0.00/0.06	 U0 : 16*5=>16
0.00/0.06	 pin : 5=>16
0.00/0.06	 pout : 14=>16
0.00/0.06	non-linear variables: {?x_1}
0.00/0.06	non-linear types: {5}
0.00/0.06	types leq non-linear types: {5}
0.00/0.06	rules applicable to terms of non-linear types:
0.00/0.06	   [ ]
0.00/0.06	Rnl:
0.00/0.06	0: {}
0.00/0.06	1: {}
0.00/0.06	2: {}
0.00/0.06	terms of non-linear types are innermost terminating
0.00/0.06	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0>
0.00/0.06	no joinable sequence for some critical pairs
0.00/0.06	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.06	   [ pin(?x) -> pout(g(?x)),
0.00/0.06	     pin(?x_1) -> U0(pin(?x_1),?x_1),
0.00/0.06	     U0(pout(g(?y_2)),?x_2) -> pout(f(?y_2)) ]
0.00/0.06	Sort Assignment:
0.00/0.06	 f : 5=>14
0.00/0.06	 g : 5=>14
0.00/0.06	 U0 : 16*5=>16
0.00/0.06	 pin : 5=>16
0.00/0.06	 pout : 14=>16
0.00/0.06	non-linear variables: {?x_1}
0.00/0.06	non-linear types: {5}
0.00/0.06	types leq non-linear types: {5}
0.00/0.06	rules applicable to terms of non-linear types:
0.00/0.06	   [ ]
0.00/0.06	terms of non-linear types are terminating
0.00/0.06	Check Joinablility of CP from NLR:
0.00/0.06	done.
0.00/0.06	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0>
0.00/0.06	no joinable sequence for some critical pairs
0.00/0.06	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.06	unknown Huet (modulo AC)
0.00/0.06	check by Reduction-Preserving Completion...
0.00/0.06	failure(empty P)
0.00/0.06	unknown Reduction-Preserving Completion
0.00/0.06	check by Ordered Rewriting...
0.00/0.06	remove redundants rules and split
0.00/0.07	R-part:
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x),
0.00/0.07	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.07	E-part:
0.00/0.07	   [ ]
0.00/0.07	...failed to find a suitable LPO.
0.00/0.07	unknown Confluence by Ordered Rewriting
0.00/0.07	Direct Methods: Can't judge
0.00/0.07	
0.00/0.07	Try Persistent Decomposition for...
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x),
0.00/0.07	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.07	Sort Assignment:
0.00/0.07	 f : 5=>14
0.00/0.07	 g : 5=>14
0.00/0.07	 U0 : 16*5=>16
0.00/0.07	 pin : 5=>16
0.00/0.07	 pout : 14=>16
0.00/0.07	maximal types: {5,14,16}
0.00/0.07	Persistent Decomposition failed: Can't judge
0.00/0.07	
0.00/0.07	Try Layer Preserving Decomposition for...
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x),
0.00/0.07	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.07	Layer Preserving Decomposition failed: Can't judge
0.00/0.07	
0.00/0.07	Try Commutative Decomposition for...
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x),
0.00/0.07	     U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.07	Outside Critical Pair: <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0>
0.00/0.07	develop reducts from lhs term...
0.00/0.07	<{1}, U0(U0(pin(?x_1),?x_1),?x_1)>
0.00/0.07	<{0}, U0(pout(g(?x_1)),?x_1)>
0.00/0.07	<{}, U0(pin(?x_1),?x_1)>
0.00/0.07	develop reducts from rhs term...
0.00/0.07	<{}, pout(g(?x_1))>
0.00/0.07	Try A Minimal Decomposition {0,1}{2}
0.00/0.07	{0,1}
0.00/0.07	(cm)Rewrite Rules:
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x) ]
0.00/0.07	Apply Direct Methods...
0.00/0.07	Inner CPs:
0.00/0.07	   [  ]
0.00/0.07	Outer CPs:
0.00/0.07	   [ pout(g(?x)) = U0(pin(?x),?x) ]
0.00/0.07	Overlay, check Innermost Termination...
0.00/0.07	unknown Innermost Terminating
0.00/0.07	unknown Knuth & Bendix
0.00/0.07	Left-Linear, not Right-Linear
0.00/0.07	unknown Development Closed
0.00/0.07	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.07	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.07	(inner) Parallel CPs: (not computed)
0.00/0.07	unknown Toyama (Parallel CPs)
0.00/0.07	Simultaneous CPs:
0.00/0.07	   [ U0(pin(?x),?x) = pout(g(?x)),
0.00/0.07	     pout(g(?x)) = U0(pin(?x),?x) ]
0.00/0.07	unknown Okui (Simultaneous CPs)
0.00/0.07	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.07	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.07	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.07	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0> preceded by []
0.00/0.07	unknown Diagram Decreasing
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x_1) -> U0(pin(?x_1),?x_1) ]
0.00/0.07	Sort Assignment:
0.00/0.07	 g : 6=>10
0.00/0.07	 U0 : 5*6=>5
0.00/0.07	 pin : 6=>5
0.00/0.07	 pout : 10=>5
0.00/0.07	non-linear variables: {?x_1}
0.00/0.07	non-linear types: {6}
0.00/0.07	types leq non-linear types: {6}
0.00/0.07	rules applicable to terms of non-linear types:
0.00/0.07	   [ ]
0.00/0.07	Rnl:
0.00/0.07	0: {}
0.00/0.07	1: {}
0.00/0.07	terms of non-linear types are innermost terminating
0.00/0.07	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0>
0.00/0.07	no joinable sequence for some critical pairs
0.00/0.07	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x_1) -> U0(pin(?x_1),?x_1) ]
0.00/0.07	Sort Assignment:
0.00/0.07	 g : 6=>10
0.00/0.07	 U0 : 5*6=>5
0.00/0.07	 pin : 6=>5
0.00/0.07	 pout : 10=>5
0.00/0.07	non-linear variables: {?x_1}
0.00/0.07	non-linear types: {6}
0.00/0.07	types leq non-linear types: {6}
0.00/0.07	rules applicable to terms of non-linear types:
0.00/0.07	   [ ]
0.00/0.07	terms of non-linear types are terminating
0.00/0.07	Check Joinablility of CP from NLR:
0.00/0.07	done.
0.00/0.07	Critical Pair <U0(pin(?x_1),?x_1), pout(g(?x_1))> by Rules <1, 0>
0.00/0.07	no joinable sequence for some critical pairs
0.00/0.07	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.07	unknown Huet (modulo AC)
0.00/0.07	check by Reduction-Preserving Completion...
0.00/0.07	failure(empty P)
0.00/0.07	unknown Reduction-Preserving Completion
0.00/0.07	check by Ordered Rewriting...
0.00/0.07	remove redundants rules and split
0.00/0.07	R-part:
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x) ]
0.00/0.07	E-part:
0.00/0.07	   [ ]
0.00/0.07	...failed to find a suitable LPO.
0.00/0.07	unknown Confluence by Ordered Rewriting
0.00/0.07	Direct Methods: Can't judge
0.00/0.07	
0.00/0.07	Try Persistent Decomposition for...
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x) ]
0.00/0.07	Sort Assignment:
0.00/0.07	 g : 6=>10
0.00/0.07	 U0 : 5*6=>5
0.00/0.07	 pin : 6=>5
0.00/0.07	 pout : 10=>5
0.00/0.07	maximal types: {5,6,10}
0.00/0.07	Persistent Decomposition failed: Can't judge
0.00/0.07	
0.00/0.07	Try Layer Preserving Decomposition for...
0.00/0.07	   [ pin(?x) -> pout(g(?x)),
0.00/0.07	     pin(?x) -> U0(pin(?x),?x) ]
0.00/0.07	Layer Preserving Decomposition failed: Can't judge
0.00/0.07	No further decomposition possible
0.00/0.07	
0.00/0.07	{2}
0.00/0.07	(cm)Rewrite Rules:
0.00/0.07	   [ U0(pout(g(?y)),?x) -> pout(f(?y)) ]
0.00/0.07	Apply Direct Methods...
0.00/0.07	Inner CPs:
0.00/0.07	   [  ]
0.00/0.07	Outer CPs:
0.00/0.07	   [  ]
0.00/0.07	Overlay, check Innermost Termination...
0.00/0.07	Innermost Terminating (hence Terminating), WCR
0.00/0.07	Knuth & Bendix
0.00/0.07	Direct Methods: CR
0.00/0.07	Commutative Decomposition failed: Can't judge
0.00/0.07	No further decomposition possible
0.00/0.07	
0.00/0.07	
0.00/0.07	Combined result: Can't judge
0.00/0.07	failed to show confluence of U(R)
0.00/0.07	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.07	(16 msec.)
0.00/0.07	EOF