YES
R
↳Dependency Pair Analysis
U101'(tt, A, B) -> xor(and(A, B), xor(A, B))
U101'(tt, A, B) -> and(A, B)
U101'(tt, A, B) -> xor(A, B)
U131'(tt, B, U') -> U132'(equal(isNotEqualTo(B, true), true), U')
U131'(tt, B, U') -> EQUAL(isNotEqualTo(B, true), true)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
U151'(tt, A) -> xor(A, true)
U21'(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21'(tt, A, B, C) -> and(A, B)
U21'(tt, A, B, C) -> and(A, C)
U51'(tt, A, B) -> NOT(xor(A, and(A, B)))
U51'(tt, A, B) -> xor(A, and(A, B))
U51'(tt, A, B) -> and(A, B)
U61'(tt, U', U) -> U62'(equal(isNotEqualTo(U, U'), true))
U61'(tt, U', U) -> EQUAL(isNotEqualTo(U, U'), true)
U61'(tt, U', U) -> ISNOTEQUALTO(U, U')
U81'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
U81'(tt, U', U) -> ISEQUALTO(U, U')
and(A, A) -> U11'(isBool(A), A)
and(A, A) -> ISBOOL(A)
and(A, xor(B, C)) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(A, xor(B, C)) -> AND(isBool(A), and(isBool(B), isBool(C)))
and(A, xor(B, C)) -> ISBOOL(A)
and(A, xor(B, C)) -> AND(isBool(B), isBool(C))
and(A, xor(B, C)) -> ISBOOL(B)
and(A, xor(B, C)) -> ISBOOL(C)
and(false, A) -> U31'(isBool(A))
and(false, A) -> ISBOOL(A)
and(true, A) -> U41'(isBool(A), A)
and(true, A) -> ISBOOL(A)
and(and(A, A), ext) -> and(U11(isBool(A), A), ext)
and(and(A, A), ext) -> U11'(isBool(A), A)
and(and(A, A), ext) -> ISBOOL(A)
and(and(A, xor(B, C)), ext) -> and(U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C), ext)
and(and(A, xor(B, C)), ext) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(and(A, xor(B, C)), ext) -> AND(isBool(A), and(isBool(B), isBool(C)))
and(and(A, xor(B, C)), ext) -> ISBOOL(A)
and(and(A, xor(B, C)), ext) -> AND(isBool(B), isBool(C))
and(and(A, xor(B, C)), ext) -> ISBOOL(B)
and(and(A, xor(B, C)), ext) -> ISBOOL(C)
and(and(false, A), ext) -> and(U31(isBool(A)), ext)
and(and(false, A), ext) -> U31'(isBool(A))
and(and(false, A), ext) -> ISBOOL(A)
and(and(true, A), ext) -> and(U41(isBool(A), A), ext)
and(and(true, A), ext) -> U41'(isBool(A), A)
and(and(true, A), ext) -> ISBOOL(A)
IMPLIES(A, B) -> U51'(and(isBool(A), isBool(B)), A, B)
IMPLIES(A, B) -> AND(isBool(A), isBool(B))
IMPLIES(A, B) -> ISBOOL(A)
IMPLIES(A, B) -> ISBOOL(B)
ISEQUALTO(U, U') -> U61'(and(isS(U'), isS(U)), U', U)
ISEQUALTO(U, U') -> AND(isS(U'), isS(U))
ISEQUALTO(U, U) -> U71'(isS(U))
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
ISNOTEQUALTO(U, U') -> AND(isS(U'), isS(U))
ISNOTEQUALTO(U, U) -> U91'(isS(U))
or(A, B) -> U101'(and(isBool(A), isBool(B)), A, B)
or(A, B) -> AND(isBool(A), isBool(B))
or(A, B) -> ISBOOL(A)
or(A, B) -> ISBOOL(B)
or(or(A, B), ext) -> or(U101(and(isBool(A), isBool(B)), A, B), ext)
or(or(A, B), ext) -> U101'(and(isBool(A), isBool(B)), A, B)
or(or(A, B), ext) -> AND(isBool(A), isBool(B))
or(or(A, B), ext) -> ISBOOL(A)
or(or(A, B), ext) -> ISBOOL(B)
xor(A, A) -> U111'(isBool(A))
xor(A, A) -> ISBOOL(A)
xor(false, A) -> U121'(isBool(A), A)
xor(false, A) -> ISBOOL(A)
xor(xor(A, A), ext) -> xor(U111(isBool(A)), ext)
xor(xor(A, A), ext) -> U111'(isBool(A))
xor(xor(A, A), ext) -> ISBOOL(A)
xor(xor(false, A), ext) -> xor(U121(isBool(A), A), ext)
xor(xor(false, A), ext) -> U121'(isBool(A), A)
xor(xor(false, A), ext) -> ISBOOL(A)
IFTHENELSEFI(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
IFTHENELSEFI(B, U, U') -> AND(isBool(B), and(isS(U'), isS(U)))
IFTHENELSEFI(B, U, U') -> ISBOOL(B)
IFTHENELSEFI(B, U, U') -> AND(isS(U'), isS(U))
IFTHENELSEFI(true, U, U') -> U141'(and(isS(U'), isS(U)), U)
IFTHENELSEFI(true, U, U') -> AND(isS(U'), isS(U))
ISBOOL(and(V1, V2)) -> AND(isBool(V1), isBool(V2))
ISBOOL(and(V1, V2)) -> ISBOOL(V1)
ISBOOL(and(V1, V2)) -> ISBOOL(V2)
ISBOOL(implies(V1, V2)) -> AND(isBool(V1), isBool(V2))
ISBOOL(implies(V1, V2)) -> ISBOOL(V1)
ISBOOL(implies(V1, V2)) -> ISBOOL(V2)
ISBOOL(isEqualTo(V1, V2)) -> AND(isUniversal(V1), isUniversal(V2))
ISBOOL(isNotEqualTo(V1, V2)) -> AND(isUniversal(V1), isUniversal(V2))
ISBOOL(or(V1, V2)) -> AND(isBool(V1), isBool(V2))
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> AND(isBool(V1), isBool(V2))
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(not(V1)) -> ISBOOL(V1)
NOT(A) -> U151'(isBool(A), A)
NOT(A) -> ISBOOL(A)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
ISBOOL(not(V1)) -> ISBOOL(V1)
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
ISBOOL(implies(V1, V2)) -> ISBOOL(V2)
ISBOOL(implies(V1, V2)) -> ISBOOL(V1)
ISBOOL(and(V1, V2)) -> ISBOOL(V2)
ISBOOL(and(V1, V2)) -> ISBOOL(V1)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
ISBOOL(implies(V1, V2)) -> ISBOOL(V2)
ISBOOL(implies(V1, V2)) -> ISBOOL(V1)
POL(not_(x1)) = x1 POL(_and_(x1, x2)) = x1 + x2 POL(_xor_(x1, x2)) = x1 + x2 POL(ISBOOL(x1)) = x1 POL(_or_(x1, x2)) = x1 + x2 POL(_implies_(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
ISBOOL(not(V1)) -> ISBOOL(V1)
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
ISBOOL(and(V1, V2)) -> ISBOOL(V2)
ISBOOL(and(V1, V2)) -> ISBOOL(V1)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
ISBOOL(and(V1, V2)) -> ISBOOL(V2)
ISBOOL(and(V1, V2)) -> ISBOOL(V1)
POL(not_(x1)) = x1 POL(_and_(x1, x2)) = 1 + x1 + x2 POL(_xor_(x1, x2)) = x1 + x2 POL(ISBOOL(x1)) = x1 POL(_or_(x1, x2)) = x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 11
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
ISBOOL(not(V1)) -> ISBOOL(V1)
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
ISBOOL(not(V1)) -> ISBOOL(V1)
POL(not_(x1)) = 1 + x1 POL(_xor_(x1, x2)) = x1 + x2 POL(ISBOOL(x1)) = x1 POL(_or_(x1, x2)) = x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 13
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
POL(_xor_(x1, x2)) = 1 + x1 + x2 POL(ISBOOL(x1)) = x1 POL(_or_(x1, x2)) = x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 14
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)
POL(ISBOOL(x1)) = x1 POL(_or_(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 15
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
xor(xor(false, A), ext) -> xor(U121(isBool(A), A), ext)
xor(xor(A, A), ext) -> xor(U111(isBool(A)), ext)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
xor(xor(false, A), ext) -> xor(U121(isBool(A), A), ext)
xor(xor(A, A), ext) -> xor(U111(isBool(A)), ext)
U121(tt, A) -> A
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
U111(tt) -> false
and(tt, X) -> X
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)
POL(and(x1, x2)) = x2 POL(false) = 0 POL(not_(x1)) = 0 POL(_and_(x1, x2)) = 0 POL(_xor_(x1, x2)) = 1 + x1 + x2 POL(true) = 0 POL(_isNotEqualTo_(x1, x2)) = 0 POL(U121(x1, x2)) = x2 POL(isUniversal(x1)) = 0 POL(_isEqualTo_(x1, x2)) = 0 POL(tt) = 0 POL(_or_(x1, x2)) = x1·x2 POL(_implies_(x1, x2)) = 0 POL(isBool(x1)) = 0 POL(U111(x1)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polynomial Ordering
→DP Problem 4
↳Polo
→DP Problem 5
↳Inst
and(and(true, A), ext) -> and(U41(isBool(A), A), ext)
and(and(false, A), ext) -> and(U31(isBool(A)), ext)
U21'(tt, A, B, C) -> and(A, C)
and(and(A, xor(B, C)), ext) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(and(A, xor(B, C)), ext) -> and(U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C), ext)
and(and(A, A), ext) -> and(U11(isBool(A), A), ext)
U21'(tt, A, B, C) -> and(A, B)
and(A, xor(B, C)) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
U21'(tt, A, B, C) -> and(A, C)
and(and(A, xor(B, C)), ext) -> and(U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C), ext)
and(and(false, A), ext) -> and(U31(isBool(A)), ext)
and(and(true, A), ext) -> and(U41(isBool(A), A), ext)
U21'(tt, A, B, C) -> and(A, B)
and(A, xor(B, C)) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(and(A, A), ext) -> and(U11(isBool(A), A), ext)
and(and(A, xor(B, C)), ext) -> U21'(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
U41(tt, A) -> A
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
and(tt, X) -> X
U11(tt, A) -> A
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
U111(tt) -> false
U121(tt, A) -> A
and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)
POL(and(x1, x2)) = x1·x2 POL(U31(x1)) = 0 POL(false) = 0 POL(not_(x1)) = 1 POL(_and_(x1, x2)) = 1 + 2·x1 + 2·x1·x2 + 2·x2 POL(true) = 0 POL(_xor_(x1, x2)) = 2 + x1 + x2 POL(_isNotEqualTo_(x1, x2)) = 0 POL(U121(x1, x2)) = x2 POL(U11(x1, x2)) = x2 POL(isUniversal(x1)) = 0 POL(_isEqualTo_(x1, x2)) = 0 POL(U41(x1, x2)) = x1·x2 POL(U21(x1, x2, x3, x4)) = 2 + 2·x1 + 2·x1·x2 + 2·x2 + 2·x2·x3 + 2·x2·x4 + 2·x3 + 2·x4 POL(tt) = 1 POL(U21'(x1, x2, x3, x4)) = 2 + 2·x2 + 2·x2·x3 + 2·x2·x4 + 2·x3 + 2·x4 POL(_or_(x1, x2)) = 0 POL(_implies_(x1, x2)) = 0 POL(isBool(x1)) = 1 POL(U111(x1)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polynomial Ordering
→DP Problem 5
↳Inst
U61'(tt, U', U) -> ISNOTEQUALTO(U, U')
ISEQUALTO(U, U') -> U61'(and(isS(U'), isS(U)), U', U)
U81'(tt, U', U) -> ISEQUALTO(U, U')
IFTHENELSEFI(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U81'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
U61'(tt, U', U) -> ISNOTEQUALTO(U, U')
and(tt, X) -> X
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U71(tt) -> true
U62(tt) -> false
equal(X, X) -> tt
U141(tt, U) -> U
U91(tt) -> false
U132(tt, U') -> U'
POL(U71(x1)) = 0 POL(and(x1, x2)) = x2 POL(IF_THEN_ELSE_FI(x1, x2, x3)) = 0 POL(false) = 0 POL(not_(x1)) = 0 POL(_and_(x1, x2)) = 0 POL(true) = 0 POL(U131(x1, x2, x3)) = x3 POL(U132(x1, x2)) = x2 POL(_isNotEqualTo_(x1, x2)) = 0 POL(U91(x1)) = 0 POL(U81'(x1, x2, x3)) = 0 POL(if_then_else_fi(x1, x2, x3)) = x2 + x3 POL(U62(x1)) = 0 POL(U61'(x1, x2, x3)) = x1 POL(_or_(x1, x2)) = 0 POL(isS(x1)) = 0 POL(isBool(x1)) = 1 POL(_implies_(x1, x2)) = 0 POL(equal(x1, x2)) = 1 POL(_ISNOTEQUALTO_(x1, x2)) = 0 POL(U131'(x1, x2, x3)) = 0 POL(_ISEQUALTO_(x1, x2)) = 0 POL(_xor_(x1, x2)) = 0 POL(isUniversal(x1)) = 0 POL(U81(x1, x2, x3)) = 0 POL(_isEqualTo_(x1, x2)) = 0 POL(U141(x1, x2)) = x2 POL(tt) = 1 POL(U61(x1, x2, x3)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 9
↳Dependency Graph
→DP Problem 5
↳Inst
ISEQUALTO(U, U') -> U61'(and(isS(U'), isS(U)), U', U)
U81'(tt, U', U) -> ISEQUALTO(U, U')
IFTHENELSEFI(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U81'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 9
↳DGraph
...
→DP Problem 10
↳Polynomial Ordering
→DP Problem 5
↳Inst
U81'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
IFTHENELSEFI(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
U81'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
and(tt, X) -> X
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U71(tt) -> true
U62(tt) -> false
equal(X, X) -> tt
U141(tt, U) -> U
U91(tt) -> false
U132(tt, U') -> U'
POL(U71(x1)) = 0 POL(and(x1, x2)) = x2 POL(IF_THEN_ELSE_FI(x1, x2, x3)) = 0 POL(false) = 0 POL(not_(x1)) = 0 POL(_and_(x1, x2)) = 0 POL(true) = 0 POL(U131(x1, x2, x3)) = x3 POL(U132(x1, x2)) = x2 POL(_isNotEqualTo_(x1, x2)) = 0 POL(U91(x1)) = 0 POL(U81'(x1, x2, x3)) = x1 POL(if_then_else_fi(x1, x2, x3)) = x2 + x3 POL(U62(x1)) = 0 POL(_or_(x1, x2)) = 0 POL(isS(x1)) = 0 POL(_implies_(x1, x2)) = 0 POL(isBool(x1)) = 1 POL(equal(x1, x2)) = 1 POL(_ISNOTEQUALTO_(x1, x2)) = 0 POL(U131'(x1, x2, x3)) = 0 POL(_xor_(x1, x2)) = 0 POL(U81(x1, x2, x3)) = 0 POL(isUniversal(x1)) = 0 POL(_isEqualTo_(x1, x2)) = 0 POL(U141(x1, x2)) = x2 POL(tt) = 1 POL(U61(x1, x2, x3)) = 0
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 9
↳DGraph
...
→DP Problem 12
↳Dependency Graph
→DP Problem 5
↳Inst
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
IFTHENELSEFI(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 4
↳Polo
→DP Problem 5
↳Instantiation Transformation
or(or(A, B), ext) -> or(U101(and(isBool(A), isBool(B)), A, B), ext)
U101(tt, A, B) -> xor(and(A, B), xor(A, B))
U11(tt, A) -> A
U111(tt) -> false
U121(tt, A) -> A
U131(tt, B, U') -> U132(equal(isNotEqualTo(B, true), true), U')
U132(tt, U') -> U'
U141(tt, U) -> U
U151(tt, A) -> xor(A, true)
U21(tt, A, B, C) -> xor(and(A, B), and(A, C))
U31(tt) -> false
U41(tt, A) -> A
U51(tt, A, B) -> not(xor(A, and(A, B)))
U61(tt, U', U) -> U62(equal(isNotEqualTo(U, U'), true))
U62(tt) -> false
U71(tt) -> true
U81(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U91(tt) -> false
and(A, A) -> U11(isBool(A), A)
and(A, xor(B, C)) -> U21(and(isBool(A), and(isBool(B), isBool(C))), A, B, C)
and(false, A) -> U31(isBool(A))
and(true, A) -> U41(isBool(A), A)
implies(A, B) -> U51(and(isBool(A), isBool(B)), A, B)
isEqualTo(U, U') -> U61(and(isS(U'), isS(U)), U', U)
isEqualTo(U, U) -> U71(isS(U))
isNotEqualTo(U, U') -> U81(and(isS(U'), isS(U)), U', U)
isNotEqualTo(U, U) -> U91(isS(U))
or(A, B) -> U101(and(isBool(A), isBool(B)), A, B)
xor(A, A) -> U111(isBool(A))
xor(false, A) -> U121(isBool(A), A)
and(tt, X) -> X
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
ifthenelsefi(true, U, U') -> U141(and(isS(U'), isS(U)), U)
isBool(false) -> tt
isBool(true) -> tt
isBool(and(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(implies(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(isEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(isNotEqualTo(V1, V2)) -> and(isUniversal(V1), isUniversal(V2))
isBool(or(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(xor(V1, V2)) -> and(isBool(V1), isBool(V2))
isBool(not(V1)) -> isBool(V1)
not(A) -> U151(isBool(A), A)
not(false) -> true
not(true) -> false
no new Dependency Pairs are created.
or(or(A, B), ext) -> or(U101(and(isBool(A), isBool(B)), A, B), ext)