Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/212263)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

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

  3#(0(3(1(2(x1)))))	→	3#(x1)	(223)
  0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
  0#(5(0(3(2(x1)))))	→	0#(2(3(x1)))	(140)
  0#(1(1(2(x1))))	→	3#(x1)	(222)
  5#(1(0(3(2(x1)))))	→	5#(1(2(x1)))	(137)
  2#(0(3(2(x1))))	→	3#(0(2(2(x1))))	(132)
  5#(0(1(2(x1))))	→	3#(4(5(x1)))	(133)
  4#(5(1(4(2(x1)))))	→	5#(x1)	(134)
  0#(5(0(3(2(x1)))))	→	5#(0(0(2(3(x1)))))	(131)
  3#(0(3(1(2(x1)))))	→	3#(3(0(2(3(x1)))))	(130)
  3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)
  5#(0(3(2(x1))))	→	5#(x1)	(126)
  3#(3(5(2(x1))))	→	5#(3(x1))	(123)
  0#(1(2(5(2(x1)))))	→	5#(4(x1))	(121)
  5#(0(3(1(2(x1)))))	→	5#(x1)	(120)
  0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
  5#(2(0(3(2(x1)))))	→	3#(1(x1))	(119)
  3#(0(3(4(2(x1)))))	→	3#(x1)	(209)
  0#(3(2(x1)))	→	3#(x1)	(75)
  5#(1(0(5(2(x1)))))	→	5#(5(x1))	(116)
  0#(3(2(2(x1))))	→	3#(2(x1))	(169)
  5#(1(0(3(2(x1)))))	→	4#(3(5(1(2(x1)))))	(113)
  0#(1(5(5(2(x1)))))	→	5#(1(x1))	(205)
  3#(0(3(4(2(x1)))))	→	2#(3(x1))	(204)
  0#(1(2(x1)))	→	3#(x1)	(60)
  5#(1(0(3(2(x1)))))	→	3#(5(1(2(x1))))	(110)
  3#(0(3(1(2(x1)))))	→	0#(2(3(x1)))	(203)
  0#(5(0(3(2(x1)))))	→	2#(3(x1))	(108)
  5#(1(0(3(2(x1)))))	→	0#(2(x1))	(202)
  0#(3(2(2(x1))))	→	0#(2(3(2(x1))))	(107)
  0#(1(5(5(2(x1)))))	→	5#(5(1(x1)))	(106)
  0#(5(5(2(2(x1)))))	→	5#(5(2(x1)))	(200)
  3#(0(3(4(2(x1)))))	→	3#(4(0(2(3(x1)))))	(104)
  5#(2(0(3(2(x1)))))	→	2#(3(1(x1)))	(199)
  5#(0(3(1(2(x1)))))	→	3#(5(x1))	(195)
  0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)
  0#(1(2(5(2(x1)))))	→	4#(x1)	(100)
  5#(0(1(2(x1))))	→	4#(5(x1))	(191)
  2#(0(3(2(x1))))	→	0#(2(2(x1)))	(190)
  0#(5(0(3(2(x1)))))	→	0#(0(2(3(x1))))	(98)
  3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
  0#(1(2(x1)))	→	3#(x1)	(60)
  3#(0(3(1(2(x1)))))	→	2#(3(x1))	(185)
  5#(2(0(3(2(x1)))))	→	5#(2(3(1(x1))))	(94)
  0#(5(5(2(2(x1)))))	→	5#(2(x1))	(92)
  0#(5(0(3(2(x1)))))	→	3#(x1)	(91)
  3#(0(3(2(x1))))	→	2#(3(x1))	(182)
  3#(3(5(2(x1))))	→	3#(x1)	(89)
  5#(0(2(2(x1))))	→	5#(x1)	(90)
  2#(0(3(2(x1))))	→	2#(2(x1))	(181)
  0#(3(2(2(x1))))	→	0#(4(2(3(2(x1)))))	(177)
  3#(0(3(2(x1))))	→	3#(x1)	(84)
  3#(0(3(4(2(x1)))))	→	4#(0(2(3(x1))))	(175)
  3#(0(3(4(2(x1)))))	→	0#(2(3(x1)))	(82)
  0#(3(2(x1)))	→	3#(x1)	(75)
  0#(3(2(2(x1))))	→	4#(2(3(2(x1))))	(80)
  0#(1(5(1(2(x1)))))	→	5#(x1)	(173)
  0#(3(2(x1)))	→	3#(x1)	(75)
  0#(3(2(2(x1))))	→	3#(2(x1))	(169)
  3#(0(3(2(x1))))	→	0#(0(0(2(3(x1)))))	(70)
  0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
  5#(1(0(3(2(x1)))))	→	0#(4(3(5(1(2(x1))))))	(167)
  3#(0(3(2(x1))))	→	0#(0(2(3(x1))))	(165)
  5#(2(0(3(2(x1)))))	→	0#(2(5(2(3(1(x1))))))	(164)
  0#(1(3(2(x1))))	→	3#(x1)	(65)
  0#(1(2(x1)))	→	3#(x1)	(60)
  5#(0(3(1(2(x1)))))	→	4#(3(5(x1)))	(61)
  0#(1(3(2(x1))))	→	4#(3(x1))	(158)
  5#(0(1(2(x1))))	→	5#(x1)	(156)
  5#(1(0(5(2(x1)))))	→	5#(x1)	(154)
  3#(1(5(2(x1))))	→	3#(x1)	(155)
  3#(0(3(2(x1))))	→	0#(2(3(x1)))	(57)
  3#(1(5(2(x1))))	→	5#(3(x1))	(152)
  0#(3(2(2(x1))))	→	0#(0(4(2(3(2(x1))))))	(150)
  5#(2(0(3(2(x1)))))	→	2#(5(2(3(1(x1)))))	(52)
  5#(0(3(2(x1))))	→	4#(5(x1))	(146)
  5#(0(1(3(2(x1)))))	→	3#(x1)	(50)
  5#(0(4(2(2(x1)))))	→	5#(x1)	(48)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

  2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
  0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
  0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
  0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
  0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
  0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
  0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
  3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
  3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
  5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
  3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
  0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
  0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
  5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
  0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
  4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
  0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
  5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
  0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
  0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
  0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
  5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
  0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
  3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
  5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
  0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
  0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
  0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
  0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
  5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
  5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
  5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
  0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
  0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
  0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
  5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
  0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
  5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
  4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
  5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
  5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
  3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
  0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
  5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
  0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

  3#(0(3(1(2(x1)))))	→	3#(x1)	(223)
  0#(1(1(2(x1))))	→	3#(x1)	(222)
  5#(0(1(2(x1))))	→	3#(4(5(x1)))	(133)
  4#(5(1(4(2(x1)))))	→	5#(x1)	(134)
  5#(0(3(2(x1))))	→	5#(x1)	(126)
  3#(3(5(2(x1))))	→	5#(3(x1))	(123)
  0#(1(2(5(2(x1)))))	→	5#(4(x1))	(121)
  5#(0(3(1(2(x1)))))	→	5#(x1)	(120)
  5#(2(0(3(2(x1)))))	→	3#(1(x1))	(119)
  3#(0(3(4(2(x1)))))	→	3#(x1)	(209)
  0#(3(2(x1)))	→	3#(x1)	(75)
  5#(1(0(5(2(x1)))))	→	5#(5(x1))	(116)
  0#(3(2(2(x1))))	→	3#(2(x1))	(169)
  5#(1(0(3(2(x1)))))	→	4#(3(5(1(2(x1)))))	(113)
  0#(1(5(5(2(x1)))))	→	5#(1(x1))	(205)
  0#(1(2(x1)))	→	3#(x1)	(60)
  0#(1(5(5(2(x1)))))	→	5#(5(1(x1)))	(106)
  0#(5(5(2(2(x1)))))	→	5#(5(2(x1)))	(200)
  5#(2(0(3(2(x1)))))	→	2#(3(1(x1)))	(199)
  5#(0(3(1(2(x1)))))	→	3#(5(x1))	(195)
  0#(1(2(5(2(x1)))))	→	4#(x1)	(100)
  5#(0(1(2(x1))))	→	4#(5(x1))	(191)
  0#(1(2(x1)))	→	3#(x1)	(60)
  5#(2(0(3(2(x1)))))	→	5#(2(3(1(x1))))	(94)
  0#(5(5(2(2(x1)))))	→	5#(2(x1))	(92)
  0#(5(0(3(2(x1)))))	→	3#(x1)	(91)
  3#(3(5(2(x1))))	→	3#(x1)	(89)
  5#(0(2(2(x1))))	→	5#(x1)	(90)
  3#(0(3(2(x1))))	→	3#(x1)	(84)
  3#(0(3(4(2(x1)))))	→	4#(0(2(3(x1))))	(175)
  0#(3(2(x1)))	→	3#(x1)	(75)
  0#(3(2(2(x1))))	→	4#(2(3(2(x1))))	(80)
  0#(1(5(1(2(x1)))))	→	5#(x1)	(173)
  0#(3(2(x1)))	→	3#(x1)	(75)
  0#(3(2(2(x1))))	→	3#(2(x1))	(169)
  0#(1(3(2(x1))))	→	3#(x1)	(65)
  0#(1(2(x1)))	→	3#(x1)	(60)
  5#(0(3(1(2(x1)))))	→	4#(3(5(x1)))	(61)
  0#(1(3(2(x1))))	→	4#(3(x1))	(158)
  5#(0(1(2(x1))))	→	5#(x1)	(156)
  5#(1(0(5(2(x1)))))	→	5#(x1)	(154)
  3#(1(5(2(x1))))	→	3#(x1)	(155)
  3#(1(5(2(x1))))	→	5#(3(x1))	(152)
  5#(0(3(2(x1))))	→	4#(5(x1))	(146)
  5#(0(1(3(2(x1)))))	→	3#(x1)	(50)
  5#(0(4(2(2(x1)))))	→	5#(x1)	(48)

  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

    2#(0(3(2(x1))))	→	2#(2(x1))	(181)
    2#(0(3(2(x1))))	→	0#(2(2(x1)))	(190)
    2#(0(3(2(x1))))	→	3#(0(2(2(x1))))	(132)
    0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
    0#(3(2(2(x1))))	→	0#(2(3(2(x1))))	(107)
    0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
    3#(0(3(4(2(x1)))))	→	2#(3(x1))	(204)
    3#(0(3(4(2(x1)))))	→	0#(2(3(x1)))	(82)
    3#(0(3(4(2(x1)))))	→	3#(4(0(2(3(x1)))))	(104)
    3#(0(3(2(x1))))	→	2#(3(x1))	(182)
    3#(0(3(2(x1))))	→	0#(2(3(x1)))	(57)
    3#(0(3(2(x1))))	→	0#(0(2(3(x1))))	(165)
    3#(0(3(2(x1))))	→	0#(0(0(2(3(x1)))))	(70)
    3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
    0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
    0#(3(2(2(x1))))	→	0#(4(2(3(2(x1)))))	(177)
    0#(3(2(2(x1))))	→	0#(0(4(2(3(2(x1))))))	(150)
    0#(5(0(3(2(x1)))))	→	2#(3(x1))	(108)
    0#(5(0(3(2(x1)))))	→	0#(2(3(x1)))	(140)
    0#(5(0(3(2(x1)))))	→	0#(0(2(3(x1))))	(98)
    0#(5(0(3(2(x1)))))	→	5#(0(0(2(3(x1)))))	(131)
    0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)
    5#(2(0(3(2(x1)))))	→	2#(5(2(3(1(x1)))))	(52)
    5#(2(0(3(2(x1)))))	→	0#(2(5(2(3(1(x1))))))	(164)
    5#(1(0(3(2(x1)))))	→	5#(1(2(x1)))	(137)
    5#(1(0(3(2(x1)))))	→	3#(5(1(2(x1))))	(110)
    5#(1(0(3(2(x1)))))	→	0#(4(3(5(1(2(x1))))))	(167)
    5#(1(0(3(2(x1)))))	→	0#(2(x1))	(202)
    3#(0(3(1(2(x1)))))	→	2#(3(x1))	(185)
    3#(0(3(1(2(x1)))))	→	0#(2(3(x1)))	(203)
    3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)
    3#(0(3(1(2(x1)))))	→	3#(3(0(2(3(x1)))))	(130)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

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

    together with the usable rules

    2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
    0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
    0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
    0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
    0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
    0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
    0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
    3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
    3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
    5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
    3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
    0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
    0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
    5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
    0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
    4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
    0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
    5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
    0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
    0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
    0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
    5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
    0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
    3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
    5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
    0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
    0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
    0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
    0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
    5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
    5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
    5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
    0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
    0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
    0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
    5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
    0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
    5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
    4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
    5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
    5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
    3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
    0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
    5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
    0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

    2#(0(3(2(x1))))	→	2#(2(x1))	(181)
    2#(0(3(2(x1))))	→	0#(2(2(x1)))	(190)
    2#(0(3(2(x1))))	→	3#(0(2(2(x1))))	(132)
    0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
    3#(0(3(4(2(x1)))))	→	2#(3(x1))	(204)
    3#(0(3(2(x1))))	→	2#(3(x1))	(182)
    0#(3(2(2(x1))))	→	2#(3(2(x1)))	(71)
    0#(5(0(3(2(x1)))))	→	2#(3(x1))	(108)
    5#(2(0(3(2(x1)))))	→	2#(5(2(3(1(x1)))))	(52)
    3#(0(3(1(2(x1)))))	→	2#(3(x1))	(185)

    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

      0#(3(2(2(x1))))	→	0#(2(3(2(x1))))	(107)
      0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
      3#(0(3(4(2(x1)))))	→	0#(2(3(x1)))	(82)
      3#(0(3(4(2(x1)))))	→	3#(4(0(2(3(x1)))))	(104)
      3#(0(3(2(x1))))	→	0#(2(3(x1)))	(57)
      3#(0(3(2(x1))))	→	0#(0(2(3(x1))))	(165)
      3#(0(3(2(x1))))	→	0#(0(0(2(3(x1)))))	(70)
      3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
      0#(3(2(2(x1))))	→	0#(4(2(3(2(x1)))))	(177)
      0#(3(2(2(x1))))	→	0#(0(4(2(3(2(x1))))))	(150)
      0#(5(0(3(2(x1)))))	→	0#(2(3(x1)))	(140)
      0#(5(0(3(2(x1)))))	→	0#(0(2(3(x1))))	(98)
      0#(5(0(3(2(x1)))))	→	5#(0(0(2(3(x1)))))	(131)
      0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)
      5#(2(0(3(2(x1)))))	→	0#(2(5(2(3(1(x1))))))	(164)
      5#(1(0(3(2(x1)))))	→	5#(1(2(x1)))	(137)
      5#(1(0(3(2(x1)))))	→	3#(5(1(2(x1))))	(110)
      5#(1(0(3(2(x1)))))	→	0#(4(3(5(1(2(x1))))))	(167)
      5#(1(0(3(2(x1)))))	→	0#(2(x1))	(202)
      3#(0(3(1(2(x1)))))	→	0#(2(3(x1)))	(203)
      3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)
      3#(0(3(1(2(x1)))))	→	3#(3(0(2(3(x1)))))	(130)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [0#(x1)]	=	x1 + 53064
      [1(x1)]	=	x1 + 0
      [4(x1)]	=	1
      [5(x1)]	=	28254
      [3(x1)]	=	1
      [2#(x1)]	=	0
      [4#(x1)]	=	0
      [0(x1)]	=	x1 + 0
      [3#(x1)]	=	53066
      [5#(x1)]	=	x1 + 53065
      [2(x1)]	=	1

      together with the usable rules

      2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
      0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
      0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
      0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
      0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
      0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
      0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
      3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
      3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
      5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
      3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
      0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
      0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
      5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
      0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
      4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
      0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
      5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
      0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
      0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
      0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
      5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
      0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
      3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
      5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
      0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
      0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
      0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
      0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
      5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
      5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
      5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
      0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
      0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
      0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
      5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
      0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
      5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
      4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
      5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
      5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
      3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
      0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
      5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
      0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

      3#(0(3(4(2(x1)))))	→	0#(2(3(x1)))	(82)
      3#(0(3(2(x1))))	→	0#(2(3(x1)))	(57)
      3#(0(3(2(x1))))	→	0#(0(2(3(x1))))	(165)
      3#(0(3(2(x1))))	→	0#(0(0(2(3(x1)))))	(70)
      0#(5(0(3(2(x1)))))	→	0#(2(3(x1)))	(140)
      0#(5(0(3(2(x1)))))	→	0#(0(2(3(x1))))	(98)
      0#(5(0(3(2(x1)))))	→	5#(0(0(2(3(x1)))))	(131)
      5#(2(0(3(2(x1)))))	→	0#(2(5(2(3(1(x1))))))	(164)
      5#(1(0(3(2(x1)))))	→	0#(4(3(5(1(2(x1))))))	(167)
      5#(1(0(3(2(x1)))))	→	0#(2(x1))	(202)
      3#(0(3(1(2(x1)))))	→	0#(2(3(x1)))	(203)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 3 components.

      • The 1^st component contains the pair

        0#(3(2(2(x1))))	→	0#(2(3(2(x1))))	(107)
        0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
        0#(3(2(2(x1))))	→	0#(4(2(3(2(x1)))))	(177)
        0#(3(2(2(x1))))	→	0#(0(4(2(3(2(x1))))))	(150)
        0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [0#(x1)]	=	x1 + 53064
        [1(x1)]	=	1
        [4(x1)]	=	1
        [5(x1)]	=	28117
        [3(x1)]	=	28117
        [2#(x1)]	=	0
        [4#(x1)]	=	0
        [0(x1)]	=	x1 + 28116
        [3#(x1)]	=	53066
        [5#(x1)]	=	x1 + 53065
        [2(x1)]	=	1

        together with the usable rules

        2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
        0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
        0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
        0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
        0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
        0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
        0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
        3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
        3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
        5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
        3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
        0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
        0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
        5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
        0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
        4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
        0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
        5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
        0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
        0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
        0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
        5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
        0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
        3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
        5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
        0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
        0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
        0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
        0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
        5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
        5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
        5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
        0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
        0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
        0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
        5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
        0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
        5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
        4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
        5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
        5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
        3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
        0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
        5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
        0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

        0#(3(2(2(x1))))	→	0#(2(3(2(x1))))	(107)
        0#(3(2(2(x1))))	→	0#(4(2(3(2(x1)))))	(177)

        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

          0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
          0#(3(2(2(x1))))	→	0#(0(4(2(3(2(x1))))))	(150)
          0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)

          1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the argument filter

          π(0#)	=	1
          π(1)	=	1
          π(2#)	=	1
          π(4#)	=	1
          π(0)	=	1

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

          prec(4)	=	1		status(4)	=	[]		list-extension(4)	=	Lex
          prec(5)	=	1		status(5)	=	[]		list-extension(5)	=	Lex
          prec(3)	=	2		status(3)	=	[]		list-extension(3)	=	Lex
          prec(3#)	=	0		status(3#)	=	[]		list-extension(3#)	=	Lex
          prec(5#)	=	0		status(5#)	=	[]		list-extension(5#)	=	Lex
          prec(2)	=	2		status(2)	=	[]		list-extension(2)	=	Lex

          and the following Max-polynomial interpretation

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

          together with the usable rules

          2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
          0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
          0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
          0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
          0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
          0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
          0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
          3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
          3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
          5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
          3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
          0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
          0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
          5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
          0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
          4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
          0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
          5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
          0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
          0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
          0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
          5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
          0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
          3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
          5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
          0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
          0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
          0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
          0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
          5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
          5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
          5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
          0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
          0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
          0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
          5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
          0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
          5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
          4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
          5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
          5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
          3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
          0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
          5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
          0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

          0#(3(2(2(x1))))

          →

          0#(0(4(2(3(2(x1))))))

          (150)

          could be deleted.

          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

            0#(3(2(2(x1))))	→	0#(0(2(3(2(x1)))))	(139)
            0#(5(0(3(2(x1)))))	→	0#(5(0(0(2(3(x1))))))	(193)

            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 naturals

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

            together with the usable rules

            2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
            0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
            0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
            0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
            0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
            0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
            0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
            3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
            3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
            5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
            3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
            0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
            0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
            5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
            0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
            4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
            0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
            5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
            0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
            0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
            0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
            5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
            0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
            3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
            5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
            0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
            0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
            0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
            0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
            5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
            5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
            5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
            0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
            0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
            0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
            5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
            0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
            5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
            4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
            5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
            5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
            3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
            0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
            5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
            0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

            0#(3(2(2(x1))))

            →

            0#(0(2(3(2(x1)))))

            (139)

            could be deleted.

            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

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

              →

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

              (193)

              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 naturals

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

              together with the usable rules

              2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
              0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
              0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
              0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
              0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
              0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
              0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
              3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
              3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
              5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
              3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
              0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
              0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
              5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
              0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
              4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
              0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
              5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
              0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
              0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
              0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
              5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
              0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
              3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
              5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
              0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
              0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
              0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
              0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
              5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
              5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
              5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
              0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
              0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
              0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
              5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
              0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
              5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
              4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
              5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
              5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
              3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
              0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
              5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
              0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

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

              →

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

              (193)

              could be deleted.

              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.

      • The 2^nd component contains the pair

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

        →

        5#(1(2(x1)))

        (137)

        1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

        Using the argument filter

        π(1)	=	1
        π(4)	=	1
        π(2#)	=	1
        π(4#)	=	1

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

        prec(0#)	=	0		status(0#)	=	[]		list-extension(0#)	=	Lex
        prec(5)	=	2		status(5)	=	[]		list-extension(5)	=	Lex
        prec(3)	=	1		status(3)	=	[]		list-extension(3)	=	Lex
        prec(0)	=	2		status(0)	=	[]		list-extension(0)	=	Lex
        prec(3#)	=	0		status(3#)	=	[]		list-extension(3#)	=	Lex
        prec(5#)	=	0		status(5#)	=	[1]		list-extension(5#)	=	Lex
        prec(2)	=	1		status(2)	=	[]		list-extension(2)	=	Lex

        and the following Max-polynomial interpretation

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

        together with the usable rules

        2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
        0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
        0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
        0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
        0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
        0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
        0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
        3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
        3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
        5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
        3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
        0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
        0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
        5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
        0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
        4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
        0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
        5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
        0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
        0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
        0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
        5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
        0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
        3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
        5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
        0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
        0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
        0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
        0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
        5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
        5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
        5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
        0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
        0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
        0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
        5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
        0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
        5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
        4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
        5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
        5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
        3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
        0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
        5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
        0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

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

        →

        5#(1(2(x1)))

        (137)

        could be deleted.

        1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

        The dependency pairs are split into 0 components.

      • The 3^rd component contains the pair

        3#(0(3(4(2(x1)))))	→	3#(4(0(2(3(x1)))))	(104)
        3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
        3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)
        3#(0(3(1(2(x1)))))	→	3#(3(0(2(3(x1)))))	(130)

        1.1.1.1.1.1.1.1.3 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

        [0#(x1)]	=	53064
        [1(x1)]	=	1
        [4(x1)]	=	28084
        [5(x1)]	=	28085
        [3(x1)]	=	28085
        [2#(x1)]	=	0
        [4#(x1)]	=	0
        [0(x1)]	=	28085
        [3#(x1)]	=	x1 + 53066
        [5#(x1)]	=	53065
        [2(x1)]	=	28084

        together with the usable rules

        2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
        0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
        0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
        0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
        0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
        0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
        0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
        3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
        3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
        5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
        3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
        0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
        0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
        5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
        0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
        4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
        0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
        5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
        0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
        0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
        0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
        5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
        0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
        3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
        5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
        0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
        0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
        0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
        0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
        5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
        5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
        5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
        0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
        0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
        0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
        5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
        0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
        5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
        4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
        5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
        5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
        3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
        0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
        5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
        0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

        3#(0(3(4(2(x1)))))

        →

        3#(4(0(2(3(x1)))))

        (104)

        could be deleted.

        1.1.1.1.1.1.1.1.3.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
          3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)
          3#(0(3(1(2(x1)))))	→	3#(3(0(2(3(x1)))))	(130)

          1.1.1.1.1.1.1.1.3.1.1 Reduction Pair Processor with Usable Rules

          Using the argument filter

          π(1)	=	1
          π(4)	=	1
          π(2#)	=	1
          π(4#)	=	1

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

          prec(0#)	=	0		status(0#)	=	[]		list-extension(0#)	=	Lex
          prec(5)	=	2		status(5)	=	[]		list-extension(5)	=	Lex
          prec(3)	=	1		status(3)	=	[]		list-extension(3)	=	Lex
          prec(0)	=	2		status(0)	=	[]		list-extension(0)	=	Lex
          prec(3#)	=	0		status(3#)	=	[1]		list-extension(3#)	=	Lex
          prec(5#)	=	0		status(5#)	=	[1]		list-extension(5#)	=	Lex
          prec(2)	=	1		status(2)	=	[]		list-extension(2)	=	Lex

          and the following Max-polynomial interpretation

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

          together with the usable rules

          2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
          0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
          0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
          0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
          0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
          0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
          0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
          3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
          3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
          5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
          3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
          0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
          0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
          5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
          0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
          4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
          0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
          5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
          0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
          0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
          0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
          5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
          0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
          3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
          5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
          0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
          0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
          0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
          0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
          5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
          5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
          5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
          0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
          0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
          0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
          5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
          0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
          5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
          4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
          5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
          5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
          3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
          0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
          5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
          0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

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

          →

          3#(3(0(2(3(x1)))))

          (130)

          could be deleted.

          1.1.1.1.1.1.1.1.3.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 1 component.

          • The 1^st component contains the pair

            3#(0(3(2(x1))))	→	3#(0(0(0(2(3(x1))))))	(97)
            3#(0(3(1(2(x1)))))	→	3#(0(2(3(x1))))	(215)

            1.1.1.1.1.1.1.1.3.1.1.1.1 Reduction Pair Processor with Usable Rules

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

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

            together with the usable rules

            2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
            0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
            0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
            0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
            0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
            0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
            0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
            3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
            3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
            5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
            3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
            0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
            0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
            5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
            0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
            4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
            0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
            5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
            0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
            0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
            0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
            5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
            0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
            3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
            5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
            0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
            0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
            0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
            0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
            5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
            5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
            5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
            0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
            0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
            0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
            5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
            0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
            5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
            4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
            5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
            5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
            3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
            0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
            5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
            0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

            3#(0(3(2(x1))))

            →

            3#(0(0(0(2(3(x1))))))

            (97)

            could be deleted.

            1.1.1.1.1.1.1.1.3.1.1.1.1.1 Dependency Graph Processor

            The dependency pairs are split into 1 component.

            • The 1^st component contains the pair

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

              →

              3#(0(2(3(x1))))

              (215)

              1.1.1.1.1.1.1.1.3.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

              Using the Max-polynomial interpretation

              [0#(x1)]	=	53064
              [1(x1)]	=	9728
              [4(x1)]	=	9728
              [5(x1)]	=	9729
              [3(x1)]	=	9729
              [2#(x1)]	=	0
              [4#(x1)]	=	0
              [0(x1)]	=	x1 + 1
              [3#(x1)]	=	x1 + 53066
              [5#(x1)]	=	53065
              [2(x1)]	=	9728

              together with the usable rules

              2(0(3(2(x1))))	→	1(3(0(2(2(x1)))))	(18)
              0(1(2(x1)))	→	0(2(4(1(1(x1)))))	(4)
              0(1(5(2(x1))))	→	5(0(2(1(1(x1)))))	(15)
              0(3(2(x1)))	→	0(0(2(1(1(3(x1))))))	(8)
              0(1(2(x1)))	→	0(2(1(1(x1))))	(1)
              0(1(2(x1)))	→	0(2(1(1(3(x1)))))	(3)
              0(3(2(2(x1))))	→	0(0(2(3(2(x1)))))	(16)
              3(3(5(2(x1))))	→	3(0(2(1(5(3(x1))))))	(21)
              3(0(3(4(2(x1)))))	→	1(3(4(0(2(3(x1))))))	(36)
              5(1(2(2(x1))))	→	0(2(1(5(2(1(x1))))))	(26)
              3(0(3(2(x1))))	→	3(0(0(0(2(3(x1))))))	(19)
              0(5(0(1(2(x1)))))	→	0(4(5(0(2(1(x1))))))	(32)
              0(3(2(2(x1))))	→	0(0(4(2(3(2(x1))))))	(17)
              5(1(2(2(x1))))	→	2(1(5(2(1(1(x1))))))	(27)
              0(5(5(2(2(x1)))))	→	0(2(1(5(5(2(x1))))))	(34)
              4(5(2(2(x1))))	→	2(5(0(2(4(1(x1))))))	(22)
              0(1(2(4(2(x1)))))	→	4(2(1(0(2(1(x1))))))	(28)
              5(1(0(5(2(x1)))))	→	5(0(2(1(5(5(x1))))))	(44)
              0(1(2(x1)))	→	0(2(4(1(3(x1)))))	(5)
              0(5(0(3(2(x1)))))	→	0(5(0(0(2(3(x1))))))	(33)
              0(1(2(2(x1))))	→	0(2(2(1(1(x1)))))	(10)
              5(0(3(1(2(x1)))))	→	0(2(1(4(3(5(x1))))))	(39)
              0(3(2(x1)))	→	0(2(1(1(3(x1)))))	(7)
              3(1(5(2(x1))))	→	0(2(1(5(3(x1)))))	(20)
              5(0(3(2(x1))))	→	3(0(2(1(4(5(x1))))))	(25)
              0(1(5(1(2(x1)))))	→	1(0(2(1(1(5(x1))))))	(30)
              0(1(3(2(x1))))	→	3(0(2(4(1(1(x1))))))	(14)
              0(1(5(5(2(x1)))))	→	0(2(1(5(5(1(x1))))))	(31)
              0(1(3(2(x1))))	→	0(2(1(4(3(x1)))))	(12)
              5(2(0(3(2(x1)))))	→	0(2(5(2(3(1(x1))))))	(45)
              5(0(1(2(x1))))	→	0(2(1(3(4(5(x1))))))	(23)
              5(0(2(2(x1))))	→	2(0(2(4(1(5(x1))))))	(24)
              0(1(2(2(x1))))	→	0(2(3(2(1(x1)))))	(11)
              0(1(1(2(x1))))	→	0(2(1(1(3(x1)))))	(9)
              0(1(3(2(x1))))	→	3(3(0(2(1(x1)))))	(13)
              5(0(4(2(2(x1)))))	→	2(0(2(4(1(5(x1))))))	(40)
              0(3(2(x1)))	→	0(2(1(3(x1))))	(6)
              5(0(1(3(2(x1)))))	→	3(5(0(2(1(3(x1))))))	(38)
              4(5(1(4(2(x1)))))	→	2(4(4(4(1(5(x1))))))	(37)
              5(1(0(3(2(x1)))))	→	0(4(3(5(1(2(x1))))))	(41)
              5(1(0(3(2(x1)))))	→	5(3(1(1(0(2(x1))))))	(42)
              3(0(3(1(2(x1)))))	→	1(3(3(0(2(3(x1))))))	(35)
              0(1(2(5(2(x1)))))	→	2(0(2(1(5(4(x1))))))	(29)
              5(1(0(5(2(x1)))))	→	3(5(5(0(2(1(x1))))))	(43)
              0(1(2(x1)))	→	0(2(1(3(x1))))	(2)

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

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

              →

              3#(0(2(3(x1))))

              (215)

              could be deleted.

              1.1.1.1.1.1.1.1.3.1.1.1.1.1.1.1 Dependency Graph Processor

              The dependency pairs are split into 0 components.