MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() , tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1(reduce'ii'out()) -> tautology'i'out() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , u'1'1^#(intersect'ii'out()) -> c_4() , u'2'1^#(intersect'ii'out()) -> c_5() , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , u'8'1^#(reduce'ii'out()) -> c_25() , u'11'1^#(reduce'ii'out()) -> c_28() , u'13'1^#(reduce'ii'out()) -> c_31() , u'9'1^#(reduce'ii'out()) -> c_26() , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'3'1^#(reduce'ii'out()) -> c_19() , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , u'7'1^#(reduce'ii'out()) -> c_24() , u'4'1^#(reduce'ii'out()) -> c_20() , u'5'1^#(reduce'ii'out()) -> c_21() , u'10'1^#(reduce'ii'out()) -> c_27() , u'14'1^#(reduce'ii'out()) -> c_32() , u'15'1^#(intersect'ii'out()) -> c_33() , u'6'2^#(reduce'ii'out()) -> c_23() , u'12'2^#(reduce'ii'out()) -> c_30() , tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1^#(reduce'ii'out()) -> c_35() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , u'1'1^#(intersect'ii'out()) -> c_4() , u'2'1^#(intersect'ii'out()) -> c_5() , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , u'8'1^#(reduce'ii'out()) -> c_25() , u'11'1^#(reduce'ii'out()) -> c_28() , u'13'1^#(reduce'ii'out()) -> c_31() , u'9'1^#(reduce'ii'out()) -> c_26() , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'3'1^#(reduce'ii'out()) -> c_19() , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , u'7'1^#(reduce'ii'out()) -> c_24() , u'4'1^#(reduce'ii'out()) -> c_20() , u'5'1^#(reduce'ii'out()) -> c_21() , u'10'1^#(reduce'ii'out()) -> c_27() , u'14'1^#(reduce'ii'out()) -> c_32() , u'15'1^#(intersect'ii'out()) -> c_33() , u'6'2^#(reduce'ii'out()) -> c_23() , u'12'2^#(reduce'ii'out()) -> c_30() , tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1^#(reduce'ii'out()) -> c_35() } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() , tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1(reduce'ii'out()) -> tautology'i'out() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,4,5,19,20,21,22,24,26,27,28,29,30,31,32,33,35} by applications of Pre({3,4,5,19,20,21,22,24,26,27,28,29,30,31,32,33,35}) = {1,2,6,7,8,9,11,13,14,15,16,17,18,23,25,34}. Here rules are labeled as follows: DPs: { 1: intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , 3: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , 4: u'1'1^#(intersect'ii'out()) -> c_4() , 5: u'2'1^#(intersect'ii'out()) -> c_5() , 6: reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , 7: reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , 8: reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , 9: reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , 10: reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , 11: reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , 12: reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , 13: reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , 14: reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , 15: reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , 16: reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , 17: reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , 18: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , 19: u'8'1^#(reduce'ii'out()) -> c_25() , 20: u'11'1^#(reduce'ii'out()) -> c_28() , 21: u'13'1^#(reduce'ii'out()) -> c_31() , 22: u'9'1^#(reduce'ii'out()) -> c_26() , 23: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , 24: u'3'1^#(reduce'ii'out()) -> c_19() , 25: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , 26: u'7'1^#(reduce'ii'out()) -> c_24() , 27: u'4'1^#(reduce'ii'out()) -> c_20() , 28: u'5'1^#(reduce'ii'out()) -> c_21() , 29: u'10'1^#(reduce'ii'out()) -> c_27() , 30: u'14'1^#(reduce'ii'out()) -> c_32() , 31: u'15'1^#(intersect'ii'out()) -> c_33() , 32: u'6'2^#(reduce'ii'out()) -> c_23() , 33: u'12'2^#(reduce'ii'out()) -> c_30() , 34: tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , 35: u'16'1^#(reduce'ii'out()) -> c_35() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } Weak DPs: { intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , u'1'1^#(intersect'ii'out()) -> c_4() , u'2'1^#(intersect'ii'out()) -> c_5() , u'8'1^#(reduce'ii'out()) -> c_25() , u'11'1^#(reduce'ii'out()) -> c_28() , u'13'1^#(reduce'ii'out()) -> c_31() , u'9'1^#(reduce'ii'out()) -> c_26() , u'3'1^#(reduce'ii'out()) -> c_19() , u'7'1^#(reduce'ii'out()) -> c_24() , u'4'1^#(reduce'ii'out()) -> c_20() , u'5'1^#(reduce'ii'out()) -> c_21() , u'10'1^#(reduce'ii'out()) -> c_27() , u'14'1^#(reduce'ii'out()) -> c_32() , u'15'1^#(intersect'ii'out()) -> c_33() , u'6'2^#(reduce'ii'out()) -> c_23() , u'12'2^#(reduce'ii'out()) -> c_30() , u'16'1^#(reduce'ii'out()) -> c_35() } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() , tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1(reduce'ii'out()) -> tautology'i'out() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , u'1'1^#(intersect'ii'out()) -> c_4() , u'2'1^#(intersect'ii'out()) -> c_5() , u'8'1^#(reduce'ii'out()) -> c_25() , u'11'1^#(reduce'ii'out()) -> c_28() , u'13'1^#(reduce'ii'out()) -> c_31() , u'9'1^#(reduce'ii'out()) -> c_26() , u'3'1^#(reduce'ii'out()) -> c_19() , u'7'1^#(reduce'ii'out()) -> c_24() , u'4'1^#(reduce'ii'out()) -> c_20() , u'5'1^#(reduce'ii'out()) -> c_21() , u'10'1^#(reduce'ii'out()) -> c_27() , u'14'1^#(reduce'ii'out()) -> c_32() , u'15'1^#(intersect'ii'out()) -> c_33() , u'6'2^#(reduce'ii'out()) -> c_23() , u'12'2^#(reduce'ii'out()) -> c_30() , u'16'1^#(reduce'ii'out()) -> c_35() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() , tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1(reduce'ii'out()) -> tautology'i'out() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys)), intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)), reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_9(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(if(A, B), if(B, A)), Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)), reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))), reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))), reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2)), intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)), reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)), reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))), reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(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) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_16(reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_17(reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , tautology'i'in^#(F) -> c_18(reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() , tautology'i'in(F) -> u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) , u'16'1(reduce'ii'out()) -> tautology'i'out() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(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) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_16(reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_17(reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) , tautology'i'in^#(F) -> c_18(reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) -->_1 intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) :2 -->_1 intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) :1 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) -->_1 intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) :2 -->_1 intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) :1 3: reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 4: reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 5: reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 6: reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 7: reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) -->_1 u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_16(reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) :16 -->_2 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_2 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_2 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_2 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_2 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_2 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_2 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_2 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_2 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 8: reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 9: reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) -->_1 u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_17(reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) :17 -->_2 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_2 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_2 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_2 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_2 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_2 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_2 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_2 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_2 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 10: reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 11: reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 12: reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 13: reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) -->_1 reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) :15 -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 14: reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) -->_1 reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) :15 -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 15: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) -->_1 intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) :2 -->_1 intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) :1 16: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_16(reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 17: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_17(reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) -->_1 reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) :13 -->_1 reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) :12 -->_1 reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) :11 -->_1 reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) :10 -->_1 reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) :9 -->_1 reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) :8 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 18: tautology'i'in^#(F) -> c_18(reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) -->_1 reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) :14 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) :7 -->_1 reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(reduce'ii'in^#(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), NF)) :6 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) :5 -->_1 reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) :4 -->_1 reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) :3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { tautology'i'in^#(F) -> c_18(reduce'ii'in^#(sequent(nil(), cons(F, nil())), sequent(nil(), nil()))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(intersect'ii'in^#(Xs, Ys)) , intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(intersect'ii'in^#(Xs, Ys)) , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> c_3(reduce'ii'in^#(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> c_4(reduce'ii'in^#(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> c_5(reduce'ii'in^#(sequent(cons(G1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> c_6(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) -> c_7(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF), reduce'ii'in^#(sequent(Fs, cons(G1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> c_8(reduce'ii'in^#(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> c_9(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF), reduce'ii'in^#(sequent(cons(F1, Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> c_10(reduce'ii'in^#(sequent(Fs, cons(F1, Gs)), NF)) , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> c_11(reduce'ii'in^#(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), NF)) , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> c_12(reduce'ii'in^#(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) -> c_13(reduce'ii'in^#(sequent(Fs, Gs), sequent(cons(p(V), Left), Right))) , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), sequent(Left, Right)) -> c_14(reduce'ii'in^#(sequent(nil(), Gs), sequent(Left, cons(p(V), Right)))) , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_15(intersect'ii'in^#(F1, F2)) , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_16(reduce'ii'in^#(sequent(Fs, cons(G2, Gs)), NF)) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_17(reduce'ii'in^#(sequent(cons(F2, Fs), Gs), NF)) } Weak Trs: { intersect'ii'in(Xs, cons(X0, Ys)) -> u'1'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X0, Xs), Ys) -> u'2'1(intersect'ii'in(Xs, Ys)) , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() , u'1'1(intersect'ii'out()) -> intersect'ii'out() , u'2'1(intersect'ii'out()) -> intersect'ii'out() , 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(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(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(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(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(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(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(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(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)) , 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() , 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() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..