diff options
author | dos-reis <gdr@axiomatics.org> | 2008-04-14 02:09:13 +0000 |
---|---|---|
committer | dos-reis <gdr@axiomatics.org> | 2008-04-14 02:09:13 +0000 |
commit | 1d44d2feb01bc10dcc8690c4f71a3157b07502bc (patch) | |
tree | 1f3a91143489620629f548e3b159c189f9061bc3 /src/share/algebra/category.daase | |
parent | 663089e7f95f4901a46939ef34c60982dd5aadda (diff) | |
download | open-axiom-1d44d2feb01bc10dcc8690c4f71a3157b07502bc.tar.gz |
Update databases.
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r-- | src/share/algebra/category.daase | 1126 |
1 files changed, 563 insertions, 563 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 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)) |