0.00/0.34	MAYBE
0.00/0.34	(ignored inputs)COMMENT [79] Example 9
0.00/0.34	Conditional Rewrite Rules:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> dot(?y,dot(?x,?l)) | les(?x,?y) == true,
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Check whether all rules are type 3
0.00/0.34	OK
0.00/0.34	Check whether the input is deterministic
0.00/0.34	OK
0.00/0.34	Result of unraveling:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Check whether U(R) is terminating
0.00/0.34	failed to show termination
0.00/0.34	Check whether the input is weakly left-linear
0.00/0.34	OK
0.00/0.34	Conditional critical pairs (CCPs):
0.00/0.34	   [ dot(?x_1,dot(?y,dot(?x,?l))) = dot(?x,dot(?x_1,dot(?y,?l))) | les(?x,?y) == true,les(?x_1,?x) == true ]
0.00/0.34	Check whether the input is almost orthogonale
0.00/0.34	not almost orthogonal
0.00/0.34	OK
0.00/0.34	Check U(R) is confluent
0.00/0.34	Rewrite Rules:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [ dot(?x_1,U0(les(?x,?y),?l,?x,?y)) = U0(les(?x_1,?x),dot(?y,?l),?x_1,?x) ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	not Overlay, check Termination...
0.00/0.34	unknown/not Terminating
0.00/0.34	unknown Knuth & Bendix
0.00/0.34	Left-Linear, not Right-Linear
0.00/0.34	unknown Development Closed
0.00/0.34	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.00/0.34	inner CP cond (upside-parallel)
0.00/0.34	innter CP Cond (outside)
0.00/0.34	unknown Upside-Parallel-Closed/Outside-Closed
0.00/0.34	(inner) Parallel CPs: (not computed)
0.00/0.34	unknown Toyama (Parallel CPs)
0.00/0.34	Simultaneous CPs:
0.00/0.34	   [ dot(?x,U0(les(?y,?y_1),?l_1,?y,?y_1)) = U0(les(?x,?y),dot(?y_1,?l_1),?x,?y),
0.00/0.34	     U0(les(?x_1,?x),U0(les(?y,?y_2),?l_2,?y,?y_2),?x_1,?x) = dot(?x_1,U0(les(?x,?y),dot(?y_2,?l_2),?x,?y)),
0.00/0.34	     U0(les(?x_1,?x),dot(?y,?l),?x_1,?x) = dot(?x_1,U0(les(?x,?y),?l,?x,?y)) ]
0.00/0.34	unknown Okui (Simultaneous CPs)
0.00/0.34	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.34	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.00/0.34	check Locally Decreasing Diagrams by Rule Labelling...
0.00/0.34	Critical Pair <dot(?x_1,U0(les(?x,?y),?l,?x,?y)), U0(les(?x_1,?x),dot(?y,?l),?x_1,?x)> by Rules <0, 0> preceded by [(dot,2)]
0.00/0.34	unknown Diagram Decreasing
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l_1,?x_1,?y_1) -> dot(?y_1,dot(?x_1,?l_1)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x_2))) -> les(0,s(?x_2)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x_3)),0) -> les(s(?x_3),0),
0.00/0.34	     les(s(?x_4),s(?y_4)) -> les(?x_4,?y_4) ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>12
0.00/0.34	 s : 12=>12
0.00/0.34	 U0 : 27*33*12*12=>33
0.00/0.34	 dot : 12*33=>33
0.00/0.34	 les : 12*12=>27
0.00/0.34	 true : =>27
0.00/0.34	 false : =>27
0.00/0.34	non-linear variables: {?x,?y}
0.00/0.34	non-linear types: {12}
0.00/0.34	types leq non-linear types: {12}
0.00/0.34	rules applicable to terms of non-linear types:
0.00/0.34	   [ ]
0.00/0.34	Rnl:
0.00/0.34	0: {}
0.00/0.34	1: {}
0.00/0.34	2: {}
0.00/0.34	3: {}
0.00/0.34	4: {}
0.00/0.34	5: {}
0.00/0.34	6: {}
0.00/0.34	7: {}
0.00/0.34	terms of non-linear types are innermost terminating
0.00/0.34	Critical Pair <dot(?x_1,U0(les(?x,?y),?l,?x,?y)), U0(les(?x_1,?x),dot(?y,?l),?x_1,?x)> by Rules <0, 0>
0.00/0.34	no joinable sequence for some critical pairs
0.00/0.34	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l_1,?x_1,?y_1) -> dot(?y_1,dot(?x_1,?l_1)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x_2))) -> les(0,s(?x_2)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x_3)),0) -> les(s(?x_3),0),
0.00/0.34	     les(s(?x_4),s(?y_4)) -> les(?x_4,?y_4) ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>12
0.00/0.34	 s : 12=>12
0.00/0.34	 U0 : 27*33*12*12=>33
0.00/0.34	 dot : 12*33=>33
0.00/0.34	 les : 12*12=>27
0.00/0.34	 true : =>27
0.00/0.34	 false : =>27
0.00/0.34	non-linear variables: {?x,?y}
0.00/0.34	non-linear types: {12}
0.00/0.34	types leq non-linear types: {12}
0.00/0.34	rules applicable to terms of non-linear types:
0.00/0.34	   [ ]
0.00/0.34	terms of non-linear types are terminating
0.00/0.34	Check Joinablility of CP from NLR:
0.00/0.34	done.
0.00/0.34	Critical Pair <dot(?x_1,U0(les(?x,?y),?l,?x,?y)), U0(les(?x_1,?x),dot(?y,?l),?x_1,?x)> by Rules <0, 0>
0.00/0.34	no joinable sequence for some critical pairs
0.00/0.34	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.00/0.34	unknown Huet (modulo AC)
0.00/0.34	check by Reduction-Preserving Completion...
0.00/0.34	STEP: 1 (parallel)
0.00/0.34	S:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	P:
0.00/0.34	   [ les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0) ]
0.00/0.34	P: not reversible
0.00/0.34	failure(Step 1)
0.00/0.34	STEP: 2 (linear)
0.00/0.34	S:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	P:
0.00/0.34	   [ les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0) ]
0.00/0.34	P: not reversible
0.00/0.34	failure(Step 2)
0.00/0.34	STEP: 3 (relative)
0.00/0.34	S:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	P:
0.00/0.34	   [ les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0) ]
0.00/0.34	P: not reversible
0.00/0.34	failure(Step 3)
0.00/0.34	failure(no possibility remains)
0.00/0.34	unknown Reduction-Preserving Completion
0.00/0.34	check by Ordered Rewriting...
0.00/0.34	remove redundants rules and split
0.00/0.34	R-part:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	E-part:
0.00/0.34	   [ ]
0.00/0.34	...failed to find a suitable LPO.
0.00/0.34	unknown Confluence by Ordered Rewriting
0.00/0.34	Direct Methods: Can't judge
0.00/0.34	
0.00/0.34	Try Persistent Decomposition for...
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Sort Assignment:
0.00/0.34	 0 : =>12
0.00/0.34	 s : 12=>12
0.00/0.34	 U0 : 27*33*12*12=>33
0.00/0.34	 dot : 12*33=>33
0.00/0.34	 les : 12*12=>27
0.00/0.34	 true : =>27
0.00/0.34	 false : =>27
0.00/0.34	maximal types: {12,27,33}
0.00/0.34	Persistent Decomposition failed: Can't judge
0.00/0.34	
0.00/0.34	Try Layer Preserving Decomposition for...
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Layer Preserving Decomposition failed: Can't judge
0.00/0.34	
0.00/0.34	Try Commutative Decomposition for...
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y),
0.00/0.34	     U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)),
0.00/0.34	     les(0,0) -> false,
0.00/0.34	     les(0,s(0)) -> true,
0.00/0.34	     les(0,s(s(?x))) -> les(0,s(?x)),
0.00/0.34	     les(s(0),0) -> false,
0.00/0.34	     les(s(s(?x)),0) -> les(s(?x),0),
0.00/0.34	     les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Try A Minimal Decomposition {0}{1}{2}{3}{4}{5}{6}{7}
0.00/0.34	{0}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ dot(?x,dot(?y,?l)) -> U0(les(?x,?y),?l,?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [ dot(?x_1,U0(les(?x,?y),?l,?x,?y)) = U0(les(?x_1,?x),dot(?y,?l),?x_1,?x) ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	not Overlay, check Termination...
0.00/0.34	Terminating, not WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: not CR
0.00/0.34	{1}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ U0(true,?l,?x,?y) -> dot(?y,dot(?x,?l)) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{2}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(0,0) -> false ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{3}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(0,s(0)) -> true ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{4}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(0,s(s(?x))) -> les(0,s(?x)) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{5}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(s(0),0) -> false ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{6}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(s(s(?x)),0) -> les(s(?x),0) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.34	{7}
0.00/0.34	(cm)Rewrite Rules:
0.00/0.34	   [ les(s(?x),s(?y)) -> les(?x,?y) ]
0.00/0.34	Apply Direct Methods...
0.00/0.34	Inner CPs:
0.00/0.34	   [  ]
0.00/0.34	Outer CPs:
0.00/0.34	   [  ]
0.00/0.34	Overlay, check Innermost Termination...
0.00/0.34	Innermost Terminating (hence Terminating), WCR
0.00/0.34	Knuth & Bendix
0.00/0.34	Direct Methods: CR
0.00/0.35	Commutative Decomposition failed: Can't judge
0.00/0.35	No further decomposition possible
0.00/0.35	
0.00/0.35	
0.00/0.35	Combined result: Can't judge
0.00/0.35	failed to show confluence of U(R)
0.00/0.35	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.35	(216 msec.)
0.00/0.35	EOF