(benchmark autogen
  :logic QF_UF
  :extrasorts (ELEMENT)
  :extrafuns ((normal ELEMENT)
              (reverse ELEMENT)
              (void ELEMENT)
              (actual_pos ELEMENT))
  :extrapreds ((POSITION ELEMENT))
  :extramacros ((in (lambda (?x ELEMENT) (?p (ELEMENT boolean)) . (?p ?x)))
                (emptyset (lambda (?v ELEMENT) . false))
                (omega (lambda (?x ELEMENT) . true))
                (singleton (lambda (?x ELEMENT) . (lambda (?y ELEMENT) . (= ?x ?y))))
                (intersection (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                      (lambda (?x ELEMENT) . (and (?p ?x) (?q ?x)))))
                (union (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                               (lambda (?x ELEMENT) . (or (?p ?x) (?q ?x)))))
                (difference (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                    (lambda (?x ELEMENT) .
                                            (and (?p ?x) (not (?q ?x))))))
                (symmetric_difference
                 (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                         (lambda (?x ELEMENT) .
                                 (or (and (?p ?x) (not (?q ?x)))
                                     (and (?q ?x) (not (?p ?x)))))))
                (subset (lambda (?p (ELEMENT boolean)) (?q (ELEMENT boolean)) .
                                (forall (?x ELEMENT) . (implies (?p ?x) (?q ?x)))))
                (set3 (lambda (?e1 ELEMENT) (?e2 ELEMENT) (?e3 ELEMENT) .
                      (lambda (?y ELEMENT) . (or (= ?y ?e1) (= ?y ?e2) (= ?y ?e3)))))
                (set5 (lambda (?e1 ELEMENT) (?e2 ELEMENT) (?e3 ELEMENT) (?e4 ELEMENT) (?e5 ELEMENT) .
                      (lambda (?y ELEMENT) . (or (= ?y ?e1) (= ?y ?e2) (= ?y ?e3) (= ?y ?e4) (= ?y ?e5)))))
                )
  :formula
(and
  (and
    (in normal POSITION)
    (in reverse POSITION)
    (in void POSITION)
    (and (not (= void reverse)) (not (= void normal)) (not (= reverse normal)))
    (forall (?e4 ELEMENT) (implies (in ?e4 POSITION) (or (= ?e4 normal) (= ?e4 reverse) (= ?e4 void)))))
  (and (not (= reverse normal)) (not (= void normal)) (not (= void reverse)))
  (in actual_pos POSITION)
  (not
    (implies
      (and
        (and
          (in normal POSITION)
          (in reverse POSITION)
          (in void POSITION)
          (and (not (= void reverse)) (not (= void normal)) (not (= reverse normal)))
          (forall (?e4 ELEMENT) (implies (in ?e4 POSITION) (or (= ?e4 normal) (= ?e4 reverse) (= ?e4 void)))))
        (and (not (= reverse normal)) (not (= void normal)) (not (= void reverse)))
        (in actual_pos POSITION))
      (forall (?m1 ELEMENT) (?m2 ELEMENT) (?m3 ELEMENT) (implies
true
(and
  (implies (and (in normal (set3 ?m1 ?m2 ?m3)) (not (in reverse (set3 ?m1 ?m2 ?m3)))) (in actual_pos POSITION))
  (implies (and (in reverse (set3 ?m1 ?m2 ?m3)) (not (in normal (set3 ?m1 ?m2 ?m3)))) (in actual_pos POSITION))
  (implies
    (not
      (or
        (and (in normal (set3 ?m1 ?m2 ?m3)) (not (in reverse (set3 ?m1 ?m2 ?m3))))
        (and (in reverse (set3 ?m1 ?m2 ?m3)) (not (in normal (set3 ?m1 ?m2 ?m3))))))
    (in actual_pos POSITION))))))))

  :status unknown
)
