NO
/home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/gncr.trs
Input rules:
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     f(0) -> 0,
     f(?x:Nat) -> if(zero(?x:Nat),s(0),0) ]
Sorts having no ground terms: 
Rules applicable to ground terms:
   [ zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     if(true,?y:Nat,?z:Nat) -> ?y:Nat,
     if(false,?y:Nat,?z:Nat) -> ?z:Nat,
     f(0) -> 0,
     f(?x:Nat) -> if(zero(?x:Nat),s(0),0) ]
Constructor pattern: [s(?x_1),0,true,false]
Defined pattern: [f(?x_1),if(?x_3,?x_4,?x_5),zero(?x_1)]
Constructor subsystem:
   [ ]
Modified Constructor subsystem:
   [ ]
candidate for f(?x_1):
   [ f(?x) -> if(zero(?x),s(0),0) ]
candidate for if(?x_3,?x_4,?x_5):
   [ if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z ]
candidate for zero(?x_1):
   [ zero(0) -> true,
     zero(s(?x)) -> false ]
Find a quasi-ordering ...
order successfully found
Precedence:
 f : Mul;
 if : Mul;
 s : Mul;
 zero : Mul;
 0 : Mul;
 false : Mul,  true : Mul;
Rules:
   [ f(?x) -> if(zero(?x),s(0),0),
     if(true,?y,?z) -> ?y,
     if(false,?y,?z) -> ?z,
     zero(0) -> true,
     zero(s(?x)) -> false ]
Conjectures:
   [ f(0) = 0 ]
STEP 0
ES:
   [ f(0) = 0 ]
HS:
   [ ]
ES0:
   [ s(0) = 0 ]
HS0:
   [ ]
ES1:
   [ s(0) = 0 ]
HS1:
   [ ]
: Success(not GCR)
(7 msec.)