0.00/0.07	MAYBE
0.00/0.07	(ignored inputs)COMMENT [75] Example 38 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.07	Conditional Rewrite Rules:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> true | up(?x) == ?y,down(?z) == ?y ]
0.00/0.07	Check whether all rules are type 3
0.00/0.07	OK
0.00/0.07	Check whether the input is deterministic
0.00/0.07	OK
0.00/0.07	Result of unraveling:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
0.00/0.07	Check whether U(R) is terminating
0.00/0.07	failed to show termination
0.00/0.07	Check whether the input is weakly left-linear
0.00/0.07	OK
0.00/0.07	Conditional critical pairs (CCPs):
0.00/0.07	   [ up(s(?x_2)) = ?x_2,
0.00/0.07	     down(?x_3) = s(?x_3),
0.00/0.07	     ?x = up(s(?x)),
0.00/0.07	     s(?x_3) = down(?x_3) ]
0.00/0.07	Check whether the input is almost orthogonale
0.00/0.07	not almost orthogonal
0.00/0.07	OK
0.00/0.07	Check U(R) is confluent
0.00/0.07	Rewrite Rules:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
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	   [ ?x = up(s(?x)),
0.00/0.07	     s(?x_3) = down(?x_3) ]
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	not Left-Linear, not Right-Linear
0.00/0.07	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
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	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3),
0.00/0.07	     between(?x_4,?y_4,?z_4) -> U0(up(?x_4),?x_4,?y_4,?z_4),
0.00/0.07	     U0(?y_5,?x_5,?y_5,?z_5) -> U1(down(?z_5),?x_5,?z_5,?y_5),
0.00/0.07	     U1(?y_6,?x_6,?z_6,?y_6) -> true ]
0.00/0.07	Sort Assignment:
0.00/0.07	 s : 24=>24
0.00/0.07	 U0 : 24*24*24*24=>35
0.00/0.07	 U1 : 24*24*24*24=>35
0.00/0.07	 up : 24=>24
0.00/0.07	 down : 24=>24
0.00/0.07	 true : =>35
0.00/0.07	 between : 24*24*24=>35
0.00/0.07	non-linear variables: {?y_5,?y_6}
0.00/0.07	non-linear types: {24}
0.00/0.07	types leq non-linear types: {24}
0.00/0.07	rules applicable to terms of non-linear types:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3) ]
0.00/0.07	unknown innermost-termination for terms of non-linear types
0.00/0.07	unknown Quasi-Left-Linear & Parallel-Closed
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3),
0.00/0.07	     between(?x_4,?y_4,?z_4) -> U0(up(?x_4),?x_4,?y_4,?z_4),
0.00/0.07	     U0(?y_5,?x_5,?y_5,?z_5) -> U1(down(?z_5),?x_5,?z_5,?y_5),
0.00/0.07	     U1(?y_6,?x_6,?z_6,?y_6) -> true ]
0.00/0.07	Sort Assignment:
0.00/0.07	 s : 24=>24
0.00/0.07	 U0 : 24*24*24*24=>35
0.00/0.07	 U1 : 24*24*24*24=>35
0.00/0.07	 up : 24=>24
0.00/0.07	 down : 24=>24
0.00/0.07	 true : =>35
0.00/0.07	 between : 24*24*24=>35
0.00/0.07	non-linear variables: {?x_4,?y_5,?z_5,?y_6}
0.00/0.07	non-linear types: {24}
0.00/0.07	types leq non-linear types: {24}
0.00/0.07	rules applicable to terms of non-linear types:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3) ]
0.00/0.07	Rnl:
0.00/0.07	0: {}
0.00/0.07	1: {}
0.00/0.07	2: {}
0.00/0.07	3: {}
0.00/0.07	4: {0,1,2,3}
0.00/0.07	5: {0,1,2,3}
0.00/0.07	6: {0,1,2,3}
0.00/0.07	unknown innermost-termination for terms of non-linear types
0.00/0.07	unknown Quasi-Linear & Linearized-Decreasing
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3),
0.00/0.07	     between(?x_4,?y_4,?z_4) -> U0(up(?x_4),?x_4,?y_4,?z_4),
0.00/0.07	     U0(?y_5,?x_5,?y_5,?z_5) -> U1(down(?z_5),?x_5,?z_5,?y_5),
0.00/0.07	     U1(?y_6,?x_6,?z_6,?y_6) -> true ]
0.00/0.07	Sort Assignment:
0.00/0.07	 s : 24=>24
0.00/0.07	 U0 : 24*24*24*24=>35
0.00/0.07	 U1 : 24*24*24*24=>35
0.00/0.07	 up : 24=>24
0.00/0.07	 down : 24=>24
0.00/0.07	 true : =>35
0.00/0.07	 between : 24*24*24=>35
0.00/0.07	non-linear variables: {?x_4,?y_5,?z_5,?y_6}
0.00/0.07	non-linear types: {24}
0.00/0.07	types leq non-linear types: {24}
0.00/0.07	rules applicable to terms of non-linear types:
0.00/0.07	   [ up(?x) -> ?x,
0.00/0.07	     down(?x_1) -> ?x_1,
0.00/0.07	     up(?x_2) -> up(s(?x_2)),
0.00/0.07	     down(s(?x_3)) -> down(?x_3) ]
0.00/0.07	unknown innermost-termination for terms of non-linear types
0.00/0.07	unknown Strongly Quasi-Linear & Hierarchically Decreasing
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	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
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	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
0.00/0.07	Sort Assignment:
0.00/0.07	 s : 24=>24
0.00/0.07	 U0 : 24*24*24*24=>35
0.00/0.07	 U1 : 24*24*24*24=>35
0.00/0.07	 up : 24=>24
0.00/0.07	 down : 24=>24
0.00/0.07	 true : =>35
0.00/0.07	 between : 24*24*24=>35
0.00/0.07	maximal types: {24,35}
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	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
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	   [ up(?x) -> ?x,
0.00/0.07	     down(?x) -> ?x,
0.00/0.07	     up(?x) -> up(s(?x)),
0.00/0.07	     down(s(?x)) -> down(?x),
0.00/0.07	     between(?x,?y,?z) -> U0(up(?x),?x,?y,?z),
0.00/0.07	     U0(?y,?x,?y,?z) -> U1(down(?z),?x,?z,?y),
0.00/0.07	     U1(?y,?x,?z,?y) -> true ]
0.00/0.07	Commutative Decomposition failed (not left-linear): 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/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.07	(30 msec.)
0.00/0.07	EOF