0.00/0.36 YES 0.00/0.36 /export/starexec/sandbox/benchmark/theBenchmark.trs 0.00/0.36 Input rules: 0.00/0.36 [ f(a) -> f(f(a)), 0.00/0.36 a -> b, 0.00/0.36 f(?x:o) -> f(b) ] 0.00/0.36 Sorts having no ground terms: 0.00/0.36 Rules applicable to ground terms: 0.00/0.36 [ f(a) -> f(f(a)), 0.00/0.36 a -> b, 0.00/0.36 f(?x:o) -> f(b) ] 0.00/0.36 Constructor pattern: [f(?x_1),b] 0.00/0.36 Defined pattern: [a] 0.00/0.36 Constructor subsystem: 0.00/0.36 [ f(?x) -> f(b) ] 0.00/0.36 f(?x) -> f(b) 0.00/0.36 {?x:=b} 0.00/0.36 [ {?x:=f(?x_1)} ] 0.00/0.36 Modified Constructor subsystem: 0.00/0.36 [ f(f(?x_1)) -> f(b) ] 0.00/0.36 candidate for a: 0.00/0.36 [ a -> b ] 0.00/0.36 Find a quasi-ordering ... 0.00/0.36 order successfully found 0.00/0.36 Precedence: 0.00/0.36 f : Mul; 0.00/0.36 a : Mul; 0.00/0.36 b : Mul; 0.00/0.36 Rules: 0.00/0.36 [ a -> b, 0.00/0.36 f(f(?x_1)) -> f(b) ] 0.00/0.36 Check confluence of constructor subsystem... 0.00/0.36 Check Termination... 0.00/0.36 Terminating, WCR: CR 0.00/0.36 Conjectures: 0.00/0.36 [ f(a) = f(f(a)) ] 0.00/0.36 STEP 0 0.00/0.36 ES: 0.00/0.36 [ f(a) = f(f(a)) ] 0.00/0.36 HS: 0.00/0.36 [ ] 0.00/0.36 ES0: 0.00/0.36 [ f(b) = f(b) ] 0.00/0.36 HS0: 0.00/0.36 [ ] 0.00/0.36 ES1: 0.00/0.36 [ ] 0.00/0.36 HS1: 0.00/0.36 [ ] 0.00/0.36 : Success(GCR) 0.00/0.36 (4 msec.) 0.00/0.36 0.00/0.36 ============================= 0.00/0.36 Total: 1 Success, 0 Failure: 4 millisec. 0.00/0.36 EOF