aboutsummaryrefslogtreecommitdiff
path: root/src/share/algebra/category.daase
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2008-08-08 14:47:57 +0000
committerdos-reis <gdr@axiomatics.org>2008-08-08 14:47:57 +0000
commit7727c94cc7b39a4ddb33c31ae328f2aa6a32d296 (patch)
tree682b38ba892d95b5294b37436c04a66efefe61cf /src/share/algebra/category.daase
parent3efb135761426b4756d3fa22b5353ac17f781ff7 (diff)
downloadopen-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.daase1130
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))