diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 214 |
1 files changed, 107 insertions, 107 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index b70e36df..a139019c 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(161804 . 3452261764) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(161804 . 3452516859) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) ((((-564)) . T) (($) -2733 (|has| |#1| (-307)) (|has| |#1| (-363)) (|has| |#1| (-349)) (|has| |#1| (-556))) (((-407 (-564))) -2733 (|has| |#1| (-363)) (|has| |#1| (-349)) (|has| |#1| (-1034 (-407 (-564))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-564)) . T)) @@ -48,12 +48,12 @@ (((|#1|) . T) (((-564)) |has| |#1| (-1034 (-564))) (((-407 (-564))) |has| |#1| (-1034 (-407 (-564))))) (-2733 (|has| |#2| (-172)) (|has| |#2| (-452)) (|has| |#2| (-556)) (|has| |#2| (-905))) (-2733 (|has| |#1| (-172)) (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) -(((|#2| (-482 (-2069 |#1|) (-767))) . T)) +(((|#2| (-482 (-2155 |#1|) (-767))) . T)) (((|#1| (-531 (-1170))) . T)) (((#0=(-866 |#1|) #0#) . T) ((#1=(-407 (-564)) #1#) . T) (($ $) . T)) ((((-1152)) . T) (((-954 (-129))) . T) (((-858)) . T)) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (|has| |#4| (-368)) (|has| |#3| (-368)) (((|#1|) . T)) @@ -70,7 +70,7 @@ ((((-564)) . T) (((-407 (-564))) -2733 (|has| |#2| (-38 (-407 (-564)))) (|has| |#2| (-1034 (-407 (-564))))) ((|#2|) . T) (($) -2733 (|has| |#2| (-452)) (|has| |#2| (-556)) (|has| |#2| (-905))) (((-860 |#1|)) . T)) (-2733 (|has| |#1| (-363)) (|has| |#1| (-556))) (-2733 (|has| |#1| (-363)) (|has| |#1| (-556))) -((((-2 (|:| -2014 |#1|) (|:| -2531 |#2|))) . T)) +((((-2 (|:| -2068 |#1|) (|:| -2005 |#2|))) . T)) ((($) . T)) ((((-564)) . T) (((-407 (-564))) -2733 (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-1034 (-407 (-564))))) ((|#1|) . T) (($) -2733 (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) (((-1170)) . T)) ((((-858)) -2733 (|has| |#1| (-611 (-858))) (|has| |#1| (-846)) (|has| |#1| (-1094)))) @@ -114,7 +114,7 @@ (|has| |#1| (-368)) (((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) ((((-858)) . T)) (((|#1| |#2|) . T)) @@ -238,8 +238,8 @@ (((|#1|) . T)) ((((-407 (-564))) |has| |#1| (-1034 (-407 (-564)))) (((-564)) |has| |#1| (-1034 (-564))) ((|#1|) . T)) (((|#1|) . T) (((-564)) |has| |#1| (-637 (-564)))) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (|has| |#1| (-556)) ((((-564)) -2733 (|has| |#4| (-172)) (|has| |#4| (-844)) (-12 (|has| |#4| (-1034 (-564))) (|has| |#4| (-1094))) (|has| |#4| (-1045))) ((|#4|) -2733 (|has| |#4| (-172)) (|has| |#4| (-1094))) (((-407 (-564))) -12 (|has| |#4| (-1034 (-407 (-564)))) (|has| |#4| (-1094)))) ((((-564)) -2733 (|has| |#3| (-172)) (|has| |#3| (-844)) (-12 (|has| |#3| (-1034 (-564))) (|has| |#3| (-1094))) (|has| |#3| (-1045))) ((|#3|) -2733 (|has| |#3| (-172)) (|has| |#3| (-1094))) (((-407 (-564))) -12 (|has| |#3| (-1034 (-407 (-564)))) (|has| |#3| (-1094)))) @@ -266,11 +266,11 @@ ((((-536)) |has| |#2| (-612 (-536))) (((-888 (-379))) |has| |#2| (-612 (-888 (-379)))) (((-888 (-564))) |has| |#2| (-612 (-888 (-564))))) ((((-858)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -2014 |#1|) (|:| -2531 |#2|))) . T) (((-858)) . T)) +((((-2 (|:| -2068 |#1|) (|:| -2005 |#2|))) . T) (((-858)) . T)) ((((-536)) |has| |#1| (-612 (-536))) (((-888 (-379))) |has| |#1| (-612 (-888 (-379)))) (((-888 (-564))) |has| |#1| (-612 (-888 (-564))))) (((|#4|) -2733 (|has| |#4| (-172)) (|has| |#4| (-363)) (|has| |#4| (-1045))) (($) |has| |#4| (-172))) (((|#3|) -2733 (|has| |#3| (-172)) (|has| |#3| (-363)) (|has| |#3| (-1045))) (($) |has| |#3| (-172))) -((((-2 (|:| -2014 |#1|) (|:| -2531 |#2|))) . T)) +((((-2 (|:| -2068 |#1|) (|:| -2005 |#2|))) . T)) ((((-858)) . T)) ((((-858)) . T)) ((((-536)) . T) (((-564)) . T) (((-888 (-564))) . T) (((-379)) . T) (((-225)) . T)) @@ -278,7 +278,7 @@ (((|#1|) . T) (((-564)) |has| |#1| (-1034 (-564))) (((-407 (-564))) |has| |#1| (-1034 (-407 (-564))))) ((($) . T) (((-407 (-564))) |has| |#2| (-38 (-407 (-564)))) ((|#2|) . T)) ((((-407 $) (-407 $)) |has| |#2| (-556)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-905)) ((((-1152) (-52)) . T)) @@ -314,7 +314,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1145)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (|has| (-1245 |#1| |#2| |#3| |#4|) (-145)) (|has| (-1245 |#1| |#2| |#3| |#4|) (-147)) (|has| |#1| (-145)) @@ -332,10 +332,10 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-1045))) ((((-858)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((|#1|) . T)) -((((-1259 (-339 (-2336) (-2336 (QUOTE X)) (-695)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) ((#0=(-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) #0#) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))))) +((((-1259 (-339 (-2415) (-2415 (QUOTE X)) (-695)))) . T)) +(((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) ((#0=(-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) #0#) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))))) ((((-858)) . T)) ((((-564) |#1|) . T)) ((((-536)) -12 (|has| |#1| (-612 (-536))) (|has| |#2| (-612 (-536)))) (((-888 (-379))) -12 (|has| |#1| (-612 (-888 (-379)))) (|has| |#2| (-612 (-888 (-379))))) (((-888 (-564))) -12 (|has| |#1| (-612 (-888 (-564)))) (|has| |#2| (-612 (-888 (-564)))))) @@ -431,11 +431,11 @@ ((((-144)) . T)) (((|#3|) |has| |#3| (-1094)) (((-564)) -12 (|has| |#3| (-1034 (-564))) (|has| |#3| (-1094))) (((-407 (-564))) -12 (|has| |#3| (-1034 (-407 (-564)))) (|has| |#3| (-1094)))) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) . T)) ((((-858)) -2733 (|has| |#1| (-611 (-858))) (|has| |#1| (-846)) (|has| |#1| (-1094)))) ((((-536)) |has| |#1| (-612 (-536)))) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) (|has| |#1| (-363)) ((((-1175)) . T)) (-2733 (|has| |#1| (-21)) (|has| |#1| (-844))) @@ -445,13 +445,13 @@ (|has| |#1| (-844)) (-2733 (|has| |#1| (-846)) (|has| |#1| (-1094))) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-536)) |has| |#1| (-612 (-536)))) (((|#1| |#2|) . T)) ((((-1170)) -12 (|has| |#1| (-363)) (|has| |#1| (-896 (-1170))))) ((((-1152) |#1|) . T)) (((|#1| |#2| |#3| (-531 |#3|)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (|has| |#1| (-368)) (|has| |#1| (-368)) (|has| |#1| (-368)) @@ -655,7 +655,7 @@ (((|#4| |#4|) -12 (|has| |#4| (-309 |#4|)) (|has| |#4| (-1094)))) (((|#2|) . T) (((-564)) |has| |#2| (-1034 (-564))) (((-407 (-564))) |has| |#2| (-1034 (-407 (-564))))) (((|#3| |#3|) -12 (|has| |#3| (-309 |#3|)) (|has| |#3| (-1094)))) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) @@ -663,7 +663,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-2733 (|has| |#1| (-846)) (|has| |#1| (-1094))) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((|#2|) . T)) ((((-858)) -2733 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-611 (-858))) (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-368)) (|has| |#2| (-722)) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#2| (-1045)) (|has| |#2| (-1094))) (((-1259 |#2|)) . T)) ((((-407 (-564))) |has| |#1| (-1034 (-407 (-564)))) ((|#1|) . T) (((-564)) . T) (($) . T)) @@ -742,9 +742,9 @@ (-2733 (|has| |#1| (-452)) (|has| |#1| (-905))) ((((-564) |#2|) . T)) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) ((($) -2733 (|has| |#3| (-172)) (|has| |#3| (-844)) (|has| |#3| (-1045))) ((|#3|) -2733 (|has| |#3| (-172)) (|has| |#3| (-363)) (|has| |#3| (-1045)))) ((((-564) |#1|) . T)) @@ -759,11 +759,11 @@ (|has| |#1| (-556)) (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-38 (-407 (-564)))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-858)) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (|has| |#1| (-38 (-407 (-564)))) -((((-388) (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-388) (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (|has| |#1| (-38 (-407 (-564)))) (|has| |#2| (-1145)) (-2733 (|has| |#1| (-363)) (|has| |#1| (-556))) @@ -959,7 +959,7 @@ (|has| |#1| (-147)) (|has| |#1| (-145)) (|has| |#4| (-844)) -(((|#2| (-240 (-2069 |#1|) (-767)) (-860 |#1|)) . T)) +(((|#2| (-240 (-2155 |#1|) (-767)) (-860 |#1|)) . T)) (|has| |#3| (-844)) (((|#1| (-531 |#3|) |#3|) . T)) (|has| |#1| (-147)) @@ -980,7 +980,7 @@ (|has| |#2| (-172)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-233)) (|has| |#2| (-1045))) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (-2733 (|has| |#3| (-789)) (|has| |#3| (-844))) (-2733 (|has| |#3| (-789)) (|has| |#3| (-844))) ((((-858)) . T)) @@ -1011,10 +1011,10 @@ (((|#1| (-407 (-564))) . T)) (((|#3|) . T) (((-610 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-564)) -2733 (|has| |#2| (-172)) (|has| |#2| (-844)) (-12 (|has| |#2| (-1034 (-564))) (|has| |#2| (-1094))) (|has| |#2| (-1045))) ((|#2|) -2733 (|has| |#2| (-172)) (|has| |#2| (-1094))) (((-407 (-564))) -12 (|has| |#2| (-1034 (-407 (-564)))) (|has| |#2| (-1094)))) (((|#1|) . T) (((-407 (-564))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1023,8 +1023,8 @@ ((((-858)) . T)) ((((-858)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) -(((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) (((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) +(((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) (((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))))) ((((-858)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1037,7 +1037,7 @@ (|has| |#1| (-1094)) (((|#2| |#2|) -2733 (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-1045))) (($ $) |has| |#2| (-172))) (((|#2|) -2733 (|has| |#2| (-172)) (|has| |#2| (-363)))) -((((-564) (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T) ((|#1| |#2|) . T)) +((((-564) (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -2733 (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-1045))) (($) |has| |#2| (-172))) ((((-1175)) . T)) ((((-767)) . T)) @@ -1070,7 +1070,7 @@ (-2733 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-368)) (|has| |#2| (-722)) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#2| (-1045)) (|has| |#2| (-1094))) (-12 (|has| |#3| (-233)) (|has| |#3| (-1045))) (|has| |#2| (-1145)) -(((#0=(-52)) . T) (((-2 (|:| -3026 (-1170)) (|:| -3683 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -1922 (-1170)) (|:| -3736 #0#))) . T)) (((|#1| |#2|) . T)) (-2733 (|has| |#3| (-172)) (|has| |#3| (-844)) (|has| |#3| (-1045))) (((|#1| (-564) (-1076)) . T)) @@ -1097,7 +1097,7 @@ ((((-564)) -2733 (|has| |#3| (-172)) (|has| |#3| (-844)) (-12 (|has| |#3| (-1034 (-564))) (|has| |#3| (-1094))) (|has| |#3| (-1045))) ((|#3|) -2733 (|has| |#3| (-172)) (|has| |#3| (-1094))) (((-407 (-564))) -12 (|has| |#3| (-1034 (-407 (-564)))) (|has| |#3| (-1094)))) (((|#1|) . T)) (((|#4|) . T) (((-858)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (|has| |#1| (-556)) (((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) ((((-858)) . T)) @@ -1157,7 +1157,7 @@ (-12 (|has| |#1| (-789)) (|has| |#2| (-789))) (-2733 (|has| |#2| (-172)) (|has| |#2| (-844)) (|has| |#2| (-1045))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (|has| |#1| (-1194)) (((#0=(-564) #0#) . T) ((#1=(-407 (-564)) #1#) . T) (($ $) . T)) ((((-407 (-564))) . T) (($) . T)) @@ -1187,7 +1187,7 @@ ((($) . T) (((-407 (-564))) -2733 (|has| |#1| (-363)) (|has| |#1| (-349))) ((|#1|) . T)) (-2733 (|has| |#1| (-172)) (|has| |#1| (-556))) ((($) . T)) -(((#0=(-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) #0#) |has| (-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))))) +(((#0=(-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) #0#) |has| (-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))))) ((($) . T)) (((|#2|) |has| |#2| (-1094))) ((((-858)) -2733 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-611 (-858))) (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-368)) (|has| |#2| (-722)) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#2| (-1045)) (|has| |#2| (-1094))) (((-1259 |#2|)) . T)) @@ -1196,10 +1196,10 @@ ((((-564)) |has| #0=(-407 |#2|) (-637 (-564))) ((#0#) . T)) ((($) . T) (((-564)) . T)) ((((-564) (-144)) . T)) -((((-564) (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T) ((|#1| |#2|) . T)) +((((-564) (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T) ((|#1| |#2|) . T)) ((((-407 (-564))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-858)) . T)) ((((-906 |#1|)) . T)) (|has| |#1| (-363)) @@ -1226,7 +1226,7 @@ ((((-858)) . T)) ((($) . T)) (((|#2|) . T) (($) . T)) -((((-564) (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T) ((|#1| |#2|) . T)) +((((-564) (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-172))) ((($) |has| |#1| (-556)) ((|#1|) |has| |#1| (-172)) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) @@ -1240,7 +1240,7 @@ (((|#1|) . T)) ((((-536)) |has| |#1| (-612 (-536))) (((-888 (-379))) |has| |#1| (-612 (-888 (-379)))) (((-888 (-564))) |has| |#1| (-612 (-888 (-564))))) ((((-858)) . T)) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-506)) . T)) (|has| |#2| (-844)) ((((-506)) . T)) @@ -1269,7 +1269,7 @@ (((|#1|) . T)) ((((-1170)) |has| (-407 |#2|) (-896 (-1170)))) (((|#2|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) @@ -1280,7 +1280,7 @@ (((|#2|) . T) (((-564)) . T)) ((((-858)) . T)) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T) ((|#2|) . T)) ((((-858)) . T)) ((((-858)) . T)) ((((-1152) (-1170) (-564) (-225) (-858)) . T)) @@ -1369,7 +1369,7 @@ ((((-995 |#1|)) . T) ((|#1|) . T)) ((((-858)) . T)) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-407 (-564))) . T) (((-407 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1166 |#1|)) . T)) ((((-564)) . T) (($) . T) (((-407 (-564))) . T)) @@ -1377,7 +1377,7 @@ (|has| |#1| (-846)) (((|#2|) . T)) ((((-564)) . T) (($) . T) (((-407 (-564))) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) ((((-564) |#2|) . T)) ((((-858)) -2733 (|has| |#1| (-611 (-858))) (|has| |#1| (-1094)))) (((|#2|) . T)) @@ -1392,7 +1392,7 @@ (|has| |#1| (-1094)) (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-38 (-407 (-564)))) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((|#2| |#2|) . T)) (|has| |#1| (-38 (-407 (-564)))) (((|#2|) . T)) @@ -1427,7 +1427,7 @@ (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) (((|#1| |#2|) . T)) ((((-564) (-144)) . T)) -(((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) +(((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) ((($) -2733 (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) ((|#1|) |has| |#1| (-172)) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) (|has| |#1| (-846)) (((|#2| (-767) (-1076)) . T)) @@ -1471,7 +1471,7 @@ ((((-388) (-1152)) . T)) ((($) |has| |#1| (-556)) ((|#1|) |has| |#1| (-172)) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) ((((-858)) -2733 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-611 (-858))) (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-368)) (|has| |#2| (-722)) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#2| (-1045)) (|has| |#2| (-1094))) (((-1259 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -3026 (-1152)) (|:| -3683 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -1922 (-1152)) (|:| -3736 #0#))) . T)) (((|#1|) . T)) ((((-858)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) @@ -1500,7 +1500,7 @@ ((((-858)) . T)) ((((-858)) . T)) (|has| |#1| (-1094)) -(((|#2| (-482 (-2069 |#1|) (-767)) (-860 |#1|)) . T)) +(((|#2| (-482 (-2155 |#1|) (-767)) (-860 |#1|)) . T)) ((((-407 (-564))) . #0=(|has| |#2| (-363))) (($) . #0#)) (((|#1| (-531 (-1170)) (-1170)) . T)) (((|#1|) . T)) @@ -1520,11 +1520,11 @@ (|has| |#1| (-147)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +(((|#1|) . T) (((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((((-1168 |#1| |#2| |#3|)) |has| |#1| (-363))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-1170) (-52)) . T)) ((($ $) . T)) (((|#1| (-564)) . T)) @@ -1570,11 +1570,11 @@ (|has| |#1| (-38 (-407 (-564)))) (-2733 (|has| |#1| (-363)) (|has| |#1| (-349))) (|has| |#1| (-38 (-407 (-564)))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-1170)) |has| |#1| (-896 (-1170))) (((-1076)) . T)) (((|#1|) . T)) (|has| |#1| (-844)) -(((#0=(-2 (|:| -3026 (-1152)) (|:| -3683 (-52))) #0#) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))))) +(((#0=(-2 (|:| -1922 (-1152)) (|:| -3736 (-52))) #0#) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) (|has| |#1| (-1094)) ((((-858)) . T) (((-1175)) . T)) @@ -1620,7 +1620,7 @@ (((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) ((#0=(-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) #0#) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) ((#0=(-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) #0#) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))))) (-2733 (|has| |#2| (-452)) (|has| |#2| (-905))) (-2733 (|has| |#1| (-452)) (|has| |#1| (-905))) (((|#1|) . T) (($) . T)) @@ -1645,7 +1645,7 @@ ((((-407 (-564))) -2733 (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-363))) (($) -2733 (|has| |#1| (-363)) (|has| |#1| (-556))) (((-1168 |#1| |#2| |#3|)) |has| |#1| (-363)) ((|#1|) |has| |#1| (-172))) (((|#1|) |has| |#1| (-172)) (((-407 (-564))) -2733 (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-363))) (($) -2733 (|has| |#1| (-363)) (|has| |#1| (-556)))) ((($) |has| |#1| (-556)) ((|#1|) |has| |#1| (-172)) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((((-407 |#2|)) . T) (((-407 (-564))) . T) (($) . T)) ((((-668 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1713,7 +1713,7 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) ((($ $) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((($ $) . T)) ((((-564) (-112)) . T)) ((($) . T)) @@ -1742,7 +1742,7 @@ (((|#1| (-1223 |#1| |#2| |#3|)) . T)) (((|#1| (-767)) . T)) (((|#1|) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-858)) . T)) (|has| |#1| (-1094)) ((((-1152) |#1|) . T)) @@ -1781,7 +1781,7 @@ (|has| |#1| (-556)) (((|#1|) . T)) ((((-858)) . T)) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((|#1|) |has| |#1| (-172))) ((($) |has| |#1| (-556)) ((|#1|) |has| |#1| (-172)) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) @@ -1800,7 +1800,7 @@ (|has| |#1| (-844)) (((|#1| (-564) (-1076)) . T)) (-2733 (|has| |#1| (-896 (-1170))) (|has| |#1| (-1045))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1| (-407 (-564)) (-1076)) . T)) (((|#1| (-767) (-1076)) . T)) (|has| |#1| (-846)) @@ -1818,11 +1818,11 @@ (|has| |#1| (-1094)) ((((-564)) -12 (|has| |#1| (-363)) (|has| |#2| (-637 (-564)))) ((|#2|) |has| |#1| (-363))) (-2733 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-363)) (|has| |#2| (-368)) (|has| |#2| (-722)) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#2| (-1045)) (|has| |#2| (-1094))) -((((-685 (-339 (-2336) (-2336 (QUOTE X) (QUOTE HESS)) (-695)))) . T)) +((((-685 (-339 (-2415) (-2415 (QUOTE X) (QUOTE HESS)) (-695)))) . T)) (((|#2|) |has| |#2| (-172))) (((|#1|) |has| |#1| (-172))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) ((((-858)) . T)) (|has| |#3| (-844)) ((((-858)) . T)) @@ -1836,9 +1836,9 @@ (((|#2|) |has| |#2| (-363))) ((($) . T) ((|#1|) . T) (((-407 (-564))) |has| |#1| (-363))) (|has| |#1| (-846)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) |has| (-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))))) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) |has| (-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))))) (-2733 (|has| |#1| (-452)) (|has| |#1| (-905))) (((|#2|) . T) (((-564)) |has| |#2| (-637 (-564)))) ((((-858)) . T)) @@ -1888,7 +1888,7 @@ ((((-641 |#1|)) . T)) (|has| |#1| (-905)) (((|#2|) |has| |#2| (-1045))) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (|has| |#1| (-363)) (((|#1|) |has| |#1| (-172))) (((|#1| |#1|) . T)) @@ -1937,14 +1937,14 @@ ((((-112)) |has| |#1| (-1094)) (((-858)) -2733 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-172)) (|has| |#1| (-363)) (|has| |#1| (-473)) (|has| |#1| (-722)) (|has| |#1| (-896 (-1170))) (|has| |#1| (-1045)) (|has| |#1| (-1106)) (|has| |#1| (-1094)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))) . T)) ((((-858)) . T)) ((((-564) |#1|) . T)) ((((-858)) . T)) ((((-695)) . T) (((-407 (-564))) . T) (((-564)) . T)) (((|#1| |#1|) |has| |#1| (-172))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) ((((-379)) . T)) ((((-695)) . T)) ((((-407 (-564))) . #0=(|has| |#2| (-363))) (($) . #0#)) @@ -1961,7 +1961,7 @@ (|has| |#1| (-363)) ((((-1170)) |has| |#2| (-896 (-1170)))) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-407 (-564))) . T) (($) . T)) (|has| |#1| (-473)) (|has| |#1| (-368)) @@ -1989,11 +1989,11 @@ (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-38 (-407 (-564)))) (|has| |#1| (-846)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-147)) (|has| |#1| (-145)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)))) ((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)))) ((|#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094)))) (((|#2|) . T)) (((|#3|) . T)) ((((-116 |#1|)) . T)) @@ -2011,7 +2011,7 @@ ((((-536)) |has| |#1| (-612 (-536))) (((-888 (-564))) |has| |#1| (-612 (-888 (-564)))) (((-888 (-379))) |has| |#1| (-612 (-888 (-379)))) (((-379)) . #0=(|has| |#1| (-1018))) (((-225)) . #0#)) (((|#1|) |has| |#1| (-363))) ((((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((($ $) . T) (((-610 $) $) . T)) (-2733 (|has| |#1| (-363)) (|has| |#1| (-556))) ((($) . T) (((-1245 |#1| |#2| |#3| |#4|)) . T) (((-407 (-564))) . T)) @@ -2071,7 +2071,7 @@ ((((-948 |#1|)) . T) (((-858)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -2733 (|has| |#1| (-290)) (|has| |#1| (-363))) ((#0=(-407 (-564)) #0#) |has| |#1| (-363))) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((((-948 |#1|)) . T)) ((($) . T)) ((((-564) |#1|) . T)) @@ -2111,7 +2111,7 @@ ((($) -2733 (|has| |#1| (-363)) (|has| |#1| (-349))) (((-407 (-564))) -2733 (|has| |#1| (-363)) (|has| |#1| (-349))) ((|#1|) . T)) ((((-564)) . T)) (|has| |#1| (-38 (-407 (-564)))) -((((-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))))) +((((-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))))) (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) (|has| |#1| (-844)) (|has| |#1| (-38 (-407 (-564)))) @@ -2154,10 +2154,10 @@ ((($) -2733 (|has| |#1| (-172)) (|has| |#1| (-363)) (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) ((|#1|) . T) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) ((((-536)) |has| |#4| (-612 (-536)))) ((((-858)) . T) (((-641 |#4|)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-844)) -(((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) (((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) |has| (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|)) (-309 (-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))))) +(((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094))) (((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) |has| (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|)) (-309 (-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))))) (|has| |#1| (-1094)) (|has| |#1| (-363)) (((|#1|) . T)) @@ -2198,7 +2198,7 @@ ((((-858)) . T)) ((((-858)) . T)) ((((-536)) |has| |#1| (-612 (-536)))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-1170) |#1|) |has| |#1| (-514 (-1170) |#1|)) ((|#1| |#1|) |has| |#1| (-309 |#1|))) (((|#1|) -2733 (|has| |#1| (-172)) (|has| |#1| (-363)))) ((((-316 |#1|)) . T)) @@ -2226,7 +2226,7 @@ (|has| |#1| (-556)) (((|#2|) . T)) ((((-564)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) . T)) (-2733 (|has| |#1| (-145)) (|has| |#1| (-147)) (|has| |#1| (-172)) (|has| |#1| (-556)) (|has| |#1| (-1045))) ((((-581 |#1|)) . T)) @@ -2344,14 +2344,14 @@ (|has| |#2| (-905)) (|has| |#1| (-905)) (((|#2|) |has| |#2| (-172))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-1251 |#1| |#2| |#3|)) |has| |#1| (-363))) ((((-858)) . T)) ((((-858)) . T)) ((((-536)) . T) (((-564)) . T) (((-888 (-564))) . T) (((-379)) . T) (((-225)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))) . T)) (((|#1|) . T)) ((((-858)) . T)) (((|#1| |#2|) . T)) @@ -2373,7 +2373,7 @@ ((((-858)) . T)) ((((-858)) . T)) ((((-187)) . T) (((-858)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-858)) . T)) ((((-858)) . T)) @@ -2386,7 +2386,7 @@ ((((-858)) . T)) ((((-1152)) . T)) ((((-1170) |#1|) |has| |#1| (-514 (-1170) |#1|)) ((|#1| |#1|) |has| |#1| (-309 |#1|))) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (|has| |#1| (-846)) ((((-858)) . T)) ((((-536)) |has| |#1| (-612 (-536)))) @@ -2443,8 +2443,8 @@ (-2733 (|has| |#1| (-145)) (|has| |#1| (-368))) (-2733 (|has| |#1| (-145)) (|has| |#1| (-368))) (-2733 (|has| |#1| (-145)) (|has| |#1| (-368))) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) -(((#0=(-52)) . T) (((-2 (|:| -3026 (-1170)) (|:| -3683 #0#))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -1922 (-1170)) (|:| -3736 #0#))) . T)) (|has| |#1| (-349)) ((((-564)) . T)) ((((-858)) . T)) @@ -2521,7 +2521,7 @@ (|has| |#2| (-1018)) ((($) . T)) (|has| |#1| (-905)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2542,12 +2542,12 @@ ((((-564)) . T) (($) . T)) ((((-564)) . T) (($) . T)) ((((-767) |#1|) . T)) -(((|#2| (-240 (-2069 |#1|) (-767))) . T)) +(((|#2| (-240 (-2155 |#1|) (-767))) . T)) (((|#1| (-531 |#3|)) . T)) ((((-407 (-564))) . T)) (-2733 (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) ((((-1152)) . T) (((-858)) . T)) -(((#0=(-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) #0#) |has| (-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))))) +(((#0=(-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) #0#) |has| (-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))))) ((((-1152)) . T)) (|has| |#1| (-905)) (|has| |#2| (-363)) @@ -2583,7 +2583,7 @@ (((|#2|) |has| |#1| (-363))) (((|#2|) |has| |#1| (-363))) ((((-564)) . T) (($) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-172))) (((|#1|) . T)) @@ -2623,9 +2623,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-2733 (|has| |#2| (-172)) (|has| |#2| (-722)) (|has| |#2| (-844)) (|has| |#2| (-1045))) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (|has| |#1| (-38 (-407 (-564)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-407 (-564)))) @@ -2748,7 +2748,7 @@ (|has| |#2| (-363)) ((((-581 |#1|)) . T) (((-407 (-564))) . T) (($) . T) (((-564)) . T)) ((((-564)) . T) (((-407 (-564))) . T) (($) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 (-52)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-564)) . T)) (((|#1|) -12 (|has| |#1| (-309 |#1|)) (|has| |#1| (-1094)))) @@ -2806,7 +2806,7 @@ ((($) -2733 (|has| |#1| (-172)) (|has| |#1| (-452)) (|has| |#1| (-556)) (|has| |#1| (-905))) ((|#1|) . T) (((-407 (-564))) |has| |#1| (-38 (-407 (-564))))) ((((-858)) . T)) (((|#1|) . T)) -((((-2 (|:| -3026 (-1152)) (|:| -3683 |#1|))) . T)) +((((-2 (|:| -1922 (-1152)) (|:| -3736 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2923,7 +2923,7 @@ (((|#1|) . T)) ((((-858)) . T)) (|has| |#2| (-905)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((((-536)) |has| |#2| (-612 (-536))) (((-888 (-379))) |has| |#2| (-612 (-888 (-379)))) (((-888 (-564))) |has| |#2| (-612 (-888 (-564))))) ((((-858)) . T)) ((((-858)) . T)) @@ -2964,7 +2964,7 @@ ((((-407 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1094)) -(((|#2| (-482 (-2069 |#1|) (-767))) . T)) +(((|#2| (-482 (-2155 |#1|) (-767))) . T)) ((((-564) |#1|) . T)) ((((-1152)) . T) (((-858)) . T)) (((|#2| |#2|) . T)) @@ -3020,7 +3020,7 @@ (((|#1|) . T)) (|has| |#1| (-233)) (((|#1| (-531 |#3|)) . T)) -(((|#2| (-240 (-2069 |#1|) (-767))) . T)) +(((|#2| (-240 (-2155 |#1|) (-767))) . T)) (|has| |#1| (-368)) (|has| |#1| (-368)) (|has| |#1| (-368)) @@ -3106,7 +3106,7 @@ ((((-1208)) . T) (((-858)) . T) (((-1175)) . T)) ((((-1175)) . T)) ((((-1175)) . T)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) |has| (-2 (|:| -3026 (-1170)) (|:| -3683 (-52))) (-309 (-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))))) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) |has| (-2 (|:| -1922 (-1170)) (|:| -3736 (-52))) (-309 (-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))))) (-2733 (|has| |#2| (-452)) (|has| |#2| (-556)) (|has| |#2| (-905))) ((((-564) |#1|) . T)) ((((-564) |#1|) . T)) @@ -3298,7 +3298,7 @@ (-2733 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-131)) (|has| |#2| (-131))) (-12 (|has| |#1| (-789)) (|has| |#2| (-789)))) ((((-564)) . T)) ((((-564)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-2733 (|has| |#2| (-172)) (|has| |#2| (-722)) (|has| |#2| (-844)) (|has| |#2| (-1045))) @@ -3398,11 +3398,11 @@ ((((-1168 |#1| |#2| |#3|)) |has| |#1| (-363))) ((((-1134 |#1| |#2|)) . T)) ((((-1168 |#1| |#2| |#3|)) |has| |#1| (-363))) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((($) . T)) (|has| |#1| (-1018)) -(((|#2|) . T) (((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) ((((-858)) . T)) ((((-536)) |has| |#2| (-612 (-536))) (((-888 (-564))) |has| |#2| (-612 (-888 (-564)))) (((-888 (-379))) |has| |#2| (-612 (-888 (-379)))) (((-379)) . #0=(|has| |#2| (-1018))) (((-225)) . #0#)) ((((-294 |#3|)) . T)) @@ -3456,7 +3456,7 @@ ((((-858)) . T)) ((((-858)) . T)) (((|#1| (-531 |#2|)) . T)) -((((-2 (|:| -3026 (-1170)) (|:| -3683 (-52)))) . T)) +((((-2 (|:| -1922 (-1170)) (|:| -3736 (-52)))) . T)) ((((-564) (-129)) . T)) (((|#1| (-564)) . T)) (((|#1| (-407 (-564))) . T)) @@ -3492,7 +3492,7 @@ (((|#1| |#2|) . T)) ((((-1152) |#1|) . T)) ((((-407 |#2|)) . T)) -((((-2 (|:| -3026 |#1|) (|:| -3683 |#2|))) . T)) +((((-2 (|:| -1922 |#1|) (|:| -3736 |#2|))) . T)) (|has| |#1| (-556)) (|has| |#1| (-556)) ((($) . T) ((|#2|) . T)) @@ -3520,7 +3520,7 @@ (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1134 |#1| |#2|) #0#) |has| (-1134 |#1| |#2|) (-309 (-1134 |#1| |#2|)))) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) #0#) |has| (-2 (|:| -3026 |#1|) (|:| -3683 |#2|)) (-309 (-2 (|:| -3026 |#1|) (|:| -3683 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-309 |#2|)) (|has| |#2| (-1094))) ((#0=(-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) #0#) |has| (-2 (|:| -1922 |#1|) (|:| -3736 |#2|)) (-309 (-2 (|:| -1922 |#1|) (|:| -3736 |#2|))))) (((#0=(-116 |#1|)) |has| #0# (-309 #0#))) ((($ $) . T)) (-2733 (|has| |#1| (-846)) (|has| |#1| (-1094))) |