Az üvös kockara az algoritmus peldaul a lentebb megadott könyvben is megtalahato, es meg csak nem is szörnyen kompliklalt. Lehet, hogy az optimali lepesszamban tevedek, de ugy emlekszem egy olyan tekeressorozatot (visszaforditva a büvös kocka nyelvre) talal, hogy a leghosszabb kirakas optimalis (ez sem hosszu: körülbelül a permutaciocsoport foka), a rövidebben kirakhatok nem feltetlenül optimalisak, de nagyon közel vannak hozza.

A tetelbizonyito progrmmal nyilvan az a baj, hogy cel nelkül kezd bizonyitgatni, szerintem elvileg lehetseges celokat is beepiteni egy ilyen programba, es akkor lenyegesen jobb eredmenyeket produkalna. Söt a legjobb egy rugalmas önfelülvizsglao es modosito celrendszer lenne. Szerintem ez is lehetseges, csak nem tudok rol, hogy valaki is megvalositotta volna.