Quelle allen_interval_properties.prf Sprache: Lisp

(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)
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.39 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.