(benchmark frame_prop.induction.smt
  :source {
The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unsat
:category { industrial }
:difficulty { 0 }
  :logic QF_LRA
  
  :extrafuns ((x_0 Real))
  :extrafuns ((x_1 Real))
  :extrafuns ((x_2 Real))
  :extrafuns ((x_3 Real))
  :extrafuns ((x_4 Real))
  :extrafuns ((x_5 Real))
  :extrapreds ((x_6))
  :extrapreds ((x_7))
  :extrafuns ((x_8 Real))
  :extrafuns ((x_9 Real))
  :extrapreds ((x_10))
  :extrapreds ((x_11))
  :extrapreds ((x_12))
  :extrapreds ((x_13))
  :extrapreds ((x_14))
  :extrapreds ((x_15))
  :extrapreds ((x_16))
  :extrapreds ((x_17))
  :extrapreds ((x_18))
  :extrapreds ((x_19))
  :extrapreds ((x_20))
  :extrapreds ((x_21))
  :extrafuns ((x_22 Real))
  :extrafuns ((x_23 Real))
  :extrafuns ((x_24 Real))
  :extrafuns ((x_25 Real))
  :extrafuns ((x_26 Real))
  :extrafuns ((x_27 Real))
  :extrafuns ((x_28 Real))
  :extrapreds ((x_29))
  :extrapreds ((x_30))
  :extrapreds ((x_31))
  :extrapreds ((x_32))
  :extrapreds ((x_33))
  :extrapreds ((x_34))
  :extrapreds ((x_35))
  :extrapreds ((x_36))
  :extrapreds ((x_37))
  :extrapreds ((x_38))
  :extrafuns ((x_39 Real))
  :extrafuns ((x_40 Real))
  :extrafuns ((x_41 Real))
  :extrafuns ((x_42 Real))
  :extrafuns ((x_43 Real))
  :extrafuns ((x_44 Real))
  :extrafuns ((x_45 Real))
  :extrafuns ((x_46 Real))
  :extrafuns ((x_47 Real))
  :extrafuns ((x_48 Real))
  :extrafuns ((x_49 Real))
  :extrafuns ((x_50 Real))
  :extrafuns ((x_51 Real))
  :extrafuns ((x_52 Real))
  :extrapreds ((x_53))
  :extrafuns ((x_54 Real))
  :extrafuns ((x_55 Real))
  :extrafuns ((x_56 Real))
  :formula
(let (?cvcl_26 (+ x_3 x_4)) (flet ($cvcl_71 (<= x_0 x_5)) (flet ($cvcl_54 (iff x_6 x_7)) (flet ($cvcl_10 (= x_8 0)) (flet ($cvcl_11 (< x_0 x_9)) (flet ($cvcl_38 (= x_5 x_0)) (flet ($cvcl_61 $cvcl_38) (flet ($cvcl_62 (= x_8 2)) (flet ($cvcl_64 (iff x_10 x_11)) (flet ($cvcl_65 (and (iff x_12 x_13) (iff x_14 x_15))) (flet ($cvcl_52 (iff x_16 x_17)) (flet ($cvcl_53 (and (iff x_18 x_19) (iff x_20 x_21))) (flet ($cvcl_66 (= x_22 x_23)) (flet ($cvcl_67 (and (= x_24 x_25) (= x_26 x_27))) (flet ($cvcl_21 (= x_28 x_9)) (flet ($cvcl_51 (iff x_29 x_30)) (flet ($cvcl_49 (iff x_31 x_32)) (flet ($cvcl_50 (and (iff x_33 x_34) (iff x_35 x_36))) (flet ($cvcl_68 (iff x_37 x_38)) (let (?cvcl_72 (- x_39 x_3)) (flet ($cvcl_42 (= x_8 1)) (let (?cvcl_46 (+ x_4 x_3)) (flet ($cvcl_41 (<= x_40 x_5)) (flet ($cvcl_48 (iff x_10 (or x_11  (and $cvcl_41 x_32) ))) (flet ($cvcl_28 (<= x_1 ?cvcl_26)) (flet ($cvcl_30 (<= x_2 ?cvcl_26)) (flet ($cvcl_22 (<= x_1 x_4)) (flet ($cvcl_27 $cvcl_22) (flet ($cvcl_24 (<= x_2 x_4)) (flet ($cvcl_29 $cvcl_24) (flet ($cvcl_23 (not x_13)) (flet ($cvcl_33 $cvcl_23) (flet ($cvcl_55 (< x_1 x_0)) (flet ($cvcl_56 (= x_5 x_1)) (flet ($cvcl_25 (not x_15)) (flet ($cvcl_35 $cvcl_25) (flet ($cvcl_57 (< x_2 x_0)) (flet ($cvcl_58 (= x_5 x_2)) (flet ($cvcl_14 (not x_11)) (flet ($cvcl_37 $cvcl_14) (flet ($cvcl_73 (not $cvcl_71)) (flet ($cvcl_32 (not x_34)) (flet ($cvcl_34 (not x_36)) (flet ($cvcl_36 (not x_32)) (flet ($cvcl_39 (and (not $cvcl_22) (<= x_1 x_5))) (flet ($cvcl_40 (and (not $cvcl_24) (<= x_2 x_5))) (flet ($cvcl_47 (and (iff x_12 (or x_13  (and $cvcl_39 x_34) )) (iff x_14 (or x_15  (and $cvcl_40 x_36) )))) (flet ($cvcl_31 (<= x_40 ?cvcl_26)) (flet ($cvcl_59 (< x_40 x_0)) (flet ($cvcl_60 (= x_5 x_40)) (flet ($cvcl_63 (<= (ite x_17 (ite x_21 (ite x_19 3 2) x_41) (ite x_21 x_41 (ite x_19 1 0))) (* (* (ite x_11 (ite x_15 (ite x_13 0 1) x_42) (ite x_15 x_42 (ite x_13 2 3))) 1) (/ 1 2)))) (flet ($cvcl_74 $cvcl_41) (flet ($cvcl_43 (not $cvcl_28)) (flet ($cvcl_44 (not $cvcl_30)) (flet ($cvcl_0 (and (not (<= x_40 x_4)) $cvcl_41)) (flet ($cvcl_1 $cvcl_0) (flet ($cvcl_4 (and (not (<= x_43 x_4)) (<= x_43 x_5))) (flet ($cvcl_2 $cvcl_4) (flet ($cvcl_5 $cvcl_0) (flet ($cvcl_6 $cvcl_4) (flet ($cvcl_45 (not $cvcl_31)) (flet ($cvcl_20 (= x_22 0)) (flet ($cvcl_9 (= x_22 3)) (flet ($cvcl_16 (= x_24 0)) (flet ($cvcl_7 (= x_24 3)) (flet ($cvcl_18 (= x_26 0)) (flet ($cvcl_8 (= x_26 3)) (flet ($cvcl_3 (and (not (<= x_46 x_4)) (<= x_46 x_5))) (flet ($cvcl_12 (= x_24 (ite $cvcl_23 (ite (and $cvcl_39 (< x_25 3)) (+ x_25 1) x_25) x_25))) (flet ($cvcl_13 (= x_26 (ite $cvcl_25 (ite (and $cvcl_40 (< x_27 3)) (+ x_27 1) x_27) x_27))) (flet ($cvcl_15 (or x_13  $cvcl_7 )) (flet ($cvcl_17 (or x_15  $cvcl_8 )) (flet ($cvcl_19 (or x_11  $cvcl_9 )) (flet ($cvcl_69 (= x_49 0)) (flet ($cvcl_70 (= x_49 1)) (flet ($cvcl_75 (<= x_39 x_50)) (flet ($cvcl_76 (<= x_39 x_51)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_49 2) (>= x_49 0)) (<= x_8 2)) (>= x_8 0)) (>= x_0 0)) (>= x_1 0)) (>= x_2 0)) (> x_3 0)) (>= x_3 0)) (>= x_4 0)) (>= x_5 0)) (>= x_9 0)) (or (or (or $cvcl_20  (= x_22 1) )  (= x_22 2) )  $cvcl_9 )) (not (< x_22 0))) (<= x_22 3)) (or (or (or (= x_23 0)  (= x_23 1) )  (= x_23 2) )  (= x_23 3) )) (not (< x_23 0))) (<= x_23 3)) (or (or (or $cvcl_16  (= x_24 1) )  (= x_24 2) )  $cvcl_7 )) (not (< x_24 0))) (<= x_24 3)) (or (or (or (= x_25 0)  (= x_25 1) )  (= x_25 2) )  (= x_25 3) )) (not (< x_25 0))) (<= x_25 3)) (or (or (or $cvcl_18  (= x_26 1) )  (= x_26 2) )  $cvcl_8 )) (not (< x_26 0))) (<= x_26 3)) (or (or (or (= x_27 0)  (= x_27 1) )  (= x_27 2) )  (= x_27 3) )) (not (< x_27 0))) (<= x_27 3)) (>= x_28 0)) (>= x_39 0)) (>= x_40 0)) (>= x_43 0)) (>= x_46 0)) (>= x_50 0)) (>= x_51 0)) (not (<= x_52 (* x_3 3)))) (>= x_52 0)) (>= x_54 0)) (>= x_55 0)) (>= x_56 0)) (not (<= x_0 x_1))) (not (<= x_0 x_2))) (< (- x_0 x_1) x_3)) (< (- x_0 x_2) x_3)) (= x_41 (ite x_19 2 1))) (= x_42 (ite x_13 1 2))) (= x_44 (ite $cvcl_1 2 1))) (= x_45 (ite $cvcl_5 2 1))) (= x_47 (+ (ite $cvcl_3 (ite $cvcl_2 (ite $cvcl_1 3 2) x_44) (ite $cvcl_2 x_44 (ite $cvcl_1 1 0))) x_23))) (= x_48 (+ (ite $cvcl_3 (ite $cvcl_6 (ite $cvcl_5 3 2) x_45) (ite $cvcl_6 x_45 (ite $cvcl_5 1 0))) x_23))) (or (or (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and $cvcl_10 $cvcl_11) $cvcl_38) $cvcl_12) $cvcl_13) (= x_22 (ite $cvcl_14 (ite (not (< x_47 3)) 3 x_47) x_23))) (iff x_12 $cvcl_15)) (iff x_14 $cvcl_17)) (iff x_10 $cvcl_19)) $cvcl_51) $cvcl_21)  (and (and (and (and (and (and (and (and (and (and $cvcl_10 (not $cvcl_11)) x_29) (= x_5 x_9)) $cvcl_12) $cvcl_13) (= x_22 (ite $cvcl_14 (ite (not (< x_48 3)) 3 x_48) x_23))) (iff x_12 (or $cvcl_15  $cvcl_16 ))) (iff x_14 (or $cvcl_17  $cvcl_18 ))) (iff x_10 (or $cvcl_19  $cvcl_20 ))) $cvcl_21) ) $cvcl_49) $cvcl_50) $cvcl_68) $cvcl_52) $cvcl_53) $cvcl_54)  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_42 (or (or (and (and (and (not $cvcl_27) $cvcl_33) $cvcl_32) $cvcl_28)  (and (and (and (not $cvcl_29) $cvcl_35) $cvcl_34) $cvcl_30) )  (and (and $cvcl_37 $cvcl_36) $cvcl_31) )) (not x_37)) (or (or (or (or $cvcl_27  $cvcl_43 )  x_34 )  x_13 )  (not (< x_5 x_1)) )) (or (or (or (or $cvcl_29  $cvcl_44 )  x_36 )  x_15 )  (not (< x_5 x_2)) )) (or (or (or $cvcl_45  x_32 )  x_11 )  (not (< x_5 x_40)) )) (or (or (or (and (and (and (and $cvcl_32 $cvcl_33) $cvcl_28) $cvcl_55) $cvcl_56)  (and (and (and (and $cvcl_34 $cvcl_35) $cvcl_30) $cvcl_57) $cvcl_58) )  (and (and (and (and $cvcl_36 $cvcl_37) $cvcl_31) $cvcl_59) $cvcl_60) )  (and (< x_0 ?cvcl_46) $cvcl_61) )) (iff x_33 (or x_34  $cvcl_39 ))) (iff x_35 (or x_36  $cvcl_40 ))) (iff x_31 (or x_32  $cvcl_41 ))) $cvcl_47) $cvcl_48)  (and (and (and (and (and (and (and (and (and $cvcl_42 (or (or (or $cvcl_27  x_34 )  x_13 )  $cvcl_43 )) (or (or (or $cvcl_29  x_36 )  x_15 )  $cvcl_44 )) (or (or x_32  x_11 )  $cvcl_45 )) x_37) (= x_5 ?cvcl_46)) $cvcl_47) $cvcl_48) $cvcl_49) $cvcl_50) ) $cvcl_66) $cvcl_67) $cvcl_21) $cvcl_51) $cvcl_52) $cvcl_53) $cvcl_54) )  (and (and (and (and (and (and (and (or (and (and (and (and (and (and (and (and (and (and (and $cvcl_62 $cvcl_63) (not x_6)) (or (or (or $cvcl_27  x_19 )  x_13 )  (<= x_5 x_1) )) (or (or (or $cvcl_29  x_21 )  x_15 )  (<= x_5 x_2) )) (or (or x_17  x_11 )  (<= x_5 x_40) )) (or (or (or (and (and (and (and (not x_19) $cvcl_33) (< x_4 x_1)) $cvcl_55) $cvcl_56)  (and (and (and (and (not x_21) $cvcl_35) (< x_4 x_2)) $cvcl_57) $cvcl_58) )  (and (and (and (not x_17) $cvcl_37) $cvcl_59) $cvcl_60) )  $cvcl_61 )) (iff x_18 (or x_19  (= x_1 x_5) ))) (iff x_20 (or x_21  (= x_2 x_5) ))) (iff x_16 (or x_17  (= x_40 x_5) ))) $cvcl_64) $cvcl_65)  (and (and (and (and (and (and (and $cvcl_62 (not $cvcl_63)) x_6) $cvcl_64) $cvcl_65) (= x_5 x_4)) $cvcl_52) $cvcl_53) ) $cvcl_66) $cvcl_67) $cvcl_21) $cvcl_51) $cvcl_49) $cvcl_50) $cvcl_68) )) (or (or (and $cvcl_69 (= x_8 (ite (not x_30) x_49 1)))  (and $cvcl_70 (= x_8 (ite (not x_38) x_49 2))) )  (and (and (not $cvcl_69) (not $cvcl_70)) (= x_8 x_49)) )) (or (and (and $cvcl_71 (not $cvcl_75)) (not (<= x_50 ?cvcl_72)))  (and $cvcl_73 (= x_50 x_1)) )) (or (and (and $cvcl_71 (not $cvcl_76)) (not (<= x_51 ?cvcl_72)))  (and $cvcl_73 (= x_51 x_2)) )) (or (and (and $cvcl_71 (= x_39 (+ x_0 x_52))) x_53)  (and (and $cvcl_73 (not x_53)) (= x_39 x_0)) )) (or (and (and (and (and $cvcl_74 (not (<= x_54 x_5))) (not (<= x_55 x_5))) (< x_54 x_55)) (< x_55 x_56))  (and (and (and (not $cvcl_74) (= x_54 x_40)) (= x_55 x_43)) (= x_56 x_46)) )) (or (or (or $cvcl_75  $cvcl_76 )  (not (< (- x_39 x_50) x_3)) )  (not (< (- x_39 x_51) x_3)) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)