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