Termination Proof using AProVE

MAYBE Termination Proof using AProVETerm Rewriting System R:
[A, B, C, U', U, X, z, y, x]
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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
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:

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) -> IF_{THEN_{ELSE_FI}}(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)
IF_{THEN_{ELSE_FI}}(B, U, U') -> U61'(tt, B, U')
IF_{THEN_{ELSE_FI}}(true, U, U') -> U71'(tt, U)
NOT(A) -> xor(A, true)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pair:

xor(xor(A, A), ext) -> xor(false, ext)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pair can be strictly oriented:

xor(xor(A, A), ext) -> xor(false, ext)

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

xor(A, A) -> false
xor(false, A) -> A

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(false) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Remaining

       →DP Problem 4

         ↳Remaining

Dependency Pairs:

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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The following dependency pairs can be strictly oriented:

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)

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

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

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(false) = 0

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

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

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

POL(tt) = 2

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

POL(true) = 0

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

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
Dependency Pairs:
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')
IF_{THEN_{ELSE_FI}}(B, U, U') -> U61'(tt, B, U')
U42'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
Dependency Pair:
or(or(A, B), ext) -> or(U51(tt, A, B), ext)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
Dependency Pairs:
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')
IF_{THEN_{ELSE_FI}}(B, U, U') -> U61'(tt, B, U')
U42'(tt, U', U) -> IF_{THEN_{ELSE_FI}}(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)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false
Dependency Pair:
or(or(A, B), ext) -> or(U51(tt, A, B), ext)

Rules:

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) -> if_{then_{else_fi}}(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
if_{then_{else_fi}}(B, U, U') -> U61(tt, B, U')
if_{then_{else_fi}}(true, U, U') -> U71(tt, U)
not(A) -> xor(A, true)
not(false) -> true
not(true) -> false

The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
5:00 minutes Timeout: aborting command ``runme'' with signal 9

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

POL(false)	= 0
POL(U12(x₁, x₂, x₃, x₄))	= 2·x₁ + 2·x₁·x₂ + x₁·x₂·x₄ + x₁·x₄ + 2·x₂·x₃ + 2·x₃
POL(U12'(x₁, x₂, x₃, x₄))	= 1 + x₁ + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄
POL(_and_(x₁, x₂))	= 1 + 2·x₁ + 2·x₁·x₂ + 2·x₂
POL(tt)	= 2
POL(_xor_(x₁, x₂))	= 2 + x₁ + x₂
POL(true)	= 0
POL(U13(x₁, x₂, x₃, x₄))	= 2·x₁ + 2·x₁·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄
POL(U13'(x₁, x₂, x₃, x₄))	= x₁ + x₁·x₂·x₄ + 2·x₂ + 2·x₂·x₃ + 2·x₃ + 2·x₄
POL(U11(x₁, x₂, x₃, x₄))	= 2·x₁ + 2·x₁·x₂ + x₁·x₂·x₃ + x₁·x₂·x₄ + x₁·x₃ + x₁·x₄
POL(U11'(x₁, x₂, x₃, x₄))	= 2·x₁ + 2·x₂ + 2·x₂·x₃ + 2·x₂·x₄ + 2·x₃ + 2·x₄