MAYBE Time: 14.065 Problem: Equations: _xor_AC(_xor_AC(x8,x9),x10) -> _xor_AC(x8,_xor_AC(x9,x10)) _xor_AC(x8,x9) -> _xor_AC(x9,x8) _and_AC(_and_AC(x8,x9),x10) -> _and_AC(x8,_and_AC(x9,x10)) _and_AC(x8,x9) -> _and_AC(x9,x8) _or_AC(_or_AC(x8,x9),x10) -> _or_AC(x8,_or_AC(x9,x10)) _or_AC(x8,x9) -> _or_AC(x9,x8) _xor_AC(x8,_xor_AC(x9,x10)) -> _xor_AC(_xor_AC(x8,x9),x10) _xor_AC(x9,x8) -> _xor_AC(x8,x9) _and_AC(x8,_and_AC(x9,x10)) -> _and_AC(_and_AC(x8,x9),x10) _and_AC(x9,x8) -> _and_AC(x8,x9) _or_AC(x8,_or_AC(x9,x10)) -> _or_AC(_or_AC(x8,x9),x10) _or_AC(x9,x8) -> _or_AC(x8,x9) TRS: U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(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(),V1,V2) -> U152(isBool(V1),V2) U152(tt(),V2) -> U153(isBool(V2)) U153(tt()) -> tt() U161(tt(),V1,V2) -> U162(isBool(V1),V2) U162(tt(),V2) -> U163(isBool(V2)) U163(tt()) -> tt() U171(tt(),V1,V2) -> U172(isBool(V1),V2) U172(tt(),V2) -> U173(isBool(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isBool(V1),V2) U182(tt(),V2) -> U183(isBool(V2)) U183(tt()) -> tt() U191(tt(),V1) -> U192(isBool(V1)) U192(tt()) -> tt() U201(tt(),A) -> _xor_AC(A,true()) U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C)) U31(tt()) -> false() U41(tt(),A) -> A U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(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_AC(A,A) -> U11(and(isBool(A),isBoolKind(A)),A) _and_AC(A,_xor_AC(B,C)) -> U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_AC(false(),A) -> U31(and(isBool(A),isBoolKind(A))) _and_AC(true(),A) -> U41(and(isBool(A),isBoolKind(A)),A) _implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U))) _isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U))) _or_AC(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _xor_AC(A,A) -> U111(and(isBool(A),isBoolKind(A))) _xor_AC(false(),A) -> U121(and(isBool(A),isBoolKind(A)),A) and(tt(),X) -> X equal(X,X) -> tt() if_then_else_fi(B,U,U') -> U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))),B,U') if_then_else_fi(true(),U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U) isBool(false()) -> tt() isBool(true()) -> tt() isBool(_and_AC(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_isEqualTo_(V1,V2)) -> tt() isBool(_isNotEqualTo_(V1,V2)) -> tt() isBool(_or_AC(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_xor_AC(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(not_(V1)) -> U191(isBoolKind(V1),V1) isBoolKind(false()) -> tt() isBoolKind(true()) -> tt() isBoolKind(_and_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_isEqualTo_(V1,V2)) -> tt() isBoolKind(_isNotEqualTo_(V1,V2)) -> tt() isBoolKind(_or_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_xor_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(not_(V1)) -> isBoolKind(V1) not_(A) -> U201(and(isBool(A),isBoolKind(A)),A) not_(false()) -> true() not_(true()) -> false() Proof: DP Processor: Equations#: _xor_{AC,#}(_xor_AC(x8,x9),x10) -> _xor_{AC,#}(x8,_xor_AC(x9,x10)) _xor_{AC,#}(x8,x9) -> _xor_{AC,#}(x9,x8) _and_{AC,#}(_and_AC(x8,x9),x10) -> _and_{AC,#}(x8,_and_AC(x9,x10)) _and_{AC,#}(x8,x9) -> _and_{AC,#}(x9,x8) _or_{AC,#}(_or_AC(x8,x9),x10) -> _or_{AC,#}(x8,_or_AC(x9,x10)) _or_{AC,#}(x8,x9) -> _or_{AC,#}(x9,x8) _xor_{AC,#}(x8,_xor_AC(x9,x10)) -> _xor_{AC,#}(_xor_AC(x8,x9),x10) _xor_{AC,#}(x9,x8) -> _xor_{AC,#}(x8,x9) _and_{AC,#}(x8,_and_AC(x9,x10)) -> _and_{AC,#}(_and_AC(x8,x9),x10) _and_{AC,#}(x9,x8) -> _and_{AC,#}(x8,x9) _or_{AC,#}(x8,_or_AC(x9,x10)) -> _or_{AC,#}(_or_AC(x8,x9),x10) _or_{AC,#}(x9,x8) -> _or_{AC,#}(x8,x9) DPs: U101#(tt(),A,B) -> _xor_{AC,#}(A,B) U101#(tt(),A,B) -> _and_{AC,#}(A,B) U101#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B)) U131#(tt(),B,U') -> _isNotEqualTo_#(B,true()) U131#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true()) U131#(tt(),B,U') -> U132#(equal(_isNotEqualTo_(B,true()),true()),U') U151#(tt(),V1,V2) -> isBool#(V1) U151#(tt(),V1,V2) -> U152#(isBool(V1),V2) U152#(tt(),V2) -> isBool#(V2) U152#(tt(),V2) -> U153#(isBool(V2)) U161#(tt(),V1,V2) -> isBool#(V1) U161#(tt(),V1,V2) -> U162#(isBool(V1),V2) U162#(tt(),V2) -> isBool#(V2) U162#(tt(),V2) -> U163#(isBool(V2)) U171#(tt(),V1,V2) -> isBool#(V1) U171#(tt(),V1,V2) -> U172#(isBool(V1),V2) U172#(tt(),V2) -> isBool#(V2) U172#(tt(),V2) -> U173#(isBool(V2)) U181#(tt(),V1,V2) -> isBool#(V1) U181#(tt(),V1,V2) -> U182#(isBool(V1),V2) U182#(tt(),V2) -> isBool#(V2) U182#(tt(),V2) -> U183#(isBool(V2)) U191#(tt(),V1) -> isBool#(V1) U191#(tt(),V1) -> U192#(isBool(V1)) U201#(tt(),A) -> _xor_{AC,#}(A,true()) U21#(tt(),A,B,C) -> _and_{AC,#}(A,C) U21#(tt(),A,B,C) -> _and_{AC,#}(A,B) U21#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C)) U51#(tt(),A,B) -> _and_{AC,#}(A,B) U51#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B)) U51#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B))) U61#(tt(),U',U) -> _isNotEqualTo_#(U,U') U61#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true()) U61#(tt(),U',U) -> U62#(equal(_isNotEqualTo_(U,U'),true())) U81#(tt(),U',U) -> _isEqualTo_#(U,U') U81#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true()) _and_{AC,#}(A,A) -> isBoolKind#(A) _and_{AC,#}(A,A) -> isBool#(A) _and_{AC,#}(A,A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(A,A) -> U11#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(C) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(C) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(C),isBoolKind(C)) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(B) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(B) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(B),isBoolKind(B)) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C))) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(A) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C)))) _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_{AC,#}(false(),A) -> isBoolKind#(A) _and_{AC,#}(false(),A) -> isBool#(A) _and_{AC,#}(false(),A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(false(),A) -> U31#(and(isBool(A),isBoolKind(A))) _and_{AC,#}(true(),A) -> isBoolKind#(A) _and_{AC,#}(true(),A) -> isBool#(A) _and_{AC,#}(true(),A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(true(),A) -> U41#(and(isBool(A),isBoolKind(A)),A) _implies_#(A,B) -> isBoolKind#(B) _implies_#(A,B) -> isBool#(B) _implies_#(A,B) -> and#(isBool(B),isBoolKind(B)) _implies_#(A,B) -> isBoolKind#(A) _implies_#(A,B) -> isBool#(A) _implies_#(A,B) -> and#(isBool(A),isBoolKind(A)) _implies_#(A,B) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _implies_#(A,B) -> U51#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _isEqualTo_#(U,U') -> and#(isS(U),isSKind(U)) _isEqualTo_#(U,U') -> and#(isS(U'),isSKind(U')) _isEqualTo_#(U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) _isEqualTo_#(U,U') -> U61#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isEqualTo_#(U,U) -> and#(isS(U),isSKind(U)) _isEqualTo_#(U,U) -> U71#(and(isS(U),isSKind(U))) _isNotEqualTo_#(U,U') -> and#(isS(U),isSKind(U)) _isNotEqualTo_#(U,U') -> and#(isS(U'),isSKind(U')) _isNotEqualTo_#(U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) _isNotEqualTo_#(U,U') -> U81#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isNotEqualTo_#(U,U) -> and#(isS(U),isSKind(U)) _isNotEqualTo_#(U,U) -> U91#(and(isS(U),isSKind(U))) _or_{AC,#}(A,B) -> isBoolKind#(B) _or_{AC,#}(A,B) -> isBool#(B) _or_{AC,#}(A,B) -> and#(isBool(B),isBoolKind(B)) _or_{AC,#}(A,B) -> isBoolKind#(A) _or_{AC,#}(A,B) -> isBool#(A) _or_{AC,#}(A,B) -> and#(isBool(A),isBoolKind(A)) _or_{AC,#}(A,B) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _or_{AC,#}(A,B) -> U101#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _xor_{AC,#}(A,A) -> isBoolKind#(A) _xor_{AC,#}(A,A) -> isBool#(A) _xor_{AC,#}(A,A) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(A,A) -> U111#(and(isBool(A),isBoolKind(A))) _xor_{AC,#}(false(),A) -> isBoolKind#(A) _xor_{AC,#}(false(),A) -> isBool#(A) _xor_{AC,#}(false(),A) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(false(),A) -> U121#(and(isBool(A),isBoolKind(A)),A) if_then_else_fi#(B,U,U') -> and#(isS(U),isSKind(U)) if_then_else_fi#(B,U,U') -> and#(isS(U'),isSKind(U')) if_then_else_fi#(B,U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) if_then_else_fi#(B,U,U') -> isBoolKind#(B) if_then_else_fi#(B,U,U') -> isBool#(B) if_then_else_fi#(B,U,U') -> and#(isBool(B),isBoolKind(B)) if_then_else_fi#(B,U,U') -> and#(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))) if_then_else_fi#(B,U,U') -> U131#(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))), B,U') if_then_else_fi#(true(),U,U') -> and#(isS(U),isSKind(U)) if_then_else_fi#(true(),U,U') -> and#(isS(U'),isSKind(U')) if_then_else_fi#(true(),U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) if_then_else_fi#(true(),U,U') -> U141#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U) isBool#(_and_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_and_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_and_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_and_AC(V1,V2)) -> U151#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_implies_(V1,V2)) -> isBoolKind#(V2) isBool#(_implies_(V1,V2)) -> isBoolKind#(V1) isBool#(_implies_(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_implies_(V1,V2)) -> U161#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_or_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_or_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_or_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_or_AC(V1,V2)) -> U171#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_xor_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_xor_AC(V1,V2)) -> U181#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(not_(V1)) -> isBoolKind#(V1) isBool#(not_(V1)) -> U191#(isBoolKind(V1),V1) isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_and_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_implies_(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_or_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_xor_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(not_(V1)) -> isBoolKind#(V1) not_#(A) -> isBoolKind#(A) not_#(A) -> isBool#(A) not_#(A) -> and#(isBool(A),isBoolKind(A)) not_#(A) -> U201#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x11,_and_AC(A,A)) -> isBoolKind#(A) _and_{AC,#}(x11,_and_AC(A,A)) -> isBool#(A) _and_{AC,#}(x11,_and_AC(A,A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x11,_and_AC(A,A)) -> U11#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x11,_and_AC(A,A)) -> _and_{AC,#}(x11,U11(and(isBool(A),isBoolKind(A)),A)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(C),isBoolKind(C)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(B) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(B) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(B),isBoolKind(B)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C))) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(A) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(A) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C)))) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x12,U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C)) _and_{AC,#}(x13,_and_AC(false(),A)) -> isBoolKind#(A) _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A) _and_{AC,#}(x13,_and_AC(false(),A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(and(isBool(A),isBoolKind(A))) _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(and(isBool(A),isBoolKind(A)))) _and_{AC,#}(x14,_and_AC(true(),A)) -> isBoolKind#(A) _and_{AC,#}(x14,_and_AC(true(),A)) -> isBool#(A) _and_{AC,#}(x14,_and_AC(true(),A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x14,_and_AC(true(),A)) -> U41#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x14,_and_AC(true(),A)) -> _and_{AC,#}(x14,U41(and(isBool(A),isBoolKind(A)),A)) _or_{AC,#}(x15,_or_AC(A,B)) -> isBoolKind#(B) _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(B) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(B),isBoolKind(B)) _or_{AC,#}(x15,_or_AC(A,B)) -> isBoolKind#(A) _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(A) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(A),isBoolKind(A)) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)) _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBoolKind#(A) _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A) _xor_{AC,#}(x16,_xor_AC(A,A)) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(and(isBool(A),isBoolKind(A))) _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(and(isBool(A),isBoolKind(A)))) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBoolKind#(A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBool#(A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> U121#(and(isBool(A),isBoolKind(A)),A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> _xor_{AC,#}(x17,U121(and(isBool(A),isBoolKind(A)),A)) Equations: _xor_AC(_xor_AC(x8,x9),x10) -> _xor_AC(x8,_xor_AC(x9,x10)) _xor_AC(x8,x9) -> _xor_AC(x9,x8) _and_AC(_and_AC(x8,x9),x10) -> _and_AC(x8,_and_AC(x9,x10)) _and_AC(x8,x9) -> _and_AC(x9,x8) _or_AC(_or_AC(x8,x9),x10) -> _or_AC(x8,_or_AC(x9,x10)) _or_AC(x8,x9) -> _or_AC(x9,x8) _xor_AC(x8,_xor_AC(x9,x10)) -> _xor_AC(_xor_AC(x8,x9),x10) _xor_AC(x9,x8) -> _xor_AC(x8,x9) _and_AC(x8,_and_AC(x9,x10)) -> _and_AC(_and_AC(x8,x9),x10) _and_AC(x9,x8) -> _and_AC(x8,x9) _or_AC(x8,_or_AC(x9,x10)) -> _or_AC(_or_AC(x8,x9),x10) _or_AC(x9,x8) -> _or_AC(x8,x9) TRS: U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(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(),V1,V2) -> U152(isBool(V1),V2) U152(tt(),V2) -> U153(isBool(V2)) U153(tt()) -> tt() U161(tt(),V1,V2) -> U162(isBool(V1),V2) U162(tt(),V2) -> U163(isBool(V2)) U163(tt()) -> tt() U171(tt(),V1,V2) -> U172(isBool(V1),V2) U172(tt(),V2) -> U173(isBool(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isBool(V1),V2) U182(tt(),V2) -> U183(isBool(V2)) U183(tt()) -> tt() U191(tt(),V1) -> U192(isBool(V1)) U192(tt()) -> tt() U201(tt(),A) -> _xor_AC(A,true()) U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C)) U31(tt()) -> false() U41(tt(),A) -> A U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(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_AC(A,A) -> U11(and(isBool(A),isBoolKind(A)),A) _and_AC(A,_xor_AC(B,C)) -> U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_AC(false(),A) -> U31(and(isBool(A),isBoolKind(A))) _and_AC(true(),A) -> U41(and(isBool(A),isBoolKind(A)),A) _implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U))) _isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U))) _or_AC(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _xor_AC(A,A) -> U111(and(isBool(A),isBoolKind(A))) _xor_AC(false(),A) -> U121(and(isBool(A),isBoolKind(A)),A) and(tt(),X) -> X equal(X,X) -> tt() if_then_else_fi(B,U,U') -> U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))),B,U') if_then_else_fi(true(),U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U) isBool(false()) -> tt() isBool(true()) -> tt() isBool(_and_AC(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_isEqualTo_(V1,V2)) -> tt() isBool(_isNotEqualTo_(V1,V2)) -> tt() isBool(_or_AC(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_xor_AC(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(not_(V1)) -> U191(isBoolKind(V1),V1) isBoolKind(false()) -> tt() isBoolKind(true()) -> tt() isBoolKind(_and_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_isEqualTo_(V1,V2)) -> tt() isBoolKind(_isNotEqualTo_(V1,V2)) -> tt() isBoolKind(_or_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_xor_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(not_(V1)) -> isBoolKind(V1) not_(A) -> U201(and(isBool(A),isBoolKind(A)),A) not_(false()) -> true() not_(true()) -> false() S: _xor_{AC,#}(_xor_AC(x18,x19),x20) -> _xor_{AC,#}(x18,x19) _xor_{AC,#}(x18,_xor_AC(x19,x20)) -> _xor_{AC,#}(x19,x20) _and_{AC,#}(_and_AC(x18,x19),x20) -> _and_{AC,#}(x18,x19) _and_{AC,#}(x18,_and_AC(x19,x20)) -> _and_{AC,#}(x19,x20) _or_{AC,#}(_or_AC(x18,x19),x20) -> _or_{AC,#}(x18,x19) _or_{AC,#}(x18,_or_AC(x19,x20)) -> _or_{AC,#}(x19,x20) AC-EDG Processor: Equations#: _xor_{AC,#}(_xor_AC(x8,x9),x10) -> _xor_{AC,#}(x8,_xor_AC(x9,x10)) _xor_{AC,#}(x8,x9) -> _xor_{AC,#}(x9,x8) _and_{AC,#}(_and_AC(x8,x9),x10) -> _and_{AC,#}(x8,_and_AC(x9,x10)) _and_{AC,#}(x8,x9) -> _and_{AC,#}(x9,x8) _or_{AC,#}(_or_AC(x8,x9),x10) -> _or_{AC,#}(x8,_or_AC(x9,x10)) _or_{AC,#}(x8,x9) -> _or_{AC,#}(x9,x8) _xor_{AC,#}(x8,_xor_AC(x9,x10)) -> _xor_{AC,#}(_xor_AC(x8,x9),x10) _xor_{AC,#}(x9,x8) -> _xor_{AC,#}(x8,x9) _and_{AC,#}(x8,_and_AC(x9,x10)) -> _and_{AC,#}(_and_AC(x8,x9),x10) _and_{AC,#}(x9,x8) -> _and_{AC,#}(x8,x9) _or_{AC,#}(x8,_or_AC(x9,x10)) -> _or_{AC,#}(_or_AC(x8,x9),x10) _or_{AC,#}(x9,x8) -> _or_{AC,#}(x8,x9) DPs: U101#(tt(),A,B) -> _xor_{AC,#}(A,B) U101#(tt(),A,B) -> _and_{AC,#}(A,B) U101#(tt(),A,B) -> _xor_{AC,#}(_and_AC(A,B),_xor_AC(A,B)) U131#(tt(),B,U') -> _isNotEqualTo_#(B,true()) U131#(tt(),B,U') -> equal#(_isNotEqualTo_(B,true()),true()) U131#(tt(),B,U') -> U132#(equal(_isNotEqualTo_(B,true()),true()),U') U151#(tt(),V1,V2) -> isBool#(V1) U151#(tt(),V1,V2) -> U152#(isBool(V1),V2) U152#(tt(),V2) -> isBool#(V2) U152#(tt(),V2) -> U153#(isBool(V2)) U161#(tt(),V1,V2) -> isBool#(V1) U161#(tt(),V1,V2) -> U162#(isBool(V1),V2) U162#(tt(),V2) -> isBool#(V2) U162#(tt(),V2) -> U163#(isBool(V2)) U171#(tt(),V1,V2) -> isBool#(V1) U171#(tt(),V1,V2) -> U172#(isBool(V1),V2) U172#(tt(),V2) -> isBool#(V2) U172#(tt(),V2) -> U173#(isBool(V2)) U181#(tt(),V1,V2) -> isBool#(V1) U181#(tt(),V1,V2) -> U182#(isBool(V1),V2) U182#(tt(),V2) -> isBool#(V2) U182#(tt(),V2) -> U183#(isBool(V2)) U191#(tt(),V1) -> isBool#(V1) U191#(tt(),V1) -> U192#(isBool(V1)) U201#(tt(),A) -> _xor_{AC,#}(A,true()) U21#(tt(),A,B,C) -> _and_{AC,#}(A,C) U21#(tt(),A,B,C) -> _and_{AC,#}(A,B) U21#(tt(),A,B,C) -> _xor_{AC,#}(_and_AC(A,B),_and_AC(A,C)) U51#(tt(),A,B) -> _and_{AC,#}(A,B) U51#(tt(),A,B) -> _xor_{AC,#}(A,_and_AC(A,B)) U51#(tt(),A,B) -> not_#(_xor_AC(A,_and_AC(A,B))) U61#(tt(),U',U) -> _isNotEqualTo_#(U,U') U61#(tt(),U',U) -> equal#(_isNotEqualTo_(U,U'),true()) U61#(tt(),U',U) -> U62#(equal(_isNotEqualTo_(U,U'),true())) U81#(tt(),U',U) -> _isEqualTo_#(U,U') U81#(tt(),U',U) -> if_then_else_fi#(_isEqualTo_(U,U'),false(),true()) _and_{AC,#}(A,A) -> isBoolKind#(A) _and_{AC,#}(A,A) -> isBool#(A) _and_{AC,#}(A,A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(A,A) -> U11#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(C) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(C) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(C),isBoolKind(C)) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(B) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(B) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(B),isBoolKind(B)) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C))) _and_{AC,#}(A,_xor_AC(B,C)) -> isBoolKind#(A) _and_{AC,#}(A,_xor_AC(B,C)) -> isBool#(A) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(A,_xor_AC(B,C)) -> and#(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C)))) _and_{AC,#}(A,_xor_AC(B,C)) -> U21#(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_{AC,#}(false(),A) -> isBoolKind#(A) _and_{AC,#}(false(),A) -> isBool#(A) _and_{AC,#}(false(),A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(false(),A) -> U31#(and(isBool(A),isBoolKind(A))) _and_{AC,#}(true(),A) -> isBoolKind#(A) _and_{AC,#}(true(),A) -> isBool#(A) _and_{AC,#}(true(),A) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(true(),A) -> U41#(and(isBool(A),isBoolKind(A)),A) _implies_#(A,B) -> isBoolKind#(B) _implies_#(A,B) -> isBool#(B) _implies_#(A,B) -> and#(isBool(B),isBoolKind(B)) _implies_#(A,B) -> isBoolKind#(A) _implies_#(A,B) -> isBool#(A) _implies_#(A,B) -> and#(isBool(A),isBoolKind(A)) _implies_#(A,B) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _implies_#(A,B) -> U51#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _isEqualTo_#(U,U') -> and#(isS(U),isSKind(U)) _isEqualTo_#(U,U') -> and#(isS(U'),isSKind(U')) _isEqualTo_#(U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) _isEqualTo_#(U,U') -> U61#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isEqualTo_#(U,U) -> and#(isS(U),isSKind(U)) _isEqualTo_#(U,U) -> U71#(and(isS(U),isSKind(U))) _isNotEqualTo_#(U,U') -> and#(isS(U),isSKind(U)) _isNotEqualTo_#(U,U') -> and#(isS(U'),isSKind(U')) _isNotEqualTo_#(U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) _isNotEqualTo_#(U,U') -> U81#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isNotEqualTo_#(U,U) -> and#(isS(U),isSKind(U)) _isNotEqualTo_#(U,U) -> U91#(and(isS(U),isSKind(U))) _or_{AC,#}(A,B) -> isBoolKind#(B) _or_{AC,#}(A,B) -> isBool#(B) _or_{AC,#}(A,B) -> and#(isBool(B),isBoolKind(B)) _or_{AC,#}(A,B) -> isBoolKind#(A) _or_{AC,#}(A,B) -> isBool#(A) _or_{AC,#}(A,B) -> and#(isBool(A),isBoolKind(A)) _or_{AC,#}(A,B) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _or_{AC,#}(A,B) -> U101#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _xor_{AC,#}(A,A) -> isBoolKind#(A) _xor_{AC,#}(A,A) -> isBool#(A) _xor_{AC,#}(A,A) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(A,A) -> U111#(and(isBool(A),isBoolKind(A))) _xor_{AC,#}(false(),A) -> isBoolKind#(A) _xor_{AC,#}(false(),A) -> isBool#(A) _xor_{AC,#}(false(),A) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(false(),A) -> U121#(and(isBool(A),isBoolKind(A)),A) if_then_else_fi#(B,U,U') -> and#(isS(U),isSKind(U)) if_then_else_fi#(B,U,U') -> and#(isS(U'),isSKind(U')) if_then_else_fi#(B,U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) if_then_else_fi#(B,U,U') -> isBoolKind#(B) if_then_else_fi#(B,U,U') -> isBool#(B) if_then_else_fi#(B,U,U') -> and#(isBool(B),isBoolKind(B)) if_then_else_fi#(B,U,U') -> and#(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))) if_then_else_fi#(B,U,U') -> U131#(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))), B,U') if_then_else_fi#(true(),U,U') -> and#(isS(U),isSKind(U)) if_then_else_fi#(true(),U,U') -> and#(isS(U'),isSKind(U')) if_then_else_fi#(true(),U,U') -> and#(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))) if_then_else_fi#(true(),U,U') -> U141#(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U) isBool#(_and_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_and_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_and_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_and_AC(V1,V2)) -> U151#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_implies_(V1,V2)) -> isBoolKind#(V2) isBool#(_implies_(V1,V2)) -> isBoolKind#(V1) isBool#(_implies_(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_implies_(V1,V2)) -> U161#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_or_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_or_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_or_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_or_AC(V1,V2)) -> U171#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V2) isBool#(_xor_AC(V1,V2)) -> isBoolKind#(V1) isBool#(_xor_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBool#(_xor_AC(V1,V2)) -> U181#(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool#(not_(V1)) -> isBoolKind#(V1) isBool#(not_(V1)) -> U191#(isBoolKind(V1),V1) isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_and_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_and_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_implies_(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_implies_(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_or_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_or_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V2) isBoolKind#(_xor_AC(V1,V2)) -> isBoolKind#(V1) isBoolKind#(_xor_AC(V1,V2)) -> and#(isBoolKind(V1),isBoolKind(V2)) isBoolKind#(not_(V1)) -> isBoolKind#(V1) not_#(A) -> isBoolKind#(A) not_#(A) -> isBool#(A) not_#(A) -> and#(isBool(A),isBoolKind(A)) not_#(A) -> U201#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x11,_and_AC(A,A)) -> isBoolKind#(A) _and_{AC,#}(x11,_and_AC(A,A)) -> isBool#(A) _and_{AC,#}(x11,_and_AC(A,A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x11,_and_AC(A,A)) -> U11#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x11,_and_AC(A,A)) -> _and_{AC,#}(x11,U11(and(isBool(A),isBoolKind(A)),A)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(C),isBoolKind(C)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(B) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(B) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(B),isBoolKind(B)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C))) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBoolKind#(A) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> isBool#(A) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> and#(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)),and(isBool(C),isBoolKind(C)))) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> U21#(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_{AC,#}(x12,_and_AC(A,_xor_AC(B,C))) -> _and_{AC,#}(x12,U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C)) _and_{AC,#}(x13,_and_AC(false(),A)) -> isBoolKind#(A) _and_{AC,#}(x13,_and_AC(false(),A)) -> isBool#(A) _and_{AC,#}(x13,_and_AC(false(),A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x13,_and_AC(false(),A)) -> U31#(and(isBool(A),isBoolKind(A))) _and_{AC,#}(x13,_and_AC(false(),A)) -> _and_{AC,#}(x13,U31(and(isBool(A),isBoolKind(A)))) _and_{AC,#}(x14,_and_AC(true(),A)) -> isBoolKind#(A) _and_{AC,#}(x14,_and_AC(true(),A)) -> isBool#(A) _and_{AC,#}(x14,_and_AC(true(),A)) -> and#(isBool(A),isBoolKind(A)) _and_{AC,#}(x14,_and_AC(true(),A)) -> U41#(and(isBool(A),isBoolKind(A)),A) _and_{AC,#}(x14,_and_AC(true(),A)) -> _and_{AC,#}(x14,U41(and(isBool(A),isBoolKind(A)),A)) _or_{AC,#}(x15,_or_AC(A,B)) -> isBoolKind#(B) _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(B) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(B),isBoolKind(B)) _or_{AC,#}(x15,_or_AC(A,B)) -> isBoolKind#(A) _or_{AC,#}(x15,_or_AC(A,B)) -> isBool#(A) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(isBool(A),isBoolKind(A)) _or_{AC,#}(x15,_or_AC(A,B)) -> and#(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))) _or_{AC,#}(x15,_or_AC(A,B)) -> U101#(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _or_{AC,#}(x15,_or_AC(A,B)) -> _or_{AC,#}(x15,U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B)) _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBoolKind#(A) _xor_{AC,#}(x16,_xor_AC(A,A)) -> isBool#(A) _xor_{AC,#}(x16,_xor_AC(A,A)) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(x16,_xor_AC(A,A)) -> U111#(and(isBool(A),isBoolKind(A))) _xor_{AC,#}(x16,_xor_AC(A,A)) -> _xor_{AC,#}(x16,U111(and(isBool(A),isBoolKind(A)))) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBoolKind#(A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> isBool#(A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> and#(isBool(A),isBoolKind(A)) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> U121#(and(isBool(A),isBoolKind(A)),A) _xor_{AC,#}(x17,_xor_AC(false(),A)) -> _xor_{AC,#}(x17,U121(and(isBool(A),isBoolKind(A)),A)) Equations: _xor_AC(_xor_AC(x8,x9),x10) -> _xor_AC(x8,_xor_AC(x9,x10)) _xor_AC(x8,x9) -> _xor_AC(x9,x8) _and_AC(_and_AC(x8,x9),x10) -> _and_AC(x8,_and_AC(x9,x10)) _and_AC(x8,x9) -> _and_AC(x9,x8) _or_AC(_or_AC(x8,x9),x10) -> _or_AC(x8,_or_AC(x9,x10)) _or_AC(x8,x9) -> _or_AC(x9,x8) _xor_AC(x8,_xor_AC(x9,x10)) -> _xor_AC(_xor_AC(x8,x9),x10) _xor_AC(x9,x8) -> _xor_AC(x8,x9) _and_AC(x8,_and_AC(x9,x10)) -> _and_AC(_and_AC(x8,x9),x10) _and_AC(x9,x8) -> _and_AC(x8,x9) _or_AC(x8,_or_AC(x9,x10)) -> _or_AC(_or_AC(x8,x9),x10) _or_AC(x9,x8) -> _or_AC(x8,x9) TRS: U101(tt(),A,B) -> _xor_AC(_and_AC(A,B),_xor_AC(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(),V1,V2) -> U152(isBool(V1),V2) U152(tt(),V2) -> U153(isBool(V2)) U153(tt()) -> tt() U161(tt(),V1,V2) -> U162(isBool(V1),V2) U162(tt(),V2) -> U163(isBool(V2)) U163(tt()) -> tt() U171(tt(),V1,V2) -> U172(isBool(V1),V2) U172(tt(),V2) -> U173(isBool(V2)) U173(tt()) -> tt() U181(tt(),V1,V2) -> U182(isBool(V1),V2) U182(tt(),V2) -> U183(isBool(V2)) U183(tt()) -> tt() U191(tt(),V1) -> U192(isBool(V1)) U192(tt()) -> tt() U201(tt(),A) -> _xor_AC(A,true()) U21(tt(),A,B,C) -> _xor_AC(_and_AC(A,B),_and_AC(A,C)) U31(tt()) -> false() U41(tt(),A) -> A U51(tt(),A,B) -> not_(_xor_AC(A,_and_AC(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_AC(A,A) -> U11(and(isBool(A),isBoolKind(A)),A) _and_AC(A,_xor_AC(B,C)) -> U21(and(and(isBool(A),isBoolKind(A)),and(and(isBool(B),isBoolKind(B)), and(isBool(C),isBoolKind(C)))), A,B,C) _and_AC(false(),A) -> U31(and(isBool(A),isBoolKind(A))) _and_AC(true(),A) -> U41(and(isBool(A),isBoolKind(A)),A) _implies_(A,B) -> U51(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _isEqualTo_(U,U') -> U61(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isEqualTo_(U,U) -> U71(and(isS(U),isSKind(U))) _isNotEqualTo_(U,U') -> U81(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U',U) _isNotEqualTo_(U,U) -> U91(and(isS(U),isSKind(U))) _or_AC(A,B) -> U101(and(and(isBool(A),isBoolKind(A)),and(isBool(B),isBoolKind(B))),A,B) _xor_AC(A,A) -> U111(and(isBool(A),isBoolKind(A))) _xor_AC(false(),A) -> U121(and(isBool(A),isBoolKind(A)),A) and(tt(),X) -> X equal(X,X) -> tt() if_then_else_fi(B,U,U') -> U131(and(and(isBool(B),isBoolKind(B)),and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U)))), B,U') if_then_else_fi(true(),U,U') -> U141(and(and(isS(U'),isSKind(U')),and(isS(U),isSKind(U))),U) isBool(false()) -> tt() isBool(true()) -> tt() isBool(_and_AC(V1,V2)) -> U151(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_implies_(V1,V2)) -> U161(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_isEqualTo_(V1,V2)) -> tt() isBool(_isNotEqualTo_(V1,V2)) -> tt() isBool(_or_AC(V1,V2)) -> U171(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(_xor_AC(V1,V2)) -> U181(and(isBoolKind(V1),isBoolKind(V2)),V1,V2) isBool(not_(V1)) -> U191(isBoolKind(V1),V1) isBoolKind(false()) -> tt() isBoolKind(true()) -> tt() isBoolKind(_and_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_implies_(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_isEqualTo_(V1,V2)) -> tt() isBoolKind(_isNotEqualTo_(V1,V2)) -> tt() isBoolKind(_or_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(_xor_AC(V1,V2)) -> and(isBoolKind(V1),isBoolKind(V2)) isBoolKind(not_(V1)) -> isBoolKind(V1) not_(A) -> U201(and(isBool(A),isBoolKind(A)),A) not_(false()) -> true() not_(true()) -> false() S: _xor_{AC,#}(_xor_AC(x18,x19),x20) -> _xor_{AC,#}(x18,x19) _xor_{AC,#}(x18,_xor_AC(x19,x20)) -> _xor_{AC,#}(x19,x20) _and_{AC,#}(_and_AC(x18,x19),x20) -> _and_{AC,#}(x18,x19) _and_{AC,#}(x18,_and_AC(x19,x20)) -> _and_{AC,#}(x19,x20) _or_{AC,#}(_or_AC(x18,x19),x20) -> _or_{AC,#}(x18,x19) _or_{AC,#}(x18,_or_AC(x19,x20)) -> _or_{AC,#}(x19,x20) Open