pure-prover-gtrailで newgoallistの制御がおかしくて消えていく

[sazare]

★unifyに失敗しているのにgoallistから消去しているのはなぜ???
pure-prover-gtrailで newgoallistの制御がおかしくて消えていく

(require :gtrail)
(in-package :rubbish)
(defparameter fkname "kqc/cake/cake006-sim1.kqc")
;; run
(defparameter max-clauses 10000)
(defparameter max-trials 1000)
(defparameter max-steps 1000)
(defparameter timeout-sec 10)

(logshow)
の最後あたりをみよ。

何か変だ

[sazare]

step-solverで
(setq newgoal (step-solver goal))

     (multiple-value-setq (newgoals cs ts) (gathercontra newgoal) )
     (setq *contradictions* (append cs *contradictions*))

     (setq valids (append ts valids))
     (setq goallist (append (list newgoal) newgoals goallist))

; (setq goallist (append goallist newgoals))
(setq newgoal nil)
(setq goallist goallist)

goallistをupdateしているが、どうもうまくいっていない。

そもそもどうなっていればよいのか、考え直すこと