(assert! (rule (smaller () ?x)))
(assert! (rule (smaller (a . ?x) (a . ?y))
(smaller ?x ?y)))
(assert! (rule (plus () ?y ?y)))
(assert! (rule (plus (a . ?x) ?y (a . ?z))
(plus ?x ?y ?z)))
(assert! (rule (times () ?x ())))
(assert! (rule (times (a . ?x) ?y ?z)
(and (smaller (a . ?x) ?z)
(smaller ?y ?z)
(times ?x ?y ?w)
(plus ?w ?y ?z))))