MAYBE
(ignored inputs)COMMENT cops number: 58 submitted by: Takahito Aoto , Junichi Yoshida , Yoshihito Toyama [14] p. 208
input TRS:
   [ D : 0,
     I : 0,
     K : 0,
     S : 0,
     Ap : 2,
     D0 : 0,
     D1 : 0 ]
   [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)),
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(I,?x) -> ?x,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
unknown Strongly Non-Overlapping
unknown Right-Reducible
Check distinct normal forms in critical pair closure...failed
UNR Proof by the Knuth-Bendix criterion
checking TRS:
   [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)),
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(I,?x) -> ?x,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z ]
containing trivial rules..remove trivial rules and forget nonUNR
not Overlay, check Termination...
unknown/not Terminating...failed

UNR proof by Transformation (Strongly Closed)
Not linear, apply linear-approximation if possible
Approximation failed...
UNR proof by Transformation (Parallel Closed)
Not left-linear, apply linear-approximation if possible
Approximation failed...
UNR proof by Collapse Mapping
...failed
UNR proof by SRR elimination
...failed
Try to prove CR of the approximated TRS...
Rewrite Rules:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_1),?z1_1))),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) = Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) = Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)),
     Ap(Ap(D,?z0_4),?z1_4) = Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),Ap(D1,Ap(Ap(D,?z0),?z1))) = Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) = Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)),
     Ap(Ap(D,?z0_3),?z1_3) = Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_3),?z1_3))),?z1_3) = Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,?z0_4),Ap(D1,Ap(Ap(D,?z0_4),?z1_4))) = Ap(Ap(D,?z0_4),?z1_4),
     Ap(D1,Ap(Ap(D,?z0),?z1)) = ?z1,
     Ap(D1,Ap(Ap(D,?z0_1),?z1_1)) = Ap(D1,Ap(Ap(D,?z0_1),?z1_1)),
     Ap(D1,?z_2) = Ap(D1,?z_2),
     Ap(D0,Ap(Ap(D,?z0),?z1)) = Ap(D0,Ap(Ap(D,?z0),?z1)),
     Ap(D0,Ap(Ap(D,?z0_1),?z1_1)) = ?z0_1,
     Ap(D0,?z_2) = Ap(D0,?z_2),
     Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) = Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1),
     Ap(Ap(D,?z0),Ap(D1,Ap(Ap(D,?z0),?z1))) = Ap(Ap(D,?z0),Ap(D1,Ap(Ap(D,?z0),?z1))) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
not Left-Linear, not 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
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
Sort Assignment:
 D : =>25
 I : =>25
 K : =>25
 S : =>25
 Ap : 25*25=>25
 D0 : =>25
 D1 : =>25
non-linear variables: {?z1,?z0_1,?z_2}
non-linear types: {25}
types leq non-linear types: {25}
rules applicable to terms of non-linear types:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
unknown innermost-termination for terms of non-linear types
unknown Quasi-Left-Linear & Parallel-Closed
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
Sort Assignment:
 D : =>25
 I : =>25
 K : =>25
 S : =>25
 Ap : 25*25=>25
 D0 : =>25
 D1 : =>25
non-linear variables: {?z1,?z0_1,?z_2,?z_7}
non-linear types: {25}
types leq non-linear types: {25}
rules applicable to terms of non-linear types:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
Rnl:
0: {0,1,2,3,4,5,6,7}
1: {0,1,2,3,4,5,6,7}
2: {0,1,2,3,4,5,6,7}
3: {}
4: {}
5: {}
6: {}
7: {0,1,2,3,4,5,6,7}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
Sort Assignment:
 D : =>25
 I : =>25
 K : =>25
 S : =>25
 Ap : 25*25=>25
 D0 : =>25
 D1 : =>25
non-linear variables: {?z1,?z0_1,?z_2,?z_7}
non-linear types: {25}
types leq non-linear types: {25}
rules applicable to terms of non-linear types:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0),?z1))),?z1) -> Ap(Ap(D,?z0),?z1),
     Ap(Ap(D,?z0_1),Ap(D1,Ap(Ap(D,?z0_1),?z1_1))) -> Ap(Ap(D,?z0_1),?z1_1),
     Ap(Ap(D,Ap(D0,?z_2)),Ap(D1,?z_2)) -> ?z_2,
     Ap(D1,Ap(Ap(D,?z0_3),?z1_3)) -> ?z1_3,
     Ap(D0,Ap(Ap(D,?z0_4),?z1_4)) -> ?z0_4,
     Ap(I,?x_5) -> ?x_5,
     Ap(Ap(K,?x_6),?y_6) -> ?x_6,
     Ap(Ap(Ap(S,?x_7),?y_7),?z_7) -> Ap(Ap(?x_7,?z_7),Ap(?y_7,?z_7)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check by Ordered Rewriting...
remove redundants rules and split
R-part:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
E-part:
   [ ]
...failed to find a suitable LPO.
unknown Confluence by Ordered Rewriting
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
Sort Assignment:
 D : =>25
 I : =>25
 K : =>25
 S : =>25
 Ap : 25*25=>25
 D0 : =>25
 D1 : =>25
maximal types: {25}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
Commutative Decomposition failed (not left-linear): Can't judge
No further decomposition possible


Combined result: Can't judge
...CR proof of approximated TRS failed
Try to prove UNC of the approximated TRS...
input TRS:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
Try persistent and layer-preserving decomposition...
Sort Assignment:
 D : =>25
 I : =>25
 K : =>25
 S : =>25
 Ap : 25*25=>25
 D0 : =>25
 D1 : =>25
maximal types: {25}
...decomposition failed.
TRS:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
unknown Non-Omega-Overlapping
unknown Parallel Closed Conditional Linearization
unknown Strongly Closed Conditional Linearization
unknown Right-Reducible
Check distinct normal forms in critical pair closure...failed
Obtained TRSs:
   [ Ap(Ap(D,Ap(D0,Ap(Ap(D,?z0_4),?z1_4))),?z1_4) -> Ap(Ap(D,?z0_4),?z1_4),
     Ap(Ap(D,?z0_3),Ap(D1,Ap(Ap(D,?z0_3),?z1_3))) -> Ap(Ap(D,?z0_3),?z1_3),
     Ap(Ap(D,Ap(D0,?z)),Ap(D1,?z)) -> ?z,
     Ap(D1,Ap(Ap(D,?z0),?z1)) -> ?z1,
     Ap(D0,Ap(Ap(D,?z0),?z1)) -> ?z0,
     Ap(I,?x) -> ?x,
     Ap(Ap(K,?x),?y) -> ?x,
     Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)) ]
unknown UNC Completion (General)
Check distinct normal forms in critical pair closure...failed
...UNC proof of approximated TRS failed
cops-IcvZ6bPr.trs: Failure(unknown UNR)
(199 msec.)