theorem
  ?t1.0 \<in> {0..1} \<Longrightarrow>
  ?p1.0 = (1 - ?t1.0) *\<^sub>R fst ?l1.0 + ?t1.0 *\<^sub>R snd ?l1.0 \<Longrightarrow>
  fst (fst ?l1.0) < fst (snd ?l1.0) \<Longrightarrow>
  fst (fst ?l2.0) < fst (snd ?l2.0) \<Longrightarrow>
  fst (snd ?l1.0) < fst (fst ?l2.0) \<Longrightarrow>
  fst ((1 - ?t1.0) *\<^sub>R fst ?l1.0 + ?t1.0 *\<^sub>R snd ?l1.0) \<le> fst (snd ?l1.0) 
SMT: Assertions:
       \<forall>i l u. (i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)
       \<forall>i l u. (i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)
       \<forall>i l u. (i \<in> {l..u}) = (l \<le> i \<and> i \<le> u)
       \<forall>x y. fst (x + y) = fst x + fst y
       \<forall>x y. fst (x + y) = fst x + fst y
       \<forall>r A. fst (r *\<^sub>R A) = r *\<^sub>R fst A
       \<forall>r A. fst (r *\<^sub>R A) = r *\<^sub>R fst A
       \<forall>u a. (1 - u) *\<^sub>R a + u *\<^sub>R a = a
       \<forall>u a. (1 - u) *\<^sub>R a + u *\<^sub>R a = a
       \<forall>u a. (1 - u) *\<^sub>R a + u *\<^sub>R a = a
       \<forall>x y a. x \<le> y \<and> 0 \<le> a \<longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y
       \<forall>x y a. x \<le> y \<and> 0 \<le> a \<longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y
       \<forall>x y a. x \<le> y \<and> 0 \<le> a \<longrightarrow> a *\<^sub>R x \<le> a *\<^sub>R y
       t1 \<in> {0..1}
       p1 = (1 - t1) *\<^sub>R fst l1 + t1 *\<^sub>R snd l1
       fst (fst l1) < fst (snd l1)
       fst (fst l2) < fst (snd l2)
       fst (snd l1) < fst (fst l2)
       \<not> fst ((1 - t1) *\<^sub>R fst l1 + t1 *\<^sub>R snd l1) \<le> fst (snd l1) 
SMT: Names:
       sorts:
         Real_set$ = real set
         Real_real_prod$ = real \<times> real
         Real_real_prod_set$ = (real \<times> real) set
         Real_real_prod_real_real_prod_prod$ = (real \<times> real) \<times> real \<times> real
         Real_real_prod_real_real_prod_prod_set$ = ((real \<times> real) \<times> real \<times> real) set
       functions:
         l1$ = l1
         l2$ = l2
         p1$ = p1
         t1$ = t1
         fst$ = fst
         snd$ = snd
         fst$a = fst
         plus$ = (+)
         plus$a = (+)
         member$ = (\<in>)
         scaleR$ = (*\<^sub>R)
         less_eq$ = (\<le>)
         member$a = (\<in>)
         member$b = (\<in>)
         scaleR$a = (*\<^sub>R)
         scaleR$b = (*\<^sub>R)
         less_eq$a = (\<le>)
         atLeastAtMost$ = atLeastAtMost
         atLeastAtMost$a = atLeastAtMost
         atLeastAtMost$b = atLeastAtMost 
