## TODO - [ ] reduce - [ ] apply - [ ] better satisfy all - [ ] o(1) check for unsatisifability keep track of leaves
