0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 Narrowing (⇔)
↳20 QDP
↳21 Rewriting (⇔)
↳22 QDP
↳23 Rewriting (⇔)
↳24 QDP
↳25 Rewriting (⇔)
↳26 QDP
↳27 Rewriting (⇔)
↳28 QDP
↳29 Rewriting (⇔)
↳30 QDP
↳31 Narrowing (⇔)
↳32 QDP
↳33 DependencyGraphProof (⇔)
↳34 QDP
↳35 Narrowing (⇔)
↳36 QDP
↳37 Rewriting (⇔)
↳38 QDP
↳39 Rewriting (⇔)
↳40 QDP
↳41 Rewriting (⇔)
↳42 QDP
↳43 Rewriting (⇔)
↳44 QDP
↳45 Rewriting (⇔)
↳46 QDP
↳47 Narrowing (⇔)
↳48 QDP
↳49 DependencyGraphProof (⇔)
↳50 QDP
↳51 Narrowing (⇔)
↳52 QDP
↳53 DependencyGraphProof (⇔)
↳54 QDP
↳55 Rewriting (⇔)
↳56 QDP
↳57 Narrowing (⇔)
↳58 QDP
↳59 DependencyGraphProof (⇔)
↳60 QDP
↳61 Narrowing (⇔)
↳62 QDP
↳63 DependencyGraphProof (⇔)
↳64 QDP
↳65 Narrowing (⇔)
↳66 QDP
↳67 DependencyGraphProof (⇔)
↳68 QDP
↳69 Rewriting (⇔)
↳70 QDP
↳71 Narrowing (⇔)
↳72 QDP
↳73 DependencyGraphProof (⇔)
↳74 QDP
↳75 Instantiation (⇔)
↳76 QDP
↳77 DependencyGraphProof (⇔)
↳78 QDP
↳79 Narrowing (⇔)
↳80 QDP
↳81 DependencyGraphProof (⇔)
↳82 QDP
↳83 Instantiation (⇔)
↳84 QDP
↳85 DependencyGraphProof (⇔)
↳86 QDP
↳87 Instantiation (⇔)
↳88 QDP
↳89 UsableRulesProof (⇔)
↳90 QDP
↳91 Rewriting (⇔)
↳92 QDP
↳93 UsableRulesProof (⇔)
↳94 QDP
↳95 QReductionProof (⇔)
↳96 QDP
↳97 Instantiation (⇔)
↳98 QDP
↳99 Rewriting (⇔)
↳100 QDP
↳101 Instantiation (⇔)
↳102 QDP
↳103 Instantiation (⇔)
↳104 QDP
↳105 DependencyGraphProof (⇔)
↳106 AND
↳107 QDP
↳108 UsableRulesProof (⇔)
↳109 QDP
↳110 ForwardInstantiation (⇔)
↳111 QDP
↳112 ForwardInstantiation (⇔)
↳113 QDP
↳114 ForwardInstantiation (⇔)
↳115 QDP
↳116 ForwardInstantiation (⇔)
↳117 QDP
↳118 ForwardInstantiation (⇔)
↳119 QDP
↳120 QDPSizeChangeProof (⇔)
↳121 TRUE
↳122 QDP
↳123 ForwardInstantiation (⇔)
↳124 QDP
↳125 Rewriting (⇔)
↳126 QDP
↳127 Rewriting (⇔)
↳128 QDP
↳129 ForwardInstantiation (⇔)
↳130 QDP
↳131 ForwardInstantiation (⇔)
↳132 QDP
↳133 ForwardInstantiation (⇔)
↳134 QDP
↳135 ForwardInstantiation (⇔)
↳136 QDP
↳137 Rewriting (⇔)
↳138 QDP
↳139 Rewriting (⇔)
↳140 QDP
↳141 Rewriting (⇔)
↳142 QDP
↳143 Rewriting (⇔)
↳144 QDP
↳145 Rewriting (⇔)
↳146 QDP
↳147 Rewriting (⇔)
↳148 QDP
↳149 ForwardInstantiation (⇔)
↳150 QDP
↳151 ForwardInstantiation (⇔)
↳152 QDP
↳153 ForwardInstantiation (⇔)
↳154 QDP
↳155 ForwardInstantiation (⇔)
↳156 QDP
↳157 ForwardInstantiation (⇔)
↳158 QDP
↳159 ForwardInstantiation (⇔)
↳160 QDP
↳161 ForwardInstantiation (⇔)
↳162 QDP
↳163 QDPSizeChangeProof (⇔)
↳164 TRUE
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND1(true, x, y, z) → GR(x, 0)
COND2(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), p(x), y, z)
COND2(true, x, y, z) → OR(gr(x, z), gr(y, z))
COND2(true, x, y, z) → GR(x, z)
COND2(true, x, y, z) → GR(y, z)
COND2(true, x, y, z) → P(x)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND2(false, x, y, z) → GR(y, 0)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(true, x, y, z) → OR(gr(x, z), gr(y, z))
COND3(true, x, y, z) → GR(x, z)
COND3(true, x, y, z) → GR(y, z)
COND3(true, x, y, z) → P(y)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND3(false, x, y, z) → OR(gr(x, z), gr(y, z))
COND3(false, x, y, z) → GR(x, z)
COND3(false, x, y, z) → GR(y, z)
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
From the DPs we obtained the following set of size-change graphs:
COND2(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), p(x), y, z)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
cond1(true, x, y, z) → cond2(gr(x, 0), x, y, z)
cond2(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), p(x), y, z)
cond2(false, x, y, z) → cond3(gr(y, 0), x, y, z)
cond3(true, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, p(y), z)
cond3(false, x, y, z) → cond1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), p(x), y, z)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
cond1(true, x0, x1, x2)
cond2(true, x0, x1, x2)
cond2(false, x0, x1, x2)
cond3(true, x0, x1, x2)
cond3(false, x0, x1, x2)
COND2(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), p(x), y, z)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), p(0), y1, x0)
COND2(true, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), p(s(x0)), y1, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), p(s(x0)), y1, s(x1))
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), p(y0), s(x0), 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), p(0), y1, x0)
COND2(true, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), p(s(x0)), y1, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), p(s(x0)), y1, s(x1))
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), p(y0), s(x0), 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), p(s(x0)), y1, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), p(s(x0)), y1, s(x1))
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), p(y0), s(x0), 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, s(x0), y1, 0) → COND1(true, p(s(x0)), y1, 0)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), p(s(x0)), y1, s(x1))
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), p(y0), s(x0), 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND2(true, s(x0), y1, 0) → COND1(true, p(s(x0)), y1, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), p(y0), s(x0), 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND2(true, s(x0), y1, 0) → COND1(true, p(s(x0)), y1, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND2(true, s(x0), y1, 0) → COND1(true, p(s(x0)), y1, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, x, y, z) → COND2(gr(x, 0), x, y, z)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, p(y), z)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), s(x0), p(y1), 0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, p(0), x0)
COND3(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, p(s(x0)), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, p(s(x0)), s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), s(x0), p(y1), 0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, p(0), x0)
COND3(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, p(s(x0)), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, p(s(x0)), s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, p(0), x0)
COND3(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, p(s(x0)), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, p(s(x0)), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, p(s(x0)), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, p(s(x0)), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, y0, s(x0), 0) → COND1(true, y0, p(s(x0)), 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, p(s(x0)), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, p(s(x0)), 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, p(s(x0)), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, x, y, z) → COND3(gr(y, 0), x, y, z)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, x, y, z) → COND1(or(gr(x, z), gr(y, z)), x, y, z)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND3(false, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), s(x0), y1, 0)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, s(x0), 0)
COND3(false, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, s(x0), s(x1))
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(false, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND3(false, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), s(x0), y1, 0)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, y0, s(x0), 0) → COND1(or(gr(y0, 0), true), y0, s(x0), 0)
COND3(false, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, s(x0), s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, 0) → COND1(or(true, gr(y1, 0)), s(x0), y1, 0)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND3(false, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, y1, x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, 0, 0, x0) → COND1(or(false, false), 0, 0, x0)
COND3(false, 0, s(x0), 0) → COND1(or(false, true), 0, s(x0), 0)
COND3(false, 0, s(x0), s(x1)) → COND1(or(false, gr(x0, x1)), 0, s(x0), s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND3(false, 0, 0, x0) → COND1(or(false, false), 0, 0, x0)
COND3(false, 0, s(x0), 0) → COND1(or(false, true), 0, s(x0), 0)
COND3(false, 0, s(x0), s(x1)) → COND1(or(false, gr(x0, x1)), 0, s(x0), s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, 0, x0) → COND1(or(gr(y0, x0), false), p(y0), 0, x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, 0, 0, y1) → COND1(or(gr(0, y1), false), 0, 0, y1)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(true, 0, 0, y1) → COND1(or(gr(0, y1), false), 0, 0, y1)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), p(y0), s(x0), s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, 0, s(y1), s(y2)) → COND1(or(gr(0, s(y2)), gr(y1, y2)), 0, s(y1), s(y2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(s(x0), s(y2)), gr(y1, y2)), x0, s(y1), s(y2))
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, 0, s(y1), s(y2)) → COND1(or(gr(0, s(y2)), gr(y1, y2)), 0, s(y1), s(y2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(s(x0), s(y2)), gr(y1, y2)), x0, s(y1), s(y2))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(s(x0), s(y2)), gr(y1, y2)), x0, s(y1), s(y2))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, y0, s(x0), 0) → COND1(true, p(y0), s(x0), 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, 0, s(y1), 0) → COND1(true, 0, s(y1), 0)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, 0, s(y1), 0) → COND1(true, 0, s(y1), 0)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, 0, y2) → COND3(false, y0, 0, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, 0, 0, z1) → COND3(false, 0, 0, z1)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(false, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), y1, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
COND3(false, s(x0), y1, 0) → COND1(true, s(x0), y1, 0)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(false, 0, 0, z1) → COND3(false, 0, 0, z1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(false, 0, 0, z1) → COND3(false, 0, 0, z1)
COND3(false, y0, 0, x0) → COND1(or(gr(y0, x0), false), y0, 0, x0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(false, 0, 0, x0) → COND1(or(false, false), 0, 0, x0)
COND3(false, s(x0), 0, 0) → COND1(or(true, false), s(x0), 0, 0)
COND3(false, s(x0), 0, s(x1)) → COND1(or(gr(x0, x1), false), s(x0), 0, s(x1))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(false, 0, 0, z1) → COND3(false, 0, 0, z1)
COND3(false, 0, 0, x0) → COND1(or(false, false), 0, 0, x0)
COND3(false, s(x0), 0, 0) → COND1(or(true, false), s(x0), 0, 0)
COND3(false, s(x0), 0, s(x1)) → COND1(or(gr(x0, x1), false), s(x0), 0, s(x1))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, y0, s(x0), y2) → COND3(true, y0, s(x0), y2)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), s(x0), p(y1), s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, s(x0), y1, 0) → COND1(true, s(x0), p(y1), 0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, y1, x0) → COND1(or(false, gr(y1, x0)), 0, p(y1), x0)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, p(s(z0)), z1)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, p(s(z0)), z1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(true, x) → true
or(x, true) → true
p(0) → 0
p(s(x)) → x
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, p(s(z0)), z1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
p(s(x)) → x
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
p(s(x)) → x
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
p(0)
p(s(x0))
p(0)
p(s(x0))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, y0, s(x0), s(x1)) → COND1(or(gr(y0, s(x1)), gr(x0, x1)), y0, x0, s(x1))
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(z0), s(x2)) → COND1(or(gr(0, s(x2)), gr(z0, x2)), 0, z0, s(x2))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(gr(0, s(x2)), gr(z0, x2)), 0, z0, s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND1(true, s(x0), y1, y2) → COND2(true, s(x0), y1, y2)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, y0, s(x0), 0) → COND1(true, y0, x0, 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND1(true, 0, y1, y2) → COND2(false, 0, y1, y2)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, s(z0), z1) → COND1(or(false, gr(s(z0), z1)), 0, z0, z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(s(y_1)), x1) → COND1(or(false, gr(s(s(y_1)), x1)), 0, s(y_1), x1)
COND2(false, 0, s(x1), z1) → COND3(true, 0, s(x1), z1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
COND3(true, 0, s(s(y_1)), x1) → COND1(or(false, gr(s(s(y_1)), x1)), 0, s(y_1), x1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(false, 0, s(x0), s(y_1)) → COND3(true, 0, s(x0), s(y_1))
COND2(false, 0, s(x0), 0) → COND3(true, 0, s(x0), 0)
COND2(false, 0, s(s(y_0)), x1) → COND3(true, 0, s(s(y_0)), x1)
COND3(true, 0, s(z0), s(x2)) → COND1(or(false, gr(z0, x2)), 0, z0, s(x2))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
COND3(true, 0, s(s(y_1)), x1) → COND1(or(false, gr(s(s(y_1)), x1)), 0, s(y_1), x1)
COND2(false, 0, s(x0), s(y_1)) → COND3(true, 0, s(x0), s(y_1))
COND2(false, 0, s(x0), 0) → COND3(true, 0, s(x0), 0)
COND2(false, 0, s(s(y_0)), x1) → COND3(true, 0, s(s(y_0)), x1)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(s(y_1)), s(x1)) → COND1(or(false, gr(s(y_1), x1)), 0, s(y_1), s(x1))
COND3(true, 0, s(z0), 0) → COND1(true, 0, z0, 0)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
COND3(true, 0, s(s(y_1)), x1) → COND1(or(false, gr(s(s(y_1)), x1)), 0, s(y_1), x1)
COND2(false, 0, s(x0), s(y_1)) → COND3(true, 0, s(x0), s(y_1))
COND2(false, 0, s(x0), 0) → COND3(true, 0, s(x0), 0)
COND2(false, 0, s(s(y_0)), x1) → COND3(true, 0, s(s(y_0)), x1)
COND3(true, 0, s(s(y_1)), s(x1)) → COND1(or(false, gr(s(y_1), x1)), 0, s(y_1), s(x1))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND3(true, 0, s(s(y_0)), 0) → COND1(true, 0, s(y_0), 0)
COND1(true, 0, s(y_0), x1) → COND2(false, 0, s(y_0), x1)
COND3(true, 0, s(s(y_1)), x1) → COND1(or(false, gr(s(s(y_1)), x1)), 0, s(y_1), x1)
COND2(false, 0, s(x0), s(y_1)) → COND3(true, 0, s(x0), s(y_1))
COND2(false, 0, s(x0), 0) → COND3(true, 0, s(x0), 0)
COND2(false, 0, s(s(y_0)), x1) → COND3(true, 0, s(s(y_0)), x1)
COND3(true, 0, s(s(y_1)), s(x1)) → COND1(or(false, gr(s(y_1), x1)), 0, s(y_1), s(x1))
COND3(true, 0, s(s(y_0)), 0) → COND1(true, 0, s(y_0), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x) → false
or(false, false) → false
or(x, true) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
From the DPs we obtained the following set of size-change graphs:
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND2(true, s(x0), y1, s(x1)) → COND1(or(gr(x0, x1), gr(y1, s(x1))), x0, y1, s(x1))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), gr(0, s(x2))), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(s(y_2), s(x2))), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), gr(0, s(x2))), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(s(y_2), s(x2))), s(y_1), s(y_2), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(s(y_2), s(x2))), s(y_1), s(y_2), s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), z1, s(z2)) → COND2(true, s(x0), z1, s(z2))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(x0), s(y_1), s(x2)) → COND2(true, s(x0), s(y_1), s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), y1, 0) → COND1(true, x0, y1, 0)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND1(true, s(x0), z1, 0) → COND2(true, s(x0), z1, 0)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(x0), s(y_1), 0) → COND2(true, s(x0), s(y_1), 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), 0, y1) → COND1(or(gr(s(x0), y1), false), x0, 0, y1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(y_1)), 0, s(y_2)) → COND1(or(gr(s(s(y_1)), s(y_2)), false), s(y_1), 0, s(y_2))
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(s(y_1))), s(y_3)), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(y_1)), 0, 0) → COND1(or(gr(s(s(y_1)), 0), false), s(y_1), 0, 0)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(gr(s(s(s(y_1))), 0), false), s(s(y_1)), 0, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(y_1)), 0, s(y_2)) → COND1(or(gr(s(s(y_1)), s(y_2)), false), s(y_1), 0, s(y_2))
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(s(y_1))), s(y_3)), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(y_1)), 0, 0) → COND1(or(gr(s(s(y_1)), 0), false), s(y_1), 0, 0)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(gr(s(s(s(y_1))), 0), false), s(s(y_1)), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), 0, s(y_2)) → COND1(or(gr(s(y_1), y_2), false), s(y_1), 0, s(y_2))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(s(y_1))), s(y_3)), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(y_1)), 0, 0) → COND1(or(gr(s(s(y_1)), 0), false), s(y_1), 0, 0)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(gr(s(s(s(y_1))), 0), false), s(s(y_1)), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(y_1)), 0, 0) → COND1(or(gr(s(s(y_1)), 0), false), s(y_1), 0, 0)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(gr(s(s(s(y_1))), 0), false), s(s(y_1)), 0, 0)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), 0, 0) → COND1(or(true, false), s(y_1), 0, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(gr(s(s(s(y_1))), 0), false), s(s(y_1)), 0, 0)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(y_1)), 0, 0) → COND1(or(true, false), s(y_1), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(true, false), s(s(y_1)), 0, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(y_1)), 0, 0) → COND1(or(true, false), s(y_1), 0, 0)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(true, false), s(s(y_1)), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), 0, 0) → COND1(true, s(y_1), 0, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(or(true, false), s(s(y_1)), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(x0), 0, z1) → COND2(true, s(x0), 0, z1)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(s(y_0)), 0, s(y_2)) → COND2(true, s(s(y_0)), 0, s(y_2))
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(x0), s(y1), 0) → COND1(true, x0, s(y1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_0)), s(x1), 0) → COND1(true, s(y_0), s(x1), 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(x0), s(z1), 0) → COND2(true, s(x0), s(z1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(s(y_0)), s(x1), 0) → COND2(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(x0), s(y1), s(y2)) → COND1(or(gr(x0, y2), gr(y1, y2)), x0, s(y1), s(y2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND2(true, s(s(y_1)), s(x1), s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, x2)), s(y_1), s(x1), s(x2))
COND2(true, s(s(s(y_1))), s(x1), s(x2)) → COND1(or(gr(s(s(y_1)), x2), gr(x1, x2)), s(s(y_1)), s(x1), s(x2))
COND1(true, s(x0), s(z1), s(z2)) → COND2(true, s(x0), s(z1), s(z2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
COND2(true, s(s(s(y_1))), s(x1), s(x2)) → COND1(or(gr(s(s(y_1)), x2), gr(x1, x2)), s(s(y_1)), s(x1), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(s(y_0)), s(x1), s(x2)) → COND2(true, s(s(y_0)), s(x1), s(x2))
COND1(true, s(s(s(y_0))), s(x1), s(x2)) → COND2(true, s(s(s(y_0))), s(x1), s(x2))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(x0), 0, s(x2)) → COND2(true, s(x0), 0, s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
COND2(true, s(s(s(y_1))), s(x1), s(x2)) → COND1(or(gr(s(s(y_1)), x2), gr(x1, x2)), s(s(y_1)), s(x1), s(x2))
COND1(true, s(s(s(y_0))), s(x1), s(x2)) → COND2(true, s(s(s(y_0))), s(x1), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(s(y_0)), 0, s(x1)) → COND2(true, s(s(y_0)), 0, s(x1))
COND1(true, s(s(s(y_0))), 0, s(x1)) → COND2(true, s(s(s(y_0))), 0, s(x1))
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(x0), 0, 0) → COND2(true, s(x0), 0, 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
COND2(true, s(s(s(y_1))), s(x1), s(x2)) → COND1(or(gr(s(s(y_1)), x2), gr(x1, x2)), s(s(y_1)), s(x1), s(x2))
COND1(true, s(s(s(y_0))), s(x1), s(x2)) → COND2(true, s(s(s(y_0))), s(x1), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(y_1)), x1, s(x2)) → COND1(or(gr(s(y_1), x2), gr(x1, s(x2))), s(y_1), x1, s(x2))
COND2(true, s(s(y_1)), 0, s(x2)) → COND1(or(gr(s(y_1), x2), false), s(y_1), 0, s(x2))
COND2(true, s(s(y_1)), s(y_2), s(x2)) → COND1(or(gr(s(y_1), x2), gr(y_2, x2)), s(y_1), s(y_2), s(x2))
COND1(true, s(s(y_0)), x1, s(x2)) → COND2(true, s(s(y_0)), x1, s(x2))
COND1(true, s(s(y_0)), 0, s(x2)) → COND2(true, s(s(y_0)), 0, s(x2))
COND1(true, s(s(y_0)), s(y_1), s(x2)) → COND2(true, s(s(y_0)), s(y_1), s(x2))
COND2(true, s(s(y_0)), x1, 0) → COND1(true, s(y_0), x1, 0)
COND2(true, s(s(y_0)), 0, 0) → COND1(true, s(y_0), 0, 0)
COND2(true, s(s(y_0)), s(y_1), 0) → COND1(true, s(y_0), s(y_1), 0)
COND1(true, s(s(y_0)), x1, 0) → COND2(true, s(s(y_0)), x1, 0)
COND1(true, s(s(y_0)), 0, 0) → COND2(true, s(s(y_0)), 0, 0)
COND1(true, s(s(y_0)), s(y_1), 0) → COND2(true, s(s(y_0)), s(y_1), 0)
COND2(true, s(s(y_1)), 0, x1) → COND1(or(gr(s(s(y_1)), x1), false), s(y_1), 0, x1)
COND2(true, s(s(s(y_1))), 0, s(y_3)) → COND1(or(gr(s(s(y_1)), y_3), false), s(s(y_1)), 0, s(y_3))
COND2(true, s(s(s(y_1))), 0, 0) → COND1(true, s(s(y_1)), 0, 0)
COND1(true, s(s(y_0)), 0, x1) → COND2(true, s(s(y_0)), 0, x1)
COND1(true, s(s(s(y_0))), 0, s(y_1)) → COND2(true, s(s(s(y_0))), 0, s(y_1))
COND1(true, s(s(s(y_0))), 0, 0) → COND2(true, s(s(s(y_0))), 0, 0)
COND2(true, s(s(s(y_0))), s(x1), 0) → COND1(true, s(s(y_0)), s(x1), 0)
COND1(true, s(s(s(y_0))), s(x1), 0) → COND2(true, s(s(s(y_0))), s(x1), 0)
COND2(true, s(s(s(y_1))), s(x1), s(x2)) → COND1(or(gr(s(s(y_1)), x2), gr(x1, x2)), s(s(y_1)), s(x1), s(x2))
COND1(true, s(s(s(y_0))), s(x1), s(x2)) → COND2(true, s(s(s(y_0))), s(x1), s(x2))
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
or(false, false) → false
or(x, true) → true
gr(0, x) → false
or(true, x) → true
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
or(false, false)
or(true, x0)
or(x0, true)
From the DPs we obtained the following set of size-change graphs: