Maude> in jugs .
==========================================
mod WATER-JUGS
Maude> search [1] jug(1,3,0) & jug(2,5,0) =>+ jug(2,5,4) & S:State .
search [1] in WATER-JUGS : jug(1, 3, 0) & jug(2, 5, 0) =>+ S:State & jug(2, 5,
    4) .

Solution 1 (state 13)
states: 14  rewrites: 190 in 1ms cpu (1ms real) (190000 rewrites/second)
S:State --> jug(1, 3, 3)
Maude> show path 13 .
state 0, State: jug(1, 3, 0) & jug(2, 5, 0)
===[ rl jug(J1, Cap, F1) => jug(J1, Cap, Cap) [label fill] . ]===>
state 2, State: jug(1, 3, 0) & jug(2, 5, 5)
===[ crl jug(J1, Cap1, F1) & jug(J2, Cap2, F2) => jug(J1, Cap1, F1 - (Cap2 -
    F2)) & jug(J2, Cap2, Cap2) if F1 > 0 = true /\ F1 - (Cap2 - F2) >= 0 = true
    [label transfer2] . ]===>
state 5, State: jug(1, 3, 3) & jug(2, 5, 2)
===[ rl jug(J1, Cap, F1) => jug(J1, Cap, 0) [label spill] . ]===>
state 7, State: jug(1, 3, 0) & jug(2, 5, 2)
===[ crl jug(J1, Cap1, F1) & jug(J2, Cap2, F2) => jug(J1, Cap1, 0) & jug(J2,
    Cap2, F1 + F2) if F1 > 0 = true /\ F1 + F2 <= Cap2 = true [label transfer1]
    . ]===>
state 9, State: jug(1, 3, 2) & jug(2, 5, 0)
===[ rl jug(J1, Cap, F1) => jug(J1, Cap, Cap) [label fill] . ]===>
state 11, State: jug(1, 3, 2) & jug(2, 5, 5)
===[ crl jug(J1, Cap1, F1) & jug(J2, Cap2, F2) => jug(J1, Cap1, F1 - (Cap2 -
    F2)) & jug(J2, Cap2, Cap2) if F1 > 0 = true /\ F1 - (Cap2 - F2) >= 0 = true
    [label transfer2] . ]===>
state 13, State: jug(1, 3, 3) & jug(2, 5, 4)
Maude>