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>