YES
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/if3.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,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z: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,0) -> 0,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     +(?x:Nat,s(?y:Nat)) -> s(+(?y:Nat,?x:Nat)),
     *(0,?y:Nat) -> 0,
     *(s(?x:Nat),?y:Nat) -> +(*(?x:Nat,?y:Nat),?y:Nat),
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z: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,0) -> 0,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)) ]
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;
 false : Mul,  true : Mul;
 0 : Mul;
 if : Mul;
 - : Mul;
 s : Mul;
Rules:
   [ +(0,0) -> 0,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?y,?x)),
     *(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:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     s(+(?y_1,s(?x))) = s(+(?x,s(?y_1))) ]
STEP 0
ES:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     s(+(?y_1,s(?x))) = s(+(?x,s(?y_1))) ]
HS:
   [ ]
ES0:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     s(s(+(?x,?y_1))) = s(s(+(?y_1,?x))) ]
HS0:
   [ ]
ES1:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     s(s(+(?x,?y_1))) = s(s(+(?y_1,?x))) ]
HS1:
   [ ]
Expand s(s(+(?x,?y_1))) = s(s(+(?y_1,?x)))
   [ s(s(0)) = s(s(+(0,0))),
     s(s(s(+(?x_2,?y_2)))) = s(s(+(?y_2,s(?x_2)))),
     s(s(s(+(?y_3,?x_3)))) = s(s(+(s(?y_3),?x_3))) ]
ES2:
   [ s(s(0)) = s(s(+(0,0))),
     s(s(s(+(?x_2,?y_2)))) = s(s(+(?y_2,s(?x_2)))),
     s(s(s(+(?y_3,?x_3)))) = s(s(+(s(?y_3),?x_3))),
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS2:
   [ s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
STEP 1
ES:
   [ s(s(0)) = s(s(+(0,0))),
     s(s(s(+(?x_2,?y_2)))) = s(s(+(?y_2,s(?x_2)))),
     s(s(s(+(?y_3,?x_3)))) = s(s(+(s(?y_3),?x_3))),
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS:
   [ s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
ES0:
   [ s(s(0)) = s(s(0)),
     s(s(s(+(?x_2,?y_2)))) = s(s(s(+(?x_2,?y_2)))),
     s(s(s(+(?y_3,?x_3)))) = s(s(s(+(?y_3,?x_3)))),
     fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS0:
   [ s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
ES1:
   [ fact(?x) = if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
HS1:
   [ s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
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),
     s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
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),
     s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
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),
     s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
ES1:
   [ ]
HS1:
   [ if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) -> fact(?x),
     s(s(+(?x,?y_1))) -> s(s(+(?y_1,?x))) ]
: Success(GCR)
(39 msec.)