diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 202 |
1 files changed, 101 insertions, 101 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index f4b38e55..a1e8f1d0 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(205732 . 3507556011) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(205732 . 3507561101) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) ((((-560)) . T) (($) -2222 (|has| |#1| (-319)) (|has| |#1| (-376)) (|has| |#1| (-363)) (|has| |#1| (-571))) (((-421 (-560))) -2222 (|has| |#1| (-376)) (|has| |#1| (-363)) (|has| |#1| (-1069 (-421 (-560))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-560)) . T)) @@ -59,7 +59,7 @@ (((|#1| (-545 (-1207))) . T)) ((((-1189)) . T) (((-987 (-130))) . T) (((-887)) . T)) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((#0=(-893 |#1|) #0#) . T) ((#1=(-421 (-560)) #1#) . T) (($ $) . T)) (|has| |#4| (-381)) (|has| |#3| (-381)) @@ -78,7 +78,7 @@ ((((-560)) . T) (((-421 (-560))) -2222 (|has| |#2| (-38 (-421 (-560)))) (|has| |#2| (-1069 (-421 (-560))))) ((|#2|) . T) (($) -2222 (|has| |#2| (-466)) (|has| |#2| (-571)) (|has| |#2| (-939))) (((-888 |#1|)) . T)) (-2222 (|has| |#1| (-376)) (|has| |#1| (-571))) (-2222 (|has| |#1| (-376)) (|has| |#1| (-571))) -((((-2 (|:| -3973 |#1|) (|:| -4353 |#2|))) . T)) +((((-2 (|:| -3972 |#1|) (|:| -1736 |#2|))) . T)) ((($) . T)) ((((-887)) |has| |#1| (-632 (-887))) ((|#1|) . T)) ((((-560)) . T) (((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-1069 (-421 (-560))))) ((|#1|) . T) (($) -2222 (|has| |#1| (-466)) (|has| |#1| (-571)) (|has| |#1| (-939))) (((-1207)) . T)) @@ -134,7 +134,7 @@ ((((-887)) . T)) ((((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376))) (((-1287 |#1| |#2| |#3|)) |has| |#1| (-376)) (($) . T) ((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T) (((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376))) (($) . T)) (((|#1|) . T) (((-421 (-560))) |has| |#1| (-38 (-421 (-560)))) (($) . T)) (-2222 (|has| |#1| (-102)) (|has| |#1| (-871)) (|has| |#1| (-1132))) @@ -280,8 +280,8 @@ (((|#1|) . T)) ((((-421 (-560))) |has| |#1| (-1069 (-421 (-560)))) (((-560)) |has| |#1| (-1069 (-560))) ((|#1|) . T)) (((|#1|) . T) (((-560)) |has| |#1| (-660 (-560)))) -(((|#2|) . T) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) (|has| |#1| (-571)) ((((-560)) -2222 (-12 (|has| |#4| (-1069 (-560))) (|has| |#4| (-1132))) (|has| |#4| (-1080))) ((|#4|) |has| |#4| (-1132)) (((-421 (-560))) -12 (|has| |#4| (-1069 (-421 (-560)))) (|has| |#4| (-1132)))) ((((-560)) -2222 (-12 (|has| |#3| (-1069 (-560))) (|has| |#3| (-1132))) (|has| |#3| (-1080))) ((|#3|) |has| |#3| (-1132)) (((-421 (-560))) -12 (|has| |#3| (-1069 (-421 (-560)))) (|has| |#3| (-1132)))) @@ -314,11 +314,11 @@ ((((-549)) |has| |#2| (-633 (-549))) (((-915 (-391))) |has| |#2| (-633 (-915 (-391)))) (((-915 (-560))) |has| |#2| (-633 (-915 (-560))))) ((((-887)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -3973 |#1|) (|:| -4353 |#2|))) . T) (((-887)) . T)) +((((-2 (|:| -3972 |#1|) (|:| -1736 |#2|))) . T) (((-887)) . T)) ((((-549)) |has| |#1| (-633 (-549))) (((-915 (-391))) |has| |#1| (-633 (-915 (-391)))) (((-915 (-560))) |has| |#1| (-633 (-915 (-560))))) (((|#4|) -2222 (|has| |#4| (-175)) (|has| |#4| (-376)) (|has| |#4| (-1080)))) (((|#3|) -2222 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-1080)))) -((((-2 (|:| -3973 |#1|) (|:| -4353 |#2|))) . T)) +((((-2 (|:| -3972 |#1|) (|:| -1736 |#2|))) . T)) ((((-887)) . T)) ((((-887)) . T)) ((((-549)) . T) (((-560)) . T) (((-915 (-560))) . T) (((-391)) . T) (((-229)) . T)) @@ -327,7 +327,7 @@ ((($) . T) (((-421 (-560))) |has| |#2| (-38 (-421 (-560)))) ((|#2|) . T) (((-560)) |has| |#2| (-660 (-560)))) ((((-421 $) (-421 $)) |has| |#2| (-571)) (($ $) . T) ((|#2| |#2|) . T)) ((($ (-1207)) -2222 (|has| |#2| (-927 (-1207))) (|has| |#2| (-929 (-1207))))) -((((-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-939)) ((((-1189) (-51)) . T)) @@ -369,7 +369,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1182)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#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))) ((((-887)) . T)) (|has| |#1| (-870)) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#1|) . T)) -((((-1297 (-352 (-2450) (-2450 (QUOTE X)) (-721)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) ((#0=(-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) #0#) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))))) +((((-1297 (-352 (-2451) (-2451 (QUOTE X)) (-721)))) . T)) +(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) ((#0=(-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) #0#) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))))) ((((-887)) . T)) ((((-560) |#1|) . T)) ((((-549)) -12 (|has| |#1| (-633 (-549))) (|has| |#2| (-633 (-549)))) (((-915 (-391))) -12 (|has| |#1| (-633 (-915 (-391)))) (|has| |#2| (-633 (-915 (-391))))) (((-915 (-560))) -12 (|has| |#1| (-633 (-915 (-560)))) (|has| |#2| (-633 (-915 (-560)))))) @@ -516,12 +516,12 @@ ((((-246 |#1| |#2|) |#2|) . T)) ((((-887)) . T)) (((|#3|) |has| |#3| (-1132)) (((-560)) -12 (|has| |#3| (-1069 (-560))) (|has| |#3| (-1132))) (((-421 (-560))) -12 (|has| |#3| (-1069 (-421 (-560)))) (|has| |#3| (-1132)))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T)) ((((-887)) -2222 (|has| |#1| (-632 (-887))) (|has| |#1| (-871)) (|has| |#1| (-1132)))) ((((-549)) |has| |#1| (-633 (-549)))) (((|#1|) |has| |#1| (-175))) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) (|has| |#1| (-376)) ((((-1212)) . T)) (((|#1|) . T)) @@ -531,7 +531,7 @@ (|has| |#2| (-842)) (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-870)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1| |#2| |#3| (-545 |#3|)) . T)) ((((-887)) . T)) @@ -562,7 +562,7 @@ ((((-560) |#3|) . T)) (((|#1|) . T) (((-560)) |has| |#1| (-660 (-560)))) (|has| |#2| (-1080)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (-2222 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-466)) (|has| |#2| (-571)) (|has| |#2| (-939))) ((((-887)) . 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| (-1132)))) (((|#3| |#3|) -12 (|has| |#3| (-321 |#3|)) (|has| |#3| (-1132)))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#2|) . T) (((-560)) |has| |#2| (-1069 (-560))) (((-421 (-560))) |has| |#2| (-1069 (-421 (-560))))) (|has| |#1| (-870)) (((|#1|) . T)) @@ -782,7 +782,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-2222 (|has| |#1| (-871)) (|has| |#1| (-1132))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#2|) . T)) ((((-887)) -2222 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-632 (-887))) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1132))) (((-1297 |#2|)) . T)) ((((-421 (-560))) |has| |#1| (-1069 (-421 (-560)))) ((|#1|) . T) (((-560)) . T) (($) . T)) @@ -881,9 +881,9 @@ (-2222 (|has| |#1| (-466)) (|has| |#1| (-939))) ((((-560) |#2|) . T)) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) (((|#3|) -2222 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-1080))) (($) |has| |#3| (-1080)) (((-560)) -12 (|has| |#3| (-660 (-560))) (|has| |#3| (-1080)))) ((((-560) |#1|) . T)) @@ -898,11 +898,11 @@ (|has| |#1| (-571)) (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-38 (-421 (-560)))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-887)) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) (|has| |#1| (-38 (-421 (-560)))) -((((-402) (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-402) (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) (|has| |#1| (-38 (-421 (-560)))) (|has| |#2| (-1182)) (-2222 (|has| |#1| (-376)) (|has| |#1| (-571))) @@ -1148,7 +1148,7 @@ ((((-1173 |#2| |#1|)) . T) ((|#1|) . T)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) -(((|#2|) . T) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (|has| |#3| (-815)) (|has| |#3| (-815)) ((((-887)) . T)) @@ -1180,13 +1180,13 @@ (((|#1|) . T)) (((|#3|) . T) (((-630 $)) . T)) (((|#1| (-421 (-560))) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T) (($) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) ((($ (-1294 |#2|)) . T) (($ (-1207)) -12 (|has| |#1| (-15 * (|#1| (-421 (-560)) |#1|))) (|has| |#1| (-927 (-1207))))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-560)) -2222 (-12 (|has| |#2| (-1069 (-560))) (|has| |#2| (-1132))) (|has| |#2| (-1080))) ((|#2|) |has| |#2| (-1132)) (((-421 (-560))) -12 (|has| |#2| (-1069 (-421 (-560)))) (|has| |#2| (-1132)))) (((|#1|) . T) (((-421 (-560))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1195,8 +1195,8 @@ ((((-887)) . T)) ((((-887)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) -(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) (((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) +(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) (((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))))) ((((-887)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1213,7 +1213,7 @@ (|has| (-1120 |#1|) (-1132)) (((|#2| |#2|) -2222 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-1080)))) (((|#2|) -2222 (|has| |#2| (-175)) (|has| |#2| (-376)))) -((((-560) (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T) ((|#1| |#2|) . T)) +((((-560) (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -2222 (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-1080)))) ((((-560)) . T)) ((((-1212)) . T)) @@ -1260,7 +1260,7 @@ (-2222 (|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| (-1132))) (-12 (|has| |#3| (-240)) (|has| |#3| (-1080))) (|has| |#2| (-1182)) -(((#0=(-51)) . T) (((-2 (|:| -3819 (-1207)) (|:| -2309 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3820 (-1207)) (|:| -2308 #0#))) . T)) (((|#1| |#2|) . T)) (((|#1| (-657 |#2|)) . T)) (|has| |#3| (-1080)) @@ -1298,7 +1298,7 @@ (((|#4|) . T)) (((|#3|) . T) ((|#2|) . T) (((-560)) . T) ((|#4|) -2222 (|has| |#4| (-175)) (|has| |#4| (-376)) (|has| |#4| (-748)) (|has| |#4| (-1080))) (($) |has| |#4| (-1080))) (((|#2|) . T) (((-560)) . T) ((|#3|) -2222 (|has| |#3| (-175)) (|has| |#3| (-376)) (|has| |#3| (-748)) (|has| |#3| (-1080))) (($) |has| |#3| (-1080))) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#4|) . T) (((-887)) . T)) (|has| |#1| (-571)) (((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) @@ -1361,7 +1361,7 @@ (-12 (|has| |#1| (-815)) (|has| |#2| (-815))) (|has| |#2| (-1080)) ((($) . T) (((-560)) . T) ((|#2|) . T)) -(((|#2|) . T) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#2|) . T) (($) . T)) (|has| |#1| (-1233)) (((#0=(-560) #0#) . T) ((#1=(-421 (-560)) #1#) . T) (($ $) . T)) @@ -1393,7 +1393,7 @@ (((|#1|) . T)) (-2222 (|has| |#1| (-175)) (|has| |#1| (-571))) ((($) . T)) -(((#0=(-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) #0#) |has| (-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))))) +(((#0=(-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) #0#) |has| (-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))))) ((((-560) |#3|) . T)) (((|#2|) . T)) ((($) . T)) @@ -1412,10 +1412,10 @@ ((((-560)) |has| #0=(-421 |#2|) (-660 (-560))) ((#0#) . T)) ((($) . T) (((-560)) . T)) ((((-560) (-146)) . T)) -((((-560) (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T) ((|#1| |#2|) . T)) +((((-560) (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T) ((|#1| |#2|) . T)) ((((-421 (-560))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-887)) . T)) ((((-935 |#1|)) . T)) (|has| |#1| (-376)) @@ -1443,7 +1443,7 @@ ((((-549)) . T)) ((((-887)) . T)) ((($) . T)) -((((-560) (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T) (((-1264 (-560)) $) . T) ((|#1| |#2|) . T)) +((((-560) (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T) (((-1264 (-560)) $) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-175))) @@ -1461,7 +1461,7 @@ ((((-549)) |has| |#1| (-633 (-549))) (((-915 (-391))) |has| |#1| (-633 (-915 (-391)))) (((-915 (-560))) |has| |#1| (-633 (-915 (-560))))) ((((-887)) . T)) ((((-893 |#1|)) . T) (($) . T) (((-421 (-560))) . T)) -(((|#2|) . T) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-520)) . T)) ((((-520)) . T)) ((((-1207)) -2222 (-12 (|has| |#4| (-927 (-1207))) (|has| |#4| (-1080))) (-12 (|has| |#4| (-929 (-1207))) (|has| |#4| (-1080))))) @@ -1504,7 +1504,7 @@ (((|#1|) . T) (((-421 (-560))) |has| |#1| (-38 (-421 (-560)))) (((-560)) . T) (($) . T)) ((((-1207)) |has| (-421 |#2|) (-927 (-1207)))) (((|#2|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) ((($) . T)) ((((-421 (-560))) |has| |#2| (-38 (-421 (-560)))) ((|#2|) |has| |#2| (-175)) (($) -2222 (|has| |#2| (-466)) (|has| |#2| (-571)) (|has| |#2| (-939)))) ((((-421 (-560))) |has| |#2| (-38 (-421 (-560)))) ((|#2|) . T) (($) -2222 (|has| |#2| (-175)) (|has| |#2| (-466)) (|has| |#2| (-571)) (|has| |#2| (-939)))) @@ -1523,7 +1523,7 @@ (((|#2|) . T) (((-560)) . T)) ((((-887)) . T)) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T) ((|#2|) . T)) ((((-887)) . T)) ((((-887)) . T)) ((((-1189) (-1207) (-560) (-229) (-887)) . T)) @@ -1613,7 +1613,7 @@ ((((-1027 |#1|)) . T) ((|#1|) . T)) ((((-1207)) -2222 (|has| |#1| (-927 (-1207))) (|has| |#1| (-929 (-1207)))) (((-840 (-1207))) . T)) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-421 (-560))) . T) (((-421 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1201 |#1|)) . T)) ((((-560)) . T) (($) . T) (((-421 (-560))) . T)) @@ -1622,7 +1622,7 @@ (((|#1|) . T) (((-560)) . T) (($) . T)) (((|#2|) . T)) ((((-560)) . T) (($) . T) (((-421 (-560))) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) ((((-887)) -2222 (|has| |#1| (-632 (-887))) (|has| |#1| (-1132)))) ((((-560) |#2|) . T)) (((|#1|) . T) (((-421 (-560))) . T) (((-560)) . T) (($) . T)) @@ -1636,7 +1636,7 @@ (((|#3|) -12 (|has| |#3| (-321 |#3|)) (|has| |#3| (-1132)))) ((((-1287 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-1287 |#1| |#2| |#3|)) |has| |#1| (-376))) -(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#2| |#2|) . T)) (-2222 (|has| |#1| (-15 * (|#1| (-560) |#1|))) (-12 (|has| |#1| (-376)) (|has| |#2| (-240))) (-12 (|has| |#1| (-376)) (|has| |#2| (-239)))) (|has| |#2| (-376)) @@ -1688,7 +1688,7 @@ (((|#1| |#2|) . T)) (-2222 (|has| |#2| (-240)) (|has| |#2| (-239))) ((((-560) (-146)) . T) (((-1264 (-560)) $) . T)) -(((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132)))) +(((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132)))) ((($) -2222 (|has| |#1| (-466)) (|has| |#1| (-571)) (|has| |#1| (-939))) ((|#1|) |has| |#1| (-175)) (((-421 (-560))) |has| |#1| (-38 (-421 (-560))))) (|has| |#1| (-871)) (((|#2| (-793) (-1113)) . T)) @@ -1749,7 +1749,7 @@ ((($ (-1207)) . T)) ((($) |has| |#1| (-571)) ((|#1|) |has| |#1| (-175)) (((-421 (-560))) |has| |#1| (-38 (-421 (-560))))) ((((-887)) -2222 (|has| |#2| (-21)) (|has| |#2| (-23)) (|has| |#2| (-25)) (|has| |#2| (-133)) (|has| |#2| (-632 (-887))) (|has| |#2| (-175)) (|has| |#2| (-376)) (|has| |#2| (-381)) (|has| |#2| (-748)) (|has| |#2| (-815)) (|has| |#2| (-871)) (|has| |#2| (-1080)) (|has| |#2| (-1132))) (((-1297 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3819 (-1189)) (|:| -2309 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3820 (-1189)) (|:| -2308 #0#))) . T)) (((|#1|) . T)) ((((-887)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132)))) @@ -1801,13 +1801,13 @@ (((|#2|) |has| |#2| (-175))) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-1205 |#1| |#2| |#3|)) |has| |#1| (-376))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-1207) (-51)) . T)) ((((-421 (-560)) |#1|) . T) (($ $) . T)) (((|#1| (-560)) . T)) @@ -1863,11 +1863,11 @@ (-2222 (|has| |#1| (-376)) (|has| |#1| (-363))) (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-38 (-421 (-560)))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-1207)) |has| |#1| (-927 (-1207))) (((-1113)) . T)) (((|#1|) . T)) (|has| |#1| (-870)) -(((#0=(-2 (|:| -3819 (-1189)) (|:| -2309 (-51))) #0#) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))))) +(((#0=(-2 (|:| -3820 (-1189)) (|:| -2308 (-51))) #0#) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) (|has| |#1| (-1132)) ((((-887)) . T) (((-1212)) . T)) @@ -1940,7 +1940,7 @@ ((($) |has| |#1| (-381))) (((|#1| |#2|) . T)) (-2222 (|has| |#2| (-466)) (|has| |#2| (-939))) -(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) ((#0=(-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) #0#) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) ((#0=(-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) #0#) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))))) (-2222 (|has| |#1| (-466)) (|has| |#1| (-939))) (((|#1|) . T)) (((|#1|) . T) (($) . T)) @@ -1966,7 +1966,7 @@ ((((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376))) (($) -2222 (|has| |#1| (-376)) (|has| |#1| (-571))) (((-1205 |#1| |#2| |#3|)) |has| |#1| (-376)) ((|#1|) |has| |#1| (-175))) (((|#1|) |has| |#1| (-175)) (((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376))) (($) -2222 (|has| |#1| (-376)) (|has| |#1| (-571)))) ((($) |has| |#1| (-571)) ((|#1|) |has| |#1| (-175)) (((-421 (-560))) |has| |#1| (-38 (-421 (-560))))) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((((-560)) |has| #0=(-421 |#2|) (-660 (-560))) ((#0#) . T) (((-421 (-560))) . T) (($) . T)) ((((-694 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -2048,7 +2048,7 @@ ((((-887)) . T)) ((((-887)) . T)) ((($ $) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((($) -2222 (|has| |#1| (-15 * (|#1| (-560) |#1|))) (-12 (|has| |#1| (-376)) (|has| |#2| (-240))) (-12 (|has| |#1| (-376)) (|has| |#2| (-239))))) ((($) |has| |#1| (-15 * (|#1| (-421 (-560)) |#1|)))) ((((-1002)) . T)) @@ -2081,7 +2081,7 @@ (((|#1| (-1257 |#1| |#2| |#3|)) . T)) ((((-887)) . T)) (|has| |#1| (-1132)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1| (-793)) . T)) ((((-1189) |#1|) . T)) (((|#1|) . T)) @@ -2131,7 +2131,7 @@ ((($) -2222 (|has| |#1| (-175)) (|has| |#1| (-376)) (|has| |#1| (-571))) (((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376))) (((-1205 |#1| |#2| |#3|)) |has| |#1| (-376)) ((|#1|) . T)) (((|#1|) . T) (($) -2222 (|has| |#1| (-175)) (|has| |#1| (-376)) (|has| |#1| (-571))) (((-421 (-560))) -2222 (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-376)))) ((($) -2222 (|has| |#1| (-175)) (|has| |#1| (-571))) ((|#1|) . T) (((-421 (-560))) |has| |#1| (-38 (-421 (-560))))) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#1|) |has| |#1| (-175))) ((((-887)) . T)) ((($) |has| |#1| (-571)) ((|#1|) |has| |#1| (-175)) (((-421 (-560))) |has| |#1| (-38 (-421 (-560))))) @@ -2160,7 +2160,7 @@ (|has| |#1| (-870)) (((|#1| (-560) (-1113)) . T)) (-2222 (|has| |#1| (-927 (-1207))) (|has| |#1| (-1080))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1| (-421 (-560)) (-1113)) . T)) (((|#1| (-793) (-1113)) . T)) (|has| |#1| (-871)) @@ -2179,11 +2179,11 @@ (-2222 (|has| |#1| (-102)) (|has| |#1| (-1132))) ((((-560)) -12 (|has| |#1| (-376)) (|has| |#2| (-660 (-560)))) ((|#2|) |has| |#1| (-376))) (-2222 (|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| (-1132))) -((((-711 (-352 (-2450) (-2450 (QUOTE X) (QUOTE HESS)) (-721)))) . T)) +((((-711 (-352 (-2451) (-2451 (QUOTE X) (QUOTE HESS)) (-721)))) . T)) (((|#2|) |has| |#2| (-175))) (((|#1|) |has| |#1| (-175))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) ((((-887)) . T)) ((((-887)) . T)) ((((-887)) . T)) @@ -2198,11 +2198,11 @@ ((($) . T) ((|#1|) . T) (((-421 (-560))) |has| |#1| (-376)) (((-560)) |has| |#1| (-660 (-560)))) (|has| |#1| (-871)) (((|#1|) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T) (((-560)) . T)) (((|#2|) . T)) ((((-560)) . T) ((|#3|) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) |has| (-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))))) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) |has| (-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))))) (-2222 (|has| |#1| (-466)) (|has| |#1| (-939))) (((|#2|) . T) (((-560)) |has| |#2| (-660 (-560)))) ((((-887)) . T)) @@ -2273,7 +2273,7 @@ (((|#2|) |has| |#2| (-1080))) (|has| |#1| (-376)) ((($) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (((|#1|) |has| |#1| (-175))) ((($ (-888 |#1|)) . T)) (((|#1| |#1|) . T)) @@ -2327,7 +2327,7 @@ (((|#1| |#2|) . T)) ((($) . T) (((-560)) . T) (((-421 (-560))) . T)) ((((-560)) . T) (($) . T) (((-421 (-560))) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))) . T)) (((|#1|) . T) (((-421 (-560))) . T) (((-560)) . T) (($) . T)) (((|#1|) . T) (((-421 (-560))) . T) (((-560)) . T) (($) . T)) (((|#1|) . T) (((-421 (-560))) . T) (((-560)) . T) (($) . T)) @@ -2342,7 +2342,7 @@ (((|#2|) . T)) ((($) . T) (((-560)) . T) (((-421 (-560))) -2222 (|has| |#1| (-376)) (|has| |#1| (-363))) ((|#1|) . T)) ((((-560) |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) ((((-391)) . T)) ((((-721)) . T)) ((((-421 (-560))) . #0=(|has| |#2| (-376))) (($) . #0#)) @@ -2362,7 +2362,7 @@ ((((-1207)) |has| |#2| (-927 (-1207)))) (|has| |#1| (-871)) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (|has| |#1| (-813)) ((((-421 (-560))) . T) (($) . T)) (|has| |#1| (-487)) @@ -2393,12 +2393,12 @@ (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-38 (-421 (-560)))) (|has| |#1| (-871)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-560)) . T)) (|has| |#1| (-149)) (|has| |#1| (-147)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)))) ((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132)))) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)))) ((|#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132)))) (((|#2|) . T)) (|has| |#1| (-15 * (|#1| (-560) |#1|))) (((|#3|) . T)) @@ -2423,7 +2423,7 @@ (((|#1|) |has| |#1| (-376))) (((|#1|) |has| |#1| (-376))) ((((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((($ $) . T) (((-630 $) $) . T)) (-2222 (|has| |#1| (-376)) (|has| |#1| (-571))) ((($) . T) (((-1284 |#1| |#2| |#3| |#4|)) . T) (((-421 (-560))) . T)) @@ -2506,7 +2506,7 @@ (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -2222 (|has| |#1| (-302)) (|has| |#1| (-376))) ((#0=(-421 (-560)) #0#) |has| |#1| (-376))) ((((-975 |#1|)) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((($) . T)) ((((-560) |#1|) . T)) ((((-1207)) |has| (-421 |#2|) (-927 (-1207)))) @@ -2553,7 +2553,7 @@ (((|#1|) . T) (((-560)) |has| |#1| (-660 (-560)))) ((($) -2222 (|has| |#1| (-376)) (|has| |#1| (-363))) (((-421 (-560))) -2222 (|has| |#1| (-376)) (|has| |#1| (-363))) ((|#1|) . T)) ((((-560)) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))))) +((((-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))))) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) (|has| |#1| (-870)) ((((-560) $) . T) (((-663 (-560)) $) . T)) @@ -2609,10 +2609,10 @@ ((((-549)) |has| |#4| (-633 (-549)))) (-2222 (|has| |#1| (-102)) (|has| |#1| (-1132))) ((((-887)) . T) (((-663 |#4|)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-376)) -(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) (((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) |has| (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|)) (-321 (-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))))) +(((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132))) (((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) |has| (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|)) (-321 (-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))))) (-2222 (-12 (|has| |#1| (-376)) (|has| |#2| (-842))) (-12 (|has| |#1| (-376)) (|has| |#2| (-871)))) (((|#1|) . T)) (((|#1|) . T)) @@ -2657,7 +2657,7 @@ ((((-887)) . T)) ((((-887)) . T)) ((((-549)) |has| |#1| (-633 (-549)))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-560)) . T) (($) . T) (((-421 (-560))) . T)) ((((-1207) |#1|) |has| |#1| (-528 (-1207) |#1|)) ((|#1| |#1|) |has| |#1| (-321 |#1|))) (((|#1|) -2222 (|has| |#1| (-175)) (|has| |#1| (-376)))) @@ -2699,7 +2699,7 @@ (|has| |#1| (-571)) (((|#2|) . T)) ((((-560)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T)) (-2222 (|has| |#1| (-147)) (|has| |#1| (-149)) (|has| |#1| (-175)) (|has| |#1| (-571)) (|has| |#1| (-1080))) ((((-595 |#1|)) . T)) @@ -2849,16 +2849,16 @@ (|has| |#1| (-939)) ((($) -2222 (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) (-12 (|has| |#2| (-239)) (|has| |#2| (-1080))))) (((|#2|) |has| |#2| (-175))) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-1287 |#1| |#2| |#3|)) |has| |#1| (-376))) ((((-887)) . T)) ((((-887)) . T)) ((((-549)) . T) (((-560)) . T) (((-915 (-560))) . T) (((-391)) . T) (((-229)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-560)) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))) . T)) (((|#1|) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((((-887)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-560)) . T)) @@ -2880,7 +2880,7 @@ ((((-887)) . T)) ((((-887)) . T)) ((((-186)) . T) (((-887)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-887)) . T)) ((((-887)) . T)) @@ -2897,7 +2897,7 @@ (|has| |#1| (-871)) ((((-887)) . T)) ((((-549)) |has| |#1| (-633 (-549)))) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) ((($) -2222 (-12 (|has| (-1205 |#1| |#2| |#3|) (-240)) (|has| |#1| (-376))) (-12 (|has| (-1205 |#1| |#2| |#3|) (-239)) (|has| |#1| (-376))) (|has| |#1| (-15 * (|#1| (-560) |#1|))))) ((((-887)) . T)) (((|#2|) |has| |#2| (-376))) @@ -2964,10 +2964,10 @@ (-2222 (|has| |#1| (-147)) (|has| |#1| (-381))) (-2222 (|has| |#1| (-147)) (|has| |#1| (-381))) (-2222 (|has| |#1| (-147)) (|has| |#1| (-381))) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((((-560) |#3|) . T)) (((|#1|) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3819 (-1207)) (|:| -2309 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3820 (-1207)) (|:| -2308 #0#))) . T)) (|has| |#1| (-363)) ((((-560)) . T)) ((((-887)) . T)) @@ -3057,7 +3057,7 @@ (|has| |#2| (-1051)) ((($) . T)) (|has| |#1| (-939)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#4|) . T)) ((($) . T)) (((|#2|) . T)) @@ -3087,7 +3087,7 @@ ((((-421 (-560))) . T)) (-2222 (|has| |#1| (-466)) (|has| |#1| (-571)) (|has| |#1| (-939))) ((((-1189)) . T) (((-887)) . T)) -(((#0=(-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) #0#) |has| (-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))))) +(((#0=(-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) #0#) |has| (-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))))) ((((-1189)) . T)) (|has| |#1| (-939)) (|has| |#2| (-376)) @@ -3132,7 +3132,7 @@ (-2222 (|has| |#4| (-815)) (|has| |#4| (-871))) (-2222 (|has| |#3| (-815)) (|has| |#3| (-871))) ((((-560)) . T) (($) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-175))) @@ -3185,9 +3185,9 @@ (((|#2|) . T)) (((|#2|) . T)) (|has| |#2| (-1080)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (|has| |#1| (-38 (-421 (-560)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-421 (-560)))) @@ -3335,7 +3335,7 @@ ((($) -2222 (-12 (|has| |#2| (-240)) (|has| |#2| (-1080))) (-12 (|has| |#2| (-239)) (|has| |#2| (-1080))))) ((((-595 |#1|)) . T) (((-421 (-560))) . T) (($) . T) (((-560)) . T)) ((((-560)) . T) (((-421 (-560))) . T) (($) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 (-51)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-560)) . T)) (((|#1|) -12 (|has| |#1| (-321 |#1|)) (|has| |#1| (-1132)))) @@ -3399,7 +3399,7 @@ ((((-887)) . T)) (((|#1|) . T)) (((|#1|) . T)) -((((-2 (|:| -3819 (-1189)) (|:| -2309 |#1|))) . T)) +((((-2 (|:| -3820 (-1189)) (|:| -2308 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -3542,7 +3542,7 @@ (((|#1|) . T)) ((((-887)) . T)) (|has| |#2| (-939)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((((-549)) |has| |#2| (-633 (-549))) (((-915 (-391))) |has| |#2| (-633 (-915 (-391)))) (((-915 (-560))) |has| |#2| (-633 (-915 (-560))))) ((((-887)) . T)) ((((-887)) . T)) @@ -3752,7 +3752,7 @@ ((((-1212)) . T)) ((((-887)) . T) (((-1212)) . T)) ((((-1212)) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) |has| (-2 (|:| -3819 (-1207)) (|:| -2309 (-51))) (-321 (-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))))) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) |has| (-2 (|:| -3820 (-1207)) (|:| -2308 (-51))) (-321 (-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))))) (-2222 (|has| |#2| (-466)) (|has| |#2| (-571)) (|has| |#2| (-939))) ((((-560) |#1|) . T)) ((((-560) |#1|) . T)) @@ -3972,7 +3972,7 @@ ((((-887)) . T)) ((((-560)) . T)) ((((-560)) . T)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#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 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((($) . T)) (|has| |#1| (-1051)) -(((|#2|) . T) (((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) ((($) . T)) ((((-887)) . T)) ((((-549)) |has| |#2| (-633 (-549))) (((-915 (-560))) |has| |#2| (-633 (-915 (-560)))) (((-915 (-391))) |has| |#2| (-633 (-915 (-391)))) (((-391)) . #0=(|has| |#2| (-1051))) (((-229)) . #0#)) @@ -4143,7 +4143,7 @@ ((((-887)) . T)) ((((-887)) . T)) (((|#1| (-545 |#2|)) . T)) -((((-2 (|:| -3819 (-1207)) (|:| -2309 (-51)))) . T)) +((((-2 (|:| -3820 (-1207)) (|:| -2308 (-51)))) . T)) ((((-560) (-130)) . T)) (((|#1| (-560)) . T)) (((|#1| (-421 (-560))) . T)) @@ -4182,7 +4182,7 @@ ((((-421 |#2|)) . T)) (|has| |#1| (-571)) (|has| |#1| (-571)) -((((-2 (|:| -3819 |#1|) (|:| -2309 |#2|))) . T)) +((((-2 (|:| -3820 |#1|) (|:| -2308 |#2|))) . T)) (((|#2| (-793)) . T)) ((($) . T) ((|#2|) . T)) ((($) . T) (((-421 (-560))) . 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| (-1132))) ((#0=(-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) #0#) |has| (-2 (|:| -3819 |#1|) (|:| -2309 |#2|)) (-321 (-2 (|:| -3819 |#1|) (|:| -2309 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-321 |#2|)) (|has| |#2| (-1132))) ((#0=(-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) #0#) |has| (-2 (|:| -3820 |#1|) (|:| -2308 |#2|)) (-321 (-2 (|:| -3820 |#1|) (|:| -2308 |#2|))))) (-2222 (|has| |#1| (-240)) (|has| |#1| (-239))) (((#0=(-118 |#1|)) |has| #0# (-321 #0#))) ((($ $) . T)) |