(demo04
 (Ex1 0
  (Ex1-1 nil 3305971091 3305971445
   ("" (flatten)
    (("" (split)
      (("1" (propax) nil nil) ("2" (propax) nil nil)
       ("3" (propax) nil nil))
      nil))
    nil)
   unchecked nil 353915 3510 t shostak))
 (Laplante 0
  (Laplante-2 "semantics" 3306144402 3306144402
   ("" (bddsimp) (("1" (postpone) nil nil) ("2" (postpone) nil nil))
    nil)
   unfinished nil 78356 2390 t shostak)
  (Laplante-1 nil 3306142636 3306144319
   ("" (flatten)
    (("" (split 1)
      (("1" (split -2)
        (("1" (split)
          (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)
         ("2" (split)
          (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil))
        nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   unfinished nil 1682883 6420 t shostak)))