* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys))
            intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out()
            intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys))
            reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) -> u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs))
                                                                               ,NF))
            reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) -> u'9'1(reduce'ii'in(sequent(Fs
                                                                                        ,cons(x'2a(if(A,B),if(B,A)),Gs))
                                                                                ,NF))
            reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) -> u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF)
                                                                       ,Fs
                                                                       ,G2
                                                                       ,Gs
                                                                       ,NF)
            reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) -> u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs)))
                                                                                    ,NF))
            reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) -> u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))
            reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) -> u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs)
                                                                               ,NF))
            reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) -> u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs)
                                                                                        ,Gs)
                                                                                ,NF))
            reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> u'10'1(reduce'ii'in(sequent(Fs,Gs)
                                                                                              ,sequent(cons(p(V),Left)
                                                                                                      ,Right)))
            reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) -> u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs)
                                                                                   ,NF))
            reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) -> u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF)
                                                                      ,F2
                                                                      ,Fs
                                                                      ,Gs
                                                                      ,NF)
            reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) -> u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))
            reduce'ii'in(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> u'14'1(reduce'ii'in(sequent(nil(),Gs)
                                                                                                 ,sequent(Left
                                                                                                         ,cons(p(V)
                                                                                                              ,Right))))
            reduce'ii'in(sequent(nil(),nil()),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2))
            tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
            u'1'1(intersect'ii'out()) -> intersect'ii'out()
            u'10'1(reduce'ii'out()) -> reduce'ii'out()
            u'11'1(reduce'ii'out()) -> reduce'ii'out()
            u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))
            u'12'2(reduce'ii'out()) -> reduce'ii'out()
            u'13'1(reduce'ii'out()) -> reduce'ii'out()
            u'14'1(reduce'ii'out()) -> reduce'ii'out()
            u'15'1(intersect'ii'out()) -> reduce'ii'out()
            u'16'1(reduce'ii'out()) -> tautology'i'out()
            u'2'1(intersect'ii'out()) -> intersect'ii'out()
            u'3'1(reduce'ii'out()) -> reduce'ii'out()
            u'4'1(reduce'ii'out()) -> reduce'ii'out()
            u'5'1(reduce'ii'out()) -> reduce'ii'out()
            u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))
            u'6'2(reduce'ii'out()) -> reduce'ii'out()
            u'7'1(reduce'ii'out()) -> reduce'ii'out()
            u'8'1(reduce'ii'out()) -> reduce'ii'out()
            u'9'1(reduce'ii'out()) -> reduce'ii'out()
        - Signature:
            {intersect'ii'in/2,reduce'ii'in/2,tautology'i'in/1,u'1'1/1,u'10'1/1,u'11'1/1,u'12'1/5,u'12'2/1,u'13'1/1
            ,u'14'1/1,u'15'1/1,u'16'1/1,u'2'1/1,u'3'1/1,u'4'1/1,u'5'1/1,u'6'1/5,u'6'2/1,u'7'1/1,u'8'1/1
            ,u'9'1/1} / {cons/2,if/2,iff/2,intersect'ii'out/0,nil/0,p/1,reduce'ii'out/0,sequent/2,tautology'i'out/0
            ,x'2a/2,x'2b/2,x'2d/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {intersect'ii'in,reduce'ii'in,tautology'i'in,u'1'1,u'10'1
            ,u'11'1,u'12'1,u'12'2,u'13'1,u'14'1,u'15'1,u'16'1,u'2'1,u'3'1,u'4'1,u'5'1,u'6'1,u'6'2,u'7'1,u'8'1
            ,u'9'1} and constructors {cons,if,iff,intersect'ii'out,nil,p,reduce'ii'out,sequent,tautology'i'out,x'2a,x'2b
            ,x'2d}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            intersect'ii'in(Xs,cons(X0,Ys)) -> u'1'1(intersect'ii'in(Xs,Ys))
            intersect'ii'in(cons(X,X0),cons(X,X1)) -> intersect'ii'out()
            intersect'ii'in(cons(X0,Xs),Ys) -> u'2'1(intersect'ii'in(Xs,Ys))
            reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF) -> u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs))
                                                                               ,NF))
            reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF) -> u'9'1(reduce'ii'in(sequent(Fs
                                                                                        ,cons(x'2a(if(A,B),if(B,A)),Gs))
                                                                                ,NF))
            reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) -> u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF)
                                                                       ,Fs
                                                                       ,G2
                                                                       ,Gs
                                                                       ,NF)
            reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) -> u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs)))
                                                                                    ,NF))
            reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF) -> u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))
            reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF) -> u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs)
                                                                               ,NF))
            reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF) -> u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs)
                                                                                        ,Gs)
                                                                                ,NF))
            reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) -> u'10'1(reduce'ii'in(sequent(Fs,Gs)
                                                                                              ,sequent(cons(p(V),Left)
                                                                                                      ,Right)))
            reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) -> u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs)
                                                                                   ,NF))
            reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) -> u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF)
                                                                      ,F2
                                                                      ,Fs
                                                                      ,Gs
                                                                      ,NF)
            reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF) -> u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))
            reduce'ii'in(sequent(nil(),cons(p(V),Gs)),sequent(Left,Right)) -> u'14'1(reduce'ii'in(sequent(nil(),Gs)
                                                                                                 ,sequent(Left
                                                                                                         ,cons(p(V)
                                                                                                              ,Right))))
            reduce'ii'in(sequent(nil(),nil()),sequent(F1,F2)) -> u'15'1(intersect'ii'in(F1,F2))
            tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(),cons(F,nil())),sequent(nil(),nil())))
            u'1'1(intersect'ii'out()) -> intersect'ii'out()
            u'10'1(reduce'ii'out()) -> reduce'ii'out()
            u'11'1(reduce'ii'out()) -> reduce'ii'out()
            u'12'1(reduce'ii'out(),Fs,G2,Gs,NF) -> u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))
            u'12'2(reduce'ii'out()) -> reduce'ii'out()
            u'13'1(reduce'ii'out()) -> reduce'ii'out()
            u'14'1(reduce'ii'out()) -> reduce'ii'out()
            u'15'1(intersect'ii'out()) -> reduce'ii'out()
            u'16'1(reduce'ii'out()) -> tautology'i'out()
            u'2'1(intersect'ii'out()) -> intersect'ii'out()
            u'3'1(reduce'ii'out()) -> reduce'ii'out()
            u'4'1(reduce'ii'out()) -> reduce'ii'out()
            u'5'1(reduce'ii'out()) -> reduce'ii'out()
            u'6'1(reduce'ii'out(),F2,Fs,Gs,NF) -> u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))
            u'6'2(reduce'ii'out()) -> reduce'ii'out()
            u'7'1(reduce'ii'out()) -> reduce'ii'out()
            u'8'1(reduce'ii'out()) -> reduce'ii'out()
            u'9'1(reduce'ii'out()) -> reduce'ii'out()
        - Signature:
            {intersect'ii'in/2,reduce'ii'in/2,tautology'i'in/1,u'1'1/1,u'10'1/1,u'11'1/1,u'12'1/5,u'12'2/1,u'13'1/1
            ,u'14'1/1,u'15'1/1,u'16'1/1,u'2'1/1,u'3'1/1,u'4'1/1,u'5'1/1,u'6'1/5,u'6'2/1,u'7'1/1,u'8'1/1
            ,u'9'1/1} / {cons/2,if/2,iff/2,intersect'ii'out/0,nil/0,p/1,reduce'ii'out/0,sequent/2,tautology'i'out/0
            ,x'2a/2,x'2b/2,x'2d/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {intersect'ii'in,reduce'ii'in,tautology'i'in,u'1'1,u'10'1
            ,u'11'1,u'12'1,u'12'2,u'13'1,u'14'1,u'15'1,u'16'1,u'2'1,u'3'1,u'4'1,u'5'1,u'6'1,u'6'2,u'7'1,u'8'1
            ,u'9'1} and constructors {cons,if,iff,intersect'ii'out,nil,p,reduce'ii'out,sequent,tautology'i'out,x'2a,x'2b
            ,x'2d}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          intersect'ii'in(x,z){z -> cons(y,z)} =
            intersect'ii'in(x,cons(y,z)) ->^+ u'1'1(intersect'ii'in(x,z))
              = C[intersect'ii'in(x,z) = intersect'ii'in(x,z){}]

WORST_CASE(Omega(n^1),?)