(STRATEGY
    INNERMOST)

(VAR
    a1 a2 o1 o2 p t1 t2 x1 x2 y1 y2)
(DATATYPES
    A = µX.< T, True, F, Or(X, X), False, And(X, X) >)
(SIGNATURES
    disj :: [A] -> A
    conj :: [A] -> A
    bool :: [A] -> A
    isConsTerm :: [A x A] -> A
    isOp :: [A] -> A
    isAnd :: [A] -> A
    getSecond :: [A] -> A
    getFirst :: [A] -> A
    disjconj :: [A] -> A
    and :: [A x A] -> A)
(RULES
    disj(T()) -> True()
    disj(F()) -> True()
    conj(Or(o1,o2)) -> False()
    conj(T()) -> True()
    conj(F()) -> True()
    disj(And(a1,a2)) -> conj(And(a1
                                ,a2))
    disj(Or(t1,t2)) -> and(conj(t1)
                          ,disj(t1))
    conj(And(t1,t2)) -> and(disj(t1)
                           ,conj(t1))
    bool(T()) -> True()
    bool(F()) -> True()
    bool(And(a1,a2)) -> False()
    bool(Or(o1,o2)) -> False()
    isConsTerm(T(),T()) -> True()
    isConsTerm(T(),F()) -> False()
    isConsTerm(T(),And(y1,y2)) ->
      False()
    isConsTerm(T(),Or(x1,x2)) ->
      False()
    isConsTerm(F(),T()) -> False()
    isConsTerm(F(),F()) -> True()
    isConsTerm(F(),And(y1,y2)) ->
      False()
    isConsTerm(F(),Or(x1,x2)) ->
      False()
    isConsTerm(And(a1,a2),T()) ->
      False()
    isConsTerm(And(a1,a2),F()) ->
      False()
    isConsTerm(And(a1,a2)
              ,And(y1,y2)) -> True()
    isConsTerm(And(a1,a2)
              ,Or(x1,x2)) -> False()
    isConsTerm(Or(o1,o2),T()) ->
      False()
    isConsTerm(Or(o1,o2),F()) ->
      False()
    isConsTerm(Or(o1,o2)
              ,And(y1,y2)) -> False()
    isConsTerm(Or(o1,o2)
              ,Or(x1,x2)) -> True()
    isOp(T()) -> False()
    isOp(F()) -> False()
    isOp(And(t1,t2)) -> True()
    isOp(Or(t1,t2)) -> True()
    isAnd(T()) -> False()
    isAnd(F()) -> False()
    isAnd(And(t1,t2)) -> True()
    isAnd(Or(t1,t2)) -> False()
    getSecond(And(t1,t2)) -> t1
    getSecond(Or(t1,t2)) -> t1
    getFirst(And(t1,t2)) -> t1
    getFirst(Or(t1,t2)) -> t1
    disjconj(p) -> disj(p)
    and(False(),False()) ->= False()
    and(True(),False()) ->= False()
    and(False(),True()) ->= False()
    and(True(),True()) ->= True())