MAYBE
R
↳Dependency Pair Analysis
U11'(tt, A, B, C) -> U12'(tt, A, B, C)
U12'(tt, A, B, C) -> U13'(tt, A, B, C)
U13'(tt, A, B, C) -> xor(and(A, B), and(A, C))
U13'(tt, A, B, C) -> and(A, B)
U13'(tt, A, B, C) -> and(A, C)
U21'(tt, A, B) -> U22'(tt, A, B)
U22'(tt, A, B) -> NOT(xor(A, and(A, B)))
U22'(tt, A, B) -> xor(A, and(A, B))
U22'(tt, A, B) -> and(A, B)
U31'(tt, U', U) -> U32'(tt, U', U)
U32'(tt, U', U) -> U33'(equal(isNotEqualTo(U, U'), true))
U32'(tt, U', U) -> EQUAL(isNotEqualTo(U, U'), true)
U32'(tt, U', U) -> ISNOTEQUALTO(U, U')
U41'(tt, U', U) -> U42'(tt, U', U)
U42'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
U42'(tt, U', U) -> ISEQUALTO(U, U')
U51'(tt, A, B) -> U52'(tt, A, B)
U52'(tt, A, B) -> xor(and(A, B), xor(A, B))
U52'(tt, A, B) -> and(A, B)
U52'(tt, A, B) -> xor(A, B)
U61'(tt, B, U') -> U62'(tt, B, U')
U62'(tt, B, U') -> U63'(tt, B, U')
U63'(tt, B, U') -> U64'(equal(isNotEqualTo(B, true), true), U')
U63'(tt, B, U') -> EQUAL(isNotEqualTo(B, true), true)
U63'(tt, B, U') -> ISNOTEQUALTO(B, true)
U71'(tt, U) -> U72'(tt, U)
and(A, xor(B, C)) -> U11'(tt, A, B, C)
and(and(A, A), ext) -> and(A, ext)
and(and(A, xor(B, C)), ext) -> and(U11(tt, A, B, C), ext)
and(and(A, xor(B, C)), ext) -> U11'(tt, A, B, C)
and(and(false, A), ext) -> and(false, ext)
IMPLIES(A, B) -> U21'(tt, A, B)
ISEQUALTO(U, U') -> U31'(tt, U', U)
ISNOTEQUALTO(U, U') -> U41'(tt, U', U)
or(A, B) -> U51'(tt, A, B)
or(or(A, B), ext) -> or(U51(tt, A, B), ext)
or(or(A, B), ext) -> U51'(tt, A, B)
xor(xor(A, A), ext) -> xor(false, ext)
IFTHENELSEFI(B, U, U') -> U61'(tt, B, U')
IFTHENELSEFI(true, U, U') -> U71'(tt, U)
NOT(A) -> xor(A, true)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
xor(xor(A, A), ext) -> xor(false, ext)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
xor(xor(A, A), ext) -> xor(false, ext)
xor(A, A) -> false
xor(false, A) -> A
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)
POL(false) = 0 POL(_xor_(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
U13'(tt, A, B, C) -> and(A, C)
and(and(false, A), ext) -> and(false, ext)
and(and(A, xor(B, C)), ext) -> U11'(tt, A, B, C)
and(and(A, xor(B, C)), ext) -> and(U11(tt, A, B, C), ext)
and(and(A, A), ext) -> and(A, ext)
and(A, xor(B, C)) -> U11'(tt, A, B, C)
U13'(tt, A, B, C) -> and(A, B)
U12'(tt, A, B, C) -> U13'(tt, A, B, C)
U11'(tt, A, B, C) -> U12'(tt, A, B, C)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
U13'(tt, A, B, C) -> and(A, C)
U13'(tt, A, B, C) -> and(A, B)
and(A, xor(B, C)) -> U11'(tt, A, B, C)
U12'(tt, A, B, C) -> U13'(tt, A, B, C)
and(and(A, A), ext) -> and(A, ext)
and(and(false, A), ext) -> and(false, ext)
U11'(tt, A, B, C) -> U12'(tt, A, B, C)
and(and(A, xor(B, C)), ext) -> U11'(tt, A, B, C)
and(and(A, xor(B, C)), ext) -> and(U11(tt, A, B, C), ext)
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U12(tt, A, B, C) -> U13(tt, A, B, C)
U11(tt, A, B, C) -> U12(tt, A, B, C)
xor(A, A) -> false
xor(false, 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(false) = 0 POL(U12(x1, x2, x3, x4)) = 2·x1 + 2·x1·x2 + x1·x2·x4 + x1·x4 + 2·x2·x3 + 2·x3 POL(U12'(x1, x2, x3, x4)) = 1 + x1 + 2·x2 + 2·x2·x3 + 2·x2·x4 + 2·x3 + 2·x4 POL(_and_(x1, x2)) = 1 + 2·x1 + 2·x1·x2 + 2·x2 POL(tt) = 2 POL(_xor_(x1, x2)) = 2 + x1 + x2 POL(true) = 0 POL(U13(x1, x2, x3, x4)) = 2·x1 + 2·x1·x2 + 2·x2·x3 + 2·x2·x4 + 2·x3 + 2·x4 POL(U13'(x1, x2, x3, x4)) = x1 + x1·x2·x4 + 2·x2 + 2·x2·x3 + 2·x3 + 2·x4 POL(U11(x1, x2, x3, x4)) = 2·x1 + 2·x1·x2 + x1·x2·x3 + x1·x2·x4 + x1·x3 + x1·x4 POL(U11'(x1, x2, x3, x4)) = 2·x1 + 2·x2 + 2·x2·x3 + 2·x2·x4 + 2·x3 + 2·x4
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
ISEQUALTO(U, U') -> U31'(tt, U', U)
U42'(tt, U', U) -> ISEQUALTO(U, U')
U63'(tt, B, U') -> ISNOTEQUALTO(B, true)
U62'(tt, B, U') -> U63'(tt, B, U')
U61'(tt, B, U') -> U62'(tt, B, U')
IFTHENELSEFI(B, U, U') -> U61'(tt, B, U')
U42'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
U41'(tt, U', U) -> U42'(tt, U', U)
ISNOTEQUALTO(U, U') -> U41'(tt, U', U)
U32'(tt, U', U) -> ISNOTEQUALTO(U, U')
U31'(tt, U', U) -> U32'(tt, U', U)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
or(or(A, B), ext) -> or(U51(tt, A, B), ext)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
ISEQUALTO(U, U') -> U31'(tt, U', U)
U42'(tt, U', U) -> ISEQUALTO(U, U')
U63'(tt, B, U') -> ISNOTEQUALTO(B, true)
U62'(tt, B, U') -> U63'(tt, B, U')
U61'(tt, B, U') -> U62'(tt, B, U')
IFTHENELSEFI(B, U, U') -> U61'(tt, B, U')
U42'(tt, U', U) -> IFTHENELSEFI(isEqualTo(U, U'), false, true)
U41'(tt, U', U) -> U42'(tt, U', U)
ISNOTEQUALTO(U, U') -> U41'(tt, U', U)
U32'(tt, U', U) -> ISNOTEQUALTO(U, U')
U31'(tt, U', U) -> U32'(tt, U', U)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
or(or(A, B), ext) -> or(U51(tt, A, B), ext)
U11(tt, A, B, C) -> U12(tt, A, B, C)
U12(tt, A, B, C) -> U13(tt, A, B, C)
U13(tt, A, B, C) -> xor(and(A, B), and(A, C))
U21(tt, A, B) -> U22(tt, A, B)
U22(tt, A, B) -> not(xor(A, and(A, B)))
U31(tt, U', U) -> U32(tt, U', U)
U32(tt, U', U) -> U33(equal(isNotEqualTo(U, U'), true))
U33(tt) -> false
U41(tt, U', U) -> U42(tt, U', U)
U42(tt, U', U) -> ifthenelsefi(isEqualTo(U, U'), false, true)
U51(tt, A, B) -> U52(tt, A, B)
U52(tt, A, B) -> xor(and(A, B), xor(A, B))
U61(tt, B, U') -> U62(tt, B, U')
U62(tt, B, U') -> U63(tt, B, U')
U63(tt, B, U') -> U64(equal(isNotEqualTo(B, true), true), U')
U64(tt, U') -> U'
U71(tt, U) -> U72(tt, U)
U72(tt, U) -> U
and(A, A) -> A
and(A, xor(B, C)) -> U11(tt, A, B, C)
and(false, A) -> false
and(true, A) -> A
implies(A, B) -> U21(tt, A, B)
isEqualTo(U, U') -> U31(tt, U', U)
isEqualTo(U, U) -> true
isNotEqualTo(U, U') -> U41(tt, U', U)
isNotEqualTo(U, U) -> false
or(A, B) -> U51(tt, A, B)
xor(A, A) -> false
xor(false, A) -> A
equal(X, X) -> tt
ifthenelsefi(B, U, U') -> U61(tt, B, U')
ifthenelsefi(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false