Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/Isabelle/HOL/SMT_Examples/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Extended_Nonnegative_Real.thy Sprache: Isabelle

Anforderungen.certs Begriffe der KonzeptbildungText {Text[555] Haskell[591] CS[785]}Entwicklung

d4888d8ad473d347e6ab6d509244a7583a7babd4 17 0
unsat
(assume a0 (! (not (! (= (! (and p$ true) :named @p_1) p$) :named @p_3)) :named @p_5))
(step t2 (cl (= @p_1 (! (and p$) :named @p_2))) :rule and_simplify)
(step t3 (cl (= @p_2 p$)) :rule and_simplify)
(step t4 (cl @p_3) :rule trans :premises (t2 t3))
(step t5 (cl (= @p_3 (! (= p$ p$) :named @p_4))) :rule cong :premises (t4))
(step t6 (cl (= @p_4 true)) :rule equiv_simplify)
(step t7 (cl (= @p_3 true)) :rule trans :premises (t5 t6))
(step t8 (cl (= @p_5 (! (not true) :named @p_6))) :rule cong :premises (t7))
(step t9 (cl (= @p_6 false)) :rule not_simplify)
(step t10 (cl (! (= @p_5 false) :named @p_7)) :rule trans :premises (t8 t9))
(step t11 (cl (! (not @p_7) :named @p_9) (! (not @p_5) :named @p_8) false) :rule equiv_pos2)
(step t12 (cl (not @p_8) @p_3) :rule not_not)
(step t13 (cl @p_9 @p_3 false) :rule th_resolution :premises (t12 t11))
(step t14 (cl false) :rule th_resolution :premises (a0 t10 t13))
(step t15 (cl (not false)) :rule false)
(step t16 (cl) :rule resolution :premises (t14 t15))
95a654bfff554e647800fe77ff2ba30347402e24 9 0
unsat
(assume a0 (! (not true) :named @p_1))
(step t2 (cl (! (= @p_1 false) :named @p_2)) :rule not_simplify)
(step t3 (cl (! (not @p_2) :named @p_4) (! (not @p_1) :named @p_3) false) :rule equiv_pos2)
(step t4 (cl (not @p_3) true) :rule not_not)
(step t5 (cl @p_4 true false) :rule th_resolution :premises (t4 t3))
(step t6 (cl false) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (not false)) :rule false)
(step t8 (cl) :rule resolution :premises (t6 t7))
064ce4a7bbfaa11e79501270fc838c420c703181 12 0
unsat
(assume a0 (! (not (! (or p$ (not p$)) :named @p_1)) :named @p_2))
(step t2 (cl (= @p_1 true)) :rule or_simplify)
(step t3 (cl (= @p_2 (! (not true) :named @p_3))) :rule cong :premises (t2))
(step t4 (cl (= @p_3 false)) :rule not_simplify)
(step t5 (cl (! (= @p_2 false) :named @p_4)) :rule trans :premises (t3 t4))
(step t6 (cl (! (not @p_4) :named @p_6) (! (not @p_2) :named @p_5) false) :rule equiv_pos2)
(step t7 (cl (not @p_5) @p_1) :rule not_not)
(step t8 (cl @p_6 @p_1 false) :rule th_resolution :premises (t7 t6))
(step t9 (cl false) :rule th_resolution :premises (a0 t5 t8))
(step t10 (cl (not false)) :rule false)
(step t11 (cl) :rule resolution :premises (t9 t10))
10d84ea161ad298d0be18624997ac708a1f26ba1 12 0
unsat
(assume a0 (! (not (! (=> (! (or (and a$ b$) (and c$ d$)) :named @p_1) @p_1) :named @p_6)) :named @p_2))
(step t2 (cl (! (= @p_2 (! (and @p_1 (not @p_1)) :named @p_4)) :named @p_3)) :rule bool_simplify)
(step t3 (cl (! (not @p_3) :named @p_7) (! (not @p_2) :named @p_5) @p_4) :rule equiv_pos2)
(step t4 (cl (not @p_5) @p_6) :rule not_not)
(step t5 (cl @p_7 @p_6 @p_4) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_4) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (! (= @p_4 false) :named @p_8)) :rule and_simplify)
(step t8 (cl (not @p_8) (not @p_4) false) :rule equiv_pos2)
(step t9 (cl false) :rule th_resolution :premises (t6 t7 t8))
(step t10 (cl (not false)) :rule false)
(step t11 (cl) :rule resolution :premises (t9 t10))
9edc95cdafbdeeaebc87884ea4bcc53a0e812967 12 0
unsat
(assume a0 (! (not (! (=> (! (or (and p1$ p2$) p3$) :named @p_2) (! (or (! (=> p1$ (or (and p3$ p2$) (and p1$ p3$))) :named @p_10) p1$) :named @p_3)) :named @p_7)) :named @p_1))
(step t2 (cl (! (= @p_1 (! (and @p_2 (! (not @p_3) :named @p_9)) :named @p_5)) :named @p_4)) :rule bool_simplify)
(step t3 (cl (! (not @p_4) :named @p_8) (! (not @p_1) :named @p_6) @p_5) :rule equiv_pos2)
(step t4 (cl (not @p_6) @p_7) :rule not_not)
(step t5 (cl @p_8 @p_7 @p_5) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_5) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl @p_9) :rule and :premises (t6))
(step t8 (cl (not @p_10)) :rule not_or :premises (t7))
(step t9 (cl p1$) :rule not_implies1 :premises (t8))
(step t10 (cl (not p1$)) :rule not_or :premises (t7))
(step t11 (cl) :rule resolution :premises (t10 t9))
337e2bffaa7ce02e1ab772f593ffdbb243d5e449 15 0
unsat
(assume a0 (! (not (! (=> (! (and (! (or p$ q$) :named @p_8) (! (not p$) :named @p_9)) :named @p_2) q$) :named @p_6)) :named @p_1))
(step t2 (cl (! (= @p_1 (! (and @p_2 (! (not q$) :named @p_10)) :named @p_4)) :named @p_3)) :rule bool_simplify)
(step t3 (cl (! (not @p_3) :named @p_7) (! (not @p_1) :named @p_5) @p_4) :rule equiv_pos2)
(step t4 (cl (not @p_5) @p_6) :rule not_not)
(step t5 (cl @p_7 @p_6 @p_4) :rule th_resolution :premises (t4 t3))
(step t6 (cl @p_4) :rule th_resolution :premises (a0 t2 t5))
(step t7 (cl (! (= @p_4 (! (and @p_8 @p_9 @p_10) :named @p_12)) :named @p_11)) :rule ac_simp)
(step t8 (cl (not @p_11) (not @p_4) @p_12) :rule equiv_pos2)
(step t9 (cl @p_12) :rule th_resolution :premises (t6 t7 t8))
(step t10 (cl @p_8) :rule and :premises (t9))
(step t11 (cl p$ q$) :rule or :premises (t10))
(step t12 (cl @p_9) :rule and :premises (t9))
(step t13 (cl @p_10) :rule and :premises (t9))
(step t14 (cl) :rule resolution :premises (t11 t12 t13))
ef250e7a4e9499952e8416cff69ed029a37c7aa3 59 0
unsat
(assume a0 (! (or a$ (or b$ (or c$ d$))) :named @p_1))
(assume a2 (! (or (! (not (! (or a$ (! (and c$ (! (not c$) :named @p_40)) :named @p_4)) :named @p_5)) :named @p_8) b$) :named @p_9))
(assume a3 (! (or (! (not (! (and b$ (! (or x$ (not x$)) :named @p_13)) :named @p_14)) :named @p_17) c$) :named @p_18))
(assume a4 (! (or (! (not (! (or d$ false) :named @p_22)) :named @p_24) c$) :named @p_25))
(assume a5 (! (not (! (or c$ (! (and (! (not p$) :named @p_34) (! (or p$ (! (and q$ (not q$)) :named @p_29)) :named @p_30)) :named @p_33)) :named @p_36)) :named @p_39))
(step t6 (cl (! (= @p_1 (! (or a$ b$ c$ d$) :named @p_3)) :named @p_2)) :rule ac_simp)
(step t7 (cl (not @p_2) (not @p_1) @p_3) :rule equiv_pos2)
(step t8 (cl @p_3) :rule th_resolution :premises (a0 t6 t7))
(step t9 (cl (= @p_4 false)) :rule and_simplify)
(step t10 (cl (= @p_5 (! (or a$ false) :named @p_6))) :rule cong :premises (t9))
(step t11 (cl (= @p_6 (! (or a$) :named @p_7))) :rule or_simplify)
(step t12 (cl (= @p_7 a$)) :rule or_simplify)
(step t13 (cl (= @p_5 a$)) :rule trans :premises (t10 t11 t12))
(step t14 (cl (= @p_8 (! (not a$) :named @p_10))) :rule cong :premises (t13))
(step t15 (cl (! (= @p_9 (! (or @p_10 b$) :named @p_12)) :named @p_11)) :rule cong :premises (t14))
(step t16 (cl (not @p_11) (not @p_9) @p_12) :rule equiv_pos2)
(step t17 (cl @p_12) :rule th_resolution :premises (a2 t15 t16))
(step t18 (cl (= @p_13 true)) :rule or_simplify)
(step t19 (cl (= @p_14 (! (and b$ true) :named @p_15))) :rule cong :premises (t18))
(step t20 (cl (= @p_15 (! (and b$) :named @p_16))) :rule and_simplify)
(step t21 (cl (= @p_16 b$)) :rule and_simplify)
(step t22 (cl (= @p_14 b$)) :rule trans :premises (t19 t20 t21))
(step t23 (cl (= @p_17 (! (not b$) :named @p_19))) :rule cong :premises (t22))
(step t24 (cl (! (= @p_18 (! (or @p_19 c$) :named @p_21)) :named @p_20)) :rule cong :premises (t23))
(step t25 (cl (not @p_20) (not @p_18) @p_21) :rule equiv_pos2)
(step t26 (cl @p_21) :rule th_resolution :premises (a3 t24 t25))
(step t27 (cl (= @p_22 (! (or d$) :named @p_23))) :rule or_simplify)
(step t28 (cl (= @p_23 d$)) :rule or_simplify)
(step t29 (cl (= @p_22 d$)) :rule trans :premises (t27 t28))
(step t30 (cl (= @p_24 (! (not d$) :named @p_26))) :rule cong :premises (t29))
(step t31 (cl (! (= @p_25 (! (or @p_26 c$) :named @p_28)) :named @p_27)) :rule cong :premises (t30))
(step t32 (cl (not @p_27) (not @p_25) @p_28) :rule equiv_pos2)
(step t33 (cl @p_28) :rule th_resolution :premises (a4 t31 t32))
(step t34 (cl (= @p_29 false)) :rule and_simplify)
(step t35 (cl (= @p_30 (! (or p$ false) :named @p_31))) :rule cong :premises (t34))
(step t36 (cl (= @p_31 (! (or p$) :named @p_32))) :rule or_simplify)
(step t37 (cl (= @p_32 p$)) :rule or_simplify)
(step t38 (cl (= @p_30 p$)) :rule trans :premises (t35 t36 t37))
(step t39 (cl (= @p_33 (! (and @p_34 p$) :named @p_35))) :rule cong :premises (t38))
(step t40 (cl (= @p_35 false)) :rule and_simplify)
(step t41 (cl (= @p_33 false)) :rule trans :premises (t39 t40))
(step t42 (cl (= @p_36 (! (or c$ false) :named @p_37))) :rule cong :premises (t41))
(step t43 (cl (= @p_37 (! (or c$) :named @p_38))) :rule or_simplify)
(step t44 (cl (= @p_38 c$)) :rule or_simplify)
(step t45 (cl (= @p_36 c$)) :rule trans :premises (t42 t43 t44))
(step t46 (cl (! (= @p_39 @p_40) :named @p_41)) :rule cong :premises (t45))
(step t47 (cl (! (not @p_41) :named @p_43) (! (not @p_39) :named @p_42) @p_40) :rule equiv_pos2)
(step t48 (cl (not @p_42) @p_36) :rule not_not)
(step t49 (cl @p_43 @p_36 @p_40) :rule th_resolution :premises (t48 t47))
(step t50 (cl @p_40) :rule th_resolution :premises (a5 t46 t49))
(step t51 (cl a$ b$ c$ d$) :rule or :premises (t8))
(step t52 (cl @p_10 b$) :rule or :premises (t17))
(step t53 (cl @p_19 c$) :rule or :premises (t26))
(step t54 (cl @p_26 c$) :rule or :premises (t33))
(step t55 (cl @p_19) :rule resolution :premises (t53 t50))
(step t56 (cl @p_26) :rule resolution :premises (t54 t50))
(step t57 (cl a$) :rule resolution :premises (t51 t55 t50 t56))
(step t58 (cl) :rule resolution :premises (t52 t55 t57))
f8dcc171fd9ab79494da2e1c5e4771e075fd9d51 29 0
unsat
(assume a0 (! (not (! (= (! (= (! (= (! (= (! (= (! (= (! (= (! (= (! (= p$ p$) :named @p_1) p$) :named @p_2) p$) :named @p_4) p$) :named @p_5) p$) :named @p_6) p$) :named @p_7) p$) :named @p_8) p$) :named @p_9) p$) :named @p_10)) :named @p_11))
(step t2 (cl (= @p_1 true)) :rule equiv_simplify)
(step t3 (cl (= @p_2 (! (= true p$) :named @p_3))) :rule cong :premises (t2))
(step t4 (cl (= @p_3 p$)) :rule equiv_simplify)
(step t5 (cl @p_4) :rule trans :premises (t3 t4))
(step t6 (cl (= @p_4 @p_1)) :rule cong :premises (t5))
(step t7 (cl (= @p_4 true)) :rule trans :premises (t6 t2))
(step t8 (cl (= @p_5 @p_3)) :rule cong :premises (t7))
(step t9 (cl @p_6) :rule trans :premises (t8 t4))
(step t10 (cl (= @p_6 @p_1)) :rule cong :premises (t9))
(step t11 (cl (= @p_6 true)) :rule trans :premises (t10 t2))
(step t12 (cl (= @p_7 @p_3)) :rule cong :premises (t11))
(step t13 (cl @p_8) :rule trans :premises (t12 t4))
(step t14 (cl (= @p_8 @p_1)) :rule cong :premises (t13))
(step t15 (cl (= @p_8 true)) :rule trans :premises (t14 t2))
(step t16 (cl (= @p_9 @p_3)) :rule cong :premises (t15))
(step t17 (cl @p_10) :rule trans :premises (t16 t4))
(step t18 (cl (= @p_10 @p_1)) :rule cong :premises (t17))
(step t19 (cl (= @p_10 true)) :rule trans :premises (t18 t2))
(step t20 (cl (= @p_11 (! (not true) :named @p_12))) :rule cong :premises (t19))
(step t21 (cl (= @p_12 false)) :rule not_simplify)
(step t22 (cl (! (= @p_11 false) :named @p_13)) :rule trans :premises (t20 t21))
(step t23 (cl (! (not @p_13) :named @p_15) (! (not @p_11) :named @p_14) false) :rule equiv_pos2)
(step t24 (cl (not @p_14) @p_10) :rule not_not)
(step t25 (cl @p_15 @p_10 false) :rule th_resolution :premises (t24 t23))
(step t26 (cl false) :rule th_resolution :premises (a0 t22 t25))
(step t27 (cl (not false)) :rule false)
(step t28 (cl) :rule resolution :premises (t26 t27))
a331481eed4f18a666baadda4e1010ca7a295ccf 38 0
unsat
(assume a0 (! (forall ((?v0 A$) (?v1 A$)) (! (= (! (symm_f$ ?v0 ?v1) :named @p_2) (! (symm_f$ ?v1 ?v0) :named @p_6)) :named @p_8)) :named @p_1))
(assume a1 (! (not (! (and (! (= a$ a$) :named @p_19) (! (= (symm_f$ a$ b$) (symm_f$ b$ a$)) :named @p_21)) :named @p_20)) :named @p_24))
(anchor :step t3 :args ((:= ?v0 veriT_vr0) (:= ?v1 veriT_vr1)))
(step t3.t1 (cl (! (= ?v0 veriT_vr0) :named @p_5)) :rule refl)
(step t3.t2 (cl (! (= ?v1 veriT_vr1) :named @p_4)) :rule refl)
(step t3.t3 (cl (= @p_2 (! (symm_f$ veriT_vr0 veriT_vr1) :named @p_3))) :rule cong :premises (t3.t1 t3.t2))
(step t3.t4 (cl @p_4) :rule refl)
(step t3.t5 (cl @p_5) :rule refl)
(step t3.t6 (cl (= @p_6 (! (symm_f$ veriT_vr1 veriT_vr0) :named @p_7))) :rule cong :premises (t3.t4 t3.t5))
(step t3.t7 (cl (= @p_8 (! (= @p_3 @p_7) :named @p_9))) :rule cong :premises (t3.t3 t3.t6))
(step t3 (cl (! (= @p_1 (! (forall ((veriT_vr0 A$) (veriT_vr1 A$)) @p_9) :named @p_11)) :named @p_10)) :rule bind)
(step t4 (cl (not @p_10) (not @p_1) @p_11) :rule equiv_pos2)
(step t5 (cl @p_11) :rule th_resolution :premises (a0 t3 t4))
(anchor :step t6 :args ((:= veriT_vr0 veriT_vr2) (:= veriT_vr1 veriT_vr3)))
(step t6.t1 (cl (! (= veriT_vr0 veriT_vr2) :named @p_14)) :rule refl)
(step t6.t2 (cl (! (= veriT_vr1 veriT_vr3) :named @p_13)) :rule refl)
(step t6.t3 (cl (= @p_3 (! (symm_f$ veriT_vr2 veriT_vr3) :named @p_12))) :rule cong :premises (t6.t1 t6.t2))
(step t6.t4 (cl @p_13) :rule refl)
(step t6.t5 (cl @p_14) :rule refl)
(step t6.t6 (cl (= @p_7 (! (symm_f$ veriT_vr3 veriT_vr2) :named @p_15))) :rule cong :premises (t6.t4 t6.t5))
(step t6.t7 (cl (= @p_9 (! (= @p_12 @p_15) :named @p_16))) :rule cong :premises (t6.t3 t6.t6))
(step t6 (cl (! (= @p_11 (! (forall ((veriT_vr2 A$) (veriT_vr3 A$)) @p_16) :named @p_18)) :named @p_17)) :rule bind)
(step t7 (cl (not @p_17) (not @p_11) @p_18) :rule equiv_pos2)
(step t8 (cl @p_18) :rule th_resolution :premises (t5 t6 t7))
(step t9 (cl (= @p_19 true)) :rule eq_simplify)
(step t10 (cl (= @p_20 (! (and true @p_21) :named @p_22))) :rule cong :premises (t9))
(step t11 (cl (= @p_22 (! (and @p_21) :named @p_23))) :rule and_simplify)
(step t12 (cl (= @p_23 @p_21)) :rule and_simplify)
(step t13 (cl (= @p_20 @p_21)) :rule trans :premises (t10 t11 t12))
(step t14 (cl (! (= @p_24 (! (not @p_21) :named @p_26)) :named @p_25)) :rule cong :premises (t13))
(step t15 (cl (! (not @p_25) :named @p_28) (! (not @p_24) :named @p_27) @p_26) :rule equiv_pos2)
(step t16 (cl (not @p_27) @p_20) :rule not_not)
(step t17 (cl @p_28 @p_20 @p_26) :rule th_resolution :premises (t16 t15))
(step t18 (cl @p_26) :rule th_resolution :premises (a1 t14 t17))
(step t19 (cl (or (! (not @p_18) :named @p_29) @p_21)) :rule forall_inst :args ((:= veriT_vr2 a$) (:= veriT_vr3 b$)))
(step t20 (cl @p_29 @p_21) :rule or :premises (t19))
(step t21 (cl) :rule resolution :premises (t20 t8 t18))
8616c6debd3ebae49adf8409b8c1ecb6665bc881 654 0
unsat
(assume a0 (! (forall ((?v0 Int)) (! (= (! (fun_app$ uua$ ?v0) :named @p_13) (! (line_integral_exists$ f$ (! (insert$ j$ bot$) :named @p_7)) :named @p_12)) :named @p_15)) :named @p_11))
(assume a1 (! (forall ((?v0 Int)) (! (= (! (fun_app$ uu$ ?v0) :named @p_25) (! (line_integral_exists$ f$ (! (insert$ i$ bot$) :named @p_5)) :named @p_24)) :named @p_27)) :named @p_23))
(assume a2 (! (forall ((?v0 Int_real_real_real_prod_fun_bool_fun_fun$) (?v1 Int_real_real_real_prod_fun_prod$)) (! (= (! (case_prod$ ?v0 ?v1) :named @p_36) (! (fun_app$a (! (fun_app$ ?v0 (! (fst$ ?v1) :named @p_40)) :named @p_42) (! (snd$ ?v1) :named @p_44)) :named @p_46)) :named @p_48)) :named @p_35))
(assume a3 (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod$)) (! (=> (! (= (! (insert$ ?v0 bot$) :named @p_3) (! (insert$ ?v1 bot$) :named @p_64)) :named @p_66) (! (= ?v0 ?v1) :named @p_70)) :named @p_72)) :named @p_62))
(assume a4 (! (forall ((?v0 Int) (?v1 Real_real_real_prod_fun$)) (! (= ?v1 (! (snd$ (! (pair$ ?v0 ?v1) :named @p_87)) :named @p_89)) :named @p_91)) :named @p_85))
(assume a5 (! (forall ((?v0 Real) (?v1 Real)) (! (= ?v1 (! (snd$a (! (fun_app$b (! (pair$a ?v0) :named @p_102) ?v1) :named @p_105)) :named @p_107)) :named @p_109)) :named @p_101))
(assume a6 (! (member$ (! (pair$ k$ g$) :named @p_403) one_chain_typeI$) :named @p_402))
(assume a7 (! (forall ((?v0 Real_real_prod_set$) (?v1 Real_real_prod$) (?v2 Real_real_prod_set$)) (! (= (! (= bot$ (! (inf$ ?v0 (! (insert$ ?v1 ?v2) :named @p_1)) :named @p_122)) :named @p_124) (! (and (! (not (! (member$a ?v1 ?v0) :named @p_128)) :named @p_130) (! (= bot$ (! (inf$ ?v0 ?v2) :named @p_133)) :named @p_135)) :named @p_137)) :named @p_139)) :named @p_120))
(assume a8 (! (finite$ bot$) :named @p_414))
(assume a9 (! (forall ((?v0 Real_real_prod_set$) (?v1 Real_real_prod$)) (! (=> (! (finite$ ?v0) :named @p_4) (! (finite$ (! (insert$ ?v1 ?v0) :named @p_160)) :named @p_162)) :named @p_164)) :named @p_157))
(assume a10 (! (= i$ (! (fun_app$b (pair$a 1.0) 0.0) :named @p_417)) :named @p_499))
(assume a11 (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod_set$)) (! (=> (! (member$a ?v0 ?v1) :named @p_176) (! (= ?v1 (! (insert$ ?v0 ?v1) :named @p_2)) :named @p_181)) :named @p_183)) :named @p_175))
(assume a12 (! (= j$ (! (fun_app$b (pair$a 0.0) 1.0) :named @p_419)) :named @p_500))
(assume a13 (! (forall ((?v0 Real_real_prod_set$)) (! (= bot$ (! (inf$ ?v0 bot$) :named @p_196)) :named @p_198)) :named @p_195))
(assume a14 (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod$) (?v2 Real_real_prod_set$)) (! (= (! (insert$ ?v0 @p_1) :named @p_208) (! (insert$ ?v1 (! (insert$ ?v0 ?v2) :named @p_213)) :named @p_215)) :named @p_217)) :named @p_206))
(assume a15 (! (forall ((?v0 Real_real_prod$) (?v1 Real_real_prod_set$)) (! (= @p_2 (! (sup$ @p_3 ?v1) :named @p_236)) :named @p_238)) :named @p_231))
(assume a16 (! (forall ((?v0 Real_real_prod_set$) (?v1 Real_real_prod_real_real_prod_fun$) (?v2 Real_real_prod_set$) (?v3 Real_real_real_prod_fun$) (?v4 Real_real_prod_set$)) (! (=> (! (and @p_4 (! (and (! (fun_app$a (! (line_integral_exists$ ?v1 ?v2) :named @p_252) ?v3) :named @p_254) (! (and (! (fun_app$a (! (line_integral_exists$ ?v1 ?v4) :named @p_257) ?v3) :named @p_260) (! (and (! (= ?v0 (! (sup$ ?v2 ?v4) :named @p_265)) :named @p_267) (! (= bot$ (! (inf$ ?v2 ?v4) :named @p_269)) :named @p_271)) :named @p_273)) :named @p_275)) :named @p_277)) :named @p_279) (! (= (! (line_integral$ ?v1 ?v0 ?v3) :named @p_281) (! (+ (! (line_integral$ ?v1 ?v2 ?v3) :named @p_283) (! (line_integral$ ?v1 ?v4 ?v3) :named @p_285)) :named @p_287)) :named @p_289)) :named @p_291)) :named @p_250))
(assume a17 (! (and (! (= (one_chain_line_integral$ f$ @p_5 one_chain_typeI$) (one_chain_line_integral$ f$ @p_5 one_chain_typeII$)) :named @p_337) (! (and (! (forall ((?v0 Int_real_real_real_prod_fun_prod$)) (! (=> (! (member$ ?v0 one_chain_typeI$) :named @p_9) (! (case_prod$ uu$ ?v0) :named @p_6)) :named @p_326)) :named @p_322) (! (forall ((?v0 Int_real_real_real_prod_fun_prod$)) (! (=> (! (member$ ?v0 one_chain_typeII$) :named @p_8) @p_6) :named @p_331)) :named @p_328)) :named @p_333)) :named @p_336))
(assume a18 (! (and (! (= (one_chain_line_integral$ f$ @p_7 one_chain_typeII$) (one_chain_line_integral$ f$ @p_7 one_chain_typeI$)) :named @p_377) (! (and (! (forall ((?v0 Int_real_real_real_prod_fun_prod$)) (! (=> @p_8 (! (case_prod$ uua$ ?v0) :named @p_10)) :named @p_366)) :named @p_362) (! (forall ((?v0 Int_real_real_real_prod_fun_prod$)) (! (=> @p_9 @p_10) :named @p_371)) :named @p_368)) :named @p_373)) :named @p_376))
(assume a19 (not (! (= (! (line_integral$ f$ (! (insert$ i$ @p_7) :named @p_407) g$) :named @p_462) (! (+ (! (line_integral$ f$ @p_5 g$) :named @p_404) (! (line_integral$ f$ @p_7 g$) :named @p_405)) :named @p_463)) :named @p_410)))
(anchor :step t21 :args ((:= ?v0 veriT_vr0)))
(step t21.t1 (cl (= ?v0 veriT_vr0)) :rule refl)
(step t21.t2 (cl (= @p_13 (! (fun_app$ uua$ veriT_vr0) :named @p_14))) :rule cong :premises (t21.t1))
(step t21.t3 (cl (= @p_15 (! (= @p_12 @p_14) :named @p_16))) :rule cong :premises (t21.t2))
(step t21 (cl (! (= @p_11 (! (forall ((veriT_vr0 Int)) @p_16) :named @p_18)) :named @p_17)) :rule bind)
(step t22 (cl (not @p_17) (not @p_11) @p_18) :rule equiv_pos2)
(step t23 (cl @p_18) :rule th_resolution :premises (a0 t21 t22))
(anchor :step t24 :args ((:= veriT_vr0 veriT_vr1)))
(step t24.t1 (cl (= veriT_vr0 veriT_vr1)) :rule refl)
(step t24.t2 (cl (= @p_14 (! (fun_app$ uua$ veriT_vr1) :named @p_19))) :rule cong :premises (t24.t1))
(step t24.t3 (cl (= @p_16 (! (= @p_12 @p_19) :named @p_20))) :rule cong :premises (t24.t2))
(step t24 (cl (! (= @p_18 (! (forall ((veriT_vr1 Int)) @p_20) :named @p_22)) :named @p_21)) :rule bind)
(step t25 (cl (not @p_21) (not @p_18) @p_22) :rule equiv_pos2)
(step t26 (cl @p_22) :rule th_resolution :premises (t23 t24 t25))
(anchor :step t27 :args ((:= ?v0 veriT_vr2)))
(step t27.t1 (cl (= ?v0 veriT_vr2)) :rule refl)
(step t27.t2 (cl (= @p_25 (! (fun_app$ uu$ veriT_vr2) :named @p_26))) :rule cong :premises (t27.t1))
(step t27.t3 (cl (= @p_27 (! (= @p_24 @p_26) :named @p_28))) :rule cong :premises (t27.t2))
(step t27 (cl (! (= @p_23 (! (forall ((veriT_vr2 Int)) @p_28) :named @p_30)) :named @p_29)) :rule bind)
(step t28 (cl (not @p_29) (not @p_23) @p_30) :rule equiv_pos2)
(step t29 (cl @p_30) :rule th_resolution :premises (a1 t27 t28))
(anchor :step t30 :args ((:= veriT_vr2 veriT_vr3)))
(step t30.t1 (cl (= veriT_vr2 veriT_vr3)) :rule refl)
(step t30.t2 (cl (= @p_26 (! (fun_app$ uu$ veriT_vr3) :named @p_31))) :rule cong :premises (t30.t1))
(step t30.t3 (cl (= @p_28 (! (= @p_24 @p_31) :named @p_32))) :rule cong :premises (t30.t2))
(step t30 (cl (! (= @p_30 (! (forall ((veriT_vr3 Int)) @p_32) :named @p_34)) :named @p_33)) :rule bind)
(step t31 (cl (not @p_33) (not @p_30) @p_34) :rule equiv_pos2)
(step t32 (cl @p_34) :rule th_resolution :premises (t29 t30 t31))
(anchor :step t33 :args ((:= ?v0 veriT_vr4) (:= ?v1 veriT_vr5)))
(step t33.t1 (cl (! (= ?v0 veriT_vr4) :named @p_38)) :rule refl)
(step t33.t2 (cl (! (= ?v1 veriT_vr5) :named @p_39)) :rule refl)
(step t33.t3 (cl (= @p_36 (! (case_prod$ veriT_vr4 veriT_vr5) :named @p_37))) :rule cong :premises (t33.t1 t33.t2))
(step t33.t4 (cl @p_38) :rule refl)
(step t33.t5 (cl @p_39) :rule refl)
(step t33.t6 (cl (= @p_40 (! (fst$ veriT_vr5) :named @p_41))) :rule cong :premises (t33.t5))
(step t33.t7 (cl (= @p_42 (! (fun_app$ veriT_vr4 @p_41) :named @p_43))) :rule cong :premises (t33.t4 t33.t6))
(step t33.t8 (cl @p_39) :rule refl)
(step t33.t9 (cl (= @p_44 (! (snd$ veriT_vr5) :named @p_45))) :rule cong :premises (t33.t8))
(step t33.t10 (cl (= @p_46 (! (fun_app$a @p_43 @p_45) :named @p_47))) :rule cong :premises (t33.t7 t33.t9))
(step t33.t11 (cl (= @p_48 (! (= @p_37 @p_47) :named @p_49))) :rule cong :premises (t33.t3 t33.t10))
(step t33 (cl (! (= @p_35 (! (forall ((veriT_vr4 Int_real_real_real_prod_fun_bool_fun_fun$) (veriT_vr5 Int_real_real_real_prod_fun_prod$)) @p_49) :named @p_51)) :named @p_50)) :rule bind)
(step t34 (cl (not @p_50) (not @p_35) @p_51) :rule equiv_pos2)
(step t35 (cl @p_51) :rule th_resolution :premises (a2 t33 t34))
(anchor :step t36 :args ((:= veriT_vr4 veriT_vr6) (:= veriT_vr5 veriT_vr7)))
(step t36.t1 (cl (! (= veriT_vr4 veriT_vr6) :named @p_53)) :rule refl)
(step t36.t2 (cl (! (= veriT_vr5 veriT_vr7) :named @p_54)) :rule refl)
(step t36.t3 (cl (= @p_37 (! (case_prod$ veriT_vr6 veriT_vr7) :named @p_52))) :rule cong :premises (t36.t1 t36.t2))
(step t36.t4 (cl @p_53) :rule refl)
(step t36.t5 (cl @p_54) :rule refl)
(step t36.t6 (cl (= @p_41 (! (fst$ veriT_vr7) :named @p_55))) :rule cong :premises (t36.t5))
(step t36.t7 (cl (= @p_43 (! (fun_app$ veriT_vr6 @p_55) :named @p_56))) :rule cong :premises (t36.t4 t36.t6))
(step t36.t8 (cl @p_54) :rule refl)
(step t36.t9 (cl (= @p_45 (! (snd$ veriT_vr7) :named @p_57))) :rule cong :premises (t36.t8))
(step t36.t10 (cl (= @p_47 (! (fun_app$a @p_56 @p_57) :named @p_58))) :rule cong :premises (t36.t7 t36.t9))
(step t36.t11 (cl (= @p_49 (! (= @p_52 @p_58) :named @p_59))) :rule cong :premises (t36.t3 t36.t10))
(step t36 (cl (! (= @p_51 (! (forall ((veriT_vr6 Int_real_real_real_prod_fun_bool_fun_fun$) (veriT_vr7 Int_real_real_real_prod_fun_prod$)) @p_59) :named @p_61)) :named @p_60)) :rule bind)
(step t37 (cl (not @p_60) (not @p_51) @p_61) :rule equiv_pos2)
(step t38 (cl @p_61) :rule th_resolution :premises (t35 t36 t37))
(anchor :step t39 :args ((:= ?v0 veriT_vr8) (:= ?v1 veriT_vr9)))
(step t39.t1 (cl (! (= ?v0 veriT_vr8) :named @p_68)) :rule refl)
(step t39.t2 (cl (= @p_3 (! (insert$ veriT_vr8 bot$) :named @p_63))) :rule cong :premises (t39.t1))
(step t39.t3 (cl (! (= ?v1 veriT_vr9) :named @p_69)) :rule refl)
(step t39.t4 (cl (= @p_64 (! (insert$ veriT_vr9 bot$) :named @p_65))) :rule cong :premises (t39.t3))
(step t39.t5 (cl (= @p_66 (! (= @p_63 @p_65) :named @p_67))) :rule cong :premises (t39.t2 t39.t4))
(step t39.t6 (cl @p_68) :rule refl)
(step t39.t7 (cl @p_69) :rule refl)
(step t39.t8 (cl (= @p_70 (! (= veriT_vr8 veriT_vr9) :named @p_71))) :rule cong :premises (t39.t6 t39.t7))
(step t39.t9 (cl (= @p_72 (! (=> @p_67 @p_71) :named @p_73))) :rule cong :premises (t39.t5 t39.t8))
(step t39 (cl (! (= @p_62 (! (forall ((veriT_vr8 Real_real_prod$) (veriT_vr9 Real_real_prod$)) @p_73) :named @p_75)) :named @p_74)) :rule bind)
(step t40 (cl (not @p_74) (not @p_62) @p_75) :rule equiv_pos2)
(step t41 (cl @p_75) :rule th_resolution :premises (a3 t39 t40))
(anchor :step t42 :args ((:= veriT_vr8 veriT_vr10) (:= veriT_vr9 veriT_vr11)))
(step t42.t1 (cl (! (= veriT_vr8 veriT_vr10) :named @p_79)) :rule refl)
(step t42.t2 (cl (= @p_63 (! (insert$ veriT_vr10 bot$) :named @p_76))) :rule cong :premises (t42.t1))
(step t42.t3 (cl (! (= veriT_vr9 veriT_vr11) :named @p_80)) :rule refl)
(step t42.t4 (cl (= @p_65 (! (insert$ veriT_vr11 bot$) :named @p_77))) :rule cong :premises (t42.t3))
(step t42.t5 (cl (= @p_67 (! (= @p_76 @p_77) :named @p_78))) :rule cong :premises (t42.t2 t42.t4))
(step t42.t6 (cl @p_79) :rule refl)
(step t42.t7 (cl @p_80) :rule refl)
(step t42.t8 (cl (= @p_71 (! (= veriT_vr10 veriT_vr11) :named @p_81))) :rule cong :premises (t42.t6 t42.t7))
(step t42.t9 (cl (= @p_73 (! (=> @p_78 @p_81) :named @p_82))) :rule cong :premises (t42.t5 t42.t8))
(step t42 (cl (! (= @p_75 (! (forall ((veriT_vr10 Real_real_prod$) (veriT_vr11 Real_real_prod$)) @p_82) :named @p_84)) :named @p_83)) :rule bind)
(step t43 (cl (not @p_83) (not @p_75) @p_84) :rule equiv_pos2)
(step t44 (cl @p_84) :rule th_resolution :premises (t41 t42 t43))
(anchor :step t45 :args ((:= ?v0 veriT_vr12) (:= ?v1 veriT_vr13)))
(step t45.t1 (cl (! (= ?v1 veriT_vr13) :named @p_86)) :rule refl)
(step t45.t2 (cl (= ?v0 veriT_vr12)) :rule refl)
(step t45.t3 (cl @p_86) :rule refl)
(step t45.t4 (cl (= @p_87 (! (pair$ veriT_vr12 veriT_vr13) :named @p_88))) :rule cong :premises (t45.t2 t45.t3))
(step t45.t5 (cl (= @p_89 (! (snd$ @p_88) :named @p_90))) :rule cong :premises (t45.t4))
(step t45.t6 (cl (= @p_91 (! (= veriT_vr13 @p_90) :named @p_92))) :rule cong :premises (t45.t1 t45.t5))
(step t45 (cl (! (= @p_85 (! (forall ((veriT_vr12 Int) (veriT_vr13 Real_real_real_prod_fun$)) @p_92) :named @p_94)) :named @p_93)) :rule bind)
(step t46 (cl (not @p_93) (not @p_85) @p_94) :rule equiv_pos2)
(step t47 (cl @p_94) :rule th_resolution :premises (a4 t45 t46))
(anchor :step t48 :args ((:= veriT_vr12 veriT_vr14) (:= veriT_vr13 veriT_vr15)))
(step t48.t1 (cl (! (= veriT_vr13 veriT_vr15) :named @p_95)) :rule refl)
(step t48.t2 (cl (= veriT_vr12 veriT_vr14)) :rule refl)
(step t48.t3 (cl @p_95) :rule refl)
(step t48.t4 (cl (= @p_88 (! (pair$ veriT_vr14 veriT_vr15) :named @p_96))) :rule cong :premises (t48.t2 t48.t3))
(step t48.t5 (cl (= @p_90 (! (snd$ @p_96) :named @p_97))) :rule cong :premises (t48.t4))
(step t48.t6 (cl (= @p_92 (! (= veriT_vr15 @p_97) :named @p_98))) :rule cong :premises (t48.t1 t48.t5))
(step t48 (cl (! (= @p_94 (! (forall ((veriT_vr14 Int) (veriT_vr15 Real_real_real_prod_fun$)) @p_98) :named @p_100)) :named @p_99)) :rule bind)
(step t49 (cl (not @p_99) (not @p_94) @p_100) :rule equiv_pos2)
(step t50 (cl @p_100) :rule th_resolution :premises (t47 t48 t49))
(anchor :step t51 :args ((:= ?v0 veriT_vr16) (:= ?v1 veriT_vr17)))
(step t51.t1 (cl (! (= ?v1 veriT_vr17) :named @p_104)) :rule refl)
(step t51.t2 (cl (= ?v0 veriT_vr16)) :rule refl)
(step t51.t3 (cl (= @p_102 (! (pair$a veriT_vr16) :named @p_103))) :rule cong :premises (t51.t2))
(step t51.t4 (cl @p_104) :rule refl)
(step t51.t5 (cl (= @p_105 (! (fun_app$b @p_103 veriT_vr17) :named @p_106))) :rule cong :premises (t51.t3 t51.t4))
(step t51.t6 (cl (= @p_107 (! (snd$a @p_106) :named @p_108))) :rule cong :premises (t51.t5))
(step t51.t7 (cl (= @p_109 (! (= veriT_vr17 @p_108) :named @p_110))) :rule cong :premises (t51.t1 t51.t6))
(step t51 (cl (! (= @p_101 (! (forall ((veriT_vr16 Real) (veriT_vr17 Real)) @p_110) :named @p_112)) :named @p_111)) :rule bind)
(step t52 (cl (not @p_111) (not @p_101) @p_112) :rule equiv_pos2)
(step t53 (cl @p_112) :rule th_resolution :premises (a5 t51 t52))
(anchor :step t54 :args ((:= veriT_vr16 veriT_vr18) (:= veriT_vr17 veriT_vr19)))
(step t54.t1 (cl (! (= veriT_vr17 veriT_vr19) :named @p_114)) :rule refl)
(step t54.t2 (cl (= veriT_vr16 veriT_vr18)) :rule refl)
(step t54.t3 (cl (= @p_103 (! (pair$a veriT_vr18) :named @p_113))) :rule cong :premises (t54.t2))
(step t54.t4 (cl @p_114) :rule refl)
(step t54.t5 (cl (= @p_106 (! (fun_app$b @p_113 veriT_vr19) :named @p_115))) :rule cong :premises (t54.t3 t54.t4))
(step t54.t6 (cl (= @p_108 (! (snd$a @p_115) :named @p_116))) :rule cong :premises (t54.t5))
(step t54.t7 (cl (= @p_110 (! (= veriT_vr19 @p_116) :named @p_117))) :rule cong :premises (t54.t1 t54.t6))
(step t54 (cl (! (= @p_112 (! (forall ((veriT_vr18 Real) (veriT_vr19 Real)) @p_117) :named @p_119)) :named @p_118)) :rule bind)
(step t55 (cl (not @p_118) (not @p_112) @p_119) :rule equiv_pos2)
(step t56 (cl @p_119) :rule th_resolution :premises (t53 t54 t55))
(anchor :step t57 :args ((:= ?v0 veriT_vr20) (:= ?v1 veriT_vr21) (:= ?v2 veriT_vr22)))
(step t57.t1 (cl (! (= ?v0 veriT_vr20) :named @p_127)) :rule refl)
(step t57.t2 (cl (! (= ?v1 veriT_vr21) :named @p_126)) :rule refl)
(step t57.t3 (cl (! (= ?v2 veriT_vr22) :named @p_132)) :rule refl)
(step t57.t4 (cl (= @p_1 (! (insert$ veriT_vr21 veriT_vr22) :named @p_121))) :rule cong :premises (t57.t2 t57.t3))
(step t57.t5 (cl (= @p_122 (! (inf$ veriT_vr20 @p_121) :named @p_123))) :rule cong :premises (t57.t1 t57.t4))
(step t57.t6 (cl (= @p_124 (! (= bot$ @p_123) :named @p_125))) :rule cong :premises (t57.t5))
(step t57.t7 (cl @p_126) :rule refl)
(step t57.t8 (cl @p_127) :rule refl)
(step t57.t9 (cl (= @p_128 (! (member$a veriT_vr21 veriT_vr20) :named @p_129))) :rule cong :premises (t57.t7 t57.t8))
(step t57.t10 (cl (= @p_130 (! (not @p_129) :named @p_131))) :rule cong :premises (t57.t9))
(step t57.t11 (cl @p_127) :rule refl)
(step t57.t12 (cl @p_132) :rule refl)
(step t57.t13 (cl (= @p_133 (! (inf$ veriT_vr20 veriT_vr22) :named @p_134))) :rule cong :premises (t57.t11 t57.t12))
(step t57.t14 (cl (= @p_135 (! (= bot$ @p_134) :named @p_136))) :rule cong :premises (t57.t13))
(step t57.t15 (cl (= @p_137 (! (and @p_131 @p_136) :named @p_138))) :rule cong :premises (t57.t10 t57.t14))
(step t57.t16 (cl (= @p_139 (! (= @p_125 @p_138) :named @p_140))) :rule cong :premises (t57.t6 t57.t15))
(step t57 (cl (! (= @p_120 (! (forall ((veriT_vr20 Real_real_prod_set$) (veriT_vr21 Real_real_prod$) (veriT_vr22 Real_real_prod_set$)) @p_140) :named @p_142)) :named @p_141)) :rule bind)
(step t58 (cl (not @p_141) (not @p_120) @p_142) :rule equiv_pos2)
(step t59 (cl @p_142) :rule th_resolution :premises (a7 t57 t58))
(anchor :step t60 :args ((:= veriT_vr20 veriT_vr23) (:= veriT_vr21 veriT_vr24) (:= veriT_vr22 veriT_vr25)))
(step t60.t1 (cl (! (= veriT_vr20 veriT_vr23) :named @p_147)) :rule refl)
(step t60.t2 (cl (! (= veriT_vr21 veriT_vr24) :named @p_146)) :rule refl)
(step t60.t3 (cl (! (= veriT_vr22 veriT_vr25) :named @p_150)) :rule refl)
(step t60.t4 (cl (= @p_121 (! (insert$ veriT_vr24 veriT_vr25) :named @p_143))) :rule cong :premises (t60.t2 t60.t3))
(step t60.t5 (cl (= @p_123 (! (inf$ veriT_vr23 @p_143) :named @p_144))) :rule cong :premises (t60.t1 t60.t4))
(step t60.t6 (cl (= @p_125 (! (= bot$ @p_144) :named @p_145))) :rule cong :premises (t60.t5))
(step t60.t7 (cl @p_146) :rule refl)
(step t60.t8 (cl @p_147) :rule refl)
(step t60.t9 (cl (= @p_129 (! (member$a veriT_vr24 veriT_vr23) :named @p_148))) :rule cong :premises (t60.t7 t60.t8))
(step t60.t10 (cl (= @p_131 (! (not @p_148) :named @p_149))) :rule cong :premises (t60.t9))
(step t60.t11 (cl @p_147) :rule refl)
(step t60.t12 (cl @p_150) :rule refl)
(step t60.t13 (cl (= @p_134 (! (inf$ veriT_vr23 veriT_vr25) :named @p_151))) :rule cong :premises (t60.t11 t60.t12))
(step t60.t14 (cl (= @p_136 (! (= bot$ @p_151) :named @p_152))) :rule cong :premises (t60.t13))
(step t60.t15 (cl (= @p_138 (! (and @p_149 @p_152) :named @p_153))) :rule cong :premises (t60.t10 t60.t14))
(step t60.t16 (cl (= @p_140 (! (= @p_145 @p_153) :named @p_154))) :rule cong :premises (t60.t6 t60.t15))
(step t60 (cl (! (= @p_142 (! (forall ((veriT_vr23 Real_real_prod_set$) (veriT_vr24 Real_real_prod$) (veriT_vr25 Real_real_prod_set$)) @p_154) :named @p_156)) :named @p_155)) :rule bind)
(step t61 (cl (not @p_155) (not @p_142) @p_156) :rule equiv_pos2)
(step t62 (cl @p_156) :rule th_resolution :premises (t59 t60 t61))
(anchor :step t63 :args ((:= ?v0 veriT_vr26) (:= ?v1 veriT_vr27)))
(step t63.t1 (cl (! (= ?v0 veriT_vr26) :named @p_159)) :rule refl)
(step t63.t2 (cl (= @p_4 (! (finite$ veriT_vr26) :named @p_158))) :rule cong :premises (t63.t1))
(step t63.t3 (cl (= ?v1 veriT_vr27)) :rule refl)
(step t63.t4 (cl @p_159) :rule refl)
(step t63.t5 (cl (= @p_160 (! (insert$ veriT_vr27 veriT_vr26) :named @p_161))) :rule cong :premises (t63.t3 t63.t4))
(step t63.t6 (cl (= @p_162 (! (finite$ @p_161) :named @p_163))) :rule cong :premises (t63.t5))
(step t63.t7 (cl (= @p_164 (! (=> @p_158 @p_163) :named @p_165))) :rule cong :premises (t63.t2 t63.t6))
(step t63 (cl (! (= @p_157 (! (forall ((veriT_vr26 Real_real_prod_set$) (veriT_vr27 Real_real_prod$)) @p_165) :named @p_167)) :named @p_166)) :rule bind)
(step t64 (cl (not @p_166) (not @p_157) @p_167) :rule equiv_pos2)
(step t65 (cl @p_167) :rule th_resolution :premises (a9 t63 t64))
(anchor :step t66 :args ((:= veriT_vr26 veriT_vr28) (:= veriT_vr27 veriT_vr29)))
(step t66.t1 (cl (! (= veriT_vr26 veriT_vr28) :named @p_169)) :rule refl)
(step t66.t2 (cl (= @p_158 (! (finite$ veriT_vr28) :named @p_168))) :rule cong :premises (t66.t1))
(step t66.t3 (cl (= veriT_vr27 veriT_vr29)) :rule refl)
(step t66.t4 (cl @p_169) :rule refl)
(step t66.t5 (cl (= @p_161 (! (insert$ veriT_vr29 veriT_vr28) :named @p_170))) :rule cong :premises (t66.t3 t66.t4))
(step t66.t6 (cl (= @p_163 (! (finite$ @p_170) :named @p_171))) :rule cong :premises (t66.t5))
(step t66.t7 (cl (= @p_165 (! (=> @p_168 @p_171) :named @p_172))) :rule cong :premises (t66.t2 t66.t6))
(step t66 (cl (! (= @p_167 (! (forall ((veriT_vr28 Real_real_prod_set$) (veriT_vr29 Real_real_prod$)) @p_172) :named @p_174)) :named @p_173)) :rule bind)
(step t67 (cl (not @p_173) (not @p_167) @p_174) :rule equiv_pos2)
(step t68 (cl @p_174) :rule th_resolution :premises (t65 t66 t67))
(anchor :step t69 :args ((:= ?v0 veriT_vr30) (:= ?v1 veriT_vr31)))
(step t69.t1 (cl (! (= ?v0 veriT_vr30) :named @p_179)) :rule refl)
(step t69.t2 (cl (! (= ?v1 veriT_vr31) :named @p_178)) :rule refl)
(step t69.t3 (cl (= @p_176 (! (member$a veriT_vr30 veriT_vr31) :named @p_177))) :rule cong :premises (t69.t1 t69.t2))
(step t69.t4 (cl @p_178) :rule refl)
(step t69.t5 (cl @p_179) :rule refl)
(step t69.t6 (cl @p_178) :rule refl)
(step t69.t7 (cl (= @p_2 (! (insert$ veriT_vr30 veriT_vr31) :named @p_180))) :rule cong :premises (t69.t5 t69.t6))
(step t69.t8 (cl (= @p_181 (! (= veriT_vr31 @p_180) :named @p_182))) :rule cong :premises (t69.t4 t69.t7))
(step t69.t9 (cl (= @p_183 (! (=> @p_177 @p_182) :named @p_184))) :rule cong :premises (t69.t3 t69.t8))
(step t69 (cl (! (= @p_175 (! (forall ((veriT_vr30 Real_real_prod$) (veriT_vr31 Real_real_prod_set$)) @p_184) :named @p_186)) :named @p_185)) :rule bind)
(step t70 (cl (not @p_185) (not @p_175) @p_186) :rule equiv_pos2)
(step t71 (cl @p_186) :rule th_resolution :premises (a11 t69 t70))
(anchor :step t72 :args ((:= veriT_vr30 veriT_vr32) (:= veriT_vr31 veriT_vr33)))
(step t72.t1 (cl (! (= veriT_vr30 veriT_vr32) :named @p_189)) :rule refl)
(step t72.t2 (cl (! (= veriT_vr31 veriT_vr33) :named @p_188)) :rule refl)
(step t72.t3 (cl (= @p_177 (! (member$a veriT_vr32 veriT_vr33) :named @p_187))) :rule cong :premises (t72.t1 t72.t2))
(step t72.t4 (cl @p_188) :rule refl)
(step t72.t5 (cl @p_189) :rule refl)
(step t72.t6 (cl @p_188) :rule refl)
(step t72.t7 (cl (= @p_180 (! (insert$ veriT_vr32 veriT_vr33) :named @p_190))) :rule cong :premises (t72.t5 t72.t6))
(step t72.t8 (cl (= @p_182 (! (= veriT_vr33 @p_190) :named @p_191))) :rule cong :premises (t72.t4 t72.t7))
(step t72.t9 (cl (= @p_184 (! (=> @p_187 @p_191) :named @p_192))) :rule cong :premises (t72.t3 t72.t8))
(step t72 (cl (! (= @p_186 (! (forall ((veriT_vr32 Real_real_prod$) (veriT_vr33 Real_real_prod_set$)) @p_192) :named @p_194)) :named @p_193)) :rule bind)
(step t73 (cl (not @p_193) (not @p_186) @p_194) :rule equiv_pos2)
(step t74 (cl @p_194) :rule th_resolution :premises (t71 t72 t73))
(anchor :step t75 :args ((:= ?v0 veriT_vr34)))
(step t75.t1 (cl (= ?v0 veriT_vr34)) :rule refl)
(step t75.t2 (cl (= @p_196 (! (inf$ veriT_vr34 bot$) :named @p_197))) :rule cong :premises (t75.t1))
(step t75.t3 (cl (= @p_198 (! (= bot$ @p_197) :named @p_199))) :rule cong :premises (t75.t2))
(step t75 (cl (! (= @p_195 (! (forall ((veriT_vr34 Real_real_prod_set$)) @p_199) :named @p_201)) :named @p_200)) :rule bind)
(step t76 (cl (not @p_200) (not @p_195) @p_201) :rule equiv_pos2)
(step t77 (cl @p_201) :rule th_resolution :premises (a13 t75 t76))
(anchor :step t78 :args ((:= veriT_vr34 veriT_vr35)))
(step t78.t1 (cl (= veriT_vr34 veriT_vr35)) :rule refl)
(step t78.t2 (cl (= @p_197 (! (inf$ veriT_vr35 bot$) :named @p_202))) :rule cong :premises (t78.t1))
(step t78.t3 (cl (= @p_199 (! (= bot$ @p_202) :named @p_203))) :rule cong :premises (t78.t2))
(step t78 (cl (! (= @p_201 (! (forall ((veriT_vr35 Real_real_prod_set$)) @p_203) :named @p_205)) :named @p_204)) :rule bind)
(step t79 (cl (not @p_204) (not @p_201) @p_205) :rule equiv_pos2)
(step t80 (cl @p_205) :rule th_resolution :premises (t77 t78 t79))
(anchor :step t81 :args ((:= ?v0 veriT_vr36) (:= ?v1 veriT_vr37) (:= ?v2 veriT_vr38)))
(step t81.t1 (cl (! (= ?v0 veriT_vr36) :named @p_211)) :rule refl)
(step t81.t2 (cl (! (= ?v1 veriT_vr37) :named @p_210)) :rule refl)
(step t81.t3 (cl (! (= ?v2 veriT_vr38) :named @p_212)) :rule refl)
(step t81.t4 (cl (= @p_1 (! (insert$ veriT_vr37 veriT_vr38) :named @p_207))) :rule cong :premises (t81.t2 t81.t3))
(step t81.t5 (cl (= @p_208 (! (insert$ veriT_vr36 @p_207) :named @p_209))) :rule cong :premises (t81.t1 t81.t4))
(step t81.t6 (cl @p_210) :rule refl)
(step t81.t7 (cl @p_211) :rule refl)
(step t81.t8 (cl @p_212) :rule refl)
(step t81.t9 (cl (= @p_213 (! (insert$ veriT_vr36 veriT_vr38) :named @p_214))) :rule cong :premises (t81.t7 t81.t8))
(step t81.t10 (cl (= @p_215 (! (insert$ veriT_vr37 @p_214) :named @p_216))) :rule cong :premises (t81.t6 t81.t9))
(step t81.t11 (cl (= @p_217 (! (= @p_209 @p_216) :named @p_218))) :rule cong :premises (t81.t5 t81.t10))
(step t81 (cl (! (= @p_206 (! (forall ((veriT_vr36 Real_real_prod$) (veriT_vr37 Real_real_prod$) (veriT_vr38 Real_real_prod_set$)) @p_218) :named @p_220)) :named @p_219)) :rule bind)
(step t82 (cl (not @p_219) (not @p_206) @p_220) :rule equiv_pos2)
(step t83 (cl @p_220) :rule th_resolution :premises (a14 t81 t82))
(anchor :step t84 :args ((:= veriT_vr36 veriT_vr39) (:= veriT_vr37 veriT_vr40) (:= veriT_vr38 veriT_vr41)))
(step t84.t1 (cl (! (= veriT_vr36 veriT_vr39) :named @p_224)) :rule refl)
(step t84.t2 (cl (! (= veriT_vr37 veriT_vr40) :named @p_223)) :rule refl)
(step t84.t3 (cl (! (= veriT_vr38 veriT_vr41) :named @p_225)) :rule refl)
(step t84.t4 (cl (= @p_207 (! (insert$ veriT_vr40 veriT_vr41) :named @p_221))) :rule cong :premises (t84.t2 t84.t3))
(step t84.t5 (cl (= @p_209 (! (insert$ veriT_vr39 @p_221) :named @p_222))) :rule cong :premises (t84.t1 t84.t4))
(step t84.t6 (cl @p_223) :rule refl)
(step t84.t7 (cl @p_224) :rule refl)
(step t84.t8 (cl @p_225) :rule refl)
(step t84.t9 (cl (= @p_214 (! (insert$ veriT_vr39 veriT_vr41) :named @p_226))) :rule cong :premises (t84.t7 t84.t8))
(step t84.t10 (cl (= @p_216 (! (insert$ veriT_vr40 @p_226) :named @p_227))) :rule cong :premises (t84.t6 t84.t9))
(step t84.t11 (cl (= @p_218 (! (= @p_222 @p_227) :named @p_228))) :rule cong :premises (t84.t5 t84.t10))
(step t84 (cl (! (= @p_220 (! (forall ((veriT_vr39 Real_real_prod$) (veriT_vr40 Real_real_prod$) (veriT_vr41 Real_real_prod_set$)) @p_228) :named @p_230)) :named @p_229)) :rule bind)
(step t85 (cl (not @p_229) (not @p_220) @p_230) :rule equiv_pos2)
(step t86 (cl @p_230) :rule th_resolution :premises (t83 t84 t85))
(anchor :step t87 :args ((:= ?v0 veriT_vr42) (:= ?v1 veriT_vr43)))
(step t87.t1 (cl (! (= ?v0 veriT_vr42) :named @p_233)) :rule refl)
(step t87.t2 (cl (! (= ?v1 veriT_vr43) :named @p_235)) :rule refl)
(step t87.t3 (cl (= @p_2 (! (insert$ veriT_vr42 veriT_vr43) :named @p_232))) :rule cong :premises (t87.t1 t87.t2))
(step t87.t4 (cl @p_233) :rule refl)
(step t87.t5 (cl (= @p_3 (! (insert$ veriT_vr42 bot$) :named @p_234))) :rule cong :premises (t87.t4))
(step t87.t6 (cl @p_235) :rule refl)
(step t87.t7 (cl (= @p_236 (! (sup$ @p_234 veriT_vr43) :named @p_237))) :rule cong :premises (t87.t5 t87.t6))
(step t87.t8 (cl (= @p_238 (! (= @p_232 @p_237) :named @p_239))) :rule cong :premises (t87.t3 t87.t7))
(step t87 (cl (! (= @p_231 (! (forall ((veriT_vr42 Real_real_prod$) (veriT_vr43 Real_real_prod_set$)) @p_239) :named @p_241)) :named @p_240)) :rule bind)
(step t88 (cl (not @p_240) (not @p_231) @p_241) :rule equiv_pos2)
(step t89 (cl @p_241) :rule th_resolution :premises (a15 t87 t88))
(anchor :step t90 :args ((:= veriT_vr42 veriT_vr44) (:= veriT_vr43 veriT_vr45)))
(step t90.t1 (cl (! (= veriT_vr42 veriT_vr44) :named @p_243)) :rule refl)
(step t90.t2 (cl (! (= veriT_vr43 veriT_vr45) :named @p_245)) :rule refl)
(step t90.t3 (cl (= @p_232 (! (insert$ veriT_vr44 veriT_vr45) :named @p_242))) :rule cong :premises (t90.t1 t90.t2))
(step t90.t4 (cl @p_243) :rule refl)
(step t90.t5 (cl (= @p_234 (! (insert$ veriT_vr44 bot$) :named @p_244))) :rule cong :premises (t90.t4))
(step t90.t6 (cl @p_245) :rule refl)
(step t90.t7 (cl (= @p_237 (! (sup$ @p_244 veriT_vr45) :named @p_246))) :rule cong :premises (t90.t5 t90.t6))
(step t90.t8 (cl (= @p_239 (! (= @p_242 @p_246) :named @p_247))) :rule cong :premises (t90.t3 t90.t7))
(step t90 (cl (! (= @p_241 (! (forall ((veriT_vr44 Real_real_prod$) (veriT_vr45 Real_real_prod_set$)) @p_247) :named @p_249)) :named @p_248)) :rule bind)
(step t91 (cl (not @p_248) (not @p_241) @p_249) :rule equiv_pos2)
(step t92 (cl @p_249) :rule th_resolution :premises (t89 t90 t91))
(anchor :step t93 :args ((:= ?v0 veriT_vr46) (:= ?v1 veriT_vr47) (:= ?v2 veriT_vr48) (:= ?v3 veriT_vr49) (:= ?v4 veriT_vr50)))
(step t93.t1 (cl (! (= ?v0 veriT_vr46) :named @p_262)) :rule refl)
(step t93.t2 (cl (= @p_4 (! (finite$ veriT_vr46) :named @p_251))) :rule cong :premises (t93.t1))
(step t93.t3 (cl (! (= ?v1 veriT_vr47) :named @p_256)) :rule refl)
(step t93.t4 (cl (! (= ?v2 veriT_vr48) :named @p_263)) :rule refl)
(step t93.t5 (cl (= @p_252 (! (line_integral_exists$ veriT_vr47 veriT_vr48) :named @p_253))) :rule cong :premises (t93.t3 t93.t4))
(step t93.t6 (cl (! (= ?v3 veriT_vr49) :named @p_259)) :rule refl)
(step t93.t7 (cl (= @p_254 (! (fun_app$a @p_253 veriT_vr49) :named @p_255))) :rule cong :premises (t93.t5 t93.t6))
(step t93.t8 (cl @p_256) :rule refl)
(step t93.t9 (cl (! (= ?v4 veriT_vr50) :named @p_264)) :rule refl)
(step t93.t10 (cl (= @p_257 (! (line_integral_exists$ veriT_vr47 veriT_vr50) :named @p_258))) :rule cong :premises (t93.t8 t93.t9))
(step t93.t11 (cl @p_259) :rule refl)
(step t93.t12 (cl (= @p_260 (! (fun_app$a @p_258 veriT_vr49) :named @p_261))) :rule cong :premises (t93.t10 t93.t11))
(step t93.t13 (cl @p_262) :rule refl)
(step t93.t14 (cl @p_263) :rule refl)
(step t93.t15 (cl @p_264) :rule refl)
(step t93.t16 (cl (= @p_265 (! (sup$ veriT_vr48 veriT_vr50) :named @p_266))) :rule cong :premises (t93.t14 t93.t15))
(step t93.t17 (cl (= @p_267 (! (= veriT_vr46 @p_266) :named @p_268))) :rule cong :premises (t93.t13 t93.t16))
(step t93.t18 (cl @p_263) :rule refl)
(step t93.t19 (cl @p_264) :rule refl)
(step t93.t20 (cl (= @p_269 (! (inf$ veriT_vr48 veriT_vr50) :named @p_270))) :rule cong :premises (t93.t18 t93.t19))
(step t93.t21 (cl (= @p_271 (! (= bot$ @p_270) :named @p_272))) :rule cong :premises (t93.t20))
(step t93.t22 (cl (= @p_273 (! (and @p_268 @p_272) :named @p_274))) :rule cong :premises (t93.t17 t93.t21))
(step t93.t23 (cl (= @p_275 (! (and @p_261 @p_274) :named @p_276))) :rule cong :premises (t93.t12 t93.t22))
(step t93.t24 (cl (= @p_277 (! (and @p_255 @p_276) :named @p_278))) :rule cong :premises (t93.t7 t93.t23))
(step t93.t25 (cl (= @p_279 (! (and @p_251 @p_278) :named @p_280))) :rule cong :premises (t93.t2 t93.t24))
(step t93.t26 (cl @p_256) :rule refl)
(step t93.t27 (cl @p_262) :rule refl)
(step t93.t28 (cl @p_259) :rule refl)
(step t93.t29 (cl (= @p_281 (! (line_integral$ veriT_vr47 veriT_vr46 veriT_vr49) :named @p_282))) :rule cong :premises (t93.t26 t93.t27 t93.t28))
(step t93.t30 (cl @p_256) :rule refl)
(step t93.t31 (cl @p_263) :rule refl)
(step t93.t32 (cl @p_259) :rule refl)
(step t93.t33 (cl (= @p_283 (! (line_integral$ veriT_vr47 veriT_vr48 veriT_vr49) :named @p_284))) :rule cong :premises (t93.t30 t93.t31 t93.t32))
(step t93.t34 (cl @p_256) :rule refl)
(step t93.t35 (cl @p_264) :rule refl)
(step t93.t36 (cl @p_259) :rule refl)
(step t93.t37 (cl (= @p_285 (! (line_integral$ veriT_vr47 veriT_vr50 veriT_vr49) :named @p_286))) :rule cong :premises (t93.t34 t93.t35 t93.t36))
(step t93.t38 (cl (= @p_287 (! (+ @p_284 @p_286) :named @p_288))) :rule cong :premises (t93.t33 t93.t37))
(step t93.t39 (cl (= @p_289 (! (= @p_282 @p_288) :named @p_290))) :rule cong :premises (t93.t29 t93.t38))
(step t93.t40 (cl (= @p_291 (! (=> @p_280 @p_290) :named @p_292))) :rule cong :premises (t93.t25 t93.t39))
(step t93 (cl (! (= @p_250 (! (forall ((veriT_vr46 Real_real_prod_set$) (veriT_vr47 Real_real_prod_real_real_prod_fun$) (veriT_vr48 Real_real_prod_set$) (veriT_vr49 Real_real_real_prod_fun$) (veriT_vr50 Real_real_prod_set$)) @p_292) :named @p_294)) :named @p_293)) :rule bind)
(step t94 (cl (not @p_293) (not @p_250) @p_294) :rule equiv_pos2)
(step t95 (cl @p_294) :rule th_resolution :premises (a16 t93 t94))
(anchor :step t96 :args (veriT_vr46 veriT_vr47 veriT_vr48 veriT_vr49 veriT_vr50))
(step t96.t1 (cl (= @p_280 (! (and @p_251 @p_255 @p_261 @p_268 @p_272) :named @p_295))) :rule ac_simp)
(step t96.t2 (cl (= @p_292 (! (=> @p_295 @p_290) :named @p_296))) :rule cong :premises (t96.t1))
(step t96 (cl (! (= @p_294 (! (forall ((veriT_vr46 Real_real_prod_set$) (veriT_vr47 Real_real_prod_real_real_prod_fun$) (veriT_vr48 Real_real_prod_set$) (veriT_vr49 Real_real_real_prod_fun$) (veriT_vr50 Real_real_prod_set$)) @p_296) :named @p_298)) :named @p_297)) :rule bind)
(step t97 (cl (not @p_297) (not @p_294) @p_298) :rule equiv_pos2)
(step t98 (cl @p_298) :rule th_resolution :premises (t95 t96 t97))
(anchor :step t99 :args ((:= veriT_vr46 veriT_vr51) (:= veriT_vr47 veriT_vr52) (:= veriT_vr48 veriT_vr53) (:= veriT_vr49 veriT_vr54) (:= veriT_vr50 veriT_vr55)))
(step t99.t1 (cl (! (= veriT_vr46 veriT_vr51) :named @p_306)) :rule refl)
(step t99.t2 (cl (= @p_251 (! (finite$ veriT_vr51) :named @p_299))) :rule cong :premises (t99.t1))
(step t99.t3 (cl (! (= veriT_vr47 veriT_vr52) :named @p_302)) :rule refl)
(step t99.t4 (cl (! (= veriT_vr48 veriT_vr53) :named @p_307)) :rule refl)
(step t99.t5 (cl (= @p_253 (! (line_integral_exists$ veriT_vr52 veriT_vr53) :named @p_300))) :rule cong :premises (t99.t3 t99.t4))
(step t99.t6 (cl (! (= veriT_vr49 veriT_vr54) :named @p_304)) :rule refl)
(step t99.t7 (cl (= @p_255 (! (fun_app$a @p_300 veriT_vr54) :named @p_301))) :rule cong :premises (t99.t5 t99.t6))
(step t99.t8 (cl @p_302) :rule refl)
(step t99.t9 (cl (! (= veriT_vr50 veriT_vr55) :named @p_308)) :rule refl)
(step t99.t10 (cl (= @p_258 (! (line_integral_exists$ veriT_vr52 veriT_vr55) :named @p_303))) :rule cong :premises (t99.t8 t99.t9))
(step t99.t11 (cl @p_304) :rule refl)
(step t99.t12 (cl (= @p_261 (! (fun_app$a @p_303 veriT_vr54) :named @p_305))) :rule cong :premises (t99.t10 t99.t11))
(step t99.t13 (cl @p_306) :rule refl)
(step t99.t14 (cl @p_307) :rule refl)
(step t99.t15 (cl @p_308) :rule refl)
(step t99.t16 (cl (= @p_266 (! (sup$ veriT_vr53 veriT_vr55) :named @p_309))) :rule cong :premises (t99.t14 t99.t15))
(step t99.t17 (cl (= @p_268 (! (= veriT_vr51 @p_309) :named @p_310))) :rule cong :premises (t99.t13 t99.t16))
(step t99.t18 (cl @p_307) :rule refl)
(step t99.t19 (cl @p_308) :rule refl)
(step t99.t20 (cl (= @p_270 (! (inf$ veriT_vr53 veriT_vr55) :named @p_311))) :rule cong :premises (t99.t18 t99.t19))
(step t99.t21 (cl (= @p_272 (! (= bot$ @p_311) :named @p_312))) :rule cong :premises (t99.t20))
(step t99.t22 (cl (= @p_295 (! (and @p_299 @p_301 @p_305 @p_310 @p_312) :named @p_313))) :rule cong :premises (t99.t2 t99.t7 t99.t12 t99.t17 t99.t21))
(step t99.t23 (cl @p_302) :rule refl)
(step t99.t24 (cl @p_306) :rule refl)
(step t99.t25 (cl @p_304) :rule refl)
(step t99.t26 (cl (= @p_282 (! (line_integral$ veriT_vr52 veriT_vr51 veriT_vr54) :named @p_314))) :rule cong :premises (t99.t23 t99.t24 t99.t25))
(step t99.t27 (cl @p_302) :rule refl)
(step t99.t28 (cl @p_307) :rule refl)
(step t99.t29 (cl @p_304) :rule refl)
(step t99.t30 (cl (= @p_284 (! (line_integral$ veriT_vr52 veriT_vr53 veriT_vr54) :named @p_315))) :rule cong :premises (t99.t27 t99.t28 t99.t29))
(step t99.t31 (cl @p_302) :rule refl)
(step t99.t32 (cl @p_308) :rule refl)
(step t99.t33 (cl @p_304) :rule refl)
(step t99.t34 (cl (= @p_286 (! (line_integral$ veriT_vr52 veriT_vr55 veriT_vr54) :named @p_316))) :rule cong :premises (t99.t31 t99.t32 t99.t33))
(step t99.t35 (cl (= @p_288 (! (+ @p_315 @p_316) :named @p_317))) :rule cong :premises (t99.t30 t99.t34))
(step t99.t36 (cl (= @p_290 (! (= @p_314 @p_317) :named @p_318))) :rule cong :premises (t99.t26 t99.t35))
(step t99.t37 (cl (= @p_296 (! (=> @p_313 @p_318) :named @p_319))) :rule cong :premises (t99.t22 t99.t36))
(step t99 (cl (! (= @p_298 (! (forall ((veriT_vr51 Real_real_prod_set$) (veriT_vr52 Real_real_prod_real_real_prod_fun$) (veriT_vr53 Real_real_prod_set$) (veriT_vr54 Real_real_real_prod_fun$) (veriT_vr55 Real_real_prod_set$)) @p_319) :named @p_321)) :named @p_320)) :rule bind)
(step t100 (cl (not @p_320) (not @p_298) @p_321) :rule equiv_pos2)
(step t101 (cl @p_321) :rule th_resolution :premises (t98 t99 t100))
(anchor :step t102 :args ((:= ?v0 veriT_vr56)))
(step t102.t1 (cl (! (= ?v0 veriT_vr56) :named @p_324)) :rule refl)
(step t102.t2 (cl (= @p_9 (! (member$ veriT_vr56 one_chain_typeI$) :named @p_323))) :rule cong :premises (t102.t1))
(step t102.t3 (cl @p_324) :rule refl)
(step t102.t4 (cl (! (= @p_6 (! (case_prod$ uu$ veriT_vr56) :named @p_325)) :named @p_330)) :rule cong :premises (t102.t3))
(step t102.t5 (cl (= @p_326 (! (=> @p_323 @p_325) :named @p_327))) :rule cong :premises (t102.t2 t102.t4))
(step t102 (cl (= @p_322 (! (forall ((veriT_vr56 Int_real_real_real_prod_fun_prod$)) @p_327) :named @p_334))) :rule bind)
(anchor :step t103 :args ((:= ?v0 veriT_vr56)))
(step t103.t1 (cl @p_324) :rule refl)
(step t103.t2 (cl (= @p_8 (! (member$ veriT_vr56 one_chain_typeII$) :named @p_329))) :rule cong :premises (t103.t1))
(step t103.t3 (cl @p_324) :rule refl)
(step t103.t4 (cl @p_330) :rule cong :premises (t103.t3))
(step t103.t5 (cl (= @p_331 (! (=> @p_329 @p_325) :named @p_332))) :rule cong :premises (t103.t2 t103.t4))
(step t103 (cl (= @p_328 (! (forall ((veriT_vr56 Int_real_real_real_prod_fun_prod$)) @p_332) :named @p_335))) :rule bind)
(step t104 (cl (= @p_333 (! (and @p_334 @p_335) :named @p_338))) :rule cong :premises (t102 t103))
(step t105 (cl (! (= @p_336 (! (and @p_337 @p_338) :named @p_340)) :named @p_339)) :rule cong :premises (t104))
(step t106 (cl (not @p_339) (not @p_336) @p_340) :rule equiv_pos2)
(step t107 (cl @p_340) :rule th_resolution :premises (a17 t105 t106))
(step t108 (cl (! (= @p_340 (! (and @p_337 @p_334 @p_335) :named @p_342)) :named @p_341)) :rule ac_simp)
(step t109 (cl (not @p_341) (not @p_340) @p_342) :rule equiv_pos2)
(step t110 (cl @p_342) :rule th_resolution :premises (t107 t108 t109))
(anchor :step t111 :args ((:= veriT_vr56 veriT_vr57)))
(step t111.t1 (cl (! (= veriT_vr56 veriT_vr57) :named @p_344)) :rule refl)
(step t111.t2 (cl (= @p_329 (! (member$ veriT_vr57 one_chain_typeII$) :named @p_343))) :rule cong :premises (t111.t1))
(step t111.t3 (cl @p_344) :rule refl)
(step t111.t4 (cl (= @p_325 (! (case_prod$ uu$ veriT_vr57) :named @p_345))) :rule cong :premises (t111.t3))
(step t111.t5 (cl (= @p_332 (! (=> @p_343 @p_345) :named @p_346))) :rule cong :premises (t111.t2 t111.t4))
(step t111 (cl (= @p_335 (! (forall ((veriT_vr57 Int_real_real_real_prod_fun_prod$)) @p_346) :named @p_347))) :rule bind)
(step t112 (cl (! (= @p_342 (! (and @p_337 @p_334 @p_347) :named @p_349)) :named @p_348)) :rule cong :premises (t111))
(step t113 (cl (not @p_348) (not @p_342) @p_349) :rule equiv_pos2)
(step t114 (cl @p_349) :rule th_resolution :premises (t110 t112 t113))
(anchor :step t115 :args ((:= veriT_vr56 veriT_vr58)))
(step t115.t1 (cl (! (= veriT_vr56 veriT_vr58) :named @p_351)) :rule refl)
(step t115.t2 (cl (= @p_323 (! (member$ veriT_vr58 one_chain_typeI$) :named @p_350))) :rule cong :premises (t115.t1))
(step t115.t3 (cl @p_351) :rule refl)
(step t115.t4 (cl (= @p_325 (! (case_prod$ uu$ veriT_vr58) :named @p_352))) :rule cong :premises (t115.t3))
(step t115.t5 (cl (= @p_327 (! (=> @p_350 @p_352) :named @p_353))) :rule cong :premises (t115.t2 t115.t4))
(step t115 (cl (= @p_334 (! (forall ((veriT_vr58 Int_real_real_real_prod_fun_prod$)) @p_353) :named @p_358))) :rule bind)
(anchor :step t116 :args ((:= veriT_vr57 veriT_vr59)))
(step t116.t1 (cl (! (= veriT_vr57 veriT_vr59) :named @p_355)) :rule refl)
(step t116.t2 (cl (= @p_343 (! (member$ veriT_vr59 one_chain_typeII$) :named @p_354))) :rule cong :premises (t116.t1))
(step t116.t3 (cl @p_355) :rule refl)
(step t116.t4 (cl (= @p_345 (! (case_prod$ uu$ veriT_vr59) :named @p_356))) :rule cong :premises (t116.t3))
(step t116.t5 (cl (= @p_346 (! (=> @p_354 @p_356) :named @p_357))) :rule cong :premises (t116.t2 t116.t4))
(step t116 (cl (= @p_347 (! (forall ((veriT_vr59 Int_real_real_real_prod_fun_prod$)) @p_357) :named @p_359))) :rule bind)
(step t117 (cl (! (= @p_349 (! (and @p_337 @p_358 @p_359) :named @p_361)) :named @p_360)) :rule cong :premises (t115 t116))
(step t118 (cl (not @p_360) (not @p_349) @p_361) :rule equiv_pos2)
(step t119 (cl @p_361) :rule th_resolution :premises (t114 t117 t118))
(anchor :step t120 :args ((:= ?v0 veriT_vr60)))
(step t120.t1 (cl (! (= ?v0 veriT_vr60) :named @p_364)) :rule refl)
(step t120.t2 (cl (= @p_8 (! (member$ veriT_vr60 one_chain_typeII$) :named @p_363))) :rule cong :premises (t120.t1))
(step t120.t3 (cl @p_364) :rule refl)
(step t120.t4 (cl (! (= @p_10 (! (case_prod$ uua$ veriT_vr60) :named @p_365)) :named @p_370)) :rule cong :premises (t120.t3))
(step t120.t5 (cl (= @p_366 (! (=> @p_363 @p_365) :named @p_367))) :rule cong :premises (t120.t2 t120.t4))
(step t120 (cl (= @p_362 (! (forall ((veriT_vr60 Int_real_real_real_prod_fun_prod$)) @p_367) :named @p_374))) :rule bind)
(anchor :step t121 :args ((:= ?v0 veriT_vr60)))
(step t121.t1 (cl @p_364) :rule refl)
(step t121.t2 (cl (= @p_9 (! (member$ veriT_vr60 one_chain_typeI$) :named @p_369))) :rule cong :premises (t121.t1))
(step t121.t3 (cl @p_364) :rule refl)
(step t121.t4 (cl @p_370) :rule cong :premises (t121.t3))
(step t121.t5 (cl (= @p_371 (! (=> @p_369 @p_365) :named @p_372))) :rule cong :premises (t121.t2 t121.t4))
(step t121 (cl (= @p_368 (! (forall ((veriT_vr60 Int_real_real_real_prod_fun_prod$)) @p_372) :named @p_375))) :rule bind)
(step t122 (cl (= @p_373 (! (and @p_374 @p_375) :named @p_378))) :rule cong :premises (t120 t121))
(step t123 (cl (! (= @p_376 (! (and @p_377 @p_378) :named @p_380)) :named @p_379)) :rule cong :premises (t122))
(step t124 (cl (not @p_379) (not @p_376) @p_380) :rule equiv_pos2)
(step t125 (cl @p_380) :rule th_resolution :premises (a18 t123 t124))
(step t126 (cl (! (= @p_380 (! (and @p_377 @p_374 @p_375) :named @p_382)) :named @p_381)) :rule ac_simp)
(step t127 (cl (not @p_381) (not @p_380) @p_382) :rule equiv_pos2)
(step t128 (cl @p_382) :rule th_resolution :premises (t125 t126 t127))
(anchor :step t129 :args ((:= veriT_vr60 veriT_vr61)))
(step t129.t1 (cl (! (= veriT_vr60 veriT_vr61) :named @p_384)) :rule refl)
(step t129.t2 (cl (= @p_369 (! (member$ veriT_vr61 one_chain_typeI$) :named @p_383))) :rule cong :premises (t129.t1))
(step t129.t3 (cl @p_384) :rule refl)
(step t129.t4 (cl (= @p_365 (! (case_prod$ uua$ veriT_vr61) :named @p_385))) :rule cong :premises (t129.t3))
(step t129.t5 (cl (= @p_372 (! (=> @p_383 @p_385) :named @p_386))) :rule cong :premises (t129.t2 t129.t4))
(step t129 (cl (= @p_375 (! (forall ((veriT_vr61 Int_real_real_real_prod_fun_prod$)) @p_386) :named @p_387))) :rule bind)
(step t130 (cl (! (= @p_382 (! (and @p_377 @p_374 @p_387) :named @p_389)) :named @p_388)) :rule cong :premises (t129))
(step t131 (cl (not @p_388) (not @p_382) @p_389) :rule equiv_pos2)
(step t132 (cl @p_389) :rule th_resolution :premises (t128 t130 t131))
(anchor :step t133 :args ((:= veriT_vr60 veriT_vr62)))
(step t133.t1 (cl (! (= veriT_vr60 veriT_vr62) :named @p_391)) :rule refl)
(step t133.t2 (cl (= @p_363 (! (member$ veriT_vr62 one_chain_typeII$) :named @p_390))) :rule cong :premises (t133.t1))
(step t133.t3 (cl @p_391) :rule refl)
(step t133.t4 (cl (= @p_365 (! (case_prod$ uua$ veriT_vr62) :named @p_392))) :rule cong :premises (t133.t3))
(step t133.t5 (cl (= @p_367 (! (=> @p_390 @p_392) :named @p_393))) :rule cong :premises (t133.t2 t133.t4))
(step t133 (cl (= @p_374 (! (forall ((veriT_vr62 Int_real_real_real_prod_fun_prod$)) @p_393) :named @p_398))) :rule bind)
(anchor :step t134 :args ((:= veriT_vr61 veriT_vr63)))
(step t134.t1 (cl (! (= veriT_vr61 veriT_vr63) :named @p_395)) :rule refl)
(step t134.t2 (cl (= @p_383 (! (member$ veriT_vr63 one_chain_typeI$) :named @p_394))) :rule cong :premises (t134.t1))
(step t134.t3 (cl @p_395) :rule refl)
(step t134.t4 (cl (= @p_385 (! (case_prod$ uua$ veriT_vr63) :named @p_396))) :rule cong :premises (t134.t3))
(step t134.t5 (cl (= @p_386 (! (=> @p_394 @p_396) :named @p_397))) :rule cong :premises (t134.t2 t134.t4))
(step t134 (cl (= @p_387 (! (forall ((veriT_vr63 Int_real_real_real_prod_fun_prod$)) @p_397) :named @p_399))) :rule bind)
(step t135 (cl (! (= @p_389 (! (and @p_377 @p_398 @p_399) :named @p_401)) :named @p_400)) :rule cong :premises (t133 t134))
(step t136 (cl (not @p_400) (not @p_389) @p_401) :rule equiv_pos2)
(step t137 (cl @p_401) :rule th_resolution :premises (t132 t135 t136))
(step t138 (cl @p_358) :rule and :premises (t119))
(step t139 (cl @p_399) :rule and :premises (t137))
(step t140 (cl (or (! (not @p_399) :named @p_422) (! (=> @p_402 (! (case_prod$ uua$ @p_403) :named @p_421)) :named @p_420))) :rule forall_inst :args ((:= veriT_vr63 @p_403)))
(step t141 (cl (or (! (not @p_358) :named @p_427) (! (=> @p_402 (! (case_prod$ uu$ @p_403) :named @p_426)) :named @p_424))) :rule forall_inst :args ((:= veriT_vr58 @p_403)))
(step t142 (cl (or (! (not @p_321) :named @p_406) (! (=> (! (and (! (finite$ @p_5) :named @p_415) (! (fun_app$a @p_12 g$) :named @p_409) (! (fun_app$a @p_24 g$) :named @p_408) (! (= @p_5 (! (sup$ @p_7 @p_5) :named @p_466)) :named @p_430) (! (= bot$ (inf$ @p_7 @p_5)) :named @p_431)) :named @p_429) (! (= @p_404 (! (+ @p_405 @p_404) :named @p_528)) :named @p_433)) :named @p_432))) :rule forall_inst :args ((:= veriT_vr51 @p_5) (:= veriT_vr52 f$) (:= veriT_vr53 @p_7) (:= veriT_vr54 g$) (:= veriT_vr55 @p_5)))
(step t143 (cl (or @p_406 (! (=> (! (and (! (finite$ @p_407) :named @p_412) @p_408 @p_409 (! (= @p_407 (sup$ @p_5 @p_7)) :named @p_411) (! (= bot$ (inf$ @p_5 @p_7)) :named @p_437)) :named @p_434) @p_410) :named @p_438))) :rule forall_inst :args ((:= veriT_vr51 @p_407) (:= veriT_vr52 f$) (:= veriT_vr53 @p_5) (:= veriT_vr54 g$) (:= veriT_vr55 @p_7)))
(step t144 (cl (or (! (not @p_249) :named @p_441) @p_411)) :rule forall_inst :args ((:= veriT_vr44 i$) (:= veriT_vr45 @p_7)))
(step t145 (cl (or (! (not @p_230) :named @p_442) (! (= @p_407 (! (insert$ j$ @p_5) :named @p_467)) :named @p_443))) :rule forall_inst :args ((:= veriT_vr39 j$) (:= veriT_vr40 i$) (:= veriT_vr41 bot$)))
(step t146 (cl (or (! (not @p_194) :named @p_447) (! (=> (! (member$a i$ @p_7) :named @p_445) (! (= @p_7 @p_407) :named @p_446)) :named @p_444))) :rule forall_inst :args ((:= veriT_vr32 i$) (:= veriT_vr33 @p_7)))
(step t147 (cl (or (! (not @p_174) :named @p_413) (! (=> (! (finite$ @p_7) :named @p_416) @p_412) :named @p_448))) :rule forall_inst :args ((:= veriT_vr28 @p_7) (:= veriT_vr29 i$)))
(step t148 (cl (or @p_413 (! (=> @p_414 @p_415) :named @p_449))) :rule forall_inst :args ((:= veriT_vr28 bot$) (:= veriT_vr29 i$)))
(step t149 (cl (or @p_413 (! (=> @p_414 @p_416) :named @p_451))) :rule forall_inst :args ((:= veriT_vr28 bot$) (:= veriT_vr29 j$)))
(step t150 (cl (or (! (not @p_119) :named @p_418) (! (= 0.0 (! (snd$a @p_417) :named @p_495)) :named @p_454))) :rule forall_inst :args ((:= veriT_vr18 1.0) (:= veriT_vr19 0.0)))
(step t151 (cl (or @p_418 (! (= 1.0 (! (snd$a @p_419) :named @p_496)) :named @p_455))) :rule forall_inst :args ((:= veriT_vr18 0.0) (:= veriT_vr19 1.0)))
(step t152 (cl (or (! (not @p_100) :named @p_456) (! (= g$ (! (snd$ @p_403) :named @p_471)) :named @p_457))) :rule forall_inst :args ((:= veriT_vr14 k$) (:= veriT_vr15 g$)))
(step t153 (cl (or (! (not @p_84) :named @p_461) (! (=> (! (= @p_7 @p_5) :named @p_459) (! (= j$ i$) :named @p_460)) :named @p_458))) :rule forall_inst :args ((:= veriT_vr10 i$) (:= veriT_vr11 j$)))
(step t154 (cl (! (not @p_420) :named @p_423) (! (not @p_402) :named @p_425) @p_421) :rule implies_pos)
(step t155 (cl @p_422 @p_420) :rule or :premises (t140))
(step t156 (cl @p_423 @p_421) :rule resolution :premises (t154 a6))
(step t157 (cl @p_420) :rule resolution :premises (t155 t139))
(step t158 (cl @p_421) :rule resolution :premises (t156 t157))
(step t159 (cl (! (not @p_424) :named @p_428) @p_425 @p_426) :rule implies_pos)
(step t160 (cl @p_427 @p_424) :rule or :premises (t141))
(step t161 (cl @p_428 @p_426) :rule resolution :premises (t159 a6))
(step t162 (cl @p_424) :rule resolution :premises (t160 t138))
(step t163 (cl @p_426) :rule resolution :premises (t161 t162))
(step t164 (cl @p_429 (not @p_415) (! (not @p_409) :named @p_436) (! (not @p_408) :named @p_435) (not @p_430) (not @p_431)) :rule and_neg)
(step t165 (cl (not @p_432) (not @p_429) @p_433) :rule implies_pos)
(step t166 (cl @p_406 @p_432) :rule or :premises (t142))
(step t167 (cl @p_432) :rule resolution :premises (t166 t101))
(step t168 (cl @p_434 (not @p_412) @p_435 @p_436 (not @p_411) (! (not @p_437) :named @p_515)) :rule and_neg)
(step t169 (cl (! (not @p_438) :named @p_439) (! (not @p_434) :named @p_440) @p_410) :rule implies_pos)
(step t170 (cl @p_406 @p_438) :rule or :premises (t143))
(step t171 (cl @p_439 @p_440) :rule resolution :premises (t169 a19))
(step t172 (cl @p_438) :rule resolution :premises (t170 t101))
(step t173 (cl @p_440) :rule resolution :premises (t171 t172))
(step t174 (cl @p_441 @p_411) :rule or :premises (t144))
(step t175 (cl @p_411) :rule resolution :premises (t174 t92))
(step t176 (cl @p_442 @p_443) :rule or :premises (t145))
(step t177 (cl @p_443) :rule resolution :premises (t176 t86))
(step t178 (cl (not @p_444) (! (not @p_445) :named @p_470) @p_446) :rule implies_pos)
(step t179 (cl @p_447 @p_444) :rule or :premises (t146))
(step t180 (cl @p_444) :rule resolution :premises (t179 t74))
(step t181 (cl (not @p_448) (not @p_416) @p_412) :rule implies_pos)
(step t182 (cl @p_413 @p_448) :rule or :premises (t147))
(step t183 (cl @p_448) :rule resolution :premises (t182 t68))
(step t184 (cl (! (not @p_449) :named @p_450) (! (not @p_414) :named @p_452) @p_415) :rule implies_pos)
(step t185 (cl @p_413 @p_449) :rule or :premises (t148))
(step t186 (cl @p_450 @p_415) :rule resolution :premises (t184 a8))
(step t187 (cl @p_449) :rule resolution :premises (t185 t68))
(step t188 (cl @p_415) :rule resolution :premises (t186 t187))
(step t189 (cl (! (not @p_451) :named @p_453) @p_452 @p_416) :rule implies_pos)
(step t190 (cl @p_413 @p_451) :rule or :premises (t149))
(step t191 (cl @p_453 @p_416) :rule resolution :premises (t189 a8))
(step t192 (cl @p_451) :rule resolution :premises (t190 t68))
(step t193 (cl @p_416) :rule resolution :premises (t191 t192))
(step t194 (cl @p_412) :rule resolution :premises (t181 t193 t183))
(step t195 (cl @p_418 @p_454) :rule or :premises (t150))
(step t196 (cl @p_454) :rule resolution :premises (t195 t56))
(step t197 (cl @p_418 @p_455) :rule or :premises (t151))
(step t198 (cl @p_455) :rule resolution :premises (t197 t56))
(step t199 (cl @p_456 @p_457) :rule or :premises (t152))
(step t200 (cl @p_457) :rule resolution :premises (t199 t50))
(step t201 (cl (not @p_458) (! (not @p_459) :named @p_507) @p_460) :rule implies_pos)
(step t202 (cl @p_461 @p_458) :rule or :premises (t153))
(step t203 (cl @p_458) :rule resolution :premises (t202 t44))
(step t204 (cl (or @p_410 (! (not (! (<= @p_462 @p_463) :named @p_534)) :named @p_464) (! (not (! (<= @p_463 @p_462) :named @p_535)) :named @p_465))) :rule la_disequality)
(step t205 (cl @p_410 @p_464 @p_465) :rule or :premises (t204))
(step t206 (cl @p_464 @p_465) :rule resolution :premises (t205 a19))
(step t207 (cl (or @p_441 (! (= @p_466 @p_467) :named @p_474))) :rule forall_inst :args ((:= veriT_vr44 j$) (:= veriT_vr45 @p_5)))
(step t208 (cl (or @p_447 (! (=> (! (member$a j$ @p_5) :named @p_468) (! (= @p_5 @p_467) :named @p_477)) :named @p_475))) :rule forall_inst :args ((:= veriT_vr32 j$) (:= veriT_vr33 @p_5)))
--> --------------------

--> maximum size reached

--> --------------------