YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if8.trs
Input rules:
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fib(0) -> 0,
     fib(s(?x:Nat)) -> if(zero(?x:Nat),s(0),+(fib(?x:Nat),fib(-(?x:Nat,s(0))))),
     +(fib(s(?x:Nat)),fib(?x:Nat)) -> fib(s(s(?x:Nat))),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fib(0) -> 0,
     fib(s(?x:Nat)) -> if(zero(?x:Nat),s(0),+(fib(?x:Nat),fib(-(?x:Nat,s(0))))),
     +(fib(s(?x:Nat)),fib(?x:Nat)) -> fib(s(s(?x:Nat))),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     if(?x:Bool,?y:Nat,?y:Nat) -> ?y:Nat,
     -(?x:Nat,0) -> ?x:Nat,
     -(0,s(?y:Nat)) -> 0,
     -(s(?x:Nat),s(?y:Nat)) -> -(?x:Nat,?y:Nat) ]
Constructor pattern: [s(?x_1),0,true,false]
Defined pattern: [+(?x_2,?x_3),-(?x_2,?x_3),if(?x_3,?x_4,?x_5),fib(?x_1),zero(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for +(?x_2,?x_3):
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
candidate for -(?x_2,?x_3):
   [ -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z ]
candidate for fib(?x_1):
   [ fib(0) -> 0,
     fib(s(?x)) -> if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
candidate for zero(?x_1):
   [ zero(0) -> true,
     zero(s(?x)) -> false ]
Find a quasi-ordering ...
encodeSameNthStatus +/0, +/1
encodeSameNthStatus(sub) logArF:1, logArG:1
encodeSameNthStatus -/0, -/1
encodeSameNthStatus(sub) logArF:1, logArG:1
encodeSameNthStatus if/0, if/1
encodeSameNthStatus(sub) logArF:2, logArG:2
encodeSameNthStatus if/0, if/2
encodeSameNthStatus(sub) logArF:2, logArG:2
encodeSameNthStatus if/1, if/2
encodeSameNthStatus(sub) logArF:2, logArG:2
failed to find an ordering.
Try to supplement auxiliary rules.
{}{}{}{fib(-(?x,s(0))),fib(?x)}{}{}{+(?x,?y)}{}{}{}{}{}{-(?x,?y)}Supplemented Rules:
   [ fib(s(0)) -> s(0),
     fib(s(s(?x_1))) -> +(fib(s(?x_1)),fib(?x_1)) ]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for +(?x_2,?x_3):
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)) ]
candidate for -(?x_2,?x_3):
   [ -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z ]
candidate for fib(?x_1):
   [ fib(0) -> 0,
     fib(s(?x)) -> if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
   [ fib(0) -> 0,
     fib(s(0)) -> s(0),
     fib(s(s(?x_1))) -> +(fib(s(?x_1)),fib(?x_1)) ]
candidate for zero(?x_1):
   [ zero(0) -> true,
     zero(s(?x)) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 fib : Mul;
 true : Mul,  0 : Mul;
 - : Mul,  + : Mul;
 if : Mul;
 zero : Mul,  s : Mul;
 false : Mul;
Rules:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     fib(0) -> 0,
     fib(s(0)) -> s(0),
     fib(s(s(?x_1))) -> +(fib(s(?x_1)),fib(?x_1)),
     zero(0) -> true,
     zero(s(?x)) -> false ]
Conjectures:
   [ +(fib(s(?x)),fib(?x)) = fib(s(s(?x))),
     if(?x,?y,?y) = ?y,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
STEP 0
ES:
   [ +(fib(s(?x)),fib(?x)) = fib(s(s(?x))),
     if(?x,?y,?y) = ?y,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS:
   [ ]
ES0:
   [ +(fib(s(?x)),fib(?x)) = +(fib(s(?x)),fib(?x)),
     if(?x,?y,?y) = ?y,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS0:
   [ ]
ES1:
   [ if(?x,?y,?y) = ?y,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS1:
   [ ]
Expand if(?x,?y,?y) = ?y
   [ ?z_6 = ?z_6,
     ?z_7 = ?z_7 ]
ES2:
   [ ?z_6 = ?z_6,
     ?z_7 = ?z_7,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS2:
   [ if(?x,?y,?y) -> ?y ]
STEP 1
ES:
   [ ?z_6 = ?z_6,
     ?z_7 = ?z_7,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS:
   [ if(?x,?y,?y) -> ?y ]
ES0:
   [ ?z_6 = ?z_6,
     ?z_7 = ?z_7,
     fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS0:
   [ if(?x,?y,?y) -> ?y ]
ES1:
   [ fib(s(?x)) = if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) ]
HS1:
   [ if(?x,?y,?y) -> ?y ]
Expand if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) = fib(s(?x))
   [ if(true,s(0),+(fib(0),fib(-(0,s(0))))) = fib(s(0)),
     if(false,s(0),+(fib(s(?x_9)),fib(-(s(?x_9),s(0))))) = fib(s(s(?x_9))) ]
ES2:
   [ s(0) = fib(s(0)),
     +(fib(s(?x_9)),fib(?x_9)) = fib(s(s(?x_9))) ]
HS2:
   [ if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) -> fib(s(?x)),
     if(?x,?y,?y) -> ?y ]
STEP 2
ES:
   [ s(0) = fib(s(0)),
     +(fib(s(?x_9)),fib(?x_9)) = fib(s(s(?x_9))) ]
HS:
   [ if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) -> fib(s(?x)),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ s(0) = s(0),
     +(fib(s(?x_9)),fib(?x_9)) = +(fib(s(?x_9)),fib(?x_9)) ]
HS0:
   [ if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) -> fib(s(?x)),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ ]
HS1:
   [ if(zero(?x),s(0),+(fib(?x),fib(-(?x,s(0))))) -> fib(s(?x)),
     if(?x,?y,?y) -> ?y ]
: Success(GCR)
(77 msec.)