diff options
| author | dos-reis <gdr@axiomatics.org> | 2008-09-22 03:05:49 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2008-09-22 03:05:49 +0000 |
| commit | ce18c80b41c0dc210d9bab1d0bfeadaf9845d853 (patch) | |
| tree | cca9330df601ff7e225024f1d6e911f577699f7c /src/share/algebra/category.daase | |
| parent | b79e1543c220c230e3c88dbbee3837d9859f54bf (diff) | |
| download | open-axiom-ce18c80b41c0dc210d9bab1d0bfeadaf9845d853.tar.gz | |
Tidy Syntax and SpadAst.
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 192 |
1 files changed, 96 insertions, 96 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index 3750fe91..bad68a14 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(144986 . 3431030416) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(144986 . 3431041364) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#2| |#2|) . T)) ((((-549)) . T)) ((($ $) -1536 (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-444)) (|has| |#2| (-541)) (|has| |#2| (-880))) ((|#2| |#2|) . T) ((#0=(-400 (-549)) #0#) |has| |#2| (-38 (-400 (-549))))) @@ -45,7 +45,7 @@ (((|#2| (-474 (-3774 |#1|) (-747))) . T)) (((|#1| (-521 (-1142))) . T)) (((#0=(-841 |#1|) #0#) . T) ((#1=(-400 (-549)) #1#) . T) (($ $) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#4| (-361)) (|has| |#3| (-361)) (((|#1|) . T)) @@ -93,7 +93,7 @@ ((($) . T)) (|has| |#1| (-361)) (((|#1|) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) ((((-834)) . T)) ((((-834)) . T)) @@ -205,8 +205,8 @@ (((|#1|) . T)) ((((-400 (-549))) |has| |#1| (-1009 (-400 (-549)))) (((-549)) |has| |#1| (-1009 (-549))) ((|#1|) . T)) (((|#1|) . T) (((-549)) |has| |#1| (-617 (-549)))) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (|has| |#1| (-541)) (|has| |#1| (-541)) (((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) @@ -241,7 +241,7 @@ (((|#1|) . T) (((-549)) |has| |#1| (-1009 (-549))) (((-400 (-549))) |has| |#1| (-1009 (-400 (-549))))) ((($) . T) (((-400 (-549))) |has| |#2| (-38 (-400 (-549)))) ((|#2|) . T)) ((((-400 $) (-400 $)) |has| |#2| (-541)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-880)) ((((-1124) (-52)) . T)) @@ -277,7 +277,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1117)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (|has| (-1211 |#1| |#2| |#3| |#4|) (-143)) (|has| (-1211 |#1| |#2| |#3| |#4|) (-145)) (|has| |#1| (-143)) @@ -294,9 +294,9 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-1018))) ((((-834)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#1|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) ((#0=(-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) #0#) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) ((#0=(-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) #0#) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))))) ((((-549) |#1|) . T)) ((((-834)) . T)) ((((-525)) -12 (|has| |#1| (-594 (-525))) (|has| |#2| (-594 (-525)))) (((-863 (-372))) -12 (|has| |#1| (-594 (-863 (-372)))) (|has| |#2| (-594 (-863 (-372))))) (((-863 (-549))) -12 (|has| |#1| (-594 (-863 (-549)))) (|has| |#2| (-594 (-863 (-549)))))) @@ -387,11 +387,11 @@ ((((-142)) . T)) (((|#3|) |has| |#3| (-1066)) (((-549)) -12 (|has| |#3| (-1009 (-549))) (|has| |#3| (-1066))) (((-400 (-549))) -12 (|has| |#3| (-1009 (-400 (-549)))) (|has| |#3| (-1066)))) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) . T)) ((((-834)) -1536 (|has| |#1| (-593 (-834))) (|has| |#1| (-823)) (|has| |#1| (-1066)))) ((((-525)) |has| |#1| (-594 (-525)))) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) (|has| |#1| (-356)) (-1536 (|has| |#1| (-21)) (|has| |#1| (-821))) ((((-1142) |#1|) |has| |#1| (-505 (-1142) |#1|)) ((|#1| |#1|) |has| |#1| (-302 |#1|))) @@ -400,13 +400,13 @@ (|has| |#1| (-821)) (-1536 (|has| |#1| (-823)) (|has| |#1| (-1066))) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-525)) |has| |#1| (-594 (-525)))) (((|#1| |#2|) . T)) ((((-1142)) -12 (|has| |#1| (-356)) (|has| |#1| (-871 (-1142))))) ((((-1124) |#1|) . T)) (((|#1| |#2| |#3| (-521 |#3|)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#1| (-361)) (|has| |#1| (-361)) (|has| |#1| (-361)) @@ -593,7 +593,7 @@ (((|#4| |#4|) -12 (|has| |#4| (-302 |#4|)) (|has| |#4| (-1066)))) (((|#2|) . T) (((-549)) |has| |#2| (-1009 (-549))) (((-400 (-549))) |has| |#2| (-1009 (-400 (-549))))) (((|#3| |#3|) -12 (|has| |#3| (-302 |#3|)) (|has| |#3| (-1066)))) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#1|) . T)) (((|#1| |#2|) . T)) ((($) . T)) @@ -601,7 +601,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-1536 (|has| |#1| (-823)) (|has| |#1| (-1066))) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#2|) . T)) ((((-834)) -1536 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-593 (-834))) (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-361)) (|has| |#2| (-703)) (|has| |#2| (-769)) (|has| |#2| (-821)) (|has| |#2| (-1018)) (|has| |#2| (-1066))) (((-1225 |#2|)) . T)) (((|#1|) |has| |#1| (-170))) @@ -677,9 +677,9 @@ (-1536 (|has| |#1| (-444)) (|has| |#1| (-880))) ((((-549) |#2|) . T)) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) ((($) -1536 (|has| |#3| (-170)) (|has| |#3| (-821)) (|has| |#3| (-1018))) ((|#3|) -1536 (|has| |#3| (-170)) (|has| |#3| (-356)) (|has| |#3| (-1018)))) ((((-549) |#1|) . T)) @@ -694,11 +694,11 @@ (|has| |#1| (-541)) (|has| |#1| (-38 (-400 (-549)))) (|has| |#1| (-38 (-400 (-549)))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-834)) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (|has| |#1| (-38 (-400 (-549)))) -((((-381) (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-381) (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (|has| |#1| (-38 (-400 (-549)))) (|has| |#2| (-1117)) (-1536 (|has| |#1| (-356)) (|has| |#1| (-541))) @@ -897,7 +897,7 @@ (|has| |#2| (-170)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-227)) (|has| |#2| (-1018))) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (-1536 (|has| |#3| (-769)) (|has| |#3| (-821))) (-1536 (|has| |#3| (-769)) (|has| |#3| (-821))) ((((-834)) . T)) @@ -927,10 +927,10 @@ (((|#1| (-400 (-549))) . T)) (((|#3|) . T) (((-592 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((($ $) . T) ((|#2| $) . T)) (((|#1|) . T) (((-400 (-549))) . T) (($) . T)) (((#0=(-1140 |#1| |#2| |#3|) #0#) -12 (|has| (-1140 |#1| |#2| |#3|) (-302 (-1140 |#1| |#2| |#3|))) (|has| |#1| (-356))) (((-1142) #0#) -12 (|has| (-1140 |#1| |#2| |#3|) (-505 (-1142) (-1140 |#1| |#2| |#3|))) (|has| |#1| (-356)))) @@ -938,8 +938,8 @@ ((((-834)) . T)) ((((-834)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) -(((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) (((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) +(((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) (((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))))) ((((-834)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -952,7 +952,7 @@ (|has| |#1| (-1066)) (((|#2| |#2|) -1536 (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-1018))) (($ $) |has| |#2| (-170))) (((|#2|) -1536 (|has| |#2| (-170)) (|has| |#2| (-356)))) -((((-549) (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T) ((|#1| |#2|) . T)) +((((-549) (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -1536 (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-1018))) (($) |has| |#2| (-170))) ((((-747)) . T)) ((((-549)) . T)) @@ -983,7 +983,7 @@ (-1536 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-361)) (|has| |#2| (-703)) (|has| |#2| (-769)) (|has| |#2| (-821)) (|has| |#2| (-1018)) (|has| |#2| (-1066))) (-12 (|has| |#3| (-227)) (|has| |#3| (-1018))) (|has| |#2| (-1117)) -(((#0=(-52)) . T) (((-2 (|:| -3336 (-1142)) (|:| -1791 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -3337 (-1142)) (|:| -1792 #0#))) . T)) (((|#1| |#2|) . T)) (-1536 (|has| |#3| (-170)) (|has| |#3| (-821)) (|has| |#3| (-1018))) (((|#1| (-549) (-1048)) . T)) @@ -1008,7 +1008,7 @@ ((((-834)) . T)) (|has| |#1| (-342)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (|has| |#1| (-541)) (((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) ((((-834)) . T)) @@ -1060,7 +1060,7 @@ (-12 (|has| |#1| (-769)) (|has| |#2| (-769))) (-1536 (|has| |#2| (-170)) (|has| |#2| (-821)) (|has| |#2| (-1018))) (((|#2|) . T) (($) . T)) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#1| (-1164)) (((#0=(-549) #0#) . T) ((#1=(-400 (-549)) #1#) . T) (($ $) . T)) ((((-400 (-549))) . T) (($) . T)) @@ -1090,7 +1090,7 @@ ((($) . T) (((-400 (-549))) -1536 (|has| |#1| (-356)) (|has| |#1| (-342))) ((|#1|) . T)) (-1536 (|has| |#1| (-170)) (|has| |#1| (-541))) ((($) . T)) -(((#0=(-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) #0#) |has| (-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))))) +(((#0=(-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) #0#) |has| (-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))))) (|has| |#2| (-823)) ((($) . T)) (((|#2|) |has| |#2| (-1066))) @@ -1102,10 +1102,10 @@ ((((-834)) . T)) ((((-549)) |has| #0=(-400 |#2|) (-617 (-549))) ((#0#) . T)) ((((-549) (-142)) . T)) -((((-549) (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T) ((|#1| |#2|) . T)) +((((-549) (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T) ((|#1| |#2|) . T)) ((((-400 (-549))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-834)) . T)) ((((-881 |#1|)) . T)) (|has| |#1| (-356)) @@ -1130,7 +1130,7 @@ ((((-834)) . T)) ((($) . T)) (((|#2|) . T) (($) . T)) -((((-549) (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T) ((|#1| |#2|) . T)) +((((-549) (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-170))) ((($) |has| |#1| (-541)) ((|#1|) |has| |#1| (-170)) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) @@ -1143,7 +1143,7 @@ (((|#1|) . T)) ((((-525)) |has| |#1| (-594 (-525))) (((-863 (-372))) |has| |#1| (-594 (-863 (-372)))) (((-863 (-549))) |has| |#1| (-594 (-863 (-549))))) ((((-834)) . T)) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#2| (-821)) (-12 (|has| |#2| (-227)) (|has| |#2| (-1018))) (|has| |#1| (-541)) @@ -1168,7 +1168,7 @@ (((|#1|) . T)) (((|#2|) . T)) ((((-1142)) |has| (-400 |#2|) (-871 (-1142)))) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) ((($) . T)) ((($) . T)) (((|#2|) . T)) @@ -1178,7 +1178,7 @@ (((|#2| |#2|) -1536 (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-1018))) (($ $) |has| |#2| (-170))) ((((-834)) . T)) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T) ((|#2|) . T)) ((((-834)) . T)) ((((-834)) . T)) ((((-1124) (-1142) (-549) (-219) (-834)) . T)) @@ -1262,7 +1262,7 @@ ((((-970 |#1|)) . T) ((|#1|) . T)) ((((-834)) . T)) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-400 (-549))) . T) (((-400 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1138 |#1|)) . T)) ((((-549)) . T) (($) . T) (((-400 (-549))) . T)) @@ -1270,7 +1270,7 @@ (|has| |#1| (-823)) (((|#2|) . T)) ((((-549)) . T) (($) . T) (((-400 (-549))) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) ((((-549) |#2|) . T)) ((((-834)) -1536 (|has| |#1| (-593 (-834))) (|has| |#1| (-1066)))) (((|#2|) . T)) @@ -1287,7 +1287,7 @@ (|has| |#1| (-38 (-400 (-549)))) (((|#2|) . T)) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#2| |#2|) . T)) (|has| |#2| (-356)) (((|#2|) . T) (((-549)) |has| |#2| (-1009 (-549))) (((-400 (-549))) |has| |#2| (-1009 (-400 (-549))))) @@ -1317,7 +1317,7 @@ (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) (((|#1| |#2|) . T)) ((((-549) (-142)) . T)) -(((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) +(((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) ((($) -1536 (|has| |#1| (-444)) (|has| |#1| (-541)) (|has| |#1| (-880))) ((|#1|) |has| |#1| (-170)) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) (|has| |#1| (-823)) (((|#2| (-747) (-1048)) . T)) @@ -1359,7 +1359,7 @@ ((((-381) (-1124)) . T)) ((($) |has| |#1| (-541)) ((|#1|) |has| |#1| (-170)) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) ((((-834)) -1536 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-593 (-834))) (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-361)) (|has| |#2| (-703)) (|has| |#2| (-769)) (|has| |#2| (-821)) (|has| |#2| (-1018)) (|has| |#2| (-1066))) (((-1225 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -3336 (-1124)) (|:| -1791 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -3337 (-1124)) (|:| -1792 #0#))) . T)) (((|#1|) . T)) ((((-834)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) @@ -1405,11 +1405,11 @@ (|has| |#1| (-145)) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +(((|#1|) . T) (((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) ((((-1140 |#1| |#2| |#3|)) |has| |#1| (-356))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-1142) (-52)) . T)) ((($ $) . T)) (((|#1| (-549)) . T)) @@ -1454,11 +1454,11 @@ (|has| |#1| (-38 (-400 (-549)))) (-1536 (|has| |#1| (-356)) (|has| |#1| (-342))) (|has| |#1| (-38 (-400 (-549)))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-1142)) |has| |#1| (-871 (-1142))) (((-1048)) . T)) (((|#1|) . T)) (|has| |#1| (-821)) -(((#0=(-2 (|:| -3336 (-1124)) (|:| -1791 (-52))) #0#) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))))) +(((#0=(-2 (|:| -3337 (-1124)) (|:| -1792 (-52))) #0#) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) (|has| |#1| (-1066)) ((((-834)) . T) (((-1147)) . T)) @@ -1500,7 +1500,7 @@ (((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) ((#0=(-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) #0#) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) ((#0=(-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) #0#) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))))) (-1536 (|has| |#2| (-444)) (|has| |#2| (-880))) (-1536 (|has| |#1| (-444)) (|has| |#1| (-880))) (((|#1|) . T) (($) . T)) @@ -1525,7 +1525,7 @@ ((((-400 (-549))) -1536 (|has| |#1| (-38 (-400 (-549)))) (|has| |#1| (-356))) (($) -1536 (|has| |#1| (-356)) (|has| |#1| (-541))) (((-1140 |#1| |#2| |#3|)) |has| |#1| (-356)) ((|#1|) |has| |#1| (-170))) (((|#1|) |has| |#1| (-170)) (((-400 (-549))) -1536 (|has| |#1| (-38 (-400 (-549)))) (|has| |#1| (-356))) (($) -1536 (|has| |#1| (-356)) (|has| |#1| (-541)))) ((($) |has| |#1| (-541)) ((|#1|) |has| |#1| (-170)) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) ((((-400 |#2|)) . T) (((-400 (-549))) . T) (($) . T)) ((((-648 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1586,7 +1586,7 @@ (((|#1|) . T)) (((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) ((($ $) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((($ $) . T)) ((((-549) (-112)) . T)) ((($) . T)) @@ -1615,7 +1615,7 @@ (((|#1| (-1189 |#1| |#2| |#3|)) . T)) (((|#1| (-747)) . T)) (((|#1|) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-834)) . T)) (|has| |#1| (-1066)) ((((-1124) |#1|) . T)) @@ -1654,7 +1654,7 @@ (|has| |#1| (-541)) (((|#1|) . T)) ((((-834)) . T)) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((|#1|) |has| |#1| (-170))) ((($) |has| |#1| (-541)) ((|#1|) |has| |#1| (-170)) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) @@ -1672,7 +1672,7 @@ (|has| |#1| (-821)) (((|#1| (-549) (-1048)) . T)) (-1536 (|has| |#1| (-871 (-1142))) (|has| |#1| (-1018))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1| (-400 (-549)) (-1048)) . T)) (((|#1| (-747) (-1048)) . T)) (|has| |#1| (-823)) @@ -1691,8 +1691,8 @@ (-1536 (|has| |#2| (-25)) (|has| |#2| (-130)) (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-361)) (|has| |#2| (-703)) (|has| |#2| (-769)) (|has| |#2| (-821)) (|has| |#2| (-1018)) (|has| |#2| (-1066))) (((|#2|) |has| |#2| (-170))) (((|#1|) |has| |#1| (-170))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) ((((-834)) . T)) (|has| |#3| (-821)) ((((-834)) . T)) @@ -1706,9 +1706,9 @@ (((|#2|) |has| |#2| (-356))) ((($) . T) ((|#1|) . T) (((-400 (-549))) |has| |#1| (-356))) (|has| |#1| (-823)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) |has| (-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))))) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) |has| (-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))))) (-1536 (|has| |#1| (-444)) (|has| |#1| (-880))) (((|#2|) . T) (((-549)) |has| |#2| (-617 (-549)))) ((((-834)) . T)) @@ -1756,7 +1756,7 @@ (|has| (-400 |#2|) (-227)) (|has| |#1| (-880)) (((|#2|) |has| |#2| (-1018))) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (|has| |#1| (-356)) (((|#1|) |has| |#1| (-170))) (((|#1| |#1|) . T)) @@ -1803,13 +1803,13 @@ ((((-112)) |has| |#1| (-1066)) (((-834)) -1536 (|has| |#1| (-21)) (|has| |#1| (-25)) (|has| |#1| (-170)) (|has| |#1| (-356)) (|has| |#1| (-465)) (|has| |#1| (-703)) (|has| |#1| (-871 (-1142))) (|has| |#1| (-1018)) (|has| |#1| (-1078)) (|has| |#1| (-1066)))) (((|#1|) . T) (($) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))) . T)) ((((-834)) . T)) ((((-549) |#1|) . T)) ((((-675)) . T) (((-400 (-549))) . T) (((-549)) . T)) (((|#1| |#1|) |has| |#1| (-170))) (((|#2|) . T)) -(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) ((((-372)) . T)) ((((-675)) . T)) ((((-400 (-549))) . #0=(|has| |#2| (-356))) (($) . #0#)) @@ -1827,7 +1827,7 @@ (|has| |#1| (-823)) ((((-1142)) |has| |#2| (-871 (-1142)))) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-400 (-549))) . T) (($) . T)) (|has| |#1| (-465)) (|has| |#1| (-361)) @@ -1855,11 +1855,11 @@ (|has| |#1| (-38 (-400 (-549)))) (|has| |#1| (-38 (-400 (-549)))) (|has| |#1| (-823)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (((|#1| |#2|) . T)) (|has| |#1| (-145)) (|has| |#1| (-143)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)))) ((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)))) ((|#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066)))) (((|#2|) . T)) (((|#3|) . T)) ((((-116 |#1|)) . T)) @@ -1877,7 +1877,7 @@ ((((-525)) |has| |#1| (-594 (-525))) (((-863 (-549))) |has| |#1| (-594 (-863 (-549)))) (((-863 (-372))) |has| |#1| (-594 (-863 (-372)))) (((-372)) . #0=(|has| |#1| (-993))) (((-219)) . #0#)) (((|#1|) |has| |#1| (-356))) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((($ $) . T) (((-592 $) $) . T)) (-1536 (|has| |#1| (-356)) (|has| |#1| (-541))) ((($) . T) (((-1211 |#1| |#2| |#3| |#4|)) . T) (((-400 (-549))) . T)) @@ -1937,7 +1937,7 @@ ((((-834)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -1536 (|has| |#1| (-283)) (|has| |#1| (-356))) ((#0=(-400 (-549)) #0#) |has| |#1| (-356))) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) ((($) . T)) ((((-549) |#1|) . T)) ((((-1142)) |has| (-400 |#2|) (-871 (-1142)))) @@ -1976,7 +1976,7 @@ ((($) -1536 (|has| |#1| (-356)) (|has| |#1| (-342))) (((-400 (-549))) -1536 (|has| |#1| (-356)) (|has| |#1| (-342))) ((|#1|) . T)) ((((-549)) . T)) (|has| |#1| (-38 (-400 (-549)))) -((((-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))))) +((((-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))))) (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) (|has| |#1| (-821)) (|has| |#1| (-38 (-400 (-549)))) @@ -2015,10 +2015,10 @@ (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) ((((-525)) |has| |#4| (-594 (-525)))) ((((-834)) . T) (((-621 |#4|)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-821)) -(((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) (((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) |has| (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|)) (-302 (-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))))) +(((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066))) (((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) |has| (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|)) (-302 (-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))))) (|has| |#1| (-1066)) (|has| |#1| (-356)) (|has| |#1| (-823)) @@ -2058,7 +2058,7 @@ ((((-834)) . T)) ((((-834)) . T)) ((((-525)) |has| |#1| (-594 (-525)))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-1142) |#1|) |has| |#1| (-505 (-1142) |#1|)) ((|#1| |#1|) |has| |#1| (-302 |#1|))) (((|#1|) -1536 (|has| |#1| (-170)) (|has| |#1| (-356)))) ((((-309 |#1|)) . T)) @@ -2085,7 +2085,7 @@ (|has| |#1| (-541)) (((|#2|) . T)) ((((-549)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) . T)) (-1536 (|has| |#1| (-143)) (|has| |#1| (-145)) (|has| |#1| (-170)) (|has| |#1| (-541)) (|has| |#1| (-1018))) ((((-563 |#1|)) . T)) @@ -2198,14 +2198,14 @@ (|has| |#2| (-880)) (|has| |#1| (-880)) (((|#2|) |has| |#2| (-170))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-1217 |#1| |#2| |#3|)) |has| |#1| (-356))) ((((-834)) . T)) ((((-834)) . T)) ((((-525)) . T) (((-549)) . T) (((-863 (-549))) . T) (((-372)) . T) (((-219)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))) . T)) (((|#1|) . T)) ((((-834)) . T)) (((|#1| |#2|) . T)) @@ -2226,7 +2226,7 @@ ((((-400 (-549))) . T) (($) . T)) ((((-834)) . T)) ((((-834)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-834)) . T)) ((((-834)) . T)) @@ -2237,7 +2237,7 @@ (((|#1|) . T)) ((((-834)) . T)) ((((-621 (-142))) . T) (((-1124)) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) ((((-1142) |#1|) |has| |#1| (-505 (-1142) |#1|)) ((|#1| |#1|) |has| |#1| (-302 |#1|))) (|has| |#1| (-823)) ((((-834)) . T)) @@ -2291,8 +2291,8 @@ (-1536 (|has| |#1| (-143)) (|has| |#1| (-361))) (-1536 (|has| |#1| (-143)) (|has| |#1| (-361))) (-1536 (|has| |#1| (-143)) (|has| |#1| (-361))) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) -(((#0=(-52)) . T) (((-2 (|:| -3336 (-1142)) (|:| -1791 #0#))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -3337 (-1142)) (|:| -1792 #0#))) . T)) (|has| |#1| (-342)) ((((-549)) . T)) ((((-834)) . T)) @@ -2362,7 +2362,7 @@ (|has| |#2| (-993)) ((($) . T)) (|has| |#1| (-880)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2384,7 +2384,7 @@ ((((-400 (-549))) . T)) (-1536 (|has| |#1| (-444)) (|has| |#1| (-541)) (|has| |#1| (-880))) ((((-834)) . T)) -(((#0=(-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) #0#) |has| (-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))))) +(((#0=(-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) #0#) |has| (-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))))) (|has| |#1| (-880)) (|has| |#2| (-356)) (-1536 (|has| |#2| (-130)) (|has| |#2| (-170)) (|has| |#2| (-356)) (|has| |#2| (-769)) (|has| |#2| (-821)) (|has| |#2| (-1018))) @@ -2418,7 +2418,7 @@ (((|#1|) . T)) (((|#2|) |has| |#1| (-356))) (((|#2|) |has| |#1| (-356))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-170))) (((|#1|) . T)) @@ -2455,9 +2455,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-1536 (|has| |#2| (-170)) (|has| |#2| (-703)) (|has| |#2| (-821)) (|has| |#2| (-1018))) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#1| (-38 (-400 (-549)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-400 (-549)))) @@ -2572,7 +2572,7 @@ (|has| |#1| (-227)) (((|#1| (-521 (-1054 (-1142)))) . T)) (|has| |#2| (-356)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 (-52)))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-302 |#1|)) (|has| |#1| (-1066)))) ((((-834)) . T)) @@ -2622,7 +2622,7 @@ (|has| |#1| (-880)) ((($) -1536 (|has| |#1| (-170)) (|has| |#1| (-444)) (|has| |#1| (-541)) (|has| |#1| (-880))) ((|#1|) . T) (((-400 (-549))) |has| |#1| (-38 (-400 (-549))))) (((|#1|) . T)) -((((-2 (|:| -3336 (-1124)) (|:| -1791 |#1|))) . T)) +((((-2 (|:| -3337 (-1124)) (|:| -1792 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1| |#1|) . T)) @@ -2736,7 +2736,7 @@ (((|#1|) . T)) ((((-834)) . T)) (|has| |#2| (-880)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) ((((-525)) |has| |#2| (-594 (-525))) (((-863 (-372))) |has| |#2| (-594 (-863 (-372)))) (((-863 (-549))) |has| |#2| (-594 (-863 (-549))))) ((((-834)) . T)) ((((-834)) . T)) @@ -2894,7 +2894,7 @@ ((((-834)) . T)) ((((-834)) . T) (((-1147)) . T)) ((((-1178)) . T) (((-834)) . T) (((-1147)) . T)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) |has| (-2 (|:| -3336 (-1142)) (|:| -1791 (-52))) (-302 (-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))))) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) |has| (-2 (|:| -3337 (-1142)) (|:| -1792 (-52))) (-302 (-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))))) (-1536 (|has| |#2| (-444)) (|has| |#2| (-541)) (|has| |#2| (-880))) ((((-549) |#1|) . T)) ((((-549) |#1|) . T)) @@ -3066,7 +3066,7 @@ (-1536 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-130)) (|has| |#2| (-130))) (-12 (|has| |#1| (-769)) (|has| |#2| (-769)))) ((((-549)) . T)) ((((-549)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-1536 (|has| |#2| (-170)) (|has| |#2| (-703)) (|has| |#2| (-821)) (|has| |#2| (-1018))) @@ -3157,11 +3157,11 @@ ((((-1140 |#1| |#2| |#3|)) |has| |#1| (-356))) ((((-1106 |#1| |#2|)) . T)) ((((-1140 |#1| |#2| |#3|)) |has| |#1| (-356))) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) ((($) . T)) (|has| |#1| (-993)) -(((|#2|) . T) (((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) ((((-834)) . T)) ((((-525)) |has| |#2| (-594 (-525))) (((-863 (-549))) |has| |#2| (-594 (-863 (-549)))) (((-863 (-372))) |has| |#2| (-594 (-863 (-372)))) (((-372)) . #0=(|has| |#2| (-993))) (((-219)) . #0#)) ((((-1142) (-52)) . T)) @@ -3207,7 +3207,7 @@ ((((-834)) . T)) ((((-834)) . T)) (((|#1| (-521 |#2|)) . T)) -((((-2 (|:| -3336 (-1142)) (|:| -1791 (-52)))) . T)) +((((-2 (|:| -3337 (-1142)) (|:| -1792 (-52)))) . T)) (((|#1| (-549)) . T)) (((|#1| (-400 (-549))) . T)) (((|#1| (-747)) . T)) @@ -3233,7 +3233,7 @@ (((|#1| |#2|) . T)) ((((-1124) |#1|) . T)) ((((-400 |#2|)) . T)) -((((-2 (|:| -3336 |#1|) (|:| -1791 |#2|))) . T)) +((((-2 (|:| -3337 |#1|) (|:| -1792 |#2|))) . T)) (|has| |#1| (-541)) (|has| |#1| (-541)) ((($) . T) ((|#2|) . T)) @@ -3257,7 +3257,7 @@ (((|#1|) . T)) (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1106 |#1| |#2|) #0#) |has| (-1106 |#1| |#2|) (-302 (-1106 |#1| |#2|)))) -(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) #0#) |has| (-2 (|:| -3336 |#1|) (|:| -1791 |#2|)) (-302 (-2 (|:| -3336 |#1|) (|:| -1791 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-302 |#2|)) (|has| |#2| (-1066))) ((#0=(-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) #0#) |has| (-2 (|:| -3337 |#1|) (|:| -1792 |#2|)) (-302 (-2 (|:| -3337 |#1|) (|:| -1792 |#2|))))) (((#0=(-116 |#1|)) |has| #0# (-302 #0#))) ((($ $) . T)) (-1536 (|has| |#1| (-823)) (|has| |#1| (-1066))) |