NO

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(0 1)
(1 1)
(2 1)
(fSNonEmpty)
)
(RULES
0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))) -> 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))
0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))) -> 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))
0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))) -> 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))
0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))) -> 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))
0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))) -> 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))
0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))) -> 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))
0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))) -> 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))
0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))) -> 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))
0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))) -> 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))
1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))) -> 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))
1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))) -> 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))
1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))) -> 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))
1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))) -> 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))
1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))) -> 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))
2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))) -> 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))
2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))) -> 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))
2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))) -> 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))
2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))) -> 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))
2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))) -> 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(0 1)
(1 1)
(2 1)
(fSNonEmpty)
)
(RULES
0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))) -> 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))
0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))) -> 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))
0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))) -> 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))
0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))) -> 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))
0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))) -> 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))
0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))) -> 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))
0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))) -> 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))
0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))) -> 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))
0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))) -> 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))
1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))) -> 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))
1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))) -> 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))
1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))) -> 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))
1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))) -> 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))
1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))) -> 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))
2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))) -> 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))
2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))) -> 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))
2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))) -> 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))
2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))) -> 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))
2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))) -> 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))) -> 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))
 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))) -> 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))
 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))) -> 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))
 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))) -> 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))
 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))) -> 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))
 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))) -> 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))
 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))) -> 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))
 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))) -> 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))
 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))) -> 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))
 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))) -> 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))
 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))) -> 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))
 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))) -> 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))
 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))) -> 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))
 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))) -> 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))
 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))) -> 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))
 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))) -> 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))
 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))) -> 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))
 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))) -> 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))
 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))) -> 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))
-> Vars:
 x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x

