(STRATEGY
    INNERMOST)

(VAR
    x4 x6 x3 x2 x1 x44 x40 x8 x32 x28 x48 x20)
(RULES
    table_make#3(x4,Nil(),x6) -> Cons(Pair(aux#2(Nil(),x4),eval#2(x4,x6)),Nil())
    table_make#3(x4,Cons(x3,x2),x1) -> concat#2(table_make#3(Cons(Pair(x3
                                                                      ,True())
                                                                 ,x4)
                                                            ,x2
                                                            ,x1)
                                               ,table_make#3(Cons(Pair(x3
                                                                      ,False())
                                                                 ,x4)
                                                            ,x2
                                                            ,x1))
    eval#2(x4,Var(x2)) -> assoc#2(x2,x4)
    eval#2(x4,Not(x2)) -> lnot#1(eval#2(x4,x2))
    eval#2(x6,And(x4,x2)) -> land#2(eval#2(x6,x4),eval#2(x6,x2))
    eval#2(x6,Or(x4,x2)) -> lor#2(eval#2(x6,x4),eval#2(x6,x2))
    concat#2(Nil(),x44) -> x44
    concat#2(Cons(x6,x4),x2) -> Cons(x6,concat#2(x4,x2))
    aux#2(x40,Nil()) -> x40
    aux#2(x6,Cons(x4,x2)) -> aux#2(Cons(x4,x6),x2)
    assoc#2(x2,Nil()) -> bot[0]#1()
    assoc#2(x8,Cons(Pair(x6,x4),x2)) -> ite#3(eqNat#2(x6,x8),x4,assoc#2(x8,x2))
    lor#2(True(),x32) -> True()
    lor#2(False(),x32) -> x32
    land#2(False(),x28) -> False()
    land#2(True(),x28) -> x28
    lnot#1(True()) -> False()
    lnot#1(False()) -> True()
    ite#3(True(),x40,x48) -> x40
    ite#3(False(),x40,x48) -> x48
    eqNat#2(0(),0()) -> True()
    eqNat#2(S(x20),0()) -> False()
    eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
    eqNat#2(0(),S(x20)) -> False()
    main(x3,x2,x1) -> table_make#3(x2,x1,x3))