Created
April 5, 2020 01:50
-
-
Save texdraft/ac651d1494a9d15a8be598b5181099de to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ________________________________________________________________________ | |
| /* 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