1: ... [by parsing ] 2: :temporalBoundsSubsume s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 3: :temporallySubsumes s:subPropertyOf :temporalBoundsSubsume . [by erasure from step 1] 4: :DanC a . [by erasure from step 1] 5: :MonthFn s:range :CalendarMonth . [by erasure from step 1] 6: 5 :MonthOfYearFn :May . [by erasure from step 1] 7: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 8: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 9: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 10: @forAll :E, :WHEN, :YEARNUM, :YYYY . { ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum :YEARNUM . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g100 . :YEARNUM k:YearFn run:_g100 . } . [by erasure from step 1] 11: ... [by rule from step 10 applied to steps [7, 8, 9] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-08"', 'YEARNUM': '"2006...2006"', 'E': ''}] 12: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 13: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 14: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 15: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 16: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 17: @forAll :E, :MM, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g104, run:_g105 . ( :MM 0 ) math:sum run:_g105 . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g104 . run:_g104 k:YearFn :YEAR . run:_g105 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g106 . ( :MONTH_TYPE :YEAR ) k:MonthFn run:_g106 . } . [by erasure from step 1] 18: ... [by rule from step 17 applied to steps [6, 12, 13, 14, 15, 16] with bindings {'_g_L69C20': '"5...5"', 'MONTH_TYPE': '', 'E': '', '_g_L68C22': '"2006...2006"', 'MM': '"05...05"', 'WHEN': '"2006...5-08"', 'YYYY': '"2006...2006"', 'YEAR': '[...]'}] 19: @forSome :_g85, :_g93 . ( k:May :_g85 ) k:MonthFn :_g93 . [by erasure from step 18] 20: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 21: ... [by rule from step 20 applied to steps [5, 19] with bindings {'C': '', '_g_L135C3': '?', 'O': '[...]', '_g_L135C6': ''}] 22: @forSome :_g93 . :_g93 a k:CalendarMonth . [by erasure from step 21] 23: @forAll :WHEN, :WHO . { :WHEN a k:CalendarMonth . :WHO a . } log:implies { @forSome run:_g99 . run:_g99 a trav:PersonMonth . :WHEN k:temporallySubsumes run:_g99 . :WHO k:subAbstractions run:_g99 . } . [by erasure from step 1] 24: ... [by rule from step 23 applied to steps [4, 22] with bindings {'WHO': '', 'WHEN': '[...]'}] 25: @forSome :_g82, :_g93 . :_g93 k:temporallySubsumes :_g82 . [by erasure from step 24] 26: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 27: ... [by rule from step 26 applied to steps [3, 25] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 28: @forSome :_g82, :_g93 . :_g93 k:temporalBoundsSubsume :_g82 . [by erasure from step 27] 29: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 30: ... [by rule from step 29 applied to steps [2, 28] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 31: 5 :MonthOfYearFn :May . [by erasure from step 1] 32: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 33: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 34: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 35: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 36: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 37: @forSome :_g85, :_g93 . ( k:May :_g85 ) k:MonthFn :_g93 . [by erasure from step 18] 38: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 39: ... [by rule from step 38 applied to steps [31, 32, 33, 34, 35, 36, 37] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-08"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 40: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 41: 5 :MonthOfYearFn :May . [by erasure from step 1] 42: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 43: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 44: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 45: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 46: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 47: 5 :MonthOfYearFn :May . [by erasure from step 1] 48: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 49: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 50: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 51: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 52: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 53: @forAll :E, :MM, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g104, run:_g105 . ( :MM 0 ) math:sum run:_g105 . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g104 . run:_g104 k:YearFn :YEAR . run:_g105 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g106 . ( :MONTH_TYPE :YEAR ) k:MonthFn run:_g106 . } . [by erasure from step 1] 54: ... [by rule from step 53 applied to steps [47, 48, 49, 50, 51, 52] with bindings {'_g_L69C20': '"5...5"', 'MONTH_TYPE': '', 'E': '', '_g_L68C22': '"2006...2006"', 'MM': '"05...05"', 'WHEN': '"2006...5-15"', 'YYYY': '"2006...2006"', 'YEAR': '[...]'}] 55: @forSome :_g84, :_g85 . ( k:May :_g85 ) k:MonthFn :_g84 . [by erasure from step 54] 56: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 57: ... [by rule from step 56 applied to steps [41, 42, 43, 44, 45, 46, 55] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-15"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 58: @forSome :_g84 . trav:XTech k:startsDuring :_g84 . [by erasure from step 57] 59: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 60: ... [by rule from step 59 applied to steps [40, 58] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 61: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 62: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 63: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 64: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 65: @forAll :E, :WHEN, :YEARNUM, :YYYY . { ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum :YEARNUM . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g100 . :YEARNUM k:YearFn run:_g100 . } . [by erasure from step 1] 66: ... [by rule from step 65 applied to steps [62, 63, 64] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-15"', 'YEARNUM': '"2006...2006"', 'E': ''}] 67: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 68: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 69: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 70: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 71: @forAll :E, :WHEN, :YEAR, :YYYY . { @forSome run:_g103 . ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum run:_g103 . run:_g103 k:YearFn :YEAR . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :YEAR . } . [by erasure from step 1] 72: ... [by rule from step 71 applied to steps [67, 68, 69, 70] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-08"', 'E': '', '_g_L63C22': '"2006...2006"', 'YEAR': '[...]'}] 73: @forSome :_g92 . trav:WWW2007 k:startsDuring :_g92 . [by erasure from step 72] 74: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 75: ... [by rule from step 74 applied to steps [61, 73] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 76: :temporallySubsumes s:subPropertyOf :temporalBoundsSubsume . [by erasure from step 1] 77: :DanC a . [by erasure from step 1] 78: :MonthFn s:range :CalendarMonth . [by erasure from step 1] 79: 5 :MonthOfYearFn :May . [by erasure from step 1] 80: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 81: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 82: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 83: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 84: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 85: @forAll :E, :MM, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g104, run:_g105 . ( :MM 0 ) math:sum run:_g105 . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g104 . run:_g104 k:YearFn :YEAR . run:_g105 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g106 . ( :MONTH_TYPE :YEAR ) k:MonthFn run:_g106 . } . [by erasure from step 1] 86: ... [by rule from step 85 applied to steps [79, 80, 81, 82, 83, 84] with bindings {'_g_L69C20': '"5...5"', 'MONTH_TYPE': '', 'E': '', '_g_L68C22': '"2006...2006"', 'MM': '"05...05"', 'WHEN': '"2006...5-15"', 'YYYY': '"2006...2006"', 'YEAR': '[...]'}] 87: @forSome :_g92, :_g97 . ( k:May :_g92 ) k:MonthFn :_g97 . [by erasure from step 86] 88: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 89: ... [by rule from step 88 applied to steps [78, 87] with bindings {'C': '', '_g_L135C3': '?', 'O': '[...]', '_g_L135C6': ''}] 90: @forSome :_g97 . :_g97 a k:CalendarMonth . [by erasure from step 89] 91: @forAll :WHEN, :WHO . { :WHEN a k:CalendarMonth . :WHO a . } log:implies { @forSome run:_g99 . run:_g99 a trav:PersonMonth . :WHEN k:temporallySubsumes run:_g99 . :WHO k:subAbstractions run:_g99 . } . [by erasure from step 1] 92: ... [by rule from step 91 applied to steps [77, 90] with bindings {'WHO': '', 'WHEN': '[...]'}] 93: @forSome :_g96, :_g97 . :_g97 k:temporallySubsumes :_g96 . [by erasure from step 92] 94: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 95: ... [by rule from step 94 applied to steps [76, 93] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 96: @forSome :_g96, :_g97 . :_g97 k:temporalBoundsSubsume :_g96 . [by erasure from step 95] 97: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 98: 5 :MonthOfYearFn :May . [by erasure from step 1] 99: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 100: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 101: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 102: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 103: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 104: @forSome :_g92, :_g97 . ( k:May :_g92 ) k:MonthFn :_g97 . [by erasure from step 86] 105: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 106: ... [by rule from step 105 applied to steps [98, 99, 100, 101, 102, 103, 104] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-08"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 107: @forSome :_g97 . trav:WWW2007 k:startsDuring :_g97 . [by erasure from step 106] 108: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 109: ... [by rule from step 108 applied to steps [97, 107] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 110: @forSome :_g97 . trav:WWW2007 k:temporalBoundsIntersect :_g97 . [by erasure from step 109] 111: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 112: ... [by rule from step 111 applied to steps [96, 110] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 113: :temporalBoundsSubsume s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 114: :temporallySubsumes s:subPropertyOf :temporalBoundsSubsume . [by erasure from step 1] 115: :DanC a . [by erasure from step 1] 116: :MonthFn s:range :CalendarMonth . [by erasure from step 1] 117: @forSome :_g84, :_g85 . ( k:May :_g85 ) k:MonthFn :_g84 . [by erasure from step 54] 118: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 119: ... [by rule from step 118 applied to steps [116, 117] with bindings {'C': '', '_g_L135C3': '?', 'O': '[...]', '_g_L135C6': ''}] 120: @forSome :_g84 . :_g84 a k:CalendarMonth . [by erasure from step 119] 121: @forAll :WHEN, :WHO . { :WHEN a k:CalendarMonth . :WHO a . } log:implies { @forSome run:_g99 . run:_g99 a trav:PersonMonth . :WHEN k:temporallySubsumes run:_g99 . :WHO k:subAbstractions run:_g99 . } . [by erasure from step 1] 122: ... [by rule from step 121 applied to steps [115, 120] with bindings {'WHO': '', 'WHEN': '[...]'}] 123: @forSome :_g84, :_g94 . :_g84 k:temporallySubsumes :_g94 . [by erasure from step 122] 124: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 125: ... [by rule from step 124 applied to steps [114, 123] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 126: @forSome :_g84, :_g94 . :_g84 k:temporalBoundsSubsume :_g94 . [by erasure from step 125] 127: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 128: ... [by rule from step 127 applied to steps [113, 126] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 129: @forSome :_g81 . :_g81 owl:maxCardinality 1 . [by erasure from step 1] 130: @forSome :_g81 . :_g81 owl:onProperty trav:trip . [by erasure from step 1] 131: @forSome :_g81 . trav:RestrictedPersonMonth s:subClassOf :_g81 . [by erasure from step 1] 132: :DanC a :OneTripPerMonthAgent . [by erasure from step 1] 133: @forSome :_g82 . :_g82 a trav:PersonMonth . [by erasure from step 24] 134: @forSome :_g82 . trav:DanC k:subAbstractions :_g82 . [by erasure from step 24] 135: @forAll :WHO, :WHO_WHEN . { :WHO a trav:OneTripPerMonthAgent; k:subAbstractions :WHO_WHEN . :WHO_WHEN a trav:PersonMonth . } log:implies {:WHO_WHEN a trav:RestrictedPersonMonth . } . [by erasure from step 1] 136: ... [by rule from step 135 applied to steps [132, 133, 134] with bindings {'WHO': '', 'WHO_WHEN': '[...]'}] 137: @forSome :_g82 . :_g82 a trav:RestrictedPersonMonth . [by erasure from step 136] 138: @forAll :C, :S . { @forSome run:_g98 . run:_g98 s:subClassOf :C . :S a run:_g98 . } log:implies {:S a :C . } . [by erasure from step 1] 139: ... [by rule from step 138 applied to steps [131, 137] with bindings {'_g_L134C8': '', 'C': '[...]', 'S': '[...]'}] 140: @forSome :_g81, :_g82 . :_g82 a :_g81 . [by erasure from step 139] 141: :WWW2007 cal:attendee :DanC . [by erasure from step 1] 142: @forSome :_g82 . trav:DanC k:subAbstractions :_g82 . [by erasure from step 24] 143: @forSome :_g82, :_g93 . :_g93 k:temporalBoundsSubsume :_g82 . [by erasure from step 27] 144: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 145: @forSome :_g93 . trav:WWW2007 k:startsDuring :_g93 . [by erasure from step 39] 146: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 147: ... [by rule from step 146 applied to steps [144, 145] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 148: @forSome :_g93 . trav:WWW2007 k:temporalBoundsIntersect :_g93 . [by erasure from step 147] 149: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 150: ... [by rule from step 149 applied to steps [143, 148] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 151: @forSome :_g82 . trav:WWW2007 k:temporalBoundsIntersect :_g82 . [by erasure from step 150] 152: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 153: ... [by rule from step 152 applied to steps [141, 142, 151] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 154: @forSome :_g82 . :_g82 trav:trip trav:WWW2007 . [by erasure from step 153] 155: @forSome :_g82 . :_g82 trav:trip trav:WWW2007 . [by erasure from step 153] 156: @forAll :O1, :O2, :P, :S . { @forSome run:_g83 . run:_g83 owl:maxCardinality 1; owl:onProperty :P . :S a run:_g83; :P :O1, :O2 . } log:implies {:O1 = :O2 . } . [by erasure from step 1] 157: ... [by rule from step 156 applied to steps [129, 130, 140, 154, 155] with bindings {'P': '', 'S': '[...]', 'O1': '', '_g_L120C8': '[...]', 'O2': ''}] 158: :temporallyDisjoint s:subPropertyOf owl:differentFrom . [by erasure from step 1] 159: :WWW2007 cal:dtend "2006-05-12"^^dt:date . [by erasure from step 1] 160: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 161: "2006-05-12"^^:date str:lessThan "2006-05-15"^^:date . [by built-in Axiom str:lessThan] 162: @forAll one:E1, one:E2 . { @forSome :_g101, :_g102 . :_g101 str:lessThan :_g102 . one:E1 cal:dtend :_g101 . one:E2 cal:dtstart :_g102 . } log:implies {one:E1 k:temporallyDisjoint one:E2 . } . [by erasure from step 1] 163: ... [by rule from step 162 applied to steps [159, 160, 161] with bindings {'_g_L113C17': '"2006...5-12"', '_g_L113C32': '"2006...5-15"', 'E1': '', 'E2': ''}] 164: :WWW2007 k:temporallyDisjoint :XTech . [by erasure from step 163] 165: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 166: ... [by rule from step 165 applied to steps [158, 164] with bindings {'P': '', 'S': '', 'O': '', '_g_L136C6': ''}] 167: @forSome :_g81 . :_g81 owl:maxCardinality 1 . [by erasure from step 1] 168: @forSome :_g81 . :_g81 owl:onProperty trav:trip . [by erasure from step 1] 169: @forSome :_g81, :_g82 . :_g82 a :_g81 . [by erasure from step 139] 170: :XTech cal:attendee :DanC . [by erasure from step 1] 171: @forSome :_g82 . trav:DanC k:subAbstractions :_g82 . [by erasure from step 24] 172: @forSome :_g82, :_g93 . :_g93 k:temporalBoundsSubsume :_g82 . [by erasure from step 27] 173: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 174: 5 :MonthOfYearFn :May . [by erasure from step 1] 175: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 176: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 177: @forSome :_g85, :_g93 . ( k:May :_g85 ) k:MonthFn :_g93 . [by erasure from step 18] 178: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 179: ... [by rule from step 178 applied to steps [174, 175, 176, 44, 45, 46, 177] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-15"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 180: @forSome :_g93 . trav:XTech k:startsDuring :_g93 . [by erasure from step 179] 181: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 182: ... [by rule from step 181 applied to steps [173, 180] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 183: @forSome :_g93 . trav:XTech k:temporalBoundsIntersect :_g93 . [by erasure from step 182] 184: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 185: ... [by rule from step 184 applied to steps [172, 183] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 186: @forSome :_g82 . trav:XTech k:temporalBoundsIntersect :_g82 . [by erasure from step 185] 187: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 188: ... [by rule from step 187 applied to steps [170, 171, 186] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 189: @forSome :_g82 . :_g82 trav:trip trav:XTech . [by erasure from step 188] 190: @forSome :_g82 . :_g82 trav:trip trav:WWW2007 . [by erasure from step 153] 191: @forAll :O1, :O2, :P, :S . { @forSome run:_g83 . run:_g83 owl:maxCardinality 1; owl:onProperty :P . :S a run:_g83; :P :O1, :O2 . } log:implies {:O1 = :O2 . } . [by erasure from step 1] 192: ... [by rule from step 191 applied to steps [167, 168, 169, 189, 190] with bindings {'P': '', 'S': '[...]', 'O1': '', '_g_L120C8': '[...]', 'O2': ''}] 193: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 194: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 195: 5 :MonthOfYearFn :May . [by erasure from step 1] 196: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 197: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 198: @forSome :_g84, :_g85 . ( k:May :_g85 ) k:MonthFn :_g84 . [by erasure from step 54] 199: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 200: ... [by rule from step 199 applied to steps [195, 196, 197, 34, 35, 36, 198] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-08"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 201: @forSome :_g84 . trav:WWW2007 k:startsDuring :_g84 . [by erasure from step 200] 202: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 203: ... [by rule from step 202 applied to steps [194, 201] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 204: @forSome :_g84 . trav:WWW2007 k:temporalBoundsIntersect :_g84 . [by erasure from step 203] 205: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 206: ... [by rule from step 205 applied to steps [193, 204] with bindings {'P': '', 'S': '', 'O': '[...]'}] 207: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 208: @forSome :_g82 . trav:WWW2007 k:temporalBoundsIntersect :_g82 . [by erasure from step 150] 209: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 210: ... [by rule from step 209 applied to steps [207, 208] with bindings {'P': '', 'S': '', 'O': '[...]'}] 211: 5 :MonthOfYearFn :May . [by erasure from step 1] 212: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 213: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 214: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 215: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 216: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 217: @forSome :_g92, :_g97 . ( k:May :_g92 ) k:MonthFn :_g97 . [by erasure from step 86] 218: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 219: ... [by rule from step 218 applied to steps [211, 212, 213, 214, 215, 216, 217] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-15"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 220: :temporalBoundsSubsume s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 221: :temporallySubsumes s:subPropertyOf :temporalBoundsSubsume . [by erasure from step 1] 222: :DanC a . [by erasure from step 1] 223: :MonthFn s:range :CalendarMonth . [by erasure from step 1] 224: 5 :MonthOfYearFn :May . [by erasure from step 1] 225: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 226: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 227: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-(\\d\\d)-" ) :search ( "2006" "05" ) . [by built-in Axiom str:search] 228: ( "05" 0 ) :sum 5 . [by built-in Axiom math:sum] 229: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 230: @forAll :E, :MM, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g104, run:_g105 . ( :MM 0 ) math:sum run:_g105 . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g104 . run:_g104 k:YearFn :YEAR . run:_g105 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies { @forSome run:_g106 . ( :MONTH_TYPE :YEAR ) k:MonthFn run:_g106 . } . [by erasure from step 1] 231: ... [by rule from step 230 applied to steps [224, 225, 226, 227, 228, 229] with bindings {'_g_L69C20': '"5...5"', 'MONTH_TYPE': '', 'E': '', '_g_L68C22': '"2006...2006"', 'MM': '"05...05"', 'WHEN': '"2006...5-08"', 'YYYY': '"2006...2006"', 'YEAR': '[...]'}] 232: @forSome :_g90, :_g92 . ( k:May :_g92 ) k:MonthFn :_g90 . [by erasure from step 231] 233: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 234: ... [by rule from step 233 applied to steps [223, 232] with bindings {'C': '', '_g_L135C3': '?', 'O': '[...]', '_g_L135C6': ''}] 235: @forSome :_g90 . :_g90 a k:CalendarMonth . [by erasure from step 234] 236: @forAll :WHEN, :WHO . { :WHEN a k:CalendarMonth . :WHO a . } log:implies { @forSome run:_g99 . run:_g99 a trav:PersonMonth . :WHEN k:temporallySubsumes run:_g99 . :WHO k:subAbstractions run:_g99 . } . [by erasure from step 1] 237: ... [by rule from step 236 applied to steps [222, 235] with bindings {'WHO': '', 'WHEN': '[...]'}] 238: @forSome :_g88, :_g90 . :_g90 k:temporallySubsumes :_g88 . [by erasure from step 237] 239: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 240: ... [by rule from step 239 applied to steps [221, 238] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 241: @forSome :_g88, :_g90 . :_g90 k:temporalBoundsSubsume :_g88 . [by erasure from step 240] 242: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 243: ... [by rule from step 242 applied to steps [220, 241] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 244: :YearFn s:range :CalendarYear . [by erasure from step 1] 245: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 246: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 247: ... [by rule from step 246 applied to steps [244, 245] with bindings {'C': '', '_g_L135C3': '"2006...2006"', 'O': '[...]', '_g_L135C6': ''}] 248: :XTech cal:attendee :DanC . [by erasure from step 1] 249: @forSome :_g88 . trav:DanC k:subAbstractions :_g88 . [by erasure from step 237] 250: @forSome :_g88, :_g90 . :_g90 k:temporalBoundsSubsume :_g88 . [by erasure from step 240] 251: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 252: 5 :MonthOfYearFn :May . [by erasure from step 1] 253: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 254: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 255: @forSome :_g90, :_g92 . ( k:May :_g92 ) k:MonthFn :_g90 . [by erasure from step 231] 256: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 257: ... [by rule from step 256 applied to steps [252, 253, 254, 214, 215, 216, 255] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-15"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 258: @forSome :_g90 . trav:XTech k:startsDuring :_g90 . [by erasure from step 257] 259: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 260: ... [by rule from step 259 applied to steps [251, 258] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 261: @forSome :_g90 . trav:XTech k:temporalBoundsIntersect :_g90 . [by erasure from step 260] 262: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 263: ... [by rule from step 262 applied to steps [250, 261] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 264: @forSome :_g88 . trav:XTech k:temporalBoundsIntersect :_g88 . [by erasure from step 263] 265: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 266: ... [by rule from step 265 applied to steps [248, 249, 264] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 267: :MonthOfYearFn s:range :MonthOfYearType . [by erasure from step 1] 268: 5 :MonthOfYearFn :May . [by erasure from step 1] 269: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 270: ... [by rule from step 269 applied to steps [267, 268] with bindings {'C': '', '_g_L135C3': '"5...5"', 'O': '', '_g_L135C6': ''}] 271: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 272: @forSome :_g84 . trav:XTech k:temporalBoundsIntersect :_g84 . [by erasure from step 60] 273: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 274: ... [by rule from step 273 applied to steps [271, 272] with bindings {'P': '', 'S': '', 'O': '[...]'}] 275: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 276: @forSome :_g88 . trav:XTech k:temporalBoundsIntersect :_g88 . [by erasure from step 263] 277: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 278: ... [by rule from step 277 applied to steps [275, 276] with bindings {'P': '', 'S': '', 'O': '[...]'}] 279: :WWW2007 cal:attendee :DanC . [by erasure from step 1] 280: @forSome :_g88 . trav:DanC k:subAbstractions :_g88 . [by erasure from step 237] 281: @forSome :_g88, :_g90 . :_g90 k:temporalBoundsSubsume :_g88 . [by erasure from step 240] 282: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 283: 5 :MonthOfYearFn :May . [by erasure from step 1] 284: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 285: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 286: @forSome :_g90, :_g92 . ( k:May :_g92 ) k:MonthFn :_g90 . [by erasure from step 231] 287: @forAll :E, :MM, :MONTH, :MONTH_TYPE, :WHEN, :YEAR, :YYYY . { @forSome run:_g107, run:_g108 . ( :MM 0 ) math:sum run:_g108 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum run:_g107 . run:_g107 k:YearFn :YEAR . run:_g108 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } . [by erasure from step 1] 288: ... [by rule from step 287 applied to steps [283, 284, 285, 101, 102, 103, 286] with bindings {'MONTH_TYPE': '', 'E': '', 'MM': '"05...05"', 'YEAR': '[...]', 'WHEN': '"2006...5-08"', 'MONTH': '[...]', 'YYYY': '"2006...2006"', '_g_L76C22': '"2006...2006"', '_g_L77C20': '"5...5"'}] 289: @forSome :_g90 . trav:WWW2007 k:startsDuring :_g90 . [by erasure from step 288] 290: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 291: ... [by rule from step 290 applied to steps [282, 289] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 292: @forSome :_g90 . trav:WWW2007 k:temporalBoundsIntersect :_g90 . [by erasure from step 291] 293: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 294: ... [by rule from step 293 applied to steps [281, 292] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 295: @forSome :_g88 . trav:WWW2007 k:temporalBoundsIntersect :_g88 . [by erasure from step 294] 296: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 297: ... [by rule from step 296 applied to steps [279, 280, 295] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 298: @forSome :_g84, :_g94 . :_g84 k:temporalBoundsSubsume :_g94 . [by erasure from step 125] 299: @forSome :_g84 . trav:XTech k:temporalBoundsIntersect :_g84 . [by erasure from step 60] 300: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 301: ... [by rule from step 300 applied to steps [298, 299] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 302: :temporallySubsumes s:subPropertyOf :temporallyIntersect . [by erasure from step 1] 303: @forSome :_g88, :_g90 . :_g90 k:temporallySubsumes :_g88 . [by erasure from step 237] 304: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 305: ... [by rule from step 304 applied to steps [302, 303] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 306: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 307: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 308: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 309: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 310: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 311: @forAll :E, :WHEN, :YEAR, :YYYY . { @forSome run:_g103 . ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum run:_g103 . run:_g103 k:YearFn :YEAR . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :YEAR . } . [by erasure from step 1] 312: ... [by rule from step 311 applied to steps [307, 308, 309, 310] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-15"', 'E': '', '_g_L63C22': '"2006...2006"', 'YEAR': '[...]'}] 313: @forSome :_g92 . trav:XTech k:startsDuring :_g92 . [by erasure from step 312] 314: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 315: ... [by rule from step 314 applied to steps [306, 313] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 316: :YearFn s:range :CalendarYear . [by erasure from step 1] 317: @forSome :_g92 . 2006 k:YearFn :_g92 . [by erasure from step 66] 318: @forAll :C, :O . { @forSome run:_g86, run:_g87 . run:_g86 run:_g87 :O . run:_g87 s:range :C . } log:implies {:O a :C . } . [by erasure from step 1] 319: ... [by rule from step 318 applied to steps [316, 317] with bindings {'C': '', '_g_L135C3': '"2006...2006"', 'O': '[...]', '_g_L135C6': ''}] 320: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 321: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 322: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 323: :XTech cal:dtstart "2006-05-15"^^dt:date . [by erasure from step 1] 324: ( "2006-05-15"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 325: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 326: @forAll :E, :WHEN, :YEAR, :YYYY . { @forSome run:_g103 . ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum run:_g103 . run:_g103 k:YearFn :YEAR . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :YEAR . } . [by erasure from step 1] 327: ... [by rule from step 326 applied to steps [322, 323, 324, 325] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-15"', 'E': '', '_g_L63C22': '"2006...2006"', 'YEAR': '[...]'}] 328: @forSome :_g85 . trav:XTech k:startsDuring :_g85 . [by erasure from step 327] 329: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 330: ... [by rule from step 329 applied to steps [321, 328] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 331: @forSome :_g85 . trav:XTech k:temporalBoundsIntersect :_g85 . [by erasure from step 330] 332: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 333: ... [by rule from step 332 applied to steps [320, 331] with bindings {'P': '', 'S': '', 'O': '[...]'}] 334: @forSome :_g82, :_g93 . :_g93 k:temporalBoundsSubsume :_g82 . [by erasure from step 27] 335: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 336: @forSome :_g82, :_g93 . :_g93 k:temporalBoundsIntersect :_g82 . [by erasure from step 30] 337: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 338: ... [by rule from step 337 applied to steps [335, 336] with bindings {'P': '', 'S': '[...]', 'O': '[...]'}] 339: @forSome :_g82, :_g93 . :_g82 k:temporalBoundsIntersect :_g93 . [by erasure from step 338] 340: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 341: ... [by rule from step 340 applied to steps [334, 339] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': '[...]'}] 342: :DanC a :OneTripPerMonthAgent . [by erasure from step 1] 343: @forSome :_g96 . :_g96 a trav:PersonMonth . [by erasure from step 92] 344: @forSome :_g96 . trav:DanC k:subAbstractions :_g96 . [by erasure from step 92] 345: @forAll :WHO, :WHO_WHEN . { :WHO a trav:OneTripPerMonthAgent; k:subAbstractions :WHO_WHEN . :WHO_WHEN a trav:PersonMonth . } log:implies {:WHO_WHEN a trav:RestrictedPersonMonth . } . [by erasure from step 1] 346: ... [by rule from step 345 applied to steps [342, 343, 344] with bindings {'WHO': '', 'WHO_WHEN': '[...]'}] 347: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 348: @forSome :_g93 . trav:XTech k:temporalBoundsIntersect :_g93 . [by erasure from step 182] 349: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 350: ... [by rule from step 349 applied to steps [347, 348] with bindings {'P': '', 'S': '', 'O': '[...]'}] 351: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 352: @forSome :_g84, :_g94 . :_g84 k:temporalBoundsSubsume :_g94 . [by erasure from step 125] 353: @forSome :_g84 . trav:WWW2007 k:temporalBoundsIntersect :_g84 . [by erasure from step 203] 354: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 355: ... [by rule from step 354 applied to steps [352, 353] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 356: @forSome :_g94 . trav:WWW2007 k:temporalBoundsIntersect :_g94 . [by erasure from step 355] 357: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 358: ... [by rule from step 357 applied to steps [351, 356] with bindings {'P': '', 'S': '', 'O': '[...]'}] 359: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 360: @forSome :_g82 . trav:XTech k:temporalBoundsIntersect :_g82 . [by erasure from step 185] 361: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 362: ... [by rule from step 361 applied to steps [359, 360] with bindings {'P': '', 'S': '', 'O': '[...]'}] 363: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 364: @forSome :_g90 . trav:XTech k:temporalBoundsIntersect :_g90 . [by erasure from step 260] 365: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 366: ... [by rule from step 365 applied to steps [363, 364] with bindings {'P': '', 'S': '', 'O': '[...]'}] 367: :WWW2007 owl:differentFrom :XTech . [by erasure from step 166] 368: @forSome :_g81 . :_g81 owl:maxCardinality 1 . [by erasure from step 1] 369: @forSome :_g81 . :_g81 owl:onProperty trav:trip . [by erasure from step 1] 370: @forSome :_g81, :_g82 . :_g82 a :_g81 . [by erasure from step 139] 371: @forSome :_g82 . :_g82 trav:trip trav:WWW2007 . [by erasure from step 153] 372: @forSome :_g82 . :_g82 trav:trip trav:XTech . [by erasure from step 188] 373: @forAll :O1, :O2, :P, :S . { @forSome run:_g83 . run:_g83 owl:maxCardinality 1; owl:onProperty :P . :S a run:_g83; :P :O1, :O2 . } log:implies {:O1 = :O2 . } . [by erasure from step 1] 374: ... [by rule from step 373 applied to steps [368, 369, 370, 371, 372] with bindings {'P': '', 'S': '[...]', 'O1': '', '_g_L120C8': '[...]', 'O2': ''}] 375: :XTech = :WWW2007 . [by erasure from step 374] 376: @forAll :O, :P, :S . { @forSome run:_g95 . run:_g95 = :O . :S :P run:_g95 . } log:implies {:S :P :O . } . [by erasure from step 1] 377: ... [by rule from step 376 applied to steps [367, 375] with bindings {'P': '', 'S': '', '_g_L129C9': '', 'O': ''}] 378: :DanC a :OneTripPerMonthAgent . [by erasure from step 1] 379: @forSome :_g94 . :_g94 a trav:PersonMonth . [by erasure from step 122] 380: @forSome :_g94 . trav:DanC k:subAbstractions :_g94 . [by erasure from step 122] 381: @forAll :WHO, :WHO_WHEN . { :WHO a trav:OneTripPerMonthAgent; k:subAbstractions :WHO_WHEN . :WHO_WHEN a trav:PersonMonth . } log:implies {:WHO_WHEN a trav:RestrictedPersonMonth . } . [by erasure from step 1] 382: ... [by rule from step 381 applied to steps [378, 379, 380] with bindings {'WHO': '', 'WHO_WHEN': '[...]'}] 383: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 384: @forSome :_g92 . trav:XTech k:temporalBoundsIntersect :_g92 . [by erasure from step 315] 385: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 386: ... [by rule from step 385 applied to steps [383, 384] with bindings {'P': '', 'S': '', 'O': '[...]'}] 387: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 388: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 389: @forSome :_g85 . 2006 k:YearFn :_g85 . [by erasure from step 11] 390: :WWW2007 cal:dtstart "2006-05-08"^^dt:date . [by erasure from step 1] 391: ( "2006-05-08"^^dt:date "(\\d\\d\\d\\d)-" ) :search ( "2006" ) . [by built-in Axiom str:search] 392: ( "2006" 0 ) :sum 2006 . [by built-in Axiom math:sum] 393: @forAll :E, :WHEN, :YEAR, :YYYY . { @forSome run:_g103 . ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum run:_g103 . run:_g103 k:YearFn :YEAR . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :YEAR . } . [by erasure from step 1] 394: ... [by rule from step 393 applied to steps [389, 390, 391, 392] with bindings {'YYYY': '"2006...2006"', 'WHEN': '"2006...5-08"', 'E': '', '_g_L63C22': '"2006...2006"', 'YEAR': '[...]'}] 395: @forSome :_g85 . trav:WWW2007 k:startsDuring :_g85 . [by erasure from step 394] 396: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 397: ... [by rule from step 396 applied to steps [388, 395] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 398: @forSome :_g85 . trav:WWW2007 k:temporalBoundsIntersect :_g85 . [by erasure from step 397] 399: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 400: ... [by rule from step 399 applied to steps [387, 398] with bindings {'P': '', 'S': '', 'O': '[...]'}] 401: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 402: @forSome :_g96 . trav:WWW2007 k:temporalBoundsIntersect :_g96 . [by erasure from step 112] 403: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 404: ... [by rule from step 403 applied to steps [401, 402] with bindings {'P': '', 'S': '', 'O': '[...]'}] 405: :temporallySubsumes s:subPropertyOf :temporallyIntersect . [by erasure from step 1] 406: @forSome :_g96, :_g97 . :_g97 k:temporallySubsumes :_g96 . [by erasure from step 92] 407: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 408: ... [by rule from step 407 applied to steps [405, 406] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 409: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 410: @forSome :_g92 . trav:WWW2007 k:temporalBoundsIntersect :_g92 . [by erasure from step 75] 411: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 412: ... [by rule from step 411 applied to steps [409, 410] with bindings {'P': '', 'S': '', 'O': '[...]'}] 413: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 414: @forSome :_g97 . trav:WWW2007 k:temporalBoundsIntersect :_g97 . [by erasure from step 109] 415: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 416: ... [by rule from step 415 applied to steps [413, 414] with bindings {'P': '', 'S': '', 'O': '[...]'}] 417: @forSome :_g81 . trav:RestrictedPersonMonth s:subClassOf :_g81 . [by erasure from step 1] 418: @forSome :_g96 . :_g96 a trav:RestrictedPersonMonth . [by erasure from step 346] 419: @forAll :C, :S . { @forSome run:_g98 . run:_g98 s:subClassOf :C . :S a run:_g98 . } log:implies {:S a :C . } . [by erasure from step 1] 420: ... [by rule from step 419 applied to steps [417, 418] with bindings {'_g_L134C8': '', 'C': '[...]', 'S': '[...]'}] 421: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 422: @forSome :_g88, :_g90 . :_g90 k:temporalBoundsIntersect :_g88 . [by erasure from step 243] 423: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 424: ... [by rule from step 423 applied to steps [421, 422] with bindings {'P': '', 'S': '[...]', 'O': '[...]'}] 425: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 426: @forSome :_g84, :_g94 . :_g84 k:temporalBoundsIntersect :_g94 . [by erasure from step 128] 427: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 428: ... [by rule from step 427 applied to steps [425, 426] with bindings {'P': '', 'S': '[...]', 'O': '[...]'}] 429: @forSome :_g81 . trav:RestrictedPersonMonth s:subClassOf :_g81 . [by erasure from step 1] 430: @forSome :_g94 . :_g94 a trav:RestrictedPersonMonth . [by erasure from step 382] 431: @forAll :C, :S . { @forSome run:_g98 . run:_g98 s:subClassOf :C . :S a run:_g98 . } log:implies {:S a :C . } . [by erasure from step 1] 432: ... [by rule from step 431 applied to steps [429, 430] with bindings {'_g_L134C8': '', 'C': '[...]', 'S': '[...]'}] 433: :startsDuring s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 434: @forSome :_g97 . trav:XTech k:startsDuring :_g97 . [by erasure from step 219] 435: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 436: ... [by rule from step 435 applied to steps [433, 434] with bindings {'P': '', 'S': '', 'O': '[...]', '_g_L136C6': ''}] 437: :temporalBoundsSubsume s:subPropertyOf :temporalBoundsIntersect . [by erasure from step 1] 438: @forSome :_g96, :_g97 . :_g97 k:temporalBoundsSubsume :_g96 . [by erasure from step 95] 439: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 440: ... [by rule from step 439 applied to steps [437, 438] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 441: @forSome :_g81 . :_g81 owl:maxCardinality 1 . [by erasure from step 1] 442: @forSome :_g81 . :_g81 owl:onProperty trav:trip . [by erasure from step 1] 443: @forSome :_g81, :_g82 . :_g82 a :_g81 . [by erasure from step 139] 444: @forSome :_g82 . :_g82 trav:trip trav:XTech . [by erasure from step 188] 445: @forSome :_g82 . :_g82 trav:trip trav:XTech . [by erasure from step 188] 446: @forAll :O1, :O2, :P, :S . { @forSome run:_g83 . run:_g83 owl:maxCardinality 1; owl:onProperty :P . :S a run:_g83; :P :O1, :O2 . } log:implies {:O1 = :O2 . } . [by erasure from step 1] 447: ... [by rule from step 446 applied to steps [441, 442, 443, 444, 445] with bindings {'P': '', 'S': '[...]', 'O1': '', '_g_L120C8': '[...]', 'O2': ''}] 448: @forSome :_g81 . trav:RestrictedPersonMonth s:subClassOf :_g81 . [by erasure from step 1] 449: :DanC a :OneTripPerMonthAgent . [by erasure from step 1] 450: @forSome :_g88 . :_g88 a trav:PersonMonth . [by erasure from step 237] 451: @forSome :_g88 . trav:DanC k:subAbstractions :_g88 . [by erasure from step 237] 452: @forAll :WHO, :WHO_WHEN . { :WHO a trav:OneTripPerMonthAgent; k:subAbstractions :WHO_WHEN . :WHO_WHEN a trav:PersonMonth . } log:implies {:WHO_WHEN a trav:RestrictedPersonMonth . } . [by erasure from step 1] 453: ... [by rule from step 452 applied to steps [449, 450, 451] with bindings {'WHO': '', 'WHO_WHEN': '[...]'}] 454: @forSome :_g88 . :_g88 a trav:RestrictedPersonMonth . [by erasure from step 453] 455: @forAll :C, :S . { @forSome run:_g98 . run:_g98 s:subClassOf :C . :S a run:_g98 . } log:implies {:S a :C . } . [by erasure from step 1] 456: ... [by rule from step 455 applied to steps [448, 454] with bindings {'_g_L134C8': '', 'C': '[...]', 'S': '[...]'}] 457: @forSome :_g84, :_g94 . :_g84 k:temporalBoundsSubsume :_g94 . [by erasure from step 125] 458: @forSome :_g84, :_g94 . :_g94 k:temporalBoundsIntersect :_g84 . [by erasure from step 428] 459: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 460: ... [by rule from step 459 applied to steps [457, 458] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': '[...]'}] 461: @forSome :_g96, :_g97 . :_g97 k:temporalBoundsSubsume :_g96 . [by erasure from step 95] 462: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 463: @forSome :_g96, :_g97 . :_g97 k:temporalBoundsIntersect :_g96 . [by erasure from step 440] 464: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 465: ... [by rule from step 464 applied to steps [462, 463] with bindings {'P': '', 'S': '[...]', 'O': '[...]'}] 466: @forSome :_g96, :_g97 . :_g96 k:temporalBoundsIntersect :_g97 . [by erasure from step 465] 467: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 468: ... [by rule from step 467 applied to steps [461, 466] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': '[...]'}] 469: :WWW2007 cal:attendee :DanC . [by erasure from step 1] 470: @forSome :_g96 . trav:DanC k:subAbstractions :_g96 . [by erasure from step 92] 471: @forSome :_g96 . trav:WWW2007 k:temporalBoundsIntersect :_g96 . [by erasure from step 112] 472: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 473: ... [by rule from step 472 applied to steps [469, 470, 471] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 474: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 475: @forSome :_g88 . trav:WWW2007 k:temporalBoundsIntersect :_g88 . [by erasure from step 294] 476: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 477: ... [by rule from step 476 applied to steps [474, 475] with bindings {'P': '', 'S': '', 'O': '[...]'}] 478: @forSome :_g88, :_g90 . :_g90 k:temporalBoundsSubsume :_g88 . [by erasure from step 240] 479: @forSome :_g88, :_g90 . :_g88 k:temporalBoundsIntersect :_g90 . [by erasure from step 424] 480: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 481: ... [by rule from step 480 applied to steps [478, 479] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': '[...]'}] 482: :temporallySubsumes s:subPropertyOf :temporallyIntersect . [by erasure from step 1] 483: @forSome :_g82, :_g93 . :_g93 k:temporallySubsumes :_g82 . [by erasure from step 24] 484: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 485: ... [by rule from step 484 applied to steps [482, 483] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 486: :XTech cal:attendee :DanC . [by erasure from step 1] 487: @forSome :_g96 . trav:DanC k:subAbstractions :_g96 . [by erasure from step 92] 488: @forSome :_g96, :_g97 . :_g97 k:temporalBoundsSubsume :_g96 . [by erasure from step 95] 489: @forSome :_g97 . trav:XTech k:temporalBoundsIntersect :_g97 . [by erasure from step 436] 490: @forAll :BIG, :E, :LITTLE . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . [by erasure from step 1] 491: ... [by rule from step 490 applied to steps [488, 489] with bindings {'BIG': '[...]', 'LITTLE': '[...]', 'E': ''}] 492: @forSome :_g96 . trav:XTech k:temporalBoundsIntersect :_g96 . [by erasure from step 491] 493: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 494: ... [by rule from step 493 applied to steps [486, 487, 492] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 495: :WWW2007 k:temporallyDisjoint :XTech . [by erasure from step 163] 496: :XTech = :WWW2007 . [by erasure from step 374] 497: @forAll :O, :P, :S . { @forSome run:_g95 . run:_g95 = :O . :S :P run:_g95 . } log:implies {:S :P :O . } . [by erasure from step 1] 498: ... [by rule from step 497 applied to steps [495, 496] with bindings {'P': '', 'S': '', '_g_L129C9': '', 'O': ''}] 499: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 500: @forSome :_g94 . trav:XTech k:temporalBoundsIntersect :_g94 . [by erasure from step 301] 501: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 502: ... [by rule from step 501 applied to steps [499, 500] with bindings {'P': '', 'S': '', 'O': '[...]'}] 503: :XTech cal:attendee :DanC . [by erasure from step 1] 504: @forSome :_g94 . trav:DanC k:subAbstractions :_g94 . [by erasure from step 122] 505: @forSome :_g94 . trav:XTech k:temporalBoundsIntersect :_g94 . [by erasure from step 301] 506: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 507: ... [by rule from step 506 applied to steps [503, 504, 505] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 508: :temporallySubsumes s:subPropertyOf :temporallyIntersect . [by erasure from step 1] 509: @forSome :_g84, :_g94 . :_g84 k:temporallySubsumes :_g94 . [by erasure from step 122] 510: @forAll :O, :P, :S . { @forSome run:_g91 . run:_g91 s:subPropertyOf :P . :S run:_g91 :O . } log:implies {:S :P :O . } . [by erasure from step 1] 511: ... [by rule from step 510 applied to steps [508, 509] with bindings {'P': '', 'S': '[...]', 'O': '[...]', '_g_L136C6': ''}] 512: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 513: @forSome :_g97 . trav:XTech k:temporalBoundsIntersect :_g97 . [by erasure from step 436] 514: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 515: ... [by rule from step 514 applied to steps [512, 513] with bindings {'P': '', 'S': '', 'O': '[...]'}] 516: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 517: @forSome :_g96 . trav:XTech k:temporalBoundsIntersect :_g96 . [by erasure from step 491] 518: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 519: ... [by rule from step 518 applied to steps [516, 517] with bindings {'P': '', 'S': '', 'O': '[...]'}] 520: :WWW2007 cal:attendee :DanC . [by erasure from step 1] 521: @forSome :_g94 . trav:DanC k:subAbstractions :_g94 . [by erasure from step 122] 522: @forSome :_g94 . trav:WWW2007 k:temporalBoundsIntersect :_g94 . [by erasure from step 355] 523: @forAll :E, :WHO_WHEN . { @forSome run:_g89 . run:_g89 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee run:_g89 . } log:implies {:WHO_WHEN trav:trip :E . } . [by erasure from step 1] 524: ... [by rule from step 523 applied to steps [520, 521, 522] with bindings {'E': '', 'WHO_WHEN': '[...]', '_g_L83C19': ''}] 525: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 526: @forSome :_g90 . trav:WWW2007 k:temporalBoundsIntersect :_g90 . [by erasure from step 291] 527: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 528: ... [by rule from step 527 applied to steps [525, 526] with bindings {'P': '', 'S': '', 'O': '[...]'}] 529: :temporalBoundsIntersect a owl:SymmetricProperty . [by erasure from step 1] 530: @forSome :_g93 . trav:WWW2007 k:temporalBoundsIntersect :_g93 . [by erasure from step 147] 531: @forAll :O, :P, :S . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . [by erasure from step 1] 532: ... [by rule from step 531 applied to steps [529, 530] with bindings {'P': '', 'S': '', 'O': '[...]'}] 533: @forAll one:BIG, one:C, one:E, one:E1, one:E2, one:LITTLE, one:MM, one:MONTH, one:MONTH_TYPE, one:O, one:O1, one:O2, one:P, one:S, one:WHEN, one:WHO, one:WHO_WHEN, one:YEAR, one:YEARNUM, one:YYYY. @forSome :_g81, :_g82, :_g84, :_g85, :_g88, :_g90, :_g92, :_g93, :_g94, :_g96, :_g97 . 2006 k:YearFn :_g85, :_g92 . 5 k:MonthOfYearFn k:May . ( k:May :_g85 ) k:MonthFn :_g84, :_g93 . ( k:May :_g92 ) k:MonthFn :_g90, :_g97 . :_g81 owl:maxCardinality 1; owl:onProperty trav:trip . :_g82 a :_g81, trav:PersonMonth, trav:RestrictedPersonMonth; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect :_g82, :_g93, trav:WWW2007, trav:XTech . :_g84 a k:CalendarMonth; k:temporalBoundsIntersect :_g94, trav:WWW2007, trav:XTech; k:temporalBoundsSubsume :_g94; k:temporallyIntersect :_g94; k:temporallySubsumes :_g94 . :_g85 a k:CalendarYear; k:temporalBoundsIntersect trav:WWW2007, trav:XTech . :_g88 a :_g81, trav:PersonMonth, trav:RestrictedPersonMonth; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect :_g88, :_g90, trav:WWW2007, trav:XTech . :_g90 a k:CalendarMonth; k:temporalBoundsIntersect :_g88, trav:WWW2007, trav:XTech; k:temporalBoundsSubsume :_g88; k:temporallyIntersect :_g88; k:temporallySubsumes :_g88 . :_g92 a k:CalendarYear; k:temporalBoundsIntersect trav:WWW2007, trav:XTech . :_g93 a k:CalendarMonth; k:temporalBoundsIntersect :_g82, trav:WWW2007, trav:XTech; k:temporalBoundsSubsume :_g82; k:temporallyIntersect :_g82; k:temporallySubsumes :_g82 . :_g94 a :_g81, trav:PersonMonth, trav:RestrictedPersonMonth; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect :_g84, :_g94, trav:WWW2007, trav:XTech . :_g96 a :_g81, trav:PersonMonth, trav:RestrictedPersonMonth; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect :_g96, :_g97, trav:WWW2007, trav:XTech . :_g97 a k:CalendarMonth; k:temporalBoundsIntersect :_g96, trav:WWW2007, trav:XTech; k:temporalBoundsSubsume :_g96; k:temporallyIntersect :_g96; k:temporallySubsumes :_g96 . trav:DanC a trav:OneTripPerMonthAgent, ; k:subAbstractions :_g82, :_g88, :_g94, :_g96 . trav:RestrictedPersonMonth s:subClassOf :_g81, trav:PersonMonth . trav:WWW2007 k:startsDuring :_g84, :_g85, :_g90, :_g92, :_g93, :_g97; k:temporalBoundsIntersect :_g82, :_g84, :_g85, :_g88, :_g90, :_g92, :_g93, :_g94, :_g96, :_g97; k:temporallyDisjoint trav:WWW2007, trav:XTech; owl:differentFrom trav:WWW2007, trav:XTech; = trav:WWW2007, trav:XTech; cal:attendee trav:DanC; cal:dtend "2006-05-12"^^dt:date; cal:dtstart "2006-05-08"^^dt:date . trav:XTech k:startsDuring :_g84, :_g85, :_g90, :_g92, :_g93, :_g97; k:temporalBoundsIntersect :_g82, :_g84, :_g85, :_g88, :_g90, :_g92, :_g93, :_g94, :_g96, :_g97; = trav:WWW2007, trav:XTech; cal:attendee trav:DanC; cal:dtend "2006-05-18"^^dt:date; cal:dtstart "2006-05-15"^^dt:date . s:seeAlso . k:May a k:MonthOfYearType . k:MonthFn s:range k:CalendarMonth . k:MonthOfYearFn s:range k:MonthOfYearType . k:YearFn s:range k:CalendarYear . k:startsDuring s:subPropertyOf k:temporalBoundsIntersect . k:temporalBoundsIntersect a owl:SymmetricProperty . k:temporalBoundsSubsume s:subPropertyOf k:temporalBoundsIntersect . k:temporallyDisjoint s:subPropertyOf owl:differentFrom . k:temporallySubsumes s:subPropertyOf k:temporalBoundsSubsume, k:temporallyIntersect . owl:sameAs a owl:SymmetricProperty . { one:BIG k:temporalBoundsSubsume one:LITTLE . one:E k:temporalBoundsIntersect one:BIG . } log:implies {one:E k:temporalBoundsIntersect one:LITTLE . } . { one:P a owl:SymmetricProperty . one:S one:P one:O . } log:implies {one:O one:P one:S . } . { one:WHEN a k:CalendarMonth . one:WHO a . } log:implies { @forSome :_g99 . :_g99 a trav:PersonMonth . one:WHEN k:temporallySubsumes :_g99 . one:WHO k:subAbstractions :_g99 . } . { @forSome :_g91 . :_g91 s:subPropertyOf one:P . one:S :_g91 one:O . } log:implies {one:S one:P one:O . } . { @forSome :_g95 . :_g95 = one:O . one:S one:P :_g95 . } log:implies {one:S one:P one:O . } . { @forSome :_g98 . :_g98 s:subClassOf one:C . one:S a :_g98 . } log:implies {one:S a one:C . } . { @forSome :_g86, :_g87 . :_g86 :_g87 one:O . :_g87 s:range one:C . } log:implies {one:O a one:C . } . { ( one:WHEN "(\\d\\d\\d\\d)-" ) str:search ( one:YYYY ) . ( one:YYYY 0 ) math:sum one:YEARNUM . one:E cal:dtstart one:WHEN . } log:implies { @forSome :_g100 . one:YEARNUM k:YearFn :_g100 . } . { one:WHO a trav:OneTripPerMonthAgent; k:subAbstractions one:WHO_WHEN . one:WHO_WHEN a trav:PersonMonth . } log:implies {one:WHO_WHEN a trav:RestrictedPersonMonth . } . { @forSome :_g89 . :_g89 k:subAbstractions one:WHO_WHEN . one:E k:temporalBoundsIntersect one:WHO_WHEN; cal:attendee :_g89 . } log:implies {one:WHO_WHEN trav:trip one:E . } . { one:P a owl:TransitiveProperty . one:S one:P [ one:P one:O ] . } log:implies {one:S one:P one:O . } . { @forSome :_g101, :_g102 . :_g101 str:lessThan :_g102 . one:E1 cal:dtend :_g101 . one:E2 cal:dtstart :_g102 . } log:implies {one:E1 k:temporallyDisjoint one:E2 . } . { @forSome :_g103 . ( one:WHEN "(\\d\\d\\d\\d)-" ) str:search ( one:YYYY ) . ( one:YYYY 0 ) math:sum :_g103 . :_g103 k:YearFn one:YEAR . one:E cal:dtstart one:WHEN . } log:implies {one:E k:startsDuring one:YEAR . } . { @forSome :_g83 . :_g83 owl:maxCardinality 1; owl:onProperty one:P . one:S a :_g83; one:P one:O1, one:O2 . } log:implies {one:O1 = one:O2 . } . { @forSome :_g104, :_g105 . ( one:MM 0 ) math:sum :_g105 . ( one:WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( one:YYYY one:MM ) . ( one:YYYY 0 ) math:sum :_g104 . :_g104 k:YearFn one:YEAR . :_g105 k:MonthOfYearFn one:MONTH_TYPE . one:E cal:dtstart one:WHEN . } log:implies { @forSome :_g106 . ( one:MONTH_TYPE one:YEAR ) k:MonthFn :_g106 . } . { @forSome :_g107, :_g108 . ( one:MM 0 ) math:sum :_g108 . ( one:MONTH_TYPE one:YEAR ) k:MonthFn one:MONTH . ( one:WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( one:YYYY one:MM ) . ( one:YYYY 0 ) math:sum :_g107 . :_g107 k:YearFn one:YEAR . :_g108 k:MonthOfYearFn one:MONTH_TYPE . one:E cal:dtstart one:WHEN . } log:implies {one:E k:startsDuring one:MONTH . } . [by conjoining steps [30, 1, 27, 24, 21, 18, 11, 39, 60, 57, 54, 75, 72, 66, 112, 95, 92, 89, 86, 109, 106, 128, 125, 122, 119, 157, 139, 136, 153, 150, 147, 166, 163, 192, 188, 185, 182, 179, 206, 203, 200, 210, 219, 243, 240, 237, 234, 231, 247, 266, 263, 260, 257, 270, 274, 278, 297, 294, 291, 288, 301, 305, 315, 312, 319, 333, 330, 327, 341, 338, 346, 350, 358, 355, 362, 366, 377, 374, 382, 386, 400, 397, 394, 404, 408, 412, 416, 420, 424, 428, 432, 436, 440, 447, 456, 453, 460, 468, 465, 473, 477, 481, 485, 494, 491, 498, 502, 507, 511, 515, 519, 524, 528, 532]] @prefix : . @prefix cal: . @prefix dt: . @prefix k: . @prefix log: . @prefix math: . @prefix owl: . @prefix run: . @prefix s: . @prefix str: . @prefix trav: . @forAll :BIG, :C, :E, :E1, :E2, :LITTLE, :MM, :MONTH, :MONTH_TYPE, :O, :O1, :O2, :P, :S, :WHEN, :WHO, :WHO_WHEN, :YEAR, :YEARNUM, :YYYY. @forSome run:_g100, run:_g106, run:_g99, , , , , , , , , , , :_g_L31C4 . 2006 k:YearFn run:_g100 . 5 k:MonthOfYearFn k:May . ( k:May ) k:MonthFn run:_g106 . ( k:May ) k:MonthFn run:_g106 . run:_g99 a trav:PersonMonth . a k:CalendarYear; k:temporalBoundsIntersect trav:WWW2007, trav:XTech . a k:CalendarYear; k:temporalBoundsIntersect trav:WWW2007, trav:XTech . a k:CalendarMonth; k:temporalBoundsIntersect , trav:WWW2007, trav:XTech; k:temporalBoundsSubsume ; k:temporallyIntersect ; k:temporallySubsumes run:_g99 . a k:CalendarMonth; k:temporalBoundsIntersect , trav:WWW2007, trav:XTech; k:temporalBoundsSubsume ; k:temporallyIntersect ; k:temporallySubsumes run:_g99 . a k:CalendarMonth; k:temporalBoundsIntersect , trav:WWW2007, trav:XTech; k:temporalBoundsSubsume ; k:temporallyIntersect ; k:temporallySubsumes run:_g99 . a k:CalendarMonth; k:temporalBoundsIntersect , trav:WWW2007, trav:XTech; k:temporalBoundsSubsume ; k:temporallyIntersect ; k:temporallySubsumes run:_g99 . a trav:RestrictedPersonMonth, :_g_L31C4; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect , , trav:WWW2007, trav:XTech . a trav:RestrictedPersonMonth, :_g_L31C4; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect , , trav:WWW2007, trav:XTech . a trav:RestrictedPersonMonth, :_g_L31C4; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect , , trav:WWW2007, trav:XTech . a trav:RestrictedPersonMonth, :_g_L31C4; trav:trip trav:WWW2007, trav:XTech; k:temporalBoundsIntersect , , trav:WWW2007, trav:XTech . trav:DanC a trav:OneTripPerMonthAgent, ; k:subAbstractions run:_g99 . trav:RestrictedPersonMonth s:subClassOf trav:PersonMonth, :_g_L31C4 . trav:WWW2007 k:startsDuring , , , , , ; k:temporalBoundsIntersect , , , , , , , , , ; k:temporallyDisjoint trav:WWW2007, trav:XTech; owl:differentFrom trav:WWW2007, trav:XTech; = trav:WWW2007, trav:XTech; cal:attendee trav:DanC; cal:dtend "2006-05-12"^^dt:date; cal:dtstart "2006-05-08"^^dt:date . trav:XTech k:startsDuring , , , , , ; k:temporalBoundsIntersect , , , , , , , , , ; = trav:WWW2007, trav:XTech; cal:attendee trav:DanC; cal:dtend "2006-05-18"^^dt:date; cal:dtstart "2006-05-15"^^dt:date . s:seeAlso . :_g_L31C4 owl:maxCardinality 1; owl:onProperty trav:trip . k:May a k:MonthOfYearType . k:MonthFn s:range k:CalendarMonth . k:MonthOfYearFn s:range k:MonthOfYearType . k:YearFn s:range k:CalendarYear . k:startsDuring s:subPropertyOf k:temporalBoundsIntersect . k:temporalBoundsIntersect a owl:SymmetricProperty . k:temporalBoundsSubsume s:subPropertyOf k:temporalBoundsIntersect . k:temporallyDisjoint s:subPropertyOf owl:differentFrom . k:temporallySubsumes s:subPropertyOf k:temporalBoundsSubsume, k:temporallyIntersect . owl:sameAs a owl:SymmetricProperty . { :BIG k:temporalBoundsSubsume :LITTLE . :E k:temporalBoundsIntersect :BIG . } log:implies {:E k:temporalBoundsIntersect :LITTLE . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :WHEN a k:CalendarMonth . :WHO a . } log:implies { @forSome :_g_L40C30 . :_g_L40C30 a trav:PersonMonth . :WHEN k:temporallySubsumes :_g_L40C30 . :WHO k:subAbstractions :_g_L40C30 . } . { @forSome :_g_L129C9 . :_g_L129C9 = :O . :S :P :_g_L129C9 . } log:implies {:S :P :O . } . { @forSome :_g_L134C8 . :_g_L134C8 s:subClassOf :C . :S a :_g_L134C8 . } log:implies {:S a :C . } . { @forSome :_g_L136C6 . :_g_L136C6 s:subPropertyOf :P . :S :_g_L136C6 :O . } log:implies {:S :P :O . } . { @forSome :_g_L135C3, :_g_L135C6 . :_g_L135C3 :_g_L135C6 :O . :_g_L135C6 s:range :C . } log:implies {:O a :C . } . { ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum :YEARNUM . :E cal:dtstart :WHEN . } log:implies { @forSome :_g_L59C8 . :YEARNUM k:YearFn :_g_L59C8 . } . { :WHO a trav:OneTripPerMonthAgent; k:subAbstractions :WHO_WHEN . :WHO_WHEN a trav:PersonMonth . } log:implies {:WHO_WHEN a trav:RestrictedPersonMonth . } . { @forSome :_g_L127C9 . :_g_L127C9 :P :O . :P a owl:TransitiveProperty . :S :P :_g_L127C9 . } log:implies {:S :P :O . } . { @forSome :_g_L83C19 . :_g_L83C19 k:subAbstractions :WHO_WHEN . :E k:temporalBoundsIntersect :WHO_WHEN; cal:attendee :_g_L83C19 . } log:implies {:WHO_WHEN trav:trip :E . } . { @forSome :_g_L113C17, :_g_L113C32 . :_g_L113C17 str:lessThan :_g_L113C32 . :E1 cal:dtend :_g_L113C17 . :E2 cal:dtstart :_g_L113C32 . } log:implies {:E1 k:temporallyDisjoint :E2 . } . { @forSome :_g_L63C22 . ( :WHEN "(\\d\\d\\d\\d)-" ) str:search ( :YYYY ) . ( :YYYY 0 ) math:sum :_g_L63C22 . :_g_L63C22 k:YearFn :YEAR . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :YEAR . } . { @forSome :_g_L120C8 . :_g_L120C8 owl:maxCardinality 1; owl:onProperty :P . :S a :_g_L120C8; :P :O1, :O2 . } log:implies {:O1 = :O2 . } . { @forSome :_g_L68C22, :_g_L69C20 . ( :MM 0 ) math:sum :_g_L69C20 . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum :_g_L68C22 . :_g_L68C22 k:YearFn :YEAR . :_g_L69C20 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies { @forSome :_g_L71C32 . ( :MONTH_TYPE :YEAR ) k:MonthFn :_g_L71C32 . } . { @forSome :_g_L76C22, :_g_L77C20 . ( :MM 0 ) math:sum :_g_L77C20 . ( :MONTH_TYPE :YEAR ) k:MonthFn :MONTH . ( :WHEN "(\\d\\d\\d\\d)-(\\d\\d)-" ) str:search ( :YYYY :MM ) . ( :YYYY 0 ) math:sum :_g_L76C22 . :_g_L76C22 k:YearFn :YEAR . :_g_L77C20 k:MonthOfYearFn :MONTH_TYPE . :E cal:dtstart :WHEN . } log:implies {:E k:startsDuring :MONTH . } .