MAYBE 1185.20/297.89 MAYBE 1185.20/297.89 1185.20/297.89 We are left with following problem, upon which TcT provides the 1185.20/297.89 certificate MAYBE. 1185.20/297.89 1185.20/297.89 Strict Trs: 1185.20/297.89 { intersect'ii'in(Xs, cons(X0, Ys)) -> 1185.20/297.89 u'1'1(intersect'ii'in(Xs, Ys)) 1185.20/297.89 , intersect'ii'in(cons(X0, Xs), Ys) -> 1185.20/297.89 u'2'1(intersect'ii'in(Xs, Ys)) 1185.20/297.89 , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() 1185.20/297.89 , u'1'1(intersect'ii'out()) -> intersect'ii'out() 1185.20/297.89 , u'2'1(intersect'ii'out()) -> intersect'ii'out() 1185.20/297.89 , reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.20/297.89 u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) 1185.20/297.89 , reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.20/297.89 u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) 1185.20/297.89 , reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.20/297.89 u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) 1185.20/297.89 , reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.20/297.89 u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.20/297.89 NF)) 1185.20/297.89 , reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.20/297.89 u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) 1185.20/297.89 , reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.20/297.89 u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) 1185.20/297.89 , reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.20/297.89 u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) 1185.20/297.89 , reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.20/297.89 u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) 1185.20/297.89 , reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.20/297.89 u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), 1185.20/297.89 NF)) 1185.20/297.89 , reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.20/297.89 u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) 1185.20/297.89 , reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.20/297.89 -> 1185.20/297.89 u'10'1(reduce'ii'in(sequent(Fs, Gs), 1185.20/297.89 sequent(cons(p(V), Left), Right))) 1185.20/297.89 , reduce'ii'in(sequent(nil(), cons(p(V), Gs)), 1185.20/297.89 sequent(Left, Right)) 1185.20/297.89 -> 1185.20/297.89 u'14'1(reduce'ii'in(sequent(nil(), Gs), 1185.20/297.89 sequent(Left, cons(p(V), Right)))) 1185.20/297.89 , reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.20/297.89 u'15'1(intersect'ii'in(F1, F2)) 1185.20/297.89 , u'3'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'4'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'5'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'6'1(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.20/297.89 u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) 1185.20/297.89 , u'6'2(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'7'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'8'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'9'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'10'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'11'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'12'1(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.20/297.89 u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) 1185.20/297.89 , u'12'2(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'13'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'14'1(reduce'ii'out()) -> reduce'ii'out() 1185.20/297.89 , u'15'1(intersect'ii'out()) -> reduce'ii'out() 1185.20/297.89 , tautology'i'in(F) -> 1185.20/297.89 u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.20/297.89 sequent(nil(), nil()))) 1185.20/297.89 , u'16'1(reduce'ii'out()) -> tautology'i'out() } 1185.20/297.89 Obligation: 1185.20/297.89 runtime complexity 1185.20/297.89 Answer: 1185.20/297.89 MAYBE 1185.20/297.89 1185.20/297.89 None of the processors succeeded. 1185.20/297.89 1185.20/297.89 Details of failed attempt(s): 1185.20/297.89 ----------------------------- 1185.20/297.89 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1185.20/297.89 following reason: 1185.20/297.89 1185.20/297.89 Computation stopped due to timeout after 297.0 seconds. 1185.20/297.89 1185.20/297.89 2) 'Best' failed due to the following reason: 1185.20/297.89 1185.20/297.89 None of the processors succeeded. 1185.20/297.89 1185.20/297.89 Details of failed attempt(s): 1185.20/297.89 ----------------------------- 1185.20/297.89 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1185.20/297.89 seconds)' failed due to the following reason: 1185.20/297.89 1185.20/297.89 Computation stopped due to timeout after 148.0 seconds. 1185.20/297.89 1185.20/297.89 2) 'Best' failed due to the following reason: 1185.20/297.89 1185.20/297.89 None of the processors succeeded. 1185.20/297.89 1185.20/297.89 Details of failed attempt(s): 1185.20/297.89 ----------------------------- 1185.20/297.89 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1185.20/297.89 following reason: 1185.20/297.89 1185.20/297.89 The processor is inapplicable, reason: 1185.20/297.89 Processor only applicable for innermost runtime complexity analysis 1185.20/297.89 1185.20/297.89 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1185.20/297.89 to the following reason: 1185.20/297.89 1185.20/297.89 The processor is inapplicable, reason: 1185.20/297.89 Processor only applicable for innermost runtime complexity analysis 1185.20/297.89 1185.20/297.89 1185.20/297.89 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1185.20/297.89 failed due to the following reason: 1185.20/297.89 1185.20/297.89 None of the processors succeeded. 1185.20/297.89 1185.20/297.89 Details of failed attempt(s): 1185.20/297.89 ----------------------------- 1185.20/297.89 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1185.20/297.89 failed due to the following reason: 1185.20/297.89 1185.20/297.89 match-boundness of the problem could not be verified. 1185.20/297.89 1185.20/297.89 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1185.20/297.89 failed due to the following reason: 1185.20/297.89 1185.20/297.89 match-boundness of the problem could not be verified. 1185.20/297.89 1185.20/297.89 1185.20/297.89 1185.20/297.89 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1185.20/297.89 the following reason: 1185.20/297.89 1185.20/297.89 We add the following weak dependency pairs: 1185.20/297.89 1185.20/297.89 Strict DPs: 1185.20/297.89 { intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.20/297.89 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.20/297.89 , intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.20/297.89 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.20/297.89 , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.20/297.89 , u'1'1^#(intersect'ii'out()) -> c_4() 1185.20/297.89 , u'2'1^#(intersect'ii'out()) -> c_5() 1185.20/297.89 , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.20/297.89 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.20/297.89 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.20/297.89 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.20/297.89 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.20/297.89 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.20/297.89 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.20/297.89 Fs, 1185.20/297.89 G2, 1185.20/297.89 Gs, 1185.20/297.89 NF)) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.20/297.89 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.20/297.89 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.20/297.89 F2, 1185.20/297.89 Fs, 1185.20/297.89 Gs, 1185.20/297.89 NF)) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.20/297.89 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.20/297.89 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.20/297.89 Fs), 1185.20/297.89 Gs), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.20/297.89 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.20/297.89 NF))) 1185.20/297.89 , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.20/297.89 -> 1185.20/297.89 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.20/297.89 sequent(cons(p(V), Left), Right)))) 1185.20/297.89 , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.20/297.89 sequent(Left, Right)) 1185.20/297.89 -> 1185.20/297.89 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.20/297.89 sequent(Left, cons(p(V), Right))))) 1185.20/297.89 , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.20/297.89 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.20/297.89 , u'8'1^#(reduce'ii'out()) -> c_25() 1185.20/297.90 , u'11'1^#(reduce'ii'out()) -> c_28() 1185.20/297.90 , u'13'1^#(reduce'ii'out()) -> c_31() 1185.20/297.90 , u'9'1^#(reduce'ii'out()) -> c_26() 1185.20/297.90 , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.20/297.90 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.20/297.90 , u'3'1^#(reduce'ii'out()) -> c_19() 1185.20/297.90 , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.20/297.90 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.20/297.90 , u'7'1^#(reduce'ii'out()) -> c_24() 1185.20/297.90 , u'4'1^#(reduce'ii'out()) -> c_20() 1185.20/297.90 , u'5'1^#(reduce'ii'out()) -> c_21() 1185.20/297.90 , u'10'1^#(reduce'ii'out()) -> c_27() 1185.20/297.90 , u'14'1^#(reduce'ii'out()) -> c_32() 1185.20/297.90 , u'15'1^#(intersect'ii'out()) -> c_33() 1185.20/297.90 , u'6'2^#(reduce'ii'out()) -> c_23() 1185.20/297.90 , u'12'2^#(reduce'ii'out()) -> c_30() 1185.20/297.90 , tautology'i'in^#(F) -> 1185.20/297.90 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.20/297.90 sequent(nil(), nil())))) 1185.20/297.90 , u'16'1^#(reduce'ii'out()) -> c_35() } 1185.20/297.90 1185.20/297.90 and mark the set of starting terms. 1185.20/297.90 1185.20/297.90 We are left with following problem, upon which TcT provides the 1185.20/297.90 certificate MAYBE. 1185.20/297.90 1185.20/297.90 Strict DPs: 1185.20/297.90 { intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.20/297.90 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.20/297.90 , intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.20/297.90 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.20/297.90 , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.20/297.90 , u'1'1^#(intersect'ii'out()) -> c_4() 1185.20/297.90 , u'2'1^#(intersect'ii'out()) -> c_5() 1185.20/297.90 , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.20/297.90 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.20/297.90 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.20/297.90 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.20/297.90 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.20/297.90 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.20/297.90 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.20/297.90 Fs, 1185.20/297.90 G2, 1185.20/297.90 Gs, 1185.20/297.90 NF)) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.20/297.90 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.20/297.90 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.20/297.90 F2, 1185.20/297.90 Fs, 1185.20/297.90 Gs, 1185.20/297.90 NF)) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.20/297.90 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.20/297.90 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.20/297.90 Fs), 1185.20/297.90 Gs), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.20/297.90 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.20/297.90 NF))) 1185.20/297.90 , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.20/297.90 -> 1185.20/297.90 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.20/297.90 sequent(cons(p(V), Left), Right)))) 1185.20/297.90 , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.20/297.90 sequent(Left, Right)) 1185.20/297.90 -> 1185.20/297.90 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.20/297.90 sequent(Left, cons(p(V), Right))))) 1185.20/297.90 , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.20/297.90 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.20/297.90 , u'8'1^#(reduce'ii'out()) -> c_25() 1185.20/297.90 , u'11'1^#(reduce'ii'out()) -> c_28() 1185.20/297.90 , u'13'1^#(reduce'ii'out()) -> c_31() 1185.20/297.90 , u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.90 , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.90 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.90 , u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.90 , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.90 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.90 , u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.90 , u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.90 , u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.90 , u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.90 , u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.90 , u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.90 , u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.90 , u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.90 , tautology'i'in^#(F) -> 1185.62/297.90 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.90 sequent(nil(), nil())))) 1185.62/297.90 , u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.90 Strict Trs: 1185.62/297.90 { intersect'ii'in(Xs, cons(X0, Ys)) -> 1185.62/297.90 u'1'1(intersect'ii'in(Xs, Ys)) 1185.62/297.90 , intersect'ii'in(cons(X0, Xs), Ys) -> 1185.62/297.90 u'2'1(intersect'ii'in(Xs, Ys)) 1185.62/297.90 , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() 1185.62/297.90 , u'1'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.90 , u'2'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.90 u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.90 u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.90 u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.90 u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.90 u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) 1185.62/297.90 , reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.90 u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.90 u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.90 u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 u'10'1(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.90 sequent(cons(p(V), Left), Right))) 1185.62/297.90 , reduce'ii'in(sequent(nil(), cons(p(V), Gs)), 1185.62/297.90 sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 u'14'1(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.90 sequent(Left, cons(p(V), Right)))) 1185.62/297.90 , reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.90 u'15'1(intersect'ii'in(F1, F2)) 1185.62/297.90 , u'3'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'4'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'5'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'6'1(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.90 u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) 1185.62/297.90 , u'6'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'7'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'8'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'9'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'10'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'11'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'12'1(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.90 u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) 1185.62/297.90 , u'12'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'13'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'14'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'15'1(intersect'ii'out()) -> reduce'ii'out() 1185.62/297.90 , tautology'i'in(F) -> 1185.62/297.90 u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.90 sequent(nil(), nil()))) 1185.62/297.90 , u'16'1(reduce'ii'out()) -> tautology'i'out() } 1185.62/297.90 Obligation: 1185.62/297.90 runtime complexity 1185.62/297.90 Answer: 1185.62/297.90 MAYBE 1185.62/297.90 1185.62/297.90 We estimate the number of application of 1185.62/297.90 {3,4,5,19,20,21,22,24,26,27,28,29,30,31,32,33,35} by applications 1185.62/297.90 of Pre({3,4,5,19,20,21,22,24,26,27,28,29,30,31,32,33,35}) = 1185.62/297.90 {1,2,6,7,8,9,11,13,14,15,16,17,18,23,25,34}. Here rules are labeled 1185.62/297.90 as follows: 1185.62/297.90 1185.62/297.90 DPs: 1185.62/297.90 { 1: intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.90 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.90 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , 3: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.90 , 4: u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.90 , 5: u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.90 , 6: reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.90 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , 7: reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.90 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.90 NF))) 1185.62/297.90 , 8: reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.90 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.90 , 9: reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.90 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.90 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , 10: reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.90 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.90 Fs, 1185.62/297.90 G2, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , 11: reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.90 NF))) 1185.62/297.90 , 12: reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.90 F2, 1185.62/297.90 Fs, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , 13: reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.90 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.90 , 14: reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.90 Fs), 1185.62/297.90 Gs), 1185.62/297.90 NF))) 1185.62/297.90 , 15: reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.90 NF))) 1185.62/297.90 , 16: reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), 1185.62/297.90 sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.90 sequent(cons(p(V), Left), Right)))) 1185.62/297.90 , 17: reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.90 sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.90 sequent(Left, cons(p(V), Right))))) 1185.62/297.90 , 18: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.90 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.90 , 19: u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.90 , 20: u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.90 , 21: u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.90 , 22: u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.90 , 23: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.90 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.90 , 24: u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.90 , 25: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.90 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.90 , 26: u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.90 , 27: u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.90 , 28: u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.90 , 29: u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.90 , 30: u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.90 , 31: u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.90 , 32: u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.90 , 33: u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.90 , 34: tautology'i'in^#(F) -> 1185.62/297.90 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.90 sequent(nil(), nil())))) 1185.62/297.90 , 35: u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.90 1185.62/297.90 We are left with following problem, upon which TcT provides the 1185.62/297.90 certificate MAYBE. 1185.62/297.90 1185.62/297.90 Strict DPs: 1185.62/297.90 { intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.90 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.90 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.90 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.90 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.90 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.90 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.90 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.90 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.90 Fs, 1185.62/297.90 G2, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.90 F2, 1185.62/297.90 Fs, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.90 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.90 Fs), 1185.62/297.90 Gs), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.90 NF))) 1185.62/297.90 , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.90 sequent(cons(p(V), Left), Right)))) 1185.62/297.90 , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.90 sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.90 sequent(Left, cons(p(V), Right))))) 1185.62/297.90 , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.90 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.90 , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.90 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.90 , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.90 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.90 , tautology'i'in^#(F) -> 1185.62/297.90 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.90 sequent(nil(), nil())))) } 1185.62/297.90 Strict Trs: 1185.62/297.90 { intersect'ii'in(Xs, cons(X0, Ys)) -> 1185.62/297.90 u'1'1(intersect'ii'in(Xs, Ys)) 1185.62/297.90 , intersect'ii'in(cons(X0, Xs), Ys) -> 1185.62/297.90 u'2'1(intersect'ii'in(Xs, Ys)) 1185.62/297.90 , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() 1185.62/297.90 , u'1'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.90 , u'2'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.90 u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.90 u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.90 u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.90 u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.90 u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) 1185.62/297.90 , reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.90 u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.90 u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.90 u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), 1185.62/297.90 NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) 1185.62/297.90 , reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 u'10'1(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.90 sequent(cons(p(V), Left), Right))) 1185.62/297.90 , reduce'ii'in(sequent(nil(), cons(p(V), Gs)), 1185.62/297.90 sequent(Left, Right)) 1185.62/297.90 -> 1185.62/297.90 u'14'1(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.90 sequent(Left, cons(p(V), Right)))) 1185.62/297.90 , reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.90 u'15'1(intersect'ii'in(F1, F2)) 1185.62/297.90 , u'3'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'4'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'5'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'6'1(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.90 u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) 1185.62/297.90 , u'6'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'7'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'8'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'9'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'10'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'11'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'12'1(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.90 u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) 1185.62/297.90 , u'12'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'13'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'14'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.90 , u'15'1(intersect'ii'out()) -> reduce'ii'out() 1185.62/297.90 , tautology'i'in(F) -> 1185.62/297.90 u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.90 sequent(nil(), nil()))) 1185.62/297.90 , u'16'1(reduce'ii'out()) -> tautology'i'out() } 1185.62/297.90 Weak DPs: 1185.62/297.90 { intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.90 , u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.90 , u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.90 , u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.90 , u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.90 , u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.90 , u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.90 , u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.90 , u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.90 , u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.90 , u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.90 , u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.90 , u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.90 , u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.90 , u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.90 , u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.90 , u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.90 Obligation: 1185.62/297.90 runtime complexity 1185.62/297.90 Answer: 1185.62/297.90 MAYBE 1185.62/297.90 1185.62/297.90 We estimate the number of application of 1185.62/297.90 {1,2,3,4,5,6,8,10,11,12,13,14,15,16,17,18} by applications of 1185.62/297.90 Pre({1,2,3,4,5,6,8,10,11,12,13,14,15,16,17,18}) = {7,9}. Here rules 1185.62/297.90 are labeled as follows: 1185.62/297.90 1185.62/297.90 DPs: 1185.62/297.90 { 1: intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.90 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , 2: intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.90 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.90 , 3: reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.90 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , 4: reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.90 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.90 NF))) 1185.62/297.90 , 5: reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.90 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.90 , 6: reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.90 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.90 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.90 NF))) 1185.62/297.90 , 7: reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.90 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.90 Fs, 1185.62/297.90 G2, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , 8: reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.90 NF))) 1185.62/297.90 , 9: reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.90 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.90 F2, 1185.62/297.90 Fs, 1185.62/297.90 Gs, 1185.62/297.90 NF)) 1185.62/297.90 , 10: reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.90 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.90 , 11: reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.90 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.90 Fs), 1185.62/297.90 Gs), 1185.62/297.91 NF))) 1185.62/297.91 , 12: reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , 13: reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right)))) 1185.62/297.91 , 14: reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right))))) 1185.62/297.91 , 15: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.91 , 16: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.91 , 17: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.91 , 18: tautology'i'in^#(F) -> 1185.62/297.91 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil())))) 1185.62/297.91 , 19: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.91 , 20: u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.91 , 21: u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.91 , 22: u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.91 , 23: u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.91 , 24: u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.91 , 25: u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.91 , 26: u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.91 , 27: u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.91 , 28: u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.91 , 29: u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.91 , 30: u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.91 , 31: u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.91 , 32: u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.91 , 33: u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.91 , 34: u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.91 , 35: u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.91 1185.62/297.91 We are left with following problem, upon which TcT provides the 1185.62/297.91 certificate MAYBE. 1185.62/297.91 1185.62/297.91 Strict DPs: 1185.62/297.91 { reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.91 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.91 Fs, 1185.62/297.91 G2, 1185.62/297.91 Gs, 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.91 F2, 1185.62/297.91 Fs, 1185.62/297.91 Gs, 1185.62/297.91 NF)) } 1185.62/297.91 Strict Trs: 1185.62/297.91 { intersect'ii'in(Xs, cons(X0, Ys)) -> 1185.62/297.91 u'1'1(intersect'ii'in(Xs, Ys)) 1185.62/297.91 , intersect'ii'in(cons(X0, Xs), Ys) -> 1185.62/297.91 u'2'1(intersect'ii'in(Xs, Ys)) 1185.62/297.91 , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() 1185.62/297.91 , u'1'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.91 , u'2'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.91 u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.91 u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.91 u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.91 u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.91 u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) 1185.62/297.91 , reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.91 u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.91 u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.91 u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 u'10'1(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right))) 1185.62/297.91 , reduce'ii'in(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 u'14'1(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right)))) 1185.62/297.91 , reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 u'15'1(intersect'ii'in(F1, F2)) 1185.62/297.91 , u'3'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'4'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'5'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'6'1(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) 1185.62/297.91 , u'6'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'7'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'8'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'9'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'10'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'11'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'12'1(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) 1185.62/297.91 , u'12'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'13'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'14'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'15'1(intersect'ii'out()) -> reduce'ii'out() 1185.62/297.91 , tautology'i'in(F) -> 1185.62/297.91 u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil()))) 1185.62/297.91 , u'16'1(reduce'ii'out()) -> tautology'i'out() } 1185.62/297.91 Weak DPs: 1185.62/297.91 { intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.91 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.91 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.91 , u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.91 , u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.91 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.91 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.91 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.91 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.91 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.91 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.91 Fs), 1185.62/297.91 Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right)))) 1185.62/297.91 , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right))))) 1185.62/297.91 , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.91 , u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.91 , u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.91 , u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.91 , u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.91 , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.91 , u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.91 , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.91 , u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.91 , u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.91 , u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.91 , u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.91 , u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.91 , u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.91 , u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.91 , u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.91 , tautology'i'in^#(F) -> 1185.62/297.91 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil())))) 1185.62/297.91 , u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.91 Obligation: 1185.62/297.91 runtime complexity 1185.62/297.91 Answer: 1185.62/297.91 MAYBE 1185.62/297.91 1185.62/297.91 We estimate the number of application of {1,2} by applications of 1185.62/297.91 Pre({1,2}) = {}. Here rules are labeled as follows: 1185.62/297.91 1185.62/297.91 DPs: 1185.62/297.91 { 1: reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.91 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.91 Fs, 1185.62/297.91 G2, 1185.62/297.91 Gs, 1185.62/297.91 NF)) 1185.62/297.91 , 2: reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.91 F2, 1185.62/297.91 Fs, 1185.62/297.91 Gs, 1185.62/297.91 NF)) 1185.62/297.91 , 3: intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.91 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , 4: intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.91 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , 5: intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.91 , 6: u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.91 , 7: u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.91 , 8: reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.91 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , 9: reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.91 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.91 NF))) 1185.62/297.91 , 10: reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.91 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.91 , 11: reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.91 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.91 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , 12: reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , 13: reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.91 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.91 , 14: reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.91 Fs), 1185.62/297.91 Gs), 1185.62/297.91 NF))) 1185.62/297.91 , 15: reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , 16: reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right)))) 1185.62/297.91 , 17: reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right))))) 1185.62/297.91 , 18: reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.91 , 19: u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.91 , 20: u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.91 , 21: u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.91 , 22: u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.91 , 23: u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.91 , 24: u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.91 , 25: u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.91 , 26: u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.91 , 27: u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.91 , 28: u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.91 , 29: u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.91 , 30: u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.91 , 31: u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.91 , 32: u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.91 , 33: u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.91 , 34: tautology'i'in^#(F) -> 1185.62/297.91 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil())))) 1185.62/297.91 , 35: u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.91 1185.62/297.91 We are left with following problem, upon which TcT provides the 1185.62/297.91 certificate MAYBE. 1185.62/297.91 1185.62/297.91 Strict Trs: 1185.62/297.91 { intersect'ii'in(Xs, cons(X0, Ys)) -> 1185.62/297.91 u'1'1(intersect'ii'in(Xs, Ys)) 1185.62/297.91 , intersect'ii'in(cons(X0, Xs), Ys) -> 1185.62/297.91 u'2'1(intersect'ii'in(Xs, Ys)) 1185.62/297.91 , intersect'ii'in(cons(X, X0), cons(X, X1)) -> intersect'ii'out() 1185.62/297.91 , u'1'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.91 , u'2'1(intersect'ii'out()) -> intersect'ii'out() 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.91 u'8'1(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.91 u'11'1(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.91 u'13'1(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.91 u'9'1(reduce'ii'in(sequent(Fs, cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.91 u'12'1(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), Fs, G2, Gs, NF) 1185.62/297.91 , reduce'ii'in(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.91 u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 u'6'1(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), F2, Fs, Gs, NF) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.91 u'7'1(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.91 u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), Fs), Gs), 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 u'5'1(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), NF)) 1185.62/297.91 , reduce'ii'in(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 u'10'1(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right))) 1185.62/297.91 , reduce'ii'in(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 u'14'1(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right)))) 1185.62/297.91 , reduce'ii'in(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 u'15'1(intersect'ii'in(F1, F2)) 1185.62/297.91 , u'3'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'4'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'5'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'6'1(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 u'6'2(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF)) 1185.62/297.91 , u'6'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'7'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'8'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'9'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'10'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'11'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'12'1(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 u'12'2(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF)) 1185.62/297.91 , u'12'2(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'13'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'14'1(reduce'ii'out()) -> reduce'ii'out() 1185.62/297.91 , u'15'1(intersect'ii'out()) -> reduce'ii'out() 1185.62/297.91 , tautology'i'in(F) -> 1185.62/297.91 u'16'1(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil()))) 1185.62/297.91 , u'16'1(reduce'ii'out()) -> tautology'i'out() } 1185.62/297.91 Weak DPs: 1185.62/297.91 { intersect'ii'in^#(Xs, cons(X0, Ys)) -> 1185.62/297.91 c_1(u'1'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , intersect'ii'in^#(cons(X0, Xs), Ys) -> 1185.62/297.91 c_2(u'2'1^#(intersect'ii'in(Xs, Ys))) 1185.62/297.91 , intersect'ii'in^#(cons(X, X0), cons(X, X1)) -> c_3() 1185.62/297.91 , u'1'1^#(intersect'ii'out()) -> c_4() 1185.62/297.91 , u'2'1^#(intersect'ii'out()) -> c_5() 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(if(A, B), Gs)), NF) -> 1185.62/297.91 c_6(u'8'1^#(reduce'ii'in(sequent(Fs, cons(x'2b(x'2d(B), A), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(x'2b(G1, G2), Gs)), NF) -> 1185.62/297.91 c_7(u'11'1^#(reduce'ii'in(sequent(Fs, cons(G1, cons(G2, Gs))), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(x'2d(G1), Gs)), NF) -> 1185.62/297.91 c_8(u'13'1^#(reduce'ii'in(sequent(cons(G1, Fs), Gs), NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(iff(A, B), Gs)), NF) -> 1185.62/297.91 c_9(u'9'1^#(reduce'ii'in(sequent(Fs, 1185.62/297.91 cons(x'2a(if(A, B), if(B, A)), Gs)), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(Fs, cons(x'2a(G1, G2), Gs)), NF) -> 1185.62/297.91 c_10(u'12'1^#(reduce'ii'in(sequent(Fs, cons(G1, Gs)), NF), 1185.62/297.91 Fs, 1185.62/297.91 G2, 1185.62/297.91 Gs, 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(if(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_11(u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B), A), Fs), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2b(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_12(u'6'1^#(reduce'ii'in(sequent(cons(F1, Fs), Gs), NF), 1185.62/297.91 F2, 1185.62/297.91 Fs, 1185.62/297.91 Gs, 1185.62/297.91 NF)) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2d(F1), Fs), Gs), NF) -> 1185.62/297.91 c_13(u'7'1^#(reduce'ii'in(sequent(Fs, cons(F1, Gs)), NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(iff(A, B), Fs), Gs), NF) -> 1185.62/297.91 c_14(u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A, B), if(B, A)), 1185.62/297.91 Fs), 1185.62/297.91 Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(x'2a(F1, F2), Fs), Gs), NF) -> 1185.62/297.91 c_15(u'5'1^#(reduce'ii'in(sequent(cons(F1, cons(F2, Fs)), Gs), 1185.62/297.91 NF))) 1185.62/297.91 , reduce'ii'in^#(sequent(cons(p(V), Fs), Gs), sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_16(u'10'1^#(reduce'ii'in(sequent(Fs, Gs), 1185.62/297.91 sequent(cons(p(V), Left), Right)))) 1185.62/297.91 , reduce'ii'in^#(sequent(nil(), cons(p(V), Gs)), 1185.62/297.91 sequent(Left, Right)) 1185.62/297.91 -> 1185.62/297.91 c_17(u'14'1^#(reduce'ii'in(sequent(nil(), Gs), 1185.62/297.91 sequent(Left, cons(p(V), Right))))) 1185.62/297.91 , reduce'ii'in^#(sequent(nil(), nil()), sequent(F1, F2)) -> 1185.62/297.91 c_18(u'15'1^#(intersect'ii'in(F1, F2))) 1185.62/297.91 , u'8'1^#(reduce'ii'out()) -> c_25() 1185.62/297.91 , u'11'1^#(reduce'ii'out()) -> c_28() 1185.62/297.91 , u'13'1^#(reduce'ii'out()) -> c_31() 1185.62/297.91 , u'9'1^#(reduce'ii'out()) -> c_26() 1185.62/297.91 , u'12'1^#(reduce'ii'out(), Fs, G2, Gs, NF) -> 1185.62/297.91 c_29(u'12'2^#(reduce'ii'in(sequent(Fs, cons(G2, Gs)), NF))) 1185.62/297.91 , u'3'1^#(reduce'ii'out()) -> c_19() 1185.62/297.91 , u'6'1^#(reduce'ii'out(), F2, Fs, Gs, NF) -> 1185.62/297.91 c_22(u'6'2^#(reduce'ii'in(sequent(cons(F2, Fs), Gs), NF))) 1185.62/297.91 , u'7'1^#(reduce'ii'out()) -> c_24() 1185.62/297.91 , u'4'1^#(reduce'ii'out()) -> c_20() 1185.62/297.91 , u'5'1^#(reduce'ii'out()) -> c_21() 1185.62/297.91 , u'10'1^#(reduce'ii'out()) -> c_27() 1185.62/297.91 , u'14'1^#(reduce'ii'out()) -> c_32() 1185.62/297.91 , u'15'1^#(intersect'ii'out()) -> c_33() 1185.62/297.91 , u'6'2^#(reduce'ii'out()) -> c_23() 1185.62/297.91 , u'12'2^#(reduce'ii'out()) -> c_30() 1185.62/297.91 , tautology'i'in^#(F) -> 1185.62/297.91 c_34(u'16'1^#(reduce'ii'in(sequent(nil(), cons(F, nil())), 1185.62/297.91 sequent(nil(), nil())))) 1185.62/297.91 , u'16'1^#(reduce'ii'out()) -> c_35() } 1185.62/297.91 Obligation: 1185.62/297.91 runtime complexity 1185.62/297.91 Answer: 1185.62/297.91 MAYBE 1185.62/297.91 1185.62/297.91 Empty strict component of the problem is NOT empty. 1185.62/297.91 1185.62/297.91 1185.62/297.91 Arrrr.. 1186.55/298.87 EOF