Certification Problem

Input (COPS 995)

We consider the TRS containing the following rules:

The underlying signature is as follows:

Property / Task

Answer / Result

Proof (by csi @ CoCo 2020)

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

All redundant rules that were added or removed can be simulated in 2 steps .

1.1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

All redundant rules that were added or removed can be simulated in 2 steps .

1.1.1 Decreasing Diagrams

1.1.1.2 Rule Labeling

• a(a(x))

  →

  c(c(x))

  (12)

  ↦ 5

• c(b(x))

  →

  a(b(x))

  (11)

  ↦ 7

• b(a(x))

  →

  a(b(x))

  (10)

  ↦ 9

• a(c(x))

  →

  a(b(x))

  (9)

  ↦ 15

• c(a(x))

  →

  c(c(x))

  (8)

  ↦ 0

• b(c(x))

  →

  c(c(x))

  (1)

  ↦ 0

• a(a(x))

  →

  a(b(x))

  (2)

  ↦ 12

• c(b(x))

  →

  c(a(x))

  (3)

  ↦ 7

• b(a(x))

  →

  c(a(x))

  (4)

  ↦ 1

• a(c(x))

  →

  c(a(x))

  (5)

  ↦ 15

• c(a(x))

  →

  a(b(x))

  (6)

  ↦ 9

• a(b(x))

  →

  c(c(x))

  (7)

  ↦ 0

• c(b(x))

  →

  c(c(x))

  (13)

  ↦ 0

• b(a(x))

  →

  c(c(x))

  (14)

  ↦ 0

• a(c(x))

  →

  c(c(x))

  (15)

  ↦ 0

• The critical peak s = a(c(c(x915)))←→_ε c(c(a(x915))) = t can be joined as follows.
  s ↔ c(c(c(x915))) ↔ t
• The critical peak s = b(c(c(x916)))←→_ε a(b(a(x916))) = t can be joined as follows.
  s ↔ c(c(c(x916))) ↔ c(c(a(x916))) ↔ t
• The critical peak s = b(c(c(x916)))←→_ε a(b(a(x916))) = t can be joined as follows.
  s ↔ c(c(c(x916))) ↔ a(c(c(x916))) ↔ t
• The critical peak s = c(c(c(x917)))←→_ε c(c(a(x917))) = t can be joined as follows.
  s ↔ c(c(c(x917))) ↔ t