-> Rlps:
 (rule: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))) -> 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), id: 1, possubterms: 0(0(0(1(2(1(1(1(0(0(1(0(1(x)))))))))))))->[], 0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))->[1], 0(1(2(1(1(1(0(0(1(0(1(x)))))))))))->[1, 1], 1(2(1(1(1(0(0(1(0(1(x))))))))))->[1, 1, 1], 2(1(1(1(0(0(1(0(1(x)))))))))->[1, 1, 1, 1], 1(1(1(0(0(1(0(1(x))))))))->[1, 1, 1, 1, 1], 1(1(0(0(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 1(0(0(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(0(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))) -> 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), id: 2, possubterms: 0(0(1(0(0(1(1(1(0(1(2(0(1(x)))))))))))))->[], 0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))->[1], 1(0(0(1(1(1(0(1(2(0(1(x)))))))))))->[1, 1], 0(0(1(1(1(0(1(2(0(1(x))))))))))->[1, 1, 1], 0(1(1(1(0(1(2(0(1(x)))))))))->[1, 1, 1, 1], 1(1(1(0(1(2(0(1(x))))))))->[1, 1, 1, 1, 1], 1(1(0(1(2(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 1(0(1(2(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(2(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(2(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 2(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))) -> 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), id: 3, possubterms: 0(0(1(0(1(0(1(0(0(1(0(2(0(x)))))))))))))->[], 0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))->[1], 1(0(1(0(1(0(0(1(0(2(0(x)))))))))))->[1, 1], 0(1(0(1(0(0(1(0(2(0(x))))))))))->[1, 1, 1], 1(0(1(0(0(1(0(2(0(x)))))))))->[1, 1, 1, 1], 0(1(0(0(1(0(2(0(x))))))))->[1, 1, 1, 1, 1], 1(0(0(1(0(2(0(x)))))))->[1, 1, 1, 1, 1, 1], 0(0(1(0(2(0(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(0(2(0(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(0(2(0(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 0(2(0(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 2(0(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))) -> 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), id: 4, possubterms: 0(0(1(1(1(1(1(2(1(1(2(1(1(x)))))))))))))->[], 0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))->[1], 1(1(1(1(1(2(1(1(2(1(1(x)))))))))))->[1, 1], 1(1(1(1(2(1(1(2(1(1(x))))))))))->[1, 1, 1], 1(1(1(2(1(1(2(1(1(x)))))))))->[1, 1, 1, 1], 1(1(2(1(1(2(1(1(x))))))))->[1, 1, 1, 1, 1], 1(2(1(1(2(1(1(x)))))))->[1, 1, 1, 1, 1, 1], 2(1(1(2(1(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(1(2(1(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(2(1(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 2(1(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))) -> 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), id: 5, possubterms: 0(1(0(2(0(2(1(0(0(1(0(1(1(x)))))))))))))->[], 1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))->[1], 0(2(0(2(1(0(0(1(0(1(1(x)))))))))))->[1, 1], 2(0(2(1(0(0(1(0(1(1(x))))))))))->[1, 1, 1], 0(2(1(0(0(1(0(1(1(x)))))))))->[1, 1, 1, 1], 2(1(0(0(1(0(1(1(x))))))))->[1, 1, 1, 1, 1], 1(0(0(1(0(1(1(x)))))))->[1, 1, 1, 1, 1, 1], 0(0(1(0(1(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(0(1(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))) -> 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), id: 6, possubterms: 0(1(0(2(2(1(1(2(1(2(2(0(1(x)))))))))))))->[], 1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))->[1], 0(2(2(1(1(2(1(2(2(0(1(x)))))))))))->[1, 1], 2(2(1(1(2(1(2(2(0(1(x))))))))))->[1, 1, 1], 2(1(1(2(1(2(2(0(1(x)))))))))->[1, 1, 1, 1], 1(1(2(1(2(2(0(1(x))))))))->[1, 1, 1, 1, 1], 1(2(1(2(2(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 2(1(2(2(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(2(2(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 2(2(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 2(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))) -> 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), id: 7, possubterms: 0(1(1(0(1(1(0(1(0(2(1(0(0(x)))))))))))))->[], 1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))->[1], 1(0(1(1(0(1(0(2(1(0(0(x)))))))))))->[1, 1], 0(1(1(0(1(0(2(1(0(0(x))))))))))->[1, 1, 1], 1(1(0(1(0(2(1(0(0(x)))))))))->[1, 1, 1, 1], 1(0(1(0(2(1(0(0(x))))))))->[1, 1, 1, 1, 1], 0(1(0(2(1(0(0(x)))))))->[1, 1, 1, 1, 1, 1], 1(0(2(1(0(0(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(2(1(0(0(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 2(1(0(0(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(0(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(0(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))) -> 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), id: 8, possubterms: 0(1(1(1(2(1(2(0(1(2(1(0(1(x)))))))))))))->[], 1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))->[1], 1(1(2(1(2(0(1(2(1(0(1(x)))))))))))->[1, 1], 1(2(1(2(0(1(2(1(0(1(x))))))))))->[1, 1, 1], 2(1(2(0(1(2(1(0(1(x)))))))))->[1, 1, 1, 1], 1(2(0(1(2(1(0(1(x))))))))->[1, 1, 1, 1, 1], 2(0(1(2(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 0(1(2(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(2(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 2(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))) -> 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), id: 9, possubterms: 0(2(0(0(1(1(2(0(1(0(1(0(2(x)))))))))))))->[], 2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))->[1], 0(0(1(1(2(0(1(0(1(0(2(x)))))))))))->[1, 1], 0(1(1(2(0(1(0(1(0(2(x))))))))))->[1, 1, 1], 1(1(2(0(1(0(1(0(2(x)))))))))->[1, 1, 1, 1], 1(2(0(1(0(1(0(2(x))))))))->[1, 1, 1, 1, 1], 2(0(1(0(1(0(2(x)))))))->[1, 1, 1, 1, 1, 1], 0(1(0(1(0(2(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(0(1(0(2(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(2(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(2(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(2(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 2(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))) -> 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), id: 10, possubterms: 1(0(2(0(0(2(0(1(2(0(1(0(1(x)))))))))))))->[], 0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))->[1], 2(0(0(2(0(1(2(0(1(0(1(x)))))))))))->[1, 1], 0(0(2(0(1(2(0(1(0(1(x))))))))))->[1, 1, 1], 0(2(0(1(2(0(1(0(1(x)))))))))->[1, 1, 1, 1], 2(0(1(2(0(1(0(1(x))))))))->[1, 1, 1, 1, 1], 0(1(2(0(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 1(2(0(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 2(0(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))) -> 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), id: 11, possubterms: 1(0(2(0(2(1(0(2(0(1(1(2(0(x)))))))))))))->[], 0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))->[1], 2(0(2(1(0(2(0(1(1(2(0(x)))))))))))->[1, 1], 0(2(1(0(2(0(1(1(2(0(x))))))))))->[1, 1, 1], 2(1(0(2(0(1(1(2(0(x)))))))))->[1, 1, 1, 1], 1(0(2(0(1(1(2(0(x))))))))->[1, 1, 1, 1, 1], 0(2(0(1(1(2(0(x)))))))->[1, 1, 1, 1, 1, 1], 2(0(1(1(2(0(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(1(2(0(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(1(2(0(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(2(0(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 2(0(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))) -> 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), id: 12, possubterms: 1(1(0(0(2(2(2(0(1(2(0(1(1(x)))))))))))))->[], 1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))->[1], 0(0(2(2(2(0(1(2(0(1(1(x)))))))))))->[1, 1], 0(2(2(2(0(1(2(0(1(1(x))))))))))->[1, 1, 1], 2(2(2(0(1(2(0(1(1(x)))))))))->[1, 1, 1, 1], 2(2(0(1(2(0(1(1(x))))))))->[1, 1, 1, 1, 1], 2(0(1(2(0(1(1(x)))))))->[1, 1, 1, 1, 1, 1], 0(1(2(0(1(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(2(0(1(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 2(0(1(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))) -> 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), id: 13, possubterms: 1(2(0(1(0(2(0(1(0(1(2(1(0(x)))))))))))))->[], 2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))->[1], 0(1(0(2(0(1(0(1(2(1(0(x)))))))))))->[1, 1], 1(0(2(0(1(0(1(2(1(0(x))))))))))->[1, 1, 1], 0(2(0(1(0(1(2(1(0(x)))))))))->[1, 1, 1, 1], 2(0(1(0(1(2(1(0(x))))))))->[1, 1, 1, 1, 1], 0(1(0(1(2(1(0(x)))))))->[1, 1, 1, 1, 1, 1], 1(0(1(2(1(0(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(2(1(0(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(2(1(0(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 2(1(0(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))) -> 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), id: 14, possubterms: 1(2(1(2(0(0(0(1(1(1(0(0(1(x)))))))))))))->[], 2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))->[1], 1(2(0(0(0(1(1(1(0(0(1(x)))))))))))->[1, 1], 2(0(0(0(1(1(1(0(0(1(x))))))))))->[1, 1, 1], 0(0(0(1(1(1(0(0(1(x)))))))))->[1, 1, 1, 1], 0(0(1(1(1(0(0(1(x))))))))->[1, 1, 1, 1, 1], 0(1(1(1(0(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 1(1(1(0(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(1(0(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(0(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 0(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))) -> 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), id: 15, possubterms: 2(0(0(0(2(2(0(2(2(0(1(0(1(x)))))))))))))->[], 0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))->[1], 0(0(2(2(0(2(2(0(1(0(1(x)))))))))))->[1, 1], 0(2(2(0(2(2(0(1(0(1(x))))))))))->[1, 1, 1], 2(2(0(2(2(0(1(0(1(x)))))))))->[1, 1, 1, 1], 2(0(2(2(0(1(0(1(x))))))))->[1, 1, 1, 1, 1], 0(2(2(0(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 2(2(0(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 2(0(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))) -> 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), id: 16, possubterms: 2(0(2(1(0(0(1(0(0(0(1(1(1(x)))))))))))))->[], 0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))->[1], 2(1(0(0(1(0(0(0(1(1(1(x)))))))))))->[1, 1], 1(0(0(1(0(0(0(1(1(1(x))))))))))->[1, 1, 1], 0(0(1(0(0(0(1(1(1(x)))))))))->[1, 1, 1, 1], 0(1(0(0(0(1(1(1(x))))))))->[1, 1, 1, 1, 1], 1(0(0(0(1(1(1(x)))))))->[1, 1, 1, 1, 1, 1], 0(0(0(1(1(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(0(1(1(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(1(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(1(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))) -> 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), id: 17, possubterms: 2(0(2(1(1(1(1(0(2(0(1(0(1(x)))))))))))))->[], 0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))->[1], 2(1(1(1(1(0(2(0(1(0(1(x)))))))))))->[1, 1], 1(1(1(1(0(2(0(1(0(1(x))))))))))->[1, 1, 1], 1(1(1(0(2(0(1(0(1(x)))))))))->[1, 1, 1, 1], 1(1(0(2(0(1(0(1(x))))))))->[1, 1, 1, 1, 1], 1(0(2(0(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 0(2(0(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 2(0(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))) -> 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), id: 18, possubterms: 2(1(2(2(1(1(2(2(0(1(1(0(1(x)))))))))))))->[], 1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))->[1], 2(2(1(1(2(2(0(1(1(0(1(x)))))))))))->[1, 1], 2(1(1(2(2(0(1(1(0(1(x))))))))))->[1, 1, 1], 1(1(2(2(0(1(1(0(1(x)))))))))->[1, 1, 1, 1], 1(2(2(0(1(1(0(1(x))))))))->[1, 1, 1, 1, 1], 2(2(0(1(1(0(1(x)))))))->[1, 1, 1, 1, 1, 1], 2(0(1(1(0(1(x))))))->[1, 1, 1, 1, 1, 1, 1], 0(1(1(0(1(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 1(1(0(1(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(1(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])
 (rule: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))) -> 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), id: 19, possubterms: 2(2(1(1(1(1(0(1(1(2(0(1(0(x)))))))))))))->[], 2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))->[1], 1(1(1(1(0(1(1(2(0(1(0(x)))))))))))->[1, 1], 1(1(1(0(1(1(2(0(1(0(x))))))))))->[1, 1, 1], 1(1(0(1(1(2(0(1(0(x)))))))))->[1, 1, 1, 1], 1(0(1(1(2(0(1(0(x))))))))->[1, 1, 1, 1, 1], 0(1(1(2(0(1(0(x)))))))->[1, 1, 1, 1, 1, 1], 1(1(2(0(1(0(x))))))->[1, 1, 1, 1, 1, 1, 1], 1(2(0(1(0(x)))))->[1, 1, 1, 1, 1, 1, 1, 1], 2(0(1(0(x))))->[1, 1, 1, 1, 1, 1, 1, 1, 1], 0(1(0(x)))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 1(0(x))->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1], 0(x)->[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1])

-> Unifications:
(R1 unifies with R3 at p: [1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 0(0(1(0(1(x))))), sig: {x -> 0(1(0(0(1(0(2(0(x'))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R1 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R1 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R1 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R1 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R1 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R1 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R1 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R1 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R1 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R2 unifies with R13 at p: [1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(2(0(1(x)))), sig: {x -> 0(2(0(1(0(1(2(1(0(x')))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R2 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R2 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R2 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R2 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R2 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R2 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R2 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R2 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R2 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R3 unifies with R5 at p: [1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(1(0(2(0(x))))), sig: {x -> 2(1(0(0(1(0(1(1(x'))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R3 unifies with R10 at p: [1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 1(0(2(0(x)))), sig: {x -> 0(2(0(1(2(0(1(0(1(x')))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R3 unifies with R11 at p: [1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 1(0(2(0(x)))), sig: {x -> 2(1(0(2(0(1(1(2(0(x')))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R3 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(2(0(x))), sig: {x -> 0(1(1(2(0(1(0(1(0(2(x'))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R3 unifies with R15 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 0(0(2(2(0(2(2(0(1(0(1(x')))))))))))}, l': 2(0(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x'))))))))))))))))))
(R3 unifies with R16 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 2(1(0(0(1(0(0(0(1(1(1(x')))))))))))}, l': 2(0(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x'))))))))))))))))))
(R3 unifies with R17 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 2(1(1(1(1(0(2(0(1(0(1(x')))))))))))}, l': 2(0(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x'))))))))))))))))))
(R3 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R3 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R3 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R3 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R3 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R3 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R3 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R3 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R3 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))), lp: 0(x), sig: {x -> 2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R4 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(1(x)), sig: {x -> 0(0(2(2(2(0(1(2(0(1(1(x')))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R4 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R4 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R4 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R4 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R4 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R5 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 0(1(1(x))), sig: {x -> 0(1(1(0(1(0(2(1(0(0(x'))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R5 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 0(1(1(x))), sig: {x -> 1(2(1(2(0(1(2(1(0(1(x'))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R5 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(1(x)), sig: {x -> 0(0(2(2(2(0(1(2(0(1(1(x')))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R5 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R5 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R5 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R5 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R5 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R6 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R6 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R6 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R6 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R6 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R6 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R6 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R6 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R6 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R7 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(0(x)), sig: {x -> 0(1(2(1(1(1(0(0(1(0(1(x')))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R7 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(0(x)), sig: {x -> 1(0(0(1(1(1(0(1(2(0(1(x')))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R7 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(0(x)), sig: {x -> 1(0(1(0(1(0(0(1(0(2(0(x')))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R7 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(0(x)), sig: {x -> 1(1(1(1(1(2(1(1(2(1(1(x')))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R7 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R7 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R7 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R7 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R7 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R7 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R7 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R7 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R7 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))), lp: 0(x), sig: {x -> 2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R8 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R8 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R8 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R8 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R8 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R8 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R8 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R8 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R8 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R9 unifies with R5 at p: [1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 0(1(0(2(x)))), sig: {x -> 0(2(1(0(0(1(0(1(1(x')))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R9 unifies with R6 at p: [1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 0(1(0(2(x)))), sig: {x -> 2(1(1(2(1(2(2(0(1(x')))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R9 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 1(0(2(x))), sig: {x -> 0(0(2(0(1(2(0(1(0(1(x'))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R9 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 1(0(2(x))), sig: {x -> 0(2(1(0(2(0(1(1(2(0(x'))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R9 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 0(2(x)), sig: {x -> 0(0(1(1(2(0(1(0(1(0(2(x')))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R9 unifies with R15 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 2(x), sig: {x -> 0(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))}, l': 2(0(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x'))))))))))))))))))
(R9 unifies with R16 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 2(x), sig: {x -> 0(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))}, l': 2(0(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x'))))))))))))))))))
(R9 unifies with R17 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 2(x), sig: {x -> 0(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))}, l': 2(0(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x'))))))))))))))))))
(R9 unifies with R18 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 2(x), sig: {x -> 1(2(2(1(1(2(2(0(1(1(0(1(x'))))))))))))}, l': 2(1(2(2(1(1(2(2(0(1(1(0(1(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x'))))))))))))))))))
(R9 unifies with R19 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))), lp: 2(x), sig: {x -> 2(1(1(1(1(0(1(1(2(0(1(0(x'))))))))))))}, l': 2(2(1(1(1(1(0(1(1(2(0(1(0(x'))))))))))))), r: 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x))))))))))))))))), r': 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x'))))))))))))))))))
(R10 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R10 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R10 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R10 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R10 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R10 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R10 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R10 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R10 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R11 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 1(2(0(x))), sig: {x -> 1(0(2(0(1(0(1(2(1(0(x'))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R11 unifies with R15 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 0(0(2(2(0(2(2(0(1(0(1(x')))))))))))}, l': 2(0(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x'))))))))))))))))))
(R11 unifies with R16 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 2(1(0(0(1(0(0(0(1(1(1(x')))))))))))}, l': 2(0(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x'))))))))))))))))))
(R11 unifies with R17 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 2(0(x)), sig: {x -> 2(1(1(1(1(0(2(0(1(0(1(x')))))))))))}, l': 2(0(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x'))))))))))))))))))
(R11 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R11 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R11 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R11 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R11 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R11 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R11 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R11 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R11 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))), lp: 0(x), sig: {x -> 2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R12 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 0(1(1(x))), sig: {x -> 0(1(1(0(1(0(2(1(0(0(x'))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R12 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 0(1(1(x))), sig: {x -> 1(2(1(2(0(1(2(1(0(1(x'))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R12 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(1(x)), sig: {x -> 0(0(2(2(2(0(1(2(0(1(1(x')))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R12 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R12 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R12 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R12 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R12 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R13 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 1(0(x)), sig: {x -> 2(0(0(2(0(1(2(0(1(0(1(x')))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R13 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 1(0(x)), sig: {x -> 2(0(2(1(0(2(0(1(1(2(0(x')))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R13 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R13 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R13 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R13 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R13 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R13 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R13 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R13 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R13 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))), lp: 0(x), sig: {x -> 2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))
(R14 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(0(1(x))), sig: {x -> 0(0(1(1(1(0(1(2(0(1(x'))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R14 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(0(1(x))), sig: {x -> 0(1(0(1(0(0(1(0(2(0(x'))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R14 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(0(1(x))), sig: {x -> 1(1(1(1(2(1(1(2(1(1(x'))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R14 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R14 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R14 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R14 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R14 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R14 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R14 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R14 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R14 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R15 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R15 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R15 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R15 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R15 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R15 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R15 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R15 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R15 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R16 unifies with R4 at p: [1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 0(0(1(1(1(x))))), sig: {x -> 1(1(2(1(1(2(1(1(x'))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R16 unifies with R8 at p: [1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 0(1(1(1(x)))), sig: {x -> 2(1(2(0(1(2(1(0(1(x')))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R16 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(1(x)), sig: {x -> 0(0(2(2(2(0(1(2(0(1(1(x')))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R16 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R16 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R16 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R16 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R16 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R17 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R17 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R17 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R17 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R17 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R17 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R17 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R17 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R17 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R18 unifies with R7 at p: [1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 0(1(1(0(1(x))))), sig: {x -> 1(0(1(0(2(1(0(0(x'))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R18 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(0(2(1(0(0(1(0(1(1(x')))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R18 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 0(2(2(1(1(2(1(2(2(0(1(x')))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R18 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(0(1(1(0(1(0(2(1(0(0(x')))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R18 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 0(1(x)), sig: {x -> 1(1(2(1(2(0(1(2(1(0(1(x')))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R18 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R18 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R18 unifies with R12 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))}, l': 1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))
(R18 unifies with R13 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R18 unifies with R14 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))), lp: 1(x), sig: {x -> 2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))}, l': 1(2(1(2(0(0(0(1(1(1(0(0(1(x'))))))))))))), r: 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x))))))))))))))))), r': 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))
(R19 unifies with R13 at p: [1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 1(2(0(1(0(x))))), sig: {x -> 2(0(1(0(1(2(1(0(x'))))))))}, l': 1(2(0(1(0(2(0(1(0(1(2(1(0(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))
(R19 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(1(0(x))), sig: {x -> 2(0(2(1(0(0(1(0(1(1(x'))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R19 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(1(0(x))), sig: {x -> 2(2(1(1(2(1(2(2(0(1(x'))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R19 unifies with R10 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 1(0(x)), sig: {x -> 2(0(0(2(0(1(2(0(1(0(1(x')))))))))))}, l': 1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))
(R19 unifies with R11 at p: [1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 1(0(x)), sig: {x -> 2(0(2(1(0(2(0(1(1(2(0(x')))))))))))}, l': 1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))
(R19 unifies with R1 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))}, l': 0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))
(R19 unifies with R2 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))}, l': 0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))
(R19 unifies with R3 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))}, l': 0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))
(R19 unifies with R4 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))}, l': 0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))
(R19 unifies with R5 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))}, l': 0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))
(R19 unifies with R6 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))}, l': 0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))
(R19 unifies with R7 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))}, l': 0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))
(R19 unifies with R8 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))}, l': 0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))
(R19 unifies with R9 at p: [1,1,1,1,1,1,1,1,1,1,1,1], l: 2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))), lp: 0(x), sig: {x -> 2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))}, l': 0(2(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))), r: 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x))))))))))))))))), r': 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))

-> Critical pairs info:
<0(0(1(0(1(0(1(0(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<1(2(1(2(0(0(0(1(1(1(0(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N2
<0(1(1(0(1(1(0(1(0(2(1(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x')))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(1(1(1(1(2(1(1(2(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<0(0(1(1(1(1(1(2(1(1(2(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N4
<1(0(2(0(0(2(0(1(2(0(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N5
<1(0(2(0(2(1(0(2(0(1(1(2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x')))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N6
<2(0(2(1(1(1(1(0(2(0(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N7
<2(2(1(1(1(1(0(1(1(2(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x')))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N8
<1(2(0(1(0(2(0(1(0(1(2(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x')))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(2(0(2(1(0(2(0(1(1(2(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N9
<2(1(2(2(1(1(2(2(0(1(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N10
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N11
<2(1(2(2(1(1(2(2(0(1(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N12
<1(1(0(0(2(2(2(0(1(2(0(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N13
<0(0(1(0(1(0(1(0(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x')))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(2(0(1(2(0(1(0(1(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N14
<1(1(0(0(2(2(2(0(1(2(0(1(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N15
<1(0(2(0(2(1(0(2(0(1(1(2(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(0(0(1(2(1(1(1(0(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N16
<2(0(0(0(2(2(0(2(2(0(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N17
<0(0(1(0(1(0(1(0(0(1(0(2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x')))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N18
<0(1(0(2(0(2(1(0(0(1(0(1(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N19
<0(2(0(0(1(1(2(0(1(0(1(0(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x'))))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(2(1(0(0(1(0(0(0(1(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N20
<0(0(1(0(0(1(1(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x')))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(0(2(0(1(0(1(2(1(0(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N21
<0(0(0(1(2(1(1(1(0(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N22
<1(2(1(2(0(0(0(1(1(1(0(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N23
<2(2(1(1(1(1(0(1(1(2(0(1(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(0(0(1(2(1(1(1(0(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N24
<0(0(1(0(0(1(1(1(0(1(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N25
<0(2(0(0(1(1(2(0(1(0(1(0(2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x'))))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(2(1(1(1(1(0(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N26
<2(0(0(0(2(2(0(2(2(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N27
<0(0(1(0(0(1(1(1(0(1(2(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N28
<0(0(1(0(1(0(1(0(0(1(0(2(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(2(0(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N29
<0(0(1(0(0(1(1(1(0(1(2(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N30
<0(1(1(1(2(1(2(0(1(2(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N31
<0(0(1(0(0(1(1(1(0(1(2(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N32
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N33
<0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N34
<0(2(0(0(1(1(2(0(1(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x')))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(0(1(1(2(0(1(0(1(0(2(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N35
<0(1(1(0(1(1(0(1(0(2(1(0(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(2(0(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N36
<2(0(2(1(1(1(1(0(2(0(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N37
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(1(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N38
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N39
<2(1(2(2(1(1(2(2(0(1(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N40
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(1(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N41
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N42
<2(1(2(2(1(1(2(2(0(1(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N43
<0(2(0(0(1(1(2(0(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N44
<2(0(0(0(2(2(0(2(2(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N45
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N46
<1(0(2(0(2(1(0(2(0(1(1(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x')))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N47
<0(1(1(0(1(1(0(1(0(2(1(0(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(0(0(1(2(1(1(1(0(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N48
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N49
<0(1(0(2(2(1(1(2(1(2(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N50
<1(2(1(2(0(0(0(1(1(1(0(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N51
<0(0(1(0(0(1(1(1(0(1(2(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N52
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N53
<2(1(2(2(1(1(2(2(0(1(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N54
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N55
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N56
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N57
<0(0(0(1(2(1(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N58
<0(1(0(2(0(2(1(0(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N59
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N60
<2(1(2(2(1(1(2(2(0(1(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N61
<2(0(2(1(1(1(1(0(2(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N62
<2(0(2(1(0(0(1(0(0(0(1(1(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N63
<2(0(2(1(1(1(1(0(2(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N64
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N65
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N66
<0(0(0(1(2(1(1(1(0(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N67
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N68
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N69
<2(0(2(1(0(0(1(0(0(0(1(1(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N70
<1(2(1(2(0(0(0(1(1(1(0(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N71
<1(0(2(0(0(2(0(1(2(0(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N72
<2(0(0(0(2(2(0(2(2(0(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N73
<1(2(0(1(0(2(0(1(0(1(2(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N74
<1(0(2(0(0(2(0(1(2(0(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N75
<1(2(1(2(0(0(0(1(1(1(0(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N76
<2(0(2(1(1(1(1(0(2(0(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N77
<0(0(1(1(1(1(1(2(1(1(2(1(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N78
<2(0(2(1(0(0(1(0(0(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N79
<0(1(1(1(2(1(2(0(1(2(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N80
<0(2(0(0(1(1(2(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N81
<1(2(1(2(0(0(0(1(1(1(0(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N82
<0(0(1(0(1(0(1(0(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N83
<0(1(0(2(0(2(1(0(0(1(0(1(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N84
<2(2(1(1(1(1(0(1(1(2(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N85
<2(0(0(0(2(2(0(2(2(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N86
<1(2(1(2(0(0(0(1(1(1(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N87
<1(0(2(0(0(2(0(1(2(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N88
<0(1(0(2(0(2(1(0(0(1(0(1(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N89
<1(0(2(0(0(2(0(1(2(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N90
<1(1(0(0(2(2(2(0(1(2(0(1(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N91
<2(2(1(1(1(1(0(1(1(2(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N92
<2(0(2(1(0(0(1(0(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N93
<2(1(2(2(1(1(2(2(0(1(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N94
<0(1(0(2(2(1(1(2(1(2(2(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N95
<0(0(1(0(1(0(1(0(0(1(0(2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x')))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(0(2(2(0(2(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N96
<1(0(2(0(2(1(0(2(0(1(1(2(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(2(0(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N97
<0(2(0(0(1(1(2(0(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N98
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(1(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N99
<2(1(2(2(1(1(2(2(0(1(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N100
<0(1(1(1(2(1(2(0(1(2(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N101
<2(2(1(1(1(1(0(1(1(2(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(0(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N102
<2(2(1(1(1(1(0(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N103
<0(0(0(1(2(1(1(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N104
<2(0(2(1(1(1(1(0(2(0(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N105
<2(0(2(1(0(0(1(0(0(0(1(1(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N106
<0(1(1(0(1(1(0(1(0(2(1(0(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N107
<0(0(1(0(0(1(1(1(0(1(2(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N108
<1(2(1(2(0(0(0(1(1(1(0(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N109
<0(2(0(0(1(1(2(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N110
<0(0(1(0(1(0(1(0(0(1(0(2(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(0(1(2(1(1(1(0(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N111
<2(0(2(1(0(0(1(0(0(0(1(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x')))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N112
<0(0(1(1(1(1(1(2(1(1(2(1(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N113
<2(2(1(1(1(1(0(1(1(2(0(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N114
<0(0(1(0(1(0(1(0(0(1(0(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x')))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(2(1(0(0(1(0(0(0(1(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N115
<0(1(0(2(2(1(1(2(1(2(2(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N116
<2(0(2(1(1(1(1(0(2(0(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N117
<2(0(2(1(0(0(1(0(0(0(1(1(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N118
<0(0(0(1(2(1(1(1(0(0(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N119
<0(0(1(1(1(1(1(2(1(1(2(1(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N120
<2(0(0(0(2(2(0(2(2(0(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N121
<1(2(1(2(0(0(0(1(1(1(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N122
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N123
<2(1(2(2(1(1(2(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N124
<1(0(2(0(0(2(0(1(2(0(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N125
<0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N126
<1(1(0(0(2(2(2(0(1(2(0(1(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N127
<2(0(0(0(2(2(0(2(2(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N128
<0(0(1(0(1(0(1(0(0(1(0(2(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N129
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N130
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x')))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(0(1(2(1(1(1(0(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N131
<0(0(0(1(2(1(1(1(0(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N132
<0(0(1(1(1(1(1(2(1(1(2(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x')))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N133
<0(1(0(2(2(1(1(2(1(2(2(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N134
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N135
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N136
<1(2(1(2(0(0(0(1(1(1(0(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N137
<0(2(0(0(1(1(2(0(1(0(1(0(0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x'))))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(2(1(1(1(1(0(1(1(2(0(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N138
<1(0(2(0(2(1(0(2(0(1(1(2(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(1(0(2(0(2(1(0(0(1(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N139
<1(2(1(2(0(0(0(1(1(1(0(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N140
<0(0(1(0(0(1(1(1(0(1(2(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N141
<0(0(1(0(0(1(1(1(0(1(2(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N142
<0(2(0(0(1(1(2(0(1(0(1(0(2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x'))))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(1(2(2(1(1(2(2(0(1(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N143
<0(1(0(2(2(1(1(2(1(2(2(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N144
<0(0(1(0(0(1(1(1(0(1(2(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N145
<2(1(2(2(1(1(2(2(0(1(1(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x')))))))))))))))))))))))))))),2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(1(0(1(1(0(1(0(2(1(0(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N146
<1(0(2(0(2(1(0(2(0(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N147
<0(1(1(1(2(1(2(0(1(2(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N148
<0(1(1(1(2(1(2(0(1(2(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N149
<1(2(1(2(0(0(0(1(1(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x'))))))))))))))))))))))))))),1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(0(1(0(1(0(0(1(0(2(0(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N150
<0(1(0(2(2(1(1(2(1(2(2(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N151
<2(0(0(0(2(2(0(2(2(0(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N152
<0(1(1(0(1(1(0(1(0(2(1(0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x')))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(1(0(2(0(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N153
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N154
<0(1(1(0(1(1(0(1(0(2(1(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x')))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(0(1(1(1(0(1(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N155
<1(1(0(0(2(2(2(0(1(2(0(1(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N156
<2(0(2(1(1(1(1(0(2(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N157
<1(0(2(0(0(2(0(1(2(0(1(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N158
<2(2(1(1(1(1(0(1(1(2(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x')))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N159
<2(0(0(0(2(2(0(2(2(0(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N160
<1(1(0(0(2(2(2(0(1(2(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N161
<1(1(0(0(2(2(2(0(1(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N162
<0(1(0(2(0(2(1(0(0(1(0(1(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N163
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N164
<1(0(2(0(2(1(0(2(0(1(1(2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x')))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(2(1(1(1(1(0(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N165
<0(2(0(0(1(1(2(0(1(0(1(0(2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x'))))))))))))))))))))))))))))),0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(0(0(0(2(2(0(2(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N166
<0(1(0(2(2(1(1(2(1(2(2(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N167
<1(0(2(0(0(2(0(1(2(0(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N168
<0(1(1(1(2(1(2(0(1(2(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N169
<0(0(1(0(1(0(1(0(0(1(0(2(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N170
<0(0(0(1(2(1(1(1(0(0(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N171
<2(0(2(1(1(1(1(0(2(0(1(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x')))))))))))))))))))))))))))),2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(0(2(2(1(1(2(1(2(2(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N172
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(1(1(0(1(1(0(1(0(2(1(0(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N173
<0(1(1(0(1(1(0(1(0(2(1(0(0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(1(2(1(1(2(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N174
<1(1(0(0(2(2(2(0(1(2(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x')))))))))))))))))))))))))))),1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N175
<1(2(0(1(0(2(0(1(0(1(2(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x')))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(2(0(0(2(0(1(2(0(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N176
<0(1(0(2(0(2(1(0(0(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N177
<0(1(0(2(2(1(1(2(1(2(2(0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x')))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(0(2(0(2(1(0(0(1(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N178
<0(0(0(1(2(1(1(1(0(0(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N179
<0(1(1(1(2(1(2(0(1(2(1(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x'))))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(0(2(0(2(1(0(2(0(1(1(2(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N180
<0(1(0(2(2(1(1(2(1(2(2(0(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N181
<0(1(0(2(0(2(1(0(0(1(0(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N182
<1(0(2(0(0(2(0(1(2(0(1(0(1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x'))))))))))))))))))))))))))))),1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(2(1(2(0(0(0(1(1(1(0(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N183
<2(2(1(1(1(1(0(1(1(2(0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x'))))))))))))))))))))))))))),0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(2(2(1(1(2(1(2(2(0(1(x')))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N184
<1(0(2(0(2(1(0(2(0(1(1(2(0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x'))))))))))))))))))))))))))))),1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(0(1(0(0(1(1(1(0(1(2(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N185
<1(2(0(1(0(2(0(1(0(1(2(1(0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(0(0(1(2(1(1(1(0(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N186
<1(2(0(1(0(2(0(1(0(1(2(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(1(1(1(2(1(2(0(1(2(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N187
<2(0(2(1(0(0(1(0(0(0(1(1(1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x'))))))))))))))))))))))))))))),0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(2(0(1(0(2(0(1(0(1(2(1(0(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N188
<0(1(1(1(2(1(2(0(1(2(1(0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x')))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(1(1(2(1(2(0(1(2(1(0(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N189
<1(2(0(1(0(2(0(1(0(1(2(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))))),1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(2(0(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N190
<0(1(1(1(2(1(2(0(1(2(1(0(1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x'))))))))))))))))))))))))))))),0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(0(2(0(0(2(0(1(2(0(1(0(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N191
<0(0(1(0(1(0(1(0(0(1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x')))))))))))))))))))))))))),0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(2(1(0(2(0(1(1(2(0(x'))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N192
<0(0(1(1(1(1(1(2(1(1(2(1(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x'))))))))))))))))))))))))))))),0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(1(0(0(2(2(2(0(1(2(0(1(1(x')))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N193
<0(1(0(2(0(2(1(0(0(1(0(1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x')))))))))))))))))))))))))))),0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(0(0(2(2(2(0(1(2(0(1(1(x'))))))))))))))))))))))))))))>   =>  Not trivial, Not overlay, Proper, NW0, N194

-> Problem conclusions:
 Left linear, Right linear, Linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 


Problem 1: 
No Convergence Brute Force Procedure:
-> Rewritings:
s: 0(0(1(0(1(0(1(0(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x')))))))))))))))))))))))))))
Nodes: [0]
Edges: []
ID: 0 => ('0(0(1(0(1(0(1(0(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x')))))))))))))))))))))))))))', D0)
t: 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))
Nodes: [0]
Edges: []
ID: 0 => ('0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))', D0)
0(0(1(0(1(0(1(0(0(1(0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x'))))))))))))))))))))))))))) ->* no union *<- 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(0(1(1(2(0(1(0(1(0(2(x')))))))))))))))))))))))))))
"Not joinable"

The problem is not confluent.