#txn1 = (f, 1).(r11,3).(w11,infty).txn1; #lockmgr1 = (r11, infty).lockmgr1_1; #lockmgr1_1 = (w11, 5).lockmgr1; #lockmgr2 = (r12, infty).lockmgr2_1; #lockmgr2_1 = (w12, 6).lockmgr2; (txn1) (lockmgr1 <> lockmgr2)