proof-2-100.n3 10.5 KB
Newer Older
josd's avatar
josd committed
1
#Processed by EYE v18.0515.2100 josd
josd's avatar
josd committed
2
#eye --proof http://josd.github.io/eye/reasoning/djiti/proof-100.n3 --query http://josd.github.io/eye/reasoning/djiti/query.n3
josd's avatar
josd committed
3 4

PREFIX r: <http://www.w3.org/2000/10/swap/reason#>
josd's avatar
josd committed
5
PREFIX : <http://josd.github.io/eye/reasoning#>
josd's avatar
josd committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

[] a r:Proof, r:Conjunction;
  r:component <#lemma1>;
  r:component <#lemma2>;
  r:component <#lemma3>;
  r:component <#lemma4>;
  r:component <#lemma5>;
  r:component <#lemma6>;
  r:gives {
    :a :b (:i522 :i474 :i797 :i690 :i967).
    :a :b (:i831 :i976 :i797 :i690 :i967).
    :a :b (:i214 :i257 :i158 :i233 :i31).
    :a :b (:i745 :i214 :i277 :i911 :i35).
    :a :b (:i773 :i905 :i127 :i879 :i80).
    :a :b (:i123 :i646 :i533 :i556 :i435).
  }.

<#lemma1> a r:Inference;
  r:gives {
    :a :b (:i522 :i474 :i797 :i690 :i967).
  };
  r:evidence (
    <#lemma7>
    <#lemma8>
  );
  r:rule <#lemma9>.

<#lemma2> a r:Inference;
  r:gives {
    :a :b (:i831 :i976 :i797 :i690 :i967).
  };
  r:evidence (
    <#lemma10>
    <#lemma8>
  );
  r:rule <#lemma9>.

<#lemma3> a r:Inference;
  r:gives {
    :a :b (:i214 :i257 :i158 :i233 :i31).
  };
  r:evidence (
    <#lemma11>
    <#lemma12>
  );
  r:rule <#lemma9>.

<#lemma4> a r:Inference;
  r:gives {
    :a :b (:i745 :i214 :i277 :i911 :i35).
  };
  r:evidence (
    <#lemma13>
    <#lemma14>
  );
  r:rule <#lemma9>.

<#lemma5> a r:Inference;
  r:gives {
    :a :b (:i773 :i905 :i127 :i879 :i80).
  };
  r:evidence (
    <#lemma15>
    <#lemma16>
  );
  r:rule <#lemma9>.

<#lemma6> a r:Inference;
  r:gives {
    :a :b (:i123 :i646 :i533 :i556 :i435).
  };
  r:evidence (
    <#lemma17>
    <#lemma18>
  );
  r:rule <#lemma9>.

