In my previous post I solved this problem with prolog. Here I have written a solution using the rewrite logic of the Maude system.

```
mod FARMER is
sort GameState .
sort Bank .
sort Actor .
subsort Actor < Bank .
op state : Bank Bank -> GameState [ ctor ] .
ops Farmer, Fox, Chicken, Grain : -> Actor [ ctor ] .
op Empty : -> Bank [ ctor ] .
op __ : Bank Bank -> Bank [ctor assoc comm id: Empty] .
op safe : Bank -> Bool .
vars A1 : Actor .
vars X Y Z : Bank .
eq safe( Farmer X ) = true .
eq safe( Chicken Fox X) = false .
eq safe( Chicken Grain X) = false .
eq safe( X ) = true [owise] .
crl [cross_with] : state((Farmer A1 X),Y) => state(X,(Farmer A1 Y)) if safe(X) .
crl [cross_alone] : state((Farmer X),Z) => state(X,(Farmer Z)) if safe(X) .
crl [cross_back_with] : state(X,(Farmer A1 Z)) => state((Farmer A1 X),Z) if safe(Z) .
crl [cross_back_alone] : state(X,(Farmer Z)) => state((Farmer X),Z) if safe(Z) .
endm
```

Maude has a built-in search mechanism that allows us to find a solution:

```
Maude> search state(Farmer Fox Chicken Grain,Empty) =>+ state(Empty, Farmer Grain Chicken Fox) .
search in FARMER : state(Farmer Fox Chicken Grain, Empty) =>+ state(Empty, Farmer Fox Chicken Grain) .
Solution 1 (state 9)
states: 10 rewrites: 43 in 0ms cpu (0ms real) (~ rewrites/second)
empty substitution
No more solutions.
states: 10 rewrites: 50 in 0ms cpu (0ms real) (~ rewrites/second)
Maude> show path 9 .
state 0, GameState: state(Farmer Fox Chicken Grain, Empty)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 1, GameState: state(Fox Grain, Farmer Chicken)
===[ crl state(X, Farmer Z) => state(Farmer X, Z) if safe(Z) = true [label cross_back_alone] . ]===>
state 2, GameState: state(Farmer Fox Grain, Chicken)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 3, GameState: state(Grain, Farmer Fox Chicken)
===[ crl state(X, Farmer Z A1) => state(Farmer X A1, Z) if safe(Z) = true [label cross_back_with] . ]===>
state 5, GameState: state(Farmer Chicken Grain, Fox)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 7, GameState: state(Chicken, Farmer Fox Grain)
===[ crl state(X, Farmer Z) => state(Farmer X, Z) if safe(Z) = true [label cross_back_alone] . ]===>
state 8, GameState: state(Farmer Chicken, Fox Grain)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 9, GameState: state(Empty, Farmer Fox Chicken Grain)
```