diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 1126 |
1 files changed, 563 insertions, 563 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 3aa7b910..1a02dcf1 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,14 +1,14 @@ -(143277 . 3420952957) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(143277 . 3421035927) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#2| |#2|) . T)) ((((-525)) . T)) -((($ $) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525))))) ((($) . T)) (((|#1|) . T)) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) -((($) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) (|has| |#1| (-844)) ((((-798)) . T)) ((((-798)) . T)) @@ -23,28 +23,28 @@ ((((-205)) . T) (((-798)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) -((($ $) . T) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -(-3279 (|has| |#1| (-762)) (|has| |#1| (-789))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +(-3275 (|has| |#1| (-762)) (|has| |#1| (-789))) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-787)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#2| |#3|) . T)) (((|#4|) . T)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) |has| |#1| (-1020))) (((|#1|) . T) ((|#2|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(((|#2| (-458 (-3596 |#1|) (-713))) . T)) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(((|#2| (-458 (-3594 |#1|) (-713))) . T)) (((|#1| (-497 (-1091))) . T)) (((#0=(-805 |#1|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#4| (-346)) (|has| |#3| (-346)) (((|#1|) . T)) @@ -54,10 +54,10 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-517)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) @@ -66,59 +66,59 @@ ((((-798)) . T)) ((((-798)) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +(((|#1|) . T) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1| |#2|) . T)) ((((-798)) . T)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#1|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) ((($ $) . T)) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) ((($) . T)) (|has| |#1| (-346)) (((|#1|) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) (((|#1| |#1|) . T)) (|has| |#1| (-517)) (((|#2| |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-288 |#2|))) (((-1091) |#2|) -12 (|has| |#1| (-341)) (|has| |#2| (-486 (-1091) |#2|)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-787)) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3279 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3279 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-3275 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-1020)) @@ -132,21 +132,21 @@ ((((-525)) . T)) ((((-525)) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| (-713)) . T)) (|has| |#2| (-735)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (|has| |#2| (-787)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) ((((-1074) |#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#3| (-713)) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-1020)) ((((-385 (-525))) . T) (((-525)) . T)) ((((-1091) |#2|) |has| |#2| (-486 (-1091) |#2|)) ((|#2| |#2|) |has| |#2| (-288 |#2|))) @@ -154,7 +154,7 @@ (((|#1|) . T) (($) . T)) ((((-525)) . T)) ((((-525)) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) ((((-525)) . T)) ((((-525)) . T)) (((#0=(-641) (-1087 #0#)) . T)) @@ -173,12 +173,12 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -189,25 +189,25 @@ ((((-798)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) (|has| |#1| (-341)) (-12 (|has| |#4| (-213)) (|has| |#4| (-977))) (-12 (|has| |#3| (-213)) (|has| |#3| (-977))) -(-3279 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) @@ -218,11 +218,11 @@ (((|#2|) . T) (($) . T) (((-385 (-525))) . T)) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(((|#3| |#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) -(((|#4| |#4|) -3279 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($ $) |has| |#4| (-160))) +(((|#3| |#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) +(((|#4| |#4|) -3275 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($ $) |has| |#4| (-160))) (((|#1|) . T)) (((|#2|) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) @@ -231,21 +231,21 @@ ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525))))) ((((-798)) . T)) -(((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) -(((|#4|) -3279 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($) |has| |#4| (-160))) +(((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) +(((|#4|) -3275 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977))) (($) |has| |#4| (-160))) ((((-798)) . T)) ((((-501)) . T) (((-525)) . T) (((-827 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) ((((-385 $) (-385 $)) |has| |#2| (-517)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))) . T)) (((|#1|) . T)) (|has| |#2| (-844)) ((((-1074) (-51)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-588 (-525))) ((#0#) . T)) ((((-501)) . T) (((-205)) . T) (((-357)) . T) (((-827 (-357))) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) (((|#1|) |has| |#1| (-160))) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-798)) . T)) @@ -256,15 +256,15 @@ (|has| |#1| (-789)) (|has| |#1| (-1020)) (((|#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-125)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-125)) . T)) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-213)) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| (-497 (-760 (-1091)))) . T)) (((|#1| (-904)) . T)) (((#0=(-805 |#1|) $) |has| #0# (-265 #0# #0#))) @@ -273,7 +273,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1067)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (|has| (-1159 |#1| |#2| |#3| |#4|) (-136)) (|has| (-1159 |#1| |#2| |#3| |#4|) (-138)) (|has| |#1| (-136)) @@ -290,20 +290,20 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-977))) ((((-798)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) #0#) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) #0#) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))))) ((((-525) |#1|) . T)) ((((-798)) . T)) ((((-501)) -12 (|has| |#1| (-567 (-501))) (|has| |#2| (-567 (-501)))) (((-827 (-357))) -12 (|has| |#1| (-567 (-827 (-357)))) (|has| |#2| (-567 (-827 (-357))))) (((-827 (-525))) -12 (|has| |#1| (-567 (-827 (-525)))) (|has| |#2| (-567 (-827 (-525)))))) ((((-798)) . T)) ((((-798)) . T)) ((($) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((($) . T)) ((($) . T)) ((($) . T)) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) ((((-798)) . T)) (|has| (-1158 |#2| |#3| |#4|) (-138)) @@ -314,16 +314,16 @@ ((((-798)) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) (((|#1|) . T)) ((((-525) |#1|) . T)) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) ((((-798)) |has| |#1| (-1020))) -(-3279 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-845 |#1|)) . T)) ((((-385 |#2|) |#3|) . T)) (|has| |#1| (-15 * (|#1| (-525) |#1|))) @@ -335,7 +335,7 @@ (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) (|has| |#1| (-341)) -(-3279 (-12 (|has| (-1165 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-3275 (-12 (|has| (-1165 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) ((((-525)) . T)) @@ -347,31 +347,31 @@ (((|#1|) . T)) ((((-525) |#1|) . T)) (((|#2|) . T)) -(-3279 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (((|#1|) . T)) ((((-1091)) -12 (|has| |#3| (-835 (-1091))) (|has| |#3| (-977)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) -(-3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) +(-3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($ $) |has| |#1| (-517))) (((#0=(-641) (-1087 #0#)) . T)) ((((-798)) . T)) ((((-798)) . T) (((-1173 |#4|)) . T)) ((((-798)) . T) (((-1173 |#3|)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517))) ((((-798)) . T)) ((($) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1165 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1165 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (((|#3|) |has| |#3| (-977))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-1020)) (((|#2| (-761 |#1|)) . T)) (((|#1|) . T)) @@ -383,37 +383,37 @@ ((((-135)) . T)) (((|#3|) |has| |#3| (-1020)) (((-525)) -12 (|has| |#3| (-968 (-525))) (|has| |#3| (-1020))) (((-385 (-525))) -12 (|has| |#3| (-968 (-385 (-525)))) (|has| |#3| (-1020)))) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) ((((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#2| (-762)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-787)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-501)) |has| |#1| (-567 (-501)))) (((|#1| |#2|) . T)) ((((-1091)) -12 (|has| |#1| (-341)) (|has| |#1| (-835 (-1091))))) ((((-1074) |#1|) . T)) (((|#1| |#2| |#3| (-497 |#3|)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) ((((-798)) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (|has| |#1| (-346)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-525)) . T)) ((((-525)) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((((-798)) . T)) ((((-798)) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) @@ -422,10 +422,10 @@ ((((-525) |#4|) . T)) ((((-525) |#3|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-1159 |#1| |#2| |#3| |#4|)) . T)) ((((-385 (-525))) . T) (((-525)) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1| |#1|) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -454,38 +454,38 @@ ((($) . T)) ((($ $) . T) ((#0=(-1091) $) . T) ((#0# |#1|) . T)) (((|#2|) |has| |#2| (-160))) -((($) -3279 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) -(((|#2| |#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +((($) -3275 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +(((|#2| |#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) ((((-135)) . T)) (((|#1|) . T)) (-12 (|has| |#1| (-346)) (|has| |#2| (-346))) ((((-798)) . T)) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) (((|#1|) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) (|has| $ (-138)) ((((-525) |#1|) . T)) -((($) -3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1091))))) (|has| |#1| (-341)) -(-3279 (-12 (|has| (-1089 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) +(-3275 (-12 (|has| (-1089 |#1| |#2| |#3|) (-213)) (|has| |#1| (-341))) (|has| |#1| (-15 * (|#1| (-525) |#1|)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) (|has| |#1| (-15 * (|#1| (-713) |#1|))) (((|#1|) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) ((((-525) (-125)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#2| (-497 (-800 |#1|))) . T)) ((((-798)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1|) . T) (($) . T)) @@ -502,28 +502,28 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#2| |#3| |#4| |#5|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1089 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((#1=(-1089 |#1| |#2| |#3|) #1#) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-977))) (|has| |#1| (-1020)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) -(((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) . T)) +(((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) |has| |#1| (-160)) (($) . T)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-798)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($ $) . T) ((|#2| $) . T) ((|#2| |#1|) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) (((#0=(-1005) |#1|) . T) ((#0# $) . T) (($ $) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) (($) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#2|) |has| |#1| (-341))) (((|#1|) . T)) (((|#2|) |has| |#2| (-1020)) (((-525)) -12 (|has| |#2| (-968 (-525))) (|has| |#2| (-1020))) (((-385 (-525))) -12 (|has| |#2| (-968 (-385 (-525)))) (|has| |#2| (-1020)))) @@ -538,8 +538,8 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-136)) (|has| |#1| (-138)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) @@ -550,12 +550,12 @@ (((|#1| (-713) (-1005)) . T)) ((((-385 (-525))) |has| |#2| (-341)) (($) . T)) (((|#1| (-497 (-1010 (-1091))) (-1010 (-1091))) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#2| (-735)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) @@ -588,63 +588,63 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#2|) . T) (((-525)) |has| |#2| (-968 (-525))) (((-385 (-525))) |has| |#2| (-968 (-385 (-525))))) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) ((($) . T)) (((|#2|) . T)) (((|#3|) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#2|) . T)) -((((-798)) -3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) +((((-798)) -3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) (((|#1|) |has| |#1| (-160))) ((((-525)) . T)) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-525) (-135)) . T)) -((($) -3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +((($) -3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((|#2|) |has| |#1| (-341))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) . T) (($ $) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| (-497 #0=(-1091)) #0#) . T)) (((|#1|) . T) (($) . T)) (|has| |#4| (-160)) (|has| |#3| (-160)) (((#0=(-385 (-887 |#1|)) #0#) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (|has| |#1| (-1020)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1| |#1|) |has| |#1| (-160))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) ((((-385 (-887 |#1|))) . T)) ((((-525) (-125)) . T)) (((|#1|) |has| |#1| (-160))) ((((-125)) . T)) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-798)) . T)) ((((-1159 |#1| |#2| |#3| |#4|)) . T)) (((|#1|) |has| |#1| (-977)) (((-525)) -12 (|has| |#1| (-588 (-525))) (|has| |#1| (-977)))) (((|#1| |#2|) . T)) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (|has| |#3| (-735)) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) (|has| |#3| (-787)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#2|) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) (((|#2|) . T)) ((((-525) (-125)) . T)) ((((-798)) . T)) @@ -660,22 +660,22 @@ (|has| |#1| (-1020)) (((|#2|) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) -(((|#4|) -3279 (|has| |#4| (-160)) (|has| |#4| (-341)))) -(((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#4|) -3275 (|has| |#4| (-160)) (|has| |#4| (-341)))) +(((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)))) ((((-798)) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) ((($ $) . T) ((#0=(-1091) $) |has| |#1| (-213)) ((#0# |#1|) |has| |#1| (-213)) ((#1=(-760 (-1091)) |#1|) . T) ((#1# $) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) ((((-525) |#2|) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -((($) -3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) +((($) -3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) ((((-525) |#1|) . T)) (|has| (-385 |#2|) (-138)) (|has| (-385 |#2|) (-136)) @@ -688,22 +688,22 @@ (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-366) (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-366) (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#2| (-1067)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((|#1|) . T)) ((((-366) (-1074)) . T)) (|has| |#1| (-517)) ((((-112 |#1|)) . T)) ((((-125)) . T)) ((((-525) |#1|) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T)) ((((-798)) . T)) ((((-761 |#1|)) . T)) @@ -716,7 +716,7 @@ (((|#1|) |has| |#1| (-160))) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#2|) |has| |#2| (-288 |#2|))) (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) (((|#1|) . T)) @@ -726,7 +726,7 @@ (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) ((($) . T) (((-525)) . T) (((-385 (-525))) . T)) (|has| |#2| (-346)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) @@ -737,9 +737,9 @@ ((((-1089 |#1| |#2| |#3|) $) -12 (|has| (-1089 |#1| |#2| |#3|) (-265 (-1089 |#1| |#2| |#3|) (-1089 |#1| |#2| |#3|))) (|has| |#1| (-341))) (($ $) . T)) ((((-798)) . T)) ((((-798)) . T)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((($ $) . T)) ((($ $) . T)) ((((-798)) . T)) @@ -749,12 +749,12 @@ (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525) (-135)) . T)) ((((-135)) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((((-108)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-108)) . T)) @@ -762,38 +762,38 @@ ((((-501)) |has| |#1| (-567 (-501))) (((-205)) . #0=(|has| |#1| (-953))) (((-357)) . #0#)) ((((-798)) . T)) (|has| |#1| (-762)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#1| (-789)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-517)) (|has| |#1| (-844)) (((|#1|) . T)) (|has| |#1| (-1020)) ((((-798)) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1| (-1173 |#1|) (-1173 |#1|)) . T)) ((((-525) (-135)) . T)) ((($) . T)) -(-3279 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (|has| |#1| (-1020)) (((|#1| (-904)) . T)) (((|#1| |#1|) . T)) ((($) . T)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3279 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) (((|#1|) . T)) (|has| |#2| (-735)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (((|#1| |#2|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#2| (-787)) @@ -808,7 +808,7 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) (|has| |#1| (-770)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (|has| |#1| (-1020)) @@ -819,8 +819,8 @@ (((|#3|) |has| |#3| (-1020))) (|has| |#3| (-346)) (((|#1|) . T) (((-798)) . T)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((((-798)) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) @@ -830,30 +830,30 @@ (((|#1|) . T)) (((|#1|) |has| |#1| (-160))) ((((-385 (-525))) . T) (((-525)) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) ((((-135)) . T)) (((|#1|) . T)) ((((-135)) . T)) -((($) -3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) +((($) -3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977)))) ((((-135)) . T)) (((|#1| |#2| |#3|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (|has| $ (-138)) (|has| $ (-138)) (|has| |#1| (-1020)) ((((-798)) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) ((($ $) |has| |#1| (-265 $ $)) ((|#1| $) |has| |#1| (-265 |#1| |#1|))) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) ((((-1091)) . T)) (|has| |#1| (-517)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) @@ -864,7 +864,7 @@ (|has| |#1| (-138)) (|has| |#1| (-136)) (|has| |#4| (-787)) -(((|#2| (-220 (-3596 |#1|) (-713)) (-800 |#1|)) . T)) +(((|#2| (-220 (-3594 |#1|) (-713)) (-800 |#1|)) . T)) (|has| |#3| (-787)) (((|#1| (-497 |#3|) |#3|) . T)) (|has| |#1| (-138)) @@ -878,21 +878,21 @@ (|has| |#1| (-136)) ((((-385 (-525))) |has| |#2| (-341)) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-327)) (|has| |#1| (-346))) ((((-1058 |#2| |#1|)) . T) ((|#1|) . T)) (|has| |#2| (-160)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) (((|#1|) . T)) (((|#2|) . T) (($) . T)) (((|#1|) . T) (($) . T)) ((((-641)) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#1| (-517)) (((|#1|) . T)) (((|#1|) . T)) @@ -914,10 +914,10 @@ (((|#1| (-385 (-525))) . T)) (((|#3|) . T) (((-565 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((#0=(-1089 |#1| |#2| |#3|) #0#) -12 (|has| (-1089 |#1| |#2| |#3|) (-288 (-1089 |#1| |#2| |#3|))) (|has| |#1| (-341))) (((-1091) #0#) -12 (|has| (-1089 |#1| |#2| |#3|) (-486 (-1091) (-1089 |#1| |#2| |#3|))) (|has| |#1| (-341)))) @@ -925,8 +925,8 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))))) ((((-798)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -937,10 +937,10 @@ ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) (|has| |#1| (-770)) (|has| |#1| (-1020)) -(((|#2| |#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)))) -((((-525) (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T) ((|#1| |#2|) . T)) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +(((|#2| |#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)))) +((((-525) (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T) ((|#1| |#2|) . T)) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) ((((-713)) . T)) ((((-525)) . T)) (|has| |#1| (-517)) @@ -953,29 +953,29 @@ ((((-112 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-138)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) ((((-827 (-525))) . T) (((-827 (-357))) . T) (((-501)) . T) (((-1091)) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((($) . T)) ((((-798)) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#2|) |has| |#2| (-160))) -((($) -3279 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) +((($) -3275 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((|#2|) |has| |#2| (-160)) (((-385 (-525))) |has| |#2| (-37 (-385 (-525))))) ((((-805 |#1|)) . T)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (-12 (|has| |#3| (-213)) (|has| |#3| (-977))) (|has| |#2| (-1067)) -(((#0=(-51)) . T) (((-2 (|:| -3423 (-1091)) (|:| -2545 #0#))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3420 (-1091)) (|:| -2542 #0#))) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) (((|#1| (-525) (-1005)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| (-385 (-525)) (-1005)) . T)) -((($) -3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-525) |#2|) . T)) (((|#1| |#2|) . T)) (((|#1| |#2|) . T)) @@ -983,37 +983,37 @@ (-12 (|has| |#1| (-346)) (|has| |#2| (-346))) ((((-798)) . T)) ((((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (((|#1|) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) (|has| |#1| (-327)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (|has| |#1| (-517)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) ((((-385 (-525))) . T) (((-525)) . T)) ((((-525)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((($) . T)) ((((-798)) . T)) (((|#1|) . T)) ((((-805 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) ((((-798)) . T)) -(((|#3| |#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) +(((|#3| |#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($ $) |has| |#3| (-160))) (|has| |#1| (-953)) ((((-798)) . T)) -(((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) +(((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977))) (($) |has| |#3| (-160))) ((((-525) (-108)) . T)) (((|#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-346)) @@ -1021,31 +1021,31 @@ (|has| |#1| (-346)) ((((-1091) $) |has| |#1| (-486 (-1091) $)) (($ $) |has| |#1| (-288 $)) ((|#1| |#1|) |has| |#1| (-288 |#1|)) (((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|))) ((((-1091)) |has| |#1| (-835 (-1091)))) -(-3279 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) +(-3275 (-12 (|has| |#1| (-213)) (|has| |#1| (-341))) (|has| |#1| (-327))) ((((-366) (-1038)) . T)) (((|#1| |#4|) . T)) (((|#1| |#3|) . T)) ((((-366) |#1|) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1020)) ((((-798)) . T)) ((((-798)) . T)) ((((-845 |#1|)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) (((|#1| |#2|) . T)) ((($) . T)) (((|#1| |#1|) . T)) (((#0=(-805 |#1|)) |has| #0# (-288 #0#))) (((|#1| |#2|) . T)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (((|#1|) . T)) (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#1| (-1113)) (((#0=(-525) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) ((((-385 (-525))) . T) (($) . T)) @@ -1056,8 +1056,8 @@ (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (|has| |#1| (-341)) ((((-525)) . T) (((-385 (-525))) . T) (($) . T)) -((($ $) . T) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((($ $) . T) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1| |#1|) . T)) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -1072,14 +1072,14 @@ (((|#1| |#2|) . T)) (|has| |#1| (-787)) (|has| |#1| (-787)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) -(((#0=(-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) #0#) |has| (-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))))) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) +(((#0=(-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) #0#) |has| (-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))))) ((($) . T)) (|has| |#2| (-789)) ((($) . T)) (((|#2|) |has| |#2| (-1020))) -((((-798)) -3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) +((((-798)) -3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) (|has| |#1| (-789)) (|has| |#1| (-789)) ((((-1074) (-51)) . T)) @@ -1087,10 +1087,10 @@ ((((-798)) . T)) ((((-525)) |has| #0=(-385 |#2|) (-588 (-525))) ((#0#) . T)) ((((-525) (-135)) . T)) -((((-525) (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T) ((|#1| |#2|) . T)) ((((-385 (-525))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-798)) . T)) ((((-845 |#1|)) . T)) (|has| |#1| (-341)) @@ -1115,31 +1115,31 @@ ((($) . T)) (((|#2|) . T) (($) . T)) (((|#1|) |has| |#1| (-160))) -((((-525) (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T) ((|#1| |#2|) . T)) +((((-525) (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#3|) . T)) (((|#1|) |has| |#1| (-160))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844)))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) (((|#1|) . T)) ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525))))) ((((-798)) . T)) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#2| (-787)) (-12 (|has| |#2| (-213)) (|has| |#2| (-977))) (|has| |#1| (-517)) (|has| |#1| (-1067)) ((((-1074) |#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-525))) (((-525)) |has| |#1| (-968 (-525))) (((-1091)) |has| |#1| (-968 (-1091))) ((|#1|) . T)) ((((-525) |#2|) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1|) . T)) ((((-592 |#4|)) . T) (((-798)) . T)) ((((-501)) |has| |#4| (-567 (-501)))) @@ -1152,17 +1152,17 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1091)) |has| (-385 |#2|) (-835 (-1091)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) -((((-798)) -3279 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-566 (-798))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) (((-1173 |#3|)) . T)) +((((-798)) -3275 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-566 (-798))) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) (((-1173 |#3|)) . T)) ((((-525) |#2|) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) -(((|#2| |#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(((|#2| |#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($ $) |has| |#2| (-160))) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T) ((|#2|) . T)) ((((-798)) . T)) ((((-798)) . T)) ((((-1074) (-1091) (-525) (-205) (-798)) . T)) @@ -1197,8 +1197,8 @@ (|has| |#1| (-37 (-385 (-525)))) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-977))) (($) |has| |#2| (-160))) (|has| $ (-138)) ((((-385 |#2|)) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-968 (-385 (-525)))) (((-525)) |has| #0# (-968 (-525))) ((#0#) . T)) @@ -1209,11 +1209,11 @@ (((|#3|) |has| |#3| (-160))) (|has| |#1| (-138)) (|has| |#1| (-136)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) @@ -1244,7 +1244,7 @@ ((((-931 |#1|)) . T) ((|#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-385 (-525))) . T) (((-385 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1087 |#1|)) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) @@ -1252,9 +1252,9 @@ (|has| |#1| (-789)) (((|#2|) . T)) ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) ((((-525) |#2|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#2|) . T)) ((((-525) |#3|) . T)) (((|#2|) . T)) @@ -1269,7 +1269,7 @@ (((|#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-341)) (((|#2|) . T) (((-525)) |has| |#2| (-968 (-525))) (((-385 (-525))) |has| |#2| (-968 (-385 (-525))))) @@ -1299,19 +1299,19 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#2|) . T)) ((((-525) (-135)) . T)) -(((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#1| (-789)) (((|#2| (-713) (-1005)) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) (|has| |#1| (-733)) (((|#1|) |has| |#1| (-160))) (((|#4|) . T)) (((|#4|) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) -(-3279 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) +(-3275 (|has| |#1| (-138)) (-12 (|has| |#1| (-341)) (|has| |#2| (-138)))) +(-3275 (|has| |#1| (-136)) (-12 (|has| |#1| (-341)) (|has| |#2| (-136)))) (((|#4|) . T)) (|has| |#1| (-136)) ((((-1074) |#1|) . T)) @@ -1324,10 +1324,10 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#3|) . T)) ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020))) (((-892 |#1|)) . T)) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020))) (((-892 |#1|)) . T)) (|has| |#1| (-787)) (|has| |#1| (-787)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -1340,8 +1340,8 @@ ((($) . T)) ((((-366) (-1074)) . T)) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-798)) -3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3423 (-1074)) (|:| -2545 #0#))) . T)) +((((-798)) -3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-566 (-798))) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((-1173 |#2|)) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3420 (-1074)) (|:| -2542 #0#))) . T)) (((|#1|) . T)) ((((-798)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) @@ -1349,7 +1349,7 @@ (|has| |#2| (-136)) (|has| |#2| (-138)) (|has| |#1| (-450)) -(-3279 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) (|has| |#1| (-341)) ((((-798)) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -1358,8 +1358,8 @@ (|has| |#1| (-787)) (|has| |#1| (-787)) ((((-798)) . T)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1165 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1091)) |has| |#1| (-835 (-1091)))) @@ -1367,7 +1367,7 @@ ((((-798)) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) -(((|#2| (-458 (-3596 |#1|) (-713)) (-800 |#1|)) . T)) +(((|#2| (-458 (-3594 |#1|) (-713)) (-800 |#1|)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1| (-497 (-1091)) (-1091)) . T)) (((|#1|) . T)) @@ -1387,16 +1387,16 @@ (|has| |#1| (-138)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +(((|#1|) . T) (((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) ((((-1089 |#1| |#2| |#3|)) |has| |#1| (-341))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-1091) (-51)) . T)) ((($ $) . T)) (((|#1| (-525)) . T)) ((((-845 |#1|)) . T)) -(((|#1|) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977))) (($) -3279 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)))) +(((|#1|) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977))) (($) -3275 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)))) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) (|has| |#1| (-789)) (|has| |#1| (-789)) @@ -1411,13 +1411,13 @@ (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#1|) |has| |#1| (-160))) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) -(((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#2| (-789)) (|has| |#1| (-789)) -(-3279 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-844))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-525) |#2|) . T)) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)))) (|has| |#1| (-327)) (((|#3| |#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) ((($) . T) (((-385 (-525))) . T)) @@ -1425,7 +1425,7 @@ (|has| |#1| (-762)) (|has| |#1| (-762)) (((|#1|) . T)) -(-3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-787)) (|has| |#1| (-787)) (|has| |#1| (-787)) @@ -1434,13 +1434,13 @@ ((((-525)) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-1091)) |has| |#1| (-835 (-1091))) (((-1005)) . T)) (((|#1|) . T)) (|has| |#1| (-787)) -(((#0=(-2 (|:| -3423 (-1074)) (|:| -2545 (-51))) #0#) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))))) +(((#0=(-2 (|:| -3420 (-1074)) (|:| -2542 (-51))) #0#) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#1| (-1020)) (((|#1|) . T)) @@ -1459,7 +1459,7 @@ (((|#1|) . T)) ((((-135)) . T)) (((|#2|) |has| |#2| (-160))) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((|#1|) . T)) (|has| |#1| (-136)) (|has| |#1| (-138)) @@ -1481,32 +1481,32 @@ (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) #0#) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))))) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) +(((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) ((#0=(-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) #0#) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) (((|#1|) . T) (($) . T)) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)))) +(((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)))) (|has| |#1| (-789)) (|has| |#1| (-517)) ((((-538 |#1|)) . T)) ((($) . T)) (((|#2|) . T)) -(-3279 (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-789)))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-789)))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-845 |#1|)) . T)) (((|#1| (-469 |#1| |#3|) (-469 |#1| |#2|)) . T)) (((|#1| |#4| |#5|) . T)) (((|#1| (-713)) . T)) ((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517))) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) -(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517)))) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-1089 |#1| |#2| |#3|)) |has| |#1| (-341)) ((|#1|) |has| |#1| (-160))) +(((|#1|) |has| |#1| (-160)) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517)))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((((-617 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1514,17 +1514,17 @@ ((((-798)) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#2|) . T)) -(-3279 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) (|has| |#1| (-1113)) (|has| |#1| (-1113)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (|has| |#1| (-1113)) (|has| |#1| (-1113)) (((|#3| |#3|) . T)) @@ -1537,43 +1537,43 @@ (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((((-1074) (-51)) . T)) (|has| |#1| (-1020)) -(-3279 (|has| |#2| (-762)) (|has| |#2| (-789))) +(-3275 (|has| |#2| (-762)) (|has| |#2| (-789))) (((|#1|) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) (((|#1|) |has| |#1| (-160)) (($) . T)) ((($) . T)) ((((-1089 |#1| |#2| |#3|)) -12 (|has| (-1089 |#1| |#2| |#3|) (-288 (-1089 |#1| |#2| |#3|))) (|has| |#1| (-341)))) ((((-798)) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((($) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) (|has| |#2| (-844)) (|has| |#1| (-341)) (((|#2|) |has| |#2| (-1020))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((($) . T) ((|#2|) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) (|has| |#1| (-844)) (|has| |#1| (-844)) ((((-501)) . T) (((-385 (-1087 (-525)))) . T) (((-205)) . T) (((-357)) . T)) ((((-357)) . T) (((-205)) . T) (((-798)) . T)) (|has| |#1| (-844)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) ((($ $) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((($ $) . T)) ((((-525) (-108)) . T)) ((($) . T)) (((|#1|) . T)) ((((-525)) . T)) ((((-108)) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-37 (-385 (-525)))) (((|#1| (-525)) . T)) ((($) . T)) @@ -1595,7 +1595,7 @@ (((|#1| (-1137 |#1| |#2| |#3|)) . T)) (((|#1| (-713)) . T)) (((|#1|) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-798)) . T)) (|has| |#1| (-1020)) ((((-1074) |#1|) . T)) @@ -1615,18 +1615,18 @@ (((|#1|) . T)) ((((-525)) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-798)) . T)) (((|#3|) . T)) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) ((((-1158 |#2| |#3| |#4|)) . T) (((-1159 |#1| |#2| |#3| |#4|)) . T)) ((((-798)) . T)) -((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (((-565 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) -3279 (-12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (|has| |#1| (-968 (-385 (-525))))) (((-385 (-887 |#1|))) |has| |#1| (-517)) (((-887 |#1|)) |has| |#1| (-977)) (((-1091)) . T)) +((((-47)) -12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (((-565 $)) . T) ((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) -3275 (-12 (|has| |#1| (-517)) (|has| |#1| (-968 (-525)))) (|has| |#1| (-968 (-385 (-525))))) (((-385 (-887 |#1|))) |has| |#1| (-517)) (((-887 |#1|)) |has| |#1| (-977)) (((-1091)) . T)) (((|#1|) . T) (($) . T)) (((|#1| (-713)) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-288 |#1|))) ((((-1159 |#1| |#2| |#3| |#4|)) . T)) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) @@ -1634,14 +1634,14 @@ (|has| |#1| (-517)) (((|#1|) . T)) ((((-798)) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((|#1|) |has| |#1| (-160))) ((($) |has| |#1| (-517)) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#1|) . T)) (((|#3|) |has| |#3| (-1020))) -(((|#2|) -3279 (|has| |#2| (-160)) (|has| |#2| (-341)))) +(((|#2|) -3275 (|has| |#2| (-160)) (|has| |#2| (-341)))) ((((-1158 |#2| |#3| |#4|)) . T)) ((((-108)) . T)) (|has| |#1| (-762)) @@ -1651,8 +1651,8 @@ (|has| |#1| (-787)) (|has| |#1| (-787)) (((|#1| (-525) (-1005)) . T)) -(-3279 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +(-3275 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1| (-385 (-525)) (-1005)) . T)) (((|#1| (-713) (-1005)) . T)) (|has| |#1| (-789)) @@ -1668,28 +1668,28 @@ (((|#1|) . T)) (|has| |#1| (-1020)) ((((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-588 (-525)))) ((|#2|) |has| |#1| (-341))) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((|#2|) |has| |#2| (-160))) (((|#1|) |has| |#1| (-160))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) ((((-798)) . T)) (|has| |#3| (-787)) ((((-798)) . T)) ((((-1158 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-798)) . T)) -(((|#1| |#1|) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) +(((|#1| |#1|) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) (((|#1|) . T)) ((((-525)) . T)) ((((-525)) . T)) -(((|#1|) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) +(((|#1|) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-977)))) (((|#2|) |has| |#2| (-341))) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-789)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) |has| (-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-844))) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) |has| (-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-844))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) ((((-798)) . T)) ((((-798)) . T)) @@ -1724,18 +1724,18 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (((|#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-798)) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| (-385 |#2|) (-213)) (|has| |#1| (-844)) (((|#2|) |has| |#2| (-977))) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (|has| |#1| (-341)) (((|#1|) |has| |#1| (-160))) (((|#1| |#1|) . T)) @@ -1760,7 +1760,7 @@ (((|#1| (-385 (-525)) (-1005)) . T)) (((|#1| (-713) (-1005)) . T)) (((#0=(-385 |#2|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) -(((|#1|) . T) (((-525)) -3279 (|has| (-385 (-525)) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) . T)) +(((|#1|) . T) (((-525)) -3275 (|has| (-385 (-525)) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) . T)) (((|#1| (-556 |#1| |#3|) (-556 |#1| |#2|)) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) @@ -1779,24 +1779,24 @@ ((((-641)) . T)) (((|#2|) |has| |#2| (-160))) (|has| |#2| (-787)) -((((-108)) |has| |#1| (-1020)) (((-798)) -3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020)))) +((((-108)) |has| |#1| (-1020)) (((-798)) -3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))) . T)) ((((-798)) . T)) ((((-525) |#1|) . T)) ((((-641)) . T) (((-385 (-525))) . T) (((-525)) . T)) (((|#1| |#1|) |has| |#1| (-160))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) ((((-357)) . T)) ((((-641)) . T)) ((((-385 (-525))) . #0=(|has| |#2| (-341))) (($) . #0#)) (((|#1|) |has| |#1| (-160))) ((((-385 (-887 |#1|))) . T)) (((|#2| |#2|) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T)) (|has| |#2| (-789)) (((|#3|) |has| |#3| (-977))) @@ -1806,14 +1806,14 @@ (|has| |#1| (-789)) ((((-1091)) |has| |#2| (-835 (-1091)))) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-450)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-346)) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-450)) (|has| |#1| (-517)) (|has| |#1| (-977)) (|has| |#1| (-1032))) (|has| |#1| (-37 (-385 (-525)))) ((((-112 |#1|)) . T)) ((((-112 |#1|)) . T)) @@ -1834,11 +1834,11 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-789)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)))) ((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#2|) . T)) (((|#3|) . T)) ((((-112 |#1|)) . T)) @@ -1856,11 +1856,11 @@ ((((-501)) |has| |#1| (-567 (-501))) (((-827 (-525))) |has| |#1| (-567 (-827 (-525)))) (((-827 (-357))) |has| |#1| (-567 (-827 (-357)))) (((-357)) . #0=(|has| |#1| (-953))) (((-205)) . #0#)) (((|#1|) |has| |#1| (-341))) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((($ $) . T) (((-565 $) $) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((($) . T) (((-1159 |#1| |#2| |#3| |#4|)) . T) (((-385 (-525))) . T)) -((($) -3279 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-517))) +((($) -3275 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-517))) (|has| |#1| (-341)) (|has| |#1| (-341)) (|has| |#1| (-341)) @@ -1871,11 +1871,11 @@ ((((-357)) . T)) (((|#3|) -12 (|has| |#3| (-288 |#3|)) (|has| |#3| (-1020)))) ((((-798)) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-844))) (((|#1|) . T)) (|has| |#1| (-789)) (|has| |#1| (-789)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (|has| |#1| (-1020)) @@ -1884,13 +1884,13 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((((-525)) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((#0=(-1158 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525)))) (($) . T)) ((((-525)) . T)) (|has| |#1| (-341)) -(-3279 (-12 (|has| (-1165 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3279 (-12 (|has| (-1165 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-3275 (-12 (|has| (-1165 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-3275 (-12 (|has| (-1165 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) (|has| |#1| (-341)) (|has| |#1| (-136)) (|has| |#1| (-138)) @@ -1907,18 +1907,18 @@ (((|#1| |#2|) . T)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) (((|#3|) |has| |#3| (-160))) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) ((((-525)) . T)) (((|#1| $) |has| |#1| (-265 |#1| |#1|))) ((((-385 (-525))) . T) (($) . T) (((-385 |#1|)) . T) ((|#1|) . T)) ((((-798)) . T)) (((|#3|) . T)) -(((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +(((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-269)) (|has| |#1| (-341))) ((#0=(-385 (-525)) #0#) |has| |#1| (-341))) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) ((($) . T)) ((((-525) |#1|) . T)) ((((-1091)) |has| (-385 |#2|) (-835 (-1091)))) -(((|#1|) . T) (($) -3279 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) +(((|#1|) . T) (($) -3275 (|has| |#1| (-269)) (|has| |#1| (-341))) (((-385 (-525))) |has| |#1| (-341))) ((((-501)) |has| |#2| (-567 (-501)))) ((((-632 |#2|)) . T) (((-798)) . T)) (((|#1|) . T)) @@ -1926,8 +1926,8 @@ (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) ((((-805 |#1|)) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3279 (|has| |#4| (-735)) (|has| |#4| (-787))) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) ((((-798)) . T)) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) @@ -1943,17 +1943,17 @@ ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) ((((-385 (-525))) . T) (($) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-1131))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-1131))) ((($) . T)) ((((-385 (-525))) |has| #0=(-385 |#2|) (-968 (-385 (-525)))) (((-525)) |has| #0# (-968 (-525))) ((#0#) . T)) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (((|#1| (-713)) . T)) (|has| |#1| (-789)) (((|#1|) . T) (((-525)) |has| |#1| (-588 (-525)))) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-525)) . T)) (|has| |#1| (-37 (-385 (-525)))) -((((-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))))) +((((-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))))) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (|has| |#1| (-787)) (|has| |#1| (-37 (-385 (-525)))) @@ -1978,24 +1978,24 @@ (((|#1| |#2|) . T)) ((((-135)) . T)) ((((-722 |#1| (-800 |#2|))) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (|has| |#1| (-1113)) (((|#1|) . T)) -(-3279 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) +(-3275 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-346)) (|has| |#3| (-669)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977)) (|has| |#3| (-1020))) ((((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|))) (((|#2|) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-845 |#1|)) . T)) ((($) . T)) ((((-385 (-887 |#1|))) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-501)) |has| |#4| (-567 (-501)))) ((((-798)) . T) (((-592 |#4|)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-787)) -(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) |has| (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|)) (-288 (-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))))) +(((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020))) (((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) |has| (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|)) (-288 (-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))))) (|has| |#1| (-1020)) (|has| |#1| (-341)) (|has| |#1| (-789)) @@ -2003,16 +2003,16 @@ (((|#1|) . T)) (((|#1|) . T)) ((($) . T) (((-385 (-525))) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) |has| |#1| (-160))) (|has| |#1| (-136)) (|has| |#1| (-138)) -(-3279 (-12 (|has| (-1089 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) -(-3279 (-12 (|has| (-1089 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) +(-3275 (-12 (|has| (-1089 |#1| |#2| |#3|) (-138)) (|has| |#1| (-341))) (|has| |#1| (-138))) +(-3275 (-12 (|has| (-1089 |#1| |#2| |#3|) (-136)) (|has| |#1| (-341))) (|has| |#1| (-136))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-138)) (|has| |#1| (-136)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) (|has| |#1| (-787)) (((|#1| |#2|) . T)) @@ -2035,9 +2035,9 @@ ((((-798)) . T)) ((((-798)) . T)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) -(((|#1|) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)))) +(((|#1|) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)))) ((((-294 |#1|)) . T)) (((|#2|) |has| |#2| (-341))) (((|#2|) . T)) @@ -2058,14 +2058,14 @@ (|has| |#1| (-136)) (|has| |#1| (-138)) ((($ $) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) (|has| |#1| (-517)) (((|#2|) . T)) ((((-525)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) ((((-538 |#1|)) . T)) ((($) . T)) (((|#1| (-57 |#1|) (-57 |#1|)) . T)) @@ -2090,12 +2090,12 @@ (((|#1| |#2|) . T)) ((((-1091) |#1|) . T)) (((|#4|) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((((-1091) (-51)) . T)) ((((-1158 |#2| |#3| |#4|) (-297 |#2| |#3| |#4|)) . T)) ((((-385 (-525))) |has| |#1| (-968 (-385 (-525)))) (((-525)) |has| |#1| (-968 (-525))) ((|#1|) . T)) ((((-798)) . T)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-346)) (|has| |#2| (-669)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977)) (|has| |#2| (-1020))) (((#0=(-1159 |#1| |#2| |#3| |#4|) #0#) . T) ((#1=(-385 (-525)) #1#) . T) (($ $) . T)) (((|#1| |#1|) |has| |#1| (-160)) ((#0=(-385 (-525)) #0#) |has| |#1| (-517)) (($ $) |has| |#1| (-517))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) @@ -2114,14 +2114,14 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((|#2| |#3|) . T)) -(-3279 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-341)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1| (-497 |#2|)) . T)) (((|#1| (-713)) . T)) (((|#1| (-497 (-1010 (-1091)))) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (|has| |#2| (-844)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) ((((-798)) . T)) ((($ $) . T) ((#0=(-1158 |#2| |#3| |#4|) #0#) . T) ((#1=(-385 (-525)) #1#) |has| #0# (-37 (-385 (-525))))) ((((-845 |#1|)) . T)) @@ -2130,13 +2130,13 @@ ((($) . T)) ((($) . T)) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327)) (|has| |#1| (-517))) (|has| |#1| (-341)) ((($) . T) ((#0=(-1158 |#2| |#3| |#4|)) . T) (((-385 (-525))) |has| #0# (-37 (-385 (-525))))) (((|#1| |#2|) . T)) ((((-1089 |#1| |#2| |#3|)) |has| |#1| (-341))) -(-3279 (-12 (|has| |#1| (-286)) (|has| |#1| (-844))) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3279 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) +(-3275 (-12 (|has| |#1| (-286)) (|has| |#1| (-844))) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-835 (-1091))) (|has| |#1| (-977))) ((((-525)) |has| |#1| (-588 (-525))) ((|#1|) . T)) (((|#1| |#2|) . T)) ((((-798)) . T)) @@ -2168,27 +2168,27 @@ (((|#1|) |has| |#1| (-160))) ((((-798)) . T)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) -(((|#2|) -3279 (|has| |#2| (-6 (-4257 "*"))) (|has| |#2| (-160)))) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(((|#2|) -3275 (|has| |#2| (-6 (-4257 "*"))) (|has| |#2| (-160)))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#2| (-789)) (|has| |#2| (-844)) (|has| |#1| (-844)) (((|#2|) |has| |#2| (-160))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-798)) . T)) ((((-798)) . T)) ((((-501)) . T) (((-525)) . T) (((-827 (-525))) . T) (((-357)) . T) (((-205)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))) . T)) (((|#1|) . T)) ((((-798)) . T)) (((|#1| |#2|) . T)) (((|#1| (-385 (-525))) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-269)) (|has| |#1| (-341))) +(-3275 (|has| |#1| (-269)) (|has| |#1| (-341))) ((((-135)) . T)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) (|has| |#1| (-787)) @@ -2203,7 +2203,7 @@ ((((-385 (-525))) . T) (($) . T)) ((((-798)) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -2214,7 +2214,7 @@ (((|#1|) . T)) ((((-592 (-135))) . T) (((-1074)) . T)) ((((-798)) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) ((((-1091) |#1|) |has| |#1| (-486 (-1091) |#1|)) ((|#1| |#1|) |has| |#1| (-288 |#1|))) (|has| |#1| (-789)) ((((-798)) . T)) @@ -2226,16 +2226,16 @@ ((((-798)) . T) (((-592 |#4|)) . T)) (((|#2|) . T)) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3279 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-1091) (-51)) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) (|has| |#1| (-844)) (|has| |#1| (-844)) (((|#2|) . T)) @@ -2250,12 +2250,12 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (|has| |#1| (-762)) (((#0=(-845 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((((-385 |#2|)) . T)) (|has| |#1| (-787)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) . T) ((#1=(-525) #1#) . T) (($ $) . T)) ((((-845 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) @@ -2265,25 +2265,25 @@ (|has| |#1| (-136)) (((|#2|) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) -(((#0=(-51)) . T) (((-2 (|:| -3423 (-1091)) (|:| -2545 #0#))) . T)) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) +(((#0=(-51)) . T) (((-2 (|:| -3420 (-1091)) (|:| -2542 #0#))) . T)) (|has| |#1| (-327)) ((((-525)) . T)) ((((-798)) . T)) (((#0=(-1159 |#1| |#2| |#3| |#4|) $) |has| #0# (-265 #0# #0#))) (|has| |#1| (-341)) (((#0=(-1005) |#1|) . T) ((#0# $) . T) (($ $) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (((#0=(-385 (-525)) #0#) . T) ((#1=(-641) #1#) . T) (($ $) . T)) ((((-294 |#1|)) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) |has| |#1| (-341))) (|has| |#1| (-1020)) (((|#1|) . T)) -(((|#1|) -3279 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) -(((|#1|) -3279 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -3275 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) +(((|#1|) -3275 (|has| |#2| (-345 |#1|)) (|has| |#2| (-395 |#1|)))) (((|#2|) . T)) ((((-385 (-525))) . T) (((-641)) . T) (($) . T)) (((|#3| |#3|) . T)) @@ -2302,7 +2302,7 @@ (((|#2|) . T)) (((|#1|) . T)) ((((-525)) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (((|#1| |#2|) . T)) ((($) . T)) @@ -2339,7 +2339,7 @@ (|has| |#2| (-953)) ((($) . T)) (|has| |#1| (-844)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2347,24 +2347,24 @@ ((($) . T)) (|has| |#1| (-341)) ((((-845 |#1|)) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) -(-3279 (|has| |#1| (-346)) (|has| |#1| (-789))) +(-3275 (|has| |#1| (-346)) (|has| |#1| (-789))) (((|#1|) . T)) ((((-798)) . T)) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1091))))) ((((-385 |#2|) |#3|) . T)) ((($) . T) (((-385 (-525))) . T)) ((((-713) |#1|) . T)) -(((|#2| (-220 (-3596 |#1|) (-713))) . T)) +(((|#2| (-220 (-3594 |#1|) (-713))) . T)) (((|#1| (-497 |#3|)) . T)) ((((-385 (-525))) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-798)) . T)) -(((#0=(-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) #0#) |has| (-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))))) +(((#0=(-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) #0#) |has| (-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))))) (|has| |#1| (-844)) (|has| |#2| (-341)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-798)) . T)) (((|#1|) . T)) @@ -2381,11 +2381,11 @@ (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-37 (-385 (-525)))) (-12 (|has| |#1| (-510)) (|has| |#1| (-770))) ((((-798)) . T)) -((((-1091)) -3279 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-835 (-1091)))))) +((((-1091)) -3275 (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))) (-12 (|has| |#1| (-341)) (|has| |#2| (-835 (-1091)))))) (|has| |#1| (-341)) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1091))))) (|has| |#1| (-341)) @@ -2395,7 +2395,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-341))) (((|#2|) |has| |#1| (-341))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) @@ -2418,31 +2418,31 @@ (((|#2|) |has| |#1| (-341))) ((((-357)) -12 (|has| |#1| (-341)) (|has| |#2| (-821 (-357)))) (((-525)) -12 (|has| |#1| (-341)) (|has| |#2| (-821 (-525))))) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) (|has| |#1| (-341)) (|has| |#1| (-517)) (((|#4| |#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) (((|#3|) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#2|) . T)) (((|#2|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#1| (-37 (-385 (-525)))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) ((((-1074) |#1|) . T)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-346))) (|has| |#1| (-138)) ((((-538 |#1|)) . T)) ((($) . T)) @@ -2450,7 +2450,7 @@ (|has| |#1| (-517)) (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-37 (-385 (-525)))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-327))) (|has| |#1| (-138)) ((((-798)) . T)) ((($) . T)) @@ -2475,7 +2475,7 @@ (|has| |#1| (-733)) (|has| |#1| (-733)) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-110)) . T) ((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2496,7 +2496,7 @@ ((((-525)) . T)) ((((-798)) . T)) ((((-525)) . T)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) ((((-157 (-357))) . T) (((-205)) . T) (((-357)) . T)) ((((-798)) . T)) ((((-798)) . T)) @@ -2508,9 +2508,9 @@ (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (|has| |#1| (-341)) (|has| |#1| (-341)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-450)) (|has| |#1| (-669)) (|has| |#1| (-835 (-1091))) (|has| |#1| (-977)) (|has| |#1| (-1032)) (|has| |#1| (-1020))) (|has| |#1| (-1067)) ((((-525) |#1|) . T)) (((|#1|) . T)) @@ -2528,8 +2528,8 @@ (((|#1|) . T)) (|has| |#1| (-517)) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) ((((-357)) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -2538,7 +2538,7 @@ (|has| |#1| (-517)) (|has| |#1| (-1020)) ((((-722 |#1| (-800 |#2|))) |has| (-722 |#1| (-800 |#2|)) (-288 (-722 |#1| (-800 |#2|))))) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1|) . T)) (((|#2| |#3|) . T)) (|has| |#2| (-844)) @@ -2548,12 +2548,12 @@ (|has| |#1| (-213)) (((|#1| (-497 (-1010 (-1091)))) . T)) (|has| |#2| (-341)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 (-51)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) ((((-798)) . T)) ((((-798)) . T)) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) @@ -2562,8 +2562,8 @@ ((((-525)) . T)) (((|#3|) . T)) ((((-798)) . T)) -(-3279 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3279 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) +(-3275 (|has| |#1| (-286)) (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-160)) (|has| |#1| (-517)) (|has| |#1| (-977))) (((#0=(-538 |#1|) #0#) . T) (($ $) . T) ((#1=(-385 (-525)) #1#) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1|) |has| |#1| (-160))) @@ -2576,7 +2576,7 @@ (((|#1|) . T)) ((((-798)) |has| |#1| (-566 (-798)))) ((((-273 |#3|)) . T)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#2| |#2|) . T) ((|#6| |#6|) . T)) (((|#1|) . T)) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) @@ -2584,20 +2584,20 @@ (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) (((|#1|) . T) (((-385 (-525))) . T) (($) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#2|) . T) ((|#6|) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-844)) (|has| |#1| (-844)) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T)) -((((-2 (|:| -3423 (-1074)) (|:| -2545 |#1|))) . T)) +((((-2 (|:| -3420 (-1074)) (|:| -2542 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2611,10 +2611,10 @@ (((|#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020)))) (((#0=(-385 (-525)) #0#) . T)) ((((-385 (-525))) . T)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1|) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-501)) . T)) ((((-798)) . T)) ((((-1091)) |has| |#2| (-835 (-1091))) (((-1005)) . T)) @@ -2628,12 +2628,12 @@ ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) ((((-1091)) |has| |#1| (-835 (-1091)))) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) -(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#1|) . T)) +(((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525)))) ((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) ((($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) -((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-517)))) +((((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-517)))) (|has| |#1| (-517)) (((|#1|) |has| |#1| (-341))) ((((-525)) . T)) @@ -2652,8 +2652,8 @@ ((((-798)) . T)) (|has| |#2| (-762)) (|has| |#2| (-762)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) -(((|#1|) . T) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) (($) . T) ((|#1|) . T)) +(((|#1|) . T) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) . T)) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1|) . T) (((-525)) |has| |#1| (-968 (-525))) (((-385 (-525))) |has| |#1| (-968 (-385 (-525))))) ((((-525)) |has| |#1| (-821 (-525))) (((-357)) |has| |#1| (-821 (-357)))) @@ -2679,12 +2679,12 @@ (((|#2| (-713)) . T)) ((((-1091)) . T)) ((((-805 |#1|)) . T)) -(-3279 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-25)) (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-798)) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-735)) (|has| |#2| (-787))) -(-3279 (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (-12 (|has| |#1| (-789)) (|has| |#2| (-789)))) +(-3275 (|has| |#2| (-735)) (|has| |#2| (-787))) +(-3275 (-12 (|has| |#1| (-735)) (|has| |#2| (-735))) (-12 (|has| |#1| (-789)) (|has| |#2| (-789)))) ((((-805 |#1|)) . T)) (((|#1|) . T)) (|has| |#1| (-346)) @@ -2710,7 +2710,7 @@ (((|#1|) . T)) ((((-798)) . T)) (|has| |#2| (-844)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525))))) ((((-798)) . T)) ((((-798)) . T)) @@ -2743,11 +2743,11 @@ ((((-385 |#2|) |#3|) . T)) (((|#1|) . T)) (|has| |#1| (-1020)) -(((|#2| (-458 (-3596 |#1|) (-713))) . T)) +(((|#2| (-458 (-3594 |#1|) (-713))) . T)) ((((-525) |#1|) . T)) (((|#2| |#2|) . T)) (((|#1| (-497 (-1091))) . T)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-525)) . T)) (((|#2|) . T)) (((|#2|) . T)) @@ -2757,9 +2757,9 @@ ((($) . T) (((-385 (-525))) . T)) ((($) . T)) ((($) . T)) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) (((|#1|) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-798)) . T)) ((((-135)) . T)) (((|#1|) . T) (((-385 (-525))) . T)) @@ -2799,27 +2799,27 @@ (|has| |#1| (-213)) (((|#1| (-497 |#3|)) . T)) (|has| |#1| (-346)) -(((|#2| (-220 (-3596 |#1|) (-713))) . T)) +(((|#2| (-220 (-3594 |#1|) (-713))) . T)) (|has| |#1| (-346)) (|has| |#1| (-346)) (((|#1|) . T) (($) . T)) (((|#1| (-497 |#2|)) . T)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1| (-713)) . T)) (|has| |#1| (-517)) -(-3279 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-25)) (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-787)) (|has| |#2| (-977))) (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) ((((-798)) . T)) -(-3279 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) -(-3279 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-3275 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) (((|#1|) |has| |#1| (-160))) (((|#4|) |has| |#4| (-977))) (((|#3|) |has| |#3| (-977))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) (-12 (|has| |#1| (-341)) (|has| |#2| (-762))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-385 |#2|)) . T) (((-385 (-525))) . T) (($) . T)) ((($ $) . T) ((#0=(-385 (-525)) #0#) . T)) @@ -2832,14 +2832,14 @@ (((|#2|) |has| |#2| (-977)) (((-525)) -12 (|has| |#2| (-588 (-525))) (|has| |#2| (-977)))) (((|#1|) . T)) (|has| |#2| (-341)) -(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) +(((#0=(-385 (-525)) #0#) |has| |#2| (-37 (-385 (-525)))) ((|#2| |#2|) . T) (($ $) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1| |#1|) . T) ((#0=(-385 (-525)) #0#) |has| |#1| (-37 (-385 (-525))))) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#1| |#1|) . T) (($ $) . T) ((#0=(-385 (-525)) #0#) . T)) (((|#2| |#2|) . T)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T) (($) -3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) (((|#1|) . T) (($) . T) (((-385 (-525))) . T)) @@ -2858,25 +2858,25 @@ (((|#1|) |has| |#2| (-395 |#1|))) (((|#1|) |has| |#2| (-395 |#1|))) ((((-845 |#1|)) . T) (((-385 (-525))) . T) (($) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) ((((-798)) . T)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) |has| (-2 (|:| -3423 (-1091)) (|:| -2545 (-51))) (-288 (-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))))) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) |has| (-2 (|:| -3420 (-1091)) (|:| -2542 (-51))) (-288 (-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) ((((-525) |#1|) . T)) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-525) |#1|) . T)) (((|#1|) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((((-1091)) |has| |#1| (-835 (-1091))) (((-760 (-1091))) . T)) -(-3279 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-126)) (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-735)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((((-761 |#1|)) . T)) (((|#1| |#2|) . T)) ((((-798)) . T)) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (((|#1| |#2|) . T)) (|has| |#1| (-37 (-385 (-525)))) ((((-798)) . T)) @@ -2884,15 +2884,15 @@ (((|#1|) |has| |#1| (-160)) (($) |has| |#1| (-517)) (((-385 (-525))) |has| |#1| (-517))) (((|#2|) . T) (((-525)) |has| |#2| (-588 (-525)))) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (-12 (|has| |#1| (-341)) (|has| |#2| (-213)))) +(-3275 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (-12 (|has| |#1| (-341)) (|has| |#2| (-213)))) (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-341)) (((|#1|) . T)) -(((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) +(((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1| |#1|) . T)) ((((-525) |#1|) . T)) ((((-294 |#1|)) . T)) (((#0=(-641) (-1087 #0#)) . T)) -((((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) +((((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (|has| |#1| (-787)) ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) @@ -2909,12 +2909,12 @@ (((#0=(-1159 |#1| |#2| |#3| |#4|)) |has| #0# (-288 #0#))) ((($) . T)) (((|#1|) . T)) -((($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) -(((|#1| |#1|) . T) (($ $) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2| |#2|) |has| |#1| (-341)) ((|#1| |#1|) . T)) +(((|#1| |#1|) . T) (($ $) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) ((#0=(-385 (-525)) #0#) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) (|has| |#2| (-213)) (|has| $ (-138)) ((((-798)) . T)) -((($) . T) (((-385 (-525))) -3279 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) +((($) . T) (((-385 (-525))) -3275 (|has| |#1| (-341)) (|has| |#1| (-327))) ((|#1|) . T)) ((((-798)) . T)) (|has| |#1| (-787)) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091))))) @@ -2926,23 +2926,23 @@ (((|#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#4|) . T)) (|has| |#1| (-517)) -((($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) -((((-1091)) -3279 (-12 (|has| (-1165 |#1| |#2| |#3|) (-835 (-1091))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))))) -(((|#1|) . T) (($) -3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3279 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) +((($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341))) ((|#2|) |has| |#1| (-341)) ((|#1|) . T)) +((((-1091)) -3275 (-12 (|has| (-1165 |#1| |#2| |#3|) (-835 (-1091))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))))) +(((|#1|) . T) (($) -3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-517))) (((-385 (-525))) -3275 (|has| |#1| (-37 (-385 (-525)))) (|has| |#1| (-341)))) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1091))))) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-713) |#1|))) (|has| |#1| (-835 (-1091))))) (((|#4|) -12 (|has| |#4| (-288 |#4|)) (|has| |#4| (-1020)))) ((((-525) |#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) (((|#1|) . T)) (((|#1| (-497 (-760 (-1091)))) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) (((|#1|) . T)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3279 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) ((($) . T) (((-805 |#1|)) . T) (((-385 (-525))) . T)) ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) @@ -2951,15 +2951,15 @@ (((|#1|) . T)) (((|#1|) . T)) ((((-385 |#2|)) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#2| |#2|) . T) ((#0=(-385 (-525)) #0#) . T) (($ $) . T)) ((((-525)) . T)) @@ -2988,32 +2988,32 @@ ((((-1165 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1091)) . T) (((-798)) . T)) (|has| |#1| (-341)) -((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) +((((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) |has| |#2| (-160)) (($) -3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844)))) (((|#2|) . T) ((|#6|) . T)) ((($) . T) (((-385 (-525))) |has| |#2| (-37 (-385 (-525)))) ((|#2|) . T)) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((((-1024)) . T)) ((((-798)) . T)) -((($) -3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) ((($) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525)))) ((|#1|) . T)) ((($) . T)) -((($) -3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) +((($) -3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((|#1|) |has| |#1| (-160)) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (|has| |#2| (-844)) (|has| |#1| (-844)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) |has| |#1| (-160))) ((((-641)) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) |has| |#1| (-160))) (((|#1|) |has| |#1| (-160))) ((((-385 (-525))) . T) (($) . T)) (((|#1| (-525)) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-341)) (|has| |#1| (-341)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) -(-3279 (|has| |#1| (-160)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-160)) (|has| |#1| (-517))) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-713)) . T)) @@ -3028,16 +3028,16 @@ ((((-827 (-357))) . T) (((-827 (-525))) . T) (((-1091)) . T) (((-501)) . T)) (((|#1|) . T)) ((((-798)) . T)) -(-3279 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) -(-3279 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) +(-3275 (|has| |#2| (-126)) (|has| |#2| (-160)) (|has| |#2| (-341)) (|has| |#2| (-735)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-126)) (|has| |#2| (-126))) (-12 (|has| |#1| (-735)) (|has| |#2| (-735)))) ((((-525)) . T)) ((((-525)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) -(-3279 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) +(-3275 (|has| |#2| (-160)) (|has| |#2| (-669)) (|has| |#2| (-787)) (|has| |#2| (-977))) ((((-1091)) -12 (|has| |#2| (-835 (-1091))) (|has| |#2| (-977)))) -(-3279 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) +(-3275 (-12 (|has| |#1| (-450)) (|has| |#2| (-450))) (-12 (|has| |#1| (-669)) (|has| |#2| (-669)))) (|has| |#1| (-136)) (|has| |#1| (-138)) (|has| |#1| (-341)) @@ -3061,7 +3061,7 @@ ((((-1074) (-1091) (-525) (-205) (-798)) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((|#1| |#2|) . T)) -(-3279 (|has| |#1| (-327)) (|has| |#1| (-346))) +(-3275 (|has| |#1| (-327)) (|has| |#1| (-346))) (((|#1| |#2|) . T)) ((($) . T) ((|#1|) . T)) ((((-798)) . T)) @@ -3069,7 +3069,7 @@ ((($) . T) ((|#1|) . T) (((-385 (-525))) |has| |#1| (-37 (-385 (-525))))) (((|#2|) |has| |#2| (-1020)) (((-525)) -12 (|has| |#2| (-968 (-525))) (|has| |#2| (-1020))) (((-385 (-525))) -12 (|has| |#2| (-968 (-385 (-525)))) (|has| |#2| (-1020)))) ((((-501)) |has| |#1| (-567 (-501)))) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-789)) (|has| |#1| (-1020)))) ((($) . T) (((-385 (-525))) . T)) (|has| |#1| (-844)) (|has| |#1| (-844)) @@ -3078,14 +3078,14 @@ ((((-798)) . T)) (((|#2| |#2|) . T)) (((|#1| |#1|) |has| |#1| (-160))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-517))) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-517))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) (((|#2|) . T)) -(-3279 (|has| |#1| (-21)) (|has| |#1| (-787))) +(-3275 (|has| |#1| (-21)) (|has| |#1| (-787))) (((|#1|) |has| |#1| (-160))) (((|#1|) . T)) (((|#1|) . T)) -((((-798)) -3279 (-12 (|has| |#1| (-566 (-798))) (|has| |#2| (-566 (-798)))) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))))) +((((-798)) -3275 (-12 (|has| |#1| (-566 (-798))) (|has| |#2| (-566 (-798)))) (-12 (|has| |#1| (-1020)) (|has| |#2| (-1020))))) ((((-385 |#2|) |#3|) . T)) ((((-385 (-525))) . T) (($) . T)) (|has| |#1| (-37 (-385 (-525)))) @@ -3097,17 +3097,17 @@ (((|#1|) . T) (((-385 (-525))) . T) (((-525)) . T) (($) . T)) (((#0=(-525) #0#) . T)) ((($) . T) (((-385 (-525))) . T)) -(-3279 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) -(-3279 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) +(-3275 (|has| |#4| (-160)) (|has| |#4| (-669)) (|has| |#4| (-787)) (|has| |#4| (-977))) +(-3275 (|has| |#3| (-160)) (|has| |#3| (-669)) (|has| |#3| (-787)) (|has| |#3| (-977))) (|has| |#4| (-735)) -(-3279 (|has| |#4| (-735)) (|has| |#4| (-787))) +(-3275 (|has| |#4| (-735)) (|has| |#4| (-787))) (|has| |#4| (-787)) (|has| |#3| (-735)) -(-3279 (|has| |#3| (-735)) (|has| |#3| (-787))) +(-3275 (|has| |#3| (-735)) (|has| |#3| (-787))) (|has| |#3| (-787)) ((((-525)) . T)) (((|#2|) . T)) -((((-1091)) -3279 (-12 (|has| (-1089 |#1| |#2| |#3|) (-835 (-1091))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))))) +((((-1091)) -3275 (-12 (|has| (-1089 |#1| |#2| |#3|) (-835 (-1091))) (|has| |#1| (-341))) (-12 (|has| |#1| (-15 * (|#1| (-525) |#1|))) (|has| |#1| (-835 (-1091)))))) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-385 (-525)) |#1|))) (|has| |#1| (-835 (-1091))))) ((((-1091)) -12 (|has| |#1| (-15 * (|#1| (-713) |#1|))) (|has| |#1| (-835 (-1091))))) (((|#1| |#1|) . T) (($ $) . T)) @@ -3122,11 +3122,11 @@ ((((-1089 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1089 |#1| |#2| |#3|)) |has| |#1| (-341))) ((((-1056 |#1| |#2|)) . T)) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) ((($) . T)) (|has| |#1| (-953)) -(((|#2|) . T) (((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) ((((-798)) . T)) ((((-501)) |has| |#2| (-567 (-501))) (((-827 (-525))) |has| |#2| (-567 (-827 (-525)))) (((-827 (-357))) |has| |#2| (-567 (-827 (-357)))) (((-357)) . #0=(|has| |#2| (-953))) (((-205)) . #0#)) ((((-1091) (-51)) . T)) @@ -3138,15 +3138,15 @@ ((((-1089 |#1| |#2| |#3|)) . T)) ((((-1089 |#1| |#2| |#3|)) . T) (((-1082 |#1| |#2| |#3|)) . T)) ((((-798)) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-525) |#1|) . T)) ((((-1089 |#1| |#2| |#3|)) |has| |#1| (-341))) (((|#1| |#2| |#3| |#4|) . T)) (((|#1|) . T)) (((|#2|) . T)) (|has| |#2| (-341)) -(((|#3|) . T) ((|#2|) . T) (($) -3279 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) ((|#4|) -3279 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977)))) -(((|#2|) . T) (($) -3279 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3279 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) +(((|#3|) . T) ((|#2|) . T) (($) -3275 (|has| |#4| (-160)) (|has| |#4| (-787)) (|has| |#4| (-977))) ((|#4|) -3275 (|has| |#4| (-160)) (|has| |#4| (-341)) (|has| |#4| (-977)))) +(((|#2|) . T) (($) -3275 (|has| |#3| (-160)) (|has| |#3| (-787)) (|has| |#3| (-977))) ((|#3|) -3275 (|has| |#3| (-160)) (|has| |#3| (-341)) (|has| |#3| (-977)))) (((|#1|) . T)) (((|#1|) . T)) (|has| |#1| (-341)) @@ -3158,7 +3158,7 @@ ((((-798)) . T)) ((((-798)) . T)) (((|#1|) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) ((((-125)) . T) (((-798)) . T)) ((((-525) |#1|) . T)) (((|#1|) . T)) @@ -3166,30 +3166,30 @@ (((|#1|) . T)) (((|#2| $) -12 (|has| |#1| (-341)) (|has| |#2| (-265 |#2| |#2|))) (($ $) . T)) ((($ $) . T)) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-429)) (|has| |#1| (-844))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((((-798)) . T)) ((((-798)) . T)) ((((-798)) . T)) (((|#1| (-497 |#2|)) . T)) -((((-2 (|:| -3423 (-1091)) (|:| -2545 (-51)))) . T)) +((((-2 (|:| -3420 (-1091)) (|:| -2542 (-51)))) . T)) (((|#1| (-525)) . T)) (((|#1| (-385 (-525))) . T)) (((|#1| (-713)) . T)) ((((-112 |#1|)) . T) (($) . T) (((-385 (-525))) . T)) -(-3279 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) -(-3279 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) +(-3275 (|has| |#2| (-429)) (|has| |#2| (-517)) (|has| |#2| (-844))) +(-3275 (|has| |#1| (-429)) (|has| |#1| (-517)) (|has| |#1| (-844))) ((($) . T)) (((|#2| (-497 (-800 |#1|))) . T)) ((((-525) |#1|) . T)) (((|#2|) . T)) (((|#2| (-713)) . T)) -((((-798)) -3279 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) +((((-798)) -3275 (|has| |#1| (-566 (-798))) (|has| |#1| (-1020)))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((((-1074) |#1|) . T)) ((((-385 |#2|)) . T)) -((((-2 (|:| -3423 |#1|) (|:| -2545 |#2|))) . T)) +((((-2 (|:| -3420 |#1|) (|:| -2542 |#2|))) . T)) (|has| |#1| (-517)) (|has| |#1| (-517)) ((($) . T) ((|#2|) . T)) @@ -3197,12 +3197,12 @@ (((|#1| |#2|) . T)) (((|#2| $) |has| |#2| (-265 |#2| |#2|))) (((|#1| (-592 |#1|)) |has| |#1| (-787))) -(-3279 (|has| |#1| (-213)) (|has| |#1| (-327))) -(-3279 (|has| |#1| (-341)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-213)) (|has| |#1| (-327))) +(-3275 (|has| |#1| (-341)) (|has| |#1| (-327))) (|has| |#1| (-1020)) (((|#1|) . T)) ((((-385 (-525))) . T) (($) . T)) -((((-931 |#1|)) . T) ((|#1|) . T) (((-525)) -3279 (|has| (-931 |#1|) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) -3279 (|has| (-931 |#1|) (-968 (-385 (-525)))) (|has| |#1| (-968 (-385 (-525)))))) +((((-931 |#1|)) . T) ((|#1|) . T) (((-525)) -3275 (|has| (-931 |#1|) (-968 (-525))) (|has| |#1| (-968 (-525)))) (((-385 (-525))) -3275 (|has| (-931 |#1|) (-968 (-385 (-525)))) (|has| |#1| (-968 (-385 (-525)))))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) (((|#1| |#1|) -12 (|has| |#1| (-288 |#1|)) (|has| |#1| (-1020)))) @@ -3213,9 +3213,9 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1056 |#1| |#2|) #0#) |has| (-1056 |#1| |#2|) (-288 (-1056 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) #0#) |has| (-2 (|:| -3423 |#1|) (|:| -2545 |#2|)) (-288 (-2 (|:| -3423 |#1|) (|:| -2545 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-288 |#2|)) (|has| |#2| (-1020))) ((#0=(-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) #0#) |has| (-2 (|:| -3420 |#1|) (|:| -2542 |#2|)) (-288 (-2 (|:| -3420 |#1|) (|:| -2542 |#2|))))) (((#0=(-112 |#1|)) |has| #0# (-288 #0#))) -(-3279 (|has| |#1| (-789)) (|has| |#1| (-1020))) +(-3275 (|has| |#1| (-789)) (|has| |#1| (-1020))) ((($ $) . T)) ((($ $) . T) ((#0=(-800 |#1|) $) . T) ((#0# |#2|) . T)) ((($ $) . T) ((|#2| $) |has| |#1| (-213)) ((|#2| |#1|) |has| |#1| (-213)) ((|#3| |#1|) . T) ((|#3| $) . T)) |