(STRATEGY
    INNERMOST)

(VAR
    x22 x20 x14 x10 x6 x8 x4 x2 x12 x32 x28 x24 x1 x3)
(RULES
    eval2#5(x22,x20,x14,x10,Var(x6)) -> ite_b#2(eqNat#2(x6,x22)
                                               ,x20
                                               ,ite#3(eqNat#2(x6,x14),x10))
    eval2#5(x10,x8,x6,x4,Not(x2)) -> lnot#1(eval2#5(x10,x8,x6,x4,x2))
    eval2#5(x12,x10,x8,x6,And(x4,x2)) -> land#2(eval2#5(x12,x10,x8,x6,x4)
                                               ,eval2#5(x12,x10,x8,x6,x2))
    eval2#5(x12,x10,x8,x6,Or(x4,x2)) -> lor#2(eval2#5(x12,x10,x8,x6,x4)
                                             ,eval2#5(x12,x10,x8,x6,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_b#2(True(),x20,x24) -> x20
    ite_b#2(False(),x20,x24) -> x24
    ite#3(True(),x1) -> x1
    ite#3(False(),x1) -> bot[0]#1()
    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) -> Cons(Triple(True(),True(),eval2#5(x3,True(),x2,True(),x1))
                          ,Cons(Triple(True()
                                      ,False()
                                      ,eval2#5(x3,True(),x2,False(),x1))
                               ,Cons(Triple(False()
                                           ,True()
                                           ,eval2#5(x3,False(),x2,True(),x1))
                                    ,Cons(Triple(False()
                                                ,False()
                                                ,eval2#5(x3
                                                        ,False()
                                                        ,x2
                                                        ,False()
                                                        ,x1))
                                         ,Nil())))))