Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/3268)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  5#(4(0(x1)))	→	5#(1(5(2(1(0(x1))))))	(119)
  5#(4(0(x1)))	→	4#(0(4(4(0(x1)))))	(117)
  5#(4(4(x1)))	→	2#(4(x1))	(118)
  5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
  1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
  5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
  5#(4(x1))	→	1#(1(1(x1)))	(116)
  5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
  0#(5(5(0(x1))))	→	2#(0(0(3(0(x1)))))	(75)
  0#(5(5(4(x1))))	→	1#(3(4(3(4(x1)))))	(73)
  5#(4(0(x1)))	→	4#(4(0(x1)))	(72)
  0#(5(5(4(x1))))	→	3#(4(3(4(x1))))	(115)
  0#(5(5(x1)))	→	1#(0(1(3(4(2(x1))))))	(71)
  5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
  4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
  0#(5(5(0(x1))))	→	0#(0(3(0(x1))))	(68)
  3#(5(4(x1)))	→	3#(x1)	(67)
  0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
  3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
  5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
  4#(1(4(x1)))	→	1#(x1)	(64)
  1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
  1#(4(x1))	→	2#(4(x1))	(63)
  5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
  5#(4(x1))	→	4#(2(3(1(1(1(x1))))))	(112)
  5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
  1#(4(x1))	→	2#(2(4(x1)))	(111)
  0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
  5#(4(x1))	→	3#(1(1(1(x1))))	(110)
  5#(5(4(x1)))	→	4#(4(1(2(2(x1)))))	(59)
  0#(5(5(4(x1))))	→	4#(3(4(x1)))	(109)
  0#(5(5(x1)))	→	2#(x1)	(58)
  5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
  1#(4(x1))	→	1#(2(2(4(x1))))	(57)
  1#(4(5(4(x1))))	→	5#(0(2(1(x1))))	(107)
  4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
  2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
  1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
  5#(4(0(0(x1))))	→	2#(x1)	(104)
  5#(4(0(0(x1))))	→	0#(2(2(x1)))	(55)
  5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
  3#(5(4(x1)))	→	2#(3(x1))	(54)
  3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
  0#(5(5(4(x1))))	→	0#(1(3(4(3(4(x1))))))	(52)
  5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
  1#(5(4(x1)))	→	0#(2(5(2(0(4(x1))))))	(51)
  0#(5(5(0(x1))))	→	0#(3(0(x1)))	(100)
  5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
  0#(5(5(x1)))	→	0#(1(3(4(2(x1)))))	(50)
  0#(5(5(4(x1))))	→	3#(4(x1))	(99)
  4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
  2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
  1#(5(4(x1)))	→	0#(4(x1))	(47)
  4#(3(0(5(x1))))	→	5#(5(x1))	(98)
  4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
  5#(4(x1))	→	1#(x1)	(45)
  5#(5(4(x1)))	→	2#(2(x1))	(97)
  5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
  1#(4(5(4(x1))))	→	2#(1(x1))	(44)
  1#(4(5(5(x1))))	→	4#(1(x1))	(96)
  4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
  1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
  1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
  1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
  1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
  5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
  0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
  5#(4(0(x1)))	→	1#(0(x1))	(93)
  1#(5(4(x1)))	→	5#(2(0(4(x1))))	(37)
  5#(5(4(x1)))	→	2#(x1)	(92)
  2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
  0#(3(0(x1)))	→	2#(0(x1))	(35)
  5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
  4#(1(4(x1)))	→	3#(1(x1))	(90)
  0#(5(5(x1)))	→	1#(3(4(2(x1))))	(34)
  5#(4(x1))	→	1#(1(x1))	(89)
  5#(4(0(0(x1))))	→	4#(0(2(2(x1))))	(33)
  5#(4(0(0(x1))))	→	2#(2(x1))	(32)
  0#(3(0(x1)))	→	0#(2(0(x1)))	(88)
  1#(4(5(4(x1))))	→	0#(2(1(x1)))	(31)
  5#(4(0(2(x1))))	→	5#(0(2(x1)))	(86)
  0#(5(5(0(x1))))	→	3#(0(x1))	(87)
  0#(5(5(x1)))	→	4#(2(x1))	(85)
  4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
  5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
  0#(5(5(x1)))	→	3#(4(2(x1)))	(84)
  4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
  3#(5(4(x1)))	→	4#(2(3(x1)))	(83)
  5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
  1#(4(5(5(x1))))	→	0#(0(1(3(4(1(x1))))))	(25)
  2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
  1#(4(5(4(x1))))	→	1#(x1)	(82)
  1#(4(5(5(x1))))	→	1#(x1)	(80)
  3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
  1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)
  0#(5(5(0(x1))))	→	0#(2(0(0(3(0(x1))))))	(23)
  1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
  4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
  5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)
  5#(4(0(x1)))	→	5#(2(1(0(x1))))	(79)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

  0(5(5(x1)))	→	1(0(1(3(4(2(x1))))))	(4)
  1(4(5(5(x1))))	→	0(0(1(3(4(1(x1))))))	(15)
  1(4(x1))	→	3(1(1(2(2(4(x1))))))	(1)
  0(3(0(x1)))	→	2(1(1(0(2(0(x1))))))	(3)
  2(5(4(0(x1))))	→	0(4(1(2(4(0(x1))))))	(16)
  4(3(0(5(x1))))	→	3(3(2(3(5(5(x1))))))	(17)
  1(5(4(x1)))	→	0(2(5(2(0(4(x1))))))	(5)
  4(1(4(x1)))	→	3(3(2(2(3(1(x1))))))	(7)
  1(4(5(4(x1))))	→	0(4(5(0(2(1(x1))))))	(14)
  0(5(5(0(x1))))	→	0(2(0(0(3(0(x1))))))	(12)
  0(5(5(4(x1))))	→	0(1(3(4(3(4(x1))))))	(13)
  3(5(4(x1)))	→	4(1(3(4(2(3(x1))))))	(6)

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

  0#(5(5(0(x1))))	→	2#(0(0(3(0(x1)))))	(75)
  0#(5(5(4(x1))))	→	1#(3(4(3(4(x1)))))	(73)
  0#(5(5(4(x1))))	→	3#(4(3(4(x1))))	(115)
  0#(5(5(x1)))	→	1#(0(1(3(4(2(x1))))))	(71)
  0#(5(5(0(x1))))	→	0#(0(3(0(x1))))	(68)
  0#(5(5(4(x1))))	→	4#(3(4(x1)))	(109)
  0#(5(5(x1)))	→	2#(x1)	(58)
  0#(5(5(4(x1))))	→	0#(1(3(4(3(4(x1))))))	(52)
  0#(5(5(0(x1))))	→	0#(3(0(x1)))	(100)
  0#(5(5(x1)))	→	0#(1(3(4(2(x1)))))	(50)
  0#(5(5(4(x1))))	→	3#(4(x1))	(99)
  0#(5(5(x1)))	→	1#(3(4(2(x1))))	(34)
  0#(5(5(0(x1))))	→	3#(0(x1))	(87)
  0#(5(5(x1)))	→	4#(2(x1))	(85)
  0#(5(5(x1)))	→	3#(4(2(x1)))	(84)
  0#(5(5(0(x1))))	→	0#(2(0(0(3(0(x1))))))	(23)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    5#(4(0(0(x1))))	→	2#(x1)	(104)
    5#(4(0(0(x1))))	→	2#(2(x1))	(32)
    5#(4(0(0(x1))))	→	0#(2(2(x1)))	(55)
    5#(4(0(0(x1))))	→	4#(0(2(2(x1))))	(33)
    5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
    5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
    1#(4(5(5(x1))))	→	1#(x1)	(80)
    1#(4(5(5(x1))))	→	4#(1(x1))	(96)
    1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
    1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
    1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
    1#(4(5(5(x1))))	→	0#(0(1(3(4(1(x1))))))	(25)
    5#(4(0(x1)))	→	4#(4(0(x1)))	(72)
    5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
    5#(4(0(x1)))	→	4#(0(4(4(0(x1)))))	(117)
    5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
    1#(4(x1))	→	2#(4(x1))	(63)
    1#(4(x1))	→	2#(2(4(x1)))	(111)
    1#(4(x1))	→	1#(2(2(4(x1))))	(57)
    1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
    1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
    0#(3(0(x1)))	→	2#(0(x1))	(35)
    0#(3(0(x1)))	→	0#(2(0(x1)))	(88)
    0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
    0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
    0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
    2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
    2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
    2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
    2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
    5#(4(0(2(x1))))	→	5#(0(2(x1)))	(86)
    5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
    5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
    5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
    4#(3(0(5(x1))))	→	5#(5(x1))	(98)
    4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
    4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
    4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
    4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
    1#(5(4(x1)))	→	0#(4(x1))	(47)
    1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
    1#(5(4(x1)))	→	5#(2(0(4(x1))))	(37)
    1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
    1#(5(4(x1)))	→	0#(2(5(2(0(4(x1))))))	(51)
    5#(4(4(x1)))	→	2#(4(x1))	(118)
    5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
    5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
    5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
    5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
    4#(1(4(x1)))	→	1#(x1)	(64)
    4#(1(4(x1)))	→	3#(1(x1))	(90)
    4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
    4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
    4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
    4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
    1#(4(5(4(x1))))	→	1#(x1)	(82)
    1#(4(5(4(x1))))	→	2#(1(x1))	(44)
    1#(4(5(4(x1))))	→	0#(2(1(x1)))	(31)
    1#(4(5(4(x1))))	→	5#(0(2(1(x1))))	(107)
    1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)
    1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
    5#(5(4(x1)))	→	2#(x1)	(92)
    5#(5(4(x1)))	→	2#(2(x1))	(97)
    5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
    5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
    5#(5(4(x1)))	→	4#(4(1(2(2(x1)))))	(59)
    5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
    5#(4(0(x1)))	→	1#(0(x1))	(93)
    5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
    5#(4(0(x1)))	→	5#(2(1(0(x1))))	(79)
    5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
    5#(4(0(x1)))	→	5#(1(5(2(1(0(x1))))))	(119)
    3#(5(4(x1)))	→	3#(x1)	(67)
    3#(5(4(x1)))	→	2#(3(x1))	(54)
    3#(5(4(x1)))	→	4#(2(3(x1)))	(83)
    3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
    3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
    3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
    5#(4(x1))	→	1#(x1)	(45)
    5#(4(x1))	→	1#(1(x1))	(89)
    5#(4(x1))	→	1#(1(1(x1)))	(116)
    5#(4(x1))	→	3#(1(1(1(x1))))	(110)
    5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)
    5#(4(x1))	→	4#(2(3(1(1(1(x1))))))	(112)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

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

    together with the usable rules

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

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

    5#(4(0(2(x1))))	→	5#(0(2(x1)))	(86)
    1#(5(4(x1)))	→	5#(2(0(4(x1))))	(37)
    1#(4(5(4(x1))))	→	5#(0(2(1(x1))))	(107)
    5#(4(0(x1)))	→	5#(2(1(0(x1))))	(79)
    5#(4(0(x1)))	→	5#(1(5(2(1(0(x1))))))	(119)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 1 component.

    • The 1^st component contains the pair

      5#(4(0(0(x1))))	→	2#(x1)	(104)
      5#(4(0(0(x1))))	→	2#(2(x1))	(32)
      5#(4(0(0(x1))))	→	0#(2(2(x1)))	(55)
      5#(4(0(0(x1))))	→	4#(0(2(2(x1))))	(33)
      5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
      5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
      1#(4(5(5(x1))))	→	1#(x1)	(80)
      1#(4(5(5(x1))))	→	4#(1(x1))	(96)
      1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
      1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
      1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
      1#(4(5(5(x1))))	→	0#(0(1(3(4(1(x1))))))	(25)
      5#(4(0(x1)))	→	4#(4(0(x1)))	(72)
      5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
      5#(4(0(x1)))	→	4#(0(4(4(0(x1)))))	(117)
      5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
      1#(4(x1))	→	2#(4(x1))	(63)
      1#(4(x1))	→	2#(2(4(x1)))	(111)
      1#(4(x1))	→	1#(2(2(4(x1))))	(57)
      1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
      1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
      0#(3(0(x1)))	→	2#(0(x1))	(35)
      0#(3(0(x1)))	→	0#(2(0(x1)))	(88)
      0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
      0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
      0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
      2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
      2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
      2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
      2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
      5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
      5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
      5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
      4#(3(0(5(x1))))	→	5#(5(x1))	(98)
      4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
      4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
      4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
      4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
      1#(5(4(x1)))	→	0#(4(x1))	(47)
      1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
      1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
      1#(5(4(x1)))	→	0#(2(5(2(0(4(x1))))))	(51)
      5#(4(4(x1)))	→	2#(4(x1))	(118)
      5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
      5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
      5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
      5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
      4#(1(4(x1)))	→	1#(x1)	(64)
      4#(1(4(x1)))	→	3#(1(x1))	(90)
      4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
      4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
      4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
      4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
      1#(4(5(4(x1))))	→	1#(x1)	(82)
      1#(4(5(4(x1))))	→	2#(1(x1))	(44)
      1#(4(5(4(x1))))	→	0#(2(1(x1)))	(31)
      1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)
      1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
      5#(5(4(x1)))	→	2#(x1)	(92)
      5#(5(4(x1)))	→	2#(2(x1))	(97)
      5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
      5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
      5#(5(4(x1)))	→	4#(4(1(2(2(x1)))))	(59)
      5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
      5#(4(0(x1)))	→	1#(0(x1))	(93)
      5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
      5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
      3#(5(4(x1)))	→	3#(x1)	(67)
      3#(5(4(x1)))	→	2#(3(x1))	(54)
      3#(5(4(x1)))	→	4#(2(3(x1)))	(83)
      3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
      3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
      3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
      5#(4(x1))	→	1#(x1)	(45)
      5#(4(x1))	→	1#(1(x1))	(89)
      5#(4(x1))	→	1#(1(1(x1)))	(116)
      5#(4(x1))	→	3#(1(1(1(x1))))	(110)
      5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)
      5#(4(x1))	→	4#(2(3(1(1(1(x1))))))	(112)

      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)]	=	36237
      [5(x1)]	=	x1 + 26954
      [3(x1)]	=	36237
      [2#(x1)]	=	36237
      [4#(x1)]	=	36237
      [0(x1)]	=	36236
      [3#(x1)]	=	36237
      [5#(x1)]	=	36237
      [2(x1)]	=	36236
      [1#(x1)]	=	36237

      together with the usable rules

      0(5(5(x1)))	→	1(0(1(3(4(2(x1))))))	(4)
      1(4(5(5(x1))))	→	0(0(1(3(4(1(x1))))))	(15)
      1(4(x1))	→	3(1(1(2(2(4(x1))))))	(1)
      0(3(0(x1)))	→	2(1(1(0(2(0(x1))))))	(3)
      2(5(4(0(x1))))	→	0(4(1(2(4(0(x1))))))	(16)
      4(3(0(5(x1))))	→	3(3(2(3(5(5(x1))))))	(17)
      1(5(4(x1)))	→	0(2(5(2(0(4(x1))))))	(5)
      4(1(4(x1)))	→	3(3(2(2(3(1(x1))))))	(7)
      1(4(5(4(x1))))	→	0(4(5(0(2(1(x1))))))	(14)
      0(5(5(0(x1))))	→	0(2(0(0(3(0(x1))))))	(12)
      0(5(5(4(x1))))	→	0(1(3(4(3(4(x1))))))	(13)
      3(5(4(x1)))	→	4(1(3(4(2(3(x1))))))	(6)

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

      5#(4(0(0(x1))))	→	0#(2(2(x1)))	(55)
      1#(4(5(5(x1))))	→	0#(0(1(3(4(1(x1))))))	(25)
      0#(3(0(x1)))	→	0#(2(0(x1)))	(88)
      1#(5(4(x1)))	→	0#(2(5(2(0(4(x1))))))	(51)
      1#(4(5(4(x1))))	→	0#(2(1(x1)))	(31)

      could be deleted.

      1.1.1.1.1.1.1.1 Dependency Graph Processor

      The dependency pairs are split into 1 component.

      • The 1^st component contains the pair

        5#(4(0(0(x1))))	→	2#(x1)	(104)
        5#(4(0(0(x1))))	→	2#(2(x1))	(32)
        5#(4(0(0(x1))))	→	4#(0(2(2(x1))))	(33)
        5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
        5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
        1#(4(5(5(x1))))	→	1#(x1)	(80)
        1#(4(5(5(x1))))	→	4#(1(x1))	(96)
        1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
        1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
        1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
        5#(4(0(x1)))	→	4#(4(0(x1)))	(72)
        5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
        5#(4(0(x1)))	→	4#(0(4(4(0(x1)))))	(117)
        5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
        1#(4(x1))	→	2#(4(x1))	(63)
        1#(4(x1))	→	2#(2(4(x1)))	(111)
        1#(4(x1))	→	1#(2(2(4(x1))))	(57)
        1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
        1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
        0#(3(0(x1)))	→	2#(0(x1))	(35)
        0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
        0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
        0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
        2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
        2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
        2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
        2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
        5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
        5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
        5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
        4#(3(0(5(x1))))	→	5#(5(x1))	(98)
        4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
        4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
        4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
        4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
        1#(5(4(x1)))	→	0#(4(x1))	(47)
        1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
        1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
        5#(4(4(x1)))	→	2#(4(x1))	(118)
        5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
        5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
        5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
        5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
        4#(1(4(x1)))	→	1#(x1)	(64)
        4#(1(4(x1)))	→	3#(1(x1))	(90)
        4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
        4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
        4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
        4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
        1#(4(5(4(x1))))	→	1#(x1)	(82)
        1#(4(5(4(x1))))	→	2#(1(x1))	(44)
        1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)
        1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
        5#(5(4(x1)))	→	2#(x1)	(92)
        5#(5(4(x1)))	→	2#(2(x1))	(97)
        5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
        5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
        5#(5(4(x1)))	→	4#(4(1(2(2(x1)))))	(59)
        5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
        5#(4(0(x1)))	→	1#(0(x1))	(93)
        5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
        5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
        3#(5(4(x1)))	→	3#(x1)	(67)
        3#(5(4(x1)))	→	2#(3(x1))	(54)
        3#(5(4(x1)))	→	4#(2(3(x1)))	(83)
        3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
        3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
        3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
        5#(4(x1))	→	1#(x1)	(45)
        5#(4(x1))	→	1#(1(x1))	(89)
        5#(4(x1))	→	1#(1(1(x1)))	(116)
        5#(4(x1))	→	3#(1(1(1(x1))))	(110)
        5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)
        5#(4(x1))	→	4#(2(3(1(1(1(x1))))))	(112)

        1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

        Using the Max-polynomial interpretation

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

        together with the usable rules

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

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

        5#(4(0(0(x1))))	→	4#(0(2(2(x1))))	(33)
        5#(4(0(x1)))	→	4#(4(0(x1)))	(72)
        5#(4(0(x1)))	→	4#(0(4(4(0(x1)))))	(117)
        5#(5(4(x1)))	→	4#(4(1(2(2(x1)))))	(59)
        3#(5(4(x1)))	→	4#(2(3(x1)))	(83)
        5#(4(x1))	→	4#(2(3(1(1(1(x1))))))	(112)

        could be deleted.

        1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

        The dependency pairs are split into 1 component.

        • The 1^st component contains the pair

          5#(4(0(0(x1))))	→	2#(x1)	(104)
          5#(4(0(0(x1))))	→	2#(2(x1))	(32)
          5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
          5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
          1#(4(5(5(x1))))	→	1#(x1)	(80)
          1#(4(5(5(x1))))	→	4#(1(x1))	(96)
          1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
          1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
          1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
          5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
          5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
          1#(4(x1))	→	2#(4(x1))	(63)
          1#(4(x1))	→	2#(2(4(x1)))	(111)
          1#(4(x1))	→	1#(2(2(4(x1))))	(57)
          1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
          1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
          0#(3(0(x1)))	→	2#(0(x1))	(35)
          0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
          0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
          0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
          2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
          2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
          2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
          2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
          5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
          5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
          5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
          4#(3(0(5(x1))))	→	5#(5(x1))	(98)
          4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
          4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
          4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
          4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
          1#(5(4(x1)))	→	0#(4(x1))	(47)
          1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
          1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
          5#(4(4(x1)))	→	2#(4(x1))	(118)
          5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
          5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
          5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
          5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
          4#(1(4(x1)))	→	1#(x1)	(64)
          4#(1(4(x1)))	→	3#(1(x1))	(90)
          4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
          4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
          4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
          4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
          1#(4(5(4(x1))))	→	1#(x1)	(82)
          1#(4(5(4(x1))))	→	2#(1(x1))	(44)
          1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)
          1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
          5#(5(4(x1)))	→	2#(x1)	(92)
          5#(5(4(x1)))	→	2#(2(x1))	(97)
          5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
          5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
          5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
          5#(4(0(x1)))	→	1#(0(x1))	(93)
          5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
          5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
          3#(5(4(x1)))	→	3#(x1)	(67)
          3#(5(4(x1)))	→	2#(3(x1))	(54)
          3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
          3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
          3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
          5#(4(x1))	→	1#(x1)	(45)
          5#(4(x1))	→	1#(1(x1))	(89)
          5#(4(x1))	→	1#(1(1(x1)))	(116)
          5#(4(x1))	→	3#(1(1(1(x1))))	(110)
          5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)

          1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

          Using the argument filter

          π(3)	=	1
          π(4#)	=	1

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

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

          and the following Max-polynomial interpretation

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

          together with the usable rules

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

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

          5#(4(0(2(x1))))	→	4#(5(0(2(x1))))	(102)
          1#(4(5(4(x1))))	→	4#(5(0(2(1(x1)))))	(24)

          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

            5#(4(0(0(x1))))	→	2#(x1)	(104)
            5#(4(0(0(x1))))	→	2#(2(x1))	(32)
            5#(4(0(0(x1))))	→	0#(4(0(2(2(x1)))))	(65)
            5#(4(0(0(x1))))	→	1#(0(4(0(2(2(x1))))))	(29)
            1#(4(5(5(x1))))	→	1#(x1)	(80)
            1#(4(5(5(x1))))	→	4#(1(x1))	(96)
            1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
            1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
            1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
            5#(4(0(x1)))	→	0#(4(4(0(x1))))	(62)
            5#(4(0(x1)))	→	2#(4(0(4(4(0(x1))))))	(69)
            1#(4(x1))	→	2#(4(x1))	(63)
            1#(4(x1))	→	2#(2(4(x1)))	(111)
            1#(4(x1))	→	1#(2(2(4(x1))))	(57)
            1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
            1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
            0#(3(0(x1)))	→	2#(0(x1))	(35)
            0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
            0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
            0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
            2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
            2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
            2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
            2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
            5#(4(0(2(x1))))	→	0#(4(5(0(2(x1)))))	(74)
            5#(4(0(2(x1))))	→	3#(0(4(5(0(2(x1))))))	(43)
            4#(3(0(5(x1))))	→	5#(5(x1))	(98)
            4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
            4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
            4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
            4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)
            1#(5(4(x1)))	→	0#(4(x1))	(47)
            1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
            1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
            5#(4(4(x1)))	→	2#(4(x1))	(118)
            5#(4(4(x1)))	→	3#(2(4(x1)))	(77)
            5#(4(4(x1)))	→	1#(3(2(4(x1))))	(39)
            5#(4(4(x1)))	→	1#(1(3(2(4(x1)))))	(36)
            5#(4(4(x1)))	→	4#(1(1(3(2(4(x1))))))	(27)
            4#(1(4(x1)))	→	1#(x1)	(64)
            4#(1(4(x1)))	→	3#(1(x1))	(90)
            4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
            4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
            4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
            4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
            1#(4(5(4(x1))))	→	1#(x1)	(82)
            1#(4(5(4(x1))))	→	2#(1(x1))	(44)
            1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
            5#(5(4(x1)))	→	2#(x1)	(92)
            5#(5(4(x1)))	→	2#(2(x1))	(97)
            5#(5(4(x1)))	→	1#(2(2(x1)))	(103)
            5#(5(4(x1)))	→	4#(1(2(2(x1))))	(78)
            5#(5(4(x1)))	→	3#(4(4(1(2(2(x1))))))	(61)
            5#(4(0(x1)))	→	1#(0(x1))	(93)
            5#(4(0(x1)))	→	2#(1(0(x1)))	(108)
            5#(4(0(x1)))	→	1#(5(2(1(0(x1)))))	(101)
            3#(5(4(x1)))	→	3#(x1)	(67)
            3#(5(4(x1)))	→	2#(3(x1))	(54)
            3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
            3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
            3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)
            5#(4(x1))	→	1#(x1)	(45)
            5#(4(x1))	→	1#(1(x1))	(89)
            5#(4(x1))	→	1#(1(1(x1)))	(116)
            5#(4(x1))	→	3#(1(1(1(x1))))	(110)
            5#(4(x1))	→	2#(3(1(1(1(x1)))))	(20)

            1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

            Using the Max-polynomial interpretation

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

            together with the usable rules

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

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

            4#(3(0(5(x1))))	→	5#(5(x1))	(98)
            4#(3(0(5(x1))))	→	3#(5(5(x1)))	(46)
            4#(3(0(5(x1))))	→	2#(3(5(5(x1))))	(42)
            4#(3(0(5(x1))))	→	3#(2(3(5(5(x1)))))	(56)
            4#(3(0(5(x1))))	→	3#(3(2(3(5(5(x1))))))	(70)

            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

              1#(4(5(5(x1))))	→	1#(x1)	(80)
              1#(4(5(5(x1))))	→	4#(1(x1))	(96)
              1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
              1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
              1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
              1#(4(x1))	→	2#(4(x1))	(63)
              1#(4(x1))	→	2#(2(4(x1)))	(111)
              1#(4(x1))	→	1#(2(2(4(x1))))	(57)
              1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
              1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
              0#(3(0(x1)))	→	2#(0(x1))	(35)
              0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
              0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
              0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
              2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
              2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
              2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
              2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
              1#(5(4(x1)))	→	0#(4(x1))	(47)
              1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
              1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
              4#(1(4(x1)))	→	1#(x1)	(64)
              4#(1(4(x1)))	→	3#(1(x1))	(90)
              4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
              4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
              4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
              4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
              1#(4(5(4(x1))))	→	1#(x1)	(82)
              1#(4(5(4(x1))))	→	2#(1(x1))	(44)
              1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
              3#(5(4(x1)))	→	3#(x1)	(67)
              3#(5(4(x1)))	→	2#(3(x1))	(54)
              3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
              3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
              3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)

              1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

              Using the Max-polynomial interpretation

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

              together with the usable rules

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

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

              1#(4(x1))	→	2#(4(x1))	(63)
              1#(4(x1))	→	2#(2(4(x1)))	(111)
              0#(3(0(x1)))	→	2#(0(x1))	(35)
              0#(3(0(x1)))	→	2#(1(1(0(2(0(x1))))))	(66)
              2#(5(4(0(x1))))	→	2#(4(0(x1)))	(106)
              1#(5(4(x1)))	→	2#(0(4(x1)))	(113)
              4#(1(4(x1)))	→	2#(3(1(x1)))	(22)
              4#(1(4(x1)))	→	2#(2(3(1(x1))))	(28)
              1#(4(5(4(x1))))	→	2#(1(x1))	(44)
              3#(5(4(x1)))	→	2#(3(x1))	(54)

              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 1 component.

              • The 1^st component contains the pair

                1#(4(5(5(x1))))	→	1#(x1)	(80)
                1#(4(5(5(x1))))	→	4#(1(x1))	(96)
                1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
                1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
                1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
                1#(4(x1))	→	1#(2(2(4(x1))))	(57)
                1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
                1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
                0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
                0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
                2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
                2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
                2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
                1#(5(4(x1)))	→	0#(4(x1))	(47)
                1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
                4#(1(4(x1)))	→	1#(x1)	(64)
                4#(1(4(x1)))	→	3#(1(x1))	(90)
                4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
                4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
                1#(4(5(4(x1))))	→	1#(x1)	(82)
                1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
                3#(5(4(x1)))	→	3#(x1)	(67)
                3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
                3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
                3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

                Using the Max-polynomial interpretation

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

                together with the usable rules

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

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

                1#(4(5(5(x1))))	→	1#(x1)	(80)
                1#(4(5(5(x1))))	→	4#(1(x1))	(96)
                1#(4(5(5(x1))))	→	3#(4(1(x1)))	(21)
                1#(4(5(5(x1))))	→	1#(3(4(1(x1))))	(105)
                1#(4(5(5(x1))))	→	0#(1(3(4(1(x1)))))	(95)
                1#(4(x1))	→	1#(2(2(4(x1))))	(57)
                1#(4(x1))	→	1#(1(2(2(4(x1)))))	(40)
                1#(4(x1))	→	3#(1(1(2(2(4(x1))))))	(41)
                0#(3(0(x1)))	→	1#(0(2(0(x1))))	(38)
                0#(3(0(x1)))	→	1#(1(0(2(0(x1)))))	(60)
                2#(5(4(0(x1))))	→	1#(2(4(0(x1))))	(48)
                2#(5(4(0(x1))))	→	4#(1(2(4(0(x1)))))	(26)
                2#(5(4(0(x1))))	→	0#(4(1(2(4(0(x1))))))	(91)
                1#(5(4(x1)))	→	0#(4(x1))	(47)
                1#(5(4(x1)))	→	2#(5(2(0(4(x1)))))	(76)
                4#(1(4(x1)))	→	1#(x1)	(64)
                4#(1(4(x1)))	→	3#(1(x1))	(90)
                4#(1(4(x1)))	→	3#(2(2(3(1(x1)))))	(30)
                4#(1(4(x1)))	→	3#(3(2(2(3(1(x1))))))	(49)
                1#(4(5(4(x1))))	→	1#(x1)	(82)
                1#(4(5(4(x1))))	→	0#(4(5(0(2(1(x1))))))	(94)
                3#(5(4(x1)))	→	3#(x1)	(67)
                3#(5(4(x1)))	→	3#(4(2(3(x1))))	(53)
                3#(5(4(x1)))	→	1#(3(4(2(3(x1)))))	(114)
                3#(5(4(x1)))	→	4#(1(3(4(2(3(x1))))))	(81)

                could be deleted.

                1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

                The dependency pairs are split into 0 components.