diff options
Diffstat (limited to 'src/share/algebra/category.daase')
| -rw-r--r-- | src/share/algebra/category.daase | 198 |
1 files changed, 99 insertions, 99 deletions
diff --git a/src/share/algebra/category.daase b/src/share/algebra/category.daase index a48f255c..9f1265e3 100644 --- a/src/share/algebra/category.daase +++ b/src/share/algebra/category.daase @@ -1,6 +1,6 @@ -(189904 . 3485328472) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(189904 . 3485354335) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) ((((-570)) . T) (($) -3684 (|has| |#1| (-311)) (|has| |#1| (-368)) (|has| |#1| (-354)) (|has| |#1| (-562))) (((-413 (-570))) -3684 (|has| |#1| (-368)) (|has| |#1| (-354)) (|has| |#1| (-1047 (-413 (-570))))) ((|#1|) . T)) (((|#2| |#2|) . T)) ((((-570)) . T)) @@ -57,7 +57,7 @@ (((#0=(-876 |#1|) #0#) . T) ((#1=(-413 (-570)) #1#) . T) (($ $) . T)) ((((-1168)) . T) (((-965 (-130))) . T) (((-868)) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (|has| |#4| (-373)) (|has| |#3| (-373)) (((|#1|) . T)) @@ -75,7 +75,7 @@ ((((-570)) . T) (((-413 (-570))) -3684 (|has| |#2| (-38 (-413 (-570)))) (|has| |#2| (-1047 (-413 (-570))))) ((|#2|) . T) (($) -3684 (|has| |#2| (-458)) (|has| |#2| (-562)) (|has| |#2| (-916))) (((-870 |#1|)) . T)) (-3684 (|has| |#1| (-368)) (|has| |#1| (-562))) (-3684 (|has| |#1| (-368)) (|has| |#1| (-562))) -((((-2 (|:| -4285 |#1|) (|:| -2092 |#2|))) . T)) +((((-2 (|:| -4286 |#1|) (|:| -3201 |#2|))) . T)) ((($) . T)) ((((-570)) . T) (((-413 (-570))) -3684 (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-1047 (-413 (-570))))) ((|#1|) . T) (($) -3684 (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916))) (((-1186)) . T)) ((((-868)) -3684 (|has| |#1| (-619 (-868))) (|has| |#1| (-856)) (|has| |#1| (-1109)))) @@ -132,7 +132,7 @@ (((|#1|) . T) (((-413 (-570))) |has| |#1| (-38 (-413 (-570)))) (($) . T)) (-3684 (|has| |#1| (-856)) (|has| |#1| (-1109))) (((|#1|) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-570)) . T)) ((((-868)) . T)) (((|#1| |#2|) . T)) @@ -271,8 +271,8 @@ (((|#1|) . T)) ((((-413 (-570))) |has| |#1| (-1047 (-413 (-570)))) (((-570)) |has| |#1| (-1047 (-570))) ((|#1|) . T)) (((|#1|) . T) (((-570)) |has| |#1| (-645 (-570)))) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -(((|#1|) . T) (((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (|has| |#1| (-562)) ((((-570)) -3684 (|has| |#4| (-174)) (|has| |#4| (-854)) (-12 (|has| |#4| (-1047 (-570))) (|has| |#4| (-1109))) (|has| |#4| (-1058))) ((|#4|) -3684 (|has| |#4| (-174)) (|has| |#4| (-1109))) (((-413 (-570))) -12 (|has| |#4| (-1047 (-413 (-570)))) (|has| |#4| (-1109)))) ((((-570)) -3684 (|has| |#3| (-174)) (|has| |#3| (-854)) (-12 (|has| |#3| (-1047 (-570))) (|has| |#3| (-1109))) (|has| |#3| (-1058))) ((|#3|) -3684 (|has| |#3| (-174)) (|has| |#3| (-1109))) (((-413 (-570))) -12 (|has| |#3| (-1047 (-413 (-570)))) (|has| |#3| (-1109)))) @@ -301,11 +301,11 @@ ((((-542)) |has| |#2| (-620 (-542))) (((-899 (-384))) |has| |#2| (-620 (-899 (-384)))) (((-899 (-570))) |has| |#2| (-620 (-899 (-570))))) ((((-868)) . T)) (((|#1| |#2| |#3| |#4|) . T)) -((((-2 (|:| -4285 |#1|) (|:| -2092 |#2|))) . T) (((-868)) . T)) +((((-2 (|:| -4286 |#1|) (|:| -3201 |#2|))) . T) (((-868)) . T)) ((((-542)) |has| |#1| (-620 (-542))) (((-899 (-384))) |has| |#1| (-620 (-899 (-384)))) (((-899 (-570))) |has| |#1| (-620 (-899 (-570))))) (((|#4|) -3684 (|has| |#4| (-174)) (|has| |#4| (-368)) (|has| |#4| (-1058))) (($) |has| |#4| (-174))) (((|#3|) -3684 (|has| |#3| (-174)) (|has| |#3| (-368)) (|has| |#3| (-1058))) (($) |has| |#3| (-174))) -((((-2 (|:| -4285 |#1|) (|:| -2092 |#2|))) . T)) +((((-2 (|:| -4286 |#1|) (|:| -3201 |#2|))) . T)) ((((-868)) . T)) ((((-868)) . T)) ((((-542)) . T) (((-570)) . T) (((-899 (-570))) . T) (((-384)) . T) (((-227)) . T)) @@ -313,7 +313,7 @@ (((|#1|) . T) (((-570)) |has| |#1| (-1047 (-570))) (((-413 (-570))) |has| |#1| (-1047 (-413 (-570))))) ((($) . T) (((-413 (-570))) |has| |#2| (-38 (-413 (-570)))) ((|#2|) . T)) ((((-413 $) (-413 $)) |has| |#2| (-562)) (($ $) . T) ((|#2| |#2|) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))) . T)) (((|#1|) . T)) (|has| |#2| (-916)) ((((-1168) (-52)) . T)) @@ -352,7 +352,7 @@ (((|#1|) . T)) (((|#2| |#2|) . T)) (|has| |#1| (-1161)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (|has| (-1263 |#1| |#2| |#3| |#4|) (-146)) (|has| (-1263 |#1| |#2| |#3| |#4|) (-148)) (|has| |#1| (-146)) @@ -370,10 +370,10 @@ ((($) . T) ((|#1|) . T)) (((|#2|) |has| |#2| (-1058))) ((((-868)) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (((|#1|) . T)) ((((-1277 (-344 (-2848) (-2848 (QUOTE X)) (-705)))) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) ((#0=(-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) ((#0=(-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))))) ((((-868)) . T)) ((((-570) |#1|) . T)) ((((-542)) -12 (|has| |#1| (-620 (-542))) (|has| |#2| (-620 (-542)))) (((-899 (-384))) -12 (|has| |#1| (-620 (-899 (-384)))) (|has| |#2| (-620 (-899 (-384))))) (((-899 (-570))) -12 (|has| |#1| (-620 (-899 (-570)))) (|has| |#2| (-620 (-899 (-570)))))) @@ -493,12 +493,12 @@ ((((-242 |#1| |#2|) |#2|) . T)) ((((-868)) . T)) (((|#3|) |has| |#3| (-1109)) (((-570)) -12 (|has| |#3| (-1047 (-570))) (|has| |#3| (-1109))) (((-413 (-570))) -12 (|has| |#3| (-1047 (-413 (-570)))) (|has| |#3| (-1109)))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T)) ((((-868)) -3684 (|has| |#1| (-619 (-868))) (|has| |#1| (-856)) (|has| |#1| (-1109)))) ((((-542)) |has| |#1| (-620 (-542)))) (((|#1|) |has| |#1| (-174))) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) (|has| |#1| (-368)) ((((-1191)) . T)) (((|#1|) . T)) @@ -509,13 +509,13 @@ (|has| |#1| (-854)) (-3684 (|has| |#1| (-856)) (|has| |#1| (-1109))) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-542)) |has| |#1| (-620 (-542)))) (((|#1| |#2|) . T)) ((((-1186)) -12 (|has| |#1| (-368)) (|has| |#1| (-907 (-1186))))) ((((-1168) |#1|) . T)) (((|#1| |#2| |#3| (-537 |#3|)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (|has| |#1| (-373)) (|has| |#1| (-373)) (|has| |#1| (-373)) @@ -730,7 +730,7 @@ ((((-1149 |#1| |#2|)) |has| (-1149 |#1| |#2|) (-313 (-1149 |#1| |#2|)))) (((|#4| |#4|) -12 (|has| |#4| (-313 |#4|)) (|has| |#4| (-1109)))) (((|#3| |#3|) -12 (|has| |#3| (-313 |#3|)) (|has| |#3| (-1109)))) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (((|#2|) . T) (((-570)) |has| |#2| (-1047 (-570))) (((-413 (-570))) |has| |#2| (-1047 (-413 (-570))))) (((|#1|) . T)) (((|#1| |#2|) . T)) @@ -739,7 +739,7 @@ (((|#2|) . T)) (((|#3|) . T)) (-3684 (|has| |#1| (-856)) (|has| |#1| (-1109))) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (((|#2|) . T)) ((((-868)) -3684 (|has| |#2| (-25)) (|has| |#2| (-132)) (|has| |#2| (-619 (-868))) (|has| |#2| (-174)) (|has| |#2| (-368)) (|has| |#2| (-373)) (|has| |#2| (-732)) (|has| |#2| (-799)) (|has| |#2| (-854)) (|has| |#2| (-1058)) (|has| |#2| (-1109))) (((-1277 |#2|)) . T)) ((((-413 (-570))) |has| |#1| (-1047 (-413 (-570)))) ((|#1|) . T) (((-570)) . T) (($) . T)) @@ -839,9 +839,9 @@ (-3684 (|has| |#1| (-458)) (|has| |#1| (-916))) ((((-570) |#2|) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) ((($) -3684 (|has| |#3| (-174)) (|has| |#3| (-854)) (|has| |#3| (-1058))) ((|#3|) -3684 (|has| |#3| (-174)) (|has| |#3| (-368)) (|has| |#3| (-1058)))) ((((-570) |#1|) . T)) @@ -856,11 +856,11 @@ (|has| |#1| (-562)) (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-38 (-413 (-570)))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (|has| |#1| (-38 (-413 (-570)))) -((((-394) (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-394) (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (|has| |#1| (-38 (-413 (-570)))) (|has| |#2| (-1161)) (-3684 (|has| |#1| (-368)) (|has| |#1| (-562))) @@ -1098,7 +1098,7 @@ (|has| |#2| (-174)) (((|#1| |#2|) . T)) (-12 (|has| |#2| (-235)) (|has| |#2| (-1058))) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (-3684 (|has| |#3| (-799)) (|has| |#3| (-854))) (-3684 (|has| |#3| (-799)) (|has| |#3| (-854))) ((((-868)) . T)) @@ -1129,10 +1129,10 @@ (((|#1| (-413 (-570))) . T)) (((|#3|) . T) (((-618 $)) . T)) (((|#1| |#2|) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T)) (((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-570)) -3684 (|has| |#2| (-174)) (|has| |#2| (-854)) (-12 (|has| |#2| (-1047 (-570))) (|has| |#2| (-1109))) (|has| |#2| (-1058))) ((|#2|) -3684 (|has| |#2| (-174)) (|has| |#2| (-1109))) (((-413 (-570))) -12 (|has| |#2| (-1047 (-413 (-570)))) (|has| |#2| (-1109)))) (((|#1|) . T) (((-413 (-570))) . T) (($) . T)) ((($ $) . T) ((|#2| $) . T)) @@ -1141,8 +1141,8 @@ ((((-868)) . T)) ((((-868)) . T)) (((|#1| |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) -(((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) (((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) +(((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) (((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))))) ((((-868)) . T)) (((|#1|) . T)) (((|#3| |#3|) . T)) @@ -1158,7 +1158,7 @@ (|has| (-1103 |#1|) (-1109)) (((|#2| |#2|) -3684 (|has| |#2| (-174)) (|has| |#2| (-368)) (|has| |#2| (-1058))) (($ $) |has| |#2| (-174))) (((|#2|) -3684 (|has| |#2| (-174)) (|has| |#2| (-368)))) -((((-570) (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T) ((|#1| |#2|) . T)) +((((-570) (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T) ((|#1| |#2|) . T)) (((|#2|) -3684 (|has| |#2| (-174)) (|has| |#2| (-368)) (|has| |#2| (-1058))) (($) |has| |#2| (-174))) ((((-570)) . T)) ((((-1191)) . T)) @@ -1203,7 +1203,7 @@ (-3684 (|has| |#2| (-25)) (|has| |#2| (-132)) (|has| |#2| (-174)) (|has| |#2| (-368)) (|has| |#2| (-373)) (|has| |#2| (-732)) (|has| |#2| (-799)) (|has| |#2| (-854)) (|has| |#2| (-1058)) (|has| |#2| (-1109))) (-12 (|has| |#3| (-235)) (|has| |#3| (-1058))) (|has| |#2| (-1161)) -(((#0=(-52)) . T) (((-2 (|:| -4111 (-1186)) (|:| -3117 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -4111 (-1186)) (|:| -3116 #0#))) . T)) (((|#1| |#2|) . T)) (-3684 (|has| |#3| (-174)) (|has| |#3| (-854)) (|has| |#3| (-1058))) (((|#1| (-570) (-1091)) . T)) @@ -1233,7 +1233,7 @@ (((|#4|) . T) (((-868)) . T)) (((|#3|) . T) ((|#2|) . T) (($) -3684 (|has| |#4| (-174)) (|has| |#4| (-854)) (|has| |#4| (-1058))) (((-570)) . T) ((|#4|) -3684 (|has| |#4| (-174)) (|has| |#4| (-368)) (|has| |#4| (-1058)))) (((|#2|) . T) (($) -3684 (|has| |#3| (-174)) (|has| |#3| (-854)) (|has| |#3| (-1058))) (((-570)) . T) ((|#3|) -3684 (|has| |#3| (-174)) (|has| |#3| (-368)) (|has| |#3| (-1058)))) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (|has| |#1| (-562)) (((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) ((((-868)) . T)) @@ -1293,7 +1293,7 @@ (-12 (|has| |#1| (-799)) (|has| |#2| (-799))) (-3684 (|has| |#2| (-174)) (|has| |#2| (-854)) (|has| |#2| (-1058))) ((($) . T) (((-570)) . T) ((|#2|) . T)) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#2|) . T) (($) . T)) (|has| |#1| (-1212)) (((#0=(-570) #0#) . T) ((#1=(-413 (-570)) #1#) . T) (($ $) . T)) @@ -1324,7 +1324,7 @@ ((($) . T) (((-413 (-570))) -3684 (|has| |#1| (-368)) (|has| |#1| (-354))) ((|#1|) . T)) (-3684 (|has| |#1| (-174)) (|has| |#1| (-562))) ((($) . T)) -(((#0=(-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) #0#) |has| (-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))))) +(((#0=(-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) #0#) |has| (-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))))) ((($) . T)) ((($) . T)) (((|#2|) |has| |#2| (-1109))) @@ -1340,10 +1340,10 @@ ((((-570)) |has| #0=(-413 |#2|) (-645 (-570))) ((#0#) . T)) ((($) . T) (((-570)) . T)) ((((-570) (-145)) . T)) -((((-570) (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T) ((|#1| |#2|) . T)) +((((-570) (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T) ((|#1| |#2|) . T)) ((((-413 (-570))) . T) (($) . T)) (((|#1|) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-868)) . T)) ((((-917 |#1|)) . T)) (|has| |#1| (-368)) @@ -1372,7 +1372,7 @@ ((((-868)) . T)) ((($) . T)) (((|#2|) . T) (($) . T)) -((((-570) (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T) (((-1244 (-570)) $) . T) ((|#1| |#2|) . T)) +((((-570) (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T) (((-1244 (-570)) $) . T) ((|#1| |#2|) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-174))) ((($) |has| |#1| (-562)) ((|#1|) |has| |#1| (-174)) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) @@ -1391,7 +1391,7 @@ ((((-542)) |has| |#1| (-620 (-542))) (((-899 (-384))) |has| |#1| (-620 (-899 (-384)))) (((-899 (-570))) |has| |#1| (-620 (-899 (-570))))) ((((-868)) . T)) ((((-876 |#1|)) . T) (($) . T) (((-413 (-570))) . T)) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-512)) . T)) (|has| |#2| (-854)) ((((-512)) . T)) @@ -1426,7 +1426,7 @@ (((|#1|) . T)) ((((-1186)) |has| (-413 |#2|) (-907 (-1186)))) (((|#2|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) ((((-413 (-570))) |has| |#2| (-38 (-413 (-570)))) ((|#2|) |has| |#2| (-174)) (($) -3684 (|has| |#2| (-458)) (|has| |#2| (-562)) (|has| |#2| (-916)))) ((((-413 (-570))) |has| |#2| (-38 (-413 (-570)))) ((|#2|) . T) (($) -3684 (|has| |#2| (-174)) (|has| |#2| (-458)) (|has| |#2| (-562)) (|has| |#2| (-916)))) ((((-413 (-570))) |has| |#1| (-38 (-413 (-570)))) ((|#1|) |has| |#1| (-174)) (($) -3684 (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916)))) @@ -1443,7 +1443,7 @@ (((|#2|) . T) (((-570)) . T)) ((((-868)) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T) ((|#2|) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T) ((|#2|) . T)) ((((-868)) . T)) ((((-868)) . T)) ((((-1168) (-1186) (-570) (-227) (-868)) . T)) @@ -1534,7 +1534,7 @@ ((((-1008 |#1|)) . T) ((|#1|) . T)) ((((-868)) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-413 (-570))) . T) (((-413 |#1|)) . T) ((|#1|) . T) (($) . T)) (((|#1| (-1182 |#1|)) . T)) ((((-570)) . T) (($) . T) (((-413 (-570))) . T)) @@ -1543,7 +1543,7 @@ (((|#1|) . T) (((-570)) . T) (($) . T)) (((|#2|) . T)) ((((-570)) . T) (($) . T) (((-413 (-570))) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) ((((-868)) -3684 (|has| |#1| (-619 (-868))) (|has| |#1| (-1109)))) ((((-570) |#2|) . T)) (((|#1|) . T) (((-413 (-570))) . T) (((-570)) . T) (($) . T)) @@ -1557,7 +1557,7 @@ (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-38 (-413 (-570)))) ((((-1269 |#1| |#2| |#3|)) |has| |#1| (-368))) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (((|#2| |#2|) . T)) (|has| |#1| (-1109)) (|has| |#2| (-368)) @@ -1602,7 +1602,7 @@ (((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) (((|#1| |#2|) . T)) ((((-1244 (-570)) $) . T) (((-570) (-145)) . T)) -(((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109)))) +(((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)))) ((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109)))) ((($) -3684 (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916))) ((|#1|) |has| |#1| (-174)) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) (|has| |#1| (-856)) (((|#2| (-777) (-1091)) . T)) @@ -1655,7 +1655,7 @@ ((((-394) (-1168)) . T)) ((($) |has| |#1| (-562)) ((|#1|) |has| |#1| (-174)) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) ((((-868)) -3684 (|has| |#2| (-25)) (|has| |#2| (-132)) (|has| |#2| (-619 (-868))) (|has| |#2| (-174)) (|has| |#2| (-368)) (|has| |#2| (-373)) (|has| |#2| (-732)) (|has| |#2| (-799)) (|has| |#2| (-854)) (|has| |#2| (-1058)) (|has| |#2| (-1109))) (((-1277 |#2|)) . T)) -(((#0=(-52)) . T) (((-2 (|:| -4111 (-1168)) (|:| -3117 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -4111 (-1168)) (|:| -3116 #0#))) . T)) (((|#1|) . T)) ((((-868)) . T)) (((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109)))) @@ -1707,12 +1707,12 @@ (((|#2|) |has| |#2| (-174))) (((|#1|) . T)) (((|#2|) . T)) -(((|#1|) . T) (((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +(((|#1|) . T) (((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#2|) . T)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-1184 |#1| |#2| |#3|)) |has| |#1| (-368))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-1186) (-52)) . T)) ((((-413 (-570)) |#1|) . T) (($ $) . T)) (((|#1| (-570)) . T)) @@ -1764,11 +1764,11 @@ (-3684 (|has| |#1| (-368)) (|has| |#1| (-354))) (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-38 (-413 (-570)))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-1186)) |has| |#1| (-907 (-1186))) (((-1091)) . T)) (((|#1|) . T)) (|has| |#1| (-854)) -(((#0=(-2 (|:| -4111 (-1168)) (|:| -3117 (-52))) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))))) +(((#0=(-2 (|:| -4111 (-1168)) (|:| -3116 (-52))) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))))) (((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) (|has| |#1| (-1109)) ((((-868)) . T) (((-1191)) . T)) @@ -1831,7 +1831,7 @@ ((((-570) |#2|) . T)) (((|#1|) . T)) (((|#1| |#2|) . T)) -(((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) ((#0=(-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))))) +(((|#1| |#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) ((#0=(-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) #0#) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))))) (-3684 (|has| |#2| (-458)) (|has| |#2| (-916))) (-3684 (|has| |#1| (-458)) (|has| |#1| (-916))) (((|#1|) . T) (($) . T)) @@ -1856,7 +1856,7 @@ ((((-413 (-570))) -3684 (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-368))) (($) -3684 (|has| |#1| (-368)) (|has| |#1| (-562))) (((-1184 |#1| |#2| |#3|)) |has| |#1| (-368)) ((|#1|) |has| |#1| (-174))) (((|#1|) |has| |#1| (-174)) (((-413 (-570))) -3684 (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-368))) (($) -3684 (|has| |#1| (-368)) (|has| |#1| (-562)))) ((($) |has| |#1| (-562)) ((|#1|) |has| |#1| (-174)) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-413 |#2|)) . T) (((-413 (-570))) . T) (($) . T)) ((((-678 |#1|)) . T)) (((|#1| |#2| |#3| |#4|) . T)) @@ -1936,7 +1936,7 @@ ((((-980)) . T)) ((((-980)) . T) (((-868)) . T)) ((($ $) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((($ $) . T)) ((((-570) (-112)) . T)) ((($) . T)) @@ -1966,7 +1966,7 @@ (((|#1| (-777)) . T)) (((|#1|) . T)) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (|has| |#1| (-1109)) ((((-1168) |#1|) . T)) ((($) . T)) @@ -2014,7 +2014,7 @@ ((($) -3684 (|has| |#1| (-174)) (|has| |#1| (-368)) (|has| |#1| (-562))) (((-413 (-570))) -3684 (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-368))) (((-1184 |#1| |#2| |#3|)) |has| |#1| (-368)) ((|#1|) . T)) (((|#1|) . T) (($) -3684 (|has| |#1| (-174)) (|has| |#1| (-368)) (|has| |#1| (-562))) (((-413 (-570))) -3684 (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-368)))) ((($) -3684 (|has| |#1| (-174)) (|has| |#1| (-562))) ((|#1|) . T) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (((|#1|) |has| |#1| (-174))) ((((-868)) . T)) ((($) |has| |#1| (-562)) ((|#1|) |has| |#1| (-174)) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) @@ -2038,7 +2038,7 @@ (|has| |#1| (-854)) (((|#1| (-570) (-1091)) . T)) (-3684 (|has| |#1| (-907 (-1186))) (|has| |#1| (-1058))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1| (-413 (-570)) (-1091)) . T)) (((|#1| (-777) (-1091)) . T)) (|has| |#1| (-856)) @@ -2060,8 +2060,8 @@ ((((-695 (-344 (-2848) (-2848 (QUOTE X) (QUOTE HESS)) (-705)))) . T)) (((|#2|) |has| |#2| (-174))) (((|#1|) |has| |#1| (-174))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) ((((-868)) . T)) (|has| |#3| (-854)) ((((-868)) . T)) @@ -2077,11 +2077,11 @@ ((($) . T) ((|#1|) . T) (((-413 (-570))) |has| |#1| (-368))) (|has| |#1| (-856)) (((|#1|) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T) (((-570)) . T)) (((|#2|) . T)) ((((-570)) . T) ((|#3|) . T)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) |has| (-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))))) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) |has| (-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))))) (-3684 (|has| |#1| (-458)) (|has| |#1| (-916))) (((|#2|) . T) (((-570)) |has| |#2| (-645 (-570)))) ((((-868)) . T)) @@ -2140,7 +2140,7 @@ ((((-650 |#1|)) . T)) (|has| |#1| (-916)) (((|#2|) |has| |#2| (-1058))) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (|has| |#1| (-368)) (((|#1|) |has| |#1| (-174))) (((|#1| |#1|) . T)) @@ -2192,7 +2192,7 @@ (((|#1| |#2|) . T)) ((($) . T) (((-570)) . T) (((-413 (-570))) . T)) ((((-570)) . T) (($) . T) (((-413 (-570))) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))) . T)) (((|#1|) . T) (((-413 (-570))) . T) (((-570)) . T) (($) . T)) (((|#1|) . T) (((-413 (-570))) . T) (((-570)) . T) (($) . T)) (((|#1|) . T) (((-413 (-570))) . T) (((-570)) . T) (($) . T)) @@ -2206,7 +2206,7 @@ (((|#2|) . T)) ((($) . T) (((-570)) . T) (((-413 (-570))) -3684 (|has| |#1| (-368)) (|has| |#1| (-354))) ((|#1|) . T)) ((((-570) |#1|) . T)) -(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) ((((-384)) . T)) ((((-705)) . T)) ((((-413 (-570))) . #0=(|has| |#2| (-368))) (($) . #0#)) @@ -2223,7 +2223,7 @@ (|has| |#1| (-368)) ((((-1186)) |has| |#2| (-907 (-1186)))) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-413 (-570))) . T) (($) . T)) (|has| |#1| (-479)) (|has| |#1| (-373)) @@ -2251,12 +2251,12 @@ (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-38 (-413 (-570)))) (|has| |#1| (-856)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-570)) . T)) (|has| |#1| (-148)) (|has| |#1| (-146)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)))) ((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109)))) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)))) ((|#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109)))) (((|#2|) . T)) (((|#3|) . T)) ((((-117 |#1|)) . T)) @@ -2276,7 +2276,7 @@ ((((-542)) |has| |#1| (-620 (-542))) (((-899 (-570))) |has| |#1| (-620 (-899 (-570)))) (((-899 (-384))) |has| |#1| (-620 (-899 (-384)))) (((-384)) . #0=(|has| |#1| (-1031))) (((-227)) . #0#)) (((|#1|) |has| |#1| (-368))) ((((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((($ $) . T) (((-618 $) $) . T)) (-3684 (|has| |#1| (-368)) (|has| |#1| (-562))) ((($) . T) (((-1263 |#1| |#2| |#3| |#4|)) . T) (((-413 (-570))) . T)) @@ -2351,7 +2351,7 @@ ((((-959 |#1|)) . T) (((-868)) . T)) (((|#3|) . T)) (((|#1| |#1|) . T) (($ $) -3684 (|has| |#1| (-294)) (|has| |#1| (-368))) ((#0=(-413 (-570)) #0#) |has| |#1| (-368))) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-959 |#1|)) . T)) ((($) . T)) ((((-570) |#1|) . T)) @@ -2398,7 +2398,7 @@ ((($) -3684 (|has| |#1| (-368)) (|has| |#1| (-354))) (((-413 (-570))) -3684 (|has| |#1| (-368)) (|has| |#1| (-354))) ((|#1|) . T)) ((((-570)) . T)) (|has| |#1| (-38 (-413 (-570)))) -((((-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))))) +((((-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))))) (((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) (|has| |#1| (-854)) (|has| |#1| (-38 (-413 (-570)))) @@ -2442,10 +2442,10 @@ ((($) -3684 (|has| |#1| (-174)) (|has| |#1| (-368)) (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916))) ((|#1|) . T) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) ((((-542)) |has| |#4| (-620 (-542)))) ((((-868)) . T) (((-650 |#4|)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T)) (|has| |#1| (-854)) -(((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) (((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) |has| (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))))) +(((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109))) (((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) |has| (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|)) (-313 (-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))))) (|has| |#1| (-1109)) (|has| |#1| (-368)) (((|#1|) . T)) @@ -2490,7 +2490,7 @@ ((((-868)) . T)) ((((-868)) . T)) ((((-542)) |has| |#1| (-620 (-542)))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-570)) . T) (($) . T) (((-413 (-570))) . T)) ((((-1186) |#1|) |has| |#1| (-520 (-1186) |#1|)) ((|#1| |#1|) |has| |#1| (-313 |#1|))) (((|#1|) -3684 (|has| |#1| (-174)) (|has| |#1| (-368)))) @@ -2529,7 +2529,7 @@ (|has| |#1| (-562)) (((|#2|) . T)) ((((-570)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T)) (-3684 (|has| |#1| (-146)) (|has| |#1| (-148)) (|has| |#1| (-174)) (|has| |#1| (-562)) (|has| |#1| (-1058))) (((|#1| (-59 |#1|) (-59 |#1|)) . T)) @@ -2668,16 +2668,16 @@ (|has| |#2| (-916)) (|has| |#1| (-916)) (((|#2|) |has| |#2| (-174))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-1269 |#1| |#2| |#3|)) |has| |#1| (-368))) ((((-868)) . T)) ((((-868)) . T)) ((((-542)) . T) (((-570)) . T) (((-899 (-570))) . T) (((-384)) . T) (((-227)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-570)) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))) . T)) (((|#1|) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-868)) . T)) (((|#1| |#2|) . T)) ((($) . T) (((-570)) . T)) @@ -2699,7 +2699,7 @@ ((((-868)) . T)) ((((-868)) . T)) ((((-189)) . T) (((-868)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#2| |#2|) . T) ((|#1| |#1|) . T)) ((((-868)) . T)) ((((-868)) . T)) @@ -2712,7 +2712,7 @@ ((((-868)) . T)) ((((-1168)) . T)) ((((-1186) |#1|) |has| |#1| (-520 (-1186) |#1|)) ((|#1| |#1|) |has| |#1| (-313 |#1|))) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (|has| |#1| (-856)) ((((-868)) . T)) ((((-542)) |has| |#1| (-620 (-542)))) @@ -2774,9 +2774,9 @@ (-3684 (|has| |#1| (-146)) (|has| |#1| (-373))) (-3684 (|has| |#1| (-146)) (|has| |#1| (-373))) (-3684 (|has| |#1| (-146)) (|has| |#1| (-373))) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-570) |#3|) . T)) -(((#0=(-52)) . T) (((-2 (|:| -4111 (-1186)) (|:| -3117 #0#))) . T)) +(((#0=(-52)) . T) (((-2 (|:| -4111 (-1186)) (|:| -3116 #0#))) . T)) (|has| |#1| (-354)) ((((-570)) . T)) ((((-868)) . T)) @@ -2862,7 +2862,7 @@ (|has| |#2| (-1031)) ((($) . T)) (|has| |#1| (-916)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((($) . T)) (((|#2|) . T)) (((|#1|) . T)) @@ -2890,7 +2890,7 @@ ((((-413 (-570))) . T)) (-3684 (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916))) ((((-1168)) . T) (((-868)) . T)) -(((#0=(-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) #0#) |has| (-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))))) +(((#0=(-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) #0#) |has| (-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))))) ((((-1168)) . T)) (|has| |#1| (-916)) (|has| |#2| (-368)) @@ -2928,7 +2928,7 @@ (((|#2|) |has| |#1| (-368))) (((|#2|) |has| |#1| (-368))) ((((-570)) . T) (($) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1|) . T)) (((|#1|) |has| |#1| (-174))) (((|#1|) . T)) @@ -2973,9 +2973,9 @@ (((|#2|) . T)) (((|#2|) . T)) (-3684 (|has| |#2| (-174)) (|has| |#2| (-732)) (|has| |#2| (-854)) (|has| |#2| (-1058))) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (|has| |#1| (-38 (-413 (-570)))) (((|#1| |#2|) . T)) (|has| |#1| (-38 (-413 (-570)))) @@ -3109,7 +3109,7 @@ (|has| |#2| (-368)) ((((-587 |#1|)) . T) (((-413 (-570))) . T) (($) . T) (((-570)) . T)) ((((-570)) . T) (((-413 (-570))) . T) (($) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 (-52)))) . T)) (((|#1|) . T)) (((|#1|) . T) (((-570)) . T)) (((|#1|) -12 (|has| |#1| (-313 |#1|)) (|has| |#1| (-1109)))) @@ -3171,7 +3171,7 @@ ((($) -3684 (|has| |#1| (-174)) (|has| |#1| (-458)) (|has| |#1| (-562)) (|has| |#1| (-916))) ((|#1|) . T) (((-413 (-570))) |has| |#1| (-38 (-413 (-570))))) ((((-868)) . T)) (((|#1|) . T)) -((((-2 (|:| -4111 (-1168)) (|:| -3117 |#1|))) . T)) +((((-2 (|:| -4111 (-1168)) (|:| -3116 |#1|))) . T)) (((|#1|) . T)) (((|#1|) . T)) (((|#1|) . T)) @@ -3302,7 +3302,7 @@ (((|#1|) . T)) ((((-868)) . T)) (|has| |#2| (-916)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-542)) |has| |#2| (-620 (-542))) (((-899 (-384))) |has| |#2| (-620 (-899 (-384)))) (((-899 (-570))) |has| |#2| (-620 (-899 (-570))))) ((((-868)) . T)) ((((-868)) . T)) @@ -3498,7 +3498,7 @@ ((((-1191)) . T)) ((((-868)) . T) (((-1191)) . T)) ((((-1191)) . T)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) |has| (-2 (|:| -4111 (-1186)) (|:| -3117 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))))) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) |has| (-2 (|:| -4111 (-1186)) (|:| -3116 (-52))) (-313 (-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))))) (-3684 (|has| |#2| (-458)) (|has| |#2| (-562)) (|has| |#2| (-916))) ((((-570) |#1|) . T)) ((((-570) |#1|) . T)) @@ -3709,7 +3709,7 @@ (-3684 (-12 (|has| |#1| (-21)) (|has| |#2| (-21))) (-12 (|has| |#1| (-23)) (|has| |#2| (-23))) (-12 (|has| |#1| (-132)) (|has| |#2| (-132))) (-12 (|has| |#1| (-799)) (|has| |#2| (-799)))) ((((-570)) . T)) ((((-570)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (((|#1| |#2|) . T)) (((|#1|) . T)) (-3684 (|has| |#2| (-174)) (|has| |#2| (-732)) (|has| |#2| (-854)) (|has| |#2| (-1058))) @@ -3817,11 +3817,11 @@ ((((-1184 |#1| |#2| |#3|)) |has| |#1| (-368))) ((((-1149 |#1| |#2|)) . T)) ((((-1184 |#1| |#2| |#3|)) |has| |#1| (-368))) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((($) . T)) (|has| |#1| (-1031)) -(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +(((|#2|) . T) (((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) ((((-868)) . T)) ((((-542)) |has| |#2| (-620 (-542))) (((-899 (-570))) |has| |#2| (-620 (-899 (-570)))) (((-899 (-384))) |has| |#2| (-620 (-899 (-384)))) (((-384)) . #0=(|has| |#2| (-1031))) (((-227)) . #0#)) ((((-298 |#3|)) . T)) @@ -3875,7 +3875,7 @@ ((((-868)) . T)) ((((-868)) . T)) (((|#1| (-537 |#2|)) . T)) -((((-2 (|:| -4111 (-1186)) (|:| -3117 (-52)))) . T)) +((((-2 (|:| -4111 (-1186)) (|:| -3116 (-52)))) . T)) ((((-570) (-130)) . T)) (((|#1| (-570)) . T)) (((|#1| (-413 (-570))) . T)) @@ -3912,7 +3912,7 @@ (((|#1| |#2|) . T)) ((((-1168) |#1|) . T)) ((((-413 |#2|)) . T)) -((((-2 (|:| -4111 |#1|) (|:| -3117 |#2|))) . T)) +((((-2 (|:| -4111 |#1|) (|:| -3116 |#2|))) . T)) (|has| |#1| (-562)) (|has| |#1| (-562)) ((($) . T) ((|#2|) . T)) @@ -3946,7 +3946,7 @@ (((|#1| |#2| |#3| |#4|) . T)) (((#0=(-1149 |#1| |#2|) #0#) |has| (-1149 |#1| |#2|) (-313 (-1149 |#1| |#2|)))) (((|#1|) . T)) -(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3117 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3117 |#2|))))) +(((|#2| |#2|) -12 (|has| |#2| (-313 |#2|)) (|has| |#2| (-1109))) ((#0=(-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) #0#) |has| (-2 (|:| -4111 |#1|) (|:| -3116 |#2|)) (-313 (-2 (|:| -4111 |#1|) (|:| -3116 |#2|))))) (|has| |#1| (-290 |#1| |#1|)) (((#0=(-117 |#1|)) |has| #0# (-313 #0#))) ((($ $) . T)) |