Quelle  allen_interval_properties.prf

(allen_interval_properties
 (before_before 0
  (before_before-1 nil 3568526117
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (smash)
        (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_during 0
  (before_during-1 nil 3568526183
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_contains 0
  (before_contains-1 nil 3568526237
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_overlaps 0
  (before_overlaps-1 nil 3568526266
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_overlapped_by 0
  (before_overlapped_by-1 nil 3568526295
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_meets 0
  (before_meets-1 nil 3568526341
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((< const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_met_by 0
  (before_met_by-1 nil 3568526375
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_starts 0
  (before_starts-1 nil 3568526433
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_started_by 0
  (before_started_by-1 nil 3568526460
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_finishes 0
  (before_finishes-1 nil 3568526488
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (before_finished_by 0
  (before_finished_by-1 nil 3568526527
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_after 0
  (after_after-1 nil 3568526554
   ("" (skolem-typepred)
    (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil)) nil)
   ((< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_during 0
  (after_during-1 nil 3568526575
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_contains 0
  (after_contains-1 nil 3568526621
   ("" (skolem-typepred)
    (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_overlaps 0
  (after_overlaps-1 nil 3568526647
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_meets 0
  (after_meets-1 nil 3568526700
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_met_by 0
  (after_met_by-1 nil 3568526750
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_starts 0
  (after_starts-1 nil 3568526777
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_started_by 0
  (after_started_by-1 nil 3568526824
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_finishes 0
  (after_finishes-1 nil 3568526852
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (after_finished_by 0
  (after_finished_by-1 nil 3568526875
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_before 0
  (during_before-1 nil 3568526902
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_after 0
  (during_after-1 nil 3568526927
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_during 0
  (during_during-1 nil 3568526956
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_overlaps 0
  (during_overlaps-1 nil 3568527081
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_overlapped_by 0
  (during_overlapped_by-1 nil 3568527207
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_meets 0
  (during_meets-1 nil 3568527248
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_t_meet_bay 0
  (during_t_meet_bay-1 nil 3568527278
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_starts 0
  (during_starts-1 nil 3568527317
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_started_by 0
  (during_started_by-1 nil 3568527344
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_finished_by 0
  (during_finished_by-1 nil 3568527390
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (during_finishes 0
  (during_finishes-1 nil 3568527483
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_before 0
  (contains_before-1 nil 3568527518
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_after 0
  (contains_after-1 nil 3568527560
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_during 0
  (contains_during-1 nil 3568527605
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "bool" allen_interval nil)
    (con const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (dur const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_contains 0
  (contains_contains-1 nil 3568527683
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_overlaps 0
  (contains_overlaps-1 nil 3568527716
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_overlapped_by 0
  (contains_overlapped_by-1 nil 3568528075
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_meets 0
  (contains_meets-1 nil 3568528123
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_meet_by 0
  (contains_meet_by-1 nil 3568528171
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_starts 0
  (contains_starts-1 nil 3568528220
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_started_by 0
  (contains_started_by-1 nil 3568528263
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_finishes 0
  (contains_finishes-1 nil 3568528312
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (contains_finished_by 0
  (contains_finished_by-1 nil 3568528380
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_before 0
  (overlaps_before-1 nil 3568528525
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_after 0
  (overlaps_after-1 nil 3568528551
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_during 0
  (overlaps_during-1 nil 3568528605
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_overlapped_by 0
  (overlaps_overlapped_by-1 nil 3568528645
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "bool" allen_interval nil)
    (con const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (dur const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_contains 0
  (overlaps_contains-1 nil 3568529357
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_overlaps 0
  (overlaps_overlaps-1 nil 3568529402
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_meets 0
  (overlaps_meets-1 nil 3568529434
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_met_by 0
  (overlaps_met_by-1 nil 3568529467
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_starts 0
  (overlaps_starts-1 nil 3568529522
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_start_by 0
  (overlaps_start_by-1 nil 3568529547
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_finishes 0
  (overlaps_finishes-1 nil 3568529588
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlaps_finished_by 0
  (overlaps_finished_by-1 nil 3568529628
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_before 0
  (overlapped_by_before-1 nil 3568529665
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_after 0
  (overlapped_by_after-1 nil 3568529705
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_during 0
  (overlapped_by_during-1 nil 3568529737
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_contains 0
  (overlapped_by_contains-1 nil 3568529775
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_overlaps 0
  (overlapped_by_overlaps-1 nil 3568529826
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (= const-decl "bool" allen_interval nil)
    (con const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (dur const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_overlapped_by 0
  (overlapped_by_overlapped_by-1 nil 3568529883
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_meets 0
  (overlapped_by_meets-1 nil 3568529920
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_meet_by 0
  (overlapped_by_meet_by-1 nil 3568529960
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_starts 0
  (overlapped_by_starts-1 nil 3568530019
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_started_by 0
  (overlapped_by_started_by-1 nil 3568530066
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_finishes 0
  (overlapped_by_finishes-1 nil 3568530083
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (overlapped_by_finished_by 0
  (overlapped_by_finished_by-1 nil 3568530100
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_before 0
  (meets_before-1 nil 3568530121
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_after 0
  (meets_after-1 nil 3568530153
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_during 0
  (meets_during-1 nil 3568530184
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_contains 0
  (meets_contains-1 nil 3568530224
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_overlaps 0
  (meets_overlaps-1 nil 3568530502
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_overlapped_by 0
  (meets_overlapped_by-1 nil 3568530531
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_meets 0
  (meets_meets-1 nil 3568530563
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_meet_by 0
  (meets_meet_by-1 nil 3568532553
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (= const-decl "bool" allen_interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_starts 0
  (meets_starts-1 nil 3568532559
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_started_by 0
  (meets_started_by-1 nil 3568532564
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_finishes 0
  (meets_finishes-1 nil 3568532569
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meets_finished_by 0
  (meets_finished_by-1 nil 3568532574
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_before 0
  (meet_by_before-1 nil 3568532578
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (< const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_after 0
  (meet_by_after-1 nil 3568532583
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_during 0
  (meet_by_during-1 nil 3568532587
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_contains 0
  (meet_by_contains-1 nil 3568532594
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_overlaps 0
  (meet_by_overlaps-1 nil 3568532598
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_meet 0
  (meet_by_meet-1 nil 3568530728
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (= const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_overlapped_by 0
  (meet_by_overlapped_by-1 nil 3568532612
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_meet_by 0
  (meet_by_meet_by-1 nil 3568532616
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_starts 0
  (meet_by_starts-1 nil 3568532620
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_started_by 0
  (meet_by_started_by-1 nil 3568532624
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (meet_by_finishes 0
  (meet_by_finishes-1 nil 3568532628
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (met_by_finished 0
  (met_by_finished-1 nil 3568532633
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_before 0
  (starts_by_before-1 nil 3568532638
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_after 0
  (starts_by_after-1 nil 3568532642
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_during 0
  (starts_by_during-1 nil 3568532647
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_contains 0
  (starts_by_contains-1 nil 3568532650
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_overlaps 0
  (starts_by_overlaps-1 nil 3568532663
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_overlapped_by 0
  (starts_by_overlapped_by-1 nil 3568532667
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_meet 0
  (starts_by_meet-1 nil 3568532672
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_meet_by 0
  (starts_by_meet_by-1 nil 3568532677
   ("" (skolem-typepred) (("" (flatten) nil nil)) nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_starts 0
  (starts_by_starts-1 nil 3568532680
   ("" (skolem-typepred) (("" (flatten) nil nil)) nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_started_by 0
  (starts_by_started_by-1 nil 3568532684
   ("" (skolem-typepred) (("" (flatten) nil nil)) nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_finishes 0
  (starts_by_finishes-1 nil 3568532690
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (starts_by_finished_by 0
  (starts_by_finished_by-1 nil 3568532694
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_before 0
  (started_by_before-1 nil 3568532699
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (< const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_after 0
  (started_by_after-1 nil 3568532703
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_during 0
  (started_by_during-1 nil 3568532707
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_contains 0
  (started_by_contains-1 nil 3568532711
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_overlaps 0
  (started_by_overlaps-1 nil 3568532725
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_overlapped_by 0
  (started_by_overlapped_by-1 nil 3568532730
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_meet 0
  (started_by_meet-1 nil 3568532739
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_meet_by 0
  (started_by_meet_by-1 nil 3568532744
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_starts 0
  (started_by_starts-1 nil 3568532749
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (= const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_started_by 0
  (started_by_started_by-1 nil 3568532754
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_finishes 0
  (started_by_finishes-1 nil 3568532760
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (started_by_finished_by 0
  (started_by_finished_by-1 nil 3568532764
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_before 0
  (finishes_before-1 nil 3568532768
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_after 0
  (finishes_after-1 nil 3568532785
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_during 0
  (finishes_during-1 nil 3568532791
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_contains 0
  (finishes_contains-1 nil 3568532796
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_overlaps 0
  (finishes_overlaps-1 nil 3568532800
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_overlapped_by 0
  (finishes_overlapped_by-1 nil 3568532804
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_meets 0
  (finishes_meets-1 nil 3568532808
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_meet_by 0
  (finishes_meet_by-1 nil 3568532812
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_starts 0
  (finishes_starts-1 nil 3568532816
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_started_by 0
  (finishes_started_by-1 nil 3568532820
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_finishes 0
  (finishes_finishes-1 nil 3568532827
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finishes_finished_by 0
  (finishes_finished_by-1 nil 3568532832
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (= const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_before 0
  (finished_by_before-1 nil 3568532837
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_after 0
  (finished_by_after-1 nil 3568532842
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (> const-decl "bool" allen_interval nil)
    (< const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_during 0
  (finished_by_during-1 nil 3568532854
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_contains 0
  (finished_by_contains-1 nil 3568532860
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_overlaps 0
  (finished_by_overlaps-1 nil 3568532864
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_overlapped_by 0
  (finished_by_overlapped_by-1 nil 3568532870
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_meets 0
  (finished_by_meets-1 nil 3568532874
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_meet_by 0
  (finished_by_meet_by-1 nil 3568532878
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (oi const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (mi const-decl "bool" allen_interval nil)
    (m const-decl "bool" allen_interval nil)
    (meets const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_starts 0
  (finished_by_starts-1 nil 3568532882
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (overlaps const-decl "bool" allen_interval nil)
    (O const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_started_by 0
  (finished_by_started_by-1 nil 3568532886
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (di const-decl "bool" allen_interval nil)
    (d const-decl "bool" allen_interval nil)
    (during const-decl "bool" allen_interval nil)
    (si const-decl "bool" allen_interval nil)
    (s const-decl "bool" allen_interval nil)
    (starts const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (finishes const-decl "bool" allen_interval nil)
    (> const-decl "bool" reals nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_finishes 0
  (finished_by_finishes-1 nil 3568532890
   ("" (skolem-typepred)
    (("" (flatten)
      (("" (expand "StrictInterval?") (("" (smash) nil nil)) nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (finishes const-decl "bool" allen_interval nil)
    (f const-decl "bool" allen_interval nil)
    (fi const-decl "bool" allen_interval nil)
    (= const-decl "bool" allen_interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (finished_by_finished_by 0
  (finished_by_finished_by-1 nil 3568532894
   ("" (skolem-typepred) (("" (flatten) nil nil)) nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))