(benchmark Isabelle
:extrasorts ( T2 T13 T12 T11 T10 T9 T8 T7 T6 T5 T4 T1 T3)
:extrafuns (
(uf_37 T13)
(uf_34 T12)
(uf_31 T11)
(uf_28 T10)
(uf_25 T9)
(uf_22 T8)
(uf_19 T7)
(uf_16 T6)
(uf_13 T5)
(uf_10 T4)
(uf_7 T1)
(uf_4 T3)
(uf_36 Int T13 T13)
(uf_33 T13 T12 T12)
(uf_30 T12 T11 T11)
(uf_27 T11 T10 T10)
(uf_24 T10 T9 T9)
(uf_21 T9 T8 T8)
(uf_18 T8 T7 T7)
(uf_15 T7 T6 T6)
(uf_12 T6 T5 T5)
(uf_9 T5 T4 T4)
(uf_6 T4 T1 T1)
(uf_3 T1 T3 T3)
)
:extrapreds (
(up_35 Int)
(up_32 T13)
(up_29 T12)
(up_26 T11)
(up_23 T10)
(up_20 T9)
(up_17 T8)
(up_14 T7)
(up_11 T6)
(up_8 T5)
(up_5 T4)
(up_1 T1)
(up_2 T3)
)
:assumption (forall (?x1 T1) (and (up_1 ?x1) (or (up_2 (uf_3 ?x1 uf_4)) (not (up_2 (uf_3 ?x1 uf_4))))))
:assumption (forall (?x2 T4) (and (up_5 ?x2) (or (up_1 (uf_6 ?x2 uf_7)) (not (up_1 (uf_6 ?x2 uf_7))))))
:assumption (forall (?x3 T5) (and (up_8 ?x3) (or (up_5 (uf_9 ?x3 uf_10)) (not (up_5 (uf_9 ?x3 uf_10))))))
:assumption (forall (?x4 T6) (and (up_11 ?x4) (or (up_8 (uf_12 ?x4 uf_13)) (not (up_8 (uf_12 ?x4 uf_13))))))
:assumption (forall (?x5 T7) (and (up_14 ?x5) (or (up_11 (uf_15 ?x5 uf_16)) (not (up_11 (uf_15 ?x5 uf_16))))))
:assumption (forall (?x6 T8) (and (up_17 ?x6) (or (up_14 (uf_18 ?x6 uf_19)) (not (up_14 (uf_18 ?x6 uf_19))))))
:assumption (forall (?x7 T9) (and (up_20 ?x7) (or (up_17 (uf_21 ?x7 uf_22)) (not (up_17 (uf_21 ?x7 uf_22))))))
:assumption (forall (?x8 T10) (and (up_23 ?x8) (or (up_20 (uf_24 ?x8 uf_25)) (not (up_20 (uf_24 ?x8 uf_25))))))
:assumption (forall (?x9 T11) (and (up_26 ?x9) (or (up_23 (uf_27 ?x9 uf_28)) (not (up_23 (uf_27 ?x9 uf_28))))))
:assumption (forall (?x10 T12) (and (up_29 ?x10) (or (up_26 (uf_30 ?x10 uf_31)) (not (up_26 (uf_30 ?x10 uf_31))))))
:assumption (forall (?x11 T13) (and (up_32 ?x11) (or (up_29 (uf_33 ?x11 uf_34)) (not (up_29 (uf_33 ?x11 uf_34))))))
:assumption (forall (?x12 Int) (and (up_35 ?x12) (or (up_32 (uf_36 ?x12 uf_37)) (not (up_32 (uf_36 ?x12 uf_37))))))
:assumption (not (up_35 1))
:formula true
)