diff options
author | dos-reis <gdr@axiomatics.org> | 2007-11-22 17:20:27 +0000 |
---|---|---|
committer | dos-reis <gdr@axiomatics.org> | 2007-11-22 17:20:27 +0000 |
commit | fcc7f11db9c755b9b58ce43d37bbe8a702af8ebf (patch) | |
tree | 05aa94e2606b88faf554913a03a60bc424e56102 /src/share/algebra/category.daase | |
parent | 4244764830efa92de999f8e548f0cc2a800e61d1 (diff) | |
download | open-axiom-fcc7f11db9c755b9b58ce43d37bbe8a702af8ebf.tar.gz |
* as.boot: Globally substitute %noBranch for noBranch.
* ax.boot: Likewise.
* cattable.boot: Likewise.
* compiler.boot: Likewise.
* def.lisp: Likewise.
* define.boot: Likewise.
* functor.boot: Likewise.
* g-opt.boot: Likewise.
* i-analy.boot: Likewise.
* i-intern.boot: Likewise.
* i-map.boot: Likewise.
* i-object.boot: Likewise.
* i-output.boot: Likewise.
* i-spec2.boot: Likewise.
* info.boot: Likewise.
* mark.boot: Likewise.
* nrunopt.boot: Likewise.
* package.boot: Likewise.
* parse.boot: Likewise.
* pf2atree.boot: Likewise.
* pf2sex.boot: Likewise.
* postpar.boot: Likewise.
* pspad2.boot: Likewise.
* wi2.boot: Likewise.
Diffstat (limited to 'src/share/algebra/category.daase')
-rw-r--r-- | src/share/algebra/category.daase | 1124 |
1 files changed, 562 insertions, 562 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index d73ba07d..638a28c8 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(143833 . 3404130415) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(143833 . 3404712031) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#2| |#2|) . T)) ((((-517)) . T)) -((($ $) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2| |#2|) . T) (((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2| |#2|) . T) (((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517))))) ((($) . T)) (((|#1|) . T)) ((($) . T) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2|) . T)) -((($) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) . T) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) +((($) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) . T) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) (|has| |#1| (-831)) ((((-787)) . T)) ((((-787)) . T)) @@ -23,28 +23,28 @@ ((((-199)) . T) (((-787)) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) -((($ $) . T) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1| |#1|) . T)) -(-3763 (|has| |#1| (-752)) (|has| |#1| (-779))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) +((($ $) . T) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1| |#1|) . T)) +(-3782 (|has| |#1| (-752)) (|has| |#1| (-779))) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) ((((-787)) . T)) ((((-787)) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-777)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-787)) . T)) ((((-787)) |has| |#1| (-1003))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) |has| |#1| (-952 (-377 (-517))))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(((|#2| (-450 (-2210 |#1|) (-703))) . T)) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(((|#2| (-450 (-2290 |#1|) (-703))) . T)) (((|#1| (-489 (-1074))) . T)) ((((-794 |#1|) (-794 |#1|)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#4| (-338)) (|has| |#3| (-338)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-509)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((($) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) ((($) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-787)) . T)) ((((-787)) . T)) ((((-377 (-517))) . T) (($) . T)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) ((((-787)) . T)) ((((-787)) . T)) ((((-787)) . T)) (((|#1|) . T)) -(((|#1|) . T) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) +(((|#1|) . T) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) (((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) (($) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1| |#2|) . T)) ((((-787)) . T)) (((|#1|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) (((|#1|) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) ((($ $) . T)) (((|#2|) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) ((($) . T)) (|has| |#1| (-338)) (((|#1|) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-787)) . T)) ((((-787)) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) (((|#1| |#1|) . T)) (|has| |#1| (-509)) (((|#2| |#2|) -12 (|has| |#1| (-333)) (|has| |#2| (-280 |#2|))) (((-1074) |#2|) -12 (|has| |#1| (-333)) (|has| |#2| (-478 (-1074) |#2|)))) ((((-377 |#2|)) . T) (((-377 (-517))) . T) (($) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (|has| |#1| (-1003)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (|has| |#1| (-1003)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (|has| |#1| (-777)) ((($) . T) (((-377 (-517))) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) -(-3763 (|has| |#4| (-725)) (|has| |#4| (-777))) -(-3763 (|has| |#4| (-725)) (|has| |#4| (-777))) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#4| (-725)) (|has| |#4| (-777))) +(-3782 (|has| |#4| (-725)) (|has| |#4| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1003)) @@ -132,21 +132,21 @@ ((((-517)) . T)) ((((-517)) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#1| (-703)) . T)) (|has| |#2| (-725)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (|has| |#2| (-777)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1057) |#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1|) . T)) (((|#3| (-703)) . T)) (|has| |#1| (-134)) (|has| |#1| (-132)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-1003)) ((((-377 (-517))) . T) (((-517)) . T)) ((((-1074) |#2|) |has| |#2| (-478 (-1074) |#2|)) ((|#2| |#2|) |has| |#2| (-280 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-517)) . T)) ((((-517)) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) ((((-517)) . T)) ((((-517)) . T)) ((((-632) (-1070 (-632))) . T)) @@ -173,12 +173,12 @@ ((((-787)) . T)) ((((-787)) . T)) (((|#1| |#1|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T)) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) ((((-787)) . T)) ((((-787)) . T)) ((((-787)) . T)) @@ -189,25 +189,25 @@ ((((-153 (-199))) |has| |#1| (-937)) (((-153 (-349))) |has| |#1| (-937)) (((-493)) |has| |#1| (-558 (-493))) (((-1070 |#1|)) . T) (((-814 (-517))) |has| |#1| (-558 (-814 (-517)))) (((-814 (-349))) |has| |#1| (-558 (-814 (-349))))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#2|) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#2|) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) (|has| |#1| (-333)) (-12 (|has| |#4| (-207)) (|has| |#4| (-961))) (-12 (|has| |#3| (-207)) (|has| |#3| (-961))) -(-3763 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-787)) . T)) (((|#1|) . T)) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) (((|#1|) . T) (((-517)) |has| |#1| (-579 (-517)))) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (|has| |#1| (-509)) (|has| |#1| (-509)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1|) . T)) (|has| |#1| (-509)) (|has| |#1| (-509)) @@ -217,11 +217,11 @@ (-12 (|has| |#1| (-918)) (|has| |#1| (-1095))) (((|#2|) . T) (($) . T) (((-377 (-517))) . T)) ((($) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) (((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) (($) . T)) -(((|#4| |#4|) -3763 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961))) (($ $) |has| |#4| (-156))) -(((|#3| |#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($ $) |has| |#3| (-156))) +(((|#4| |#4|) -3782 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961))) (($ $) |has| |#4| (-156))) +(((|#3| |#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($ $) |has| |#3| (-156))) (((|#1|) . T)) (((|#2|) . T)) ((((-493)) |has| |#2| (-558 (-493))) (((-814 (-349))) |has| |#2| (-558 (-814 (-349)))) (((-814 (-517))) |has| |#2| (-558 (-814 (-517))))) @@ -230,21 +230,21 @@ ((((-787)) . T)) ((((-493)) |has| |#1| (-558 (-493))) (((-814 (-349))) |has| |#1| (-558 (-814 (-349)))) (((-814 (-517))) |has| |#1| (-558 (-814 (-517))))) ((((-787)) . T)) -(((|#4|) -3763 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961))) (($) |has| |#4| (-156))) -(((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($) |has| |#3| (-156))) +(((|#4|) -3782 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961))) (($) |has| |#4| (-156))) +(((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($) |has| |#3| (-156))) ((((-787)) . T)) ((((-493)) . T) (((-517)) . T) (((-814 (-517))) . T) (((-349)) . T) (((-199)) . T)) (((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) |has| |#1| (-952 (-377 (-517))))) ((($) . T) (((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T)) ((((-377 $) (-377 $)) |has| |#2| (-509)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-831)) ((((-1057) (-51)) . T)) ((((-517)) |has| (-377 |#2|) (-579 (-517))) (((-377 |#2|)) . T)) ((((-493)) . T) (((-199)) . T) (((-349)) . T) (((-814 (-349))) . T)) ((((-787)) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) (((|#1|) |has| |#1| (-156))) (((|#1| $) |has| |#1| (-258 |#1| |#1|))) ((((-787)) . T)) @@ -255,13 +255,13 @@ (|has| |#1| (-779)) (|has| |#1| (-1003)) (((|#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (|has| |#1| (-207)) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1| (-489 (-750 (-1074)))) . T)) (((|#1| (-888)) . T)) ((((-794 |#1|) $) |has| (-794 |#1|) (-258 (-794 |#1|) (-794 |#1|)))) @@ -270,7 +270,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1050)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (|has| (-1141 |#1| |#2| |#3| |#4|) (-132)) (|has| (-1141 |#1| |#2| |#3| |#4|) (-134)) (|has| |#1| (-132)) @@ -287,20 +287,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-961))) ((((-787)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))))) ((((-517) |#1|) . T)) ((((-787)) . T)) ((((-493)) -12 (|has| |#1| (-558 (-493))) (|has| |#2| (-558 (-493)))) (((-814 (-349))) -12 (|has| |#1| (-558 (-814 (-349)))) (|has| |#2| (-558 (-814 (-349))))) (((-814 (-517))) -12 (|has| |#1| (-558 (-814 (-517)))) (|has| |#2| (-558 (-814 (-517)))))) ((((-787)) . T)) ((((-787)) . T)) ((($) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-787)) . T)) ((((-787)) . T)) (|has| (-1140 |#2| |#3| |#4|) (-134)) @@ -310,16 +310,16 @@ (|has| |#1| (-1003)) (((|#1|) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) (((|#1|) . T)) ((((-517) |#1|) . T)) (((|#2|) |has| |#2| (-156))) (((|#1|) |has| |#1| (-156))) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) ((((-787)) |has| |#1| (-1003))) -(-3763 (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((((-832 |#1|)) . T)) ((((-377 |#2|) |#3|) . T)) (|has| |#1| (-15 * (|#1| (-517) |#1|))) @@ -330,7 +330,7 @@ (((|#1|) . T)) ((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) |has| |#1| (-509))) (|has| |#1| (-333)) -(-3763 (-12 (|has| (-1147 |#1| |#2| |#3|) (-207)) (|has| |#1| (-333))) (|has| |#1| (-15 * (|#1| (-517) |#1|)))) +(-3782 (-12 (|has| (-1147 |#1| |#2| |#3|) (-207)) (|has| |#1| (-333))) (|has| |#1| (-15 * (|#1| (-517) |#1|)))) (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-333)) (|has| |#1| (-15 * (|#1| (-703) |#1|))) @@ -342,31 +342,31 @@ (((|#1|) . T)) ((((-517) |#1|) . T)) (((|#2|) . T)) -(-3763 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (((|#1|) . T)) ((((-1074)) -12 (|has| |#3| (-822 (-1074))) (|has| |#3| (-961)))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (-12 (|has| |#1| (-333)) (|has| |#2| (-752))) -(-3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) -((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) +(-3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) +((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) ((($ $) |has| |#1| (-509))) ((((-632) (-1070 (-632))) . T)) ((((-787)) . T)) ((((-787)) . T) (((-1154 |#4|)) . T)) ((((-787)) . T) (((-1154 |#3|)) . T)) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) ((($) |has| |#1| (-509))) ((((-787)) . T)) ((($) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|) (-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) . T)) -(((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|) (-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) . T)) +(((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) (((|#3|) |has| |#3| (-961))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (|has| |#1| (-1003)) (((|#2| (-751 |#1|)) . T)) (((|#1|) . T)) @@ -378,37 +378,37 @@ ((((-131)) . T)) (((|#3|) |has| |#3| (-1003)) (((-517)) -12 (|has| |#3| (-952 (-517))) (|has| |#3| (-1003))) (((-377 (-517))) -12 (|has| |#3| (-952 (-377 (-517)))) (|has| |#3| (-1003)))) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) ((((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|)) ((|#1| |#1|) |has| |#1| (-280 |#1|))) (|has| |#2| (-752)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-777)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-493)) |has| |#1| (-558 (-493)))) (((|#1| |#2|) . T)) ((((-1074)) -12 (|has| |#1| (-333)) (|has| |#1| (-822 (-1074))))) ((((-1057) |#1|) . T)) (((|#1| |#2| |#3| (-489 |#3|)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| |#1| (-338)) ((((-787)) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (|has| |#1| (-338)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-517)) . T)) ((((-517)) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((((-787)) . T)) ((((-787)) . T)) (-12 (|has| |#2| (-207)) (|has| |#2| (-961))) @@ -417,10 +417,10 @@ ((((-517) |#4|) . T)) ((((-517) |#3|) . T)) (((|#1|) . T) (((-517)) |has| |#1| (-579 (-517)))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-1141 |#1| |#2| |#3| |#4|)) . T)) ((((-377 (-517))) . T) (((-517)) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) @@ -449,37 +449,37 @@ ((($) . T)) ((($ $) . T) (((-1074) $) . T) (((-1074) |#1|) . T)) (((|#2|) |has| |#2| (-156))) -((($) -3763 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) |has| |#2| (-156)) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) -(((|#2| |#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) +((($) -3782 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) |has| |#2| (-156)) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) +(((|#2| |#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) ((((-131)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-338)) (|has| |#2| (-338))) ((((-787)) . T)) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) (((|#1|) . T)) ((((-787)) . T)) (|has| |#1| (-1003)) (|has| $ (-134)) ((((-517) |#1|) . T)) -((($) -3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) -3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-822 (-1074))))) (|has| |#1| (-333)) -(-3763 (-12 (|has| (-1072 |#1| |#2| |#3|) (-207)) (|has| |#1| (-333))) (|has| |#1| (-15 * (|#1| (-517) |#1|)))) +(-3782 (-12 (|has| (-1072 |#1| |#2| |#3|) (-207)) (|has| |#1| (-333))) (|has| |#1| (-15 * (|#1| (-517) |#1|)))) (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-333)) (|has| |#1| (-15 * (|#1| (-703) |#1|))) (((|#1|) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) ((((-787)) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (((|#2| (-489 (-789 |#1|))) . T)) ((((-787)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-530 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -496,28 +496,28 @@ ((((-787)) . T)) ((((-787)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|) (-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|) (-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2|) |has| |#2| (-961))) (|has| |#1| (-1003)) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) . T)) -(((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) . T)) +(((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) |has| |#1| (-156)) (($) . T)) (((|#1|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) ((((-787)) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) ((((-989) |#1|) . T) (((-989) $) . T) (($ $) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) ((($) . T)) (((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) (($) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#2|) |has| |#1| (-333))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1003)) (((-517)) -12 (|has| |#2| (-952 (-517))) (|has| |#2| (-1003))) (((-377 (-517))) -12 (|has| |#2| (-952 (-377 (-517)))) (|has| |#2| (-1003)))) @@ -531,8 +531,8 @@ (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-132)) (|has| |#1| (-134)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-377 (-517))) . T) (($) . T)) ((((-377 (-517))) . T) (($) . T)) ((((-377 (-517))) . T) (($) . T)) @@ -543,12 +543,12 @@ (((|#1| (-703) (-989)) . T)) ((((-377 (-517))) |has| |#2| (-333)) (($) . T)) (((|#1| (-489 (-993 (-1074))) (-993 (-1074))) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (|has| |#2| (-725)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| |#1| (-338)) @@ -580,61 +580,61 @@ (((|#4| |#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) (((|#2|) . T) (((-517)) |has| |#2| (-952 (-517))) (((-377 (-517))) |has| |#2| (-952 (-377 (-517))))) (((|#3| |#3|) -12 (|has| |#3| (-280 |#3|)) (|has| |#3| (-1003)))) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#2|) . T)) -((((-787)) -3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) +((((-787)) -3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) (((|#1|) |has| |#1| (-156))) ((((-517)) . T)) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-517) (-131)) . T)) -((($) -3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +((($) -3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) (((|#2|) |has| |#1| (-333))) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| (-489 (-1074)) (-1074)) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-156)) (|has| |#3| (-156)) ((((-377 (-874 |#1|)) (-377 (-874 |#1|))) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (|has| |#1| (-1003)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (|has| |#1| (-1003)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1| |#1|) |has| |#1| (-156))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T)) ((((-377 (-874 |#1|))) . T)) (((|#1|) |has| |#1| (-156))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-787)) . T)) ((((-1141 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-961)) (((-517)) -12 (|has| |#1| (-579 (-517))) (|has| |#1| (-961)))) (((|#1| |#2|) . T)) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) (|has| |#3| (-725)) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) (|has| |#3| (-777)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#2|) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#2|) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) (((|#2|) . T)) ((((-787)) . T)) ((((-787)) . T)) @@ -649,22 +649,22 @@ (|has| |#1| (-1003)) (((|#2|) . T)) ((((-493)) |has| |#2| (-558 (-493))) (((-814 (-349))) |has| |#2| (-558 (-814 (-349)))) (((-814 (-517))) |has| |#2| (-558 (-814 (-517))))) -(((|#4|) -3763 (|has| |#4| (-156)) (|has| |#4| (-333)))) -(((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)))) +(((|#4|) -3782 (|has| |#4| (-156)) (|has| |#4| (-333)))) +(((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)))) ((((-787)) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) ((($ $) . T) (((-1074) $) |has| |#1| (-207)) (((-1074) |#1|) |has| |#1| (-207)) (((-750 (-1074)) |#1|) . T) (((-750 (-1074)) $) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) ((((-517) |#2|) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -((($) -3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961)))) +((($) -3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961)))) ((((-517) |#1|) . T)) (|has| (-377 |#2|) (-134)) (|has| (-377 |#2|) (-132)) @@ -677,21 +677,21 @@ (|has| |#1| (-509)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (|has| |#1| (-37 (-377 (-517)))) -((((-358) (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-358) (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#2| (-1050)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((|#1|) . T)) ((((-358) (-1057)) . T)) (|has| |#1| (-509)) ((((-111 |#1|)) . T)) ((((-517) |#1|) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#2|) . T)) ((((-787)) . T)) ((((-751 |#1|)) . T)) @@ -704,7 +704,7 @@ (((|#1|) |has| |#1| (-156))) ((((-787)) . T)) ((((-493)) |has| |#1| (-558 (-493)))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#2|) |has| |#2| (-280 |#2|))) ((((-517) (-517)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) (((|#1|) . T)) @@ -714,7 +714,7 @@ ((((-517) (-517)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) ((($) . T) (((-517)) . T) (((-377 (-517))) . T)) (|has| |#2| (-338)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) @@ -725,9 +725,9 @@ ((((-1072 |#1| |#2| |#3|) $) -12 (|has| (-1072 |#1| |#2| |#3|) (-258 (-1072 |#1| |#2| |#3|) (-1072 |#1| |#2| |#3|))) (|has| |#1| (-333))) (($ $) . T)) ((((-787)) . T)) ((((-787)) . T)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) ((($ $) . T)) ((($ $) . T)) ((((-787)) . T)) @@ -736,12 +736,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-377 (-517))) . T) (((-517)) . T)) ((((-517) (-131)) . T)) ((((-131)) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) ((((-107)) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-107)) . T)) @@ -749,38 +749,38 @@ ((((-493)) |has| |#1| (-558 (-493))) (((-199)) |has| |#1| (-937)) (((-349)) |has| |#1| (-937))) ((((-787)) . T)) (|has| |#1| (-752)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (|has| |#1| (-779)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) (|has| |#1| (-509)) (|has| |#1| (-831)) (((|#1|) . T)) (|has| |#1| (-1003)) ((((-787)) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((((-787)) . T)) ((((-787)) . T)) ((((-787)) . T)) (((|#1| (-1154 |#1|) (-1154 |#1|)) . T)) ((((-517) (-131)) . T)) ((($) . T)) -(-3763 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-787)) . T)) (|has| |#1| (-1003)) (((|#1| (-888)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (-12 (|has| |#1| (-442)) (|has| |#2| (-442))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) -(-3763 (-12 (|has| |#1| (-442)) (|has| |#2| (-442))) (-12 (|has| |#1| (-659)) (|has| |#2| (-659)))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (-12 (|has| |#1| (-442)) (|has| |#2| (-442))) (-12 (|has| |#1| (-659)) (|has| |#2| (-659)))) (((|#1|) . T)) (|has| |#2| (-725)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (|has| |#2| (-777)) @@ -795,7 +795,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-377 (-517))) . T) (($) . T)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) . T)) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) . T)) (|has| |#1| (-760)) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) (|has| |#1| (-1003)) @@ -806,8 +806,8 @@ (((|#3|) |has| |#3| (-1003))) (|has| |#3| (-338)) (((|#1|) . T) (((-787)) . T)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) ((((-787)) . T)) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2|) . T)) @@ -817,30 +817,30 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-156))) ((((-377 (-517))) . T) (((-517)) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) ((((-131)) . T)) (((|#1|) . T)) ((((-131)) . T)) -((($) -3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) +((($) -3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961)))) ((((-131)) . T)) (((|#1| |#2| |#3|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) (|has| $ (-134)) (|has| $ (-134)) (|has| |#1| (-1003)) ((((-787)) . T)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-442)) (|has| |#1| (-509)) (|has| |#1| (-961)) (|has| |#1| (-1015))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-442)) (|has| |#1| (-509)) (|has| |#1| (-961)) (|has| |#1| (-1015))) ((($ $) |has| |#1| (-258 $ $)) ((|#1| $) |has| |#1| (-258 |#1| |#1|))) (((|#1| (-377 (-517))) . T)) (((|#1|) . T)) ((((-1074)) . T)) (|has| |#1| (-509)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-509)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) @@ -851,7 +851,7 @@ (|has| |#1| (-134)) (|has| |#1| (-132)) (|has| |#4| (-777)) -(((|#2| (-214 (-2210 |#1|) (-703)) (-789 |#1|)) . T)) +(((|#2| (-214 (-2290 |#1|) (-703)) (-789 |#1|)) . T)) (|has| |#3| (-777)) (((|#1| (-489 |#3|) |#3|) . T)) (|has| |#1| (-134)) @@ -865,21 +865,21 @@ (|has| |#1| (-132)) ((((-377 (-517))) |has| |#2| (-333)) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-319)) (|has| |#1| (-338))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-319)) (|has| |#1| (-338))) ((((-1041 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-156)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-207)) (|has| |#2| (-961))) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) ((((-787)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-632)) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (|has| |#1| (-509)) (((|#1|) . T)) (((|#1|) . T)) @@ -901,10 +901,10 @@ (((|#1| (-377 (-517))) . T)) (((|#3|) . T) (((-556 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) ((((-1072 |#1| |#2| |#3|) (-1072 |#1| |#2| |#3|)) -12 (|has| (-1072 |#1| |#2| |#3|) (-280 (-1072 |#1| |#2| |#3|))) (|has| |#1| (-333))) (((-1074) (-1072 |#1| |#2| |#3|)) -12 (|has| (-1072 |#1| |#2| |#3|) (-478 (-1074) (-1072 |#1| |#2| |#3|))) (|has| |#1| (-333)))) @@ -912,8 +912,8 @@ ((((-787)) . T)) ((((-787)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) -(((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) +(((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))))) ((((-787)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -924,10 +924,10 @@ ((($ $) . T) (((-789 |#1|) $) . T) (((-789 |#1|) |#2|) . T)) (|has| |#1| (-760)) (|has| |#1| (-1003)) -(((|#2| |#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)))) -((((-517) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) +(((|#2| |#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)))) +((((-517) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) ((((-703)) . T)) ((((-517)) . T)) (|has| |#1| (-509)) @@ -940,29 +940,29 @@ ((((-111 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-134)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) ((((-814 (-517))) . T) (((-814 (-349))) . T) (((-493)) . T) (((-1074)) . T)) ((((-787)) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) ((($) . T)) ((((-787)) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (((|#2|) |has| |#2| (-156))) -((($) -3763 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) |has| |#2| (-156)) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) +((($) -3782 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((|#2|) |has| |#2| (-156)) (((-377 (-517))) |has| |#2| (-37 (-377 (-517))))) ((((-794 |#1|)) . T)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (-12 (|has| |#3| (-207)) (|has| |#3| (-961))) (|has| |#2| (-1050)) -((((-51)) . T) (((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +((((-51)) . T) (((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) (((|#1| (-517) (-989)) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| (-377 (-517)) (-989)) . T)) -((($) -3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) -3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-517) |#2|) . T)) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) @@ -970,37 +970,37 @@ (-12 (|has| |#1| (-338)) (|has| |#2| (-338))) ((((-787)) . T)) ((((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|)) ((|#1| |#1|) |has| |#1| (-280 |#1|))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (((|#1|) . T)) ((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) |has| |#1| (-509))) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-787)) . T)) (|has| |#1| (-319)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (|has| |#1| (-509)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-787)) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) ((((-377 (-517))) . T) (((-517)) . T)) ((((-517)) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) ((($) . T)) ((((-787)) . T)) (((|#1|) . T)) ((((-794 |#1|)) . T) (($) . T) (((-377 (-517))) . T)) ((((-787)) . T)) -(((|#3| |#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($ $) |has| |#3| (-156))) +(((|#3| |#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($ $) |has| |#3| (-156))) (|has| |#1| (-937)) ((((-787)) . T)) -(((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($) |has| |#3| (-156))) +(((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961))) (($) |has| |#3| (-156))) ((((-517) (-107)) . T)) (((|#1|) |has| |#1| (-280 |#1|))) (|has| |#1| (-338)) @@ -1008,31 +1008,31 @@ (|has| |#1| (-338)) ((((-1074) $) |has| |#1| (-478 (-1074) $)) (($ $) |has| |#1| (-280 $)) ((|#1| |#1|) |has| |#1| (-280 |#1|)) (((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|))) ((((-1074)) |has| |#1| (-822 (-1074)))) -(-3763 (-12 (|has| |#1| (-207)) (|has| |#1| (-333))) (|has| |#1| (-319))) +(-3782 (-12 (|has| |#1| (-207)) (|has| |#1| (-333))) (|has| |#1| (-319))) ((((-358) (-1021)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-358) |#1|) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-1003)) ((((-787)) . T)) ((((-787)) . T)) ((((-832 |#1|)) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) ((((-794 |#1|)) |has| (-794 |#1|) (-280 (-794 |#1|)))) (((|#1| |#2|) . T)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725))) (((|#1|) . T)) (-12 (|has| |#1| (-725)) (|has| |#2| (-725))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#1| (-1095)) ((((-517) (-517)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) ((((-377 (-517))) . T) (($) . T)) @@ -1043,8 +1043,8 @@ (((|#1| |#1|) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) (|has| |#1| (-333)) ((((-517)) . T) (((-377 (-517))) . T) (($) . T)) -((($ $) . T) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1| |#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((($ $) . T) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1| |#1|) . T)) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) ((((-787)) . T)) ((((-787)) . T)) @@ -1059,14 +1059,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-777)) (|has| |#1| (-777)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))))) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))))) ((($) . T)) (|has| |#2| (-779)) ((($) . T)) (((|#2|) |has| |#2| (-1003))) -((((-787)) -3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) +((((-787)) -3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) (|has| |#1| (-779)) (|has| |#1| (-779)) ((((-1057) (-51)) . T)) @@ -1074,10 +1074,10 @@ ((((-787)) . T)) ((((-517)) |has| (-377 |#2|) (-579 (-517))) (((-377 |#2|)) . T)) ((((-517) (-131)) . T)) -((((-517) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T) ((|#1| |#2|) . T)) +((((-517) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T) ((|#1| |#2|) . T)) ((((-377 (-517))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-787)) . T)) ((((-832 |#1|)) . T)) (|has| |#1| (-333)) @@ -1102,31 +1102,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-156))) -((((-517) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T) ((|#1| |#2|) . T)) +((((-517) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-156))) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831)))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T)) (((|#1|) . T)) ((((-493)) |has| |#1| (-558 (-493))) (((-814 (-349))) |has| |#1| (-558 (-814 (-349)))) (((-814 (-517))) |has| |#1| (-558 (-814 (-517))))) ((((-787)) . T)) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#2| (-777)) (-12 (|has| |#2| (-207)) (|has| |#2| (-961))) (|has| |#1| (-509)) (|has| |#1| (-1050)) ((((-1057) |#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) -((((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1| |#1|) . T)) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +((((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1| |#1|) . T)) ((((-377 (-517))) |has| |#1| (-952 (-517))) (((-517)) |has| |#1| (-952 (-517))) (((-1074)) |has| |#1| (-952 (-1074))) ((|#1|) . T)) ((((-517) |#2|) . T)) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) ((((-517)) |has| |#1| (-808 (-517))) (((-349)) |has| |#1| (-808 (-349)))) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1|) . T)) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1|) . T)) (((|#1|) . T)) ((((-583 |#4|)) . T) (((-787)) . T)) ((((-493)) |has| |#4| (-558 (-493)))) @@ -1139,17 +1139,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1074)) |has| (-377 |#2|) (-822 (-1074)))) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-787)) -3763 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-557 (-787))) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) (((-1154 |#3|)) . T)) +((((-787)) -3782 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-557 (-787))) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) (((-1154 |#3|)) . T)) ((((-517) |#2|) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) -(((|#2| |#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(((|#2| |#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($ $) |has| |#2| (-156))) ((((-787)) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T) ((|#2|) . T)) ((((-787)) . T)) ((((-787)) . T)) ((((-1057) (-1074) (-517) (-199) (-787)) . T)) @@ -1184,8 +1184,8 @@ (|has| |#1| (-37 (-377 (-517)))) ((((-787)) . T)) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-961))) (($) |has| |#2| (-156))) (|has| $ (-134)) ((((-377 |#2|)) . T)) ((((-377 (-517))) |has| (-377 |#2|) (-952 (-377 (-517)))) (((-517)) |has| (-377 |#2|) (-952 (-517))) (((-377 |#2|)) . T)) @@ -1196,11 +1196,11 @@ (((|#3|) |has| |#3| (-156))) (|has| |#1| (-134)) (|has| |#1| (-132)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) (((|#1|) . T)) (((|#2|) . T)) @@ -1231,7 +1231,7 @@ ((((-915 |#1|)) . T) ((|#1|) . T)) ((((-787)) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-377 (-517))) . T) (((-377 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1070 |#1|)) . T)) ((((-517)) . T) (($) . T) (((-377 (-517))) . T)) @@ -1239,9 +1239,9 @@ (|has| |#1| (-779)) (((|#2|) . T)) ((((-517)) . T) (($) . T) (((-377 (-517))) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) ((((-517) |#2|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#2|) . T)) ((((-517) |#3|) . T)) (((|#2|) . T)) @@ -1256,7 +1256,7 @@ (((|#3|) -12 (|has| |#3| (-280 |#3|)) (|has| |#3| (-1003)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-333)) (((|#2|) . T) (((-517)) |has| |#2| (-952 (-517))) (((-377 (-517))) |has| |#2| (-952 (-377 (-517))))) @@ -1286,19 +1286,19 @@ (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| |#2|) . T)) ((((-517) (-131)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (|has| |#1| (-779)) (((|#2| (-703) (-989)) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) (|has| |#1| (-723)) (((|#1|) |has| |#1| (-156))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#1| (-134)) (-12 (|has| |#1| (-333)) (|has| |#2| (-134)))) -(-3763 (|has| |#1| (-132)) (-12 (|has| |#1| (-333)) (|has| |#2| (-132)))) +(-3782 (|has| |#1| (-134)) (-12 (|has| |#1| (-333)) (|has| |#2| (-134)))) +(-3782 (|has| |#1| (-132)) (-12 (|has| |#1| (-333)) (|has| |#2| (-132)))) (((|#4|) . T)) (|has| |#1| (-132)) ((((-1057) |#1|) . T)) @@ -1311,10 +1311,10 @@ (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#3|) . T)) ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003))) (((-879 |#1|)) . T)) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003))) (((-879 |#1|)) . T)) (|has| |#1| (-777)) (|has| |#1| (-777)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) @@ -1327,8 +1327,8 @@ ((($) . T)) ((((-358) (-1057)) . T)) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((((-787)) -3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) -((((-51)) . T) (((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) . T)) +((((-787)) -3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-557 (-787))) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((-1154 |#2|)) . T)) +((((-51)) . T) (((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) . T)) (((|#1|) . T)) ((((-787)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) @@ -1336,7 +1336,7 @@ (|has| |#2| (-132)) (|has| |#2| (-134)) (|has| |#1| (-442)) -(-3763 (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) (|has| |#1| (-333)) ((((-787)) . T)) (|has| |#1| (-37 (-377 (-517)))) @@ -1345,8 +1345,8 @@ (|has| |#1| (-777)) (|has| |#1| (-777)) ((((-787)) . T)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1147 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1| |#2|) . T)) ((((-1074)) |has| |#1| (-822 (-1074)))) @@ -1354,7 +1354,7 @@ ((((-787)) . T)) ((((-787)) . T)) (|has| |#1| (-1003)) -(((|#2| (-450 (-2210 |#1|) (-703)) (-789 |#1|)) . T)) +(((|#2| (-450 (-2290 |#1|) (-703)) (-789 |#1|)) . T)) ((((-377 (-517))) |has| |#2| (-333)) (($) |has| |#2| (-333))) (((|#1| (-489 (-1074)) (-1074)) . T)) (((|#1|) . T)) @@ -1374,16 +1374,16 @@ (|has| |#1| (-134)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) ((((-1072 |#1| |#2| |#3|)) |has| |#1| (-333))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-1074) (-51)) . T)) ((($ $) . T)) (((|#1| (-517)) . T)) ((((-832 |#1|)) . T)) -(((|#1|) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961))) (($) -3763 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)))) +(((|#1|) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961))) (($) -3782 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)))) (((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) |has| |#1| (-952 (-377 (-517))))) (|has| |#1| (-779)) (|has| |#1| (-779)) @@ -1398,13 +1398,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) (((|#1|) |has| |#1| (-156))) (((|#4| |#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) -(((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)))) +(((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)))) (|has| |#2| (-779)) (|has| |#1| (-779)) -(-3763 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-831))) ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) ((((-517) |#2|) . T)) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)))) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)))) (|has| |#1| (-319)) (((|#3| |#3|) -12 (|has| |#3| (-280 |#3|)) (|has| |#3| (-1003)))) ((($) . T) (((-377 (-517))) . T)) @@ -1412,7 +1412,7 @@ (|has| |#1| (-752)) (|has| |#1| (-752)) (((|#1|) . T)) -(-3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-777)) (|has| |#1| (-777)) (|has| |#1| (-777)) @@ -1421,13 +1421,13 @@ ((((-517)) . T) (($) . T) (((-377 (-517))) . T)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-37 (-377 (-517)))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-1074)) |has| |#1| (-822 (-1074))) (((-989)) . T)) (((|#1|) . T)) (|has| |#1| (-777)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51))) (-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))))) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51))) (-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (|has| |#1| (-1003)) (((|#1|) . T)) @@ -1445,7 +1445,7 @@ (((|#1|) . T)) ((((-131)) . T)) (((|#2|) |has| |#2| (-156))) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((|#1|) . T)) (|has| |#1| (-132)) (|has| |#1| (-134)) @@ -1466,32 +1466,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))))) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) +(((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)))) +(((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)))) (|has| |#1| (-779)) (|has| |#1| (-509)) ((((-530 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-3763 (-12 (|has| |#1| (-333)) (|has| |#2| (-752))) (-12 (|has| |#1| (-333)) (|has| |#2| (-779)))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (-12 (|has| |#1| (-333)) (|has| |#2| (-752))) (-12 (|has| |#1| (-333)) (|has| |#2| (-779)))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((((-832 |#1|)) . T)) (((|#1| (-461 |#1| |#3|) (-461 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-703)) . T)) ((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) |has| |#1| (-156)) (($) |has| |#1| (-509))) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) -(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509)))) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-1072 |#1| |#2| |#3|)) |has| |#1| (-333)) ((|#1|) |has| |#1| (-156))) +(((|#1|) |has| |#1| (-156)) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509)))) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) ((((-377 |#2|)) . T) (((-377 (-517))) . T) (($) . T)) ((((-608 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1499,17 +1499,17 @@ ((((-787)) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-787)) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) ((((-787)) . T)) ((((-787)) . T)) ((((-787)) . T)) (((|#2|) . T)) -(-3763 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) (|has| |#1| (-1095)) (|has| |#1| (-1095)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (|has| |#1| (-1095)) (|has| |#1| (-1095)) (((|#3| |#3|) . T)) @@ -1522,43 +1522,43 @@ (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) ((((-1057) (-51)) . T)) (|has| |#1| (-1003)) -(-3763 (|has| |#2| (-752)) (|has| |#2| (-779))) +(-3782 (|has| |#2| (-752)) (|has| |#2| (-779))) (((|#1|) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) (((|#1|) |has| |#1| (-156)) (($) . T)) ((($) . T)) ((((-1072 |#1| |#2| |#3|)) -12 (|has| (-1072 |#1| |#2| |#3|) (-280 (-1072 |#1| |#2| |#3|))) (|has| |#1| (-333)))) ((((-787)) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((($) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-787)) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) (|has| |#2| (-831)) (|has| |#1| (-333)) (((|#2|) |has| |#2| (-1003))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((($) . T) ((|#2|) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) (|has| |#1| (-831)) (|has| |#1| (-831)) ((((-493)) . T) (((-377 (-1070 (-517)))) . T) (((-199)) . T) (((-349)) . T)) ((((-349)) . T) (((-199)) . T) (((-787)) . T)) (|has| |#1| (-831)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) ((($ $) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((($ $) . T)) ((((-517) (-107)) . T)) ((($) . T)) (((|#1|) . T)) ((((-517)) . T)) ((((-107)) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-37 (-377 (-517)))) (((|#1| (-517)) . T)) ((($) . T)) @@ -1580,7 +1580,7 @@ (((|#1| (-1119 |#1| |#2| |#3|)) . T)) (((|#1| (-703)) . T)) (((|#1|) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-787)) . T)) (|has| |#1| (-1003)) ((((-1057) |#1|) . T)) @@ -1599,18 +1599,18 @@ (((|#1|) . T)) ((((-517)) . T)) ((((-787)) . T)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-319))) ((((-787)) . T)) (|has| |#1| (-134)) (((|#3|) . T)) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-787)) . T)) ((((-1140 |#2| |#3| |#4|)) . T) (((-1141 |#1| |#2| |#3| |#4|)) . T)) ((((-787)) . T)) -((((-47)) -12 (|has| |#1| (-509)) (|has| |#1| (-952 (-517)))) (((-556 $)) . T) ((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) -3763 (-12 (|has| |#1| (-509)) (|has| |#1| (-952 (-517)))) (|has| |#1| (-952 (-377 (-517))))) (((-377 (-874 |#1|))) |has| |#1| (-509)) (((-874 |#1|)) |has| |#1| (-961)) (((-1074)) . T)) +((((-47)) -12 (|has| |#1| (-509)) (|has| |#1| (-952 (-517)))) (((-556 $)) . T) ((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) -3782 (-12 (|has| |#1| (-509)) (|has| |#1| (-952 (-517)))) (|has| |#1| (-952 (-377 (-517))))) (((-377 (-874 |#1|))) |has| |#1| (-509)) (((-874 |#1|)) |has| |#1| (-961)) (((-1074)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-703)) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) (((|#1|) |has| |#1| (-280 |#1|))) ((((-1141 |#1| |#2| |#3| |#4|)) . T)) ((((-517)) |has| |#1| (-808 (-517))) (((-349)) |has| |#1| (-808 (-349)))) @@ -1618,14 +1618,14 @@ (|has| |#1| (-509)) (((|#1|) . T)) ((((-787)) . T)) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (((|#1|) |has| |#1| (-156))) ((($) |has| |#1| (-509)) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1003))) -(((|#2|) -3763 (|has| |#2| (-156)) (|has| |#2| (-333)))) +(((|#2|) -3782 (|has| |#2| (-156)) (|has| |#2| (-333)))) ((((-1140 |#2| |#3| |#4|)) . T)) ((((-107)) . T)) (|has| |#1| (-752)) @@ -1635,8 +1635,8 @@ (|has| |#1| (-777)) (|has| |#1| (-777)) (((|#1| (-517) (-989)) . T)) -(-3763 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +(-3782 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1| (-377 (-517)) (-989)) . T)) (((|#1| (-703) (-989)) . T)) (|has| |#1| (-779)) @@ -1652,28 +1652,28 @@ (((|#1|) . T)) (|has| |#1| (-1003)) ((((-517)) -12 (|has| |#1| (-333)) (|has| |#2| (-579 (-517)))) ((|#2|) |has| |#1| (-333))) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) (((|#2|) |has| |#2| (-156))) (((|#1|) |has| |#1| (-156))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) ((((-787)) . T)) (|has| |#3| (-777)) ((((-787)) . T)) ((((-1140 |#2| |#3| |#4|) (-289 |#2| |#3| |#4|)) . T)) ((((-787)) . T)) -(((|#1| |#1|) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961)))) +(((|#1| |#1|) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961)))) (((|#1|) . T)) ((((-517)) . T)) ((((-517)) . T)) -(((|#1|) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961)))) +(((|#1|) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-961)))) (((|#2|) |has| |#2| (-333))) ((($) . T) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-333))) (|has| |#1| (-779)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-831))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-831))) (((|#2|) . T) (((-517)) |has| |#2| (-579 (-517)))) ((((-787)) . T)) ((((-787)) . T)) @@ -1707,18 +1707,18 @@ (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) (((|#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) ((((-787)) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (|has| |#1| (-333)) (|has| |#1| (-333)) (|has| (-377 |#2|) (-207)) (|has| |#1| (-831)) (((|#2|) |has| |#2| (-961))) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) (|has| |#1| (-333)) (((|#1|) |has| |#1| (-156))) (((|#1| |#1|) . T)) @@ -1743,7 +1743,7 @@ (((|#1| (-377 (-517)) (-989)) . T)) (((|#1| (-703) (-989)) . T)) ((((-377 |#2|) (-377 |#2|)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) -(((|#1|) . T) (((-517)) -3763 (|has| (-377 (-517)) (-952 (-517))) (|has| |#1| (-952 (-517)))) (((-377 (-517))) . T)) +(((|#1|) . T) (((-517)) -3782 (|has| (-377 (-517)) (-952 (-517))) (|has| |#1| (-952 (-517)))) (((-377 (-517))) . T)) (((|#1| (-548 |#1| |#3|) (-548 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-156))) (((|#1|) . T)) @@ -1762,24 +1762,24 @@ ((((-632)) . T)) (((|#2|) |has| |#2| (-156))) (|has| |#2| (-777)) -((((-107)) |has| |#1| (-1003)) (((-787)) -3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003)))) +((((-107)) |has| |#1| (-1003)) (((-787)) -3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) . T)) ((((-787)) . T)) ((((-517) |#1|) . T)) ((((-632)) . T) (((-377 (-517))) . T) (((-517)) . T)) (((|#1| |#1|) |has| |#1| (-156))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) ((((-349)) . T)) ((((-632)) . T)) ((((-377 (-517))) |has| |#2| (-333)) (($) |has| |#2| (-333))) (((|#1|) |has| |#1| (-156))) ((((-377 (-874 |#1|))) . T)) (((|#2| |#2|) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#2|) . T)) (|has| |#2| (-779)) (((|#3|) |has| |#3| (-961))) @@ -1789,14 +1789,14 @@ (|has| |#1| (-779)) ((((-1074)) |has| |#2| (-822 (-1074)))) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-377 (-517))) . T) (($) . T)) (|has| |#1| (-442)) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| |#1| (-338)) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-442)) (|has| |#1| (-509)) (|has| |#1| (-961)) (|has| |#1| (-1015))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-442)) (|has| |#1| (-509)) (|has| |#1| (-961)) (|has| |#1| (-1015))) (|has| |#1| (-37 (-377 (-517)))) ((((-111 |#1|)) . T)) ((((-111 |#1|)) . T)) @@ -1817,11 +1817,11 @@ (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-779)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-134)) (|has| |#1| (-132)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)))) ((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)))) ((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) (((|#2|) . T)) (((|#3|) . T)) ((((-111 |#1|)) . T)) @@ -1839,11 +1839,11 @@ ((((-493)) |has| |#1| (-558 (-493))) (((-814 (-517))) |has| |#1| (-558 (-814 (-517)))) (((-814 (-349))) |has| |#1| (-558 (-814 (-349)))) (((-349)) |has| |#1| (-937)) (((-199)) |has| |#1| (-937))) (((|#1|) |has| |#1| (-333))) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((($ $) . T) (((-556 $) $) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((($) . T) (((-1141 |#1| |#2| |#3| |#4|)) . T) (((-377 (-517))) . T)) -((($) -3763 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-509))) +((($) -3782 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-509))) (|has| |#1| (-333)) (|has| |#1| (-333)) (|has| |#1| (-333)) @@ -1854,11 +1854,11 @@ ((((-349)) . T)) (((|#3|) -12 (|has| |#3| (-280 |#3|)) (|has| |#3| (-1003)))) ((((-787)) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-831))) (((|#1|) . T)) (|has| |#1| (-779)) (|has| |#1| (-779)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) (((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) (|has| |#1| (-1003)) @@ -1867,13 +1867,13 @@ (|has| |#1| (-132)) (|has| |#1| (-134)) ((((-517)) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((((-1140 |#2| |#3| |#4|)) . T) (((-377 (-517))) |has| (-1140 |#2| |#3| |#4|) (-37 (-377 (-517)))) (($) . T)) ((((-517)) . T)) (|has| |#1| (-333)) -(-3763 (-12 (|has| (-1147 |#1| |#2| |#3|) (-134)) (|has| |#1| (-333))) (|has| |#1| (-134))) -(-3763 (-12 (|has| (-1147 |#1| |#2| |#3|) (-132)) (|has| |#1| (-333))) (|has| |#1| (-132))) +(-3782 (-12 (|has| (-1147 |#1| |#2| |#3|) (-134)) (|has| |#1| (-333))) (|has| |#1| (-134))) +(-3782 (-12 (|has| (-1147 |#1| |#2| |#3|) (-132)) (|has| |#1| (-333))) (|has| |#1| (-132))) (|has| |#1| (-333)) (|has| |#1| (-132)) (|has| |#1| (-134)) @@ -1890,18 +1890,18 @@ (((|#1| |#2|) . T)) (((|#1|) . T) (((-517)) |has| |#1| (-579 (-517)))) (((|#3|) |has| |#3| (-156))) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) ((((-517)) . T)) (((|#1| $) |has| |#1| (-258 |#1| |#1|))) ((((-377 (-517))) . T) (($) . T) (((-377 |#1|)) . T) ((|#1|) . T)) ((((-787)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-262)) (|has| |#1| (-333))) (((-377 (-517)) (-377 (-517))) |has| |#1| (-333))) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-262)) (|has| |#1| (-333))) (((-377 (-517)) (-377 (-517))) |has| |#1| (-333))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) ((($) . T)) ((((-517) |#1|) . T)) ((((-1074)) |has| (-377 |#2|) (-822 (-1074)))) -(((|#1|) . T) (($) -3763 (|has| |#1| (-262)) (|has| |#1| (-333))) (((-377 (-517))) |has| |#1| (-333))) +(((|#1|) . T) (($) -3782 (|has| |#1| (-262)) (|has| |#1| (-333))) (((-377 (-517))) |has| |#1| (-333))) ((((-493)) |has| |#2| (-558 (-493)))) ((((-623 |#2|)) . T) (((-787)) . T)) (((|#1|) . T)) @@ -1909,8 +1909,8 @@ (((|#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) ((((-794 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -(-3763 (|has| |#4| (-725)) (|has| |#4| (-777))) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#4| (-725)) (|has| |#4| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) ((((-787)) . T)) ((((-787)) . T)) (((|#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) @@ -1926,17 +1926,17 @@ ((((-377 (-517))) . T) (($) . T)) ((((-377 (-517))) . T) (($) . T)) ((((-377 (-517))) . T) (($) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-1113))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-1113))) ((($) . T)) ((((-377 (-517))) |has| (-377 |#2|) (-952 (-377 (-517)))) (((-517)) |has| (-377 |#2|) (-952 (-517))) (((-377 |#2|)) . T)) (((|#2|) . T) (((-517)) |has| |#2| (-579 (-517)))) (((|#1| (-703)) . T)) (|has| |#1| (-779)) (((|#1|) . T) (((-517)) |has| |#1| (-579 (-517)))) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-517)) . T)) (|has| |#1| (-37 (-377 (-517)))) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))))) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))))) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (|has| |#1| (-777)) (|has| |#1| (-37 (-377 (-517)))) @@ -1961,24 +1961,24 @@ (((|#1| |#2|) . T)) ((((-131)) . T)) ((((-712 |#1| (-789 |#2|))) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (|has| |#1| (-1095)) (((|#1|) . T)) -(-3763 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) +(-3782 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-338)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961)) (|has| |#3| (-1003))) ((((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|))) (((|#2|) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-832 |#1|)) . T)) ((($) . T)) ((((-377 (-874 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-493)) |has| |#4| (-558 (-493)))) ((((-787)) . T) (((-583 |#4|)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-777)) -(((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) |has| (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|)) (-280 (-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))))) +(((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003))) (((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) |has| (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|)) (-280 (-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))))) (|has| |#1| (-1003)) (|has| |#1| (-333)) (|has| |#1| (-779)) @@ -1986,16 +1986,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-377 (-517))) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) |has| |#1| (-156))) (|has| |#1| (-132)) (|has| |#1| (-134)) -(-3763 (-12 (|has| (-1072 |#1| |#2| |#3|) (-134)) (|has| |#1| (-333))) (|has| |#1| (-134))) -(-3763 (-12 (|has| (-1072 |#1| |#2| |#3|) (-132)) (|has| |#1| (-333))) (|has| |#1| (-132))) +(-3782 (-12 (|has| (-1072 |#1| |#2| |#3|) (-134)) (|has| |#1| (-333))) (|has| |#1| (-134))) +(-3782 (-12 (|has| (-1072 |#1| |#2| |#3|) (-132)) (|has| |#1| (-333))) (|has| |#1| (-132))) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-134)) (|has| |#1| (-132)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) (|has| |#1| (-777)) (((|#1| |#2|) . T)) @@ -2018,9 +2018,9 @@ ((((-787)) . T)) ((((-787)) . T)) ((((-493)) |has| |#1| (-558 (-493)))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|)) ((|#1| |#1|) |has| |#1| (-280 |#1|))) -(((|#1|) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)))) +(((|#1|) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)))) ((((-286 |#1|)) . T)) (((|#2|) |has| |#2| (-333))) (((|#2|) . T)) @@ -2041,14 +2041,14 @@ (|has| |#1| (-132)) (|has| |#1| (-134)) ((($ $) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003))) (|has| |#1| (-509)) (((|#2|) . T)) ((((-517)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) ((((-530 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2073,12 +2073,12 @@ (((|#1| |#2|) . T)) ((((-1074) |#1|) . T)) (((|#4|) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((((-1074) (-51)) . T)) ((((-1140 |#2| |#3| |#4|) (-289 |#2| |#3| |#4|)) . T)) ((((-377 (-517))) |has| |#1| (-952 (-377 (-517)))) (((-517)) |has| |#1| (-952 (-517))) ((|#1|) . T)) ((((-787)) . T)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-338)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961)) (|has| |#2| (-1003))) ((((-1141 |#1| |#2| |#3| |#4|) (-1141 |#1| |#2| |#3| |#4|)) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) (((|#1| |#1|) |has| |#1| (-156)) (((-377 (-517)) (-377 (-517))) |has| |#1| (-509)) (($ $) |has| |#1| (-509))) (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) @@ -2097,14 +2097,14 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) (((|#2| |#3|) . T)) -(-3763 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-333)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (((|#1| (-489 |#2|)) . T)) (((|#1| (-703)) . T)) (((|#1| (-489 (-993 (-1074)))) . T)) (((|#1|) |has| |#1| (-156))) (((|#1|) . T)) (|has| |#2| (-831)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) ((((-787)) . T)) ((($ $) . T) (((-1140 |#2| |#3| |#4|) (-1140 |#2| |#3| |#4|)) . T) (((-377 (-517)) (-377 (-517))) |has| (-1140 |#2| |#3| |#4|) (-37 (-377 (-517))))) ((((-832 |#1|)) . T)) @@ -2113,13 +2113,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319)) (|has| |#1| (-509))) (|has| |#1| (-333)) ((($) . T) (((-1140 |#2| |#3| |#4|)) . T) (((-377 (-517))) |has| (-1140 |#2| |#3| |#4|) (-37 (-377 (-517))))) (((|#1| |#2|) . T)) ((((-1072 |#1| |#2| |#3|)) |has| |#1| (-333))) -(-3763 (-12 (|has| |#1| (-278)) (|has| |#1| (-831))) (|has| |#1| (-333)) (|has| |#1| (-319))) -(-3763 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) +(-3782 (-12 (|has| |#1| (-278)) (|has| |#1| (-831))) (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-822 (-1074))) (|has| |#1| (-961))) ((((-517)) |has| |#1| (-579 (-517))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-787)) . T)) @@ -2151,27 +2151,27 @@ (((|#1|) |has| |#1| (-156))) ((((-787)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) -(((|#2|) -3763 (|has| |#2| (-6 (-4185 "*"))) (|has| |#2| (-156)))) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(((|#2|) -3782 (|has| |#2| (-6 (-4185 "*"))) (|has| |#2| (-156)))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (|has| |#2| (-779)) (|has| |#2| (-831)) (|has| |#1| (-831)) (((|#2|) |has| |#2| (-156))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) ((((-787)) . T)) ((((-787)) . T)) ((((-493)) . T) (((-517)) . T) (((-814 (-517))) . T) (((-349)) . T) (((-199)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) . T)) (((|#1|) . T)) ((((-787)) . T)) (((|#1| |#2|) . T)) (((|#1| (-377 (-517))) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-262)) (|has| |#1| (-333))) +(-3782 (|has| |#1| (-262)) (|has| |#1| (-333))) ((((-131)) . T)) ((((-377 |#2|)) . T) (((-377 (-517))) . T) (($) . T)) (|has| |#1| (-777)) @@ -2186,7 +2186,7 @@ ((((-377 (-517))) . T) (($) . T)) ((((-787)) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-787)) . T)) ((((-787)) . T)) @@ -2197,7 +2197,7 @@ (((|#1|) . T)) ((((-583 (-131))) . T) (((-1057)) . T)) ((((-787)) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) ((((-1074) |#1|) |has| |#1| (-478 (-1074) |#1|)) ((|#1| |#1|) |has| |#1| (-280 |#1|))) (|has| |#1| (-779)) ((((-787)) . T)) @@ -2209,16 +2209,16 @@ ((((-787)) . T) (((-583 |#4|)) . T)) (((|#2|) . T)) ((((-832 |#1|)) . T) (((-377 (-517))) . T) (($) . T)) -(-3763 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-1074) (-51)) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) (|has| |#1| (-831)) (|has| |#1| (-831)) (((|#2|) . T)) @@ -2233,12 +2233,12 @@ (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (|has| |#1| (-752)) ((((-832 |#1|) (-832 |#1|)) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) ((((-377 |#2|)) . T)) (|has| |#1| (-777)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) . T) (((-517) (-517)) . T) (($ $) . T)) ((((-832 |#1|)) . T) (($) . T) (((-377 (-517))) . T)) (((|#2|) |has| |#2| (-961)) (((-517)) -12 (|has| |#2| (-579 (-517))) (|has| |#2| (-961)))) @@ -2247,25 +2247,25 @@ (|has| |#1| (-134)) (|has| |#1| (-132)) (((|#2|) . T)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) -((((-51)) . T) (((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) +((((-51)) . T) (((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) (|has| |#1| (-319)) ((((-517)) . T)) ((((-787)) . T)) ((((-1141 |#1| |#2| |#3| |#4|) $) |has| (-1141 |#1| |#2| |#3| |#4|) (-258 (-1141 |#1| |#2| |#3| |#4|) (-1141 |#1| |#2| |#3| |#4|)))) (|has| |#1| (-333)) ((((-989) |#1|) . T) (((-989) $) . T) (($ $) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((((-377 (-517)) (-377 (-517))) . T) (((-632) (-632)) . T) (($ $) . T)) ((((-286 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) |has| |#1| (-333))) (|has| |#1| (-1003)) (((|#1|) . T)) -(((|#1|) -3763 (|has| |#2| (-337 |#1|)) (|has| |#2| (-387 |#1|)))) -(((|#1|) -3763 (|has| |#2| (-337 |#1|)) (|has| |#2| (-387 |#1|)))) +(((|#1|) -3782 (|has| |#2| (-337 |#1|)) (|has| |#2| (-387 |#1|)))) +(((|#1|) -3782 (|has| |#2| (-337 |#1|)) (|has| |#2| (-387 |#1|)))) (((|#2|) . T)) ((((-377 (-517))) . T) (((-632)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2284,7 +2284,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-517)) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#2|) . T) (((-517)) |has| |#2| (-579 (-517)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2321,7 +2321,7 @@ (|has| |#2| (-937)) ((($) . T)) (|has| |#1| (-831)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2329,24 +2329,24 @@ ((($) . T)) (|has| |#1| (-333)) ((((-832 |#1|)) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) -(-3763 (|has| |#1| (-338)) (|has| |#1| (-779))) +(-3782 (|has| |#1| (-338)) (|has| |#1| (-779))) (((|#1|) . T)) ((((-787)) . T)) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-822 (-1074))))) ((((-377 |#2|) |#3|) . T)) ((($) . T) (((-377 (-517))) . T)) ((((-703) |#1|) . T)) -(((|#2| (-214 (-2210 |#1|) (-703))) . T)) +(((|#2| (-214 (-2290 |#1|) (-703))) . T)) (((|#1| (-489 |#3|)) . T)) ((((-377 (-517))) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-787)) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))))) (|has| |#1| (-831)) (|has| |#2| (-333)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-153 (-349))) . T) (((-199)) . T) (((-349)) . T)) ((((-787)) . T)) (((|#1|) . T)) @@ -2363,11 +2363,11 @@ (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-37 (-377 (-517)))) (-12 (|has| |#1| (-502)) (|has| |#1| (-760))) ((((-787)) . T)) -((((-1074)) -3763 (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))) (-12 (|has| |#1| (-333)) (|has| |#2| (-822 (-1074)))))) +((((-1074)) -3782 (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))) (-12 (|has| |#1| (-333)) (|has| |#2| (-822 (-1074)))))) (|has| |#1| (-333)) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-822 (-1074))))) (|has| |#1| (-333)) @@ -2377,7 +2377,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-333))) (((|#2|) |has| |#1| (-333))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-156))) (((|#1|) . T)) @@ -2400,31 +2400,31 @@ (((|#2|) |has| |#1| (-333))) ((((-349)) -12 (|has| |#1| (-333)) (|has| |#2| (-808 (-349)))) (((-517)) -12 (|has| |#1| (-333)) (|has| |#2| (-808 (-517))))) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-333)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) (|has| |#1| (-333)) (|has| |#1| (-509)) (((|#4| |#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) (((|#3|) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#2|) . T)) (((|#2|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#1| (-37 (-377 (-517)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) ((((-1057) |#1|) . T)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-338))) (|has| |#1| (-134)) ((((-530 |#1|)) . T)) ((($) . T)) @@ -2432,7 +2432,7 @@ (|has| |#1| (-509)) (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-37 (-377 (-517)))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-319))) (|has| |#1| (-134)) ((((-787)) . T)) ((($) . T)) @@ -2457,7 +2457,7 @@ (|has| |#1| (-723)) (|has| |#1| (-723)) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-109)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2476,7 +2476,7 @@ (((|#2|) . T)) ((((-517)) . T)) ((((-517)) . T)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) ((((-153 (-349))) . T) (((-199)) . T) (((-349)) . T)) ((((-787)) . T)) ((((-787)) . T)) @@ -2488,9 +2488,9 @@ (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) (|has| |#1| (-333)) (|has| |#1| (-333)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-442)) (|has| |#1| (-659)) (|has| |#1| (-822 (-1074))) (|has| |#1| (-961)) (|has| |#1| (-1015)) (|has| |#1| (-1003))) (|has| |#1| (-1050)) ((((-517) |#1|) . T)) (((|#1|) . T)) @@ -2508,8 +2508,8 @@ (((|#1|) . T)) (|has| |#1| (-509)) ((((-377 |#2|)) . T) (((-377 (-517))) . T) (($) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) ((((-349)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2518,7 +2518,7 @@ (|has| |#1| (-509)) (|has| |#1| (-1003)) ((((-712 |#1| (-789 |#2|))) |has| (-712 |#1| (-789 |#2|)) (-280 (-712 |#1| (-789 |#2|))))) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-831)) @@ -2528,12 +2528,12 @@ (|has| |#1| (-207)) (((|#1| (-489 (-993 (-1074)))) . T)) (|has| |#2| (-333)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) ((((-787)) . T)) ((((-787)) . T)) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) ((((-787)) . T)) ((((-787)) . T)) (((|#1|) . T)) @@ -2542,8 +2542,8 @@ ((((-517)) . T)) (((|#3|) . T)) ((((-787)) . T)) -(-3763 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) -(-3763 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) +(-3782 (|has| |#1| (-278)) (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-156)) (|has| |#1| (-509)) (|has| |#1| (-961))) ((((-530 |#1|) (-530 |#1|)) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) (((|#1|) |has| |#1| (-156))) @@ -2556,27 +2556,27 @@ (((|#1|) . T)) ((((-265 |#3|)) . T)) (((|#1|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) (((|#2| |#2|) . T) ((|#6| |#6|) . T)) ((($) . T) (((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T)) ((($) . T) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) (((|#1|) . T) (((-377 (-517))) . T) (($) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2|) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-787)) . T)) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (|has| |#2| (-831)) (|has| |#1| (-831)) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T)) -((((-2 (|:| -3342 (-1057)) (|:| -1266 |#1|))) . T)) +((((-2 (|:| -3458 (-1057)) (|:| -1338 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2590,10 +2590,10 @@ (((|#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003)))) ((((-377 (-517)) (-377 (-517))) . T)) ((((-377 (-517))) . T)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#1|) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-493)) . T)) ((((-787)) . T)) ((((-1074)) |has| |#2| (-822 (-1074))) (((-989)) . T)) @@ -2607,12 +2607,12 @@ ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) ((((-1074)) |has| |#1| (-822 (-1074)))) ((((-832 |#1|)) . T) (((-377 (-517))) . T) (($) . T)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) . T)) -((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#1|) . T)) +((((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) ((($) . T) (((-377 (-517))) . T)) (((|#1|) . T) (((-377 (-517))) . T) (((-517)) . T) (($) . T)) (((|#2|) |has| |#2| (-961)) (((-517)) -12 (|has| |#2| (-579 (-517))) (|has| |#2| (-961)))) -((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-509)))) +((((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-509)))) (|has| |#1| (-509)) (((|#1|) |has| |#1| (-333))) ((((-517)) . T)) @@ -2631,8 +2631,8 @@ ((((-787)) . T)) (|has| |#2| (-752)) (|has| |#2| (-752)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2|) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2|) |has| |#1| (-333)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1|) . T) (((-517)) |has| |#1| (-952 (-517))) (((-377 (-517))) |has| |#1| (-952 (-377 (-517))))) ((((-517)) |has| |#1| (-808 (-517))) (((-349)) |has| |#1| (-808 (-349)))) @@ -2658,12 +2658,12 @@ (((|#2| (-703)) . T)) ((((-1074)) . T)) ((((-794 |#1|)) . T)) -(-3763 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-25)) (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-787)) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-725)) (|has| |#2| (-777))) -(-3763 (-12 (|has| |#1| (-725)) (|has| |#2| (-725))) (-12 (|has| |#1| (-779)) (|has| |#2| (-779)))) +(-3782 (|has| |#2| (-725)) (|has| |#2| (-777))) +(-3782 (-12 (|has| |#1| (-725)) (|has| |#2| (-725))) (-12 (|has| |#1| (-779)) (|has| |#2| (-779)))) ((((-794 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-338)) @@ -2689,7 +2689,7 @@ (((|#1|) . T)) ((((-787)) . T)) (|has| |#2| (-831)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) ((((-493)) |has| |#2| (-558 (-493))) (((-814 (-349))) |has| |#2| (-558 (-814 (-349)))) (((-814 (-517))) |has| |#2| (-558 (-814 (-517))))) ((((-787)) . T)) ((((-787)) . T)) @@ -2722,11 +2722,11 @@ ((((-377 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1003)) -(((|#2| (-450 (-2210 |#1|) (-703))) . T)) +(((|#2| (-450 (-2290 |#1|) (-703))) . T)) ((((-517) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-489 (-1074))) . T)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-517)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2736,9 +2736,9 @@ ((($) . T) (((-377 (-517))) . T)) ((($) . T)) ((($) . T)) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) (((|#1|) . T)) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-787)) . T)) ((((-131)) . T)) (((|#1|) . T) (((-377 (-517))) . T)) @@ -2777,27 +2777,27 @@ (|has| |#1| (-207)) (((|#1| (-489 |#3|)) . T)) (|has| |#1| (-338)) -(((|#2| (-214 (-2210 |#1|) (-703))) . T)) +(((|#2| (-214 (-2290 |#1|) (-703))) . T)) (|has| |#1| (-338)) (|has| |#1| (-338)) (((|#1|) . T) (($) . T)) (((|#1| (-489 |#2|)) . T)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#1| (-703)) . T)) (|has| |#1| (-509)) -(-3763 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-25)) (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-777)) (|has| |#2| (-961))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-787)) . T)) -(-3763 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) -(-3763 (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) +(-3782 (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) (((|#1|) |has| |#1| (-156))) (((|#4|) |has| |#4| (-961))) (((|#3|) |has| |#3| (-961))) (-12 (|has| |#1| (-333)) (|has| |#2| (-752))) (-12 (|has| |#1| (-333)) (|has| |#2| (-752))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) ((((-377 |#2|)) . T) (((-377 (-517))) . T) (($) . T)) ((($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) @@ -2810,14 +2810,14 @@ (((|#2|) |has| |#2| (-961)) (((-517)) -12 (|has| |#2| (-579 (-517))) (|has| |#2| (-961)))) (((|#1|) . T)) (|has| |#2| (-333)) -((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517)) (-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2| |#2|) . T) (($ $) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1| |#1|) . T) (((-377 (-517)) (-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1| |#1|) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) (((|#1| |#1|) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) (((|#1| |#1|) . T) (($ $) . T) (((-377 (-517)) (-377 (-517))) . T)) (((|#2| |#2|) . T)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T) (($) -3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) (((|#1|) . T) (($) . T) (((-377 (-517))) . T)) @@ -2836,25 +2836,25 @@ (((|#1|) |has| |#2| (-387 |#1|))) (((|#1|) |has| |#2| (-387 |#1|))) ((((-832 |#1|)) . T) (((-377 (-517))) . T) (($) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) ((((-787)) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) |has| (-2 (|:| -3342 (-1074)) (|:| -1266 (-51))) (-280 (-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))))) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) |has| (-2 (|:| -3458 (-1074)) (|:| -1338 (-51))) (-280 (-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) ((((-517) |#1|) . T)) ((((-517) |#1|) . T)) ((((-517) |#1|) . T)) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-517) |#1|) . T)) (((|#1|) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((((-1074)) |has| |#1| (-822 (-1074))) (((-750 (-1074))) . T)) -(-3763 (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-123)) (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-725)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((((-751 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-787)) . T)) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-377 (-517)))) ((((-787)) . T)) @@ -2862,15 +2862,15 @@ (((|#1|) |has| |#1| (-156)) (($) |has| |#1| (-509)) (((-377 (-517))) |has| |#1| (-509))) (((|#2|) . T) (((-517)) |has| |#2| (-579 (-517)))) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (-12 (|has| |#1| (-333)) (|has| |#2| (-207)))) +(-3782 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (-12 (|has| |#1| (-333)) (|has| |#2| (-207)))) (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-333)) (((|#1|) . T)) -((((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1| |#1|) . T)) +((((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1| |#1|) . T)) ((((-517) |#1|) . T)) ((((-286 |#1|)) . T)) ((((-632) (-1070 (-632))) . T)) -((((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1|) . T)) +((((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-777)) ((($ $) . T) (((-789 |#1|) $) . T) (((-789 |#1|) |#2|) . T)) @@ -2887,12 +2887,12 @@ ((((-1141 |#1| |#2| |#3| |#4|)) |has| (-1141 |#1| |#2| |#3| |#4|) (-280 (-1141 |#1| |#2| |#3| |#4|)))) ((($) . T)) (((|#1|) . T)) -((($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2| |#2|) |has| |#1| (-333)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2| |#2|) |has| |#1| (-333)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517)) (-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) (|has| |#2| (-207)) (|has| $ (-134)) ((((-787)) . T)) -((($) . T) (((-377 (-517))) -3763 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) +((($) . T) (((-377 (-517))) -3782 (|has| |#1| (-333)) (|has| |#1| (-319))) ((|#1|) . T)) ((((-787)) . T)) (|has| |#1| (-777)) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074))))) @@ -2904,23 +2904,23 @@ (((|#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#4|) . T)) (|has| |#1| (-509)) -((($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2|) |has| |#1| (-333)) ((|#1|) . T)) -((((-1074)) -3763 (-12 (|has| (-1147 |#1| |#2| |#3|) (-822 (-1074))) (|has| |#1| (-333))) (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))))) -(((|#1|) . T) (($) -3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3763 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) +((($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333))) ((|#2|) |has| |#1| (-333)) ((|#1|) . T)) +((((-1074)) -3782 (-12 (|has| (-1147 |#1| |#2| |#3|) (-822 (-1074))) (|has| |#1| (-333))) (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))))) +(((|#1|) . T) (($) -3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-509))) (((-377 (-517))) -3782 (|has| |#1| (-37 (-377 (-517)))) (|has| |#1| (-333)))) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-822 (-1074))))) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-703) |#1|))) (|has| |#1| (-822 (-1074))))) (((|#4|) -12 (|has| |#4| (-280 |#4|)) (|has| |#4| (-1003)))) ((((-517) |#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) (((|#1|) . T)) (((|#1| (-489 (-750 (-1074)))) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#1|) . T)) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) (((|#1|) . T)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) -(-3763 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) ((($) . T) (((-794 |#1|)) . T) (((-377 (-517))) . T)) ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) @@ -2929,15 +2929,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-377 |#2|)) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1|) . T)) (((|#2| |#2|) . T) (((-377 (-517)) (-377 (-517))) . T) (($ $) . T)) ((((-517)) . T)) @@ -2966,32 +2966,32 @@ ((((-1147 |#1| |#2| |#3|)) |has| |#1| (-333))) ((((-1074)) . T) (((-787)) . T)) (|has| |#1| (-333)) -((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) +((((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) |has| |#2| (-156)) (($) -3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-377 (-517))) |has| |#2| (-37 (-377 (-517)))) ((|#2|) . T)) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) -((($) -3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) ((((-1007)) . T)) ((((-787)) . T)) ((($) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517)))) ((|#1|) . T)) ((($) . T)) -((($) -3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) +((($) -3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((|#1|) |has| |#1| (-156)) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (|has| |#2| (-831)) (|has| |#1| (-831)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-156))) ((((-632)) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1|) |has| |#1| (-156))) (((|#1|) |has| |#1| (-156))) ((((-377 (-517))) . T) (($) . T)) (((|#1| (-517)) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-333)) (|has| |#1| (-333)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) -(-3763 (|has| |#1| (-156)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-156)) (|has| |#1| (-509))) (((|#1| (-517)) . T)) (((|#1| (-377 (-517))) . T)) (((|#1| (-703)) . T)) @@ -3006,16 +3006,16 @@ ((((-814 (-349))) . T) (((-814 (-517))) . T) (((-1074)) . T) (((-493)) . T)) (((|#1|) . T)) ((((-787)) . T)) -(-3763 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) -(-3763 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) +(-3782 (|has| |#2| (-123)) (|has| |#2| (-156)) (|has| |#2| (-333)) (|has| |#2| (-725)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-123)) (|has| |#2| (-123))) (-12 (|has| |#1| (-725)) (|has| |#2| (-725)))) ((((-517)) . T)) ((((-517)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-3763 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) +(-3782 (|has| |#2| (-156)) (|has| |#2| (-777)) (|has| |#2| (-961))) ((((-1074)) -12 (|has| |#2| (-822 (-1074))) (|has| |#2| (-961)))) -(-3763 (-12 (|has| |#1| (-442)) (|has| |#2| (-442))) (-12 (|has| |#1| (-659)) (|has| |#2| (-659)))) +(-3782 (-12 (|has| |#1| (-442)) (|has| |#2| (-442))) (-12 (|has| |#1| (-659)) (|has| |#2| (-659)))) (|has| |#1| (-132)) (|has| |#1| (-134)) (|has| |#1| (-333)) @@ -3039,7 +3039,7 @@ ((((-1057) (-1074) (-517) (-199) (-787)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-3763 (|has| |#1| (-319)) (|has| |#1| (-338))) +(-3782 (|has| |#1| (-319)) (|has| |#1| (-338))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-787)) . T)) @@ -3047,7 +3047,7 @@ ((($) . T) ((|#1|) . T) (((-377 (-517))) |has| |#1| (-37 (-377 (-517))))) (((|#2|) |has| |#2| (-1003)) (((-517)) -12 (|has| |#2| (-952 (-517))) (|has| |#2| (-1003))) (((-377 (-517))) -12 (|has| |#2| (-952 (-377 (-517)))) (|has| |#2| (-1003)))) ((((-493)) |has| |#1| (-558 (-493)))) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-779)) (|has| |#1| (-1003)))) ((($) . T) (((-377 (-517))) . T)) (|has| |#1| (-831)) (|has| |#1| (-831)) @@ -3056,10 +3056,10 @@ ((((-787)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-156))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-509))) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-509))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) (((|#2|) . T)) -(-3763 (|has| |#1| (-21)) (|has| |#1| (-777))) +(-3782 (|has| |#1| (-21)) (|has| |#1| (-777))) (((|#1|) |has| |#1| (-156))) (((|#1|) . T)) (((|#1|) . T)) @@ -3074,17 +3074,17 @@ (((|#1|) . T) (((-377 (-517))) . T) (((-517)) . T) (($) . T)) ((((-517) (-517)) . T)) ((($) . T) (((-377 (-517))) . T)) -(-3763 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) -(-3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) +(-3782 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) +(-3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) (|has| |#4| (-725)) -(-3763 (|has| |#4| (-725)) (|has| |#4| (-777))) +(-3782 (|has| |#4| (-725)) (|has| |#4| (-777))) (|has| |#4| (-777)) (|has| |#3| (-725)) -(-3763 (|has| |#3| (-725)) (|has| |#3| (-777))) +(-3782 (|has| |#3| (-725)) (|has| |#3| (-777))) (|has| |#3| (-777)) ((((-517)) . T)) (((|#2|) . T)) -((((-1074)) -3763 (-12 (|has| (-1072 |#1| |#2| |#3|) (-822 (-1074))) (|has| |#1| (-333))) (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))))) +((((-1074)) -3782 (-12 (|has| (-1072 |#1| |#2| |#3|) (-822 (-1074))) (|has| |#1| (-333))) (-12 (|has| |#1| (-15 * (|#1| (-517) |#1|))) (|has| |#1| (-822 (-1074)))))) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-377 (-517)) |#1|))) (|has| |#1| (-822 (-1074))))) ((((-1074)) -12 (|has| |#1| (-15 * (|#1| (-703) |#1|))) (|has| |#1| (-822 (-1074))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3099,11 +3099,11 @@ ((((-1072 |#1| |#2| |#3|)) |has| |#1| (-333))) ((((-1072 |#1| |#2| |#3|)) |has| |#1| (-333))) ((((-1039 |#1| |#2|)) . T)) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) ((($) . T)) (|has| |#1| (-937)) -(((|#2|) . T) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) ((((-787)) . T)) ((((-493)) |has| |#2| (-558 (-493))) (((-814 (-517))) |has| |#2| (-558 (-814 (-517)))) (((-814 (-349))) |has| |#2| (-558 (-814 (-349)))) (((-349)) |has| |#2| (-937)) (((-199)) |has| |#2| (-937))) ((((-1074) (-51)) . T)) @@ -3115,15 +3115,15 @@ ((((-1072 |#1| |#2| |#3|)) . T)) ((((-1072 |#1| |#2| |#3|)) . T) (((-1065 |#1| |#2| |#3|)) . T)) ((((-787)) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) ((((-517) |#1|) . T)) ((((-1072 |#1| |#2| |#3|)) |has| |#1| (-333))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-333)) -(((|#3|) . T) ((|#2|) . T) (($) -3763 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) ((|#4|) -3763 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961)))) -(((|#2|) . T) (($) -3763 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((|#3|) -3763 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961)))) +(((|#3|) . T) ((|#2|) . T) (($) -3782 (|has| |#4| (-156)) (|has| |#4| (-777)) (|has| |#4| (-961))) ((|#4|) -3782 (|has| |#4| (-156)) (|has| |#4| (-333)) (|has| |#4| (-961)))) +(((|#2|) . T) (($) -3782 (|has| |#3| (-156)) (|has| |#3| (-777)) (|has| |#3| (-961))) ((|#3|) -3782 (|has| |#3| (-156)) (|has| |#3| (-333)) (|has| |#3| (-961)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-333)) @@ -3135,37 +3135,37 @@ ((((-787)) . T)) ((((-787)) . T)) (((|#1|) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) ((((-517) |#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-333)) (|has| |#2| (-258 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-421)) (|has| |#1| (-831))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) ((((-787)) . T)) ((((-787)) . T)) ((((-787)) . T)) (((|#1| (-489 |#2|)) . T)) -((((-2 (|:| -3342 (-1074)) (|:| -1266 (-51)))) . T)) +((((-2 (|:| -3458 (-1074)) (|:| -1338 (-51)))) . T)) (((|#1| (-517)) . T)) (((|#1| (-377 (-517))) . T)) (((|#1| (-703)) . T)) ((((-111 |#1|)) . T) (($) . T) (((-377 (-517))) . T)) -(-3763 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) -(-3763 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) +(-3782 (|has| |#2| (-421)) (|has| |#2| (-509)) (|has| |#2| (-831))) +(-3782 (|has| |#1| (-421)) (|has| |#1| (-509)) (|has| |#1| (-831))) ((($) . T)) (((|#2| (-489 (-789 |#1|))) . T)) ((((-517) |#1|) . T)) (((|#2|) . T)) (((|#2| (-703)) . T)) -((((-787)) -3763 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) +((((-787)) -3782 (|has| |#1| (-557 (-787))) (|has| |#1| (-1003)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1057) |#1|) . T)) ((((-377 |#2|)) . T)) -((((-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) . T)) +((((-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) . T)) (|has| |#1| (-509)) (|has| |#1| (-509)) ((($) . T) ((|#2|) . T)) @@ -3173,12 +3173,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-258 |#2| |#2|))) (((|#1| (-583 |#1|)) |has| |#1| (-777))) -(-3763 (|has| |#1| (-207)) (|has| |#1| (-319))) -(-3763 (|has| |#1| (-333)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-207)) (|has| |#1| (-319))) +(-3782 (|has| |#1| (-333)) (|has| |#1| (-319))) (|has| |#1| (-1003)) (((|#1|) . T)) ((((-377 (-517))) . T) (($) . T)) -((((-915 |#1|)) . T) ((|#1|) . T) (((-517)) -3763 (|has| (-915 |#1|) (-952 (-517))) (|has| |#1| (-952 (-517)))) (((-377 (-517))) -3763 (|has| (-915 |#1|) (-952 (-377 (-517)))) (|has| |#1| (-952 (-377 (-517)))))) +((((-915 |#1|)) . T) ((|#1|) . T) (((-517)) -3782 (|has| (-915 |#1|) (-952 (-517))) (|has| |#1| (-952 (-517)))) (((-377 (-517))) -3782 (|has| (-915 |#1|) (-952 (-377 (-517)))) (|has| |#1| (-952 (-377 (-517)))))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) (((|#1| |#1|) -12 (|has| |#1| (-280 |#1|)) (|has| |#1| (-1003)))) @@ -3189,9 +3189,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) ((((-1039 |#1| |#2|) (-1039 |#1| |#2|)) |has| (-1039 |#1| |#2|) (-280 (-1039 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))) |has| (-2 (|:| -3342 |#1|) (|:| -1266 |#2|)) (-280 (-2 (|:| -3342 |#1|) (|:| -1266 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-280 |#2|)) (|has| |#2| (-1003))) (((-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))) |has| (-2 (|:| -3458 |#1|) (|:| -1338 |#2|)) (-280 (-2 (|:| -3458 |#1|) (|:| -1338 |#2|))))) ((((-111 |#1|)) |has| (-111 |#1|) (-280 (-111 |#1|)))) -(-3763 (|has| |#1| (-779)) (|has| |#1| (-1003))) +(-3782 (|has| |#1| (-779)) (|has| |#1| (-1003))) ((($ $) . T)) ((($ $) . T) (((-789 |#1|) $) . T) (((-789 |#1|) |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-207)) ((|#2| |#1|) |has| |#1| (-207)) ((|#3| |#1|) . T) ((|#3| $) . T)) |