Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4970)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by matchbox @ termCOMP 2023)

1 Dependency Pair Transformation

There are 166 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

  5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
  5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
  5#(5(x1))	→	5#(2(1(x1)))	(24)
  5#(5(x1))	→	4#(x1)	(25)
  4#(5(5(5(x1))))	→	2#(1(0(5(x1))))	(97)
  2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
  5#(5(x1))	→	4#(5(2(1(x1))))	(26)
  4#(5(5(5(x1))))	→	0#(5(x1))	(102)
  0#(1(5(5(5(3(5(x1)))))))	→	5#(1(0(1(2(0(5(x1)))))))	(181)
  5#(5(x1))	→	4#(4(0(4(x1))))	(27)
  4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
  5#(5(x1))	→	4#(1(1(1(1(4(4(0(4(x1)))))))))	(28)
  4#(5(2(4(x1))))	→	4#(1(5(5(2(0(3(1(3(3(x1))))))))))	(106)
  4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
  5#(5(x1))	→	4#(0(4(x1)))	(29)
  4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
  5#(5(x1))	→	4#(0(2(5(4(5(2(1(x1))))))))	(30)
  4#(4(5(2(4(2(2(x1)))))))	→	5#(1(2(2(1(x1)))))	(113)
  5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
  2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
  4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
  4#(4(5(2(4(2(2(x1)))))))	→	4#(0(5(5(4(5(1(2(2(1(x1))))))))))	(115)
  4#(4(5(2(4(2(2(x1)))))))	→	2#(2(1(x1)))	(116)
  2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
  4#(4(5(2(4(2(2(x1)))))))	→	2#(1(x1))	(117)
  2#(5(5(x1)))	→	4#(0(0(1(1(2(x1))))))	(138)
  4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
  0#(1(5(5(5(3(5(x1)))))))	→	2#(5(1(0(1(2(0(5(x1))))))))	(182)
  2#(5(5(x1)))	→	2#(x1)	(139)
  2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
  2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
  0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
  2#(5(5(x1)))	→	0#(0(1(1(2(x1)))))	(144)
  0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
  0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
  2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
  4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
  4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
  2#(5(5(3(4(x1)))))	→	4#(0(2(4(4(x1)))))	(149)
  2#(5(5(3(4(x1)))))	→	2#(4(4(x1)))	(150)
  2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
  2#(5(0(4(x1))))	→	5#(1(0(0(x1))))	(153)
  5#(5(x1))	→	2#(1(x1))	(32)
  2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
  2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
  2#(5(0(4(x1))))	→	2#(4(4(5(1(0(0(x1)))))))	(158)
  2#(5(0(4(x1))))	→	0#(x1)	(160)
  2#(5(0(4(x1))))	→	0#(0(x1))	(161)
  5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
  5#(5(x1))	→	0#(4(x1))	(39)
  5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
  5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
  5#(5(5(x1)))	→	4#(5(0(0(x1))))	(43)
  5#(5(5(x1)))	→	4#(1(0(1(4(5(0(0(x1))))))))	(44)
  5#(5(5(x1)))	→	0#(x1)	(47)
  5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
  5#(5(5(x1)))	→	0#(0(x1))	(49)
  5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
  5#(5(5(1(4(x1)))))	→	4#(0(x1))	(53)
  5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
  5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
  5#(5(3(x1)))	→	5#(0(x1))	(58)
  5#(5(3(x1)))	→	4#(4(1(0(1(5(0(x1)))))))	(59)
  5#(5(3(x1)))	→	4#(1(0(1(5(0(x1))))))	(60)
  5#(5(3(x1)))	→	0#(x1)	(63)
  5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
  5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
  5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
  5#(5(2(4(5(0(x1))))))	→	4#(0(4(2(0(x1)))))	(74)
  5#(5(2(4(5(0(x1))))))	→	2#(4(0(4(2(0(x1))))))	(75)
  5#(5(2(4(5(0(x1))))))	→	2#(1(1(4(2(4(0(4(2(0(x1))))))))))	(76)
  5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
  5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
  5#(2(5(5(0(4(x1))))))	→	5#(2(1(4(4(x1)))))	(81)
  5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
  5#(2(5(5(0(4(x1))))))	→	2#(1(4(4(x1))))	(85)
  5#(2(4(x1)))	→	4#(2(x1))	(89)
  5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
  5#(2(4(x1)))	→	2#(x1)	(91)
  5#(2(4(x1)))	→	2#(4(2(x1)))	(92)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

  [5(x1)]	=	0 0 0 0 · x1 + -∞ -∞
  [4(x1)]	=	0 0 0 0 · x1 + -∞ -∞
  [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
  [2(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
  [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
  [0(x1)]	=	0 0 0 0 · x1 + -∞ -∞
  [5#(x1)]	=	14 16 14 16 · x1 + -∞ -∞
  [4#(x1)]	=	15 16 15 16 · x1 + -∞ -∞
  [2#(x1)]	=	15 16 15 16 · x1 + -∞ -∞
  [0#(x1)]	=	16 16 16 16 · x1 + -∞ -∞

  together with the usable rules

  5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
  5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
  2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
  5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
  5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
  5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
  5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
  2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
  4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
  4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
  0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
  2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
  5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
  0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
  1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
  4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
  4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
  5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
  5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
  0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
  4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

  5#(5(x1))	→	5#(2(1(x1)))	(24)
  4#(5(5(5(x1))))	→	2#(1(0(5(x1))))	(97)
  0#(1(5(5(5(3(5(x1)))))))	→	5#(1(0(1(2(0(5(x1)))))))	(181)
  5#(5(x1))	→	4#(1(1(1(1(4(4(0(4(x1)))))))))	(28)
  4#(5(2(4(x1))))	→	4#(1(5(5(2(0(3(1(3(3(x1))))))))))	(106)
  4#(4(5(2(4(2(2(x1)))))))	→	5#(1(2(2(1(x1)))))	(113)
  4#(4(5(2(4(2(2(x1)))))))	→	2#(2(1(x1)))	(116)
  4#(4(5(2(4(2(2(x1)))))))	→	2#(1(x1))	(117)
  2#(5(0(4(x1))))	→	5#(1(0(0(x1))))	(153)
  5#(5(x1))	→	2#(1(x1))	(32)
  5#(5(5(x1)))	→	4#(1(0(1(4(5(0(0(x1))))))))	(44)
  5#(5(3(x1)))	→	4#(1(0(1(5(0(x1))))))	(60)
  5#(5(2(4(5(0(x1))))))	→	2#(1(1(4(2(4(0(4(2(0(x1))))))))))	(76)
  5#(2(5(5(0(4(x1))))))	→	5#(2(1(4(4(x1)))))	(81)
  5#(2(5(5(0(4(x1))))))	→	2#(1(4(4(x1))))	(85)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
    5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
    5#(5(x1))	→	4#(x1)	(25)
    4#(5(5(5(x1))))	→	0#(5(x1))	(102)
    0#(1(5(5(5(3(5(x1)))))))	→	2#(5(1(0(1(2(0(5(x1))))))))	(182)
    2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
    5#(5(x1))	→	4#(5(2(1(x1))))	(26)
    4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
    5#(5(x1))	→	4#(4(0(4(x1))))	(27)
    4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
    5#(5(x1))	→	4#(0(4(x1)))	(29)
    4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
    5#(5(x1))	→	4#(0(2(5(4(5(2(1(x1))))))))	(30)
    4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
    4#(4(5(2(4(2(2(x1)))))))	→	4#(0(5(5(4(5(1(2(2(1(x1))))))))))	(115)
    4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
    0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
    2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
    4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
    4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
    2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
    2#(5(5(x1)))	→	4#(0(0(1(1(2(x1))))))	(138)
    2#(5(5(x1)))	→	2#(x1)	(139)
    2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
    2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
    0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
    0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
    2#(5(5(x1)))	→	0#(0(1(1(2(x1)))))	(144)
    2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
    2#(5(5(3(4(x1)))))	→	4#(0(2(4(4(x1)))))	(149)
    2#(5(5(3(4(x1)))))	→	2#(4(4(x1)))	(150)
    2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
    2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
    2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
    2#(5(0(4(x1))))	→	2#(4(4(5(1(0(0(x1)))))))	(158)
    2#(5(0(4(x1))))	→	0#(x1)	(160)
    2#(5(0(4(x1))))	→	0#(0(x1))	(161)
    5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
    5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
    5#(5(x1))	→	0#(4(x1))	(39)
    5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
    5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
    5#(5(5(x1)))	→	4#(5(0(0(x1))))	(43)
    5#(5(5(x1)))	→	0#(x1)	(47)
    5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
    5#(5(5(x1)))	→	0#(0(x1))	(49)
    5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
    5#(5(5(1(4(x1)))))	→	4#(0(x1))	(53)
    5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
    5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
    5#(5(3(x1)))	→	5#(0(x1))	(58)
    5#(5(3(x1)))	→	4#(4(1(0(1(5(0(x1)))))))	(59)
    5#(5(3(x1)))	→	0#(x1)	(63)
    5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
    5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
    5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
    5#(5(2(4(5(0(x1))))))	→	4#(0(4(2(0(x1)))))	(74)
    5#(5(2(4(5(0(x1))))))	→	2#(4(0(4(2(0(x1))))))	(75)
    5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
    5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
    5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
    5#(2(4(x1)))	→	4#(2(x1))	(89)
    5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
    5#(2(4(x1)))	→	2#(x1)	(91)
    5#(2(4(x1)))	→	2#(4(2(x1)))	(92)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

    [5(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
    [4(x1)]	=	0 0 0 0 · x1 + -∞ -∞
    [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
    [2(x1)]	=	0 0 0 0 · x1 + -∞ -∞
    [1(x1)]	=	0 0 0 0 · x1 + -∞ -∞
    [0(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
    [5#(x1)]	=	4 4 4 4 · x1 + -∞ -∞
    [4#(x1)]	=	2 4 2 4 · x1 + -∞ -∞
    [2#(x1)]	=	4 4 4 4 · x1 + -∞ -∞
    [0#(x1)]	=	2 4 2 4 · x1 + -∞ -∞

    together with the usable rules

    5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
    5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
    2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
    5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
    5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
    5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
    5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
    2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
    4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
    4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
    0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
    2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
    5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
    0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
    1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
    4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
    4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
    5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
    5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
    0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
    4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

    5#(5(x1))	→	4#(0(4(x1)))	(29)
    5#(5(x1))	→	4#(0(2(5(4(5(2(1(x1))))))))	(30)
    4#(4(5(2(4(2(2(x1)))))))	→	4#(0(5(5(4(5(1(2(2(1(x1))))))))))	(115)
    2#(5(5(x1)))	→	4#(0(0(1(1(2(x1))))))	(138)
    2#(5(5(x1)))	→	0#(0(1(1(2(x1)))))	(144)
    2#(5(5(3(4(x1)))))	→	4#(0(2(4(4(x1)))))	(149)
    2#(5(0(4(x1))))	→	0#(0(x1))	(161)
    5#(5(5(x1)))	→	4#(5(0(0(x1))))	(43)
    5#(5(5(x1)))	→	0#(0(x1))	(49)
    5#(5(5(1(4(x1)))))	→	4#(0(x1))	(53)
    5#(5(2(4(5(0(x1))))))	→	4#(0(4(2(0(x1)))))	(74)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
      5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
      5#(5(x1))	→	4#(x1)	(25)
      4#(5(5(5(x1))))	→	0#(5(x1))	(102)
      0#(1(5(5(5(3(5(x1)))))))	→	2#(5(1(0(1(2(0(5(x1))))))))	(182)
      2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
      5#(5(x1))	→	4#(5(2(1(x1))))	(26)
      4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
      5#(5(x1))	→	4#(4(0(4(x1))))	(27)
      4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
      5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
      2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
      4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
      5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
      0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
      2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
      4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
      4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
      0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
      0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
      4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
      4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
      2#(5(5(x1)))	→	2#(x1)	(139)
      2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
      2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
      2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
      2#(5(5(3(4(x1)))))	→	2#(4(4(x1)))	(150)
      2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
      2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
      2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
      2#(5(0(4(x1))))	→	2#(4(4(5(1(0(0(x1)))))))	(158)
      2#(5(0(4(x1))))	→	0#(x1)	(160)
      5#(5(x1))	→	0#(4(x1))	(39)
      5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
      5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
      5#(5(5(x1)))	→	0#(x1)	(47)
      5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
      5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
      5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
      5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
      5#(5(3(x1)))	→	5#(0(x1))	(58)
      5#(5(3(x1)))	→	4#(4(1(0(1(5(0(x1)))))))	(59)
      5#(5(3(x1)))	→	0#(x1)	(63)
      5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
      5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
      5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
      5#(5(2(4(5(0(x1))))))	→	2#(4(0(4(2(0(x1))))))	(75)
      5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
      5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
      5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
      5#(2(4(x1)))	→	4#(2(x1))	(89)
      5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
      5#(2(4(x1)))	→	2#(x1)	(91)
      5#(2(4(x1)))	→	2#(4(2(x1)))	(92)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

      [5(x1)]	=	0 0 0 0 · x1 + -∞ -∞
      [4(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
      [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
      [2(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
      [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
      [0(x1)]	=	0 0 0 0 · x1 + -∞ -∞
      [5#(x1)]	=	16 16 16 16 · x1 + -∞ -∞
      [4#(x1)]	=	16 16 16 16 · x1 + -∞ -∞
      [2#(x1)]	=	15 16 15 16 · x1 + -∞ -∞
      [0#(x1)]	=	16 16 16 16 · x1 + -∞ -∞

      together with the usable rules

      5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
      5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
      2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
      5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
      5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
      5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
      5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
      2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
      4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
      4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
      0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
      2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
      5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
      0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
      1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
      4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
      4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
      5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
      5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
      0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
      4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

      2#(5(5(3(4(x1)))))	→	2#(4(4(x1)))	(150)
      2#(5(0(4(x1))))	→	2#(4(4(5(1(0(0(x1)))))))	(158)
      5#(5(2(4(5(0(x1))))))	→	2#(4(0(4(2(0(x1))))))	(75)
      5#(2(4(x1)))	→	2#(4(2(x1)))	(92)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
        5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
        5#(5(x1))	→	4#(x1)	(25)
        4#(5(5(5(x1))))	→	0#(5(x1))	(102)
        0#(1(5(5(5(3(5(x1)))))))	→	2#(5(1(0(1(2(0(5(x1))))))))	(182)
        2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
        5#(5(x1))	→	4#(5(2(1(x1))))	(26)
        4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
        5#(5(x1))	→	4#(4(0(4(x1))))	(27)
        4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
        5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
        2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
        4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
        5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
        0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
        2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
        4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
        4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
        0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
        0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
        4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
        4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
        2#(5(5(x1)))	→	2#(x1)	(139)
        2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
        2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
        2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
        2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
        2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
        2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
        2#(5(0(4(x1))))	→	0#(x1)	(160)
        5#(5(x1))	→	0#(4(x1))	(39)
        5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
        5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
        5#(5(5(x1)))	→	0#(x1)	(47)
        5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
        5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
        5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
        5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
        5#(5(3(x1)))	→	5#(0(x1))	(58)
        5#(5(3(x1)))	→	4#(4(1(0(1(5(0(x1)))))))	(59)
        5#(5(3(x1)))	→	0#(x1)	(63)
        5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
        5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
        5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
        5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
        5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
        5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
        5#(2(4(x1)))	→	4#(2(x1))	(89)
        5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
        5#(2(4(x1)))	→	2#(x1)	(91)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

        [5(x1)]	=	0 0 0 0 · x1 + -∞ -∞
        [4(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
        [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
        [2(x1)]	=	0 0 0 0 · x1 + -∞ -∞
        [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
        [0(x1)]	=	0 0 0 0 · x1 + -∞ -∞
        [5#(x1)]	=	16 16 16 16 · x1 + -∞ -∞
        [4#(x1)]	=	14 16 14 16 · x1 + -∞ -∞
        [2#(x1)]	=	14 16 14 16 · x1 + -∞ -∞
        [0#(x1)]	=	16 16 16 16 · x1 + -∞ -∞

        together with the usable rules

        5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
        5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
        2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
        5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
        5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
        5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
        5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
        2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
        4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
        4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
        0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
        2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
        5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
        0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
        1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
        4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
        4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
        5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
        5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
        0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
        4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

        5#(5(3(x1)))

        →

        4#(4(1(0(1(5(0(x1)))))))

        (59)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
          5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
          5#(5(x1))	→	4#(x1)	(25)
          4#(5(5(5(x1))))	→	0#(5(x1))	(102)
          0#(1(5(5(5(3(5(x1)))))))	→	2#(5(1(0(1(2(0(5(x1))))))))	(182)
          2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
          5#(5(x1))	→	4#(5(2(1(x1))))	(26)
          4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
          5#(5(x1))	→	4#(4(0(4(x1))))	(27)
          4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
          5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
          2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
          4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
          5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
          0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
          2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
          4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
          4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
          0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
          0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
          4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
          4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
          2#(5(5(x1)))	→	2#(x1)	(139)
          2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
          2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
          2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
          2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
          2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
          2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
          2#(5(0(4(x1))))	→	0#(x1)	(160)
          5#(5(x1))	→	0#(4(x1))	(39)
          5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
          5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
          5#(5(5(x1)))	→	0#(x1)	(47)
          5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
          5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
          5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
          5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
          5#(5(3(x1)))	→	5#(0(x1))	(58)
          5#(5(3(x1)))	→	0#(x1)	(63)
          5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
          5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
          5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
          5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
          5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
          5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
          5#(2(4(x1)))	→	4#(2(x1))	(89)
          5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
          5#(2(4(x1)))	→	2#(x1)	(91)

          1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

          [5(x1)]	=	0 2 0 0 · x1 + -∞ -∞
          [4(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
          [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
          [2(x1)]	=	0 0 0 0 · x1 + -∞ -∞
          [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
          [0(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
          [5#(x1)]	=	11 13 11 13 · x1 + -∞ -∞
          [4#(x1)]	=	11 11 11 11 · x1 + -∞ -∞
          [2#(x1)]	=	10 11 10 11 · x1 + -∞ -∞
          [0#(x1)]	=	9 9 9 9 · x1 + -∞ -∞

          together with the usable rules

          5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
          5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
          2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
          5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
          5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
          5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
          5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
          2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
          4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
          4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
          0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
          2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
          5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
          0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
          1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
          4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
          4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
          5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
          5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
          0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
          4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

          5#(5(x1))	→	4#(x1)	(25)
          4#(5(5(5(x1))))	→	0#(5(x1))	(102)
          2#(5(5(x1)))	→	5#(4(4(0(0(1(1(2(x1))))))))	(135)
          5#(5(x1))	→	4#(4(0(4(x1))))	(27)
          2#(5(5(x1)))	→	4#(4(0(0(1(1(2(x1)))))))	(136)
          4#(4(5(2(4(2(2(x1)))))))	→	5#(4(5(1(2(2(1(x1)))))))	(112)
          5#(5(x1))	→	0#(5(4(0(2(5(4(5(2(1(x1))))))))))	(38)
          0#(1(5(5(5(3(5(x1)))))))	→	2#(0(5(x1)))	(183)
          2#(5(5(x1)))	→	4#(2(5(4(4(0(0(1(1(2(x1))))))))))	(137)
          4#(4(5(2(4(2(2(x1)))))))	→	4#(5(1(2(2(1(x1))))))	(114)
          4#(4(5(2(4(2(2(x1)))))))	→	0#(5(5(4(5(1(2(2(1(x1)))))))))	(120)
          0#(1(5(5(5(3(5(x1)))))))	→	0#(5(x1))	(186)
          0#(1(5(5(5(3(5(x1)))))))	→	0#(1(2(0(5(x1)))))	(187)
          4#(2(5(5(1(5(x1))))))	→	4#(2(5(x1)))	(121)
          4#(2(5(5(1(5(x1))))))	→	2#(5(x1))	(123)
          2#(5(5(x1)))	→	2#(x1)	(139)
          2#(5(5(x1)))	→	2#(5(4(4(0(0(1(1(2(x1)))))))))	(140)
          2#(5(5(x1)))	→	0#(1(1(2(x1))))	(143)
          2#(5(5(3(4(x1)))))	→	4#(4(x1))	(147)
          2#(5(5(3(4(x1)))))	→	0#(2(4(4(x1))))	(152)
          2#(5(0(4(x1))))	→	0#(x1)	(160)
          5#(5(x1))	→	0#(4(x1))	(39)
          5#(5(x1))	→	0#(2(5(4(5(2(1(x1)))))))	(40)
          5#(5(5(x1)))	→	5#(0(0(x1)))	(42)
          5#(5(5(x1)))	→	0#(x1)	(47)
          5#(5(5(x1)))	→	0#(1(4(5(0(0(x1))))))	(48)
          5#(5(5(1(4(x1)))))	→	4#(4(0(x1)))	(51)
          5#(5(5(1(4(x1)))))	→	0#(x1)	(54)
          5#(5(3(x1)))	→	5#(4(4(1(0(1(5(0(x1))))))))	(57)
          5#(5(3(x1)))	→	5#(0(x1))	(58)
          5#(5(3(x1)))	→	0#(x1)	(63)
          5#(5(3(x1)))	→	0#(1(5(0(x1))))	(65)
          5#(5(2(4(5(0(x1))))))	→	4#(2(4(0(4(2(0(x1)))))))	(72)
          5#(5(2(4(5(0(x1))))))	→	4#(2(0(x1)))	(73)
          5#(5(2(4(5(0(x1))))))	→	2#(0(x1))	(77)
          5#(5(2(4(5(0(x1))))))	→	0#(4(2(0(x1))))	(80)
          5#(2(5(5(0(4(x1))))))	→	4#(4(x1))	(82)
          5#(2(4(x1)))	→	4#(2(x1))	(89)
          5#(2(4(x1)))	→	4#(2(4(2(x1))))	(90)
          5#(2(4(x1)))	→	2#(x1)	(91)

          could be deleted.

          1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

          Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

          [5(x1)]	=	x1 + 0
          [4(x1)]	=	x1 + 0
          [3(x1)]	=	x1 + 0
          [2(x1)]	=	x1 + 0
          [1(x1)]	=	x1 + 0
          [0(x1)]	=	x1 + 0
          [5#(x1)]	=	x1 + 0
          [4#(x1)]	=	x1 + 0
          [2#(x1)]	=	x1 + 0
          [0#(x1)]	=	x1 + 1

          together with the usable rules

          5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
          5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
          2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
          5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
          5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
          5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
          5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
          2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
          4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
          4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
          0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
          2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
          5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
          0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
          1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
          4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
          4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
          5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
          5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
          0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
          4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

          0#(1(5(5(5(3(5(x1)))))))

          →

          2#(5(1(0(1(2(0(5(x1))))))))

          (182)

          and no rules could be deleted.

          1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 1 component.

          • The 1^st component contains the pair

            5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
            5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
            5#(5(x1))	→	4#(5(2(1(x1))))	(26)
            4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
            5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
            2#(5(0(4(x1))))	→	4#(5(1(0(0(x1)))))	(154)
            4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)
            2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)

            1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

            Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

            [5(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
            [4(x1)]	=	0 0 0 0 · x1 + -∞ -∞
            [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
            [2(x1)]	=	0 0 0 0 · x1 + -∞ -∞
            [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
            [0(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
            [5#(x1)]	=	12 12 12 12 · x1 + -∞ -∞
            [4#(x1)]	=	10 12 10 12 · x1 + -∞ -∞
            [2#(x1)]	=	12 12 12 12 · x1 + -∞ -∞

            together with the usable rules

            5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
            5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
            2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
            5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
            5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
            5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
            5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
            2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
            4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
            4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
            0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
            2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
            5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
            0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
            1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
            4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
            4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
            5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
            5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
            0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
            4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

            2#(5(0(4(x1))))

            →

            4#(5(1(0(0(x1)))))

            (154)

            could be deleted.

            1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

            The dependency pairs are split into 1 component.

            • The 1^st component contains the pair

              5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
              5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)
              5#(5(x1))	→	4#(5(2(1(x1))))	(26)
              4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
              5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
              2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
              4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

              Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

              [5(x1)]	=	0 0 0 0 · x1 + -∞ -∞
              [4(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
              [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
              [2(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
              [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
              [0(x1)]	=	0 0 0 0 · x1 + -∞ -∞
              [5#(x1)]	=	1 3 1 3 · x1 + -∞ -∞
              [4#(x1)]	=	3 3 3 3 · x1 + -∞ -∞
              [2#(x1)]	=	3 3 3 3 · x1 + -∞ -∞

              together with the usable rules

              5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
              5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
              2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
              5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
              5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
              5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
              5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
              2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
              4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
              4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
              0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
              2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
              5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
              0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
              1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
              4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
              4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
              5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
              5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
              0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
              4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

              5#(5(x1))	→	5#(4(5(2(1(x1)))))	(22)
              5#(5(x1))	→	5#(4(0(2(5(4(5(2(1(x1)))))))))	(23)

              could be deleted.

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

              The dependency pairs are split into 1 component.

              • The 1^st component contains the pair

                5#(5(x1))	→	4#(5(2(1(x1))))	(26)
                4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
                5#(5(x1))	→	2#(5(4(5(2(1(x1))))))	(31)
                2#(5(0(4(x1))))	→	4#(4(5(1(0(0(x1))))))	(155)
                4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                Using the matrix interpretations of dimension 2 with strict dimension 1 over the arctic semiring over the naturals

                [5(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
                [4(x1)]	=	0 0 -2 0 · x1 + -∞ -∞
                [3(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
                [2(x1)]	=	0 0 0 0 · x1 + -∞ -∞
                [1(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
                [0(x1)]	=	0 0 -2 -2 · x1 + -∞ -∞
                [5#(x1)]	=	3 3 3 3 · x1 + -∞ -∞
                [4#(x1)]	=	1 3 1 3 · x1 + -∞ -∞
                [2#(x1)]	=	1 1 1 1 · x1 + -∞ -∞

                together with the usable rules

                5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
                5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
                2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
                5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
                5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
                5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
                5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
                2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
                4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
                4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
                0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
                2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
                5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
                0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
                1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
                4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
                4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
                5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
                5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
                0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
                4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

                5#(5(x1))

                →

                2#(5(4(5(2(1(x1))))))

                (31)

                could be deleted.

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

                Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

                [5(x1)]	=	x1 + 0
                [4(x1)]	=	x1 + 0
                [3(x1)]	=	x1 + 0
                [2(x1)]	=	x1 + 0
                [1(x1)]	=	x1 + 0
                [0(x1)]	=	x1 + 0
                [5#(x1)]	=	x1 + 0
                [4#(x1)]	=	x1 + 0
                [2#(x1)]	=	x1 + 1

                together with the usable rules

                5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
                5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
                2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
                5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
                5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
                5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
                5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
                2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
                4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
                4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
                0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
                2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
                5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
                0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
                1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
                4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
                4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
                5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
                5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
                0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
                4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

                2#(5(0(4(x1))))

                →

                4#(4(5(1(0(0(x1))))))

                (155)

                and no rules could be deleted.

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

                The dependency pairs are split into 1 component.

                • The 1^st component contains the pair

                  5#(5(x1))	→	4#(5(2(1(x1))))	(26)
                  4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)
                  4#(4(5(2(4(2(2(x1)))))))	→	5#(5(4(5(1(2(2(1(x1))))))))	(111)

                  1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                  Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals

                  [5(x1)]	=	0 · x1 + 1
                  [4(x1)]	=	0 · x1 + 2
                  [3(x1)]	=	0 · x1 + 0
                  [2(x1)]	=	1 · x1 + 1
                  [1(x1)]	=	0 · x1 + 0
                  [0(x1)]	=	0 · x1 + 1
                  [5#(x1)]	=	0 · x1 + 2
                  [4#(x1)]	=	2 · x1 + 0

                  together with the usable rules

                  5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
                  5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
                  2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
                  5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
                  5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
                  5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
                  5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
                  2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
                  4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
                  4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
                  0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
                  2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
                  5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
                  0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
                  1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
                  4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
                  4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
                  5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
                  5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
                  0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
                  4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

                  4#(4(5(2(4(2(2(x1)))))))

                  →

                  5#(5(4(5(1(2(2(1(x1))))))))

                  (111)

                  could be deleted.

                  1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

                  The dependency pairs are split into 1 component.

                  • The 1^st component contains the pair

                    5#(5(x1))	→	4#(5(2(1(x1))))	(26)
                    4#(5(2(4(x1))))	→	5#(5(2(0(3(1(3(3(x1))))))))	(104)

                    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                    Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals

                    [5(x1)]	=	1 · x1 + 0
                    [4(x1)]	=	0 · x1 + 1
                    [3(x1)]	=	0 · x1 + 0
                    [2(x1)]	=	1 · x1 + 1
                    [1(x1)]	=	0 · x1 + 0
                    [0(x1)]	=	0 · x1 + 0
                    [5#(x1)]	=	0 · x1 + 2
                    [4#(x1)]	=	1 · x1 + 0

                    together with the usable rules

                    5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
                    5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
                    2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
                    5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
                    5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
                    5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
                    5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
                    2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
                    4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
                    4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
                    0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
                    2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
                    5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
                    0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
                    1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
                    4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
                    4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
                    5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
                    5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
                    0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
                    4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

                    5#(5(x1))

                    →

                    4#(5(2(1(x1))))

                    (26)

                    could be deleted.

                    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

                    Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1

                    [5(x1)]	=	x1 + 0
                    [4(x1)]	=	x1 + 0
                    [3(x1)]	=	x1 + 0
                    [2(x1)]	=	x1 + 0
                    [1(x1)]	=	x1 + 0
                    [0(x1)]	=	x1 + 0
                    [5#(x1)]	=	x1 + 0
                    [4#(x1)]	=	x1 + 1

                    together with the usable rules

                    5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
                    5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
                    2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
                    5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
                    5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
                    5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
                    5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
                    2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
                    4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
                    4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
                    0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
                    2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
                    5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
                    0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
                    1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
                    4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
                    4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
                    5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
                    5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
                    0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
                    4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

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

                    4#(5(2(4(x1))))

                    →

                    5#(5(2(0(3(1(3(3(x1))))))))

                    (104)

                    and no rules could be deleted.

                    1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

                    The dependency pairs are split into 0 components.