Fixed: split literals were deleted too aggressively from PEL
Suppose we need to split p and q to show c. Before, the following would happen: 1. p 2. q 3. ~q 4. ~p because during 2./3., q was deleted from PEL. Now, the following happens: 1. p 2. q 3. ~q 4. ~p 5. q 6. ~q 7. q 8. ~q Sadly, this is much more expensive, obviously.
Loading
Please register or sign in to comment