diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 208 |
1 files changed, 104 insertions, 104 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 7d2ad6a5..9c3dd555 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(162070 . 3442535953) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(162070 . 3442698070) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) ((((-562)) . T) (($) -4037 (|has| |#1| (-306)) (|has| |#1| (-362)) (|has| |#1| (-348)) (|has| |#1| (-554))) (((-406 (-562))) -4037 (|has| |#1| (-362)) (|has| |#1| (-348)) (|has| |#1| (-1033 (-406 (-562))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-562)) . T)) @@ -52,7 +52,7 @@ (((|#1| (-530 (-1168))) . T)) (((#0=(-865 |#1|) #0#) . T) ((#1=(-406 (-562)) #1#) . T) (($ $) . T)) ((((-1150)) . T) (((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (|has| |#4| (-367)) (|has| |#3| (-367)) (((|#1|) . T)) @@ -68,7 +68,7 @@ ((((-562)) . T) (((-406 (-562))) -4037 (|has| |#2| (-38 (-406 (-562)))) (|has| |#2| (-1033 (-406 (-562))))) ((|#2|) . T) (($) -4037 (|has| |#2| (-451)) (|has| |#2| (-554)) (|has| |#2| (-904))) (((-859 |#1|)) . T)) (-4037 (|has| |#1| (-362)) (|has| |#1| (-554))) (-4037 (|has| |#1| (-362)) (|has| |#1| (-554))) -((((-2 (|:| -2466 |#1|) (|:| -1960 |#2|))) . T)) +((((-2 (|:| -2464 |#1|) (|:| -1300 |#2|))) . T)) ((($) . T)) ((((-562)) . T) (((-406 (-562))) -4037 (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-1033 (-406 (-562))))) ((|#1|) . T) (($) -4037 (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) (((-1168)) . T)) ((((-857)) -4037 (|has| |#1| (-609 (-857))) (|has| |#1| (-845)) (|has| |#1| (-1092)))) @@ -112,7 +112,7 @@ (|has| |#1| (-367)) (((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) ((((-857)) . T)) (((|#1| |#2|) . T)) @@ -236,8 +236,8 @@ (((|#1|) . T)) ((((-406 (-562))) |has| |#1| (-1033 (-406 (-562)))) (((-562)) |has| |#1| (-1033 (-562))) ((|#1|) . T)) (((|#1|) . T) (((-562)) |has| |#1| (-635 (-562)))) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (|has| |#1| (-554)) ((((-562)) -4037 (|has| |#4| (-171)) (|has| |#4| (-843)) (-12 (|has| |#4| (-1033 (-562))) (|has| |#4| (-1092))) (|has| |#4| (-1044))) ((|#4|) -4037 (|has| |#4| (-171)) (|has| |#4| (-1092))) (((-406 (-562))) -12 (|has| |#4| (-1033 (-406 (-562)))) (|has| |#4| (-1092)))) ((((-562)) -4037 (|has| |#3| (-171)) (|has| |#3| (-843)) (-12 (|has| |#3| (-1033 (-562))) (|has| |#3| (-1092))) (|has| |#3| (-1044))) ((|#3|) -4037 (|has| |#3| (-171)) (|has| |#3| (-1092))) (((-406 (-562))) -12 (|has| |#3| (-1033 (-406 (-562)))) (|has| |#3| (-1092)))) @@ -264,11 +264,11 @@ ((((-535)) |has| |#2| (-610 (-535))) (((-887 (-378))) |has| |#2| (-610 (-887 (-378)))) (((-887 (-562))) |has| |#2| (-610 (-887 (-562))))) ((((-857)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -2466 |#1|) (|:| -1960 |#2|))) . T) (((-857)) . T)) +((((-2 (|:| -2464 |#1|) (|:| -1300 |#2|))) . T) (((-857)) . T)) ((((-535)) |has| |#1| (-610 (-535))) (((-887 (-378))) |has| |#1| (-610 (-887 (-378)))) (((-887 (-562))) |has| |#1| (-610 (-887 (-562))))) (((|#4|) -4037 (|has| |#4| (-171)) (|has| |#4| (-362)) (|has| |#4| (-1044))) (($) |has| |#4| (-171))) (((|#3|) -4037 (|has| |#3| (-171)) (|has| |#3| (-362)) (|has| |#3| (-1044))) (($) |has| |#3| (-171))) -((((-2 (|:| -2466 |#1|) (|:| -1960 |#2|))) . T)) +((((-2 (|:| -2464 |#1|) (|:| -1300 |#2|))) . T)) ((((-857)) . T)) ((((-857)) . T)) ((((-535)) . T) (((-562)) . T) (((-887 (-562))) . T) (((-378)) . T) (((-224)) . T)) @@ -276,7 +276,7 @@ (((|#1|) . T) (((-562)) |has| |#1| (-1033 (-562))) (((-406 (-562))) |has| |#1| (-1033 (-406 (-562))))) ((($) . T) (((-406 (-562))) |has| |#2| (-38 (-406 (-562)))) ((|#2|) . T)) ((((-406 $) (-406 $)) |has| |#2| (-554)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-904)) ((((-1150) (-52)) . T)) @@ -312,7 +312,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1143)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (|has| (-1242 |#1| |#2| |#3| |#4|) (-144)) (|has| (-1242 |#1| |#2| |#3| |#4|) (-146)) (|has| |#1| (-144)) @@ -330,10 +330,10 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-1044))) ((((-857)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((|#1|) . T)) -((((-1256 (-338 (-4066) (-4066 (QUOTE X)) (-693)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) ((#0=(-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) #0#) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))))) +((((-1256 (-338 (-4064) (-4064 (QUOTE X)) (-693)))) . T)) +(((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) ((#0=(-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) #0#) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))))) ((((-857)) . T)) ((((-562) |#1|) . T)) ((((-535)) -12 (|has| |#1| (-610 (-535))) (|has| |#2| (-610 (-535)))) (((-887 (-378))) -12 (|has| |#1| (-610 (-887 (-378)))) (|has| |#2| (-610 (-887 (-378))))) (((-887 (-562))) -12 (|has| |#1| (-610 (-887 (-562)))) (|has| |#2| (-610 (-887 (-562)))))) @@ -430,11 +430,11 @@ ((((-143)) . T)) (((|#3|) |has| |#3| (-1092)) (((-562)) -12 (|has| |#3| (-1033 (-562))) (|has| |#3| (-1092))) (((-406 (-562))) -12 (|has| |#3| (-1033 (-406 (-562)))) (|has| |#3| (-1092)))) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) . T)) ((((-857)) -4037 (|has| |#1| (-609 (-857))) (|has| |#1| (-845)) (|has| |#1| (-1092)))) ((((-535)) |has| |#1| (-610 (-535)))) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) (|has| |#1| (-362)) ((((-1173)) . T)) (-4037 (|has| |#1| (-21)) (|has| |#1| (-843))) @@ -444,13 +444,13 @@ (|has| |#1| (-843)) (-4037 (|has| |#1| (-845)) (|has| |#1| (-1092))) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-535)) |has| |#1| (-610 (-535)))) (((|#1| |#2|) . T)) ((((-1168)) -12 (|has| |#1| (-362)) (|has| |#1| (-895 (-1168))))) ((((-1150) |#1|) . T)) (((|#1| |#2| |#3| (-530 |#3|)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (|has| |#1| (-367)) (|has| |#1| (-367)) (|has| |#1| (-367)) @@ -654,7 +654,7 @@ (((|#4| |#4|) -12 (|has| |#4| (-308 |#4|)) (|has| |#4| (-1092)))) (((|#2|) . T) (((-562)) |has| |#2| (-1033 (-562))) (((-406 (-562))) |has| |#2| (-1033 (-406 (-562))))) (((|#3| |#3|) -12 (|has| |#3| (-308 |#3|)) (|has| |#3| (-1092)))) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) @@ -662,7 +662,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-4037 (|has| |#1| (-845)) (|has| |#1| (-1092))) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((|#2|) . T)) ((((-857)) -4037 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-609 (-857))) (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-367)) (|has| |#2| (-721)) (|has| |#2| (-788)) (|has| |#2| (-843)) (|has| |#2| (-1044)) (|has| |#2| (-1092))) (((-1256 |#2|)) . T)) ((((-406 (-562))) |has| |#1| (-1033 (-406 (-562)))) ((|#1|) . T) (((-562)) . T) (($) . T)) @@ -742,9 +742,9 @@ (-4037 (|has| |#1| (-451)) (|has| |#1| (-904))) ((((-562) |#2|) . T)) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) ((($) -4037 (|has| |#3| (-171)) (|has| |#3| (-843)) (|has| |#3| (-1044))) ((|#3|) -4037 (|has| |#3| (-171)) (|has| |#3| (-362)) (|has| |#3| (-1044)))) ((((-562) |#1|) . T)) @@ -759,11 +759,11 @@ (|has| |#1| (-554)) (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-38 (-406 (-562)))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-857)) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (|has| |#1| (-38 (-406 (-562)))) -((((-387) (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-387) (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (|has| |#1| (-38 (-406 (-562)))) (|has| |#2| (-1143)) (-4037 (|has| |#1| (-362)) (|has| |#1| (-554))) @@ -982,7 +982,7 @@ (|has| |#2| (-171)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-232)) (|has| |#2| (-1044))) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (-4037 (|has| |#3| (-788)) (|has| |#3| (-843))) (-4037 (|has| |#3| (-788)) (|has| |#3| (-843))) ((((-857)) . T)) @@ -1013,10 +1013,10 @@ (((|#1| (-406 (-562))) . T)) (((|#3|) . T) (((-608 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-562)) -4037 (|has| |#2| (-171)) (|has| |#2| (-843)) (-12 (|has| |#2| (-1033 (-562))) (|has| |#2| (-1092))) (|has| |#2| (-1044))) ((|#2|) -4037 (|has| |#2| (-171)) (|has| |#2| (-1092))) (((-406 (-562))) -12 (|has| |#2| (-1033 (-406 (-562)))) (|has| |#2| (-1092)))) (((|#1|) . T) (((-406 (-562))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1025,8 +1025,8 @@ ((((-857)) . T)) ((((-857)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) -(((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) (((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) +(((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) (((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))))) ((((-857)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1039,7 +1039,7 @@ (|has| |#1| (-1092)) (((|#2| |#2|) -4037 (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-1044))) (($ $) |has| |#2| (-171))) (((|#2|) -4037 (|has| |#2| (-171)) (|has| |#2| (-362)))) -((((-562) (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T) ((|#1| |#2|) . T)) +((((-562) (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -4037 (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-1044))) (($) |has| |#2| (-171))) ((((-1173)) . T)) ((((-766)) . T)) @@ -1072,7 +1072,7 @@ (-4037 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-367)) (|has| |#2| (-721)) (|has| |#2| (-788)) (|has| |#2| (-843)) (|has| |#2| (-1044)) (|has| |#2| (-1092))) (-12 (|has| |#3| (-232)) (|has| |#3| (-1044))) (|has| |#2| (-1143)) -(((#0=(-52)) . T) (((-2 (|:| -2320 (-1168)) (|:| -2694 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2319 (-1168)) (|:| -2693 #0#))) . T)) (((|#1| |#2|) . T)) (-4037 (|has| |#3| (-171)) (|has| |#3| (-843)) (|has| |#3| (-1044))) (((|#1| (-562) (-1074)) . T)) @@ -1099,7 +1099,7 @@ ((((-562)) -4037 (|has| |#3| (-171)) (|has| |#3| (-843)) (-12 (|has| |#3| (-1033 (-562))) (|has| |#3| (-1092))) (|has| |#3| (-1044))) ((|#3|) -4037 (|has| |#3| (-171)) (|has| |#3| (-1092))) (((-406 (-562))) -12 (|has| |#3| (-1033 (-406 (-562)))) (|has| |#3| (-1092)))) (((|#1|) . T)) (((|#4|) . T) (((-857)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (|has| |#1| (-554)) (((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) ((((-857)) . T)) @@ -1159,7 +1159,7 @@ (-12 (|has| |#1| (-788)) (|has| |#2| (-788))) (-4037 (|has| |#2| (-171)) (|has| |#2| (-843)) (|has| |#2| (-1044))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (|has| |#1| (-1192)) (((#0=(-562) #0#) . T) ((#1=(-406 (-562)) #1#) . T) (($ $) . T)) ((((-406 (-562))) . T) (($) . T)) @@ -1189,7 +1189,7 @@ ((($) . T) (((-406 (-562))) -4037 (|has| |#1| (-362)) (|has| |#1| (-348))) ((|#1|) . T)) (-4037 (|has| |#1| (-171)) (|has| |#1| (-554))) ((($) . T)) -(((#0=(-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) #0#) |has| (-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))))) +(((#0=(-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) #0#) |has| (-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))))) (|has| |#2| (-845)) ((($) . T)) (((|#2|) |has| |#2| (-1092))) @@ -1202,10 +1202,10 @@ ((((-562)) |has| #0=(-406 |#2|) (-635 (-562))) ((#0#) . T)) ((($) . T) (((-562)) . T)) ((((-562) (-143)) . T)) -((((-562) (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T) ((|#1| |#2|) . T)) +((((-562) (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T) ((|#1| |#2|) . T)) ((((-406 (-562))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-857)) . T)) ((((-905 |#1|)) . T)) (|has| |#1| (-362)) @@ -1232,7 +1232,7 @@ ((((-857)) . T)) ((($) . T)) (((|#2|) . T) (($) . T)) -((((-562) (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T) ((|#1| |#2|) . T)) +((((-562) (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-171))) ((($) |has| |#1| (-554)) ((|#1|) |has| |#1| (-171)) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) @@ -1246,7 +1246,7 @@ (((|#1|) . T)) ((((-535)) |has| |#1| (-610 (-535))) (((-887 (-378))) |has| |#1| (-610 (-887 (-378)))) (((-887 (-562))) |has| |#1| (-610 (-887 (-562))))) ((((-857)) . T)) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-505)) . T)) (|has| |#2| (-843)) ((((-505)) . T)) @@ -1275,7 +1275,7 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1168)) |has| (-406 |#2|) (-895 (-1168)))) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) @@ -1286,7 +1286,7 @@ (((|#2|) . T) (((-562)) . T)) ((((-857)) . T)) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T) ((|#2|) . T)) ((((-857)) . T)) ((((-857)) . T)) ((((-1150) (-1168) (-562) (-224) (-857)) . T)) @@ -1375,7 +1375,7 @@ ((((-994 |#1|)) . T) ((|#1|) . T)) ((((-857)) . T)) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-406 (-562))) . T) (((-406 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1164 |#1|)) . T)) ((((-562)) . T) (($) . T) (((-406 (-562))) . T)) @@ -1383,7 +1383,7 @@ (|has| |#1| (-845)) (((|#2|) . T)) ((((-562)) . T) (($) . T) (((-406 (-562))) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) ((((-562) |#2|) . T)) ((((-857)) -4037 (|has| |#1| (-609 (-857))) (|has| |#1| (-1092)))) (((|#2|) . T)) @@ -1398,7 +1398,7 @@ (|has| |#1| (-1092)) (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-38 (-406 (-562)))) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((|#2| |#2|) . T)) (|has| |#1| (-38 (-406 (-562)))) (((|#2|) . T)) @@ -1433,7 +1433,7 @@ (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) (((|#1| |#2|) . T)) ((((-562) (-143)) . T)) -(((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) +(((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) ((($) -4037 (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) ((|#1|) |has| |#1| (-171)) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) (|has| |#1| (-845)) (((|#2| (-766) (-1074)) . T)) @@ -1477,7 +1477,7 @@ ((((-387) (-1150)) . T)) ((($) |has| |#1| (-554)) ((|#1|) |has| |#1| (-171)) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) ((((-857)) -4037 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-609 (-857))) (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-367)) (|has| |#2| (-721)) (|has| |#2| (-788)) (|has| |#2| (-843)) (|has| |#2| (-1044)) (|has| |#2| (-1092))) (((-1256 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2320 (-1150)) (|:| -2694 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2319 (-1150)) (|:| -2693 #0#))) . T)) (((|#1|) . T)) ((((-857)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) @@ -1526,11 +1526,11 @@ (|has| |#1| (-146)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +(((|#1|) . T) (((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-362))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-1168) (-52)) . T)) ((($ $) . T)) (((|#1| (-562)) . T)) @@ -1577,11 +1577,11 @@ (|has| |#1| (-38 (-406 (-562)))) (-4037 (|has| |#1| (-362)) (|has| |#1| (-348))) (|has| |#1| (-38 (-406 (-562)))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-1168)) |has| |#1| (-895 (-1168))) (((-1074)) . T)) (((|#1|) . T)) (|has| |#1| (-843)) -(((#0=(-2 (|:| -2320 (-1150)) (|:| -2694 (-52))) #0#) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))))) +(((#0=(-2 (|:| -2319 (-1150)) (|:| -2693 (-52))) #0#) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) (|has| |#1| (-1092)) ((((-857)) . T) (((-1173)) . T)) @@ -1627,7 +1627,7 @@ (((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) ((#0=(-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) #0#) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) ((#0=(-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) #0#) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))))) (-4037 (|has| |#2| (-451)) (|has| |#2| (-904))) (-4037 (|has| |#1| (-451)) (|has| |#1| (-904))) (((|#1|) . T) (($) . T)) @@ -1652,7 +1652,7 @@ ((((-406 (-562))) -4037 (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-362))) (($) -4037 (|has| |#1| (-362)) (|has| |#1| (-554))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-362)) ((|#1|) |has| |#1| (-171))) (((|#1|) |has| |#1| (-171)) (((-406 (-562))) -4037 (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-362))) (($) -4037 (|has| |#1| (-362)) (|has| |#1| (-554)))) ((($) |has| |#1| (-554)) ((|#1|) |has| |#1| (-171)) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((((-406 |#2|)) . T) (((-406 (-562))) . T) (($) . T)) ((((-666 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1720,7 +1720,7 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) ((($ $) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((($ $) . T)) ((((-562) (-112)) . T)) ((($) . T)) @@ -1749,7 +1749,7 @@ (((|#1| (-1220 |#1| |#2| |#3|)) . T)) (((|#1| (-766)) . T)) (((|#1|) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-857)) . T)) (|has| |#1| (-1092)) ((((-1150) |#1|) . T)) @@ -1788,7 +1788,7 @@ (|has| |#1| (-554)) (((|#1|) . T)) ((((-857)) . T)) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((|#1|) |has| |#1| (-171))) ((($) |has| |#1| (-554)) ((|#1|) |has| |#1| (-171)) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) @@ -1807,7 +1807,7 @@ (|has| |#1| (-843)) (((|#1| (-562) (-1074)) . T)) (-4037 (|has| |#1| (-895 (-1168))) (|has| |#1| (-1044))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1| (-406 (-562)) (-1074)) . T)) (((|#1| (-766) (-1074)) . T)) (|has| |#1| (-845)) @@ -1825,11 +1825,11 @@ (|has| |#1| (-1092)) ((((-562)) -12 (|has| |#1| (-362)) (|has| |#2| (-635 (-562)))) ((|#2|) |has| |#1| (-362))) (-4037 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-171)) (|has| |#2| (-362)) (|has| |#2| (-367)) (|has| |#2| (-721)) (|has| |#2| (-788)) (|has| |#2| (-843)) (|has| |#2| (-1044)) (|has| |#2| (-1092))) -((((-683 (-338 (-4066) (-4066 (QUOTE X) (QUOTE HESS)) (-693)))) . T)) +((((-683 (-338 (-4064) (-4064 (QUOTE X) (QUOTE HESS)) (-693)))) . T)) (((|#2|) |has| |#2| (-171))) (((|#1|) |has| |#1| (-171))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) ((((-857)) . T)) (|has| |#3| (-843)) ((((-857)) . T)) @@ -1843,9 +1843,9 @@ (((|#2|) |has| |#2| (-362))) ((($) . T) ((|#1|) . T) (((-406 (-562))) |has| |#1| (-362))) (|has| |#1| (-845)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) |has| (-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))))) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) |has| (-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))))) (-4037 (|has| |#1| (-451)) (|has| |#1| (-904))) (((|#2|) . T) (((-562)) |has| |#2| (-635 (-562)))) ((((-857)) . T)) @@ -1895,7 +1895,7 @@ ((((-639 |#1|)) . T)) (|has| |#1| (-904)) (((|#2|) |has| |#2| (-1044))) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (|has| |#1| (-362)) (((|#1|) |has| |#1| (-171))) (((|#1| |#1|) . T)) @@ -1946,14 +1946,14 @@ ((((-112)) |has| |#1| (-1092)) (((-857)) -4037 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-171)) (|has| |#1| (-362)) (|has| |#1| (-472)) (|has| |#1| (-721)) (|has| |#1| (-895 (-1168))) (|has| |#1| (-1044)) (|has| |#1| (-1104)) (|has| |#1| (-1092)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))) . T)) ((((-857)) . T)) ((((-562) |#1|) . T)) ((((-857)) . T)) ((((-693)) . T) (((-406 (-562))) . T) (((-562)) . T)) (((|#1| |#1|) |has| |#1| (-171))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) ((((-378)) . T)) ((((-693)) . T)) ((((-406 (-562))) . #0=(|has| |#2| (-362))) (($) . #0#)) @@ -1972,7 +1972,7 @@ (((|#3|) |has| |#3| (-1044))) ((((-1168)) |has| |#2| (-895 (-1168)))) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-406 (-562))) . T) (($) . T)) (|has| |#1| (-472)) (|has| |#1| (-367)) @@ -2000,11 +2000,11 @@ (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-38 (-406 (-562)))) (|has| |#1| (-845)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-146)) (|has| |#1| (-144)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)))) ((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)))) ((|#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092)))) (((|#2|) . T)) (((|#3|) . T)) ((((-116 |#1|)) . T)) @@ -2022,7 +2022,7 @@ ((((-535)) |has| |#1| (-610 (-535))) (((-887 (-562))) |has| |#1| (-610 (-887 (-562)))) (((-887 (-378))) |has| |#1| (-610 (-887 (-378)))) (((-378)) . #0=(|has| |#1| (-1017))) (((-224)) . #0#)) (((|#1|) |has| |#1| (-362))) ((((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((($ $) . T) (((-608 $) $) . T)) (-4037 (|has| |#1| (-362)) (|has| |#1| (-554))) ((($) . T) (((-1242 |#1| |#2| |#3| |#4|)) . T) (((-406 (-562))) . T)) @@ -2084,7 +2084,7 @@ ((((-947 |#1|)) . T) (((-857)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -4037 (|has| |#1| (-289)) (|has| |#1| (-362))) ((#0=(-406 (-562)) #0#) |has| |#1| (-362))) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((((-947 |#1|)) . T)) ((($) . T)) ((((-562) |#1|) . T)) @@ -2124,7 +2124,7 @@ ((($) -4037 (|has| |#1| (-362)) (|has| |#1| (-348))) (((-406 (-562))) -4037 (|has| |#1| (-362)) (|has| |#1| (-348))) ((|#1|) . T)) ((((-562)) . T)) (|has| |#1| (-38 (-406 (-562)))) -((((-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))))) +((((-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))))) (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) (|has| |#1| (-843)) (|has| |#1| (-38 (-406 (-562)))) @@ -2166,10 +2166,10 @@ ((($) -4037 (|has| |#1| (-171)) (|has| |#1| (-362)) (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) ((|#1|) . T) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) ((((-535)) |has| |#4| (-610 (-535)))) ((((-857)) . T) (((-639 |#4|)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-843)) -(((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) (((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) |has| (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|)) (-308 (-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))))) +(((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092))) (((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) |has| (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|)) (-308 (-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))))) (|has| |#1| (-1092)) (|has| |#1| (-362)) (|has| |#1| (-845)) @@ -2211,7 +2211,7 @@ ((((-857)) . T)) ((((-857)) . T)) ((((-535)) |has| |#1| (-610 (-535)))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-1168) |#1|) |has| |#1| (-513 (-1168) |#1|)) ((|#1| |#1|) |has| |#1| (-308 |#1|))) (((|#1|) -4037 (|has| |#1| (-171)) (|has| |#1| (-362)))) ((((-315 |#1|)) . T)) @@ -2239,7 +2239,7 @@ (|has| |#1| (-554)) (((|#2|) . T)) ((((-562)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) . T)) (-4037 (|has| |#1| (-144)) (|has| |#1| (-146)) (|has| |#1| (-171)) (|has| |#1| (-554)) (|has| |#1| (-1044))) ((((-579 |#1|)) . T)) @@ -2250,7 +2250,7 @@ ((($) . T)) (((|#1|) . T)) ((((-857)) . T)) -(((|#2|) |has| |#2| (-6 (-4404 "*")))) +(((|#2|) |has| |#2| (-6 (-4405 "*")))) (((|#1|) . T)) (((|#1|) . T)) (((|#3|) . T)) @@ -2351,21 +2351,21 @@ (((|#1|) |has| |#1| (-171))) ((((-857)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-308 |#4|)) (|has| |#4| (-1092)))) -(((|#2|) -4037 (|has| |#2| (-6 (-4404 "*"))) (|has| |#2| (-171)))) +(((|#2|) -4037 (|has| |#2| (-6 (-4405 "*"))) (|has| |#2| (-171)))) (-4037 (|has| |#2| (-451)) (|has| |#2| (-554)) (|has| |#2| (-904))) (-4037 (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) (|has| |#2| (-845)) (|has| |#2| (-904)) (|has| |#1| (-904)) (((|#2|) |has| |#2| (-171))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-1248 |#1| |#2| |#3|)) |has| |#1| (-362))) ((((-857)) . T)) ((((-857)) . T)) ((((-535)) . T) (((-562)) . T) (((-887 (-562))) . T) (((-378)) . T) (((-224)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))) . T)) (((|#1|) . T)) ((((-857)) . T)) (((|#1| |#2|) . T)) @@ -2387,7 +2387,7 @@ ((((-857)) . T)) ((((-857)) . T)) ((((-186)) . T) (((-857)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-857)) . T)) ((((-857)) . T)) @@ -2400,7 +2400,7 @@ ((((-857)) . T)) ((((-1150)) . T)) ((((-1168) |#1|) |has| |#1| (-513 (-1168) |#1|)) ((|#1| |#1|) |has| |#1| (-308 |#1|))) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (|has| |#1| (-845)) ((((-857)) . T)) ((((-535)) |has| |#1| (-610 (-535)))) @@ -2457,8 +2457,8 @@ (-4037 (|has| |#1| (-144)) (|has| |#1| (-367))) (-4037 (|has| |#1| (-144)) (|has| |#1| (-367))) (-4037 (|has| |#1| (-144)) (|has| |#1| (-367))) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2320 (-1168)) (|:| -2694 #0#))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2319 (-1168)) (|:| -2693 #0#))) . T)) (|has| |#1| (-348)) ((((-562)) . T)) ((((-857)) . T)) @@ -2535,7 +2535,7 @@ (|has| |#2| (-1017)) ((($) . T)) (|has| |#1| (-904)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2561,7 +2561,7 @@ ((((-406 (-562))) . T)) (-4037 (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) ((((-1150)) . T) (((-857)) . T)) -(((#0=(-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) #0#) |has| (-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))))) +(((#0=(-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) #0#) |has| (-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))))) ((((-1150)) . T)) (|has| |#1| (-904)) (|has| |#2| (-362)) @@ -2597,7 +2597,7 @@ (((|#2|) |has| |#1| (-362))) (((|#2|) |has| |#1| (-362))) ((((-562)) . T) (($) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-171))) (((|#1|) . T)) @@ -2637,9 +2637,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-4037 (|has| |#2| (-171)) (|has| |#2| (-721)) (|has| |#2| (-843)) (|has| |#2| (-1044))) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (|has| |#1| (-38 (-406 (-562)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-406 (-562)))) @@ -2761,7 +2761,7 @@ (|has| |#2| (-362)) ((((-579 |#1|)) . T) (((-406 (-562))) . T) (($) . T) (((-562)) . T)) ((((-562)) . T) (((-406 (-562))) . T) (($) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 (-52)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-562)) . T)) (((|#1|) -12 (|has| |#1| (-308 |#1|)) (|has| |#1| (-1092)))) @@ -2791,7 +2791,7 @@ ((((-579 |#1|)) . T) (($) . T) (((-406 (-562))) . T)) ((($) . T) (((-406 (-562))) . T)) ((($) . T) (((-406 (-562))) . T)) -(((|#2|) |has| |#2| (-6 (-4404 "*")))) +(((|#2|) |has| |#2| (-6 (-4405 "*")))) (((|#1|) . T)) ((((-406 (-562))) |has| |#1| (-1033 (-406 (-562)))) ((|#1|) . T) (((-562)) . T)) (((|#1|) . T)) @@ -2819,7 +2819,7 @@ ((($) -4037 (|has| |#1| (-171)) (|has| |#1| (-451)) (|has| |#1| (-554)) (|has| |#1| (-904))) ((|#1|) . T) (((-406 (-562))) |has| |#1| (-38 (-406 (-562))))) ((((-857)) . T)) (((|#1|) . T)) -((((-2 (|:| -2320 (-1150)) (|:| -2694 |#1|))) . T)) +((((-2 (|:| -2319 (-1150)) (|:| -2693 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2936,7 +2936,7 @@ (((|#1|) . T)) ((((-857)) . T)) (|has| |#2| (-904)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((((-535)) |has| |#2| (-610 (-535))) (((-887 (-378))) |has| |#2| (-610 (-887 (-378)))) (((-887 (-562))) |has| |#2| (-610 (-887 (-562))))) ((((-857)) . T)) ((((-857)) . T)) @@ -3119,7 +3119,7 @@ ((((-1206)) . T) (((-857)) . T) (((-1173)) . T)) ((((-1173)) . T)) ((((-1173)) . T)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) |has| (-2 (|:| -2320 (-1168)) (|:| -2694 (-52))) (-308 (-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))))) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) |has| (-2 (|:| -2319 (-1168)) (|:| -2693 (-52))) (-308 (-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))))) (-4037 (|has| |#2| (-451)) (|has| |#2| (-554)) (|has| |#2| (-904))) ((((-562) |#1|) . T)) ((((-562) |#1|) . T)) @@ -3311,7 +3311,7 @@ (-4037 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-130)) (|has| |#2| (-130))) (-12 (|has| |#1| (-788)) (|has| |#2| (-788)))) ((((-562)) . T)) ((((-562)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-4037 (|has| |#2| (-171)) (|has| |#2| (-721)) (|has| |#2| (-843)) (|has| |#2| (-1044))) @@ -3411,11 +3411,11 @@ ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-362))) ((((-1132 |#1| |#2|)) . T)) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-362))) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((($) . T)) (|has| |#1| (-1017)) -(((|#2|) . T) (((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) ((((-857)) . T)) ((((-535)) |has| |#2| (-610 (-535))) (((-887 (-562))) |has| |#2| (-610 (-887 (-562)))) (((-887 (-378))) |has| |#2| (-610 (-887 (-378)))) (((-378)) . #0=(|has| |#2| (-1017))) (((-224)) . #0#)) ((((-293 |#3|)) . T)) @@ -3469,7 +3469,7 @@ ((((-857)) . T)) ((((-857)) . T)) (((|#1| (-530 |#2|)) . T)) -((((-2 (|:| -2320 (-1168)) (|:| -2694 (-52)))) . T)) +((((-2 (|:| -2319 (-1168)) (|:| -2693 (-52)))) . T)) ((((-562) (-129)) . T)) (((|#1| (-562)) . T)) (((|#1| (-406 (-562))) . T)) @@ -3505,7 +3505,7 @@ (((|#1| |#2|) . T)) ((((-1150) |#1|) . T)) ((((-406 |#2|)) . T)) -((((-2 (|:| -2320 |#1|) (|:| -2694 |#2|))) . T)) +((((-2 (|:| -2319 |#1|) (|:| -2693 |#2|))) . T)) (|has| |#1| (-554)) (|has| |#1| (-554)) ((($) . T) ((|#2|) . T)) @@ -3533,7 +3533,7 @@ (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1132 |#1| |#2|) #0#) |has| (-1132 |#1| |#2|) (-308 (-1132 |#1| |#2|)))) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) #0#) |has| (-2 (|:| -2320 |#1|) (|:| -2694 |#2|)) (-308 (-2 (|:| -2320 |#1|) (|:| -2694 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-308 |#2|)) (|has| |#2| (-1092))) ((#0=(-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) #0#) |has| (-2 (|:| -2319 |#1|) (|:| -2693 |#2|)) (-308 (-2 (|:| -2319 |#1|) (|:| -2693 |#2|))))) (((#0=(-116 |#1|)) |has| #0# (-308 #0#))) ((($ $) . T)) (-4037 (|has| |#1| (-845)) (|has| |#1| (-1092))) |