0.003/0.003 NO 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S s:S:S x:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (M_1) 0.003/0.003 (cons_1 1) 0.003/0.003 (cons_10 1) 0.003/0.003 (cons_11 1) 0.003/0.003 (cons_2 1) 0.003/0.003 (cons_3 1) 0.003/0.003 (cons_4 1) 0.003/0.003 (cons_5 1) 0.003/0.003 (cons_6 1) 0.003/0.003 (cons_7 1) 0.003/0.003 (cons_8 1) 0.003/0.003 (cons_9 1) 0.003/0.003 (h_0 1) 0.003/0.003 (tail_0 1) 0.003/0.003 (tail_1 1) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (garbage_collection_0) 0.003/0.003 (h_1 1) 0.003/0.003 (num0_0) 0.003/0.003 (num1_0) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(tail_1(cons_1(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_10(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_11(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_5(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_6(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(h_1(cons_1(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_1(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_10(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_11(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_2(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_3(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_4(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_5(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_6(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_7(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_8(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_9(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 M_1 -> h_1(cons_1(num0_0,tail_0(M_1))) 0.003/0.003 cons_1(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_10(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_11(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_2(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_3(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_4(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_5(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_6(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_7(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_8(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_9(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_0(s:S:S) 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_10(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_11(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_5(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_6(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(h_1(cons_1(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_1(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_10(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_11(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_2(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_3(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_4(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_5(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_6(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_7(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_8(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_9(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(tail_1(cons_1(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_10(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_11(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_5(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_6(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(h_1(cons_1(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_1(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_10(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_11(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_2(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_3(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_4(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_5(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_6(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_7(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_8(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_9(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_1(cons_1(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_2(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_3(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_4(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_7(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_8(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_9(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 CleanTRS Processor: 0.003/0.003 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S s:S:S x:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (M_1) 0.003/0.003 (cons_1 1) 0.003/0.003 (cons_10 1) 0.003/0.003 (cons_11 1) 0.003/0.003 (cons_2 1) 0.003/0.003 (cons_3 1) 0.003/0.003 (cons_4 1) 0.003/0.003 (cons_5 1) 0.003/0.003 (cons_6 1) 0.003/0.003 (cons_7 1) 0.003/0.003 (cons_8 1) 0.003/0.003 (cons_9 1) 0.003/0.003 (h_0 1) 0.003/0.003 (tail_0 1) 0.003/0.003 (tail_1 1) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (garbage_collection_0) 0.003/0.003 (h_1 1) 0.003/0.003 (num0_0) 0.003/0.003 (num1_0) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(tail_1(cons_1(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_10(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_11(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_5(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_6(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(h_1(cons_1(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_1(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_10(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_11(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_2(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_3(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_4(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_5(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_6(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_7(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_8(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_9(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 M_1 -> h_1(cons_1(num0_0,tail_0(M_1))) 0.003/0.003 cons_1(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_10(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_11(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_2(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_3(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_4(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_5(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_6(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_7(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_8(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_9(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_0(s:S:S) 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_10(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_11(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_5(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_6(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(h_1(cons_1(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_1(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_10(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_11(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_2(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_3(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_4(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_5(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_6(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_7(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_8(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_9(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(tail_1(cons_1(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_10(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_11(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_5(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_6(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(h_1(cons_1(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_1(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_10(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_11(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_2(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_3(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_4(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_5(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_6(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_7(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_8(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_9(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_1(cons_1(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_2(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_3(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_4(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_7(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_8(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_9(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 0.003/0.003 Modular Confluence Combinations Decomposition Processor: 0.003/0.003 It is a CTRS -> No modular confluence 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 Left-Homogeneous u-Replacing Variables Processor: 0.003/0.003 R satisfies LHRV condition 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 Confluence Problem: 0.003/0.003 (VAR vNonEmpty:S v_NonEmpty:S:S s:S:S x:S:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (M_1) 0.003/0.003 (cons_1 1) 0.003/0.003 (cons_10 1) 0.003/0.003 (cons_11 1) 0.003/0.003 (cons_2 1) 0.003/0.003 (cons_3 1) 0.003/0.003 (cons_4 1) 0.003/0.003 (cons_5 1) 0.003/0.003 (cons_6 1) 0.003/0.003 (cons_7 1) 0.003/0.003 (cons_8 1) 0.003/0.003 (cons_9 1) 0.003/0.003 (h_0 1) 0.003/0.003 (tail_0 1) 0.003/0.003 (tail_1 1) 0.003/0.003 (fSNonEmpty) 0.003/0.003 (garbage_collection_0) 0.003/0.003 (h_1 1) 0.003/0.003 (num0_0) 0.003/0.003 (num1_0) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(tail_1(cons_1(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_10(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_11(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_5(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_6(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(h_1(cons_1(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_1(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_10(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_11(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_2(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_3(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_4(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_5(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_6(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_7(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_8(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_9(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 M_1 -> h_1(cons_1(num0_0,tail_0(M_1))) 0.003/0.003 cons_1(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_10(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_11(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_2(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_3(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_4(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_5(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_6(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_7(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_8(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_9(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_0(s:S:S) 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_10(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_11(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_5(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_6(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(h_1(cons_1(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_1(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_10(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_11(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_2(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_3(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_4(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_5(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_6(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_7(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_8(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_9(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(tail_1(cons_1(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_10(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_11(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_5(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_6(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(h_1(cons_1(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_1(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_10(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_11(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_2(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_3(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_4(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_5(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_6(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_7(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_8(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_9(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_1(cons_1(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_2(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_3(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_4(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_7(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_8(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_9(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 ) 0.003/0.003 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.003/0.003 0.003/0.003 Huet Levy Processor: 0.003/0.003 -> Rules: 0.003/0.003 *top*_0(tail_1(cons_1(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_10(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_11(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_5(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(tail_1(cons_6(x:S:S,s:S:S))) -> *top*_0(s:S:S) 0.003/0.003 *top*_0(h_1(cons_1(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_1(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_10(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_11(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_2(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_3(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_4(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_5(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_6(num0_0,s:S:S))) -> *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_7(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_8(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 *top*_0(h_1(cons_9(num1_0,s:S:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 M_1 -> h_1(cons_1(num0_0,tail_0(M_1))) 0.003/0.003 cons_1(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_10(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_11(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_2(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_3(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_4(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_5(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_6(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_7(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_8(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 cons_9(x:S:S,s:S:S) -> garbage_collection_0 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_0(s:S:S) 0.003/0.003 h_0(tail_1(cons_1(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_10(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_11(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_5(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(tail_1(cons_6(x:S:S,s:S:S))) -> h_1(s:S:S) 0.003/0.003 h_0(h_1(cons_1(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_1(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_10(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_11(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_2(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_3(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_4(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_5(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_6(num0_0,s:S:S))) -> h_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 h_0(h_1(cons_7(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_8(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 h_0(h_1(cons_9(num1_0,s:S:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(tail_1(cons_1(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_10(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_11(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_5(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(tail_1(cons_6(x:S:S,s:S:S))) -> tail_1(s:S:S) 0.003/0.003 tail_0(h_1(cons_1(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_1(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_10(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_11(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_2(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_3(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_4(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_5(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_6(num0_0,s:S:S))) -> tail_1(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_7(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_8(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_0(h_1(cons_9(num1_0,s:S:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S)))) 0.003/0.003 tail_1(cons_1(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_2(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_3(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_4(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_7(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_8(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 tail_1(cons_9(x:S:S,s:S:S)) -> s:S:S 0.003/0.003 -> Vars: 0.003/0.003 s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S, s:S, x:S 0.003/0.003 -> UVars: 0.003/0.003 (UV-RuleId: 1, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 19, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [x:S], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 34, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 35, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 48, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 49, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 50, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 51, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 52, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 59, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 62, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 63, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 64, UV-LActive: [], UV-RActive: [], UV-LFrozen: [s:S], UV-RFrozen: [s:S]) 0.003/0.003 (UV-RuleId: 65, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 66, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 67, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 68, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 69, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 70, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 71, UV-LActive: [x:S], UV-RActive: [s:S], UV-LFrozen: [s:S], UV-RFrozen: []) 0.003/0.003 -> FVars: 0.003/0.003 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, x107 0.003/0.003 -> PVars: 0.003/0.003 s:S: [x4, x6, x8, x10, x12, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x28, x30, x32, x34, x36, x38, x40, x42, x44, x46, x48, x50, x52, x54, x56, x58, x60, x61, x62, x63, x64, x65, x66, x67, x68, x69, x70, x71, x72, x74, x76, x78, x80, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x94, x96, x98, x100, x102, x104, x106], x:S: [x5, x7, x9, x11, x13, x27, x29, x31, x33, x35, x37, x39, x41, x43, x45, x47, x49, x51, x53, x55, x57, x59, x73, x75, x77, x79, x81, x95, x97, x99, x101, x103, x105, x107] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: *top*_0(tail_1(cons_1(x5:S,x4:S))) -> *top*_0(x4:S), id: 1, possubterms: *top*_0(tail_1(cons_1(x5:S,x4:S)))->[], tail_1(cons_1(x5:S,x4:S))->[1], cons_1(x5:S,x4:S)->[1, 1]) 0.003/0.003 (rule: *top*_0(tail_1(cons_10(x7:S,x6:S))) -> *top*_0(x6:S), id: 2, possubterms: *top*_0(tail_1(cons_10(x7:S,x6:S)))->[], tail_1(cons_10(x7:S,x6:S))->[1], cons_10(x7:S,x6:S)->[1, 1]) 0.003/0.003 (rule: *top*_0(tail_1(cons_11(x9:S,x8:S))) -> *top*_0(x8:S), id: 3, possubterms: *top*_0(tail_1(cons_11(x9:S,x8:S)))->[], tail_1(cons_11(x9:S,x8:S))->[1], cons_11(x9:S,x8:S)->[1, 1]) 0.003/0.003 (rule: *top*_0(tail_1(cons_5(x11:S,x10:S))) -> *top*_0(x10:S), id: 4, possubterms: *top*_0(tail_1(cons_5(x11:S,x10:S)))->[], tail_1(cons_5(x11:S,x10:S))->[1], cons_5(x11:S,x10:S)->[1, 1]) 0.003/0.003 (rule: *top*_0(tail_1(cons_6(x13:S,x12:S))) -> *top*_0(x12:S), id: 5, possubterms: *top*_0(tail_1(cons_6(x13:S,x12:S)))->[], tail_1(cons_6(x13:S,x12:S))->[1], cons_6(x13:S,x12:S)->[1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_1(num0_0,x14:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x14:S)))), id: 6, possubterms: *top*_0(h_1(cons_1(num0_0,x14:S)))->[], h_1(cons_1(num0_0,x14:S))->[1], cons_1(num0_0,x14:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_1(num1_0,x15:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x15:S)))), id: 7, possubterms: *top*_0(h_1(cons_1(num1_0,x15:S)))->[], h_1(cons_1(num1_0,x15:S))->[1], cons_1(num1_0,x15:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_10(num1_0,x16:S))) -> *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(x16:S)))), id: 8, possubterms: *top*_0(h_1(cons_10(num1_0,x16:S)))->[], h_1(cons_10(num1_0,x16:S))->[1], cons_10(num1_0,x16:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_11(num1_0,x17:S))) -> *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(x17:S)))), id: 9, possubterms: *top*_0(h_1(cons_11(num1_0,x17:S)))->[], h_1(cons_11(num1_0,x17:S))->[1], cons_11(num1_0,x17:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_2(num0_0,x18:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x18:S)))), id: 10, possubterms: *top*_0(h_1(cons_2(num0_0,x18:S)))->[], h_1(cons_2(num0_0,x18:S))->[1], cons_2(num0_0,x18:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_3(num0_0,x19:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x19:S)))), id: 11, possubterms: *top*_0(h_1(cons_3(num0_0,x19:S)))->[], h_1(cons_3(num0_0,x19:S))->[1], cons_3(num0_0,x19:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_4(num0_0,x20:S))) -> *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x20:S)))), id: 12, possubterms: *top*_0(h_1(cons_4(num0_0,x20:S)))->[], h_1(cons_4(num0_0,x20:S))->[1], cons_4(num0_0,x20:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_5(num0_0,x21:S))) -> *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(x21:S)))), id: 13, possubterms: *top*_0(h_1(cons_5(num0_0,x21:S)))->[], h_1(cons_5(num0_0,x21:S))->[1], cons_5(num0_0,x21:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_6(num0_0,x22:S))) -> *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(x22:S)))), id: 14, possubterms: *top*_0(h_1(cons_6(num0_0,x22:S)))->[], h_1(cons_6(num0_0,x22:S))->[1], cons_6(num0_0,x22:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_7(num1_0,x23:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x23:S)))), id: 15, possubterms: *top*_0(h_1(cons_7(num1_0,x23:S)))->[], h_1(cons_7(num1_0,x23:S))->[1], cons_7(num1_0,x23:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_8(num1_0,x24:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x24:S)))), id: 16, possubterms: *top*_0(h_1(cons_8(num1_0,x24:S)))->[], h_1(cons_8(num1_0,x24:S))->[1], cons_8(num1_0,x24:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(h_1(cons_9(num1_0,x25:S))) -> *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x25:S)))), id: 17, possubterms: *top*_0(h_1(cons_9(num1_0,x25:S)))->[], h_1(cons_9(num1_0,x25:S))->[1], cons_9(num1_0,x25:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: M_1 -> h_1(cons_1(num0_0,tail_0(M_1))), id: 18, possubterms: M_1->[]) 0.003/0.003 (rule: cons_1(x27:S,x26:S) -> garbage_collection_0, id: 19, possubterms: cons_1(x27:S,x26:S)->[]) 0.003/0.003 (rule: cons_10(x29:S,x28:S) -> garbage_collection_0, id: 20, possubterms: cons_10(x29:S,x28:S)->[]) 0.003/0.003 (rule: cons_11(x31:S,x30:S) -> garbage_collection_0, id: 21, possubterms: cons_11(x31:S,x30:S)->[]) 0.003/0.003 (rule: cons_2(x33:S,x32:S) -> garbage_collection_0, id: 22, possubterms: cons_2(x33:S,x32:S)->[]) 0.003/0.003 (rule: cons_3(x35:S,x34:S) -> garbage_collection_0, id: 23, possubterms: cons_3(x35:S,x34:S)->[]) 0.003/0.003 (rule: cons_4(x37:S,x36:S) -> garbage_collection_0, id: 24, possubterms: cons_4(x37:S,x36:S)->[]) 0.003/0.003 (rule: cons_5(x39:S,x38:S) -> garbage_collection_0, id: 25, possubterms: cons_5(x39:S,x38:S)->[]) 0.003/0.003 (rule: cons_6(x41:S,x40:S) -> garbage_collection_0, id: 26, possubterms: cons_6(x41:S,x40:S)->[]) 0.003/0.003 (rule: cons_7(x43:S,x42:S) -> garbage_collection_0, id: 27, possubterms: cons_7(x43:S,x42:S)->[]) 0.003/0.003 (rule: cons_8(x45:S,x44:S) -> garbage_collection_0, id: 28, possubterms: cons_8(x45:S,x44:S)->[]) 0.003/0.003 (rule: cons_9(x47:S,x46:S) -> garbage_collection_0, id: 29, possubterms: cons_9(x47:S,x46:S)->[]) 0.003/0.003 (rule: h_0(tail_1(cons_1(x49:S,x48:S))) -> h_0(x48:S), id: 30, possubterms: h_0(tail_1(cons_1(x49:S,x48:S)))->[], tail_1(cons_1(x49:S,x48:S))->[1], cons_1(x49:S,x48:S)->[1, 1]) 0.003/0.003 (rule: h_0(tail_1(cons_1(x51:S,x50:S))) -> h_1(x50:S), id: 31, possubterms: h_0(tail_1(cons_1(x51:S,x50:S)))->[], tail_1(cons_1(x51:S,x50:S))->[1], cons_1(x51:S,x50:S)->[1, 1]) 0.003/0.003 (rule: h_0(tail_1(cons_10(x53:S,x52:S))) -> h_1(x52:S), id: 32, possubterms: h_0(tail_1(cons_10(x53:S,x52:S)))->[], tail_1(cons_10(x53:S,x52:S))->[1], cons_10(x53:S,x52:S)->[1, 1]) 0.003/0.003 (rule: h_0(tail_1(cons_11(x55:S,x54:S))) -> h_1(x54:S), id: 33, possubterms: h_0(tail_1(cons_11(x55:S,x54:S)))->[], tail_1(cons_11(x55:S,x54:S))->[1], cons_11(x55:S,x54:S)->[1, 1]) 0.003/0.003 (rule: h_0(tail_1(cons_5(x57:S,x56:S))) -> h_1(x56:S), id: 34, possubterms: h_0(tail_1(cons_5(x57:S,x56:S)))->[], tail_1(cons_5(x57:S,x56:S))->[1], cons_5(x57:S,x56:S)->[1, 1]) 0.003/0.003 (rule: h_0(tail_1(cons_6(x59:S,x58:S))) -> h_1(x58:S), id: 35, possubterms: h_0(tail_1(cons_6(x59:S,x58:S)))->[], tail_1(cons_6(x59:S,x58:S))->[1], cons_6(x59:S,x58:S)->[1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_1(num0_0,x60:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(x60:S)))), id: 36, possubterms: h_0(h_1(cons_1(num0_0,x60:S)))->[], h_1(cons_1(num0_0,x60:S))->[1], cons_1(num0_0,x60:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_1(num1_0,x61:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(x61:S)))), id: 37, possubterms: h_0(h_1(cons_1(num1_0,x61:S)))->[], h_1(cons_1(num1_0,x61:S))->[1], cons_1(num1_0,x61:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_10(num1_0,x62:S))) -> h_1(cons_10(num1_0,cons_2(num0_0,h_1(x62:S)))), id: 38, possubterms: h_0(h_1(cons_10(num1_0,x62:S)))->[], h_1(cons_10(num1_0,x62:S))->[1], cons_10(num1_0,x62:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_11(num1_0,x63:S))) -> h_1(cons_10(num1_0,cons_3(num0_0,h_1(x63:S)))), id: 39, possubterms: h_0(h_1(cons_11(num1_0,x63:S)))->[], h_1(cons_11(num1_0,x63:S))->[1], cons_11(num1_0,x63:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_2(num0_0,x64:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(x64:S)))), id: 40, possubterms: h_0(h_1(cons_2(num0_0,x64:S)))->[], h_1(cons_2(num0_0,x64:S))->[1], cons_2(num0_0,x64:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_3(num0_0,x65:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(x65:S)))), id: 41, possubterms: h_0(h_1(cons_3(num0_0,x65:S)))->[], h_1(cons_3(num0_0,x65:S))->[1], cons_3(num0_0,x65:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_4(num0_0,x66:S))) -> h_1(cons_6(num0_0,cons_1(num1_0,h_0(x66:S)))), id: 42, possubterms: h_0(h_1(cons_4(num0_0,x66:S)))->[], h_1(cons_4(num0_0,x66:S))->[1], cons_4(num0_0,x66:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_5(num0_0,x67:S))) -> h_1(cons_6(num0_0,cons_7(num1_0,h_1(x67:S)))), id: 43, possubterms: h_0(h_1(cons_5(num0_0,x67:S)))->[], h_1(cons_5(num0_0,x67:S))->[1], cons_5(num0_0,x67:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_6(num0_0,x68:S))) -> h_1(cons_6(num0_0,cons_8(num1_0,h_1(x68:S)))), id: 44, possubterms: h_0(h_1(cons_6(num0_0,x68:S)))->[], h_1(cons_6(num0_0,x68:S))->[1], cons_6(num0_0,x68:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_7(num1_0,x69:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(x69:S)))), id: 45, possubterms: h_0(h_1(cons_7(num1_0,x69:S)))->[], h_1(cons_7(num1_0,x69:S))->[1], cons_7(num1_0,x69:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_8(num1_0,x70:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(x70:S)))), id: 46, possubterms: h_0(h_1(cons_8(num1_0,x70:S)))->[], h_1(cons_8(num1_0,x70:S))->[1], cons_8(num1_0,x70:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: h_0(h_1(cons_9(num1_0,x71:S))) -> h_1(cons_10(num1_0,cons_1(num0_0,h_0(x71:S)))), id: 47, possubterms: h_0(h_1(cons_9(num1_0,x71:S)))->[], h_1(cons_9(num1_0,x71:S))->[1], cons_9(num1_0,x71:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(tail_1(cons_1(x73:S,x72:S))) -> tail_1(x72:S), id: 48, possubterms: tail_0(tail_1(cons_1(x73:S,x72:S)))->[], tail_1(cons_1(x73:S,x72:S))->[1], cons_1(x73:S,x72:S)->[1, 1]) 0.003/0.003 (rule: tail_0(tail_1(cons_10(x75:S,x74:S))) -> tail_1(x74:S), id: 49, possubterms: tail_0(tail_1(cons_10(x75:S,x74:S)))->[], tail_1(cons_10(x75:S,x74:S))->[1], cons_10(x75:S,x74:S)->[1, 1]) 0.003/0.003 (rule: tail_0(tail_1(cons_11(x77:S,x76:S))) -> tail_1(x76:S), id: 50, possubterms: tail_0(tail_1(cons_11(x77:S,x76:S)))->[], tail_1(cons_11(x77:S,x76:S))->[1], cons_11(x77:S,x76:S)->[1, 1]) 0.003/0.003 (rule: tail_0(tail_1(cons_5(x79:S,x78:S))) -> tail_1(x78:S), id: 51, possubterms: tail_0(tail_1(cons_5(x79:S,x78:S)))->[], tail_1(cons_5(x79:S,x78:S))->[1], cons_5(x79:S,x78:S)->[1, 1]) 0.003/0.003 (rule: tail_0(tail_1(cons_6(x81:S,x80:S))) -> tail_1(x80:S), id: 52, possubterms: tail_0(tail_1(cons_6(x81:S,x80:S)))->[], tail_1(cons_6(x81:S,x80:S))->[1], cons_6(x81:S,x80:S)->[1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_1(num0_0,x82:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x82:S)))), id: 53, possubterms: tail_0(h_1(cons_1(num0_0,x82:S)))->[], h_1(cons_1(num0_0,x82:S))->[1], cons_1(num0_0,x82:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_1(num1_0,x83:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x83:S)))), id: 54, possubterms: tail_0(h_1(cons_1(num1_0,x83:S)))->[], h_1(cons_1(num1_0,x83:S))->[1], cons_1(num1_0,x83:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_10(num1_0,x84:S))) -> tail_1(cons_10(num1_0,cons_2(num0_0,h_1(x84:S)))), id: 55, possubterms: tail_0(h_1(cons_10(num1_0,x84:S)))->[], h_1(cons_10(num1_0,x84:S))->[1], cons_10(num1_0,x84:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_11(num1_0,x85:S))) -> tail_1(cons_10(num1_0,cons_3(num0_0,h_1(x85:S)))), id: 56, possubterms: tail_0(h_1(cons_11(num1_0,x85:S)))->[], h_1(cons_11(num1_0,x85:S))->[1], cons_11(num1_0,x85:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_2(num0_0,x86:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x86:S)))), id: 57, possubterms: tail_0(h_1(cons_2(num0_0,x86:S)))->[], h_1(cons_2(num0_0,x86:S))->[1], cons_2(num0_0,x86:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_3(num0_0,x87:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x87:S)))), id: 58, possubterms: tail_0(h_1(cons_3(num0_0,x87:S)))->[], h_1(cons_3(num0_0,x87:S))->[1], cons_3(num0_0,x87:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_4(num0_0,x88:S))) -> tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x88:S)))), id: 59, possubterms: tail_0(h_1(cons_4(num0_0,x88:S)))->[], h_1(cons_4(num0_0,x88:S))->[1], cons_4(num0_0,x88:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_5(num0_0,x89:S))) -> tail_1(cons_6(num0_0,cons_7(num1_0,h_1(x89:S)))), id: 60, possubterms: tail_0(h_1(cons_5(num0_0,x89:S)))->[], h_1(cons_5(num0_0,x89:S))->[1], cons_5(num0_0,x89:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_6(num0_0,x90:S))) -> tail_1(cons_6(num0_0,cons_8(num1_0,h_1(x90:S)))), id: 61, possubterms: tail_0(h_1(cons_6(num0_0,x90:S)))->[], h_1(cons_6(num0_0,x90:S))->[1], cons_6(num0_0,x90:S)->[1, 1], num0_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_7(num1_0,x91:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x91:S)))), id: 62, possubterms: tail_0(h_1(cons_7(num1_0,x91:S)))->[], h_1(cons_7(num1_0,x91:S))->[1], cons_7(num1_0,x91:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_8(num1_0,x92:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x92:S)))), id: 63, possubterms: tail_0(h_1(cons_8(num1_0,x92:S)))->[], h_1(cons_8(num1_0,x92:S))->[1], cons_8(num1_0,x92:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_0(h_1(cons_9(num1_0,x93:S))) -> tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x93:S)))), id: 64, possubterms: tail_0(h_1(cons_9(num1_0,x93:S)))->[], h_1(cons_9(num1_0,x93:S))->[1], cons_9(num1_0,x93:S)->[1, 1], num1_0->[1, 1, 1]) 0.003/0.003 (rule: tail_1(cons_1(x95:S,x94:S)) -> x94:S, id: 65, possubterms: tail_1(cons_1(x95:S,x94:S))->[], cons_1(x95:S,x94:S)->[1]) 0.003/0.003 (rule: tail_1(cons_2(x97:S,x96:S)) -> x96:S, id: 66, possubterms: tail_1(cons_2(x97:S,x96:S))->[], cons_2(x97:S,x96:S)->[1]) 0.003/0.003 (rule: tail_1(cons_3(x99:S,x98:S)) -> x98:S, id: 67, possubterms: tail_1(cons_3(x99:S,x98:S))->[], cons_3(x99:S,x98:S)->[1]) 0.003/0.003 (rule: tail_1(cons_4(x101:S,x100:S)) -> x100:S, id: 68, possubterms: tail_1(cons_4(x101:S,x100:S))->[], cons_4(x101:S,x100:S)->[1]) 0.003/0.003 (rule: tail_1(cons_7(x103:S,x102:S)) -> x102:S, id: 69, possubterms: tail_1(cons_7(x103:S,x102:S))->[], cons_7(x103:S,x102:S)->[1]) 0.003/0.003 (rule: tail_1(cons_8(x105:S,x104:S)) -> x104:S, id: 70, possubterms: tail_1(cons_8(x105:S,x104:S))->[], cons_8(x105:S,x104:S)->[1]) 0.003/0.003 (rule: tail_1(cons_9(x107:S,x106:S)) -> x106:S, id: 71, possubterms: tail_1(cons_9(x107:S,x106:S))->[], cons_9(x107:S,x106:S)->[1]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 (R1 unifies with R65 at p: [1], l: *top*_0(tail_1(cons_1(x5:S,x4:S))), lp: tail_1(cons_1(x5:S,x4:S)), sig: {x4:S -> s:S:S,x5:S -> x:S:S}, l': tail_1(cons_1(x:S:S,s:S:S)), r: *top*_0(x4:S), r': s:S:S) 0.003/0.003 (R1 unifies with R19 at p: [1,1], l: *top*_0(tail_1(cons_1(x5:S,x4:S))), lp: cons_1(x5:S,x4:S), sig: {x4:S -> s:S:S,x5:S -> x:S:S}, l': cons_1(x:S:S,s:S:S), r: *top*_0(x4:S), r': garbage_collection_0) 0.003/0.003 (R2 unifies with R20 at p: [1,1], l: *top*_0(tail_1(cons_10(x7:S,x6:S))), lp: cons_10(x7:S,x6:S), sig: {x6:S -> s:S:S,x7:S -> x:S:S}, l': cons_10(x:S:S,s:S:S), r: *top*_0(x6:S), r': garbage_collection_0) 0.003/0.003 (R3 unifies with R21 at p: [1,1], l: *top*_0(tail_1(cons_11(x9:S,x8:S))), lp: cons_11(x9:S,x8:S), sig: {x8:S -> s:S:S,x9:S -> x:S:S}, l': cons_11(x:S:S,s:S:S), r: *top*_0(x8:S), r': garbage_collection_0) 0.003/0.003 (R4 unifies with R25 at p: [1,1], l: *top*_0(tail_1(cons_5(x11:S,x10:S))), lp: cons_5(x11:S,x10:S), sig: {x10:S -> s:S:S,x11:S -> x:S:S}, l': cons_5(x:S:S,s:S:S), r: *top*_0(x10:S), r': garbage_collection_0) 0.003/0.003 (R5 unifies with R26 at p: [1,1], l: *top*_0(tail_1(cons_6(x13:S,x12:S))), lp: cons_6(x13:S,x12:S), sig: {x12:S -> s:S:S,x13:S -> x:S:S}, l': cons_6(x:S:S,s:S:S), r: *top*_0(x12:S), r': garbage_collection_0) 0.003/0.003 (R6 unifies with R19 at p: [1,1], l: *top*_0(h_1(cons_1(num0_0,x14:S))), lp: cons_1(num0_0,x14:S), sig: {x:S:S -> num0_0,x14:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x14:S)))), r': garbage_collection_0) 0.003/0.003 (R7 unifies with R19 at p: [1,1], l: *top*_0(h_1(cons_1(num1_0,x15:S))), lp: cons_1(num1_0,x15:S), sig: {x:S:S -> num1_0,x15:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x15:S)))), r': garbage_collection_0) 0.003/0.003 (R8 unifies with R20 at p: [1,1], l: *top*_0(h_1(cons_10(num1_0,x16:S))), lp: cons_10(num1_0,x16:S), sig: {x:S:S -> num1_0,x16:S -> s:S:S}, l': cons_10(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_2(num0_0,h_1(x16:S)))), r': garbage_collection_0) 0.003/0.003 (R9 unifies with R21 at p: [1,1], l: *top*_0(h_1(cons_11(num1_0,x17:S))), lp: cons_11(num1_0,x17:S), sig: {x:S:S -> num1_0,x17:S -> s:S:S}, l': cons_11(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_3(num0_0,h_1(x17:S)))), r': garbage_collection_0) 0.003/0.003 (R10 unifies with R22 at p: [1,1], l: *top*_0(h_1(cons_2(num0_0,x18:S))), lp: cons_2(num0_0,x18:S), sig: {x:S:S -> num0_0,x18:S -> s:S:S}, l': cons_2(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x18:S)))), r': garbage_collection_0) 0.003/0.003 (R11 unifies with R23 at p: [1,1], l: *top*_0(h_1(cons_3(num0_0,x19:S))), lp: cons_3(num0_0,x19:S), sig: {x:S:S -> num0_0,x19:S -> s:S:S}, l': cons_3(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x19:S)))), r': garbage_collection_0) 0.003/0.003 (R12 unifies with R24 at p: [1,1], l: *top*_0(h_1(cons_4(num0_0,x20:S))), lp: cons_4(num0_0,x20:S), sig: {x:S:S -> num0_0,x20:S -> s:S:S}, l': cons_4(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_1(num1_0,h_0(x20:S)))), r': garbage_collection_0) 0.003/0.003 (R13 unifies with R25 at p: [1,1], l: *top*_0(h_1(cons_5(num0_0,x21:S))), lp: cons_5(num0_0,x21:S), sig: {x:S:S -> num0_0,x21:S -> s:S:S}, l': cons_5(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_7(num1_0,h_1(x21:S)))), r': garbage_collection_0) 0.003/0.003 (R14 unifies with R26 at p: [1,1], l: *top*_0(h_1(cons_6(num0_0,x22:S))), lp: cons_6(num0_0,x22:S), sig: {x:S:S -> num0_0,x22:S -> s:S:S}, l': cons_6(x:S:S,s:S:S), r: *top*_0(cons_6(num0_0,cons_8(num1_0,h_1(x22:S)))), r': garbage_collection_0) 0.003/0.003 (R15 unifies with R27 at p: [1,1], l: *top*_0(h_1(cons_7(num1_0,x23:S))), lp: cons_7(num1_0,x23:S), sig: {x:S:S -> num1_0,x23:S -> s:S:S}, l': cons_7(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x23:S)))), r': garbage_collection_0) 0.003/0.003 (R16 unifies with R28 at p: [1,1], l: *top*_0(h_1(cons_8(num1_0,x24:S))), lp: cons_8(num1_0,x24:S), sig: {x:S:S -> num1_0,x24:S -> s:S:S}, l': cons_8(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x24:S)))), r': garbage_collection_0) 0.003/0.003 (R17 unifies with R29 at p: [1,1], l: *top*_0(h_1(cons_9(num1_0,x25:S))), lp: cons_9(num1_0,x25:S), sig: {x:S:S -> num1_0,x25:S -> s:S:S}, l': cons_9(x:S:S,s:S:S), r: *top*_0(cons_10(num1_0,cons_1(num0_0,h_0(x25:S)))), r': garbage_collection_0) 0.003/0.003 (R30 unifies with R65 at p: [1], l: h_0(tail_1(cons_1(x49:S,x48:S))), lp: tail_1(cons_1(x49:S,x48:S)), sig: {x48:S -> s:S:S,x49:S -> x:S:S}, l': tail_1(cons_1(x:S:S,s:S:S)), r: h_0(x48:S), r': s:S:S) 0.003/0.003 (R30 unifies with R19 at p: [1,1], l: h_0(tail_1(cons_1(x49:S,x48:S))), lp: cons_1(x49:S,x48:S), sig: {x48:S -> s:S:S,x49:S -> x:S:S}, l': cons_1(x:S:S,s:S:S), r: h_0(x48:S), r': garbage_collection_0) 0.003/0.003 (R31 unifies with R30 at p: [], l: h_0(tail_1(cons_1(x51:S,x50:S))), lp: h_0(tail_1(cons_1(x51:S,x50:S))), sig: {x50:S -> s:S:S,x51:S -> x:S:S}, l': h_0(tail_1(cons_1(x:S:S,s:S:S))), r: h_1(x50:S), r': h_0(s:S:S)) 0.003/0.003 (R31 unifies with R65 at p: [1], l: h_0(tail_1(cons_1(x51:S,x50:S))), lp: tail_1(cons_1(x51:S,x50:S)), sig: {x50:S -> s:S:S,x51:S -> x:S:S}, l': tail_1(cons_1(x:S:S,s:S:S)), r: h_1(x50:S), r': s:S:S) 0.003/0.003 (R31 unifies with R19 at p: [1,1], l: h_0(tail_1(cons_1(x51:S,x50:S))), lp: cons_1(x51:S,x50:S), sig: {x50:S -> s:S:S,x51:S -> x:S:S}, l': cons_1(x:S:S,s:S:S), r: h_1(x50:S), r': garbage_collection_0) 0.003/0.003 (R32 unifies with R20 at p: [1,1], l: h_0(tail_1(cons_10(x53:S,x52:S))), lp: cons_10(x53:S,x52:S), sig: {x52:S -> s:S:S,x53:S -> x:S:S}, l': cons_10(x:S:S,s:S:S), r: h_1(x52:S), r': garbage_collection_0) 0.003/0.003 (R33 unifies with R21 at p: [1,1], l: h_0(tail_1(cons_11(x55:S,x54:S))), lp: cons_11(x55:S,x54:S), sig: {x54:S -> s:S:S,x55:S -> x:S:S}, l': cons_11(x:S:S,s:S:S), r: h_1(x54:S), r': garbage_collection_0) 0.003/0.003 (R34 unifies with R25 at p: [1,1], l: h_0(tail_1(cons_5(x57:S,x56:S))), lp: cons_5(x57:S,x56:S), sig: {x56:S -> s:S:S,x57:S -> x:S:S}, l': cons_5(x:S:S,s:S:S), r: h_1(x56:S), r': garbage_collection_0) 0.003/0.003 (R35 unifies with R26 at p: [1,1], l: h_0(tail_1(cons_6(x59:S,x58:S))), lp: cons_6(x59:S,x58:S), sig: {x58:S -> s:S:S,x59:S -> x:S:S}, l': cons_6(x:S:S,s:S:S), r: h_1(x58:S), r': garbage_collection_0) 0.003/0.003 (R36 unifies with R19 at p: [1,1], l: h_0(h_1(cons_1(num0_0,x60:S))), lp: cons_1(num0_0,x60:S), sig: {x:S:S -> num0_0,x60:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_1(num1_0,h_0(x60:S)))), r': garbage_collection_0) 0.003/0.003 (R37 unifies with R19 at p: [1,1], l: h_0(h_1(cons_1(num1_0,x61:S))), lp: cons_1(num1_0,x61:S), sig: {x:S:S -> num1_0,x61:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_1(num0_0,h_0(x61:S)))), r': garbage_collection_0) 0.003/0.003 (R38 unifies with R20 at p: [1,1], l: h_0(h_1(cons_10(num1_0,x62:S))), lp: cons_10(num1_0,x62:S), sig: {x:S:S -> num1_0,x62:S -> s:S:S}, l': cons_10(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_2(num0_0,h_1(x62:S)))), r': garbage_collection_0) 0.003/0.003 (R39 unifies with R21 at p: [1,1], l: h_0(h_1(cons_11(num1_0,x63:S))), lp: cons_11(num1_0,x63:S), sig: {x:S:S -> num1_0,x63:S -> s:S:S}, l': cons_11(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_3(num0_0,h_1(x63:S)))), r': garbage_collection_0) 0.003/0.003 (R40 unifies with R22 at p: [1,1], l: h_0(h_1(cons_2(num0_0,x64:S))), lp: cons_2(num0_0,x64:S), sig: {x:S:S -> num0_0,x64:S -> s:S:S}, l': cons_2(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_1(num1_0,h_0(x64:S)))), r': garbage_collection_0) 0.003/0.003 (R41 unifies with R23 at p: [1,1], l: h_0(h_1(cons_3(num0_0,x65:S))), lp: cons_3(num0_0,x65:S), sig: {x:S:S -> num0_0,x65:S -> s:S:S}, l': cons_3(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_1(num1_0,h_0(x65:S)))), r': garbage_collection_0) 0.003/0.003 (R42 unifies with R24 at p: [1,1], l: h_0(h_1(cons_4(num0_0,x66:S))), lp: cons_4(num0_0,x66:S), sig: {x:S:S -> num0_0,x66:S -> s:S:S}, l': cons_4(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_1(num1_0,h_0(x66:S)))), r': garbage_collection_0) 0.003/0.003 (R43 unifies with R25 at p: [1,1], l: h_0(h_1(cons_5(num0_0,x67:S))), lp: cons_5(num0_0,x67:S), sig: {x:S:S -> num0_0,x67:S -> s:S:S}, l': cons_5(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_7(num1_0,h_1(x67:S)))), r': garbage_collection_0) 0.003/0.003 (R44 unifies with R26 at p: [1,1], l: h_0(h_1(cons_6(num0_0,x68:S))), lp: cons_6(num0_0,x68:S), sig: {x:S:S -> num0_0,x68:S -> s:S:S}, l': cons_6(x:S:S,s:S:S), r: h_1(cons_6(num0_0,cons_8(num1_0,h_1(x68:S)))), r': garbage_collection_0) 0.003/0.003 (R45 unifies with R27 at p: [1,1], l: h_0(h_1(cons_7(num1_0,x69:S))), lp: cons_7(num1_0,x69:S), sig: {x:S:S -> num1_0,x69:S -> s:S:S}, l': cons_7(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_1(num0_0,h_0(x69:S)))), r': garbage_collection_0) 0.003/0.003 (R46 unifies with R28 at p: [1,1], l: h_0(h_1(cons_8(num1_0,x70:S))), lp: cons_8(num1_0,x70:S), sig: {x:S:S -> num1_0,x70:S -> s:S:S}, l': cons_8(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_1(num0_0,h_0(x70:S)))), r': garbage_collection_0) 0.003/0.003 (R47 unifies with R29 at p: [1,1], l: h_0(h_1(cons_9(num1_0,x71:S))), lp: cons_9(num1_0,x71:S), sig: {x:S:S -> num1_0,x71:S -> s:S:S}, l': cons_9(x:S:S,s:S:S), r: h_1(cons_10(num1_0,cons_1(num0_0,h_0(x71:S)))), r': garbage_collection_0) 0.003/0.003 (R48 unifies with R65 at p: [1], l: tail_0(tail_1(cons_1(x73:S,x72:S))), lp: tail_1(cons_1(x73:S,x72:S)), sig: {x72:S -> s:S:S,x73:S -> x:S:S}, l': tail_1(cons_1(x:S:S,s:S:S)), r: tail_1(x72:S), r': s:S:S) 0.003/0.003 (R48 unifies with R19 at p: [1,1], l: tail_0(tail_1(cons_1(x73:S,x72:S))), lp: cons_1(x73:S,x72:S), sig: {x72:S -> s:S:S,x73:S -> x:S:S}, l': cons_1(x:S:S,s:S:S), r: tail_1(x72:S), r': garbage_collection_0) 0.003/0.003 (R49 unifies with R20 at p: [1,1], l: tail_0(tail_1(cons_10(x75:S,x74:S))), lp: cons_10(x75:S,x74:S), sig: {x74:S -> s:S:S,x75:S -> x:S:S}, l': cons_10(x:S:S,s:S:S), r: tail_1(x74:S), r': garbage_collection_0) 0.003/0.003 (R50 unifies with R21 at p: [1,1], l: tail_0(tail_1(cons_11(x77:S,x76:S))), lp: cons_11(x77:S,x76:S), sig: {x76:S -> s:S:S,x77:S -> x:S:S}, l': cons_11(x:S:S,s:S:S), r: tail_1(x76:S), r': garbage_collection_0) 0.003/0.003 (R51 unifies with R25 at p: [1,1], l: tail_0(tail_1(cons_5(x79:S,x78:S))), lp: cons_5(x79:S,x78:S), sig: {x78:S -> s:S:S,x79:S -> x:S:S}, l': cons_5(x:S:S,s:S:S), r: tail_1(x78:S), r': garbage_collection_0) 0.003/0.003 (R52 unifies with R26 at p: [1,1], l: tail_0(tail_1(cons_6(x81:S,x80:S))), lp: cons_6(x81:S,x80:S), sig: {x80:S -> s:S:S,x81:S -> x:S:S}, l': cons_6(x:S:S,s:S:S), r: tail_1(x80:S), r': garbage_collection_0) 0.003/0.003 (R53 unifies with R19 at p: [1,1], l: tail_0(h_1(cons_1(num0_0,x82:S))), lp: cons_1(num0_0,x82:S), sig: {x:S:S -> num0_0,x82:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x82:S)))), r': garbage_collection_0) 0.003/0.003 (R54 unifies with R19 at p: [1,1], l: tail_0(h_1(cons_1(num1_0,x83:S))), lp: cons_1(num1_0,x83:S), sig: {x:S:S -> num1_0,x83:S -> s:S:S}, l': cons_1(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x83:S)))), r': garbage_collection_0) 0.003/0.003 (R55 unifies with R20 at p: [1,1], l: tail_0(h_1(cons_10(num1_0,x84:S))), lp: cons_10(num1_0,x84:S), sig: {x:S:S -> num1_0,x84:S -> s:S:S}, l': cons_10(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_2(num0_0,h_1(x84:S)))), r': garbage_collection_0) 0.003/0.003 (R56 unifies with R21 at p: [1,1], l: tail_0(h_1(cons_11(num1_0,x85:S))), lp: cons_11(num1_0,x85:S), sig: {x:S:S -> num1_0,x85:S -> s:S:S}, l': cons_11(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_3(num0_0,h_1(x85:S)))), r': garbage_collection_0) 0.003/0.003 (R57 unifies with R22 at p: [1,1], l: tail_0(h_1(cons_2(num0_0,x86:S))), lp: cons_2(num0_0,x86:S), sig: {x:S:S -> num0_0,x86:S -> s:S:S}, l': cons_2(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x86:S)))), r': garbage_collection_0) 0.003/0.003 (R58 unifies with R23 at p: [1,1], l: tail_0(h_1(cons_3(num0_0,x87:S))), lp: cons_3(num0_0,x87:S), sig: {x:S:S -> num0_0,x87:S -> s:S:S}, l': cons_3(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x87:S)))), r': garbage_collection_0) 0.003/0.003 (R59 unifies with R24 at p: [1,1], l: tail_0(h_1(cons_4(num0_0,x88:S))), lp: cons_4(num0_0,x88:S), sig: {x:S:S -> num0_0,x88:S -> s:S:S}, l': cons_4(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_1(num1_0,h_0(x88:S)))), r': garbage_collection_0) 0.003/0.003 (R60 unifies with R25 at p: [1,1], l: tail_0(h_1(cons_5(num0_0,x89:S))), lp: cons_5(num0_0,x89:S), sig: {x:S:S -> num0_0,x89:S -> s:S:S}, l': cons_5(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_7(num1_0,h_1(x89:S)))), r': garbage_collection_0) 0.003/0.003 (R61 unifies with R26 at p: [1,1], l: tail_0(h_1(cons_6(num0_0,x90:S))), lp: cons_6(num0_0,x90:S), sig: {x:S:S -> num0_0,x90:S -> s:S:S}, l': cons_6(x:S:S,s:S:S), r: tail_1(cons_6(num0_0,cons_8(num1_0,h_1(x90:S)))), r': garbage_collection_0) 0.003/0.003 (R62 unifies with R27 at p: [1,1], l: tail_0(h_1(cons_7(num1_0,x91:S))), lp: cons_7(num1_0,x91:S), sig: {x:S:S -> num1_0,x91:S -> s:S:S}, l': cons_7(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x91:S)))), r': garbage_collection_0) 0.003/0.003 (R63 unifies with R28 at p: [1,1], l: tail_0(h_1(cons_8(num1_0,x92:S))), lp: cons_8(num1_0,x92:S), sig: {x:S:S -> num1_0,x92:S -> s:S:S}, l': cons_8(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x92:S)))), r': garbage_collection_0) 0.003/0.003 (R64 unifies with R29 at p: [1,1], l: tail_0(h_1(cons_9(num1_0,x93:S))), lp: cons_9(num1_0,x93:S), sig: {x:S:S -> num1_0,x93:S -> s:S:S}, l': cons_9(x:S:S,s:S:S), r: tail_1(cons_10(num1_0,cons_1(num0_0,h_0(x93:S)))), r': garbage_collection_0) 0.003/0.003 (R65 unifies with R19 at p: [1], l: tail_1(cons_1(x95:S,x94:S)), lp: cons_1(x95:S,x94:S), sig: {x94:S -> s:S:S,x95:S -> x:S:S}, l': cons_1(x:S:S,s:S:S), r: x94:S, r': garbage_collection_0) 0.003/0.003 (R66 unifies with R22 at p: [1], l: tail_1(cons_2(x97:S,x96:S)), lp: cons_2(x97:S,x96:S), sig: {x96:S -> s:S:S,x97:S -> x:S:S}, l': cons_2(x:S:S,s:S:S), r: x96:S, r': garbage_collection_0) 0.003/0.003 (R67 unifies with R23 at p: [1], l: tail_1(cons_3(x99:S,x98:S)), lp: cons_3(x99:S,x98:S), sig: {x98:S -> s:S:S,x99:S -> x:S:S}, l': cons_3(x:S:S,s:S:S), r: x98:S, r': garbage_collection_0) 0.003/0.003 (R68 unifies with R24 at p: [1], l: tail_1(cons_4(x101:S,x100:S)), lp: cons_4(x101:S,x100:S), sig: {x100:S -> s:S:S,x101:S -> x:S:S}, l': cons_4(x:S:S,s:S:S), r: x100:S, r': garbage_collection_0) 0.003/0.003 (R69 unifies with R27 at p: [1], l: tail_1(cons_7(x103:S,x102:S)), lp: cons_7(x103:S,x102:S), sig: {x102:S -> s:S:S,x103:S -> x:S:S}, l': cons_7(x:S:S,s:S:S), r: x102:S, r': garbage_collection_0) 0.003/0.003 (R70 unifies with R28 at p: [1], l: tail_1(cons_8(x105:S,x104:S)), lp: cons_8(x105:S,x104:S), sig: {x104:S -> s:S:S,x105:S -> x:S:S}, l': cons_8(x:S:S,s:S:S), r: x104:S, r': garbage_collection_0) 0.003/0.003 (R71 unifies with R29 at p: [1], l: tail_1(cons_9(x107:S,x106:S)), lp: cons_9(x107:S,x106:S), sig: {x106:S -> s:S:S,x107:S -> x:S:S}, l': cons_9(x:S:S,s:S:S), r: x106:S, r': garbage_collection_0) 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 => Not trivial, Overlay, NW0, N1 0.003/0.003 <*top*_0(tail_1(garbage_collection_0)),*top*_0(s:S:S)> => Not trivial, Not overlay, NW0, N2 0.003/0.003 => Not trivial, Not overlay, NW0, N3 0.003/0.003 => Not trivial, Not overlay, NW0, N4 0.003/0.003 => Not trivial, Not overlay, NW0, N5 0.003/0.003 <*top*_0(tail_1(garbage_collection_0)),*top*_0(s:S:S)> => Not trivial, Not overlay, NW0, N6 0.003/0.003 => Not trivial, Not overlay, NW0, N7 0.003/0.003 => Not trivial, Not overlay, NW0, N8 0.003/0.003 => Not trivial, Not overlay, NW0, N9 0.003/0.003 => Not trivial, Not overlay, NW0, N10 0.003/0.003 <*top*_0(tail_1(garbage_collection_0)),*top*_0(s:S:S)> => Not trivial, Not overlay, NW0, N11 0.003/0.003 => Not trivial, Not overlay, NW0, N12 0.003/0.003 => Not trivial, Not overlay, NW0, N13 0.003/0.003 => Not trivial, Not overlay, NW0, N14 0.003/0.003 => Not trivial, Not overlay, NW0, N15 0.003/0.003 => Not trivial, Not overlay, NW0, N16 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N17 0.003/0.003 => Not trivial, Not overlay, NW0, N18 0.003/0.003 => Not trivial, Not overlay, NW0, N19 0.003/0.003 => Not trivial, Not overlay, NW0, N20 0.003/0.003 => Trivial, Not overlay, NW0, N21 0.003/0.003 => Not trivial, Not overlay, NW0, N22 0.003/0.003 => Not trivial, Not overlay, NW0, N23 0.003/0.003 => Not trivial, Not overlay, NW0, N24 0.003/0.003 => Not trivial, Not overlay, NW0, N25 0.003/0.003 => Not trivial, Not overlay, NW0, N26 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_7(num1_0,h_1(s:S:S))))> => Not trivial, Not overlay, NW0, N27 0.003/0.003 => Not trivial, Not overlay, NW0, N28 0.003/0.003 => Not trivial, Not overlay, NW0, N29 0.003/0.003 <*top*_0(tail_1(garbage_collection_0)),*top*_0(s:S:S)> => Not trivial, Not overlay, NW0, N30 0.003/0.003 => Not trivial, Not overlay, NW0, N31 0.003/0.003 => Not trivial, Not overlay, NW0, N32 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N33 0.003/0.003 => Not trivial, Not overlay, NW0, N34 0.003/0.003 => Not trivial, Not overlay, NW0, N35 0.003/0.003 => Not trivial, Not overlay, NW0, N36 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N37 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_2(num0_0,h_1(s:S:S))))> => Not trivial, Not overlay, NW0, N38 0.003/0.003 => Not trivial, Not overlay, NW0, N39 0.003/0.003 => Not trivial, Not overlay, NW0, N40 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_8(num1_0,h_1(s:S:S))))> => Not trivial, Not overlay, NW0, N41 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N42 0.003/0.003 => Not trivial, Not overlay, NW0, N43 0.003/0.003 => Not trivial, Not overlay, NW0, N44 0.003/0.003 <*top*_0(s:S:S),*top*_0(s:S:S)> => Trivial, Not overlay, NW0, N45 0.003/0.003 => Not trivial, Not overlay, NW0, N46 0.003/0.003 => Not trivial, Not overlay, NW0, N47 0.003/0.003 <*top*_0(tail_1(garbage_collection_0)),*top*_0(s:S:S)> => Not trivial, Not overlay, NW0, N48 0.003/0.003 => Not trivial, Not overlay, NW0, N49 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N50 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_3(num0_0,h_1(s:S:S))))> => Not trivial, Not overlay, NW0, N51 0.003/0.003 => Not trivial, Not overlay, NW0, N52 0.003/0.003 => Not trivial, Not overlay, NW0, N53 0.003/0.003 => Not trivial, Not overlay, NW0, N54 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N55 0.003/0.003 => Not trivial, Not overlay, NW0, N56 0.003/0.003 => Not trivial, Not overlay, NW0, N57 0.003/0.003 => Not trivial, Not overlay, NW0, N58 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_10(num1_0,cons_1(num0_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N59 0.003/0.003 => Not trivial, Not overlay, NW0, N60 0.003/0.003 => Not trivial, Not overlay, NW0, N61 0.003/0.003 <*top*_0(h_1(garbage_collection_0)),*top*_0(cons_6(num0_0,cons_1(num1_0,h_0(s:S:S))))> => Not trivial, Not overlay, NW0, N62 0.003/0.003 => Not trivial, Not overlay, NW0, N63 0.003/0.003 => Not trivial, Not overlay, NW0, N64 0.003/0.003 0.003/0.003 -> Problem conclusions: 0.003/0.003 Left linear, Right linear, Linear 0.003/0.003 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.003/0.003 Not Huet-Levy confluent, Not Newman confluent 0.003/0.003 R is a CS-TRS, Left-homogeneous u-replacing variables 0.003/0.003 0.003/0.003 0.003/0.003 Problem 1: 0.003/0.003 Different Normal CP Terms Processor: 0.003/0.003 => Not trivial, Overlay, NW0, N1, Normal and not trivial cp 0.003/0.003 0.003/0.003 The problem is not joinable. 0.003/0.003 0.02user 0.00system 0:00.03elapsed 93%CPU (0avgtext+0avgdata 14952maxresident)k 0.003/0.003 16inputs+0outputs (0major+1968minor)pagefaults 0swaps