4. even(sum(two_squared,b))                      [8]
3. two_squared = four                            [6]
8. ~zero(X) | difference(four,X) = sum(four,X)   [15]
1. zero(b)                                       [4]
5. ~even(difference(two_squared,b))              [8]
2. X = X                                         [4]

w = 2+1, p = = > alphabetic

6. 4P3 = even(sum(four,b))                       [8]

7. 5P3 = ~even(difference(four,b))               [8]

6P3 = even(sum(two_squared,b))                   [8]   WASTE OF TIME

7+3 = WASTE OF TIME

8+3 = ~zero(X) | difference(two_squared,X) = sum(four,X)
8+3 = ~zero(X) | difference(four,X) = sum(two_squared,X)

9. 8+6 = ~zero(b) | even(difference(four,b))     [8]
8+7 = ~zero(b) | ~even(sum(four,b))              [8]

9+3 = ~zero(b) | even(difference(two_squared,b)) [8]

etc. Left to the reader