<#lemma7> a r:Inference;
  r:gives {
    (:i522 :i474 :i797) :p :o.
  };
  r:evidence (
    <#lemma19>
    <#lemma20>
    [ a r:Fact; r:gives {{(:i522 :i474 :i797) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i522 :i474 :i797) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma8> a r:Inference;
  r:gives {
    (:i797 :i690 :i967) :p :o.
  };
  r:evidence (
    <#lemma22>
    <#lemma23>
    [ a r:Fact; r:gives {{(:i797 :i690 :i967) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i797 :i690 :i967) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma9> a r:Extraction;
  r:gives {
    {(?x_0_1 ?x_1_1 ?x_2_1) :p :o.
     (?x_2_1 ?x_3_1 ?x_4_1) :p :o} => {:a :b (?x_0_1 ?x_1_1 ?x_2_1 ?x_3_1 ?x_4_1)}.
  };
josd's avatar
josd committed
110
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/query.n3>].
josd's avatar
josd committed
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212

<#lemma10> a r:Inference;
  r:gives {
    (:i831 :i976 :i797) :p :o.
  };
  r:evidence (
    <#lemma24>
    <#lemma25>
    [ a r:Fact; r:gives {{(:i831 :i976 :i797) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i831 :i976 :i797) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma11> a r:Inference;
  r:gives {
    (:i214 :i257 :i158) :p :o.
  };
  r:evidence (
    <#lemma26>
    <#lemma27>
    [ a r:Fact; r:gives {{(:i214 :i257 :i158) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i214 :i257 :i158) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma12> a r:Inference;
  r:gives {
    (:i158 :i233 :i31) :p :o.
  };
  r:evidence (
    <#lemma28>
    <#lemma29>
    [ a r:Fact; r:gives {{(:i158 :i233 :i31) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i158 :i233 :i31) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma13> a r:Inference;
  r:gives {
    (:i745 :i214 :i277) :p :o.
  };
  r:evidence (
    <#lemma30>
    <#lemma31>
    [ a r:Fact; r:gives {{(:i745 :i214 :i277) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i745 :i214 :i277) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma14> a r:Inference;
  r:gives {
    (:i277 :i911 :i35) :p :o.
  };
  r:evidence (
    <#lemma32>
    <#lemma33>
    [ a r:Fact; r:gives {{(:i277 :i911 :i35) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i277 :i911 :i35) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma15> a r:Inference;
  r:gives {
    (:i773 :i905 :i127) :p :o.
  };
  r:evidence (
    <#lemma34>
    <#lemma35>
    [ a r:Fact; r:gives {{(:i773 :i905 :i127) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i773 :i905 :i127) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma16> a r:Inference;
  r:gives {
    (:i127 :i879 :i80) :p :o.
  };
  r:evidence (
    <#lemma36>
    <#lemma37>
    [ a r:Fact; r:gives {{(:i127 :i879 :i80) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i127 :i879 :i80) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma17> a r:Inference;
  r:gives {
    (:i123 :i646 :i533) :p :o.
  };
  r:evidence (
    <#lemma38>
    <#lemma39>
    [ a r:Fact; r:gives {{(:i123 :i646 :i533) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i123 :i646 :i533) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma18> a r:Inference;
  r:gives {
    (:i533 :i556 :i435) :p :o.
  };
  r:evidence (
    <#lemma40>
    <#lemma41>
    [ a r:Fact; r:gives {{(:i533 :i556 :i435) :p :o} <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {(:i533 :i556 :i435) :p :o}}]
  );
  r:rule <#lemma21>.

<#lemma19> a r:Extraction;
  r:gives {
josd's avatar
josd committed
213
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma7> a r:Extraction.
josd's avatar
josd committed
214
  };
josd's avatar
josd committed
215
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
216 217 218

<#lemma20> a r:Extraction;
  r:gives {
josd's avatar
josd committed
219
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma7> r:gives {(:i522 :i474 :i797) :p :o}.
josd's avatar
josd committed
220
  };
josd's avatar
josd committed
221
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
222 223 224 225 226 227 228 229 230 231 232

<#lemma21> a r:Extraction;
  r:gives {
    {?x_0_2 a r:Extraction.
     ?x_0_2 r:gives ?x_1_2.
     ?x_1_2 <http://eulersharp.sourceforge.net/2003/03swap/log-rules#graphMember> {?x_3_2 ?x_2_2 ?x_4_2}} => {?x_3_2 ?x_2_2 ?x_4_2}.
  };
  r:because [ a r:Parsing; r:source <http://eulersharp.sourceforge.net/2003/03swap/proof-lemma>].

<#lemma22> a r:Extraction;
  r:gives {
josd's avatar
josd committed
233
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma8> a r:Extraction.
josd's avatar
josd committed
234
  };
josd's avatar
josd committed
235
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
236 237 238

<#lemma23> a r:Extraction;
  r:gives {
josd's avatar
josd committed
239
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma8> r:gives {(:i797 :i690 :i967) :p :o}.
josd's avatar
josd committed
240
  };
josd's avatar
josd committed
241
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
242 243 244

<#lemma24> a r:Extraction;
  r:gives {
josd's avatar
josd committed
245
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma10> a r:Extraction.
josd's avatar
josd committed
246
  };
josd's avatar
josd committed
247
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
248 249 250

<#lemma25> a r:Extraction;
  r:gives {
josd's avatar
josd committed
251
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma10> r:gives {(:i831 :i976 :i797) :p :o}.
josd's avatar
josd committed
252
  };
josd's avatar
josd committed
253
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
254 255 256

<#lemma26> a r:Extraction;
  r:gives {
josd's avatar
josd committed
257
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma11> a r:Extraction.
josd's avatar
josd committed
258
  };
josd's avatar
josd committed
259
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
260 261 262

<#lemma27> a r:Extraction;
  r:gives {
josd's avatar
josd committed
263
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma11> r:gives {(:i214 :i257 :i158) :p :o}.
josd's avatar
josd committed
264
  };
josd's avatar
josd committed
265
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
266 267 268

<#lemma28> a r:Extraction;
  r:gives {
josd's avatar
josd committed
269
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma12> a r:Extraction.
josd's avatar
josd committed
270
  };
josd's avatar
josd committed
271
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
272 273 274

<#lemma29> a r:Extraction;
  r:gives {
josd's avatar
josd committed
275
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma12> r:gives {(:i158 :i233 :i31) :p :o}.
josd's avatar
josd committed
276
  };
josd's avatar
josd committed
277
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
278 279 280

<#lemma30> a r:Extraction;
  r:gives {
josd's avatar
josd committed
281
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma13> a r:Extraction.
josd's avatar
josd committed
282
  };
josd's avatar
josd committed
283
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
284 285 286

<#lemma31> a r:Extraction;
  r:gives {
josd's avatar
josd committed
287
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma13> r:gives {(:i745 :i214 :i277) :p :o}.
josd's avatar
josd committed
288
  };
josd's avatar
josd committed
289
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
290 291 292

<#lemma32> a r:Extraction;
  r:gives {
josd's avatar
josd committed
293
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma14> a r:Extraction.
josd's avatar
josd committed
294
  };
josd's avatar
josd committed
295
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
296 297 298

<#lemma33> a r:Extraction;
  r:gives {
josd's avatar
josd committed
299
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma14> r:gives {(:i277 :i911 :i35) :p :o}.
josd's avatar
josd committed
300
  };
josd's avatar
josd committed
301
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
302 303 304

<#lemma34> a r:Extraction;
  r:gives {
josd's avatar
josd committed
305
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma15> a r:Extraction.
josd's avatar
josd committed
306
  };
josd's avatar
josd committed
307
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
308 309 310

<#lemma35> a r:Extraction;
  r:gives {
josd's avatar
josd committed
311
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma15> r:gives {(:i773 :i905 :i127) :p :o}.
josd's avatar
josd committed
312
  };
josd's avatar
josd committed
313
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
314 315 316

<#lemma36> a r:Extraction;
  r:gives {
josd's avatar
josd committed
317
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma16> a r:Extraction.
josd's avatar
josd committed
318
  };
josd's avatar
josd committed
319
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
320 321 322

<#lemma37> a r:Extraction;
  r:gives {
josd's avatar
josd committed
323
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma16> r:gives {(:i127 :i879 :i80) :p :o}.
josd's avatar
josd committed
324
  };
josd's avatar
josd committed
325
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
326 327 328

<#lemma38> a r:Extraction;
  r:gives {
josd's avatar
josd committed
329
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma17> a r:Extraction.
josd's avatar
josd committed
330
  };
josd's avatar
josd committed
331
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
332 333 334

<#lemma39> a r:Extraction;
  r:gives {
josd's avatar
josd committed
335
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma17> r:gives {(:i123 :i646 :i533) :p :o}.
josd's avatar
josd committed
336
  };
josd's avatar
josd committed
337
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
338 339 340

<#lemma40> a r:Extraction;
  r:gives {
josd's avatar
josd committed
341
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma18> a r:Extraction.
josd's avatar
josd committed
342
  };
josd's avatar
josd committed
343
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
344 345 346

<#lemma41> a r:Extraction;
  r:gives {
josd's avatar
josd committed
347
    <http://josd.github.io/eye/reasoning/djiti/proof-100.n3#lemma18> r:gives {(:i533 :i556 :i435) :p :o}.
josd's avatar
josd committed
348
  };
josd's avatar
josd committed
349
  r:because [ a r:Parsing; r:source <http://josd.github.io/eye/reasoning/djiti/proof-100.n3>].
josd's avatar
josd committed
350

josd's avatar
josd committed
351
#2018-09-01T23:14:42.317Z in=124 out=6 ent=23 step=48 brake=2 inf=70154 sec=0.054 inf/sec=1299148
josd's avatar
josd committed
352 353
#ENDS