0.00/0.03 NO 0.00/0.03 /export/starexec/sandbox/benchmark/theBenchmark.trs 0.00/0.03 Input rules: 0.00/0.03 [ zero(0) -> true, 0.00/0.03 zero(s(?x:Nat)) -> false, 0.00/0.03 if(true,?y:Nat,?z:Nat) -> ?y:Nat, 0.00/0.03 if(false,?y:Nat,?z:Nat) -> ?z:Nat, 0.00/0.03 f(0) -> 0, 0.00/0.03 f(?x:Nat) -> if(zero(?x:Nat),s(0),0) ] 0.00/0.03 Sorts having no ground terms: 0.00/0.03 Rules applicable to ground terms: 0.00/0.03 [ zero(0) -> true, 0.00/0.03 zero(s(?x:Nat)) -> false, 0.00/0.03 if(true,?y:Nat,?z:Nat) -> ?y:Nat, 0.00/0.03 if(false,?y:Nat,?z:Nat) -> ?z:Nat, 0.00/0.03 f(0) -> 0, 0.00/0.03 f(?x:Nat) -> if(zero(?x:Nat),s(0),0) ] 0.00/0.03 Constructor pattern: [s(?x_1),0,true,false] 0.00/0.03 Defined pattern: [f(?x_1),if(?x_3,?x_4,?x_5),zero(?x_1)] 0.00/0.03 Constructor subsystem: 0.00/0.03 [ ] 0.00/0.03 Modified Constructor subsystem: 0.00/0.03 [ ] 0.00/0.03 candidate for f(?x_1): 0.00/0.03 [ f(?x) -> if(zero(?x),s(0),0) ] 0.00/0.03 candidate for if(?x_3,?x_4,?x_5): 0.00/0.03 [ if(true,?y,?z) -> ?y, 0.00/0.03 if(false,?y,?z) -> ?z ] 0.00/0.03 candidate for zero(?x_1): 0.00/0.03 [ zero(0) -> true, 0.00/0.03 zero(s(?x)) -> false ] 0.00/0.03 Find a quasi-ordering ... 0.00/0.03 order successfully found 0.00/0.03 Precedence: 0.00/0.03 f : Mul; 0.00/0.03 zero : Mul; 0.00/0.03 true : Mul; 0.00/0.03 s : Mul; 0.00/0.03 false : Mul; 0.00/0.03 if : Mul; 0.00/0.03 0 : Mul; 0.00/0.03 Rules: 0.00/0.03 [ f(?x) -> if(zero(?x),s(0),0), 0.00/0.03 if(true,?y,?z) -> ?y, 0.00/0.03 if(false,?y,?z) -> ?z, 0.00/0.03 zero(0) -> true, 0.00/0.03 zero(s(?x)) -> false ] 0.00/0.03 Conjectures: 0.00/0.03 [ f(0) = 0 ] 0.00/0.03 STEP 0 0.00/0.03 ES: 0.00/0.03 [ f(0) = 0 ] 0.00/0.03 HS: 0.00/0.03 [ ] 0.00/0.03 ES0: 0.00/0.03 [ s(0) = 0 ] 0.00/0.03 HS0: 0.00/0.03 [ ] 0.00/0.03 ES1: 0.00/0.03 [ s(0) = 0 ] 0.00/0.03 HS1: 0.00/0.03 [ ] 0.00/0.03 : Success(not GCR) 0.00/0.03 (6 msec.) 0.00/0.03 0.00/0.03 ============================= 0.00/0.03 Total: 1 Success, 0 Failure: 7 millisec. 0.00/0.03 EOF