diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 1126 |
1 files changed, 563 insertions, 563 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 6c515db3..6b7fd020 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(142764 . 3417777702) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(142764 . 3419169932) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#2| |#2|) . T)) ((((-525)) . T)) -((($ $) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525))))) ((($) . T)) (((|#1|) . T)) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) -((($) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) (|has| |#1| (-842)) ((((-796)) . T)) ((((-796)) . T)) @@ -23,28 +23,28 @@ ((((-205)) . T) (((-796)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) -((($ $) . T) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -(-3321 (|has| |#1| (-761)) (|has| |#1| (-788))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +(-3150 (|has| |#1| (-761)) (|has| |#1| (-788))) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) ((((-796)) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-786)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-796)) . T)) ((((-796)) |has| |#1| (-1018))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) |has| |#1| (-966 (-385 (-525))))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(((|#2| (-458 (-4045 |#1|) (-712))) . T)) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(((|#2| (-458 (-2028 |#1|) (-712))) . T)) (((|#1| (-497 (-1089))) . T)) (((#0=(-803 |#1|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#4| (-346)) (|has| |#3| (-346)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-517)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-796)) . T)) ((((-796)) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) ((((-796)) . T)) ((((-796)) . T)) ((((-796)) . T)) (((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +(((|#1|) . T) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1| |#2|) . T)) ((((-796)) . T)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) (((|#1|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) ((($ $) . T)) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) ((($) . T)) (|has| |#1| (-346)) (((|#1|) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-796)) . T)) ((((-796)) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) (((|#1| |#1|) . T)) (|has| |#1| (-517)) (((|#2| |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-288 |#2|))) (((-1089) |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-486 (-1089) |#2|)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (|has| |#1| (-1018)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (|has| |#1| (-1018)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (|has| |#1| (-786)) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3321 (|has| |#4| (-734)) (|has| |#4| (-786))) -(-3321 (|has| |#4| (-734)) (|has| |#4| (-786))) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#4| (-734)) (|has| |#4| (-786))) +(-3150 (|has| |#4| (-734)) (|has| |#4| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1018)) @@ -132,21 +132,21 @@ ((((-525)) . T)) ((((-525)) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#1| (-712)) . T)) (|has| |#2| (-734)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (|has| |#2| (-786)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1072) |#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1|) . T)) (((|#3| (-712)) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-1018)) ((((-385 (-525))) . T) (((-525)) . T)) ((((-1089) |#2|) |has| |#2| (-486 (-1089) |#2|)) ((|#2| |#2|) |has| |#2| (-288 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-525)) . T)) ((((-525)) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) ((((-525)) . T)) ((((-525)) . T)) (((#0=(-640) (-1085 #0#)) . T)) @@ -173,12 +173,12 @@ ((((-796)) . T)) ((((-796)) . T)) (((|#1| |#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) ((((-796)) . T)) ((((-796)) . T)) ((((-796)) . T)) @@ -189,25 +189,25 @@ ((((-796)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) (|has| |#1| (-341)) (-12 (|has| |#4| (-213)) (|has| |#4| (-975))) (-12 (|has| |#3| (-213)) (|has| |#3| (-975))) -(-3321 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-796)) . T)) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-587 (-525)))) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1|) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) @@ -218,11 +218,11 @@ (((|#2|) . T) (($) . T) (((-385 (-525))) . T)) (-12 (|has| |#1| (-1018)) (|has| |#2| (-1018))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(((|#3| |#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($ $) |has| |#3| (-160))) -(((|#4| |#4|) -3321 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975))) (($ $) |has| |#4| (-160))) +(((|#3| |#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($ $) |has| |#3| (-160))) +(((|#4| |#4|) -3150 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975))) (($ $) |has| |#4| (-160))) (((|#1|) . T)) (((|#2|) . T)) ((((-501)) |has| |#2| (-566 (-501))) (((-825 (-357))) |has| |#2| (-566 (-825 (-357)))) (((-825 (-525))) |has| |#2| (-566 (-825 (-525))))) @@ -231,21 +231,21 @@ ((((-796)) . T)) ((((-501)) |has| |#1| (-566 (-501))) (((-825 (-357))) |has| |#1| (-566 (-825 (-357)))) (((-825 (-525))) |has| |#1| (-566 (-825 (-525))))) ((((-796)) . T)) -(((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($) |has| |#3| (-160))) -(((|#4|) -3321 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975))) (($) |has| |#4| (-160))) +(((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($) |has| |#3| (-160))) +(((|#4|) -3150 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975))) (($) |has| |#4| (-160))) ((((-796)) . T)) ((((-501)) . T) (((-525)) . T) (((-825 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) |has| |#1| (-966 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) ((((-385 $) (-385 $)) |has| |#2| (-517)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-842)) ((((-1072) (-51)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-587 (-525))) ((#0#) . T)) ((((-501)) . T) (((-205)) . T) (((-357)) . T) (((-825 (-357))) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) (((|#1|) |has| |#1| (-160))) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-796)) . T)) @@ -256,15 +256,15 @@ (|has| |#1| (-788)) (|has| |#1| (-1018)) (((|#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) ((((-125)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((((-125)) . T)) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-213)) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| (-497 (-759 (-1089)))) . T)) (((|#1| (-902)) . T)) (((#0=(-803 |#1|) $) |has| #0# (-265 #0# #0#))) @@ -273,7 +273,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1065)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (|has| (-1157 |#1| |#2| |#3| |#4|) (-136)) (|has| (-1157 |#1| |#2| |#3| |#4|) (-138)) (|has| |#1| (-136)) @@ -290,20 +290,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-975))) ((((-796)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) ((#0=(-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) #0#) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) ((#0=(-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) #0#) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))))) ((((-525) |#1|) . T)) ((((-796)) . T)) ((((-501)) -12 (|has| |#1| (-566 (-501))) (|has| |#2| (-566 (-501)))) (((-825 (-357))) -12 (|has| |#1| (-566 (-825 (-357)))) (|has| |#2| (-566 (-825 (-357))))) (((-825 (-525))) -12 (|has| |#1| (-566 (-825 (-525)))) (|has| |#2| (-566 (-825 (-525)))))) ((((-796)) . T)) ((((-796)) . T)) ((($) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-796)) . T)) ((((-796)) . T)) (|has| (-1156 |#2| |#3| |#4|) (-138)) @@ -314,16 +314,16 @@ ((((-796)) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) (((|#1|) . T)) ((((-525) |#1|) . T)) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) ((((-796)) |has| |#1| (-1018))) -(-3321 (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-843 |#1|)) . T)) ((((-385 |#2|) |#3|) . T)) (|has| |#1| (-15 * (|#1| (-525) |#1|))) @@ -335,7 +335,7 @@ (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) (|has| |#1| (-341)) -(-3321 (-12 (|has| (-1163 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-3150 (-12 (|has| (-1163 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) ((((-525)) . T)) @@ -347,31 +347,31 @@ (((|#1|) . T)) ((((-525) |#1|) . T)) (((|#2|) . T)) -(-3321 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (((|#1|) . T)) ((((-1089)) -12 (|has| |#3| (-833 (-1089))) (|has| |#3| (-975)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-761))) -(-3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) +(-3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($ $) |has| |#1| (-517))) (((#0=(-640) (-1085 #0#)) . T)) ((((-796)) . T)) ((((-796)) . T) (((-1171 |#4|)) . T)) ((((-796)) . T) (((-1171 |#3|)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517))) ((((-796)) . T)) ((($) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1163 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1163 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (((|#3|) |has| |#3| (-975))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-1018)) (((|#2| (-760 |#1|)) . T)) (((|#1|) . T)) @@ -383,37 +383,37 @@ ((((-135)) . T)) (((|#3|) |has| |#3| (-1018)) (((-525)) -12 (|has| |#3| (-966 (-525))) (|has| |#3| (-1018))) (((-385 (-525))) -12 (|has| |#3| (-966 (-385 (-525)))) (|has| |#3| (-1018)))) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) ((((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#2| (-761)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-786)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-501)) |has| |#1| (-566 (-501)))) (((|#1| |#2|) . T)) ((((-1089)) -12 (|has| |#1| (-341)) (|has| |#1| (-833 (-1089))))) ((((-1072) |#1|) . T)) (((|#1| |#2| |#3| (-497 |#3|)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) ((((-796)) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (|has| |#1| (-346)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-525)) . T)) ((((-525)) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((((-796)) . T)) ((((-796)) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-975))) @@ -422,10 +422,10 @@ ((((-525) |#4|) . T)) ((((-525) |#3|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-587 (-525)))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-1157 |#1| |#2| |#3| |#4|)) . T)) ((((-385 (-525))) . T) (((-525)) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) @@ -454,38 +454,38 @@ ((($) . T)) ((($ $) . T) ((#0=(-1089) $) . T) ((#0# |#1|) . T)) (((|#2|) |has| |#2| (-160))) -((($) -3321 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) -(((|#2| |#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) +((($) -3150 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +(((|#2| |#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) ((((-135)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-346)) (|has| |#2| (-346))) ((((-796)) . T)) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) (((|#1|) . T)) ((((-796)) . T)) (|has| |#1| (-1018)) (|has| $ (-138)) ((((-525) |#1|) . T)) -((($) -3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-833 (-1089))))) (|has| |#1| (-341)) -(-3321 (-12 (|has| (-1087 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-3150 (-12 (|has| (-1087 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) (|has| |#1| (-15 * (|#1| (-712) |#1|))) (((|#1|) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) ((((-796)) . T)) ((((-525) (-125)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (((|#2| (-497 (-798 |#1|))) . T)) ((((-796)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -502,28 +502,28 @@ ((((-796)) . T)) ((((-796)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1087 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1087 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-975))) (|has| |#1| (-1018)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) |has| |#1| (-160)) (($) . T)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((((-796)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) (((#0=(-1003) |#1|) . T) ((#0# $) . T) (($ $) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#2|) |has| |#1| (-341))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1018)) (((-525)) -12 (|has| |#2| (-966 (-525))) (|has| |#2| (-1018))) (((-385 (-525))) -12 (|has| |#2| (-966 (-385 (-525)))) (|has| |#2| (-1018)))) @@ -538,8 +538,8 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-136)) (|has| |#1| (-138)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) @@ -550,12 +550,12 @@ (((|#1| (-712) (-1003)) . T)) ((((-385 (-525))) |has| |#2| (-341)) (($) . T)) (((|#1| (-497 (-1008 (-1089))) (-1008 (-1089))) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (|has| |#2| (-734)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) @@ -588,63 +588,63 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) (((|#2|) . T) (((-525)) |has| |#2| (-966 (-525))) (((-385 (-525))) |has| |#2| (-966 (-385 (-525))))) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1018)))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#2|) . T)) -((((-796)) -3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) +((((-796)) -3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) (((|#1|) |has| |#1| (-160))) ((((-525)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-525) (-135)) . T)) -((($) -3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +((($) -3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) (((|#2|) |has| |#1| (-341))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| (-497 #0=(-1089)) #0#) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-160)) (|has| |#3| (-160)) (((#0=(-385 (-885 |#1|)) #0#) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (|has| |#1| (-1018)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (|has| |#1| (-1018)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1| |#1|) |has| |#1| (-160))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T)) ((((-385 (-885 |#1|))) . T)) ((((-525) (-125)) . T)) (((|#1|) |has| |#1| (-160))) ((((-125)) . T)) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-796)) . T)) ((((-1157 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-975)) (((-525)) -12 (|has| |#1| (-587 (-525))) (|has| |#1| (-975)))) (((|#1| |#2|) . T)) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) (|has| |#3| (-734)) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) (|has| |#3| (-786)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) (((|#2|) . T)) ((((-525) (-125)) . T)) ((((-796)) . T)) @@ -660,22 +660,22 @@ (|has| |#1| (-1018)) (((|#2|) . T)) ((((-501)) |has| |#2| (-566 (-501))) (((-825 (-357))) |has| |#2| (-566 (-825 (-357)))) (((-825 (-525))) |has| |#2| (-566 (-825 (-525))))) -(((|#4|) -3321 (|has| |#4| (-160)) (|has| |#4| (-341)))) -(((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#4|) -3150 (|has| |#4| (-160)) (|has| |#4| (-341)))) +(((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)))) ((((-796)) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) ((($ $) . T) ((#0=(-1089) $) |has| |#1| (-213)) ((#0# |#1|) |has| |#1| (-213)) ((#1=(-759 (-1089)) |#1|) . T) ((#1# $) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) ((((-525) |#2|) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -((($) -3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975)))) +((($) -3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975)))) ((((-525) |#1|) . T)) (|has| (-385 |#2|) (-138)) (|has| (-385 |#2|) (-136)) @@ -688,22 +688,22 @@ (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-366) (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-366) (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#2| (-1065)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((|#1|) . T)) ((((-366) (-1072)) . T)) (|has| |#1| (-517)) ((((-112 |#1|)) . T)) ((((-125)) . T)) ((((-525) |#1|) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#2|) . T)) ((((-796)) . T)) ((((-760 |#1|)) . T)) @@ -716,7 +716,7 @@ (((|#1|) |has| |#1| (-160))) ((((-796)) . T)) ((((-501)) |has| |#1| (-566 (-501)))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#2|) |has| |#2| (-288 |#2|))) (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) (((|#1|) . T)) @@ -726,7 +726,7 @@ (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) ((($) . T) (((-525)) . T) (((-385 (-525))) . T)) (|has| |#2| (-346)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) @@ -737,9 +737,9 @@ ((((-1087 |#1| |#2| |#3|) $) -12 (|has| (-1087 |#1| |#2| |#3|) (-265 (-1087 |#1| |#2| |#3|) (-1087 |#1| |#2| |#3|))) (|has| |#1| (-341))) (($ $) . T)) ((((-796)) . T)) ((((-796)) . T)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) ((($ $) . T)) ((($ $) . T)) ((((-796)) . T)) @@ -749,12 +749,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525) (-135)) . T)) ((((-135)) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) ((((-108)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-108)) . T)) @@ -762,38 +762,38 @@ ((((-501)) |has| |#1| (-566 (-501))) (((-205)) . #0=(|has| |#1| (-951))) (((-357)) . #0#)) ((((-796)) . T)) (|has| |#1| (-761)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (|has| |#1| (-788)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-517)) (|has| |#1| (-842)) (((|#1|) . T)) (|has| |#1| (-1018)) ((((-796)) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-796)) . T)) ((((-796)) . T)) ((((-796)) . T)) (((|#1| (-1171 |#1|) (-1171 |#1|)) . T)) ((((-525) (-135)) . T)) ((($) . T)) -(-3321 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-796)) . T)) (|has| |#1| (-1018)) (((|#1| (-902)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(-3321 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-668)) (|has| |#2| (-668)))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-668)) (|has| |#2| (-668)))) (((|#1|) . T)) (|has| |#2| (-734)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (|has| |#2| (-786)) @@ -808,7 +808,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) (|has| |#1| (-769)) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) (|has| |#1| (-1018)) @@ -819,8 +819,8 @@ (((|#3|) |has| |#3| (-1018))) (|has| |#3| (-346)) (((|#1|) . T) (((-796)) . T)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((((-796)) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) @@ -830,30 +830,30 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-160))) ((((-385 (-525))) . T) (((-525)) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) ((((-135)) . T)) (((|#1|) . T)) ((((-135)) . T)) -((($) -3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) +((($) -3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975)))) ((((-135)) . T)) (((|#1| |#2| |#3|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) (|has| $ (-138)) (|has| $ (-138)) (|has| |#1| (-1018)) ((((-796)) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-975)) (|has| |#1| (-1030))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-975)) (|has| |#1| (-1030))) ((($ $) |has| |#1| (-265 $ $)) ((|#1| $) |has| |#1| (-265 |#1| |#1|))) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) ((((-1089)) . T)) (|has| |#1| (-517)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) @@ -864,7 +864,7 @@ (|has| |#1| (-138)) (|has| |#1| (-136)) (|has| |#4| (-786)) -(((|#2| (-220 (-4045 |#1|) (-712)) (-798 |#1|)) . T)) +(((|#2| (-220 (-2028 |#1|) (-712)) (-798 |#1|)) . T)) (|has| |#3| (-786)) (((|#1| (-497 |#3|) |#3|) . T)) (|has| |#1| (-138)) @@ -878,21 +878,21 @@ (|has| |#1| (-136)) ((((-385 (-525))) |has| |#2| (-341)) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-327)) (|has| |#1| (-346))) ((((-1056 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-160)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-975))) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) ((((-796)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-640)) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (|has| |#1| (-517)) (((|#1|) . T)) (((|#1|) . T)) @@ -914,10 +914,10 @@ (((|#1| (-385 (-525))) . T)) (((|#3|) . T) (((-564 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((#0=(-1087 |#1| |#2| |#3|) #0#) -12 (|has| (-1087 |#1| |#2| |#3|) (-288 (-1087 |#1| |#2| |#3|))) (|has| |#1| (-341))) (((-1089) #0#) -12 (|has| (-1087 |#1| |#2| |#3|) (-486 (-1089) (-1087 |#1| |#2| |#3|))) (|has| |#1| (-341)))) @@ -925,8 +925,8 @@ ((((-796)) . T)) ((((-796)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) (((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) (((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))))) ((((-796)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -937,10 +937,10 @@ ((($ $) . T) ((#0=(-798 |#1|) $) . T) ((#0# |#2|) . T)) (|has| |#1| (-769)) (|has| |#1| (-1018)) -(((|#2| |#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)))) -((((-525) (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) +(((|#2| |#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)))) +((((-525) (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) ((((-712)) . T)) ((((-525)) . T)) (|has| |#1| (-517)) @@ -953,29 +953,29 @@ ((((-112 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-138)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-825 (-525))) . T) (((-825 (-357))) . T) (((-501)) . T) (((-1089)) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) ((($) . T)) ((((-796)) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (((|#2|) |has| |#2| (-160))) -((($) -3321 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -3150 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) ((((-803 |#1|)) . T)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (-12 (|has| |#3| (-213)) (|has| |#3| (-975))) (|has| |#2| (-1065)) -(((#0=(-51)) . T) (((-2 (|:| -2019 (-1089)) (|:| -1221 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1265 (-1089)) (|:| -1568 #0#))) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) (((|#1| (-525) (-1003)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| (-385 (-525)) (-1003)) . T)) -((($) -3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-525) |#2|) . T)) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) @@ -983,37 +983,37 @@ (-12 (|has| |#1| (-346)) (|has| |#2| (-346))) ((((-796)) . T)) ((((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-796)) . T)) (|has| |#1| (-327)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-796)) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((($) . T)) ((((-796)) . T)) (((|#1|) . T)) ((((-803 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) ((((-796)) . T)) -(((|#3| |#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($ $) |has| |#3| (-160))) +(((|#3| |#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($ $) |has| |#3| (-160))) (|has| |#1| (-951)) ((((-796)) . T)) -(((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($) |has| |#3| (-160))) +(((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975))) (($) |has| |#3| (-160))) ((((-525) (-108)) . T)) (((|#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-346)) @@ -1021,31 +1021,31 @@ (|has| |#1| (-346)) ((((-1089) $) |has| |#1| (-486 (-1089) $)) (($ $) |has| |#1| (-288 $)) ((|#1| |#1|) |has| |#1| (-288 |#1|)) (((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|))) ((((-1089)) |has| |#1| (-833 (-1089)))) -(-3321 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) +(-3150 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) ((((-366) (-1036)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-366) |#1|) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1018)) ((((-796)) . T)) ((((-796)) . T)) ((((-843 |#1|)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) (((#0=(-803 |#1|)) |has| #0# (-288 #0#))) (((|#1| |#2|) . T)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734))) (((|#1|) . T)) (-12 (|has| |#1| (-734)) (|has| |#2| (-734))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#1| (-1111)) (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) ((((-385 (-525))) . T) (($) . T)) @@ -1056,8 +1056,8 @@ (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (|has| |#1| (-341)) ((((-525)) . T) (((-385 (-525))) . T) (($) . T)) -((($ $) . T) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) ((((-796)) . T)) ((((-796)) . T)) @@ -1072,14 +1072,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-786)) (|has| |#1| (-786)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) -(((#0=(-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) #0#) |has| (-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))))) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) +(((#0=(-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) #0#) |has| (-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))))) ((($) . T)) (|has| |#2| (-788)) ((($) . T)) (((|#2|) |has| |#2| (-1018))) -((((-796)) -3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) +((((-796)) -3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) (|has| |#1| (-788)) (|has| |#1| (-788)) ((((-1072) (-51)) . T)) @@ -1087,10 +1087,10 @@ ((((-796)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-587 (-525))) ((#0#) . T)) ((((-525) (-135)) . T)) -((((-525) (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T) ((|#1| |#2|) . T)) ((((-385 (-525))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-796)) . T)) ((((-843 |#1|)) . T)) (|has| |#1| (-341)) @@ -1115,31 +1115,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-160))) -((((-525) (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-160))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842)))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) (((|#1|) . T)) ((((-501)) |has| |#1| (-566 (-501))) (((-825 (-357))) |has| |#1| (-566 (-825 (-357)))) (((-825 (-525))) |has| |#1| (-566 (-825 (-525))))) ((((-796)) . T)) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#2| (-786)) (-12 (|has| |#2| (-213)) (|has| |#2| (-975))) (|has| |#1| (-517)) (|has| |#1| (-1065)) ((((-1072) |#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-385 (-525))) |has| |#1| (-966 (-525))) (((-525)) |has| |#1| (-966 (-525))) (((-1089)) |has| |#1| (-966 (-1089))) ((|#1|) . T)) ((((-525) |#2|) . T)) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) ((((-525)) |has| |#1| (-819 (-525))) (((-357)) |has| |#1| (-819 (-357)))) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1|) . T)) ((((-591 |#4|)) . T) (((-796)) . T)) ((((-501)) |has| |#4| (-566 (-501)))) @@ -1152,17 +1152,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1089)) |has| (-385 |#2|) (-833 (-1089)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-796)) -3321 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-565 (-796))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) (((-1171 |#3|)) . T)) +((((-796)) -3150 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-565 (-796))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) (((-1171 |#3|)) . T)) ((((-525) |#2|) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) -(((|#2| |#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(((|#2| |#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($ $) |has| |#2| (-160))) ((((-796)) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T) ((|#2|) . T)) ((((-796)) . T)) ((((-796)) . T)) ((((-1072) (-1089) (-525) (-205) (-796)) . T)) @@ -1197,8 +1197,8 @@ (|has| |#1| (-37 (-385 (-525)))) ((((-796)) . T)) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-975))) (($) |has| |#2| (-160))) (|has| $ (-138)) ((((-385 |#2|)) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-966 (-385 (-525)))) (((-525)) |has| #0# (-966 (-525))) ((#0#) . T)) @@ -1209,11 +1209,11 @@ (((|#3|) |has| |#3| (-160))) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) @@ -1244,7 +1244,7 @@ ((((-929 |#1|)) . T) ((|#1|) . T)) ((((-796)) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-385 (-525))) . T) (((-385 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1085 |#1|)) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) @@ -1252,9 +1252,9 @@ (|has| |#1| (-788)) (((|#2|) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) ((((-525) |#2|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#2|) . T)) ((((-525) |#3|) . T)) (((|#2|) . T)) @@ -1269,7 +1269,7 @@ (((|#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1018)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-341)) (((|#2|) . T) (((-525)) |has| |#2| (-966 (-525))) (((-385 (-525))) |has| |#2| (-966 (-385 (-525))))) @@ -1299,19 +1299,19 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| |#2|) . T)) ((((-525) (-135)) . T)) -(((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-788)) (((|#2| (-712) (-1003)) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-732)) (((|#1|) |has| |#1| (-160))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) -(-3321 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) +(-3150 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) +(-3150 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) (((|#4|) . T)) (|has| |#1| (-136)) ((((-1072) |#1|) . T)) @@ -1324,10 +1324,10 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#3|) . T)) ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018))) (((-890 |#1|)) . T)) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018))) (((-890 |#1|)) . T)) (|has| |#1| (-786)) (|has| |#1| (-786)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) @@ -1340,8 +1340,8 @@ ((($) . T)) ((((-366) (-1072)) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-796)) -3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2019 (-1072)) (|:| -1221 #0#))) . T)) +((((-796)) -3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-565 (-796))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((-1171 |#2|)) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1265 (-1072)) (|:| -1568 #0#))) . T)) (((|#1|) . T)) ((((-796)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) @@ -1349,7 +1349,7 @@ (|has| |#2| (-136)) (|has| |#2| (-138)) (|has| |#1| (-450)) -(-3321 (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) (|has| |#1| (-341)) ((((-796)) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -1358,8 +1358,8 @@ (|has| |#1| (-786)) (|has| |#1| (-786)) ((((-796)) . T)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1163 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1089)) |has| |#1| (-833 (-1089)))) @@ -1367,7 +1367,7 @@ ((((-796)) . T)) ((((-796)) . T)) (|has| |#1| (-1018)) -(((|#2| (-458 (-4045 |#1|) (-712)) (-798 |#1|)) . T)) +(((|#2| (-458 (-2028 |#1|) (-712)) (-798 |#1|)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1| (-497 (-1089)) (-1089)) . T)) (((|#1|) . T)) @@ -1387,16 +1387,16 @@ (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) ((((-1087 |#1| |#2| |#3|)) |has| |#1| (-341))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-1089) (-51)) . T)) ((($ $) . T)) (((|#1| (-525)) . T)) ((((-843 |#1|)) . T)) -(((|#1|) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975))) (($) -3321 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)))) +(((|#1|) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975))) (($) -3150 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)))) (((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) |has| |#1| (-966 (-385 (-525))))) (|has| |#1| (-788)) (|has| |#1| (-788)) @@ -1411,13 +1411,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) (((|#1|) |has| |#1| (-160))) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) -(((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#2| (-788)) (|has| |#1| (-788)) -(-3321 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-842))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-525) |#2|) . T)) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)))) (|has| |#1| (-327)) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1018)))) ((($) . T) (((-385 (-525))) . T)) @@ -1425,7 +1425,7 @@ (|has| |#1| (-761)) (|has| |#1| (-761)) (((|#1|) . T)) -(-3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-786)) (|has| |#1| (-786)) (|has| |#1| (-786)) @@ -1434,13 +1434,13 @@ ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-1089)) |has| |#1| (-833 (-1089))) (((-1003)) . T)) (((|#1|) . T)) (|has| |#1| (-786)) -(((#0=(-2 (|:| -2019 (-1072)) (|:| -1221 (-51))) #0#) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))))) +(((#0=(-2 (|:| -1265 (-1072)) (|:| -1568 (-51))) #0#) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (|has| |#1| (-1018)) (((|#1|) . T)) @@ -1459,7 +1459,7 @@ (((|#1|) . T)) ((((-135)) . T)) (((|#2|) |has| |#2| (-160))) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((|#1|) . T)) (|has| |#1| (-136)) (|has| |#1| (-138)) @@ -1481,32 +1481,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) ((#0=(-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) #0#) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))))) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) ((#0=(-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) #0#) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#1| (-788)) (|has| |#1| (-517)) ((((-538 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-3321 (-12 (|has| |#1| (-341)) (|has| |#2| (-761))) (-12 (|has| |#1| (-341)) (|has| |#2| (-788)))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (-12 (|has| |#1| (-341)) (|has| |#2| (-761))) (-12 (|has| |#1| (-341)) (|has| |#2| (-788)))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-843 |#1|)) . T)) (((|#1| (-469 |#1| |#3|) (-469 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-712)) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1087 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((((-616 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1514,17 +1514,17 @@ ((((-796)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-796)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) ((((-796)) . T)) ((((-796)) . T)) ((((-796)) . T)) (((|#2|) . T)) -(-3321 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) (|has| |#1| (-1111)) (|has| |#1| (-1111)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (|has| |#1| (-1111)) (|has| |#1| (-1111)) (((|#3| |#3|) . T)) @@ -1537,43 +1537,43 @@ (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((((-1072) (-51)) . T)) (|has| |#1| (-1018)) -(-3321 (|has| |#2| (-761)) (|has| |#2| (-788))) +(-3150 (|has| |#2| (-761)) (|has| |#2| (-788))) (((|#1|) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) (((|#1|) |has| |#1| (-160)) (($) . T)) ((($) . T)) ((((-1087 |#1| |#2| |#3|)) -12 (|has| (-1087 |#1| |#2| |#3|) (-288 (-1087 |#1| |#2| |#3|))) (|has| |#1| (-341)))) ((((-796)) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((($) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-796)) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) (|has| |#2| (-842)) (|has| |#1| (-341)) (((|#2|) |has| |#2| (-1018))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((($) . T) ((|#2|) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) (|has| |#1| (-842)) (|has| |#1| (-842)) ((((-501)) . T) (((-385 (-1085 (-525)))) . T) (((-205)) . T) (((-357)) . T)) ((((-357)) . T) (((-205)) . T) (((-796)) . T)) (|has| |#1| (-842)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) ((($ $) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((($ $) . T)) ((((-525) (-108)) . T)) ((($) . T)) (((|#1|) . T)) ((((-525)) . T)) ((((-108)) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-37 (-385 (-525)))) (((|#1| (-525)) . T)) ((($) . T)) @@ -1595,7 +1595,7 @@ (((|#1| (-1135 |#1| |#2| |#3|)) . T)) (((|#1| (-712)) . T)) (((|#1|) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-796)) . T)) (|has| |#1| (-1018)) ((((-1072) |#1|) . T)) @@ -1615,18 +1615,18 @@ (((|#1|) . T)) ((((-525)) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-796)) . T)) (((|#3|) . T)) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-796)) . T)) ((((-1156 |#2| |#3| |#4|)) . T) (((-1157 |#1| |#2| |#3| |#4|)) . T)) ((((-796)) . T)) -((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-966 (-525)))) (((-564 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) -3321 (-12 (|has| |#1| (-517)) (|has| |#1| (-966 (-525)))) (|has| |#1| (-966 (-385 (-525))))) (((-385 (-885 |#1|))) |has| |#1| (-517)) (((-885 |#1|)) |has| |#1| (-975)) (((-1089)) . T)) +((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-966 (-525)))) (((-564 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) -3150 (-12 (|has| |#1| (-517)) (|has| |#1| (-966 (-525)))) (|has| |#1| (-966 (-385 (-525))))) (((-385 (-885 |#1|))) |has| |#1| (-517)) (((-885 |#1|)) |has| |#1| (-975)) (((-1089)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-712)) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-288 |#1|))) ((((-1157 |#1| |#2| |#3| |#4|)) . T)) ((((-525)) |has| |#1| (-819 (-525))) (((-357)) |has| |#1| (-819 (-357)))) @@ -1634,14 +1634,14 @@ (|has| |#1| (-517)) (((|#1|) . T)) ((((-796)) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((|#1|) |has| |#1| (-160))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1018))) -(((|#2|) -3321 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -3150 (|has| |#2| (-160)) (|has| |#2| (-341)))) ((((-1156 |#2| |#3| |#4|)) . T)) ((((-108)) . T)) (|has| |#1| (-761)) @@ -1651,8 +1651,8 @@ (|has| |#1| (-786)) (|has| |#1| (-786)) (((|#1| (-525) (-1003)) . T)) -(-3321 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +(-3150 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1| (-385 (-525)) (-1003)) . T)) (((|#1| (-712) (-1003)) . T)) (|has| |#1| (-788)) @@ -1668,28 +1668,28 @@ (((|#1|) . T)) (|has| |#1| (-1018)) ((((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-587 (-525)))) ((|#2|) |has| |#1| (-341))) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) ((((-796)) . T)) (|has| |#3| (-786)) ((((-796)) . T)) ((((-1156 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-796)) . T)) -(((|#1| |#1|) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975)))) +(((|#1| |#1|) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975)))) (((|#1|) . T)) ((((-525)) . T)) ((((-525)) . T)) -(((|#1|) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975)))) +(((|#1|) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-975)))) (((|#2|) |has| |#2| (-341))) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-788)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) |has| (-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-842))) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) |has| (-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-842))) (((|#2|) . T) (((-525)) |has| |#2| (-587 (-525)))) ((((-796)) . T)) ((((-796)) . T)) @@ -1724,18 +1724,18 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (((|#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-796)) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| (-385 |#2|) (-213)) (|has| |#1| (-842)) (((|#2|) |has| |#2| (-975))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (|has| |#1| (-341)) (((|#1|) |has| |#1| (-160))) (((|#1| |#1|) . T)) @@ -1760,7 +1760,7 @@ (((|#1| (-385 (-525)) (-1003)) . T)) (((|#1| (-712) (-1003)) . T)) (((#0=(-385 |#2|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -(((|#1|) . T) (((-525)) -3321 (|has| (-385 (-525)) (-966 (-525))) (|has| |#1| (-966 (-525)))) (((-385 (-525))) . T)) +(((|#1|) . T) (((-525)) -3150 (|has| (-385 (-525)) (-966 (-525))) (|has| |#1| (-966 (-525)))) (((-385 (-525))) . T)) (((|#1| (-556 |#1| |#3|) (-556 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) @@ -1779,24 +1779,24 @@ ((((-640)) . T)) (((|#2|) |has| |#2| (-160))) (|has| |#2| (-786)) -((((-108)) |has| |#1| (-1018)) (((-796)) -3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018)))) +((((-108)) |has| |#1| (-1018)) (((-796)) -3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))) . T)) ((((-796)) . T)) ((((-525) |#1|) . T)) ((((-640)) . T) (((-385 (-525))) . T) (((-525)) . T)) (((|#1| |#1|) |has| |#1| (-160))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) ((((-357)) . T)) ((((-640)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1|) |has| |#1| (-160))) ((((-385 (-885 |#1|))) . T)) (((|#2| |#2|) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#2|) . T)) (|has| |#2| (-788)) (((|#3|) |has| |#3| (-975))) @@ -1806,14 +1806,14 @@ (|has| |#1| (-788)) ((((-1089)) |has| |#2| (-833 (-1089)))) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-450)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-975)) (|has| |#1| (-1030))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-975)) (|has| |#1| (-1030))) (|has| |#1| (-37 (-385 (-525)))) ((((-112 |#1|)) . T)) ((((-112 |#1|)) . T)) @@ -1834,11 +1834,11 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-788)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (((|#2|) . T)) (((|#3|) . T)) ((((-112 |#1|)) . T)) @@ -1856,11 +1856,11 @@ ((((-501)) |has| |#1| (-566 (-501))) (((-825 (-525))) |has| |#1| (-566 (-825 (-525)))) (((-825 (-357))) |has| |#1| (-566 (-825 (-357)))) (((-357)) . #0=(|has| |#1| (-951))) (((-205)) . #0#)) (((|#1|) |has| |#1| (-341))) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((($ $) . T) (((-564 $) $) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T) (((-1157 |#1| |#2| |#3| |#4|)) . T) (((-385 (-525))) . T)) -((($) -3321 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-517))) +((($) -3150 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-517))) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| |#1| (-341)) @@ -1871,11 +1871,11 @@ ((((-357)) . T)) (((|#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1018)))) ((((-796)) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-842))) (((|#1|) . T)) (|has| |#1| (-788)) (|has| |#1| (-788)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (|has| |#1| (-1018)) @@ -1884,13 +1884,13 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((((-525)) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((#0=(-1156 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525)))) (($) . T)) ((((-525)) . T)) (|has| |#1| (-341)) -(-3321 (-12 (|has| (-1163 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3321 (-12 (|has| (-1163 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-3150 (-12 (|has| (-1163 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-3150 (-12 (|has| (-1163 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) (|has| |#1| (-341)) (|has| |#1| (-136)) (|has| |#1| (-138)) @@ -1907,18 +1907,18 @@ (((|#1| |#2|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-587 (-525)))) (((|#3|) |has| |#3| (-160))) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) ((((-525)) . T)) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-385 (-525))) . T) (($) . T) (((-385 |#1|)) . T) ((|#1|) . T)) ((((-796)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) ((($) . T)) ((((-525) |#1|) . T)) ((((-1089)) |has| (-385 |#2|) (-833 (-1089)))) -(((|#1|) . T) (($) -3321 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) +(((|#1|) . T) (($) -3150 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) ((((-501)) |has| |#2| (-566 (-501)))) ((((-631 |#2|)) . T) (((-796)) . T)) (((|#1|) . T)) @@ -1926,8 +1926,8 @@ (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) ((((-803 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -(-3321 (|has| |#4| (-734)) (|has| |#4| (-786))) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#4| (-734)) (|has| |#4| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) ((((-796)) . T)) ((((-796)) . T)) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) @@ -1943,17 +1943,17 @@ ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-1129))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-1129))) ((($) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-966 (-385 (-525)))) (((-525)) |has| #0# (-966 (-525))) ((#0#) . T)) (((|#2|) . T) (((-525)) |has| |#2| (-587 (-525)))) (((|#1| (-712)) . T)) (|has| |#1| (-788)) (((|#1|) . T) (((-525)) |has| |#1| (-587 (-525)))) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-525)) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))))) +((((-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (|has| |#1| (-786)) (|has| |#1| (-37 (-385 (-525)))) @@ -1978,24 +1978,24 @@ (((|#1| |#2|) . T)) ((((-135)) . T)) ((((-721 |#1| (-798 |#2|))) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (|has| |#1| (-1111)) (((|#1|) . T)) -(-3321 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) +(-3150 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975)) (|has| |#3| (-1018))) ((((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|))) (((|#2|) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-843 |#1|)) . T)) ((($) . T)) ((((-385 (-885 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-501)) |has| |#4| (-566 (-501)))) ((((-796)) . T) (((-591 |#4|)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-786)) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) (((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) |has| (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|)) (-288 (-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018))) (((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) |has| (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|)) (-288 (-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))))) (|has| |#1| (-1018)) (|has| |#1| (-341)) (|has| |#1| (-788)) @@ -2003,16 +2003,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-385 (-525))) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (|has| |#1| (-136)) (|has| |#1| (-138)) -(-3321 (-12 (|has| (-1087 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3321 (-12 (|has| (-1087 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-3150 (-12 (|has| (-1087 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-3150 (-12 (|has| (-1087 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) (|has| |#1| (-786)) (((|#1| |#2|) . T)) @@ -2035,9 +2035,9 @@ ((((-796)) . T)) ((((-796)) . T)) ((((-501)) |has| |#1| (-566 (-501)))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(((|#1|) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)))) +(((|#1|) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)))) ((((-294 |#1|)) . T)) (((|#2|) |has| |#2| (-341))) (((|#2|) . T)) @@ -2058,14 +2058,14 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((($ $) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018))) (|has| |#1| (-517)) (((|#2|) . T)) ((((-525)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2090,12 +2090,12 @@ (((|#1| |#2|) . T)) ((((-1089) |#1|) . T)) (((|#4|) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-1089) (-51)) . T)) ((((-1156 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-385 (-525))) |has| |#1| (-966 (-385 (-525)))) (((-525)) |has| |#1| (-966 (-525))) ((|#1|) . T)) ((((-796)) . T)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975)) (|has| |#2| (-1018))) (((#0=(-1157 |#1| |#2| |#3| |#4|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) (((|#1| |#1|) |has| |#1| (-160)) ((#0=(-385 (-525)) #0#) |has| |#1| (-517)) (($ $) |has| |#1| (-517))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) @@ -2114,14 +2114,14 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (((|#2| |#3|) . T)) -(-3321 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (((|#1| (-497 |#2|)) . T)) (((|#1| (-712)) . T)) (((|#1| (-497 (-1008 (-1089)))) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (|has| |#2| (-842)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) ((((-796)) . T)) ((($ $) . T) ((#0=(-1156 |#2| |#3| |#4|) #0#) . T) ((#1=(-385 (-525)) #1#) |has| #0# (-37 (-385 (-525))))) ((((-843 |#1|)) . T)) @@ -2130,13 +2130,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (|has| |#1| (-341)) ((($) . T) ((#0=(-1156 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1087 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3321 (-12 (|has| |#1| (-286)) (|has| |#1| (-842))) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3321 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) +(-3150 (-12 (|has| |#1| (-286)) (|has| |#1| (-842))) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-833 (-1089))) (|has| |#1| (-975))) ((((-525)) |has| |#1| (-587 (-525))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-796)) . T)) @@ -2168,27 +2168,27 @@ (((|#1|) |has| |#1| (-160))) ((((-796)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) -(((|#2|) -3321 (|has| |#2| (-6 (-4252 "*"))) (|has| |#2| (-160)))) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(((|#2|) -3150 (|has| |#2| (-6 (-4252 "*"))) (|has| |#2| (-160)))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (|has| |#2| (-788)) (|has| |#2| (-842)) (|has| |#1| (-842)) (((|#2|) |has| |#2| (-160))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-796)) . T)) ((((-796)) . T)) ((((-501)) . T) (((-525)) . T) (((-825 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))) . T)) (((|#1|) . T)) ((((-796)) . T)) (((|#1| |#2|) . T)) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-269)) (|has| |#1| (-341))) +(-3150 (|has| |#1| (-269)) (|has| |#1| (-341))) ((((-135)) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) (|has| |#1| (-786)) @@ -2203,7 +2203,7 @@ ((((-385 (-525))) . T) (($) . T)) ((((-796)) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-796)) . T)) ((((-796)) . T)) @@ -2214,7 +2214,7 @@ (((|#1|) . T)) ((((-591 (-135))) . T) (((-1072)) . T)) ((((-796)) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) ((((-1089) |#1|) |has| |#1| (-486 (-1089) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-788)) ((((-796)) . T)) @@ -2226,16 +2226,16 @@ ((((-796)) . T) (((-591 |#4|)) . T)) (((|#2|) . T)) ((((-843 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3321 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-1089) (-51)) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) (|has| |#1| (-842)) (|has| |#1| (-842)) (((|#2|) . T)) @@ -2250,12 +2250,12 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (|has| |#1| (-761)) (((#0=(-843 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((((-385 |#2|)) . T)) (|has| |#1| (-786)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) ((#1=(-525) #1#) . T) (($ $) . T)) ((((-843 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) (((|#2|) |has| |#2| (-975)) (((-525)) -12 (|has| |#2| (-587 (-525))) (|has| |#2| (-975)))) @@ -2265,25 +2265,25 @@ (|has| |#1| (-136)) (((|#2|) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -2019 (-1089)) (|:| -1221 #0#))) . T)) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1265 (-1089)) (|:| -1568 #0#))) . T)) (|has| |#1| (-327)) ((((-525)) . T)) ((((-796)) . T)) (((#0=(-1157 |#1| |#2| |#3| |#4|) $) |has| #0# (-265 #0# #0#))) (|has| |#1| (-341)) (((#0=(-1003) |#1|) . T) ((#0# $) . T) (($ $) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (((#0=(-385 (-525)) #0#) . T) ((#1=(-640) #1#) . T) (($ $) . T)) ((((-294 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-1018)) (((|#1|) . T)) -(((|#1|) -3321 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) -(((|#1|) -3321 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -3150 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -3150 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) (((|#2|) . T)) ((((-385 (-525))) . T) (((-640)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2302,7 +2302,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-525)) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#2|) . T) (((-525)) |has| |#2| (-587 (-525)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2339,7 +2339,7 @@ (|has| |#2| (-951)) ((($) . T)) (|has| |#1| (-842)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2347,24 +2347,24 @@ ((($) . T)) (|has| |#1| (-341)) ((((-843 |#1|)) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3321 (|has| |#1| (-346)) (|has| |#1| (-788))) +(-3150 (|has| |#1| (-346)) (|has| |#1| (-788))) (((|#1|) . T)) ((((-796)) . T)) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-833 (-1089))))) ((((-385 |#2|) |#3|) . T)) ((($) . T) (((-385 (-525))) . T)) ((((-712) |#1|) . T)) -(((|#2| (-220 (-4045 |#1|) (-712))) . T)) +(((|#2| (-220 (-2028 |#1|) (-712))) . T)) (((|#1| (-497 |#3|)) . T)) ((((-385 (-525))) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-796)) . T)) -(((#0=(-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) #0#) |has| (-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))))) +(((#0=(-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) #0#) |has| (-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))))) (|has| |#1| (-842)) (|has| |#2| (-341)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-796)) . T)) (((|#1|) . T)) @@ -2381,11 +2381,11 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) (-12 (|has| |#1| (-510)) (|has| |#1| (-769))) ((((-796)) . T)) -((((-1089)) -3321 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-833 (-1089)))))) +((((-1089)) -3150 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-833 (-1089)))))) (|has| |#1| (-341)) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-833 (-1089))))) (|has| |#1| (-341)) @@ -2395,7 +2395,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-341))) (((|#2|) |has| |#1| (-341))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) @@ -2418,31 +2418,31 @@ (((|#2|) |has| |#1| (-341))) ((((-357)) -12 (|has| |#1| (-341)) (|has| |#2| (-819 (-357)))) (((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-819 (-525))))) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (|has| |#1| (-517)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) (((|#3|) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#2|) . T)) (((|#2|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) ((((-1072) |#1|) . T)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) ((((-538 |#1|)) . T)) ((($) . T)) @@ -2450,7 +2450,7 @@ (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-796)) . T)) ((($) . T)) @@ -2475,7 +2475,7 @@ (|has| |#1| (-732)) (|has| |#1| (-732)) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-110)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2496,7 +2496,7 @@ ((((-525)) . T)) ((((-796)) . T)) ((((-525)) . T)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-796)) . T)) ((((-796)) . T)) @@ -2508,9 +2508,9 @@ (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-341)) (|has| |#1| (-341)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-668)) (|has| |#1| (-833 (-1089))) (|has| |#1| (-975)) (|has| |#1| (-1030)) (|has| |#1| (-1018))) (|has| |#1| (-1065)) ((((-525) |#1|) . T)) (((|#1|) . T)) @@ -2528,8 +2528,8 @@ (((|#1|) . T)) (|has| |#1| (-517)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-357)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2538,7 +2538,7 @@ (|has| |#1| (-517)) (|has| |#1| (-1018)) ((((-721 |#1| (-798 |#2|))) |has| (-721 |#1| (-798 |#2|)) (-288 (-721 |#1| (-798 |#2|))))) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-842)) @@ -2548,12 +2548,12 @@ (|has| |#1| (-213)) (((|#1| (-497 (-1008 (-1089)))) . T)) (|has| |#2| (-341)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) ((((-796)) . T)) ((((-796)) . T)) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) ((((-796)) . T)) ((((-796)) . T)) (((|#1|) . T)) @@ -2562,8 +2562,8 @@ ((((-525)) . T)) (((|#3|) . T)) ((((-796)) . T)) -(-3321 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3321 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) +(-3150 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-975))) (((#0=(-538 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1|) |has| |#1| (-160))) @@ -2576,7 +2576,7 @@ (((|#1|) . T)) ((((-796)) |has| |#1| (-565 (-796)))) ((((-273 |#3|)) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) (((|#2| |#2|) . T) ((|#6| |#6|) . T)) (((|#1|) . T)) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) @@ -2584,20 +2584,20 @@ (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((((-796)) . T)) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-842)) (|has| |#1| (-842)) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-2 (|:| -2019 (-1072)) (|:| -1221 |#1|))) . T)) +((((-2 (|:| -1265 (-1072)) (|:| -1568 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2611,10 +2611,10 @@ (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018)))) (((#0=(-385 (-525)) #0#) . T)) ((((-385 (-525))) . T)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#1|) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-501)) . T)) ((((-796)) . T)) ((((-1089)) |has| |#2| (-833 (-1089))) (((-1003)) . T)) @@ -2628,12 +2628,12 @@ ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-1089)) |has| |#1| (-833 (-1089)))) ((((-843 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((|#2|) |has| |#2| (-975)) (((-525)) -12 (|has| |#2| (-587 (-525))) (|has| |#2| (-975)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-517)))) (|has| |#1| (-517)) (((|#1|) |has| |#1| (-341))) ((((-525)) . T)) @@ -2652,8 +2652,8 @@ ((((-796)) . T)) (|has| |#2| (-761)) (|has| |#2| (-761)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1|) . T) (((-525)) |has| |#1| (-966 (-525))) (((-385 (-525))) |has| |#1| (-966 (-385 (-525))))) ((((-525)) |has| |#1| (-819 (-525))) (((-357)) |has| |#1| (-819 (-357)))) @@ -2679,12 +2679,12 @@ (((|#2| (-712)) . T)) ((((-1089)) . T)) ((((-803 |#1|)) . T)) -(-3321 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-796)) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-734)) (|has| |#2| (-786))) -(-3321 (-12 (|has| |#1| (-734)) (|has| |#2| (-734))) (-12 (|has| |#1| (-788)) (|has| |#2| (-788)))) +(-3150 (|has| |#2| (-734)) (|has| |#2| (-786))) +(-3150 (-12 (|has| |#1| (-734)) (|has| |#2| (-734))) (-12 (|has| |#1| (-788)) (|has| |#2| (-788)))) ((((-803 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-346)) @@ -2710,7 +2710,7 @@ (((|#1|) . T)) ((((-796)) . T)) (|has| |#2| (-842)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) ((((-501)) |has| |#2| (-566 (-501))) (((-825 (-357))) |has| |#2| (-566 (-825 (-357)))) (((-825 (-525))) |has| |#2| (-566 (-825 (-525))))) ((((-796)) . T)) ((((-796)) . T)) @@ -2743,11 +2743,11 @@ ((((-385 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1018)) -(((|#2| (-458 (-4045 |#1|) (-712))) . T)) +(((|#2| (-458 (-2028 |#1|) (-712))) . T)) ((((-525) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-497 (-1089))) . T)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-525)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2757,9 +2757,9 @@ ((($) . T) (((-385 (-525))) . T)) ((($) . T)) ((($) . T)) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) (((|#1|) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-796)) . T)) ((((-135)) . T)) (((|#1|) . T) (((-385 (-525))) . T)) @@ -2799,27 +2799,27 @@ (|has| |#1| (-213)) (((|#1| (-497 |#3|)) . T)) (|has| |#1| (-346)) -(((|#2| (-220 (-4045 |#1|) (-712))) . T)) +(((|#2| (-220 (-2028 |#1|) (-712))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (((|#1|) . T) (($) . T)) (((|#1| (-497 |#2|)) . T)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#1| (-712)) . T)) (|has| |#1| (-517)) -(-3321 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-786)) (|has| |#2| (-975))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-796)) . T)) -(-3321 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) -(-3321 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) +(-3150 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) (((|#1|) |has| |#1| (-160))) (((|#4|) |has| |#4| (-975))) (((|#3|) |has| |#3| (-975))) (-12 (|has| |#1| (-341)) (|has| |#2| (-761))) (-12 (|has| |#1| (-341)) (|has| |#2| (-761))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) @@ -2832,14 +2832,14 @@ (((|#2|) |has| |#2| (-975)) (((-525)) -12 (|has| |#2| (-587 (-525))) (|has| |#2| (-975)))) (((|#1|) . T)) (|has| |#2| (-341)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#2| |#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) @@ -2858,25 +2858,25 @@ (((|#1|) |has| |#2| (-395 |#1|))) (((|#1|) |has| |#2| (-395 |#1|))) ((((-843 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) ((((-796)) . T)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) |has| (-2 (|:| -2019 (-1089)) (|:| -1221 (-51))) (-288 (-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))))) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) |has| (-2 (|:| -1265 (-1089)) (|:| -1568 (-51))) (-288 (-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-525) |#1|) . T)) (((|#1|) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((((-1089)) |has| |#1| (-833 (-1089))) (((-759 (-1089))) . T)) -(-3321 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-734)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((((-760 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-796)) . T)) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) ((((-796)) . T)) @@ -2884,15 +2884,15 @@ (((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517)) (((-385 (-525))) |has| |#1| (-517))) (((|#2|) . T) (((-525)) |has| |#2| (-587 (-525)))) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (-12 (|has| |#1| (-341)) (|has| |#2| (-213)))) +(-3150 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (-12 (|has| |#1| (-341)) (|has| |#2| (-213)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-525) |#1|) . T)) ((((-294 |#1|)) . T)) (((#0=(-640) (-1085 #0#)) . T)) -((((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-786)) ((($ $) . T) ((#0=(-798 |#1|) $) . T) ((#0# |#2|) . T)) @@ -2909,12 +2909,12 @@ (((#0=(-1157 |#1| |#2| |#3| |#4|)) |has| #0# (-288 #0#))) ((($) . T)) (((|#1|) . T)) -((($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (|has| |#2| (-213)) (|has| $ (-138)) ((((-796)) . T)) -((($) . T) (((-385 (-525))) -3321 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3150 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-796)) . T)) (|has| |#1| (-786)) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089))))) @@ -2926,23 +2926,23 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#4|) . T)) (|has| |#1| (-517)) -((($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) -((((-1089)) -3321 (-12 (|has| (-1163 |#1| |#2| |#3|) (-833 (-1089))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))))) -(((|#1|) . T) (($) -3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3321 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) +((((-1089)) -3150 (-12 (|has| (-1163 |#1| |#2| |#3|) (-833 (-1089))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))))) +(((|#1|) . T) (($) -3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3150 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-833 (-1089))))) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-712) |#1|))) (|has| |#1| (-833 (-1089))))) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1018)))) ((((-525) |#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) (((|#1|) . T)) (((|#1| (-497 (-759 (-1089)))) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#1|) . T)) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) (((|#1|) . T)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(-3321 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) ((($) . T) (((-803 |#1|)) . T) (((-385 (-525))) . T)) ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) @@ -2951,15 +2951,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 |#2|)) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1|) . T)) (((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-525)) . T)) @@ -2988,32 +2988,32 @@ ((((-1163 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1089)) . T) (((-796)) . T)) (|has| |#1| (-341)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-1022)) . T)) ((((-796)) . T)) -((($) -3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) -((($) -3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-842)) (|has| |#1| (-842)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-160))) ((((-640)) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-160))) ((((-385 (-525))) . T) (($) . T)) (((|#1| (-525)) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-341)) (|has| |#1| (-341)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3321 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-160)) (|has| |#1| (-517))) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-712)) . T)) @@ -3028,16 +3028,16 @@ ((((-825 (-357))) . T) (((-825 (-525))) . T) (((-1089)) . T) (((-501)) . T)) (((|#1|) . T)) ((((-796)) . T)) -(-3321 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) -(-3321 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) +(-3150 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-734)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-734)) (|has| |#2| (-734)))) ((((-525)) . T)) ((((-525)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-3321 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) +(-3150 (|has| |#2| (-160)) (|has| |#2| (-786)) (|has| |#2| (-975))) ((((-1089)) -12 (|has| |#2| (-833 (-1089))) (|has| |#2| (-975)))) -(-3321 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-668)) (|has| |#2| (-668)))) +(-3150 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-668)) (|has| |#2| (-668)))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-341)) @@ -3061,7 +3061,7 @@ ((((-1072) (-1089) (-525) (-205) (-796)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-3321 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-3150 (|has| |#1| (-327)) (|has| |#1| (-346))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-796)) . T)) @@ -3069,7 +3069,7 @@ ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-1018)) (((-525)) -12 (|has| |#2| (-966 (-525))) (|has| |#2| (-1018))) (((-385 (-525))) -12 (|has| |#2| (-966 (-385 (-525)))) (|has| |#2| (-1018)))) ((((-501)) |has| |#1| (-566 (-501)))) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-788)) (|has| |#1| (-1018)))) ((($) . T) (((-385 (-525))) . T)) (|has| |#1| (-842)) (|has| |#1| (-842)) @@ -3078,14 +3078,14 @@ ((((-796)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-160))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) (((|#2|) . T)) -(-3321 (|has| |#1| (-21)) (|has| |#1| (-786))) +(-3150 (|has| |#1| (-21)) (|has| |#1| (-786))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (((|#1|) . T)) -((((-796)) -3321 (-12 (|has| |#1| (-565 (-796))) (|has| |#2| (-565 (-796)))) (-12 (|has| |#1| (-1018)) (|has| |#2| (-1018))))) +((((-796)) -3150 (-12 (|has| |#1| (-565 (-796))) (|has| |#2| (-565 (-796)))) (-12 (|has| |#1| (-1018)) (|has| |#2| (-1018))))) ((((-385 |#2|) |#3|) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -3097,17 +3097,17 @@ (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((#0=(-525) #0#) . T)) ((($) . T) (((-385 (-525))) . T)) -(-3321 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) -(-3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) +(-3150 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) +(-3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) (|has| |#4| (-734)) -(-3321 (|has| |#4| (-734)) (|has| |#4| (-786))) +(-3150 (|has| |#4| (-734)) (|has| |#4| (-786))) (|has| |#4| (-786)) (|has| |#3| (-734)) -(-3321 (|has| |#3| (-734)) (|has| |#3| (-786))) +(-3150 (|has| |#3| (-734)) (|has| |#3| (-786))) (|has| |#3| (-786)) ((((-525)) . T)) (((|#2|) . T)) -((((-1089)) -3321 (-12 (|has| (-1087 |#1| |#2| |#3|) (-833 (-1089))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))))) +((((-1089)) -3150 (-12 (|has| (-1087 |#1| |#2| |#3|) (-833 (-1089))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-833 (-1089)))))) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-833 (-1089))))) ((((-1089)) -12 (|has| |#1| (-15 * (|#1| (-712) |#1|))) (|has| |#1| (-833 (-1089))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3122,11 +3122,11 @@ ((((-1087 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1087 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1054 |#1| |#2|)) . T)) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) ((($) . T)) (|has| |#1| (-951)) -(((|#2|) . T) (((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) ((((-796)) . T)) ((((-501)) |has| |#2| (-566 (-501))) (((-825 (-525))) |has| |#2| (-566 (-825 (-525)))) (((-825 (-357))) |has| |#2| (-566 (-825 (-357)))) (((-357)) . #0=(|has| |#2| (-951))) (((-205)) . #0#)) ((((-1089) (-51)) . T)) @@ -3138,15 +3138,15 @@ ((((-1087 |#1| |#2| |#3|)) . T)) ((((-1087 |#1| |#2| |#3|)) . T) (((-1080 |#1| |#2| |#3|)) . T)) ((((-796)) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) ((((-525) |#1|) . T)) ((((-1087 |#1| |#2| |#3|)) |has| |#1| (-341))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-341)) -(((|#3|) . T) ((|#2|) . T) (($) -3321 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) ((|#4|) -3321 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975)))) -(((|#2|) . T) (($) -3321 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((|#3|) -3321 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975)))) +(((|#3|) . T) ((|#2|) . T) (($) -3150 (|has| |#4| (-160)) (|has| |#4| (-786)) (|has| |#4| (-975))) ((|#4|) -3150 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-975)))) +(((|#2|) . T) (($) -3150 (|has| |#3| (-160)) (|has| |#3| (-786)) (|has| |#3| (-975))) ((|#3|) -3150 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-975)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-341)) @@ -3158,37 +3158,37 @@ ((((-796)) . T)) ((((-796)) . T)) (((|#1|) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) ((((-525) |#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-341)) (|has| |#2| (-265 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-842))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) ((((-796)) . T)) ((((-796)) . T)) ((((-796)) . T)) (((|#1| (-497 |#2|)) . T)) -((((-2 (|:| -2019 (-1089)) (|:| -1221 (-51)))) . T)) +((((-2 (|:| -1265 (-1089)) (|:| -1568 (-51)))) . T)) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-712)) . T)) ((((-112 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) -(-3321 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) -(-3321 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) +(-3150 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-842))) +(-3150 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-842))) ((($) . T)) (((|#2| (-497 (-798 |#1|))) . T)) ((((-525) |#1|) . T)) (((|#2|) . T)) (((|#2| (-712)) . T)) -((((-796)) -3321 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) +((((-796)) -3150 (|has| |#1| (-565 (-796))) (|has| |#1| (-1018)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1072) |#1|) . T)) ((((-385 |#2|)) . T)) -((((-2 (|:| -2019 |#1|) (|:| -1221 |#2|))) . T)) +((((-2 (|:| -1265 |#1|) (|:| -1568 |#2|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) ((($) . T) ((|#2|) . T)) @@ -3196,12 +3196,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-265 |#2| |#2|))) (((|#1| (-591 |#1|)) |has| |#1| (-786))) -(-3321 (|has| |#1| (-213)) (|has| |#1| (-327))) -(-3321 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-213)) (|has| |#1| (-327))) +(-3150 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1018)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-929 |#1|)) . T) ((|#1|) . T) (((-525)) -3321 (|has| (-929 |#1|) (-966 (-525))) (|has| |#1| (-966 (-525)))) (((-385 (-525))) -3321 (|has| (-929 |#1|) (-966 (-385 (-525)))) (|has| |#1| (-966 (-385 (-525)))))) +((((-929 |#1|)) . T) ((|#1|) . T) (((-525)) -3150 (|has| (-929 |#1|) (-966 (-525))) (|has| |#1| (-966 (-525)))) (((-385 (-525))) -3150 (|has| (-929 |#1|) (-966 (-385 (-525)))) (|has| |#1| (-966 (-385 (-525)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1018)))) @@ -3212,9 +3212,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1054 |#1| |#2|) #0#) |has| (-1054 |#1| |#2|) (-288 (-1054 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) #0#) |has| (-2 (|:| -2019 |#1|) (|:| -1221 |#2|)) (-288 (-2 (|:| -2019 |#1|) (|:| -1221 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1018))) ((#0=(-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) #0#) |has| (-2 (|:| -1265 |#1|) (|:| -1568 |#2|)) (-288 (-2 (|:| -1265 |#1|) (|:| -1568 |#2|))))) (((#0=(-112 |#1|)) |has| #0# (-288 #0#))) -(-3321 (|has| |#1| (-788)) (|has| |#1| (-1018))) +(-3150 (|has| |#1| (-788)) (|has| |#1| (-1018))) ((($ $) . T)) ((($ $) . T) ((#0=(-798 |#1|) $) . T) ((#0# |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-213)) ((|#2| |#1|) |has| |#1| (-213)) ((|#3| |#1|) . T) ((|#3| $) . T)) |