0.002/0.002 NO 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S s:S x:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (*top*_0 1) 0.002/0.002 (M_1) 0.002/0.002 (cons_1) 0.002/0.002 (cons_10) 0.002/0.002 (cons_11) 0.002/0.002 (cons_2) 0.002/0.002 (cons_3) 0.002/0.002 (cons_4) 0.002/0.002 (cons_5) 0.002/0.002 (cons_6) 0.002/0.002 (cons_7) 0.002/0.002 (cons_8) 0.002/0.002 (cons_9) 0.002/0.002 (h_0 1) 0.002/0.002 (tail_0 1) 0.002/0.002 (tail_1) 0.002/0.002 (0_0) 0.002/0.002 (1_0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (garbage_collection_0) 0.002/0.002 (h_1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 *top*_0(tail_1(cons_1(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_10(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_11(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_5(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_6(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(h_1(cons_1(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_1(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_10(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_11(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_2(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_3(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_4(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_5(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_6(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_7(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_8(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_9(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 M_1 -> h_1(cons_1(0_0,tail_0(M_1))) 0.002/0.002 cons_1(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_10(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_11(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_2(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_3(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_4(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_5(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_6(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_7(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_8(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_9(x:S,s:S) -> garbage_collection_0 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_0(s:S) 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_10(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_11(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_5(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_6(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(h_1(cons_1(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_1(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_10(1_0,s:S))) -> h_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_11(1_0,s:S))) -> h_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_2(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_3(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_4(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_5(0_0,s:S))) -> h_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_6(0_0,s:S))) -> h_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_7(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_8(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_9(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(tail_1(cons_1(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_10(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_11(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_5(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_6(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(h_1(cons_1(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_1(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_10(1_0,s:S))) -> tail_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_11(1_0,s:S))) -> tail_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_2(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_3(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_4(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_5(0_0,s:S))) -> tail_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_6(0_0,s:S))) -> tail_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_7(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_8(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_9(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_1(cons_1(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_2(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_3(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_4(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_7(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_8(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_9(x:S,s:S)) -> s:S 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 CleanTRS Processor: 0.002/0.002 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S s:S x:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (*top*_0 1) 0.002/0.002 (M_1) 0.002/0.002 (cons_1) 0.002/0.002 (cons_10) 0.002/0.002 (cons_11) 0.002/0.002 (cons_2) 0.002/0.002 (cons_3) 0.002/0.002 (cons_4) 0.002/0.002 (cons_5) 0.002/0.002 (cons_6) 0.002/0.002 (cons_7) 0.002/0.002 (cons_8) 0.002/0.002 (cons_9) 0.002/0.002 (h_0 1) 0.002/0.002 (tail_0 1) 0.002/0.002 (tail_1) 0.002/0.002 (0_0) 0.002/0.002 (1_0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (garbage_collection_0) 0.002/0.002 (h_1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 *top*_0(tail_1(cons_1(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_10(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_11(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_5(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_6(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(h_1(cons_1(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_1(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_10(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_11(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_2(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_3(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_4(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_5(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_6(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_7(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_8(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_9(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 M_1 -> h_1(cons_1(0_0,tail_0(M_1))) 0.002/0.002 cons_1(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_10(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_11(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_2(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_3(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_4(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_5(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_6(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_7(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_8(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_9(x:S,s:S) -> garbage_collection_0 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_0(s:S) 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_10(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_11(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_5(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_6(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(h_1(cons_1(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_1(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_10(1_0,s:S))) -> h_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_11(1_0,s:S))) -> h_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_2(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_3(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_4(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_5(0_0,s:S))) -> h_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_6(0_0,s:S))) -> h_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_7(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_8(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_9(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(tail_1(cons_1(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_10(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_11(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_5(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_6(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(h_1(cons_1(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_1(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_10(1_0,s:S))) -> tail_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_11(1_0,s:S))) -> tail_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_2(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_3(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_4(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_5(0_0,s:S))) -> tail_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_6(0_0,s:S))) -> tail_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_7(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_8(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_9(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_1(cons_1(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_2(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_3(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_4(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_7(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_8(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_9(x:S,s:S)) -> s:S 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 0.002/0.002 Modular Confluence Combinations Decomposition Processor: 0.002/0.002 It is a CTRS -> No modular confluence 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 Left-Homogeneous u-Replacing Variables Processor: 0.002/0.002 R satisfies LHRV condition 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 Confluence Problem: 0.002/0.002 (VAR vNonEmpty:S s:S x:S) 0.002/0.002 (STRATEGY CONTEXTSENSITIVE 0.002/0.002 (*top*_0 1) 0.002/0.002 (M_1) 0.002/0.002 (cons_1) 0.002/0.002 (cons_10) 0.002/0.002 (cons_11) 0.002/0.002 (cons_2) 0.002/0.002 (cons_3) 0.002/0.002 (cons_4) 0.002/0.002 (cons_5) 0.002/0.002 (cons_6) 0.002/0.002 (cons_7) 0.002/0.002 (cons_8) 0.002/0.002 (cons_9) 0.002/0.002 (h_0 1) 0.002/0.002 (tail_0 1) 0.002/0.002 (tail_1) 0.002/0.002 (0_0) 0.002/0.002 (1_0) 0.002/0.002 (fSNonEmpty) 0.002/0.002 (garbage_collection_0) 0.002/0.002 (h_1) 0.002/0.002 ) 0.002/0.002 (RULES 0.002/0.002 *top*_0(tail_1(cons_1(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_10(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_11(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_5(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_6(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(h_1(cons_1(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_1(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_10(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_11(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_2(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_3(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_4(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_5(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_6(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_7(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_8(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_9(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 M_1 -> h_1(cons_1(0_0,tail_0(M_1))) 0.002/0.002 cons_1(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_10(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_11(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_2(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_3(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_4(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_5(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_6(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_7(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_8(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_9(x:S,s:S) -> garbage_collection_0 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_0(s:S) 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_10(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_11(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_5(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_6(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(h_1(cons_1(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_1(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_10(1_0,s:S))) -> h_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_11(1_0,s:S))) -> h_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_2(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_3(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_4(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_5(0_0,s:S))) -> h_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_6(0_0,s:S))) -> h_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_7(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_8(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_9(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(tail_1(cons_1(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_10(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_11(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_5(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_6(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(h_1(cons_1(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_1(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_10(1_0,s:S))) -> tail_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_11(1_0,s:S))) -> tail_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_2(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_3(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_4(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_5(0_0,s:S))) -> tail_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_6(0_0,s:S))) -> tail_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_7(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_8(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_9(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_1(cons_1(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_2(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_3(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_4(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_7(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_8(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_9(x:S,s:S)) -> s:S 0.002/0.002 ) 0.002/0.002 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.002/0.002 0.002/0.002 Huet Levy Processor: 0.002/0.002 -> Rules: 0.002/0.002 *top*_0(tail_1(cons_1(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_10(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_11(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_5(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(tail_1(cons_6(x:S,s:S))) -> *top*_0(s:S) 0.002/0.002 *top*_0(h_1(cons_1(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_1(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_10(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_11(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_2(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_3(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_4(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_5(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_6(0_0,s:S))) -> *top*_0(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 *top*_0(h_1(cons_7(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_8(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 *top*_0(h_1(cons_9(1_0,s:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 M_1 -> h_1(cons_1(0_0,tail_0(M_1))) 0.002/0.002 cons_1(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_10(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_11(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_2(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_3(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_4(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_5(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_6(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_7(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_8(x:S,s:S) -> garbage_collection_0 0.002/0.002 cons_9(x:S,s:S) -> garbage_collection_0 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_0(s:S) 0.002/0.002 h_0(tail_1(cons_1(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_10(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_11(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_5(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(tail_1(cons_6(x:S,s:S))) -> h_1(s:S) 0.002/0.002 h_0(h_1(cons_1(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_1(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_10(1_0,s:S))) -> h_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_11(1_0,s:S))) -> h_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_2(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_3(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_4(0_0,s:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_5(0_0,s:S))) -> h_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_6(0_0,s:S))) -> h_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 h_0(h_1(cons_7(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_8(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 h_0(h_1(cons_9(1_0,s:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(tail_1(cons_1(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_10(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_11(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_5(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(tail_1(cons_6(x:S,s:S))) -> tail_1(s:S) 0.002/0.002 tail_0(h_1(cons_1(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_1(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_10(1_0,s:S))) -> tail_1(cons_10(1_0,cons_2(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_11(1_0,s:S))) -> tail_1(cons_10(1_0,cons_3(0_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_2(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_3(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_4(0_0,s:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_5(0_0,s:S))) -> tail_1(cons_6(0_0,cons_7(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_6(0_0,s:S))) -> tail_1(cons_6(0_0,cons_8(1_0,h_1(s:S)))) 0.002/0.002 tail_0(h_1(cons_7(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_8(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_0(h_1(cons_9(1_0,s:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(s:S)))) 0.002/0.002 tail_1(cons_1(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_2(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_3(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_4(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_7(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_8(x:S,s:S)) -> s:S 0.002/0.002 tail_1(cons_9(x:S,s:S)) -> s:S 0.002/0.002 -> Vars: 0.002/0.002 s, x, s, x, s, x, s, x, s, x, s, s, s, s, s, s, s, s, s, s, s, s, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, x, s, s, s, s, s, s, s, s, s, s, s, s, s, x, s, x, s, x, s, x, s, x, s, s, s, s, s, s, s, s, s, s, s, s, s, x, s, x, s, x, s, x, s, x, s, x, s, x 0.002/0.002 -> UVars: 0.002/0.002 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 50, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s, x], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 59, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 62, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 63, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 64, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s], UV-RFrozen: [s]) 0.002/0.002 (UV-RuleId: 65, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 66, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 67, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 68, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 69, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 70, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 (UV-RuleId: 71, UV-LActive: [], UV-RActive: [s], UV-LFrozen: [s, x], UV-RFrozen: []) 0.002/0.002 -> FVars: 0.002/0.002 x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x94, x95, x96, x97, x98, x99, x100, x101, x102, x103, x104, x105, x106 0.002/0.002 -> PVars: 0.002/0.002 s: [x3, x5, x7, x9, x11, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x27, x29, x31, x33, x35, x37, x39, x41, x43, x45, x47, x49, x51, x53, x55, x57, x59, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x73, x75, x77, x79, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x95, x97, x99, x101, x103, x105], x: [x4, x6, x8, x10, x12, x26, x28, x30, x32, x34, x36, x38, x40, x42, x44, x46, x48, x50, x52, x54, x56, x58, x72, x74, x76, x78, x80, x94, x96, x98, x100, x102, x104, x106] 0.002/0.002 0.002/0.002 -> Rlps: 0.002/0.002 (rule: *top*_0(tail_1(cons_1(x4:S,x3:S))) -> *top*_0(x3:S), id: 1, possubterms: *top*_0(tail_1(cons_1(x4:S,x3:S)))->[], tail_1(cons_1(x4:S,x3:S))->[1]) 0.002/0.002 (rule: *top*_0(tail_1(cons_10(x6:S,x5:S))) -> *top*_0(x5:S), id: 2, possubterms: *top*_0(tail_1(cons_10(x6:S,x5:S)))->[], tail_1(cons_10(x6:S,x5:S))->[1]) 0.002/0.002 (rule: *top*_0(tail_1(cons_11(x8:S,x7:S))) -> *top*_0(x7:S), id: 3, possubterms: *top*_0(tail_1(cons_11(x8:S,x7:S)))->[], tail_1(cons_11(x8:S,x7:S))->[1]) 0.002/0.002 (rule: *top*_0(tail_1(cons_5(x10:S,x9:S))) -> *top*_0(x9:S), id: 4, possubterms: *top*_0(tail_1(cons_5(x10:S,x9:S)))->[], tail_1(cons_5(x10:S,x9:S))->[1]) 0.002/0.002 (rule: *top*_0(tail_1(cons_6(x12:S,x11:S))) -> *top*_0(x11:S), id: 5, possubterms: *top*_0(tail_1(cons_6(x12:S,x11:S)))->[], tail_1(cons_6(x12:S,x11:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_1(0_0,x13:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(x13:S)))), id: 6, possubterms: *top*_0(h_1(cons_1(0_0,x13:S)))->[], h_1(cons_1(0_0,x13:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_1(1_0,x14:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(x14:S)))), id: 7, possubterms: *top*_0(h_1(cons_1(1_0,x14:S)))->[], h_1(cons_1(1_0,x14:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_10(1_0,x15:S))) -> *top*_0(cons_10(1_0,cons_2(0_0,h_1(x15:S)))), id: 8, possubterms: *top*_0(h_1(cons_10(1_0,x15:S)))->[], h_1(cons_10(1_0,x15:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_11(1_0,x16:S))) -> *top*_0(cons_10(1_0,cons_3(0_0,h_1(x16:S)))), id: 9, possubterms: *top*_0(h_1(cons_11(1_0,x16:S)))->[], h_1(cons_11(1_0,x16:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_2(0_0,x17:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(x17:S)))), id: 10, possubterms: *top*_0(h_1(cons_2(0_0,x17:S)))->[], h_1(cons_2(0_0,x17:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_3(0_0,x18:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(x18:S)))), id: 11, possubterms: *top*_0(h_1(cons_3(0_0,x18:S)))->[], h_1(cons_3(0_0,x18:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_4(0_0,x19:S))) -> *top*_0(cons_6(0_0,cons_1(1_0,h_0(x19:S)))), id: 12, possubterms: *top*_0(h_1(cons_4(0_0,x19:S)))->[], h_1(cons_4(0_0,x19:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_5(0_0,x20:S))) -> *top*_0(cons_6(0_0,cons_7(1_0,h_1(x20:S)))), id: 13, possubterms: *top*_0(h_1(cons_5(0_0,x20:S)))->[], h_1(cons_5(0_0,x20:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_6(0_0,x21:S))) -> *top*_0(cons_6(0_0,cons_8(1_0,h_1(x21:S)))), id: 14, possubterms: *top*_0(h_1(cons_6(0_0,x21:S)))->[], h_1(cons_6(0_0,x21:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_7(1_0,x22:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(x22:S)))), id: 15, possubterms: *top*_0(h_1(cons_7(1_0,x22:S)))->[], h_1(cons_7(1_0,x22:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_8(1_0,x23:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(x23:S)))), id: 16, possubterms: *top*_0(h_1(cons_8(1_0,x23:S)))->[], h_1(cons_8(1_0,x23:S))->[1]) 0.002/0.002 (rule: *top*_0(h_1(cons_9(1_0,x24:S))) -> *top*_0(cons_10(1_0,cons_1(0_0,h_0(x24:S)))), id: 17, possubterms: *top*_0(h_1(cons_9(1_0,x24:S)))->[], h_1(cons_9(1_0,x24:S))->[1]) 0.002/0.002 (rule: M_1 -> h_1(cons_1(0_0,tail_0(M_1))), id: 18, possubterms: M_1->[]) 0.002/0.002 (rule: cons_1(x26:S,x25:S) -> garbage_collection_0, id: 19, possubterms: cons_1(x26:S,x25:S)->[]) 0.002/0.002 (rule: cons_10(x28:S,x27:S) -> garbage_collection_0, id: 20, possubterms: cons_10(x28:S,x27:S)->[]) 0.002/0.002 (rule: cons_11(x30:S,x29:S) -> garbage_collection_0, id: 21, possubterms: cons_11(x30:S,x29:S)->[]) 0.002/0.002 (rule: cons_2(x32:S,x31:S) -> garbage_collection_0, id: 22, possubterms: cons_2(x32:S,x31:S)->[]) 0.002/0.002 (rule: cons_3(x34:S,x33:S) -> garbage_collection_0, id: 23, possubterms: cons_3(x34:S,x33:S)->[]) 0.002/0.002 (rule: cons_4(x36:S,x35:S) -> garbage_collection_0, id: 24, possubterms: cons_4(x36:S,x35:S)->[]) 0.002/0.002 (rule: cons_5(x38:S,x37:S) -> garbage_collection_0, id: 25, possubterms: cons_5(x38:S,x37:S)->[]) 0.002/0.002 (rule: cons_6(x40:S,x39:S) -> garbage_collection_0, id: 26, possubterms: cons_6(x40:S,x39:S)->[]) 0.002/0.002 (rule: cons_7(x42:S,x41:S) -> garbage_collection_0, id: 27, possubterms: cons_7(x42:S,x41:S)->[]) 0.002/0.002 (rule: cons_8(x44:S,x43:S) -> garbage_collection_0, id: 28, possubterms: cons_8(x44:S,x43:S)->[]) 0.002/0.002 (rule: cons_9(x46:S,x45:S) -> garbage_collection_0, id: 29, possubterms: cons_9(x46:S,x45:S)->[]) 0.002/0.002 (rule: h_0(tail_1(cons_1(x48:S,x47:S))) -> h_0(x47:S), id: 30, possubterms: h_0(tail_1(cons_1(x48:S,x47:S)))->[], tail_1(cons_1(x48:S,x47:S))->[1]) 0.002/0.002 (rule: h_0(tail_1(cons_1(x50:S,x49:S))) -> h_1(x49:S), id: 31, possubterms: h_0(tail_1(cons_1(x50:S,x49:S)))->[], tail_1(cons_1(x50:S,x49:S))->[1]) 0.002/0.002 (rule: h_0(tail_1(cons_10(x52:S,x51:S))) -> h_1(x51:S), id: 32, possubterms: h_0(tail_1(cons_10(x52:S,x51:S)))->[], tail_1(cons_10(x52:S,x51:S))->[1]) 0.002/0.002 (rule: h_0(tail_1(cons_11(x54:S,x53:S))) -> h_1(x53:S), id: 33, possubterms: h_0(tail_1(cons_11(x54:S,x53:S)))->[], tail_1(cons_11(x54:S,x53:S))->[1]) 0.002/0.002 (rule: h_0(tail_1(cons_5(x56:S,x55:S))) -> h_1(x55:S), id: 34, possubterms: h_0(tail_1(cons_5(x56:S,x55:S)))->[], tail_1(cons_5(x56:S,x55:S))->[1]) 0.002/0.002 (rule: h_0(tail_1(cons_6(x58:S,x57:S))) -> h_1(x57:S), id: 35, possubterms: h_0(tail_1(cons_6(x58:S,x57:S)))->[], tail_1(cons_6(x58:S,x57:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_1(0_0,x59:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(x59:S)))), id: 36, possubterms: h_0(h_1(cons_1(0_0,x59:S)))->[], h_1(cons_1(0_0,x59:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_1(1_0,x60:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(x60:S)))), id: 37, possubterms: h_0(h_1(cons_1(1_0,x60:S)))->[], h_1(cons_1(1_0,x60:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_10(1_0,x61:S))) -> h_1(cons_10(1_0,cons_2(0_0,h_1(x61:S)))), id: 38, possubterms: h_0(h_1(cons_10(1_0,x61:S)))->[], h_1(cons_10(1_0,x61:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_11(1_0,x62:S))) -> h_1(cons_10(1_0,cons_3(0_0,h_1(x62:S)))), id: 39, possubterms: h_0(h_1(cons_11(1_0,x62:S)))->[], h_1(cons_11(1_0,x62:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_2(0_0,x63:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(x63:S)))), id: 40, possubterms: h_0(h_1(cons_2(0_0,x63:S)))->[], h_1(cons_2(0_0,x63:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_3(0_0,x64:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(x64:S)))), id: 41, possubterms: h_0(h_1(cons_3(0_0,x64:S)))->[], h_1(cons_3(0_0,x64:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_4(0_0,x65:S))) -> h_1(cons_6(0_0,cons_1(1_0,h_0(x65:S)))), id: 42, possubterms: h_0(h_1(cons_4(0_0,x65:S)))->[], h_1(cons_4(0_0,x65:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_5(0_0,x66:S))) -> h_1(cons_6(0_0,cons_7(1_0,h_1(x66:S)))), id: 43, possubterms: h_0(h_1(cons_5(0_0,x66:S)))->[], h_1(cons_5(0_0,x66:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_6(0_0,x67:S))) -> h_1(cons_6(0_0,cons_8(1_0,h_1(x67:S)))), id: 44, possubterms: h_0(h_1(cons_6(0_0,x67:S)))->[], h_1(cons_6(0_0,x67:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_7(1_0,x68:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(x68:S)))), id: 45, possubterms: h_0(h_1(cons_7(1_0,x68:S)))->[], h_1(cons_7(1_0,x68:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_8(1_0,x69:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(x69:S)))), id: 46, possubterms: h_0(h_1(cons_8(1_0,x69:S)))->[], h_1(cons_8(1_0,x69:S))->[1]) 0.002/0.002 (rule: h_0(h_1(cons_9(1_0,x70:S))) -> h_1(cons_10(1_0,cons_1(0_0,h_0(x70:S)))), id: 47, possubterms: h_0(h_1(cons_9(1_0,x70:S)))->[], h_1(cons_9(1_0,x70:S))->[1]) 0.002/0.002 (rule: tail_0(tail_1(cons_1(x72:S,x71:S))) -> tail_1(x71:S), id: 48, possubterms: tail_0(tail_1(cons_1(x72:S,x71:S)))->[], tail_1(cons_1(x72:S,x71:S))->[1]) 0.002/0.002 (rule: tail_0(tail_1(cons_10(x74:S,x73:S))) -> tail_1(x73:S), id: 49, possubterms: tail_0(tail_1(cons_10(x74:S,x73:S)))->[], tail_1(cons_10(x74:S,x73:S))->[1]) 0.002/0.002 (rule: tail_0(tail_1(cons_11(x76:S,x75:S))) -> tail_1(x75:S), id: 50, possubterms: tail_0(tail_1(cons_11(x76:S,x75:S)))->[], tail_1(cons_11(x76:S,x75:S))->[1]) 0.002/0.002 (rule: tail_0(tail_1(cons_5(x78:S,x77:S))) -> tail_1(x77:S), id: 51, possubterms: tail_0(tail_1(cons_5(x78:S,x77:S)))->[], tail_1(cons_5(x78:S,x77:S))->[1]) 0.002/0.002 (rule: tail_0(tail_1(cons_6(x80:S,x79:S))) -> tail_1(x79:S), id: 52, possubterms: tail_0(tail_1(cons_6(x80:S,x79:S)))->[], tail_1(cons_6(x80:S,x79:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_1(0_0,x81:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(x81:S)))), id: 53, possubterms: tail_0(h_1(cons_1(0_0,x81:S)))->[], h_1(cons_1(0_0,x81:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_1(1_0,x82:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(x82:S)))), id: 54, possubterms: tail_0(h_1(cons_1(1_0,x82:S)))->[], h_1(cons_1(1_0,x82:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_10(1_0,x83:S))) -> tail_1(cons_10(1_0,cons_2(0_0,h_1(x83:S)))), id: 55, possubterms: tail_0(h_1(cons_10(1_0,x83:S)))->[], h_1(cons_10(1_0,x83:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_11(1_0,x84:S))) -> tail_1(cons_10(1_0,cons_3(0_0,h_1(x84:S)))), id: 56, possubterms: tail_0(h_1(cons_11(1_0,x84:S)))->[], h_1(cons_11(1_0,x84:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_2(0_0,x85:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(x85:S)))), id: 57, possubterms: tail_0(h_1(cons_2(0_0,x85:S)))->[], h_1(cons_2(0_0,x85:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_3(0_0,x86:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(x86:S)))), id: 58, possubterms: tail_0(h_1(cons_3(0_0,x86:S)))->[], h_1(cons_3(0_0,x86:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_4(0_0,x87:S))) -> tail_1(cons_6(0_0,cons_1(1_0,h_0(x87:S)))), id: 59, possubterms: tail_0(h_1(cons_4(0_0,x87:S)))->[], h_1(cons_4(0_0,x87:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_5(0_0,x88:S))) -> tail_1(cons_6(0_0,cons_7(1_0,h_1(x88:S)))), id: 60, possubterms: tail_0(h_1(cons_5(0_0,x88:S)))->[], h_1(cons_5(0_0,x88:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_6(0_0,x89:S))) -> tail_1(cons_6(0_0,cons_8(1_0,h_1(x89:S)))), id: 61, possubterms: tail_0(h_1(cons_6(0_0,x89:S)))->[], h_1(cons_6(0_0,x89:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_7(1_0,x90:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(x90:S)))), id: 62, possubterms: tail_0(h_1(cons_7(1_0,x90:S)))->[], h_1(cons_7(1_0,x90:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_8(1_0,x91:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(x91:S)))), id: 63, possubterms: tail_0(h_1(cons_8(1_0,x91:S)))->[], h_1(cons_8(1_0,x91:S))->[1]) 0.002/0.002 (rule: tail_0(h_1(cons_9(1_0,x92:S))) -> tail_1(cons_10(1_0,cons_1(0_0,h_0(x92:S)))), id: 64, possubterms: tail_0(h_1(cons_9(1_0,x92:S)))->[], h_1(cons_9(1_0,x92:S))->[1]) 0.002/0.002 (rule: tail_1(cons_1(x94:S,x93:S)) -> x93:S, id: 65, possubterms: tail_1(cons_1(x94:S,x93:S))->[]) 0.002/0.002 (rule: tail_1(cons_2(x96:S,x95:S)) -> x95:S, id: 66, possubterms: tail_1(cons_2(x96:S,x95:S))->[]) 0.002/0.002 (rule: tail_1(cons_3(x98:S,x97:S)) -> x97:S, id: 67, possubterms: tail_1(cons_3(x98:S,x97:S))->[]) 0.002/0.002 (rule: tail_1(cons_4(x100:S,x99:S)) -> x99:S, id: 68, possubterms: tail_1(cons_4(x100:S,x99:S))->[]) 0.002/0.002 (rule: tail_1(cons_7(x102:S,x101:S)) -> x101:S, id: 69, possubterms: tail_1(cons_7(x102:S,x101:S))->[]) 0.002/0.002 (rule: tail_1(cons_8(x104:S,x103:S)) -> x103:S, id: 70, possubterms: tail_1(cons_8(x104:S,x103:S))->[]) 0.002/0.002 (rule: tail_1(cons_9(x106:S,x105:S)) -> x105:S, id: 71, possubterms: tail_1(cons_9(x106:S,x105:S))->[]) 0.002/0.002 0.002/0.002 -> Unifications: 0.002/0.002 (R1 unifies with R65 at p: [1], l: *top*_0(tail_1(cons_1(x4:S,x3:S))), lp: tail_1(cons_1(x4:S,x3:S)), sig: {x3:S -> s:S,x4:S -> x:S}, l': tail_1(cons_1(x:S,s:S)), r: *top*_0(x3:S), r': s:S) 0.002/0.002 (R30 unifies with R65 at p: [1], l: h_0(tail_1(cons_1(x48:S,x47:S))), lp: tail_1(cons_1(x48:S,x47:S)), sig: {x47:S -> s:S,x48:S -> x:S}, l': tail_1(cons_1(x:S,s:S)), r: h_0(x47:S), r': s:S) 0.002/0.002 (R31 unifies with R30 at p: [], l: h_0(tail_1(cons_1(x50:S,x49:S))), lp: h_0(tail_1(cons_1(x50:S,x49:S))), sig: {x49:S -> s:S,x50:S -> x:S}, l': h_0(tail_1(cons_1(x:S,s:S))), r: h_1(x49:S), r': h_0(s:S)) 0.002/0.002 (R31 unifies with R65 at p: [1], l: h_0(tail_1(cons_1(x50:S,x49:S))), lp: tail_1(cons_1(x50:S,x49:S)), sig: {x49:S -> s:S,x50:S -> x:S}, l': tail_1(cons_1(x:S,s:S)), r: h_1(x49:S), r': s:S) 0.002/0.002 (R48 unifies with R65 at p: [1], l: tail_0(tail_1(cons_1(x72:S,x71:S))), lp: tail_1(cons_1(x72:S,x71:S)), sig: {x71:S -> s:S,x72:S -> x:S}, l': tail_1(cons_1(x:S,s:S)), r: tail_1(x71:S), r': s:S) 0.002/0.002 0.002/0.002 -> Critical pairs info: 0.002/0.002 => Not trivial, Not overlay, NW0, N1 0.002/0.002 => Trivial, Not overlay, NW0, N2 0.002/0.002 <*top*_0(s:S),*top*_0(s:S)> => Trivial, Not overlay, NW0, N3 0.002/0.002 => Not trivial, Not overlay, NW0, N4 0.002/0.002 => Not trivial, Overlay, NW0, N5 0.002/0.002 0.002/0.002 -> Problem conclusions: 0.002/0.002 Left linear, Right linear, Linear 0.002/0.002 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.002/0.002 Not Huet-Levy confluent, Not Newman confluent 0.002/0.002 R is a CS-TRS, Left-homogeneous u-replacing variables 0.002/0.002 0.002/0.002 0.002/0.002 Problem 1: 0.002/0.002 Different Normal CP Terms Processor: 0.002/0.002 => Not trivial, Not overlay, NW0, N1, Normal and not trivial cp 0.002/0.002 0.002/0.002 The problem is not joinable. 0.002/0.002 0.01user 0.00system 0:00.02elapsed 86%CPU (0avgtext+0avgdata 12316maxresident)k 0.002/0.002 0inputs+0outputs (0major+1268minor)pagefaults 0swaps