Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/157593)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

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

  1#(4(4(0(x1))))	→	1#(x1)	(312)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  1#(4(4(0(x1))))	→	0#(1(x1))	(308)
  1#(4(4(1(x1))))	→	1#(4(x1))	(299)
  4#(4(4(1(x1))))	→	4#(1(4(x1)))	(300)
  4#(0(0(1(x1))))	→	0#(4(x1))	(297)
  0#(0(4(1(x1))))	→	1#(0(x1))	(267)
  4#(1(0(0(1(x1)))))	→	1#(0(x1))	(284)
  1#(4(4(0(1(x1)))))	→	1#(4(4(1(2(0(x1))))))	(282)
  1#(4(4(4(1(x1)))))	→	1#(4(4(1(x1))))	(279)
  4#(3(1(5(0(x1)))))	→	1#(x1)	(274)
  0#(4(4(1(x1))))	→	0#(1(x1))	(271)
  1#(4(4(0(1(x1)))))	→	0#(x1)	(269)
  0#(0(4(1(x1))))	→	1#(0(x1))	(267)
  0#(4(4(1(x1))))	→	4#(x1)	(264)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  4#(1(0(0(1(x1)))))	→	0#(1(1(0(x1))))	(261)
  4#(4(4(4(1(x1)))))	→	4#(x1)	(258)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  4#(4(4(1(x1))))	→	1#(4(x1))	(249)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(0(4(0(x1))))	→	0#(0(4(x1)))	(247)
  4#(3(4(0(x1))))	→	0#(3(x1))	(233)
  1#(4(4(4(1(x1)))))	→	4#(1(4(4(1(x1)))))	(243)
  0#(4(4(0(x1))))	→	4#(x1)	(242)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(1(0(0(1(x1)))))	→	0#(x1)	(236)
  4#(3(4(0(x1))))	→	0#(3(x1))	(233)
  0#(0(4(1(x1))))	→	0#(1(0(x1)))	(85)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  0#(4(4(1(x1))))	→	4#(0(1(x1)))	(218)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  4#(0(0(1(x1))))	→	1#(0(4(x1)))	(214)
  4#(1(0(0(1(x1)))))	→	1#(1(0(x1)))	(209)
  4#(0(0(4(1(x1)))))	→	0#(x1)	(206)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  1#(4(4(1(x1))))	→	1#(4(1(x1)))	(123)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  0#(3(4(0(0(x1)))))	→	0#(0(0(x1)))	(194)
  1#(4(4(1(x1))))	→	4#(x1)	(184)
  4#(0(0(4(1(x1)))))	→	0#(1(0(x1)))	(191)
  1#(4(4(1(x1))))	→	4#(x1)	(184)
  4#(3(4(1(x1))))	→	1#(4(x1))	(138)
  0#(4(4(1(x1))))	→	1#(0(x1))	(172)
  0#(4(3(4(0(x1)))))	→	4#(4(0(x1)))	(161)
  4#(0(0(1(x1))))	→	4#(x1)	(160)
  4#(3(4(0(x1))))	→	0#(4(4(5(x1))))	(158)
  4#(4(4(4(1(x1)))))	→	4#(4(4(1(2(4(x1))))))	(159)
  1#(4(4(1(x1))))	→	4#(1(4(1(x1))))	(155)
  4#(0(0(4(1(x1)))))	→	1#(0(x1))	(145)
  4#(0(0(1(x1))))	→	0#(1(0(4(x1))))	(142)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(3(4(1(x1))))	→	1#(4(x1))	(138)
  4#(0(4(0(x1))))	→	0#(4(x1))	(134)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  1#(4(4(1(x1))))	→	1#(4(1(x1)))	(123)
  4#(0(4(0(x1))))	→	4#(x1)	(124)
  0#(0(4(0(0(x1)))))	→	0#(0(0(x1)))	(122)
  4#(3(5(0(1(x1)))))	→	4#(0(1(x1)))	(118)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(3(1(5(0(x1)))))	→	0#(1(x1))	(108)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  0#(4(4(0(x1))))	→	0#(0(x1))	(91)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  0#(0(4(1(x1))))	→	0#(1(0(x1)))	(85)

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

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

  together with the usable rules

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

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

  1#(4(4(0(x1))))	→	1#(x1)	(312)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  1#(4(4(0(x1))))	→	0#(1(x1))	(308)
  1#(4(4(1(x1))))	→	1#(4(x1))	(299)
  4#(4(4(1(x1))))	→	4#(1(4(x1)))	(300)
  4#(0(0(1(x1))))	→	0#(4(x1))	(297)
  0#(0(4(1(x1))))	→	1#(0(x1))	(267)
  4#(1(0(0(1(x1)))))	→	1#(0(x1))	(284)
  1#(4(4(0(1(x1)))))	→	1#(4(4(1(2(0(x1))))))	(282)
  1#(4(4(4(1(x1)))))	→	1#(4(4(1(x1))))	(279)
  4#(3(1(5(0(x1)))))	→	1#(x1)	(274)
  0#(4(4(1(x1))))	→	0#(1(x1))	(271)
  1#(4(4(0(1(x1)))))	→	0#(x1)	(269)
  0#(0(4(1(x1))))	→	1#(0(x1))	(267)
  0#(4(4(1(x1))))	→	4#(x1)	(264)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  4#(1(0(0(1(x1)))))	→	0#(1(1(0(x1))))	(261)
  4#(4(4(4(1(x1)))))	→	4#(x1)	(258)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  4#(4(4(1(x1))))	→	1#(4(x1))	(249)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(0(4(0(x1))))	→	0#(0(4(x1)))	(247)
  4#(3(4(0(x1))))	→	0#(3(x1))	(233)
  1#(4(4(4(1(x1)))))	→	4#(1(4(4(1(x1)))))	(243)
  0#(4(4(0(x1))))	→	4#(x1)	(242)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(1(0(0(1(x1)))))	→	0#(x1)	(236)
  4#(3(4(0(x1))))	→	0#(3(x1))	(233)
  0#(0(4(1(x1))))	→	0#(1(0(x1)))	(85)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  0#(4(4(1(x1))))	→	4#(0(1(x1)))	(218)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  4#(0(0(1(x1))))	→	1#(0(4(x1)))	(214)
  4#(1(0(0(1(x1)))))	→	1#(1(0(x1)))	(209)
  4#(0(0(4(1(x1)))))	→	0#(x1)	(206)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  1#(4(4(1(x1))))	→	1#(4(1(x1)))	(123)
  4#(3(4(1(x1))))	→	4#(x1)	(197)
  0#(3(4(0(0(x1)))))	→	0#(0(0(x1)))	(194)
  1#(4(4(1(x1))))	→	4#(x1)	(184)
  4#(0(0(4(1(x1)))))	→	0#(1(0(x1)))	(191)
  1#(4(4(1(x1))))	→	4#(x1)	(184)
  4#(3(4(1(x1))))	→	1#(4(x1))	(138)
  0#(4(4(1(x1))))	→	1#(0(x1))	(172)
  0#(4(3(4(0(x1)))))	→	4#(4(0(x1)))	(161)
  4#(0(0(1(x1))))	→	4#(x1)	(160)
  4#(3(4(0(x1))))	→	0#(4(4(5(x1))))	(158)
  4#(4(4(4(1(x1)))))	→	4#(4(4(1(2(4(x1))))))	(159)
  1#(4(4(1(x1))))	→	4#(1(4(1(x1))))	(155)
  4#(0(0(4(1(x1)))))	→	1#(0(x1))	(145)
  4#(0(0(1(x1))))	→	0#(1(0(4(x1))))	(142)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(3(4(1(x1))))	→	1#(4(x1))	(138)
  4#(0(4(0(x1))))	→	0#(4(x1))	(134)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  1#(4(4(1(x1))))	→	1#(4(1(x1)))	(123)
  4#(0(4(0(x1))))	→	4#(x1)	(124)
  0#(0(4(0(0(x1)))))	→	0#(0(0(x1)))	(122)
  0#(4(4(1(x1))))	→	0#(x1)	(116)
  4#(3(1(5(0(x1)))))	→	0#(1(x1))	(108)
  0#(0(4(1(x1))))	→	0#(x1)	(93)
  0#(4(4(0(x1))))	→	0#(0(x1))	(91)
  4#(4(4(1(x1))))	→	4#(x1)	(87)
  0#(0(4(1(x1))))	→	0#(1(0(x1)))	(85)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

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

    →

    4#(0(1(x1)))

    (118)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the argument filter

    π(3)

    =

    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(1)	=	2		status(1)	=	[]		list-extension(1)	=	Lex
    prec(4)	=	2		status(4)	=	[]		list-extension(4)	=	Lex
    prec(5)	=	3		status(5)	=	[]		list-extension(5)	=	Lex
    prec(4#)	=	0		status(4#)	=	[1]		list-extension(4#)	=	Lex
    prec(0)	=	0		status(0)	=	[]		list-extension(0)	=	Lex
    prec(2)	=	0		status(2)	=	[]		list-extension(2)	=	Lex
    prec(1#)	=	0		status(1#)	=	[]		list-extension(1#)	=	Lex

    and the following Max-polynomial interpretation

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

    together with the usable rules

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

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

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

    →

    4#(0(1(x1)))

    (118)

    could be deleted.

    1.1.1.1.1.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.