4. even(sum(two_sq,b))                          [15]
2. two_sq = four                                [9]
5. ~zero(X) | diff(four,X) = sum(four,X)        [26]
1. zero(b)                                      [8]
3. ~even(diff(two_sq,b))                        [14]

6.  5+2 = ~zero(X) | diff(four,X) = sum(two_sq,X) [25]

7. 6+4 = ~zero(b) | even(diff(four,b))           [23]

8. 7+2 = ~zero(b) | even(diff(two_sq,b))         [22]

9. 8+3 = ~zero(b)                                [8]

9+1 = FALSE

{{zero(b),zero(b)}}   <     {{even(diff(four,b))}}

{zero(b),zero(b)}     <     {even(diff(four,b))}

zero(b)               <     even(diff(four,b))