MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     fact(?x) -> if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     *(s(?x),fact(?x)) -> fact(s(?x)),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,true,false}
Defined function symbols: {*,+,-,if,fact,zero}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     fact(?x) -> if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
   [ *(s(?x),fact(?x)) -> fact(s(?x)),
     if(?x,?y,?y) -> ?y ]
Trying with:
R:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     fact(?x) -> if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
E:
   [ *(s(?x),fact(?x)) = fact(s(?x)),
     if(?x,?y,?y) = ?y ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,Bool}
Signature:
   [ zero : Nat -> Bool,
     fact : Nat -> Nat,
     if : Bool,Nat,Nat -> Nat,
     - : Nat,Nat -> Nat,
     * : Nat,Nat -> Nat,
     + : Nat,Nat -> Nat,
     s : Nat -> Nat,
     0 : Nat,
     true : Bool,
     false : Bool ]
Rule Part:
   [ zero(0) -> true,
     zero(s(?x)) -> false,
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y),
     fact(?x) -> if(zero(?x),s(0),*(?x,fact(-(?x,s(0))))) ]
Conjecture Part:
   [ *(s(?x),fact(?x)) = fact(s(?x)),
     if(?x,?y,?y) = ?y ]
Termination proof failed.
new/if5.trs: Failure(unknown)
(1592 msec.)