0.00/0.04	YES
0.00/0.04	(ignored inputs)COMMENT [62] Example 4.2 http://www.w3.org/People/Massimo/papers/MIT-LCS-TM-405.pdf submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ plus(0,?X) -> ?X,
0.00/0.04	     plus(s(?X),?Y) -> plus(?X,s(?Y)),
0.00/0.04	     fib(0) -> pair(s(0),0),
0.00/0.04	     fib(s(?X)) -> pair(?W,?Y) | fib(?X) == pair(?Y,?Z),plus(?Y,?Z) == ?W ]
0.00/0.04	Check whether all rules are type 3
0.00/0.04	OK
0.00/0.04	Check whether the input is deterministic
0.00/0.04	OK
0.00/0.04	Result of unraveling:
0.00/0.04	   [ plus(0,?X) -> ?X,
0.00/0.04	     plus(s(?X),?Y) -> plus(?X,s(?Y)),
0.00/0.04	     fib(0) -> pair(s(0),0),
0.00/0.04	     fib(s(?X)) -> U0(fib(?X),?X),
0.00/0.04	     U0(pair(?Y,?Z),?X) -> U1(plus(?Y,?Z),?X,?Y,?Z),
0.00/0.04	     U1(?W,?X,?Y,?Z) -> pair(?W,?Y) ]
0.00/0.04	Check whether U(R) is terminating
0.00/0.04	OK
0.00/0.04	Check whether the input is weakly left-linear
0.00/0.04	OK
0.00/0.04	Check whether U(R) is confluent
0.00/0.04	OK
0.00/0.04	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.04	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(CR)
0.00/0.04	(9 msec.)
0.00/0.04	EOF