MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: app#2(Cons(x6,x4),Cons(x2,Nil())) -> Cons(x6,app#2(x4,Cons(x2,Nil()))) app#2(Nil(),Cons(x2,Nil())) -> Cons(x2,Nil()) cond_deleteMin_ts(Pair(Node(x4,x3,x2),x1)) -> merge#2(rev#1(x2),x1) cond_insTree_t_xs_1(False(),Node(S(x9),x8,Cons(Node(x4,x5,x6),x7)),Node(x3,x2,x1),Nil()) -> Cons(link#2(Node(S(x9),x8,Cons(Node(x4,x5,x6),x7)),Node(x3,x2,x1)),Nil()) cond_insTree_t_xs_1(True(),Node(S(x10),x9,Cons(Node(x5,x6,x7),x8)),Node(x4,x3,x2),x1) -> Cons(Node(S(x10) ,x9 ,Cons(Node(x5 ,x6 ,x7) ,x8)) ,Cons(Node(x4 ,x3 ,x2) ,x1)) cond_link_t1_t2_2(False(),Node(x9,x10,x11),Node(x6,x7,x8),x5,x4,x3,x2,x1) -> Node(S(x5) ,x2 ,Cons(Node(x9,x10,x11),x1)) cond_link_t1_t2_2(True(),Node(x9,x10,x11),Node(x6,x7,x8),x5,x4,x3,x2,x1) -> Node(S(x5) ,x4 ,Cons(Node(x6,x7,x8),x3)) cond_merge_ts1_ts2_2(False() ,Cons(Node(x14,x15,x16),x13) ,Cons(Node(x10,x11,x12),x9) ,Node(x8,x7,x6) ,x5 ,Node(x4,x3,x2) ,x1) -> cond_merge_ts1_ts2_3(lt#2(x4,x8) ,Cons(Node(x14,x15,x16),x13) ,Node(x8,x7,x6) ,x5 ,Node(x4,x3,x2) ,x1) cond_merge_ts1_ts2_2(True() ,Cons(Node(x14,x15,x16),x13) ,Cons(Node(x10,x11,x12),x9) ,Node(x6,x7,x8) ,x5 ,Node(x2,x3,x4) ,x1) -> Cons(Node(x6,x7,x8),merge#2(x5,Cons(Node(x10,x11,x12),x9))) cond_merge_ts1_ts2_3(False(),Cons(Node(x10,x11,x12),x9),Node(x6,x7,x8),x5,Node(x2,x3,x4),x1) -> insTree#2(link#2(Node(x6,x7,x8),Node(x2,x3,x4)),merge#2(x5,x1)) cond_merge_ts1_ts2_3(True(),Cons(Node(x10,x11,x12),x9),Node(x6,x7,x8),x5,Node(x2,x3,x4),x1) -> Cons(Node(x2 ,x3 ,x4) ,merge#2(Cons(Node(x10 ,x11 ,x12) ,x9) ,x1)) cond_removeMinTree_xs_2(Pair(Node(x12,x16,x20),x19),Node(x25,x33,x41),Cons(x7,x11)) -> cond_removeMinTree_xs_3(leqElem#2(x33,x16),Node(x25,x33,x41),Cons(x7,x11),Node(x12,x16,x20),x19) cond_removeMinTree_xs_3(False(),Node(x7,x8,x9),Cons(x6,x5),Node(x2,x3,x4),x1) -> Pair(Node(x2,x3,x4) ,Cons(Node(x7,x8,x9),x1)) cond_removeMinTree_xs_3(True(),Node(x7,x8,x9),Cons(x6,x5),Node(x2,x3,x4),x1) -> Pair(Node(x7,x8,x9) ,Cons(x6,x5)) insTree#2(x2,Nil()) -> Cons(x2,Nil()) insTree#2(Node(S(x10),x9,Cons(Node(x5,x6,x7),x8)),Cons(Node(x4,x3,x2),x1)) -> cond_insTree_t_xs_1(lt#2(S(x10),x4),Node(S(x10),x9,Cons(Node(x5,x6,x7),x8)),Node(x4,x3,x2),x1) leq#2(0(),x20) -> True() leq#2(S(x24),0()) -> False() leq#2(S(x4),S(x2)) -> leq#2(x4,x2) leqElem#2(Elem(x4),Elem(x2)) -> leq#2(x4,x2) link#2(Node(x12,x10,x8),Node(x6,x4,x2)) -> cond_link_t1_t2_2(leqElem#2(x10,x4) ,Node(x12,x10,x8) ,Node(x6,x4,x2) ,x12 ,x10 ,x8 ,x4 ,x2) lt#2(0(),0()) -> False() lt#2(0(),S(x20)) -> True() lt#2(S(x20),0()) -> False() lt#2(S(x4),S(x2)) -> lt#2(x4,x2) main(x24) -> cond_deleteMin_ts(removeMinTree#1(x24)) merge#2(Cons(x4,x2),Nil()) -> Cons(x4,x2) merge#2(Cons(Node(x34,x50,x66),x30),Cons(Node(x16,x24,x32),x14)) -> cond_merge_ts1_ts2_2(lt#2(x34,x16) ,Cons(Node(x34 ,x50 ,x66) ,x30) ,Cons(Node(x16 ,x24 ,x32) ,x14) ,Node(x34,x50,x66) ,x30 ,Node(x16,x24,x32) ,x14) merge#2(Nil(),x2) -> x2 removeMinTree#1(Cons(x1,Nil())) -> Pair(x1,Nil()) removeMinTree#1(Cons(x3,Cons(x2,x1))) -> cond_removeMinTree_xs_2(removeMinTree#1(Cons(x2,x1)) ,x3 ,Cons(x2,x1)) rev#1(Cons(x2,x1)) -> app#2(rev#1(x1),Cons(x2,Nil())) rev#1(Nil()) -> Nil() - Signature: {app#2/2,cond_deleteMin_ts/1,cond_insTree_t_xs_1/4,cond_link_t1_t2_2/8,cond_merge_ts1_ts2_2/7 ,cond_merge_ts1_ts2_3/6,cond_removeMinTree_xs_2/3,cond_removeMinTree_xs_3/5,insTree#2/2,leq#2/2,leqElem#2/2 ,link#2/2,lt#2/2,main/1,merge#2/2,removeMinTree#1/1,rev#1/1} / {0/0,Cons/2,Elem/1,False/0,Nil/0,Node/3 ,Pair/2,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {app#2,cond_deleteMin_ts,cond_insTree_t_xs_1 ,cond_link_t1_t2_2,cond_merge_ts1_ts2_2,cond_merge_ts1_ts2_3,cond_removeMinTree_xs_2,cond_removeMinTree_xs_3 ,insTree#2,leq#2,leqElem#2,link#2,lt#2,main,merge#2,removeMinTree#1,rev#1} and constructors {0,Cons,Elem ,False,Nil,Node,Pair,S,True} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE