2 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005)
3 %%For: (zacchiro) Stefano Zacchiroli,,,
6 %%BoundingBox: 35 35 680 885
15 /EncodingVector 256 array def
18 ISOLatin1Encoding 0 255 getinterval putinterval
71 % Set up ISO Latin 1 character encoding
73 dup dup findfont dup length dict begin
74 { 1 index /FID ne { def }{ pop pop } ifelse
76 /Encoding EncodingVector def
77 currentdict end definefont
79 /Times-Roman starnetISO def
80 /Times-Italic starnetISO def
81 /Times-Bold starnetISO def
82 /Times-BoldItalic starnetISO def
83 /Helvetica starnetISO def
84 /Helvetica-Oblique starnetISO def
85 /Helvetica-Bold starnetISO def
86 /Helvetica-BoldOblique starnetISO def
87 /Courier starnetISO def
88 /Courier-Oblique starnetISO def
89 /Courier-Bold starnetISO def
90 /Courier-BoldOblique starnetISO def
94 %%BeginResource: procset graphviz 0 0
95 /coord-font-family /Times-Roman def
96 /default-font-family /Times-Roman def
97 /coordfont coord-font-family findfont 8 scalefont def
99 /InvScaleFactor 1.0 def
101 dup 1 exch div /InvScaleFactor exch def
106 /solid { [] 0 setdash } bind def
107 /dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
108 /dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
109 /invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
110 /bold { 2 setlinewidth } bind def
112 /unfilled { } bind def
113 /rounded { } bind def
114 /diagonals { } bind def
116 % hooks for setting color
117 /nodecolor { sethsbcolor } bind def
118 /edgecolor { sethsbcolor } bind def
119 /graphcolor { sethsbcolor } bind def
120 /nopcolor {pop pop pop} bind def
122 /beginpage { % i j npages
131 (\() show i str cvs show (,) show j str cvs show (\)) show
141 % draw aligned label in bounding box aligned to current point
142 /alignedtext { % width adj text
148 text stringwidth pop adj mul 0 rmoveto
155 /boxprim { % xcorner ycorner xsize ysize
178 /endpage { showpage } bind def
182 [ % layer color sequence - darkest to lightest
191 /layerlen layercolorseq length def
193 /setlayer {/maxlayer exch def /curlayer exch def
194 layercolorseq curlayer 1 sub layerlen mod get
195 aload pop sethsbcolor
196 /nodecolor {nopcolor} def
197 /edgecolor {nopcolor} def
198 /graphcolor {nopcolor} def
201 /onlayer { curlayer ne {invis} if } def
217 14 default-font-family set_font
219 % /arrowlength 10 def
222 % make sure pdfmark is harmless for PS-interpreters other than Distiller
223 /pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
224 % make '<<' and '>>' safe on PS Level 1 devices
225 /languagelevel where {pop languagelevel}{1} ifelse
227 userdict (<<) cvn ([) cvn load put
228 userdict (>>) cvn ([) cvn load put
233 %%PageBoundingBox: 36 36 680 885
234 %%PageOrientation: Portrait
236 35 35 645 850 boxprim clip newpath
239 0 0 translate 0 rotate
240 0.000 0.000 0.000 graphcolor
241 24.00 /Times-Roman set_font
245 497 574 75 25 ellipse_path
250 [10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72]
257 432 480 54 25 ellipse_path
262 [10.56 6.72 10.56 12 10.56 10.56 6.72 10.56]
267 % acic_content -> cic_acic
268 newpath 480 549 moveto
269 472 538 463 525 455 513 curveto
274 0.000 0.000 0.000 edgecolor
275 newpath 457 510 moveto
280 0.000 0.000 0.000 edgecolor
281 newpath 457 510 moveto
290 441 386 110 25 ellipse_path
295 [10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12]
300 % cic_acic -> cic_proof_checking
301 newpath 434 454 moveto
302 435 444 436 433 437 422 curveto
307 0.000 0.000 0.000 edgecolor
308 newpath 440 422 moveto
313 0.000 0.000 0.000 edgecolor
314 newpath 440 422 moveto
323 318 662 109 25 ellipse_path
328 [10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12]
333 % cic_disambiguation -> acic_content
334 newpath 365 639 moveto
335 390 627 420 612 445 599 curveto
340 0.000 0.000 0.000 edgecolor
341 newpath 446 602 moveto
346 0.000 0.000 0.000 edgecolor
347 newpath 446 602 moveto
356 316 574 86 25 ellipse_path
361 [10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12]
366 % cic_disambiguation -> cic_unification
367 newpath 317 636 moveto
368 317 628 317 619 317 610 curveto
373 0.000 0.000 0.000 edgecolor
374 newpath 321 610 moveto
379 0.000 0.000 0.000 edgecolor
380 newpath 321 610 moveto
389 164 574 44 25 ellipse_path
394 [17.28 12 10.56 6.72 12]
399 % cic_disambiguation -> whelp
400 newpath 276 638 moveto
401 254 626 227 610 205 597 curveto
406 0.000 0.000 0.000 edgecolor
407 newpath 206 594 moveto
412 0.000 0.000 0.000 edgecolor
413 newpath 206 594 moveto
422 523 662 76 25 ellipse_path
427 [10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36]
432 % content_pres -> acic_content
433 newpath 515 637 moveto
434 513 628 510 619 508 610 curveto
439 0.000 0.000 0.000 edgecolor
440 newpath 511 609 moveto
445 0.000 0.000 0.000 edgecolor
446 newpath 511 609 moveto
455 554 750 46 25 ellipse_path
460 [12 7.92 10.56 7.92 6.72 6.72 10.56]
465 % grafite -> content_pres
466 newpath 545 725 moveto
467 542 716 539 706 535 697 curveto
472 0.000 0.000 0.000 edgecolor
473 newpath 538 696 moveto
478 0.000 0.000 0.000 edgecolor
479 newpath 538 696 moveto
486 % cic_unification -> cic_proof_checking
487 newpath 323 549 moveto
488 330 522 345 479 368 448 curveto
489 376 437 387 426 397 417 curveto
494 0.000 0.000 0.000 edgecolor
495 newpath 400 419 moveto
500 0.000 0.000 0.000 edgecolor
501 newpath 400 419 moveto
510 144 662 45 25 ellipse_path
515 [6.72 10.56 10.56 6.72 6.72 10.56 9.36]
520 % tactics -> cic_unification
521 newpath 178 645 moveto
522 202 632 236 615 264 601 curveto
527 0.000 0.000 0.000 edgecolor
528 newpath 266 604 moveto
533 0.000 0.000 0.000 edgecolor
534 newpath 266 604 moveto
542 newpath 150 637 moveto
543 152 628 154 618 156 609 curveto
548 0.000 0.000 0.000 edgecolor
549 newpath 159 609 moveto
554 0.000 0.000 0.000 edgecolor
555 newpath 159 609 moveto
564 151 750 90 25 ellipse_path
569 [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12]
574 % paramodulation -> tactics
575 newpath 149 724 moveto
576 148 716 148 707 147 698 curveto
581 0.000 0.000 0.000 edgecolor
582 newpath 150 698 moveto
587 0.000 0.000 0.000 edgecolor
588 newpath 150 698 moveto
597 412 298 28 25 ellipse_path
609 332 210 70 25 ellipse_path
614 [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92]
620 newpath 394 278 moveto
621 384 267 372 254 361 241 curveto
626 0.000 0.000 0.000 edgecolor
627 newpath 364 239 moveto
632 0.000 0.000 0.000 edgecolor
633 newpath 364 239 moveto
642 431 122 33 25 ellipse_path
653 newpath 415 272 moveto
654 418 242 424 192 427 158 curveto
659 0.000 0.000 0.000 edgecolor
660 newpath 430 158 moveto
665 0.000 0.000 0.000 edgecolor
666 newpath 430 158 moveto
673 % cic_proof_checking -> cic
674 newpath 433 361 moveto
675 430 352 427 342 423 333 curveto
680 0.000 0.000 0.000 edgecolor
681 newpath 426 332 moveto
686 0.000 0.000 0.000 edgecolor
687 newpath 426 332 moveto
696 274 298 42 25 ellipse_path
701 [12 10.56 6.72 6.72 10.56 7.92]
706 % cic_proof_checking -> getter
707 newpath 396 362 moveto
708 371 349 340 332 315 320 curveto
713 0.000 0.000 0.000 edgecolor
714 newpath 316 317 moveto
719 0.000 0.000 0.000 edgecolor
720 newpath 316 317 moveto
727 % getter -> urimanager
728 newpath 290 274 moveto
729 296 265 304 254 310 244 curveto
734 0.000 0.000 0.000 edgecolor
735 newpath 313 245 moveto
740 0.000 0.000 0.000 edgecolor
741 newpath 313 245 moveto
750 190 210 52 25 ellipse_path
755 [7.92 10.56 12 6.72 9.36 6.72 7.92 12]
761 newpath 253 276 moveto
762 243 265 230 252 219 240 curveto
767 0.000 0.000 0.000 edgecolor
768 newpath 222 238 moveto
773 0.000 0.000 0.000 edgecolor
774 newpath 222 238 moveto
783 159 386 58 25 ellipse_path
788 [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56]
794 newpath 203 369 moveto
795 211 366 219 363 227 360 curveto
796 277 342 337 322 374 310 curveto
801 0.000 0.000 0.000 edgecolor
802 newpath 375 313 moveto
807 0.000 0.000 0.000 edgecolor
808 newpath 375 313 moveto
816 newpath 188 364 moveto
817 203 352 223 337 240 324 curveto
822 0.000 0.000 0.000 edgecolor
823 newpath 242 327 moveto
828 0.000 0.000 0.000 edgecolor
829 newpath 242 327 moveto
838 161 298 50 25 ellipse_path
843 [12 18.72 12 9.36 12 6.72]
849 newpath 160 360 moveto
850 160 352 160 343 160 334 curveto
855 0.000 0.000 0.000 edgecolor
856 newpath 164 334 moveto
861 0.000 0.000 0.000 edgecolor
862 newpath 164 334 moveto
870 newpath 163 548 moveto
871 162 515 161 459 160 422 curveto
876 0.000 0.000 0.000 edgecolor
877 newpath 164 422 moveto
882 0.000 0.000 0.000 edgecolor
883 newpath 164 422 moveto
892 431 34 42 25 ellipse_path
897 [10.56 12 6.72 6.72 6.72 12]
904 571 210 54 25 ellipse_path
909 [12 12 12 12 18.72 10.56]
915 newpath 538 189 moveto
916 517 176 488 158 466 144 curveto
921 0.000 0.000 0.000 edgecolor
922 newpath 468 141 moveto
927 0.000 0.000 0.000 edgecolor
928 newpath 468 141 moveto
936 newpath 169 273 moveto
937 172 264 175 254 179 245 curveto
942 0.000 0.000 0.000 edgecolor
943 newpath 182 246 moveto
948 0.000 0.000 0.000 edgecolor
949 newpath 182 246 moveto
957 newpath 229 193 moveto
958 237 190 245 187 252 184 curveto
959 299 166 354 147 390 135 curveto
964 0.000 0.000 0.000 edgecolor
965 newpath 391 138 moveto
970 0.000 0.000 0.000 edgecolor
971 newpath 391 138 moveto
979 newpath 431 96 moveto
980 431 88 431 79 431 70 curveto
985 0.000 0.000 0.000 edgecolor
986 newpath 435 70 moveto
991 0.000 0.000 0.000 edgecolor
992 newpath 435 70 moveto
1002 0.584 0.220 0.933 nodecolor
1003 0.584 0.220 0.933 nodecolor
1004 newpath 136 512 moveto
1010 0.584 0.220 0.933 nodecolor
1011 newpath 136 512 moveto
1018 0.000 0.000 0.000 nodecolor
1021 [17.28 10.56 12 10.56 12 12 10.56 12 10.56 12]
1025 [17.28 12 10.56 6.72 12 10.56 10.56 7.92]
1030 % DependencyAnalyzer -> metadata
1031 newpath 99 448 moveto
1032 109 438 119 427 129 417 curveto
1037 0.000 0.000 0.000 edgecolor
1038 newpath 131 420 moveto
1043 0.000 0.000 0.000 edgecolor
1044 newpath 131 420 moveto
1054 0.584 0.220 0.933 nodecolor
1055 0.584 0.220 0.933 nodecolor
1056 newpath 312 404 moveto
1062 0.584 0.220 0.933 nodecolor
1063 newpath 312 404 moveto
1070 0.000 0.000 0.000 nodecolor
1073 [17.28 10.56 6.72 6.72 10.56 7.92]
1079 newpath 274 368 moveto
1080 274 358 274 346 274 334 curveto
1085 0.000 0.000 0.000 edgecolor
1086 newpath 278 334 moveto
1091 0.000 0.000 0.000 edgecolor
1092 newpath 278 334 moveto
1102 0.584 0.220 0.933 nodecolor
1103 0.584 0.220 0.933 nodecolor
1104 newpath 454 848 moveto
1110 0.584 0.220 0.933 nodecolor
1111 newpath 454 848 moveto
1118 0.000 0.000 0.000 nodecolor
1121 [21.36 10.56 6.72 6.72 6.72 10.56]
1126 % Matita -> cic_disambiguation
1127 newpath 376 815 moveto
1128 343 801 300 783 296 776 curveto
1129 281 752 289 721 299 696 curveto
1134 0.000 0.000 0.000 edgecolor
1135 newpath 302 698 moveto
1140 0.000 0.000 0.000 edgecolor
1141 newpath 302 698 moveto
1149 newpath 447 812 moveto
1150 466 801 491 786 512 774 curveto
1155 0.000 0.000 0.000 edgecolor
1156 newpath 514 777 moveto
1161 0.000 0.000 0.000 edgecolor
1162 newpath 514 777 moveto
1169 % Matita -> paramodulation
1170 newpath 376 818 moveto
1171 336 806 272 787 223 772 curveto
1176 0.000 0.000 0.000 edgecolor
1177 newpath 224 769 moveto
1182 0.000 0.000 0.000 edgecolor
1183 newpath 224 769 moveto
1191 newpath 454 827 moveto
1192 524 814 562 831 610 776 curveto
1193 643 737 629 713 629 662 curveto
1194 629 662 629 662 629 386 curveto
1195 629 334 606 278 590 244 curveto
1200 0.000 0.000 0.000 edgecolor
1201 newpath 593 242 moveto
1206 0.000 0.000 0.000 edgecolor
1207 newpath 593 242 moveto
1217 0.584 0.220 0.933 nodecolor
1218 0.584 0.220 0.933 nodecolor
1219 newpath 601 512 moveto
1225 0.584 0.220 0.933 nodecolor
1226 newpath 601 512 moveto
1233 0.000 0.000 0.000 nodecolor
1236 [13.44 7.92 12 12 7.92]
1240 [16.08 12 10.56 10.56 12 10.56 7.92]
1245 % ProofChecker -> cic_proof_checking
1246 newpath 515 448 moveto
1247 503 438 490 427 478 417 curveto
1252 0.000 0.000 0.000 edgecolor
1253 newpath 480 414 moveto
1258 0.000 0.000 0.000 edgecolor
1259 newpath 480 414 moveto
1269 0.584 0.220 0.933 nodecolor
1270 0.584 0.220 0.933 nodecolor
1271 newpath 489 768 moveto
1277 0.584 0.220 0.933 nodecolor
1278 newpath 489 768 moveto
1285 0.000 0.000 0.000 nodecolor
1288 [17.28 17.28 12 12 12]
1293 % Uwobo -> content_pres
1294 newpath 462 732 moveto
1295 472 721 484 707 495 695 curveto
1300 0.000 0.000 0.000 edgecolor
1301 newpath 498 697 moveto
1306 0.000 0.000 0.000 edgecolor
1307 newpath 498 697 moveto
1317 0.584 0.220 0.933 nodecolor
1318 0.584 0.220 0.933 nodecolor
1319 newpath 385 768 moveto
1325 0.584 0.220 0.933 nodecolor
1326 newpath 385 768 moveto
1333 0.000 0.000 0.000 nodecolor
1336 [22.56 12 10.56 6.72 12]
1341 % Whelp -> cic_disambiguation
1342 newpath 339 732 moveto
1343 336 722 332 709 329 698 curveto
1348 0.000 0.000 0.000 edgecolor
1349 newpath 332 697 moveto
1354 0.000 0.000 0.000 edgecolor
1355 newpath 332 697 moveto
1362 % Whelp -> content_pres
1363 newpath 378 732 moveto
1364 383 729 389 726 394 724 curveto
1365 418 712 446 699 469 687 curveto
1370 0.000 0.000 0.000 edgecolor
1371 newpath 470 690 moveto
1376 0.000 0.000 0.000 edgecolor
1377 newpath 470 690 moveto