aboutsummaryrefslogtreecommitdiff
path: root/src/share/algebra/category.daase
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2008-04-14 02:09:13 +0000
committerdos-reis <gdr@axiomatics.org>2008-04-14 02:09:13 +0000
commit1d44d2feb01bc10dcc8690c4f71a3157b07502bc (patch)
tree1f3a91143489620629f548e3b159c189f9061bc3 /src/share/algebra/category.daase
parent663089e7f95f4901a46939ef34c60982dd5aadda (diff)
downloadopen-axiom-1d44d2feb01bc10dcc8690c4f71a3157b07502bc.tar.gz
Update databases.
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r--src/share/algebra/category.daase1126
1 files changed, 563 insertions, 563 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase
index 94f9b9eb..2bd895b7 100644
--- a/src/share/algebra/category.daase
+++ b/src/share/algebra/category.daase
@@ -1,14 +1,14 @@
-(142548 . 3416412006)
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(142548 . 3417125214)
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#2| |#2|) . T))
((((-523)) . T))
-((($ $) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2| |#2|) . T) ((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2| |#2|) . T) ((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))))
((($) . T))
(((|#1|) . T))
((($) . T) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#2|) . T))
-((($) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) . T) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) . T) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
(|has| |#1| (-840))
((((-794)) . T))
((((-794)) . T))
@@ -23,28 +23,28 @@
((((-203)) . T) (((-794)) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
-((($ $) . T) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1| |#1|) . T))
-(-3172 (|has| |#1| (-759)) (|has| |#1| (-786)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
+((($ $) . T) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1| |#1|) . T))
+(-3255 (|has| |#1| (-759)) (|has| |#1| (-786)))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
((((-794)) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-784))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| |#2| |#3|) . T))
(((|#4|) . T))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-794)) . T))
((((-794)) |has| |#1| (-1016)))
(((|#1|) . T) ((|#2|) . T))
(((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) |has| |#1| (-964 (-383 (-523)))))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(((|#2| (-456 (-2810 |#1|) (-710))) . T))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(((|#2| (-456 (-1271 |#1|) (-710))) . T))
(((|#1| (-495 (-1087))) . T))
(((#0=(-801 |#1|) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#4| (-344))
(|has| |#3| (-344))
(((|#1|) . T))
@@ -54,10 +54,10 @@
(|has| |#1| (-134))
(|has| |#1| (-136))
(|has| |#1| (-515))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
((($) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
((($) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T))
((($) . T))
@@ -66,59 +66,59 @@
((((-794)) . T))
((((-794)) . T))
((((-383 (-523))) . T) (($) . T))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
((((-794)) . T))
((((-794)) . T))
((((-794)) . T))
(((|#1|) . T))
-(((|#1|) . T) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
+(((|#1|) . T) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
(((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) (($) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1| |#2|) . T))
((((-794)) . T))
(((|#1|) . T))
-(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
(((|#1|) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
-(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
((($ $) . T))
(((|#2|) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
((($) . T))
(|has| |#1| (-344))
(((|#1|) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-794)) . T))
((((-794)) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
(((|#1| |#1|) . T))
(|has| |#1| (-515))
(((|#2| |#2|) -12 (|has| |#1| (-339)) (|has| |#2| (-286 |#2|))) (((-1087) |#2|) -12 (|has| |#1| (-339)) (|has| |#2| (-484 (-1087) |#2|))))
((((-383 |#2|)) . T) (((-383 (-523))) . T) (($) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(|has| |#1| (-1016))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(|has| |#1| (-1016))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(|has| |#1| (-784))
((($) . T) (((-383 (-523))) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
-(-3172 (|has| |#4| (-732)) (|has| |#4| (-784)))
-(-3172 (|has| |#4| (-732)) (|has| |#4| (-784)))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#4| (-732)) (|has| |#4| (-784)))
+(-3255 (|has| |#4| (-732)) (|has| |#4| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
(((|#1| |#2|) . T))
(((|#1| |#2|) . T))
(|has| |#1| (-1016))
@@ -132,21 +132,21 @@
((((-523)) . T))
((((-523)) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#1| (-710)) . T))
(|has| |#2| (-732))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(|has| |#2| (-784))
(((|#1| |#2| |#3| |#4|) . T))
(((|#1| |#2|) . T))
((((-1070) |#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1|) . T))
(((|#3| (-710)) . T))
(|has| |#1| (-136))
(|has| |#1| (-134))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-1016))
((((-383 (-523))) . T) (((-523)) . T))
((((-1087) |#2|) |has| |#2| (-484 (-1087) |#2|)) ((|#2| |#2|) |has| |#2| (-286 |#2|)))
@@ -154,7 +154,7 @@
(((|#1|) . T) (($) . T))
((((-523)) . T))
((((-523)) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
((((-523)) . T))
((((-523)) . T))
(((#0=(-638) (-1083 #0#)) . T))
@@ -173,12 +173,12 @@
((((-794)) . T))
((((-794)) . T))
(((|#1| |#1|) . T))
-(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) . T))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
((((-794)) . T))
((((-794)) . T))
((((-794)) . T))
@@ -189,25 +189,25 @@
((((-155 (-203))) |has| |#1| (-949)) (((-155 (-355))) |has| |#1| (-949)) (((-499)) |has| |#1| (-564 (-499))) (((-1083 |#1|)) . T) (((-823 (-523))) |has| |#1| (-564 (-823 (-523)))) (((-823 (-355))) |has| |#1| (-564 (-823 (-355)))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#2|) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#2|) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
(|has| |#1| (-339))
(-12 (|has| |#4| (-211)) (|has| |#4| (-973)))
(-12 (|has| |#3| (-211)) (|has| |#3| (-973)))
-(-3172 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-794)) . T))
(((|#1|) . T))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
(((|#1|) . T) (((-523)) |has| |#1| (-585 (-523))))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-(((|#1|) . T) (((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+(((|#1|) . T) (((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(|has| |#1| (-515))
(|has| |#1| (-515))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1|) . T))
(|has| |#1| (-515))
(|has| |#1| (-515))
@@ -218,11 +218,11 @@
(((|#2|) . T) (($) . T) (((-383 (-523))) . T))
(-12 (|has| |#1| (-1016)) (|has| |#2| (-1016)))
((($) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
-(((|#1|) . T) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
+(((|#1|) . T) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
(((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) (($) . T))
-(((|#4| |#4|) -3172 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))) (($ $) |has| |#4| (-158)))
-(((|#3| |#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($ $) |has| |#3| (-158)))
+(((|#4| |#4|) -3255 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))) (($ $) |has| |#4| (-158)))
+(((|#3| |#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($ $) |has| |#3| (-158)))
(((|#1|) . T))
(((|#2|) . T))
((((-499)) |has| |#2| (-564 (-499))) (((-823 (-355))) |has| |#2| (-564 (-823 (-355)))) (((-823 (-523))) |has| |#2| (-564 (-823 (-523)))))
@@ -231,21 +231,21 @@
((((-794)) . T))
((((-499)) |has| |#1| (-564 (-499))) (((-823 (-355))) |has| |#1| (-564 (-823 (-355)))) (((-823 (-523))) |has| |#1| (-564 (-823 (-523)))))
((((-794)) . T))
-(((|#4|) -3172 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))) (($) |has| |#4| (-158)))
-(((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($) |has| |#3| (-158)))
+(((|#4|) -3255 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))) (($) |has| |#4| (-158)))
+(((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($) |has| |#3| (-158)))
((((-794)) . T))
((((-499)) . T) (((-523)) . T) (((-823 (-523))) . T) (((-355)) . T) (((-203)) . T))
(((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) |has| |#1| (-964 (-383 (-523)))))
((($) . T) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T))
((((-383 $) (-383 $)) |has| |#2| (-515)) (($ $) . T) ((|#2| |#2|) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 (-51)))) . T))
(((|#1|) . T))
(|has| |#2| (-840))
((((-1070) (-51)) . T))
((((-523)) |has| #0=(-383 |#2|) (-585 (-523))) ((#0#) . T))
((((-499)) . T) (((-203)) . T) (((-355)) . T) (((-823 (-355))) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
(((|#1|) |has| |#1| (-158)))
(((|#1| $) |has| |#1| (-263 |#1| |#1|)))
((((-794)) . T))
@@ -256,13 +256,13 @@
(|has| |#1| (-786))
(|has| |#1| (-1016))
(((|#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(|has| |#1| (-211))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1| (-495 (-757 (-1087)))) . T))
(((|#1| (-900)) . T))
(((#0=(-801 |#1|) $) |has| #0# (-263 #0# #0#)))
@@ -271,7 +271,7 @@
(((|#1|) . T))
(((|#2| |#2|) . T))
(|has| |#1| (-1063))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(|has| (-1155 |#1| |#2| |#3| |#4|) (-134))
(|has| (-1155 |#1| |#2| |#3| |#4|) (-136))
(|has| |#1| (-134))
@@ -288,20 +288,20 @@
((($) . T) ((|#1|) . T))
(((|#2|) |has| |#2| (-973)))
((((-794)) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#1|) . T))
-(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) ((#0=(-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) #0#) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)))))
+(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) ((#0=(-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) #0#) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)))))
((((-523) |#1|) . T))
((((-794)) . T))
((((-499)) -12 (|has| |#1| (-564 (-499))) (|has| |#2| (-564 (-499)))) (((-823 (-355))) -12 (|has| |#1| (-564 (-823 (-355)))) (|has| |#2| (-564 (-823 (-355))))) (((-823 (-523))) -12 (|has| |#1| (-564 (-823 (-523)))) (|has| |#2| (-564 (-823 (-523))))))
((((-794)) . T))
((((-794)) . T))
((($) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
((($) . T))
((($) . T))
((($) . T))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-794)) . T))
((((-794)) . T))
(|has| (-1154 |#2| |#3| |#4|) (-136))
@@ -312,16 +312,16 @@
((((-794)) . T))
(((|#1|) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
(((|#1|) . T))
((((-523) |#1|) . T))
(((|#2|) |has| |#2| (-158)))
(((|#1|) |has| |#1| (-158)))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
((((-794)) |has| |#1| (-1016)))
-(-3172 (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
((((-841 |#1|)) . T))
((((-383 |#2|) |#3|) . T))
(|has| |#1| (-15 * (|#1| (-523) |#1|)))
@@ -333,7 +333,7 @@
(((|#1|) . T))
((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) |has| |#1| (-515)))
(|has| |#1| (-339))
-(-3172 (-12 (|has| (-1161 |#1| |#2| |#3|) (-211)) (|has| |#1| (-339))) (|has| |#1| (-15 * (|#1| (-523) |#1|))))
+(-3255 (-12 (|has| (-1161 |#1| |#2| |#3|) (-211)) (|has| |#1| (-339))) (|has| |#1| (-15 * (|#1| (-523) |#1|))))
(|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|)))
(|has| |#1| (-339))
((((-523)) . T))
@@ -345,31 +345,31 @@
(((|#1|) . T))
((((-523) |#1|) . T))
(((|#2|) . T))
-(-3172 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(((|#1|) . T))
((((-1087)) -12 (|has| |#3| (-831 (-1087))) (|has| |#3| (-973))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(-12 (|has| |#1| (-339)) (|has| |#2| (-759)))
-(-3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515)))
-(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
+(-3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515)))
+(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
((($ $) |has| |#1| (-515)))
(((#0=(-638) (-1083 #0#)) . T))
((((-794)) . T))
((((-794)) . T) (((-1169 |#4|)) . T))
((((-794)) . T) (((-1169 |#3|)) . T))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
((($) |has| |#1| (-515)))
((((-794)) . T))
((($) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((#1=(-1161 |#1| |#2| |#3|) #1#) |has| |#1| (-339)) ((|#1| |#1|) . T))
-(((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) . T))
-(((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((#1=(-1161 |#1| |#2| |#3|) #1#) |has| |#1| (-339)) ((|#1| |#1|) . T))
+(((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) . T))
+(((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
(((|#3|) |has| |#3| (-973)))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(|has| |#1| (-1016))
(((|#2| (-758 |#1|)) . T))
(((|#1|) . T))
@@ -381,37 +381,37 @@
((((-133)) . T))
(((|#3|) |has| |#3| (-1016)) (((-523)) -12 (|has| |#3| (-964 (-523))) (|has| |#3| (-1016))) (((-383 (-523))) -12 (|has| |#3| (-964 (-383 (-523)))) (|has| |#3| (-1016))))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
((((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)) ((|#1| |#1|) |has| |#1| (-286 |#1|)))
(|has| |#2| (-759))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-784))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-499)) |has| |#1| (-564 (-499))))
(((|#1| |#2|) . T))
((((-1087)) -12 (|has| |#1| (-339)) (|has| |#1| (-831 (-1087)))))
((((-1070) |#1|) . T))
(((|#1| |#2| |#3| (-495 |#3|)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#1| (-344))
(|has| |#1| (-344))
(|has| |#1| (-344))
((((-794)) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(|has| |#1| (-344))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-523)) . T))
((((-523)) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
((((-794)) . T))
((((-794)) . T))
(-12 (|has| |#2| (-211)) (|has| |#2| (-973)))
@@ -420,10 +420,10 @@
((((-523) |#4|) . T))
((((-523) |#3|) . T))
(((|#1|) . T) (((-523)) |has| |#1| (-585 (-523))))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-1155 |#1| |#2| |#3| |#4|)) . T))
((((-383 (-523))) . T) (((-523)) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1| |#1|) . T))
(((|#1|) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
@@ -452,37 +452,37 @@
((($) . T))
((($ $) . T) ((#0=(-1087) $) . T) ((#0# |#1|) . T))
(((|#2|) |has| |#2| (-158)))
-((($) -3172 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) |has| |#2| (-158)) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
-(((|#2| |#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
+((($) -3255 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) |has| |#2| (-158)) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
+(((|#2| |#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
((((-133)) . T))
(((|#1|) . T))
(-12 (|has| |#1| (-344)) (|has| |#2| (-344)))
((((-794)) . T))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
(((|#1|) . T))
((((-794)) . T))
(|has| |#1| (-1016))
(|has| $ (-136))
((((-523) |#1|) . T))
-((($) -3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) -3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|))) (|has| |#1| (-831 (-1087)))))
(|has| |#1| (-339))
-(-3172 (-12 (|has| (-1085 |#1| |#2| |#3|) (-211)) (|has| |#1| (-339))) (|has| |#1| (-15 * (|#1| (-523) |#1|))))
+(-3255 (-12 (|has| (-1085 |#1| |#2| |#3|) (-211)) (|has| |#1| (-339))) (|has| |#1| (-15 * (|#1| (-523) |#1|))))
(|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|)))
(|has| |#1| (-339))
(|has| |#1| (-15 * (|#1| (-710) |#1|)))
(((|#1|) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
((((-794)) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(((|#2| (-495 (-796 |#1|))) . T))
((((-794)) . T))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-536 |#1|)) . T))
((($) . T))
(((|#1|) . T) (($) . T))
@@ -499,28 +499,28 @@
((((-794)) . T))
((((-794)) . T))
(((|#1| |#2| |#3| |#4| |#5|) . T))
-(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((#1=(-1085 |#1| |#2| |#3|) #1#) |has| |#1| (-339)) ((|#1| |#1|) . T))
-(((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((#1=(-1085 |#1| |#2| |#3|) #1#) |has| |#1| (-339)) ((|#1| |#1|) . T))
+(((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
(((|#2|) |has| |#2| (-973)))
(|has| |#1| (-1016))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) . T))
-(((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) . T))
+(((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) |has| |#1| (-158)) (($) . T))
(((|#1|) . T))
-(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
((((-794)) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
(((#0=(-1001) |#1|) . T) ((#0# $) . T) (($ $) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
((($) . T))
(((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) (($) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#2|) |has| |#1| (-339)))
(((|#1|) . T))
(((|#2|) |has| |#2| (-1016)) (((-523)) -12 (|has| |#2| (-964 (-523))) (|has| |#2| (-1016))) (((-383 (-523))) -12 (|has| |#2| (-964 (-383 (-523)))) (|has| |#2| (-1016))))
@@ -535,8 +535,8 @@
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-134))
(|has| |#1| (-136))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-383 (-523))) . T) (($) . T))
((((-383 (-523))) . T) (($) . T))
((((-383 (-523))) . T) (($) . T))
@@ -547,12 +547,12 @@
(((|#1| (-710) (-1001)) . T))
((((-383 (-523))) |has| |#2| (-339)) (($) . T))
(((|#1| (-495 (-1006 (-1087))) (-1006 (-1087))) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(|has| |#2| (-732))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(|has| |#1| (-344))
(|has| |#1| (-344))
(|has| |#1| (-344))
@@ -584,61 +584,61 @@
(((|#4| |#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
(((|#2|) . T) (((-523)) |has| |#2| (-964 (-523))) (((-383 (-523))) |has| |#2| (-964 (-383 (-523)))))
(((|#3| |#3|) -12 (|has| |#3| (-286 |#3|)) (|has| |#3| (-1016))))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#1|) . T))
(((|#1| |#2|) . T))
((($) . T))
((($) . T))
(((|#2|) . T))
(((|#3|) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#2|) . T))
-((((-794)) -3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
+((((-794)) -3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
(((|#1|) |has| |#1| (-158)))
((((-523)) . T))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-523) (-133)) . T))
-((($) -3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+((($) -3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
(((|#2|) |has| |#1| (-339)))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| |#1|) . T) (($ $) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| (-495 #0=(-1087)) #0#) . T))
(((|#1|) . T) (($) . T))
(|has| |#4| (-158))
(|has| |#3| (-158))
(((#0=(-383 (-883 |#1|)) #0#) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(|has| |#1| (-1016))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(|has| |#1| (-1016))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1| |#1|) |has| |#1| (-158)))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T))
((((-383 (-883 |#1|))) . T))
(((|#1|) |has| |#1| (-158)))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-794)) . T))
((((-1155 |#1| |#2| |#3| |#4|)) . T))
(((|#1|) |has| |#1| (-973)) (((-523)) -12 (|has| |#1| (-585 (-523))) (|has| |#1| (-973))))
(((|#1| |#2|) . T))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
(|has| |#3| (-732))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
(|has| |#3| (-784))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#2|) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#2|) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
(((|#2|) . T))
((((-794)) . T))
((((-794)) . T))
@@ -653,22 +653,22 @@
(|has| |#1| (-1016))
(((|#2|) . T))
((((-499)) |has| |#2| (-564 (-499))) (((-823 (-355))) |has| |#2| (-564 (-823 (-355)))) (((-823 (-523))) |has| |#2| (-564 (-823 (-523)))))
-(((|#4|) -3172 (|has| |#4| (-158)) (|has| |#4| (-339))))
-(((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339))))
+(((|#4|) -3255 (|has| |#4| (-158)) (|has| |#4| (-339))))
+(((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339))))
((((-794)) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
((($ $) . T) ((#0=(-1087) $) |has| |#1| (-211)) ((#0# |#1|) |has| |#1| (-211)) ((#1=(-757 (-1087)) |#1|) . T) ((#1# $) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
((((-523) |#2|) . T))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-((($) -3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973))) ((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))))
+((($) -3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973))) ((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))))
((((-523) |#1|) . T))
(|has| (-383 |#2|) (-136))
(|has| (-383 |#2|) (-134))
@@ -681,21 +681,21 @@
(|has| |#1| (-515))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-794)) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(|has| |#1| (-37 (-383 (-523))))
-((((-364) (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-364) (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#2| (-1063))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(((|#1|) . T))
((((-364) (-1070)) . T))
(|has| |#1| (-515))
((((-112 |#1|)) . T))
((((-523) |#1|) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#2|) . T))
((((-794)) . T))
((((-758 |#1|)) . T))
@@ -708,7 +708,7 @@
(((|#1|) |has| |#1| (-158)))
((((-794)) . T))
((((-499)) |has| |#1| (-564 (-499))))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#2|) |has| |#2| (-286 |#2|)))
(((#0=(-523) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
(((|#1|) . T))
@@ -718,7 +718,7 @@
(((#0=(-523) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
((($) . T) (((-523)) . T) (((-383 (-523))) . T))
(|has| |#2| (-344))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
@@ -729,9 +729,9 @@
((((-1085 |#1| |#2| |#3|) $) -12 (|has| (-1085 |#1| |#2| |#3|) (-263 (-1085 |#1| |#2| |#3|) (-1085 |#1| |#2| |#3|))) (|has| |#1| (-339))) (($ $) . T))
((((-794)) . T))
((((-794)) . T))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
((($ $) . T))
((($ $) . T))
((((-794)) . T))
@@ -741,12 +741,12 @@
(((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-383 (-523))) . T) (((-523)) . T))
((((-523) (-133)) . T))
((((-133)) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
((((-108)) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-108)) . T))
@@ -754,38 +754,38 @@
((((-499)) |has| |#1| (-564 (-499))) (((-203)) . #0=(|has| |#1| (-949))) (((-355)) . #0#))
((((-794)) . T))
(|has| |#1| (-759))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(|has| |#1| (-786))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
(|has| |#1| (-515))
(|has| |#1| (-840))
(((|#1|) . T))
(|has| |#1| (-1016))
((((-794)) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
((((-794)) . T))
((((-794)) . T))
((((-794)) . T))
(((|#1| (-1169 |#1|) (-1169 |#1|)) . T))
((((-523) (-133)) . T))
((($) . T))
-(-3172 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-794)) . T))
(|has| |#1| (-1016))
(((|#1| (-900)) . T))
(((|#1| |#1|) . T))
((($) . T))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(-12 (|has| |#1| (-448)) (|has| |#2| (-448)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(-3172 (-12 (|has| |#1| (-448)) (|has| |#2| (-448))) (-12 (|has| |#1| (-666)) (|has| |#2| (-666))))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (-12 (|has| |#1| (-448)) (|has| |#2| (-448))) (-12 (|has| |#1| (-666)) (|has| |#2| (-666))))
(((|#1|) . T))
(|has| |#2| (-732))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(((|#1| |#2|) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(|has| |#2| (-784))
@@ -800,7 +800,7 @@
(((|#1|) . T))
(((|#1|) . T))
((((-383 (-523))) . T) (($) . T))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) . T))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) . T))
(|has| |#1| (-767))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
(|has| |#1| (-1016))
@@ -811,8 +811,8 @@
(((|#3|) |has| |#3| (-1016)))
(|has| |#3| (-344))
(((|#1|) . T) (((-794)) . T))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
((((-794)) . T))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#2|) . T))
@@ -822,30 +822,30 @@
(((|#1|) . T))
(((|#1|) |has| |#1| (-158)))
((((-383 (-523))) . T) (((-523)) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
((((-133)) . T))
(((|#1|) . T))
((((-133)) . T))
-((($) -3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
+((($) -3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973))) ((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))))
((((-133)) . T))
(((|#1| |#2| |#3|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
(|has| $ (-136))
(|has| $ (-136))
(|has| |#1| (-1016))
((((-794)) . T))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-448)) (|has| |#1| (-515)) (|has| |#1| (-973)) (|has| |#1| (-1028)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-448)) (|has| |#1| (-515)) (|has| |#1| (-973)) (|has| |#1| (-1028)))
((($ $) |has| |#1| (-263 $ $)) ((|#1| $) |has| |#1| (-263 |#1| |#1|)))
(((|#1| (-383 (-523))) . T))
(((|#1|) . T))
((((-1087)) . T))
(|has| |#1| (-515))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-515))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
@@ -856,7 +856,7 @@
(|has| |#1| (-136))
(|has| |#1| (-134))
(|has| |#4| (-784))
-(((|#2| (-218 (-2810 |#1|) (-710)) (-796 |#1|)) . T))
+(((|#2| (-218 (-1271 |#1|) (-710)) (-796 |#1|)) . T))
(|has| |#3| (-784))
(((|#1| (-495 |#3|) |#3|) . T))
(|has| |#1| (-136))
@@ -870,21 +870,21 @@
(|has| |#1| (-134))
((((-383 (-523))) |has| |#2| (-339)) (($) . T))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-325)) (|has| |#1| (-344)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-325)) (|has| |#1| (-344)))
((((-1054 |#2| |#1|)) . T) ((|#1|) . T))
(|has| |#2| (-158))
(((|#1| |#2|) . T))
(-12 (|has| |#2| (-211)) (|has| |#2| (-973)))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
((((-794)) . T))
(((|#1|) . T))
(((|#2|) . T) (($) . T))
(((|#1|) . T) (($) . T))
((((-638)) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(|has| |#1| (-515))
(((|#1|) . T))
(((|#1|) . T))
@@ -906,10 +906,10 @@
(((|#1| (-383 (-523))) . T))
(((|#3|) . T) (((-562 $)) . T))
(((|#1| |#2|) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((($ $) . T) ((|#2| $) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((#0=(-1085 |#1| |#2| |#3|) #0#) -12 (|has| (-1085 |#1| |#2| |#3|) (-286 (-1085 |#1| |#2| |#3|))) (|has| |#1| (-339))) (((-1087) #0#) -12 (|has| (-1085 |#1| |#2| |#3|) (-484 (-1087) (-1085 |#1| |#2| |#3|))) (|has| |#1| (-339))))
@@ -917,8 +917,8 @@
((((-794)) . T))
((((-794)) . T))
(((|#1| |#1|) . T))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
-(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) (((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)))))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
+(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) (((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)))))
((((-794)) . T))
(((|#1|) . T))
(((|#3| |#3|) . T))
@@ -929,10 +929,10 @@
((($ $) . T) ((#0=(-796 |#1|) $) . T) ((#0# |#2|) . T))
(|has| |#1| (-767))
(|has| |#1| (-1016))
-(((|#2| |#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339))))
-((((-523) (-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T) ((|#1| |#2|) . T))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
+(((|#2| |#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339))))
+((((-523) (-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T) ((|#1| |#2|) . T))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
((((-710)) . T))
((((-523)) . T))
(|has| |#1| (-515))
@@ -945,29 +945,29 @@
((((-112 |#1|)) . T))
(((|#1|) . T))
(|has| |#1| (-136))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
((((-823 (-523))) . T) (((-823 (-355))) . T) (((-499)) . T) (((-1087)) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
((($) . T))
((((-794)) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(((|#2|) |has| |#2| (-158)))
-((($) -3172 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) |has| |#2| (-158)) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))) ((|#2|) |has| |#2| (-158)) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))))
((((-801 |#1|)) . T))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
(-12 (|has| |#3| (-211)) (|has| |#3| (-973)))
(|has| |#2| (-1063))
-(((#0=(-51)) . T) (((-2 (|:| -3772 (-1087)) (|:| -2482 #0#))) . T))
+(((#0=(-51)) . T) (((-2 (|:| -2402 (-1087)) (|:| -2746 #0#))) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
(((|#1| (-523) (-1001)) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| (-383 (-523)) (-1001)) . T))
-((($) -3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) -3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-523) |#2|) . T))
(((|#1| |#2|) . T))
(((|#1| |#2|) . T))
@@ -975,37 +975,37 @@
(-12 (|has| |#1| (-344)) (|has| |#2| (-344)))
((((-794)) . T))
((((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)) ((|#1| |#1|) |has| |#1| (-286 |#1|)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(((|#1|) . T))
((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) |has| |#1| (-515)))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-794)) . T))
(|has| |#1| (-325))
(((|#1|) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(|has| |#1| (-515))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-794)) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
((((-383 (-523))) . T) (((-523)) . T))
((((-523)) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
((($) . T))
((((-794)) . T))
(((|#1|) . T))
((((-801 |#1|)) . T) (($) . T) (((-383 (-523))) . T))
((((-794)) . T))
-(((|#3| |#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($ $) |has| |#3| (-158)))
+(((|#3| |#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($ $) |has| |#3| (-158)))
(|has| |#1| (-949))
((((-794)) . T))
-(((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($) |has| |#3| (-158)))
+(((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))) (($) |has| |#3| (-158)))
((((-523) (-108)) . T))
(((|#1|) |has| |#1| (-286 |#1|)))
(|has| |#1| (-344))
@@ -1013,31 +1013,31 @@
(|has| |#1| (-344))
((((-1087) $) |has| |#1| (-484 (-1087) $)) (($ $) |has| |#1| (-286 $)) ((|#1| |#1|) |has| |#1| (-286 |#1|)) (((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)))
((((-1087)) |has| |#1| (-831 (-1087))))
-(-3172 (-12 (|has| |#1| (-211)) (|has| |#1| (-339))) (|has| |#1| (-325)))
+(-3255 (-12 (|has| |#1| (-211)) (|has| |#1| (-339))) (|has| |#1| (-325)))
((((-364) (-1034)) . T))
(((|#1| |#4|) . T))
(((|#1| |#3|) . T))
((((-364) |#1|) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-1016))
((((-794)) . T))
((((-794)) . T))
((((-841 |#1|)) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
(((|#1| |#2|) . T))
((($) . T))
(((|#1| |#1|) . T))
(((#0=(-801 |#1|)) |has| #0# (-286 #0#)))
(((|#1| |#2|) . T))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
(-12 (|has| |#1| (-732)) (|has| |#2| (-732)))
(((|#1|) . T))
(-12 (|has| |#1| (-732)) (|has| |#2| (-732)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#2|) . T) (($) . T))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#1| (-1109))
(((#0=(-523) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
((((-383 (-523))) . T) (($) . T))
@@ -1048,8 +1048,8 @@
(((|#1| |#1|) . T) (($ $) . T) ((#0=(-383 (-523)) #0#) . T))
(|has| |#1| (-339))
((((-523)) . T) (((-383 (-523))) . T) (($) . T))
-((($ $) . T) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1| |#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((($ $) . T) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1| |#1|) . T))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
((((-794)) . T))
((((-794)) . T))
@@ -1064,14 +1064,14 @@
(((|#1| |#2|) . T))
(|has| |#1| (-784))
(|has| |#1| (-784))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
-(((#0=(-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) #0#) |has| (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))))))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(((#0=(-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) #0#) |has| (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))))))
((($) . T))
(|has| |#2| (-786))
((($) . T))
(((|#2|) |has| |#2| (-1016)))
-((((-794)) -3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
+((((-794)) -3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
(|has| |#1| (-786))
(|has| |#1| (-786))
((((-1070) (-51)) . T))
@@ -1079,10 +1079,10 @@
((((-794)) . T))
((((-523)) |has| #0=(-383 |#2|) (-585 (-523))) ((#0#) . T))
((((-523) (-133)) . T))
-((((-523) (-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T) ((|#1| |#2|) . T))
+((((-523) (-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T) ((|#1| |#2|) . T))
((((-383 (-523))) . T) (($) . T))
(((|#1|) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-794)) . T))
((((-841 |#1|)) . T))
(|has| |#1| (-339))
@@ -1107,31 +1107,31 @@
((($) . T))
(((|#2|) . T) (($) . T))
(((|#1|) |has| |#1| (-158)))
-((((-523) (-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T) ((|#1| |#2|) . T))
+((((-523) (-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T) ((|#1| |#2|) . T))
(((|#1|) . T))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#3|) . T))
(((|#1|) |has| |#1| (-158)))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) . T))
(((|#1|) . T))
((((-499)) |has| |#1| (-564 (-499))) (((-823 (-355))) |has| |#1| (-564 (-823 (-355)))) (((-823 (-523))) |has| |#1| (-564 (-823 (-523)))))
((((-794)) . T))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#2| (-784))
(-12 (|has| |#2| (-211)) (|has| |#2| (-973)))
(|has| |#1| (-515))
(|has| |#1| (-1063))
((((-1070) |#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1| |#1|) . T))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1| |#1|) . T))
((((-383 (-523))) |has| |#1| (-964 (-523))) (((-523)) |has| |#1| (-964 (-523))) (((-1087)) |has| |#1| (-964 (-1087))) ((|#1|) . T))
((((-523) |#2|) . T))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
((((-523)) |has| |#1| (-817 (-523))) (((-355)) |has| |#1| (-817 (-355))))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1|) . T))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1|) . T))
(((|#1|) . T))
((((-589 |#4|)) . T) (((-794)) . T))
((((-499)) |has| |#4| (-564 (-499))))
@@ -1144,17 +1144,17 @@
(((|#1|) . T))
(((|#2|) . T))
((((-1087)) |has| (-383 |#2|) (-831 (-1087))))
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
((($) . T))
((($) . T))
(((|#2|) . T))
-((((-794)) -3172 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-563 (-794))) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016))) (((-1169 |#3|)) . T))
+((((-794)) -3255 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-563 (-794))) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016))) (((-1169 |#3|)) . T))
((((-523) |#2|) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
-(((|#2| |#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(((|#2| |#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($ $) |has| |#2| (-158)))
((((-794)) . T))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T) ((|#2|) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T) ((|#2|) . T))
((((-794)) . T))
((((-794)) . T))
((((-1070) (-1087) (-523) (-203) (-794)) . T))
@@ -1189,8 +1189,8 @@
(|has| |#1| (-37 (-383 (-523))))
((((-794)) . T))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-973))) (($) |has| |#2| (-158)))
(|has| $ (-136))
((((-383 |#2|)) . T))
((((-383 (-523))) |has| #0=(-383 |#2|) (-964 (-383 (-523)))) (((-523)) |has| #0# (-964 (-523))) ((#0#) . T))
@@ -1201,11 +1201,11 @@
(((|#3|) |has| |#3| (-158)))
(|has| |#1| (-136))
(|has| |#1| (-134))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
(((|#1|) . T))
(((|#2|) . T))
@@ -1236,7 +1236,7 @@
((((-927 |#1|)) . T) ((|#1|) . T))
((((-794)) . T))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-383 (-523))) . T) (((-383 |#1|)) . T) ((|#1|) . T) (($) . T))
(((|#1| (-1083 |#1|)) . T))
((((-523)) . T) (($) . T) (((-383 (-523))) . T))
@@ -1244,9 +1244,9 @@
(|has| |#1| (-786))
(((|#2|) . T))
((((-523)) . T) (($) . T) (((-383 (-523))) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
((((-523) |#2|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#2|) . T))
((((-523) |#3|) . T))
(((|#2|) . T))
@@ -1261,7 +1261,7 @@
(((|#3|) -12 (|has| |#3| (-286 |#3|)) (|has| |#3| (-1016))))
(((|#2|) . T))
(((|#1|) . T))
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#2| |#2|) . T))
(|has| |#2| (-339))
(((|#2|) . T) (((-523)) |has| |#2| (-964 (-523))) (((-383 (-523))) |has| |#2| (-964 (-383 (-523)))))
@@ -1291,19 +1291,19 @@
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| |#2|) . T))
((((-523) (-133)) . T))
-(((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+(((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(|has| |#1| (-786))
(((|#2| (-710) (-1001)) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
(|has| |#1| (-730))
(((|#1|) |has| |#1| (-158)))
(((|#4|) . T))
(((|#4|) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#1| (-136)) (-12 (|has| |#1| (-339)) (|has| |#2| (-136))))
-(-3172 (|has| |#1| (-134)) (-12 (|has| |#1| (-339)) (|has| |#2| (-134))))
+(-3255 (|has| |#1| (-136)) (-12 (|has| |#1| (-339)) (|has| |#2| (-136))))
+(-3255 (|has| |#1| (-134)) (-12 (|has| |#1| (-339)) (|has| |#2| (-134))))
(((|#4|) . T))
(|has| |#1| (-134))
((((-1070) |#1|) . T))
@@ -1316,10 +1316,10 @@
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#3|) . T))
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))) (((-888 |#1|)) . T))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))) (((-888 |#1|)) . T))
(|has| |#1| (-784))
(|has| |#1| (-784))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
@@ -1332,8 +1332,8 @@
((($) . T))
((((-364) (-1070)) . T))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((((-794)) -3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
-(((#0=(-51)) . T) (((-2 (|:| -3772 (-1070)) (|:| -2482 #0#))) . T))
+((((-794)) -3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-563 (-794))) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016))) (((-1169 |#2|)) . T))
+(((#0=(-51)) . T) (((-2 (|:| -2402 (-1070)) (|:| -2746 #0#))) . T))
(((|#1|) . T))
((((-794)) . T))
(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
@@ -1341,7 +1341,7 @@
(|has| |#2| (-134))
(|has| |#2| (-136))
(|has| |#1| (-448))
-(-3172 (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
(|has| |#1| (-339))
((((-794)) . T))
(|has| |#1| (-37 (-383 (-523))))
@@ -1350,8 +1350,8 @@
(|has| |#1| (-784))
(|has| |#1| (-784))
((((-794)) . T))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1| |#2|) . T))
((((-1087)) |has| |#1| (-831 (-1087))))
@@ -1359,7 +1359,7 @@
((((-794)) . T))
((((-794)) . T))
(|has| |#1| (-1016))
-(((|#2| (-456 (-2810 |#1|) (-710)) (-796 |#1|)) . T))
+(((|#2| (-456 (-1271 |#1|) (-710)) (-796 |#1|)) . T))
((((-383 (-523))) . #0=(|has| |#2| (-339))) (($) . #0#))
(((|#1| (-495 (-1087)) (-1087)) . T))
(((|#1|) . T))
@@ -1379,16 +1379,16 @@
(|has| |#1| (-136))
(((|#1|) . T))
(((|#2|) . T))
-(((|#1|) . T) (((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+(((|#1|) . T) (((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
((((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-1087) (-51)) . T))
((($ $) . T))
(((|#1| (-523)) . T))
((((-841 |#1|)) . T))
-(((|#1|) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))) (($) -3172 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973))))
+(((|#1|) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))) (($) -3255 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973))))
(((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) |has| |#1| (-964 (-383 (-523)))))
(|has| |#1| (-786))
(|has| |#1| (-786))
@@ -1403,13 +1403,13 @@
(((|#4| |#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
(((|#1|) |has| |#1| (-158)))
(((|#4| |#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
-(((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339))))
+(((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339))))
(|has| |#2| (-786))
(|has| |#1| (-786))
-(-3172 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-840)))
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
((((-523) |#2|) . T))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339))))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339))))
(|has| |#1| (-325))
(((|#3| |#3|) -12 (|has| |#3| (-286 |#3|)) (|has| |#3| (-1016))))
((($) . T) (((-383 (-523))) . T))
@@ -1417,7 +1417,7 @@
(|has| |#1| (-759))
(|has| |#1| (-759))
(((|#1|) . T))
-(-3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-784))
(|has| |#1| (-784))
(|has| |#1| (-784))
@@ -1426,13 +1426,13 @@
((((-523)) . T) (($) . T) (((-383 (-523))) . T))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-37 (-383 (-523))))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-1087)) |has| |#1| (-831 (-1087))) (((-1001)) . T))
(((|#1|) . T))
(|has| |#1| (-784))
-(((#0=(-2 (|:| -3772 (-1070)) (|:| -2482 (-51))) #0#) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 (-51))))))
+(((#0=(-2 (|:| -2402 (-1070)) (|:| -2746 (-51))) #0#) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 (-51))))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(|has| |#1| (-1016))
(((|#1|) . T))
@@ -1450,7 +1450,7 @@
(((|#1|) . T))
((((-133)) . T))
(((|#2|) |has| |#2| (-158)))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
(((|#1|) . T))
(|has| |#1| (-134))
(|has| |#1| (-136))
@@ -1472,32 +1472,32 @@
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T))
(((|#1| |#2|) . T))
-(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) ((#0=(-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) #0#) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)))))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
+(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) ((#0=(-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) #0#) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)))))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
(((|#1|) . T) (($) . T))
(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(((|#1| |#2|) . T))
(((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
-(((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339))))
+(((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339))))
(|has| |#1| (-786))
(|has| |#1| (-515))
((((-536 |#1|)) . T))
((($) . T))
(((|#2|) . T))
-(-3172 (-12 (|has| |#1| (-339)) (|has| |#2| (-759))) (-12 (|has| |#1| (-339)) (|has| |#2| (-786))))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (-12 (|has| |#1| (-339)) (|has| |#2| (-759))) (-12 (|has| |#1| (-339)) (|has| |#2| (-786))))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
((((-841 |#1|)) . T))
(((|#1| (-467 |#1| |#3|) (-467 |#1| |#2|)) . T))
(((|#1| |#4| |#5|) . T))
(((|#1| (-710)) . T))
((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) |has| |#1| (-158)) (($) |has| |#1| (-515)))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
-(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)) ((|#1|) |has| |#1| (-158)))
+(((|#1|) |has| |#1| (-158)) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
((((-383 |#2|)) . T) (((-383 (-523))) . T) (($) . T))
((((-614 |#1|)) . T))
(((|#1| |#2| |#3| |#4|) . T))
@@ -1505,17 +1505,17 @@
((((-794)) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-794)) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
((((-794)) . T))
((((-794)) . T))
((((-794)) . T))
(((|#2|) . T))
-(-3172 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
(|has| |#1| (-1109))
(|has| |#1| (-1109))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
(|has| |#1| (-1109))
(|has| |#1| (-1109))
(((|#3| |#3|) . T))
@@ -1528,43 +1528,43 @@
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
((((-1070) (-51)) . T))
(|has| |#1| (-1016))
-(-3172 (|has| |#2| (-759)) (|has| |#2| (-786)))
+(-3255 (|has| |#2| (-759)) (|has| |#2| (-786)))
(((|#1|) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
(((|#1|) |has| |#1| (-158)) (($) . T))
((($) . T))
((((-1085 |#1| |#2| |#3|)) -12 (|has| (-1085 |#1| |#2| |#3|) (-286 (-1085 |#1| |#2| |#3|))) (|has| |#1| (-339))))
((((-794)) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
((($) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-794)) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
(|has| |#2| (-840))
(|has| |#1| (-339))
(((|#2|) |has| |#2| (-1016)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((($) . T) ((|#2|) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
(|has| |#1| (-840))
(|has| |#1| (-840))
((((-499)) . T) (((-383 (-1083 (-523)))) . T) (((-203)) . T) (((-355)) . T))
((((-355)) . T) (((-203)) . T) (((-794)) . T))
(|has| |#1| (-840))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1|) . T))
(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
((($ $) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((($ $) . T))
((((-523) (-108)) . T))
((($) . T))
(((|#1|) . T))
((((-523)) . T))
((((-108)) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-37 (-383 (-523))))
(((|#1| (-523)) . T))
((($) . T))
@@ -1586,7 +1586,7 @@
(((|#1| (-1133 |#1| |#2| |#3|)) . T))
(((|#1| (-710)) . T))
(((|#1|) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-794)) . T))
(|has| |#1| (-1016))
((((-1070) |#1|) . T))
@@ -1606,18 +1606,18 @@
(((|#1|) . T))
((((-523)) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-325)))
((((-794)) . T))
(|has| |#1| (-136))
(((|#3|) . T))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-794)) . T))
((((-1154 |#2| |#3| |#4|)) . T) (((-1155 |#1| |#2| |#3| |#4|)) . T))
((((-794)) . T))
-((((-47)) -12 (|has| |#1| (-515)) (|has| |#1| (-964 (-523)))) (((-562 $)) . T) ((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) -3172 (-12 (|has| |#1| (-515)) (|has| |#1| (-964 (-523)))) (|has| |#1| (-964 (-383 (-523))))) (((-383 (-883 |#1|))) |has| |#1| (-515)) (((-883 |#1|)) |has| |#1| (-973)) (((-1087)) . T))
+((((-47)) -12 (|has| |#1| (-515)) (|has| |#1| (-964 (-523)))) (((-562 $)) . T) ((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) -3255 (-12 (|has| |#1| (-515)) (|has| |#1| (-964 (-523)))) (|has| |#1| (-964 (-383 (-523))))) (((-383 (-883 |#1|))) |has| |#1| (-515)) (((-883 |#1|)) |has| |#1| (-973)) (((-1087)) . T))
(((|#1|) . T) (($) . T))
(((|#1| (-710)) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
(((|#1|) |has| |#1| (-286 |#1|)))
((((-1155 |#1| |#2| |#3| |#4|)) . T))
((((-523)) |has| |#1| (-817 (-523))) (((-355)) |has| |#1| (-817 (-355))))
@@ -1625,14 +1625,14 @@
(|has| |#1| (-515))
(((|#1|) . T))
((((-794)) . T))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((|#1|) |has| |#1| (-158)))
((($) |has| |#1| (-515)) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(((|#1|) . T))
(((|#3|) |has| |#3| (-1016)))
-(((|#2|) -3172 (|has| |#2| (-158)) (|has| |#2| (-339))))
+(((|#2|) -3255 (|has| |#2| (-158)) (|has| |#2| (-339))))
((((-1154 |#2| |#3| |#4|)) . T))
((((-108)) . T))
(|has| |#1| (-759))
@@ -1642,8 +1642,8 @@
(|has| |#1| (-784))
(|has| |#1| (-784))
(((|#1| (-523) (-1001)) . T))
-(-3172 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+(-3255 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1| (-383 (-523)) (-1001)) . T))
(((|#1| (-710) (-1001)) . T))
(|has| |#1| (-786))
@@ -1659,28 +1659,28 @@
(((|#1|) . T))
(|has| |#1| (-1016))
((((-523)) -12 (|has| |#1| (-339)) (|has| |#2| (-585 (-523)))) ((|#2|) |has| |#1| (-339)))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
(((|#2|) |has| |#2| (-158)))
(((|#1|) |has| |#1| (-158)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
((((-794)) . T))
(|has| |#3| (-784))
((((-794)) . T))
((((-1154 |#2| |#3| |#4|) (-295 |#2| |#3| |#4|)) . T))
((((-794)) . T))
-(((|#1| |#1|) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))))
+(((|#1| |#1|) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))))
(((|#1|) . T))
((((-523)) . T))
((((-523)) . T))
-(((|#1|) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))))
+(((|#1|) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-973))))
(((|#2|) |has| |#2| (-339)))
((($) . T) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-339)))
(|has| |#1| (-786))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#2|) . T))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) |has| (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))))))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-840)))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) |has| (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))))))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-840)))
(((|#2|) . T) (((-523)) |has| |#2| (-585 (-523))))
((((-794)) . T))
((((-794)) . T))
@@ -1714,18 +1714,18 @@
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
(((|#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) . T) (($ $) . T))
((((-794)) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
((($) . T) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(|has| |#1| (-339))
(|has| |#1| (-339))
(|has| (-383 |#2|) (-211))
(|has| |#1| (-840))
(((|#2|) |has| |#2| (-973)))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(|has| |#1| (-339))
(((|#1|) |has| |#1| (-158)))
(((|#1| |#1|) . T))
@@ -1750,7 +1750,7 @@
(((|#1| (-383 (-523)) (-1001)) . T))
(((|#1| (-710) (-1001)) . T))
(((#0=(-383 |#2|) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
-(((|#1|) . T) (((-523)) -3172 (|has| (-383 (-523)) (-964 (-523))) (|has| |#1| (-964 (-523)))) (((-383 (-523))) . T))
+(((|#1|) . T) (((-523)) -3255 (|has| (-383 (-523)) (-964 (-523))) (|has| |#1| (-964 (-523)))) (((-383 (-523))) . T))
(((|#1| (-554 |#1| |#3|) (-554 |#1| |#2|)) . T))
(((|#1|) |has| |#1| (-158)))
(((|#1|) . T))
@@ -1769,24 +1769,24 @@
((((-638)) . T))
(((|#2|) |has| |#2| (-158)))
(|has| |#2| (-784))
-((((-108)) |has| |#1| (-1016)) (((-794)) -3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016))))
+((((-108)) |has| |#1| (-1016)) (((-794)) -3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016))))
(((|#1|) . T) (($) . T))
(((|#1| |#2|) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 (-51)))) . T))
((((-794)) . T))
((((-523) |#1|) . T))
((((-638)) . T) (((-383 (-523))) . T) (((-523)) . T))
(((|#1| |#1|) |has| |#1| (-158)))
(((|#2|) . T))
-(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
((((-355)) . T))
((((-638)) . T))
((((-383 (-523))) . #0=(|has| |#2| (-339))) (($) . #0#))
(((|#1|) |has| |#1| (-158)))
((((-383 (-883 |#1|))) . T))
(((|#2| |#2|) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#2|) . T))
(|has| |#2| (-786))
(((|#3|) |has| |#3| (-973)))
@@ -1796,14 +1796,14 @@
(|has| |#1| (-786))
((((-1087)) |has| |#2| (-831 (-1087))))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-383 (-523))) . T) (($) . T))
(|has| |#1| (-448))
(|has| |#1| (-344))
(|has| |#1| (-344))
(|has| |#1| (-344))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-448)) (|has| |#1| (-515)) (|has| |#1| (-973)) (|has| |#1| (-1028)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-448)) (|has| |#1| (-515)) (|has| |#1| (-973)) (|has| |#1| (-1028)))
(|has| |#1| (-37 (-383 (-523))))
((((-112 |#1|)) . T))
((((-112 |#1|)) . T))
@@ -1824,11 +1824,11 @@
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-786))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(((|#1| |#2|) . T))
(|has| |#1| (-136))
(|has| |#1| (-134))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))) ((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))) ((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(((|#2|) . T))
(((|#3|) . T))
((((-112 |#1|)) . T))
@@ -1846,11 +1846,11 @@
((((-499)) |has| |#1| (-564 (-499))) (((-823 (-523))) |has| |#1| (-564 (-823 (-523)))) (((-823 (-355))) |has| |#1| (-564 (-823 (-355)))) (((-355)) . #0=(|has| |#1| (-949))) (((-203)) . #0#))
(((|#1|) |has| |#1| (-339)))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((($ $) . T) (((-562 $) $) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
((($) . T) (((-1155 |#1| |#2| |#3| |#4|)) . T) (((-383 (-523))) . T))
-((($) -3172 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-515)))
+((($) -3255 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-515)))
(|has| |#1| (-339))
(|has| |#1| (-339))
(|has| |#1| (-339))
@@ -1861,11 +1861,11 @@
((((-355)) . T))
(((|#3|) -12 (|has| |#3| (-286 |#3|)) (|has| |#3| (-1016))))
((((-794)) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-840)))
(((|#1|) . T))
(|has| |#1| (-786))
(|has| |#1| (-786))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(|has| |#1| (-1016))
@@ -1874,13 +1874,13 @@
(|has| |#1| (-134))
(|has| |#1| (-136))
((((-523)) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(((#0=(-1154 |#2| |#3| |#4|)) . T) (((-383 (-523))) |has| #0# (-37 (-383 (-523)))) (($) . T))
((((-523)) . T))
(|has| |#1| (-339))
-(-3172 (-12 (|has| (-1161 |#1| |#2| |#3|) (-136)) (|has| |#1| (-339))) (|has| |#1| (-136)))
-(-3172 (-12 (|has| (-1161 |#1| |#2| |#3|) (-134)) (|has| |#1| (-339))) (|has| |#1| (-134)))
+(-3255 (-12 (|has| (-1161 |#1| |#2| |#3|) (-136)) (|has| |#1| (-339))) (|has| |#1| (-136)))
+(-3255 (-12 (|has| (-1161 |#1| |#2| |#3|) (-134)) (|has| |#1| (-339))) (|has| |#1| (-134)))
(|has| |#1| (-339))
(|has| |#1| (-134))
(|has| |#1| (-136))
@@ -1897,18 +1897,18 @@
(((|#1| |#2|) . T))
(((|#1|) . T) (((-523)) |has| |#1| (-585 (-523))))
(((|#3|) |has| |#3| (-158)))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
((((-523)) . T))
(((|#1| $) |has| |#1| (-263 |#1| |#1|)))
((((-383 (-523))) . T) (($) . T) (((-383 |#1|)) . T) ((|#1|) . T))
((((-794)) . T))
(((|#3|) . T))
-(((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-267)) (|has| |#1| (-339))) ((#0=(-383 (-523)) #0#) |has| |#1| (-339)))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+(((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-267)) (|has| |#1| (-339))) ((#0=(-383 (-523)) #0#) |has| |#1| (-339)))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
((($) . T))
((((-523) |#1|) . T))
((((-1087)) |has| (-383 |#2|) (-831 (-1087))))
-(((|#1|) . T) (($) -3172 (|has| |#1| (-267)) (|has| |#1| (-339))) (((-383 (-523))) |has| |#1| (-339)))
+(((|#1|) . T) (($) -3255 (|has| |#1| (-267)) (|has| |#1| (-339))) (((-383 (-523))) |has| |#1| (-339)))
((((-499)) |has| |#2| (-564 (-499))))
((((-629 |#2|)) . T) (((-794)) . T))
(((|#1|) . T))
@@ -1916,8 +1916,8 @@
(((|#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
((((-801 |#1|)) . T))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-(-3172 (|has| |#4| (-732)) (|has| |#4| (-784)))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#4| (-732)) (|has| |#4| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
((((-794)) . T))
((((-794)) . T))
(((|#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
@@ -1933,17 +1933,17 @@
((((-383 (-523))) . T) (($) . T))
((((-383 (-523))) . T) (($) . T))
((((-383 (-523))) . T) (($) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-1127)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-1127)))
((($) . T))
((((-383 (-523))) |has| #0=(-383 |#2|) (-964 (-383 (-523)))) (((-523)) |has| #0# (-964 (-523))) ((#0#) . T))
(((|#2|) . T) (((-523)) |has| |#2| (-585 (-523))))
(((|#1| (-710)) . T))
(|has| |#1| (-786))
(((|#1|) . T) (((-523)) |has| |#1| (-585 (-523))))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-523)) . T))
(|has| |#1| (-37 (-383 (-523))))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 (-51)))) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 (-51))))))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 (-51)))) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 (-51))))))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(|has| |#1| (-784))
(|has| |#1| (-37 (-383 (-523))))
@@ -1968,24 +1968,24 @@
(((|#1| |#2|) . T))
((((-133)) . T))
((((-719 |#1| (-796 |#2|))) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(|has| |#1| (-1109))
(((|#1|) . T))
-(-3172 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016)))
+(-3255 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-344)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)) (|has| |#3| (-1016)))
((((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)))
(((|#2|) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-841 |#1|)) . T))
((($) . T))
((((-383 (-883 |#1|))) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-499)) |has| |#4| (-564 (-499))))
((((-794)) . T) (((-589 |#4|)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) . T))
(|has| |#1| (-784))
-(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) (((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) |has| (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)) (-286 (-2 (|:| -3772 (-1070)) (|:| -2482 |#1|)))))
+(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))) (((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) |has| (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)) (-286 (-2 (|:| -2402 (-1070)) (|:| -2746 |#1|)))))
(|has| |#1| (-1016))
(|has| |#1| (-339))
(|has| |#1| (-786))
@@ -1993,16 +1993,16 @@
(((|#1|) . T))
(((|#1|) . T))
((($) . T) (((-383 (-523))) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) |has| |#1| (-158)))
(|has| |#1| (-134))
(|has| |#1| (-136))
-(-3172 (-12 (|has| (-1085 |#1| |#2| |#3|) (-136)) (|has| |#1| (-339))) (|has| |#1| (-136)))
-(-3172 (-12 (|has| (-1085 |#1| |#2| |#3|) (-134)) (|has| |#1| (-339))) (|has| |#1| (-134)))
+(-3255 (-12 (|has| (-1085 |#1| |#2| |#3|) (-136)) (|has| |#1| (-339))) (|has| |#1| (-136)))
+(-3255 (-12 (|has| (-1085 |#1| |#2| |#3|) (-134)) (|has| |#1| (-339))) (|has| |#1| (-134)))
(|has| |#1| (-134))
(|has| |#1| (-136))
(|has| |#1| (-136))
(|has| |#1| (-134))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
(|has| |#1| (-784))
(((|#1| |#2|) . T))
@@ -2025,9 +2025,9 @@
((((-794)) . T))
((((-794)) . T))
((((-499)) |has| |#1| (-564 (-499))))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)) ((|#1| |#1|) |has| |#1| (-286 |#1|)))
-(((|#1|) -3172 (|has| |#1| (-158)) (|has| |#1| (-339))))
+(((|#1|) -3255 (|has| |#1| (-158)) (|has| |#1| (-339))))
((((-292 |#1|)) . T))
(((|#2|) |has| |#2| (-339)))
(((|#2|) . T))
@@ -2048,14 +2048,14 @@
(|has| |#1| (-134))
(|has| |#1| (-136))
((($ $) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016)))
(|has| |#1| (-515))
(((|#2|) . T))
((((-523)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
((((-536 |#1|)) . T))
((($) . T))
(((|#1| (-57 |#1|) (-57 |#1|)) . T))
@@ -2080,12 +2080,12 @@
(((|#1| |#2|) . T))
((((-1087) |#1|) . T))
(((|#4|) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
((((-1087) (-51)) . T))
((((-1154 |#2| |#3| |#4|) (-295 |#2| |#3| |#4|)) . T))
((((-383 (-523))) |has| |#1| (-964 (-383 (-523)))) (((-523)) |has| |#1| (-964 (-523))) ((|#1|) . T))
((((-794)) . T))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-344)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)) (|has| |#2| (-1016)))
(((#0=(-1155 |#1| |#2| |#3| |#4|) #0#) . T) ((#1=(-383 (-523)) #1#) . T) (($ $) . T))
(((|#1| |#1|) |has| |#1| (-158)) ((#0=(-383 (-523)) #0#) |has| |#1| (-515)) (($ $) |has| |#1| (-515)))
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
@@ -2104,14 +2104,14 @@
(((|#1|) . T))
(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(((|#2| |#3|) . T))
-(-3172 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-339)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(((|#1| (-495 |#2|)) . T))
(((|#1| (-710)) . T))
(((|#1| (-495 (-1006 (-1087)))) . T))
(((|#1|) |has| |#1| (-158)))
(((|#1|) . T))
(|has| |#2| (-840))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
((((-794)) . T))
((($ $) . T) ((#0=(-1154 |#2| |#3| |#4|) #0#) . T) ((#1=(-383 (-523)) #1#) |has| #0# (-37 (-383 (-523)))))
((((-841 |#1|)) . T))
@@ -2120,13 +2120,13 @@
((($) . T))
((($) . T))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)) (|has| |#1| (-515)))
(|has| |#1| (-339))
((($) . T) ((#0=(-1154 |#2| |#3| |#4|)) . T) (((-383 (-523))) |has| #0# (-37 (-383 (-523)))))
(((|#1| |#2|) . T))
((((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)))
-(-3172 (-12 (|has| |#1| (-284)) (|has| |#1| (-840))) (|has| |#1| (-339)) (|has| |#1| (-325)))
-(-3172 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
+(-3255 (-12 (|has| |#1| (-284)) (|has| |#1| (-840))) (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)))
((((-523)) |has| |#1| (-585 (-523))) ((|#1|) . T))
(((|#1| |#2|) . T))
((((-794)) . T))
@@ -2158,27 +2158,27 @@
(((|#1|) |has| |#1| (-158)))
((((-794)) . T))
(((|#4| |#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
-(((|#2|) -3172 (|has| |#2| (-6 (-4250 "*"))) (|has| |#2| (-158))))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(((|#2|) -3255 (|has| |#2| (-6 (-4250 "*"))) (|has| |#2| (-158))))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(|has| |#2| (-786))
(|has| |#2| (-840))
(|has| |#1| (-840))
(((|#2|) |has| |#2| (-158)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
((((-794)) . T))
((((-794)) . T))
((((-499)) . T) (((-523)) . T) (((-823 (-523))) . T) (((-355)) . T) (((-203)) . T))
(((|#1| |#2|) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 (-51)))) . T))
(((|#1|) . T))
((((-794)) . T))
(((|#1| |#2|) . T))
(((|#1| (-383 (-523))) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-267)) (|has| |#1| (-339)))
+(-3255 (|has| |#1| (-267)) (|has| |#1| (-339)))
((((-133)) . T))
((((-383 |#2|)) . T) (((-383 (-523))) . T) (($) . T))
(|has| |#1| (-784))
@@ -2193,7 +2193,7 @@
((((-383 (-523))) . T) (($) . T))
((((-794)) . T))
((((-794)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#2| |#2|) . T) ((|#1| |#1|) . T))
((((-794)) . T))
((((-794)) . T))
@@ -2204,7 +2204,7 @@
(((|#1|) . T))
((((-589 (-133))) . T) (((-1070)) . T))
((((-794)) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
((((-1087) |#1|) |has| |#1| (-484 (-1087) |#1|)) ((|#1| |#1|) |has| |#1| (-286 |#1|)))
(|has| |#1| (-786))
((((-794)) . T))
@@ -2216,16 +2216,16 @@
((((-794)) . T) (((-589 |#4|)) . T))
(((|#2|) . T))
((((-841 |#1|)) . T) (((-383 (-523))) . T) (($) . T))
-(-3172 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-1087) (-51)) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(|has| |#1| (-840))
(|has| |#1| (-840))
(((|#2|) . T))
@@ -2240,12 +2240,12 @@
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(|has| |#1| (-759))
(((#0=(-841 |#1|) #0#) . T) (($ $) . T) ((#1=(-383 (-523)) #1#) . T))
((((-383 |#2|)) . T))
(|has| |#1| (-784))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) . T) ((#1=(-523) #1#) . T) (($ $) . T))
((((-841 |#1|)) . T) (($) . T) (((-383 (-523))) . T))
(((|#2|) |has| |#2| (-973)) (((-523)) -12 (|has| |#2| (-585 (-523))) (|has| |#2| (-973))))
@@ -2255,25 +2255,25 @@
(|has| |#1| (-134))
(((|#2|) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
-(((#0=(-51)) . T) (((-2 (|:| -3772 (-1087)) (|:| -2482 #0#))) . T))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
+(((#0=(-51)) . T) (((-2 (|:| -2402 (-1087)) (|:| -2746 #0#))) . T))
(|has| |#1| (-325))
((((-523)) . T))
((((-794)) . T))
(((#0=(-1155 |#1| |#2| |#3| |#4|) $) |has| #0# (-263 #0# #0#)))
(|has| |#1| (-339))
(((#0=(-1001) |#1|) . T) ((#0# $) . T) (($ $) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
(((#0=(-383 (-523)) #0#) . T) ((#1=(-638) #1#) . T) (($ $) . T))
((((-292 |#1|)) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) |has| |#1| (-339)))
(|has| |#1| (-1016))
(((|#1|) . T))
-(((|#1|) -3172 (|has| |#2| (-343 |#1|)) (|has| |#2| (-393 |#1|))))
-(((|#1|) -3172 (|has| |#2| (-343 |#1|)) (|has| |#2| (-393 |#1|))))
+(((|#1|) -3255 (|has| |#2| (-343 |#1|)) (|has| |#2| (-393 |#1|))))
+(((|#1|) -3255 (|has| |#2| (-343 |#1|)) (|has| |#2| (-393 |#1|))))
(((|#2|) . T))
((((-383 (-523))) . T) (((-638)) . T) (($) . T))
(((|#3| |#3|) . T))
@@ -2292,7 +2292,7 @@
(((|#2|) . T))
(((|#1|) . T))
((((-523)) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#2|) . T) (((-523)) |has| |#2| (-585 (-523))))
(((|#1| |#2|) . T))
((($) . T))
@@ -2329,7 +2329,7 @@
(|has| |#2| (-949))
((($) . T))
(|has| |#1| (-840))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((($) . T))
(((|#2|) . T))
(((|#1|) . T))
@@ -2337,24 +2337,24 @@
((($) . T))
(|has| |#1| (-339))
((((-841 |#1|)) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
-(-3172 (|has| |#1| (-344)) (|has| |#1| (-786)))
+(-3255 (|has| |#1| (-344)) (|has| |#1| (-786)))
(((|#1|) . T))
((((-794)) . T))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|))) (|has| |#1| (-831 (-1087)))))
((((-383 |#2|) |#3|) . T))
((($) . T) (((-383 (-523))) . T))
((((-710) |#1|) . T))
-(((|#2| (-218 (-2810 |#1|) (-710))) . T))
+(((|#2| (-218 (-1271 |#1|) (-710))) . T))
(((|#1| (-495 |#3|)) . T))
((((-383 (-523))) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-794)) . T))
-(((#0=(-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) #0#) |has| (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))))))
+(((#0=(-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) #0#) |has| (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))))))
(|has| |#1| (-840))
(|has| |#2| (-339))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-155 (-355))) . T) (((-203)) . T) (((-355)) . T))
((((-794)) . T))
(((|#1|) . T))
@@ -2371,11 +2371,11 @@
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-37 (-383 (-523))))
(-12 (|has| |#1| (-508)) (|has| |#1| (-767)))
((((-794)) . T))
-((((-1087)) -3172 (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087)))) (-12 (|has| |#1| (-339)) (|has| |#2| (-831 (-1087))))))
+((((-1087)) -3255 (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087)))) (-12 (|has| |#1| (-339)) (|has| |#2| (-831 (-1087))))))
(|has| |#1| (-339))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|))) (|has| |#1| (-831 (-1087)))))
(|has| |#1| (-339))
@@ -2385,7 +2385,7 @@
(((|#1|) . T))
(((|#2|) |has| |#1| (-339)))
(((|#2|) |has| |#1| (-339)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1|) . T))
(((|#1|) |has| |#1| (-158)))
(((|#1|) . T))
@@ -2408,31 +2408,31 @@
(((|#2|) |has| |#1| (-339)))
((((-355)) -12 (|has| |#1| (-339)) (|has| |#2| (-817 (-355)))) (((-523)) -12 (|has| |#1| (-339)) (|has| |#2| (-817 (-523)))))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-339))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
(|has| |#1| (-339))
(|has| |#1| (-515))
(((|#4| |#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
(((|#3|) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#2|) . T))
(((|#2|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#1| (-37 (-383 (-523))))
(((|#1| |#2|) . T))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
((((-1070) |#1|) . T))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-344)))
(|has| |#1| (-136))
((((-536 |#1|)) . T))
((($) . T))
@@ -2440,7 +2440,7 @@
(|has| |#1| (-515))
(|has| |#1| (-37 (-383 (-523))))
(|has| |#1| (-37 (-383 (-523))))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-325)))
(|has| |#1| (-136))
((((-794)) . T))
((($) . T))
@@ -2465,7 +2465,7 @@
(|has| |#1| (-730))
(|has| |#1| (-730))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-110)) . T) ((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
@@ -2486,7 +2486,7 @@
((((-523)) . T))
((((-794)) . T))
((((-523)) . T))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
((((-155 (-355))) . T) (((-203)) . T) (((-355)) . T))
((((-794)) . T))
((((-794)) . T))
@@ -2498,9 +2498,9 @@
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
(|has| |#1| (-339))
(|has| |#1| (-339))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016)))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-448)) (|has| |#1| (-666)) (|has| |#1| (-831 (-1087))) (|has| |#1| (-973)) (|has| |#1| (-1028)) (|has| |#1| (-1016)))
(|has| |#1| (-1063))
((((-523) |#1|) . T))
(((|#1|) . T))
@@ -2518,8 +2518,8 @@
(((|#1|) . T))
(|has| |#1| (-515))
((((-383 |#2|)) . T) (((-383 (-523))) . T) (($) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
((((-355)) . T))
(((|#1|) . T))
(((|#1|) . T))
@@ -2528,7 +2528,7 @@
(|has| |#1| (-515))
(|has| |#1| (-1016))
((((-719 |#1| (-796 |#2|))) |has| (-719 |#1| (-796 |#2|)) (-286 (-719 |#1| (-796 |#2|)))))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(((|#1|) . T))
(((|#2| |#3|) . T))
(|has| |#2| (-840))
@@ -2538,12 +2538,12 @@
(|has| |#1| (-211))
(((|#1| (-495 (-1006 (-1087)))) . T))
(|has| |#2| (-339))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 (-51)))) . T))
(((|#1|) . T))
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
((((-794)) . T))
((((-794)) . T))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
((((-794)) . T))
((((-794)) . T))
(((|#1|) . T))
@@ -2552,8 +2552,8 @@
((((-523)) . T))
(((|#3|) . T))
((((-794)) . T))
-(-3172 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
-(-3172 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
+(-3255 (|has| |#1| (-284)) (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-134)) (|has| |#1| (-136)) (|has| |#1| (-158)) (|has| |#1| (-515)) (|has| |#1| (-973)))
(((#0=(-536 |#1|) #0#) . T) (($ $) . T) ((#1=(-383 (-523)) #1#) . T))
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
(((|#1|) |has| |#1| (-158)))
@@ -2566,7 +2566,7 @@
(((|#1|) . T))
((((-794)) |has| |#1| (-563 (-794))))
((((-271 |#3|)) . T))
-(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
(((|#2| |#2|) . T) ((|#6| |#6|) . T))
(((|#1|) . T))
((($) . T) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T))
@@ -2574,20 +2574,20 @@
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
(((|#1|) . T) (((-383 (-523))) . T) (($) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
(((|#2|) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
(((|#2|) . T) ((|#6|) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
((((-794)) . T))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(|has| |#2| (-840))
(|has| |#1| (-840))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) . T))
-((((-2 (|:| -3772 (-1070)) (|:| -2482 |#1|))) . T))
+((((-2 (|:| -2402 (-1070)) (|:| -2746 |#1|))) . T))
(((|#1|) . T))
(((|#1|) . T))
(((|#1| |#1|) . T))
@@ -2601,10 +2601,10 @@
(((|#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))))
(((#0=(-383 (-523)) #0#) . T))
((((-383 (-523))) . T))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#1|) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-499)) . T))
((((-794)) . T))
((((-1087)) |has| |#2| (-831 (-1087))) (((-1001)) . T))
@@ -2618,12 +2618,12 @@
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
((((-1087)) |has| |#1| (-831 (-1087))))
((((-841 |#1|)) . T) (((-383 (-523))) . T) (($) . T))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) . T))
-(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#1|) . T))
+(((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))) ((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
((($) . T) (((-383 (-523))) . T))
(((|#1|) . T) (((-383 (-523))) . T) (((-523)) . T) (($) . T))
(((|#2|) |has| |#2| (-973)) (((-523)) -12 (|has| |#2| (-585 (-523))) (|has| |#2| (-973))))
-((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-515))))
+((((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-515))))
(|has| |#1| (-515))
(((|#1|) |has| |#1| (-339)))
((((-523)) . T))
@@ -2642,8 +2642,8 @@
((((-794)) . T))
(|has| |#2| (-759))
(|has| |#2| (-759))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2|) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
-(((|#1|) . T) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2|) |has| |#1| (-339)) (($) . T) ((|#1|) . T))
+(((|#1|) . T) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) . T))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1|) . T) (((-523)) |has| |#1| (-964 (-523))) (((-383 (-523))) |has| |#1| (-964 (-383 (-523)))))
((((-523)) |has| |#1| (-817 (-523))) (((-355)) |has| |#1| (-817 (-355))))
@@ -2669,12 +2669,12 @@
(((|#2| (-710)) . T))
((((-1087)) . T))
((((-801 |#1|)) . T))
-(-3172 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-25)) (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-794)) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-732)) (|has| |#2| (-784)))
-(-3172 (-12 (|has| |#1| (-732)) (|has| |#2| (-732))) (-12 (|has| |#1| (-786)) (|has| |#2| (-786))))
+(-3255 (|has| |#2| (-732)) (|has| |#2| (-784)))
+(-3255 (-12 (|has| |#1| (-732)) (|has| |#2| (-732))) (-12 (|has| |#1| (-786)) (|has| |#2| (-786))))
((((-801 |#1|)) . T))
(((|#1|) . T))
(|has| |#1| (-344))
@@ -2700,7 +2700,7 @@
(((|#1|) . T))
((((-794)) . T))
(|has| |#2| (-840))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
((((-499)) |has| |#2| (-564 (-499))) (((-823 (-355))) |has| |#2| (-564 (-823 (-355)))) (((-823 (-523))) |has| |#2| (-564 (-823 (-523)))))
((((-794)) . T))
((((-794)) . T))
@@ -2733,11 +2733,11 @@
((((-383 |#2|) |#3|) . T))
(((|#1|) . T))
(|has| |#1| (-1016))
-(((|#2| (-456 (-2810 |#1|) (-710))) . T))
+(((|#2| (-456 (-1271 |#1|) (-710))) . T))
((((-523) |#1|) . T))
(((|#2| |#2|) . T))
(((|#1| (-495 (-1087))) . T))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-523)) . T))
(((|#2|) . T))
(((|#2|) . T))
@@ -2747,9 +2747,9 @@
((($) . T) (((-383 (-523))) . T))
((($) . T))
((($) . T))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
(((|#1|) . T))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-794)) . T))
((((-133)) . T))
(((|#1|) . T) (((-383 (-523))) . T))
@@ -2789,27 +2789,27 @@
(|has| |#1| (-211))
(((|#1| (-495 |#3|)) . T))
(|has| |#1| (-344))
-(((|#2| (-218 (-2810 |#1|) (-710))) . T))
+(((|#2| (-218 (-1271 |#1|) (-710))) . T))
(|has| |#1| (-344))
(|has| |#1| (-344))
(((|#1|) . T) (($) . T))
(((|#1| (-495 |#2|)) . T))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#1| (-710)) . T))
(|has| |#1| (-515))
-(-3172 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-25)) (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(-12 (|has| |#1| (-21)) (|has| |#2| (-21)))
((((-794)) . T))
-(-3172 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
-(-3172 (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
+(-3255 (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
(((|#1|) |has| |#1| (-158)))
(((|#4|) |has| |#4| (-973)))
(((|#3|) |has| |#3| (-973)))
(-12 (|has| |#1| (-339)) (|has| |#2| (-759)))
(-12 (|has| |#1| (-339)) (|has| |#2| (-759)))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
((((-383 |#2|)) . T) (((-383 (-523))) . T) (($) . T))
((($ $) . T) ((#0=(-383 (-523)) #0#) . T))
@@ -2822,14 +2822,14 @@
(((|#2|) |has| |#2| (-973)) (((-523)) -12 (|has| |#2| (-585 (-523))) (|has| |#2| (-973))))
(((|#1|) . T))
(|has| |#2| (-339))
-(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
+(((#0=(-383 (-523)) #0#) |has| |#2| (-37 (-383 (-523)))) ((|#2| |#2|) . T) (($ $) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1| |#1|) . T) ((#0=(-383 (-523)) #0#) |has| |#1| (-37 (-383 (-523)))))
(((|#1| |#1|) . T) (($ $) . T) ((#0=(-383 (-523)) #0#) . T))
(((|#1| |#1|) . T) (($ $) . T) ((#0=(-383 (-523)) #0#) . T))
(((|#1| |#1|) . T) (($ $) . T) ((#0=(-383 (-523)) #0#) . T))
(((|#2| |#2|) . T))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T) (($) -3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
(((|#1|) . T) (($) . T) (((-383 (-523))) . T))
@@ -2848,25 +2848,25 @@
(((|#1|) |has| |#2| (-393 |#1|)))
(((|#1|) |has| |#2| (-393 |#1|)))
((((-841 |#1|)) . T) (((-383 (-523))) . T) (($) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
((((-794)) . T))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) |has| (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))) (-286 (-2 (|:| -3772 (-1087)) (|:| -2482 (-51))))))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) |has| (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))) (-286 (-2 (|:| -2402 (-1087)) (|:| -2746 (-51))))))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
((((-523) |#1|) . T))
((((-523) |#1|) . T))
((((-523) |#1|) . T))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-523) |#1|) . T))
(((|#1|) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((((-1087)) |has| |#1| (-831 (-1087))) (((-757 (-1087))) . T))
-(-3172 (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-124)) (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-732)) (|has| |#3| (-784)) (|has| |#3| (-973)))
((((-758 |#1|)) . T))
(((|#1| |#2|) . T))
((((-794)) . T))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
(((|#1| |#2|) . T))
(|has| |#1| (-37 (-383 (-523))))
((((-794)) . T))
@@ -2874,15 +2874,15 @@
(((|#1|) |has| |#1| (-158)) (($) |has| |#1| (-515)) (((-383 (-523))) |has| |#1| (-515)))
(((|#2|) . T) (((-523)) |has| |#2| (-585 (-523))))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (-12 (|has| |#1| (-339)) (|has| |#2| (-211))))
+(-3255 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (-12 (|has| |#1| (-339)) (|has| |#2| (-211))))
(|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|)))
(|has| |#1| (-339))
(((|#1|) . T))
-(((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1| |#1|) . T))
+(((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1| |#1|) . T))
((((-523) |#1|) . T))
((((-292 |#1|)) . T))
(((#0=(-638) (-1083 #0#)) . T))
-((((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1|) . T))
+((((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((|#1|) . T))
(((|#1| |#2| |#3| |#4|) . T))
(|has| |#1| (-784))
((($ $) . T) ((#0=(-796 |#1|) $) . T) ((#0# |#2|) . T))
@@ -2899,12 +2899,12 @@
(((#0=(-1155 |#1| |#2| |#3| |#4|)) |has| #0# (-286 #0#)))
((($) . T))
(((|#1|) . T))
-((($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2| |#2|) |has| |#1| (-339)) ((|#1| |#1|) . T))
-(((|#1| |#1|) . T) (($ $) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2| |#2|) |has| |#1| (-339)) ((|#1| |#1|) . T))
+(((|#1| |#1|) . T) (($ $) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) ((#0=(-383 (-523)) #0#) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
(|has| |#2| (-211))
(|has| $ (-136))
((((-794)) . T))
-((($) . T) (((-383 (-523))) -3172 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
+((($) . T) (((-383 (-523))) -3255 (|has| |#1| (-339)) (|has| |#1| (-325))) ((|#1|) . T))
((((-794)) . T))
(|has| |#1| (-784))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087)))))
@@ -2916,23 +2916,23 @@
(((|#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#4|) . T))
(|has| |#1| (-515))
-((($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2|) |has| |#1| (-339)) ((|#1|) . T))
-((((-1087)) -3172 (-12 (|has| (-1161 |#1| |#2| |#3|) (-831 (-1087))) (|has| |#1| (-339))) (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087))))))
-(((|#1|) . T) (($) -3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3172 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
+((($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))) ((|#2|) |has| |#1| (-339)) ((|#1|) . T))
+((((-1087)) -3255 (-12 (|has| (-1161 |#1| |#2| |#3|) (-831 (-1087))) (|has| |#1| (-339))) (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087))))))
+(((|#1|) . T) (($) -3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-515))) (((-383 (-523))) -3255 (|has| |#1| (-37 (-383 (-523)))) (|has| |#1| (-339))))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|))) (|has| |#1| (-831 (-1087)))))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-710) |#1|))) (|has| |#1| (-831 (-1087)))))
(((|#4|) -12 (|has| |#4| (-286 |#4|)) (|has| |#4| (-1016))))
((((-523) |#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
(((|#1|) . T))
(((|#1| (-495 (-757 (-1087)))) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#1|) . T))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
(((|#1|) . T))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(-3172 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
((($) . T) (((-801 |#1|)) . T) (((-383 (-523))) . T))
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
@@ -2941,15 +2941,15 @@
(((|#1|) . T))
(((|#1|) . T))
((((-383 |#2|)) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1|) . T))
(((|#2| |#2|) . T) ((#0=(-383 (-523)) #0#) . T) (($ $) . T))
((((-523)) . T))
@@ -2978,32 +2978,32 @@
((((-1161 |#1| |#2| |#3|)) |has| |#1| (-339)))
((((-1087)) . T) (((-794)) . T))
(|has| |#1| (-339))
-((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
+((((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) |has| |#2| (-158)) (($) -3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840))))
(((|#2|) . T) ((|#6|) . T))
((($) . T) (((-383 (-523))) |has| |#2| (-37 (-383 (-523)))) ((|#2|) . T))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
-((($) -3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
((((-1020)) . T))
((((-794)) . T))
((($) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))) ((|#1|) . T))
((($) . T))
-((($) -3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
+((($) -3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840))) ((|#1|) |has| |#1| (-158)) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(|has| |#2| (-840))
(|has| |#1| (-840))
(((|#1|) . T))
(((|#1|) . T))
(((|#1| |#1|) |has| |#1| (-158)))
((((-638)) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1|) |has| |#1| (-158)))
(((|#1|) |has| |#1| (-158)))
((((-383 (-523))) . T) (($) . T))
(((|#1| (-523)) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-339))
(|has| |#1| (-339))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
-(-3172 (|has| |#1| (-158)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-158)) (|has| |#1| (-515)))
(((|#1| (-523)) . T))
(((|#1| (-383 (-523))) . T))
(((|#1| (-710)) . T))
@@ -3018,16 +3018,16 @@
((((-823 (-355))) . T) (((-823 (-523))) . T) (((-1087)) . T) (((-499)) . T))
(((|#1|) . T))
((((-794)) . T))
-(-3172 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
-(-3172 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
+(-3255 (|has| |#2| (-124)) (|has| |#2| (-158)) (|has| |#2| (-339)) (|has| |#2| (-732)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-124)) (|has| |#2| (-124))) (-12 (|has| |#1| (-732)) (|has| |#2| (-732))))
((((-523)) . T))
((((-523)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(((|#1| |#2|) . T))
(((|#1|) . T))
-(-3172 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
+(-3255 (|has| |#2| (-158)) (|has| |#2| (-784)) (|has| |#2| (-973)))
((((-1087)) -12 (|has| |#2| (-831 (-1087))) (|has| |#2| (-973))))
-(-3172 (-12 (|has| |#1| (-448)) (|has| |#2| (-448))) (-12 (|has| |#1| (-666)) (|has| |#2| (-666))))
+(-3255 (-12 (|has| |#1| (-448)) (|has| |#2| (-448))) (-12 (|has| |#1| (-666)) (|has| |#2| (-666))))
(|has| |#1| (-134))
(|has| |#1| (-136))
(|has| |#1| (-339))
@@ -3051,7 +3051,7 @@
((((-1070) (-1087) (-523) (-203) (-794)) . T))
(((|#1| |#2| |#3| |#4|) . T))
(((|#1| |#2|) . T))
-(-3172 (|has| |#1| (-325)) (|has| |#1| (-344)))
+(-3255 (|has| |#1| (-325)) (|has| |#1| (-344)))
(((|#1| |#2|) . T))
((($) . T) ((|#1|) . T))
((((-794)) . T))
@@ -3059,7 +3059,7 @@
((($) . T) ((|#1|) . T) (((-383 (-523))) |has| |#1| (-37 (-383 (-523)))))
(((|#2|) |has| |#2| (-1016)) (((-523)) -12 (|has| |#2| (-964 (-523))) (|has| |#2| (-1016))) (((-383 (-523))) -12 (|has| |#2| (-964 (-383 (-523)))) (|has| |#2| (-1016))))
((((-499)) |has| |#1| (-564 (-499))))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-786)) (|has| |#1| (-1016))))
((($) . T) (((-383 (-523))) . T))
(|has| |#1| (-840))
(|has| |#1| (-840))
@@ -3068,14 +3068,14 @@
((((-794)) . T))
(((|#2| |#2|) . T))
(((|#1| |#1|) |has| |#1| (-158)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-515)))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-515)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
(((|#2|) . T))
-(-3172 (|has| |#1| (-21)) (|has| |#1| (-784)))
+(-3255 (|has| |#1| (-21)) (|has| |#1| (-784)))
(((|#1|) |has| |#1| (-158)))
(((|#1|) . T))
(((|#1|) . T))
-((((-794)) -3172 (-12 (|has| |#1| (-563 (-794))) (|has| |#2| (-563 (-794)))) (-12 (|has| |#1| (-1016)) (|has| |#2| (-1016)))))
+((((-794)) -3255 (-12 (|has| |#1| (-563 (-794))) (|has| |#2| (-563 (-794)))) (-12 (|has| |#1| (-1016)) (|has| |#2| (-1016)))))
((((-383 |#2|) |#3|) . T))
((((-383 (-523))) . T) (($) . T))
(|has| |#1| (-37 (-383 (-523))))
@@ -3087,17 +3087,17 @@
(((|#1|) . T) (((-383 (-523))) . T) (((-523)) . T) (($) . T))
(((#0=(-523) #0#) . T))
((($) . T) (((-383 (-523))) . T))
-(-3172 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
-(-3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
+(-3255 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973)))
+(-3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973)))
(|has| |#4| (-732))
-(-3172 (|has| |#4| (-732)) (|has| |#4| (-784)))
+(-3255 (|has| |#4| (-732)) (|has| |#4| (-784)))
(|has| |#4| (-784))
(|has| |#3| (-732))
-(-3172 (|has| |#3| (-732)) (|has| |#3| (-784)))
+(-3255 (|has| |#3| (-732)) (|has| |#3| (-784)))
(|has| |#3| (-784))
((((-523)) . T))
(((|#2|) . T))
-((((-1087)) -3172 (-12 (|has| (-1085 |#1| |#2| |#3|) (-831 (-1087))) (|has| |#1| (-339))) (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087))))))
+((((-1087)) -3255 (-12 (|has| (-1085 |#1| |#2| |#3|) (-831 (-1087))) (|has| |#1| (-339))) (-12 (|has| |#1| (-15 * (|#1| (-523) |#1|))) (|has| |#1| (-831 (-1087))))))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-383 (-523)) |#1|))) (|has| |#1| (-831 (-1087)))))
((((-1087)) -12 (|has| |#1| (-15 * (|#1| (-710) |#1|))) (|has| |#1| (-831 (-1087)))))
(((|#1| |#1|) . T) (($ $) . T))
@@ -3112,11 +3112,11 @@
((((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)))
((((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)))
((((-1052 |#1| |#2|)) . T))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
((($) . T))
(|has| |#1| (-949))
-(((|#2|) . T) (((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+(((|#2|) . T) (((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
((((-794)) . T))
((((-499)) |has| |#2| (-564 (-499))) (((-823 (-523))) |has| |#2| (-564 (-823 (-523)))) (((-823 (-355))) |has| |#2| (-564 (-823 (-355)))) (((-355)) . #0=(|has| |#2| (-949))) (((-203)) . #0#))
((((-1087) (-51)) . T))
@@ -3128,15 +3128,15 @@
((((-1085 |#1| |#2| |#3|)) . T))
((((-1085 |#1| |#2| |#3|)) . T) (((-1078 |#1| |#2| |#3|)) . T))
((((-794)) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
((((-523) |#1|) . T))
((((-1085 |#1| |#2| |#3|)) |has| |#1| (-339)))
(((|#1| |#2| |#3| |#4|) . T))
(((|#1|) . T))
(((|#2|) . T))
(|has| |#2| (-339))
-(((|#3|) . T) ((|#2|) . T) (($) -3172 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973))) ((|#4|) -3172 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))))
-(((|#2|) . T) (($) -3172 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973))) ((|#3|) -3172 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))))
+(((|#3|) . T) ((|#2|) . T) (($) -3255 (|has| |#4| (-158)) (|has| |#4| (-784)) (|has| |#4| (-973))) ((|#4|) -3255 (|has| |#4| (-158)) (|has| |#4| (-339)) (|has| |#4| (-973))))
+(((|#2|) . T) (($) -3255 (|has| |#3| (-158)) (|has| |#3| (-784)) (|has| |#3| (-973))) ((|#3|) -3255 (|has| |#3| (-158)) (|has| |#3| (-339)) (|has| |#3| (-973))))
(((|#1|) . T))
(((|#1|) . T))
(|has| |#1| (-339))
@@ -3148,37 +3148,37 @@
((((-794)) . T))
((((-794)) . T))
(((|#1|) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
((((-523) |#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
(((|#1|) . T))
(((|#2| $) -12 (|has| |#1| (-339)) (|has| |#2| (-263 |#2| |#2|))) (($ $) . T))
((($ $) . T))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-427)) (|has| |#1| (-840)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
((((-794)) . T))
((((-794)) . T))
((((-794)) . T))
(((|#1| (-495 |#2|)) . T))
-((((-2 (|:| -3772 (-1087)) (|:| -2482 (-51)))) . T))
+((((-2 (|:| -2402 (-1087)) (|:| -2746 (-51)))) . T))
(((|#1| (-523)) . T))
(((|#1| (-383 (-523))) . T))
(((|#1| (-710)) . T))
((((-112 |#1|)) . T) (($) . T) (((-383 (-523))) . T))
-(-3172 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
-(-3172 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
+(-3255 (|has| |#2| (-427)) (|has| |#2| (-515)) (|has| |#2| (-840)))
+(-3255 (|has| |#1| (-427)) (|has| |#1| (-515)) (|has| |#1| (-840)))
((($) . T))
(((|#2| (-495 (-796 |#1|))) . T))
((((-523) |#1|) . T))
(((|#2|) . T))
(((|#2| (-710)) . T))
-((((-794)) -3172 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
+((((-794)) -3255 (|has| |#1| (-563 (-794))) (|has| |#1| (-1016))))
(((|#1|) . T))
(((|#1| |#2|) . T))
((((-1070) |#1|) . T))
((((-383 |#2|)) . T))
-((((-2 (|:| -3772 |#1|) (|:| -2482 |#2|))) . T))
+((((-2 (|:| -2402 |#1|) (|:| -2746 |#2|))) . T))
(|has| |#1| (-515))
(|has| |#1| (-515))
((($) . T) ((|#2|) . T))
@@ -3186,12 +3186,12 @@
(((|#1| |#2|) . T))
(((|#2| $) |has| |#2| (-263 |#2| |#2|)))
(((|#1| (-589 |#1|)) |has| |#1| (-784)))
-(-3172 (|has| |#1| (-211)) (|has| |#1| (-325)))
-(-3172 (|has| |#1| (-339)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-211)) (|has| |#1| (-325)))
+(-3255 (|has| |#1| (-339)) (|has| |#1| (-325)))
(|has| |#1| (-1016))
(((|#1|) . T))
((((-383 (-523))) . T) (($) . T))
-((((-927 |#1|)) . T) ((|#1|) . T) (((-523)) -3172 (|has| (-927 |#1|) (-964 (-523))) (|has| |#1| (-964 (-523)))) (((-383 (-523))) -3172 (|has| (-927 |#1|) (-964 (-383 (-523)))) (|has| |#1| (-964 (-383 (-523))))))
+((((-927 |#1|)) . T) ((|#1|) . T) (((-523)) -3255 (|has| (-927 |#1|) (-964 (-523))) (|has| |#1| (-964 (-523)))) (((-383 (-523))) -3255 (|has| (-927 |#1|) (-964 (-383 (-523)))) (|has| |#1| (-964 (-383 (-523))))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
(((|#1| |#1|) -12 (|has| |#1| (-286 |#1|)) (|has| |#1| (-1016))))
@@ -3202,9 +3202,9 @@
(((|#1|) . T))
(((|#1| |#2| |#3| |#4|) . T))
(((#0=(-1052 |#1| |#2|) #0#) |has| (-1052 |#1| |#2|) (-286 (-1052 |#1| |#2|))))
-(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) #0#) |has| (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)) (-286 (-2 (|:| -3772 |#1|) (|:| -2482 |#2|)))))
+(((|#2| |#2|) -12 (|has| |#2| (-286 |#2|)) (|has| |#2| (-1016))) ((#0=(-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) #0#) |has| (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)) (-286 (-2 (|:| -2402 |#1|) (|:| -2746 |#2|)))))
(((#0=(-112 |#1|)) |has| #0# (-286 #0#)))
-(-3172 (|has| |#1| (-786)) (|has| |#1| (-1016)))
+(-3255 (|has| |#1| (-786)) (|has| |#1| (-1016)))
((($ $) . T))
((($ $) . T) ((#0=(-796 |#1|) $) . T) ((#0# |#2|) . T))
((($ $) . T) ((|#2| $) |has| |#1| (-211)) ((|#2| |#1|) |has| |#1| (-211)) ((|#3| |#1|) . T) ((|#3| $) . T))