0.00/0.16 NO 0.00/0.16 /export/starexec/sandbox2/benchmark/theBenchmark.trs 0.00/0.16 Input rules: 0.00/0.16 [ a -> b, 0.00/0.16 f(g(a)) -> f(a) ] 0.00/0.16 Sorts having no ground terms: 0.00/0.16 Rules applicable to ground terms: 0.00/0.16 [ a -> b, 0.00/0.16 f(g(a)) -> f(a) ] 0.00/0.16 Constructor pattern: [b,f(?x_1),g(?x_1)] 0.00/0.16 Defined pattern: [a] 0.00/0.16 Constructor subsystem: 0.00/0.16 [ ] 0.00/0.16 Modified Constructor subsystem: 0.00/0.16 [ ] 0.00/0.16 candidate for a: 0.00/0.16 [ a -> b ] 0.00/0.16 Find a quasi-ordering ... 0.00/0.16 order successfully found 0.00/0.16 Precedence: 0.00/0.16 a : Mul; 0.00/0.16 b : Mul; 0.00/0.16 f : Mul, g : Mul; 0.00/0.16 Rules: 0.00/0.16 [ a -> b ] 0.00/0.16 Conjectures: 0.00/0.16 [ f(g(a)) = f(a) ] 0.00/0.16 STEP 0 0.00/0.16 ES: 0.00/0.16 [ f(g(a)) = f(a) ] 0.00/0.16 HS: 0.00/0.16 [ ] 0.00/0.16 ES0: 0.00/0.16 [ f(g(b)) = f(b) ] 0.00/0.16 HS0: 0.00/0.16 [ ] 0.00/0.16 ES1: 0.00/0.16 [ f(g(b)) = f(b) ] 0.00/0.16 HS1: 0.00/0.16 [ ] 0.00/0.16 No equation to expand 0.00/0.16 check Non-Ground-Confluence... 0.00/0.16 ground constructor terms for instantiation: {b,f(b),g(b)} 0.00/0.16 ground terms for instantiation: {b:o,f(b):o,g(b):o} 0.00/0.16 obtain 3 rules by 3 steps unfolding 0.00/0.16 obtain 3 candidates for checking non-joinability 0.00/0.16 check by TCAP-Approximation (success) 0.00/0.16 Witness for Non-Confluence: f(b)> 0.00/0.16 : Success(not GCR) 0.00/0.16 (4 msec.) 0.00/0.16 0.00/0.16 ============================= 0.00/0.16 Total: 1 Success, 0 Failure: 5 millisec. 0.00/0.16 EOF