diff options
author | dos-reis <gdr@axiomatics.org> | 2008-08-08 14:47:57 +0000 |
---|---|---|
committer | dos-reis <gdr@axiomatics.org> | 2008-08-08 14:47:57 +0000 |
commit | 7727c94cc7b39a4ddb33c31ae328f2aa6a32d296 (patch) | |
tree | 682b38ba892d95b5294b37436c04a66efefe61cf /src/share/algebra/category.daase | |
parent | 3efb135761426b4756d3fa22b5353ac17f781ff7 (diff) | |
download | open-axiom-7727c94cc7b39a4ddb33c31ae328f2aa6a32d296.tar.gz |
* algebra/aggcat.spad.pamphlet (part?$SetAggregate): Rename
from <$SetAggregate.
(part?$FiniteSetAggregate): Rename from <$FiniteSetAggregate
* algebra/mset.spad.pamphlet (part?$Multiset): Rename from
<$Mulitset.
* input/mset.input.pamphlet: Adjust.
* input/mset2.input.pamphlet: Likewise.
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r-- | src/share/algebra/category.daase | 1130 |
1 files changed, 565 insertions, 565 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 894b5e47..ba964731 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(143295 . 3425075217) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(143295 . 3427192343) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((|#2| |#2|) . T)) ((((-525)) . T)) -((($ $) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#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)) -((($) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) (|has| |#1| (-844)) ((((-798)) . T)) ((((-798)) . T)) @@ -23,28 +23,28 @@ ((((-205)) . T) (((-798)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) -((($ $) . T) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -(-3254 (|has| |#1| (-762)) (|has| |#1| (-789))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +(-2067 (|has| |#1| (-762)) (|has| |#1| (-789))) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-787)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) |has| |#1| (-1020))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(((|#2| (-458 (-3522 |#1|) (-713))) . T)) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(((|#2| (-458 (-2827 |#1|) (-713))) . T)) (((|#1| (-497 (-1092))) . T)) (((#0=(-805 |#1|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#4| (-346)) (|has| |#3| (-346)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-517)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-798)) . T)) ((((-798)) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +(((|#1|) . T) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1| |#2|) . T)) ((((-798)) . T)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#1|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#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) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) ((($ $) . T)) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) ((($) . T)) (|has| |#1| (-346)) (((|#1|) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) (((|#1| |#1|) . T)) (|has| |#1| (-517)) (((|#2| |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-288 |#2|))) (((-1092) |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-486 (-1092) |#2|)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-787)) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3254 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3254 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-2067 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1020)) @@ -132,21 +132,21 @@ ((((-525)) . T)) ((((-525)) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| (-713)) . T)) (|has| |#2| (-735)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (|has| |#2| (-787)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1075) |#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#3| (-713)) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-1020)) ((((-385 (-525))) . T) (((-525)) . T)) ((((-1092) |#2|) |has| |#2| (-486 (-1092) |#2|)) ((|#2| |#2|) |has| |#2| (-288 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-525)) . T)) ((((-525)) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) ((((-525)) . T)) ((((-525)) . T)) (((#0=(-641) (-1088 #0#)) . T)) @@ -173,12 +173,12 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -189,25 +189,25 @@ ((((-798)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) (|has| |#1| (-341)) (-12 (|has| |#4| (-213)) (|has| |#4| (-977))) (-12 (|has| |#3| (-213)) (|has| |#3| (-977))) -(-3254 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) @@ -218,11 +218,11 @@ (((|#2|) . T) (($) . T) (((-385 (-525))) . T)) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(((|#3| |#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) -(((|#4| |#4|) -3254 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($ $) |has| |#4| (-160))) +(((|#3| |#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) +(((|#4| |#4|) -2067 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($ $) |has| |#4| (-160))) (((|#1|) . T)) (((|#2|) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) @@ -231,21 +231,21 @@ ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525))))) ((((-798)) . T)) -(((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) -(((|#4|) -3254 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($) |has| |#4| (-160))) +(((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) +(((|#4|) -2067 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($) |has| |#4| (-160))) ((((-798)) . T)) ((((-501)) . T) (((-525)) . T) (((-827 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) ((((-385 $) (-385 $)) |has| |#2| (-517)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-844)) ((((-1075) (-51)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-588 (-525))) ((#0#) . T)) ((((-501)) . T) (((-205)) . T) (((-357)) . T) (((-827 (-357))) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) (((|#1|) |has| |#1| (-160))) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-798)) . T)) @@ -256,15 +256,15 @@ (|has| |#1| (-789)) (|has| |#1| (-1020)) (((|#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-125)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-125)) . T)) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-213)) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| (-497 (-760 (-1092)))) . T)) (((|#1| (-904)) . T)) (((#0=(-805 |#1|) $) |has| #0# (-265 #0# #0#))) @@ -273,7 +273,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1068)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (|has| (-1160 |#1| |#2| |#3| |#4|) (-136)) (|has| (-1160 |#1| |#2| |#3| |#4|) (-138)) (|has| |#1| (-136)) @@ -290,20 +290,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-977))) ((((-798)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) #0#) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) #0#) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))))) ((((-525) |#1|) . T)) ((((-798)) . T)) ((((-501)) -12 (|has| |#1| (-567 (-501))) (|has| |#2| (-567 (-501)))) (((-827 (-357))) -12 (|has| |#1| (-567 (-827 (-357)))) (|has| |#2| (-567 (-827 (-357))))) (((-827 (-525))) -12 (|has| |#1| (-567 (-827 (-525)))) (|has| |#2| (-567 (-827 (-525)))))) ((((-798)) . T)) ((((-798)) . T)) ((($) . T)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) ((((-798)) . T)) (|has| (-1159 |#2| |#3| |#4|) (-138)) @@ -314,16 +314,16 @@ ((((-798)) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) (((|#1|) . T)) ((((-525) |#1|) . T)) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) ((((-798)) |has| |#1| (-1020))) -(-3254 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-845 |#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)) -(-3254 (-12 (|has| (-1166 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-2067 (-12 (|has| (-1166 |#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)) -(-3254 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (((|#1|) . T)) ((((-1092)) -12 (|has| |#3| (-835 (-1092))) (|has| |#3| (-977)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) -(-3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) +(-2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($ $) |has| |#1| (-517))) (((#0=(-641) (-1088 #0#)) . T)) ((((-798)) . T)) ((((-798)) . T) (((-1174 |#4|)) . T)) ((((-798)) . T) (((-1174 |#3|)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517))) ((((-798)) . T)) ((($) . T)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1166 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1166 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (((|#3|) |has| |#3| (-977))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-1020)) (((|#2| (-761 |#1|)) . T)) (((|#1|) . T)) @@ -383,37 +383,37 @@ ((((-135)) . T)) (((|#3|) |has| |#3| (-1020)) (((-525)) -12 (|has| |#3| (-968 (-525))) (|has| |#3| (-1020))) (((-385 (-525))) -12 (|has| |#3| (-968 (-385 (-525)))) (|has| |#3| (-1020)))) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) ((((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#2| (-762)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-787)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-501)) |has| |#1| (-567 (-501)))) (((|#1| |#2|) . T)) ((((-1092)) -12 (|has| |#1| (-341)) (|has| |#1| (-835 (-1092))))) ((((-1075) |#1|) . T)) (((|#1| |#2| |#3| (-497 |#3|)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) ((((-798)) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (|has| |#1| (-346)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-525)) . T)) ((((-525)) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((((-798)) . T)) ((((-798)) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) @@ -422,10 +422,10 @@ ((((-525) |#4|) . T)) ((((-525) |#3|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-1160 |#1| |#2| |#3| |#4|)) . T)) ((((-385 (-525))) . T) (((-525)) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -454,38 +454,38 @@ ((($) . T)) ((($ $) . T) ((#0=(-1092) $) . T) ((#0# |#1|) . T)) (((|#2|) |has| |#2| (-160))) -((($) -3254 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) -(((|#2| |#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +((($) -2067 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +(((|#2| |#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) ((((-135)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-346)) (|has| |#2| (-346))) ((((-798)) . T)) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) (((|#1|) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) (|has| $ (-138)) ((((-525) |#1|) . T)) -((($) -3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1092))))) (|has| |#1| (-341)) -(-3254 (-12 (|has| (-1090 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-2067 (-12 (|has| (-1090 |#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| (-713) |#1|))) (((|#1|) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) ((((-525) (-125)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#2| (-497 (-800 |#1|))) . T)) ((((-798)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -502,28 +502,28 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1090 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3254 (|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) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1090 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-977))) (|has| |#1| (-1020)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -2067 (|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) (($ $) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-798)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) (((#0=(-1005) |#1|) . T) ((#0# $) . T) (($ $) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#2|) |has| |#1| (-341))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1020)) (((-525)) -12 (|has| |#2| (-968 (-525))) (|has| |#2| (-1020))) (((-385 (-525))) -12 (|has| |#2| (-968 (-385 (-525)))) (|has| |#2| (-1020)))) @@ -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)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#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| (-713) (-1005)) . T)) ((((-385 (-525))) |has| |#2| (-341)) (($) . T)) (((|#1| (-497 (-1010 (-1092))) (-1010 (-1092))) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#2| (-735)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) @@ -588,63 +588,63 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#2|) . T) (((-525)) |has| |#2| (-968 (-525))) (((-385 (-525))) |has| |#2| (-968 (-385 (-525))))) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((|#2|) . T)) -((((-798)) -3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) +((((-798)) -2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) (((|#1|) |has| |#1| (-160))) ((((-525)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-525) (-135)) . T)) -((($) -3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +((($) -2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((|#2|) |has| |#1| (-341))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| (-497 #0=(-1092)) #0#) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-160)) (|has| |#3| (-160)) (((#0=(-385 (-887 |#1|)) #0#) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1| |#1|) |has| |#1| (-160))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|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| (-1020)))) (((|#1|) . T)) ((((-385 (-887 |#1|))) . T)) ((((-525) (-125)) . T)) (((|#1|) |has| |#1| (-160))) ((((-125)) . T)) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-798)) . T)) ((((-1160 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-977)) (((-525)) -12 (|has| |#1| (-588 (-525))) (|has| |#1| (-977)))) (((|#1| |#2|) . T)) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (|has| |#3| (-735)) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) (|has| |#3| (-787)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) (((|#2|) . T)) ((((-525) (-125)) . T)) ((((-798)) . T)) @@ -660,22 +660,22 @@ (|has| |#1| (-1020)) (((|#2|) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) -(((|#4|) -3254 (|has| |#4| (-160)) (|has| |#4| (-341)))) -(((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#4|) -2067 (|has| |#4| (-160)) (|has| |#4| (-341)))) +(((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)))) ((((-798)) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) ((($ $) . T) ((#0=(-1092) $) |has| |#1| (-213)) ((#0# |#1|) |has| |#1| (-213)) ((#1=(-760 (-1092)) |#1|) . T) ((#1# $) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) ((((-525) |#2|) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -((($) -3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) +((($) -2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) ((((-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 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-366) (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-366) (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#2| (-1068)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((|#1|) . T)) ((((-366) (-1075)) . T)) (|has| |#1| (-517)) ((((-112 |#1|)) . T)) ((((-125)) . T)) ((((-525) |#1|) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T)) ((((-798)) . T)) ((((-761 |#1|)) . T)) @@ -716,7 +716,7 @@ (((|#1|) |has| |#1| (-160))) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#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)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) @@ -737,9 +737,9 @@ ((((-1090 |#1| |#2| |#3|) $) -12 (|has| (-1090 |#1| |#2| |#3|) (-265 (-1090 |#1| |#2| |#3|) (-1090 |#1| |#2| |#3|))) (|has| |#1| (-341))) (($ $) . T)) ((((-798)) . T)) ((((-798)) . T)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((($ $) . T)) ((($ $) . T)) ((((-798)) . T)) @@ -749,12 +749,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525) (-135)) . T)) ((((-135)) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((((-108)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-108)) . T)) @@ -762,38 +762,38 @@ ((((-501)) |has| |#1| (-567 (-501))) (((-205)) . #0=(|has| |#1| (-953))) (((-357)) . #0#)) ((((-798)) . T)) (|has| |#1| (-762)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#1| (-789)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-517)) (|has| |#1| (-844)) (((|#1|) . T)) (|has| |#1| (-1020)) ((((-798)) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1| (-1174 |#1|) (-1174 |#1|)) . T)) ((((-525) (-135)) . T)) ((($) . T)) -(-3254 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (|has| |#1| (-1020)) (((|#1| (-904)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3254 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) (((|#1|) . T)) (|has| |#2| (-735)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#2| (-787)) @@ -808,7 +808,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) (|has| |#1| (-770)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (|has| |#1| (-1020)) @@ -819,8 +819,8 @@ (((|#3|) |has| |#3| (-1020))) (|has| |#3| (-346)) (((|#1|) . T) (((-798)) . T)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((((-798)) . 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)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) ((((-135)) . T)) (((|#1|) . T)) ((((-135)) . T)) -((($) -3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +((($) -2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) ((((-135)) . T)) (((|#1| |#2| |#3|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (|has| $ (-138)) (|has| $ (-138)) (|has| |#1| (-1020)) ((((-798)) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) ((($ $) |has| |#1| (-265 $ $)) ((|#1| $) |has| |#1| (-265 |#1| |#1|))) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) ((((-1092)) . T)) (|has| |#1| (-517)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|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| (-787)) -(((|#2| (-220 (-3522 |#1|) (-713)) (-800 |#1|)) . T)) +(((|#2| (-220 (-2827 |#1|) (-713)) (-800 |#1|)) . T)) (|has| |#3| (-787)) (((|#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| (-1020)))) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-327)) (|has| |#1| (-346))) ((((-1059 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-160)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-641)) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#1| (-517)) (((|#1|) . T)) (((|#1|) . T)) @@ -914,10 +914,10 @@ (((|#1| (-385 (-525))) . T)) (((|#3|) . T) (((-565 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((#0=(-1090 |#1| |#2| |#3|) #0#) -12 (|has| (-1090 |#1| |#2| |#3|) (-288 (-1090 |#1| |#2| |#3|))) (|has| |#1| (-341))) (((-1092) #0#) -12 (|has| (-1090 |#1| |#2| |#3|) (-486 (-1092) (-1090 |#1| |#2| |#3|))) (|has| |#1| (-341)))) @@ -925,8 +925,8 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))))) ((((-798)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -937,10 +937,10 @@ ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) (|has| |#1| (-770)) (|has| |#1| (-1020)) -(((|#2| |#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)))) -((((-525) (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +(((|#2| |#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)))) +((((-525) (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) ((((-713)) . T)) ((((-525)) . T)) (|has| |#1| (-517)) @@ -953,29 +953,29 @@ ((((-112 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-138)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-827 (-525))) . T) (((-827 (-357))) . T) (((-501)) . T) (((-1092)) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((($) . T)) ((((-798)) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#2|) |has| |#2| (-160))) -((($) -3254 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -2067 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) ((((-805 |#1|)) . T)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (-12 (|has| |#3| (-213)) (|has| |#3| (-977))) (|has| |#2| (-1068)) -(((#0=(-51)) . T) (((-2 (|:| -3364 (-1092)) (|:| -4201 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1556 (-1092)) (|:| -3448 #0#))) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) (((|#1| (-525) (-1005)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| (-385 (-525)) (-1005)) . T)) -((($) -3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|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))) ((((-798)) . T)) ((((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) (|has| |#1| (-327)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($) . T)) ((((-798)) . T)) (((|#1|) . T)) ((((-805 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) ((((-798)) . T)) -(((|#3| |#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) +(((|#3| |#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) (|has| |#1| (-953)) ((((-798)) . T)) -(((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) +(((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) ((((-525) (-108)) . T)) (((|#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-346)) @@ -1021,31 +1021,31 @@ (|has| |#1| (-346)) ((((-1092) $) |has| |#1| (-486 (-1092) $)) (($ $) |has| |#1| (-288 $)) ((|#1| |#1|) |has| |#1| (-288 |#1|)) (((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|))) ((((-1092)) |has| |#1| (-835 (-1092)))) -(-3254 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) +(-2067 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) ((((-366) (-1039)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-366) |#1|) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1020)) ((((-798)) . T)) ((((-798)) . T)) ((((-845 |#1|)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) (((#0=(-805 |#1|)) |has| #0# (-288 #0#))) (((|#1| |#2|) . T)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (((|#1|) . T)) (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#1| (-1114)) (((#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#) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -1072,14 +1072,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-787)) (|has| |#1| (-787)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) -(((#0=(-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) #0#) |has| (-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))))) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) +(((#0=(-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) #0#) |has| (-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))))) ((($) . T)) (|has| |#2| (-789)) ((($) . T)) (((|#2|) |has| |#2| (-1020))) -((((-798)) -3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) +((((-798)) -2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) (|has| |#1| (-789)) (|has| |#1| (-789)) ((((-1075) (-51)) . T)) @@ -1087,10 +1087,10 @@ ((((-798)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-588 (-525))) ((#0#) . T)) ((((-525) (-135)) . T)) -((((-525) (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T) ((|#1| |#2|) . T)) ((((-385 (-525))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-798)) . T)) ((((-845 |#1|)) . T)) (|has| |#1| (-341)) @@ -1115,31 +1115,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-160))) -((((-525) (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -1556 |#1|) (|:| -3448 |#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| (-1020)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-160))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) (((|#1|) . T)) ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525))))) ((((-798)) . T)) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#2| (-787)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) (|has| |#1| (-517)) (|has| |#1| (-1068)) ((((-1075) |#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-525))) (((-525)) |has| |#1| (-968 (-525))) (((-1092)) |has| |#1| (-968 (-1092))) ((|#1|) . T)) ((((-525) |#2|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1|) . T)) ((((-592 |#4|)) . T) (((-798)) . T)) ((((-501)) |has| |#4| (-567 (-501)))) @@ -1152,17 +1152,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1092)) |has| (-385 |#2|) (-835 (-1092)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-798)) -3254 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-566 (-798))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) (((-1174 |#3|)) . T)) +((((-798)) -2067 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-566 (-798))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) (((-1174 |#3|)) . T)) ((((-525) |#2|) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(((|#2| |#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(((|#2| |#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T) ((|#2|) . T)) ((((-798)) . T)) ((((-798)) . T)) ((((-1075) (-1092) (-525) (-205) (-798)) . T)) @@ -1197,8 +1197,8 @@ (|has| |#1| (-37 (-385 (-525)))) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) (|has| $ (-138)) ((((-385 |#2|)) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-968 (-385 (-525)))) (((-525)) |has| #0# (-968 (-525))) ((#0#) . T)) @@ -1209,11 +1209,11 @@ (((|#3|) |has| |#3| (-160))) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) @@ -1244,7 +1244,7 @@ ((((-931 |#1|)) . T) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-385 (-525))) . T) (((-385 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1088 |#1|)) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) @@ -1252,9 +1252,9 @@ (|has| |#1| (-789)) (((|#2|) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) ((((-525) |#2|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#2|) . T)) ((((-525) |#3|) . T)) (((|#2|) . T)) @@ -1269,7 +1269,7 @@ (((|#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-341)) (((|#2|) . T) (((-525)) |has| |#2| (-968 (-525))) (((-385 (-525))) |has| |#2| (-968 (-385 (-525))))) @@ -1299,19 +1299,19 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#2|) . T)) ((((-525) (-135)) . T)) -(((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-789)) (((|#2| (-713) (-1005)) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-733)) (((|#1|) |has| |#1| (-160))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) -(-3254 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) +(-2067 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) +(-2067 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) (((|#4|) . T)) (|has| |#1| (-136)) ((((-1075) |#1|) . T)) @@ -1324,10 +1324,10 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#3|) . T)) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020))) (((-892 |#1|)) . T)) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020))) (((-892 |#1|)) . T)) (|has| |#1| (-787)) (|has| |#1| (-787)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -1340,8 +1340,8 @@ ((($) . T)) ((((-366) (-1075)) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-798)) -3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3364 (-1075)) (|:| -4201 #0#))) . T)) +((((-798)) -2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1174 |#2|)) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1556 (-1075)) (|:| -3448 #0#))) . T)) (((|#1|) . T)) ((((-798)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) @@ -1349,7 +1349,7 @@ (|has| |#2| (-136)) (|has| |#2| (-138)) (|has| |#1| (-450)) -(-3254 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) (|has| |#1| (-341)) ((((-798)) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -1358,8 +1358,8 @@ (|has| |#1| (-787)) (|has| |#1| (-787)) ((((-798)) . T)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1166 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1092)) |has| |#1| (-835 (-1092)))) @@ -1367,7 +1367,7 @@ ((((-798)) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) -(((|#2| (-458 (-3522 |#1|) (-713)) (-800 |#1|)) . T)) +(((|#2| (-458 (-2827 |#1|) (-713)) (-800 |#1|)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1| (-497 (-1092)) (-1092)) . T)) (((|#1|) . T)) @@ -1387,16 +1387,16 @@ (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) ((((-1090 |#1| |#2| |#3|)) |has| |#1| (-341))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-1092) (-51)) . T)) ((($ $) . T)) (((|#1| (-525)) . T)) ((((-845 |#1|)) . T)) -(((|#1|) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977))) (($) -3254 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)))) +(((|#1|) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977))) (($) -2067 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)))) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) (|has| |#1| (-789)) (|has| |#1| (-789)) @@ -1411,13 +1411,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#1|) |has| |#1| (-160))) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) -(((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#2| (-789)) (|has| |#1| (-789)) -(-3254 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-844))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-525) |#2|) . T)) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)))) (|has| |#1| (-327)) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) ((($) . T) (((-385 (-525))) . T)) @@ -1425,7 +1425,7 @@ (|has| |#1| (-762)) (|has| |#1| (-762)) (((|#1|) . T)) -(-3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-787)) (|has| |#1| (-787)) (|has| |#1| (-787)) @@ -1434,13 +1434,13 @@ ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-1092)) |has| |#1| (-835 (-1092))) (((-1005)) . T)) (((|#1|) . T)) (|has| |#1| (-787)) -(((#0=(-2 (|:| -3364 (-1075)) (|:| -4201 (-51))) #0#) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))))) +(((#0=(-2 (|:| -1556 (-1075)) (|:| -3448 (-51))) #0#) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#1| (-1020)) (((|#1|) . T)) @@ -1459,7 +1459,7 @@ (((|#1|) . T)) ((((-135)) . T)) (((|#2|) |has| |#2| (-160))) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((|#1|) . T)) (|has| |#1| (-136)) (|has| |#1| (-138)) @@ -1481,32 +1481,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) #0#) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))))) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) #0#) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#1| (-789)) (|has| |#1| (-517)) ((((-538 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-3254 (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-789)))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-789)))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-845 |#1|)) . T)) (((|#1| (-469 |#1| |#3|) (-469 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-713)) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1090 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((((-617 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1514,17 +1514,17 @@ ((((-798)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#2|) . T)) -(-3254 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (|has| |#1| (-1114)) (|has| |#1| (-1114)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (|has| |#1| (-1114)) (|has| |#1| (-1114)) (((|#3| |#3|) . T)) @@ -1537,43 +1537,43 @@ (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((((-1075) (-51)) . T)) (|has| |#1| (-1020)) -(-3254 (|has| |#2| (-762)) (|has| |#2| (-789))) +(-2067 (|has| |#2| (-762)) (|has| |#2| (-789))) (((|#1|) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) (((|#1|) |has| |#1| (-160)) (($) . T)) ((($) . T)) ((((-1090 |#1| |#2| |#3|)) -12 (|has| (-1090 |#1| |#2| |#3|) (-288 (-1090 |#1| |#2| |#3|))) (|has| |#1| (-341)))) ((((-798)) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((($) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) (|has| |#2| (-844)) (|has| |#1| (-341)) (((|#2|) |has| |#2| (-1020))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((($) . T) ((|#2|) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) (|has| |#1| (-844)) (|has| |#1| (-844)) ((((-501)) . T) (((-385 (-1088 (-525)))) . T) (((-205)) . T) (((-357)) . T)) ((((-357)) . T) (((-205)) . T) (((-798)) . T)) (|has| |#1| (-844)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) ((($ $) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((($ $) . T)) ((((-525) (-108)) . T)) ((($) . T)) (((|#1|) . T)) ((((-525)) . T)) ((((-108)) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-37 (-385 (-525)))) (((|#1| (-525)) . T)) ((($) . T)) @@ -1595,7 +1595,7 @@ (((|#1| (-1138 |#1| |#2| |#3|)) . T)) (((|#1| (-713)) . T)) (((|#1|) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) ((((-1075) |#1|) . T)) @@ -1615,18 +1615,18 @@ (((|#1|) . T)) ((((-525)) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-798)) . T)) (((|#3|) . T)) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) ((((-1159 |#2| |#3| |#4|)) . T) (((-1160 |#1| |#2| |#3| |#4|)) . T)) ((((-798)) . T)) -((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (((-565 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) -3254 (-12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (|has| |#1| (-968 (-385 (-525))))) (((-385 (-887 |#1|))) |has| |#1| (-517)) (((-887 |#1|)) |has| |#1| (-977)) (((-1092)) . T)) +((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (((-565 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) -2067 (-12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (|has| |#1| (-968 (-385 (-525))))) (((-385 (-887 |#1|))) |has| |#1| (-517)) (((-887 |#1|)) |has| |#1| (-977)) (((-1092)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-713)) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-288 |#1|))) ((((-1160 |#1| |#2| |#3| |#4|)) . T)) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) @@ -1634,14 +1634,14 @@ (|has| |#1| (-517)) (((|#1|) . T)) ((((-798)) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#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| (-1020)))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1020))) -(((|#2|) -3254 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -2067 (|has| |#2| (-160)) (|has| |#2| (-341)))) ((((-1159 |#2| |#3| |#4|)) . T)) ((((-108)) . T)) (|has| |#1| (-762)) @@ -1651,8 +1651,8 @@ (|has| |#1| (-787)) (|has| |#1| (-787)) (((|#1| (-525) (-1005)) . T)) -(-3254 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +(-2067 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1| (-385 (-525)) (-1005)) . T)) (((|#1| (-713) (-1005)) . T)) (|has| |#1| (-789)) @@ -1668,28 +1668,28 @@ (((|#1|) . T)) (|has| |#1| (-1020)) ((((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-588 (-525)))) ((|#2|) |has| |#1| (-341))) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) ((((-798)) . T)) (|has| |#3| (-787)) ((((-798)) . T)) ((((-1159 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-798)) . T)) -(((|#1| |#1|) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) +(((|#1| |#1|) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) (((|#1|) . T)) ((((-525)) . T)) ((((-525)) . T)) -(((|#1|) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) +(((|#1|) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) (((|#2|) |has| |#2| (-341))) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-789)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) |has| (-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-844))) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) |has| (-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-844))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) ((((-798)) . T)) ((((-798)) . T)) @@ -1724,18 +1724,18 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (((|#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-798)) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| (-385 |#2|) (-213)) (|has| |#1| (-844)) (((|#2|) |has| |#2| (-977))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (|has| |#1| (-341)) (((|#1|) |has| |#1| (-160))) (((|#1| |#1|) . T)) @@ -1760,7 +1760,7 @@ (((|#1| (-385 (-525)) (-1005)) . T)) (((|#1| (-713) (-1005)) . T)) (((#0=(-385 |#2|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -(((|#1|) . T) (((-525)) -3254 (|has| (-385 (-525)) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) . T)) +(((|#1|) . T) (((-525)) -2067 (|has| (-385 (-525)) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) . T)) (((|#1| (-556 |#1| |#3|) (-556 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) @@ -1779,24 +1779,24 @@ ((((-641)) . T)) (((|#2|) |has| |#2| (-160))) (|has| |#2| (-787)) -((((-108)) |has| |#1| (-1020)) (((-798)) -3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020)))) +((((-108)) |has| |#1| (-1020)) (((-798)) -2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))) . T)) ((((-798)) . T)) ((((-525) |#1|) . T)) ((((-641)) . T) (((-385 (-525))) . T) (((-525)) . T)) (((|#1| |#1|) |has| |#1| (-160))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) ((((-357)) . T)) ((((-641)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1|) |has| |#1| (-160))) ((((-385 (-887 |#1|))) . T)) (((|#2| |#2|) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T)) (|has| |#2| (-789)) (((|#3|) |has| |#3| (-977))) @@ -1806,14 +1806,14 @@ (|has| |#1| (-789)) ((((-1092)) |has| |#2| (-835 (-1092)))) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-450)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) (|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| (-789)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#2|) . T)) (((|#3|) . T)) ((((-112 |#1|)) . T)) @@ -1856,11 +1856,11 @@ ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525)))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-357)) . #0=(|has| |#1| (-953))) (((-205)) . #0#)) (((|#1|) |has| |#1| (-341))) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((($ $) . T) (((-565 $) $) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T) (((-1160 |#1| |#2| |#3| |#4|)) . T) (((-385 (-525))) . T)) -((($) -3254 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-517))) +((($) -2067 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((|#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| (-1020)))) ((((-798)) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-844))) (((|#1|) . T)) (|has| |#1| (-789)) (|has| |#1| (-789)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (|has| |#1| (-1020)) @@ -1884,13 +1884,13 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((((-525)) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((#0=(-1159 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525)))) (($) . T)) ((((-525)) . T)) (|has| |#1| (-341)) -(-3254 (-12 (|has| (-1166 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3254 (-12 (|has| (-1166 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-2067 (-12 (|has| (-1166 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-2067 (-12 (|has| (-1166 |#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| (-588 (-525)))) (((|#3|) |has| |#3| (-160))) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) ((((-525)) . T)) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-385 (-525))) . T) (($) . T) (((-385 |#1|)) . T) ((|#1|) . T)) ((((-798)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) ((($) . T)) ((((-525) |#1|) . T)) ((((-1092)) |has| (-385 |#2|) (-835 (-1092)))) -(((|#1|) . T) (($) -3254 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) +(((|#1|) . T) (($) -2067 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) ((((-501)) |has| |#2| (-567 (-501)))) ((((-632 |#2|)) . T) (((-798)) . T)) (((|#1|) . T)) @@ -1926,8 +1926,8 @@ (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) ((((-805 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3254 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) ((((-798)) . T)) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) @@ -1943,17 +1943,17 @@ ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-1132))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-1132))) ((($) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-968 (-385 (-525)))) (((-525)) |has| #0# (-968 (-525))) ((#0#) . T)) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (((|#1| (-713)) . T)) (|has| |#1| (-789)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-525)) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))))) +((((-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#1| (-787)) (|has| |#1| (-37 (-385 (-525)))) @@ -1978,24 +1978,24 @@ (((|#1| |#2|) . T)) ((((-135)) . T)) ((((-722 |#1| (-800 |#2|))) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (|has| |#1| (-1114)) (((|#1|) . T)) -(-3254 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) +(-2067 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) ((((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|))) (((|#2|) . T)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-845 |#1|)) . T)) ((($) . T)) ((((-385 (-887 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-501)) |has| |#4| (-567 (-501)))) ((((-798)) . T) (((-592 |#4|)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-787)) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) |has| (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|)) (-288 (-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) |has| (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|)) (-288 (-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))))) (|has| |#1| (-1020)) (|has| |#1| (-341)) (|has| |#1| (-789)) @@ -2003,16 +2003,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-385 (-525))) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (|has| |#1| (-136)) (|has| |#1| (-138)) -(-3254 (-12 (|has| (-1090 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3254 (-12 (|has| (-1090 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-2067 (-12 (|has| (-1090 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-2067 (-12 (|has| (-1090 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) (|has| |#1| (-787)) (((|#1| |#2|) . T)) @@ -2035,9 +2035,9 @@ ((((-798)) . T)) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(((|#1|) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)))) +(((|#1|) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)))) ((((-294 |#1|)) . T)) (((|#2|) |has| |#2| (-341))) (((|#2|) . T)) @@ -2058,13 +2058,13 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((($ $) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) (|has| |#1| (-517)) (((|#2|) . T)) ((((-525)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2073,7 +2073,7 @@ ((($) . T)) (((|#1|) . T)) ((((-798)) . T)) -(((|#2|) |has| |#2| (-6 (-4260 "*")))) +(((|#2|) |has| |#2| (-6 (-4261 "*")))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2090,12 +2090,12 @@ (((|#1| |#2|) . T)) ((((-1092) |#1|) . T)) (((|#4|) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-1092) (-51)) . T)) ((((-1159 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-798)) . T)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((#0=(-1160 |#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| (-1020)))) (((|#2| |#3|) . T)) -(-3254 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1| (-497 |#2|)) . T)) (((|#1| (-713)) . T)) (((|#1| (-497 (-1010 (-1092)))) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (|has| |#2| (-844)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) ((((-798)) . T)) ((($ $) . T) ((#0=(-1159 |#2| |#3| |#4|) #0#) . T) ((#1=(-385 (-525)) #1#) |has| #0# (-37 (-385 (-525))))) ((((-845 |#1|)) . T)) @@ -2130,13 +2130,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (|has| |#1| (-341)) ((($) . T) ((#0=(-1159 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1090 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3254 (-12 (|has| |#1| (-286)) (|has| |#1| (-844))) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3254 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) +(-2067 (-12 (|has| |#1| (-286)) (|has| |#1| (-844))) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-835 (-1092))) (|has| |#1| (-977))) ((((-525)) |has| |#1| (-588 (-525))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-798)) . T)) @@ -2168,27 +2168,27 @@ (((|#1|) |has| |#1| (-160))) ((((-798)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) -(((|#2|) -3254 (|has| |#2| (-6 (-4260 "*"))) (|has| |#2| (-160)))) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(((|#2|) -2067 (|has| |#2| (-6 (-4261 "*"))) (|has| |#2| (-160)))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#1| (-844)) (((|#2|) |has| |#2| (-160))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-798)) . T)) ((((-798)) . T)) ((((-501)) . T) (((-525)) . T) (((-827 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))) . T)) (((|#1|) . T)) ((((-798)) . T)) (((|#1| |#2|) . T)) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-269)) (|has| |#1| (-341))) +(-2067 (|has| |#1| (-269)) (|has| |#1| (-341))) ((((-135)) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) (|has| |#1| (-787)) @@ -2203,7 +2203,7 @@ ((((-385 (-525))) . T) (($) . T)) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -2214,7 +2214,7 @@ (((|#1|) . T)) ((((-592 (-135))) . T) (((-1075)) . T)) ((((-798)) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) ((((-1092) |#1|) |has| |#1| (-486 (-1092) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-789)) ((((-798)) . T)) @@ -2226,16 +2226,16 @@ ((((-798)) . T) (((-592 |#4|)) . T)) (((|#2|) . T)) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3254 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-1092) (-51)) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#1| (-844)) (|has| |#1| (-844)) (((|#2|) . T)) @@ -2250,12 +2250,12 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#1| (-762)) (((#0=(-845 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((((-385 |#2|)) . T)) (|has| |#1| (-787)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) ((#1=(-525) #1#) . T) (($ $) . T)) ((((-845 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) @@ -2265,25 +2265,25 @@ (|has| |#1| (-136)) (((|#2|) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3364 (-1092)) (|:| -4201 #0#))) . T)) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -1556 (-1092)) (|:| -3448 #0#))) . T)) (|has| |#1| (-327)) ((((-525)) . T)) ((((-798)) . T)) (((#0=(-1160 |#1| |#2| |#3| |#4|) $) |has| #0# (-265 #0# #0#))) (|has| |#1| (-341)) (((#0=(-1005) |#1|) . T) ((#0# $) . T) (($ $) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (((#0=(-385 (-525)) #0#) . T) ((#1=(-641) #1#) . T) (($ $) . T)) ((((-294 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-1020)) (((|#1|) . T)) -(((|#1|) -3254 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) -(((|#1|) -3254 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -2067 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -2067 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) (((|#2|) . T)) ((((-385 (-525))) . T) (((-641)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2302,7 +2302,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-525)) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2339,7 +2339,7 @@ (|has| |#2| (-953)) ((($) . T)) (|has| |#1| (-844)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2347,24 +2347,24 @@ ((($) . T)) (|has| |#1| (-341)) ((((-845 |#1|)) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3254 (|has| |#1| (-346)) (|has| |#1| (-789))) +(-2067 (|has| |#1| (-346)) (|has| |#1| (-789))) (((|#1|) . T)) ((((-798)) . T)) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1092))))) ((((-385 |#2|) |#3|) . T)) ((($) . T) (((-385 (-525))) . T)) ((((-713) |#1|) . T)) -(((|#2| (-220 (-3522 |#1|) (-713))) . T)) +(((|#2| (-220 (-2827 |#1|) (-713))) . T)) (((|#1| (-497 |#3|)) . T)) ((((-385 (-525))) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-798)) . T)) -(((#0=(-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) #0#) |has| (-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))))) +(((#0=(-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) #0#) |has| (-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))))) (|has| |#1| (-844)) (|has| |#2| (-341)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-798)) . T)) (((|#1|) . T)) @@ -2381,11 +2381,11 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) (-12 (|has| |#1| (-510)) (|has| |#1| (-770))) ((((-798)) . T)) -((((-1092)) -3254 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-835 (-1092)))))) +((((-1092)) -2067 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-835 (-1092)))))) (|has| |#1| (-341)) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1092))))) (|has| |#1| (-341)) @@ -2395,7 +2395,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-341))) (((|#2|) |has| |#1| (-341))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#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| (-821 (-357)))) (((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-821 (-525))))) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (|has| |#1| (-517)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#3|) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#2|) . T)) (((|#2|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) ((((-1075) |#1|) . T)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-2067 (|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)))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-798)) . T)) ((($) . T)) @@ -2475,7 +2475,7 @@ (|has| |#1| (-733)) (|has| |#1| (-733)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-110)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2496,7 +2496,7 @@ ((((-525)) . T)) ((((-798)) . T)) ((((-525)) . T)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -2508,9 +2508,9 @@ (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-341)) (|has| |#1| (-341)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1092))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) (|has| |#1| (-1068)) ((((-525) |#1|) . T)) (((|#1|) . T)) @@ -2528,8 +2528,8 @@ (((|#1|) . T)) (|has| |#1| (-517)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-357)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2538,7 +2538,7 @@ (|has| |#1| (-517)) (|has| |#1| (-1020)) ((((-722 |#1| (-800 |#2|))) |has| (-722 |#1| (-800 |#2|)) (-288 (-722 |#1| (-800 |#2|))))) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-844)) @@ -2548,12 +2548,12 @@ (|has| |#1| (-213)) (((|#1| (-497 (-1010 (-1092)))) . T)) (|has| |#2| (-341)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) ((((-798)) . T)) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) @@ -2562,8 +2562,8 @@ ((((-525)) . T)) (((|#3|) . T)) ((((-798)) . T)) -(-3254 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3254 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-2067 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((#0=(-538 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1|) |has| |#1| (-160))) @@ -2571,12 +2571,12 @@ ((((-538 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) ((($) . T) (((-385 (-525))) . T)) ((($) . T) (((-385 (-525))) . T)) -(((|#2|) |has| |#2| (-6 (-4260 "*")))) +(((|#2|) |has| |#2| (-6 (-4261 "*")))) (((|#1|) . T)) (((|#1|) . T)) ((((-798)) |has| |#1| (-566 (-798)))) ((((-273 |#3|)) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#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)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-844)) (|has| |#1| (-844)) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-2 (|:| -3364 (-1075)) (|:| -4201 |#1|))) . T)) +((((-2 (|:| -1556 (-1075)) (|:| -3448 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2611,10 +2611,10 @@ (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((#0=(-385 (-525)) #0#) . T)) ((((-385 (-525))) . T)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1|) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-501)) . T)) ((((-798)) . T)) ((((-1092)) |has| |#2| (-835 (-1092))) (((-1005)) . T)) @@ -2629,12 +2629,12 @@ ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-1092)) |has| |#1| (-835 (-1092)))) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-517)))) (|has| |#1| (-517)) (((|#1|) |has| |#1| (-341))) ((((-525)) . T)) @@ -2653,8 +2653,8 @@ ((((-798)) . T)) (|has| |#2| (-762)) (|has| |#2| (-762)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) @@ -2680,12 +2680,12 @@ (((|#2| (-713)) . T)) ((((-1092)) . T)) ((((-805 |#1|)) . T)) -(-3254 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3254 (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (-12 (|has| |#1| (-789)) (|has| |#2| (-789)))) +(-2067 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-2067 (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (-12 (|has| |#1| (-789)) (|has| |#2| (-789)))) ((((-805 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-346)) @@ -2711,7 +2711,7 @@ (((|#1|) . T)) ((((-798)) . T)) (|has| |#2| (-844)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) ((((-798)) . T)) ((((-798)) . T)) @@ -2744,11 +2744,11 @@ ((((-385 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1020)) -(((|#2| (-458 (-3522 |#1|) (-713))) . T)) +(((|#2| (-458 (-2827 |#1|) (-713))) . T)) ((((-525) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-497 (-1092))) . T)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-525)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2758,9 +2758,9 @@ ((($) . T) (((-385 (-525))) . T)) ((($) . T)) ((($) . T)) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) ((((-135)) . T)) (((|#1|) . T) (((-385 (-525))) . T)) @@ -2800,27 +2800,27 @@ (|has| |#1| (-213)) (((|#1| (-497 |#3|)) . T)) (|has| |#1| (-346)) -(((|#2| (-220 (-3522 |#1|) (-713))) . T)) +(((|#2| (-220 (-2827 |#1|) (-713))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (((|#1|) . T) (($) . T)) (((|#1| (-497 |#2|)) . T)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| (-713)) . T)) (|has| |#1| (-517)) -(-3254 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-798)) . T)) -(-3254 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) -(-3254 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-2067 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1|) |has| |#1| (-160))) (((|#4|) |has| |#4| (-977))) (((|#3|) |has| |#3| (-977))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) @@ -2833,14 +2833,14 @@ (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) (((|#1|) . T)) (|has| |#2| (-341)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#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) (($) -3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#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)) @@ -2859,25 +2859,25 @@ (((|#1|) |has| |#2| (-395 |#1|))) (((|#1|) |has| |#2| (-395 |#1|))) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-798)) . T)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) |has| (-2 (|:| -3364 (-1092)) (|:| -4201 (-51))) (-288 (-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))))) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) |has| (-2 (|:| -1556 (-1092)) (|:| -3448 (-51))) (-288 (-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-525) |#1|) . T)) (((|#1|) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-1092)) |has| |#1| (-835 (-1092))) (((-760 (-1092))) . T)) -(-3254 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-761 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-798)) . T)) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) ((((-798)) . T)) @@ -2885,15 +2885,15 @@ (((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517)) (((-385 (-525))) |has| |#1| (-517))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (-12 (|has| |#1| (-341)) (|has| |#2| (-213)))) +(-2067 (|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#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-525) |#1|) . T)) ((((-294 |#1|)) . T)) (((#0=(-641) (-1088 #0#)) . T)) -((((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-787)) ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) @@ -2910,12 +2910,12 @@ (((#0=(-1160 |#1| |#2| |#3| |#4|)) |has| #0# (-288 #0#))) ((($) . T)) (((|#1|) . T)) -((($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (|has| |#2| (-213)) (|has| $ (-138)) ((((-798)) . T)) -((($) . T) (((-385 (-525))) -3254 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -2067 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-798)) . T)) (|has| |#1| (-787)) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092))))) @@ -2927,23 +2927,23 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#4|) . T)) (|has| |#1| (-517)) -((($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) -((((-1092)) -3254 (-12 (|has| (-1166 |#1| |#2| |#3|) (-835 (-1092))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))))) -(((|#1|) . T) (($) -3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3254 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) +((((-1092)) -2067 (-12 (|has| (-1166 |#1| |#2| |#3|) (-835 (-1092))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))))) +(((|#1|) . T) (($) -2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -2067 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1092))))) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-713) |#1|))) (|has| |#1| (-835 (-1092))))) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) ((((-525) |#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1|) . T)) (((|#1| (-497 (-760 (-1092)))) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3254 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) ((($) . T) (((-805 |#1|)) . T) (((-385 (-525))) . T)) ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) @@ -2952,15 +2952,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 |#2|)) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-525)) . T)) @@ -2989,32 +2989,32 @@ ((((-1166 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1092)) . T) (((-798)) . T)) (|has| |#1| (-341)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-1024)) . T)) ((((-798)) . T)) -((($) -3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) -((($) -3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-844)) (|has| |#1| (-844)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-160))) ((((-641)) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-160))) ((((-385 (-525))) . T) (($) . T)) (((|#1| (-525)) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-341)) (|has| |#1| (-341)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3254 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-160)) (|has| |#1| (-517))) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-713)) . T)) @@ -3029,16 +3029,16 @@ ((((-827 (-357))) . T) (((-827 (-525))) . T) (((-1092)) . T) (((-501)) . T)) (((|#1|) . T)) ((((-798)) . T)) -(-3254 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3254 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-2067 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) ((((-525)) . T)) ((((-525)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-3254 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-2067 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-1092)) -12 (|has| |#2| (-835 (-1092))) (|has| |#2| (-977)))) -(-3254 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) +(-2067 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-341)) @@ -3062,7 +3062,7 @@ ((((-1075) (-1092) (-525) (-205) (-798)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-3254 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-2067 (|has| |#1| (-327)) (|has| |#1| (-346))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-798)) . T)) @@ -3070,7 +3070,7 @@ ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-1020)) (((-525)) -12 (|has| |#2| (-968 (-525))) (|has| |#2| (-1020))) (((-385 (-525))) -12 (|has| |#2| (-968 (-385 (-525)))) (|has| |#2| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((($) . T) (((-385 (-525))) . T)) (|has| |#1| (-844)) (|has| |#1| (-844)) @@ -3079,14 +3079,14 @@ ((((-798)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-160))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) (((|#2|) . T)) -(-3254 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-2067 (|has| |#1| (-21)) (|has| |#1| (-787))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (((|#1|) . T)) -((((-798)) -3254 (-12 (|has| |#1| (-566 (-798))) (|has| |#2| (-566 (-798)))) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))))) +((((-798)) -2067 (-12 (|has| |#1| (-566 (-798))) (|has| |#2| (-566 (-798)))) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))))) ((((-385 |#2|) |#3|) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -3098,17 +3098,17 @@ (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((#0=(-525) #0#) . T)) ((($) . T) (((-385 (-525))) . T)) -(-3254 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3254 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-2067 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-2067 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (|has| |#4| (-735)) -(-3254 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-2067 (|has| |#4| (-735)) (|has| |#4| (-787))) (|has| |#4| (-787)) (|has| |#3| (-735)) -(-3254 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-2067 (|has| |#3| (-735)) (|has| |#3| (-787))) (|has| |#3| (-787)) ((((-525)) . T)) (((|#2|) . T)) -((((-1092)) -3254 (-12 (|has| (-1090 |#1| |#2| |#3|) (-835 (-1092))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))))) +((((-1092)) -2067 (-12 (|has| (-1090 |#1| |#2| |#3|) (-835 (-1092))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1092)))))) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1092))))) ((((-1092)) -12 (|has| |#1| (-15 * (|#1| (-713) |#1|))) (|has| |#1| (-835 (-1092))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3123,11 +3123,11 @@ ((((-1090 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1057 |#1| |#2|)) . T)) ((((-1090 |#1| |#2| |#3|)) |has| |#1| (-341))) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) ((($) . T)) (|has| |#1| (-953)) -(((|#2|) . T) (((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) ((((-798)) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525)))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-357)) . #0=(|has| |#2| (-953))) (((-205)) . #0#)) ((((-1092) (-51)) . T)) @@ -3139,15 +3139,15 @@ ((((-1090 |#1| |#2| |#3|)) . T)) ((((-1090 |#1| |#2| |#3|)) . T) (((-1083 |#1| |#2| |#3|)) . T)) ((((-798)) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-525) |#1|) . T)) ((((-1090 |#1| |#2| |#3|)) |has| |#1| (-341))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-341)) -(((|#3|) . T) ((|#2|) . T) (($) -3254 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) ((|#4|) -3254 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977)))) -(((|#2|) . T) (($) -3254 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3254 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) +(((|#3|) . T) ((|#2|) . T) (($) -2067 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) ((|#4|) -2067 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977)))) +(((|#2|) . T) (($) -2067 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -2067 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-341)) @@ -3159,7 +3159,7 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-125)) . T) (((-798)) . T)) ((((-525) |#1|) . T)) (((|#1|) . T)) @@ -3167,30 +3167,30 @@ (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-341)) (|has| |#2| (-265 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1| (-497 |#2|)) . T)) -((((-2 (|:| -3364 (-1092)) (|:| -4201 (-51)))) . T)) +((((-2 (|:| -1556 (-1092)) (|:| -3448 (-51)))) . T)) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-713)) . T)) ((((-112 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) -(-3254 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3254 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-2067 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-2067 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((($) . T)) (((|#2| (-497 (-800 |#1|))) . T)) ((((-525) |#1|) . T)) (((|#2|) . T)) (((|#2| (-713)) . T)) -((((-798)) -3254 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -2067 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1075) |#1|) . T)) ((((-385 |#2|)) . T)) -((((-2 (|:| -3364 |#1|) (|:| -4201 |#2|))) . T)) +((((-2 (|:| -1556 |#1|) (|:| -3448 |#2|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) ((($) . T) ((|#2|) . T)) @@ -3198,12 +3198,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-265 |#2| |#2|))) (((|#1| (-592 |#1|)) |has| |#1| (-787))) -(-3254 (|has| |#1| (-213)) (|has| |#1| (-327))) -(-3254 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-213)) (|has| |#1| (-327))) +(-2067 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1020)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-931 |#1|)) . T) ((|#1|) . T) (((-525)) -3254 (|has| (-931 |#1|) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) -3254 (|has| (-931 |#1|) (-968 (-385 (-525)))) (|has| |#1| (-968 (-385 (-525)))))) +((((-931 |#1|)) . T) ((|#1|) . T) (((-525)) -2067 (|has| (-931 |#1|) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) -2067 (|has| (-931 |#1|) (-968 (-385 (-525)))) (|has| |#1| (-968 (-385 (-525)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -3214,9 +3214,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1057 |#1| |#2|) #0#) |has| (-1057 |#1| |#2|) (-288 (-1057 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) #0#) |has| (-2 (|:| -3364 |#1|) (|:| -4201 |#2|)) (-288 (-2 (|:| -3364 |#1|) (|:| -4201 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) #0#) |has| (-2 (|:| -1556 |#1|) (|:| -3448 |#2|)) (-288 (-2 (|:| -1556 |#1|) (|:| -3448 |#2|))))) (((#0=(-112 |#1|)) |has| #0# (-288 #0#))) -(-3254 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-2067 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((($ $) . T)) ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-213)) ((|#2| |#1|) |has| |#1| (-213)) ((|#3| |#1|) . T) ((|#3| $) . T)) |