Skip to content

Instantly share code, notes, and snippets.

@texdraft

texdraft/cards.txt

Created April 5, 2020 01:50
Show Gist options
  • Save texdraft/ac651d1494a9d15a8be598b5181099de to your computer and use it in GitHub Desktop.
Save texdraft/ac651d1494a9d15a8be598b5181099de to your computer and use it in GitHub Desktop.
Download ZIP
Raw
cards.txt
________________________________________________________________________
/* M948-1207 LEVIN,LISP,TEST,2,3,250,0 |
| * * * * |
|* * * * * * * |
|000000000*0000*00*00*0**0***0*0*00***00000000000000000000000000000000000|
|1111111*1111111111111111111111111111111111111111111111111111111111111111|
|22222222*22222222222*2222*22*222*222222222222222222222222222222222222222|
|333333333333*3333**333**33**3***333*333333333333333333333333333333333333|
|*4*4*4444444444444444444444444444444444444444444444444444444444444444444|
|5555555555555**5*5555555*55555555*55555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|7777777777*7777777777*77777777777777777777777777777777777777777777777777|
|*8888*88888888888*8888*8888*8*8*888*888888888888888888888888888888888888|
|999*99999999999*999*9999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ TEST WANG ALGORITHM FOR THE PROPOSITIONAL CALCULUS |
| * * * * * * * * ** * * * ** * |
| * * ** * ** ***** ** * * * |
|00000000*0**0000*0000000000*0000000*00000000*0*0000000000*0**00000000000|
|11111111111111111*111*1111111111111111111111111111*111*11111111111111111|
|2222222222*222222222222222222222222222222222*222222222222222*22222222222|
|33333333*33*3333333333*3333*3333333*3333333333*3333*3*3**3*3333333333333|
|44444444444444444444444444444*444444444444444444444444444*4*444444444444|
|555555555*55555555*555555555555555555*55555555555*5555555555555555555555|
|6666666666666666*6666666*666666**66666666*6*6666*66666666666666666666666|
|7777777777777777777*777*777777777777777*77*77777777777777777777777777777|
|8888888888888888888888888888*8888888*88888888888888888888888888888888888|
|9999999999999999999999999**999999*999999*9999*9*999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/DEFINE(( |
|**** *** |
| * |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|*44444444444444444444444444444444444444444444444444444444444444444444444|
|5*55****5555555555555555555555555555555555555555555555555555555555555555|
|66*666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888**8888888888888888888888888888888888888888888888888888888888888888|
|999*99999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(THEOREM (LAMBDA (S) (TH1 NIL NIL (CADR S) (CADDR S)))) |
|* ** * * * *** * * * * * **** ***** |
| ** * * * * * * * * * * * **** |
|0*0000000000000000*000*00000000000000000*000000000*000000000000000000000|
|11111111111*111*11111111*11111111111*11111111*11111111111111111111111111|
|2222222222222*2222*222222222222222222222*222222222*222222222222222222222|
|3*33333333*33333333333*33333*333*33*33333333*333333333333333333333333333|
|4444444*4444*4*4444444444444444444444*44444444**444444444444444444444444|
|*55*55*55*5555555*5*5*5555*555*555*555555*5*5555555****55555555555555555|
|6666*6666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888888*8888888*8*8*8*8888888888*888888*8*8888888****88888888888888888|
|99999*999999999999999999999*999*999999*999999999*99999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH1 (LAMBDA (A1 A2 A C) (COND ((NULL A) |
|* * * * *** ** * * * ** * ** * |
| * * * ** * ** * |
|0*00000000000000000000000000000000*0000000000000000000000000000000000000|
|111*111*111*11**1*11*11111111111111111*111111111111111111111111111111111|
|222222222*22222222*22222222222222222222222222222222222222222222222222222|
|3*3333*333333333333333*333*33333333**33333333333333333333333333333333333|
|44444444*4*444444444444444444*4444*4444444444444444444444444444444444444|
|*5555*5555555*555555555*5*55*55***55555*55555555555555555555555555555555|
|666666666666666666666666666*66666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*88*8888888*888888888*8*88888**888888*88888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH2 A1 A2 NIL NIL C)) (T |
| * * * * * * * * |
| * * * * ** |
|00000*0000000000000000000000*0000000000000000000000000000000000000000000|
|111111111**1*11111111111111111111111111111111111111111111111111111111111|
|2222222*22222*2222222222222222222222222222222222222222222222222222222222|
|33333*33333333333*333*3*3333*3333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555*5555555555*555*5555**5*55555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*88888888888888888**8*88888888888888888888888888888888888888888888|
|9999999999999999*999*999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (OR (MEMBER (CAR A) C) (COND ((ATOM (CAR A)) |
| * * * ** *** * * ** * *** *** * |
| ** * * * * * * ** ** * ** |
|000000000000000000000000000000000000*00000000000000000000000000000000000|
|111111111111111111*11*1111111111111*111111*11*11111111111111111111111111|
|222222222222*22222222222222222222222222222222222222222222222222222222222|
|33333333333333333*333333*333*3333333*3333*333333333333333333333333333333|
|444444444*4*4444444444444444444*444444*444444444444444444444444444444444|
|5555*555*5*55*55*55555*55*5*55*55**55555*55555**555555555555555555555555|
|66666*66666666666666666666666*6666666*6666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*888*8888888*88888*88*8*88888**88888*88888**888888888888888888888888|
|999999*9999999*9999*99999999999999999999999*9999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH1 (COND ((MEMBER (CAR A) A1) A1) |
| * * ** * ** * ** *** * * * |
| ** * * * * * * * |
|00000*000000000000000000000000000000000000000000000000000000000000000000|
|1111111*111111111111111111*11*11**11**1111111111111111111111111111111111|
|22222222222222222222*222222222222222222222222222222222222222222222222222|
|33333*3333*33333333333333*3333333333333333333333333333333333333333333333|
|4444444444444*444*4*4444444444444444444444444444444444444444444444444444|
|5555*5555*55*55**5*55*55*55555*555*555*555555555555555555555555555555555|
|66666666666*666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*88*88888**8888888*88888*888*888*888888888888888888888888888888888|
|9999999999999999999999*9999*99999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (CONS (CAR A) A1))) A2 (CDR A) C)) |
| * ** *** * * * *** * * |
| ** * * *** * * ** |
|00000*00000*000000000000000000000000000000000000000000000000000000000000|
|111111111111111*11*11**1111*1111111*111111111111111111111111111111111111|
|22222222222*2222222222222222*2222222222222222222222222222222222222222222|
|33333*33*33333*3333333333333333*333333*333333333333333333333333333333333|
|44444444444444444444444444444444*444444444444444444444444444444444444444|
|5555*55*55*55*55555*555***5555*55555*55**5555555555555555555555555555555|
|666666666*66666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*88888*88888*888***8888*88888*88**8888888888888888888888888888888|
|9999999999999999*9999999999999999*99999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (TH1 A1 (COND ((MEMBER (CAR A) A2) A2) |
| * * * * ** * ** * ** *** * * * |
| ** * * * * * * * |
|00000*00*000000000000000000000000000000000000000000000000000000000000000|
|1111111111*1**111111111111111111*11*11*111*11111111111111111111111111111|
|22222222222222222222222222*222222222222*222*2222222222222222222222222222|
|33333*33*3333333*33333333333333*3333333333333333333333333333333333333333|
|4444444444444444444*444*4*4444444444444444444444444444444444444444444444|
|5555*55*5555555*55*55**5*55*55*55555*555*555*555555555555555555555555555|
|66666666666666666*666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*8*88888*88888**8888888*88888*888*888*888888888888888888888888888|
|9999999999999999999999999999*9999*99999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (CONS (CAR A) A2))) (CDR A) C)))))))) |
| * ** *** * * *** * * |
| ** * * *** * * ******** |
|00000*00000*000000000000000000000000000000000000000000000000000000000000|
|111111111111111*11*11*1111111111*111111111111111111111111111111111111111|
|22222222222*2222222222*2222222222222222222222222222222222222222222222222|
|33333*33*33333*3333333333333*333333*333333333333333333333333333333333333|
|44444444444444444444444444444*444444444444444444444444444444444444444444|
|5555*55*55*55*55555*555***5*55555*55********5555555555555555555555555555|
|666666666*66666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*88888*88888*888***8*88888*88********8888888888888888888888888888|
|9999999999999999*9999999999999*99999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH2 (LAMBDA (A1 A2 C1 C2 C) (COND |
|* * * * *** ** * * * * ** * |
| * * * ** |
|0*0000000000000000000000000000000000000000000000000000000000000000000000|
|1111111*111*11**1*111*11111111111111111111111111111111111111111111111111|
|222*22222*22222222*22222*22222222222222222222222222222222222222222222222|
|3*3333*3333333333333*33*33*333*33333333333333333333333333333333333333333|
|44444444*4*4444444444444444444444*44444444444444444444444444444444444444|
|*5555*5555555*5555555555555*5*55*555555555555555555555555555555555555555|
|6666666666666666666666666666666*6666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*88*8888888*8888888888888*8*888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((NULL C) (TH A1 A2 C1 C2)) |
| ** * * * * * * * |
| * ** * ** |
|0000000*0000000*00000000000000000000000000000000000000000000000000000000|
|111111111111111111**1*111*1111111111111111111111111111111111111111111111|
|2222222222222222222222*22222*2222222222222222222222222222222222222222222|
|33333333**3*333*33333333*33*33333333333333333333333333333333333333333333|
|4444444*4444444444444444444444444444444444444444444444444444444444444444|
|5555***55555*5*55555555555555**55555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**888888*8*8*888888888888**88888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM (CAR C)) (TH2 A1 A2 (COND |
| *** *** * * * * * ** * |
| ** * ** ** |
|0000000*0000000000000*00000000000000000000000000000000000000000000000000|
|111111*111111*11111111111**1*1111111111111111111111111111111111111111111|
|22222222222222222222222*22222*222222222222222222222222222222222222222222|
|3333333*3333*333*3333*3333333333*333333333333333333333333333333333333333|
|444444444*4444444444444444444444444*444444444444444444444444444444444444|
|5555**55555*55555**5*5555555555*55*5555555555555555555555555555555555555|
|66666666*666666666666666666666666*66666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**88888*88888**8*8*88888888*8888888888888888888888888888888888888888|
|99999999999999*999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((MEMBER (CAR C) C1) C1) (T |
| ** * ** *** * * * * |
| * * * * * * * |
|000000000000000000000000000000*00000000000000000000000000000000000000000|
|111111111111111*111111*111*111111111111111111111111111111111111111111111|
|222222222*22222222222222222222222222222222222222222222222222222222222222|
|33333333333333*333*33*333*3333*33333333333333333333333333333333333333333|
|444444*4*444444444444444444444444444444444444444444444444444444444444444|
|5555**5*55*55*55555*555*555*5*555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8888888*88888*888*888*8*888888888888888888888888888888888888888888|
|99999999999*9999*9999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (CONS (CAR C) C1))) C2 (CDR C))) |
| ** *** * * * *** * |
| ** * * *** * *** |
|00000000*000000000000000000000000000000000000000000000000000000000000000|
|111111111111*111111*1111111111111111111111111111111111111111111111111111|
|22222222*2222222222222222*2222222222222222222222222222222222222222222222|
|33333*33333*333*33*33333*333*333*333333333333333333333333333333333333333|
|44444444444444444444444444444*444444444444444444444444444444444444444444|
|5555*55*55*55555*555***5555*55555***555555555555555555555555555555555555|
|666666*66666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88888*88888*888***8888*88888***888888888888888888888888888888888888|
|9999999999999*9999999999999999*99999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (TH2 A1 A2 C1 (COND ((MEMBER |
| * * * * * * ** * ** * ** |
| ** * * * |
|00000*00*000000000000000000000000000000000000000000000000000000000000000|
|111111111111**1*111*1111111111111111111111111111111111111111111111111111|
|2222222222*22222*222222222222222*222222222222222222222222222222222222222|
|33333*33*333333333*333*3333333333333333333333333333333333333333333333333|
|4444444444444444444444444*444*4*4444444444444444444444444444444444444444|
|5555*55*5555555555555*55*55**5*55*55555555555555555555555555555555555555|
|66666666666666666666666*666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*8*88888888888*88888**8888888888888888888888888888888888888888888|
|9999999999999999999999999999999999*9999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (CAR C) C2) C2) (T (CONS (CAR C) C2))) |
| *** * * * * ** *** * * |
| * * * * ** * * *** |
|000000000000000000000*00000*00000000000000000000000000000000000000000000|
|111111*111111111111111111111111*1111111111111111111111111111111111111111|
|2222222222222*222*222222222*2222222222*222222222222222222222222222222222|
|33333*333*33*333*3333*33*33333*333*33*3333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555*55555*555*555*5*55*55*55*55555*555***555555555555555555555555555555|
|6666666666666666666666666*6666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88888*888*888*8*88*88888*88888*888***888888888888888888888888888888|
|9999999*999999999999999999999999*999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (CDR C)))))) |
| *** * |
| * ****** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|33333*333*33333333333333333333333333333333333333333333333333333333333333|
|444444*44444444444444444444444444444444444444444444444444444444444444444|
|5555*55555******55555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88888******88888888888888888888888888888888888888888888888888888888|
|9999999*9999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH (LAMBDA (A1 A2 C1 C2) (COND ((NULL A2) (AND (NOT (NULL C2)) |
|* * * * *** ** * * * ** * ** * ** * * * * |
| * * * ** * ** * * ** * ** ** |
|0*000000000000000000000000000000000*000000000000000*000*0000000000000000|
|111111*111*11**1*111*111111111111111111*1111*111111111111111111111111111|
|22222222*22222222*22222*2222222222222222*2222222222222222222*22222222222|
|3*333*3333333333333*33*3333*33333333**3333333333333*3333**3*333333333333|
|4444444*4*44444444444444444444*4444*4444444444*44444444*4444444444444444|
|*555*5555555*55555555555*5*55*55***555555*5*5*55**555**555555**555555555|
|6666666666666666666666666666*666666666666666666666*666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*8*8888888*88888888888*8*88888**8888888*8*8888*8888*8888888**888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (THR (CAR C2) A1 A2 C1 (CDR C2)))) (T (THL (CAR A2) A1 (CDR A2) |
| * * *** * * * * *** * * * * *** * * *** * |
| * * * * **** * * * * * |
|00000*0000000000000000000000000000000000*00*0000000000000000000000000000|
|11111111111*111111**1*111*11111111111111111111111*11*111**111111*1111111|
|222222222222222*222222*2222222222*2222222222222222222*22222222222*222222|
|33333*3333*333*333333333*333*333*3333333*33*3*33*33333333333*33333333333|
|44444444444444444444444444444*4444444444444444444444444444444*4444444444|
|5555*5555*555555*5555555555*555555****5*55*5555*555555*5555*555555*55555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*88*888888*8888888888*888888****8*88*8*88*888888*8888*888888*88888|
|9999999*9999*99999999999999999*9999999999999999999*99999999999*999999999|
|________________________________________________________________________|
________________________________________________________________________
/ C1 C2))))) |
| * * |
| ***** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|11111*111111111111111111111111111111111111111111111111111111111111111111|
|22222222*222222222222222222222222222222222222222222222222222222222222222|
|3333*33*3333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|555555555*****5555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888888*****8888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(THL (LAMBDA (U A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*000000000000*000000000000000000000000000000000000000000000000000000000|
|1111111*111*1111**1*111*111111111111111111111111111111111111111111111111|
|222222222*2222222222*22222*222222222222222222222222222222222222222222222|
|3*3*33*333333333333333*33*3333*33333333333333333333333333333333333333333|
|44444444*4*444*444444444444444444*44444444444444444444444444444444444444|
|*5555*5555555*5555555555555*5*55*555555555555555555555555555555555555555|
|6666666666666666666666666666666*6666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*88*8888888*8888888888888*8*888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE NOT)) (TH1R (CADR U) A1 A2 C1 C2)) |
| *** *** * * * * **** * * * * |
| * * * * * ** ** * * * ** |
|00000000000000*0000*0*0000*0000*0000000000*00000000000000000000000000000|
|11111111111*111111111111111111111*1111*111111**1*111*1111111111111111111|
|2222222222222222222222222222222222222222222222222*22222*2222222222222222|
|3333333333*3333333333*3333*3333*33333*3333333333333*33*33333333333333333|
|44444444444444*4444*4444444444444444444*44*44444444444444444444444444444|
|5555***55*55555*5*5555*5*55**5*55555*555555*555555555555**55555555555555|
|66666666666666666666*6666*6666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**88888888**8*8*888*888888*888888888888**88888888888888|
|999999999999*999999999999999999999*99999*9999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE AND)) (TH2L (CDR U) A1 A2 C1 C2)) |
| *** *** * * * * * * *** * * * * |
| * * * * * * ** * * * ** |
|00000000000000*0000*0*000000000*000000000*000000000000000000000000000000|
|11111111111*111111111111*1111111111111111111**1*111*11111111111111111111|
|222222222222222222222222222222222*22222222222222*22222*22222222222222222|
|3333333333*3333333333*333333333*33*33*333333333333*33*333333333333333333|
|44444444444444*4444*444444*44444444444*44*444444444444444444444444444444|
|5555***55*55555*5*5555*55*5**5*55555*55555*555555555555**555555555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**88888888**8*8*888*88888*888888888888**888888888888888|
|999999999999*99999999999999999999999999*99999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE OR)) (AND (TH1L (CADR U) A1 A2 C1 C2) |
| *** *** * * ** * * * **** * * * * |
| * * * * * **** * * * * * |
|00000000000000*0000*0*0000000000000*0000000000*0000000000000000000000000|
|11111111111*111111111111111111*111111*1111*111111**1*111*111111111111111|
|22222222222222222222222222222222222222222222222222222*22222*222222222222|
|3333333333*3333333333*3333333333333*33*33*3333333333333*33*3333333333333|
|44444444444444*4444*444444444444*4444444444*44*4444444444444444444444444|
|5555***55*55555*5*5555*555**5*5*55*55555*555555*555555555555*55555555555|
|66666666666666666666*666*66666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**8888888**8*8888*8*888*888888*888888888888*88888888888|
|999999999999*999999999999*999999999999999999*999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH1L (CADDR U) A1 A2 C1 C2) )) |
| * * ***** * * * * |
| * * * * ** |
|00000*00000000000*000000000000000000000000000000000000000000000000000000|
|1111111*1111*1111111**1*111*11111111111111111111111111111111111111111111|
|222222222222222222222222*22222*22222222222222222222222222222222222222222|
|33333*33*33*33333333333333*33*333333333333333333333333333333333333333333|
|4444444444444**44*444444444444444444444444444444444444444444444444444444|
|5555*55555*5555555*555555555555*5**5555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*888*8888888*888888888888*8**8888888888888888888888888888888888888|
|999999999999999*99999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE IMPLIES)) (AND (TH1L (CADDR U) A1 A2 C1 |
| *** *** * * * ** ** * * * ***** * * * |
| * * * * * *** ** * * * * |
|00000000000000*0000*0*00000000*000000000*00000000000*0000000000000000000|
|11111111111*11111111111111111111111*111111*1111*1111111**1*111*111111111|
|222222222222222222222222222222*2222222222222222222222222222*222222222222|
|3333333333*3333333333*33333*333333333333*33*33*33333333333333*3333333333|
|44444444444444*4444*44444*44444444444*4444444444**44*4444444444444444444|
|5555***55*55555*5*5555*555555*5**5*5*55*55555*5555555*555555555555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|77777777777777777777777777*777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**888888888888**8*8888*8*888*8888888*888888888888888888|
|999999999999*99999999999*999*999999999999999999999*999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ C2) (TH1R (CADR U) A1 A2 C1 C2) )) |
| * * * **** * * * * |
| * * * * * ** |
|000000000*0000000000*000000000000000000000000000000000000000000000000000|
|11111111111*1111*111111**1*111*11111111111111111111111111111111111111111|
|22222*222222222222222222222*22222*22222222222222222222222222222222222222|
|3333*3333*33333*3333333333333*33*333333333333333333333333333333333333333|
|44444444444444444*44*444444444444444444444444444444444444444444444444444|
|555555*5*55555*555555*555555555555*5**5555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888*8*8*888*888888*888888888888*8**8888888888888888888888888888888888|
|999999999999*99999*99999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH2L (CDR U) A1 A2 C1 C2) |
| *** *** * * * * ** * * * *** * * * * |
| * * * * * * ** * * * * * |
|00000000000000*0000*0*0000*0*000000000*000000000*00000000000000000000000|
|11111111111*111111111111111111111*11111111111111111**1*111*1111111111111|
|2222222222222222222222222222222222222222*22222222222222*22222*2222222222|
|3333333333*3333333333*3333333333333333*33*33*333333333333*33*33333333333|
|44444444444444*4444*444444*44444444*444444444*44*44444444444444444444444|
|5555***55*55555*5*5555*5*555***5*5*55*55555*55555*555555555555*555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**888888*888**8*8888*8*888*88888*888888888888*888888888|
|999999999999*99999999999999*999999999999999999*9999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH2R (CDR U) A1 A2 C1 C2) )) |
| * * *** * * * * |
| * * * * ** |
|00000*000000000*00000000000000000000000000000000000000000000000000000000|
|111111111111111111**1*111*1111111111111111111111111111111111111111111111|
|2222222*22222222222222*22222*2222222222222222222222222222222222222222222|
|33333*33333*333333333333*33*33333333333333333333333333333333333333333333|
|444444444444*44*44444444444444444444444444444444444444444444444444444444|
|5555*55555*55555*555555555555*5**555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*888*88888*888888888888*8**888888888888888888888888888888888888888|
|99999999*9999*9999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (ERROR (LIST (QUOTE THL) U A1 A2 C1 C2))) |
| * ** * * * * * * * * * |
| **** * * * ** *** |
|00000*00000000000**000*0*00*0000*000000000000000000000000000000000000000|
|1111111111111111111111111111111111**1*111*111111111111111111111111111111|
|22222222222222222*22222222222222222222*22222*222222222222222222222222222|
|33333*333333333*33*33333*33*3*3333333333*33*3333333333333333333333333333|
|4444444444444444444444*444444444*444444444444444444444444444444444444444|
|5555*55**55555*55555*5555*5555*55555555555555***555555555555555555555555|
|66666666666*66666666666*666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888888*88888**888888*8*88888888888888***888888888888888888888888|
|999999999**9*999*9999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(THR (LAMBDA (U A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*000000000000*000000000000000000000000000000000000000000000000000000000|
|1111111*111*1111**1*111*111111111111111111111111111111111111111111111111|
|222222222*2222222222*22222*222222222222222222222222222222222222222222222|
|3*3333*333333333333333*33*3333*33333333333333333333333333333333333333333|
|44444444*4*444*444444444444444444*44444444444444444444444444444444444444|
|*5555*5555555*5555555555555*5*55*555555555555555555555555555555555555555|
|6666666666666666666666666666666*6666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*88*8888888*8888888888888*8*888888888888888888888888888888888888888888|
|999*99999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE NOT)) (TH1L (CADR U) A1 A2 C1 C2)) |
| *** *** * * * * **** * * * * |
| * * * * * ** ** * * * ** |
|00000000000000*0000*0*0000*0000*0000000000*00000000000000000000000000000|
|11111111111*111111111111111111111*1111*111111**1*111*1111111111111111111|
|2222222222222222222222222222222222222222222222222*22222*2222222222222222|
|3333333333*3333333333*3333*3333*33*33*3333333333333*33*33333333333333333|
|44444444444444*4444*4444444444444444444*44*44444444444444444444444444444|
|5555***55*55555*5*5555*5*55**5*55555*555555*555555555555**55555555555555|
|66666666666666666666*6666*6666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**88888888**8*8*888*888888*888888888888**88888888888888|
|999999999999*999999999999999999999999999*9999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE AND)) (AND (TH1R (CADR U) A1 A2 C1 C2) |
| *** *** * * * * ** * * * **** * * * * |
| * * * * * * ** * * * * * |
|00000000000000*0000*0*00000000000000*0000000000*000000000000000000000000|
|11111111111*111111111111*111111*111111*1111*111111**1*111*11111111111111|
|222222222222222222222222222222222222222222222222222222*22222*22222222222|
|3333333333*3333333333*33333333333333*33333*3333333333333*33*333333333333|
|44444444444444*4444*444444*444444*4444444444*44*444444444444444444444444|
|5555***55*55555*5*5555*55*5**5*5*55*55555*555555*555555555555*5555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**88888888**8*8888*8*888*888888*888888888888*8888888888|
|999999999999*99999999999999999999999999*99999*99999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH1R (CADDR U) A1 A2 C1 C2) )) |
| * * ***** * * * * |
| * * * * ** |
|00000*00000000000*000000000000000000000000000000000000000000000000000000|
|1111111*1111*1111111**1*111*11111111111111111111111111111111111111111111|
|222222222222222222222222*22222*22222222222222222222222222222222222222222|
|33333*33333*33333333333333*33*333333333333333333333333333333333333333333|
|4444444444444**44*444444444444444444444444444444444444444444444444444444|
|5555*55555*5555555*555555555555*5**5555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*888*8888888*888888888888*8**8888888888888888888888888888888888888|
|99999999*999999*99999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE OR)) (TH2R (CDR U) A1 A2 C1 C2)) |
| *** *** * * * * *** * * * * |
| * * * * * **** * * * ** |
|00000000000000*0000*0*00000000*000000000*0000000000000000000000000000000|
|11111111111*1111111111111111111111111111111**1*111*111111111111111111111|
|22222222222222222222222222222222*22222222222222*22222*222222222222222222|
|3333333333*3333333333*33333333*33333*333333333333*33*3333333333333333333|
|44444444444444*4444*44444444444444444*44*4444444444444444444444444444444|
|5555***55*55555*5*5555*555**5*55555*55555*555555555555**5555555555555555|
|66666666666666666666*666*66666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**8888888**8*8*888*88888*888888888888**8888888888888888|
|999999999999*999999999999*9999999*9999*999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE IMPLIES)) (TH11 (CADR U) (CADDR U) |
| *** *** * * * ** * * **** ***** |
| * * * * * *** ** * * * * |
|00000000000000*0000*0*00000000*0000*0000000000*000000000*000000000000000|
|11111111111*1111111111111111111111111**111*11111111*11111111111111111111|
|222222222222222222222222222222*22222222222222222222222222222222222222222|
|3333333333*3333333333*33333*3333333*33333*33333333*333333333333333333333|
|44444444444444*4444*44444*44444444444444444*44*44444**44*444444444444444|
|5555***55*55555*5*5555*555555*5**5*55555*555555*5*5555555*55555555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|77777777777777777777777777*777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**888888888888**8*8*888*888888*8*8888888*88888888888888|
|999999999999*99999999999*999*999999999999999*999999999*99999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ A1 A2 C1 C2)) |
| * * * * |
| ** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|11111**1*111*11111111111111111111111111111111111111111111111111111111111|
|222222222*22222*22222222222222222222222222222222222222222222222222222222|
|33333333333*33*333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555555555555555**555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888888888888888**888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH11 (CADR U) (CADDR U) |
| *** *** * * * * ** * * * **** ***** |
| * * * * * * ** * * * * * |
|00000000000000*0000*0*0000*0*000000000*0000000000*000000000*000000000000|
|11111111111*111111111111111111111*111111**111*11111111*11111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|3333333333*3333333333*3333333333333333*33333*33333333*333333333333333333|
|44444444444444*4444*444444*44444444*4444444444*44*44444**44*444444444444|
|5555***55*55555*5*5555*5*555***5*5*55*55555*555555*5*5555555*55555555555|
|66666666666666666666*666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8*8*88888*8**888888*888**8*8888*8*888*888888*8*8888888*88888888888|
|999999999999*99999999999999*9999999999999999999*999999999*99999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ A1 A2 C1 C2) (TH11 (CADDR U) (CADR U) A1 A2 C1 C2) )) |
| * * * * * * ***** **** * * * * |
| * * * * * * ** |
|000000000000000000*00000000000*00000000*00000000000000000000000000000000|
|1111**1*111*11111111**111*111111111*111111**1*111*1111111111111111111111|
|22222222*22222*2222222222222222222222222222222*22222*2222222222222222222|
|3333333333*33*3333*33333*333333333*3333333333333*33*33333333333333333333|
|44444444444444444444444444**44*44444*44*44444444444444444444444444444444|
|555555555555555*5*55555*5555555*5*555555*555555555555*5**555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888888888888*8*8*888*8888888*8*888888*888888888888*8**888888888888888|
|9999999999999999999999999999*99999999*9999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (ERROR (LIST (QUOTE THR) U A1 A2 C1 C2))) |
| * ** * * * * * * * * * |
| **** * * * ** *** |
|00000*00000000000**000*0*00*0000*000000000000000000000000000000000000000|
|1111111111111111111111111111111111**1*111*111111111111111111111111111111|
|22222222222222222*22222222222222222222*22222*222222222222222222222222222|
|33333*333333333*33*33333*33*333333333333*33*3333333333333333333333333333|
|4444444444444444444444*444444444*444444444444444444444444444444444444444|
|5555*55**55555*55555*5555*5555*55555555555555***555555555555555555555555|
|66666666666*66666666666*666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888888*88888**888888*8*88888888888888***888888888888888888888888|
|999999999**9*999*999999999999*999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH1L (LAMBDA (V A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*0000000000000*00000000000000000000000000000000000000000000000000000000|
|111*1111*111*1111**1*111*11111111111111111111111111111111111111111111111|
|2222222222*2222222222*22222*22222222222222222222222222222222222222222222|
|3*33*33*333333333333333*33*3333*3333333333333333333333333333333333333333|
|444444444*4*4444444444444444444444*4444444444444444444444444444444444444|
|*55555*5555555**555555555555*5*55*55555555555555555555555555555555555555|
|66666666666666666666666666666666*666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888*8888888*8888888888888*8*88888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM V) (OR (MEMBER V C1) |
| *** * * * ** * |
| ** * ** * * * * |
|0000000*000*00000000000000*000000000000000000000000000000000000000000000|
|111111*1111111111111111111111*111111111111111111111111111111111111111111|
|2222222222222222222222*2222222222222222222222222222222222222222222222222|
|3333333*33333333333333333333*3333333333333333333333333333333333333333333|
|444444444*444444444*4*44444444444444444444444444444444444444444444444444|
|5555**55555**5*555*5*55*55*555*55555555555555555555555555555555555555555|
|66666666*666666*66666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**888888*8*888*88888888888*88888888888888888888888888888888888888888|
|9999999999999999*9999999*99999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH (CONS V A1) A2 C1 C2) )) |
| * * ** * * * * |
| ** * * ** |
|00000*000000*0*000000000000000000000000000000000000000000000000000000000|
|1111111111111111**11*111*11111111111111111111111111111111111111111111111|
|222222222222*22222222*22222*22222222222222222222222222222222222222222222|
|33333*333*3333333333333*33*333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555*555*55*55*555*555555555*5**5555555555555555555555555555555555555555|
|6666666666*6666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*8*888888888*888888888*8**8888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (OR (MEMBER V C2) (TH A1 (CONS V A2) C1 C2) )) |
| * * * * ** * * * * ** * * * |
| ** * * * * ** * * ** |
|00000*0000000000000*000000*000000000*0*000000000000000000000000000000000|
|11111111111111111111111111111**111111111*1111*11111111111111111111111111|
|222222222222222*222222*2222222222222*2222*222222*22222222222222222222222|
|33333*333333333333333*3333*333333*3333333333*33*333333333333333333333333|
|444444444444*4*444444444444444444444444444444444444444444444444444444444|
|5555*55*555*5*55*55*555*5*555555*55*55*555*555555*5**5555555555555555555|
|66666666*6666666666666666666666666*6666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888*88888888888*8*8*8888*888888888*888888*8**8888888888888888888|
|999999999*9999999*999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH1R (LAMBDA (V A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*0000000000000*00000000000000000000000000000000000000000000000000000000|
|111*1111*111*1111**1*111*11111111111111111111111111111111111111111111111|
|2222222222*2222222222*22222*22222222222222222222222222222222222222222222|
|3*33333*333333333333333*33*3333*3333333333333333333333333333333333333333|
|444444444*4*4444444444444444444444*4444444444444444444444444444444444444|
|*55555*5555555**555555555555*5*55*55555555555555555555555555555555555555|
|66666666666666666666666666666666*666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888*8888888*8888888888888*8*88888888888888888888888888888888888888888|
|9999*9999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM V) (OR (MEMBER V A1) |
| *** * * * ** * |
| ** * ** * * * * |
|0000000*000*00000000000000*000000000000000000000000000000000000000000000|
|111111*111111111111111111111**111111111111111111111111111111111111111111|
|2222222222222222222222*2222222222222222222222222222222222222222222222222|
|3333333*3333333333333333333333333333333333333333333333333333333333333333|
|444444444*444444444*4*44444444444444444444444444444444444444444444444444|
|5555**55555**5*555*5*55*55*555*55555555555555555555555555555555555555555|
|66666666*666666*66666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**888888*8*888*88888888888*88888888888888888888888888888888888888888|
|9999999999999999*9999999*99999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH A1 A2 (CONS V C1) C2) )) |
| * * * * ** * * |
| ** * * ** |
|00000*000000000000*0*000000000000000000000000000000000000000000000000000|
|11111111**1*11111111111*111111111111111111111111111111111111111111111111|
|222222222222*22222*22222222*22222222222222222222222222222222222222222222|
|33333*333333333*333333*333*333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555*555555555*55*55*555*555*5**5555555555555555555555555555555555555555|
|6666666666666666*6666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*8888888*888888888*888*8**8888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (OR (MEMBER V A2) (TH A1 A2 C1 (CONS V C2)))) |
| * * * * ** * * * * * * ** * |
| ** * * * * ** **** |
|00000*0000000000000*000000*000000000000000*0*000000000000000000000000000|
|111111111111111111111*1111111**1*111*11111111111111111111111111111111111|
|222222222222222*222222*2222222222*22222222*2222*222222222222222222222222|
|33333*33333333333333333333*33333333*333*333333*3333333333333333333333333|
|444444444444*4*444444444444444444444444444444444444444444444444444444444|
|5555*55*555*5*55*55*555*5*555555555555*55*55*555****55555555555555555555|
|66666666*6666666666666666666666666666666*6666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888*88888888888*8*8*8888888888*888888888****88888888888888888888|
|999999999*9999999*999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH2L (LAMBDA (V A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*0000000000000*00000000000000000000000000000000000000000000000000000000|
|11111111*111*1111**1*111*11111111111111111111111111111111111111111111111|
|222*222222*2222222222*22222*22222222222222222222222222222222222222222222|
|3*33*33*333333333333333*33*3333*3333333333333333333333333333333333333333|
|444444444*4*4444444444444444444444*4444444444444444444444444444444444444|
|*55555*5555555**555555555555*5*55*55555555555555555555555555555555555555|
|66666666666666666666666666666666*666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888*8888888*8888888888888*8*88888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM (CAR V)) (OR (MEMBER (CAR V) C1) |
| *** *** * * * ** *** * |
| ** * ** ** * * * * * * |
|0000000*00000000*00000000000000000000*0000000000000000000000000000000000|
|111111*111111*11111111111111111111*111111*111111111111111111111111111111|
|2222222222222222222222222222*2222222222222222222222222222222222222222222|
|3333333*3333*33333333333333333333*333333*3333333333333333333333333333333|
|444444444*444444444444444*4*44444444444444444444444444444444444444444444|
|5555**55555*5555***5*555*5*55*55*5555**555*55555555555555555555555555555|
|66666666*666666666666*66666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**88888*88888**8*888*8888888*88888*888*88888888888888888888888888888|
|99999999999999*9999999*9999999*9999*999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2))) |
| * * **** ** *** * * * * |
| * * * ** * * * *** |
|00000*0000000000*000000*000000*00000000000000000000000000000000000000000|
|1111111*1111*11111111111111*11111**11*111*111111111111111111111111111111|
|22222222222222222222222*22222222222222*22222*222222222222222222222222222|
|33333*33*33*33333333*33333*3333333333333*33*3333333333333333333333333333|
|4444444444444*4444444444444444444444444444444444444444444444444444444444|
|5555*55555*55555**5*55*55*5555**555*555555555***555555555555555555555555|
|666666666666666666666*66666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*888*888888*8*88888*88888*888*888888888***888888888888888888888888|
|99999999999999*9999999999999*9999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (OR (MEMBER (CAR V) C2) (TH1L (CADR V) A1 (CONS (CAR V) |
| * * * * ** *** * * * **** * ** *** |
| ** * * * * * * * * * ** * * |
|00000*000000000000000000*0000000*0000000000*000000000*000000*00000000000|
|111111111111111111111*111111111111*1111*111111**111111111*11111111111111|
|222222222222222*222222222222*222222222222222222222222*222222222222222222|
|33333*33333333333333*333333*3333*33*33*33333333333*33333*333333333333333|
|444444444444*4*4444444444444444444444444*4444444444444444444444444444444|
|5555*55*555*5*55*55*5555**555*5*55555*55555**5555*55*55*5555**5555555555|
|66666666*666666666666666666666666666666666666666666*66666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888*8888888*88888*888*8*8*888*888888*8888*88888*88888*8888888888|
|999999999*9999999*9999*999999999999999999*9999999999999999*9999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ A2) C1 C2))) |
| * * * |
| * *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|1111*1111*11111111111111111111111111111111111111111111111111111111111111|
|22222*222222*22222222222222222222222222222222222222222222222222222222222|
|33333333*33*333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|555555*555555***55555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888*888888***88888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH2R (LAMBDA (V A1 A2 C1 C2) (COND |
|* * * * *** * * * * * ** * |
| * * * * ** |
|0*0000000000000*00000000000000000000000000000000000000000000000000000000|
|11111111*111*1111**1*111*11111111111111111111111111111111111111111111111|
|222*222222*2222222222*22222*22222222222222222222222222222222222222222222|
|3*33333*333333333333333*33*3333*3333333333333333333333333333333333333333|
|444444444*4*4444444444444444444444*4444444444444444444444444444444444444|
|*55555*5555555**555555555555*5*55*55555555555555555555555555555555555555|
|66666666666666666666666666666666*666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888*8888888*8888888888888*8*88888888888888888888888888888888888888888|
|9999*9999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM (CAR V)) (OR (MEMBER (CAR V) A1) |
| *** *** * * * ** *** * |
| ** * ** ** * * * * * * |
|0000000*00000000*00000000000000000000*0000000000000000000000000000000000|
|111111*111111*11111111111111111111*11111**111111111111111111111111111111|
|2222222222222222222222222222*2222222222222222222222222222222222222222222|
|3333333*3333*33333333333333333333*33333333333333333333333333333333333333|
|444444444*444444444444444*4*44444444444444444444444444444444444444444444|
|5555**55555*5555***5*555*5*55*55*5555**555*55555555555555555555555555555|
|66666666*666666666666*66666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**88888*88888**8*888*8888888*88888*888*88888888888888888888888888888|
|99999999999999*9999999*9999999*9999*999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2))) |
| * * **** * * ** *** * * |
| * * * ** * * * *** |
|00000*0000000000*000000000000*000000*00000000000000000000000000000000000|
|1111111*1111*111111**1*1111111111*111111*1111111111111111111111111111111|
|22222222222222222222222*22222*22222222222222*222222222222222222222222222|
|33333*33333*33333333333333*33333*333333*333*3333333333333333333333333333|
|4444444444444*4444444444444444444444444444444444444444444444444444444444|
|5555*55555*55555**5555555*55*55*5555**555*555***555555555555555555555555|
|666666666666666666666666666*66666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*8*888*888888*8888888*88888*88888*888*888***888888888888888888888888|
|99999999*99999*9999999999999999999*9999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (OR (MEMBER (CAR V) A2) (TH1R (CADR V) A1 A2 C1 |
| * * * * ** *** * * * **** * * * |
| ** * * * * * * * * * |
|00000*000000000000000000*0000000*0000000000*0000000000000000000000000000|
|111111111111111111111*11111*111111*1111*111111**1*111*111111111111111111|
|222222222222222*222222222222*222222222222222222222*222222222222222222222|
|33333*33333333333333*33333333333*33333*3333333333333*3333333333333333333|
|444444444444*4*4444444444444444444444444*4444444444444444444444444444444|
|5555*55*555*5*55*55*5555**555*5*55555*55555**555555555555555555555555555|
|66666666*666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888*8888888*88888*888*8*8*888*888888*888888888888888888888888888|
|999999999*9999999*9999*999999999999*99999*999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (CONS (CAR V) C2)))) |
| ** *** * |
| ** * * **** |
|00000000*000000*00000000000000000000000000000000000000000000000000000000|
|111111111111*11111111111111111111111111111111111111111111111111111111111|
|22222222*2222222222*2222222222222222222222222222222222222222222222222222|
|33333*33333*333333*33333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555*55*55*5555**555****555555555555555555555555555555555555555555555555|
|666666*66666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88888*88888*888****888888888888888888888888888888888888888888888888|
|9999999999999*9999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/(TH11 (LAMBDA (VI V2 A1 A2 C1 C2) (COND |
|* * * * *** * * * * * * ** * |
| * * * ** |
|0*0000000000000*00*00000000000000000000000000000000000000000000000000000|
|111**111*111*11111111**1*111*1111111111111111111111111111111111111111111|
|2222222222*22222222*22222*22222*2222222222222222222222222222222222222222|
|3*33333*3333333333333333333*33*3333*333333333333333333333333333333333333|
|444444444*4*44444444444444444444444444*444444444444444444444444444444444|
|*55555*5555555**55*5555555555555*5*55*5555555555555555555555555555555555|
|666666666666666666666666666666666666*66666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|*8*888*8888888*88888888888888888*8*8888888888888888888888888888888888888|
|9999999999999999*9999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ((ATOM VI) (OR (MEMBER VI C1) (TH1R V2 (CONS VI A1) A2 C1 |
| *** * * * * ** * * * * ** * * * * |
| ** * ** * * * * * ** * |
|0000000*000*000000000000000*0000000*0000*000000*0*0000000000000000000000|
|111111*111111111111111111111111*11111*11111111111111**11*111*11111111111|
|22222222222222222222222*22222222222222222*22222*222222222*22222222222222|
|3333333*3333333333333333333333*3333*33333333*33333333333333*333333333333|
|444444444*4444444444*4*4444444444444444444444444444444444444444444444444|
|5555**55555*5*5*555*5*55*55*5555*5*55555*55*55*55*5555*55555555555555555|
|66666666*6666666*6666666666666666666666666666*66666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888**8888888*8*888*888888888888*8*8*888888*8888888888*88888888888888888|
|999999999999*9999*9999999*99*999999999*99999999999*999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ C2))) |
| * |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|22222*222222222222222222222222222222222222222222222222222222222222222222|
|3333*3333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|555555***555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888***888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ (T (OR (MEMBER VI C2) (TH1R V2 A1 (CONS VI A2) C1 C2))) |
| * * * * ** * * * * * ** * * * * |
| ** * * * * * ** * *** |
|00000*0000000000000*0000000*0000*000000000*0*000000000000000000000000000|
|11111111111111111111111111111*11111**1111111111*1111*1111111111111111111|
|222222222222222*2222222*222222222*22222222*22222*222222*2222222222222222|
|33333*3333333333333333*3333*33333333333*33333333333*33*33333333333333333|
|444444444444*4*444444444444444444444444444444444444444444444444444444444|
|5555*55*555*5*55*55*5555*5*55555*55555*55*55*5555*555555***5555555555555|
|66666666*6666666666666666666666666666666*6666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888*88*888*888888888888*8*8*888888888*8888888888*888888***8888888888888|
|999999999*9999999*99*999999999*99999999999999*99999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ ))) |
| |
| *** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***55555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8888***88888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/)) |
| |
|** |
|000000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|**5555555555555555555555555555555555555555555555555555555555555555555555|
|666666666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|**8888888888888888888888888888888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/TRACE ((THEOREM TH1 TH2 TH THL THR TH1L TH1R TH2L TH2R TH11)) |
| *** ** ** * * * * * * * * * * * |
| * ** * * * * * * * ** |
|*0000000*0000000*000*000*00*000*000*0000*0000*0000*0000*0000000000000000|
|11*111111111111111*111111111111111111*1111*11111111111111**1111111111111|
|2222222222222222222222*222222222222222222222222*2222*2222222222222222222|
|*33*3333*3333333*333*333*33*3*3*333*33*3*3333*33*3*3333*3333333333333333|
|44444444444444*444444444444444444444444444444444444444444444444444444444|
|5555*5**55*55*555555555555555555555555555555555555555555555**55555555555|
|66666666666*666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|888888**8*8888888*888*888*88*888*888*8888*8888*8888*8888*88**88888888888|
|9*9999999999*99999999999999999999*999999999*999999999*999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/THEOREM |
| ** * |
| ** * |
|*00000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|*33333333333333333333333333333333333333333333333333333333333333333333333|
|444444*44444444444444444444444444444444444444444444444444444444444444444|
|55*55*555555555555555555555555555555555555555555555555555555555555555555|
|666*66666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8*8888888888888888888888888888888888888888888888888888888888888888888888|
|9999*9999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/((ARROW (P) ((OR P Q)))) |
|*** * ** |
| *** ** ** * ***** |
|000000*00000000000000000000000000000000000000000000000000000000000000000|
|11*111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|333333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|**555555*5*5**555555****555555555555555555555555555555555555555555555555|
|66666**6666666*666666666666666666666666666666666666666666666666666666666|
|777777777*7777777*777777777777777777777777777777777777777777777777777777|
|**888888*8*8**88888*****888888888888888888888888888888888888888888888888|
|999**9999999999*99999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/UNTRACE ((THEOREM TH1 TH2 THR THL TH1L TH1R TH2L TH2R TH11)) |
| *** ** ** * * * * * * * * * * |
| * * ** * * * * * * * ** |
|*0*0000000*0000000*000*000*000*000*0000*0000*0000*0000*00000000000000000|
|1111*111111111111111*111111111111111*1111*11111111111111**11111111111111|
|222222222222222222222222*222222222222222222222*2222*22222222222222222222|
|33*33*3333*3333333*333*333*333*3*3*33*3*3333*33*3*3333*33333333333333333|
|*444444444444444*4444444444444444444444444444444444444444444444444444444|
|5*5555*5**55*55*555555555555555555555555555555555555555555**555555555555|
|6666666666666*6666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|88888888**8*8888888*888*888*888*888*8888*8888*8888*8888*88**888888888888|
|999*9999999999*9999999999999*9999999999999*999999999*9999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/THEOREM |
| ** * |
| ** * |
|*00000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|222222222222222222222222222222222222222222222222222222222222222222222222|
|*33333333333333333333333333333333333333333333333333333333333333333333333|
|444444*44444444444444444444444444444444444444444444444444444444444444444|
|55*55*555555555555555555555555555555555555555555555555555555555555555555|
|666*66666666666666666666666666666666666666666666666666666666666666666666|
|777777777777777777777777777777777777777777777777777777777777777777777777|
|8*8888888888888888888888888888888888888888888888888888888888888888888888|
|9999*9999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/((ARROW ((OR A (NOT B))) ((IMPLIES (AND P Q) (EQUIV P Q))) )) |
|*** ** * * * *** ** ** * ** * |
| *** ** ** *** *** * * ** * * **** ** |
|000000*00000000000*00000000000000*00000000000000*0*000000000000000000000|
|11*1111111111*1111111111111111111111*11111111111111111111111111111111111|
|22222222222222222222*222222222222*22222222222222222222222222222222222222|
|333333333333333333*33333333333*33333333333333333333333333333333333333333|
|4444444444444444444444444444*444444444*444444444*44444444444444444444444|
|**555555**55555**5555***5**55555*55*5*55555*5**555*5555***5**55555555555|
|66666**666*666666*666666666666666666666666666666666666666666666666666666|
|77777777777777777777777777777*7777777777*77777777777*7777777777777777777|
|**888888**88888*88888***8**88888888*888888**8*8*888888****8**88888888888|
|999**999999*999999999999999*999*99999999999999999*9999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/STOP))) ))) ))) ))) |
| |
| ***** *** *** *** |
|**0000000000000000000000000000000000000000000000000000000000000000000000|
|111111111111111111111111111111111111111111111111111111111111111111111111|
|*22222222222222222222222222222222222222222222222222222222222222222222222|
|3*3333333333333333333333333333333333333333333333333333333333333333333333|
|444444444444444444444444444444444444444444444444444444444444444444444444|
|5555***5555***55555***55555***555555555555555555555555555555555555555555|
|66*666666666666666666666666666666666666666666666666666666666666666666666|
|777*77777777777777777777777777777777777777777777777777777777777777777777|
|8888***8888***88888***88888***888888888888888888888888888888888888888888|
|999999999999999999999999999999999999999999999999999999999999999999999999|
|________________________________________________________________________|
________________________________________________________________________
/ FIN END OF LISP RUN M948-1207 LEVIN |
| ** * * * * * * |
| * * * * * * * * * * * |
|0000000000000000000000000*000*0000000000000000*0000*00000000000000000000|
|11111111111111111111111111111111111111111111*111111111111111111111111111|
|2222222222222222222222222*2222222222222222222*22222222222222222222222222|
|33333333333333333333333*3333333333333333333333333*3333333333333333333333|
|444444444444444444*4444444444*444444444*4*444444444444444444444444444444|
|555555555*555555**555555555555*5555555555555555555**5*555555555555555555|
|6666666*666666666666**66666666666666666666666666666666666666666666666666|
|77777777777777777777777777*77777777777777777777*777777777777777777777777|
|888888888888888888888888888888888888888888*88888888888888888888888888888|
|99999999*999999999999999*999*99999999999*99999999999*9999999999999999999|
|________________________________________________________________________|
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment