YES
(ignored inputs)COMMENT doi:10.1006/jsco.1996.0002 [112] p. 31 ( signature extension and currying do not preserve NFP ) submitted by: Bertram Felgenhauer
input TRS:
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x) -> g,
     f(b,?x) -> g,
     f(c,?x) -> g,
     f(?x,a) -> g,
     f(?x,b) -> g,
     f(?x,c) -> g ]
TRS:
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x) -> g,
     f(b,?x) -> g,
     f(c,?x) -> g,
     f(?x,a) -> g,
     f(?x,b) -> g,
     f(?x,c) -> g ]
unknown Non-Omega-Overlapping
unknown Parallel Closed Conditional Linearization
unknown Strongly Closed Conditional Linearization
unknown Weight-Decreasing Joinable
unknown Right-Reducible
Check distinct normal forms in critical pair closure...failed
Obtained TRSs:
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x) -> g,
     f(b,?x) -> g,
     f(c,?x) -> g,
     f(?x,a) -> g,
     f(?x,b) -> g,
     f(?x,c) -> g,
     c -> b ]
unknown UNC Completion (General)
Check distinct normal forms in critical pair closure...failed
Try to prove CR of the result of UNC completion...
Rewrite Rules:
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x) -> g,
     f(b,?x) -> g,
     f(c,?x) -> g,
     f(?x,a) -> g,
     f(?x,b) -> g,
     f(?x,c) -> g,
     c -> b ]
Apply Direct Methods...
Inner CPs:
   [ f(b,?x_1) = g,
     f(c,?x_1) = g,
     f(b,?x_2) = g,
     f(c,?x_3) = g,
     f(b,?x_3) = g,
     f(?x_4,b) = g,
     f(?x_4,c) = g,
     f(?x_5,b) = g,
     f(?x_6,c) = g,
     f(?x_6,b) = g ]
Outer CPs:
   [ g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     b = c,
     c = b,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g,
     g = g ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
not Left-Linear, Right-Linear
unknown Simple-Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x_1) -> g,
     f(b,?x_2) -> g,
     f(c,?x_3) -> g,
     f(?x_4,a) -> g,
     f(?x_5,b) -> g,
     f(?x_6,c) -> g,
     c -> b ]
Sort Assignment:
 a : =>15
 b : =>15
 c : =>15
 f : 15*15=>16
 g : =>16
non-linear variables: {?x}
non-linear types: {15}
types leq non-linear types: {15}
rules applicable to terms of non-linear types:
   [ a -> b,
     a -> c,
     b -> b,
     c -> c,
     c -> b ]
unknown innermost-termination for terms of non-linear types
unknown Quasi-Left-Linear & Parallel-Closed
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x_1) -> g,
     f(b,?x_2) -> g,
     f(c,?x_3) -> g,
     f(?x_4,a) -> g,
     f(?x_5,b) -> g,
     f(?x_6,c) -> g,
     c -> b ]
Sort Assignment:
 a : =>15
 b : =>15
 c : =>15
 f : 15*15=>16
 g : =>16
non-linear variables: {?x}
non-linear types: {15}
types leq non-linear types: {15}
rules applicable to terms of non-linear types:
   [ a -> b,
     a -> c,
     b -> b,
     c -> c,
     c -> b ]
Rnl:
0: {1,2,3,4,11}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {}
9: {}
10: {}
11: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ f(?x,?x) -> g,
     a -> b,
     a -> c,
     b -> b,
     c -> c,
     f(a,?x_1) -> g,
     f(b,?x_2) -> g,
     f(c,?x_3) -> g,
     f(?x_4,a) -> g,
     f(?x_5,b) -> g,
     f(?x_6,c) -> g,
     c -> b ]
Sort Assignment:
 a : =>15
 b : =>15
 c : =>15
 f : 15*15=>16
 g : =>16
non-linear variables: {?x}
non-linear types: {15}
types leq non-linear types: {15}
rules applicable to terms of non-linear types:
   [ a -> b,
     a -> c,
     b -> b,
     c -> c,
     c -> b ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
Weight-Decreasing Joinable
Direct Methods: CR

Combined result: CR
...CR proof of the result of UNC completion is successful.
problems/525.trs: Success(UNC)
(8 msec.)