src/HOL/Multivariate_Analysis/Integration.certs

 #425 := [unit-resolution #424 #319 #414 #321 #421]: #379
 #426 := [unit-resolution #383 #425]: #378
 #427 := [unit-resolution #411 #426]: #395
 [th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
 unsat
-02d40f3e43c6a17458cd5dc30adbe4da03d87a0c 57 0
+abf6187dd71c2713828c15119491112c5b865e88 57 0
 #2 := false
 #41 := 0::Real
 decl f12 :: (-> S5 Real)
 decl f13 :: (-> S4 S4 S5)
 decl f14 :: (-> S3 S4)

 #139 := (forall (vars (?v0 S4) (?v1 S4)) #137)
 #245 := (iff #139 #242)
 #243 := (iff #137 #137)
 #244 := [refl]: #243
 #246 := [quant-intro #244]: #245
-#146 := (~ #139 #139)
-#148 := (~ #137 #137)
-#145 := [refl]: #148
-#143 := [nnf-pos #145]: #146
+#155 := (~ #139 #139)
+#143 := (~ #137 #137)
+#144 := [refl]: #143
+#156 := [nnf-pos #144]: #155
 #47 := (<= 0::Real #46)
 #48 := (forall (vars (?v0 S4) (?v1 S4)) #47)
 #140 := (iff #48 #139)
 #136 := (iff #47 #137)
 #138 := [rewrite]: #136
 #141 := [quant-intro #138]: #140
 #133 := [asserted]: #48
 #142 := [mp #133 #141]: #139
-#144 := [mp~ #142 #143]: #139
-#247 := [mp #144 #246]: #242
+#157 := [mp~ #142 #156]: #139
+#247 := [mp #157 #246]: #242
 #251 := (not #242)
 #252 := (or #251 #248)
 #253 := [quant-inst #37 #38]: #252
 [unit-resolution #253 #247 #258]: false
 unsat