| author | haftmann |
| Mon, 04 Jan 2010 14:09:56 +0100 | |
| changeset 34244 | 03f8dcab55f3 |
| parent 33010 | 39f73a59e855 |
| permissions | -rw-r--r-- |
#2 := false decl up_1 :: bool #4 := up_1 #5 := (not up_1) #6 := (or up_1 #5) #7 := (not #6) #31 := (iff #7 false) #1 := true #26 := (not true) #29 := (iff #26 false) #30 := [rewrite]: #29 #27 := (iff #7 #26) #24 := (iff #6 true) #25 := [rewrite]: #24 #28 := [monotonicity #25]: #27 #32 := [trans #28 #30]: #31 #23 := [asserted]: #7 [mp #23 #32]: false unsat