MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { and(false(), false()) -> false() , and(false(), true()) -> false() , and(true(), false()) -> false() , and(true(), true()) -> true() , eq(nil(), nil()) -> true() , eq(nil(), cons(T, L)) -> false() , eq(cons(T, L), nil()) -> false() , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) , eq(var(L), var(Lp)) -> eq(L, Lp) , eq(var(L), apply(T, S)) -> false() , eq(var(L), lambda(X, T)) -> false() , eq(apply(T, S), var(L)) -> false() , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) , eq(apply(T, S), lambda(X, Tp)) -> false() , eq(lambda(X, T), var(L)) -> false() , eq(lambda(X, T), apply(Tp, Sp)) -> false() , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) , if(false(), var(K), var(L)) -> var(L) , if(true(), var(K), var(L)) -> var(K) , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) , ren(X, Y, lambda(Z, T)) -> lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } 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) '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) '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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { and^#(false(), false()) -> c_1() , and^#(false(), true()) -> c_2() , and^#(true(), false()) -> c_3() , and^#(true(), true()) -> c_4() , eq^#(nil(), nil()) -> c_5() , eq^#(nil(), cons(T, L)) -> c_6() , eq^#(cons(T, L), nil()) -> c_7() , eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , eq^#(var(L), apply(T, S)) -> c_10() , eq^#(var(L), lambda(X, T)) -> c_11() , eq^#(apply(T, S), var(L)) -> c_12() , eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , eq^#(lambda(X, T), var(L)) -> c_15() , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() , eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) , if^#(false(), var(K), var(L)) -> c_18(L) , if^#(true(), var(K), var(L)) -> c_19(K) , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(false(), false()) -> c_1() , and^#(false(), true()) -> c_2() , and^#(true(), false()) -> c_3() , and^#(true(), true()) -> c_4() , eq^#(nil(), nil()) -> c_5() , eq^#(nil(), cons(T, L)) -> c_6() , eq^#(cons(T, L), nil()) -> c_7() , eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , eq^#(var(L), apply(T, S)) -> c_10() , eq^#(var(L), lambda(X, T)) -> c_11() , eq^#(apply(T, S), var(L)) -> c_12() , eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , eq^#(lambda(X, T), var(L)) -> c_15() , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() , eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) , if^#(false(), var(K), var(L)) -> c_18(L) , if^#(true(), var(K), var(L)) -> c_19(K) , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) } Strict Trs: { and(false(), false()) -> false() , and(false(), true()) -> false() , and(true(), false()) -> false() , and(true(), true()) -> true() , eq(nil(), nil()) -> true() , eq(nil(), cons(T, L)) -> false() , eq(cons(T, L), nil()) -> false() , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) , eq(var(L), var(Lp)) -> eq(L, Lp) , eq(var(L), apply(T, S)) -> false() , eq(var(L), lambda(X, T)) -> false() , eq(apply(T, S), var(L)) -> false() , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) , eq(apply(T, S), lambda(X, Tp)) -> false() , eq(lambda(X, T), var(L)) -> false() , eq(lambda(X, T), apply(Tp, Sp)) -> false() , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) , if(false(), var(K), var(L)) -> var(L) , if(true(), var(K), var(L)) -> var(K) , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) , ren(X, Y, lambda(Z, T)) -> lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,5,6,7,10,11,12,14,15,16} by applications of Pre({1,2,3,4,5,6,7,10,11,12,14,15,16}) = {8,9,13,17,18,19,21}. Here rules are labeled as follows: DPs: { 1: and^#(false(), false()) -> c_1() , 2: and^#(false(), true()) -> c_2() , 3: and^#(true(), false()) -> c_3() , 4: and^#(true(), true()) -> c_4() , 5: eq^#(nil(), nil()) -> c_5() , 6: eq^#(nil(), cons(T, L)) -> c_6() , 7: eq^#(cons(T, L), nil()) -> c_7() , 8: eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , 9: eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , 10: eq^#(var(L), apply(T, S)) -> c_10() , 11: eq^#(var(L), lambda(X, T)) -> c_11() , 12: eq^#(apply(T, S), var(L)) -> c_12() , 13: eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , 14: eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , 15: eq^#(lambda(X, T), var(L)) -> c_15() , 16: eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() , 17: eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) , 18: if^#(false(), var(K), var(L)) -> c_18(L) , 19: if^#(true(), var(K), var(L)) -> c_19(K) , 20: ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , 21: ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , 22: ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) , if^#(false(), var(K), var(L)) -> c_18(L) , if^#(true(), var(K), var(L)) -> c_19(K) , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) } Strict Trs: { and(false(), false()) -> false() , and(false(), true()) -> false() , and(true(), false()) -> false() , and(true(), true()) -> true() , eq(nil(), nil()) -> true() , eq(nil(), cons(T, L)) -> false() , eq(cons(T, L), nil()) -> false() , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) , eq(var(L), var(Lp)) -> eq(L, Lp) , eq(var(L), apply(T, S)) -> false() , eq(var(L), lambda(X, T)) -> false() , eq(apply(T, S), var(L)) -> false() , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) , eq(apply(T, S), lambda(X, Tp)) -> false() , eq(lambda(X, T), var(L)) -> false() , eq(lambda(X, T), apply(Tp, Sp)) -> false() , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) , if(false(), var(K), var(L)) -> var(L) , if(true(), var(K), var(L)) -> var(K) , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) , ren(X, Y, lambda(Z, T)) -> lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } Weak DPs: { and^#(false(), false()) -> c_1() , and^#(false(), true()) -> c_2() , and^#(true(), false()) -> c_3() , and^#(true(), true()) -> c_4() , eq^#(nil(), nil()) -> c_5() , eq^#(nil(), cons(T, L)) -> c_6() , eq^#(cons(T, L), nil()) -> c_7() , eq^#(var(L), apply(T, S)) -> c_10() , eq^#(var(L), lambda(X, T)) -> c_11() , eq^#(apply(T, S), var(L)) -> c_12() , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , eq^#(lambda(X, T), var(L)) -> c_15() , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,3,4} by applications of Pre({1,3,4}) = {2,5,6,8}. Here rules are labeled as follows: DPs: { 1: eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , 2: eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , 3: eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , 4: eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) , 5: if^#(false(), var(K), var(L)) -> c_18(L) , 6: if^#(true(), var(K), var(L)) -> c_19(K) , 7: ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , 8: ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , 9: ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) , 10: and^#(false(), false()) -> c_1() , 11: and^#(false(), true()) -> c_2() , 12: and^#(true(), false()) -> c_3() , 13: and^#(true(), true()) -> c_4() , 14: eq^#(nil(), nil()) -> c_5() , 15: eq^#(nil(), cons(T, L)) -> c_6() , 16: eq^#(cons(T, L), nil()) -> c_7() , 17: eq^#(var(L), apply(T, S)) -> c_10() , 18: eq^#(var(L), lambda(X, T)) -> c_11() , 19: eq^#(apply(T, S), var(L)) -> c_12() , 20: eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , 21: eq^#(lambda(X, T), var(L)) -> c_15() , 22: eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { eq^#(var(L), var(Lp)) -> c_9(eq^#(L, Lp)) , if^#(false(), var(K), var(L)) -> c_18(L) , if^#(true(), var(K), var(L)) -> c_19(K) , ren^#(X, Y, apply(T, S)) -> c_20(ren^#(X, Y, T), ren^#(X, Y, S)) , ren^#(X, Y, lambda(Z, T)) -> c_21(X, Y, Z, T, ren^#(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren^#(var(L), var(K), var(Lp)) -> c_22(if^#(eq(L, Lp), var(K), var(Lp))) } Strict Trs: { and(false(), false()) -> false() , and(false(), true()) -> false() , and(true(), false()) -> false() , and(true(), true()) -> true() , eq(nil(), nil()) -> true() , eq(nil(), cons(T, L)) -> false() , eq(cons(T, L), nil()) -> false() , eq(cons(T, L), cons(Tp, Lp)) -> and(eq(T, Tp), eq(L, Lp)) , eq(var(L), var(Lp)) -> eq(L, Lp) , eq(var(L), apply(T, S)) -> false() , eq(var(L), lambda(X, T)) -> false() , eq(apply(T, S), var(L)) -> false() , eq(apply(T, S), apply(Tp, Sp)) -> and(eq(T, Tp), eq(S, Sp)) , eq(apply(T, S), lambda(X, Tp)) -> false() , eq(lambda(X, T), var(L)) -> false() , eq(lambda(X, T), apply(Tp, Sp)) -> false() , eq(lambda(X, T), lambda(Xp, Tp)) -> and(eq(T, Tp), eq(X, Xp)) , if(false(), var(K), var(L)) -> var(L) , if(true(), var(K), var(L)) -> var(K) , ren(X, Y, apply(T, S)) -> apply(ren(X, Y, T), ren(X, Y, S)) , ren(X, Y, lambda(Z, T)) -> lambda(var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), ren(X, Y, ren(Z, var(cons(X, cons(Y, cons(lambda(Z, T), nil())))), T))) , ren(var(L), var(K), var(Lp)) -> if(eq(L, Lp), var(K), var(Lp)) } Weak DPs: { and^#(false(), false()) -> c_1() , and^#(false(), true()) -> c_2() , and^#(true(), false()) -> c_3() , and^#(true(), true()) -> c_4() , eq^#(nil(), nil()) -> c_5() , eq^#(nil(), cons(T, L)) -> c_6() , eq^#(cons(T, L), nil()) -> c_7() , eq^#(cons(T, L), cons(Tp, Lp)) -> c_8(and^#(eq(T, Tp), eq(L, Lp))) , eq^#(var(L), apply(T, S)) -> c_10() , eq^#(var(L), lambda(X, T)) -> c_11() , eq^#(apply(T, S), var(L)) -> c_12() , eq^#(apply(T, S), apply(Tp, Sp)) -> c_13(and^#(eq(T, Tp), eq(S, Sp))) , eq^#(apply(T, S), lambda(X, Tp)) -> c_14() , eq^#(lambda(X, T), var(L)) -> c_15() , eq^#(lambda(X, T), apply(Tp, Sp)) -> c_16() , eq^#(lambda(X, T), lambda(Xp, Tp)) -> c_17(and^#(eq(T, Tp), eq(X, Xp))) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..