2 %%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005)
3 %%For: (zacchiro) Stefano Zacchiroli,,,
6 %%BoundingBox: 35 35 819 801
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 819 801
234 %%PageOrientation: Portrait
236 35 35 784 766 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 536 562 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 487 474 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 522 537 moveto
269 517 528 511 518 506 508 curveto
274 0.000 0.000 0.000 edgecolor
275 newpath 509 506 moveto
280 0.000 0.000 0.000 edgecolor
281 newpath 509 506 moveto
290 487 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 487 448 moveto
302 487 440 487 431 487 422 curveto
307 0.000 0.000 0.000 edgecolor
308 newpath 491 422 moveto
313 0.000 0.000 0.000 edgecolor
314 newpath 491 422 moveto
323 377 650 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 420 626 moveto
335 441 615 466 601 487 589 curveto
340 0.000 0.000 0.000 edgecolor
341 newpath 489 592 moveto
346 0.000 0.000 0.000 edgecolor
347 newpath 489 592 moveto
356 355 562 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 371 624 moveto
368 369 616 366 607 364 598 curveto
373 0.000 0.000 0.000 edgecolor
374 newpath 367 597 moveto
379 0.000 0.000 0.000 edgecolor
380 newpath 367 597 moveto
389 205 562 44 25 ellipse_path
394 [17.28 12 10.56 6.72 12]
399 % cic_disambiguation -> whelp
400 newpath 331 627 moveto
401 305 614 273 597 247 584 curveto
406 0.000 0.000 0.000 edgecolor
407 newpath 248 581 moveto
412 0.000 0.000 0.000 edgecolor
413 newpath 248 581 moveto
422 643 650 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 614 626 moveto
434 602 616 586 603 573 593 curveto
439 0.000 0.000 0.000 edgecolor
440 newpath 575 590 moveto
445 0.000 0.000 0.000 edgecolor
446 newpath 575 590 moveto
455 706 562 75 25 ellipse_path
460 [12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36]
465 % content_pres -> utf8_macros
466 newpath 661 625 moveto
467 668 616 676 605 682 595 curveto
472 0.000 0.000 0.000 edgecolor
473 newpath 685 597 moveto
478 0.000 0.000 0.000 edgecolor
479 newpath 685 597 moveto
488 644 738 46 25 ellipse_path
493 [12 7.92 10.56 7.92 6.72 6.72 10.56]
498 % grafite -> content_pres
499 newpath 644 712 moveto
500 644 704 643 695 643 686 curveto
505 0.000 0.000 0.000 edgecolor
506 newpath 647 686 moveto
511 0.000 0.000 0.000 edgecolor
512 newpath 647 686 moveto
519 % cic_unification -> cic_proof_checking
520 newpath 367 537 moveto
521 380 513 400 476 423 448 curveto
522 431 438 441 427 450 418 curveto
527 0.000 0.000 0.000 edgecolor
528 newpath 453 420 moveto
533 0.000 0.000 0.000 edgecolor
534 newpath 453 420 moveto
543 165 650 45 25 ellipse_path
548 [6.72 10.56 10.56 6.72 6.72 10.56 9.36]
553 % tactics -> cic_unification
554 newpath 201 633 moveto
555 228 620 267 603 299 588 curveto
560 0.000 0.000 0.000 edgecolor
561 newpath 300 591 moveto
566 0.000 0.000 0.000 edgecolor
567 newpath 300 591 moveto
575 newpath 176 625 moveto
576 181 616 185 606 190 596 curveto
581 0.000 0.000 0.000 edgecolor
582 newpath 193 598 moveto
587 0.000 0.000 0.000 edgecolor
588 newpath 193 598 moveto
597 132 738 90 25 ellipse_path
602 [12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12]
607 % paramodulation -> tactics
608 newpath 142 713 moveto
609 145 704 149 694 152 684 curveto
614 0.000 0.000 0.000 edgecolor
615 newpath 155 686 moveto
620 0.000 0.000 0.000 edgecolor
621 newpath 155 686 moveto
630 427 298 28 25 ellipse_path
642 347 210 70 25 ellipse_path
647 [12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92]
653 newpath 409 278 moveto
654 399 267 387 254 376 241 curveto
659 0.000 0.000 0.000 edgecolor
660 newpath 379 239 moveto
665 0.000 0.000 0.000 edgecolor
666 newpath 379 239 moveto
675 205 122 33 25 ellipse_path
686 newpath 435 273 moveto
687 441 248 446 209 427 184 curveto
688 405 156 307 137 249 128 curveto
693 0.000 0.000 0.000 edgecolor
694 newpath 249 125 moveto
699 0.000 0.000 0.000 edgecolor
700 newpath 249 125 moveto
707 % cic_proof_checking -> cic
708 newpath 470 361 moveto
709 463 351 455 339 448 328 curveto
714 0.000 0.000 0.000 edgecolor
715 newpath 451 326 moveto
720 0.000 0.000 0.000 edgecolor
721 newpath 451 326 moveto
730 318 298 42 25 ellipse_path
735 [12 10.56 6.72 6.72 10.56 7.92]
740 % cic_proof_checking -> getter
741 newpath 442 363 moveto
742 416 350 384 333 359 320 curveto
747 0.000 0.000 0.000 edgecolor
748 newpath 360 317 moveto
753 0.000 0.000 0.000 edgecolor
754 newpath 360 317 moveto
761 % getter -> urimanager
762 newpath 326 273 moveto
763 329 264 332 254 336 245 curveto
768 0.000 0.000 0.000 edgecolor
769 newpath 339 246 moveto
774 0.000 0.000 0.000 edgecolor
775 newpath 339 246 moveto
784 205 210 52 25 ellipse_path
789 [7.92 10.56 12 6.72 9.36 6.72 7.92 12]
795 newpath 292 278 moveto
796 277 266 258 251 241 238 curveto
801 0.000 0.000 0.000 edgecolor
802 newpath 243 235 moveto
807 0.000 0.000 0.000 edgecolor
808 newpath 243 235 moveto
817 205 386 58 25 ellipse_path
822 [18.72 10.56 6.72 10.56 12 10.56 6.72 10.56]
828 newpath 249 369 moveto
829 257 366 265 363 273 360 curveto
830 316 343 327 341 370 324 curveto
831 377 321 384 318 391 314 curveto
836 0.000 0.000 0.000 edgecolor
837 newpath 393 317 moveto
842 0.000 0.000 0.000 edgecolor
843 newpath 393 317 moveto
851 newpath 234 364 moveto
852 249 352 268 337 283 324 curveto
857 0.000 0.000 0.000 edgecolor
858 newpath 285 327 moveto
863 0.000 0.000 0.000 edgecolor
864 newpath 285 327 moveto
873 205 298 50 25 ellipse_path
878 [12 18.72 12 9.36 12 6.72]
884 newpath 205 360 moveto
885 205 352 205 343 205 334 curveto
890 0.000 0.000 0.000 edgecolor
891 newpath 209 334 moveto
896 0.000 0.000 0.000 edgecolor
897 newpath 209 334 moveto
905 newpath 205 536 moveto
906 205 506 205 456 205 422 curveto
911 0.000 0.000 0.000 edgecolor
912 newpath 209 422 moveto
917 0.000 0.000 0.000 edgecolor
918 newpath 209 422 moveto
927 205 34 42 25 ellipse_path
932 [10.56 12 6.72 6.72 6.72 12]
939 79 210 54 25 ellipse_path
944 [12 12 12 12 18.72 10.56]
950 newpath 110 189 moveto
951 128 176 152 159 172 146 curveto
956 0.000 0.000 0.000 edgecolor
957 newpath 174 149 moveto
962 0.000 0.000 0.000 edgecolor
963 newpath 174 149 moveto
971 newpath 205 272 moveto
972 205 264 205 255 205 246 curveto
977 0.000 0.000 0.000 edgecolor
978 newpath 209 246 moveto
983 0.000 0.000 0.000 edgecolor
984 newpath 209 246 moveto
992 newpath 205 184 moveto
993 205 176 205 167 205 158 curveto
998 0.000 0.000 0.000 edgecolor
999 newpath 209 158 moveto
1004 0.000 0.000 0.000 edgecolor
1005 newpath 209 158 moveto
1013 newpath 205 96 moveto
1014 205 88 205 79 205 70 curveto
1019 0.000 0.000 0.000 edgecolor
1020 newpath 209 70 moveto
1025 0.000 0.000 0.000 edgecolor
1026 newpath 209 70 moveto
1036 0.584 0.220 0.933 nodecolor
1037 0.584 0.220 0.933 nodecolor
1038 newpath 128 404 moveto
1044 0.584 0.220 0.933 nodecolor
1045 newpath 128 404 moveto
1052 0.000 0.000 0.000 nodecolor
1055 [17.28 7.92 10.56 17.28 17.28 7.92 10.56 12 12]
1060 % DrawGraph -> getter
1061 newpath 113 368 moveto
1062 121 365 129 362 137 360 curveto
1063 193 342 209 345 265 324 curveto
1064 269 322 272 321 276 319 curveto
1069 0.000 0.000 0.000 edgecolor
1070 newpath 277 322 moveto
1075 0.000 0.000 0.000 edgecolor
1076 newpath 277 322 moveto
1086 0.584 0.220 0.933 nodecolor
1087 0.584 0.220 0.933 nodecolor
1088 newpath 358 404 moveto
1094 0.584 0.220 0.933 nodecolor
1095 newpath 358 404 moveto
1102 0.000 0.000 0.000 nodecolor
1105 [17.28 10.56 6.72 6.72 10.56 7.92]
1111 newpath 320 368 moveto
1112 320 358 319 346 319 334 curveto
1117 0.000 0.000 0.000 edgecolor
1118 newpath 323 334 moveto
1123 0.000 0.000 0.000 edgecolor
1124 newpath 323 334 moveto
1134 0.584 0.220 0.933 nodecolor
1135 0.584 0.220 0.933 nodecolor
1136 newpath 319 756 moveto
1142 0.584 0.220 0.933 nodecolor
1143 newpath 319 756 moveto
1150 0.000 0.000 0.000 nodecolor
1153 [21.36 10.56 6.72 6.72 6.72 10.56]
1158 % Matita -> cic_disambiguation
1159 newpath 300 720 moveto
1160 313 709 328 695 342 682 curveto
1165 0.000 0.000 0.000 edgecolor
1166 newpath 345 684 moveto
1171 0.000 0.000 0.000 edgecolor
1172 newpath 345 684 moveto
1180 newpath 256 720 moveto
1181 240 708 219 691 200 677 curveto
1186 0.000 0.000 0.000 edgecolor
1187 newpath 202 674 moveto
1192 0.000 0.000 0.000 edgecolor
1193 newpath 202 674 moveto
1203 0.584 0.220 0.933 nodecolor
1204 0.584 0.220 0.933 nodecolor
1205 newpath 710 492 moveto
1211 0.584 0.220 0.933 nodecolor
1212 newpath 710 492 moveto
1219 0.000 0.000 0.000 nodecolor
1222 [13.44 7.92 12 12 7.92 16.08 12 10.56 10.56 12 10.56 7.92]
1227 % ProofChecker -> cic_proof_checking
1228 newpath 605 456 moveto
1229 585 445 559 428 536 415 curveto
1234 0.000 0.000 0.000 edgecolor
1235 newpath 537 412 moveto
1240 0.000 0.000 0.000 edgecolor
1241 newpath 537 412 moveto
1251 0.584 0.220 0.933 nodecolor
1252 0.584 0.220 0.933 nodecolor
1253 newpath 579 756 moveto
1259 0.584 0.220 0.933 nodecolor
1260 newpath 579 756 moveto
1267 0.000 0.000 0.000 nodecolor
1270 [17.28 17.28 12 12 12]
1275 % Uwobo -> acic_content
1276 newpath 536 720 moveto
1277 536 692 536 635 536 598 curveto
1282 0.000 0.000 0.000 edgecolor
1283 newpath 540 598 moveto
1288 0.000 0.000 0.000 edgecolor
1289 newpath 540 598 moveto
1296 % Uwobo -> content_pres
1297 newpath 558 720 moveto
1298 572 709 590 694 606 681 curveto
1303 0.000 0.000 0.000 edgecolor
1304 newpath 609 683 moveto
1309 0.000 0.000 0.000 edgecolor
1310 newpath 609 683 moveto
1320 0.584 0.220 0.933 nodecolor
1321 0.584 0.220 0.933 nodecolor
1322 newpath 417 756 moveto
1328 0.584 0.220 0.933 nodecolor
1329 newpath 417 756 moveto
1336 0.000 0.000 0.000 nodecolor
1339 [22.56 12 10.56 6.72 12]
1344 % Whelp -> cic_disambiguation
1345 newpath 377 720 moveto
1346 377 710 377 698 377 686 curveto
1351 0.000 0.000 0.000 edgecolor
1352 newpath 381 686 moveto
1357 0.000 0.000 0.000 edgecolor
1358 newpath 381 686 moveto
1366 newpath 343 720 moveto
1367 338 717 333 714 328 712 curveto
1368 296 695 282 701 258 676 curveto
1369 237 653 223 621 214 597 curveto
1374 0.000 0.000 0.000 edgecolor
1375 newpath 217 596 moveto
1380 0.000 0.000 0.000 edgecolor
1381 newpath 217 596 moveto