• The critical peak s = c(c(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(c(c(x919)))←→_ε a(b(a(x919))) = t can be joined as follows.
  s ↔ a(c(c(x919))) ↔ t
• The critical peak s = b(c(c(x920)))←→_ε c(a(a(x920))) = t can be joined as follows.
  s ↔ c(c(c(x920))) ↔ t
• The critical peak s = c(c(c(x921)))←→_ε a(b(a(x921))) = t can be joined as follows.
  s ↔ c(c(c(x921))) ↔ c(c(a(x921))) ↔ t
• The critical peak s = c(c(c(x921)))←→_ε a(b(a(x921))) = t can be joined as follows.
  s ↔ c(c(c(x921))) ↔ a(c(c(x921))) ↔ t
• The critical peak s = b(c(c(x922)))←→_ε c(c(a(x922))) = t can be joined as follows.
  s ↔ c(c(c(x922))) ↔ t
• The critical peak s = a(a(b(x923)))←→_ε a(b(b(x923))) = t can be joined as follows.
  s ↔ c(c(b(x923))) ↔ t
• The critical peak s = a(a(b(x923)))←→_ε a(b(b(x923))) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(a(b(x924)))←→_ε c(c(b(x924))) = t can be joined as follows.
  s ↔ c(a(b(x924))) ↔ t
• The critical peak s = b(a(b(x924)))←→_ε c(c(b(x924))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ a(b(x)) ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(a(b(x926)))←→_ε c(a(b(x926))) = t can be joined as follows.
  s ↔ c(c(b(x926))) ↔ t
• The critical peak s = a(a(b(x926)))←→_ε c(a(b(x926))) = t can be joined as follows.
  s ↔ a(b(b(x926))) ↔ t
• The critical peak s = a(b(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(a(b(x928)))←→_ε c(c(b(x928))) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(a(b(x929))) ↔ c(c(a(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(b(x929))) ↔ a(a(b(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ a(b(b(x929))) ↔ c(c(b(x929))) ↔ a(a(b(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ a(b(b(x929))) ↔ a(a(b(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(c(x929))) ↔ c(c(a(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(c(x929))) ↔ a(c(c(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(b(x929))) ↔ c(c(c(x929))) ↔ c(c(a(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(b(x929))) ↔ c(c(c(x929))) ↔ a(c(c(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(b(x929))) ↔ c(c(a(x929))) ↔ t
• The critical peak s = c(a(b(x929)))←→_ε a(b(a(x929))) = t can be joined as follows.
  s ↔ c(c(b(x929))) ↔ c(c(a(x929))) ↔ a(c(a(x929))) ↔ t
• The critical peak s = c(a(b(x930)))←→_ε c(a(a(x930))) = t can be joined as follows.
  s ↔ c(a(b(x930))) ↔ t
• The critical peak s = c(a(b(x930)))←→_ε c(a(a(x930))) = t can be joined as follows.
  s ↔ c(c(c(x930))) ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ a(b(x)) ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ c(c(b(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ a(b(b(x932))) ↔ c(c(b(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ a(b(b(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ c(c(b(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ c(c(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ c(c(b(x932))) ↔ c(c(c(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ c(c(b(x932))) ↔ c(c(c(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ a(c(c(x932))) ↔ c(c(c(x932))) ↔ t
• The critical peak s = a(a(b(x932)))←→_ε c(c(a(x932))) = t can be joined as follows.
  s ↔ a(c(c(x932))) ↔ c(c(c(x932))) ↔ c(a(b(x932))) ↔ t
• The critical peak s = c(a(b(x933)))←→_ε c(c(a(x933))) = t can be joined as follows.
  s ↔ c(a(b(x933))) ↔ t
• The critical peak s = c(a(b(x933)))←→_ε c(c(a(x933))) = t can be joined as follows.
  s ↔ c(c(c(x933))) ↔ t
• The critical peak s = a(b(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(a(b(x935)))←→_ε c(c(c(x935))) = t can be joined as follows.
  s ↔ c(c(b(x935))) ↔ t
• The critical peak s = a(a(b(x935)))←→_ε c(c(c(x935))) = t can be joined as follows.
  s ↔ a(c(c(x935))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ c(a(b(x936))) ↔ c(c(c(x936))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ c(a(b(x936))) ↔ c(c(c(x936))) ↔ a(c(c(x936))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ b(c(c(x936))) ↔ c(c(c(x936))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ b(c(c(x936))) ↔ c(c(c(x936))) ↔ a(c(c(x936))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ c(c(b(x936))) ↔ c(c(c(x936))) ↔ t
• The critical peak s = b(a(b(x936)))←→_ε a(b(c(x936))) = t can be joined as follows.
  s ↔ c(c(b(x936))) ↔ c(c(c(x936))) ↔ a(c(c(x936))) ↔ t
• The critical peak s = c(a(b(x937)))←→_ε c(c(c(x937))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(a(b(x938)))←→_ε a(b(c(x938))) = t can be joined as follows.
  s ↔ a(c(c(x938))) ↔ t
• The critical peak s = b(a(b(x939)))←→_ε c(a(c(x939))) = t can be joined as follows.
  s ↔ c(a(b(x939))) ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ a(b(x)) ↔ t
• The critical peak s = a(b(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(a(b(x941)))←→_ε a(b(c(x941))) = t can be joined as follows.
  s ↔ c(c(c(x941))) ↔ t
• The critical peak s = b(a(b(x942)))←→_ε c(c(c(x942))) = t can be joined as follows.
  s ↔ c(a(b(x942))) ↔ t
• The critical peak s = b(a(b(x942)))←→_ε c(c(c(x942))) = t can be joined as follows.
  s ↔ b(c(c(x942))) ↔ t
• The critical peak s = b(a(b(x942)))←→_ε c(c(c(x942))) = t can be joined as follows.
  s ↔ c(c(b(x942))) ↔ t
• The critical peak s = a(b(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(c(x944)))←→_ε a(b(a(x944))) = t can be joined as follows.
  s ↔ a(c(c(x944))) ↔ t
• The critical peak s = b(c(c(x945)))←→_ε c(c(a(x945))) = t can be joined as follows.
  s ↔ c(c(c(x945))) ↔ t
• The critical peak s = a(c(c(x946)))←→_ε c(a(a(x946))) = t can be joined as follows.
  s ↔ c(c(c(x946))) ↔ t
• The critical peak s = c(c(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(c(c(x948)))←→_ε c(c(a(x948))) = t can be joined as follows.
  s ↔ c(c(c(x948))) ↔ t
• The critical peak s = c(c(c(x949)))←→_ε a(b(c(x949))) = t can be joined as follows.
  s ↔ c(c(c(x949))) ↔ t
• The critical peak s = c(c(c(x950)))←→_ε c(a(c(x950))) = t can be joined as follows.
  s ↔ c(c(c(x950))) ↔ t
• The critical peak s = a(c(c(x951)))←→_ε c(c(c(x951))) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(c(c(x952)))←→_ε c(c(c(x952))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(b(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ c(c(b(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ a(b(b(x954))) ↔ c(c(b(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ a(b(b(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ c(c(b(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ c(c(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ c(c(b(x954))) ↔ c(c(c(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ c(c(b(x954))) ↔ c(c(c(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ a(c(c(x954))) ↔ c(c(c(x954))) ↔ t
• The critical peak s = a(a(b(x954)))←→_ε c(c(a(x954))) = t can be joined as follows.
  s ↔ a(c(c(x954))) ↔ c(c(c(x954))) ↔ c(a(b(x954))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ a(b(b(x955))) ↔ a(a(b(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(a(b(x955))) ↔ a(b(b(x955))) ↔ a(a(b(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(a(b(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ c(a(b(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ a(a(b(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ a(b(b(x955))) ↔ c(c(b(x955))) ↔ a(a(b(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(a(b(x955))) ↔ c(c(b(x955))) ↔ a(a(b(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(a(b(x955))) ↔ c(c(c(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(a(b(x955))) ↔ c(c(c(x955))) ↔ a(c(c(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ b(c(c(x955))) ↔ c(c(c(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ b(c(c(x955))) ↔ c(c(c(x955))) ↔ a(c(c(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ c(c(c(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ c(c(c(x955))) ↔ a(c(c(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ c(c(a(x955))) ↔ t
• The critical peak s = b(a(b(x955)))←→_ε a(b(a(x955))) = t can be joined as follows.
  s ↔ c(c(b(x955))) ↔ c(c(a(x955))) ↔ a(c(a(x955))) ↔ t
• The critical peak s = c(a(b(x956)))←→_ε c(c(a(x956))) = t can be joined as follows.
  s ↔ c(a(b(x956))) ↔ t
• The critical peak s = c(a(b(x956)))←→_ε c(c(a(x956))) = t can be joined as follows.
  s ↔ c(c(c(x956))) ↔ t
• The critical peak s = a(a(b(x957)))←→_ε a(b(a(x957))) = t can be joined as follows.
  s ↔ a(a(b(x957))) ↔ t
• The critical peak s = a(a(b(x957)))←→_ε a(b(a(x957))) = t can be joined as follows.
  s ↔ a(c(c(x957))) ↔ t
• The critical peak s = b(a(b(x958)))←→_ε c(a(a(x958))) = t can be joined as follows.
  s ↔ c(a(b(x958))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(a(b(x959))) ↔ c(c(a(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(b(x959))) ↔ a(a(b(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ a(b(b(x959))) ↔ c(c(b(x959))) ↔ a(a(b(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ a(b(b(x959))) ↔ a(a(b(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(c(x959))) ↔ c(c(a(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(c(x959))) ↔ a(c(c(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(b(x959))) ↔ c(c(c(x959))) ↔ c(c(a(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(b(x959))) ↔ c(c(c(x959))) ↔ a(c(c(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(b(x959))) ↔ c(c(a(x959))) ↔ t
• The critical peak s = c(a(b(x959)))←→_ε a(b(a(x959))) = t can be joined as follows.
  s ↔ c(c(b(x959))) ↔ c(c(a(x959))) ↔ a(c(a(x959))) ↔ t
• The critical peak s = b(a(b(x960)))←→_ε c(c(a(x960))) = t can be joined as follows.
  s ↔ c(a(b(x960))) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(c(a(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ a(b(a(x962))) ↔ c(c(a(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(a(a(x962))) ↔ c(c(a(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ a(c(c(x962))) ↔ c(c(c(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(a(a(x962))) ↔ c(c(c(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(c(a(x962))) ↔ c(c(c(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(a(a(x962))) ↔ c(a(b(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ c(c(a(x962))) ↔ c(a(b(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ a(a(b(x962))) ↔ c(c(b(x962))) ↔ t
• The critical peak s = a(c(a(x962)))←→_ε a(b(b(x962))) = t can be joined as follows.
  s ↔ a(a(b(x962))) ↔ t
• The critical peak s = b(c(a(x963)))←→_ε c(c(b(x963))) = t can be joined as follows.
  s ↔ c(c(a(x963))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(c(a(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(b(a(x964))) ↔ c(c(a(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(a(a(x964))) ↔ c(c(a(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(c(c(x964))) ↔ c(c(c(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(c(c(x964))) ↔ c(c(c(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(a(a(x964))) ↔ c(c(c(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(a(a(x964))) ↔ c(c(c(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(c(a(x964))) ↔ c(c(c(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(c(a(x964))) ↔ c(c(c(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(a(a(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ c(c(a(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(a(b(x964))) ↔ c(c(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(a(b(x964))) ↔ c(c(b(x964))) ↔ a(b(b(x964))) ↔ t
• The critical peak s = a(c(a(x964)))←→_ε c(a(b(x964))) = t can be joined as follows.
  s ↔ a(a(b(x964))) ↔ a(b(b(x964))) ↔ t
• The critical peak s = c(a(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(a(x966)))←→_ε c(c(b(x966))) = t can be joined as follows.
  s ↔ c(c(a(x966))) ↔ t
• The critical peak s = c(c(a(x967)))←→_ε a(b(a(x967))) = t can be joined as follows.
  s ↔ c(c(a(x967))) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(c(a(x969)))←→_ε c(a(a(x969))) = t can be joined as follows.
  s ↔ c(c(a(x969))) ↔ t
• The critical peak s = c(c(a(x969)))←→_ε c(a(a(x969))) = t can be joined as follows.
  s ↔ c(c(c(x969))) ↔ t
• The critical peak s = c(c(a(x969)))←→_ε c(a(a(x969))) = t can be joined as follows.
  s ↔ c(a(b(x969))) ↔ t
• The critical peak s = a(c(a(x970)))←→_ε c(c(a(x970))) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(c(a(x971)))←→_ε c(c(a(x971))) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(a(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(a(x973)))←→_ε c(c(c(x973))) = t can be joined as follows.
  s ↔ a(c(c(x973))) ↔ t
• The critical peak s = a(c(a(x973)))←→_ε c(c(c(x973))) = t can be joined as follows.
  s ↔ c(a(a(x973))) ↔ t
• The critical peak s = a(c(a(x973)))←→_ε c(c(c(x973))) = t can be joined as follows.
  s ↔ c(c(a(x973))) ↔ t
• The critical peak s = b(c(a(x974)))←→_ε a(b(c(x974))) = t can be joined as follows.
  s ↔ b(c(c(x974))) ↔ c(c(c(x974))) ↔ t
• The critical peak s = b(c(a(x974)))←→_ε a(b(c(x974))) = t can be joined as follows.
  s ↔ b(c(c(x974))) ↔ c(c(c(x974))) ↔ a(c(c(x974))) ↔ t
• The critical peak s = b(c(a(x974)))←→_ε a(b(c(x974))) = t can be joined as follows.
  s ↔ c(c(a(x974))) ↔ c(c(c(x974))) ↔ t
• The critical peak s = b(c(a(x974)))←→_ε a(b(c(x974))) = t can be joined as follows.
  s ↔ c(c(a(x974))) ↔ c(c(c(x974))) ↔ a(c(c(x974))) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(a(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = c(c(a(x976)))←→_ε c(c(c(x976))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(a(x977)))←→_ε a(b(c(x977))) = t can be joined as follows.
  s ↔ a(c(c(x977))) ↔ t
• The critical peak s = b(c(a(x978)))←→_ε c(a(c(x978))) = t can be joined as follows.
  s ↔ c(c(a(x978))) ↔ t
• The critical peak s = c(c(a(x979)))←→_ε a(b(c(x979))) = t can be joined as follows.
  s ↔ c(c(c(x979))) ↔ t
• The critical peak s = b(c(a(x980)))←→_ε c(c(c(x980))) = t can be joined as follows.
  s ↔ b(c(c(x980))) ↔ t
• The critical peak s = b(c(a(x980)))←→_ε c(c(c(x980))) = t can be joined as follows.
  s ↔ c(c(a(x980))) ↔ t
• The critical peak s = c(a(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(a(b(x982)))←→_ε a(b(a(x982))) = t can be joined as follows.
  s ↔ a(a(b(x982))) ↔ t
• The critical peak s = a(a(b(x982)))←→_ε a(b(a(x982))) = t can be joined as follows.
  s ↔ a(c(c(x982))) ↔ t
• The critical peak s = a(b(x))←→_ε c(c(x)) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(a(b(x984)))←→_ε c(c(a(x984))) = t can be joined as follows.
  s ↔ c(a(b(x984))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(a(b(x985))) ↔ a(b(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(b(b(x985))) ↔ c(c(b(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(b(b(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(c(c(x985))) ↔ a(b(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(a(b(x985))) ↔ c(c(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(c(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(c(a(x985))) ↔ a(b(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(c(c(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(c(c(x985))) ↔ c(c(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ c(c(b(x985))) ↔ c(c(c(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(c(c(x985))) ↔ c(c(c(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(c(c(x985))) ↔ c(c(c(x985))) ↔ c(c(a(x985))) ↔ t
• The critical peak s = a(a(b(x985)))←→_ε c(a(a(x985))) = t can be joined as follows.
  s ↔ a(c(c(x985))) ↔ c(c(c(x985))) ↔ c(a(b(x985))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ c(c(b(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ a(b(b(x986))) ↔ c(c(b(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ a(b(b(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ c(c(b(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ c(c(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ c(c(b(x986))) ↔ c(c(c(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ c(c(b(x986))) ↔ c(c(c(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ a(c(c(x986))) ↔ c(c(c(x986))) ↔ t
• The critical peak s = a(a(b(x986)))←→_ε c(c(a(x986))) = t can be joined as follows.
  s ↔ a(c(c(x986))) ↔ c(c(c(x986))) ↔ c(a(b(x986))) ↔ t
• The critical peak s = a(c(c(x987)))←→_ε c(c(b(x987))) = t can be joined as follows.
  s ↔ c(c(c(x987))) ↔ t
• The critical peak s = b(c(c(x988)))←→_ε a(b(b(x988))) = t can be joined as follows.
  s ↔ c(c(c(x988))) ↔ c(c(b(x988))) ↔ t
• The critical peak s = c(c(c(x989)))←→_ε c(c(b(x989))) = t can be joined as follows.
  s ↔ c(c(c(x989))) ↔ t
• The critical peak s = a(c(c(x990)))←→_ε a(b(b(x990))) = t can be joined as follows.
  s ↔ c(c(c(x990))) ↔ c(c(b(x990))) ↔ t
• The critical peak s = a(c(c(x990)))←→_ε a(b(b(x990))) = t can be joined as follows.
  s ↔ a(b(c(x990))) ↔ c(c(c(x990))) ↔ c(c(b(x990))) ↔ t
• The critical peak s = a(c(c(x990)))←→_ε a(b(b(x990))) = t can be joined as follows.
  s ↔ c(a(c(x990))) ↔ c(c(c(x990))) ↔ c(c(b(x990))) ↔ t
• The critical peak s = a(c(c(x990)))←→_ε a(b(b(x990))) = t can be joined as follows.
  s ↔ c(a(c(x990))) ↔ c(a(b(x990))) ↔ c(c(b(x990))) ↔ t
• The critical peak s = a(c(c(x990)))←→_ε a(b(b(x990))) = t can be joined as follows.
  s ↔ c(a(c(x990))) ↔ c(c(a(x990))) ↔ c(c(b(x990))) ↔ t
• The critical peak s = b(c(c(x991)))←→_ε c(a(b(x991))) = t can be joined as follows.
  s ↔ c(c(c(x991))) ↔ t
• The critical peak s = c(c(c(x992)))←→_ε a(b(b(x992))) = t can be joined as follows.
  s ↔ c(c(c(x992))) ↔ c(c(b(x992))) ↔ t
• The critical peak s = b(c(c(x993)))←→_ε c(c(b(x993))) = t can be joined as follows.
  s ↔ c(c(c(x993))) ↔ t
• The critical peak s = c(c(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(c(c(x995)))←→_ε a(b(b(x995))) = t can be joined as follows.
  s ↔ c(c(c(x995))) ↔ c(c(b(x995))) ↔ t
• The critical peak s = a(c(c(x995)))←→_ε a(b(b(x995))) = t can be joined as follows.
  s ↔ a(b(c(x995))) ↔ c(c(c(x995))) ↔ c(c(b(x995))) ↔ t
• The critical peak s = a(c(c(x995)))←→_ε a(b(b(x995))) = t can be joined as follows.
  s ↔ c(a(c(x995))) ↔ c(c(c(x995))) ↔ c(c(b(x995))) ↔ t
• The critical peak s = a(c(c(x995)))←→_ε a(b(b(x995))) = t can be joined as follows.
  s ↔ c(a(c(x995))) ↔ c(a(b(x995))) ↔ c(c(b(x995))) ↔ t
• The critical peak s = a(c(c(x995)))←→_ε a(b(b(x995))) = t can be joined as follows.
  s ↔ c(a(c(x995))) ↔ c(c(a(x995))) ↔ c(c(b(x995))) ↔ t
• The critical peak s = b(c(c(x996)))←→_ε c(c(b(x996))) = t can be joined as follows.
  s ↔ c(c(c(x996))) ↔ t
• The critical peak s = c(c(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(c(c(x998)))←→_ε c(a(b(x998))) = t can be joined as follows.
  s ↔ c(c(c(x998))) ↔ t
• The critical peak s = a(c(c(x999)))←→_ε c(c(b(x999))) = t can be joined as follows.
  s ↔ c(c(c(x999))) ↔ t
• The critical peak s = c(c(c(x1000)))←→_ε a(b(a(x1000))) = t can be joined as follows.
  s ↔ c(c(c(x1000))) ↔ c(c(a(x1000))) ↔ t
• The critical peak s = c(c(c(x1000)))←→_ε a(b(a(x1000))) = t can be joined as follows.
  s ↔ c(c(c(x1000))) ↔ a(c(c(x1000))) ↔ t
• The critical peak s = c(c(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(c(c(x1002)))←→_ε c(a(a(x1002))) = t can be joined as follows.
  s ↔ c(c(c(x1002))) ↔ t
• The critical peak s = c(c(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = a(c(c(x1004)))←→_ε c(c(a(x1004))) = t can be joined as follows.
  s ↔ c(c(c(x1004))) ↔ t
• The critical peak s = c(c(c(x1005)))←→_ε c(c(a(x1005))) = t can be joined as follows.
  s ↔ c(c(c(x1005))) ↔ t
• The critical peak s = a(c(c(x1006)))←→_ε c(c(c(x1006))) = t can be joined as follows.
  s ↔ t
• The critical peak s = b(c(c(x1007)))←→_ε a(b(c(x1007))) = t can be joined as follows.
  s ↔ c(c(c(x1007))) ↔ t
• The critical peak s = c(c(x))←→_ε a(b(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(c(c(x1009)))←→_ε c(c(c(x1009))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(c(x1010)))←→_ε a(b(c(x1010))) = t can be joined as follows.
  s ↔ a(c(c(x1010))) ↔ t
• The critical peak s = a(c(c(x1010)))←→_ε a(b(c(x1010))) = t can be joined as follows.
  s ↔ t
• The critical peak s = a(c(c(x1010)))←→_ε a(b(c(x1010))) = t can be joined as follows.
  s ↔ c(c(c(x1010))) ↔ t
• The critical peak s = b(c(c(x1011)))←→_ε c(a(c(x1011))) = t can be joined as follows.
  s ↔ c(c(c(x1011))) ↔ t
• The critical peak s = c(c(x))←→_ε c(a(x)) = t can be joined as follows.
  s ↔ c(c(x)) ↔ t
• The critical peak s = c(c(c(x1013)))←→_ε a(b(c(x1013))) = t can be joined as follows.
  s ↔ c(c(c(x1013))) ↔ t
• The critical peak s = b(c(c(x1014)))←→_ε c(c(c(x1014))) = t can be joined as follows.
  s ↔ t