MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { and(true(), y) -> y , and(false(), y) -> false() , eq(nil(), nil()) -> true() , eq(nil(), cons(t, l)) -> false() , eq(cons(t, l), nil()) -> false() , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')) , eq(var(l), var(l')) -> eq(l, l') , 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(t', s')) -> and(eq(t, t'), eq(s, s')) , eq(apply(t, s), lambda(x, t)) -> false() , eq(lambda(x, t), var(l)) -> false() , eq(lambda(x, t), apply(t, s)) -> false() , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')) , if(true(), var(k), var(l')) -> var(k) , if(false(), var(k), var(l')) -> var(l') , 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(l')) -> if(eq(l, l'), var(k), var(l')) } 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) '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 2) '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 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: { and^#(true(), y) -> c_1(y) , and^#(false(), y) -> c_2() , eq^#(nil(), nil()) -> c_3() , eq^#(nil(), cons(t, l)) -> c_4() , eq^#(cons(t, l), nil()) -> c_5() , eq^#(cons(t, l), cons(t', l')) -> c_6(and^#(eq(t, t'), eq(l, l'))) , eq^#(var(l), var(l')) -> c_7(eq^#(l, l')) , eq^#(var(l), apply(t, s)) -> c_8() , eq^#(var(l), lambda(x, t)) -> c_9() , eq^#(apply(t, s), var(l)) -> c_10() , eq^#(apply(t, s), apply(t', s')) -> c_11(and^#(eq(t, t'), eq(s, s'))) , eq^#(apply(t, s), lambda(x, t)) -> c_12() , eq^#(lambda(x, t), var(l)) -> c_13() , eq^#(lambda(x, t), apply(t, s)) -> c_14() , eq^#(lambda(x, t), lambda(x', t')) -> c_15(and^#(eq(x, x'), eq(t, t'))) , if^#(true(), var(k), var(l')) -> c_16(k) , if^#(false(), var(k), var(l')) -> c_17(l') , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s)) , ren^#(x, y, lambda(z, t)) -> c_19(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(l')) -> c_20(if^#(eq(l, l'), var(k), var(l'))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(true(), y) -> c_1(y) , and^#(false(), y) -> c_2() , eq^#(nil(), nil()) -> c_3() , eq^#(nil(), cons(t, l)) -> c_4() , eq^#(cons(t, l), nil()) -> c_5() , eq^#(cons(t, l), cons(t', l')) -> c_6(and^#(eq(t, t'), eq(l, l'))) , eq^#(var(l), var(l')) -> c_7(eq^#(l, l')) , eq^#(var(l), apply(t, s)) -> c_8() , eq^#(var(l), lambda(x, t)) -> c_9() , eq^#(apply(t, s), var(l)) -> c_10() , eq^#(apply(t, s), apply(t', s')) -> c_11(and^#(eq(t, t'), eq(s, s'))) , eq^#(apply(t, s), lambda(x, t)) -> c_12() , eq^#(lambda(x, t), var(l)) -> c_13() , eq^#(lambda(x, t), apply(t, s)) -> c_14() , eq^#(lambda(x, t), lambda(x', t')) -> c_15(and^#(eq(x, x'), eq(t, t'))) , if^#(true(), var(k), var(l')) -> c_16(k) , if^#(false(), var(k), var(l')) -> c_17(l') , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s)) , ren^#(x, y, lambda(z, t)) -> c_19(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(l')) -> c_20(if^#(eq(l, l'), var(k), var(l'))) } Strict Trs: { and(true(), y) -> y , and(false(), y) -> false() , eq(nil(), nil()) -> true() , eq(nil(), cons(t, l)) -> false() , eq(cons(t, l), nil()) -> false() , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')) , eq(var(l), var(l')) -> eq(l, l') , 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(t', s')) -> and(eq(t, t'), eq(s, s')) , eq(apply(t, s), lambda(x, t)) -> false() , eq(lambda(x, t), var(l)) -> false() , eq(lambda(x, t), apply(t, s)) -> false() , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')) , if(true(), var(k), var(l')) -> var(k) , if(false(), var(k), var(l')) -> var(l') , 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(l')) -> if(eq(l, l'), var(k), var(l')) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,3,4,5,8,9,10,12,13,14} by applications of Pre({2,3,4,5,8,9,10,12,13,14}) = {1,6,7,11,15,16,17,19}. Here rules are labeled as follows: DPs: { 1: and^#(true(), y) -> c_1(y) , 2: and^#(false(), y) -> c_2() , 3: eq^#(nil(), nil()) -> c_3() , 4: eq^#(nil(), cons(t, l)) -> c_4() , 5: eq^#(cons(t, l), nil()) -> c_5() , 6: eq^#(cons(t, l), cons(t', l')) -> c_6(and^#(eq(t, t'), eq(l, l'))) , 7: eq^#(var(l), var(l')) -> c_7(eq^#(l, l')) , 8: eq^#(var(l), apply(t, s)) -> c_8() , 9: eq^#(var(l), lambda(x, t)) -> c_9() , 10: eq^#(apply(t, s), var(l)) -> c_10() , 11: eq^#(apply(t, s), apply(t', s')) -> c_11(and^#(eq(t, t'), eq(s, s'))) , 12: eq^#(apply(t, s), lambda(x, t)) -> c_12() , 13: eq^#(lambda(x, t), var(l)) -> c_13() , 14: eq^#(lambda(x, t), apply(t, s)) -> c_14() , 15: eq^#(lambda(x, t), lambda(x', t')) -> c_15(and^#(eq(x, x'), eq(t, t'))) , 16: if^#(true(), var(k), var(l')) -> c_16(k) , 17: if^#(false(), var(k), var(l')) -> c_17(l') , 18: ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s)) , 19: ren^#(x, y, lambda(z, t)) -> c_19(x, y, z, t, ren^#(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil())))), t))) , 20: ren^#(var(l), var(k), var(l')) -> c_20(if^#(eq(l, l'), var(k), var(l'))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { and^#(true(), y) -> c_1(y) , eq^#(cons(t, l), cons(t', l')) -> c_6(and^#(eq(t, t'), eq(l, l'))) , eq^#(var(l), var(l')) -> c_7(eq^#(l, l')) , eq^#(apply(t, s), apply(t', s')) -> c_11(and^#(eq(t, t'), eq(s, s'))) , eq^#(lambda(x, t), lambda(x', t')) -> c_15(and^#(eq(x, x'), eq(t, t'))) , if^#(true(), var(k), var(l')) -> c_16(k) , if^#(false(), var(k), var(l')) -> c_17(l') , ren^#(x, y, apply(t, s)) -> c_18(ren^#(x, y, t), ren^#(x, y, s)) , ren^#(x, y, lambda(z, t)) -> c_19(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(l')) -> c_20(if^#(eq(l, l'), var(k), var(l'))) } Strict Trs: { and(true(), y) -> y , and(false(), y) -> false() , eq(nil(), nil()) -> true() , eq(nil(), cons(t, l)) -> false() , eq(cons(t, l), nil()) -> false() , eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l')) , eq(var(l), var(l')) -> eq(l, l') , 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(t', s')) -> and(eq(t, t'), eq(s, s')) , eq(apply(t, s), lambda(x, t)) -> false() , eq(lambda(x, t), var(l)) -> false() , eq(lambda(x, t), apply(t, s)) -> false() , eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t')) , if(true(), var(k), var(l')) -> var(k) , if(false(), var(k), var(l')) -> var(l') , 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(l')) -> if(eq(l, l'), var(k), var(l')) } Weak DPs: { and^#(false(), y) -> c_2() , eq^#(nil(), nil()) -> c_3() , eq^#(nil(), cons(t, l)) -> c_4() , eq^#(cons(t, l), nil()) -> c_5() , eq^#(var(l), apply(t, s)) -> c_8() , eq^#(var(l), lambda(x, t)) -> c_9() , eq^#(apply(t, s), var(l)) -> c_10() , eq^#(apply(t, s), lambda(x, t)) -> c_12() , eq^#(lambda(x, t), var(l)) -> c_13() , eq^#(lambda(x, t), apply(t, s)) -> c_14() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..