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: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(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^#(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(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(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(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(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(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(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(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(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(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(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(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(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , 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^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(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(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(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(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(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(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(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(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(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(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(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(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(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , u'16'1^#(reduce'ii'out()) -> c_35() } 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: 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))) , 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(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))) , 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))) , 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))) , 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))) , 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)) , 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))) , 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)) , 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))) , 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))) , 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))) , 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)))) , 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))))) , 18: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , 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^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(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(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(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(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(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(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(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(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(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(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(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(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(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(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())))) } 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() } 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() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,5,6,8,10,11,12,13,14,15,16,17,18} by applications of Pre({1,2,3,4,5,6,8,10,11,12,13,14,15,16,17,18}) = {7,9}. 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))) , 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) , 3: 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))) , 4: 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))) , 5: 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))) , 6: 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))) , 7: 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)) , 8: 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))) , 9: 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)) , 10: 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))) , 11: 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))) , 12: 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))) , 13: 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)))) , 14: 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))))) , 15: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(intersect'ii'in(F1, F2))) , 16: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) , 17: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) , 18: tautology'i'in^#(F) -> c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), sequent(nil(), nil())))) , 19: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , 20: u'1'1^#(intersect'ii'out()) -> c_4() , 21: u'2'1^#(intersect'ii'out()) -> c_5() , 22: u'8'1^#(reduce'ii'out()) -> c_25() , 23: u'11'1^#(reduce'ii'out()) -> c_28() , 24: u'13'1^#(reduce'ii'out()) -> c_31() , 25: u'9'1^#(reduce'ii'out()) -> c_26() , 26: u'3'1^#(reduce'ii'out()) -> c_19() , 27: u'7'1^#(reduce'ii'out()) -> c_24() , 28: u'4'1^#(reduce'ii'out()) -> c_20() , 29: u'5'1^#(reduce'ii'out()) -> c_21() , 30: u'10'1^#(reduce'ii'out()) -> c_27() , 31: u'14'1^#(reduce'ii'out()) -> c_32() , 32: u'15'1^#(intersect'ii'out()) -> c_33() , 33: u'6'2^#(reduce'ii'out()) -> c_23() , 34: u'12'2^#(reduce'ii'out()) -> c_30() , 35: u'16'1^#(reduce'ii'out()) -> c_35() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { 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(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)) } 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() } Weak DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(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^#(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(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(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(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(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'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(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(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(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(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(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , u'16'1^#(reduce'ii'out()) -> c_35() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2} by applications of Pre({1,2}) = {}. Here rules are labeled as follows: DPs: { 1: 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)) , 2: 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)) , 3: intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) , 4: intersect'ii'in^#(cons(X0, Xs), Ys) -> c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) , 5: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() , 6: u'1'1^#(intersect'ii'out()) -> c_4() , 7: u'2'1^#(intersect'ii'out()) -> c_5() , 8: 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))) , 9: 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))) , 10: 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))) , 11: 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))) , 12: 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))) , 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))) , 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))) , 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))) , 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)))) , 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))))) , 18: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , 35: u'16'1^#(reduce'ii'out()) -> c_35() } 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() } Weak DPs: { intersect'ii'in^#(Xs, cons(X0, Ys)) -> c_1(u'1'1^#(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^#(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(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(x'2d(G1), Gs)), NF) -> c_8(u'13'1^#(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(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(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(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(x'2d(F1), Fs), Gs), NF) -> c_13(u'7'1^#(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(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(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(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(), nil()), sequent(F1, F2)) -> c_18(u'15'1^#(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))) , 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))) , 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())))) , u'16'1^#(reduce'ii'out()) -> c_35() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..