Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/RENAMED-BOOL_nokinds-noand)

The rewrite relation of the following equational TRS is considered.

Associative symbols: _and_, _or_, _xor_

Commutative symbols: _and_, _or_, _xor_

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

The following set of (strict) dependency pairs is constructed for the TRS.

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

• The 1^st component contains the pair

  _or_#(_or_(x,y),z)	→	_or_#(y,z)	(80)
  _or_#(_or_(A,B),ext)	→	_or_#(U101(isBool(A),A,B),ext)	(172)
  _or_#(x,y)	→	_or_#(y,x)	(74)
  _or_#(_or_(x,y),z)	→	_or_#(x,_or_(y,z))	(77)

  1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_or_#(x1, x2)]	=	2 · x2 + 2 · x1 + 1 · x1 · x2
  [_or_(x1, x2)]	=	2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
  [U101(x1, x2, x3)]	=	2 + 2 · x3 + 2 · x2 + 1 · x2 · x3
  [isBool(x1)]	=	1 · x1 · x1
  [U23(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [tt]	=	0
  [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
  [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [U201(x1, x2)]	=	0
  [U202(x1)]	=	0
  [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [U22(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
  [U171(x1, x2)]	=	0
  [U172(x1)]	=	0
  [isUniversal(x1)]	=	3 · x1 + 2 · x1 · x1
  [U151(x1, x2)]	=	1 · x1 + 2 · x1 · x2
  [U152(x1)]	=	0
  [true]	=	3
  [not_(x1)]	=	2 · x1 + 2 · x1 · x1
  [U211(x1)]	=	2 · x1 · x1
  [false]	=	0
  [_isEqualTo_(x1, x2)]	=	1 · x1 + 1 · x1 · x2
  [U191(x1, x2)]	=	2
  [_isNotEqualTo_(x1, x2)]	=	1 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [U181(x1, x2)]	=	1 + 1 · x2 + 2 · x1 · x2
  [_implies_(x1, x2)]	=	1 + 2 · x2 + 2 · x1
  [U161(x1, x2)]	=	0
  [U121(x1, x2)]	=	1 + 1 · x2
  [U192(x1)]	=	0
  [U182(x1)]	=	0
  [U111(x1)]	=	1
  [U162(x1)]	=	0
  [U11(x1, x2)]	=	1 · x2
  [U31(x1)]	=	0
  [U41(x1, x2)]	=	2 · x2
  [U102(x1, x2, x3)]	=	2 + 2 · x3 + 2 · x2 + 1 · x2 · x3

  together with the usable rules

  U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
  U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
  U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
  U121(tt,A)	→	A	(5)
  _or_(_or_(A,B),ext)	→	_or_(U101(isBool(A),A,B),ext)	(185)
  _or_(A,B)	→	U101(isBool(A),A,B)	(49)
  _xor_(false,A)	→	U121(isBool(A),A)	(51)
  _xor_(A,A)	→	U111(isBool(A))	(50)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
  U11(tt,A)	→	A	(3)
  U31(tt)	→	false	(29)
  _and_(false,A)	→	U31(isBool(A))	(42)
  _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
  _and_(A,A)	→	U11(isBool(A),A)	(40)
  _and_(true,A)	→	U41(isBool(A),A)	(43)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
  U111(tt)	→	false	(4)
  U101(tt,A,B)	→	U102(isBool(B),A,B)	(1)
  U102(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(2)
  U41(tt,A)	→	A	(30)
  _or_(x,y)	→	_or_(y,x)	(68)
  _or_(_or_(x,y),z)	→	_or_(x,_or_(y,z))	(71)
  _xor_(x,y)	→	_xor_(y,x)	(69)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
  _and_(x,y)	→	_and_(y,x)	(67)

  (w.r.t. the implicit argument filter of the reduction pair), the pair

  _or_#(_or_(x,y),z)

  →

  _or_#(y,z)

  (80)

  could be deleted.

  1.1.1.1 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_or_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_or_(x1, x2)]	=	1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
  [U101(x1, x2, x3)]	=	2 · x3 + 1 · x2 + 2 · x2 · x3
  [isBool(x1)]	=	2 · x1
  [U181(x1, x2)]	=	0
  [tt]	=	2
  [U182(x1)]	=	2 · x1 · x1
  [isUniversal(x1)]	=	0
  [U202(x1)]	=	1 · x1
  [U31(x1)]	=	1 · x1
  [false]	=	1
  [U41(x1, x2)]	=	1 · x2
  [U152(x1)]	=	2 · x1
  [_and_(x1, x2)]	=	2 · x1 · x2
  [U151(x1, x2)]	=	2 · x1 · x2
  [true]	=	1
  [not_(x1)]	=	3 · x1 + 3 · x1 · x1
  [U211(x1)]	=	1 · x1 · x1
  [_isEqualTo_(x1, x2)]	=	3 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [U171(x1, x2)]	=	0
  [U191(x1, x2)]	=	2 · x2 + 1 · x1
  [_xor_(x1, x2)]	=	1 · x2 + 1 · x1
  [U201(x1, x2)]	=	2 · x2
  [_isNotEqualTo_(x1, x2)]	=	3 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [_implies_(x1, x2)]	=	2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
  [U161(x1, x2)]	=	2
  [U23(x1,...,x4)]	=	2 · x2 · x4 + 2 · x2 · x3
  [U102(x1, x2, x3)]	=	1 · x3 + 1 · x2 + 2 · x2 · x3
  [U22(x1,...,x4)]	=	2 · x2 · x4 + 2 · x2 · x3
  [U192(x1)]	=	2 + 1 · x1
  [U121(x1, x2)]	=	1 + 1 · x2
  [U21(x1,...,x4)]	=	2 · x2 · x4 + 2 · x2 · x3
  [U11(x1, x2)]	=	1 · x1 · x2
  [U111(x1)]	=	1 · x1
  [U172(x1)]	=	1 · x1 · x1
  [U162(x1)]	=	2

  together with the usable rules

  U181(tt,V2)	→	U182(isUniversal(V2))	(18)
  U202(tt)	→	tt	(23)
  U31(tt)	→	false	(29)
  U41(tt,A)	→	A	(30)
  _or_(_or_(A,B),ext)	→	_or_(U101(isBool(A),A,B),ext)	(185)
  _or_(A,B)	→	U101(isBool(A),A,B)	(49)
  U152(tt)	→	tt	(13)
  isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
  isBool(true)	→	tt	(56)
  isBool(not_(V1))	→	U211(isBool(V1))	(63)
  isBool(false)	→	tt	(55)
  isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
  isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
  isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
  isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
  isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
  U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
  U101(tt,A,B)	→	U102(isBool(B),A,B)	(1)
  U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
  U211(tt)	→	tt	(25)
  U191(tt,V2)	→	U192(isBool(V2))	(20)
  U121(tt,A)	→	A	(5)
  _and_(false,A)	→	U31(isBool(A))	(42)
  _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
  _and_(A,A)	→	U11(isBool(A),A)	(40)
  _and_(true,A)	→	U41(isBool(A),A)	(43)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
  U182(tt)	→	tt	(19)
  _xor_(false,A)	→	U121(isBool(A),A)	(51)
  _xor_(A,A)	→	U111(isBool(A))	(50)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
  U111(tt)	→	false	(4)
  U172(tt)	→	tt	(17)
  U171(tt,V2)	→	U172(isUniversal(V2))	(16)
  U162(tt)	→	tt	(15)
  U161(tt,V2)	→	U162(isBool(V2))	(14)
  U102(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(2)
  U201(tt,V2)	→	U202(isBool(V2))	(22)
  U11(tt,A)	→	A	(3)
  U192(tt)	→	tt	(21)
  U151(tt,V2)	→	U152(isBool(V2))	(12)
  U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
  _or_(x,y)	→	_or_(y,x)	(68)
  _or_(_or_(x,y),z)	→	_or_(x,_or_(y,z))	(71)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
  _and_(x,y)	→	_and_(y,x)	(67)
  _xor_(x,y)	→	_xor_(y,x)	(69)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)

  (w.r.t. the implicit argument filter of the reduction pair), the pair

  _or_#(_or_(A,B),ext)

  →

  _or_#(U101(isBool(A),A,B),ext)

  (172)

  could be deleted.

  1.1.1.1.1 AC Dependency Pair Problem is trivial

  There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 2^nd component contains the pair

  U21#(tt,A,B,C)	→	U22#(isBool(B),A,B,C)	(103)
  U22#(tt,A,B,C)	→	U23#(isBool(C),A,B,C)	(105)
  U23#(tt,A,B,C)	→	_and_#(A,B)	(109)
  _and_#(A,_xor_(B,C))	→	U21#(isBool(A),A,B,C)	(125)
  _and_#(_and_(A,A),ext)	→	_and_#(U11(isBool(A),A),ext)	(160)
  _and_#(_and_(A,_xor_(B,C)),ext)	→	_and_#(U21(isBool(A),A,B,C),ext)	(163)
  _and_#(_and_(A,_xor_(B,C)),ext)	→	U21#(isBool(A),A,B,C)	(164)
  _and_#(_and_(false,A),ext)	→	_and_#(U31(isBool(A)),ext)	(166)
  _and_#(_and_(true,A),ext)	→	_and_#(U41(isBool(A),A),ext)	(169)
  _and_#(_and_(x,y),z)	→	_and_#(y,z)	(79)
  _and_#(x,y)	→	_and_#(y,x)	(73)
  _and_#(_and_(x,y),z)	→	_and_#(x,_and_(y,z))	(76)
  U23#(tt,A,B,C)	→	_and_#(A,C)	(110)

  1.1.2 AC Reduction Pair Processor with Usable Rules

  Using the non-linear polynomial interpretation over the naturals

  [_and_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
  [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
  [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 1 · x2 + 1 · x2 · x4 + 1 · x1 · x2 + 1 · x1 · x2 · x3
  [isBool(x1)]	=	1
  [U11(x1, x2)]	=	1 · x2
  [U21#(x1,...,x4)]	=	1 · x2 + 1 · x1 + 1 · x1 · x4 + 1 · x1 · x3 + 1 · x1 · x2 · x4 + 1 · x1 · x2 · x3
  [false]	=	0
  [U31(x1)]	=	0
  [U23#(x1,...,x4)]	=	1 · x3 + 1 · x2 + 1 · x2 · x4 + 1 · x1 · x4 + 1 · x2 · x3
  [tt]	=	1
  [true]	=	1
  [U41(x1, x2)]	=	1 · x2
  [U22#(x1,...,x4)]	=	1 · x4 + 1 · x3 + 1 · x2 + 1 · x2 · x4 + 1 · x1 · x2 · x3
  [U151(x1, x2)]	=	1 · x1
  [not_(x1)]	=	0
  [U211(x1)]	=	1
  [_isEqualTo_(x1, x2)]	=	1 + 1 · x2 + 1 · x1 + 1 · x1 · x2
  [U171(x1, x2)]	=	1
  [isUniversal(x1)]	=	1
  [_or_(x1, x2)]	=	1 + 1 · x2 + 1 · x1 + 1 · x1 · x2
  [U191(x1, x2)]	=	1
  [U201(x1, x2)]	=	1
  [_isNotEqualTo_(x1, x2)]	=	1 + 1 · x2 + 1 · x1 + 1 · x1 · x2
  [U181(x1, x2)]	=	1 · x1
  [_implies_(x1, x2)]	=	1 + 1 · x2 + 1 · x1 + 1 · x1 · x2
  [U161(x1, x2)]	=	1 · x1
  [U202(x1)]	=	1 · x1
  [U172(x1)]	=	1 · x1
  [U121(x1, x2)]	=	1 · x1 · x2
  [U111(x1)]	=	0
  [U192(x1)]	=	1 · x1
  [U182(x1)]	=	1 · x1
  [U22(x1,...,x4)]	=	1 · x3 + 1 · x2 + 1 · x1 + 1 · x2 · x4 + 1 · x1 · x4 + 1 · x2 · x3 + 1 · x1 · x2
  [U162(x1)]	=	1 · x1
  [U23(x1,...,x4)]	=	1 · x4 + 1 · x3 + 1 · x2 + 1 · x1 + 1 · x2 · x4 + 1 · x2 · x3 + 1 · x1 · x2
  [U152(x1)]	=	1 · x1

  together with the usable rules

  isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
  isBool(true)	→	tt	(56)
  isBool(not_(V1))	→	U211(isBool(V1))	(63)
  isBool(false)	→	tt	(55)
  isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
  isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
  isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
  isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
  isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
  U201(tt,V2)	→	U202(isBool(V2))	(22)
  U171(tt,V2)	→	U172(isUniversal(V2))	(16)
  U121(tt,A)	→	A	(5)
  U31(tt)	→	false	(29)
  U111(tt)	→	false	(4)
  U191(tt,V2)	→	U192(isBool(V2))	(20)
  U211(tt)	→	tt	(25)
  U172(tt)	→	tt	(17)
  U181(tt,V2)	→	U182(isUniversal(V2))	(18)
  U192(tt)	→	tt	(21)
  U41(tt,A)	→	A	(30)
  U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
  U182(tt)	→	tt	(19)
  _xor_(false,A)	→	U121(isBool(A),A)	(51)
  _xor_(A,A)	→	U111(isBool(A))	(50)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
  U161(tt,V2)	→	U162(isBool(V2))	(14)
  U202(tt)	→	tt	(23)
  U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
  U152(tt)	→	tt	(13)
  U151(tt,V2)	→	U152(isBool(V2))	(12)
  U11(tt,A)	→	A	(3)
  U162(tt)	→	tt	(15)
  _and_(false,A)	→	U31(isBool(A))	(42)
  _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
  _and_(A,A)	→	U11(isBool(A),A)	(40)
  _and_(true,A)	→	U41(isBool(A),A)	(43)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
  U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
  _xor_(x,y)	→	_xor_(y,x)	(69)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)
  _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
  _and_(x,y)	→	_and_(y,x)	(67)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  _and_#(_and_(true,A),ext)	→	_and_#(U41(isBool(A),A),ext)	(169)
  U21#(tt,A,B,C)	→	U22#(isBool(B),A,B,C)	(103)

  could be deleted.

  1.1.2.1 Dependency Graph Processor

  The dependency pairs are split into 1 component.

  • The 1^st component contains the pair

    _and_#(_and_(A,A),ext)	→	_and_#(U11(isBool(A),A),ext)	(160)
    _and_#(_and_(A,_xor_(B,C)),ext)	→	_and_#(U21(isBool(A),A,B,C),ext)	(163)
    _and_#(_and_(false,A),ext)	→	_and_#(U31(isBool(A)),ext)	(166)
    _and_#(_and_(x,y),z)	→	_and_#(y,z)	(79)
    _and_#(x,y)	→	_and_#(y,x)	(73)
    _and_#(_and_(x,y),z)	→	_and_#(x,_and_(y,z))	(76)

    1.1.2.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
    [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
    [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
    [isBool(x1)]	=	2 · x1
    [U11(x1, x2)]	=	1 · x2
    [false]	=	1
    [U31(x1)]	=	1 · x1
    [U152(x1)]	=	1 · x1
    [tt]	=	2
    [U121(x1, x2)]	=	1 · x2
    [U111(x1)]	=	1
    [U22(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
    [U23(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
    [U161(x1, x2)]	=	2 · x1
    [U162(x1)]	=	2
    [U181(x1, x2)]	=	2 · x1
    [U182(x1)]	=	1 · x1 · x1
    [isUniversal(x1)]	=	0
    [U151(x1, x2)]	=	1 · x1 · x2
    [true]	=	1
    [not_(x1)]	=	1 + 3 · x1 · x1
    [U211(x1)]	=	1 · x1 · x1
    [_isEqualTo_(x1, x2)]	=	2 + 2 · x1
    [U171(x1, x2)]	=	2
    [_or_(x1, x2)]	=	2 + 3 · x2 + 2 · x1
    [U191(x1, x2)]	=	2
    [U201(x1, x2)]	=	2 + 2 · x2
    [_isNotEqualTo_(x1, x2)]	=	3 · x2
    [_implies_(x1, x2)]	=	2 · x2 + 2 · x1
    [U202(x1)]	=	2
    [U41(x1, x2)]	=	1 · x2
    [U172(x1)]	=	2
    [U192(x1)]	=	2

    together with the usable rules

    U152(tt)	→	tt	(13)
    _xor_(false,A)	→	U121(isBool(A),A)	(51)
    _xor_(A,A)	→	U111(isBool(A))	(50)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
    U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
    U11(tt,A)	→	A	(3)
    U121(tt,A)	→	A	(5)
    U161(tt,V2)	→	U162(isBool(V2))	(14)
    U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
    U181(tt,V2)	→	U182(isUniversal(V2))	(18)
    U162(tt)	→	tt	(15)
    isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
    isBool(true)	→	tt	(56)
    isBool(not_(V1))	→	U211(isBool(V1))	(63)
    isBool(false)	→	tt	(55)
    isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
    isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
    isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
    isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
    isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
    U202(tt)	→	tt	(23)
    U211(tt)	→	tt	(25)
    U31(tt)	→	false	(29)
    _and_(false,A)	→	U31(isBool(A))	(42)
    _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
    _and_(A,A)	→	U11(isBool(A),A)	(40)
    _and_(true,A)	→	U41(isBool(A),A)	(43)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
    U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
    U172(tt)	→	tt	(17)
    U201(tt,V2)	→	U202(isBool(V2))	(22)
    U171(tt,V2)	→	U172(isUniversal(V2))	(16)
    U41(tt,A)	→	A	(30)
    U111(tt)	→	false	(4)
    U182(tt)	→	tt	(19)
    U191(tt,V2)	→	U192(isBool(V2))	(20)
    U151(tt,V2)	→	U152(isBool(V2))	(12)
    U192(tt)	→	tt	(21)
    _xor_(x,y)	→	_xor_(y,x)	(69)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
    _and_(x,y)	→	_and_(y,x)	(67)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(false,A),ext)

    →

    _and_#(U31(isBool(A)),ext)

    (166)

    could be deleted.

    1.1.2.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
    [_and_(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
    [_xor_(x1, x2)]	=	3 + 1 · x2 + 1 · x1
    [U21(x1,...,x4)]	=	1 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x1 + 1 · x2 · x4 + 1 · x2 · x3
    [isBool(x1)]	=	2 · x1
    [U11(x1, x2)]	=	2 · x2
    [U181(x1, x2)]	=	1 · x1 + 3 · x1 · x2
    [tt]	=	2
    [U182(x1)]	=	2
    [isUniversal(x1)]	=	0
    [U202(x1)]	=	1 · x1
    [false]	=	2
    [U121(x1, x2)]	=	2 + 1 · x2
    [U111(x1)]	=	3
    [U161(x1, x2)]	=	2 · x2
    [U162(x1)]	=	1 · x1
    [U172(x1)]	=	2 · x1
    [U31(x1)]	=	2
    [true]	=	1
    [U41(x1, x2)]	=	1 + 1 · x2
    [U192(x1)]	=	1 · x1
    [U211(x1)]	=	2 · x1
    [U151(x1, x2)]	=	1 · x1
    [not_(x1)]	=	2 · x1
    [_isEqualTo_(x1, x2)]	=	0
    [U171(x1, x2)]	=	0
    [_or_(x1, x2)]	=	2 · x2
    [U191(x1, x2)]	=	2 · x2
    [U201(x1, x2)]	=	2 · x2
    [_isNotEqualTo_(x1, x2)]	=	0
    [_implies_(x1, x2)]	=	2 · x2
    [U152(x1)]	=	2
    [U22(x1,...,x4)]	=	3 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3
    [U23(x1,...,x4)]	=	3 + 1 · x4 + 1 · x3 + 2 · x2 + 1 · x2 · x4 + 1 · x2 · x3

    together with the usable rules

    U181(tt,V2)	→	U182(isUniversal(V2))	(18)
    U202(tt)	→	tt	(23)
    _xor_(false,A)	→	U121(isBool(A),A)	(51)
    _xor_(A,A)	→	U111(isBool(A))	(50)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
    U161(tt,V2)	→	U162(isBool(V2))	(14)
    U172(tt)	→	tt	(17)
    _and_(false,A)	→	U31(isBool(A))	(42)
    _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
    _and_(A,A)	→	U11(isBool(A),A)	(40)
    _and_(true,A)	→	U41(isBool(A),A)	(43)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
    U192(tt)	→	tt	(21)
    U211(tt)	→	tt	(25)
    isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
    isBool(true)	→	tt	(56)
    isBool(not_(V1))	→	U211(isBool(V1))	(63)
    isBool(false)	→	tt	(55)
    isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
    isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
    isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
    isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
    isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
    U121(tt,A)	→	A	(5)
    U191(tt,V2)	→	U192(isBool(V2))	(20)
    U151(tt,V2)	→	U152(isBool(V2))	(12)
    U182(tt)	→	tt	(19)
    U162(tt)	→	tt	(15)
    U41(tt,A)	→	A	(30)
    U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
    U11(tt,A)	→	A	(3)
    U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
    U152(tt)	→	tt	(13)
    U201(tt,V2)	→	U202(isBool(V2))	(22)
    U171(tt,V2)	→	U172(isUniversal(V2))	(16)
    U31(tt)	→	false	(29)
    U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
    U111(tt)	→	false	(4)
    _xor_(x,y)	→	_xor_(y,x)	(69)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
    _and_(x,y)	→	_and_(y,x)	(67)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(A,_xor_(B,C)),ext)

    →

    _and_#(U21(isBool(A),A,B,C),ext)

    (163)

    could be deleted.

    1.1.2.1.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	2 · x2 + 2 · x1 + 2 · x1 · x2
    [_and_(x1, x2)]	=	1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
    [U11(x1, x2)]	=	1 + 2 · x1 · x2
    [isBool(x1)]	=	2
    [U152(x1)]	=	1 · x1
    [tt]	=	2
    [U111(x1)]	=	0
    [false]	=	0
    [U171(x1, x2)]	=	0
    [U172(x1)]	=	1 · x1 · x1
    [isUniversal(x1)]	=	0
    [U181(x1, x2)]	=	2 · x1 + 1 · x1 · x2
    [U182(x1)]	=	2 · x1
    [U151(x1, x2)]	=	1 · x1
    [U191(x1, x2)]	=	1 · x1
    [U192(x1)]	=	2
    [U41(x1, x2)]	=	2 · x2
    [U21(x1,...,x4)]	=	3 + 2 · x3 + 2 · x2 + 2 · x2 · x4 + 1 · x1 · x4 + 1 · x1 · x2 + 1 · x1 · x2 · x3
    [U22(x1,...,x4)]	=	1 + 2 · x4 + 2 · x3 + 2 · x2 + 1 · x1 + 2 · x2 · x4 + 2 · x2 · x3 + 1 · x1 · x2
    [U31(x1)]	=	0
    [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
    [true]	=	1
    [U121(x1, x2)]	=	1 · x2
    [U201(x1, x2)]	=	2
    [U202(x1)]	=	1 · x1
    [U23(x1,...,x4)]	=	1 + 2 · x4 + 2 · x3 + 2 · x2 + 1 · x1 + 2 · x2 · x4 + 2 · x2 · x3 + 1 · x1 · x2
    [not_(x1)]	=	0
    [U211(x1)]	=	2
    [_isEqualTo_(x1, x2)]	=	0
    [_or_(x1, x2)]	=	0
    [_isNotEqualTo_(x1, x2)]	=	0
    [_implies_(x1, x2)]	=	0
    [U161(x1, x2)]	=	2
    [U162(x1)]	=	1 · x1

    together with the usable rules

    U152(tt)	→	tt	(13)
    U111(tt)	→	false	(4)
    U171(tt,V2)	→	U172(isUniversal(V2))	(16)
    U181(tt,V2)	→	U182(isUniversal(V2))	(18)
    U151(tt,V2)	→	U152(isBool(V2))	(12)
    U191(tt,V2)	→	U192(isBool(V2))	(20)
    U182(tt)	→	tt	(19)
    U41(tt,A)	→	A	(30)
    U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
    _and_(false,A)	→	U31(isBool(A))	(42)
    _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
    _and_(A,A)	→	U11(isBool(A),A)	(40)
    _and_(true,A)	→	U41(isBool(A),A)	(43)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
    U11(tt,A)	→	A	(3)
    U121(tt,A)	→	A	(5)
    U201(tt,V2)	→	U202(isBool(V2))	(22)
    _xor_(false,A)	→	U121(isBool(A),A)	(51)
    _xor_(A,A)	→	U111(isBool(A))	(50)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
    U192(tt)	→	tt	(21)
    U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
    U202(tt)	→	tt	(23)
    U31(tt)	→	false	(29)
    isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
    isBool(true)	→	tt	(56)
    isBool(not_(V1))	→	U211(isBool(V1))	(63)
    isBool(false)	→	tt	(55)
    isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
    isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
    isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
    isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
    isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
    U161(tt,V2)	→	U162(isBool(V2))	(14)
    U172(tt)	→	tt	(17)
    U162(tt)	→	tt	(15)
    U211(tt)	→	tt	(25)
    U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
    _and_(x,y)	→	_and_(y,x)	(67)
    _xor_(x,y)	→	_xor_(y,x)	(69)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(x,y),z)

    →

    _and_#(y,z)

    (79)

    could be deleted.

    1.1.2.1.1.1.1.1 AC Reduction Pair Processor with Usable Rules

    Using the non-linear polynomial interpretation over the naturals

    [_and_#(x1, x2)]	=	1 · x2 + 1 · x1 + 1 · x1 · x2
    [_and_(x1, x2)]	=	1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
    [U11(x1, x2)]	=	2 · x1 · x2
    [isBool(x1)]	=	2
    [U23(x1,...,x4)]	=	3 + 2 · x4 + 2 · x3 + 2 · x2 · x4 + 2 · x2 · x3 + 2 · x1 · x2
    [tt]	=	2
    [_xor_(x1, x2)]	=	1 + 1 · x2 + 1 · x1
    [false]	=	0
    [U121(x1, x2)]	=	1 · x2
    [U111(x1)]	=	0
    [U22(x1,...,x4)]	=	3 + 2 · x4 + 2 · x2 + 2 · x2 · x4 + 2 · x2 · x3 + 1 · x1 · x3 + 1 · x1 · x2
    [U211(x1)]	=	1 · x1
    [U162(x1)]	=	2
    [U201(x1, x2)]	=	2
    [U202(x1)]	=	2
    [U31(x1)]	=	0
    [U21(x1,...,x4)]	=	3 + 2 · x4 + 2 · x3 + 2 · x2 + 2 · x2 · x4 + 2 · x2 · x3 + 1 · x1 · x2
    [true]	=	1
    [U41(x1, x2)]	=	2 · x1 · x2
    [U171(x1, x2)]	=	2 · x1 + 1 · x1 · x2
    [U172(x1)]	=	2
    [isUniversal(x1)]	=	0
    [U152(x1)]	=	2
    [U192(x1)]	=	1 · x1
    [U191(x1, x2)]	=	2
    [U182(x1)]	=	2 · x1 · x1
    [U181(x1, x2)]	=	2 + 1 · x1
    [U151(x1, x2)]	=	2
    [not_(x1)]	=	0
    [_isEqualTo_(x1, x2)]	=	0
    [_or_(x1, x2)]	=	0
    [_isNotEqualTo_(x1, x2)]	=	0
    [_implies_(x1, x2)]	=	0
    [U161(x1, x2)]	=	2

    together with the usable rules

    U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
    _xor_(false,A)	→	U121(isBool(A),A)	(51)
    _xor_(A,A)	→	U111(isBool(A))	(50)
    _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
    _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
    U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
    U211(tt)	→	tt	(25)
    U162(tt)	→	tt	(15)
    U111(tt)	→	false	(4)
    U201(tt,V2)	→	U202(isBool(V2))	(22)
    U202(tt)	→	tt	(23)
    _and_(false,A)	→	U31(isBool(A))	(42)
    _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
    _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
    _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
    _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
    _and_(A,A)	→	U11(isBool(A),A)	(40)
    _and_(true,A)	→	U41(isBool(A),A)	(43)
    _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
    U171(tt,V2)	→	U172(isUniversal(V2))	(16)
    U31(tt)	→	false	(29)
    U152(tt)	→	tt	(13)
    U192(tt)	→	tt	(21)
    U11(tt,A)	→	A	(3)
    U41(tt,A)	→	A	(30)
    U191(tt,V2)	→	U192(isBool(V2))	(20)
    U121(tt,A)	→	A	(5)
    U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
    U172(tt)	→	tt	(17)
    U182(tt)	→	tt	(19)
    U181(tt,V2)	→	U182(isUniversal(V2))	(18)
    U151(tt,V2)	→	U152(isBool(V2))	(12)
    isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
    isBool(true)	→	tt	(56)
    isBool(not_(V1))	→	U211(isBool(V1))	(63)
    isBool(false)	→	tt	(55)
    isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
    isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
    isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
    isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
    isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
    U161(tt,V2)	→	U162(isBool(V2))	(14)
    _xor_(x,y)	→	_xor_(y,x)	(69)
    _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)
    _and_(_and_(x,y),z)	→	_and_(x,_and_(y,z))	(70)
    _and_(x,y)	→	_and_(y,x)	(67)

    (w.r.t. the implicit argument filter of the reduction pair), the pair

    _and_#(_and_(A,A),ext)

    →

    _and_#(U11(isBool(A),A),ext)

    (160)

    could be deleted.

    1.1.2.1.1.1.1.1.1 AC Dependency Pair Problem is trivial

    There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 3^rd component contains the pair

  _xor_#(_xor_(false,A),ext)	→	_xor_#(U121(isBool(A),A),ext)	(178)
  _xor_#(_xor_(A,A),ext)	→	_xor_#(U111(isBool(A)),ext)	(175)
  _xor_#(_xor_(x,y),z)	→	_xor_#(y,z)	(81)
  _xor_#(x,y)	→	_xor_#(y,x)	(75)
  _xor_#(_xor_(x,y),z)	→	_xor_#(x,_xor_(y,z))	(78)

  1.1.3 AC Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [_xor_#(x1, x2)]	=	3 · x1 + 3 · x2
  [_xor_(x1, x2)]	=	3 + 1 · x1 + 1 · x2
  [U111(x1)]	=	2
  [isBool(x1)]	=	0
  [false]	=	2
  [U121(x1, x2)]	=	1 · x2
  [U172(x1)]	=	3
  [tt]	=	0
  [U211(x1)]	=	3
  [_and_(x1, x2)]	=	0
  [U151(x1, x2)]	=	3 + 3 · x2
  [true]	=	0
  [not_(x1)]	=	0
  [_isEqualTo_(x1, x2)]	=	0
  [U171(x1, x2)]	=	3 + 3 · x2
  [isUniversal(x1)]	=	0
  [_or_(x1, x2)]	=	0
  [U191(x1, x2)]	=	3 + 3 · x2
  [U201(x1, x2)]	=	3 + 3 · x2
  [_isNotEqualTo_(x1, x2)]	=	0
  [U181(x1, x2)]	=	3 + 3 · x2
  [_implies_(x1, x2)]	=	0
  [U161(x1, x2)]	=	3 + 3 · x2
  [U182(x1)]	=	3
  [U152(x1)]	=	3
  [U192(x1)]	=	3
  [U202(x1)]	=	3
  [U162(x1)]	=	3

  together with the usable rules

  _xor_(false,A)	→	U121(isBool(A),A)	(51)
  _xor_(A,A)	→	U111(isBool(A))	(50)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
  U121(tt,A)	→	A	(5)
  U111(tt)	→	false	(4)
  _xor_(x,y)	→	_xor_(y,x)	(69)
  _xor_(_xor_(x,y),z)	→	_xor_(x,_xor_(y,z))	(72)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  _xor_#(_xor_(x,y),z)	→	_xor_#(y,z)	(81)
  _xor_#(_xor_(A,A),ext)	→	_xor_#(U111(isBool(A)),ext)	(175)
  _xor_#(_xor_(false,A),ext)	→	_xor_#(U121(isBool(A),A),ext)	(178)

  could be deleted.

  1.1.3.1 AC Dependency Pair Problem is trivial

  There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.
• The 4^th component contains the pair

  U151#(tt,V2)	→	isBool#(V2)	(94)
  isBool#(_and_(V1,V2))	→	U151#(isBool(V1),V2)	(146)
  isBool#(_and_(V1,V2))	→	isBool#(V1)	(147)
  isBool#(_implies_(V1,V2))	→	U161#(isBool(V1),V2)	(148)
  U161#(tt,V2)	→	isBool#(V2)	(96)
  isBool#(_implies_(V1,V2))	→	isBool#(V1)	(149)
  isBool#(_or_(V1,V2))	→	U191#(isBool(V1),V2)	(152)
  U191#(tt,V2)	→	isBool#(V2)	(100)
  isBool#(_or_(V1,V2))	→	isBool#(V1)	(153)
  isBool#(_xor_(V1,V2))	→	U201#(isBool(V1),V2)	(154)
  U201#(tt,V2)	→	isBool#(V2)	(102)
  isBool#(_xor_(V1,V2))	→	isBool#(V1)	(155)
  isBool#(not_(V1))	→	isBool#(V1)	(157)

  1.1.4 AC Monotonic Reduction Pair Processor with Usable Rules

  Using the linear polynomial interpretation over the naturals

  [U162(x1)]	=	1 · x1
  [tt]	=	0
  [isBool(x1)]	=	2 · x1
  [_isEqualTo_(x1, x2)]	=	2 + 3 · x1 + 3 · x2
  [U171(x1, x2)]	=	2 + 2 · x1 + 3 · x2
  [isUniversal(x1)]	=	2 · x1
  [U172(x1)]	=	1 · x1
  [U202(x1)]	=	1 · x1
  [_and_(x1, x2)]	=	2 + 3 · x1 + 3 · x2
  [U151(x1, x2)]	=	2 · x1 + 3 · x2
  [_or_(x1, x2)]	=	3 · x1 + 3 · x2
  [U191(x1, x2)]	=	2 · x1 + 3 · x2
  [U181(x1, x2)]	=	2 · x1 + 3 · x2
  [U182(x1)]	=	1 · x1
  [U161(x1, x2)]	=	2 · x1 + 3 · x2
  [true]	=	0
  [not_(x1)]	=	3 + 3 · x1
  [U211(x1)]	=	2 · x1
  [U152(x1)]	=	1 · x1
  [_xor_(x1, x2)]	=	1 + 3 · x1 + 3 · x2
  [U201(x1, x2)]	=	1 + 2 · x1 + 3 · x2
  [_isNotEqualTo_(x1, x2)]	=	1 + 3 · x1 + 3 · x2
  [U192(x1)]	=	1 · x1
  [_implies_(x1, x2)]	=	3 + 3 · x1 + 3 · x2
  [false]	=	0
  [U161#(x1, x2)]	=	2 · x1 + 3 · x2
  [isBool#(x1)]	=	2 · x1
  [U201#(x1, x2)]	=	2 · x1 + 3 · x2
  [U151#(x1, x2)]	=	2 · x1 + 3 · x2
  [U191#(x1, x2)]	=	2 · x1 + 3 · x2

  together with the usable rules

  U162(tt)	→	tt	(15)
  isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
  U171(tt,V2)	→	U172(isUniversal(V2))	(16)
  U202(tt)	→	tt	(23)
  isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
  isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
  U181(tt,V2)	→	U182(isUniversal(V2))	(18)
  U161(tt,V2)	→	U162(isBool(V2))	(14)
  isBool(true)	→	tt	(56)
  isBool(not_(V1))	→	U211(isBool(V1))	(63)
  U151(tt,V2)	→	U152(isBool(V2))	(12)
  U152(tt)	→	tt	(13)
  isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
  U172(tt)	→	tt	(17)
  isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
  U201(tt,V2)	→	U202(isBool(V2))	(22)
  U192(tt)	→	tt	(21)
  isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
  isBool(false)	→	tt	(55)
  U182(tt)	→	tt	(19)
  U211(tt)	→	tt	(25)
  U191(tt,V2)	→	U192(isBool(V2))	(20)

  (w.r.t. the implicit argument filter of the reduction pair), the pairs

  isBool#(_and_(V1,V2))	→	isBool#(V1)	(147)
  isBool#(_implies_(V1,V2))	→	U161#(isBool(V1),V2)	(148)
  isBool#(_xor_(V1,V2))	→	U201#(isBool(V1),V2)	(154)
  isBool#(not_(V1))	→	isBool#(V1)	(157)
  isBool#(_or_(V1,V2))	→	isBool#(V1)	(153)
  isBool#(_implies_(V1,V2))	→	isBool#(V1)	(149)
  isBool#(_or_(V1,V2))	→	U191#(isBool(V1),V2)	(152)
  isBool#(_and_(V1,V2))	→	U151#(isBool(V1),V2)	(146)
  isBool#(_xor_(V1,V2))	→	isBool#(V1)	(155)

  and the rules

  U101(tt,A,B)	→	U102(isBool(B),A,B)	(1)
  U102(tt,A,B)	→	_xor_(_and_(A,B),_xor_(A,B))	(2)
  U11(tt,A)	→	A	(3)
  U111(tt)	→	false	(4)
  U121(tt,A)	→	A	(5)
  U131(tt,B,U',U)	→	U132(isS(U'),B,U',U)	(6)
  U132(tt,B,U',U)	→	U133(isS(U),B,U')	(7)
  U133(tt,B,U')	→	U134(equal(_isNotEqualTo_(B,true),true),U')	(8)
  U134(tt,U')	→	U'	(9)
  U141(tt,U)	→	U142(isS(U),U)	(10)
  U142(tt,U)	→	U	(11)
  U171(tt,V2)	→	U172(isUniversal(V2))	(16)
  U201(tt,V2)	→	U202(isBool(V2))	(22)
  U21(tt,A,B,C)	→	U22(isBool(B),A,B,C)	(24)
  U22(tt,A,B,C)	→	U23(isBool(C),A,B,C)	(26)
  U221(tt,A)	→	_xor_(A,true)	(27)
  U23(tt,A,B,C)	→	_xor_(_and_(A,B),_and_(A,C))	(28)
  U31(tt)	→	false	(29)
  U41(tt,A)	→	A	(30)
  U51(tt,A,B)	→	U52(isBool(B),A,B)	(31)
  U52(tt,A,B)	→	not_(_xor_(A,_and_(A,B)))	(32)
  U61(tt,U',U)	→	U62(isS(U),U',U)	(33)
  U62(tt,U',U)	→	U63(equal(_isNotEqualTo_(U,U'),true))	(34)
  U63(tt)	→	false	(35)
  U71(tt)	→	true	(36)
  U81(tt,U',U)	→	U82(isS(U),U',U)	(37)
  U82(tt,U',U)	→	if_then_else_fi(_isEqualTo_(U,U'),false,true)	(38)
  U91(tt)	→	false	(39)
  _and_(A,A)	→	U11(isBool(A),A)	(40)
  _and_(A,_xor_(B,C))	→	U21(isBool(A),A,B,C)	(41)
  _and_(false,A)	→	U31(isBool(A))	(42)
  _and_(true,A)	→	U41(isBool(A),A)	(43)
  _implies_(A,B)	→	U51(isBool(A),A,B)	(44)
  _isEqualTo_(U,U')	→	U61(isS(U'),U',U)	(45)
  _isEqualTo_(U,U)	→	U71(isS(U))	(46)
  _isNotEqualTo_(U,U')	→	U81(isS(U'),U',U)	(47)
  _isNotEqualTo_(U,U)	→	U91(isS(U))	(48)
  _or_(A,B)	→	U101(isBool(A),A,B)	(49)
  _xor_(A,A)	→	U111(isBool(A))	(50)
  _xor_(false,A)	→	U121(isBool(A),A)	(51)
  equal(X,X)	→	tt	(52)
  if_then_else_fi(B,U,U')	→	U131(isBool(B),B,U',U)	(53)
  if_then_else_fi(true,U,U')	→	U141(isS(U'),U)	(54)
  isBool(false)	→	tt	(55)
  isBool(true)	→	tt	(56)
  isBool(_and_(V1,V2))	→	U151(isBool(V1),V2)	(57)
  isBool(_implies_(V1,V2))	→	U161(isBool(V1),V2)	(58)
  isBool(_isEqualTo_(V1,V2))	→	U171(isUniversal(V1),V2)	(59)
  isBool(_isNotEqualTo_(V1,V2))	→	U181(isUniversal(V1),V2)	(60)
  isBool(_or_(V1,V2))	→	U191(isBool(V1),V2)	(61)
  isBool(_xor_(V1,V2))	→	U201(isBool(V1),V2)	(62)
  isBool(not_(V1))	→	U211(isBool(V1))	(63)
  not_(A)	→	U221(isBool(A),A)	(64)
  not_(false)	→	true	(65)
  not_(true)	→	false	(66)
  _and_(_and_(A,A),ext)	→	_and_(U11(isBool(A),A),ext)	(181)
  _and_(_and_(A,_xor_(B,C)),ext)	→	_and_(U21(isBool(A),A,B,C),ext)	(182)
  _and_(_and_(false,A),ext)	→	_and_(U31(isBool(A)),ext)	(183)
  _and_(_and_(true,A),ext)	→	_and_(U41(isBool(A),A),ext)	(184)
  _or_(_or_(A,B),ext)	→	_or_(U101(isBool(A),A,B),ext)	(185)
  _xor_(_xor_(A,A),ext)	→	_xor_(U111(isBool(A)),ext)	(186)
  _xor_(_xor_(false,A),ext)	→	_xor_(U121(isBool(A),A),ext)	(187)

  could be deleted.

  1.1.4.1 Dependency Graph Processor

  The dependency pairs are split into 0 components.