diff options
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r-- | src/share/algebra/category.daase | 222 |
1 files changed, 111 insertions, 111 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index dba73988..794b9022 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(188029 . 3453749799) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(188029 . 3453990502) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) ((((-566)) . T) (($) -2805 (|has| |#1| (-308)) (|has| |#1| (-365)) (|has| |#1| (-351)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351)) (|has| |#1| (-1038 (-409 (-566))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-566)) . T)) @@ -51,12 +51,12 @@ (((|#1|) . T) (((-566)) |has| |#1| (-1038 (-566))) (((-409 (-566))) |has| |#1| (-1038 (-409 (-566))))) (-2805 (|has| |#2| (-172)) (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))) (-2805 (|has| |#1| (-172)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) -(((|#2| (-484 (-2997 |#1|) (-771))) . T)) +(((|#2| (-484 (-3020 |#1|) (-771))) . T)) (((|#1| (-533 (-1175))) . T)) (((#0=(-870 |#1|) #0#) . T) ((#1=(-409 (-566)) #1#) . T) (($ $) . T)) ((((-1157)) . T) (((-958 (-129))) . T) (((-862)) . T)) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (|has| |#4| (-370)) (|has| |#3| (-370)) (((|#1|) . T)) @@ -73,7 +73,7 @@ ((((-566)) . T) (((-409 (-566))) -2805 (|has| |#2| (-38 (-409 (-566)))) (|has| |#2| (-1038 (-409 (-566))))) ((|#2|) . T) (($) -2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))) (((-864 |#1|)) . T)) (-2805 (|has| |#1| (-365)) (|has| |#1| (-558))) (-2805 (|has| |#1| (-365)) (|has| |#1| (-558))) -((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T)) +((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T)) ((($) . T)) ((((-566)) . T) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-1038 (-409 (-566))))) ((|#1|) . T) (($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) (((-1175)) . T)) ((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-850)) (|has| |#1| (-1099)))) @@ -129,7 +129,7 @@ (((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566)))) (($) . T)) (-2805 (|has| |#1| (-850)) (|has| |#1| (-1099))) (((|#1|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-566)) . T)) ((((-862)) . T)) (((|#1| |#2|) . T)) @@ -268,8 +268,8 @@ (((|#1|) . T)) ((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) (((-566)) |has| |#1| (-1038 (-566))) ((|#1|) . T)) (((|#1|) . T) (((-566)) |has| |#1| (-639 (-566)))) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (|has| |#1| (-558)) ((((-566)) -2805 (|has| |#4| (-172)) (|has| |#4| (-848)) (-12 (|has| |#4| (-1038 (-566))) (|has| |#4| (-1099))) (|has| |#4| (-1049))) ((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-1099))) (((-409 (-566))) -12 (|has| |#4| (-1038 (-409 (-566)))) (|has| |#4| (-1099)))) ((((-566)) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (-12 (|has| |#3| (-1038 (-566))) (|has| |#3| (-1099))) (|has| |#3| (-1049))) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-1099))) (((-409 (-566))) -12 (|has| |#3| (-1038 (-409 (-566)))) (|has| |#3| (-1099)))) @@ -298,11 +298,11 @@ ((((-538)) |has| |#2| (-614 (-538))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566))))) ((((-862)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T) (((-862)) . T)) +((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T) (((-862)) . T)) ((((-538)) |has| |#1| (-614 (-538))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566))))) (((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-365)) (|has| |#4| (-1049))) (($) |has| |#4| (-172))) (((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049))) (($) |has| |#3| (-172))) -((((-2 (|:| -2168 |#1|) (|:| -3250 |#2|))) . T)) +((((-2 (|:| -2208 |#1|) (|:| -2456 |#2|))) . T)) ((((-862)) . T)) ((((-862)) . T)) ((((-538)) . T) (((-566)) . T) (((-892 (-566))) . T) (((-381)) . T) (((-225)) . T)) @@ -310,7 +310,7 @@ (((|#1|) . T) (((-566)) |has| |#1| (-1038 (-566))) (((-409 (-566))) |has| |#1| (-1038 (-409 (-566))))) ((($) . T) (((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) . T)) ((((-409 $) (-409 $)) |has| |#2| (-558)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-909)) ((((-1157) (-52)) . T)) @@ -349,7 +349,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1150)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (|has| (-1250 |#1| |#2| |#3| |#4|) (-145)) (|has| (-1250 |#1| |#2| |#3| |#4|) (-147)) (|has| |#1| (-145)) @@ -367,10 +367,10 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-1049))) ((((-862)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((|#1|) . T)) -((((-1264 (-341 (-2523) (-2523 (QUOTE X)) (-699)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))))) +((((-1264 (-341 (-3791) (-3791 (QUOTE X)) (-699)))) . T)) +(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))))) ((((-862)) . T)) ((((-566) |#1|) . T)) ((((-538)) -12 (|has| |#1| (-614 (-538))) (|has| |#2| (-614 (-538)))) (((-892 (-381))) -12 (|has| |#1| (-614 (-892 (-381)))) (|has| |#2| (-614 (-892 (-381))))) (((-892 (-566))) -12 (|has| |#1| (-614 (-892 (-566)))) (|has| |#2| (-614 (-892 (-566)))))) @@ -488,12 +488,12 @@ ((((-144)) . T)) (((|#3|) |has| |#3| (-1099)) (((-566)) -12 (|has| |#3| (-1038 (-566))) (|has| |#3| (-1099))) (((-409 (-566))) -12 (|has| |#3| (-1038 (-409 (-566)))) (|has| |#3| (-1099)))) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T)) ((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-850)) (|has| |#1| (-1099)))) ((((-538)) |has| |#1| (-614 (-538)))) (((|#1|) |has| |#1| (-172))) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) (|has| |#1| (-365)) ((((-1180)) . T)) (((|#1|) . T)) @@ -504,13 +504,13 @@ (|has| |#1| (-848)) (-2805 (|has| |#1| (-850)) (|has| |#1| (-1099))) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-538)) |has| |#1| (-614 (-538)))) (((|#1| |#2|) . T)) ((((-1175)) -12 (|has| |#1| (-365)) (|has| |#1| (-900 (-1175))))) ((((-1157) |#1|) . T)) (((|#1| |#2| |#3| (-533 |#3|)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (|has| |#1| (-370)) (|has| |#1| (-370)) (|has| |#1| (-370)) @@ -726,7 +726,7 @@ ((((-1139 |#1| |#2|)) |has| (-1139 |#1| |#2|) (-310 (-1139 |#1| |#2|)))) (((|#4| |#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099)))) (((|#3| |#3|) -12 (|has| |#3| (-310 |#3|)) (|has| |#3| (-1099)))) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((|#2|) . T) (((-566)) |has| |#2| (-1038 (-566))) (((-409 (-566))) |has| |#2| (-1038 (-409 (-566))))) (((|#1|) . T)) (((|#1| |#2|) . T)) @@ -735,7 +735,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-2805 (|has| |#1| (-850)) (|has| |#1| (-1099))) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((|#2|) . T)) ((((-862)) -2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-613 (-862))) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) (((-1264 |#2|)) . T)) ((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) ((|#1|) . T) (((-566)) . T) (($) . T)) @@ -834,9 +834,9 @@ (-2805 (|has| |#1| (-454)) (|has| |#1| (-909))) ((((-566) |#2|) . T)) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) ((($) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049))) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049)))) ((((-566) |#1|) . T)) @@ -851,11 +851,11 @@ (|has| |#1| (-558)) (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-38 (-409 (-566)))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-862)) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (|has| |#1| (-38 (-409 (-566)))) -((((-390) (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-390) (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (|has| |#1| (-38 (-409 (-566)))) (|has| |#2| (-1150)) (-2805 (|has| |#1| (-365)) (|has| |#1| (-558))) @@ -1070,7 +1070,7 @@ (|has| |#1| (-147)) (|has| |#1| (-145)) (|has| |#4| (-848)) -(((|#2| (-240 (-2997 |#1|) (-771)) (-864 |#1|)) . T)) +(((|#2| (-240 (-3020 |#1|) (-771)) (-864 |#1|)) . T)) (|has| |#3| (-848)) (((|#1| (-533 |#3|) |#3|) . T)) (|has| |#1| (-147)) @@ -1091,7 +1091,7 @@ (|has| |#2| (-172)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-233)) (|has| |#2| (-1049))) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (-2805 (|has| |#3| (-793)) (|has| |#3| (-848))) (-2805 (|has| |#3| (-793)) (|has| |#3| (-848))) ((((-862)) . T)) @@ -1122,10 +1122,10 @@ (((|#1| (-409 (-566))) . T)) (((|#3|) . T) (((-612 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-566)) -2805 (|has| |#2| (-172)) (|has| |#2| (-848)) (-12 (|has| |#2| (-1038 (-566))) (|has| |#2| (-1099))) (|has| |#2| (-1049))) ((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-1099))) (((-409 (-566))) -12 (|has| |#2| (-1038 (-409 (-566)))) (|has| |#2| (-1099)))) (((|#1|) . T) (((-409 (-566))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1134,8 +1134,8 @@ ((((-862)) . T)) ((((-862)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) -(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) +(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))))) ((((-862)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1151,7 +1151,7 @@ (|has| |#1| (-1099)) (((|#2| |#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-1049))) (($ $) |has| |#2| (-172))) (((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365)))) -((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T)) +((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -2805 (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-1049))) (($) |has| |#2| (-172))) ((((-566)) . T)) ((((-1180)) . T)) @@ -1195,7 +1195,7 @@ (-2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) (-12 (|has| |#3| (-233)) (|has| |#3| (-1049))) (|has| |#2| (-1150)) -(((#0=(-52)) . T) (((-2 (|:| -2010 (-1175)) (|:| -2818 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2050 (-1175)) (|:| -2849 #0#))) . T)) (((|#1| |#2|) . T)) (-2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049))) (((|#1| (-566) (-1081)) . T)) @@ -1224,7 +1224,7 @@ (((|#4|) . T) (((-862)) . T)) (((|#3|) . T) ((|#2|) . T) (($) -2805 (|has| |#4| (-172)) (|has| |#4| (-848)) (|has| |#4| (-1049))) (((-566)) . T) ((|#4|) -2805 (|has| |#4| (-172)) (|has| |#4| (-365)) (|has| |#4| (-1049)))) (((|#2|) . T) (($) -2805 (|has| |#3| (-172)) (|has| |#3| (-848)) (|has| |#3| (-1049))) (((-566)) . T) ((|#3|) -2805 (|has| |#3| (-172)) (|has| |#3| (-365)) (|has| |#3| (-1049)))) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (|has| |#1| (-558)) (((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) ((((-862)) . T)) @@ -1284,7 +1284,7 @@ (-12 (|has| |#1| (-793)) (|has| |#2| (-793))) (-2805 (|has| |#2| (-172)) (|has| |#2| (-848)) (|has| |#2| (-1049))) ((($) . T) (((-566)) . T) ((|#2|) . T)) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#2|) . T) (($) . T)) (|has| |#1| (-1199)) (((#0=(-566) #0#) . T) ((#1=(-409 (-566)) #1#) . T) (($ $) . T)) @@ -1315,7 +1315,7 @@ ((($) . T) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T)) (-2805 (|has| |#1| (-172)) (|has| |#1| (-558))) ((($) . T)) -(((#0=(-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))))) +(((#0=(-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))))) ((($) . T)) ((($) . T)) (((|#2|) |has| |#2| (-1099))) @@ -1331,10 +1331,10 @@ ((((-566)) |has| #0=(-409 |#2|) (-639 (-566))) ((#0#) . T)) ((($) . T) (((-566)) . T)) ((((-566) (-144)) . T)) -((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T)) +((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T)) ((((-409 (-566))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-862)) . T)) ((((-910 |#1|)) . T)) (|has| |#1| (-365)) @@ -1363,7 +1363,7 @@ ((((-862)) . T)) ((($) . T)) (((|#2|) . T) (($) . T)) -((((-566) (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#1| |#2|) . T)) +((((-566) (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-172))) ((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) @@ -1378,7 +1378,7 @@ ((((-538)) |has| |#1| (-614 (-538))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566))))) ((((-862)) . T)) ((((-870 |#1|)) . T) (($) . T) (((-409 (-566))) . T)) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-508)) . T)) (|has| |#2| (-848)) ((((-508)) . T)) @@ -1413,7 +1413,7 @@ (((|#1|) . T)) ((((-1175)) |has| (-409 |#2|) (-900 (-1175)))) (((|#2|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) ((((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) |has| |#2| (-172)) (($) -2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909)))) ((((-409 (-566))) |has| |#2| (-38 (-409 (-566)))) ((|#2|) . T) (($) -2805 (|has| |#2| (-172)) (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909)))) ((((-409 (-566))) |has| |#1| (-38 (-409 (-566)))) ((|#1|) |has| |#1| (-172)) (($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909)))) @@ -1430,7 +1430,7 @@ (((|#2|) . T) (((-566)) . T)) ((((-862)) . T)) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T) ((|#2|) . T)) ((((-862)) . T)) ((((-862)) . T)) ((((-1157) (-1175) (-566) (-225) (-862)) . T)) @@ -1521,7 +1521,7 @@ ((((-999 |#1|)) . T) ((|#1|) . T)) ((((-862)) . T)) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-409 (-566))) . T) (((-409 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1171 |#1|)) . T)) ((((-566)) . T) (($) . T) (((-409 (-566))) . T)) @@ -1530,7 +1530,7 @@ (((|#1|) . T) (((-566)) . T) (($) . T)) (((|#2|) . T)) ((((-566)) . T) (($) . T) (((-409 (-566))) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) ((((-862)) -2805 (|has| |#1| (-613 (-862))) (|has| |#1| (-1099)))) ((((-566) |#2|) . T)) (((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T)) @@ -1544,7 +1544,7 @@ (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-38 (-409 (-566)))) ((((-1256 |#1| |#2| |#3|)) |has| |#1| (-365))) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((|#2| |#2|) . T)) (|has| |#1| (-1099)) (|has| |#1| (-38 (-409 (-566)))) @@ -1589,7 +1589,7 @@ (((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) (((|#1| |#2|) . T)) ((((-566) (-144)) . T)) -(((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099)))) +(((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099)))) ((($) -2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) (|has| |#1| (-850)) (((|#2| (-771) (-1081)) . T)) @@ -1642,7 +1642,7 @@ ((((-390) (-1157)) . T)) ((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) ((((-862)) -2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-613 (-862))) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) (((-1264 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 #0#))) . T)) (((|#1|) . T)) ((((-862)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099)))) @@ -1672,7 +1672,7 @@ ((((-862)) . T)) ((((-862)) . T)) (|has| |#1| (-1099)) -(((|#2| (-484 (-2997 |#1|) (-771)) (-864 |#1|)) . T)) +(((|#2| (-484 (-3020 |#1|) (-771)) (-864 |#1|)) . T)) ((((-409 (-566))) . #0=(|has| |#2| (-365))) (($) . #0#)) (((|#1| (-533 (-1175)) (-1175)) . T)) (((|#1|) . T)) @@ -1693,12 +1693,12 @@ (((|#2|) |has| |#2| (-172))) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-1175) (-52)) . T)) ((($ $) . T)) (((|#1| (-566)) . T)) @@ -1748,11 +1748,11 @@ (-2805 (|has| |#1| (-365)) (|has| |#1| (-351))) (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-38 (-409 (-566)))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-1175)) |has| |#1| (-900 (-1175))) (((-1081)) . T)) (((|#1|) . T)) (|has| |#1| (-848)) -(((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))))) +(((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) (|has| |#1| (-1099)) ((((-862)) . T) (((-1180)) . T)) @@ -1812,7 +1812,7 @@ (((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) #0#) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) ((#0=(-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) #0#) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))))) (-2805 (|has| |#2| (-454)) (|has| |#2| (-909))) (-2805 (|has| |#1| (-454)) (|has| |#1| (-909))) (((|#1|) . T) (($) . T)) @@ -1837,7 +1837,7 @@ ((((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (($) -2805 (|has| |#1| (-365)) (|has| |#1| (-558))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)) ((|#1|) |has| |#1| (-172))) (((|#1|) |has| |#1| (-172)) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (($) -2805 (|has| |#1| (-365)) (|has| |#1| (-558)))) ((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((((-409 |#2|)) . T) (((-409 (-566))) . T) (($) . T)) ((((-672 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1915,7 +1915,7 @@ ((((-862)) . T)) ((((-862)) . T)) ((($ $) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((($ $) . T)) ((((-566) (-112)) . T)) ((($) . T)) @@ -1944,7 +1944,7 @@ (((|#1| (-1228 |#1| |#2| |#3|)) . T)) (((|#1| (-771)) . T)) (((|#1|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-862)) . T)) (|has| |#1| (-1099)) ((((-1157) |#1|) . T)) @@ -1991,7 +1991,7 @@ ((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365))) (((-1173 |#1| |#2| |#3|)) |has| |#1| (-365)) ((|#1|) . T)) (((|#1|) . T) (($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-558))) (((-409 (-566))) -2805 (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-365)))) ((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-558))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((|#1|) |has| |#1| (-172))) ((((-862)) . T)) ((($) |has| |#1| (-558)) ((|#1|) |has| |#1| (-172)) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) @@ -2015,7 +2015,7 @@ (|has| |#1| (-848)) (((|#1| (-566) (-1081)) . T)) (-2805 (|has| |#1| (-900 (-1175))) (|has| |#1| (-1049))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1| (-409 (-566)) (-1081)) . T)) (((|#1| (-771) (-1081)) . T)) (|has| |#1| (-850)) @@ -2034,11 +2034,11 @@ (|has| |#1| (-1099)) ((((-566)) -12 (|has| |#1| (-365)) (|has| |#2| (-639 (-566)))) ((|#2|) |has| |#1| (-365))) (-2805 (|has| |#2| (-25)) (|has| |#2| (-131)) (|has| |#2| (-172)) (|has| |#2| (-365)) (|has| |#2| (-370)) (|has| |#2| (-726)) (|has| |#2| (-793)) (|has| |#2| (-848)) (|has| |#2| (-1049)) (|has| |#2| (-1099))) -((((-689 (-341 (-2523) (-2523 (QUOTE X) (QUOTE HESS)) (-699)))) . T)) +((((-689 (-341 (-3791) (-3791 (QUOTE X) (QUOTE HESS)) (-699)))) . T)) (((|#2|) |has| |#2| (-172))) (((|#1|) |has| |#1| (-172))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) ((((-862)) . T)) (|has| |#3| (-848)) ((((-862)) . T)) @@ -2054,11 +2054,11 @@ ((($) . T) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-365))) (|has| |#1| (-850)) (((|#1|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T) (((-566)) . T)) (((|#2|) . T)) ((((-566)) . T) ((|#3|) . T)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))))) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))))) (-2805 (|has| |#1| (-454)) (|has| |#1| (-909))) (((|#2|) . T) (((-566)) |has| |#2| (-639 (-566)))) ((((-862)) . T)) @@ -2117,7 +2117,7 @@ ((((-644 |#1|)) . T)) (|has| |#1| (-909)) (((|#2|) |has| |#2| (-1049))) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (|has| |#1| (-365)) (((|#1|) |has| |#1| (-172))) (((|#1| |#1|) . T)) @@ -2169,7 +2169,7 @@ (((|#1| |#2|) . T)) ((($) . T) (((-566)) . T) (((-409 (-566))) . T)) ((((-566)) . T) (($) . T) (((-409 (-566))) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T)) (((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T)) (((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T)) (((|#1|) . T) (((-409 (-566))) . T) (((-566)) . T) (($) . T)) @@ -2183,7 +2183,7 @@ (((|#2|) . T)) ((($) . T) (((-566)) . T) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T)) ((((-566) |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) ((((-381)) . T)) ((((-699)) . T)) ((((-409 (-566))) . #0=(|has| |#2| (-365))) (($) . #0#)) @@ -2200,7 +2200,7 @@ (|has| |#1| (-365)) ((((-1175)) |has| |#2| (-900 (-1175)))) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-409 (-566))) . T) (($) . T)) (|has| |#1| (-475)) (|has| |#1| (-370)) @@ -2228,12 +2228,12 @@ (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-38 (-409 (-566)))) (|has| |#1| (-850)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-566)) . T)) (|has| |#1| (-147)) (|has| |#1| (-145)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)))) ((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099)))) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)))) ((|#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099)))) (((|#2|) . T)) (((|#3|) . T)) ((((-116 |#1|)) . T)) @@ -2253,7 +2253,7 @@ ((((-538)) |has| |#1| (-614 (-538))) (((-892 (-566))) |has| |#1| (-614 (-892 (-566)))) (((-892 (-381))) |has| |#1| (-614 (-892 (-381)))) (((-381)) . #0=(|has| |#1| (-1022))) (((-225)) . #0#)) (((|#1|) |has| |#1| (-365))) ((((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((($ $) . T) (((-612 $) $) . T)) (-2805 (|has| |#1| (-365)) (|has| |#1| (-558))) ((($) . T) (((-1250 |#1| |#2| |#3| |#4|)) . T) (((-409 (-566))) . T)) @@ -2326,7 +2326,7 @@ ((((-952 |#1|)) . T) (((-862)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -2805 (|has| |#1| (-291)) (|has| |#1| (-365))) ((#0=(-409 (-566)) #0#) |has| |#1| (-365))) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((((-952 |#1|)) . T)) ((($) . T)) ((((-566) |#1|) . T)) @@ -2373,7 +2373,7 @@ ((($) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) (((-409 (-566))) -2805 (|has| |#1| (-365)) (|has| |#1| (-351))) ((|#1|) . T)) ((((-566)) . T)) (|has| |#1| (-38 (-409 (-566)))) -((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))))) +((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))))) (((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) (|has| |#1| (-848)) (|has| |#1| (-38 (-409 (-566)))) @@ -2416,10 +2416,10 @@ ((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) ((((-538)) |has| |#4| (-614 (-538)))) ((((-862)) . T) (((-644 |#4|)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-848)) -(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) |has| (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|)) (-310 (-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))))) +(((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099))) (((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) |has| (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|)) (-310 (-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))))) (|has| |#1| (-1099)) (|has| |#1| (-365)) (((|#1|) . T)) @@ -2464,7 +2464,7 @@ ((((-862)) . T)) ((((-862)) . T)) ((((-538)) |has| |#1| (-614 (-538)))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-566)) . T) (($) . T) (((-409 (-566))) . T)) ((((-1175) |#1|) |has| |#1| (-516 (-1175) |#1|)) ((|#1| |#1|) |has| |#1| (-310 |#1|))) (((|#1|) -2805 (|has| |#1| (-172)) (|has| |#1| (-365)))) @@ -2503,7 +2503,7 @@ (|has| |#1| (-558)) (((|#2|) . T)) ((((-566)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T)) (-2805 (|has| |#1| (-145)) (|has| |#1| (-147)) (|has| |#1| (-172)) (|has| |#1| (-558)) (|has| |#1| (-1049))) (((|#1| (-59 |#1|) (-59 |#1|)) . T)) @@ -2514,7 +2514,7 @@ ((($) . T)) (((|#1|) . T)) ((((-862)) . T)) -(((|#2|) |has| |#2| (-6 (-4419 "*")))) +(((|#2|) |has| |#2| (-6 (-4416 "*")))) (((|#1|) . T)) (((|#1|) . T)) ((($) . T)) @@ -2636,22 +2636,22 @@ (((|#2|) . T)) (((|#4| |#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099)))) (((|#2|) . T)) -(((|#2|) -2805 (|has| |#2| (-6 (-4419 "*"))) (|has| |#2| (-172)))) +(((|#2|) -2805 (|has| |#2| (-6 (-4416 "*"))) (|has| |#2| (-172)))) (-2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))) (-2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) (|has| |#2| (-909)) (|has| |#1| (-909)) (((|#2|) |has| |#2| (-172))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-1256 |#1| |#2| |#3|)) |has| |#1| (-365))) ((((-862)) . T)) ((((-862)) . T)) ((((-538)) . T) (((-566)) . T) (((-892 (-566))) . T) (((-381)) . T) (((-225)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-566)) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T)) (((|#1|) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-862)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-566)) . T)) @@ -2673,7 +2673,7 @@ ((((-862)) . T)) ((((-862)) . T)) ((((-187)) . T) (((-862)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-862)) . T)) ((((-862)) . T)) @@ -2686,7 +2686,7 @@ ((((-862)) . T)) ((((-1157)) . T)) ((((-1175) |#1|) |has| |#1| (-516 (-1175) |#1|)) ((|#1| |#1|) |has| |#1| (-310 |#1|))) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (|has| |#1| (-850)) ((((-862)) . T)) ((((-538)) |has| |#1| (-614 (-538)))) @@ -2748,8 +2748,8 @@ (-2805 (|has| |#1| (-145)) (|has| |#1| (-370))) (-2805 (|has| |#1| (-145)) (|has| |#1| (-370))) (-2805 (|has| |#1| (-145)) (|has| |#1| (-370))) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2010 (-1175)) (|:| -2818 #0#))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2050 (-1175)) (|:| -2849 #0#))) . T)) (|has| |#1| (-351)) ((((-566)) . T)) ((((-862)) . T)) @@ -2835,7 +2835,7 @@ (|has| |#2| (-1022)) ((($) . T)) (|has| |#1| (-909)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2858,12 +2858,12 @@ ((((-566)) . T) (($) . T)) ((((-566)) . T) (($) . T)) ((((-771) |#1|) . T)) -(((|#2| (-240 (-2997 |#1|) (-771))) . T)) +(((|#2| (-240 (-3020 |#1|) (-771))) . T)) (((|#1| (-533 |#3|)) . T)) ((((-409 (-566))) . T)) (-2805 (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((((-1157)) . T) (((-862)) . T)) -(((#0=(-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) #0#) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))))) +(((#0=(-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) #0#) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))))) ((((-1157)) . T)) (|has| |#1| (-909)) (|has| |#2| (-365)) @@ -2901,7 +2901,7 @@ (((|#2|) |has| |#1| (-365))) (((|#2|) |has| |#1| (-365))) ((((-566)) . T) (($) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-172))) (((|#1|) . T)) @@ -2947,9 +2947,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-2805 (|has| |#2| (-172)) (|has| |#2| (-726)) (|has| |#2| (-848)) (|has| |#2| (-1049))) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (|has| |#1| (-38 (-409 (-566)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-409 (-566)))) @@ -3081,7 +3081,7 @@ (|has| |#2| (-365)) ((((-583 |#1|)) . T) (((-409 (-566))) . T) (($) . T) (((-566)) . T)) ((((-566)) . T) (((-409 (-566))) . T) (($) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 (-52)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-566)) . T)) (((|#1|) -12 (|has| |#1| (-310 |#1|)) (|has| |#1| (-1099)))) @@ -3115,7 +3115,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-409 (-566))) . T)) -(((|#2|) |has| |#2| (-6 (-4419 "*")))) +(((|#2|) |has| |#2| (-6 (-4416 "*")))) (((|#1|) . T)) ((((-409 (-566))) |has| |#1| (-1038 (-409 (-566)))) ((|#1|) . T) (((-566)) . T)) (((|#1|) . T)) @@ -3143,7 +3143,7 @@ ((($) -2805 (|has| |#1| (-172)) (|has| |#1| (-454)) (|has| |#1| (-558)) (|has| |#1| (-909))) ((|#1|) . T) (((-409 (-566))) |has| |#1| (-38 (-409 (-566))))) ((((-862)) . T)) (((|#1|) . T)) -((((-2 (|:| -2010 (-1157)) (|:| -2818 |#1|))) . T)) +((((-2 (|:| -2050 (-1157)) (|:| -2849 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -3228,7 +3228,7 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-172))) (((|#4|) -12 (|has| |#4| (-310 |#4|)) (|has| |#4| (-1099)))) -(((|#2|) -2805 (|has| |#2| (-6 (-4419 "*"))) (|has| |#2| (-172)))) +(((|#2|) -2805 (|has| |#2| (-6 (-4416 "*"))) (|has| |#2| (-172)))) (((|#2|) . T)) (|has| |#1| (-365)) (((|#2|) . T)) @@ -3274,7 +3274,7 @@ (((|#1|) . T)) ((((-862)) . T)) (|has| |#2| (-909)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((((-538)) |has| |#2| (-614 (-538))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566))))) ((((-862)) . T)) ((((-862)) . T)) @@ -3317,7 +3317,7 @@ ((((-409 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1099)) -(((|#2| (-484 (-2997 |#1|) (-771))) . T)) +(((|#2| (-484 (-3020 |#1|) (-771))) . T)) ((((-566) |#1|) . T)) ((((-1157)) . T) (((-862)) . T)) (((|#2| |#2|) . T)) @@ -3376,7 +3376,7 @@ ((((-1175)) -12 (|has| |#3| (-900 (-1175))) (|has| |#3| (-1049)))) (((|#1|) . T)) (|has| |#1| (-233)) -(((|#2| (-240 (-2997 |#1|) (-771))) . T)) +(((|#2| (-240 (-3020 |#1|) (-771))) . T)) (((|#1| (-533 |#3|)) . T)) (|has| |#1| (-370)) (|has| |#1| (-370)) @@ -3465,7 +3465,7 @@ ((((-1213)) . T) (((-862)) . T) (((-1180)) . T)) ((((-1180)) . T)) ((((-1180)) . T)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) |has| (-2 (|:| -2010 (-1175)) (|:| -2818 (-52))) (-310 (-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))))) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) |has| (-2 (|:| -2050 (-1175)) (|:| -2849 (-52))) (-310 (-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))))) (-2805 (|has| |#2| (-454)) (|has| |#2| (-558)) (|has| |#2| (-909))) ((((-566) |#1|) . T)) ((((-566) |#1|) . T)) @@ -3672,7 +3672,7 @@ (-2805 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-131)) (|has| |#2| (-131))) (-12 (|has| |#1| (-793)) (|has| |#2| (-793)))) ((((-566)) . T)) ((((-566)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-2805 (|has| |#2| (-172)) (|has| |#2| (-726)) (|has| |#2| (-848)) (|has| |#2| (-1049))) @@ -3779,11 +3779,11 @@ ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365))) ((((-1139 |#1| |#2|)) . T)) ((((-1173 |#1| |#2| |#3|)) |has| |#1| (-365))) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((($) . T)) (|has| |#1| (-1022)) -(((|#2|) . T) (((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) ((((-862)) . T)) ((((-538)) |has| |#2| (-614 (-538))) (((-892 (-566))) |has| |#2| (-614 (-892 (-566)))) (((-892 (-381))) |has| |#2| (-614 (-892 (-381)))) (((-381)) . #0=(|has| |#2| (-1022))) (((-225)) . #0#)) ((((-295 |#3|)) . T)) @@ -3838,7 +3838,7 @@ ((((-862)) . T)) ((((-862)) . T)) (((|#1| (-533 |#2|)) . T)) -((((-2 (|:| -2010 (-1175)) (|:| -2818 (-52)))) . T)) +((((-2 (|:| -2050 (-1175)) (|:| -2849 (-52)))) . T)) ((((-566) (-129)) . T)) (((|#1| (-566)) . T)) (((|#1| (-409 (-566))) . T)) @@ -3875,7 +3875,7 @@ (((|#1| |#2|) . T)) ((((-1157) |#1|) . T)) ((((-409 |#2|)) . T)) -((((-2 (|:| -2010 |#1|) (|:| -2818 |#2|))) . T)) +((((-2 (|:| -2050 |#1|) (|:| -2849 |#2|))) . T)) (|has| |#1| (-558)) (|has| |#1| (-558)) ((($) . T) ((|#2|) . T)) @@ -3909,7 +3909,7 @@ (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1139 |#1| |#2|) #0#) |has| (-1139 |#1| |#2|) (-310 (-1139 |#1| |#2|)))) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) #0#) |has| (-2 (|:| -2010 |#1|) (|:| -2818 |#2|)) (-310 (-2 (|:| -2010 |#1|) (|:| -2818 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-310 |#2|)) (|has| |#2| (-1099))) ((#0=(-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) #0#) |has| (-2 (|:| -2050 |#1|) (|:| -2849 |#2|)) (-310 (-2 (|:| -2050 |#1|) (|:| -2849 |#2|))))) (((#0=(-116 |#1|)) |has| #0# (-310 #0#))) ((($ $) . T)) (-2805 (|has| |#1| (-850)) (|has| |#1| (-1099))) |