1
2
3
4
5
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
110
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
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
|
fof(axTransportationLem0, axiom,
( ! [Var_LENGTH] :
((hasType(type_LengthMeasure, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_totalLengthOfRailwaySystem(Var_AREA,Var_LENGTH)) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_Railway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA))))))))))))).
fof(axTransportationLem1, axiom,
( ! [Var_LENGTH] :
((hasType(type_LengthMeasure, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfElectrifiedRailway(Var_AREA,Var_LENGTH)) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_ElectrifiedRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA))))))))))))).
fof(axTransportationLem2, axiom,
( ! [Var_LENGTH] :
((hasType(type_LengthMeasure, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfMultipleTrackRailway(Var_AREA,Var_LENGTH)) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_MultipleTrackRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA))))))))))))).
fof(axTransportationLem3, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfBroadGaugeRailway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_BroadGaugeRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem4, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfDualGaugeRailway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_DualGaugeRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem5, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfNarrowGaugeRailway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_NarrowGaugeRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem6, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfStandardGaugeRailway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_StandardGaugeRailway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem7, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfUnclassifiedGaugeRailway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_RAILWAY] :
(hasType(type_Railway, Var_RAILWAY) &
(f_located(Var_RAILWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem8, axiom,
( ! [Var_RAIL] :
(hasType(type_MultipleTrackRailway, Var_RAIL) =>
(( ? [Var_TRACK1] :
(hasType(type_RailroadTrack, Var_TRACK1) &
(( ? [Var_TRACK2] :
(hasType(type_RailroadTrack, Var_TRACK2) &
(((Var_TRACK1 != Var_TRACK2) & (((f_part(Var_TRACK1,Var_RAIL)) & (f_part(Var_TRACK2,Var_RAIL))))))))))))))).
fof(axTransportationLem9, axiom,
( ! [Var_RR] :
(hasType(type_Railway, Var_RR) =>
(( ! [Var_WIDTH] :
((hasType(type_LengthMeasure, Var_WIDTH) & hasType(type_Quantity, Var_WIDTH)) =>
(((((f_property(Var_RR,inst_BroadGauge)) & (f_trackWidth(Var_RR,Var_WIDTH)))) => (f_greaterThan(Var_WIDTH,f_MeasureFn(1.44,inst_Meter))))))))))).
fof(axTransportationLem10, axiom,
( ! [Var_RR] :
(hasType(type_Railway, Var_RR) =>
(( ! [Var_WIDTH] :
((hasType(type_LengthMeasure, Var_WIDTH) & hasType(type_Quantity, Var_WIDTH)) =>
(((((f_property(Var_RR,inst_StandardGauge)) & (f_trackWidth(Var_RR,Var_WIDTH)))) => (f_greaterThanOrEqualTo(Var_WIDTH,f_MeasureFn(1.435,inst_Meter))))))))))).
fof(axTransportationLem11, axiom,
( ! [Var_RR] :
(hasType(type_Railway, Var_RR) =>
(( ! [Var_WIDTH] :
((hasType(type_LengthMeasure, Var_WIDTH) & hasType(type_Quantity, Var_WIDTH)) =>
(((((f_property(Var_RR,inst_StandardGauge)) & (f_trackWidth(Var_RR,Var_WIDTH)))) => (f_lessThanOrEqualTo(Var_WIDTH,f_MeasureFn(1.44,inst_Meter))))))))))).
fof(axTransportationLem12, axiom,
( ! [Var_RR] :
(hasType(type_Railway, Var_RR) =>
(( ! [Var_WIDTH] :
((hasType(type_LengthMeasure, Var_WIDTH) & hasType(type_Quantity, Var_WIDTH)) =>
(((((f_property(Var_RR,inst_NarrowGauge)) & (f_trackWidth(Var_RR,Var_WIDTH)))) => (f_lessThanOrEqualTo(Var_WIDTH,f_MeasureFn(1.435,inst_Meter))))))))))).
fof(axTransportationLem13, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_totalLengthOfHighwaySystem(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_HIGHWAY] :
(hasType(type_Roadway, Var_HIGHWAY) &
(f_located(Var_HIGHWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem14, axiom,
( ! [Var_LENGTH2] :
((hasType(type_LengthMeasure, Var_LENGTH2) & hasType(type_Quantity, Var_LENGTH2)) =>
(( ! [Var_LENGTH1] :
((hasType(type_LengthMeasure, Var_LENGTH1) & hasType(type_Quantity, Var_LENGTH1)) =>
(( ! [Var_LENGTH] :
((hasType(type_LengthMeasure, Var_LENGTH) & hasType(type_Entity, Var_LENGTH)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_totalLengthOfHighwaySystem(Var_AREA,Var_LENGTH)) & (((f_lengthOfPavedHighway(Var_AREA,Var_LENGTH1)) & (f_lengthOfUnpavedHighway(Var_AREA,Var_LENGTH2)))))) => (Var_LENGTH = f_AdditionFn(Var_LENGTH1,Var_LENGTH2)))))))))))))))).
fof(axTransportationLem15, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH2] :
((hasType(type_RealNumber, Var_LENGTH2) & hasType(type_Quantity, Var_LENGTH2)) =>
(( ! [Var_LENGTH1] :
((hasType(type_RealNumber, Var_LENGTH1) & hasType(type_Quantity, Var_LENGTH1)) =>
(( ! [Var_LENGTH] :
(hasType(type_RealNumber, Var_LENGTH) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_totalLengthOfHighwaySystem(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (((f_lengthOfPavedHighway(Var_AREA,f_MeasureFn(Var_LENGTH1,Var_UNIT))) & (f_lengthOfUnpavedHighway(Var_AREA,f_MeasureFn(Var_LENGTH2,Var_UNIT))))))) => (f_totalLengthOfHighwaySystem(Var_AREA,f_MeasureFn(f_AdditionFn(Var_LENGTH1,Var_LENGTH2),Var_UNIT)))))))))))))))))))).
fof(axTransportationLem16, axiom,
( ! [Var_PAVED] :
((hasType(type_LengthMeasure, Var_PAVED) & hasType(type_Quantity, Var_PAVED)) =>
(( ! [Var_TOTAL] :
((hasType(type_LengthMeasure, Var_TOTAL) & hasType(type_Quantity, Var_TOTAL)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_totalLengthOfHighwaySystem(Var_AREA,Var_TOTAL)) & (f_lengthOfPavedHighway(Var_AREA,Var_PAVED)))) => (f_greaterThanOrEqualTo(Var_TOTAL,Var_PAVED))))))))))))).
fof(axTransportationLem17, axiom,
( ! [Var_UNPAVED] :
((hasType(type_LengthMeasure, Var_UNPAVED) & hasType(type_Quantity, Var_UNPAVED)) =>
(( ! [Var_TOTAL] :
((hasType(type_LengthMeasure, Var_TOTAL) & hasType(type_Quantity, Var_TOTAL)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_totalLengthOfHighwaySystem(Var_AREA,Var_TOTAL)) & (f_lengthOfUnpavedHighway(Var_AREA,Var_UNPAVED)))) => (f_greaterThanOrEqualTo(Var_TOTAL,Var_UNPAVED))))))))))))).
fof(axTransportationLem18, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfPavedHighway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_HIGHWAY] :
(hasType(type_SurfacedRoadway, Var_HIGHWAY) &
(f_located(Var_HIGHWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem19, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfExpresswaySystem(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_HIGHWAY] :
(hasType(type_Expressway, Var_HIGHWAY) &
(f_located(Var_HIGHWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem20, axiom,
( ! [Var_LENGTH2] :
((hasType(type_LengthMeasure, Var_LENGTH2) & hasType(type_Quantity, Var_LENGTH2)) =>
(( ! [Var_LENGTH1] :
((hasType(type_LengthMeasure, Var_LENGTH1) & hasType(type_Quantity, Var_LENGTH1)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_lengthOfExpresswaySystem(Var_AREA,Var_LENGTH1)) & (f_lengthOfPavedHighway(Var_AREA,Var_LENGTH2)))) => (f_greaterThanOrEqualTo(Var_LENGTH2,Var_LENGTH1))))))))))))).
fof(axTransportationLem21, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_lengthOfUnpavedHighway(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_HIGHWAY] :
(hasType(type_UnsurfacedRoadway, Var_HIGHWAY) &
(f_located(Var_HIGHWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem22, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_totalLengthOfWaterways(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_WATERWAY] :
(hasType(type_Waterway, Var_WATERWAY) &
(f_located(Var_WATERWAY,Var_AREA)))))))))))))))).
fof(axTransportationLem23, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_LENGTH] :
((hasType(type_RealNumber, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_totalPipelineInArea(Var_AREA,f_MeasureFn(Var_LENGTH,Var_UNIT))) & (f_greaterThan(Var_LENGTH,0)))) => (( ? [Var_PIPE] :
(hasType(type_Pipeline, Var_PIPE) &
(f_located(Var_PIPE,Var_AREA)))))))))))))))).
fof(axTransportationLem24, axiom,
( ! [Var_AMOUNT2] :
((hasType(type_LengthMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) =>
(( ! [Var_AMOUNT1] :
((hasType(type_LengthMeasure, Var_AMOUNT1) & hasType(type_Quantity, Var_AMOUNT1)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_lengthOfCrudeOilPipeline(Var_AREA,Var_AMOUNT1)) & (f_totalPipelineInArea(Var_AREA,Var_AMOUNT2)))) => (f_lessThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2))))))))))))).
fof(axTransportationLem25, axiom,
( ! [Var_AMOUNT2] :
((hasType(type_LengthMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) =>
(( ! [Var_AMOUNT1] :
((hasType(type_LengthMeasure, Var_AMOUNT1) & hasType(type_Quantity, Var_AMOUNT1)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_lengthOfNaturalGasPipeline(Var_AREA,Var_AMOUNT1)) & (f_totalPipelineInArea(Var_AREA,Var_AMOUNT2)))) => (f_lessThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2))))))))))))).
fof(axTransportationLem26, axiom,
( ! [Var_AMOUNT2] :
((hasType(type_LengthMeasure, Var_AMOUNT2) & hasType(type_Quantity, Var_AMOUNT2)) =>
(( ! [Var_AMOUNT1] :
((hasType(type_LengthMeasure, Var_AMOUNT1) & hasType(type_Quantity, Var_AMOUNT1)) =>
(( ! [Var_AREA] :
(hasType(type_GeographicArea, Var_AREA) =>
(((((f_lengthOfPetroleumProductPipeline(Var_AREA,Var_AMOUNT1)) & (f_totalPipelineInArea(Var_AREA,Var_AMOUNT2)))) => (f_lessThanOrEqualTo(Var_AMOUNT1,Var_AMOUNT2))))))))))))).
fof(axTransportationLem27, axiom,
( ! [Var_CITY] :
(hasType(type_PortCity, Var_CITY) =>
(( ? [Var_HARBOR] :
(hasType(type_Harbor, Var_HARBOR) &
(f_geographicSubregion(Var_HARBOR,Var_CITY)))))))).
fof(axTransportationLem28, axiom,
( ! [Var_PORT] :
(hasType(type_RiverPort, Var_PORT) =>
(( ? [Var_RIVER] :
((hasType(type_River, Var_RIVER) & hasType(type_Waterway, Var_RIVER)) &
(f_meetsSpatially(Var_PORT,Var_RIVER)))))))).
fof(axTransportationLem29, axiom,
( ! [Var_OBJECT2] :
(hasType(type_Object, Var_OBJECT2) =>
(( ! [Var_OBJECT1] :
(hasType(type_Object, Var_OBJECT1) =>
(((f_meetsSpatially(Var_OBJECT1,Var_OBJECT2)) => (f_orientation(Var_OBJECT1,Var_OBJECT2,inst_Adjacent)))))))))).
fof(axTransportationLem30, axiom,
( ! [Var_PORT] :
(hasType(type_SeaPort, Var_PORT) =>
(( ? [Var_SEA] :
((hasType(type_Sea, Var_SEA) & hasType(type_Ocean, Var_SEA)) &
(((f_orientation(Var_PORT,Var_SEA,inst_Adjacent)) | (f_orientation(Var_PORT,Var_SEA,inst_Near)))))))))).
fof(axTransportationLem31, axiom,
( ! [Var_PORT] :
(hasType(type_DeepDraftPort, Var_PORT) =>
(( ? [Var_HARBOR] :
(hasType(type_DeepDraftHarbor, Var_HARBOR) &
(f_geographicSubregion(Var_HARBOR,Var_PORT)))))))).
fof(axTransportationLem32, axiom,
( ! [Var_HARBOR] :
(hasType(type_DeepDraftHarbor, Var_HARBOR) =>
(f_navigableForDraft(Var_HARBOR,f_MeasureFn(13.7,inst_Meter)))))).
fof(axTransportationLem33, axiom,
( ! [Var_HARBOR] :
(hasType(type_DeepDraftHarbor, Var_HARBOR) =>
(f_navigableForDraft(Var_HARBOR,f_MeasureFn(45,inst_FootLength)))))).
fof(axTransportationLem34, axiom,
( ! [Var_ANCHOR] :
(hasType(type_OffshoreAnchorage, Var_ANCHOR) =>
(( ? [Var_HARBOR] :
(hasType(type_Harbor, Var_HARBOR) &
(f_located(Var_ANCHOR,Var_HARBOR)))))))).
fof(axTransportationLem35, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfMass, Var_UNIT) =>
(( ! [Var_NUMBER] :
(hasType(type_RealNumber, Var_NUMBER) =>
(( ! [Var_FLEET] :
(hasType(type_Collection, Var_FLEET) =>
(((f_fleetGrossRegisteredTonnage(Var_FLEET,f_MeasureFn(Var_NUMBER,Var_UNIT))) => (Var_UNIT = inst_RegistryTon)))))))))))).
fof(axTransportationLem36, axiom,
( ! [Var_UNIT] :
(hasType(type_UnitOfMass, Var_UNIT) =>
(( ! [Var_NUMBER] :
(hasType(type_RealNumber, Var_NUMBER) =>
(( ! [Var_FLEET] :
(hasType(type_Collection, Var_FLEET) =>
(((f_fleetDeadWeightTonnage(Var_FLEET,f_MeasureFn(Var_NUMBER,Var_UNIT))) => (Var_UNIT = inst_LongTon)))))))))))).
fof(axTransportationLem37, axiom,
( ! [Var_SHIP] :
(hasType(type_MerchantMarineShip, Var_SHIP) =>
(( ! [Var_GRT] :
((hasType(type_RealNumber, Var_GRT) & hasType(type_Quantity, Var_GRT)) =>
(((f_measure(Var_SHIP,f_MeasureFn(Var_GRT,inst_RegistryTon))) => (f_greaterThanOrEqualTo(Var_GRT,1000)))))))))).
fof(axTransportationLem38, axiom,
( ! [Var_SHIP] :
(hasType(type_PetroleumTankerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_PetroleumProduct))))).
fof(axTransportationLem39, axiom,
( ! [Var_SHIP] :
(hasType(type_ChemicalTankerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_ChemicalProduct))))).
fof(axTransportationLem40, axiom,
( ! [Var_SHIP] :
(hasType(type_LiquefiedGasTankerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_ChemicalProduct))))).
fof(axTransportationLem41, axiom,
( ! [Var_SHIP] :
(hasType(type_LiquefiedGasTankerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,f_ExtensionFn(inst_Liquid)))))).
fof(axTransportationLem42, axiom,
( ! [Var_SHIP] :
(hasType(type_CombinationBulk_OilCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Object))))).
fof(axTransportationLem43, axiom,
( ! [Var_SHIP] :
(hasType(type_CombinationBulk_OilCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Petroleum))))).
fof(axTransportationLem44, axiom,
( ! [Var_SHIP] :
(hasType(type_CombinationOre_OilCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Mineral))))).
fof(axTransportationLem45, axiom,
( ! [Var_SHIP] :
(hasType(type_CombinationOre_OilCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Petroleum))))).
fof(axTransportationLem46, axiom,
( ! [Var_SHIP] :
(hasType(type_GeneralCargoShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Product))))).
fof(axTransportationLem47, axiom,
( ! [Var_SHIP] :
(hasType(type_ContainerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_ShipContainer))))).
fof(axTransportationLem48, axiom,
( ! [Var_SHIP] :
(hasType(type_VehicleCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Vehicle))))).
fof(axTransportationLem49, axiom,
( ! [Var_SHIP] :
(hasType(type_RailcarCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_RollingStock))))).
fof(axTransportationLem50, axiom,
( ! [Var_SHIP] :
(hasType(type_LivestockCarrierShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Livestock))))).
fof(axTransportationLem51, axiom,
( ! [Var_SHIP] :
(hasType(type_PassengerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,type_Human))))).
fof(axTransportationLem52, axiom,
( ! [Var_SHIP] :
(hasType(type_SpecializedTankerShip, Var_SHIP) =>
(f_cargoType(Var_SHIP,f_ExtensionFn(inst_Fluid)))))).
fof(axTransportationLem53, axiom,
( ! [Var_REGISTRATION] :
(hasType(type_ShipRegistration, Var_REGISTRATION) =>
(( ! [Var_SHIP] :
(hasType(type_Ship, Var_SHIP) =>
(( ! [Var_AREA] :
(hasType(type_GeopoliticalArea, Var_AREA) =>
(((((f_possesses(Var_SHIP,Var_REGISTRATION)) & (f_flagState(Var_SHIP,Var_AREA)))) => (f_subsumesContentInstance(f_ShipRegisterFn(Var_AREA),Var_REGISTRATION))))))))))))).
fof(axTransportationLem54, axiom,
( ! [Var_SHIP] :
(hasType(type_Ship, Var_SHIP) =>
(( ! [Var_AREA] :
(hasType(type_GeopoliticalArea, Var_AREA) =>
(((f_member(Var_SHIP,f_MerchantMarineFn(Var_AREA))) => (( ? [Var_REGISTRATION] :
(hasType(type_ShipRegistration, Var_REGISTRATION) &
(((f_possesses(Var_SHIP,Var_REGISTRATION)) & (f_subsumesContentInstance(f_ShipRegisterFn(Var_AREA),Var_REGISTRATION))))))))))))))).
fof(axTransportationLem55, axiom,
( ! [Var_AREA] :
((hasType(type_GeopoliticalArea, Var_AREA) & hasType(type_Entity, Var_AREA)) =>
(( ! [Var_COUNT] :
(hasType(type_NonnegativeInteger, Var_COUNT) =>
(( ! [Var_HOME] :
((hasType(type_GeopoliticalArea, Var_HOME) & hasType(type_Entity, Var_HOME)) =>
(( ! [Var_MM] :
((hasType(type_MerchantMarine, Var_MM) & hasType(type_Entity, Var_MM)) =>
(((((f_fOCShipsByOrigin(Var_MM,Var_HOME,Var_COUNT)) & (Var_MM = f_MerchantMarineFn(Var_AREA)))) => (Var_HOME != Var_AREA))))))))))))))).
fof(axTransportationLem56, axiom,
( ! [Var_COUNT] :
(hasType(type_NonnegativeInteger, Var_COUNT) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((f_totalFacilityTypeInArea(Var_AREA,ExtensionFn(inst_AirportWithPavedRunway),Var_COUNT)) => (( ? [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) &
(( ? [Var_RUNWAY] :
(hasType(type_PavedRunway, Var_RUNWAY) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (f_located(Var_AIRPORT,Var_AREA)))))))))))))))))).
fof(axTransportationLem57, axiom,
( ! [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) =>
(( ? [Var_LENGTH] :
(hasType(type_LengthMeasure, Var_LENGTH) &
(f_length(Var_RUNWAY,Var_LENGTH)))))))).
fof(axTransportationLem58, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_AirportWithPavedRunway)) => (( ? [Var_RUNWAY] :
(hasType(type_PavedRunway, Var_RUNWAY) &
(f_part(Var_RUNWAY,Var_AIRPORT)))))))))).
fof(axTransportationLem59, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_AirportWithUnpavedRunway)) => (( ? [Var_RUNWAY] :
(hasType(type_UnpavedRunway, Var_RUNWAY) &
(f_part(Var_RUNWAY,Var_AIRPORT)))))))))).
fof(axTransportationLem60, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_VeryShortRunwayAirport)) => (( ? [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) &
(( ? [Var_LENGTH] :
((hasType(type_PhysicalQuantity, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (((f_length(Var_RUNWAY,Var_LENGTH)) & (f_lessThan(Var_LENGTH,f_MeasureFn(914,inst_Meter)))))))))))))))))).
fof(axTransportationLem61, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_ShortRunwayAirport)) => (( ? [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) &
(( ? [Var_LENGTH] :
((hasType(type_PhysicalQuantity, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (((f_length(Var_RUNWAY,Var_LENGTH)) & (((f_greaterThanOrEqualTo(Var_LENGTH,f_MeasureFn(914,inst_Meter))) | (f_lessThanOrEqualTo(Var_LENGTH,f_MeasureFn(1523,inst_Meter)))))))))))))))))))).
fof(axTransportationLem62, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_ShortRunwayAirport)) => (( ? [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) &
(( ? [Var_LENGTH] :
((hasType(type_PhysicalQuantity, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (((f_length(Var_RUNWAY,Var_LENGTH)) & (((f_greaterThanOrEqualTo(Var_LENGTH,f_MeasureFn(1524,inst_Meter))) | (f_lessThanOrEqualTo(Var_LENGTH,f_MeasureFn(2437,inst_Meter)))))))))))))))))))).
fof(axTransportationLem63, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_LongRunwayAirport)) => (( ? [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) &
(( ? [Var_LENGTH] :
((hasType(type_PhysicalQuantity, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (((f_length(Var_RUNWAY,Var_LENGTH)) & (((f_greaterThanOrEqualTo(Var_LENGTH,f_MeasureFn(2438,inst_Meter))) | (f_lessThanOrEqualTo(Var_LENGTH,f_MeasureFn(3047,inst_Meter)))))))))))))))))))).
fof(axTransportationLem64, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(((f_attribute(Var_AIRPORT,inst_VeryLongRunwayAirport)) => (( ? [Var_RUNWAY] :
(hasType(type_Runway, Var_RUNWAY) &
(( ? [Var_LENGTH] :
((hasType(type_PhysicalQuantity, Var_LENGTH) & hasType(type_Quantity, Var_LENGTH)) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (((f_length(Var_RUNWAY,Var_LENGTH)) & (f_greaterThan(Var_LENGTH,f_MeasureFn(3047,inst_Meter)))))))))))))))))).
fof(axTransportationLem65, axiom,
( ! [Var_COUNT] :
((hasType(type_NonnegativeInteger, Var_COUNT) & hasType(type_Quantity, Var_COUNT)) =>
(( ! [Var_AREA] :
((hasType(type_GeographicArea, Var_AREA) & hasType(type_Object, Var_AREA)) =>
(((((f_totalFacilityTypeInArea(Var_AREA,ExtensionFn(inst_AirportWithUnpavedRunway),Var_COUNT)) & (f_greaterThan(Var_COUNT,0)))) => (( ? [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) &
(( ? [Var_RUNWAY] :
(hasType(type_UnpavedRunway, Var_RUNWAY) &
(((f_part(Var_RUNWAY,Var_AIRPORT)) & (f_located(Var_AIRPORT,Var_AREA)))))))))))))))))).
fof(axTransportationLem66, axiom,
( ! [Var_HELO] :
(hasType(type_Heliport, Var_HELO) =>
(f_trafficableForTrafficType(Var_HELO,type_Helicopter))))).
fof(axTransportationLem67, axiom,
( ! [Var_T2] :
(hasType(type_TimeDuration, Var_T2) =>
(( ! [Var_L2] :
(hasType(type_LengthMeasure, Var_L2) =>
(( ! [Var_SLOWPROB] :
((hasType(type_Entity, Var_SLOWPROB) & hasType(type_Quantity, Var_SLOWPROB)) =>
(( ! [Var_T1] :
(hasType(type_TimeDuration, Var_T1) =>
(( ! [Var_L1] :
(hasType(type_LengthMeasure, Var_L1) =>
(( ! [Var_FASTPROB] :
((hasType(type_Entity, Var_FASTPROB) & hasType(type_Quantity, Var_FASTPROB)) =>
(( ! [Var_Q] :
(hasType(type_FunctionQuantity, Var_Q) =>
(( ! [Var_V] :
((hasType(type_Vehicle, Var_V) & hasType(type_Object, Var_V)) =>
(((((f_topSpeed(Var_V,Var_Q)) & (((Var_FASTPROB = f_ProbabilityFn(measure(Var_V,f_SpeedFn(Var_L1,Var_T1)))) & (((Var_SLOWPROB = f_ProbabilityFn(measure(Var_V,f_SpeedFn(Var_L2,Var_T2)))) & (f_greaterThan(f_SpeedFn(Var_L1,Var_T1),f_SpeedFn(Var_L2,Var_T2))))))))) => (f_greaterThan(Var_SLOWPROB,Var_FASTPROB)))))))))))))))))))))))))))).
fof(axTransportationLem68, axiom,
( ! [Var_TRAIN] :
(hasType(type_Train, Var_TRAIN) =>
(( ? [Var_X] :
(hasType(type_RollingStock, Var_X) &
(( ? [Var_Y] :
(hasType(type_RollingStock, Var_Y) &
(Var_X != Var_Y)))))))))).
fof(axTransportationLem69, axiom,
( ! [Var_CRAFT] :
(hasType(type_WaterVehicle, Var_CRAFT) =>
(( ! [Var_EVENT] :
(hasType(type_Transportation, Var_EVENT) =>
(((f_instrument(Var_EVENT,Var_CRAFT)) => (( ? [Var_WATER] :
(hasType(type_WaterArea, Var_WATER) &
(f_located(Var_EVENT,Var_WATER))))))))))))).
fof(axTransportationLem70, axiom,
( ! [Var_NUMBER] :
((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) =>
(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_LongTon) = f_MeasureFn(f_MultiplicationFn(Var_NUMBER,2240),inst_PoundMass))))))).
fof(axTransportationLem71, axiom,
( ! [Var_QUANT] :
(hasType(type_Entity, Var_QUANT) =>
(( ! [Var_N3] :
((hasType(type_Quantity, Var_N3) & hasType(type_RealNumber, Var_N3)) =>
(( ! [Var_N2] :
((hasType(type_Quantity, Var_N2) & hasType(type_RealNumber, Var_N2)) =>
(( ! [Var_N1] :
((hasType(type_Quantity, Var_N1) & hasType(type_RealNumber, Var_N1)) =>
(( ! [Var_N4] :
((hasType(type_Entity, Var_N4) & hasType(type_RealNumber, Var_N4)) =>
(((((Var_N4 = f_MultiplicationFn(Var_N1,f_MultiplicationFn(Var_N2,Var_N3))) & (Var_QUANT = f_MultiplicationFn(f_MeasureFn(Var_N1,inst_FootLength),f_MultiplicationFn(f_MeasureFn(Var_N2,inst_FootLength),f_MeasureFn(Var_N3,inst_FootLength)))))) => (Var_QUANT = f_MeasureFn(Var_N4,inst_CubicFoot))))))))))))))))))).
fof(axTransportationLem72, axiom,
( ! [Var_NUMBER] :
((hasType(type_Entity, Var_NUMBER) & hasType(type_RealNumber, Var_NUMBER) & hasType(type_Quantity, Var_NUMBER)) =>
(((Var_NUMBER = f_MultiplicationFn(1,Var_NUMBER)) => (f_MeasureFn(Var_NUMBER,inst_RegistryTon) = f_MeasureFn(f_MultiplicationFn(Var_NUMBER,100),inst_CubicFoot))))))).
fof(axTransportationLem73, axiom,
( ! [Var_DECK] :
(hasType(type_ShipDeck, Var_DECK) =>
(( ? [Var_SHIP] :
(hasType(type_Ship, Var_SHIP) &
(f_properPart(Var_DECK,Var_SHIP)))))))).
fof(axTransportationLem74, axiom,
( ! [Var_AIRPORT] :
(hasType(type_Airport, Var_AIRPORT) =>
(f_trafficableForTrafficType(Var_AIRPORT,type_Airplane))))).
fof(axTransportationLem75, axiom,
( ! [Var_WATERWAY] :
(hasType(type_Waterway, Var_WATERWAY) =>
(( ! [Var_UNIT] :
(hasType(type_UnitOfLength, Var_UNIT) =>
(( ! [Var_DRAFT] :
((hasType(type_Quantity, Var_DRAFT) & hasType(type_RealNumber, Var_DRAFT)) =>
(( ! [Var_DEPTH] :
((hasType(type_RealNumber, Var_DEPTH) & hasType(type_Quantity, Var_DEPTH)) =>
(( ! [Var_OBJ] :
(hasType(type_Physical, Var_OBJ) =>
(((((f_depth(Var_OBJ,Var_WATERWAY,f_MeasureFn(Var_DEPTH,Var_UNIT))) & (f_lessThan(Var_DRAFT,Var_DEPTH)))) => (f_navigableForDraft(Var_WATERWAY,f_MeasureFn(Var_DRAFT,Var_UNIT)))))))))))))))))))).
fof(axTransportationLem76, axiom,
( ! [Var_SYSTEM] :
(hasType(type_TransitSystem, Var_SYSTEM) =>
(( ? [Var_ROUTE] :
(hasType(type_Transitway, Var_ROUTE) &
(f_part(Var_ROUTE,Var_SYSTEM)))))))).
fof(axTransportationLem77, axiom,
( ! [Var_TS] :
(hasType(type_TransitSystem, Var_TS) =>
(( ? [Var_G] :
(hasType(type_Graph, Var_G) &
(f_abstractCounterpart(Var_G,Var_TS)))))))).
fof(axTransportationLem78, axiom,
( ! [Var_TS] :
(hasType(type_TransitSystem, Var_TS) =>
(( ! [Var_T] :
(hasType(type_Transitway, Var_T) =>
(( ! [Var_G] :
((hasType(type_Abstract, Var_G) & hasType(type_Graph, Var_G)) =>
(((((f_abstractCounterpart(Var_G,Var_TS)) & (f_systemPart(Var_T,Var_TS)))) => (( ? [Var_GA] :
(hasType(type_GraphArc, Var_GA) &
(((f_abstractCounterpart(Var_GA,Var_T)) & (f_graphPart(Var_GA,Var_G)))))))))))))))))).
fof(axTransportationLem79, axiom,
( ! [Var_TS] :
(hasType(type_TransitSystem, Var_TS) =>
(( ! [Var_TJ] :
(hasType(type_TransitwayJunction, Var_TJ) =>
(( ! [Var_G] :
((hasType(type_Abstract, Var_G) & hasType(type_Graph, Var_G)) =>
(((((f_abstractCounterpart(Var_G,Var_TS)) & (f_systemPart(Var_TJ,Var_TS)))) => (( ? [Var_GN] :
(hasType(type_GraphNode, Var_GN) &
(((f_abstractCounterpart(Var_GN,Var_TJ)) & (f_graphPart(Var_GN,Var_G)))))))))))))))))).
fof(axTransportationLem80, axiom,
( ! [Var_ARC] :
((hasType(type_Abstract, Var_ARC) & hasType(type_GraphArc, Var_ARC)) =>
(( ! [Var_N2] :
((hasType(type_Abstract, Var_N2) & hasType(type_GraphNode, Var_N2)) =>
(( ! [Var_N1] :
((hasType(type_Abstract, Var_N1) & hasType(type_GraphNode, Var_N1)) =>
(( ! [Var_NODE2] :
((hasType(type_SelfConnectedObject, Var_NODE2) & hasType(type_Physical, Var_NODE2)) =>
(( ! [Var_NODE1] :
((hasType(type_SelfConnectedObject, Var_NODE1) & hasType(type_Physical, Var_NODE1)) =>
(( ! [Var_A] :
((hasType(type_SelfConnectedObject, Var_A) & hasType(type_Physical, Var_A)) =>
(((((f_connects(Var_A,Var_NODE1,Var_NODE2)) & (((f_abstractCounterpart(Var_N1,Var_NODE1)) & (((f_abstractCounterpart(Var_N2,Var_NODE2)) & (f_abstractCounterpart(Var_ARC,Var_A)))))))) => (f_links(Var_N1,Var_N2,Var_ARC)))))))))))))))))))))).
fof(axTransportationLem81, axiom,
( ! [Var_PATH] :
((hasType(type_Transitway, Var_PATH) & hasType(type_Physical, Var_PATH)) =>
(( ! [Var_DIST] :
(hasType(type_ConstantQuantity, Var_DIST) =>
(((f_distanceOnPath(Var_DIST,Var_PATH)) => (( ? [Var_GP] :
(hasType(type_GraphPath, Var_GP) &
(f_abstractCounterpart(Var_GP,Var_PATH))))))))))))).
fof(axTransportationLem82, axiom,
( ! [Var_GRAPH] :
((hasType(type_Abstract, Var_GRAPH) & hasType(type_Graph, Var_GRAPH) & hasType(type_GraphPath, Var_GRAPH)) =>
(( ! [Var_END] :
(hasType(type_Region, Var_END) =>
(( ! [Var_START] :
((hasType(type_Region, Var_START) & hasType(type_Physical, Var_START)) =>
(( ! [Var_SYS] :
((hasType(type_TransitSystem, Var_SYS) & hasType(type_Physical, Var_SYS)) =>
(( ! [Var_PATH] :
((hasType(type_Transitway, Var_PATH) & hasType(type_TransitSystem, Var_PATH)) =>
(( ! [Var_DIST] :
(hasType(type_ConstantQuantity, Var_DIST) =>
(((((f_distanceOnPath(Var_DIST,Var_PATH)) & (((f_pathInSystem(Var_PATH,Var_SYS)) & (((f_routeStart(Var_START,Var_PATH)) & (((f_routeEnd(Var_END,Var_PATH)) & (f_abstractCounterpart(Var_GRAPH,Var_SYS)))))))))) => (( ? [Var_EN] :
((hasType(type_Entity, Var_EN) & hasType(type_Abstract, Var_EN)) &
(( ? [Var_BN] :
((hasType(type_Entity, Var_BN) & hasType(type_Abstract, Var_BN)) &
(( ? [Var_S] :
(hasType(type_Graph, Var_S) &
(((f_subGraph(Var_S,Var_GRAPH)) & (((Var_BN = f_BeginNodeFn(Var_GRAPH)) & (((Var_EN = f_EndNodeFn(Var_GRAPH)) & (((f_abstractCounterpart(Var_BN,Var_START)) & (f_abstractCounterpart(Var_EN,Var_END))))))))))))))))))))))))))))))))))))))).
|
