Trace of algorithm applied to the Happy(Eric) example:

InTouchWithFeelings(Andy)
GiveFootMassage(Susan,Eric)
Happy(Eric)
Trained(Andy,Susan)
WeatherToday(Sunny)

h: InTouchWithFeelings(Andy) ^ GiveFootMassage(Susan,Eric) ^ 
Trained(Andy,Susan) ^ WeatherToday(Sunny) -> Happy(Eric)

WeatherToday(Rainy)
GiveFootMassage(Frank,Eric)
InTouchWithFeelings(Bob)
Trained(Bob,Frank)
Happy(Eric)

- Replace Sunny with variable w
- Replace Andy with variable x
      bind x=Andy
- Replace Susan with y
      bind y=Susan
- realize Andy must be changed in "Trained" atom
     replace it with x since that is consistent with curr variable bindings
- realize Susan must be changed in "Trained" atom
     replace it with y since that is consistent with curr variable bindings

h: InTouchWithFeelings(x) ^ GiveFootMassage(y,Eric) ^ Trained(x,y) ^
WeatherToday(w) -> Happy(Eric)

Happy(Eric)
InTouchWithFeelings(Rupp)
Trained(Rupp,Zvi)
Owns(Eric,Porche)
GiveFootMassage(Zvi,Eric)

Get rid of WeatherToday completely

h: InTouchWithFeelings(x) ^ GiveFootMassage(y,Eric) ^ Trained(x,y)
-> Happy(Eric)

This is the target function (with different variable names).