(ignored inputs)COMMENT from p.208 of \cite{Klo80} Rewrite Rules: [ 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(Ap(Ds,?z),?z) -> E ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix not Left-Linear, not Right-Linear unknown Strongly Depth-Preserving & Non-E-Overlapping check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ 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(Ap(Ds,?z),?z) -> E ] Sort Assignment: E : =>16 I : =>16 K : =>16 S : =>16 Ap : 16*16=>16 Ds : =>16 maximal types: {16} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ 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(Ap(Ds,?z),?z) -> E ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ 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(Ap(Ds,?z),?z) -> E ] Commutative Decomposition failed (not left-linear): Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/57.trs: Failure(unknown) (46 msec.)