-- PHILAC1PROOF


Derivation of

loop[source]

Narrowing the preceding formula leads to 

loop[think(a)^think(b)^think(c)^think(d)^avail(f1)^avail(f2)^avail(f3)^avail(f4)]

Reducts have been simplified.

Narrowing the preceding formula leads to 

loop[eat(d)^think(a)^think(b)^think(c)^avail(f2)^avail(f3),think(a)^
                                                           think(b)^
                                                           think(c)^
                                                           think(d)^avail(f1)^avail(f2)^avail(f3)^avail(f4)]

Reducts have been simplified.

Narrowing the preceding formula leads to 

loop[eat(b)^think(a)^eat(d)^think(c),eat(d)^think(a)^think(b)^think(c)^avail(f2)^avail(f3),think(a)^
                                                                                           think(b)^
                                                                                           think(c)^
                                                                                           think(d)^
                                                                                           avail(f1)^
                                                                                           avail(f2)^
                                                                                           avail(f3)^avail(f4)]

Reducts have been simplified.

Narrowing the preceding formula leads to 

True

Reducts have been simplified.

Number of proof steps: 4

Solutions:

True