SMT: Problem:
       ; smt.random_seed=1 smt.refine_inj_axioms=false -T:20 -smt2
       (set-option :produce-proofs true)
       (set-logic AUFLIRA)
       (declare-sort Real_set$ 0)
       (declare-sort Real_real_prod$ 0)
       (declare-sort Real_real_prod_set$ 0)
       (declare-sort Real_real_prod_real_real_prod_prod$ 0)
       (declare-sort Real_real_prod_real_real_prod_prod_set$ 0)
       (declare-fun l1$ () Real_real_prod_real_real_prod_prod$)
       (declare-fun l2$ () Real_real_prod_real_real_prod_prod$)
       (declare-fun p1$ () Real_real_prod$)
       (declare-fun t1$ () Real)
       (declare-fun fst$ (Real_real_prod_real_real_prod_prod$) Real_real_prod$)
       (declare-fun snd$ (Real_real_prod_real_real_prod_prod$) Real_real_prod$)
       (declare-fun fst$a (Real_real_prod$) Real)
       (declare-fun plus$ (Real_real_prod_real_real_prod_prod$ Real_real_prod_real_real_prod_prod$) Real_real_prod_real_real_prod_prod$)
       (declare-fun plus$a (Real_real_prod$ Real_real_prod$) Real_real_prod$)
       (declare-fun member$ (Real_real_prod_real_real_prod_prod$ Real_real_prod_real_real_prod_prod_set$) Bool)
       (declare-fun scaleR$ (Real Real_real_prod_real_real_prod_prod$) Real_real_prod_real_real_prod_prod$)
       (declare-fun less_eq$ (Real_real_prod_real_real_prod_prod$ Real_real_prod_real_real_prod_prod$) Bool)
       (declare-fun member$a (Real_real_prod$ Real_real_prod_set$) Bool)
       (declare-fun member$b (Real Real_set$) Bool)
       (declare-fun scaleR$a (Real Real_real_prod$) Real_real_prod$)
       (declare-fun scaleR$b (Real Real) Real)
       (declare-fun less_eq$a (Real_real_prod$ Real_real_prod$) Bool)
       (declare-fun atLeastAtMost$ (Real_real_prod_real_real_prod_prod$ Real_real_prod_real_real_prod_prod$) Real_real_prod_real_real_prod_prod_set$)
       (declare-fun atLeastAtMost$a (Real_real_prod$ Real_real_prod$) Real_real_prod_set$)
       (declare-fun atLeastAtMost$b (Real Real) Real_set$)
       (assert (! (forall ((?v0 Real_real_prod_real_real_prod_prod$) (?v1 Real_real_prod_real_real_prod_prod$) (?v2 Real_real_prod_real_real_prod_prod$)) (= (member$ ?v0 (atLeastAtMost$ ?v1 ?v2)) (and (less_eq$ ?v1 ?v0) (less_eq$ ?v0 ?v2)))) :named a0))
       (assert (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod$) (?v2 Real_real_prod$)) (= (member$a ?v0 (atLeastAtMost$a ?v1 ?v2)) (and (less_eq$a ?v1 ?v0) (less_eq$a ?v0 ?v2)))) :named a1))
       (assert (! (forall ((?v0 Real) (?v1 Real) (?v2 Real)) (= (member$b ?v0 (atLeastAtMost$b ?v1 ?v2)) (and (<= ?v1 ?v0) (<= ?v0 ?v2)))) :named a2))
       (assert (! (forall ((?v0 Real_real_prod_real_real_prod_prod$) (?v1 Real_real_prod_real_real_prod_prod$)) (= (fst$ (plus$ ?v0 ?v1)) (plus$a (fst$ ?v0) (fst$ ?v1)))) :named a3))
       (assert (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod$)) (= (fst$a (plus$a ?v0 ?v1)) (+ (fst$a ?v0) (fst$a ?v1)))) :named a4))
       (assert (! (forall ((?v0 Real) (?v1 Real_real_prod_real_real_prod_prod$)) (= (fst$ (scaleR$ ?v0 ?v1)) (scaleR$a ?v0 (fst$ ?v1)))) :named a5))
       (assert (! (forall ((?v0 Real) (?v1 Real_real_prod$)) (= (fst$a (scaleR$a ?v0 ?v1)) (scaleR$b ?v0 (fst$a ?v1)))) :named a6))
       (assert (! (forall ((?v0 Real) (?v1 Real)) (= (+ (scaleR$b (- 1.0 ?v0) ?v1) (scaleR$b ?v0 ?v1)) ?v1)) :named a7))
       (assert (! (forall ((?v0 Real) (?v1 Real_real_prod_real_real_prod_prod$)) (= (plus$ (scaleR$ (- 1.0 ?v0) ?v1) (scaleR$ ?v0 ?v1)) ?v1)) :named a8))
       (assert (! (forall ((?v0 Real) (?v1 Real_real_prod$)) (= (plus$a (scaleR$a (- 1.0 ?v0) ?v1) (scaleR$a ?v0 ?v1)) ?v1)) :named a9))
       (assert (! (forall ((?v0 Real_real_prod_real_real_prod_prod$) (?v1 Real_real_prod_real_real_prod_prod$) (?v2 Real)) (=> (and (less_eq$ ?v0 ?v1) (<= 0.0 ?v2)) (less_eq$ (scaleR$ ?v2 ?v0) (scaleR$ ?v2 ?v1)))) :named a10))
       (assert (! (forall ((?v0 Real) (?v1 Real) (?v2 Real)) (=> (and (<= ?v0 ?v1) (<= 0.0 ?v2)) (<= (scaleR$b ?v2 ?v0) (scaleR$b ?v2 ?v1)))) :named a11))
       (assert (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod$) (?v2 Real)) (=> (and (less_eq$a ?v0 ?v1) (<= 0.0 ?v2)) (less_eq$a (scaleR$a ?v2 ?v0) (scaleR$a ?v2 ?v1)))) :named a12))
       (assert (! (member$b t1$ (atLeastAtMost$b 0.0 1.0)) :named a13))
       (assert (! (= p1$ (plus$a (scaleR$a (- 1.0 t1$) (fst$ l1$)) (scaleR$a t1$ (snd$ l1$)))) :named a14))
       (assert (! (< (fst$a (fst$ l1$)) (fst$a (snd$ l1$))) :named a15))
       (assert (! (< (fst$a (fst$ l2$)) (fst$a (snd$ l2$))) :named a16))
       (assert (! (< (fst$a (snd$ l1$)) (fst$a (fst$ l2$))) :named a17))
       (assert (! (not (<= (fst$a (plus$a (scaleR$a (- 1.0 t1$) (fst$ l1$)) (scaleR$a t1$ (snd$ l1$)))) (fst$a (snd$ l1$)))) :named a18))
       (check-sat)
       (get-proof)
        
SMT: Invoking SMT solver "z3" ... 
SMT: Solver: 
SMT: Result: 
SMT: Time (ms):
       300 
Solver z3: Solver "z3" failed -- enable tracing using the "smt_trace" option for details