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 b69dce5b..f6836c38 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(205732 . 3498909343) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(205732 . 3499115857) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) ((((-578)) . T) (($) -2225 (|has| |#1| (-319)) (|has| |#1| (-376)) (|has| |#1| (-362)) (|has| |#1| (-570))) (((-421 (-578))) -2225 (|has| |#1| (-376)) (|has| |#1| (-362)) (|has| |#1| (-1069 (-421 (-578))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-578)) . T)) @@ -54,12 +54,12 @@ (((|#1|) . T) (((-578)) |has| |#1| (-1069 (-578))) (((-421 (-578))) |has| |#1| (-1069 (-421 (-578))))) (-2225 (|has| |#2| (-175)) (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938))) (-2225 (|has| |#1| (-175)) (|has| |#1| (-466)) (|has| |#1| (-570)) (|has| |#1| (-938))) -(((|#2| (-496 (-4415 |#1|) (-793))) . T)) +(((|#2| (-496 (-4416 |#1|) (-793))) . T)) ((((-1207)) -2225 (|has| (-421 |#2|) (-927 (-1207))) (|has| (-421 |#2|) (-929 (-1207))))) (((|#1| (-545 (-1207))) . T)) ((((-1189)) . T) (((-987 (-131))) . T) (((-886)) . T)) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((#0=(-894 |#1|) #0#) . T) ((#1=(-421 (-578)) #1#) . T) (($ $) . T)) (|has| |#4| (-381)) (|has| |#3| (-381)) @@ -78,7 +78,7 @@ ((((-578)) . T) (((-421 (-578))) -2225 (|has| |#2| (-38 (-421 (-578)))) (|has| |#2| (-1069 (-421 (-578))))) ((|#2|) . T) (($) -2225 (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938))) (((-888 |#1|)) . T)) (-2225 (|has| |#1| (-376)) (|has| |#1| (-570))) (-2225 (|has| |#1| (-376)) (|has| |#1| (-570))) -((((-2 (|:| -2480 |#1|) (|:| -3945 |#2|))) . T)) +((((-2 (|:| -2480 |#1|) (|:| -1647 |#2|))) . T)) ((($) . T)) ((((-886)) |has| |#1| (-632 (-886))) ((|#1|) . T)) ((((-578)) . T) (((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-1069 (-421 (-578))))) ((|#1|) . T) (($) -2225 (|has| |#1| (-466)) (|has| |#1| (-570)) (|has| |#1| (-938))) (((-1207)) . T)) @@ -134,7 +134,7 @@ ((((-886)) . T)) ((((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376))) (((-1290 |#1| |#2| |#3|)) |has| |#1| (-376)) (($) . T) ((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T) (((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376))) (($) . T)) (((|#1|) . T) (((-421 (-578))) |has| |#1| (-38 (-421 (-578)))) (($) . T)) (-2225 (|has| |#1| (-102)) (|has| |#1| (-871)) (|has| |#1| (-1131))) @@ -280,8 +280,8 @@ (((|#1|) . T)) ((((-421 (-578))) |has| |#1| (-1069 (-421 (-578)))) (((-578)) |has| |#1| (-1069 (-578))) ((|#1|) . T)) (((|#1|) . T) (((-578)) |has| |#1| (-660 (-578)))) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (|has| |#1| (-570)) ((((-578)) -2225 (-12 (|has| |#4| (-1069 (-578))) (|has| |#4| (-1131))) (|has| |#4| (-1080))) ((|#4|) |has| |#4| (-1131)) (((-421 (-578))) -12 (|has| |#4| (-1069 (-421 (-578)))) (|has| |#4| (-1131)))) ((((-578)) -2225 (-12 (|has| |#3| (-1069 (-578))) (|has| |#3| (-1131))) (|has| |#3| (-1080))) ((|#3|) |has| |#3| (-1131)) (((-421 (-578))) -12 (|has| |#3| (-1069 (-421 (-578)))) (|has| |#3| (-1131)))) @@ -314,11 +314,11 @@ ((((-550)) |has| |#2| (-633 (-550))) (((-917 (-392))) |has| |#2| (-633 (-917 (-392)))) (((-917 (-578))) |has| |#2| (-633 (-917 (-578))))) ((((-886)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -2480 |#1|) (|:| -3945 |#2|))) . T) (((-886)) . T)) +((((-2 (|:| -2480 |#1|) (|:| -1647 |#2|))) . T) (((-886)) . T)) ((((-550)) |has| |#1| (-633 (-550))) (((-917 (-392))) |has| |#1| (-633 (-917 (-392)))) (((-917 (-578))) |has| |#1| (-633 (-917 (-578))))) (((|#4|) -2225 (|has| |#4| (-175)) (|has| |#4| (-376)) (|has| |#4| (-1080)))) (((|#3|) -2225 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-1080)))) -((((-2 (|:| -2480 |#1|) (|:| -3945 |#2|))) . T)) +((((-2 (|:| -2480 |#1|) (|:| -1647 |#2|))) . T)) ((((-886)) . T)) ((((-886)) . T)) ((((-550)) . T) (((-578)) . T) (((-917 (-578))) . T) (((-392)) . T) (((-229)) . T)) @@ -327,7 +327,7 @@ ((($) . T) (((-421 (-578))) |has| |#2| (-38 (-421 (-578)))) ((|#2|) . T) (((-578)) |has| |#2| (-660 (-578)))) ((((-421 $) (-421 $)) |has| |#2| (-570)) (($ $) . T) ((|#2| |#2|) . T)) ((($ (-1207)) -2225 (|has| |#2| (-927 (-1207))) (|has| |#2| (-929 (-1207))))) -((((-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-938)) ((((-1189) (-52)) . T)) @@ -369,7 +369,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1183)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (|has| (-1284 |#1| |#2| |#3| |#4|) (-147)) (|has| (-1284 |#1| |#2| |#3| |#4|) (-149)) (|has| |#1| (-147)) @@ -388,10 +388,10 @@ (((|#2|) |has| |#2| (-1080))) ((((-886)) . T)) (|has| |#1| (-870)) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#1|) . T)) -((((-1298 (-352 (-2876) (-2876 (QUOTE X)) (-721)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) ((#0=(-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))))) +((((-1298 (-352 (-2877) (-2877 (QUOTE X)) (-721)))) . T)) +(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) ((#0=(-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))))) ((((-886)) . T)) ((((-578) |#1|) . T)) ((((-550)) -12 (|has| |#1| (-633 (-550))) (|has| |#2| (-633 (-550)))) (((-917 (-392))) -12 (|has| |#1| (-633 (-917 (-392)))) (|has| |#2| (-633 (-917 (-392))))) (((-917 (-578))) -12 (|has| |#1| (-633 (-917 (-578)))) (|has| |#2| (-633 (-917 (-578)))))) @@ -516,12 +516,12 @@ ((((-247 |#1| |#2|) |#2|) . T)) ((((-886)) . T)) (((|#3|) |has| |#3| (-1131)) (((-578)) -12 (|has| |#3| (-1069 (-578))) (|has| |#3| (-1131))) (((-421 (-578))) -12 (|has| |#3| (-1069 (-421 (-578)))) (|has| |#3| (-1131)))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T)) ((((-886)) -2225 (|has| |#1| (-632 (-886))) (|has| |#1| (-871)) (|has| |#1| (-1131)))) ((((-550)) |has| |#1| (-633 (-550)))) (((|#1|) |has| |#1| (-175))) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) (|has| |#1| (-376)) ((((-1212)) . T)) (((|#1|) . T)) @@ -531,7 +531,7 @@ (|has| |#2| (-842)) (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-870)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1| |#2| |#3| (-545 |#3|)) . T)) ((((-886)) . T)) @@ -562,7 +562,7 @@ ((((-578) |#3|) . T)) (((|#1|) . T) (((-578)) |has| |#1| (-660 (-578)))) (|has| |#2| (-1080)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (-2225 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938))) ((((-886)) . T)) ((((-1284 |#1| |#2| |#3| |#4|)) . T)) @@ -770,7 +770,7 @@ ((((-1171 |#1| |#2|)) |has| (-1171 |#1| |#2|) (-321 (-1171 |#1| |#2|)))) (((|#4| |#4|) -12 (|has| |#4| (-321 |#4|)) (|has| |#4| (-1131)))) (((|#3| |#3|) -12 (|has| |#3| (-321 |#3|)) (|has| |#3| (-1131)))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#2|) . T) (((-578)) |has| |#2| (-1069 (-578))) (((-421 (-578))) |has| |#2| (-1069 (-421 (-578))))) (|has| |#1| (-870)) (((|#1|) . T)) @@ -782,7 +782,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-2225 (|has| |#1| (-871)) (|has| |#1| (-1131))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#2|) . T)) ((((-886)) -2225 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-632 (-886))) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1131))) (((-1298 |#2|)) . T)) ((((-421 (-578))) |has| |#1| (-1069 (-421 (-578)))) ((|#1|) . T) (((-578)) . T) (($) . T)) @@ -881,9 +881,9 @@ (-2225 (|has| |#1| (-466)) (|has| |#1| (-938))) ((((-578) |#2|) . T)) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) (((|#3|) -2225 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-1080))) (($) |has| |#3| (-1080)) (((-578)) -12 (|has| |#3| (-660 (-578))) (|has| |#3| (-1080)))) ((((-578) |#1|) . T)) @@ -898,11 +898,11 @@ (|has| |#1| (-570)) (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-38 (-421 (-578)))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-886)) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (|has| |#1| (-38 (-421 (-578)))) -((((-402) (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-402) (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (|has| |#1| (-38 (-421 (-578)))) (|has| |#2| (-1183)) (-2225 (|has| |#1| (-376)) (|has| |#1| (-570))) @@ -1129,7 +1129,7 @@ (|has| |#1| (-149)) (|has| |#1| (-147)) (|has| |#1| (-149)) -(((|#2| (-247 (-4415 |#1|) (-793)) (-888 |#1|)) . T)) +(((|#2| (-247 (-4416 |#1|) (-793)) (-888 |#1|)) . T)) (((|#1| (-545 |#3|) |#3|) . T)) (|has| |#1| (-147)) (((#0=(-421 (-578)) #0#) |has| |#2| (-376)) (($ $) . T)) @@ -1148,7 +1148,7 @@ ((((-1173 |#2| |#1|)) . T) ((|#1|) . T)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (|has| |#3| (-815)) (|has| |#3| (-815)) ((((-886)) . T)) @@ -1180,13 +1180,13 @@ (((|#1|) . T)) (((|#3|) . T) (((-631 $)) . T)) (((|#1| (-421 (-578))) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T) (($) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) ((($ (-1294 |#2|)) . T) (($ (-1207)) -12 (|has| |#1| (-15 * (|#1| (-421 (-578)) |#1|))) (|has| |#1| (-927 (-1207))))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-578)) -2225 (-12 (|has| |#2| (-1069 (-578))) (|has| |#2| (-1131))) (|has| |#2| (-1080))) ((|#2|) |has| |#2| (-1131)) (((-421 (-578))) -12 (|has| |#2| (-1069 (-421 (-578)))) (|has| |#2| (-1131)))) (((|#1|) . T) (((-421 (-578))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1195,8 +1195,8 @@ ((((-886)) . T)) ((((-886)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) -(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) (((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) +(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) (((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))))) ((((-886)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1213,7 +1213,7 @@ (|has| (-1125 |#1|) (-1131)) (((|#2| |#2|) -2225 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-1080)))) (((|#2|) -2225 (|has| |#2| (-175)) (|has| |#2| (-376)))) -((((-578) (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T) ((|#1| |#2|) . T)) +((((-578) (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -2225 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-1080)))) ((((-578)) . T)) ((((-1212)) . T)) @@ -1260,7 +1260,7 @@ (-2225 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1131))) (-12 (|has| |#3| (-240)) (|has| |#3| (-1080))) (|has| |#2| (-1183)) -(((#0=(-52)) . T) (((-2 (|:| -2338 (-1207)) (|:| -2078 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2338 (-1207)) (|:| -2079 #0#))) . T)) (((|#1| |#2|) . T)) (((|#1| (-657 |#2|)) . T)) (|has| |#3| (-1080)) @@ -1298,7 +1298,7 @@ (((|#4|) . T)) (((|#3|) . T) ((|#2|) . T) (((-578)) . T) ((|#4|) -2225 (|has| |#4| (-175)) (|has| |#4| (-376)) (|has| |#4| (-748)) (|has| |#4| (-1080))) (($) |has| |#4| (-1080))) (((|#2|) . T) (((-578)) . T) ((|#3|) -2225 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-748)) (|has| |#3| (-1080))) (($) |has| |#3| (-1080))) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#4|) . T) (((-886)) . T)) (|has| |#1| (-570)) (((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) @@ -1361,7 +1361,7 @@ (-12 (|has| |#1| (-815)) (|has| |#2| (-815))) (|has| |#2| (-1080)) ((($) . T) (((-578)) . T) ((|#2|) . T)) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#2|) . T) (($) . T)) (|has| |#1| (-1233)) (((#0=(-578) #0#) . T) ((#1=(-421 (-578)) #1#) . T) (($ $) . T)) @@ -1393,7 +1393,7 @@ (((|#1|) . T)) (-2225 (|has| |#1| (-175)) (|has| |#1| (-570))) ((($) . T)) -(((#0=(-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) #0#) |has| (-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))))) +(((#0=(-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) #0#) |has| (-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))))) ((((-578) |#3|) . T)) (((|#2|) . T)) ((($) . T)) @@ -1412,10 +1412,10 @@ ((((-578)) |has| #0=(-421 |#2|) (-660 (-578))) ((#0#) . T)) ((($) . T) (((-578)) . T)) ((((-578) (-146)) . T)) -((((-578) (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T) ((|#1| |#2|) . T)) +((((-578) (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T) ((|#1| |#2|) . T)) ((((-421 (-578))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-886)) . T)) ((((-939 |#1|)) . T)) (|has| |#1| (-376)) @@ -1443,7 +1443,7 @@ ((((-550)) . T)) ((((-886)) . T)) ((($) . T)) -((((-578) (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T) (((-1265 (-578)) $) . T) ((|#1| |#2|) . T)) +((((-578) (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T) (((-1265 (-578)) $) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-175))) @@ -1461,7 +1461,7 @@ ((((-550)) |has| |#1| (-633 (-550))) (((-917 (-392))) |has| |#1| (-633 (-917 (-392)))) (((-917 (-578))) |has| |#1| (-633 (-917 (-578))))) ((((-886)) . T)) ((((-894 |#1|)) . T) (($) . T) (((-421 (-578))) . T)) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-520)) . T)) ((((-520)) . T)) ((((-1207)) -2225 (-12 (|has| |#4| (-927 (-1207))) (|has| |#4| (-1080))) (-12 (|has| |#4| (-929 (-1207))) (|has| |#4| (-1080))))) @@ -1504,7 +1504,7 @@ (((|#1|) . T) (((-421 (-578))) |has| |#1| (-38 (-421 (-578)))) (((-578)) . T) (($) . T)) ((((-1207)) |has| (-421 |#2|) (-927 (-1207)))) (((|#2|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) ((($) . T)) ((((-421 (-578))) |has| |#2| (-38 (-421 (-578)))) ((|#2|) |has| |#2| (-175)) (($) -2225 (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938)))) ((((-421 (-578))) |has| |#2| (-38 (-421 (-578)))) ((|#2|) . T) (($) -2225 (|has| |#2| (-175)) (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938)))) @@ -1523,7 +1523,7 @@ (((|#2|) . T) (((-578)) . T)) ((((-886)) . T)) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T) ((|#2|) . T)) ((((-886)) . T)) ((((-886)) . T)) ((((-1189) (-1207) (-578) (-229) (-886)) . T)) @@ -1613,7 +1613,7 @@ ((((-1030 |#1|)) . T) ((|#1|) . T)) ((((-1207)) -2225 (|has| |#1| (-927 (-1207))) (|has| |#1| (-929 (-1207)))) (((-840 (-1207))) . T)) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-421 (-578))) . T) (((-421 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1203 |#1|)) . T)) ((((-578)) . T) (($) . T) (((-421 (-578))) . T)) @@ -1622,7 +1622,7 @@ (((|#1|) . T) (((-578)) . T) (($) . T)) (((|#2|) . T)) ((((-578)) . T) (($) . T) (((-421 (-578))) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) ((((-886)) -2225 (|has| |#1| (-632 (-886))) (|has| |#1| (-1131)))) ((((-578) |#2|) . T)) (((|#1|) . T) (((-421 (-578))) . T) (((-578)) . T) (($) . T)) @@ -1636,7 +1636,7 @@ (((|#3|) -12 (|has| |#3| (-321 |#3|)) (|has| |#3| (-1131)))) (-2225 (|has| |#1| (-15 * (|#1| (-578) |#1|))) (-12 (|has| |#1| (-376)) (|has| |#2| (-240))) (-12 (|has| |#1| (-376)) (|has| |#2| (-239)))) (|has| |#1| (-38 (-421 (-578)))) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#2| |#2|) . T)) (|has| |#1| (-38 (-421 (-578)))) (|has| |#2| (-376)) @@ -1688,7 +1688,7 @@ (((|#1| |#2|) . T)) (-2225 (|has| |#2| (-240)) (|has| |#2| (-239))) ((((-578) (-146)) . T) (((-1265 (-578)) $) . T)) -(((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131)))) +(((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131)))) ((($) -2225 (|has| |#1| (-466)) (|has| |#1| (-570)) (|has| |#1| (-938))) ((|#1|) |has| |#1| (-175)) (((-421 (-578))) |has| |#1| (-38 (-421 (-578))))) (|has| |#1| (-871)) (((|#2| (-793) (-1113)) . T)) @@ -1749,7 +1749,7 @@ ((($ (-1207)) . T)) ((($) |has| |#1| (-570)) ((|#1|) |has| |#1| (-175)) (((-421 (-578))) |has| |#1| (-38 (-421 (-578))))) ((((-886)) -2225 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-632 (-886))) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1131))) (((-1298 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2338 (-1189)) (|:| -2078 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2338 (-1189)) (|:| -2079 #0#))) . T)) (((|#1|) . T)) ((((-886)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131)))) @@ -1780,7 +1780,7 @@ ((((-886)) . T)) ((((-886)) . T)) (-2225 (|has| |#1| (-102)) (|has| |#1| (-1131))) -(((|#2| (-496 (-4415 |#1|) (-793)) (-888 |#1|)) . T)) +(((|#2| (-496 (-4416 |#1|) (-793)) (-888 |#1|)) . T)) ((((-421 (-578))) . #0=(|has| |#2| (-376))) (($) . #0#)) (((|#1| (-545 (-1207)) (-1207)) . T)) (((|#1|) . T)) @@ -1801,13 +1801,13 @@ (((|#2|) |has| |#2| (-175))) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-1207) (-52)) . T)) ((((-421 (-578)) |#1|) . T) (($ $) . T)) (((|#1| (-578)) . T)) @@ -1863,11 +1863,11 @@ (-2225 (|has| |#1| (-376)) (|has| |#1| (-362))) (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-38 (-421 (-578)))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-1207)) |has| |#1| (-927 (-1207))) (((-1113)) . T)) (((|#1|) . T)) (|has| |#1| (-870)) -(((#0=(-2 (|:| -2338 (-1189)) (|:| -2078 (-52))) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))))) +(((#0=(-2 (|:| -2338 (-1189)) (|:| -2079 (-52))) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) (|has| |#1| (-1131)) ((((-886)) . T) (((-1212)) . T)) @@ -1940,7 +1940,7 @@ ((($) |has| |#1| (-381))) (((|#1| |#2|) . T)) (-2225 (|has| |#2| (-466)) (|has| |#2| (-938))) -(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) ((#0=(-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) ((#0=(-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) #0#) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))))) (-2225 (|has| |#1| (-466)) (|has| |#1| (-938))) (((|#1|) . T)) (((|#1|) . T) (($) . T)) @@ -1966,7 +1966,7 @@ ((((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376))) (($) -2225 (|has| |#1| (-376)) (|has| |#1| (-570))) (((-1205 |#1| |#2| |#3|)) |has| |#1| (-376)) ((|#1|) |has| |#1| (-175))) (((|#1|) |has| |#1| (-175)) (((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376))) (($) -2225 (|has| |#1| (-376)) (|has| |#1| (-570)))) ((($) |has| |#1| (-570)) ((|#1|) |has| |#1| (-175)) (((-421 (-578))) |has| |#1| (-38 (-421 (-578))))) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((((-578)) |has| #0=(-421 |#2|) (-660 (-578))) ((#0#) . T) (((-421 (-578))) . T) (($) . T)) ((((-694 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -2048,7 +2048,7 @@ ((((-886)) . T)) ((((-886)) . T)) ((($ $) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((($) -2225 (|has| |#1| (-15 * (|#1| (-578) |#1|))) (-12 (|has| |#1| (-376)) (|has| |#2| (-240))) (-12 (|has| |#1| (-376)) (|has| |#2| (-239))))) ((($) |has| |#1| (-15 * (|#1| (-421 (-578)) |#1|)))) ((((-1002)) . T)) @@ -2081,7 +2081,7 @@ (((|#1| (-1262 |#1| |#2| |#3|)) . T)) ((((-886)) . T)) (|has| |#1| (-1131)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1| (-793)) . T)) ((((-1189) |#1|) . T)) (((|#1|) . T)) @@ -2131,7 +2131,7 @@ ((($) -2225 (|has| |#1| (-175)) (|has| |#1| (-376)) (|has| |#1| (-570))) (((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376))) (((-1205 |#1| |#2| |#3|)) |has| |#1| (-376)) ((|#1|) . T)) (((|#1|) . T) (($) -2225 (|has| |#1| (-175)) (|has| |#1| (-376)) (|has| |#1| (-570))) (((-421 (-578))) -2225 (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-376)))) ((($) -2225 (|has| |#1| (-175)) (|has| |#1| (-570))) ((|#1|) . T) (((-421 (-578))) |has| |#1| (-38 (-421 (-578))))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#1|) |has| |#1| (-175))) ((((-886)) . T)) ((($) |has| |#1| (-570)) ((|#1|) |has| |#1| (-175)) (((-421 (-578))) |has| |#1| (-38 (-421 (-578))))) @@ -2160,7 +2160,7 @@ (|has| |#1| (-870)) (((|#1| (-578) (-1113)) . T)) (-2225 (|has| |#1| (-927 (-1207))) (|has| |#1| (-1080))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1| (-421 (-578)) (-1113)) . T)) (((|#1| (-793) (-1113)) . T)) (|has| |#1| (-871)) @@ -2179,11 +2179,11 @@ (-2225 (|has| |#1| (-102)) (|has| |#1| (-1131))) ((((-578)) -12 (|has| |#1| (-376)) (|has| |#2| (-660 (-578)))) ((|#2|) |has| |#1| (-376))) (-2225 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1131))) -((((-711 (-352 (-2876) (-2876 (QUOTE X) (QUOTE HESS)) (-721)))) . T)) +((((-711 (-352 (-2877) (-2877 (QUOTE X) (QUOTE HESS)) (-721)))) . T)) (((|#2|) |has| |#2| (-175))) (((|#1|) |has| |#1| (-175))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) ((((-886)) . T)) ((((-886)) . T)) ((((-886)) . T)) @@ -2198,11 +2198,11 @@ ((($) . T) ((|#1|) . T) (((-421 (-578))) |has| |#1| (-376)) (((-578)) |has| |#1| (-660 (-578)))) (|has| |#1| (-871)) (((|#1|) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T) (((-578)) . T)) (((|#2|) . T)) ((((-578)) . T) ((|#3|) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) |has| (-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))))) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) |has| (-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))))) (-2225 (|has| |#1| (-466)) (|has| |#1| (-938))) (((|#2|) . T) (((-578)) |has| |#2| (-660 (-578)))) ((((-886)) . T)) @@ -2273,7 +2273,7 @@ (((|#2|) |has| |#2| (-1080))) (|has| |#1| (-376)) ((($) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (((|#1|) |has| |#1| (-175))) ((($ (-888 |#1|)) . T)) (((|#1| |#1|) . T)) @@ -2327,7 +2327,7 @@ (((|#1| |#2|) . T)) ((($) . T) (((-578)) . T) (((-421 (-578))) . T)) ((((-578)) . T) (($) . T) (((-421 (-578))) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))) . T)) (((|#1|) . T) (((-421 (-578))) . T) (((-578)) . T) (($) . T)) (((|#1|) . T) (((-421 (-578))) . T) (((-578)) . T) (($) . T)) (((|#1|) . T) (((-421 (-578))) . T) (((-578)) . T) (($) . T)) @@ -2342,7 +2342,7 @@ (((|#2|) . T)) ((($) . T) (((-578)) . T) (((-421 (-578))) -2225 (|has| |#1| (-376)) (|has| |#1| (-362))) ((|#1|) . T)) ((((-578) |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) ((((-392)) . T)) ((((-721)) . T)) ((((-421 (-578))) . #0=(|has| |#2| (-376))) (($) . #0#)) @@ -2362,7 +2362,7 @@ ((((-1207)) |has| |#2| (-927 (-1207)))) (|has| |#1| (-871)) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (|has| |#1| (-813)) ((((-421 (-578))) . T) (($) . T)) (|has| |#1| (-487)) @@ -2393,12 +2393,12 @@ (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-38 (-421 (-578)))) (|has| |#1| (-871)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-578)) . T)) (|has| |#1| (-149)) (|has| |#1| (-147)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)))) ((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131)))) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)))) ((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131)))) (((|#2|) . T)) (|has| |#1| (-15 * (|#1| (-578) |#1|))) (((|#3|) . T)) @@ -2423,7 +2423,7 @@ (((|#1|) |has| |#1| (-376))) (((|#1|) |has| |#1| (-376))) ((((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((($ $) . T) (((-631 $) $) . T)) (-2225 (|has| |#1| (-376)) (|has| |#1| (-570))) ((($) . T) (((-1284 |#1| |#2| |#3| |#4|)) . T) (((-421 (-578))) . T)) @@ -2506,7 +2506,7 @@ (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -2225 (|has| |#1| (-302)) (|has| |#1| (-376))) ((#0=(-421 (-578)) #0#) |has| |#1| (-376))) ((((-981 |#1|)) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((($) . T)) ((((-578) |#1|) . T)) ((((-1207)) |has| (-421 |#2|) (-927 (-1207)))) @@ -2553,7 +2553,7 @@ (((|#1|) . T) (((-578)) |has| |#1| (-660 (-578)))) ((($) -2225 (|has| |#1| (-376)) (|has| |#1| (-362))) (((-421 (-578))) -2225 (|has| |#1| (-376)) (|has| |#1| (-362))) ((|#1|) . T)) ((((-578)) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))))) +((((-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))))) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) (|has| |#1| (-870)) ((((-578) $) . T) (((-666 (-578)) $) . T)) @@ -2609,10 +2609,10 @@ ((((-550)) |has| |#4| (-633 (-550)))) (-2225 (|has| |#1| (-102)) (|has| |#1| (-1131))) ((((-886)) . T) (((-666 |#4|)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-376)) -(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) (((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) |has| (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))))) +(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131))) (((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) |has| (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|)) (-321 (-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))))) (-2225 (-12 (|has| |#1| (-376)) (|has| |#2| (-842))) (-12 (|has| |#1| (-376)) (|has| |#2| (-871)))) (((|#1|) . T)) (((|#1|) . T)) @@ -2657,7 +2657,7 @@ ((((-886)) . T)) ((((-886)) . T)) ((((-550)) |has| |#1| (-633 (-550)))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-578)) . T) (($) . T) (((-421 (-578))) . T)) ((((-1207) |#1|) |has| |#1| (-528 (-1207) |#1|)) ((|#1| |#1|) |has| |#1| (-321 |#1|))) (((|#1|) -2225 (|has| |#1| (-175)) (|has| |#1| (-376)))) @@ -2699,7 +2699,7 @@ (|has| |#1| (-570)) (((|#2|) . T)) ((((-578)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T)) (-2225 (|has| |#1| (-147)) (|has| |#1| (-149)) (|has| |#1| (-175)) (|has| |#1| (-570)) (|has| |#1| (-1080))) ((((-595 |#1|)) . T)) @@ -2849,16 +2849,16 @@ (|has| |#1| (-938)) ((($) -2225 (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) (-12 (|has| |#2| (-239)) (|has| |#2| (-1080))))) (((|#2|) |has| |#2| (-175))) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-1290 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-886)) . T)) ((((-886)) . T)) ((((-550)) . T) (((-578)) . T) (((-917 (-578))) . T) (((-392)) . T) (((-229)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-578)) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))) . T)) (((|#1|) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((((-886)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-578)) . T)) @@ -2880,7 +2880,7 @@ ((((-886)) . T)) ((((-886)) . T)) ((((-190)) . T) (((-886)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-886)) . T)) ((((-886)) . T)) @@ -2897,7 +2897,7 @@ (|has| |#1| (-871)) ((((-886)) . T)) ((((-550)) |has| |#1| (-633 (-550)))) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) ((($) -2225 (-12 (|has| (-1205 |#1| |#2| |#3|) (-240)) (|has| |#1| (-376))) (-12 (|has| (-1205 |#1| |#2| |#3|) (-239)) (|has| |#1| (-376))) (|has| |#1| (-15 * (|#1| (-578) |#1|))))) ((((-886)) . T)) (((|#2|) |has| |#2| (-376))) @@ -2964,10 +2964,10 @@ (-2225 (|has| |#1| (-147)) (|has| |#1| (-381))) (-2225 (|has| |#1| (-147)) (|has| |#1| (-381))) (-2225 (|has| |#1| (-147)) (|has| |#1| (-381))) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((((-578) |#3|) . T)) (((|#1|) . T)) -(((#0=(-52)) . T) (((-2 (|:| -2338 (-1207)) (|:| -2078 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -2338 (-1207)) (|:| -2079 #0#))) . T)) (|has| |#1| (-362)) ((((-578)) . T)) ((((-886)) . T)) @@ -3057,7 +3057,7 @@ (|has| |#2| (-1053)) ((($) . T)) (|has| |#1| (-938)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#4|) . T)) ((($) . T)) (((|#2|) . T)) @@ -3082,12 +3082,12 @@ ((((-578)) . T) (($) . T)) ((((-578)) . T) (($) . T)) ((((-793) |#1|) . T)) -(((|#2| (-247 (-4415 |#1|) (-793))) . T)) +(((|#2| (-247 (-4416 |#1|) (-793))) . T)) (((|#1| (-545 |#3|)) . T)) ((((-421 (-578))) . T)) (-2225 (|has| |#1| (-466)) (|has| |#1| (-570)) (|has| |#1| (-938))) ((((-1189)) . T) (((-886)) . T)) -(((#0=(-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) #0#) |has| (-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))))) +(((#0=(-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) #0#) |has| (-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))))) ((((-1189)) . T)) (|has| |#1| (-938)) (|has| |#2| (-376)) @@ -3132,7 +3132,7 @@ (-2225 (|has| |#4| (-815)) (|has| |#4| (-871))) (-2225 (|has| |#3| (-815)) (|has| |#3| (-871))) ((((-578)) . T) (($) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-175))) @@ -3185,9 +3185,9 @@ (((|#2|) . T)) (((|#2|) . T)) (|has| |#2| (-1080)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (|has| |#1| (-38 (-421 (-578)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-421 (-578)))) @@ -3335,7 +3335,7 @@ ((($) -2225 (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) (-12 (|has| |#2| (-239)) (|has| |#2| (-1080))))) ((((-595 |#1|)) . T) (((-421 (-578))) . T) (($) . T) (((-578)) . T)) ((((-578)) . T) (((-421 (-578))) . T) (($) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 (-52)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-578)) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1131)))) @@ -3399,7 +3399,7 @@ ((((-886)) . T)) (((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -2338 (-1189)) (|:| -2078 |#1|))) . T)) +((((-2 (|:| -2338 (-1189)) (|:| -2079 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -3542,7 +3542,7 @@ (((|#1|) . T)) ((((-886)) . T)) (|has| |#2| (-938)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((((-550)) |has| |#2| (-633 (-550))) (((-917 (-392))) |has| |#2| (-633 (-917 (-392)))) (((-917 (-578))) |has| |#2| (-633 (-917 (-578))))) ((((-886)) . T)) ((((-886)) . T)) @@ -3592,7 +3592,7 @@ (((|#1|) . T)) ((((-886)) . T)) (-2225 (|has| |#1| (-102)) (|has| |#1| (-1131))) -(((|#2| (-496 (-4415 |#1|) (-793))) . T)) +(((|#2| (-496 (-4416 |#1|) (-793))) . T)) ((((-578) |#1|) . T)) ((((-1189)) . T) (((-886)) . T)) (((|#2| |#2|) . T)) @@ -3657,7 +3657,7 @@ ((((-1207)) -12 (|has| |#3| (-927 (-1207))) (|has| |#3| (-1080)))) (((|#1|) . T)) (|has| |#1| (-240)) -(((|#2| (-247 (-4415 |#1|) (-793))) . T)) +(((|#2| (-247 (-4416 |#1|) (-793))) . T)) (((|#1| (-545 |#3|)) . T)) (|has| |#1| (-381)) (|has| |#1| (-381)) @@ -3752,7 +3752,7 @@ ((((-1212)) . T)) ((((-886)) . T) (((-1212)) . T)) ((((-1212)) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) |has| (-2 (|:| -2338 (-1207)) (|:| -2078 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))))) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) |has| (-2 (|:| -2338 (-1207)) (|:| -2079 (-52))) (-321 (-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))))) (-2225 (|has| |#2| (-466)) (|has| |#2| (-570)) (|has| |#2| (-938))) ((((-578) |#1|) . T)) ((((-578) |#1|) . T)) @@ -3972,7 +3972,7 @@ ((((-886)) . T)) ((((-578)) . T)) ((((-578)) . T)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) ((((-1207)) -12 (|has| |#2| (-927 (-1207))) (|has| |#2| (-1080)))) @@ -4083,11 +4083,11 @@ ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-1171 |#1| |#2|)) . T)) ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((($) . T)) (|has| |#1| (-1053)) -(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) ((($) . T)) ((((-886)) . T)) ((((-550)) |has| |#2| (-633 (-550))) (((-917 (-578))) |has| |#2| (-633 (-917 (-578)))) (((-917 (-392))) |has| |#2| (-633 (-917 (-392)))) (((-392)) . #0=(|has| |#2| (-1053))) (((-229)) . #0#)) @@ -4143,7 +4143,7 @@ ((((-886)) . T)) ((((-886)) . T)) (((|#1| (-545 |#2|)) . T)) -((((-2 (|:| -2338 (-1207)) (|:| -2078 (-52)))) . T)) +((((-2 (|:| -2338 (-1207)) (|:| -2079 (-52)))) . T)) ((((-578) (-131)) . T)) (((|#1| (-578)) . T)) (((|#1| (-421 (-578))) . T)) @@ -4182,7 +4182,7 @@ ((((-421 |#2|)) . T)) (|has| |#1| (-570)) (|has| |#1| (-570)) -((((-2 (|:| -2338 |#1|) (|:| -2078 |#2|))) . T)) +((((-2 (|:| -2338 |#1|) (|:| -2079 |#2|))) . T)) (((|#2| (-793)) . T)) ((($) . T) ((|#2|) . T)) ((($) . T) (((-421 (-578))) . T)) @@ -4216,7 +4216,7 @@ (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1171 |#1| |#2|) #0#) |has| (-1171 |#1| |#2|) (-321 (-1171 |#1| |#2|)))) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2078 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2078 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1131))) ((#0=(-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) #0#) |has| (-2 (|:| -2338 |#1|) (|:| -2079 |#2|)) (-321 (-2 (|:| -2338 |#1|) (|:| -2079 |#2|))))) (-2225 (|has| |#1| (-240)) (|has| |#1| (-239))) (((#0=(-118 |#1|)) |has| #0# (-321 #0#))) ((($ $) . T)) |