Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/159731)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

There are 146 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(2(1(0(x1)))))	→	0#(1(0(x1)))	(187)
  3#(0(5(1(0(x1)))))	→	0#(0(x1))	(188)
  3#(0(1(0(x1))))	→	0#(0(0(x1)))	(130)
  3#(4(1(0(x1))))	→	0#(2(x1))	(96)
  3#(0(2(1(0(x1)))))	→	0#(0(x1))	(129)
  0#(1(4(1(0(x1)))))	→	0#(2(x1))	(128)
  3#(4(0(1(0(x1)))))	→	0#(2(x1))	(183)
  0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
  3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
  3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
  0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
  3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
  3#(4(0(1(0(x1)))))	→	0#(0(2(x1)))	(119)
  0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
  3#(0(1(0(x1))))	→	0#(2(x1))	(95)
  3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
  3#(3(4(1(0(x1)))))	→	3#(1(0(x1)))	(115)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  0#(3(0(1(0(x1)))))	→	3#(1(3(0(x1))))	(112)
  0#(0(1(0(x1))))	→	3#(1(x1))	(110)
  0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)
  3#(3(0(1(0(x1)))))	→	3#(0(0(x1)))	(107)
  3#(0(1(0(x1))))	→	3#(1(0(0(2(x1)))))	(108)
  0#(3(0(1(0(x1)))))	→	0#(0(3(1(3(0(x1))))))	(173)
  3#(4(1(0(x1))))	→	0#(2(x1))	(96)
  0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
  0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
  3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
  0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
  3#(0(1(0(0(x1)))))	→	3#(1(3(0(0(0(x1))))))	(165)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
  0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(3(0(1(0(x1)))))	→	0#(0(x1))	(98)
  3#(4(1(0(x1))))	→	0#(2(x1))	(96)
  3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
  3#(0(1(0(x1))))	→	0#(2(x1))	(95)
  0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(3(4(1(0(x1)))))	→	0#(2(x1))	(91)
  3#(3(4(1(0(x1)))))	→	3#(0(x1))	(153)
  0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
  0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	0#(2(0(x1)))	(86)
  0#(3(0(1(0(x1)))))	→	0#(3(1(3(0(x1)))))	(152)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
  3#(0(1(0(0(x1)))))	→	0#(0(0(x1)))	(151)
  3#(3(4(1(0(x1)))))	→	3#(4(0(2(x1))))	(84)
  0#(3(0(1(0(x1)))))	→	0#(3(1(0(x1))))	(85)
  0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
  3#(3(4(1(0(x1)))))	→	3#(1(3(4(0(2(x1))))))	(147)
  0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
  3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)
  3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
  3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
  3#(4(0(1(0(x1)))))	→	3#(0(x1))	(142)
  3#(3(0(1(0(x1)))))	→	0#(3(0(x1)))	(76)
  0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
  3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
  0#(3(0(1(0(x1)))))	→	0#(0(3(1(0(x1)))))	(75)
  3#(0(1(0(x1))))	→	0#(0(x1))	(73)
  3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
  0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)
  0#(3(0(1(0(x1)))))	→	0#(0(3(3(1(0(x1))))))	(72)
  3#(3(0(1(0(x1)))))	→	3#(0(x1))	(70)
  0#(3(4(1(0(x1)))))	→	3#(1(x1))	(136)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

  3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
  3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
  3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
  3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
  3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
  3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
  0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
  0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
  3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
  3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
  0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
  3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
  3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
  3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
  3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
  3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
  3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
  3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
  0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
  3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
  3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
  3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
  0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
  3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
  3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
  3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
  3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
  0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
  3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
  3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
  3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
  3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
  3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
  3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
  3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
  3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
  3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
  3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
  3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
  3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
  3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
  3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
  3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
  3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
  3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
  3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
  3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
  0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
  3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
  3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
  3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
  3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
  0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
  3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
  3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
  3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
  3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
  3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
  0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
  0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
  0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
  3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
  3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
  0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
  3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
  0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
  0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

  0#(3(4(1(0(x1)))))

  →

  3#(1(x1))

  (136)

  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

    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
    3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
    0#(0(1(0(x1))))	→	3#(1(x1))	(110)
    0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
    0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
    0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
    0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
    0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
    0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
    0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
    3#(3(4(1(0(x1)))))	→	3#(1(0(x1)))	(115)
    3#(0(1(0(x1))))	→	0#(2(x1))	(95)
    3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(3(0(1(0(x1)))))	→	0#(0(x1))	(98)
    3#(3(0(1(0(x1)))))	→	3#(0(0(x1)))	(107)
    0#(1(4(1(0(x1)))))	→	0#(2(x1))	(128)
    3#(4(0(1(0(x1)))))	→	0#(2(x1))	(183)
    3#(4(0(1(0(x1)))))	→	0#(0(2(x1)))	(119)
    3#(0(1(0(x1))))	→	0#(2(x1))	(95)
    3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
    3#(0(1(0(x1))))	→	3#(1(0(0(2(x1)))))	(108)
    3#(4(0(1(0(x1)))))	→	3#(0(x1))	(142)
    3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
    3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(2(1(0(x1)))))	→	0#(1(0(x1)))	(187)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)
    3#(3(4(1(0(x1)))))	→	0#(2(x1))	(91)
    3#(3(4(1(0(x1)))))	→	3#(4(0(2(x1))))	(84)
    3#(3(4(1(0(x1)))))	→	3#(1(3(4(0(2(x1))))))	(147)
    3#(0(1(0(x1))))	→	0#(2(0(x1)))	(86)
    3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
    3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
    3#(0(1(0(0(x1)))))	→	0#(0(0(x1)))	(151)
    3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)
    3#(0(1(0(0(x1)))))	→	3#(1(3(0(0(0(x1))))))	(165)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)
    3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
    3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    3#(0(1(0(x1))))	→	0#(0(0(x1)))	(130)
    3#(0(5(1(0(x1)))))	→	0#(0(x1))	(188)
    0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
    0#(3(0(1(0(x1)))))	→	0#(3(1(0(x1))))	(85)
    0#(3(0(1(0(x1)))))	→	0#(0(3(1(0(x1)))))	(75)
    3#(3(0(1(0(x1)))))	→	3#(0(x1))	(70)
    3#(3(0(1(0(x1)))))	→	0#(3(0(x1)))	(76)
    3#(0(1(0(x1))))	→	0#(0(x1))	(73)
    0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
    0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
    0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
    0#(3(0(1(0(x1)))))	→	0#(0(3(3(1(0(x1))))))	(72)
    3#(3(4(1(0(x1)))))	→	3#(0(x1))	(153)
    3#(0(2(1(0(x1)))))	→	0#(0(x1))	(129)
    3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
    0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)
    0#(3(0(1(0(x1)))))	→	3#(1(3(0(x1))))	(112)
    0#(3(0(1(0(x1)))))	→	0#(3(1(3(0(x1)))))	(152)
    0#(3(0(1(0(x1)))))	→	0#(0(3(1(3(0(x1))))))	(173)
    0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
    0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
    0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
    0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

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

    together with the usable rules

    3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
    3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
    3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
    3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
    3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
    3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
    0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
    0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
    3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
    3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
    0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
    3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
    3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
    3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
    3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
    3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
    3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
    3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
    0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
    3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
    3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
    3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
    0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
    3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
    3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
    3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
    3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
    0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
    3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
    3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
    3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
    3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
    3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
    3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
    3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
    3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
    3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
    3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
    3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
    3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
    3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
    3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
    3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
    3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
    3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
    3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
    3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
    0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
    3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
    3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
    3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
    3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
    0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
    3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
    3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
    3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
    3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
    3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
    0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
    0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
    0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
    3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
    3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
    0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
    3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
    0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
    0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

    3#(3(4(1(0(x1)))))	→	3#(1(0(x1)))	(115)
    3#(4(0(1(0(x1)))))	→	0#(2(x1))	(183)
    3#(4(0(1(0(x1)))))	→	0#(0(2(x1)))	(119)
    3#(4(0(1(0(x1)))))	→	3#(0(x1))	(142)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)
    3#(3(4(1(0(x1)))))	→	0#(2(x1))	(91)
    3#(3(4(1(0(x1)))))	→	3#(1(3(4(0(2(x1))))))	(147)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)
    3#(3(4(1(0(x1)))))	→	3#(0(x1))	(153)
    3#(4(1(0(x1))))	→	0#(2(x1))	(96)

    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

      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
      3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
      0#(0(1(0(x1))))	→	3#(1(x1))	(110)
      0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
      0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
      0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
      0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
      0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
      0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
      0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
      3#(0(1(0(x1))))	→	0#(2(x1))	(95)
      3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(3(0(1(0(x1)))))	→	0#(0(x1))	(98)
      3#(3(0(1(0(x1)))))	→	3#(0(0(x1)))	(107)
      0#(1(4(1(0(x1)))))	→	0#(2(x1))	(128)
      3#(0(1(0(x1))))	→	0#(2(x1))	(95)
      3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
      3#(0(1(0(x1))))	→	3#(1(0(0(2(x1)))))	(108)
      3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
      3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(2(1(0(x1)))))	→	0#(1(0(x1)))	(187)
      3#(0(1(0(x1))))	→	0#(2(0(x1)))	(86)
      3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
      3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
      3#(0(1(0(0(x1)))))	→	0#(0(0(x1)))	(151)
      3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)
      3#(0(1(0(0(x1)))))	→	3#(1(3(0(0(0(x1))))))	(165)
      3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
      3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      3#(0(1(0(x1))))	→	0#(0(0(x1)))	(130)
      3#(0(5(1(0(x1)))))	→	0#(0(x1))	(188)
      0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
      0#(3(0(1(0(x1)))))	→	0#(3(1(0(x1))))	(85)
      0#(3(0(1(0(x1)))))	→	0#(0(3(1(0(x1)))))	(75)
      3#(3(0(1(0(x1)))))	→	3#(0(x1))	(70)
      3#(3(0(1(0(x1)))))	→	0#(3(0(x1)))	(76)
      3#(0(1(0(x1))))	→	0#(0(x1))	(73)
      0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
      0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
      0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
      0#(3(0(1(0(x1)))))	→	0#(0(3(3(1(0(x1))))))	(72)
      3#(0(2(1(0(x1)))))	→	0#(0(x1))	(129)
      3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
      0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)
      0#(3(0(1(0(x1)))))	→	3#(1(3(0(x1))))	(112)
      0#(3(0(1(0(x1)))))	→	0#(3(1(3(0(x1)))))	(152)
      0#(3(0(1(0(x1)))))	→	0#(0(3(1(3(0(x1))))))	(173)
      0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
      0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
      0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
      0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

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

      together with the usable rules

      3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
      3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
      3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
      3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
      3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
      3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
      0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
      0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
      3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
      3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
      0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
      3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
      3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
      3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
      3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
      3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
      3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
      3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
      0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
      3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
      3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
      3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
      0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
      3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
      3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
      3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
      3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
      0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
      3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
      3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
      3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
      3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
      3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
      3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
      3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
      3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
      3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
      3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
      3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
      3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
      3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
      3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
      3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
      3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
      3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
      3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
      3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
      0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
      3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
      3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
      3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
      3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
      0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
      3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
      3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
      3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
      3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
      3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
      0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
      0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
      0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
      3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
      3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
      0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
      3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
      0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
      0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

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

      →

      0#(2(x1))

      (128)

      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

        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
        0#(0(1(0(x1))))	→	3#(1(x1))	(110)
        0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
        0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
        0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
        0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
        0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
        0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
        0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
        3#(0(1(0(x1))))	→	0#(2(x1))	(95)
        3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(3(0(1(0(x1)))))	→	0#(0(x1))	(98)
        3#(3(0(1(0(x1)))))	→	3#(0(0(x1)))	(107)
        3#(0(1(0(x1))))	→	0#(2(x1))	(95)
        3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
        3#(0(1(0(x1))))	→	3#(1(0(0(2(x1)))))	(108)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(2(0(x1)))	(86)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
        3#(0(1(0(0(x1)))))	→	0#(0(0(x1)))	(151)
        3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)
        3#(0(1(0(0(x1)))))	→	3#(1(3(0(0(0(x1))))))	(165)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(0(x1)))	(130)
        3#(0(5(1(0(x1)))))	→	0#(0(x1))	(188)
        0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
        0#(3(0(1(0(x1)))))	→	0#(3(1(0(x1))))	(85)
        0#(3(0(1(0(x1)))))	→	0#(0(3(1(0(x1)))))	(75)
        3#(3(0(1(0(x1)))))	→	3#(0(x1))	(70)
        3#(3(0(1(0(x1)))))	→	0#(3(0(x1)))	(76)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
        0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
        0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
        0#(3(0(1(0(x1)))))	→	0#(0(3(3(1(0(x1))))))	(72)
        3#(0(2(1(0(x1)))))	→	0#(0(x1))	(129)
        3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
        0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)
        0#(3(0(1(0(x1)))))	→	3#(1(3(0(x1))))	(112)
        0#(3(0(1(0(x1)))))	→	0#(3(1(3(0(x1)))))	(152)
        0#(3(0(1(0(x1)))))	→	0#(0(3(1(3(0(x1))))))	(173)
        0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
        0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
        0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
        0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

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

        together with the usable rules

        3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
        3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
        3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
        3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
        3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
        3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
        0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
        0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
        3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
        3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
        0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
        3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
        3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
        3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
        3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
        3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
        3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
        3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
        0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
        3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
        3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
        3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
        0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
        3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
        3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
        3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
        3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
        0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
        3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
        3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
        3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
        3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
        3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
        3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
        3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
        3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
        3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
        3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
        3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
        3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
        3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
        3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
        3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
        3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
        3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
        3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
        3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
        0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
        3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
        3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
        3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
        3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
        0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
        3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
        3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
        3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
        3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
        3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
        0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
        0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
        0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
        3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
        3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
        0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
        3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
        0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
        0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(2(x1))	(95)
        3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(3(0(1(0(x1)))))	→	0#(0(x1))	(98)
        3#(3(0(1(0(x1)))))	→	3#(0(0(x1)))	(107)
        3#(0(1(0(x1))))	→	0#(2(x1))	(95)
        3#(0(1(0(x1))))	→	0#(0(2(x1)))	(77)
        3#(0(1(0(x1))))	→	3#(1(0(0(2(x1)))))	(108)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(2(0(x1)))	(86)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(3(1(0(x1))))	(74)
        3#(0(1(0(0(x1)))))	→	0#(0(0(x1)))	(151)
        3#(0(1(0(0(x1)))))	→	3#(1(3(0(0(0(x1))))))	(165)
        3#(0(1(0(x1))))	→	3#(1(0(x1)))	(100)
        3#(0(1(0(x1))))	→	0#(2(3(1(0(x1)))))	(123)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        3#(0(1(0(x1))))	→	0#(0(0(x1)))	(130)
        3#(0(5(1(0(x1)))))	→	0#(0(x1))	(188)
        0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
        0#(3(0(1(0(x1)))))	→	0#(3(1(0(x1))))	(85)
        0#(3(0(1(0(x1)))))	→	0#(0(3(1(0(x1)))))	(75)
        3#(3(0(1(0(x1)))))	→	3#(0(x1))	(70)
        3#(3(0(1(0(x1)))))	→	0#(3(0(x1)))	(76)
        3#(0(1(0(x1))))	→	0#(0(x1))	(73)
        0#(3(0(1(0(x1)))))	→	3#(1(0(x1)))	(88)
        0#(3(0(1(0(x1)))))	→	0#(0(3(3(1(0(x1))))))	(72)
        3#(0(2(1(0(x1)))))	→	0#(0(x1))	(129)
        0#(3(0(1(0(x1)))))	→	3#(1(3(0(x1))))	(112)
        0#(3(0(1(0(x1)))))	→	0#(3(1(3(0(x1)))))	(152)
        0#(3(0(1(0(x1)))))	→	0#(0(3(1(3(0(x1))))))	(173)

        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

          3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
          0#(0(1(0(x1))))	→	3#(1(x1))	(110)
          0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
          0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
          0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
          3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
          0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
          0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
          0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
          0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
          3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)
          0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
          0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
          3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
          0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)
          0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
          0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
          0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
          0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)

          1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the Max-polynomial interpretation

          [0#(x1)]	=	x1 + 1
          [1(x1)]	=	23975
          [4(x1)]	=	26995
          [5(x1)]	=	x1 + 1
          [3(x1)]	=	x1 + 3020
          [0(x1)]	=	26995
          [3#(x1)]	=	26996
          [2(x1)]	=	26995

          together with the usable rules

          3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
          3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
          3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
          3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
          3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
          3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
          0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
          0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
          3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
          3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
          0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
          3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
          3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
          3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
          3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
          3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
          3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
          3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
          0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
          3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
          3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
          3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
          0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
          3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
          3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
          3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
          3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
          0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
          3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
          3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
          3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
          3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
          3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
          3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
          3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
          3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
          3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
          3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
          3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
          3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
          3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
          3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
          3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
          3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
          3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
          3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
          3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
          0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
          3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
          3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
          3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
          3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
          0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
          3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
          3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
          3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
          3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
          3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
          0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
          0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
          0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
          3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
          3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
          0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
          3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
          0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
          0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

          0#(3(0(1(0(x1)))))	→	3#(3(1(0(x1))))	(79)
          0#(3(0(1(0(x1)))))	→	3#(0(x1))	(109)

          could be deleted.

          1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

          The dependency pairs are split into 2 components.

          • The 1^st component contains the pair

            3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
            3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)

            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)]	=	0 0
            [1(x1)]	=	7480 12406
            [4(x1)]	=	1 1 1 0 · x1 + 0 12405
            [5(x1)]	=	1 0
            [3(x1)]	=	0 0 0 1 · x1 + 1 0
            [0(x1)]	=	0 0 1 0 · x1 + 1 12405
            [3#(x1)]	=	0 1 0 1 · x1 + 0 0
            [2(x1)]	=	1 12406

            together with the usable rules

            3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
            3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
            3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
            3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
            3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
            3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
            0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
            0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
            3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
            3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
            0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
            3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
            3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
            3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
            3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
            3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
            3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
            3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
            0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
            3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
            3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
            3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
            0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
            3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
            3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
            3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
            3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
            0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
            3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
            3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
            3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
            3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
            3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
            3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
            3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
            3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
            3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
            3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
            3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
            3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
            3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
            3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
            3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
            3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
            3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
            3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
            3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
            0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
            3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
            3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
            3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
            3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
            0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
            3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
            3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
            3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
            3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
            3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
            0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
            0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
            0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
            3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
            3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
            0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
            3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
            0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
            0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

            3#(0(1(0(x1))))	→	3#(0(0(x1)))	(178)
            3#(0(1(0(0(x1)))))	→	3#(0(0(0(x1))))	(145)

            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 0 components.

          • The 2^nd component contains the pair

            3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
            0#(0(1(0(x1))))	→	3#(1(x1))	(110)
            0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
            0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
            0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
            0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
            0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
            0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
            0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
            0#(3(0(1(0(x1)))))	→	0#(3(3(1(0(x1)))))	(172)
            3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
            0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
            0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
            0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
            0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)

            1.1.1.1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

            [0#(x1)]	=	0 1 0 0 · x1 + 0 0
            [1(x1)]	=	0 1 0 0 · x1 + 77330 1
            [4(x1)]	=	0 1 0 0 · x1 + 7756 7760
            [5(x1)]	=	1 1 0 0 · x1 + 54998 1
            [3(x1)]	=	0 1 0 0 · x1 + 10327 32667
            [0(x1)]	=	1 0 1 1 · x1 + 1 22336
            [3#(x1)]	=	1 0 0 0 · x1 + 22338 0
            [2(x1)]	=	0 0 1 0 · x1 + 1 2

            together with the usable rules

            3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
            3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
            3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
            3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
            3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
            3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
            0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
            0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
            3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
            3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
            0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
            3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
            3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
            3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
            3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
            3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
            3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
            3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
            0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
            3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
            3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
            3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
            0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
            3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
            3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
            3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
            3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
            0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
            3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
            3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
            3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
            3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
            3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
            3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
            3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
            3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
            3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
            3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
            3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
            3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
            3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
            3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
            3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
            3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
            3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
            3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
            3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
            0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
            3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
            3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
            3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
            3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
            0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
            3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
            3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
            3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
            3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
            3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
            0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
            0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
            0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
            3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
            3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
            0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
            3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
            0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
            0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

            3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
            0#(0(1(0(x1))))	→	3#(1(x1))	(110)
            0#(0(1(0(x1))))	→	0#(3(1(x1)))	(124)
            0#(0(1(0(x1))))	→	0#(0(3(1(x1))))	(99)
            0#(0(1(0(x1))))	→	0#(2(0(0(3(1(x1))))))	(171)
            0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
            0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
            0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
            0#(2(0(1(0(x1)))))	→	0#(0(0(3(1(x1)))))	(148)
            3#(1(0(1(0(x1)))))	→	0#(0(x1))	(141)
            0#(2(0(1(0(x1)))))	→	3#(1(x1))	(89)
            0#(2(0(1(0(x1)))))	→	0#(3(1(x1)))	(104)
            0#(2(0(1(0(x1)))))	→	0#(0(3(1(x1))))	(180)
            0#(2(0(1(0(x1)))))	→	0#(2(0(0(3(1(x1))))))	(139)

            could be deleted.

            1.1.1.1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

            The dependency pairs are split into 1 component.

            • The 1^st component contains the pair

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

              →

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

              (172)

              1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

              Using the Max-polynomial interpretation

              [0#(x1)]	=	x1 + 26996
              [1(x1)]	=	1
              [4(x1)]	=	13260
              [5(x1)]	=	x1 + 12385
              [3(x1)]	=	x1 + 13259
              [0(x1)]	=	26519
              [3#(x1)]	=	26996
              [2(x1)]	=	13260

              together with the usable rules

              3(0(1(0(x1))))	→	3(2(2(1(0(0(x1))))))	(18)
              3(0(2(1(0(x1)))))	→	3(1(2(0(5(0(x1))))))	(50)
              3(0(1(0(x1))))	→	0(2(3(1(0(x1)))))	(4)
              3(0(1(0(x1))))	→	3(1(5(1(0(0(x1))))))	(15)
              3(0(1(0(x1))))	→	3(1(5(0(0(x1)))))	(8)
              3(1(0(1(0(x1)))))	→	3(1(2(1(0(0(x1))))))	(54)
              0(0(1(0(x1))))	→	0(2(0(0(3(1(x1))))))	(1)
              0(0(1(0(x1))))	→	2(0(0(0(2(1(x1))))))	(3)
              3(0(1(0(x1))))	→	3(1(5(2(0(0(x1))))))	(16)
              3(0(1(0(x1))))	→	5(1(1(3(0(0(x1))))))	(21)
              0(2(0(1(0(x1)))))	→	2(0(0(0(3(1(x1))))))	(36)
              3(4(1(0(x1))))	→	3(1(1(5(4(0(x1))))))	(26)
              3(3(4(1(0(x1)))))	→	3(1(4(3(1(0(x1))))))	(63)
              3(0(1(0(x1))))	→	3(5(1(0(0(2(x1))))))	(19)
              3(4(1(0(x1))))	→	3(4(2(1(1(0(x1))))))	(32)
              3(0(1(0(x1))))	→	3(1(5(5(0(0(x1))))))	(17)
              3(3(0(1(0(x1)))))	→	3(1(2(3(0(0(x1))))))	(60)
              3(4(1(0(x1))))	→	3(1(2(1(4(0(x1))))))	(27)
              0(1(4(1(0(x1)))))	→	0(1(1(4(0(2(x1))))))	(34)
              3(4(1(0(x1))))	→	3(1(2(4(0(x1)))))	(22)
              3(4(1(0(x1))))	→	3(1(2(5(4(0(x1))))))	(28)
              3(4(0(1(0(x1)))))	→	3(1(4(0(0(2(x1))))))	(65)
              0(5(0(1(0(x1)))))	→	0(2(0(0(1(5(x1))))))	(44)
              3(0(1(0(x1))))	→	3(1(0(0(2(x1)))))	(5)
              3(4(1(0(x1))))	→	3(4(5(1(2(0(x1))))))	(33)
              3(4(0(1(0(x1)))))	→	0(2(4(1(3(0(x1))))))	(64)
              3(0(1(0(x1))))	→	5(0(3(1(0(x1)))))	(10)
              0(3(0(1(0(x1)))))	→	0(0(3(5(1(0(x1))))))	(39)
              3(0(1(0(x1))))	→	3(1(2(0(0(x1)))))	(7)
              3(0(1(0(x1))))	→	3(5(1(5(0(0(x1))))))	(20)
              3(4(1(0(x1))))	→	3(4(2(1(0(x1)))))	(25)
              3(0(2(1(0(x1)))))	→	3(1(2(0(1(0(x1))))))	(49)
              3(1(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(52)
              3(4(1(0(x1))))	→	3(1(5(4(0(2(x1))))))	(30)
              3(3(4(1(0(x1)))))	→	3(1(3(4(0(2(x1))))))	(62)
              3(0(1(0(x1))))	→	3(1(5(0(2(0(x1))))))	(14)
              3(1(4(1(0(x1)))))	→	3(1(5(1(4(0(x1))))))	(56)
              3(4(1(0(x1))))	→	3(1(5(5(4(0(x1))))))	(31)
              3(0(1(0(x1))))	→	2(2(0(3(1(0(x1))))))	(12)
              3(0(1(0(0(x1)))))	→	3(1(3(0(0(0(x1))))))	(45)
              3(4(1(0(x1))))	→	3(1(4(0(2(x1)))))	(23)
              3(4(1(0(x1))))	→	3(1(5(4(0(x1)))))	(24)
              3(2(0(1(0(x1)))))	→	0(2(3(1(5(0(x1))))))	(57)
              3(0(1(0(x1))))	→	2(0(2(3(1(0(x1))))))	(11)
              3(0(1(0(x1))))	→	3(5(1(0(0(x1)))))	(9)
              3(0(1(0(x1))))	→	3(1(5(0(0(0(x1))))))	(13)
              3(0(5(1(0(x1)))))	→	3(1(5(2(0(0(x1))))))	(51)
              0(3(0(1(0(x1)))))	→	2(0(0(3(1(0(x1))))))	(40)
              3(4(4(1(0(x1)))))	→	3(1(1(4(4(0(x1))))))	(67)
              3(1(4(1(0(x1)))))	→	3(1(2(1(4(0(x1))))))	(55)
              3(3(0(1(0(x1)))))	→	3(1(2(0(3(0(x1))))))	(59)
              3(0(1(0(x1))))	→	3(1(1(0(0(x1)))))	(6)
              0(3(0(1(0(x1)))))	→	0(0(3(3(1(0(x1))))))	(38)
              3(3(4(1(0(x1)))))	→	3(1(2(4(3(0(x1))))))	(61)
              3(2(0(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(58)
              3(0(2(1(0(x1)))))	→	2(3(1(5(0(0(x1))))))	(48)
              3(1(0(1(0(x1)))))	→	3(1(1(1(0(0(x1))))))	(53)
              3(0(2(1(0(x1)))))	→	2(0(3(1(1(0(x1))))))	(47)
              0(3(0(1(0(x1)))))	→	0(0(3(1(3(0(x1))))))	(37)
              0(3(4(1(0(x1)))))	→	0(2(0(4(3(1(x1))))))	(41)
              0(5(0(1(0(x1)))))	→	0(0(0(1(5(2(x1))))))	(42)
              3(0(1(1(0(x1)))))	→	3(1(0(1(2(0(x1))))))	(46)
              3(4(0(1(0(x1)))))	→	3(2(0(4(1(0(x1))))))	(66)
              0(2(0(1(0(x1)))))	→	0(2(0(0(3(1(x1))))))	(35)
              3(4(1(0(x1))))	→	3(1(4(2(0(2(x1))))))	(29)
              0(5(0(1(0(x1)))))	→	0(0(1(5(1(0(x1))))))	(43)
              0(0(1(0(x1))))	→	0(2(0(4(1(0(x1))))))	(2)

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

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

              →

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

              (172)

              could be deleted.

              1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

              The dependency pairs are split into 0 components.