Termination Proof using AProVE

YES Termination Proof using AProVETerm Rewriting System R:
[A, B, U', U, C, X, V1, V2, z, y, x]
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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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
and(x, and(y, z)) == and(and(x, y), z)
and(x, y) == and(y, x)
or(x, or(y, z)) == or(or(x, y), z)
or(x, y) == or(y, x)
xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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) -> IF_{THEN_{ELSE_FI}}(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)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
IF_{THEN_{ELSE_FI}}(B, U, U') -> AND(isBool(B), and(isS(U'), isS(U)))
IF_{THEN_{ELSE_FI}}(B, U, U') -> ISBOOL(B)
IF_{THEN_{ELSE_FI}}(B, U, U') -> AND(isS(U'), isS(U))
IF_{THEN_{ELSE_FI}}(true, U, U') -> U141'(and(isS(U'), isS(U)), U)
IF_{THEN_{ELSE_FI}}(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)

Furthermore, R contains five SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

Dependency Pairs:

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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

ISBOOL(implies(V1, V2)) -> ISBOOL(V2)
ISBOOL(implies(V1, V2)) -> ISBOOL(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(not_(x₁)) = x₁

POL(_and_(x₁, x₂)) = x₁ + x₂

POL(_xor_(x₁, x₂)) = x₁ + x₂

POL(ISBOOL(x₁)) = x₁

POL(_or_(x₁, x₂)) = x₁ + x₂

POL(_implies_(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.

     ↳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

Dependency Pairs:

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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

ISBOOL(and(V1, V2)) -> ISBOOL(V2)
ISBOOL(and(V1, V2)) -> ISBOOL(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(not_(x₁)) = x₁

POL(_and_(x₁, x₂)) = 1 + x₁ + x₂

POL(_xor_(x₁, x₂)) = x₁ + x₂

POL(ISBOOL(x₁)) = x₁

POL(_or_(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.

     ↳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

Dependency Pairs:

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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pair can be strictly oriented:

ISBOOL(not(V1)) -> ISBOOL(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(not_(x₁)) = 1 + x₁

POL(_xor_(x₁, x₂)) = x₁ + x₂

POL(ISBOOL(x₁)) = x₁

POL(_or_(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.

     ↳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

Dependency Pairs:

ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)
ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

ISBOOL(xor(V1, V2)) -> ISBOOL(V2)
ISBOOL(xor(V1, V2)) -> ISBOOL(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(_xor_(x₁, x₂)) = 1 + x₁ + x₂

POL(ISBOOL(x₁)) = x₁

POL(_or_(x₁, x₂)) = x₁ + x₂

resulting in one new DP problem.

     ↳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

Dependency Pairs:

ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

ISBOOL(or(V1, V2)) -> ISBOOL(V2)
ISBOOL(or(V1, V2)) -> ISBOOL(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(ISBOOL(x₁)) = x₁

POL(_or_(x₁, x₂)) = 1 + x₁ + x₂

resulting in one new DP problem.

     ↳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

Dependency Pair:

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

Dependency Pairs:

xor(xor(false, A), ext) -> xor(U121(isBool(A), A), ext)
xor(xor(A, A), ext) -> xor(U111(isBool(A)), ext)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

xor(xor(false, A), ext) -> xor(U121(isBool(A), A), ext)
xor(xor(A, A), ext) -> xor(U111(isBool(A)), ext)

Additionally, the following usable rules using the Ce-refinement can be oriented:

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

Oriented Equations:

xor(x, xor(y, z)) == xor(xor(x, y), z)
xor(x, y) == xor(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(and(x₁, x₂)) = x₂

POL(false) = 0

POL(not_(x₁)) = 0

POL(_and_(x₁, x₂)) = 0

POL(_xor_(x₁, x₂)) = 1 + x₁ + x₂

POL(true) = 0

POL(_isNotEqualTo_(x₁, x₂)) = 0

POL(U121(x₁, x₂)) = x₂

POL(isUniversal(x₁)) = 0

POL(_isEqualTo_(x₁, x₂)) = 0

POL(tt) = 0

POL(_or_(x₁, x₂)) = x₁·x₂

POL(_implies_(x₁, x₂)) = 0

POL(isBool(x₁)) = 0

POL(U111(x₁)) = 0

resulting in one new DP problem.

     ↳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

Dependency Pair:

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Inst

Dependency Pairs:

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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pairs can be strictly oriented:

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)

Additionally, the following usable rules using the Ce-refinement can be oriented:

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

Oriented Equations:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(and(x₁, x₂)) = x₁·x₂

POL(U31(x₁)) = 0

POL(false) = 0

POL(not_(x₁)) = 1

POL(_and_(x₁, x₂)) = 1 + 2·x₁ + 2·x₁·x₂ + 2·x₂

POL(true) = 0

POL(_xor_(x₁, x₂)) = 2 + x₁ + x₂

POL(_isNotEqualTo_(x₁, x₂)) = 0

POL(U121(x₁, x₂)) = x₂

POL(U11(x₁, x₂)) = x₂

POL(isUniversal(x₁)) = 0

POL(_isEqualTo_(x₁, x₂)) = 0

POL(U41(x₁, x₂)) = x₁·x₂

POL(U21(x₁, x₂, x₃, x₄)) = 2 + 2·x₁ + 2·x₁·x₂ + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄

POL(tt) = 1

POL(U21'(x₁, x₂, x₃, x₄)) = 2 + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄

POL(_or_(x₁, x₂)) = 0

POL(_implies_(x₁, x₂)) = 0

POL(isBool(x₁)) = 1

POL(U111(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

       →DP Problem 5

         ↳Inst

Dependency Pairs:

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')
IF_{THEN_{ELSE_FI}}(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U81'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pair can be strictly oriented:

U61'(tt, U', U) -> ISNOTEQUALTO(U, U')

Additionally, the following usable rules using the Ce-refinement can be oriented:

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))
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(true, U, U') -> U141(and(isS(U'), isS(U)), U)
U81(tt, U', U) -> if_{then_{else_fi}}(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'

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U71(x₁)) = 0

POL(and(x₁, x₂)) = x₂

POL(IF_THEN_ELSE_FI(x₁, x₂, x₃)) = 0

POL(false) = 0

POL(not_(x₁)) = 0

POL(_and_(x₁, x₂)) = 0

POL(true) = 0

POL(U131(x₁, x₂, x₃)) = x₃

POL(U132(x₁, x₂)) = x₂

POL(_isNotEqualTo_(x₁, x₂)) = 0

POL(U91(x₁)) = 0

POL(U81'(x₁, x₂, x₃)) = 0

POL(if_then_else_fi(x₁, x₂, x₃)) = x₂ + x₃

POL(U62(x₁)) = 0

POL(U61'(x₁, x₂, x₃)) = x₁

POL(_or_(x₁, x₂)) = 0

POL(isS(x₁)) = 0

POL(isBool(x₁)) = 1

POL(_implies_(x₁, x₂)) = 0

POL(equal(x₁, x₂)) = 1

POL(_ISNOTEQUALTO_(x₁, x₂)) = 0

POL(U131'(x₁, x₂, x₃)) = 0

POL(_ISEQUALTO_(x₁, x₂)) = 0

POL(_xor_(x₁, x₂)) = 0

POL(isUniversal(x₁)) = 0

POL(U81(x₁, x₂, x₃)) = 0

POL(_isEqualTo_(x₁, x₂)) = 0

POL(U141(x₁, x₂)) = x₂

POL(tt) = 1

POL(U61(x₁, x₂, x₃)) = 0

resulting in one new DP problem.

     ↳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

Dependency Pairs:

ISEQUALTO(U, U') -> U61'(and(isS(U'), isS(U)), U', U)
U81'(tt, U', U) -> ISEQUALTO(U, U')
IF_{THEN_{ELSE_FI}}(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')
U81'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳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

Dependency Pairs:

U81'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)
ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

The following dependency pair can be strictly oriented:

U81'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(isEqualTo(U, U'), false, true)

Additionally, the following usable rules using the Ce-refinement can be oriented:

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))
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(true, U, U') -> U141(and(isS(U'), isS(U)), U)
U81(tt, U', U) -> if_{then_{else_fi}}(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'

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U71(x₁)) = 0

POL(and(x₁, x₂)) = x₂

POL(IF_THEN_ELSE_FI(x₁, x₂, x₃)) = 0

POL(false) = 0

POL(not_(x₁)) = 0

POL(_and_(x₁, x₂)) = 0

POL(true) = 0

POL(U131(x₁, x₂, x₃)) = x₃

POL(U132(x₁, x₂)) = x₂

POL(_isNotEqualTo_(x₁, x₂)) = 0

POL(U91(x₁)) = 0

POL(U81'(x₁, x₂, x₃)) = x₁

POL(if_then_else_fi(x₁, x₂, x₃)) = x₂ + x₃

POL(U62(x₁)) = 0

POL(_or_(x₁, x₂)) = 0

POL(isS(x₁)) = 0

POL(_implies_(x₁, x₂)) = 0

POL(isBool(x₁)) = 1

POL(equal(x₁, x₂)) = 1

POL(_ISNOTEQUALTO_(x₁, x₂)) = 0

POL(U131'(x₁, x₂, x₃)) = 0

POL(_xor_(x₁, x₂)) = 0

POL(U81(x₁, x₂, x₃)) = 0

POL(isUniversal(x₁)) = 0

POL(_isEqualTo_(x₁, x₂)) = 0

POL(U141(x₁, x₂)) = x₂

POL(tt) = 1

POL(U61(x₁, x₂, x₃)) = 0

resulting in one new DP problem.

     ↳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

Dependency Pairs:

ISNOTEQUALTO(U, U') -> U81'(and(isS(U'), isS(U)), U', U)
U131'(tt, B, U') -> ISNOTEQUALTO(B, true)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U131'(and(isBool(B), and(isS(U'), isS(U))), B, U')

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Instantiation Transformation

Dependency Pair:

or(or(A, B), ext) -> or(U101(and(isBool(A), isBool(B)), A, B), ext)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U131(and(isBool(B), and(isS(U'), isS(U))), B, U')
if_{then_{else_fi}}(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

On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

or(or(A, B), ext) -> or(U101(and(isBool(A), isBool(B)), A, B), ext)

no new Dependency Pairs are created.
The transformation is resulting in no new DP problems.

Termination of R successfully shown.
Duration:
1:15 minutes

POL(not_(x₁))	= x₁
POL(_and_(x₁, x₂))	= x₁ + x₂
POL(_xor_(x₁, x₂))	= x₁ + x₂
POL(ISBOOL(x₁))	= x₁
POL(_or_(x₁, x₂))	= x₁ + x₂
POL(_implies_(x₁, x₂))	= 1 + x₁ + x₂

POL(not_(x₁))	= 1 + x₁
POL(_xor_(x₁, x₂))	= x₁ + x₂
POL(ISBOOL(x₁))	= x₁
POL(_or_(x₁, x₂))	= x₁ + x₂

POL(and(x₁, x₂))	= x₂
POL(false)	= 0
POL(not_(x₁))	= 0
POL(_and_(x₁, x₂))	= 0
POL(_xor_(x₁, x₂))	= 1 + x₁ + x₂
POL(true)	= 0
POL(_isNotEqualTo_(x₁, x₂))	= 0
POL(U121(x₁, x₂))	= x₂
POL(isUniversal(x₁))	= 0
POL(_isEqualTo_(x₁, x₂))	= 0
POL(tt)	= 0
POL(_or_(x₁, x₂))	= x₁·x₂
POL(_implies_(x₁, x₂))	= 0
POL(isBool(x₁))	= 0
POL(U111(x₁))	= 0

POL(and(x₁, x₂))	= x₁·x₂
POL(U31(x₁))	= 0
POL(false)	= 0
POL(not_(x₁))	= 1
POL(_and_(x₁, x₂))	= 1 + 2·x₁ + 2·x₁·x₂ + 2·x₂
POL(true)	= 0
POL(_xor_(x₁, x₂))	= 2 + x₁ + x₂
POL(_isNotEqualTo_(x₁, x₂))	= 0
POL(U121(x₁, x₂))	= x₂
POL(U11(x₁, x₂))	= x₂
POL(isUniversal(x₁))	= 0
POL(_isEqualTo_(x₁, x₂))	= 0
POL(U41(x₁, x₂))	= x₁·x₂
POL(U21(x₁, x₂, x₃, x₄))	= 2 + 2·x₁ + 2·x₁·x₂ + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄
POL(tt)	= 1
POL(U21'(x₁, x₂, x₃, x₄))	= 2 + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄
POL(_or_(x₁, x₂))	= 0
POL(_implies_(x₁, x₂))	= 0
POL(isBool(x₁))	= 1
POL(U111(x₁))	= 0

POL(U71(x₁))	= 0
POL(and(x₁, x₂))	= x₂
POL(IF_THEN_ELSE_FI(x₁, x₂, x₃))	= 0
POL(false)	= 0
POL(not_(x₁))	= 0
POL(_and_(x₁, x₂))	= 0
POL(true)	= 0
POL(U131(x₁, x₂, x₃))	= x₃
POL(U132(x₁, x₂))	= x₂
POL(_isNotEqualTo_(x₁, x₂))	= 0
POL(U91(x₁))	= 0
POL(U81'(x₁, x₂, x₃))	= 0
POL(if_then_else_fi(x₁, x₂, x₃))	= x₂ + x₃
POL(U62(x₁))	= 0
POL(U61'(x₁, x₂, x₃))	= x₁
POL(_or_(x₁, x₂))	= 0
POL(isS(x₁))	= 0
POL(isBool(x₁))	= 1
POL(_implies_(x₁, x₂))	= 0
POL(equal(x₁, x₂))	= 1
POL(_ISNOTEQUALTO_(x₁, x₂))	= 0
POL(U131'(x₁, x₂, x₃))	= 0
POL(_ISEQUALTO_(x₁, x₂))	= 0
POL(_xor_(x₁, x₂))	= 0
POL(isUniversal(x₁))	= 0
POL(U81(x₁, x₂, x₃))	= 0
POL(_isEqualTo_(x₁, x₂))	= 0
POL(U141(x₁, x₂))	= x₂
POL(tt)	= 1
POL(U61(x₁, x₂, x₃))	= 0