| XLISP version 1.6, Copyright (c) 1985, by David Betz |
| > 1> 2> 3> 3> 2> MAKE-ARRAY-2D |
| > > 1> 2> MAKE-ARRAY-INIT |
| > > 1> 2> MAKE-ARRAY-LIST |
| > > 1> 2> 2> 1> ARRAY-INIT-ELEM |
| > > 1> 2> 2> 1> ARRAY-INIT-LIST |
| > > 1> PROCLAIM |
| > > FORMAT |
| > > DECLARE |
| > > TIME |
| > > THE |
| > > 2> PUSH |
| > > UNLESS |
| > > DEFVAR |
| > DEFCONSTANT |
| > > AREF2D |
| > > FIRST |
| > SECOND |
| > > SVREF |
| > > 2> 3> 3> 2> FLOOR |
| > > FLOORD |
| > > FLOATD |
| > > 1> 2> 3> 3> 2> MEXPT |
| > > 1> INCF |
| > > 1> 2> 2> COPY-TREE |
| > > 1> SCHAR |
| > > 1> GENTEMP |
| > > > > > > > > > > FOO |
| > > 1> 4> 5> 4> 3> 4> 2> ADD-LEMMA |
| > > 1> 3> 2> 3> ADD-LEMMA-LST |
| > > 1> 3> 5> 4> 2> 4> APPLY-SUBST |
| > > 1> 3> 2> 4> APPLY-SUBST-LST |
| > > 1> 2> FALSEP |
| > > 1> 2> ONE-WAY-UNIFY |
| > > 1> 3> 5> 4> 7> 5> 2> 3> 2> 4> 3> 4> 2> ONE-WAY-UNIFY1 |
| > > 1> 3> 2> 4> 3> 4> 2> ONE-WAY-UNIFY1-&LST |
| > > 1> 1> 3> 2> 5> 4> 5> 5> REWRITE |
| > > 1> 3> 2> 4> REWRITE-ARGS |
| > > 1> 3> 2> 3> 2> REWRITE-WITH-LEMMAS |
| > > 1> 2> 5> 7> 4> 5> 6> 4> 5> 4> 5> 4> 5> 4> 5> 6> 4> 5> 6> 4> 5> 6> 6> 1> 1> 2> 5> 4> 5> 4> 5> 4> 5> 4> 5> 6> 4> 5> 6> 4> 5> 6> 4> 5> 6> 4> 5> 6> 6> 1> 1> 2> 5> 7> 6> 4> 5> 6> 7> 6> 4> 5> 6> 4> 5> 7> 6> 4> 5> 6> 6> 4> 6> 5> 6> 4> 5> 6> 4> 6> 5> 4> 6> 5> 6> 4> 5> 1> 1> 1> 2> 6> 5> 6> 4> 6> 5> 4> 5> 6> 7> 4> 6> 5> 7> 6> 7> 4> 6> 5> 4> 6> 5> 4> 5> 6> 4> 5> 6> 4> 6> 5> 4> 6> 5> 6> 4> 6> 5> 6> 1> 1> 2> 5> 6> 4> 5> 6> 4> 5> 4> 5> 4> 5> 6> 4> 6> 5> 4> 5> 6> 4> 5> 6> 4> 5> 6> 4> 5> 4> 5> 6> 4> 6> 5> 4> 6> 5> 4> 6> 5> 6> 1> 1> 2> 6> 5> 7> 4> 5> 4> 6> 5> 4> 5> 4> 6> 5> 6> 7> 4> 6> 5> 6> 6> 4> 6> 5> 4> 7> 7> 7> 6> 5> 4> 5> 4> 6> 5> 6> 4> 6> 5> 4> 6> 5> 1> 1> 1> 2> 6> 5> 4> 5> 6> 4> 6> 5> 4> 6> 5> 4> 6> 5> 4> 6> 5> 4> 6> 5> 6> 4> 5> 4> 6> 5> 4> 6> 5> 4> 6> 5> 6> 4> 5> 4> 5> 6> 4> 6> 5> 7> 6> 1> 1> 1> 2> 6> 5> 4> 5> 8> 7> 4> 5> 6> 4> 5> 6> 4> 5> 6> 7> 4> 5> 4> 5> 6> 7> 4> 6> 5> 4> 6> 5> 6> 6> 6> 6> 7> 6> 7> 4> 6> 5> 4> 5> 4> 5> 1> 1> 2> 7> 8> 10> 11> 5> 4> 6> 5> 4> 6> 5> 4> 6> 5> 6> 4> 5> 6> 6> 4> 6> 5> 6> 6> 7> 7> 8> 4> 6> 5> 6> 8> 7> 6> 7> 1> 1> 1> 1> 2> 5> 6> 6> 4> 6> 5> 6> 6> 4> 5> 6> 6> 7> 8> 7> 4> 6> 5> 6> 6> 4> 5> 6> 6> 4> 5> 6> 6> 4> 5> 6> 6> 7> 4> 6> 5> 6> 6> 4> 5> 6> 6> BOYER-SETUP |
| > > > > 1> 3> 2> 3> 2> 3> 2> 4> 3> 6> 5> 6> 4> 6> 5> 6> 4> 7> 8> 7> 6> 7> 7> 8> 2> TAUTOLOGYP |
| > > 1> 2> TAUTP |
| > > 1> 2> 3> 4> 8> 6> 8> 6> 9> 6> 7> 6> 7> 4> 7> 6> 2> 2> 2> BOYER-TEST |
| > > > > > > > > > > > > > > > > > > > > 1> 2> TRUEP |
| > > T |
| > (IMPLIES (AND (IMPLIES (F (PLUS (PLUS A B) (PLUS C (ZERO)))) (F (TIMES (TIMES A B) (PLUS C D)))) (IMPLIES (F (TIMES (TIMES A B) (PLUS C D))) (F (REVERSE (APPEND (APPEND A B) (NIL)))))) (IMPLIES (F (PLUS (PLUS A B) (PLUS C (ZERO)))) (F (REVERSE (APPEND (APPEND A B) (NIL)))))) |
| NIL |
| NIL |
| > (DONE BOYER-TEST) |
| (DONE BOYER-TEST) |
| > (ALL DONE) |
| (ALL DONE) |
| > exit 0 |
