c satplan version 1.0
c created: Thu Jul 24 14:17:32 PDT 1997
c operators: bw_orig.ops
c facts: medium.facts
c goal: 4
c wff: medium.cnf
c map: medium.map
c type: wff
p cnf 116 953
-4 -2 6 0
-4 -3 7 0
-8 -1 9 0
-8 -3 11 0
-4 -12 -5 0
-8 -14 -10 0
-12 17 0
-13 18 0
-14 19 0
-15 20 0
-1 -18 0
-2 -20 0
-4 -14 0
-4 -15 0
-4 -16 0
-8 -12 0
-8 -13 0
-8 -16 0
1 18 0
2 20 0
4 5 0
8 10 0
12 -17 0
14 -19 0
4 -6 0
4 -7 0
8 -9 0
8 -11 0
2 -6 0
3 -7 0
1 -9 0
3 -11 0
4 8 0
12 13 14 15 16 0
1 2 3 0
-4 -8 0
-8 -4 0
-12 -13 0
-12 -14 0
-12 -15 0
-12 -16 0
-13 -12 0
-13 -14 0
-13 -15 0
-13 -16 0
-14 -12 0
-14 -13 0
-14 -15 0
-14 -16 0
-15 -12 0
-15 -13 0
-15 -14 0
-15 -16 0
-16 -12 0
-16 -13 0
-16 -14 0
-16 -15 0
-1 -2 0
-1 -3 0
-2 -1 0
-2 -3 0
-3 -1 0
-3 -2 0
-4 -13 0
-8 -15 0
-4 -1 0
-8 -2 0
-13 -1 0
-15 -2 0
-16 -3 0
-26 -22 28 0
-26 -23 29 0
-26 -24 30 0
-26 -25 31 0
-32 -21 33 0
-32 -23 34 0
-32 -24 35 0
-32 -25 36 0
-37 -21 38 0
-37 -22 39 0
-37 -24 40 0
-37 -25 41 0
-42 -21 43 0
-42 -22 44 0
-42 -23 45 0
-42 -25 46 0
-26 -52 -27 0
-32 -47 -33 0
-32 -50 -35 0
-32 -51 -36 0
-37 -51 -41 0
-42 -48 -44 0
-42 -49 -45 0
-42 -51 -46 0
-52 53 0
-47 54 0
-48 55 0
-49 56 0
-50 57 0
-21 -54 0
-22 -55 0
-23 -56 0
-24 -57 0
-26 -48 0
-26 -49 0
-26 -50 0
-26 -51 0
-32 -52 0
-32 -47 5 0
-32 -49 0
-32 -50 6 0
-32 -51 7 0
-37 -52 0
-37 -47 0
-37 -48 0
-37 -50 0
-42 -52 0
-42 -47 0
-42 -48 9 0
-42 -49 10 0
-42 -51 11 0
-26 17 0
-32 18 0
-37 19 0
-42 20 0
-21 17 0
-22 18 0
-23 19 0
-24 20 0
21 -17 54 0
22 -18 55 0
23 -19 56 0
24 -20 57 0
26 27 0
32 -5 33 0
32 -6 35 0
32 -7 36 0
37 41 0
42 -9 44 0
42 -10 45 0
42 -11 46 0
52 -53 0
47 17 -54 0
48 18 -55 0
49 19 -56 0
50 20 -57 0
26 -28 0
26 -29 0
26 -30 0
26 -31 0
32 5 -33 0
32 -34 0
32 6 -35 0
32 7 -36 0
37 -38 0
37 -39 0
37 -40 0
42 -43 0
42 9 -44 0
42 10 -45 0
42 11 -46 0
22 -28 0
23 -29 0
24 -30 0
25 -31 0
21 5 -33 0
23 -34 0
24 6 -35 0
25 7 -36 0
21 -38 0
22 -39 0
24 -40 0
21 -43 0
22 9 -44 0
23 10 -45 0
25 11 -46 0
26 32 37 42 0
52 47 48 49 50 51 0
21 22 23 24 25 0
-26 -32 0
-26 -37 0
-26 -42 0
-32 -26 0
-32 -37 0
-32 -42 0
-37 -26 0
-37 -32 0
-37 -42 0
-42 -26 0
-42 -32 0
-42 -37 0
-52 -47 0
-52 -48 0
-52 -49 0
-52 -50 0
-52 -51 0
-47 -52 0
-47 -48 0
-47 -49 0
-47 -50 0
-47 -51 0
-48 -52 0
-48 -47 0
-48 -49 0
-48 -50 0
-48 -51 0
-49 -52 0
-49 -47 0
-49 -48 0
-49 -50 0
-49 -51 0
-50 -52 0
-50 -47 0
-50 -48 0
-50 -49 0
-50 -51 0
-51 -52 0
-51 -47 0
-51 -48 0
-51 -49 0
-51 -50 0
-21 -22 0
-21 -23 0
-21 -24 0
-21 -25 0
-22 -21 0
-22 -23 0
-22 -24 0
-22 -25 0
-23 -21 0
-23 -22 0
-23 -24 0
-23 -25 0
-24 -21 0
-24 -22 0
-24 -23 0
-24 -25 0
-25 -21 0
-25 -22 0
-25 -23 0
-25 -24 0
-26 -47 0
-32 -48 0
-37 -49 0
-42 -50 0
-26 -21 0
-32 -22 0
-37 -23 0
-42 -24 0
-47 -21 0
-48 -22 0
-49 -23 0
-50 -24 0
-51 -25 0
-58 -59 60 0
-58 -61 62 0
-58 -63 64 0
-58 -65 66 0
-58 -67 68 0
-69 -70 71 0
-69 -61 72 0
-69 -63 73 0
-69 -65 74 0
-69 -67 75 0
-76 -70 77 0
-76 -59 78 0
-76 -63 79 0
-76 -65 80 0
-76 -67 81 0
-82 -70 83 0
-82 -59 84 0
-82 -61 85 0
-82 -65 86 0
-82 -67 87 0
-88 -70 89 0
-88 -59 90 0
-88 -61 91 0
-88 -63 92 0
-88 -67 93 0
-58 -98 -68 0
-69 -99 -71 0
-69 -95 -72 0
-69 -96 -73 0
-69 -97 -74 0
-69 -98 -75 0
-76 -94 -78 0
-76 -96 -79 0
-76 -97 -80 0
-76 -98 -81 0
-82 -94 -84 0
-82 -95 -85 0
-82 -97 -86 0
-82 -98 -87 0
-88 -94 -90 0
-88 -95 -91 0
-88 -96 -92 0
-88 -98 -93 0
-99 100 0
-94 101 0
-95 102 0
-96 103 0
-97 104 0
-70 -100 0
-59 -101 0
-61 -102 0
-63 -103 0
-65 -104 0
-58 -94 0
-58 -95 0
-58 -96 0
-58 -97 0
-69 -99 27 0
-69 -95 28 0
-69 -96 29 0
-69 -97 30 0
-69 -98 31 0
-76 -99 0
-76 -94 33 0
-76 -96 34 0
-76 -97 35 0
-76 -98 36 0
-82 -99 0
-82 -94 38 0
-82 -95 39 0
-82 -97 40 0
-82 -98 41 0
-88 -99 0
-88 -94 43 0
-88 -95 44 0
-88 -96 45 0
-88 -98 46 0
-58 53 0
-69 54 0
-76 55 0
-82 56 0
-88 57 0
-70 53 0
-59 54 0
-61 55 0
-63 56 0
-65 57 0
70 -53 100 0
59 -54 101 0
61 -55 102 0
63 -56 103 0
65 -57 104 0
58 68 0
69 -27 71 0
69 -28 72 0
69 -29 73 0
69 -30 74 0
69 -31 75 0
76 -33 78 0
76 -34 79 0
76 -35 80 0
76 -36 81 0
82 -38 84 0
82 -39 85 0
82 -40 86 0
82 -41 87 0
88 -43 90 0
88 -44 91 0
88 -45 92 0
88 -46 93 0
99 53 -100 0
94 54 -101 0
95 55 -102 0
96 56 -103 0
97 57 -104 0
58 -60 0
58 -62 0
58 -64 0
58 -66 0
69 27 -71 0
69 28 -72 0
69 29 -73 0
69 30 -74 0
69 31 -75 0
76 -77 0
76 33 -78 0
76 34 -79 0
76 35 -80 0
76 36 -81 0
82 -83 0
82 38 -84 0
82 39 -85 0
82 40 -86 0
82 41 -87 0
88 -89 0
88 43 -90 0
88 44 -91 0
88 45 -92 0
88 46 -93 0
59 -60 0
61 -62 0
63 -64 0
65 -66 0
70 27 -71 0
61 28 -72 0
63 29 -73 0
65 30 -74 0
67 31 -75 0
70 -77 0
59 33 -78 0
63 34 -79 0
65 35 -80 0
67 36 -81 0
70 -83 0
59 38 -84 0
61 39 -85 0
65 40 -86 0
67 41 -87 0
70 -89 0
59 43 -90 0
61 44 -91 0
63 45 -92 0
67 46 -93 0
58 69 76 82 88 0
99 94 95 96 97 98 0
70 59 61 63 65 67 0
-58 -69 0
-58 -76 0
-58 -82 0
-58 -88 0
-69 -58 0
-69 -76 0
-69 -82 0
-69 -88 0
-76 -58 0
-76 -69 0
-76 -82 0
-76 -88 0
-82 -58 0
-82 -69 0
-82 -76 0
-82 -88 0
-88 -58 0
-88 -69 0
-88 -76 0
-88 -82 0
-99 -94 0
-99 -95 0
-99 -96 0
-99 -97 0
-99 -98 0
-94 -99 0
-94 -95 0
-94 -96 0
-94 -97 0
-94 -98 0
-95 -99 0
-95 -94 0
-95 -96 0
-95 -97 0
-95 -98 0
-96 -99 0
-96 -94 0
-96 -95 0
-96 -97 0
-96 -98 0
-97 -99 0
-97 -94 0
-97 -95 0
-97 -96 0
-97 -98 0
-98 -99 0
-98 -94 0
-98 -95 0
-98 -96 0
-98 -97 0
-70 -59 0
-70 -61 0
-70 -63 0
-70 -65 0
-70 -67 0
-59 -70 0
-59 -61 0
-59 -63 0
-59 -65 0
-59 -67 0
-61 -70 0
-61 -59 0
-61 -63 0
-61 -65 0
-61 -67 0
-63 -70 0
-63 -59 0
-63 -61 0
-63 -65 0
-63 -67 0
-65 -70 0
-65 -59 0
-65 -61 0
-65 -63 0
-65 -67 0
-67 -70 0
-67 -59 0
-67 -61 0
-67 -63 0
-67 -65 0
-58 -99 0
-69 -94 0
-76 -95 0
-82 -96 0
-88 -97 0
-58 -70 0
-69 -59 0
-76 -61 0
-82 -63 0
-88 -65 0
-99 -70 0
-94 -59 0
-95 -61 0
-96 -63 0
-97 -65 0
-98 -67 0
-105 -106 0
-105 -107 0
-109 -107 0
-110 -106 0
-111 -107 0
-111 -108 0
-112 -106 0
-112 -108 0
-105 -115 0
-109 -115 0
-110 -115 0
-105 -113 64 0
-105 -114 66 0
-109 -116 71 0
-109 -113 73 0
-109 -114 74 0
-110 -116 77 0
-110 -113 79 0
-110 -114 80 0
-111 -116 83 0
-111 -114 86 0
-111 -115 87 0
-112 -116 89 0
-112 -113 92 0
-112 -115 93 0
-105 100 0
-109 101 0
-110 102 0
-111 103 0
-112 104 0
-106 101 0
-107 102 0
106 -101 0
107 -102 0
105 -60 0
105 -62 0
105 -64 0
105 -66 0
109 -71 0
109 -72 0
109 -73 0
109 -74 0
110 -77 0
110 -78 0
110 -79 0
110 -80 0
111 -83 0
111 -85 0
111 -86 0
111 -87 0
112 -89 0
112 -90 0
112 -92 0
112 -93 0
116 100 0
113 103 0
114 104 0
105 68 0
109 75 0
110 81 0
111 84 0
112 91 0
108 68 0
108 75 0
108 81 0
106 84 0
107 91 0
105 109 110 111 112 0
116 113 114 115 0
106 107 108 0
-105 -109 0
-105 -110 0
-105 -111 0
-105 -112 0
-109 -105 0
-109 -110 0
-109 -111 0
-109 -112 0
-110 -105 0
-110 -109 0
-110 -111 0
-110 -112 0
-111 -105 0
-111 -109 0
-111 -110 0
-111 -112 0
-112 -105 0
-112 -109 0
-112 -110 0
-112 -111 0
-116 -113 0
-116 -114 0
-116 -115 0
-113 -116 0
-113 -114 0
-113 -115 0
-114 -116 0
-114 -113 0
-114 -115 0
-115 -116 0
-115 -113 0
-115 -114 0
-106 -107 0
-106 -108 0
-107 -106 0
-107 -108 0
-108 -106 0
-108 -107 0
-105 -116 0
-111 -113 0
-112 -114 0
-109 -106 0
-110 -107 0
-115 -108 0
-6 -9 0
-9 -6 0
-5 -6 0
-5 -7 0
-6 -5 0
-6 -7 0
-7 -5 0
-7 -6 0
-9 -10 0
-9 -11 0
-10 -9 0
-10 -11 0
-11 -9 0
-11 -10 0
-5 -17 0
-6 -20 0
-9 -18 0
-10 -19 0
-28 -33 0
-29 -38 0
-30 -43 0
-33 -28 0
-34 -39 0
-35 -44 0
-38 -29 0
-39 -34 0
-40 -45 0
-43 -30 0
-44 -35 0
-45 -40 0
-28 -39 0
-28 -44 0
-29 -34 0
-29 -45 0
-30 -35 0
-30 -40 0
-33 -38 0
-33 -43 0
-34 -29 0
-34 -45 0
-35 -30 0
-35 -40 0
-38 -33 0
-38 -43 0
-39 -28 0
-39 -44 0
-40 -30 0
-40 -35 0
-43 -33 0
-43 -38 0
-44 -28 0
-44 -39 0
-45 -29 0
-45 -34 0
-27 -28 0
-27 -29 0
-27 -30 0
-27 -31 0
-28 -27 0
-28 -29 0
-28 -30 0
-28 -31 0
-29 -27 0
-29 -28 0
-29 -30 0
-29 -31 0
-30 -27 0
-30 -28 0
-30 -29 0
-30 -31 0
-31 -27 0
-31 -28 0
-31 -29 0
-31 -30 0
-33 -34 0
-33 -35 0
-33 -36 0
-34 -33 0
-34 -35 0
-34 -36 0
-35 -33 0
-35 -34 0
-35 -36 0
-36 -33 0
-36 -34 0
-36 -35 0
-38 -39 0
-38 -40 0
-38 -41 0
-39 -38 0
-39 -40 0
-39 -41 0
-40 -38 0
-40 -39 0
-40 -41 0
-41 -38 0
-41 -39 0
-41 -40 0
-43 -44 0
-43 -45 0
-43 -46 0
-44 -43 0
-44 -45 0
-44 -46 0
-45 -43 0
-45 -44 0
-45 -46 0
-46 -43 0
-46 -44 0
-46 -45 0
-27 -53 0
-28 -55 0
-29 -56 0
-30 -57 0
-33 -54 0
-34 -56 0
-35 -57 0
-38 -54 0
-39 -55 0
-40 -57 0
-43 -54 0
-44 -55 0
-45 -56 0
-60 -71 0
-62 -77 0
-64 -83 0
-66 -89 0
-71 -60 0
-72 -78 0
-73 -84 0
-74 -90 0
-77 -62 0
-78 -72 0
-79 -85 0
-80 -91 0
-83 -64 0
-84 -73 0
-85 -79 0
-86 -92 0
-89 -66 0
-90 -74 0
-91 -80 0
-92 -86 0
-60 -78 0
-60 -84 0
-60 -90 0
-62 -72 0
-62 -85 0
-62 -91 0
-64 -73 0
-64 -79 0
-64 -92 0
-66 -74 0
-66 -80 0
-66 -86 0
-71 -77 0
-71 -83 0
-71 -89 0
-72 -62 0
-72 -85 0
-72 -91 0
-73 -64 0
-73 -79 0
-73 -92 0
-74 -66 0
-74 -80 0
-74 -86 0
-77 -71 0
-77 -83 0
-77 -89 0
-78 -60 0
-78 -84 0
-78 -90 0
-79 -64 0
-79 -73 0
-79 -92 0
-80 -66 0
-80 -74 0
-80 -86 0
-83 -71 0
-83 -77 0
-83 -89 0
-84 -60 0
-84 -78 0
-84 -90 0
-85 -62 0
-85 -72 0
-85 -91 0
-86 -66 0
-86 -74 0
-86 -80 0
-89 -71 0
-89 -77 0
-89 -83 0
-90 -60 0
-90 -78 0
-90 -84 0
-91 -62 0
-91 -72 0
-91 -85 0
-92 -64 0
-92 -73 0
-92 -79 0
-60 -62 0
-60 -64 0
-60 -66 0
-60 -68 0
-62 -60 0
-62 -64 0
-62 -66 0
-62 -68 0
-64 -60 0
-64 -62 0
-64 -66 0
-64 -68 0
-66 -60 0
-66 -62 0
-66 -64 0
-66 -68 0
-68 -60 0
-68 -62 0
-68 -64 0
-68 -66 0
-71 -72 0
-71 -73 0
-71 -74 0
-71 -75 0
-72 -71 0
-72 -73 0
-72 -74 0
-72 -75 0
-73 -71 0
-73 -72 0
-73 -74 0
-73 -75 0
-74 -71 0
-74 -72 0
-74 -73 0
-74 -75 0
-75 -71 0
-75 -72 0
-75 -73 0
-75 -74 0
-77 -78 0
-77 -79 0
-77 -80 0
-77 -81 0
-78 -77 0
-78 -79 0
-78 -80 0
-78 -81 0
-79 -77 0
-79 -78 0
-79 -80 0
-79 -81 0
-80 -77 0
-80 -78 0
-80 -79 0
-80 -81 0
-81 -77 0
-81 -78 0
-81 -79 0
-81 -80 0
-83 -84 0
-83 -85 0
-83 -86 0
-83 -87 0
-84 -83 0
-84 -85 0
-84 -86 0
-84 -87 0
-85 -83 0
-85 -84 0
-85 -86 0
-85 -87 0
-86 -83 0
-86 -84 0
-86 -85 0
-86 -87 0
-87 -83 0
-87 -84 0
-87 -85 0
-87 -86 0
-89 -90 0
-89 -91 0
-89 -92 0
-89 -93 0
-90 -89 0
-90 -91 0
-90 -92 0
-90 -93 0
-91 -89 0
-91 -90 0
-91 -92 0
-91 -93 0
-92 -89 0
-92 -90 0
-92 -91 0
-92 -93 0
-93 -89 0
-93 -90 0
-93 -91 0
-93 -92 0
-60 -101 0
-62 -102 0
-64 -103 0
-66 -104 0
-71 -100 0
-72 -102 0
-73 -103 0
-74 -104 0
-77 -100 0
-78 -101 0
-79 -103 0
-80 -104 0
-83 -100 0
-84 -101 0
-85 -102 0
-86 -104 0
-89 -100 0
-90 -101 0
-91 -102 0
-92 -103 0