An O(n3) on line algorithm for 2-satisfiability