YES
Confluence Proof
Confluence Proof
by csi
Input
The rewrite relation of the following TRS is considered.
|
b(w(x)) |
→ |
w(w(w(b(x)))) |
|
w(b(x)) |
→ |
b(x) |
|
b(b(x)) |
→ |
w(w(w(w(x)))) |
|
w(w(x)) |
→ |
w(x) |
Proof
1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
w(w(x)) |
→ |
w(x) |
|
b(b(x)) |
→ |
w(w(w(w(x)))) |
|
w(b(x)) |
→ |
b(x) |
|
b(w(x)) |
→ |
w(w(w(b(x)))) |
|
b(b(x)) |
→ |
w(w(w(x))) |
|
b(w(x)) |
→ |
w(w(b(x))) |
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.1 Decreasing Diagrams
1.1.1 Relative Termination Proof
The duplicating rules (R) terminate relative to the other rules (S).
1.1.1.1 R is empty
There are no rules in the TRS R. Hence, R/S is relative terminating.
1.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).
-
w(w(x))→w(x) ↦ 0
-
b(b(x))→w(w(w(w(x)))) ↦ 4
-
w(b(x))→b(x) ↦ 0
-
b(w(x))→w(w(w(b(x)))) ↦ 5
-
b(b(x))→w(w(w(x))) ↦ 4
-
b(w(x))→w(w(b(x))) ↦ 4
All critical pairs are joinable:
-
w(w(x113))
-
b(w(x114))←w(b(w(x114)))←w(w(b(w(x114))))←w(w(w(b(w(x114)))))
-
b(w(x114))→w(w(w(b(x114))))←w(b(w(x114)))←w(w(b(w(x114))))←w(w(w(b(w(x114)))))
-
b(w(x114))→w(w(w(b(x114))))←w(w(w(w(b(x114)))))←w(w(b(w(x114))))←w(w(w(b(w(x114)))))
-
b(w(x114))→w(w(w(b(x114))))←w(w(w(w(b(x114)))))←w(w(w(w(w(b(x114))))))←w(w(w(b(w(x114)))))
-
b(w(x115))←w(b(w(x115)))←w(w(b(w(x115))))
-
b(w(x115))→w(w(w(b(x115))))←w(b(w(x115)))←w(w(b(w(x115))))
-
b(w(x115))→w(w(w(b(x115))))←w(w(w(w(b(x115)))))←w(w(b(w(x115))))
-
b(w(w(w(w(x116)))))→b(w(w(w(x116))))→b(w(w(x116)))→b(w(x116))→w(w(w(b(x116))))←w(w(w(w(b(x116)))))
-
b(w(w(w(w(x116)))))→b(w(w(w(x116))))→b(w(w(x116)))→b(w(x116))→w(w(b(x116)))←w(w(w(b(x116))))←w(w(w(w(b(x116)))))
-
b(w(w(w(w(x116)))))→b(w(w(w(x116))))→b(w(w(x116)))→w(w(b(w(x116))))→w(w(w(w(b(x116)))))
-
b(w(w(w(w(x116)))))→b(w(w(w(x116))))→w(w(b(w(w(x116)))))→w(w(b(w(x116))))→w(w(w(w(b(x116)))))
-
b(w(w(w(w(x116)))))→w(w(b(w(w(w(x116))))))→w(w(b(w(w(x116)))))→w(w(b(w(x116))))→w(w(w(w(b(x116)))))
-
w(w(w(w(w(x117)))))→w(w(w(w(x117))))←b(b(x117))
-
w(w(w(w(x))))→w(w(w(x)))
-
b(w(w(w(w(x119)))))→b(w(w(w(x119))))→b(w(w(x119)))→b(w(x119))→w(w(w(b(x119))))
-
b(w(w(w(w(x119)))))→b(w(w(w(x119))))→b(w(w(x119)))→b(w(x119))→w(w(b(x119)))←w(w(w(b(x119))))
-
w(b(x120))
-
b(b(x121))←w(b(b(x121)))←w(w(b(b(x121))))←w(w(w(b(b(x121)))))
-
b(b(x121))→w(w(w(w(x121))))←w(b(b(x121)))←w(w(b(b(x121))))←w(w(w(b(b(x121)))))
-
b(b(x121))→w(w(w(w(x121))))←w(w(w(w(w(x121)))))←w(w(b(b(x121))))←w(w(w(b(b(x121)))))
-
b(b(x121))→w(w(w(w(x121))))←w(w(w(w(w(x121)))))←w(w(w(w(w(w(x121))))))←w(w(w(b(b(x121)))))
-
b(b(x122))←w(b(b(x122)))←w(w(b(b(x122))))
-
b(b(x122))→w(w(w(w(x122))))←w(b(b(x122)))←w(w(b(b(x122))))
-
b(b(x122))→w(w(w(w(x122))))←w(w(w(w(w(x122)))))←w(w(b(b(x122))))
-
b(w(w(w(b(x123)))))→b(w(w(b(x123))))→b(w(b(x123)))→b(b(x123))→w(w(w(w(x123))))←w(w(w(w(w(x123)))))
-
b(w(w(w(b(x123)))))→b(w(w(b(x123))))→b(w(b(x123)))→b(b(x123))→w(w(w(x123)))←w(w(w(w(x123))))←w(w(w(w(w(x123)))))
-
b(w(w(w(b(x123)))))→b(w(w(b(x123))))→b(w(b(x123)))→w(w(b(b(x123))))→w(w(w(w(w(x123)))))
-
b(w(w(w(b(x123)))))→b(w(w(b(x123))))→w(w(b(w(b(x123)))))→w(w(b(b(x123))))→w(w(w(w(w(x123)))))
-
b(w(w(w(b(x123)))))→w(w(b(w(w(b(x123))))))→w(w(b(w(b(x123)))))→w(w(b(b(x123))))→w(w(w(w(w(x123)))))
-
w(w(w(w(b(x124)))))→w(w(w(b(x124))))←b(w(x124))
-
b(w(w(w(b(x125)))))→b(w(w(b(x125))))→b(w(b(x125)))→b(b(x125))→w(w(w(w(x125))))
-
b(w(w(w(b(x125)))))→b(w(w(b(x125))))→b(w(b(x125)))→b(b(x125))→w(w(w(x125)))←w(w(w(w(x125))))
-
w(w(w(b(x))))→w(w(b(x)))
-
w(w(w(x)))←w(w(w(w(x))))
-
b(w(w(w(x128))))→b(w(w(x128)))→b(w(x128))→w(w(w(b(x128))))←w(w(w(w(b(x128)))))
-
b(w(w(w(x128))))→b(w(w(x128)))→b(w(x128))→w(w(b(x128)))←w(w(w(b(x128))))←w(w(w(w(b(x128)))))
-
b(w(w(w(x128))))→b(w(w(x128)))→w(w(b(w(x128))))→w(w(w(w(b(x128)))))
-
b(w(w(w(x128))))→w(w(b(w(w(x128)))))→w(w(b(w(x128))))→w(w(w(w(b(x128)))))
-
w(w(w(w(x129))))←b(b(x129))
-
w(w(w(w(x129))))→w(w(w(x129)))←b(b(x129))
-
b(w(w(w(x130))))→b(w(w(x130)))→b(w(x130))→w(w(w(b(x130))))
-
b(w(w(w(x130))))→b(w(w(x130)))→b(w(x130))→w(w(b(x130)))←w(w(w(b(x130))))
-
b(w(w(b(x131))))→b(w(b(x131)))→b(b(x131))→w(w(w(w(x131))))←w(w(w(w(w(x131)))))
-
b(w(w(b(x131))))→b(w(b(x131)))→b(b(x131))→w(w(w(x131)))←w(w(w(w(x131))))←w(w(w(w(w(x131)))))
-
b(w(w(b(x131))))→b(w(b(x131)))→w(w(b(b(x131))))→w(w(w(w(w(x131)))))
-
b(w(w(b(x131))))→w(w(b(w(b(x131)))))→w(w(b(b(x131))))→w(w(w(w(w(x131)))))
-
w(w(w(b(x132))))←b(w(x132))
-
w(w(w(b(x132))))→w(w(b(x132)))←b(w(x132))
-
w(w(b(x)))←w(w(w(b(x))))
-
b(w(w(b(x134))))→b(w(b(x134)))→b(b(x134))→w(w(w(w(x134))))
-
b(w(w(b(x134))))→b(w(b(x134)))→b(b(x134))→w(w(w(x134)))←w(w(w(w(x134))))
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]