0.003/0.003 YES 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 x:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (f_0 1) 0.003/0.003 (f_1) 0.003/0.003 (a_1) 0.003/0.003 (c_0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(a_1))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(a_1)))) -> *top*_0(f_0(f_0(f_0(f_0(a_1))))) 0.003/0.003 *top*_0(f_0(f_0(a_1))) -> *top*_0(f_0(f_0(f_0(a_1)))) 0.003/0.003 *top*_0(f_0(a_1)) -> *top*_0(f_0(f_0(a_1))) 0.003/0.003 *top*_0(a_1) -> *top*_0(f_0(a_1)) 0.003/0.003 f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x:S)))))))))))))))))))) -> c_0 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 x:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (f_0 1) 0.003/0.003 (f_1) 0.003/0.003 (a_1) 0.003/0.003 (c_0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(a_1))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(a_1)))) -> *top*_0(f_0(f_0(f_0(f_0(a_1))))) 0.003/0.003 *top*_0(f_0(f_0(a_1))) -> *top*_0(f_0(f_0(f_0(a_1)))) 0.003/0.003 *top*_0(f_0(a_1)) -> *top*_0(f_0(f_0(a_1))) 0.003/0.003 *top*_0(a_1) -> *top*_0(f_0(a_1)) 0.003/0.003 f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x:S)))))))))))))))))))) -> c_0 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 x:S) 0.003/0.003 (STRATEGY CONTEXTSENSITIVE 0.003/0.003 (*top*_0 1) 0.003/0.003 (f_0 1) 0.003/0.003 (f_1) 0.003/0.003 (a_1) 0.003/0.003 (c_0) 0.003/0.003 (fSNonEmpty) 0.003/0.003 ) 0.003/0.003 (RULES 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(a_1))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(a_1)))) -> *top*_0(f_0(f_0(f_0(f_0(a_1))))) 0.003/0.003 *top*_0(f_0(f_0(a_1))) -> *top*_0(f_0(f_0(f_0(a_1)))) 0.003/0.003 *top*_0(f_0(a_1)) -> *top*_0(f_0(f_0(a_1))) 0.003/0.003 *top*_0(a_1) -> *top*_0(f_0(a_1)) 0.003/0.003 f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x:S)))))))))))))))))))) -> c_0 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(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(f_0(a_1))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) 0.003/0.003 *top*_0(f_0(f_0(f_0(a_1)))) -> *top*_0(f_0(f_0(f_0(f_0(a_1))))) 0.003/0.003 *top*_0(f_0(f_0(a_1))) -> *top*_0(f_0(f_0(f_0(a_1)))) 0.003/0.003 *top*_0(f_0(a_1)) -> *top*_0(f_0(f_0(a_1))) 0.003/0.003 *top*_0(a_1) -> *top*_0(f_0(a_1)) 0.003/0.003 f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))) 0.003/0.003 f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x:S)))))))))))))))))))) -> c_0 0.003/0.003 f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x:S)))))))))))))))))))) -> c_0 0.003/0.003 -> Vars: 0.003/0.003 x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x 0.003/0.003 -> UVars: 0.003/0.003 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: []) 0.003/0.003 -> FVars: 0.003/0.003 x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21 0.003/0.003 -> PVars: 0.003/0.003 x: [x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21] 0.003/0.003 0.003/0.003 -> Rlps: 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))), id: 1, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))), id: 2, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))), id: 3, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))), id: 4, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))), id: 5, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))), id: 6, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))), id: 7, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))), id: 8, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))), id: 9, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))), id: 10, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))), id: 11, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))), id: 12, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))), id: 13, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))), id: 14, possubterms: *top*_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1], f_0(f_0(f_0(f_0(a_1))))->[1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(f_0(a_1))))) -> *top*_0(f_0(f_0(f_0(f_0(f_0(a_1)))))), id: 15, possubterms: *top*_0(f_0(f_0(f_0(f_0(a_1)))))->[], f_0(f_0(f_0(f_0(a_1))))->[1], f_0(f_0(f_0(a_1)))->[1, 1], f_0(f_0(a_1))->[1, 1, 1], f_0(a_1)->[1, 1, 1, 1], a_1->[1, 1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(f_0(a_1)))) -> *top*_0(f_0(f_0(f_0(f_0(a_1))))), id: 16, possubterms: *top*_0(f_0(f_0(f_0(a_1))))->[], f_0(f_0(f_0(a_1)))->[1], f_0(f_0(a_1))->[1, 1], f_0(a_1)->[1, 1, 1], a_1->[1, 1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(f_0(a_1))) -> *top*_0(f_0(f_0(f_0(a_1)))), id: 17, possubterms: *top*_0(f_0(f_0(a_1)))->[], f_0(f_0(a_1))->[1], f_0(a_1)->[1, 1], a_1->[1, 1, 1]) 0.003/0.003 (rule: *top*_0(f_0(a_1)) -> *top*_0(f_0(f_0(a_1))), id: 18, possubterms: *top*_0(f_0(a_1))->[], f_0(a_1)->[1], a_1->[1, 1]) 0.003/0.003 (rule: *top*_0(a_1) -> *top*_0(f_0(a_1)), id: 19, possubterms: *top*_0(a_1)->[], a_1->[1]) 0.003/0.003 (rule: f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))) -> f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))), id: 20, possubterms: f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))))->[], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))))->[1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))))->[1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))))->[1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))))->[1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))))->[1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))))->[1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))))->[1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))))->[1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(f_0(a_1)))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(f_0(a_1))))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(f_0(a_1)))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(f_0(a_1))))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(f_0(a_1)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(f_0(a_1))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], f_0(a_1)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], a_1->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]) 0.003/0.003 (rule: f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x2:S)))))))))))))))))))) -> c_0, id: 21, possubterms: f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x2:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x3:S)))))))))))))))))))) -> c_0, id: 22, possubterms: f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x3:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x4:S)))))))))))))))))))) -> c_0, id: 23, possubterms: f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x4:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x5:S)))))))))))))))))))) -> c_0, id: 24, possubterms: f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x5:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x6:S)))))))))))))))))))) -> c_0, id: 25, possubterms: f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x6:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x7:S)))))))))))))))))))) -> c_0, id: 26, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x7:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x8:S)))))))))))))))))))) -> c_0, id: 27, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x8:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x9:S)))))))))))))))))))) -> c_0, id: 28, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x9:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x10:S)))))))))))))))))))) -> c_0, id: 29, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x10:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x11:S)))))))))))))))))))) -> c_0, id: 30, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x11:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x12:S)))))))))))))))))))) -> c_0, id: 31, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x12:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x13:S)))))))))))))))))))) -> c_0, id: 32, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x13:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x14:S)))))))))))))))))))) -> c_0, id: 33, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(f_0(x14:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x15:S)))))))))))))))))))) -> c_0, id: 34, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(f_0(x15:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x16:S)))))))))))))))))))) -> c_0, id: 35, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(f_0(x16:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x17:S)))))))))))))))))))) -> c_0, id: 36, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(f_0(x17:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x18:S)))))))))))))))))))) -> c_0, id: 37, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(f_0(x18:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x19:S)))))))))))))))))))) -> c_0, id: 38, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(f_0(x19:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x20:S)))))))))))))))))))) -> c_0, id: 39, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_0(x20:S))))))))))))))))))))->[]) 0.003/0.003 (rule: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x21:S)))))))))))))))))))) -> c_0, id: 40, possubterms: f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(f_1(x21:S))))))))))))))))))))->[]) 0.003/0.003 0.003/0.003 -> Unifications: 0.003/0.003 0.003/0.003 0.003/0.003 -> Critical pairs info: 0.003/0.003 0.003/0.003 0.003/0.003 -> Problem conclusions: 0.003/0.003 Left linear, Right linear, Linear 0.003/0.003 Weakly orthogonal, Almost orthogonal, Orthogonal 0.003/0.003 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 The problem is joinable. 0.003/0.003 0.02user 0.00system 0:00.03elapsed 87%CPU (0avgtext+0avgdata 12424maxresident)k 0.003/0.003 0inputs+0outputs (0major+1405minor)pagefaults 0swaps