YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
|
+(x,y) |
→ |
+(y,x) |
|
+(s(x),y) |
→ |
+(x,s(y)) |
|
+(x,s(y)) |
→ |
+(s(x),y) |
|
*(x,s(y)) |
→ |
+(x,*(x,y)) |
|
*(s(x),y) |
→ |
+(*(x,y),y) |
|
*(x,y) |
→ |
*(y,x) |
|
sq(x) |
→ |
*(x,x) |
|
sq(s(x)) |
→ |
+(*(x,x),s(+(x,x))) |
Proof
1 Decreasing Diagrams
1.1 Relative Termination Proof
The duplicating rules (R) terminate relative to the other rules (S).
1.1.1 Rule Removal
Using the
non-linear polynomial interpretation over the naturals
| [s(x1)] |
= |
1 · x1 + 0 · x1 · x1 + 2 |
| [sq(x1)] |
= |
2 · x1 + 2 · x1 · x1 + 0 |
| [+(x1, x2)] |
= |
1 · x1 + 1 · x2 + 0 · x1 · x1 + 0 · x1 · x2 + 0 · x2 · x1 + 0 · x2 · x2 + 0 |
| [*(x1, x2)] |
= |
1 · x1 + 1 · x2 + 0 · x1 · x1 + 1 · x1 · x2 + 0 · x2 · x1 + 0 · x2 · x2 + 0 |
the
rule
remains in R.
Moreover,
the
rules
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
|
+(x,y) |
→ |
+(y,x) |
|
+(s(x),y) |
→ |
+(x,s(y)) |
|
+(x,s(y)) |
→ |
+(s(x),y) |
|
*(x,y) |
→ |
*(y,x) |
remain in S.
1.1.1.1 Rule Removal
Using the
non-linear polynomial interpretation over the naturals
| [s(x1)] |
= |
1 · x1 + 0 · x1 · x1 + 0 |
| [sq(x1)] |
= |
0 · x1 + 2 · x1 · x1 + 1 |
| [+(x1, x2)] |
= |
1 · x1 + 1 · x2 + 0 · x1 · x1 + 0 · x1 · x2 + 0 · x2 · x1 + 0 · x2 · x2 + 0 |
| [*(x1, x2)] |
= |
0 · x1 + 0 · x2 + 1 · x1 · x1 + 0 · x1 · x2 + 0 · x2 · x1 + 1 · x2 · x2 + 0 |
all rules of R could be removed.
Moreover,
the
rules
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
|
+(x,y) |
→ |
+(y,x) |
|
+(s(x),y) |
→ |
+(x,s(y)) |
|
+(x,s(y)) |
→ |
+(s(x),y) |
|
*(x,y) |
→ |
*(y,x) |
remain in S.
1.1.1.1.1 R is empty
There are no rules in the TRS R. Hence, R/S is relative terminating.
1.2 Rule Labeling
Confluence is proven, because all critical peaks can be joined decreasingly
using the following rule labeling function (rules that are not shown have label 0).
-
+(x,+(y,z))→+(+(x,y),z) ↦ 0
-
+(+(x,y),z)→+(x,+(y,z)) ↦ 0
-
+(x,y)→+(y,x) ↦ 0
-
+(s(x),y)→+(x,s(y)) ↦ 0
-
+(x,s(y))→+(s(x),y) ↦ 0
-
*(x,s(y))→+(x,*(x,y)) ↦ 1
-
*(s(x),y)→+(*(x,y),y) ↦ 1
-
*(x,y)→*(y,x) ↦ 0
-
sq(x)→*(x,x) ↦ 10
-
sq(s(x))→+(*(x,x),s(+(x,x))) ↦ 4
All critical pairs are joinable:
-
+(x,+(+(y,x344),x345))→+(x,+(y,+(x344,x345)))←+(+(x,y),+(x344,x345))
-
+(+(+(x,y),x347),x348)→+(+(x,y),+(x347,x348))←+(x,+(y,+(x347,x348)))
-
+(+(+(x,x350),x351),z)→+(+(x,+(x350,x351)),z)←+(x,+(+(x350,x351),z))
-
+(+(x,x353),x354)→+(x,+(x353,x354))←+(+(x353,x354),x)
-
+(+(s(x),x356),x357)→+(s(x),+(x356,x357))←+(x,s(+(x356,x357)))
-
+(x358,+(x359,+(y,z)))→+(+(x358,x359),+(y,z))←+(+(+(x358,x359),y),z)
-
+(x,+(x361,+(x362,z)))→+(x,+(+(x361,x362),z))←+(+(x,+(x361,x362)),z)
-
+(+(x364,+(x365,y)),z)→+(+(+(x364,x365),y),z)←+(+(x364,x365),+(y,z))
-
+(x367,+(x368,y))→+(+(x367,x368),y)←+(y,+(x367,x368))
-
+(x370,+(x371,s(y)))→+(+(x370,x371),s(y))←+(s(+(x370,x371)),y)
-
+(+(y,z),x)→+(x,+(y,z))←+(+(x,y),z)
-
+(x,+(z,y))→+(x,+(y,z))←+(+(x,y),z)
-
+(z,+(x,y))→+(+(x,y),z)←+(x,+(y,z))
-
+(+(y,x),z)→+(+(x,y),z)←+(x,+(y,z))
-
+(y,s(x))→+(s(x),y)←+(x,s(y))
-
+(y,s(x))→+(s(y),x)←+(x,s(y))
-
+(s(y),x)→+(x,s(y))←+(s(x),y)
-
+(s(y),x)→+(y,s(x))←+(s(x),y)
-
+(x385,s(+(y,z)))→+(s(x385),+(y,z))←+(+(s(x385),y),z)
-
+(x,+(x387,s(z)))→+(x,+(s(x387),z))←+(+(x,s(x387)),z)
-
+(+(x389,s(y)),z)→+(+(s(x389),y),z)←+(s(x389),+(y,z))
-
+(x391,s(y))→+(s(y),x391)←+(y,s(x391))
-
+(x391,s(y))→+(s(x391),y)←+(y,s(x391))
-
+(x393,s(s(y)))→+(s(x393),s(y))←+(s(s(x393)),y)
-
+(x,+(s(y),x396))→+(x,+(y,s(x396)))←+(+(x,y),s(x396))
-
+(s(+(x,y)),x398)→+(+(x,y),s(x398))←+(x,+(y,s(x398)))
-
+(+(s(x),x400),z)→+(+(x,s(x400)),z)←+(x,+(s(x400),z))
-
+(s(x),x402)→+(x402,s(x))←+(s(x402),x)
-
+(s(x),x402)→+(x,s(x402))←+(s(x402),x)
-
+(s(s(x)),x404)→+(s(x),s(x404))←+(x,s(s(x404)))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(s(x),*(x,x406)),x406)→+(+(x,s(*(x,x406))),x406)←+(x,+(s(*(x,x406)),x406))←+(x,+(*(x,x406),s(x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x),x406))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x),x406))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(s(x),*(x,x406)),x406)→+(+(*(x,x406),s(x)),x406)→+(*(x,x406),+(s(x),x406))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(*(x,x406),+(s(x),x406))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(s(x),*(x,x406)),x406)→+(x406,+(s(x),*(x,x406)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(s(x),*(x,x406)),x406)→+(x406,+(s(x),*(x,x406)))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x406,s(x)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(*(x,x406),s(x406)),x)←+(x,+(*(x,x406),s(x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(*(s(x),x406),s(x))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(+(*(x,x406),s(x406)),x)←+(x,+(*(x,x406),s(x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(*(x,x406),x406),s(x))→+(*(x,x406),+(x406,s(x)))→+(*(x,x406),+(s(x406),x))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(+(s(x),*(x,x406)),x406)→+(+(x,s(*(x,x406))),x406)→+(x,+(s(*(x,x406)),x406))←+(x,+(*(x,x406),s(x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x,s(x406)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(s(x406),*(x,s(x406)))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x,s(x406)),*(x,x406))←+(+(s(x406),x),*(x,x406))←+(s(x406),+(x,*(x,x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x,s(x406)),*(x,x406))←+(x,+(s(x406),*(x,x406)))←+(x,+(*(x,x406),s(x406)))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),+(*(x,x406),x406))→+(s(x),+(x406,*(x,x406)))→+(+(s(x),x406),*(x,x406))→+(+(x,s(x406)),*(x,x406))←+(*(x,x406),+(x,s(x406)))←+(+(*(x,x406),x),s(x406))←+(+(x,*(x,x406)),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),*(x406,s(x)))→+(s(x),+(x406,*(x406,x)))→+(+(s(x),x406),*(x406,x))→+(*(x406,x),+(s(x),x406))←+(*(x406,x),+(x,s(x406)))←+(+(*(x406,x),x),s(x406))←+(*(s(x406),x),s(x406))←+(*(x,s(x406)),s(x406))
-
+(s(x),*(s(x),x406))→+(s(x),*(x406,s(x)))→+(s(x),+(x406,*(x406,x)))→+(+(s(x),x406),*(x406,x))→+(+(x,s(x406)),*(x406,x))←+(*(x406,x),+(x,s(x406)))←+(+(*(x406,x),x),s(x406))←+(*(s(x406),x),s(x406))←+(*(x,s(x406)),s(x406))
-
+(x,*(x,x408))←*(x,s(x408))←*(s(x408),x)
-
+(x,*(x,x408))→+(*(x,x408),x)←+(*(x408,x),x)←*(s(x408),x)
-
+(x,*(x,x408))→+(x,*(x408,x))←+(*(x408,x),x)←*(s(x408),x)
-
+(x,*(x,x408))→+(*(x,x408),x)→+(*(x408,x),x)←*(s(x408),x)
-
+(x,*(x,x408))→+(x,*(x408,x))→+(*(x408,x),x)←*(s(x408),x)
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(x409,+(*(x409,y),s(y)))→+(x409,+(s(*(x409,y)),y))←+(+(x409,s(*(x409,y))),y)←+(+(s(x409),*(x409,y)),y)←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(x409,s(y)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(x409,s(y)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(x409,+(*(x409,y),s(y)))→+(x409,+(s(y),*(x409,y)))→+(+(x409,s(y)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(+(x409,s(y)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(x409,+(*(x409,y),s(y)))→+(+(*(x409,y),s(y)),x409)→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(x409,+(*(x409,y),s(y)))→+(+(*(x409,y),s(y)),x409)→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(y),x409))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(y,+(s(x409),*(x409,y)))←+(+(s(x409),*(x409,y)),y)←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(s(y),*(x409,s(y)))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(y,+(s(x409),*(x409,y)))←+(+(s(x409),*(x409,y)),y)←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(s(y),+(x409,*(x409,y)))→+(+(s(y),x409),*(x409,y))→+(+(y,s(x409)),*(x409,y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(x409,+(*(x409,y),s(y)))→+(x409,+(s(*(x409,y)),y))→+(+(x409,s(*(x409,y))),y)←+(+(s(x409),*(x409,y)),y)←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(x409),y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(*(s(x409),y),s(x409))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(x409),y))←+(*(x409,y),+(y,s(x409)))←+(+(*(x409,y),y),s(x409))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(x409),y))←+(+(*(x409,y),s(x409)),y)←+(+(s(x409),*(x409,y)),y)←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(+(x409,*(x409,y)),s(y))→+(+(*(x409,y),x409),s(y))→+(*(x409,y),+(x409,s(y)))→+(*(x409,y),+(s(x409),y))←+(+(s(x409),y),*(x409,y))←+(s(x409),+(y,*(x409,y)))←+(s(x409),+(*(x409,y),y))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(*(s(y),x409),s(y))→+(+(*(y,x409),x409),s(y))→+(*(y,x409),+(x409,s(y)))→+(+(x409,s(y)),*(y,x409))←+(+(s(x409),y),*(y,x409))←+(s(x409),+(y,*(y,x409)))←+(s(x409),*(y,s(x409)))←+(s(x409),*(s(x409),y))
-
+(*(x409,s(y)),s(y))→+(*(s(y),x409),s(y))→+(+(*(y,x409),x409),s(y))→+(*(y,x409),+(x409,s(y)))→+(*(y,x409),+(s(x409),y))←+(+(s(x409),y),*(y,x409))←+(s(x409),+(y,*(y,x409)))←+(s(x409),*(y,s(x409)))←+(s(x409),*(s(x409),y))
-
+(*(x411,y),y)←*(s(x411),y)←*(y,s(x411))
-
+(*(x411,y),y)→+(y,*(x411,y))←+(y,*(y,x411))←*(y,s(x411))
-
+(*(x411,y),y)→+(*(y,x411),y)←+(y,*(y,x411))←*(y,s(x411))
-
+(*(x411,y),y)→+(y,*(x411,y))→+(y,*(y,x411))←*(y,s(x411))
-
+(*(x411,y),y)→+(*(y,x411),y)→+(y,*(y,x411))←*(y,s(x411))
-
*(s(y),x)→+(*(y,x),x)←+(*(x,y),x)←+(x,*(x,y))
-
*(s(y),x)→+(*(y,x),x)←+(x,*(y,x))←+(x,*(x,y))
-
*(s(y),x)→+(*(y,x),x)→+(x,*(y,x))←+(x,*(x,y))
-
*(s(y),x)→+(*(y,x),x)→+(*(x,y),x)←+(x,*(x,y))
-
*(s(y),x)→*(x,s(y))→+(x,*(x,y))
-
*(y,s(x))→+(y,*(y,x))←+(y,*(x,y))←+(*(x,y),y)
-
*(y,s(x))→+(y,*(y,x))←+(*(y,x),y)←+(*(x,y),y)
-
*(y,s(x))→+(y,*(y,x))→+(*(y,x),y)←+(*(x,y),y)
-
*(y,s(x))→+(y,*(y,x))→+(y,*(x,y))←+(*(x,y),y)
-
*(y,s(x))→*(s(x),y)→+(*(x,y),y)
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)←+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)←+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(s(x),*(x,x)),x)←+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(s(x),*(x,x)),x)←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))←+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))←+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(*(x,x),s(x)))←+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(*(x,x),s(x)))←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(*(x,x),s(x)),x)←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(+(*(x,x),s(x)),x)←+(+(*(x,x),s(x)),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(x,+(s(x),*(x,x)))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(+(x,x)),*(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(x,+(s(x),*(x,x)))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(x),*(x,x)))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(+(x,x)),*(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(x),*(x,x)))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(+(x,x)),*(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(s(x),*(s(x),x))→+(s(x),+(*(x,x),x))→+(+(s(x),*(x,x)),x)→+(+(x,s(*(x,x))),x)←+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(+(x,x)),*(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(x,+(x,s(*(x,x))))←+(+(x,x),s(*(x,x)))←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(+(x,s(*(x,x))),x)←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
*(s(x),s(x))→+(*(x,s(x)),s(x))→+(+(x,*(x,x)),s(x))→+(x,+(*(x,x),s(x)))→+(x,+(s(*(x,x)),x))←+(x,+(s(*(x,x)),x))←+(+(s(*(x,x)),x),x)←+(s(*(x,x)),+(x,x))←+(*(x,x),s(+(x,x)))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(+(x418,x418)),*(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))→+(+(x418,s(*(x418,x418))),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(+(x418,x418)),*(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))→+(x418,+(s(*(x418,x418)),x418))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(+(*(x418,x418),s(x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(+(*(x418,x418),s(x418)),x418)←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(+(x418,x418)),*(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(x418),*(x418,x418)))←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(+(x418,x418)),*(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(x418),*(x418,x418)))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(x418),*(x418,x418)))←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(x418,x418),s(*(x418,x418)))→+(x418,+(x418,s(*(x418,x418))))→+(x418,+(s(x418),*(x418,x418)))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)→+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)→+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(x418,s(*(x418,x418))),x418)→+(+(s(x418),*(x418,x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(+(s(x418),*(x418,x418)),x418)←+(+(s(x418),*(x418,x418)),x418)←+(s(x418),+(*(x418,x418),x418))←+(s(x418),*(s(x418),x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))→+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))→+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(x418,+(s(*(x418,x418)),x418))→+(x418,+(*(x418,x418),s(x418)))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
-
+(*(x418,x418),s(+(x418,x418)))→+(s(*(x418,x418)),+(x418,x418))→+(+(s(*(x418,x418)),x418),x418)→+(+(*(x418,x418),s(x418)),x418)→+(x418,+(*(x418,x418),s(x418)))←+(x418,+(*(x418,x418),s(x418)))←+(+(x418,*(x418,x418)),s(x418))←+(*(x418,s(x418)),s(x418))←*(s(x418),s(x418))
Tool configuration
csi
- version: csi 1.2.5 [hg: unknown]
- strategy:
(sorted -ms*; ( ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!) || (( (nonconfluence -steps 0 -tcap -fun | nonconfluence -steps 2 -tcap -fun | nonconfluence -steps 25 -width 1 -tcap -fun) || (nonconfluence -steps 2 -tcap -var | nonconfluence -steps 25 -width 1 -tcap -var) || (nonconfluence -steps 0 -tree -cert -fun | nonconfluence -steps 0 -tree -cert -var | nonconfluence -steps 1 -tree -cert -fun | nonconfluence -steps 1 -tree -cert -var | nonconfluence -steps 2 -tree -cert -fun | nonconfluence -steps 2 -tree -cert -var | nonconfluence -steps 25 -tree -cert -fun | nonconfluence -steps 25 -tree -cert -var) )[6] | ((cr -m -1 -force);(redundant -narrowfwd -narrowbwd -size 7)))3*! || (((cr -m -1 -force);(redundant -remove 4)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!))! || (((cr -force -redundant);(redundant)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!)[15]?)3*! || (((cr -m -1 -force -redundant);(redundant -rhs)); ((cr -kb;((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))! || ((if linear then cr -closed -m -1;closed -strongly 7 else fail) || (if left-linear then cr -closed -m -1;(closed -development) else fail))! || (if linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (if left-linear then (cr -dup;(( lpo -quasi || (matrix -dim 1 -ib 3 -ob 4 | matrix -dim 2 -ib 2 -ob 2 | matrix -dim 3 -ib 1 -ob 2 | arctic -dim 2 -ib 2 -ob 2) || (if duplicating then fail else (bounds -rt || bounds -rt -qc))[1] || poly -ib 2 -ob 4 -nl2 -heuristic 1 || fail )[5]*);shift -lstar);(rule_labeling | rule_labeling -left)?;decreasing else fail)! || (cr -cpcs2 -cpcscert; ((( matrix -dim 1 -ib 3 -ob 5 | matrix -dim 2 -ib 2 -ob 3 | matrix -dim 3 -ib 1 -ob 1 | matrix -dim 3 -ib 1 -ob 3 | fail)[2]*);((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])! || (rev;((dp;edg[0.5]?;(sccs | (sc || sct || {ur?;( (matrix -dp -ur -dim 1 -ib 3 -ob 5 | matrix -dp -ur -dim 2 -ib 2 -ob 3 | matrix -dp -ur -dim 3 -ib 1 -ob 1 | matrix -dp -ur -dim 3 -ib 1 -ob 3) || (kbo -ur -af | lpo -ur -af) || ( arctic -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || ( arctic -bz -dp -ur -dim 2 -ib 2 -ob 2[2] | fail) || fail) }restore || fail;(bounds -dp -rfc -qc || bounds -dp -all -rfc -qc || bounds -rfc -qc)[1] || fail ))*[6])! || (( kbo || (lpo | fail;(ref;lpo)) || fail;(bounds -rfc -qc) || fail)*[7])!)))))!)[15]?)3*! ))[54]