YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if6.trs
Input rules:
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     *(s(?x:Nat),fact(?x:Nat)) -> fact(s(?x: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,
     fact(?x:Nat) -> if(zero(?x:Nat),s(0),*(?x:Nat,fact(-(?x:Nat,s(0))))),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     *(s(?x:Nat),fact(?x:Nat)) -> fact(s(?x: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),-(?x_2,?x_3),if(?x_3,?x_4,?x_5),fact(?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):
   [ *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?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 ]
No orientable rules for fact(?x_1). Add rules, and retry...
Added rules:
   [ fact(s(?x_1)) -> *(s(?x_1),fact(?x_1)),
     fact(0) -> s(0) ]
candidate for fact(?x_1):
   [ fact(s(?x_1)) -> *(s(?x_1),fact(?x_1)),
     fact(0) -> s(0) ]
candidate for zero(?x_1):
   [ zero(0) -> true,
     zero(s(?x)) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 zero : Mul;
 fact : Mul;
 * : Mul;
 + : Mul;
 - : Mul;
 if : Mul;
 false : Mul,  true : Mul,  0 : Mul;
 s : Mul;
Rules:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     fact(s(?x_1)) -> *(s(?x_1),fact(?x_1)),
     fact(0) -> s(0),
     zero(0) -> true,
     zero(s(?x)) -> false ]
Conjectures:
   [ *(s(?x),fact(?x)) = fact(s(?x)),
     if(?x,?y,?y) = ?y,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
STEP 0
ES:
   [ *(s(?x),fact(?x)) = fact(s(?x)),
     if(?x,?y,?y) = ?y,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS:
   [ ]
ES0:
   [ +(*(?x,fact(?x)),fact(?x)) = +(*(?x,fact(?x)),fact(?x)),
     if(?x,?y,?y) = ?y,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS0:
   [ ]
ES1:
   [ if(?x,?y,?y) = ?y,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS1:
   [ ]
Expand if(?x,?y,?y) = ?y
   [ ?z_8 = ?z_8,
     ?z_9 = ?z_9 ]
ES2:
   [ ?z_8 = ?z_8,
     ?z_9 = ?z_9,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS2:
   [ if(?x,?y,?y) -> ?y ]
STEP 1
ES:
   [ ?z_8 = ?z_8,
     ?z_9 = ?z_9,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS:
   [ if(?x,?y,?y) -> ?y ]
ES0:
   [ ?z_8 = ?z_8,
     ?z_9 = ?z_9,
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS0:
   [ if(?x,?y,?y) -> ?y ]
ES1:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS1:
   [ if(?x,?y,?y) -> ?y ]
Expand if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) = fact(?x)
   [ if(true,s(0),*(0,fact(-(0,s(0))))) = fact(0),
     if(false,s(0),*(s(?x_11),fact(-(s(?x_11),s(0))))) = fact(s(?x_11)) ]
ES2:
   [ s(0) = fact(0),
     +(*(?x_11,fact(?x_11)),fact(?x_11)) = fact(s(?x_11)) ]
HS2:
   [ if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) -> fact(?x),
     if(?x,?y,?y) -> ?y ]
STEP 2
ES:
   [ s(0) = fact(0),
     +(*(?x_11,fact(?x_11)),fact(?x_11)) = fact(s(?x_11)) ]
HS:
   [ if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) -> fact(?x),
     if(?x,?y,?y) -> ?y ]
ES0:
   [ s(0) = s(0),
     +(*(?x_11,fact(?x_11)),fact(?x_11)) = +(*(?x_11,fact(?x_11)),fact(?x_11)) ]
HS0:
   [ if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) -> fact(?x),
     if(?x,?y,?y) -> ?y ]
ES1:
   [ ]
HS1:
   [ if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) -> fact(?x),
     if(?x,?y,?y) -> ?y ]
: Success(GCR)
(37 msec.)