Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nosorts_noand_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

There are 103 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  There are 103 ruless (increase limit for explicit display).

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [a__U63(x1,...,x4)]	=	max(x1 + 16, x2 + 22, x3 + 23, x4 + 35, 0)
  [U21(x1, x2)]	=	max(x1 + 17, x2 + 18, 0)
  [a__U82#(x1, x2, x3)]	=	max(x1 + 61, x2 + 60, x3 + 59, 0)
  [a__U72#(x1, x2)]	=	max(x1 + 26, x2 + 23, 0)
  [a__U71#(x1, x2)]	=	max(x1 + 26, x2 + 24, 0)
  [U11(x1, x2, x3)]	=	max(x1 + 43, x2 + 42, x3 + 45, 0)
  [U64(x1, x2)]	=	max(x1 + 0, x2 + 23, 0)
  [s(x1)]	=	x1 + 0
  [a__U31#(x1, x2)]	=	max(x1 + 21, x2 + 24, 0)
  [a__head#(x1)]	=	x1 + 26
  [a__natsFrom#(x1)]	=	x1 + 22
  [a__snd#(x1)]	=	x1 + 5
  [a__afterNth(x1, x2)]	=	max(x1 + 42, x2 + 48, 0)
  [U42(x1, x2, x3)]	=	max(x1 + 62, x2 + 61, x3 + 63, 0)
  [a__U82(x1, x2, x3)]	=	max(x1 + 39, x2 + 38, x3 + 37, 0)
  [take(x1, x2)]	=	max(x1 + 48, x2 + 25586, 0)
  [U71(x1, x2)]	=	max(x1 + 4, x2 + 3, 0)
  [a__U62(x1,...,x4)]	=	max(x1 + 29, x2 + 22, x3 + 29, x4 + 35, 0)
  [pair(x1, x2)]	=	max(x1 + 20, x2 + 27, 0)
  [fst(x1)]	=	x1 + 1
  [natsFrom(x1)]	=	x1 + 18005
  [a__snd(x1)]	=	x1 + 6
  [a__U51#(x1, x2)]	=	max(x1 + 19, x2 + 24, 0)
  [U63(x1,...,x4)]	=	max(x1 + 16, x2 + 22, x3 + 23, x4 + 35, 0)
  [a__U22(x1, x2)]	=	max(x1 + 14, x2 + 1, 0)
  [splitAt(x1, x2)]	=	max(x1 + 22, x2 + 35, 0)
  [a__U64(x1, x2)]	=	max(x1 + 0, x2 + 23, 0)
  [U72(x1, x2)]	=	max(x1 + 4, x2 + 3, 0)
  [a__U11#(x1, x2, x3)]	=	max(x2 + 51, x3 + 42, 0)
  [a__U31(x1, x2)]	=	max(x1 + 7, x2 + 3, 0)
  [a__U51(x1, x2)]	=	max(x1 + 23, x2 + 29, 0)
  [a__U81(x1, x2, x3)]	=	max(x1 + 44, x2 + 46, x3 + 45, 0)
  [a__take#(x1, x2)]	=	max(x1 + 69, x2 + 14033, 0)
  [U12(x1, x2, x3)]	=	max(x1 + 22, x2 + 42, x3 + 41, 0)
  [a__U62#(x1,...,x4)]	=	max(x1 + 34, x2 + 39, x3 + 23, x4 + 37, 0)
  [a__U42#(x1, x2, x3)]	=	max(x1 + 72, x2 + 76, x3 + 74, 0)
  [a__U41(x1, x2, x3)]	=	max(x1 + 55, x2 + 3090, x3 + 63, 0)
  [a__U64#(x1, x2)]	=	max(x1 + 1, x2 + 22, 0)
  [a__U12#(x1, x2, x3)]	=	max(x1 + 16, x2 + 43, x3 + 41, 0)
  [a__U21#(x1, x2)]	=	max(x1 + 39, x2 + 40, 0)
  [a__U81#(x1, x2, x3)]	=	max(x1 + 66, x2 + 68, x3 + 67, 0)
  [a__U61#(x1,...,x4)]	=	max(x1 + 34, x2 + 39, x3 + 23, x4 + 37, 0)
  [a__fst(x1)]	=	x1 + 1
  [a__natsFrom(x1)]	=	x1 + 18005
  [tail(x1)]	=	x1 + 10
  [mark#(x1)]	=	x1 + 22
  [0]	=	4
  [a__U21(x1, x2)]	=	max(x1 + 17, x2 + 18, 0)
  [a__U32(x1, x2)]	=	max(x1 + 5, x2 + 2, 0)
  [sel(x1, x2)]	=	max(x1 + 3090, x2 + 63, 0)
  [afterNth(x1, x2)]	=	max(x1 + 42, x2 + 48, 0)
  [nil]	=	7
  [a__splitAt(x1, x2)]	=	max(x1 + 22, x2 + 35, 0)
  [U62(x1,...,x4)]	=	max(x1 + 29, x2 + 22, x3 + 29, x4 + 35, 0)
  [a__U52#(x1, x2)]	=	max(x2 + 23, 0)
  [a__sel#(x1, x2)]	=	max(x1 + 3112, x2 + 85, 0)
  [mark(x1)]	=	x1 + 0
  [a__U72(x1, x2)]	=	max(x1 + 4, x2 + 3, 0)
  [a__U11(x1, x2, x3)]	=	max(x1 + 43, x2 + 42, x3 + 45, 0)
  [U32(x1, x2)]	=	max(x1 + 5, x2 + 2, 0)
  [a__sel(x1, x2)]	=	max(x1 + 3090, x2 + 63, 0)
  [a__U42(x1, x2, x3)]	=	max(x1 + 62, x2 + 61, x3 + 63, 0)
  [a__U52(x1, x2)]	=	max(x1 + 24, x2 + 1, 0)
  [a__U12(x1, x2, x3)]	=	max(x1 + 22, x2 + 42, x3 + 41, 0)
  [a__U63#(x1,...,x4)]	=	max(x1 + 34, x2 + 39, x3 + 22, x4 + 37, 0)
  [U52(x1, x2)]	=	max(x1 + 24, x2 + 1, 0)
  [U61(x1,...,x4)]	=	max(x1 + 23, x2 + 22, x3 + 30, x4 + 35, 0)
  [a__U22#(x1, x2)]	=	max(x2 + 23, 0)
  [U31(x1, x2)]	=	max(x1 + 7, x2 + 3, 0)
  [a__U71(x1, x2)]	=	max(x1 + 4, x2 + 3, 0)
  [head(x1)]	=	x1 + 15
  [a__afterNth#(x1, x2)]	=	max(x1 + 51, x2 + 69, 0)
  [a__splitAt#(x1, x2)]	=	max(x1 + 39, x2 + 37, 0)
  [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U61(x1,...,x4)]	=	max(x1 + 23, x2 + 22, x3 + 30, x4 + 35, 0)
  [snd(x1)]	=	x1 + 6
  [a__take(x1, x2)]	=	max(x1 + 48, x2 + 25586, 0)
  [U81(x1, x2, x3)]	=	max(x1 + 44, x2 + 46, x3 + 45, 0)
  [a__U41#(x1, x2, x3)]	=	max(x1 + 77, x2 + 76, x3 + 75, 0)
  [U82(x1, x2, x3)]	=	max(x1 + 39, x2 + 38, x3 + 37, 0)
  [tt]	=	5
  [a__fst#(x1)]	=	x1 + 23
  [U22(x1, x2)]	=	max(x1 + 14, x2 + 1, 0)
  [U51(x1, x2)]	=	max(x1 + 23, x2 + 29, 0)
  [a__tail(x1)]	=	x1 + 10
  [U41(x1, x2, x3)]	=	max(x1 + 55, x2 + 3090, x3 + 63, 0)
  [a__tail#(x1)]	=	x1 + 32
  [a__U32#(x1, x2)]	=	max(x1 + 20, x2 + 23, 0)
  [a__head(x1)]	=	x1 + 15

  together with the usable rules

  a__U82(tt,N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(18)
  mark(U82(X1,X2,X3))	→	a__U82(mark(X1),X2,X3)	(50)
  a__U71(X1,X2)	→	U71(X1,X2)	(80)
  a__U22(tt,X)	→	mark(X)	(4)
  a__U71(tt,XS)	→	a__U72(tt,XS)	(15)
  a__U42(tt,N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
  mark(tail(X))	→	a__tail(mark(X))	(54)
  a__U11(tt,N,XS)	→	a__U12(tt,N,XS)	(1)
  a__U62(X1,X2,X3,X4)	→	U62(X1,X2,X3,X4)	(77)
  a__U21(tt,X)	→	a__U22(tt,X)	(3)
  a__U72(tt,XS)	→	mark(XS)	(16)
  a__head(cons(N,XS))	→	a__U31(tt,N)	(21)
  mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(36)
  a__U31(X1,X2)	→	U31(X1,X2)	(68)
  a__natsFrom(X)	→	natsFrom(X)	(85)
  a__splitAt(s(N),cons(X,XS))	→	a__U61(tt,N,X,XS)	(26)
  a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(63)
  a__afterNth(N,XS)	→	a__U11(tt,N,XS)	(19)
  mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(32)
  a__U81(tt,N,XS)	→	a__U82(tt,N,XS)	(17)
  mark(0)	→	0	(60)
  a__tail(cons(N,XS))	→	a__U71(tt,XS)	(27)
  a__tail(X)	→	tail(X)	(87)
  a__fst(X)	→	fst(X)	(84)
  mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(34)
  a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(22)
  a__take(N,XS)	→	a__U81(tt,N,XS)	(28)
  a__splitAt(X1,X2)	→	splitAt(X1,X2)	(65)
  mark(U62(X1,X2,X3,X4))	→	a__U62(mark(X1),X2,X3,X4)	(44)
  a__U31(tt,N)	→	a__U32(tt,N)	(5)
  a__head(X)	→	head(X)	(72)
  mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
  a__snd(X)	→	snd(X)	(64)
  a__U52(tt,Y)	→	mark(Y)	(10)
  mark(head(X))	→	a__head(mark(X))	(39)
  a__U41(tt,N,XS)	→	a__U42(tt,N,XS)	(7)
  a__take(X1,X2)	→	take(X1,X2)	(88)
  a__fst(pair(X,Y))	→	a__U21(tt,X)	(20)
  a__splitAt(0,XS)	→	pair(nil,mark(XS))	(25)
  mark(U81(X1,X2,X3))	→	a__U81(mark(X1),X2,X3)	(49)
  mark(natsFrom(X))	→	a__natsFrom(mark(X))	(52)
  mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(30)
  a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(62)
  a__U64(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(14)
  a__U81(X1,X2,X3)	→	U81(X1,X2,X3)	(82)
  mark(tt)	→	tt	(56)
  a__U64(X1,X2)	→	U64(X1,X2)	(79)
  mark(snd(X))	→	a__snd(mark(X))	(31)
  a__U62(tt,N,X,XS)	→	a__U63(tt,N,X,XS)	(12)
  a__U32(X1,X2)	→	U32(X1,X2)	(69)
  mark(U63(X1,X2,X3,X4))	→	a__U63(mark(X1),X2,X3,X4)	(45)
  a__U63(X1,X2,X3,X4)	→	U63(X1,X2,X3,X4)	(78)
  a__U72(X1,X2)	→	U72(X1,X2)	(81)
  a__sel(N,XS)	→	a__U41(tt,N,XS)	(23)
  a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(70)
  a__snd(pair(X,Y))	→	a__U51(tt,Y)	(24)
  a__U61(X1,X2,X3,X4)	→	U61(X1,X2,X3,X4)	(76)
  mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(57)
  a__U61(tt,N,X,XS)	→	a__U62(tt,N,X,XS)	(11)
  a__U51(tt,Y)	→	a__U52(tt,Y)	(9)
  a__U63(tt,N,X,XS)	→	a__U64(a__splitAt(mark(N),mark(XS)),X)	(13)
  mark(fst(X))	→	a__fst(mark(X))	(51)
  mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(40)
  a__U22(X1,X2)	→	U22(X1,X2)	(67)
  mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(55)
  mark(s(X))	→	s(mark(X))	(59)
  a__U32(tt,N)	→	mark(N)	(6)
  mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(38)
  mark(nil)	→	nil	(61)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(58)
  a__U51(X1,X2)	→	U51(X1,X2)	(74)
  a__U52(X1,X2)	→	U52(X1,X2)	(75)
  mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(48)
  a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(71)
  mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(53)
  mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(47)
  a__afterNth(X1,X2)	→	afterNth(X1,X2)	(73)
  mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(37)
  mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
  mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
  mark(U64(X1,X2))	→	a__U64(mark(X1),X2)	(46)
  a__U21(X1,X2)	→	U21(X1,X2)	(66)
  a__U82(X1,X2,X3)	→	U82(X1,X2,X3)	(83)
  mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(35)
  mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(29)
  mark(U61(X1,X2,X3,X4))	→	a__U61(mark(X1),X2,X3,X4)	(43)
  a__sel(X1,X2)	→	sel(X1,X2)	(86)
  a__U12(tt,N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(2)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  mark#(U41(X1,X2,X3))	→	mark#(X1)	(191)
  mark#(splitAt(X1,X2))	→	mark#(X1)	(189)
  mark#(U63(X1,X2,X3,X4))	→	mark#(X1)	(190)
  mark#(U72(X1,X2))	→	mark#(X1)	(148)
  mark#(snd(X))	→	a__snd#(mark(X))	(146)
  mark#(U63(X1,X2,X3,X4))	→	a__U63#(mark(X1),X2,X3,X4)	(147)
  a__U12#(tt,N,XS)	→	mark#(XS)	(188)
  a__splitAt#(0,XS)	→	mark#(XS)	(144)
  a__U82#(tt,N,XS)	→	mark#(XS)	(187)
  a__U82#(tt,N,XS)	→	mark#(N)	(186)
  mark#(U52(X1,X2))	→	mark#(X1)	(143)
  mark#(U51(X1,X2))	→	a__U51#(mark(X1),X2)	(185)
  a__U11#(tt,N,XS)	→	a__U12#(tt,N,XS)	(141)
  mark#(splitAt(X1,X2))	→	a__splitAt#(mark(X1),mark(X2))	(139)
  mark#(U12(X1,X2,X3))	→	a__U12#(mark(X1),X2,X3)	(140)
  mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(138)
  a__U82#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(136)
  mark#(U21(X1,X2))	→	mark#(X1)	(135)
  mark#(U11(X1,X2,X3))	→	mark#(X1)	(184)
  mark#(pair(X1,X2))	→	mark#(X1)	(133)
  a__U81#(tt,N,XS)	→	a__U82#(tt,N,XS)	(132)
  mark#(splitAt(X1,X2))	→	mark#(X2)	(131)
  a__U12#(tt,N,XS)	→	a__snd#(a__splitAt(mark(N),mark(XS)))	(182)
  mark#(sel(X1,X2))	→	mark#(X2)	(130)
  a__tail#(cons(N,XS))	→	a__U71#(tt,XS)	(181)
  a__U31#(tt,N)	→	a__U32#(tt,N)	(129)
  a__U12#(tt,N,XS)	→	mark#(N)	(180)
  mark#(U51(X1,X2))	→	mark#(X1)	(179)
  a__U42#(tt,N,XS)	→	mark#(N)	(127)
  mark#(U22(X1,X2))	→	mark#(X1)	(126)
  mark#(afterNth(X1,X2))	→	mark#(X2)	(177)
  mark#(U12(X1,X2,X3))	→	mark#(X1)	(125)
  mark#(U32(X1,X2))	→	mark#(X1)	(175)
  a__U82#(tt,N,XS)	→	a__fst#(a__splitAt(mark(N),mark(XS)))	(174)
  mark#(U64(X1,X2))	→	a__U64#(mark(X1),X2)	(123)
  mark#(U31(X1,X2))	→	a__U31#(mark(X1),X2)	(122)
  a__fst#(pair(X,Y))	→	a__U21#(tt,X)	(172)
  mark#(take(X1,X2))	→	mark#(X1)	(170)
  a__U52#(tt,Y)	→	mark#(Y)	(117)
  a__U64#(pair(YS,ZS),X)	→	mark#(ZS)	(116)
  mark#(natsFrom(X))	→	mark#(X)	(115)
  mark#(U61(X1,X2,X3,X4))	→	mark#(X1)	(114)
  mark#(U42(X1,X2,X3))	→	a__U42#(mark(X1),X2,X3)	(167)
  mark#(U81(X1,X2,X3))	→	mark#(X1)	(112)
  mark#(fst(X))	→	mark#(X)	(113)
  a__U72#(tt,XS)	→	mark#(XS)	(166)
  mark#(natsFrom(X))	→	a__natsFrom#(mark(X))	(111)
  mark#(U32(X1,X2))	→	a__U32#(mark(X1),X2)	(165)
  mark#(afterNth(X1,X2))	→	a__afterNth#(mark(X1),mark(X2))	(164)
  a__sel#(N,XS)	→	a__U41#(tt,N,XS)	(108)
  mark#(U62(X1,X2,X3,X4))	→	a__U62#(mark(X1),X2,X3,X4)	(107)
  mark#(sel(X1,X2))	→	mark#(X1)	(163)
  mark#(snd(X))	→	mark#(X)	(106)
  mark#(U42(X1,X2,X3))	→	mark#(X1)	(162)
  mark#(head(X))	→	a__head#(mark(X))	(161)
  a__take#(N,XS)	→	a__U81#(tt,N,XS)	(104)
  a__snd#(pair(X,Y))	→	a__U51#(tt,Y)	(105)
  mark#(tail(X))	→	mark#(X)	(103)
  mark#(U61(X1,X2,X3,X4))	→	a__U61#(mark(X1),X2,X3,X4)	(159)
  a__U22#(tt,X)	→	mark#(X)	(102)
  mark#(U82(X1,X2,X3))	→	mark#(X1)	(101)
  mark#(U62(X1,X2,X3,X4))	→	mark#(X1)	(158)
  mark#(take(X1,X2))	→	mark#(X2)	(157)
  a__U42#(tt,N,XS)	→	a__afterNth#(mark(N),mark(XS))	(155)
  a__U63#(tt,N,X,XS)	→	mark#(N)	(99)
  a__U42#(tt,N,XS)	→	mark#(XS)	(98)
  a__U63#(tt,N,X,XS)	→	mark#(XS)	(97)
  mark#(U31(X1,X2))	→	mark#(X1)	(153)
  mark#(pair(X1,X2))	→	mark#(X2)	(96)
  mark#(head(X))	→	mark#(X)	(95)
  a__U21#(tt,X)	→	a__U22#(tt,X)	(150)
  mark#(U11(X1,X2,X3))	→	a__U11#(mark(X1),X2,X3)	(151)
  mark#(afterNth(X1,X2))	→	mark#(X1)	(93)
  a__U32#(tt,N)	→	mark#(N)	(92)
  a__U51#(tt,Y)	→	a__U52#(tt,Y)	(91)
  a__U12#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(89)
  mark#(U71(X1,X2))	→	mark#(X1)	(149)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    a__splitAt#(s(N),cons(X,XS))	→	a__U61#(tt,N,X,XS)	(94)
    a__U62#(tt,N,X,XS)	→	a__U63#(tt,N,X,XS)	(120)
    a__U61#(tt,N,X,XS)	→	a__U62#(tt,N,X,XS)	(160)
    a__U63#(tt,N,X,XS)	→	a__splitAt#(mark(N),mark(XS))	(118)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the argument filter

    π(a__U71#)	=	2
    π(a__U31#)	=	2
    π(a__natsFrom#)	=	1
    π(fst)	=	1
    π(a__U42#)	=	2
    π(a__fst)	=	1
    π(mark)	=	1

    in combination with the following Weighted Path Order with the following precedence and status

    prec(a__U63)	=	2		status(a__U63)	=	[2, 3]		list-extension(a__U63)	=	Lex
    prec(U21)	=	1		status(U21)	=	[]		list-extension(U21)	=	Lex
    prec(a__U82#)	=	0		status(a__U82#)	=	[1, 2, 3]		list-extension(a__U82#)	=	Lex
    prec(a__U72#)	=	0		status(a__U72#)	=	[1]		list-extension(a__U72#)	=	Lex
    prec(U11)	=	8		status(U11)	=	[]		list-extension(U11)	=	Lex
    prec(U64)	=	2		status(U64)	=	[]		list-extension(U64)	=	Lex
    prec(s)	=	6		status(s)	=	[1]		list-extension(s)	=	Lex
    prec(a__head#)	=	0		status(a__head#)	=	[]		list-extension(a__head#)	=	Lex
    prec(a__snd#)	=	0		status(a__snd#)	=	[]		list-extension(a__snd#)	=	Lex
    prec(a__afterNth)	=	9		status(a__afterNth)	=	[1, 2]		list-extension(a__afterNth)	=	Lex
    prec(U42)	=	1		status(U42)	=	[]		list-extension(U42)	=	Lex
    prec(a__U82)	=	6		status(a__U82)	=	[]		list-extension(a__U82)	=	Lex
    prec(take)	=	7		status(take)	=	[]		list-extension(take)	=	Lex
    prec(U71)	=	7		status(U71)	=	[]		list-extension(U71)	=	Lex
    prec(a__U62)	=	5		status(a__U62)	=	[]		list-extension(a__U62)	=	Lex
    prec(pair)	=	2		status(pair)	=	[]		list-extension(pair)	=	Lex
    prec(natsFrom)	=	5		status(natsFrom)	=	[]		list-extension(natsFrom)	=	Lex
    prec(a__snd)	=	7		status(a__snd)	=	[]		list-extension(a__snd)	=	Lex
    prec(a__U51#)	=	0		status(a__U51#)	=	[]		list-extension(a__U51#)	=	Lex
    prec(U63)	=	2		status(U63)	=	[2, 3]		list-extension(U63)	=	Lex
    prec(a__U22)	=	1		status(a__U22)	=	[]		list-extension(a__U22)	=	Lex
    prec(splitAt)	=	6		status(splitAt)	=	[]		list-extension(splitAt)	=	Lex
    prec(a__U64)	=	2		status(a__U64)	=	[]		list-extension(a__U64)	=	Lex
    prec(U72)	=	6		status(U72)	=	[2]		list-extension(U72)	=	Lex
    prec(a__U11#)	=	0		status(a__U11#)	=	[1]		list-extension(a__U11#)	=	Lex
    prec(a__U31)	=	2		status(a__U31)	=	[2]		list-extension(a__U31)	=	Lex
    prec(a__U51)	=	7		status(a__U51)	=	[]		list-extension(a__U51)	=	Lex
    prec(a__U81)	=	6		status(a__U81)	=	[]		list-extension(a__U81)	=	Lex
    prec(a__take#)	=	0		status(a__take#)	=	[1, 2]		list-extension(a__take#)	=	Lex
    prec(U12)	=	7		status(U12)	=	[2, 3]		list-extension(U12)	=	Lex
    prec(a__U62#)	=	5		status(a__U62#)	=	[1, 2]		list-extension(a__U62#)	=	Lex
    prec(a__U41)	=	2		status(a__U41)	=	[2]		list-extension(a__U41)	=	Lex
    prec(a__U64#)	=	0		status(a__U64#)	=	[1]		list-extension(a__U64#)	=	Lex
    prec(a__U12#)	=	0		status(a__U12#)	=	[2, 1, 3]		list-extension(a__U12#)	=	Lex
    prec(a__U21#)	=	0		status(a__U21#)	=	[2, 1]		list-extension(a__U21#)	=	Lex
    prec(a__U81#)	=	0		status(a__U81#)	=	[2, 3, 1]		list-extension(a__U81#)	=	Lex
    prec(a__U61#)	=	5		status(a__U61#)	=	[1, 2]		list-extension(a__U61#)	=	Lex
    prec(a__natsFrom)	=	5		status(a__natsFrom)	=	[]		list-extension(a__natsFrom)	=	Lex
    prec(tail)	=	7		status(tail)	=	[]		list-extension(tail)	=	Lex
    prec(mark#)	=	0		status(mark#)	=	[]		list-extension(mark#)	=	Lex
    prec(0)	=	7		status(0)	=	[]		list-extension(0)	=	Lex
    prec(a__U21)	=	1		status(a__U21)	=	[]		list-extension(a__U21)	=	Lex
    prec(a__U32)	=	2		status(a__U32)	=	[]		list-extension(a__U32)	=	Lex
    prec(sel)	=	7		status(sel)	=	[2, 1]		list-extension(sel)	=	Lex
    prec(afterNth)	=	9		status(afterNth)	=	[1, 2]		list-extension(afterNth)	=	Lex
    prec(nil)	=	7		status(nil)	=	[]		list-extension(nil)	=	Lex
    prec(a__splitAt)	=	6		status(a__splitAt)	=	[]		list-extension(a__splitAt)	=	Lex
    prec(U62)	=	5		status(U62)	=	[]		list-extension(U62)	=	Lex
    prec(a__U52#)	=	0		status(a__U52#)	=	[]		list-extension(a__U52#)	=	Lex
    prec(a__sel#)	=	0		status(a__sel#)	=	[]		list-extension(a__sel#)	=	Lex
    prec(a__U72)	=	6		status(a__U72)	=	[2]		list-extension(a__U72)	=	Lex
    prec(a__U11)	=	8		status(a__U11)	=	[]		list-extension(a__U11)	=	Lex
    prec(U32)	=	2		status(U32)	=	[]		list-extension(U32)	=	Lex
    prec(a__sel)	=	7		status(a__sel)	=	[2, 1]		list-extension(a__sel)	=	Lex
    prec(a__U42)	=	1		status(a__U42)	=	[]		list-extension(a__U42)	=	Lex
    prec(a__U52)	=	5		status(a__U52)	=	[2, 1]		list-extension(a__U52)	=	Lex
    prec(a__U12)	=	7		status(a__U12)	=	[2, 3]		list-extension(a__U12)	=	Lex
    prec(a__U63#)	=	5		status(a__U63#)	=	[1, 2]		list-extension(a__U63#)	=	Lex
    prec(U52)	=	5		status(U52)	=	[2, 1]		list-extension(U52)	=	Lex
    prec(U61)	=	6		status(U61)	=	[]		list-extension(U61)	=	Lex
    prec(a__U22#)	=	0		status(a__U22#)	=	[2, 1]		list-extension(a__U22#)	=	Lex
    prec(U31)	=	2		status(U31)	=	[2]		list-extension(U31)	=	Lex
    prec(a__U71)	=	7		status(a__U71)	=	[]		list-extension(a__U71)	=	Lex
    prec(head)	=	0		status(head)	=	[1]		list-extension(head)	=	Lex
    prec(a__afterNth#)	=	0		status(a__afterNth#)	=	[]		list-extension(a__afterNth#)	=	Lex
    prec(a__splitAt#)	=	4		status(a__splitAt#)	=	[1]		list-extension(a__splitAt#)	=	Lex
    prec(cons)	=	4		status(cons)	=	[1]		list-extension(cons)	=	Lex
    prec(a__U61)	=	6		status(a__U61)	=	[]		list-extension(a__U61)	=	Lex
    prec(snd)	=	7		status(snd)	=	[]		list-extension(snd)	=	Lex
    prec(a__take)	=	7		status(a__take)	=	[]		list-extension(a__take)	=	Lex
    prec(U81)	=	6		status(U81)	=	[]		list-extension(U81)	=	Lex
    prec(a__U41#)	=	0		status(a__U41#)	=	[2, 3, 1]		list-extension(a__U41#)	=	Lex
    prec(U82)	=	6		status(U82)	=	[]		list-extension(U82)	=	Lex
    prec(tt)	=	3		status(tt)	=	[]		list-extension(tt)	=	Lex
    prec(a__fst#)	=	0		status(a__fst#)	=	[]		list-extension(a__fst#)	=	Lex
    prec(U22)	=	1		status(U22)	=	[]		list-extension(U22)	=	Lex
    prec(U51)	=	7		status(U51)	=	[]		list-extension(U51)	=	Lex
    prec(a__tail)	=	7		status(a__tail)	=	[]		list-extension(a__tail)	=	Lex
    prec(U41)	=	2		status(U41)	=	[2]		list-extension(U41)	=	Lex
    prec(a__tail#)	=	0		status(a__tail#)	=	[]		list-extension(a__tail#)	=	Lex
    prec(a__U32#)	=	0		status(a__U32#)	=	[1, 2]		list-extension(a__U32#)	=	Lex
    prec(a__head)	=	0		status(a__head)	=	[1]		list-extension(a__head)	=	Lex

    and the following Max-polynomial interpretation

    [a__U63(x1,...,x4)]	=	max(x1 + 44589, x2 + 44589, x3 + 44581, x4 + 44586, 0)
    [U21(x1, x2)]	=	x2 + 22290
    [a__U82#(x1, x2, x3)]	=	x1 + x2 + x3 + 1
    [a__U72#(x1, x2)]	=	x1 + 1
    [U11(x1, x2, x3)]	=	x2 + x3 + 48041
    [U64(x1, x2)]	=	max(x1 + 0, x2 + 44581, 0)
    [s(x1)]	=	x1 + 0
    [a__head#(x1)]	=	1
    [a__snd#(x1)]	=	1
    [a__afterNth(x1, x2)]	=	x1 + x2 + 48042
    [U42(x1, x2, x3)]	=	x2 + x3 + 62799
    [a__U82(x1, x2, x3)]	=	x2 + x3 + 44590
    [take(x1, x2)]	=	x1 + x2 + 44592
    [U71(x1, x2)]	=	x2 + 13436
    [a__U62(x1,...,x4)]	=	max(x1 + 44585, x2 + 44589, x3 + 44582, x4 + 44586, 0)
    [pair(x1, x2)]	=	max(x1 + 22290, x2 + 18842, 0)
    [natsFrom(x1)]	=	x1 + 22292
    [a__snd(x1)]	=	x1 + 3450
    [a__U51#(x1, x2)]	=	x1 + 1
    [U63(x1,...,x4)]	=	max(x1 + 44589, x2 + 44589, x3 + 44581, x4 + 44586, 0)
    [a__U22(x1, x2)]	=	x2 + 3916
    [splitAt(x1, x2)]	=	max(x1 + 44589, x2 + 44586, 0)
    [a__U64(x1, x2)]	=	max(x1 + 0, x2 + 44581, 0)
    [U72(x1, x2)]	=	x2 + 13435
    [a__U11#(x1, x2, x3)]	=	x1 + 1
    [a__U31(x1, x2)]	=	x2 + 14757
    [a__U51(x1, x2)]	=	x1 + x2 + 22291
    [a__U81(x1, x2, x3)]	=	x2 + x3 + 44591
    [a__take#(x1, x2)]	=	x1 + x2 + 0
    [U12(x1, x2, x3)]	=	x2 + x3 + 48040
    [a__U62#(x1,...,x4)]	=	max(x1 + 0, x2 + 0, 0)
    [a__U41(x1, x2, x3)]	=	x2 + x3 + 62800
    [a__U64#(x1, x2)]	=	max(x1 + 1, 0)
    [a__U12#(x1, x2, x3)]	=	x1 + x2 + x3 + 1
    [a__U21#(x1, x2)]	=	x1 + x2 + 1
    [a__U81#(x1, x2, x3)]	=	x1 + x2 + x3 + 1
    [a__U61#(x1,...,x4)]	=	max(x1 + 0, x2 + 0, 0)
    [a__natsFrom(x1)]	=	x1 + 22292
    [tail(x1)]	=	x1 + 13437
    [mark#(x1)]	=	1
    [0]	=	18841
    [a__U21(x1, x2)]	=	x2 + 22290
    [a__U32(x1, x2)]	=	x1 + x2 + 14757
    [sel(x1, x2)]	=	x1 + x2 + 62801
    [afterNth(x1, x2)]	=	x1 + x2 + 48042
    [nil]	=	0
    [a__splitAt(x1, x2)]	=	max(x1 + 44589, x2 + 44586, 0)
    [U62(x1,...,x4)]	=	max(x1 + 44585, x2 + 44589, x3 + 44582, x4 + 44586, 0)
    [a__U52#(x1, x2)]	=	1
    [a__sel#(x1, x2)]	=	1
    [a__U72(x1, x2)]	=	x2 + 13435
    [a__U11(x1, x2, x3)]	=	x2 + x3 + 48041
    [U32(x1, x2)]	=	x1 + x2 + 14757
    [a__sel(x1, x2)]	=	x1 + x2 + 62801
    [a__U42(x1, x2, x3)]	=	x2 + x3 + 62799
    [a__U52(x1, x2)]	=	x1 + x2 + 1
    [a__U12(x1, x2, x3)]	=	x2 + x3 + 48040
    [a__U63#(x1,...,x4)]	=	max(x1 + 0, x2 + 0, 0)
    [U52(x1, x2)]	=	x1 + x2 + 1
    [U61(x1,...,x4)]	=	max(x1 + 44583, x2 + 44589, x3 + 44584, x4 + 44586, 0)
    [a__U22#(x1, x2)]	=	x1 + x2 + 1
    [U31(x1, x2)]	=	x2 + 14757
    [a__U71(x1, x2)]	=	x2 + 13436
    [head(x1)]	=	x1 + 14756
    [a__afterNth#(x1, x2)]	=	x2 + 0
    [a__splitAt#(x1, x2)]	=	max(x1 + 0, 0)
    [cons(x1, x2)]	=	max(x1 + 22291, x2 + 0, 0)
    [a__U61(x1,...,x4)]	=	max(x1 + 44583, x2 + 44589, x3 + 44584, x4 + 44586, 0)
    [snd(x1)]	=	x1 + 3450
    [a__take(x1, x2)]	=	x1 + x2 + 44592
    [U81(x1, x2, x3)]	=	x2 + x3 + 44591
    [a__U41#(x1, x2, x3)]	=	x1 + x2 + x3 + 0
    [U82(x1, x2, x3)]	=	x2 + x3 + 44590
    [tt]	=	0
    [a__fst#(x1)]	=	1
    [U22(x1, x2)]	=	x2 + 3916
    [U51(x1, x2)]	=	x1 + x2 + 22291
    [a__tail(x1)]	=	x1 + 13437
    [U41(x1, x2, x3)]	=	x2 + x3 + 62800
    [a__tail#(x1)]	=	1
    [a__U32#(x1, x2)]	=	x1 + x2 + 1
    [a__head(x1)]	=	x1 + 14756

    together with the usable rules

    a__U82(tt,N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(18)
    mark(U82(X1,X2,X3))	→	a__U82(mark(X1),X2,X3)	(50)
    a__U71(X1,X2)	→	U71(X1,X2)	(80)
    a__U22(tt,X)	→	mark(X)	(4)
    a__U71(tt,XS)	→	a__U72(tt,XS)	(15)
    a__U42(tt,N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(8)
    mark(tail(X))	→	a__tail(mark(X))	(54)
    a__U11(tt,N,XS)	→	a__U12(tt,N,XS)	(1)
    a__U62(X1,X2,X3,X4)	→	U62(X1,X2,X3,X4)	(77)
    a__U21(tt,X)	→	a__U22(tt,X)	(3)
    a__U72(tt,XS)	→	mark(XS)	(16)
    a__head(cons(N,XS))	→	a__U31(tt,N)	(21)
    mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(36)
    a__U31(X1,X2)	→	U31(X1,X2)	(68)
    a__natsFrom(X)	→	natsFrom(X)	(85)
    a__splitAt(s(N),cons(X,XS))	→	a__U61(tt,N,X,XS)	(26)
    a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(63)
    a__afterNth(N,XS)	→	a__U11(tt,N,XS)	(19)
    mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(32)
    a__U81(tt,N,XS)	→	a__U82(tt,N,XS)	(17)
    mark(0)	→	0	(60)
    a__tail(cons(N,XS))	→	a__U71(tt,XS)	(27)
    a__tail(X)	→	tail(X)	(87)
    a__fst(X)	→	fst(X)	(84)
    mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(34)
    a__natsFrom(N)	→	cons(mark(N),natsFrom(s(N)))	(22)
    a__take(N,XS)	→	a__U81(tt,N,XS)	(28)
    a__splitAt(X1,X2)	→	splitAt(X1,X2)	(65)
    mark(U62(X1,X2,X3,X4))	→	a__U62(mark(X1),X2,X3,X4)	(44)
    a__U31(tt,N)	→	a__U32(tt,N)	(5)
    a__head(X)	→	head(X)	(72)
    mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
    a__snd(X)	→	snd(X)	(64)
    a__U52(tt,Y)	→	mark(Y)	(10)
    mark(head(X))	→	a__head(mark(X))	(39)
    a__U41(tt,N,XS)	→	a__U42(tt,N,XS)	(7)
    a__take(X1,X2)	→	take(X1,X2)	(88)
    a__fst(pair(X,Y))	→	a__U21(tt,X)	(20)
    a__splitAt(0,XS)	→	pair(nil,mark(XS))	(25)
    mark(U81(X1,X2,X3))	→	a__U81(mark(X1),X2,X3)	(49)
    mark(natsFrom(X))	→	a__natsFrom(mark(X))	(52)
    mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(30)
    a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(62)
    a__U64(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(14)
    a__U81(X1,X2,X3)	→	U81(X1,X2,X3)	(82)
    mark(tt)	→	tt	(56)
    a__U64(X1,X2)	→	U64(X1,X2)	(79)
    mark(snd(X))	→	a__snd(mark(X))	(31)
    a__U62(tt,N,X,XS)	→	a__U63(tt,N,X,XS)	(12)
    a__U32(X1,X2)	→	U32(X1,X2)	(69)
    mark(U63(X1,X2,X3,X4))	→	a__U63(mark(X1),X2,X3,X4)	(45)
    a__U63(X1,X2,X3,X4)	→	U63(X1,X2,X3,X4)	(78)
    a__U72(X1,X2)	→	U72(X1,X2)	(81)
    a__sel(N,XS)	→	a__U41(tt,N,XS)	(23)
    a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(70)
    a__snd(pair(X,Y))	→	a__U51(tt,Y)	(24)
    a__U61(X1,X2,X3,X4)	→	U61(X1,X2,X3,X4)	(76)
    mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(57)
    a__U61(tt,N,X,XS)	→	a__U62(tt,N,X,XS)	(11)
    a__U51(tt,Y)	→	a__U52(tt,Y)	(9)
    a__U63(tt,N,X,XS)	→	a__U64(a__splitAt(mark(N),mark(XS)),X)	(13)
    mark(fst(X))	→	a__fst(mark(X))	(51)
    mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(40)
    a__U22(X1,X2)	→	U22(X1,X2)	(67)
    mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(55)
    mark(s(X))	→	s(mark(X))	(59)
    a__U32(tt,N)	→	mark(N)	(6)
    mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(38)
    mark(nil)	→	nil	(61)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(58)
    a__U51(X1,X2)	→	U51(X1,X2)	(74)
    a__U52(X1,X2)	→	U52(X1,X2)	(75)
    mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(48)
    a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(71)
    mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(53)
    mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(47)
    a__afterNth(X1,X2)	→	afterNth(X1,X2)	(73)
    mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(37)
    mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
    mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
    mark(U64(X1,X2))	→	a__U64(mark(X1),X2)	(46)
    a__U21(X1,X2)	→	U21(X1,X2)	(66)
    a__U82(X1,X2,X3)	→	U82(X1,X2,X3)	(83)
    mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(35)
    mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(29)
    mark(U61(X1,X2,X3,X4))	→	a__U61(mark(X1),X2,X3,X4)	(43)
    a__sel(X1,X2)	→	sel(X1,X2)	(86)
    a__U12(tt,N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(2)

    (w.r.t. the implicit argument filter of the reduction pair), the pairs

    a__splitAt#(s(N),cons(X,XS))	→	a__U61#(tt,N,X,XS)	(94)
    a__U63#(tt,N,X,XS)	→	a__splitAt#(mark(N),mark(XS))	(118)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.

  • The 2^nd component contains the pair

    mark#(s(X))	→	mark#(X)	(145)
    mark#(cons(X1,X2))	→	mark#(X1)	(173)
    mark#(U64(X1,X2))	→	mark#(X1)	(137)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [a__U63(x1,...,x4)]	=	x1 + x4 + 3762
    [U21(x1, x2)]	=	x2 + 1
    [a__U82#(x1, x2, x3)]	=	0
    [a__U72#(x1, x2)]	=	0
    [a__U71#(x1, x2)]	=	0
    [U11(x1, x2, x3)]	=	1210
    [U64(x1, x2)]	=	x1 + 1512
    [s(x1)]	=	x1 + 1
    [a__U31#(x1, x2)]	=	0
    [a__head#(x1)]	=	0
    [a__natsFrom#(x1)]	=	0
    [a__snd#(x1)]	=	0
    [a__afterNth(x1, x2)]	=	x1 + x2 + 0
    [U42(x1, x2, x3)]	=	x3 + 2248
    [a__U82(x1, x2, x3)]	=	x2 + x3 + 3136
    [take(x1, x2)]	=	3
    [U71(x1, x2)]	=	x2 + 53433
    [a__U62(x1,...,x4)]	=	x1 + x3 + 3761
    [pair(x1, x2)]	=	x1 + x2 + 1
    [fst(x1)]	=	23202
    [natsFrom(x1)]	=	x1 + 27018
    [a__snd(x1)]	=	x1 + 1162
    [a__U51#(x1, x2)]	=	0
    [U63(x1,...,x4)]	=	x3 + x4 + 3761
    [a__U22(x1, x2)]	=	x1 + 3
    [splitAt(x1, x2)]	=	x1 + 887
    [a__U64(x1, x2)]	=	x2 + 3764
    [U72(x1, x2)]	=	x1 + x2 + 28312
    [a__U11#(x1, x2, x3)]	=	0
    [a__U31(x1, x2)]	=	2249
    [a__U51(x1, x2)]	=	x1 + 1163
    [a__U81(x1, x2, x3)]	=	3135
    [a__take#(x1, x2)]	=	0
    [U12(x1, x2, x3)]	=	1214
    [a__U62#(x1,...,x4)]	=	4
    [a__U42#(x1, x2, x3)]	=	0
    [a__U41(x1, x2, x3)]	=	x2 + 2246
    [a__U64#(x1, x2)]	=	0
    [a__U12#(x1, x2, x3)]	=	0
    [a__U21#(x1, x2)]	=	0
    [a__U81#(x1, x2, x3)]	=	0
    [a__U61#(x1,...,x4)]	=	4
    [a__fst(x1)]	=	x1 + 0
    [a__natsFrom(x1)]	=	x1 + 27019
    [tail(x1)]	=	x1 + 51179
    [mark#(x1)]	=	x1 + 0
    [0]	=	1373
    [a__U21(x1, x2)]	=	x1 + 2
    [a__U32(x1, x2)]	=	x1 + 2249
    [sel(x1, x2)]	=	2246
    [afterNth(x1, x2)]	=	147
    [nil]	=	25477
    [a__splitAt(x1, x2)]	=	x2 + 886
    [U62(x1,...,x4)]	=	x2 + x4 + 1898
    [a__U52#(x1, x2)]	=	0
    [a__sel#(x1, x2)]	=	0
    [mark(x1)]	=	x1 + 2251
    [a__U72(x1, x2)]	=	53433
    [a__U11(x1, x2, x3)]	=	x1 + x3 + 1211
    [U32(x1, x2)]	=	x2 + 2250
    [a__sel(x1, x2)]	=	x1 + x2 + 2245
    [a__U42(x1, x2, x3)]	=	x2 + 2247
    [a__U52(x1, x2)]	=	x1 + x2 + 2150
    [a__U12(x1, x2, x3)]	=	x2 + 1213
    [a__U63#(x1,...,x4)]	=	4
    [U52(x1, x2)]	=	x2 + 2149
    [U61(x1,...,x4)]	=	x1 + x3 + x4 + 1509
    [a__U22#(x1, x2)]	=	0
    [U31(x1, x2)]	=	x1 + 2250
    [a__U71(x1, x2)]	=	53432
    [head(x1)]	=	x1 + 2249
    [a__afterNth#(x1, x2)]	=	0
    [a__splitAt#(x1, x2)]	=	2
    [cons(x1, x2)]	=	x1 + x2 + 1047
    [a__U61(x1,...,x4)]	=	x2 + 3761
    [snd(x1)]	=	1161
    [a__take(x1, x2)]	=	x1 + x2 + 0
    [U81(x1, x2, x3)]	=	x1 + 883
    [a__U41#(x1, x2, x3)]	=	0
    [U82(x1, x2, x3)]	=	x1 + 3137
    [tt]	=	1
    [a__fst#(x1)]	=	0
    [U22(x1, x2)]	=	x2 + 2
    [U51(x1, x2)]	=	1162
    [a__tail(x1)]	=	53431
    [U41(x1, x2, x3)]	=	x3 + 2247
    [a__tail#(x1)]	=	0
    [a__U32#(x1, x2)]	=	0
    [a__head(x1)]	=	2248

    having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

    mark#(s(X))	→	mark#(X)	(145)
    mark#(cons(X1,X2))	→	mark#(X1)	(173)
    mark#(U64(X1,X2))	→	mark#(X1)	(137)

    could be deleted.

    1.1.1.1.2.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.